| # links(m5, dirs0) = 0, # entries0 = m + 1, (entries0[str] ∈ dirs ⊃ mkinode(entries0[str], dirs[entries0[str]].meta, true, dirs[entries0[str]].nlink, dirs[entries0[str]].nsubdirs, dirs[entries0[str]].size) ;mkinode(entries0[str], files[entries0[str]].meta, false, files[entries0[str]].nlink, 0, files[entries0[str]].size) ) = mkinode(m5, md3, false, 0, 0, m8), dirs1[entries0[str]] = mkdir(m0, md0, m1, m4, entries), dirs0[entries0[str]] = mkdir(0, md, # links(entries0[str], dirs0), m3, ∅), dirs0[ino1] = mkdir(m + 1, md2, # links(ino1, dirs0), m2, entries0), root[q + str '] = dnode(md1, ∅), files[m5] = mkfile(m6, md4, 0, content), 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)(dirs0), afs-cons(dirs, files -- m5), afs-cons(dirs0, files), fids-cons(root, abs-files(files), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs0, files), of-cons(of, dirs0, files), of-cons(of, dirs, files -- m5), pw(user, md2), px(user, md2), px-parent(user, q, ROOT_INO, dirs0, files), str ∈ entries0, ino1 ∈ dirs0, entries0[str] ∈ dirs0, entries0[str] ∈ dirs1, m5 ∈ files, dirs1 ≡ dirs0[ino1, mkdir(m, md2, # links(ino1, dirs0), m2 - 1, entries0 -- str)], dirs ≡ dirs1[entries0[str], mkdir(m0, md, m1 - 1, m4, entries)], 1 ≤ m1, 1 ≤ m2, psynced → asynced0 ⊦ ∃ err. pre-rmdir(path, err, user, root, fs, ofh) ∧ ⟨err0 := err; if err0 = ESUCCESS then root := root -- path; psynced := ?⟩ (abs-files(files) = abs-files(files -- entries0[str]) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ ESUCCESS = err0), # links(ino1, dirs0) = 0, entries0 = ∅, ino1 = ROOT_INO, links(ino1, dirs0) = ∅, m1 = 0, m2 = 0, m5 = ROOT_INO, is-open(m5, of), m5 ∈ dirs, ino1 ∈ dirs1, ino1 ∈ dirs, m5 ∈ dirs0, m5 ∈ dirs1 |
# entries0 = m + 1, # links(m5, dirs0) = 0, (entries0[str] ∈ dirs ⊃ mkinode(entries0[str], dirs[entries0[str]].meta, true, dirs[entries0[str]].nlink, dirs[entries0[str]].nsubdirs, dirs[entries0[str]].size) ;mkinode(entries0[str], files[entries0[str]].meta, false, files[entries0[str]].nlink, 0, files[entries0[str]].size) ) = mkinode(m5, md3, false, 0, 0, m8), files[m5] = mkfile(m6, md4, 0, content), root[q + str '] = dnode(md1, ∅), dirs0[ino1] = mkdir(m + 1, md2, # links(ino1, dirs0), m2, entries0), dirs0[entries0[str]] = mkdir(0, md, # links(entries0[str], dirs0), m3, ∅), dirs1[entries0[str]] = mkdir(m0, md0, m1, m4, entries), # links(ino1, dirs0) ≠ 0, entries0 ≠ ∅, ino1 ≠ ROOT_INO, links(ino1, dirs0) ≠ ∅, m1 ≠ 0, m2 ≠ 0, m5 ≠ ROOT_INO, root[q].dir?, root.dir?, dom of < ino0, abs(root, ROOT_INO)(dirs0), afs-cons(dirs0, files), afs-cons(dirs, files -- m5), fids-cons(root, abs-files(files), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs0, files), of-cons(of, dirs, files -- m5), of-cons(of, dirs0, files), pw(user, md2), px(user, md2), px-parent(user, q, ROOT_INO, dirs0, files), m5 ∈ files, entries0[str] ∈ dirs1, entries0[str] ∈ dirs0, ino1 ∈ dirs0, str ∈ entries0, dirs ≡ dirs1[entries0[str], mkdir(m0, md, m1 - 1, m4, entries)], dirs1 ≡ dirs0[ino1, mkdir(m, md2, # links(ino1, dirs0), m2 - 1, entries0 -- str)], 1 ≤ m2, 1 ≤ m1, ¬ is-open(m5, of), ¬ m5 ∈ dirs1, ¬ m5 ∈ dirs0, ¬ ino1 ∈ dirs, ¬ ino1 ∈ dirs1, ¬ m5 ∈ dirs, psynced → asynced0 ⊦ ∃ err. pre-rmdir(q + str ', err, user, root, abs-files(files), abs-of(of)) ∧ ⟨err0 := err; if err0 = ESUCCESS then root := root -- (q + str '); psynced := ?⟩ (abs-files(files) = abs-files(files -- entries0[str]) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ ESUCCESS = err0)