---

Step * of Lemma bigger-int-property2

∀[L:ℤ List]. ∀[n:ℤ].  (n ≤ bigger-int(n;L))
BY
{ ((InductionOnLast THEN Auto) THEN RepUR ``bigger-int`` 0 THEN Auto) }

1
1. L : ℤ List
2. ¬↑null(L)
3. ||L|| ≥ 1 
4. ∀[n:ℤ]. (n ≤ bigger-int(n;firstn(||L|| - 1;L)))
5. n : ℤ
⊢ n ≤ accumulate (with value x and list item y):
       eval x = x in
       eval y = y in
         if x ≤z y then y + 1 else x fi 
      over list:
        firstn(||L|| - 1;L) @ [last(L)]
      with starting value:
       n)

---

Latex:

---

Latex:
\mforall{}[L:\mBbbZ{}  List].  \mforall{}[n:\mBbbZ{}].    (n  \mleq{}  bigger-int(n;L))


By

---

Latex:
((InductionOnLast  THEN  Auto)  THEN  RepUR  ``bigger-int``  0  THEN  Auto)

---

Home Index