Proof step 5 from proof validval-field-norefval (previous step)

⊦ validval(str, r -- mkfs(class, ty, fieldvar) ', val, st) ↔ okval(val, ty) ∧ mkfs(class, ty, fieldvar) ' ≠ _length, is_referencevalue(val)

User applied rule insert rewrite lemma

Proof step 1:
⊦ validval(str, r -- sk, val, st) ↔ (is_fskey(sk) → validval(str, val, sk .fs .type, st) ∧ sk .fs .type ≠ void_type ∧ sk ≠ _length) ∧ (is_indexkey(sk) → validval(str, val, st[r -- _type] .type .type, st))
Proof step 4:
⊦ ( is_fskey(mkfs(class, ty, fieldvar) ') → validval(str, val, mkfs(class, ty, fieldvar) ' .fs .type, st) ∧ mkfs(class, ty, fieldvar) ' .fs .type ≠ void_type ∧ mkfs(class, ty, fieldvar) ' ≠ _length) ∧ (is_indexkey(mkfs(class, ty, fieldvar) ') → validval(str, val, st[r -- _type] .type .type, st)) ↔ okval(val, ty) ∧ mkfs(class, ty, fieldvar) ' ≠ _length, is_referencevalue(val)

[crewrite-arg: validrefkeyval-def , F , [st, val, sk, r, str] → [st, val, mkfs(class, ty, fieldvar) ', r, str] ]

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