---

Step * 2 1 1 1 of Lemma list_accum_split


1. T : Type
2. i : ℤ
3. 0 < i
4. ∀[l:T List]. ∀[f:Top ⟶ T ⟶ Top]. ∀[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:
             nth_tl(i - 1;l)
           with starting value:
            accumulate (with value x and list item a):
             f[x;a]
            over list:
              firstn(i - 1;l)
            with starting value:
             y)) 
     supposing i - 1 < ||l||
5. l : T List
6. f : Top ⟶ T ⟶ Top
7. y : Top
8. i < ||l||
9. 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:
           nth_tl(i - 1;l)
         with starting value:
          accumulate (with value x and list item a):
           f[x;a]
          over list:
            firstn(i - 1;l)
          with starting value:
           y))
⊢ f[accumulate (with value x and list item a):
     f[x;a]
    over list:
      firstn(i - 1;l)
    with starting value:
     y);l[i - 1]] ~ accumulate (with value x and list item a):
                     f[x;a]
                    over list:
                      firstn(i;l)
                    with starting value:
                     y)
BY
{ (MoveToConcl (-2)) }

1
1. T : Type
2. i : ℤ
3. 0 < i
4. ∀[l:T List]. ∀[f:Top ⟶ T ⟶ Top]. ∀[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:
             nth_tl(i - 1;l)
           with starting value:
            accumulate (with value x and list item a):
             f[x;a]
            over list:
              firstn(i - 1;l)
            with starting value:
             y)) 
     supposing i - 1 < ||l||
5. l : T List
6. f : Top ⟶ T ⟶ Top
7. y : Top
8. 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:
           nth_tl(i - 1;l)
         with starting value:
          accumulate (with value x and list item a):
           f[x;a]
          over list:
            firstn(i - 1;l)
          with starting value:
           y))
⊢ i < ||l||
⇒ (f[accumulate (with value x and list item a):
       f[x;a]
      over list:
        firstn(i - 1;l)
      with starting value:
       y);l[i - 1]] ~ accumulate (with value x and list item a):
                       f[x;a]
                      over list:
                        firstn(i;l)
                      with starting value:
                       y))

---

Latex:

---

Latex:

1.  T  :  Type
2.  i  :  \mBbbZ{}
3.  0  <  i
4.  \mforall{}[l:T  List].  \mforall{}[f:Top  {}\mrightarrow{}  T  {}\mrightarrow{}  Top].  \mforall{}[y:Top].
          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:
                          nth\_tl(i  -  1;l)
                      with  starting  value:
                        accumulate  (with  value  x  and  list  item  a):
                          f[x;a]
                        over  list:
                            firstn(i  -  1;l)
                        with  starting  value:
                          y)) 
          supposing  i  -  1  <  ||l||
5.  l  :  T  List
6.  f  :  Top  {}\mrightarrow{}  T  {}\mrightarrow{}  Top
7.  y  :  Top
8.  i  <  ||l||
9.  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:
                      nth\_tl(i  -  1;l)
                  with  starting  value:
                    accumulate  (with  value  x  and  list  item  a):
                      f[x;a]
                    over  list:
                        firstn(i  -  1;l)
                    with  starting  value:
                      y))
\mvdash{}  f[accumulate  (with  value  x  and  list  item  a):
          f[x;a]
        over  list:
            firstn(i  -  1;l)
        with  starting  value:
          y);l[i  -  1]]  \msim{}  accumulate  (with  value  x  and  list  item  a):
                                          f[x;a]
                                        over  list:
                                            firstn(i;l)
                                        with  starting  value:
                                          y)


By

---

Latex:
(MoveToConcl  (-2))

---

Home Index