Proof step 25 from proof validstatfield-put-array-norefval (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

  ⊦ 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 24:

  okval(val, st[r1 -- _type] .type .type), validstatfield(str, sk, st) ⊦ is_referencevalue(val), is_fskey(sk) ∧ sk ∈ statfields(sk .fs .class) ∧ tdname∃(str, sk .fs .class) ∧ (initdone(sk .fs .class, st[r1 -- i ', val]) → validfield(str, jvmref, sk, st[r1 -- i ', val]))

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st[r1 -- i ', val], sk, str)]]