Proof step 15 from proof validfield-put-statfield (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

  ⊦ validfield(str, r, sk, st) ↔ goodfieldandtype(r, sk, st) ∧ type∃(str, sk .fs .type) ∧ sk .fs .type ≠ void_type ∧ (is_reftype(sk .fs .type) → validrefval(str, st[r -- sk], sk .fs .type, st))

• Proof step 14:

  r ≠ jvmref ∨ sk ≠ sk0 ⊦ goodfieldandtype(r, sk0, st[jvmref -- sk, val]) ∧ type∃(str, sk0 .fs .type) ∧ sk0 .fs .type ≠ void_type ∧ (is_reftype(sk0 .fs .type) → validrefval(str, st[jvmref -- sk, val][r -- sk0], sk0 .fs .type, st[jvmref -- sk, val])) ↔ validfield(str, r, sk0, st)

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st[jvmref -- sk, val], sk0, r, str)]]