| ⟨skip⟩ (ESUCCESS = err0 ∧ dirs = dirs1 ∧ files = files1), # entries0 = m0 + 1, # links(entries0[str], dirs0) = m + 1, files0[entries0[str]] = mkfile(m1, md1, m + 1, content0), dirs0[ino1] = mkdir(m0 + 1, md0, # links(ino1, dirs0), m3, entries0), err = ESUCCESS, files = files0[entries0[str], mkfile(m1, md1, m, content0)], fs = abs-files(files0), ino = inode.ino, inode = getinode(entries0[str], dirs, files), root[q].dir?, root.dir?, dom of < ino0, abs(root, ROOT_INO)(dirs0), afs-cons(dirs1, files1), afs-cons(dirs0, files0), fids-cons(root, abs-files(files0), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs0, files0), of-cons(of, dirs1, files1), of-cons(of, dirs0, files0), pre-evict(inode, dirs, files), pw(user, md0), px(user, md0), px-parent(user, q, ROOT_INO, dirs0, files0), ino ∈ dirs, str ∈ entries0, entries0[str] ∈ files0, ino1 ∈ dirs0, dirs ≡ dirs0[ino1, mkdir(m0, md0, # links(ino1, dirs0), m3, entries0 -- str)], psynced → asynced0, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ ⟨posix_unlink#(q + str ', user, abs-of(of); err1, root, fs; psynced)⟩ (fs = abs-files(files1) ∧ abs(root, ROOT_INO)(dirs1) ∧ (psynced → asynced) ∧ err0 = err1), dirs[ino].nlink = 0, dirs = dirs1, entries0 = ∅, root[q + str '].dir?, is-open ((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], md1, false, m, 0, m1) ) .ino, of), entries0[str] ∈ dirs0 |