| files[entries[str]] = mkfile(m, md2, # links(entries[str], dirs), content0), dirs[ino1] = mkdir(m1, md, # links(ino1, dirs), m4, entries), dirs[ino] = mkdir(m0, md1, # links(ino, dirs), m2, entries1), err = ESUCCESS, new_child_inode = new_dent_inode, new_dent = negdentry(str0), new_dent_inode = mkinode(entries[str], md2, false, # links(entries[str], dirs), 0, m), new_inode = mkinode(ino, md1, true, # links(ino, dirs), m2, m0), new_parent_inode = new_inode, old_child_inode = old_dent_inode, old_dent = mkdentry(str, entries[str]), old_dent_inode = mkinode(entries[str], md2, false, # links(entries[str], dirs), 0, m), old_inode = mkinode(ino1, md, true, # links(ino1, dirs), m4, m1), old_parent_inode = old_inode, dom of < ino2, afs-cons(dirs, files), ispath(q, ROOT_INO, ino1, dirs, files), ispath(q0, ROOT_INO, ino, dirs, files), of-cons(of, dirs, files), pw(user, md), pw(user, md1), px(user, md), px(user, md1), px-parent(user, q, ROOT_INO, dirs, files), px-parent(user, q0, ROOT_INO, dirs, files), ino ∈ dirs, entries[str] ∈ files, ino1 ∈ dirs, str ∈ entries, ino = ino1 → md1 = md, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO, links(ino, dirs) ≠ ∅ ∨ ino = ROOT_INO ⊦ [abort] (afs-cons(dirs, files) → ⟪skip⟫ of-cons(of, dirs, files)), pre-rename(old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, new_child_inode, dirs, files), str0 ∈ entries1, entries[str] ∈ dirs, q + str ' ⊑ q0 + str0 ' |