[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 376 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), files = files0[entries[str], mkfile(m0, md2, # links(entries[str], dirs0) + 1, content0)], ino = inode.ino, inode = mkinode(entries0[str], md2, false, # links(entries0[str], dirs0), 0, m0), mkdentry(str, entries0[str]).dentry?, root.dir?, root[q].dir?, root[q0].dir?, dom of < ino0, abs(root, ROOT_INO)(dirs0), afs-cons(dirs, files[ino, files[ino].size:= inode.size][ino, files[ino, files[ino].size:= inode.size][ino].meta:= inode.meta]), 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, dirs, files[ino, files[ino].size:= inode.size][ino, files[ino, files[ino].size:= inode.size][ino].meta:= inode.meta]), 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), ino ∈ files, str ∈ entries0, entries[str] ∈ files0, 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(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO, links(ino2, dirs0) ≠ ∅ ∨ ino2 = ROOT_INO, links(ino3, dirs0) ≠ ∅ ∨ ino3 = ROOT_INO ⊦ ⟨posix_link#(q + str ', q0 + str0 ', user, abs-files(files0), abs-of(of); err2, root; psynced)⟩ ( abs-files(files0) = abs-files(files[ino, files[ino].size:= inode.size][ino, files[ino, files[ino].size:= inode.size][ino].meta:= inode.meta]) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ ESUCCESS = err2), 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 377:
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), # links(ino2, dirs0) ≠ 0, ino2 ≠ ROOT_INO, links(ino2, dirs0) ≠ ∅, root[q0].dir?, root[q].dir?, root.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(q, ROOT_INO, ino1, dirs0, files0), ispath(q0, ROOT_INO, ino2, 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, md), px(user, md0), px-parent(user, q, ROOT_INO, dirs0, files0), px-parent(user, q0, ROOT_INO, dirs0, files0), str ∈ entries, ino3 ∈ dirs0, ino2 ∈ dirs0, ino1 ∈ dirs0, str ∈ entries0, entries[str] ∈ files0, dirs ≡ dirs0[ino2, mkdir(# entries1 + 1, md, # links(ino2, dirs0), m3, entries1[str0, entries[str]])], ¬ root[q + str '].dir?, ¬ ino2 ∈ dirs, ¬ entries[str] ∈ dirs, ¬ entries[str] ∈ dirs0, ¬ str0 ∈ entries1, psynced → asynced0, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO, links(ino3, dirs0) ≠ ∅ ∨ ino3 = ROOT_INO ⊦ ⟨posix_link#(q + str ', q0 + str0 ', user, abs-files(files0), abs-of(of); err2, root; 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 = err2)

Rule argument

Additional information

Used simplifier rules: size-zero: ⊦ # ls ≠ 0 → ls ≠ ∅; (forward) from specification set-basic[alink-set]%size-zero-01: ⊦ ls ≠ ∅ → # ls ≠ 0; (forward) from specification set-basic[alink-set]% ⊦ afs-cons(dirs, files) → ROOT_INO ∈ dirs; (ss)% ⊦ mkdentry(str, m).dentry?; (s)% ⊦ files[ino, af][ino, af0] = files[ino, af0]; (s)% ⊦ mkfile(m, md, m0, content).meta:= md0 = mkfile(m, md0, m0, content); (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).meta = md; (s)% ⊦ mkfile(m, md, m0, content).size:= m1 = mkfile(m1, md, m0, content); (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).size = m2; (s)% ⊦ files[ino, af][ino0] = (ino0 = ino ∧ ino ∈ files ⊃ af;files[ino0]); (s)% ⊦ ino ∈ files[ino0, af] ↔ ino ∈ files; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).ino = m; (s)