Proof step 13 from proof is_valid_ref-primarray (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) ↔ class+∃(str, st[r -- _type] .type .class) ∧ ¬ is_abstract(st[r -- _type] .type .class) ∧ is_obj(r, st)

• Proof step 12:

  st[r -- _type] = typeval(mkarraytype(ty)), is_primtype(ty) ⊦ is_valid_ref(r, st) ∧ (class+∃(str, mkarraytype(ty) .class) ∧ ¬ is_abstract(mkarraytype(ty) .class) ∧ is_obj(r, st) ∨ is_array(str, r, st)) ↔ is_array(r, st)

Rule argument

Additional information

[[CONCRETESIMPRULES : ([CSIMPSEQ : ⊦ typeval(ty) .type = ty])]]