[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 175 from proof inv-link (previous step)

# links(entries[str], dirs0) = files[entries[str]].nlink, # links(ino1, dirs0) = dirs0[ino1].nlink, entries[str] = dirs0[ino].entries[str], dirs0[ino1] = mkdir(dirs0[ino1].size, md, dirs0[ino1].nlink, dirs0[ino1].nsubdirs, entries1), files[entries[str]] = mkfile(m1, md2, files[entries[str]].nlink, content0), dirs0[ino0] = mkdir(m0, md0, # links(ino0, dirs0), m3, entries0), entries0[str] = entries[str], dirs0[ino2] = mkdir(m2, md1, # links(ino2, dirs0), m6, entries), dirs = dirs0[ino1, (dirs0[ino1].entries:= dirs0[ino1].entries[p.last, entries[str]]).size:= (dirs0[ino1].size + 1)], p ≠ ε, afs-cons(dirs0, files), ispath(q, ROOT_INO, ino0, dirs0, files), ispath(parent(p), ROOT_INO, ino1, dirs0, files), of-cons(of, dirs0, files), pw(user, md), px(user, md0), px(user, md), px-parent(user, q, ROOT_INO, dirs0, files), px-parent(user, parent(p), ROOT_INO, dirs0, files), str ∈ dirs0[ino].entries, ino ∈ dirs0, str ∈ entries0, entries[str] ∈ files, ino0 ∈ dirs0, ino1 ∈ dirs0, ino2 ∈ dirs0, str ∈ entries, ¬ p.last ∈ dirs0[ino1].entries, ¬ p.last ∈ entries1, ¬ entries[str] ∈ dirs0, links(ino, dirs0) ≠ ∅ ∨ ino = ROOT_INO, links(ino0, dirs0) ≠ ∅ ∨ ino0 = ROOT_INO, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO, links(ino2, dirs0) ≠ ∅ ∨ ino2 = ROOT_INO ⊦ [afs_inc_nlink#(mkdentry(str, entries0[str]).ino; dirs, files); new_dent := mkdentry(p.last, mkdentry(str, entries0[str]).ino); afs_inode_sync#(mkinode(ino1, md, true, dirs0[ino1].nlink, dirs0[ino1].nsubdirs, dirs0[ino1].size); dirs, files); afs_inode_sync#(mkinode(entries[str], md2, false, # links(entries[str], dirs0), 0, m1); dirs, files); new_inode := (ino1 ∈ dirs ⊃ mkinode(ino1, dirs[ino1].meta, true, dirs[ino1].nlink, dirs[ino1].nsubdirs, dirs[ino1].size) ;mkinode(ino1, files[ino1].meta, false, files[ino1].nlink, 0, files[ino1].size) ); c_inode := getinode(mkdentry(str, entries0[str]).ino, dirs, files); err := ESUCCESS; asynced := ?] (afs-cons(dirs, files) → of-cons(of, dirs, files))

Heuristic elimination applied rule insert elim lemma

And obtained the following new goals

Proof step 176:
# links(ino1, dirs0) = dirs0[ino1].nlink, # links(entries[str], dirs0) = m4, dirs0[ino2] = mkdir(m2, md1, # links(ino2, dirs0), m6, entries), entries0[str] = entries[str], dirs0[ino0] = mkdir(m0, md0, # links(ino0, dirs0), m3, entries0), files[entries[str]] = mkfile(m1, md2, m4, content0), dirs0[ino1] = mkdir(dirs0[ino1].size, md, dirs0[ino1].nlink, dirs0[ino1].nsubdirs, entries1), entries[str] = dirs0[ino].entries[str], files[entries[str]] = mkfile(m, md3, m4, content), dirs = dirs0[ino1, (dirs0[ino1].entries:= dirs0[ino1].entries[p.last, entries[str]]).size:= (dirs0[ino1].size + 1)], afs-cons(dirs0, files), ispath(parent(p), ROOT_INO, ino1, dirs0, files), ispath(q, ROOT_INO, ino0, dirs0, files), of-cons(of, dirs0, files), pw(user, md), px(user, md), px(user, md0), px-parent(user, parent(p), ROOT_INO, dirs0, files), px-parent(user, q, ROOT_INO, dirs0, files), str ∈ entries, ino2 ∈ dirs0, ino1 ∈ dirs0, ino0 ∈ dirs0, entries[str] ∈ files, str ∈ entries0, ino ∈ dirs0, str ∈ dirs0[ino].entries, links(ino2, dirs0) ≠ ∅ ∨ ino2 = ROOT_INO, links(ino1, dirs0) ≠ ∅ ∨ ino1 = ROOT_INO, links(ino0, dirs0) ≠ ∅ ∨ ino0 = ROOT_INO, links(ino, dirs0) ≠ ∅ ∨ ino = ROOT_INO ⊦ [afs_inc_nlink#(mkdentry(str, entries0[str]).ino; dirs, files); new_dent := mkdentry(p.last, mkdentry(str, entries0[str]).ino); afs_inode_sync#(mkinode(ino1, md, true, dirs0[ino1].nlink, dirs0[ino1].nsubdirs, dirs0[ino1].size); dirs, files); afs_inode_sync#(mkinode(entries[str], md2, false, # links(entries[str], dirs0), 0, m1); dirs, files); new_inode := (ino1 ∈ dirs ⊃ mkinode(ino1, dirs[ino1].meta, true, dirs[ino1].nlink, dirs[ino1].nsubdirs, dirs[ino1].size) ;mkinode(ino1, files[ino1].meta, false, files[ino1].nlink, 0, files[ino1].size) ); c_inode := getinode(mkdentry(str, entries0[str]).ino, dirs, files); err := ESUCCESS; asynced := ?] (afs-cons(dirs, files) → of-cons(of, dirs, files)), p = ε, p.last ∈ dirs0[ino1].entries, p.last ∈ entries1, entries[str] ∈ dirs0

Rule argument

spec: abstract-file name: elim seq: ⊦ ((m = af.size ∧ md = af.meta) ∧ m0 = af.nlink) ∧ content = af.content ↔ af = mkfile(m, md, m0, content) subst: [af, m, md, m0, content] → [files[entries[str]], m, md3, m4, content]

Additional information

Used simplifier rules: ⊦ ((m = af.size ∧ md = af.meta) ∧ m0 = af.nlink) ∧ content = af.content ↔ af = mkfile(m, md, m0, content); (elim) Used terms: files[entries[str]], m, md3, m4, content