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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 46:

  # asar0 = m1 + 1, # zbrar0 = BRANCH_SIZE, # asar = m1 + 1, istore2[adr3] = istore[adr3], zh0[zbrar0[n0].child] = mkznode(r3, zbrar1, boolvar2, true, m2), adr = zbrar0[n0].adr, err = ESUCCESS, pstate = index(m3), remove-refsize0(gstore1) = gstore1, remove-refsize0(istore0) = istore0, union(asar0, 0, m1 + 1) = alladrs -- adr3, union(asar, 0, m1 + 1) ∩ as0 = ∅, as ∩ as0 = ∅, elems nx ∩ ginval1 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval1, # alladrs ≠ 0, alladrs ≠ ∅, (( ( ( ( btree (r0, zbrar0[n0].child, zbrar0[n0].adr, height1, true, key-range(zbrar0, n0, m1 + 1, ri), nodes(istore) | union(asar, 0, m1 + 1), asar[n0], asar0[n0], ok) * (λ n. ⌜zbrar0[n].branch?⌝ ∧ btree (r0, zbrar0[n].child, zbrar0[n].adr, height1, true, key-range(zbrar0, n, m1 + 1, ri), nodes(istore) | union(asar, 0, m1 + 1), asar[n], asar0[n], ok) )⊗_ (0, n0 )) * (λ n. ⌜zbrar0[n].branch?⌝ ∧ btree (r0, zbrar0[n].child, zbrar0[n].adr, height1, true, key-range(zbrar0, n, m1 + 1, ri), nodes(istore) | union(asar, 0, m1 + 1), asar[n], asar0[n], ok) )⊗_ (1 + n0, m1 - n0 )) * r0 => mkznode(rp, zbrar0, false, true, m1 + 1)) * P) )(zh0), ((btree(rp, r0, adr3, height1 + 1, true, ri, nodes(istore) | union(asar, 0, m1 + 1), union(asar, 0, m1 + 1), alladrs, ok) * P))(zh0), zbrar0[n0].branch?, n0 + 1 < BRANCH_SIZE, m1 + 1 < BRANCH_SIZE, n0 < BRANCH_SIZE, btree-sub-clean(r0, n0, zh0), disj(asar, 0, m1 + 1), disj(asar0, 0, m1 + 1), inv(istore), inv(gstore2 \ ginval1), inv(gstore1), inv(istore2), inv(istore0), refsize-cons(istore, as0 ∪ union(asar, 0, m1 + 1)), refsize-cons(istore2, as0 ∪ as), sorted(zbrar0, 0, m1), zbrar0[n0].child ∈ zh0, adr3 ∈ istore2, r0 ∈ zh1, m ∈ istore2, m3 ∈ istore, m ∈ istore, adr3 ∈ alladrs, adr3 ∈ istore, n0 ≤ m1, union(asar, 0, m1 + 1) ∩ dom nodes(istore2) ⊆ alladrs, union(asar, 0, m1 + 1) ∩ dom nodes(istore2) ⊆ as, as ⊆ dom nodes(istore2), as ⊆ alladrs, alladrs ⊆ dom nodes(istore2), as0 ⊆ dom nodes(istore2), asar[n0] ⊆ asar0[n0], asar[n0] ⊆ dom nodes(istore) ∩ union(asar, 0, m1 + 1), istore2 ⊑ istore, istore0 ⊑ istore2, istore0 ⊑ istore, ¬ dups(nx), ¬ adr3 ∈ as, ¬ adr3 ∈ union(asar, 0, m1 + 1), ¬ zbrar0[n0].adr ∈ asar[n0], height1 = 0 → asar[n0] = ∅, ∀ n. ¬ m1 < n → asar[n] ⊆ dom nodes(istore2), ∀ n. ¬ m1 < n → asar[n] ⊆ dom nodes(istore), ∀ n. ¬ m1 < n → asar[n] ⊆ alladrs, ∀ n. ¬ m1 < n → asar[n] ⊆ dom nodes(istore) ∩ union(asar, 0, m1 + 1), ∀ 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 < height1 +1 → 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))) ⊦ ⟪btree_commit_rec#(zbrar0[n0].child, adr1, istore0, ginval1, gstore2, gstore1, nx, maxino, ginval; adr, err, zh0, istore, pstate, syn); n := n0; if err = ESUCCESS then zh0[r0].zbranches[n].adr := adr; n := n + 1⟫ ( commit-inv (n, pstate, istore2, istore0, nx, gstore2, gstore1, ginval1, syn, err, rp, r0, adr3, height1 + 1, true, ri, istore, as, as0, alladrs, P, zh0) ∧ ¬ m1 < (zh0[r0].usedsize - n) + n0)

Rule argument

Additional information

Used simplifier rules: 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% ⊦ dom(iast | as) = dom iast ∩ as; (s)% ⊦ r ∈ zh → r ≠ null; (s)%btree-root-in-heap: ⊦ r ≠ null ∧ (( btree (rp, r, adr, height, dirty, fi, iast, as, alladrs, nstat) * P) )(zh) → r ∈ zh; (forward) from specification btree-inv%btree-adrs: ⊦ (( btree (rp, rp0, adr0, height, dirty, fi, iast, as, alladrs, nstat) * P) )(zh) → as ⊆ dom iast; (forward) from specification btree-inv%btree-refed-subseteq-alladrs: ⊦ (( btree(rp, r, adr, height, dirty, fi, iast, as, alladrs, nstat) * P) )(zh) → as ⊆ alladrs; (forward) from specification btree-inv% ⊦ ⌜bv⌝ (zh) ↔ bv; (s)% ⊦ ((P ∧ P2))(zh) ↔ P(zh) ∧ P2(zh); (s)%sep-com: ⊦ P * P2 = P2 * P; from specification heap-sep[zheap]%sep-ass: ⊦ (P * P3) * P4 = P * P3 * P4; from specification heap-sep[zheap]%and-com: ⊦ (P ∧ P2) = (P2 ∧ P); from specification heap-sep[zheap]%and-ass: ⊦ ((P ∧ P3) ∧ P4) = (P ∧ P3 ∧ P4); from specification heap-sep[zheap]% ⊦ (⌜bv⌝ ∧ P) * P2 = (⌜bv⌝ ∧ P * P2); (s)% ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s)% ⊦ n + 0 = n; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ m ≤ n → (n < m ↔ false); (s)% ⊦ m < n + 1 ↔ ¬ n < m; (s)