| dirs0[ino2] = mkdir(# entries1, md, # links(ino2, dirs0), m3, entries1), files0[entries[str]] = mkfile(m0, md2, # links(entries[str], dirs0), content0), dirs0[ino1] = mkdir(# entries0, md0, # links(ino1, dirs0), m2, entries0), entries0[str] = entries[str], dirs0[ino3] = mkdir(# entries, md1, # links(ino3, dirs0), m4, entries), err0 = err2, fs = abs-files(files0), ofh = abs-of(of), path = q + str ', path' = q0 + str0 ', root.dir?, root[q].dir?, root[q0].dir?, dom of < ino0, abs(root, ROOT_INO)(dirs0), afs-cons(dirs0, files0), afs-cons(dirs, files0[entries[str], mkfile(m0, md2, # links(entries[str], dirs0) + 1, content0)]), fids-cons(root, abs-files(files0), abs-of(of)), ispath(q0, ROOT_INO, ino2, dirs0, files0), ispath(q, ROOT_INO, ino1, dirs0, files0), of-cons(of, dirs, files0[entries[str], mkfile(m0, md2, # links(entries[str], dirs0) + 1, content0)]), of-cons(of, dirs0, files0), pw(user, md), px(user, md0), px(user, md), px-parent(user, q0, ROOT_INO, dirs0, files0), px-parent(user, q, ROOT_INO, dirs0, files0), str ∈ entries0, entries[str] ∈ files0, ino1 ∈ dirs0, ino3 ∈ dirs0, str ∈ entries, ino2 ∈ dirs0, dirs ≡ dirs0[ino2, mkdir(# entries1 + 1, md, # links(ino2, dirs0), m3, entries1[str0, entries[str]])], psynced → asynced0, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO, links(ino2, dirs0) ≠ ∅ ∨ ino2 = ROOT_INO, links(ino3, dirs0) ≠ ∅ ∨ ino3 = ROOT_INO ⊦ ⟨choose err with pre-link(path, path', err, user, root, fs, ofh) in err0 := err; if err0 = ESUCCESS then let fid = root[path].fid in root[path'] := fnode(fid); psynced := ?⟩ ( abs-files(files0) = abs-files (files0[entries[str], mkfile(m0, md2, # links(entries[str], dirs0) + 1, content0)] [entries0[str], mkfile(m0, md2, # links(entries[str], dirs0) + 1, content0) ]) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ ESUCCESS = err0), root[q + str '].dir?, str0 ∈ entries1, entries[str] ∈ dirs0 |
dirs0[ino3] = mkdir(# entries, md1, # links(ino3, dirs0), m4, entries), entries0[str] = entries[str], dirs0[ino1] = mkdir(# entries0, md0, # links(ino1, dirs0), m2, entries0), files0[entries[str]] = mkfile(m0, md2, # links(entries[str], dirs0), content0), dirs0[ino2] = mkdir(# entries1, md, # links(ino2, dirs0), m3, entries1), err0 = err2, fs = abs-files(files0), ofh = abs-of(of), path = q + str ', path' = q0 + str0 ', root[q0].dir?, root[q].dir?, root.dir?, dom of < ino0, abs(root, ROOT_INO)(dirs0), afs-cons(dirs, files0[entries[str], mkfile(m0, md2, # links(entries[str], dirs0) + 1, content0)]), afs-cons(dirs0, files0), fids-cons(root, abs-files(files0), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs0, files0), ispath(q0, ROOT_INO, ino2, dirs0, files0), of-cons(of, dirs0, files0), of-cons(of, dirs, files0[entries[str], mkfile(m0, md2, # links(entries[str], dirs0) + 1, content0)]), pw(user, md), px(user, md), px(user, md0), px-parent(user, q, ROOT_INO, dirs0, files0), px-parent(user, q0, ROOT_INO, dirs0, files0), ino2 ∈ dirs0, str ∈ entries, ino3 ∈ dirs0, ino1 ∈ dirs0, entries[str] ∈ files0, str ∈ entries0, dirs ≡ dirs0[ino2, mkdir(# entries1 + 1, md, # links(ino2, dirs0), m3, entries1[str0, entries[str]])], psynced → asynced0, links(ino3, dirs0) ≠ ∅ ∨ ino3 = ROOT_INO, links(ino2, dirs0) ≠ ∅ ∨ ino2 = ROOT_INO, links(ino1, dirs0) ≠ ∅ ∨ 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-files(files0) = abs-files (files0[entries[str], mkfile(m0, md2, # links(entries[str], dirs0) + 1, content0)] [entries0[str], mkfile(m0, md2, # links(entries[str], dirs0) + 1, content0) ]) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ ESUCCESS = err0), root[q + str '].dir?, entries[str] ∈ dirs0, str0 ∈ entries1