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

Heuristic nonrecursive calls applied rule call right

And obtained the following new goals

• Proof step 3:

  jvalid0 ↔ boolvar0, fi0 = ri, gstore = gstore1, gstore0 = gstore2, jro = ginval, lnum = n, nx = nx0, p_os = ns, pmaxino = maxino, inv(gstore2), n ∈ gstore2 ⊦ ⟪let gndx = [], jvalid = false in {index_read_gblock_nodes#(lnum, fi0, fi, jro, gstore0, gstore, nx, pmaxino, p_os, jvalid0; log, gndx; err); if err = ESUCCESS then while ¬ jvalid ∧ gndx ≠ [] do {/* (term-remove-nonend-blocks: invariant # gndx ≤ # log ∧ inv(gstore0) wfbound (jvalid ⊃ 0;# gndx)) */; if gndx.last.end then jvalid := true else {log := log.butlast; gndx := gndx.butlast}}}⟫ true, n ∈ ginval

Rule argument

Additional information

Used simplifier rules: remove-nonend-blocks: ⊦ ;