Proof step 37 from proof junkrefs-primarray (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

  ⊦ r ≠ jvmref ∧ (¬ is_valid_ref(str, r, st) ∨ ¬ st[r -- _type] .type ≤ ty) → junkrefs(str, r ' + refs, ty, st)

• Proof step 17:

  ¬ (r ≠ jvmref ∧ (¬ is_valid_ref(str, r, st) ∨ ¬ st[r -- _type] .type ≤ mkarraytype(ty))), is_primtype(ty) ⊦ junkrefs(str, r ' + refs, mkarraytype(ty), st) ↔ r ≠ jvmref ∧ ¬ okarray(r, ty, st)

• Proof step 36:

  r ≠ jvmref ∧ (¬ is_valid_ref(str, r, st) ∨ ¬ st[r -- _type] .type ≤ mkarraytype(ty)), is_primtype(ty) ⊦ true ↔ r ≠ jvmref ∧ ¬ okarray(r, ty, st)

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st, mkarraytype(ty), refs, r, str)]]