| dirs[ino1] = mkdir(# entries, md, # links(ino1, dirs), m1, entries), err0 = err1, 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, entries[str] ∈ files, ⌊err2⌋ , psynced → asynced0, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ ∃ 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) ∧ err2 = err0), root[q + str '].dir?, entries[str] ∈ dirs |
dirs[ino1] = mkdir(# entries, md, # links(ino1, dirs), m1, entries), fs = abs-files(files), 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), entries[str] ∈ files, ino1 ∈ dirs, str ∈ entries, ⌊err2⌋ , ¬ root[q + str '].dir?, ¬ entries[str] ∈ dirs, psynced → asynced0, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ ∃ err. pre-unlink(q + str ', err, user, root, fs, abs-of(of)) ∧ ⟨err0 := err; if err0 = ESUCCESS then let fid = root[q + str '].fid in {root := root -- (q + str '); if ¬ fid ∈ abs-of(of).fids ∧ ¬ fid ∈ root.fids then fs := fs -- fid}; psynced := ?⟩ (fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ err2 = err0)