---

Step * 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 : ℤ
⊢ n ≤ bigger-int(bigger-int(n;firstn(||L|| - 1;L));[last(L)])
BY
{ (InstHyp [⌜n⌝] (-2)⋅ THENA Auto) }

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

---

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


By

---

Latex:
(InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)

---

Home Index