---

Step * 1 1 1 1 of Lemma bigger-int-property2


1. L : ℤ List
2. ¬↑null(L)
3. ||L|| ≥ 1 
4. ∀[n:ℤ]. (n ≤ bigger-int(n;firstn(||L|| - 1;L)))
5. n : ℤ
6. v : ℤ
7. bigger-int(n;firstn(||L|| - 1;L)) = v ∈ ℤ
⊢ (n ≤ v) ⇒ (n ≤ bigger-int(v;[last(L)]))
BY
{ (RepUR ``bigger-int`` 0 THEN (RepeatFor 2 ((CallByValueReduce 0 THENA Auto)) THEN AutoSplit)) }

---

Latex:

---

Latex:

1.  L  :  \mBbbZ{}  List
2.  \mneg{}\muparrow{}null(L)
3.  ||L||  \mgeq{}  1 
4.  \mforall{}[n:\mBbbZ{}].  (n  \mleq{}  bigger-int(n;firstn(||L||  -  1;L)))
5.  n  :  \mBbbZ{}
6.  v  :  \mBbbZ{}
7.  bigger-int(n;firstn(||L||  -  1;L))  =  v
\mvdash{}  (n  \mleq{}  v)  {}\mRightarrow{}  (n  \mleq{}  bigger-int(v;[last(L)]))


By

---

Latex:
(RepUR  ``bigger-int``  0  THEN  (RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))  THEN  AutoSplit))

---

Home Index