---

Step * 1 1 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 : ℤ
6. v : ℤ
7. bigger-int(n;firstn(||L|| - 1;L)) = v ∈ ℤ
8. (∀x∈firstn(||L|| - 1;L).x < v)
⊢ (∀x∈firstn(||L|| - 1;L) @ [last(L)].x < bigger-int(v;[last(L)]))
BY
{ (RWW "l_all_append l_all_single" 0
   THEN Auto
   THEN Try (RepeatFor 2 (ParallelLast))⋅
   THEN 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{}].  (\mforall{}x\mmember{}firstn(||L||  -  1;L).x  <  bigger-int(n;firstn(||L||  -  1;L)))
5.  n  :  \mBbbZ{}
6.  v  :  \mBbbZ{}
7.  bigger-int(n;firstn(||L||  -  1;L))  =  v
8.  (\mforall{}x\mmember{}firstn(||L||  -  1;L).x  <  v)
\mvdash{}  (\mforall{}x\mmember{}firstn(||L||  -  1;L)  @  [last(L)].x  <  bigger-int(v;[last(L)]))


By

---

Latex:
(RWW  "l\_all\_append  l\_all\_single"  0
  THEN  Auto
  THEN  Try  (RepeatFor  2  (ParallelLast))\mcdot{}
  THEN  RepUR  ``bigger-int``  0\mcdot{}
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  AutoSplit)

---

Home Index