Proof step 18 from proof compatval-put (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 2:

  ⊦ compat(str, val, ty, st) ↔ okval(val, ty) ∧ ( is_referencevalue(val) ∧ val .refval ≠ jvmref → val .refval -- _type ∈ st ∧ is_typevalue(st[val .refval -- _type]) ∧ is_reftype(st[val .refval -- _type] .type) ∧ (has_classtype(st[val .refval -- _type] .type) → tdname+∃(str, st[val .refval -- _type] .type .jtelemtype .class)) ∧ (is_classtype(st[val .refval -- _type] .type) → class+∃(str, st[val .refval -- _type] .type .class)) ∧ asgcomp(str, val, ty, st))

• Proof step 17:

  compat(str, val, ty, st), is_referencevalue(val) ⊦ ty0 = void_type, okval(val, ty) ∧ ( is_referencevalue(val) ∧ val .refval ≠ jvmref → val .refval -- _type ∈ st[r -- mkfs(class, ty0, fieldvar) ', val0] ∧ is_typevalue(st[r -- mkfs(class, ty0, fieldvar) ', val0][val .refval -- _type]) ∧ is_reftype((st[r -- mkfs(class, ty0, fieldvar) ', val0][val .refval -- _type]) .type) ∧ ( has_classtype((st[r -- mkfs(class, ty0, fieldvar) ', val0][val .refval -- _type]) .type) → tdname+∃(str, (st[r -- mkfs(class, ty0, fieldvar) ', val0][val .refval -- _type]) .type .jtelemtype .class)) ∧ ( is_classtype((st[r -- mkfs(class, ty0, fieldvar) ', val0][val .refval -- _type]) .type) → class+∃(str, (st[r -- mkfs(class, ty0, fieldvar) ', val0][val .refval -- _type]) .type .class)) ∧ asgcomp(str, val, ty, st[r -- mkfs(class, ty0, fieldvar) ', val0]))

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st[r -- mkfs(class, ty0, fieldvar) ', val0], ty, val, str)]]