Proof step 10 from proof contains-boolarray-01 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

  ⊦ tys ≠ [] → ( contains(str, ty ' + tys) ↔ type∃(str, ty) ∧ is_reftype(ty) ∧ (∃ ty1. ty1 ≤ ty ∧ type∃(str, ty1) ∧ (is_classtype(ty1) → ¬ interface∃(str, ty1 .class) ∧ (∃ fs. fs ' ∈ instfields(ty1 .class) ∧ tys .first ≤ fs .type)) ∧ (is_arraytype(ty1) → tys .first ≤ ty1 .type) ∧ contains(str, tys)))

• Proof step 9:

  tys ≠ [] ⊦ tys = [], type∃(str, mkarraytype(boolean_type)) ∧ is_reftype(mkarraytype(boolean_type)) ∧ (∃ ty1. ty1 ≤ mkarraytype(boolean_type) ∧ type∃(str, ty1) ∧ (is_classtype(ty1) → ¬ interface∃(str, ty1 .class) ∧ (∃ fs. fs ' ∈ instfields(ty1 .class) ∧ tys .first ≤ fs .type)) ∧ (is_arraytype(ty1) → tys .first ≤ ty1 .type) ∧ contains(str, tys)) ↔ tys = boolean_type '

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (tys, mkarraytype(boolean_type), str)]]