| zh[r0] = mkznode(r, zbrar, boolvar, true, m0), adr2 = adr1, istore1 = istore, pstate = index(m), remove-refsize0(gstore0) = gstore0, remove-refsize0(istore0) = istore0, elems nx ∩ ginval = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ ginval, ((btree(null, r0, adr1, height, dirty, ri, nodes(istore), as, alladrs, ok) * true))(zh), ((btree(null, null, adr1, height0, false, fi, nodes(istore0), alladrs0, alladrs0, ok) * true))(zh), ((btree(null, r0, adr1, height, dirty, ri, nodes(istore) | as, as, alladrs, ok) * true))(zh), inv(gstore \ ginval), inv(gstore0), inv(istore), inv(istore0), refsize-cons(istore, as), refsize-cons(istore0, alladrs0), m ∈ istore, adr1 ∈ istore, r0 ∈ zh, as ⊆ alladrs, as ⊆ dom nodes(istore), alladrs0 ⊆ dom nodes(istore), alladrs0 ⊆ dom nodes(istore0), alladrs ⊆ dom nodes(istore), istore0 ⊑ istore, ¬ dups(nx), ¬ adr1 ∈ as, height = 0 → as = ∅ ⊦ [btree_commit_rec#(r0, adr1, 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?) ∧ (∃ as0, alladrs1. refsize-cons(istore, as0) ∧ as0 ∩ dom nodes(istore1) ⊆ as ∧ alladrs1 ⊆ alladrs ∪ as0 ∧ ((btree(null, r0, (err = ESUCCESS ⊃ adr1;adr2), height, err ≠ ESUCCESS, ri, nodes(istore) | as0, as0, alladrs1, ok) * true))(zh)) → (err ≠ ESUCCESS → btree-inv(r0, adr2, istore, istore0, zh, ri, fi)) ∧ ( err = ESUCCESS → btree-inv(r0, adr1, istore, istore, zh, ri, ri) ∧ btree-inv (r0, adr2, istore[adr1.lnum, istore[adr1.lnum].ref-size:= (istore[adr1.lnum].ref-size - adr1.size)], istore0, zh[r0, zh[r0].dirty:= true], ri, fi) ∧ ¬ zh[r0].dirty)) |
zh[r0] = mkznode(r, zbrar, boolvar, true, m0), adr2 = adr1, istore1 = istore, pstate = index(m), remove-refsize0(istore0) = istore0, remove-refsize0(gstore0) = gstore0, elems nx ∩ ginval = ∅, dom gstore0 ∪ elems nx = dom gstore ∪ ginval, ((btree(null, r0, adr1, height, dirty, ri, nodes(istore) | as, as, alladrs, ok) * true))(zh), ((btree(null, null, adr1, height0, false, fi, nodes(istore0), alladrs0, alladrs0, ok) * true))(zh), ((btree(null, r0, adr1, height, dirty, ri, nodes(istore), as, alladrs, ok) * true))(zh), inv(istore0), inv(istore), inv(gstore0), inv(gstore \ ginval), refsize-cons(istore0, alladrs0), refsize-cons(istore, as), r0 ∈ zh, adr1 ∈ istore, m ∈ istore, alladrs ⊆ dom nodes(istore), alladrs0 ⊆ dom nodes(istore0), alladrs0 ⊆ dom nodes(istore), as ⊆ dom nodes(istore), as ⊆ alladrs, istore0 ⊑ istore, height = 0 → as = ∅ ⊦ dups(nx), adr1 ∈ as, ∀ 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?) ∧ (∃ as0, alladrs1. refsize-cons(istore, as0) ∧ as0 ∩ dom nodes(istore1) ⊆ as ∧ alladrs1 ⊆ alladrs ∪ as0 ∧ ((btree(null, r0, (err = ESUCCESS ⊃ adr1;adr2), height, err ≠ ESUCCESS, ri, nodes(istore) | as0, as0, alladrs1, ok) * true))(zh)) → (err ≠ ESUCCESS → btree-inv(r0, adr2, istore, istore0, zh, ri, fi)) ∧ ( err = ESUCCESS → btree-inv(r0, adr1, istore, istore, zh, ri, ri) ∧ btree-inv (r0, adr2, istore[adr1.lnum, istore[adr1.lnum].ref-size:= (istore[adr1.lnum].ref-size - adr1.size)], istore0, zh[r0, zh[r0].dirty:= true], ri, fi) ∧ ¬ zh[r0].dirty)