---

Step * 1 of Lemma list_accum_split


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||
BY
{ ((D 0 THENA Auto) THEN Subst firstn(0;l) ~ [] 0) }

1
.....equality..... 
1. T : Type
2. i : ℤ
3. l : T List
⊢ firstn(0;l) ~ []

2
1. T : Type
2. i : ℤ
3. 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:
             []
           with starting value:
            y)) 
    supposing 0 < ||l||

---

Latex:

---

Latex:

1.  T  :  Type
2.  i  :  \mBbbZ{}
\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:
                        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||


By

---

Latex:
((D  0  THENA  Auto)  THEN  Subst  firstn(0;l)  \msim{}  []  0)

---

Home Index