---

Step * 1 2 of Lemma list_accum_split


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||
BY
{ (((D 0 THENM D 0) THENA Auto)
   THEN Subst accumulate (with value x and list item a):
               f[x;a]
              over list:
                []
              with starting value:
               y) ~ y 0
   ) }

1
.....equality..... 
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:
    []
  with starting value:
   y) ~ y

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

---

Latex:

---

Latex:

1.  T  :  Type
2.  i  :  \mBbbZ{}
3.  l  :  T  List
\mvdash{}  \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:
                          []
                      with  starting  value:
                        y)) 
        supposing  0  <  ||l||


By

---

Latex:
(((D  0  THENM  D  0)  THENA  Auto)
  THEN  Subst  accumulate  (with  value  x  and  list  item  a):
                          f[x;a]
                        over  list:
                            []
                        with  starting  value:
                          y)  \msim{}  y  0
  )

---

Home Index