Proof step 1373 from proof inv-renam (previous step)

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 1374:

  dirs[ino] = mkdir(m, md, # links(ino, dirs), m2, entries), dirs[ino1] = mkdir(m0, md0, # links(ino1, dirs), m3, entries0), err = ESUCCESS, err = err0, err1 = ESUCCESS, dom of < ino2, afs-cons(dirs, files), ispath(q0, ROOT_INO, ino, dirs, files), ispath(q, ROOT_INO, ino1, dirs, files), of-cons(of, dirs, files), pw(user, md), pw(user, md0), px(user, md), px(user, md0), px-parent(user, q0, ROOT_INO, dirs, files), px-parent(user, q, ROOT_INO, dirs, files), ino1 ∈ dirs, entries0[str] ∈ files, ino ∈ dirs, str ∈ entries0, ⌊err0⌋ ∨ err0 = ESUCCESS, links(ino, dirs) ≠ ∅ ∨ ino = ROOT_INO, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ ⟪let dent = negdentry(str0) in {old_inode := (ino1 ∈ dirs ⊃ mkinode(ino1, md0, true, # links(ino1, dirs), m3, m0) ;mkinode(ino1, files[ino1].meta, false, files[ino1].nlink, 0, files[ino1].size) ); old_dent := mkdentry(str, entries0[str]); old_dent_inode := getinode(mkdentry(str, entries0[str]).ino, dirs, files); new_inode := (ino ∈ dirs ⊃ mkinode(ino, dirs[ino].meta, true, dirs[ino].nlink, dirs[ino].nsubdirs, dirs[ino].size) ;mkinode(ino, files[ino].meta, false, files[ino].nlink, 0, files[ino].size) ); new_dent := negdentry(str0); new_dent_inode := getinode(mkdentry(str, entries0[str]).ino, dirs, files); afs_rename#(; old_inode, new_inode, old_dent_inode, new_dent_inode, old_dent, new_dent, err, dirs, files; asynced); if dent.dentry? then vfs_put_inode#(new_dent_inode, of, asynced; err, dirs, files)}⟫ (of-cons(of, dirs, files) ∧ afs-cons(dirs, files)), entries0[str] ∈ dirs, str0 ∈ entries, q + str ' ⊑ q0 + str0 '

• Proof step 1492:

  dirs[ino] = mkdir(m, md, # links(ino, dirs), m2, entries), dirs[ino1] = mkdir(m0, md0, # links(ino1, dirs), m3, entries0), err = err0, err1 = ESUCCESS, dom of < ino2, afs-cons(dirs, files), ispath(q0, ROOT_INO, ino, dirs, files), ispath(q, ROOT_INO, ino1, dirs, files), of-cons(of, dirs, files), pw(user, md), pw(user, md0), px(user, md), px(user, md0), px-parent(user, q0, ROOT_INO, dirs, files), px-parent(user, q, ROOT_INO, dirs, files), ino1 ∈ dirs, entries0[str] ∈ files, ino ∈ dirs, str ∈ entries0, ⌊err0⌋ ∨ err0 = ESUCCESS, links(ino, dirs) ≠ ∅ ∨ ino = ROOT_INO, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ ⟪skip⟫ (of-cons(of, dirs, files) ∧ afs-cons(dirs, files)), err = ESUCCESS, entries0[str] ∈ dirs, str0 ∈ entries, q + str ' ⊑ q0 + str0 '

Rule argument

Additional information