Proof step 48 from proof validrefnotnull-union-at-right (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ r ≠ jvmref ∧ st[r -- _type] .type = mkclasstype(class) ∧ (∃ fs. fs ' ∈ instfields(st[r -- _type] .type .class) ∧ (is_reftype(fs .type) ∨ fs .type = abstract_type) ∧ st[r -- fs '] .refval ≠ jvmref ∧ (¬ is_referencevalue(st[r -- fs ']) ∨ ¬ st[r -- (fs ' + _type)] .type ≤ fs .type ∨ ¬ validref(str, st[r -- fs '] .refval, fs .type, st))) → ¬ validref(str, r, ty, st)

• Proof step 47:

  ¬ ( r ≠ jvmref ∧ st0[r -- _type] .type = mkclasstype(st0[r -- _type] .type .class) ∧ (∃ fs. fs ' ∈ instfields(st0[r -- _type] .type .class) ∧ (is_reftype(fs .type) ∨ fs .type = abstract_type) ∧ st0[r -- fs '] .refval ≠ jvmref ∧ (¬ is_referencevalue(st0[r -- fs ']) ∨ ¬ st0[r -- (fs ' + _type)] .type ≤ fs .type ∨ ¬ validref(str, st0[r -- fs '] .refval, fs .type, st0)))), is_fskey(sk), sk ∈ instfields(class), validref(str, r, mkclasstype(class), st0) ⊦ r = jvmref, st[r -- sk] = noval, r -- sk ∈ st0

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st0[r -- _type] .type .class, st0, mkclasstype(class), r, str)]]