| adr = adr2, err1 = err, ginval = ginval2, ginval0 = ginval3, ginval1 = ginval6, gstore = gstore1, gstore0 = crash(gstore4, gstore1, ginval3, nx1), istore = istore1, istore0 = remove-refsize0(crash(istore2, istore1)), maxino = maxino1, maxino0 = maxino3, nx = nx1, nx0 = nx3, remove-refsize0(gstore1) = gstore1, remove-refsize0(istore1) = istore1, elems nx1 ∩ ginval3 = ∅, dom gstore1 ∪ elems nx1 = dom gstore4 ∪ ginval3, btree-inv(rp1, adr2, istore2, istore1, zh, fi, fi0), btree-inv(rp1, adr2, istore2, istore1, zh, ri, fi3), inv(gstore4 \ ginval3), inv(gstore1), inv(istore2), inv(istore1), ri-inj(fi), ri-inj(fi0), istore1 ⊑ istore2, pstate1.journal? → nx1 ≠ [] ∧ pstate1.lnum = nx1.last ∧ pstate1.lnum ∈ gstore4, pstate1.index? → pstate1.lnum ∈ istore2, ⌊err⌋ ∨ err = ESUCCESS ⊦ [if err1 = ESUCCESS then pstate := unbuffered, syn := true, adr0 := adr, maxino0 := maxino, nx0 := nx, ginval1 := ginval else pstate := ?, syn := ?, adr := ?, istore0 := ?, istore := ?, ginval0 := ?, gstore0 := ?, gstore := ?, nx := ?, maxino := ?, ginval := ?, adr0 := ?, maxino0 := ?, nx0 := ?, ginval1 := ?] ( ( err1 = ESUCCESS → syn ∧ inv(gstore0 \ ginval0) ∧ inv(gstore) ∧ elems nx ∩ ginval0 = ∅ ∧ ¬ dups(nx) ∧ dom gstore ∪ elems nx = dom gstore0 ∪ ginval0 ∧ 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⟫ ( ( err1 = ESUCCESS → (∃ fi3, syn0. ⟨gstore3 := crash(gstore4, gstore1, ginval3, nx1); index+persistence_recover#(; maxino3, nx3, ginval6, fi3, fi0, ginval3, gstore3, gstore1, nx1, maxino1, ginval2, syn0; err0)⟩ ( ginval3 = ginval0 ∧ gstore3 = gstore0 ∧ gstore1 = gstore ∧ nx1 = nx ∧ maxino1 = maxino ∧ ginval2 = ginval ∧ btree-inv(rp, adr, istore0, istore, zh0, fi3, fi0) ∧ (syn0 ↔ syn) ∧ maxino0 = maxino3 ∧ nx0 = nx3 ∧ ginval1 = ginval6 ∧ ESUCCESS = err0))) ∧ ( err1 ≠ ESUCCESS → (∀ fi, fi0, ginval, gstore, gstore0, nx, maxino, ginval0, syn. ⟨index+persistence_recover#(; maxino3, nx3, ginval6, fi1, fi2, ginval7, gstore5, gstore6, nx4, maxino4, ginval8, syn2; err0)⟩ ( fi = fi1 ∧ fi0 = fi2 ∧ ginval = ginval7 ∧ gstore = gstore5 ∧ gstore0 = gstore6 ∧ nx = nx4 ∧ maxino = maxino4 ∧ ginval0 = ginval8 ∧ (syn ↔ syn2) ∧ maxino0 = maxino3 ∧ nx0 = nx3 ∧ ginval1 = ginval6 ∧ err1 = err0))))), dups(nx1) |
adr = adr2, err1 = ESUCCESS, err1 = err, ginval = ginval2, ginval0 = ginval3, ginval1 = ginval6, gstore = gstore1, gstore0 = crash(gstore4, gstore1, ginval3, nx1), istore = istore1, istore0 = remove-refsize0(crash(istore2, istore1)), maxino = maxino1, maxino0 = maxino3, nx = nx1, nx0 = nx3, remove-refsize0(istore1) = istore1, remove-refsize0(gstore1) = gstore1, elems nx1 ∩ ginval3 = ∅, dom gstore1 ∪ elems nx1 = dom gstore4 ∪ ginval3, btree-inv(rp1, adr2, istore2, istore1, zh, ri, fi3), btree-inv(rp1, adr2, istore2, istore1, zh, fi, fi0), inv(istore1), inv(istore2), inv(gstore1), inv(gstore4 \ ginval3), ri-inj(fi0), ri-inj(fi), istore1 ⊑ istore2, pstate1.index? → pstate1.lnum ∈ istore2, pstate1.journal? → nx1 ≠ [] ∧ pstate1.lnum = nx1.last ∧ pstate1.lnum ∈ gstore4, ⌊err⌋ ∨ err = ESUCCESS ⊦ [pstate := unbuffered, syn := true, adr0 := adr, maxino0 := maxino, nx0 := nx, ginval1 := ginval] ( ( err1 = ESUCCESS → syn ∧ inv(gstore0 \ ginval0) ∧ inv(gstore) ∧ elems nx ∩ ginval0 = ∅ ∧ ¬ dups(nx) ∧ dom gstore ∪ elems nx = dom gstore0 ∪ ginval0 ∧ 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⟫ ( ( err1 = ESUCCESS → (∃ fi3, syn0. ⟨gstore3 := crash(gstore4, gstore1, ginval3, nx1); index+persistence_recover#(; maxino3, nx3, ginval6, fi3, fi0, ginval3, gstore3, gstore1, nx1, maxino1, ginval2, syn0; err0)⟩ ( ginval3 = ginval0 ∧ gstore3 = gstore0 ∧ gstore1 = gstore ∧ nx1 = nx ∧ maxino1 = maxino ∧ ginval2 = ginval ∧ btree-inv(rp, adr, istore0, istore, zh0, fi3, fi0) ∧ (syn0 ↔ syn) ∧ maxino0 = maxino3 ∧ nx0 = nx3 ∧ ginval1 = ginval6 ∧ ESUCCESS = err0))) ∧ ( err1 ≠ ESUCCESS → (∀ fi, fi0, ginval, gstore, gstore0, nx, maxino, ginval0, syn. ⟨index+persistence_recover#(; maxino3, nx3, ginval6, fi1, fi2, ginval7, gstore5, gstore6, nx4, maxino4, ginval8, syn2; err0)⟩ ( fi = fi1 ∧ fi0 = fi2 ∧ ginval = ginval7 ∧ gstore = gstore5 ∧ gstore0 = gstore6 ∧ nx = nx4 ∧ maxino = maxino4 ∧ ginval0 = ginval8 ∧ (syn ↔ syn2) ∧ maxino0 = maxino3 ∧ nx0 = nx3 ∧ ginval1 = ginval6 ∧ err1 = err0))))), dups(nx1)
adr = adr2, err1 = err, ginval = ginval2, ginval0 = ginval3, ginval1 = ginval6, gstore = gstore1, gstore0 = crash(gstore4, gstore1, ginval3, nx1), istore = istore1, istore0 = remove-refsize0(crash(istore2, istore1)), maxino = maxino1, maxino0 = maxino3, nx = nx1, nx0 = nx3, remove-refsize0(istore1) = istore1, remove-refsize0(gstore1) = gstore1, elems nx1 ∩ ginval3 = ∅, dom gstore1 ∪ elems nx1 = dom gstore4 ∪ ginval3, btree-inv(rp1, adr2, istore2, istore1, zh, ri, fi3), btree-inv(rp1, adr2, istore2, istore1, zh, fi, fi0), inv(istore1), inv(istore2), inv(gstore1), inv(gstore4 \ ginval3), ri-inj(fi0), ri-inj(fi), istore1 ⊑ istore2, pstate1.index? → pstate1.lnum ∈ istore2, pstate1.journal? → nx1 ≠ [] ∧ pstate1.lnum = nx1.last ∧ pstate1.lnum ∈ gstore4, ⌊err⌋ ∨ err = ESUCCESS ⊦ [pstate := ?, syn := ?, adr := ?, istore0 := ?, istore := ?, ginval0 := ?, gstore0 := ?, gstore := ?, nx := ?, maxino := ?, ginval := ?, adr0 := ?, maxino0 := ?, nx0 := ?, ginval1 := ?] ( ( err1 = ESUCCESS → syn ∧ inv(gstore0 \ ginval0) ∧ inv(gstore) ∧ elems nx ∩ ginval0 = ∅ ∧ ¬ dups(nx) ∧ dom gstore ∪ elems nx = dom gstore0 ∪ ginval0 ∧ 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⟫ ( ( err1 = ESUCCESS → (∃ fi3, syn0. ⟨gstore3 := crash(gstore4, gstore1, ginval3, nx1); index+persistence_recover#(; maxino3, nx3, ginval6, fi3, fi0, ginval3, gstore3, gstore1, nx1, maxino1, ginval2, syn0; err0)⟩ ( ginval3 = ginval0 ∧ gstore3 = gstore0 ∧ gstore1 = gstore ∧ nx1 = nx ∧ maxino1 = maxino ∧ ginval2 = ginval ∧ btree-inv(rp, adr, istore0, istore, zh0, fi3, fi0) ∧ (syn0 ↔ syn) ∧ maxino0 = maxino3 ∧ nx0 = nx3 ∧ ginval1 = ginval6 ∧ ESUCCESS = err0))) ∧ ( err1 ≠ ESUCCESS → (∀ fi, fi0, ginval, gstore, gstore0, nx, maxino, ginval0, syn. ⟨index+persistence_recover#(; maxino3, nx3, ginval6, fi1, fi2, ginval7, gstore5, gstore6, nx4, maxino4, ginval8, syn2; err0)⟩ ( fi = fi1 ∧ fi0 = fi2 ∧ ginval = ginval7 ∧ gstore = gstore5 ∧ gstore0 = gstore6 ∧ nx = nx4 ∧ maxino = maxino4 ∧ ginval0 = ginval8 ∧ (syn ↔ syn2) ∧ maxino0 = maxino3 ∧ nx0 = nx3 ∧ ginval1 = ginval6 ∧ err1 = err0))))), err1 = ESUCCESS, dups(nx1)