| isrename ↔ false, isdir ↔ isdir0, root[q].dir? ↔ ino1 ∈ dirs, dent = negdentry(str), err = ESUCCESS, ino = ino1, isdir0, 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), px-parent(user, q, ROOT_INO, dirs, files), psynced → asynced ⊦ [abort; if err = ESUCCESS then if ¬ inode.directory then err := ENOTDIR else if ¬ px(user, inode.meta) ∨ ¬ pw(user, inode.meta) then err := EACCESS else {afs_lookup#(ino, dirs, files, asynced; dent, err); if err = ESUCCESS then {afs_iget#(dent.ino, dirs, files, asynced; p_inode, err); if err = ESUCCESS then {isdir := p_inode.directory; if isdir then if p_inode.ino = ROOT_INO then err := EACCESS else if isrename ∧ ¬ pw(user, p_inode.meta) then err := EACCESS else if ¬ isrename ∧ p_inode.size ≠ 0 then err := ENOTEMPTY}}}; isdir1 := true; isdir0 := isdir; if isdir1 ∧ ¬ isdir0 then err := ENOTDIR; if ¬ isdir1 ∧ isdir0 then err := EISDIR; err1 := err; if err1 = ESUCCESS then afs_check_commit#(dirs, files; err1; asynced); fs := abs-files(files); if err1 = ESUCCESS then {afs_rmdir#(; inode, p_inode, dent, err1, dirs, files; asynced); vfs_put_inode#(p_inode, of, asynced; err1, dirs, files)}] ( of-cons(of, dirs, files) ∧ afs-cons(dirs, files) → ⟨posix_rmdir#(q + str ', user, fs, abs-of(of); err0, root; psynced)⟩ (fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ err1 = err0)), pre-iget(ino, dirs, files) |