Proof step 11 from proof is_array-union-disjoint (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:

  ⊦ st1 .refs ∩ st .refs = ∅ ∧ r ∈ st1 ∧ is_array(r, st1) → is_array(r, st1 ∪ st)

• Proof step 10:

  st1 .refs ∩ st .refs = ∅, r ∈ st1, type∃(str, st1[r -- _type] .type), is_array(r, st1), ¬ type∃(str, (st1 ∪ st)[r -- _type] .type) ∨ (st1 ∪ st)[r -- _type] .type .jtelemtype = void_type ∨ (st1 ∪ st)[r -- _type] .type .jtelemtype = abstract_type ⊦ st1[r -- _type] .type .jtelemtype = void_type, st1[r -- _type] .type .jtelemtype = abstract_type

Rule argument

Additional information

[[CONCRETESIMPRULES : ([CSIMPSEQ : ⊦ rset ∩ rset0 = rset0 ∩ rset], [CSIMPSEQ : ⊦ (rset ∩ rset0) ∩ rset1 = rset ∩ rset0 ∩ rset1])]]