Proof step 7 from proof contains-array (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

  ⊦ contains(str, ty ' + ty0 ' + 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) ∧ ty0 ≤ fs .type)) ∧ (is_arraytype(ty1) → ty0 ≤ ty1 .type) ∧ contains(str, ty0 ' + tys))

• Proof step 6:

  type∃(str, mkarraytype(ty)) ∧ is_reftype(mkarraytype(ty)) ∧ (∃ ty1. ty1 ≤ mkarraytype(ty) ∧ type∃(str, ty1) ∧ (is_classtype(ty1) → ¬ interface∃(str, ty1 .class) ∧ (∃ fs. fs ' ∈ instfields(ty1 .class) ∧ ty0 ≤ fs .type)) ∧ (is_arraytype(ty1) → ty0 ≤ ty1 .type) ∧ contains(str, ty0 ' + tys0)) ⊦ contains(str, ty ' + tys0)

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (tys0, ty0, mkarraytype(ty), str)]]