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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 207:

  zh[r0] = mkznode(r1, zbrar, true, true, m0), adr0 = adr3, istore1 = istore, pstate = index(m), remove-refsize0(gstore1) = gstore1, remove-refsize0(istore0) = istore0, elems nx ∩ ginval1 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval1, ((btree(rp, r0, adr3, 0, dirty, ri, ∅, ∅, ∅ ++ adr3, ok) * P))(zh), ((btree(rp, r0, adr3, 0, dirty, ri, nodes(istore), ∅, ∅ ++ adr3, ok) * P))(zh), btree-sub-clean(r0, m0, zh), inv(gstore2 \ ginval1), inv(gstore1), inv(istore), inv(istore0), refsize-cons(istore, as0), m ∈ istore, r0 ∈ zh, adr3 ∈ istore, as0 ⊆ dom nodes(istore), istore0 ⊑ istore, ¬ dups(nx), ∀ 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 < 0 → 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_io_save#(r0, adr1, istore0, ginval1, gstore2, gstore1, nx, maxino, ginval; adr0, zh, istore, pstate, syn; err)] ( refsize-cons(istore, as0 ∪ (err = ESUCCESS ⊃ ∅ ++ adr0;∅)) ∧ inv(istore) ∧ istore0 ⊑ istore ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore2) ∧ (pstate.index? → pstate.lnum ∈ istore) ∧ (pstate = unbuffered → syn) ∧ istore1 ⊑ istore ∧ r0 ∈ zh ∧ dom nodes(istore) = dom nodes(istore1) ∪ (err = ESUCCESS ⊃ ∅ ++ adr0;∅) ∧ (err = ESUCCESS → ¬ adr0 ∈ istore1) ∧ (( btree (rp, r0, (err = ESUCCESS ⊃ adr0;adr3), 0, err ≠ ESUCCESS, ri, nodes(istore), (err = ESUCCESS ⊃ ∅ ++ adr0;∅), (err = ESUCCESS ⊃ ∅ ++ adr0;∅ ++ adr3), ok) * P) )(zh) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → pstate.index? ∧ ¬ zh[r0].dirty) → (err = ESUCCESS → ¬ zh[r0].dirty ∧ pstate.index?) ∧ (∃ as, alladrs. refsize-cons(istore, as0 ∪ as) ∧ as ∩ dom nodes(istore1) = ∅ ∧ as ∩ as0 = ∅ ∧ alladrs ⊆ as ++ adr3 ∧ ((btree(rp, r0, (err = ESUCCESS ⊃ adr0;adr3), 0, err ≠ ESUCCESS, ri, nodes(istore) | as, as, alladrs, ok) * P))(zh)))

Rule argument

Additional information

Used simplifier rules: ⊦ ∅ -- adr = ∅; (s)% ⊦ (as ++ adr) -- adr = as -- adr; (s)% ⊦ mkznode(r, zbrar, boolvar, boolvar0, m).usedsize = m; (s)% ⊦ mkznode(r, zbrar, boolvar, boolvar0, m).dirty ↔ boolvar0; (s)% ⊦ ∅ ⊆ as; (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]%btree-adrs: ⊦ (( btree (rp, rp0, adr0, height, dirty, fi, iast, as, alladrs, nstat) * P) )(zh) → as ⊆ dom iast; (forward) from specification btree-inv% ⊦ {adr} = ∅ ++ adr; (s)% ⊦ ¬ adr ∈ ∅; (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)% ⊦ 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)%unc: ⊦ as ∪ as0 = as0 ∪ as; from specification set-union[node-store]%una: ⊦ (as ∪ as0) ∪ as1 = as ∪ as0 ∪ as1; from specification set-union[node-store]% ⊦ as ∪ ∅ = as; (s)% ⊦ adr ∈ nodes(istore) ↔ adr ∈ istore; (s)% ⊦ adr ∈ dom iast ↔ adr ∈ iast; (s)% ⊦ ∅ ++ adr ⊆ as ↔ adr ∈ as; (s)