Proof step 162 from proof inv-commit-rec-ind (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 163:

  zh0[zbrar0[n0].child] = mkznode(r3, zbrar1, boolvar2, boolvar3, m2), zh1[r0] = mkznode(r1, zbrar, false, true, m0), zh0[r0] = mkznode(r2, zbrar0, false, true, m1), remove-refsize0(istore0) = istore0, remove-refsize0(gstore1) = gstore1, elems nx ∩ ginval1 = ∅, as ∩ as0 = ∅, as1 ∩ as0 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval1, ((btree(rp, r0, adr3, height, dirty, ri, nodes(istore) | as1, as1, alladrs, ok) * P))(zh0), ((btree(rp, r0, adr3, height, dirty, ri, nodes(istore2) | as, as, alladrs, ok) * P))(zh1), n0 < # zbrar0, n0 < m1, btree-sub-clean(r0, n0, zh0), inv(istore0), inv(istore2), inv(gstore1), inv(gstore2 \ ginval1), inv(istore), refsize-cons(istore2, as0 ∪ as), refsize-cons(istore, as0 ∪ as1), m ∈ istore, m3 ∈ istore, m ∈ istore2, r0 ∈ zh1, r0 ∈ zh0, as1 ⊆ alladrs, as1 ⊆ dom nodes(istore), as1 ∩ dom nodes(istore2) ⊆ alladrs, as0 ⊆ dom nodes(istore2), alladrs ⊆ dom nodes(istore2), as ⊆ alladrs, as ⊆ dom nodes(istore2), as1 ∩ dom nodes(istore2) ⊆ as, as1 ⊆ dom nodes(istore2), istore0 ⊑ istore, istore0 ⊑ istore2, istore2 ⊑ istore, height = 0 → as1 = ∅, height = 0 → as = ∅, ∀ height0, zh, r0, r, zbrar, boolvar, m0, adr0, adr1, istore1, istore, pstate, m, istore0, gstore0, nx, ginval, as, as0, gstore, rp, dirty, ri, alladrs, P, adr, ino, ns, err, bv. height0 < height → zh[r0] = mkznode(r, zbrar, boolvar, true, m0) ∧ adr0 = adr1 ∧ istore1 = istore ∧ pstate = index(m) ∧ remove-refsize0(istore0) = istore0 ∧ remove-refsize0(gstore0) = gstore0 ∧ elems nx ∩ ginval = ∅ ∧ as ∩ as0 = ∅ ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval ∧ ((btree(rp, r0, adr1, height0, dirty, ri, nodes(istore) | as, as, alladrs, ok) * P))(zh) ∧ inv(istore0) ∧ inv(istore) ∧ inv(gstore0) ∧ inv(gstore \ ginval) ∧ refsize-cons(istore, as0 ∪ as) ∧ m ∈ istore ∧ r0 ∈ zh ∧ as0 ⊆ dom nodes(istore) ∧ alladrs ⊆ dom nodes(istore) ∧ as ⊆ alladrs ∧ as ⊆ dom nodes(istore) ∧ istore0 ⊑ istore ∧ ¬ dups(nx) ∧ ¬ adr1 ∈ as ∧ (height0 = 0 → as = ∅) → ⟪btree_commit_rec#(r0, adr, istore0, ginval, gstore, gstore0, nx, ino, ns; adr1, err, zh, istore, pstate, bv)⟫ ( istore1 ⊑ istore ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore) ∧ (pstate.index? → pstate.lnum ∈ istore) ∧ (pstate = unbuffered → bv) ∧ inv(istore) ∧ istore0 ⊑ istore ∧ r0 ∈ zh ∧ (err = ESUCCESS → ¬ zh[r0].dirty ∧ pstate.index?) ∧ (∃ as1, alladrs1. refsize-cons(istore, as0 ∪ as1) ∧ as1 ∩ dom nodes(istore1) ⊆ as ∧ as1 ∩ as0 = ∅ ∧ alladrs1 ⊆ alladrs ∪ as1 ∧ ((btree(rp, r0, (err = ESUCCESS ⊃ adr1;adr0), height0, err ≠ ESUCCESS, ri, nodes(istore) | as1, as1, alladrs1, ok) * P))(zh))) ⊦ dups(nx), adr3 ∈ as1, adr3 ∈ as, zbrar0[n0].child ≠ null ∧ boolvar3, (∃ as1. refsize-cons(istore, as0 ∪ as1) ∧ as1 ∩ dom nodes(istore2) ⊆ as ∧ as1 ∩ as0 = ∅ ∧ ((btree(rp, r0, adr3, height, dirty, ri, nodes(istore) | as1, as1, alladrs, ok) * P))(zh0)) ∧ btree-sub-clean(r0, n0 + 1, zh0)

Rule argument

Additional information

Used simplifier rules: ⊦ mkznode(r, zbrar, boolvar, boolvar0, m).leaf ↔ boolvar; (s)% ⊦ mkznode(r, zbrar, boolvar, boolvar0, m).dirty ↔ boolvar0; (s)% ⊦ mkznode(r, zbrar, boolvar, boolvar0, m).usedsize = m; (s)% ⊦ unbuffered ≠ index(m); (s)% ⊦ index(m).lnum = m; (s)% ⊦ index(m).index?; (s)% ⊦ ¬ index(m).journal?; (s)%⊦ inv-state(pstate, nx, gstore, istore, syn) ↔ ( pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore) ∧ (pstate.index? → pstate.lnum ∈ istore) ∧ (pstate = unbuffered → syn); (s)%⊦ inv-index(istore, istore0) ↔ inv(istore) ∧ inv(istore0) ∧ istore0 ⊑ istore ∧ remove-refsize0(istore0) = istore0; (s)%⊦ inv-journal(nx, gstore, gstore0, ginval) ↔ inv(gstore \ ginval) ∧ inv(gstore0) ∧ elems nx ∩ ginval = ∅ ∧ ¬ dups(nx) ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval ∧ remove-refsize0(gstore0) = gstore0; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ m + 1 ≤ n ↔ m < n; (s)