---

Step * of Lemma list_accum_split

∀[T:Type]. ∀[i:ℕ]. ∀[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) THENA Auto) THEN NatInd (-1)) THEN Reduce 0) }

1
1. T : Type
2. i : ℤ
⊢ ∀[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:
            l
          with starting value:
           accumulate (with value x and list item a):
            f[x;a]
           over list:
             firstn(0;l)
           with starting value:
            y)) 
    supposing 0 < ||l||

2
.....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||

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[i:\mBbbN{}].  \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)  THENA  Auto)  THEN  NatInd  (-1))  THEN  Reduce  0)

---

Home Index