| entries[str] ∈ dirs ↔ root[q + str '].dir?, dirs[ino1] = mkdir(# entries, md, # links(ino1, dirs), m1, entries), err0 = err2, fs = abs-files(files), ofh = abs-of(of), path = q + str ', root.dir?, root[q].dir?, dom of < ino0, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs, files), of-cons(of, dirs, files), pw(user, md), px(user, md), px-parent(user, q, ROOT_INO, dirs, files), str ∈ entries, ino1 ∈ dirs, ⌊err⌋ , psynced → asynced, entries[str] ∈ dirs ∨ entries[str] ∈ files, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ ⟨choose err with pre-unlink(path, err, user, root, fs, ofh) in err0 := err; if err0 = ESUCCESS then let fid = root[path].fid in {root := root -- path; if ¬ fid ∈ ofh.fids ∧ ¬ fid ∈ root.fids then fs := fs -- fid}; psynced := ?⟩ (fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ err = err0) |
entries[str] ∈ dirs ↔ root[q + str '].dir?, dirs[ino1] = mkdir(# entries, md, # links(ino1, dirs), m1, entries), err0 = err2, fs = abs-files(files), ofh = abs-of(of), path = q + str ', root[q].dir?, root.dir?, dom of < ino0, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs, files), of-cons(of, dirs, files), pw(user, md), px(user, md), px-parent(user, q, ROOT_INO, dirs, files), ino1 ∈ dirs, str ∈ entries, ⌊err1⌋ , psynced → asynced, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO, entries[str] ∈ dirs ∨ entries[str] ∈ files ⊦ ∃ err. pre-unlink(path, err, user, root, fs, ofh) ∧ ⟨err0 := err; if err0 = ESUCCESS then let fid = root[path].fid in {root := root -- path; if ¬ fid ∈ ofh.fids ∧ ¬ fid ∈ root.fids then fs := fs -- fid}; psynced := ?⟩ (fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ err1 = err0)