| (ino2 ∈ dirs ⊃ mkinode(ino2, dirs[ino2].meta, true, dirs[ino2].nlink, dirs[ino2].nsubdirs, dirs[ino2].size) ;mkinode(ino2, files[ino2].meta, false, files[ino2].nlink, 0, files[ino2].size) ) = mkinode(m, md1, boolvar, m0, m1, m2), root[path].dir? ↔ ino2 ∈ dirs, err0 = EACCESS, ino = ino3, ino0 = ino4, md = md0, root.dir?, dom of < ino6, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), ispath(path, ROOT_INO, ino2, dirs, files), of-cons(of, dirs, files), px-parent(user, path, ROOT_INO, dirs, files), psynced → asynced, ino2 ∈ dirs ∨ ino2 ∈ files ⊦ ⟨skip⟩ ((psynced → asynced) ∧ md0 = md ∧ ino4 = ino0 ∧ ino3 = ino ∧ EACCESS = err0), pr(user, md1) |