---

Step * 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 ≤ accumulate (with value x and list item y):
       eval x = x in
       eval y = y in
         if x ≤z y then y + 1 else x fi 
      over list:
        firstn(||L|| - 1;L) @ [last(L)]
      with starting value:
       n)
BY
{ ((RWO "list_accum_append" 0 THENA Auto) THEN Fold `bigger-int` 0) }

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

---

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{}  accumulate  (with  value  x  and  list  item  y):
              eval  x  =  x  in
              eval  y  =  y  in
                  if  x  \mleq{}z  y  then  y  +  1  else  x  fi 
            over  list:
                firstn(||L||  -  1;L)  @  [last(L)]
            with  starting  value:
              n)


By

---

Latex:
((RWO  "list\_accum\_append"  0  THENA  Auto)  THEN  Fold  `bigger-int`  0)

---

Home Index