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

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, as ∪ as0), 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), @(m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ∈ lax0, @(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) ]

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 256:
⊦ istore ⊑ istore0 ∧ n ∈ istore0 ∧ istore0[n] = indexblock(indx, lax, m0) ∧ # lax0 = # indx0 → istore ⊑ istore0[n, indexblock(indx + indx0, lax + lax0, n0)]
Proof step 257:
# @(m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ' = # save(mkznode(r0, zbrar, boolvar, true, m0)) ', zh[r] = mkznode(r0, zbrar, boolvar, true, m0), istore4[m2] = indexblock(indx, lax0, m), remove-refsize0(gstore1) = gstore1, remove-refsize0(istore2) = istore2, 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(indexblock(indx, lax0, m)), inv(gstore2 \ ginval2), inv(gstore1), inv(istore4), inv(istore2), inv (istore4 [m2, indexblock(indx + save(mkznode(r0, zbrar, boolvar, true, m0)) ', lax0 + @(m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ', m) ]), 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) ]), refsize-cons(istore4, as0 ∪ as), refsize-cons(istore4, as ∪ as0), r ∈ zh, m2 ∈ istore4, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize ≤ LEB_SIZE, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize ≤ n0, n0 ≤ LEB_SIZE, as0 ⊆ dom nodes(istore4), alladrs ⊆ dom nodes(istore4), as ⊆ alladrs, as ⊆ dom nodes(istore4), 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) ], 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, istore4 ⊑ istore4, height = 0 → as = ∅ ⊦ dups(nx), @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ∈ as, adr1 ∈ as, @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ∈ istore4, @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ∈ istore2, @(m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ∈ lax0, (( 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)]) ∧ true

Rule argument

spec: ablock-store-inv, inst: index-store name: prefix-append-in seq: ⊦ istore ⊑ istore0 ∧ n ∈ istore0 ∧ istore0[n] = indexblock(indx, lax, m0) ∧ # lax0 = # indx0 → istore ⊑ istore0[n, indexblock(indx + indx0, lax + lax0, n0)] subst: [m0, n0, lax0, lax, indx0, indx, n, istore0, istore] → [m, m + save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize, @(m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ', lax0, save(mkznode(r0, zbrar, boolvar, true, m0)) ', indx, m2, istore4, istore4] flags: <all paths>

Additional information

Used simplifier rules: ⊦ inv(istore) → istore ⊑ istore; (s)% ⊦ # ladr ' = 0 +1; (s)% ⊦ # ind ' = 0 +1; (s) Used terms: m, m + save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize, @(m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ', lax0, save(mkznode(r0, zbrar, boolvar, true, m0)) ', indx, m2, istore4, istore4