[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 387 from proof refine-link (previous step)

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), root.dir?, root[q].dir?, root[q0].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(q0, ROOT_INO, ino2, dirs0, files0), ispath(q, ROOT_INO, ino1, 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, md0), px(user, md), px-parent(user, q0, ROOT_INO, dirs0, files0), px-parent(user, q, ROOT_INO, dirs0, files0), entries[str] ∈ files0, str ∈ entries0, ino1 ∈ dirs0, ino2 ∈ dirs0, ino3 ∈ dirs0, str ∈ entries, dirs ≡ dirs0[ino2, mkdir(# entries1 + 1, md, # links(ino2, dirs0), m3, entries1[str0, entries[str]])], psynced → asynced0, links(ino3, dirs0) ≠ ∅ ∨ ino3 = ROOT_INO, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ ( ispath(q + str ', ROOT_INO, dirs0, files0) ∧ ¬ root[q + str '].dir? ∧ ¬ ispath(q0 + str0 ', ROOT_INO, dirs0, files0) ∧ parent(q0 + str0 ') ∈ root ∧ root[parent(q0 + str0 ')].dir? ∧ px(user, parent(q + str '), root, abs-files(files0)) ∧ py(user, parent(q0 + str0 '), root, abs-files(files0))) ∧ ⟨err0 := ESUCCESS; if err0 = ESUCCESS then let fid = root[q + str '].fid in root[q0 + str0 '] := 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), # links(ino2, dirs0) = 0, ino2 = ROOT_INO, links(ino2, dirs0) = ∅, root[q + str '].dir?, str0 ∈ entries1, entries[str] ∈ dirs0, entries[str] ∈ dirs, ino2 ∈ dirs

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 388:
⊦ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) → (p ∈ tree ↔ ispath(p, ino, dirs, files))
Proof step 389:
⊦ ispath(p, ino, m, dirs, files) ∧ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) → (px(user, p, tree, abs-files(files)) ↔ px(user, p, ino, dirs, files))
Proof step 390:
⊦ ispath(p, ino, m, dirs, files) ∧ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) → (py(user, p, tree, abs-files(files)) ↔ py(user, p, ino, dirs, files))
Proof step 391:
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), # links(ino2, dirs0) ≠ 0, ino2 ≠ ROOT_INO, links(ino2, dirs0) ≠ ∅, root.dir?, root[q].dir?, root[q0].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(q0, ROOT_INO, ino2, dirs0, files0), ispath(q, ROOT_INO, ino1, 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, md0), px(user, md), px-parent(user, q0, ROOT_INO, dirs0, files0), px-parent(user, q, ROOT_INO, dirs0, files0), entries[str] ∈ files0, str ∈ entries0, ino1 ∈ dirs0, ino2 ∈ dirs0, ino3 ∈ dirs0, str ∈ entries, dirs ≡ dirs0[ino2, mkdir(# entries1 + 1, md, # links(ino2, dirs0), m3, entries1[str0, entries[str]])], ¬ root[q + str '].dir?, ¬ str0 ∈ entries1, ¬ entries[str] ∈ dirs0, ¬ entries[str] ∈ dirs, ¬ ino2 ∈ dirs, psynced → asynced0, links(ino3, dirs0) ≠ ∅ ∨ ino3 = ROOT_INO, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ (entries0[str] ∈ dirs0 ∨ entries0[str] ∈ files0) ∧ px(user, q, ROOT_INO, dirs0, files0) ∧ py(user, q0, ROOT_INO, dirs0, files0) ∧ ⟨err0 := ESUCCESS; if err0 = ESUCCESS then let fid = root[q + str '].fid in root[q0 + str0 '] := 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)

Rule argument

Additional information

Used simplifier rules: path-in-eq: ⊦ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) → (p ∈ tree ↔ ispath(p, ino, dirs, files));%px: ⊦ ispath(p, ino, m, dirs, files) ∧ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) → ( px(user, p, tree, abs-files(files)) ↔ px(user, p, ino, dirs, files));%py: ⊦ ispath(p, ino, m, dirs, files) ∧ abs(tree, ino)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) → ( py(user, p, tree, abs-files(files)) ↔ py(user, p, ino, dirs, files));% ⊦ mkdir(m, md, m0, m1, entries).entries = entries; (s)% ⊦ ispath(p, n, m, dirs, files) → ispath(p, n, dirs, files); (s)% ⊦ parent(p + str ') = p; (s)%a: ⊦ (p + p0) + p1 = p + p0 + p1; from specification list[path]%⊦ ispath(str ', n, dirs, files) ↔ n ∈ dirs ∧ str ∈ dirs[n].entries ∧ (dirs[n].entries[str] ∈ dirs ∨ dirs[n].entries[str] ∈ files); (s)%⊦ ispath(p, n, m, dirs, files) → (ispath(p + q, n, dirs, files) ↔ ispath(q, m, dirs, files)); (s)