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

  ⊦ r ≠ r0 → (is_valid_ref(r, addobj(r0, class, fis, st)) ↔ is_valid_ref(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:

  ⊦ r ≠ r0 → (addobj(r, class1, fis, st)[r0 -- sk]) = st[r0 -- sk]

• Proof step 5:

  ⊦ r ≠ r0 → (is_obj(r, addobj(r0, class, fis, st)) ↔ is_obj(r, st))

• Proof step 6:

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

• Proof step 17:

  ⊦ r = r0, is_valid_ref(r, st) ∧ ( class+∃(str, st[r -- _type] .type .class) ∧ ¬ is_abstract(st[r -- _type] .type .class) ∧ is_obj(r, st) ∨ is_array(str, r, addobj(r0, class, fis, st))) ↔ is_obj(str, r, st) ∨ is_array(str, r, st)

Rule argument

Additional information

[[CONCRETESIMPRULES : ()]]