| zh0[r0] = mkznode(r1, zbrar0, boolvar0, boolvar1, m5), istore[adr1] = istore2[adr1], zh[r0] = mkznode(r, zbrar, boolvar, true, m0), istore2[m1] = indexblock(indx, lax, m4), remove-refsize0(istore0) = istore0, remove-refsize0(gstore0) = gstore0, elems nx ∩ ginval = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ ginval, ((btree(null, r0, adr1, height, true, ri, nodes(istore2) | as0, as0, alladrs1, ok) * true))(zh0), ((btree(null, r0, adr1, height, dirty, ri, nodes(istore), as, alladrs, ok) * true))(zh), ((btree(null, null, adr1, height0, false, fi, nodes(istore0), alladrs0, alladrs0, ok) * true))(zh), inv(istore0), inv(istore), inv(gstore0), inv(gstore \ ginval), inv(istore2), refsize-cons(istore0, alladrs0), refsize-cons(istore, as), refsize-cons(istore2, as0), m ∈ istore2, r0 ∈ zh, adr1 ∈ istore, m ∈ istore, r0 ∈ zh0, adr1 ∈ istore2, as0 ∩ dom nodes(istore) ⊆ alladrs, alladrs ⊆ dom nodes(istore), alladrs0 ⊆ dom nodes(istore0), alladrs0 ⊆ dom nodes(istore), as ⊆ dom nodes(istore), as ⊆ alladrs, alladrs1 ⊆ alladrs ∪ as0, as0 ∩ dom nodes(istore) ⊆ as, as0 ⊆ alladrs1, as0 ⊆ dom nodes(istore2), istore0 ⊑ istore, istore0 ⊑ istore2, istore ⊑ istore2, height = 0 → as = ∅, pstate0 = unbuffered → bv, pstate0.index? → pstate0.lnum ∈ istore2, pstate0.journal? → nx ≠ [] ∧ pstate0.lnum = nx.last ∧ pstate0.lnum ∈ gstore ⊦ err = ESUCCESS, dups(nx), adr1 ∈ as, ∃ height1, dirty0, as1, alladrs2. ((btree(null, r0, adr1, height1, dirty0, ri, nodes(istore2), as1, alladrs2, ok) * true))(zh0) ∧ refsize-cons(istore2, as1) ∧ alladrs2 ⊆ dom nodes(istore2) |
Used simplifier rules: sep-ass: ⊦ (P * P3) * P4 = P * P3 * P4; from specification heap-sep[zheap]%sep-com: ⊦ P * P2 = P2 * P; from specification heap-sep[zheap]%⊦ (( btree (rp, r0, adr, height, dirty0, ri, iast | as0, as, alladrs, nstat) * P) )(zh0) → (( btree (rp, r0, adr, height, dirty0, ri, iast, as, alladrs, nstat) * P) )(zh0); (ss)%sub-ntrans-01: ⊦ as ⊆ as0 ∧ ¬ as1 ⊆ as0 → ¬ as1 ⊆ as; (forward) from specification set-basic[node-store]%sub-ntrans: ⊦ as ⊆ as0 ∧ ¬ as ⊆ as1 → ¬ as0 ⊆ as1; (forward) from specification set-basic[node-store]% ⊦ as ∪ as0 ⊆ as1 ↔ as ⊆ as1 ∧ as0 ⊆ as1; (ws)%una: ⊦ (as ∪ as0) ∪ as1 = as ∪ as0 ∪ as1; from specification set-union[node-store]%unc: ⊦ as ∪ as0 = as0 ∪ as; from specification set-union[node-store]% ⊦ as ⊆ as0 → (as0 ⊆ as ↔ as = as0); (s)% ⊦ istore ⊑ istore0 → dom nodes(istore) ⊆ dom nodes(istore0); (ss)%⊦ ¬ pstate.journal? → (pstate.index? ↔ pstate ≠ unbuffered ∧ pstate ≠ readonly); (ss)%btree-leaf-adr: ⊦ ((btree(rp, r, adr, 0, dirty, ri, iast, as, alladrs, nstat) * P) )(zh) → alladrs = {adr} ; (forward) from specification btree-inv%btree-dirty-adr-notin: ⊦ r ∈ zh ∧ zh[r] = mkznode(rp0, zbrar, boolvar, true, height0) ∧ (( btree (rp, r, adr, height, dirty, ri, iast, as, alladrs, nstat) * P) )(zh) → ¬ adr ∈ as ∧ (height = 0 → as = ∅); (forward) from specification btree-inv% ⊦ {adr} = ∅ ++ adr; (s) Used terms: height, true, as0, alladrs1