| adr = adr2, err = err0, ginval = ginval2, ginval0 = ginval3, gstore = gstore1, gstore0 = crash(gstore2, gstore1, ginval2, nx), istore = istore1, istore0 = remove-refsize0(crash(istore2, istore1)), remove-refsize0(istore1) = istore1, remove-refsize0(gstore1) = gstore1, elems nx ∩ ginval2 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval2, btree-inv(rp, adr2, istore2, istore1, zh, ri, fi), inv(istore1), inv(istore2), inv(gstore1), inv(gstore2 \ ginval2), istore1 ⊑ istore2, pstate1.index? → pstate1.lnum ∈ istore2, pstate1.journal? → nx ≠ [] ∧ pstate1.lnum = nx.last ∧ pstate1.lnum ∈ gstore2, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ [if err = ESUCCESS then pstate := unbuffered, syn := true, adr0 := adr, maxino0 := maxino, nx0 := nx, ginval1 := ginval0 else pstate := ?, syn := ?, adr := ?, istore0 := ?, istore := ?, ginval := ?, gstore0 := ?, gstore := ?, nx := ?, maxino := ?, ginval0 := ?, adr0 := ?, maxino0 := ?, nx0 := ?, ginval1 := ?] ( ( 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)) → ⟪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))), dups(nx) |
adr = adr2, err = ESUCCESS, err = err0, ginval = ginval2, ginval0 = ginval3, gstore = gstore1, gstore0 = crash(gstore2, gstore1, ginval2, nx), istore = istore1, istore0 = remove-refsize0(crash(istore2, istore1)), remove-refsize0(gstore1) = gstore1, remove-refsize0(istore1) = istore1, elems nx ∩ ginval2 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval2, btree-inv(rp, adr2, istore2, istore1, zh, ri, fi), inv(gstore2 \ ginval2), inv(gstore1), inv(istore2), inv(istore1), istore1 ⊑ istore2, pstate1.journal? → nx ≠ [] ∧ pstate1.lnum = nx.last ∧ pstate1.lnum ∈ gstore2, pstate1.index? → pstate1.lnum ∈ istore2, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ [pstate := unbuffered, syn := true, adr0 := adr, maxino0 := maxino, nx0 := nx, ginval1 := ginval0] ( ( 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)) → ⟪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))), dups(nx)
adr = adr2, err = err0, ginval = ginval2, ginval0 = ginval3, gstore = gstore1, gstore0 = crash(gstore2, gstore1, ginval2, nx), istore = istore1, istore0 = remove-refsize0(crash(istore2, istore1)), remove-refsize0(gstore1) = gstore1, remove-refsize0(istore1) = istore1, elems nx ∩ ginval2 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval2, btree-inv(rp, adr2, istore2, istore1, zh, ri, fi), inv(gstore2 \ ginval2), inv(gstore1), inv(istore2), inv(istore1), istore1 ⊑ istore2, pstate1.journal? → nx ≠ [] ∧ pstate1.lnum = nx.last ∧ pstate1.lnum ∈ gstore2, pstate1.index? → pstate1.lnum ∈ istore2, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ [pstate := ?, syn := ?, adr := ?, istore0 := ?, istore := ?, ginval := ?, gstore0 := ?, gstore := ?, nx := ?, maxino := ?, ginval0 := ?, adr0 := ?, maxino0 := ?, nx0 := ?, ginval1 := ?] ( ( 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)) → ⟪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(nx)