| dirs[ino1] = mkdir(m, md, # links(ino1, dirs), m4, entries1), files[entries[str]] = mkfile(m1, md2, # links(entries[str], dirs), content0), dirs[ino0] = mkdir(m0, md0, # links(ino0, dirs), m3, entries0), entries0[str] = entries[str], dirs[ino] = mkdir(m2, md1, # links(ino, dirs), m6, entries), c_inode = mkinode(entries[str], md2, false, # links(entries[str], dirs), 0, m1), err = err0, err0 = ESUCCESS, new_dent = negdentry(p.last), new_inode = mkinode(ino1, md, true, # links(ino1, dirs), m4, m), old_dent = mkdentry(str, entries0[str]), p_inode = new_inode, afs-cons(dirs, files), ispath(q, ROOT_INO, ino0, dirs, files), ispath(parent(p), ROOT_INO, ino1, dirs, files), of-cons(of, dirs, files), pw(user, md), px(user, md0), px(user, md), px-parent(user, q, ROOT_INO, dirs, files), px-parent(user, parent(p), ROOT_INO, dirs, files), str ∈ entries0, entries[str] ∈ files, ino0 ∈ dirs, ino1 ∈ dirs, ino ∈ dirs, str ∈ entries, links(ino0, dirs) ≠ ∅ ∨ ino0 = ROOT_INO, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO, links(ino, dirs) ≠ ∅ ∨ ino = ROOT_INO ⊦ [abort] (afs-cons(dirs, files) → of-cons(of, dirs, files)), p = ε, pre-link(p_inode, c_inode, old_dent, new_dent, dirs, files), p.last ∈ entries1, entries[str] ∈ dirs |