---

Step * 1 of Lemma bigger-int-property


1. L : ℤ List
2. ¬↑null(L)
3. ||L|| ≥ 1 
4. ∀[n:ℤ]. (∀x∈firstn(||L|| - 1;L).x < bigger-int(n;firstn(||L|| - 1;L)))
5. n : ℤ
⊢ (∀x∈firstn(||L|| - 1;L) @ [last(L)].x < 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:ℤ]. (∀x∈firstn(||L|| - 1;L).x < bigger-int(n;firstn(||L|| - 1;L)))
5. n : ℤ
6. (∀x∈firstn(||L|| - 1;L).x < bigger-int(n;firstn(||L|| - 1;L)))
⊢ (∀x∈firstn(||L|| - 1;L) @ [last(L)].x < 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{}].  (\mforall{}x\mmember{}firstn(||L||  -  1;L).x  <  bigger-int(n;firstn(||L||  -  1;L)))
5.  n  :  \mBbbZ{}
\mvdash{}  (\mforall{}x\mmember{}firstn(||L||  -  1;L)  @  [last(L)].x  <  bigger-int(bigger-int(n;firstn(||L||  -  1;L));[last(L)]))


By

---

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

---

Home Index