| # entries0 = m + 1, dirs2[m5].nlink = 0, (entries0[str] ∈ dirs2 ⊃ mkinode(entries0[str], dirs2[entries0[str]].meta, true, dirs2[entries0[str]].nlink, dirs2[entries0[str]].nsubdirs, dirs2[entries0[str]].size) ;mkinode(entries0[str], files[entries0[str]].meta, false, files[entries0[str]].nlink, 0, files[entries0[str]].size) ) = mkinode(m5, md3, boolvar, m6, m7, m8), 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), files[m5] = mkfile(m9, md4, m10, content), root[q].dir?, root.dir?, dom of < ino0, abs(root, ROOT_INO)(dirs0), afs-cons(dirs0, files), afs-cons(dirs, 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), pw(user, md2), px(user, md2), px-parent(user, q, ROOT_INO, dirs0, files), entries0[str] ∈ dirs1, entries0[str] ∈ dirs0, ino1 ∈ dirs0, str ∈ entries0, m5 ∈ dirs2, dirs ≡ dirs2 -- m5, dirs2 ≡ 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, psynced → asynced0, m6 = 0 ∧ m8 = dirs2[m5].size ∧ m7 = dirs2[m5].nsubdirs ∧ boolvar ∨ m5 ∈ files ∧ m6 = m10 ∧ m7 = 0 ∧ ¬ boolvar, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ ⟨posix_rmdir#(q + str ', user, abs-files(files), abs-of(of); err1, root; psynced)⟩ (abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ ESUCCESS = err1), entries0 = ∅, m1 = 0, m2 = 0, m5 = ROOT_INO, is-open(m5, of), ino1 ∈ dirs2, ino1 ∈ dirs1 |
# entries0 = m + 1, dirs2[m5].nlink = 0, (entries0[str] ∈ dirs2 ⊃ mkinode(entries0[str], dirs2[entries0[str]].meta, true, dirs2[entries0[str]].nlink, dirs2[entries0[str]].nsubdirs, dirs2[entries0[str]].size) ;mkinode(entries0[str], files[entries0[str]].meta, false, files[entries0[str]].nlink, 0, files[entries0[str]].size) ) = mkinode(m5, md3, boolvar, m6, m7, m8), files[m5] = mkfile(m9, md4, m10, content), 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, ∅), entries0 ≠ ∅, m1 ≠ 0, m2 ≠ 0, m5 ≠ ROOT_INO, root.dir?, root[q].dir?, dom of < ino0, abs(root, ROOT_INO)(dirs0), afs-cons(dirs, files), afs-cons(dirs0, files), fids-cons(root, abs-files(files), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs0, files), of-cons(of, dirs, files), of-cons(of, dirs0, files), pw(user, md2), px(user, md2), px-parent(user, q, ROOT_INO, dirs0, files), m5 ∈ dirs2, str ∈ entries0, ino1 ∈ dirs0, entries0[str] ∈ dirs0, entries0[str] ∈ dirs1, dirs1 ≡ dirs0[ino1, mkdir(m, md2, # links(ino1, dirs0), m2 - 1, entries0 -- str)], dirs2 ≡ dirs1[entries0[str], mkdir(m0, md, m1 - 1, m4, entries)], dirs ≡ dirs2 -- m5, 1 ≤ m1, 1 ≤ m2, ¬ is-open(m5, of), ¬ ino1 ∈ dirs1, ¬ ino1 ∈ dirs2, psynced → asynced0, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO, m6 = 0 ∧ m8 = dirs2[m5].size ∧ m7 = dirs2[m5].nsubdirs ∧ boolvar ∨ m5 ∈ files ∧ m6 = m10 ∧ m7 = 0 ∧ ¬ boolvar ⊦ ⟨posix_rmdir#(q + str ', user, abs-files(files), abs-of(of); err1, root; psynced)⟩ (abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ ESUCCESS = err1)