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

fs1[ri1[inodekey(m)]].directory, fs1[ri1[inodekey(m)]].inode?, fo.inodes?, ro.inodes?, file-node-cons(fs1, ri1), log-cons(log0, fs1), orphans-cons(fs1, ri1, ro), replay-cons-strong(fs1, ri1, ro, fi, fo, log0), ri-inj(fi), ri-inj(ri1), ubifs-cons(fs1, ri1, ro, fi, fo, log0), ri1[inodekey(m)] ∈ fs1, inodekey(m) ∈ ri1, fs1[ri1[inodekey(m)]].nlink ≠ 0 ∨ m = ROOT_INO ⊦ adr1 = adr3, adr1 = adr2, adr2 = adr3, n = 0, replay-cons-strong (fs1[adr1, inodenode(inodekey(m), md0, true, fs1[ri1[inodekey(m)]].nlink, fs1[ri1[inodekey(m)]].nsubdirs, fs1[ri1[inodekey(m)]].size + 1)] [adr2, dentrynode(dentrykey(m, str), n) ] [adr3, inodenode(inodekey(n), md, false, 1, 0, 0) ], ri1[inodekey(m), adr1][dentrykey(m, str), adr2][inodekey(n), adr3], ro, fi, fo, ((log0 + adr1 ') + adr2 ') + adr3 '), inodekey(m) ∈ ro, dentrykey(m, str) ∈ ri1, inodekey(n) ∈ fo, inodekey(n) ∈ ri1, adr1 ∈ fs1, adr2 ∈ fs1, adr3 ∈ fs1

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 88:
nd.key = key ⊦ ¬ adr ∈ fs ∧ log-cons(log, fs) ∧ node-cons(key, nd) ∧ ri-cons(ri, fs) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) → (replay-cons-strong(fs[adr, nd], ri[key, adr], ro, fi, fo, log + adr ') ↔ replay-one(adr, nd, ri ⊖ ro) = ri[nd.key, adr] ⊖ ro)
Proof step 89:
fs1[ri1[inodekey(m)]].directory, fs1[ri1[inodekey(m)]].inode?, ro.inodes?, fo.inodes?, file-node-cons(fs1, ri1), log-cons(log0, fs1), orphans-cons(fs1, ri1, ro), replay-cons-strong(fs1, ri1, ro, fi, fo, log0), ri-inj(ri1), ri-inj(fi), ubifs-cons(fs1, ri1, ro, fi, fo, log0), inodekey(m) ∈ ri1, ri1[inodekey(m)] ∈ fs1, fs1[ri1[inodekey(m)]].nlink ≠ 0 ∨ m = ROOT_INO ⊦ adr1 = adr2, adr1 = adr3, adr2 = adr3, n = 0, replay-cons-strong (fs1[adr1, inodenode(inodekey(m), md0, true, fs1[ri1[inodekey(m)]].nlink, fs1[ri1[inodekey(m)]].nsubdirs, fs1[ri1[inodekey(m)]].size + 1)] [adr2, dentrynode(dentrykey(m, str), n) ] [adr3, inodenode(inodekey(n), md, false, 1, 0, 0) ], ri1[inodekey(m), adr1][dentrykey(m, str), adr2][inodekey(n), adr3], ro, fi, fo, ((log0 + adr1 ') + adr2 ') + adr3 '), adr3 ∈ fs1, adr2 ∈ fs1, adr1 ∈ fs1, inodekey(n) ∈ ri1, inodekey(n) ∈ fo, dentrykey(m, str) ∈ ri1, inodekey(m) ∈ ro, inodenode(inodekey(n), md, false, 1, 0, 0).key = inodekey(n) ∧ ¬ adr3 ∈ fs1[adr1, inodenode(inodekey(m), md0, true, fs1[ri1[inodekey(m)]].nlink, fs1[ri1[inodekey(m)]].nsubdirs, fs1[ri1[inodekey(m)]].size + 1)] [adr2, dentrynode(dentrykey(m, str), n) ] ∧ log-cons ((log0 + adr1 ') + adr2 ', fs1[adr1, inodenode(inodekey(m), md0, true, fs1[ri1[inodekey(m)]].nlink, fs1[ri1[inodekey(m)]].nsubdirs, fs1[ri1[inodekey(m)]].size + 1)] [adr2, dentrynode(dentrykey(m, str), n) ]) ∧ node-cons(inodekey(n), inodenode(inodekey(n), md, false, 1, 0, 0)) ∧ ri-cons (ri1[inodekey(m), adr1][dentrykey(m, str), adr2], fs1[adr1, inodenode(inodekey(m), md0, true, fs1[ri1[inodekey(m)]].nlink, fs1[ri1[inodekey(m)]].nsubdirs, fs1[ri1[inodekey(m)]].size + 1)] [adr2, dentrynode(dentrykey(m, str), n) ]) ∧ replay-cons-strong (fs1[adr1, inodenode(inodekey(m), md0, true, fs1[ri1[inodekey(m)]].nlink, fs1[ri1[inodekey(m)]].nsubdirs, fs1[ri1[inodekey(m)]].size + 1)] [adr2, dentrynode(dentrykey(m, str), n) ], ri1[inodekey(m), adr1][dentrykey(m, str), adr2], ro, fi, fo, (log0 + adr1 ') + adr2 ')
Proof step 108:
inodenode(inodekey(n), md, false, 1, 0, 0).key = inodekey(n), fs1[ri1[inodekey(m)]].directory, fs1[ri1[inodekey(m)]].inode?, ro.inodes?, fo.inodes?, file-node-cons(fs1, ri1), log-cons(log0, fs1), log-cons ((log0 + adr1 ') + adr2 ', fs1[adr1, inodenode(inodekey(m), md0, true, fs1[ri1[inodekey(m)]].nlink, fs1[ri1[inodekey(m)]].nsubdirs, fs1[ri1[inodekey(m)]].size + 1)] [adr2, dentrynode(dentrykey(m, str), n) ]), node-cons(inodekey(n), inodenode(inodekey(n), md, false, 1, 0, 0)), orphans-cons(fs1, ri1, ro), replay-cons-strong(fs1, ri1, ro, fi, fo, log0), replay-cons-strong (fs1[adr1, inodenode(inodekey(m), md0, true, fs1[ri1[inodekey(m)]].nlink, fs1[ri1[inodekey(m)]].nsubdirs, fs1[ri1[inodekey(m)]].size + 1)] [adr2, dentrynode(dentrykey(m, str), n) ], ri1[inodekey(m), adr1][dentrykey(m, str), adr2], ro, fi, fo, (log0 + adr1 ') + adr2 '), ri-cons (ri1[inodekey(m), adr1][dentrykey(m, str), adr2], fs1[adr1, inodenode(inodekey(m), md0, true, fs1[ri1[inodekey(m)]].nlink, fs1[ri1[inodekey(m)]].nsubdirs, fs1[ri1[inodekey(m)]].size + 1)] [adr2, dentrynode(dentrykey(m, str), n) ]), ri-inj(ri1), ri-inj(fi), ubifs-cons(fs1, ri1, ro, fi, fo, log0), inodekey(m) ∈ ri1, ri1[inodekey(m)] ∈ fs1, fs1[ri1[inodekey(m)]].nlink ≠ 0 ∨ m = ROOT_INO ⊦ adr1 = adr2, adr1 = adr3, adr2 = adr3, n = 0, replay-one(adr3, inodenode(inodekey(n), md, false, 1, 0, 0), ri1[inodekey(m), adr1][dentrykey(m, str), adr2] ⊖ ro) = ri1[inodekey(m), adr1][dentrykey(m, str), adr2][inodenode(inodekey(n), md, false, 1, 0, 0).key, adr3] ⊖ ro, adr3 ∈ fs1, adr2 ∈ fs1, adr1 ∈ fs1, inodekey(n) ∈ ri1, inodekey(n) ∈ fo, dentrykey(m, str) ∈ ri1, inodekey(m) ∈ ro, adr3 ∈ fs1[adr1, inodenode(inodekey(m), md0, true, fs1[ri1[inodekey(m)]].nlink, fs1[ri1[inodekey(m)]].nsubdirs, fs1[ri1[inodekey(m)]].size + 1)] [adr2, dentrynode(dentrykey(m, str), n) ]

Rule argument

spec: aubifs-replay name: replay-cons-strong-append seq: nd.key = key ⊦ ¬ adr ∈ fs ∧ log-cons(log, fs) ∧ node-cons(key, nd) ∧ ri-cons(ri, fs) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) → ( replay-cons-strong (fs[adr, nd], ri[key, adr], ro, fi, fo, log + adr ') ↔ replay-one(adr, nd, ri ⊖ ro) = ri[nd.key, adr] ⊖ ro) subst: [log, fo, fi, ro, key, ri, nd, adr, fs] → [(log0 + adr1 ') + adr2 ', fo, fi, ro, inodekey(n), ri1[inodekey(m), adr1][dentrykey(m, str), adr2], inodenode(inodekey(n), md, false, 1, 0, 0), adr3, fs1 [adr1, inodenode (inodekey(m), md0, true, fs1[ri1[inodekey(m)]].nlink, fs1[ri1[inodekey(m)]].nsubdirs, fs1[ri1[inodekey(m)]].size + 1) ] [adr2, dentrynode(dentrykey(m, str), n) ]] flags: <all paths>

Additional information

Used terms: (log0 + adr1 ') + adr2 ', fo, fi, ro, inodekey(n), ri1[inodekey(m), adr1][dentrykey(m, str), adr2], inodenode(inodekey(n), md, false, 1, 0, 0), adr3, fs1 [adr1, inodenode (inodekey(m), md0, true, fs1[ri1[inodekey(m)]].nlink, fs1[ri1[inodekey(m)]].nsubdirs, fs1[ri1[inodekey(m)]].size + 1) ] [adr2, dentrynode(dentrykey(m, str), n) ]