Proof step 321 from proof refine-unlink (previous step)

User applied rule if right

And obtained the following new goals

• Proof step 322:

  ⟨vfs_put_inode#(getinode(entries0[str], dirs1, files), of, asynced; err0, dirs, files)⟩ (err0 = ESUCCESS ∧ dirs = dirs1 ∧ files = files1), # entries0 = m0 + 1, # links(entries0[str], dirs0) = m + 1, files0[entries0[str]] = mkfile(m1, md1, m + 1, content0), dirs0[ino1] = mkdir(m0 + 1, md0, # links(ino1, dirs0), m3, entries0), dirs = dirs1, err0 = ESUCCESS, files = files0[entries0[str], mkfile(m1, md1, m, content0)], fs = abs-files(files0), root0.dir?, root0[q].dir?, dom of < ino0, abs(root0, ROOT_INO)(dirs0), afs-cons(dirs1, files1), afs-cons(dirs0, files0), fids-cons(root0, abs-files(files0), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs0, files0), of-cons(of, dirs1, files1), of-cons(of, dirs0, files0), pw(user, md0), px(user, md0), px-parent(user, q, ROOT_INO, dirs0, files0), entries0[str] ∈ files0, ino1 ∈ dirs0, str ∈ entries0, dirs1 ≡ dirs0[ino1, mkdir(m0, md0, # links(ino1, dirs0), m3, entries0 -- str)], ¬ is-open(entries0[str], of) → str ∈ entries0, psynced → asynced0, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ ⟨fs := fs -- ⌜entries0[str]⌝ ⟩ true, entries0 = ∅, root0[q + str '].dir?, is-open(entries0[str], of), entries0[str] ∈ dirs1, entries0[str] ∈ dirs0, ⌜entries0[str]⌝ ∈ (root0 -- (q + str ')).fids

• Proof step 323:

  ⟨vfs_put_inode#(getinode(entries0[str], dirs1, files), of, asynced; err0, dirs, files)⟩ (err0 = ESUCCESS ∧ dirs = dirs1 ∧ files = files1), # entries0 = m0 + 1, # links(entries0[str], dirs0) = m + 1, files0[entries0[str]] = mkfile(m1, md1, m + 1, content0), dirs0[ino1] = mkdir(m0 + 1, md0, # links(ino1, dirs0), m3, entries0), dirs = dirs1, err0 = ESUCCESS, files = files0[entries0[str], mkfile(m1, md1, m, content0)], fs = abs-files(files0), root0.dir?, root0[q].dir?, dom of < ino0, abs(root0, ROOT_INO)(dirs0), afs-cons(dirs1, files1), afs-cons(dirs0, files0), fids-cons(root0, abs-files(files0), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs0, files0), of-cons(of, dirs1, files1), of-cons(of, dirs0, files0), pw(user, md0), px(user, md0), px-parent(user, q, ROOT_INO, dirs0, files0), entries0[str] ∈ files0, ino1 ∈ dirs0, str ∈ entries0, dirs1 ≡ dirs0[ino1, mkdir(m0, md0, # links(ino1, dirs0), m3, entries0 -- str)], ¬ is-open(entries0[str], of) → str ∈ entries0, psynced → asynced0, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ ⟨skip⟩ true, entries0 = ∅, root0[q + str '].dir?, entries0[str] ∈ dirs1, entries0[str] ∈ dirs0, ¬ is-open(entries0[str], of) ∧ ¬ ⌜entries0[str]⌝ ∈ (root0 -- (q + str ')).fids

• Proof step 324:

  ⟨vfs_put_inode#(getinode(entries0[str], dirs1, files), of, asynced; err0, dirs, files)⟩ (err0 = ESUCCESS ∧ dirs = dirs1 ∧ files = files1), # entries0 = m0 + 1, # links(entries0[str], dirs0) = m + 1, files0[entries0[str]] = mkfile(m1, md1, m + 1, content0), dirs0[ino1] = mkdir(m0 + 1, md0, # links(ino1, dirs0), m3, entries0), dirs = dirs1, err0 = ESUCCESS, files = files0[entries0[str], mkfile(m1, md1, m, content0)], fs = abs-files(files0), root0.dir?, root0[q].dir?, dom of < ino0, abs(root0, ROOT_INO)(dirs0), afs-cons(dirs1, files1), afs-cons(dirs0, files0), fids-cons(root0, abs-files(files0), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs0, files0), of-cons(of, dirs1, files1), of-cons(of, dirs0, files0), pw(user, md0), px(user, md0), px-parent(user, q, ROOT_INO, dirs0, files0), entries0[str] ∈ files0, ino1 ∈ dirs0, str ∈ entries0, dirs1 ≡ dirs0[ino1, mkdir(m0, md0, # links(ino1, dirs0), m3, entries0 -- str)], psynced → asynced0, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ entries0 = ∅, root0[q + str '].dir?, entries0[str] ∈ dirs1, entries0[str] ∈ dirs0, str ∈ entries0 ∧ (¬ is-open(entries0[str], of) → str ∈ entries0)

Rule argument

Additional information