---

Step * 1 2 2 of Lemma list_accum_split


1. T : Type
2. i : ℤ
3. l : T List
4. f : Top ⟶ T ⟶ Top
5. y : Top
⊢ accumulate (with value x and list item a):
   f[x;a]
  over list:
    l
  with starting value:
   y) ~ accumulate (with value x and list item a):
         f[x;a]
        over list:
          l
        with starting value:
         y) 
  supposing 0 < ||l||
BY
{ Auto }

---

Latex:

---

Latex:

1.  T  :  Type
2.  i  :  \mBbbZ{}
3.  l  :  T  List
4.  f  :  Top  {}\mrightarrow{}  T  {}\mrightarrow{}  Top
5.  y  :  Top
\mvdash{}  accumulate  (with  value  x  and  list  item  a):
      f[x;a]
    over  list:
        l
    with  starting  value:
      y)  \msim{}  accumulate  (with  value  x  and  list  item  a):
                  f[x;a]
                over  list:
                    l
                with  starting  value:
                  y) 
    supposing  0  <  ||l||


By

---

Latex:
Auto

---

Home Index