| dirs[entries0[str]] = mkdir(0, md, # links(entries0[str], dirs), m2, ∅), dirs[ino1] = mkdir(# entries0, md2, # links(ino1, dirs), m1, entries0), root[q + str '] = dnode(md1, ∅), 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, md2), px(user, md2), px-parent(user, q, ROOT_INO, dirs, files), str ∈ entries0, ino1 ∈ dirs, entries0[str] ∈ dirs, ⌊err⌋ , psynced → asynced0, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ ⟨choose err with pre-rmdir(path, err, user, root, fs, ofh) in err0 := err; if err0 = ESUCCESS then root := root -- path; psynced := ?⟩ (abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ err = err0) |
root[q + str '] = dnode(md1, ∅), dirs[ino1] = mkdir(# entries0, md2, # links(ino1, dirs), m1, entries0), dirs[entries0[str]] = mkdir(0, md, # links(entries0[str], dirs), m2, ∅), err0 = err1, 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, md2), px(user, md2), px-parent(user, q, ROOT_INO, dirs, files), entries0[str] ∈ dirs, ino1 ∈ dirs, str ∈ entries0, ⌊err2⌋ , psynced → asynced0, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ ∃ err. pre-rmdir(path, err, user, root, fs, ofh) ∧ ⟨err0 := err; if err0 = ESUCCESS then root := root -- path; psynced := ?⟩ (abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ err2 = err0)