Proof step 9 from proof is_valid_ref-update (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 3:

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

• Proof step 8:

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

Rule argument

Additional information

[[CONCRETESIMPRULES : ([CSIMPSEQ : ⊦ r ≠ r0 → (update(r0, fis, st)[r -- sk]) = st[r -- sk]])]]