Proof step 54 from proof validrefs-primarray (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 2:

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

• Proof step 24:

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

• Proof step 53:

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

Rule argument

Additional information

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