---

Step * 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. n ≤ bigger-int(n;firstn(||L|| - 1;L))
⊢ n ≤ bigger-int(bigger-int(n;firstn(||L|| - 1;L));[last(L)])
BY
{ (MoveToConcl (-1) THEN GenConclAtAddr [1;2]) }

1
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)]))

---

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.  n  \mleq{}  bigger-int(n;firstn(||L||  -  1;L))
\mvdash{}  n  \mleq{}  bigger-int(bigger-int(n;firstn(||L||  -  1;L));[last(L)])


By

---

Latex:
(MoveToConcl  (-1)  THEN  GenConclAtAddr  [1;2])

---

Home Index