Proof step 14 from proof inv-rmdir (previous step)

Heuristic conditional right split applied rule or split right

And obtained the following new goals

• Proof step 15:

  dirs[m] = mkdir(m1, md2, # links(m, dirs), m4, entries), dirs[entries[str]] = mkdir(m0, md1, # links(entries[str], dirs), m2, ∅), c_inode = mkinode(entries[str], md, true, # links(entries[str], dirs), m2, m0), dent = mkdentry(str, entries[str]), p_inode = mkinode(m, md0, true, # links(m, dirs), m4, m1), afs-cons(dirs, files), pre-rmdir(p_inode, c_inode, dent, dirs, files), m ∈ dirs, str ∈ entries, entries[str] ∈ dirs, links(m, dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ ⟪let p_ino = p_inode.ino in {dirs[p_ino].entries := dirs[p_ino].entries -- dent.name; dirs[p_ino].size := dirs[p_ino].size - 1; dirs[p_ino].nsubdirs := dirs[p_ino].nsubdirs - 1; let ino = dent.ino in afs_drop_nlink#(ino; dirs, files); dent := negdentry(dent.name); afs_inode_sync#(p_inode; dirs, files); afs_inode_sync#(c_inode; dirs, files); p_inode := getinode(p_inode.ino, dirs, files); c_inode := getinode(c_inode.ino, dirs, files); err := ESUCCESS}; asynced := ?⟫ afs-cons(dirs, files), entries[str] = ROOT_INO

• Proof step 136:

  dirs[m] = mkdir(m1, md2, # links(m, dirs), m4, entries), dirs[entries[str]] = mkdir(m0, md1, # links(entries[str], dirs), m2, ∅), c_inode = mkinode(entries[str], md, true, # links(entries[str], dirs), m2, m0), dent = mkdentry(str, entries[str]), p_inode = mkinode(m, md0, true, # links(m, dirs), m4, m1), afs-cons(dirs, files), pre-rmdir(p_inode, c_inode, dent, dirs, files), m ∈ dirs, str ∈ entries, entries[str] ∈ dirs, links(m, dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ ⟪fail#(; ; err); asynced := ?⟫ afs-cons(dirs, files), entries[str] = ROOT_INO

Rule argument

Additional information