---

Step * 2 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||
⊢ 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))
BY
{ ((InstHyp [l;f;y] 4 THENA Auto')
   THEN HypSubst (-1) 0
   THEN (Subst nth_tl(i - 1;l) ~ [l[i - 1] / nth_tl(i;l)] 0
         THENA (((InstLemma `nth_tl_decomp` [T;i - 1;l] THENA Auto) THEN HypSubst (-1) 0) THEN EqCD THEN 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))
⊢ 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))

---

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||
\mvdash{}  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))


By

---

Latex:
((InstHyp  [l;f;y]  4  THENA  Auto')
  THEN  HypSubst  (-1)  0
  THEN  (Subst  nth\_tl(i  -  1;l)  \msim{}  [l[i  -  1]  /  nth\_tl(i;l)]  0
              THENA  (((InstLemma  `nth\_tl\_decomp`  [T;i  -  1;l]  THENA  Auto)  THEN  HypSubst  (-1)  0)
                            THEN  EqCD
                            THEN  Auto)
              ))

---

Home Index