Proof step 60 from proof validref-putrkvs (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ validref(str, r, ty, st) ∧ ( is_fskey(rk .key) → (is_referencevalue(val) → validref(str, val .refval, rk .key .fs .type, st) ∧ is_reftype(rk .key .fs .type)) ∧ (¬ is_referencevalue(val) → okval(val, rk .key .fs .type) ∧ rk .key .fs .type ≠ void_type ∧ rk .key ≠ _length)) ∧ ( is_indexkey(rk .key) → ( is_referencevalue(val) → validref(str, val .refval, st[rk .ref -- _type] .type .type, st) ∧ rk .ref ≠ jvmref ∧ is_arraytype(st[rk .ref -- _type] .type) ∧ (val .refval = jvmref → is_reftype(st[rk .ref -- _type] .type .type))) ∧ (¬ is_referencevalue(val) → okval(val, st[rk .ref -- _type] .type .type))) → validref(str, r, ty, st[rk, val])

• Proof step 59:

  ¬ ( validref(str, r, ty, st) ∧ ( is_fskey(rk .key) → (is_referencevalue(val) → validref(str, val .refval, rk .key .fs .type, st) ∧ is_reftype(rk .key .fs .type)) ∧ (¬ is_referencevalue(val) → okval(val, rk .key .fs .type) ∧ rk .key .fs .type ≠ void_type ∧ rk .key ≠ _length)) ∧ ( is_indexkey(rk .key) → ( is_referencevalue(val) → validref(str, val .refval, st[rk .ref -- _type] .type .type, st) ∧ rk .ref ≠ jvmref ∧ is_arraytype(st[rk .ref -- _type] .type) ∧ (val .refval = jvmref → is_reftype(st[rk .ref -- _type] .type .type))) ∧ (¬ is_referencevalue(val) → okval(val, st[rk .ref -- _type] .type .type)))), validref(str, r, ty, st), validval(str, rk, val, st), validvals(str, rkvs0, st), ∀ str, r, ty, st. validref(str, r, ty, st) ∧ validvals(str, rkvs0, st) → validref(str, r, ty, st[rkvs0]) ⊦ validref(str, r, ty, st[rk, val]), validref(str, r, ty, st[rk, val][rkvs0])

Rule argument

Additional information

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