Proof step 17 from proof compatrefs-mode (conclusion)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

  ⊦ compatrefs(str, st) ↔ (∀ r. r ≠ jvmref ∧ r -- _type ∈ st ∧ is_typevalue(st[r -- _type]) → (is_classtype(st[r -- _type] .type) ∧ class+∃(str, st[r -- _type] .type .class) → compatobj(str, r, st)) ∧ ( is_arraytype(st[r -- _type] .type) ∧ (¬ has_classtype(st[r -- _type] .type) ∨ tdname+∃(str, st[r -- _type] .type .jtelemtype .class)) → compatarray(str, r, st)))

• Proof step 16:

  ⊦ (∀ r. r ≠ jvmref ∧ r -- _type ∈ st[_mode, val] ∧ is_typevalue(st[_mode, val][r -- _type]) → ( is_classtype((st[_mode, val][r -- _type]) .type) ∧ class+∃(str, (st[_mode, val][r -- _type]) .type .class) → compatobj(str, r, st[_mode, val])) ∧ ( is_arraytype((st[_mode, val][r -- _type]) .type) ∧ (¬ has_classtype((st[_mode, val][r -- _type]) .type) ∨ tdname+∃(str, (st[_mode, val][r -- _type]) .type .jtelemtype .class)) → compatarray(str, r, st[_mode, val]))) ↔ compatrefs(str, st)

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st[_mode, val], str)]]