| adr1 = adr2, err = err0, ginval4 = ginval2, ginval5 = ginval3, gstore3 = crash(gstore2, gstore1, ginval2, nx1), gstore4 = gstore1, istore3 = remove-refsize0(crash(istore2, istore1)), istore4 = istore1, remove-refsize0(istore1) = istore1, remove-refsize0(gstore1) = gstore1, elems nx1 ∩ ginval2 = ∅, dom gstore1 ∪ elems nx1 = dom gstore2 ∪ ginval2, btree-inv(rp, adr2, istore2, istore1, zh, ri, fi), inv(istore1), inv(istore2), inv(gstore1), inv(gstore2 \ ginval2), istore1 ⊑ istore2, err = ESUCCESS → syn ∧ inv(gstore0 \ ginval) ∧ inv(gstore) ∧ elems nx ∩ ginval = ∅ ∧ ¬ dups(nx) ∧ dom gstore ∪ elems nx = dom gstore0 ∪ ginval ∧ remove-refsize0(gstore) = gstore ∧ inv(istore0) ∧ inv(istore) ∧ istore ⊑ istore0 ∧ remove-refsize0(istore) = istore ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore0) ∧ (pstate.index? → pstate.lnum ∈ istore0), pstate1.index? → pstate1.lnum ∈ istore2, pstate1.journal? → nx1 ≠ [] ∧ pstate1.lnum = nx1.last ∧ pstate1.lnum ∈ gstore2, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪rp := null⟫ ( err = ESUCCESS → syn ∧ (∃ ri, fi. btree-inv(rp, adr, istore0, istore, zh0, ri, fi)) ∧ inv(gstore0 \ ginval) ∧ inv(gstore) ∧ elems nx ∩ ginval = ∅ ∧ ¬ dups(nx) ∧ dom gstore ∪ elems nx = dom gstore0 ∪ ginval ∧ remove-refsize0(gstore) = gstore ∧ inv(istore0) ∧ inv(istore) ∧ istore ⊑ istore0 ∧ remove-refsize0(istore) = istore ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore0) ∧ (pstate.index? → pstate.lnum ∈ istore0)), err = ESUCCESS, dups(nx1) |