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

User applied rule case distinction

And obtained the following new goals

• Proof step 188:

  zh1[r0] = mkznode(r1, zbrar, false, true, m0), zh[r0] = mkznode(r2, zbrar0, false, true, n), zh0[r0] = mkznode(r3, zbrar1, boolvar0, boolvar1, m2), dom nodes(istore1) = dom nodes(istore) ∪ (err = ESUCCESS ⊃ ∅ ++ adr;∅), 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, (err = ESUCCESS ⊃ adr;adr3), height, err ≠ ESUCCESS, ri, nodes(istore1), (err = ESUCCESS ⊃ as1 ++ adr;as1), (err = ESUCCESS ⊃ (alladrs -- adr3) ++ adr;alladrs), ok) * P) )(zh0), ((btree(rp, r0, adr3, height, dirty, ri, nodes(istore) | as1, as1, alladrs, ok) * P))(zh), ((btree(rp, r0, adr3, height, dirty, ri, nodes(istore2) | as, as, alladrs, ok) * P))(zh1), ((btree(rp, r0, adr3, height, dirty, ri, nodes(istore), as1, alladrs, ok) * P))(zh), btree-sub-clean(r0, n, zh), inv(istore1), inv(istore0), inv(istore2), inv(gstore1), inv(gstore2 \ ginval1), inv(istore), refsize-cons(istore1, as0 ∪ (err = ESUCCESS ⊃ as1 ++ adr;as1)), refsize-cons(istore2, as0 ∪ as), refsize-cons(istore, as0 ∪ as1), r0 ∈ zh0, m ∈ istore, m1 ∈ istore, m ∈ istore2, r0 ∈ zh1, r0 ∈ zh, m ∈ istore1, m1 ∈ istore1, as1 ⊆ alladrs, 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), as0 ⊆ dom nodes(istore), alladrs ⊆ dom nodes(istore), as1 ⊆ dom nodes(istore), as1 ∩ dom nodes(istore2) ⊆ dom nodes(istore), (err = ESUCCESS ⊃ as1 ++ adr;as1) ⊆ dom nodes(istore1), (err = ESUCCESS ⊃ as1 ++ adr;as1) ⊆ (err = ESUCCESS ⊃ (alladrs -- adr3) ++ adr;alladrs), istore0 ⊑ istore1, istore ⊑ istore1, istore0 ⊑ istore, istore0 ⊑ istore2, istore2 ⊑ istore, istore2 ⊑ istore1, pstate0.journal? → nx ≠ [] ∧ pstate0.lnum = nx.last ∧ pstate0.lnum ∈ gstore2, pstate0.index? → pstate0.lnum ∈ istore1, pstate0 = unbuffered → syn, err = ESUCCESS → ¬ adr ∈ as1, err = ESUCCESS → ¬ adr ∈ istore, err = ESUCCESS → pstate0.index? ∧ ¬ boolvar1, height = 0 → as1 = ∅, height = 0 → as = ∅, err = ESUCCESS ∨ ⌊err⌋ , ∀ 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 ∈ as, adr3 ∈ as1, (err = ESUCCESS ⊃ (alladrs -- adr3) ++ adr;alladrs) ⊆ alladrs ∪ (err = ESUCCESS ⊃ as1 ++ adr;as1)

Rule argument

Additional information

Used simplifier rules: size-zero-01: ⊦ as ≠ ∅ → # as ≠ 0; (forward) from specification set-basic[node-store]% ⊦ as ∪ ∅ = as; (s)%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 ++ adr) ∪ as0 = (as ∪ as0) ++ adr; (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]% ⊦ as ∩ as0 = ∅ → (as ∩ (as0 ++ adr) = ∅ ↔ ¬ adr ∈ as); (ss)% ⊦ adr ∈ as → (as ∪ as0) ++ adr = as ∪ as0; (s)% ⊦ as ++ adr ⊆ as0 ↔ as ⊆ as0 ∧ adr ∈ as0; (ws)% ⊦ adr ∈ dom iast ↔ adr ∈ iast; (s)% ⊦ adr ∈ nodes(istore) ↔ adr ∈ istore; (s)% ⊦ as ⊆ as0 ∧ ¬ adr ∈ as → as ⊆ (as0 -- adr) ++ adr0; (s)% ⊦ adr ∈ as ++ adr0 ↔ adr = adr0 ∨ adr ∈ as; (s)%sub-in: ⊦ adr ∈ as ∧ as ⊆ as0 → adr ∈ as0; (forward) from specification set-basic[node-store]%ne-01: ⊦ adr ∈ as → as ≠ ∅; (forward) from specification set-basic[node-store]%btree-leaf-adr: ⊦ ((btree(rp, r, adr, 0, dirty, ri, iast, as, alladrs, nstat) * P) )(zh) → alladrs = {adr} ; (forward) from specification btree-inv%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-clean-alladrs: ⊦ (( btree(rp, r, adr, height, false, ri, iast, as, alladrs, nstat) * P) )(zh) → as = alladrs; (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%btree-adrs: ⊦ (( btree (rp, rp0, adr0, height, dirty, fi, iast, as, alladrs, nstat) * P) )(zh) → as ⊆ dom iast; (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%size-zero: ⊦ # as ≠ 0 → as ≠ ∅; (forward) from specification set-basic[node-store]%prefix-notin-fwd: ⊦ ¬ adr ∈ istore ∧ istore0 ⊑ istore → ¬ adr ∈ istore0; (forward) from specification ablock-store-inv[index-store]% ⊦ {adr} = ∅ ++ adr; (s)% ⊦ as = ∅ ++ adr → as -- adr = ∅; (s)% ⊦ ¬ adr ∈ as → (as ++ adr = ∅ ++ adr0 ↔ adr = adr0 ∧ as = ∅); (ws)% ⊦ adr ∈ as → as ++ adr = as; (s)% ⊦ ¬ adr ∈ as → (as ⊆ as0 ++ adr ↔ as ⊆ as0); (s)% ⊦ as ⊆ ∅ ↔ as = ∅; (s)% ⊦ adr ∈ ∅ ++ adr0 ↔ adr = adr0; (s)% ⊦ ¬ unbuffered.index?; (s)%sub-ntrans-01: ⊦ as ⊆ as0 ∧ ¬ as1 ⊆ as0 → ¬ as1 ⊆ as; (forward) from specification set-basic[node-store]% ⊦ as0 ∩ as ⊆ as1 ∩ as ↔ as0 ∩ as ⊆ as1; (ss)% ⊦ as ∩ as0 ⊆ as; (s)%⊦ ¬ adr ∈ istore → (as ++ adr) ∩ dom nodes(istore) = as ∩ dom nodes(istore); (s)