Proof step 13 from proof getarray-in (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ 0 ≤ st[r -- _length] .intval → # getarray(r, st) = i→n(st[r -- _length] .intval)

• Proof step 7:

  ¬ 0 ≤ st[r -- _length] .intval, n < # getarray(r, st) ⊦ getarray(r, st) = [], ∃ i. ¬ i < 0 ∧ ¬ st[r -- _length] .intval ≤ i ∧ st[r -- i '] = st[r -- n→i(n) ']

• Proof step 12:

  0 ≤ st[r -- _length] .intval, n < i→n(st[r -- _length] .intval) ⊦ getarray(r, st) = [], ∃ i. ¬ i < 0 ∧ ¬ st[r -- _length] .intval ≤ i ∧ st[r -- i '] = st[r -- n→i(n) ']

Rule argument

Additional information

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