Proof step 10 from proof compatarray-void (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 2:

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

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

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st, void_type, st[r -- i '], str)]]