| zh0[r0] = mkznode(r1, zbrar0, boolvar0, false, m5), istore2[m1] = indexblock(indx, lax, m4), zh[r0] = mkznode(r, zbrar, boolvar, true, m0), istore[adr1] = istore2[adr1], remove-refsize0(gstore0) = gstore0, remove-refsize0(istore0) = istore0, elems nx ∩ ginval = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ ginval, ((btree(null, r0, @(m1, m2, m3), height, false, ri, nodes(istore2), alladrs1, alladrs1, ok) * true))(zh0), ((btree(null, null, adr1, height0, false, fi, nodes(istore0), alladrs0, alladrs0, ok) * true))(zh), ((btree(null, r0, adr1, height, dirty, ri, nodes(istore), as, alladrs, ok) * true))(zh), ((btree(null, r0, @(m1, m2, m3), height, false, ri, nodes(istore2) | alladrs1, alladrs1, alladrs1, ok) * true))(zh0), inv(indexblock(indx, lax, m4)), inv(istore2), inv(gstore \ ginval), inv(gstore0), inv(istore), inv(istore0), refsize-cons(istore2, alladrs1), refsize-cons(istore, as), refsize-cons(istore0, alladrs0), adr1 ∈ istore2, r0 ∈ zh0, m1 ∈ istore2, @(m1, m2, m3) ∈ istore2, @(m1, m2, m3) ∈ alladrs1, m ∈ istore, adr1 ∈ istore, r0 ∈ zh, m ∈ istore2, m6 ∈ istore2, adr1 ∈ alladrs1, alladrs1 ∩ dom nodes(istore) ⊆ alladrs, as ⊆ alladrs, as ⊆ dom nodes(istore), alladrs0 ⊆ dom nodes(istore), alladrs0 ⊆ dom nodes(istore0), alladrs ⊆ dom nodes(istore), alladrs1 ⊆ dom nodes(istore2), istore ⊑ istore2, istore0 ⊑ istore2, istore0 ⊑ istore, height = 0 → alladrs1 = ∅ ++ @(m1, m2, m3), height = 0 → as = ∅, ∀ adr. adr ∈ alladrs1 ∩ dom nodes(istore) → adr ∈ as ⊦ # alladrs1 = 0, alladrs1 = ∅, ((btree(null, r0, adr1, height, true, ri, nodes(istore2), alladrs1 -- @(m1, m2, m3), (alladrs1 -- @(m1, m2, m3)) ++ adr1, ok) * true) )(zh0[r0, mkznode(r1, zbrar0, boolvar0, true, m5)]), dups(nx), adr1 ∈ as |
Used simplifier rules: ⊦ adr ∈ as ∩ as0 ↔ adr ∈ as ∧ adr ∈ as0; (ws)% ⊦ adr ∈ dom iast ↔ adr ∈ iast; (s)% ⊦ adr ∈ nodes(istore) ↔ adr ∈ istore; (s)%int-a: ⊦ (as ∩ as0) ∩ as1 = as ∩ as0 ∩ as1; from specification set-union[node-store]%int-c: ⊦ as ∩ as0 = as0 ∩ as; from specification set-union[node-store] Used terms: adr1