| # links(entries0[str], dirs0) = m + 1, # entries0 = m0 + 1, dirs0[ino1] = mkdir(m0 + 1, md0, # links(ino1, dirs0), m3, entries0), files0[entries0[str]] = mkfile(m1, md1, m + 1, content0), files = files0[entries0[str], mkfile(m1, md1, m, content0)], ino = inode.ino, inode = mkinode(entries0[str], md1, false, # links(entries0[str], dirs0), 0, m1), root.dir?, root[q].dir?, dom of < ino0, abs(root, ROOT_INO)(dirs0), afs-cons(dirs0, files0), fids-cons(root, abs-files(files0), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs0, files0), of-cons(of, dirs0, files0), pw(user, md0), px(user, md0), px-parent(user, q, ROOT_INO, dirs0, files0), ino ∈ dirs1, str ∈ entries0, entries0[str] ∈ files0, ino1 ∈ dirs0, dirs ≡ dirs1[ino, dirs1[ino].meta:= inode.meta], dirs1 ≡ dirs0[ino1, mkdir(m0, md0, # links(ino1, dirs0), m3, entries0 -- str)], psynced → asynced0, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ [c_inode := getinode(entries0[str], dirs, files); err := ESUCCESS; asynced := ?; vfs_put_inode#(c_inode, of, asynced; err, dirs, files)] ( of-cons(of, dirs, files) ∧ afs-cons(dirs, files) → ⟨fs := abs-files(files0); posix_unlink#(q + str ', user, abs-of(of); err1, root, fs; psynced)⟩ (fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ err = err1)), entries0 = ∅, root[q + str '].dir?, ino ∈ files, entries0[str] ∈ dirs0 |
Used simplifier rules: ⊦ mkinode(m, md, boolvar, m0, m1, m2).ino = m; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).meta = md; (s)% ⊦ ino ∈ files[ino0, af] ↔ ino ∈ files; (s)%⊦ ino ∈ dirs ∧ dirs[ino] = mkdir(n0, md, n, n1, entries) ∧ str ∈ entries ∧ afs-cons(dirs, files) → (entries[str] ∈ files ↔ ¬ entries[str] ∈ dirs); (ss)