---

Step * 2 of Lemma list_accum_split

.....upcase..... 
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||
⊢ ∀[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;l)
          with starting value:
           accumulate (with value x and list item a):
            f[x;a]
           over list:
             firstn(i;l)
           with starting value:
            y)) 
    supposing i < ||l||
BY
{ ((((D 0 THENM D 0) THENM D 0) THENA Auto) THEN (D 0 THENA Auto)) }

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. i < ||l||
⊢ 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;l)
        with starting value:
         accumulate (with value x and list item a):
          f[x;a]
         over list:
           firstn(i;l)
         with starting value:
          y))

---

Latex:

---

Latex:
.....upcase..... 
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||
\mvdash{}  \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;l)
                    with  starting  value:
                      accumulate  (with  value  x  and  list  item  a):
                        f[x;a]
                      over  list:
                          firstn(i;l)
                      with  starting  value:
                        y)) 
        supposing  i  <  ||l||


By

---

Latex:
((((D  0  THENM  D  0)  THENM  D  0)  THENA  Auto)  THEN  (D  0  THENA  Auto))

---

Home Index