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

fs0[ri[inodekey(m)]] = inodenode(key, md0, true, m0, m1, m3), fo.inodes?, orphans(fs0, ri).inodes?, afs-cons(abs-dirs(fs0, ri)[m, abs-dirs(fs0, ri)[m].meta:= md], abs-files(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, asynced0 → boolvar1 ⊦ ∃ err0. ⌊err0⌋ ∧ ⟨err := err0; asynced0 := ?⟩ ( abs-dirs(fs0, ri) = abs-dirs(fs0[adr1, inodenode(inodekey(m), md, true, m0, m1, m3)], ri[inodekey(m), adr1]) ∧ abs-files(fs0, ri) = abs-files(fs0[adr1, inodenode(inodekey(m), md, true, m0, m1, m3)], ri[inodekey(m), adr1]) ∧ orphans(fs0[adr1, inodenode(inodekey(m), md, true, m0, m1, m3)], ri[inodekey(m), adr1]) = orphans(fs0, ri) ∧ (asynced0 → boolvar) ∧ ESUCCESS = err), abs-dirs(fs0, ri)[m, abs-dirs(fs0, ri)[m].meta:= md] = abs-dirs(fs0[adr1, inodenode(inodekey(m), md, true, m0, m1, m3)], ri[inodekey(m), adr1]), m = 0, adr1 ∈ fs0

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 49:
fs0[ri[inodekey(m)]] = inodenode(key, md0, true, m0, m1, m3), m ≠ 0, fo.inodes?, orphans(fs0, ri).inodes?, afs-cons(abs-dirs(fs0, ri)[m, abs-dirs(fs0, ri)[m].meta:= md], abs-files(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, true, m0, m1, m3)], ri[inodekey(m), adr1]) ∧ abs-files(fs0, ri) = abs-files(fs0[adr1, inodenode(inodekey(m), md, true, m0, m1, m3)], ri[inodekey(m), adr1]) ∧ orphans(fs0[adr1, inodenode(inodekey(m), md, true, m0, m1, m3)], 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, true, m0, m1, m3);fs0[(m = ino ⊃ adr1;ri[inodekey(ino)])]).directory) ∧ ( inodekey(ino) ∈ ri ∧ fs0[ri[inodekey(ino)]].directory → (ino = m ⊃ mkdir(m3, md, m0, m1, abs-children(m, fs0, ri)) ;mkdir (fs0[ri[inodekey(ino)]].size, fs0[ri[inodekey(ino)]].meta, fs0[ri[inodekey(ino)]].nlink, fs0[ri[inodekey(ino)]].nsubdirs, abs-children(ino, fs0, ri)) ) = mkdir ((adr1 = (m = ino ⊃ adr1;ri[inodekey(ino)]) ⊃ inodenode(inodekey(m), md, true, m0, m1, m3);fs0[(m = ino ⊃ adr1;ri[inodekey(ino)])]).size, (adr1 = (m = ino ⊃ adr1;ri[inodekey(ino)]) ⊃ inodenode(inodekey(m), md, true, m0, m1, m3);fs0[(m = ino ⊃ adr1;ri[inodekey(ino)])]).meta, (adr1 = (m = ino ⊃ adr1;ri[inodekey(ino)]) ⊃ inodenode(inodekey(m), md, true, m0, m1, m3);fs0[(m = ino ⊃ adr1;ri[inodekey(ino)])]).nlink, (adr1 = (m = ino ⊃ adr1;ri[inodekey(ino)]) ⊃ inodenode(inodekey(m), md, true, m0, m1, m3);fs0[(m = ino ⊃ adr1;ri[inodekey(ino)])]).nsubdirs, abs-children(ino, fs0[adr1, inodenode(inodekey(m), md, true, m0, m1, m3)], ri[inodekey(m), adr1])))

Rule argument

Additional information

Used simplifier rules: at-ri: ⊦ ri[key, adr][key0] = (key = key0 ⊃ adr;ri[key0]);% ⊦ inodenode(key, md, boolvar, m, m0, m1).nsubdirs = m0; (s)% ⊦ inodenode(key, md, boolvar, m, m0, m1).nlink = m; (s)% ⊦ inodenode(key, md, boolvar, m, m0, m1).size = m1; (s)%⊦ mkdir(m, md, m0, m1, entries).meta:= md0 = mkdir(m, md0, m0, m1, entries); (s)%⊦ abs-dir(ino, fs, ri) = mkdir (fs[ri[inodekey(ino)]].size, fs[ri[inodekey(ino)]].meta, fs[ri[inodekey(ino)]].nlink, fs[ri[inodekey(ino)]].nsubdirs, abs-children(ino, fs, ri)); (s)%⊦ inodekey(ino) ∈ ri ∧ fs[ri[inodekey(ino)]].directory → abs-dirs(fs, ri)[ino] = abs-dir(ino, fs, ri); (s)% ⊦ dirs[ino, ad][ino0] = (ino0 = ino ∧ ino ∈ dirs ⊃ ad;dirs[ino0]); (s)% ⊦ fs[adr0, nd][adr1] = (adr0 = adr1 ⊃ nd;fs[adr1]); (s)% ⊦ inodekey(m) = inodekey(m0) ↔ m = m0; (s)%⊦ ino ∈ abs-dirs(fs, ri) ↔ inodekey(ino) ∈ ri ∧ fs[ri[inodekey(ino)]].directory; (s)% ⊦ ino ∈ dirs[ino0, ad] ↔ ino ∈ dirs; (s)%⊦ dirs = abs-dirs(fs, ri) ↔ (∀ ino. ( ino ∈ dirs ↔ inodekey(ino) ∈ ri ∧ fs[ri[inodekey(ino)]].directory) ∧ (ino ∈ dirs → dirs[ino] = abs-dir(ino, fs, ri))); (ss)