| adr = adr0, istore = remove-refsize0(crash(istore0, istore1)), istore2 = istore1, ginval1 = ginval2, gstore1 = crash(gstore2, gstore3, ginval2, nx0), gstore4 = gstore3, nx1 = nx0, maxino0 = maxino1, ginval3 = ginval4, ginval5 = ginval2, gstore5 = gstore2, gstore6 = gstore3, nx2 = nx0, maxino2 = maxino1, ginval6 = ginval4, btree-inv(rp, adr0, istore0, istore1, zh, fi1, fi2), ri = fi1, fi3 = fi2, syn0 ↔ syn1, syn1, inv-journal(nx2, gstore5, gstore6, ginval5), ri-inj(fi1), ri-inj(fi2), btree-inv(rp, adr0, istore0, istore1, zh, ri, fi3), inv-journal(nx0, gstore2, gstore3, ginval2), inv-index(istore0, istore1), inv-state(pstate, nx0, gstore2, istore0, syn1), maxino3 = maxino4, nx3 = nx4, ginval7 = ginval8 ⊦ ⟪btree_recover#(; maxino3, nx3, ginval7, adr1, adr, istore, istore2, ginval1, gstore1, gstore4, nx1, maxino0, ginval3, pstate0, syn2; rp0, err)⟫ ( ( err = ESUCCESS → (∃ fi, fi0, ginval, gstore, gstore0, nx, maxino, ginval0, syn. ( ginval = ginval5 ∧ gstore = crash(gstore5, gstore6, ginval5, nx2) ∧ gstore0 = gstore6 ∧ nx = nx2 ∧ maxino = maxino2 ∧ ginval0 = ginval6 ∧ fi0 = fi2) ∧ ⟨index_recover#(; maxino4, nx4, ginval8, fi0, nx, maxino, ginval0, ginval, gstore, gstore0; fi, syn, err0)⟩ ( ( ginval = ginval1 ∧ gstore = gstore1 ∧ gstore0 = gstore4 ∧ nx = nx1 ∧ maxino = maxino0 ∧ ginval0 = ginval3 ∧ btree-inv(rp0, adr, istore, istore2, zh0, fi, fi0) ∧ ri0 = fi ∧ fi4 = fi0 ∧ (syn ↔ syn2)) ∧ maxino3 = maxino4 ∧ nx3 = nx4 ∧ ginval7 = ginval8 ∧ err = err0))) ∧ ( err ≠ ESUCCESS → (∀ fi, fi0, ginval, gstore, gstore0, nx, maxino, ginval0, syn. ⟨index_recover#(; maxino4, nx4, ginval8, fi5, nx5, maxino5, ginval9, ginval10, gstore7, gstore8; fi6, syn3, err0)⟩ ( fi = fi6 ∧ fi0 = fi5 ∧ ginval = ginval10 ∧ gstore = gstore7 ∧ gstore0 = gstore8 ∧ nx = nx5 ∧ maxino = maxino5 ∧ ginval0 = ginval9 ∧ (syn ↔ syn3) ∧ maxino3 = maxino4 ∧ nx3 = nx4 ∧ ginval7 = ginval8 ∧ err = err0)))) |