Proof step 10 from proof okbar-nopath (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 2:

  ⊦ is_array(str, r, st) ∧ st[r -- _type] .type ≤ ty → ( validrefs(str, r ' + refs, ty, st) ↔ refs = [] ∨ (∃ i. 0 ≤ i ∧ i < st[r -- _length] .intval ∧ is_referencevalue(st[r -- i ']) ∧ refs .first = st[r -- i '] .refval ∧ validrefs(str, refs, st[r -- _type] .type .type, st)))

• Proof step 5:

  ¬ (is_array(str, r, st) ∧ st[r -- _type] .type ≤ mkclasstype(`java.lang.Object' .class)), okbytearray(r, st), validrefs(str, r ' + refs0, mkclasstype(`java.lang.Object' .class), st) ⊦ r = (r ' + refs0) .last

• Proof step 9:

  is_array(str, r, st) ∧ st[r -- _type] .type ≤ mkclasstype(`java.lang.Object' .class), okbytearray(r, st), refs0 = [] ∨ (∃ i. 0 ≤ i ∧ i < st[r -- _length] .intval ∧ is_referencevalue(st[r -- i ']) ∧ refs0 .first = st[r -- i '] .refval ∧ validrefs(str, refs0, st[r -- _type] .type .type, st)) ⊦ r = (r ' + refs0) .last

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (st, mkclasstype(`java.lang.Object' .class), refs0, r, str)]]