Proof step 5 from proof is_array-update (conclusion)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 1:

  ⊦ is_array(str, r, st) ↔ type∃(str, st[r -- _type] .type) ∧ st[r -- _type] .type .jtelemtype ≠ void_type ∧ st[r -- _type] .type .jtelemtype ≠ abstract_type ∧ is_array(r, st)

• Proof step 2:

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

• Proof step 3:

  ⊦ r ≠ r0 → (is_array(r, update(r0, fis, st)) ↔ is_array(r, st))

• Proof step 4:

  ⊦ is_array(str, r, st) ↔ ¬ ¬ ( type∃(str, st[r -- _type] .type) ∧ st[r -- _type] .type .jtelemtype ≠ void_type ∧ st[r -- _type] .type .jtelemtype ≠ abstract_type ∧ is_array(r, st))

Rule argument

Additional information

[[CONCRETESIMPRULES : ()]]