Proof step 12 from proof validstatfield-validref (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 2:

  ⊦ validstatfield(str, sk, st) ↔ is_fskey(sk) ∧ sk ∈ statfields(sk .fs .class) ∧ tdname∃(str, sk .fs .class) ∧ (initdone(sk .fs .class, st) → validfield(str, jvmref, sk, st))

• Proof step 11:

  sk .fs = mkfs(class, ty, fieldvar), st[jvmref -- sk] = refval(r), is_fskey(sk) ∧ sk ∈ statfields(sk .fs .class) ∧ tdname∃(str, sk .fs .class) ∧ (initdone(sk .fs .class, st) → validfield(str, jvmref, sk, st)), initdone(class, st) ⊦ validref(str, r, ty, st)

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st, sk, str)]]