| dirs[ino1] = mkdir(# entries0, md0, # links(ino1, dirs), m2, entries0), files[entries0[str]] = mkfile(m, md, # links(entries0[str], dirs), content), fs = abs-files(files), ofh = abs-of(of), path = q + str ', path' = q0 + str0 ', root[q].dir?, 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), ispath(q0, ROOT_INO, ino2, dirs, files), of-cons(of, dirs, files), px(user, md0), px-parent(user, q, ROOT_INO, dirs, files), px-parent(user, q0, ROOT_INO, dirs, files), ROOT_INO ∈ dirs, str ∈ entries0, ino1 ∈ dirs, entries0[str] ∈ files, ino2 ∈ files, psynced → asynced, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ ∃ err. pre-link(path, path', err, user, root, fs, ofh) ∧ ⟨err0 := err; if err0 = ESUCCESS then let fid = root[path].fid in root[path'] := fnode(fid); psynced := ?⟩ (abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ ENOTDIR = err0), root[q0].dir?, root[q + str '].dir?, ino2 ∈ dirs, entries0[str] ∈ dirs |
files[entries0[str]] = mkfile(m, md, # links(entries0[str], dirs), content), dirs[ino1] = mkdir(# entries0, md0, # links(ino1, dirs), m2, entries0), root.dir?, root[q].dir?, dom of < ino0, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), ispath(q0, ROOT_INO, ino2, dirs, files), ispath(q, ROOT_INO, ino1, dirs, files), of-cons(of, dirs, files), px(user, md0), px-parent(user, q0, ROOT_INO, dirs, files), px-parent(user, q, ROOT_INO, dirs, files), ino2 ∈ files, entries0[str] ∈ files, ino1 ∈ dirs, str ∈ entries0, ROOT_INO ∈ dirs, ¬ root[q + str '].dir?, ¬ root[q0].dir?, ¬ entries0[str] ∈ dirs, ¬ ino2 ∈ dirs, psynced → asynced, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ ∃ err. pre-link(q + str ', q0 + str0 ', err, user, root, abs-files(files), abs-of(of)) ∧ ⟨err0 := err; if err0 = ESUCCESS then let fid = root[q + str '].fid in root[q0 + str0 '] := fnode(fid); psynced := ?⟩ (abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ ENOTDIR = err0)