Proof step 13 from proof is_valid_ref-addobj-01 (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:

  ⊦ ¬ _type ∈ fis → (is_valid_ref(r, addobj(r, class, fis, st)) ↔ is_obj(r, addobj(r, class, fis, 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:

  ¬ _type ∈ fis ⊦ (addobj(r, class1, fis, st)[r -- _type]) = typeval(mkclasstype(class1))

• Proof step 12:

  is_obj(r, addobj(r, class, fis, st)), class+∃(str, class) ∧ ¬ is_abstract(class) ∨ is_array(str, r, addobj(r, class, fis, st)) ⊦ _type ∈ fis, is_obj(str, r, addobj(r, class, fis, st))

Rule argument

Additional information

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