| root[path].dir? ↔ ino1 ∈ dirs, err = ESUCCESS, ino = ino1, root.dir?, dom of < ino0, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), ispath(path, ROOT_INO, ino1, dirs, files), of-cons(of, dirs, files), px-parent(user, path, ROOT_INO, dirs, files), psynced → asynced ⊦ [abort; if err = ESUCCESS then if inode.directory then err := (inode.directory ⊃ EISDIR;ENOTDIR) else if ¬ pr(user, inode.meta) then err := EACCESS; err1 := err; if err1 = ESUCCESS then afs_fsync#(inode, isdir0, dirs, files; ; asynced, err1); if err1 = ESUCCESS then afs_sync#(dirs, files; ; asynced, err1)] ⟨posix_fsync#(path, isdir0, user, root, abs-files(files), abs-of(of); ; psynced, err0)⟩ ((psynced → asynced) ∧ err1 = err0), pre-iget(ino, dirs, files) |