---

Step * of Lemma bigger-int-property

∀[L:ℤ List]. ∀[n:ℤ].  (∀x∈L.x < bigger-int(n;L))
BY
{ ((InductionOnLast THEN Auto)
   THEN Try ((BLemma `l_all_nil` THEN Auto))
   THEN Unfold `bigger-int` 0
   THEN (RWO "list_accum_append" 0 THENA Auto)
   THEN Fold `bigger-int` 0
   THEN Reduce 0) }

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 : ℤ
⊢ (∀x∈firstn(||L|| - 1;L) @ [last(L)].x < bigger-int(bigger-int(n;firstn(||L|| - 1;L));[last(L)]))

---

Latex:

---

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


By

---

Latex:
((InductionOnLast  THEN  Auto)
  THEN  Try  ((BLemma  `l\_all\_nil`  THEN  Auto))
  THEN  Unfold  `bigger-int`  0
  THEN  (RWO  "list\_accum\_append"  0  THENA  Auto)
  THEN  Fold  `bigger-int`  0
  THEN  Reduce  0)

---

Home Index