Proof step 8 from proof bytearray-is-no-junk (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 1:

  ⊦ is_array(str, r, st) → ( junkref(str, r, st) ↔ (∃ i. 0 ≤ i ∧ i < st[r -- _length] .intval ∧ is_referencevalue(st[r -- i ']) ∧ st[r -- i '] .refval ≠ jvmref ∧ (¬ st[st[r -- i '] .refval -- _type] .type ≤ st[r -- _type] .type .type ∨ junkref(str, st[r -- i '] .refval, st))))

• Proof step 5:

  ¬ is_array(str, r, st), okbytearray(r, st), junkref(str, r, st) ⊦

• Proof step 7:

  is_array(str, r, st), okbytearray(r, st), ∃ i. 0 ≤ i ∧ i < st[r -- _length] .intval ∧ is_referencevalue(st[r -- i ']) ∧ st[r -- i '] .refval ≠ jvmref ∧ (¬ st[st[r -- i '] .refval -- _type] .type ≤ st[r -- _type] .type .type ∨ junkref(str, st[r -- i '] .refval, st)) ⊦

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st, r, str)]]