[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 251 from proof inv-io-save (previous step)

istore4[m2] = indexblock(indx, lax0, m), zh[r] = mkznode(r0, zbrar, boolvar, true, m0), adr = adr0, err = ESUCCESS, ginval0 = ginval2, gstore = gstore1, gstore0 = gstore2, istore = istore1, istore0 = istore2, istore1 = istore4 [m2, indexblock(indx + save(mkznode(r0, zbrar, boolvar, true, m0)) ', lax0 + @(m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ', m) ], maxino = maxino1, maxino0 = index(m2).lnum, n = m + save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize, pstate = index(m2), remove-refsize0(istore2) = istore2, remove-refsize0(gstore1) = gstore1, elems nx ∩ ginval2 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval2, ((btree(rp, r, adr1, height, dirty, ri, nodes(istore4), as, alladrs, ok) * P))(zh), btree-sub-clean(r, m0, zh), inv (istore4 [m2, indexblock(indx + save(mkznode(r0, zbrar, boolvar, true, m0)) ', lax0 + @(m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ', m) ]), inv(istore2), inv(istore4), inv(gstore1), inv(gstore2 \ ginval2), inv(indexblock(indx, lax0, m)), inv(istore[maxino0, istore[maxino0].ref-size:= n]), refsize-cons(istore4, as0 ∪ as), maxino0 ∈ istore, m2 ∈ istore4, r ∈ zh, m2 ∈ istore[maxino0, istore[maxino0].ref-size:= n], n0 ≤ LEB_SIZE, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize ≤ n0, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize ≤ LEB_SIZE, as ⊆ dom nodes(istore4), as ⊆ alladrs, alladrs ⊆ dom nodes(istore4), as0 ⊆ dom nodes(istore4), istore2 ⊑ istore4, istore2 ⊑ istore4 [m2, indexblock(indx + save(mkznode(r0, zbrar, boolvar, true, m0)) ', lax0 + @(m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ', m) ], istore2 ⊑ istore[maxino0, istore[maxino0].ref-size:= n], height = 0 → as = ∅, index(m2).index? ∨ index(m2).journal? ⊦ dups(nx), @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ∈ istore2, @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ∈ istore4, adr1 ∈ as, refsize-cons (istore[maxino0, istore[maxino0].ref-size:= n], as0 ∪ (err = ESUCCESS ⊃ as ++ @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize);as)) ∧ istore4 ⊑ istore[maxino0, istore[maxino0].ref-size:= n] ∧ r ∈ zh[r, zh[r].dirty:= false] ∧ (err = ESUCCESS → ¬ @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ∈ as) ∧ dom nodes(istore[maxino0, istore[maxino0].ref-size:= n]) = dom nodes(istore4) ∪ (err = ESUCCESS ⊃ ∅ ++ @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize);∅) ∧ (( btree (rp, r, (err = ESUCCESS ⊃ @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize);adr1), height, err ≠ ESUCCESS, ri, nodes(istore[maxino0, istore[maxino0].ref-size:= n]), (err = ESUCCESS ⊃ as ++ @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize);as), (err = ESUCCESS ⊃ (alladrs -- adr1) ++ @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize);alladrs), ok) * P) )(zh[r, zh[r].dirty:= false]) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → ¬ zh[r, zh[r].dirty:= false][r].dirty)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 252:
istore4[m2] = indexblock(indx, lax0, m), zh[r] = mkznode(r0, zbrar, boolvar, true, m0), remove-refsize0(istore2) = istore2, remove-refsize0(gstore1) = gstore1, elems nx ∩ ginval2 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval2, ((btree(rp, r, adr1, height, dirty, ri, nodes(istore4), as, alladrs, ok) * P))(zh), btree-sub-clean(r, m0, zh), inv (istore4 [m2, indexblock (indx + save(mkznode(r0, zbrar, boolvar, true, m0)) ', lax0 + @(m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ', m + save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ]), inv (istore4 [m2, indexblock(indx + save(mkznode(r0, zbrar, boolvar, true, m0)) ', lax0 + @(m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ', m) ]), inv(istore2), inv(istore4), inv(gstore1), inv(gstore2 \ ginval2), inv(indexblock(indx, lax0, m)), refsize-cons(istore4, as0 ∪ as), m2 ∈ istore4, r ∈ zh, n0 ≤ LEB_SIZE, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize ≤ n0, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize ≤ LEB_SIZE, as ⊆ dom nodes(istore4), as ⊆ alladrs, alladrs ⊆ dom nodes(istore4), as0 ⊆ dom nodes(istore4), istore2 ⊑ istore4, istore2 ⊑ istore4 [m2, indexblock(indx + save(mkznode(r0, zbrar, boolvar, true, m0)) ', lax0 + @(m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ', m) ], istore2 ⊑ istore4 [m2, indexblock (indx + save(mkznode(r0, zbrar, boolvar, true, m0)) ', lax0 + @(m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ', m + save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ], height = 0 → as = ∅ ⊦ dups(nx), @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ∈ istore2, @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ∈ istore4, adr1 ∈ as, @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ∈ as, (( btree (rp, r, @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize), height, false, ri, nodes(istore4)[@(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize), save(mkznode(r0, zbrar, boolvar, true, m0))], as ++ @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize), (alladrs -- adr1) ++ @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize), ok) * P) )(zh[r, mkznode(r0, zbrar, boolvar, false, m0)]) ∧ istore4 ⊑ istore4 [m2, indexblock (indx + save(mkznode(r0, zbrar, boolvar, true, m0)) ', lax0 + @(m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ', m + save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ] ∧ refsize-cons (istore4 [m2, indexblock (indx + save(mkznode(r0, zbrar, boolvar, true, m0)) ', lax0 + @(m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ', m + save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ], (as ∪ as0) ++ @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize))

Rule argument

Additional information

Used simplifier rules: ⊦ adr ∈ nodes(istore) ↔ adr ∈ istore; (s)% ⊦ adr ∈ dom iast ↔ adr ∈ iast; (s)%ne-01: ⊦ adr ∈ as → as ≠ ∅; (forward) from specification set-basic[node-store]%sub-in: ⊦ adr ∈ as ∧ as ⊆ as0 → adr ∈ as0; (forward) from specification set-basic[node-store]%⊦ mkznode(r, zbrar, boolvar, boolvar0, m).dirty:= boolvar2 = mkznode(r, zbrar, boolvar, boolvar2, m); (s)% ⊦ (znd.dirty:= boolvar0).dirty ↔ boolvar0; (s)% ⊦ zh[r0, znd][r] = (r = r0 ∧ r0 ∈ zh ⊃ znd;zh[r]); (s)% ⊦ as ∪ ∅ = as; (s)% ⊦ dom iast[adr, ind] = dom iast ++ adr; (s)%a: ⊦ (indx + indx0) + indx1 = indx + indx0 + indx1; from specification list[index-store]%a: ⊦ (lax + lax0) + lax1 = lax + lax0 + lax1; from specification list[laddress-list]% ⊦ @(m, m0).size = m0; (s)% ⊦ @(m, m0).off = m; (s)%n ∈ istore, ¬ ladr ∈ lax ⊦ inv(indexblock(indx, lax, m0)) ∧ istore[n] = indexblock(indx, lax, m0) → nodes(istore[n, indexblock(indx + ind ', lax + ladr ', m1)]) = nodes(istore)[@(n, ladr.off, ladr.size), ind]; (s)%⊦ istore[n] = indexblock(indx, lax, m0) ∧ n ∈ istore ∧ @(n0, n1) ∈ lax → @(n, n0, n1) ∈ istore; (ss)% ⊦ r ∈ zh[r0, znd] ↔ r ∈ zh; (s)%unc: ⊦ as ∪ as0 = as0 ∪ as; from specification set-union[node-store]%una: ⊦ (as ∪ as0) ∪ as1 = as ∪ as0 ∪ as1; from specification set-union[node-store]% ⊦ (as ++ adr) ∪ as0 = (as ∪ as0) ++ adr; (s)% ⊦ index(m).index?; (s)% ⊦ n ∈ istore[n, iblock]; (s)% ⊦ istore[n, iblock][n, iblock0] = istore[n, iblock0]; (s)% ⊦ indexblock(indx, lax, m).ref-size:= m0 = indexblock(indx, lax, m0); (s)% ⊦ istore[n, iblock][n] = iblock; (s)% ⊦ index(m).lnum = m; (s)