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

fs0[ri[inodekey(m)]] = inodenode(key, md0, false, m0, 0, m3), 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, 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), abs-files(fs0, ri)[m, mkfile(m2, md, m0, abs-content(m, fs0, ri))] = abs-files(fs0[adr1, inodenode(inodekey(m), md, false, m0, 0, m2)], ri[inodekey(m), adr1]), m = 0, adr1 ∈ fs0

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 126:
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), ( inodekey(ino) ∈ ri ∧ ¬ 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) ∧ ( inodekey(ino) ∈ ri ∧ ¬ 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])))

Rule argument

Additional information

Used simplifier rules: at-ri: ⊦ ri[key, adr][key0] = (key = key0 ⊃ adr;ri[key0]);%⊦ abs-file(ino, fs, ri) = mkfile (fs[ri[inodekey(ino)]].size, fs[ri[inodekey(ino)]].meta, fs[ri[inodekey(ino)]].nlink, abs-content(ino, fs, ri)); (s)%⊦ inodekey(ino) ∈ ri ∧ ¬ fs[ri[inodekey(ino)]].directory → abs-files(fs, ri)[ino] = abs-file(ino, fs, ri); (s)% ⊦ files[ino, af][ino0] = (ino0 = ino ∧ ino ∈ files ⊃ af;files[ino0]); (s)% ⊦ fs[adr0, nd][adr1] = (adr0 = adr1 ⊃ nd;fs[adr1]); (s)% ⊦ inodekey(m) = inodekey(m0) ↔ m = m0; (s)%⊦ ino ∈ abs-files(fs, ri) ↔ inodekey(ino) ∈ ri ∧ ¬ fs[ri[inodekey(ino)]].directory; (s)% ⊦ ino ∈ files[ino0, af] ↔ ino ∈ files; (s)%⊦ files = abs-files(fs, ri) ↔ (∀ ino. ( ino ∈ files ↔ inodekey(ino) ∈ ri ∧ ¬ fs[ri[inodekey(ino)]].directory) ∧ (ino ∈ files → files[ino] = abs-file(ino, fs, ri))); (ss)