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

User applied rule invariant right

And obtained the following new goals

• Proof step 15:

  zh[r0] = mkznode(r1, zbrar, false, true, m0), err = ESUCCESS, gstore0 = gstore2, istore1 = istore, n = 0, pstate = index(m), r = r0, remove-refsize0(gstore1) = gstore1, remove-refsize0(istore0) = istore0, as ∩ as0 = ∅, elems nx ∩ ginval1 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval1, ((btree(rp, r0, adr3, height, dirty, ri, nodes(istore) | as, as, alladrs, ok) * P))(zh), inv(gstore2 \ ginval1), inv(gstore1), inv(istore), inv(istore0), refsize-cons(istore, as0 ∪ as), r0 ∈ zh, m ∈ istore, as ⊆ dom nodes(istore), as ⊆ alladrs, alladrs ⊆ dom nodes(istore), as0 ⊆ dom nodes(istore), istore0 ⊑ istore, 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))) ⊦ commit-inv(n, pstate, istore1, istore0, nx, gstore2, gstore1, ginval1, syn, err, rp, r, adr3, height, dirty, ri, istore, as, as0, alladrs, P, zh), dups(nx), adr3 ∈ as

• Proof step 20:

  zh1[r0] = mkznode(r1, zbrar, false, true, m0), err = ESUCCESS, err0 = ESUCCESS, gstore0 = gstore2, istore1 = istore2, n = n0, n1 = 0, pstate0 = index(m), r = r0, remove-refsize0(gstore1) = gstore1, remove-refsize0(istore0) = istore0, zh = zh0, as ∩ as0 = ∅, elems nx ∩ ginval1 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval1, ((btree(rp, r0, adr3, height, dirty, ri, nodes(istore2) | as, as, alladrs, ok) * P))(zh1), n < zh[r].usedsize, commit-inv(n, pstate, istore1, istore0, nx, gstore2, gstore1, ginval1, syn, err, rp, r, adr3, height, dirty, ri, istore, as, as0, alladrs, P, zh), inv(gstore2 \ ginval1), inv(gstore1), inv(istore2), inv(istore0), refsize-cons(istore2, as0 ∪ as), r0 ∈ zh1, m ∈ istore2, as ⊆ dom nodes(istore2), as ⊆ alladrs, alladrs ⊆ dom nodes(istore2), as0 ⊆ dom nodes(istore2), istore0 ⊑ istore2, 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))) ⊦ ⟪let adr = zh[r].zbranches[n].adr, rc = zh[r].zbranches[n].child in if rc ≠ null ∧ zh[rc].dirty then {btree_commit_rec#(rc, adr1, istore0, ginval1, gstore0, gstore1, nx, maxino, ginval; adr, err, zh, istore, pstate, syn); if err = ESUCCESS then zh[r].zbranches[n].adr := adr}; n := n + 1⟫ ( commit-inv (n, pstate, istore1, istore0, nx, gstore2, gstore1, ginval1, syn, err, rp, r, adr3, height, dirty, ri, istore, as, as0, alladrs, P, zh) ∧ zh[r].usedsize - n < zh0[r].usedsize - n0), dups(nx), adr3 ∈ as

• Proof step 168:

  zh1[r0] = mkznode(r1, zbrar, false, true, m0), err0 = ESUCCESS, gstore0 = gstore2, istore1 = istore2, n1 = 0, pstate0 = index(m), r = r0, remove-refsize0(gstore1) = gstore1, remove-refsize0(istore0) = istore0, as ∩ as0 = ∅, elems nx ∩ ginval1 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval1, ((btree(rp, r0, adr3, height, dirty, ri, nodes(istore2) | as, as, alladrs, ok) * P))(zh1), commit-inv(n, pstate, istore1, istore0, nx, gstore2, gstore1, ginval1, syn, err, rp, r, adr3, height, dirty, ri, istore, as, as0, alladrs, P, zh), inv(gstore2 \ ginval1), inv(gstore1), inv(istore2), inv(istore0), refsize-cons(istore2, as0 ∪ as), r0 ∈ zh1, m ∈ istore2, as ⊆ dom nodes(istore2), as ⊆ alladrs, alladrs ⊆ dom nodes(istore2), as0 ⊆ dom nodes(istore2), istore0 ⊑ istore2, 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))) ⊦ ⟪adr0 := adr3; if err = ESUCCESS then btree_io_save#(r, adr1, istore0, ginval1, gstore0, gstore1, nx, maxino, ginval; adr0, zh, istore, pstate, syn; err)⟫ ( istore1 ⊑ istore ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore2) ∧ (pstate.index? → pstate.lnum ∈ istore) ∧ (pstate = unbuffered → syn) ∧ 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 ⊃ adr0;adr3), height, err ≠ ESUCCESS, ri, nodes(istore) | as1, as1, alladrs1, ok) * P))(zh))), dups(nx), adr3 ∈ as, n < zh[r].usedsize ∧ err = ESUCCESS

Rule argument

Additional information

Used formulas: commit-inv (n, pstate, istore1, istore0, nx, gstore2, gstore1, ginval1, syn, err, rp, r, adr3, height, dirty, ri, istore, as, as0, alladrs, P, zh), zh[r].usedsize - n = zh[r].usedsize - n