---

Step * 2 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))
⊢ accumulate (with value x and list item a):
   f[x;a]
  over list:
    [l[i - 1] / nth_tl(i;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)) ~ 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))
BY
{ ((RW (AddrC [1] (RecUnfoldTopC `list_accum`)) 0) THEN Reduce 0 THEN EqCD THEN Try (Complete (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||
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)

---

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{}  accumulate  (with  value  x  and  list  item  a):
      f[x;a]
    over  list:
        [l[i  -  1]  /  nth\_tl(i;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))  \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))


By

---

Latex:
((RW  (AddrC  [1]  (RecUnfoldTopC  `list\_accum`))  0)  THEN  Reduce  0  THEN  EqCD  THEN  Try  (Complete  (Auto)))

---

Home Index