Proof step 27 from proof isvalidref-put-array-badindex (conclusion)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 1:

  ⊦ is_valid_ref(str, r, st) ↔ ¬ ¬ (is_valid_ref(r, st) ∧ (is_obj(str, r, st) ∨ is_array(str, r, st)))

• Proof step 2:

  ⊦ is_obj(str, r, st[r0 -- i ', val]) ↔ is_obj(str, r, st)

• Proof step 3:

  ⊦ is_obj(str, r, st) ↔ class+∃(str, st[r -- _type] .type .class) ∧ ¬ is_abstract(st[r -- _type] .type .class) ∧ is_obj(r, st)

• Proof step 4:

  ⊦ is_valid_ref(str, r, st) ↔ is_obj(str, r, st) ∨ is_array(str, r, st)

• Proof step 26:

  i < 0 ⊦ is_valid_ref(r0, st[r -- i ', val]) ∧ (class+∃(str, st[r0 -- _type] .type .class) ∧ ¬ is_abstract(st[r0 -- _type] .type .class) ∧ is_obj(r0, st) ∨ is_array(str, r0, st[r -- i ', val])) ↔ is_obj(str, r0, st) ∨ is_array(str, r0, st)

Rule argument

Additional information

[[CONCRETESIMPRULES : ([CSIMPNAMEDFORWARD : int-abs, , forward-le-02, ⊦ j < i ∧ i ≤ 0 → j < 0])]]