Proof step 143 from proof validval-put-any (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• 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 142:

  validval(str, r -- sk, val0, st), validval(str, rk, val, st) ⊦ (is_fskey(sk) → validval(str, val0, sk .fs .type, st[rk, val]) ∧ sk .fs .type ≠ void_type ∧ sk ≠ _length) ∧ (is_indexkey(sk) → validval(str, val0, (st[rk, val][r -- _type]) .type .type, st[rk, val]))

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st[rk, val], val0, sk, r, str)]]