| istore4[m2] = indexblock(indx, lax0, m), zh[r] = mkznode(r0, zbrar, boolvar, true, m0), adr = adr0, 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)), 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) ], height = 0 → as = ∅, index(m2).index? ∨ index(m2).journal? ⊦ [abort] ( inv(istore) ∧ istore2 ⊑ istore ∧ m2 ∈ istore → ⟪err := ESUCCESS; if err = ESUCCESS then zh[r].dirty := false⟫ ( refsize-cons(istore, as0 ∪ (err = ESUCCESS ⊃ as ++ @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize);as)) ∧ istore4 ⊑ istore ∧ r ∈ zh ∧ (err = ESUCCESS → ¬ @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ∈ as) ∧ dom nodes(istore) = 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), (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) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → ¬ zh[r].dirty))), 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, maxino0 ∈ istore |