Proof step 17 from proof okbytearray-put-byteval (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ i < 0 ∨ ¬ i < st[r -- _length] .intval ∨ 0 ≤ i ∧ i < st[r -- _length] .intval ∧ r -- i ' ∈ st ∧ is_bytevalue(st[r -- i ']) → (okbytearray(r, st[r -- i ', byteval(by)]) ↔ okbytearray(r, st))

• Proof step 16:

  ¬ ( i < 0 ∨ ¬ i < (st[rkvs][r0 -- _length]) .intval ∨ 0 ≤ i ∧ i < (st[rkvs][r0 -- _length]) .intval ∧ r0 -- i ' ∈ st[rkvs] ∧ is_bytevalue(st[rkvs][r0 -- i '])), okbytearray(r0, st), okbytearray(r0, st[rkvs][r0 -- i ', byteval(by)]) ⊦ r0 -- _length ∈ rkvs, r0 -- i ' ∈ rkvs, okbytearray(r0, st[rkvs])

Rule argument

Additional information

[[CONCRETESIMPRULES : ()], [EXTRATERMS : (by, i, st[rkvs], r0)]]