Proof step 12 from proof compatarray-mode (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ compat(str, val, ty, st) ↔ okval(val, ty) ∧ ( is_referencevalue(val) ∧ val .refval ≠ jvmref → val .refval -- _type ∈ st ∧ is_typevalue(st[val .refval -- _type]) ∧ is_reftype(st[val .refval -- _type] .type) ∧ (has_classtype(st[val .refval -- _type] .type) → tdname+∃(str, st[val .refval -- _type] .type .jtelemtype .class)) ∧ (is_classtype(st[val .refval -- _type] .type) → class+∃(str, st[val .refval -- _type] .type .class)) ∧ asgcomp(str, val, ty, st))

• Proof step 11:

  st[r -- _length] = intval(i), st[r -- _type] .type = mkarraytype(ty), okval(st[r -- j '], ty) ∧ ( is_referencevalue(st[r -- j ']) ∧ st[r -- j '] .refval ≠ jvmref → st[r -- j '] .refval -- _type ∈ st[_mode, val] ∧ is_typevalue(st[_mode, val][st[r -- j '] .refval -- _type]) ∧ is_reftype((st[_mode, val][st[r -- j '] .refval -- _type]) .type) ∧ ( has_classtype((st[_mode, val][st[r -- j '] .refval -- _type]) .type) → tdname+∃(str, (st[_mode, val][st[r -- j '] .refval -- _type]) .type .jtelemtype .class)) ∧ ( is_classtype((st[_mode, val][st[r -- j '] .refval -- _type]) .type) → class+∃(str, (st[_mode, val][st[r -- j '] .refval -- _type]) .type .class)) ∧ asgcomp(str, st[r -- j '], ty, st[_mode, val])), 0 < i, 0 ≤ j, r ∈ st, is_arrayref(r, i, st), r -- _length ∈ st, 0 ≤ i, j < i, is_referencevalue(st[r -- j ']) ⊦ r = jvmref, compat(str, st[r -- j '], ty, st)

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st[_mode, val], ty, st[r -- j '], str)]]