Proof step 18 from proof is_array-norefval (conclusion)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 1:

  ⊦ is_array(str, r, st) ↔ type∃(str, st[r -- _type] .type) ∧ st[r -- _type] .type .jtelemtype ≠ void_type ∧ st[r -- _type] .type .jtelemtype ≠ abstract_type ∧ is_array(r, st)

• Proof step 17:

  is_reftype(st[r -- _type] .type .type), i < st[r -- _length] .intval, type∃(str, st[r -- _type] .type), is_array(r, st), 0 ≤ i, 0 < st[r -- _length] .intval ⊦ st[r -- _type] .type .jtelemtype = abstract_type, st[r -- _type] .type .jtelemtype = void_type, is_referencevalue(st[r -- i '])

Rule argument

Additional information

[[CONCRETESIMPRULES : ([CSIMPFORWARD : ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j], [CSIMPFORWARD : ⊦ i < j ∧ 0 ≤ i → 0 < j])]]