Proof step 23 from proof term-remove-nonend-blocks (previous step)

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 24:

  jvalid ↔ jvalid0, jvalid1 ↔ false, ax = ax0 + gstore2[n].ladrlist.to-adr(n), err = ESUCCESS, err = err0, gndx = gndx1, gndx0 = [], gndx2 = gndx0 + gstore2[n].gndlist, ¬ jvalid, log0 = ax, gndx.last.end, inv(gstore2), n ∈ gstore2, # gndx ≤ # log, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪jvalid := true⟫ ((# gndx ≤ # log ∧ inv(gstore2)) ∧ (jvalid ⊃ 0;# gndx) < (jvalid0 ⊃ 0;# gndx1)), gndx = [], n ∈ ginval

• Proof step 25:

  jvalid ↔ jvalid0, jvalid1 ↔ false, ax = ax0 + gstore2[n].ladrlist.to-adr(n), err = ESUCCESS, err = err0, gndx = gndx1, gndx0 = [], gndx2 = gndx0 + gstore2[n].gndlist, ¬ jvalid, log0 = ax, inv(gstore2), n ∈ gstore2, # gndx ≤ # log, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪log := log.butlast; gndx := gndx.butlast⟫ ((# gndx ≤ # log ∧ inv(gstore2)) ∧ (jvalid ⊃ 0;# gndx) < (jvalid0 ⊃ 0;# gndx1)), gndx = [], gndx.last.end, n ∈ ginval

• Proof step 27:

  jvalid ↔ jvalid0, jvalid1 ↔ false, ax = ax0 + gstore2[n].ladrlist.to-adr(n), err = ESUCCESS, err = err0, gndx = [], gndx = gndx1, gndx0 = [], gndx2 = gndx0 + gstore2[n].gndlist, ¬ jvalid, log0 = ax, inv(gstore2), n ∈ gstore2, # gndx ≤ # log, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ gndx = [], n ∈ ginval

Rule argument

Additional information