[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 131 from proof refine-write-inode (previous step)

fs0[ri[inodekey(m)]] = inodenode(key, md0, false, m0, 0, m3), inodekey(ino) = inodekey(m), orphans(fs0, ri).inodes?, fo.inodes?, afs-cons(abs-dirs(fs0, ri), abs-files(fs0, ri)), afs-cons(abs-dirs(fs0, ri), abs-files(fs0, ri)[m, mkfile(m2, md, m0, abs-content(m, fs0, ri))]), file-node-cons(fs0, ri), log-cons(log0, fs0), orphans-cons(fs0, ri, orphans(fs0, ri)), replay-cons-strong(fs0, ri, orphans(fs0, ri), fi, fo, log0), ri-cons(ri, fs0), ri-inj(ri), ri-inj(fi), ubifs-cons(fs0, ri, orphans(fs0, ri), fi, fo, log0), inodekey(m) ∈ ri, ri[inodekey(m)] ∈ fs0, inodekey(ino) ∈ ri, asynced0 → boolvar1 ⊦ ∃ err0. ⌊err0⌋ ∧ ⟨err := err0; asynced0 := ?⟩ ( abs-dirs(fs0, ri) = abs-dirs(fs0[adr1, inodenode(inodekey(m), md, false, m0, 0, m2)], ri[inodekey(m), adr1]) ∧ abs-files(fs0, ri) = abs-files(fs0[adr1, inodenode(inodekey(m), md, false, m0, 0, m2)], ri[inodekey(m), adr1]) ∧ orphans(fs0[adr1, inodenode(inodekey(m), md, false, m0, 0, m2)], ri[inodekey(m), adr1]) = orphans(fs0, ri) ∧ (asynced0 → boolvar) ∧ ESUCCESS = err), m = 0, adr1 ∈ fs0, ( ¬ fs0[ri[inodekey(ino)]].directory ↔ inodekey(ino) ∈ ri[inodekey(m), adr1] ∧ ¬ (adr1 = (m = ino ⊃ adr1;ri[inodekey(ino)]) ⊃ inodenode(inodekey(m), md, false, m0, 0, m2);fs0[(m = ino ⊃ adr1;ri[inodekey(ino)])]).directory) ∧ ( ¬ fs0[ri[inodekey(ino)]].directory → (ino = m ⊃ mkfile(m2, md, m0, abs-content(m, fs0, ri)) ;mkfile(fs0[ri[inodekey(ino)]].size, fs0[ri[inodekey(ino)]].meta, fs0[ri[inodekey(ino)]].nlink, abs-content(ino, fs0, ri)) ) = mkfile ((adr1 = (m = ino ⊃ adr1;ri[inodekey(ino)]) ⊃ inodenode(inodekey(m), md, false, m0, 0, m2);fs0[(m = ino ⊃ adr1;ri[inodekey(ino)])]).size, (adr1 = (m = ino ⊃ adr1;ri[inodekey(ino)]) ⊃ inodenode(inodekey(m), md, false, m0, 0, m2);fs0[(m = ino ⊃ adr1;ri[inodekey(ino)])]).meta, (adr1 = (m = ino ⊃ adr1;ri[inodekey(ino)]) ⊃ inodenode(inodekey(m), md, false, m0, 0, m2);fs0[(m = ino ⊃ adr1;ri[inodekey(ino)])]).nlink, abs-content(ino, fs0[adr1, inodenode(inodekey(m), md, false, m0, 0, m2)], ri[inodekey(m), adr1])))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 132:
fs0[ri[inodekey(m)]] = inodenode(key, md0, false, m0, 0, m3), m ≠ 0, fo.inodes?, orphans(fs0, ri).inodes?, afs-cons(abs-dirs(fs0, ri), abs-files(fs0, ri)[m, mkfile(m2, md, m0, abs-content(m, fs0, ri))]), afs-cons(abs-dirs(fs0, ri), abs-files(fs0, ri)), file-node-cons(fs0, ri), log-cons(log0, fs0), orphans-cons(fs0, ri, orphans(fs0, ri)), replay-cons-strong(fs0, ri, orphans(fs0, ri), fi, fo, log0), ri-cons(ri, fs0), ri-inj(fi), ri-inj(ri), ubifs-cons(fs0, ri, orphans(fs0, ri), fi, fo, log0), ri[inodekey(m)] ∈ fs0, inodekey(m) ∈ ri, ¬ adr1 ∈ fs0, asynced0 → boolvar1 ⊦ ∃ err0. ⌊err0⌋ ∧ ⟨err := err0; asynced0 := ?⟩ ( abs-dirs(fs0, ri) = abs-dirs(fs0[adr1, inodenode(inodekey(m), md, false, m0, 0, m2)], ri[inodekey(m), adr1]) ∧ abs-files(fs0, ri) = abs-files(fs0[adr1, inodenode(inodekey(m), md, false, m0, 0, m2)], ri[inodekey(m), adr1]) ∧ orphans(fs0[adr1, inodenode(inodekey(m), md, false, m0, 0, m2)], ri[inodekey(m), adr1]) = orphans(fs0, ri) ∧ (asynced0 → boolvar) ∧ ESUCCESS = err), (datakey(m, n) ∈ ri → datakey(m, n) ∈ ri[inodekey(m), adr1]) ∧ ( datakey(m, n) ∈ ri[inodekey(m), adr1] → (adr1 = ri[datakey(m, n)] ⊃ inodenode(inodekey(m), md, false, m0, 0, m2);fs0[ri[datakey(m, n)]]).data = fs0[ri[datakey(m, n)]].data)

Rule argument

Additional information

Used simplifier rules: at-ri: ⊦ ri[key, adr][key0] = (key = key0 ⊃ adr;ri[key0]);% ⊦ fs[adr0, nd][adr1] = (adr0 = adr1 ⊃ nd;fs[adr1]); (s)%⊦ datakey(ino, n) ∈ ri → abs-content(ino, fs, ri)[n] = fs[ri[datakey(ino, n)]].data; (s)% ⊦ inodekey(m) ≠ datakey(m0, m1); (s)% ⊦ key ∈ ri[key0, adr] ↔ key = key0 ∨ key ∈ ri; (ws)% ⊦ n ∈ abs-content(ino, fs, ri) ↔ datakey(ino, n) ∈ ri; (s)%⊦ content = abs-content(ino, fs, ri) ↔ (∀ n. (n ∈ content ↔ datakey(ino, n) ∈ ri) ∧ (n ∈ content → content[n] = fs[ri[datakey(ino, n)]].data)); (ss)%⊦ mkfile(m0, md0, n0, content0) = mkfile(m1, md1, n1, content1) ↔ ¬(n0 ≠ n1 ∨ md0 ≠ md1 ∨ m0 ≠ m1 ∨ content0 ≠ content1); (ss)% ⊦ key ∈ ri[key, adr]; (s)% ⊦ inodenode(key, md, boolvar, m, m0, m1).nlink = m; (s)% ⊦ inodenode(key, md, boolvar, m, m0, m1).meta = md; (s)% ⊦ inodenode(key, md, boolvar, m, m0, m1).size = m1; (s)% ⊦ inodenode(key, md, boolvar, m, m0, m1).directory ↔ boolvar; (s)% ⊦ inodekey(m) = inodekey(m0) ↔ m = m0; (s)