---

Step * 2 1 of Lemma list_accum_functionality


1. T : Type
2. A : Type
3. f : T ⟶ A ⟶ T
4. g : T ⟶ A ⟶ T
5. ys : A List
6. y : A
7. ∀y,z:T.
     ((∀L':A List. ∀a:A.
         (L' @ [a] ≤ ys
         ⇒ (f[accumulate (with value x and list item a):
                f[x;a]
               over list:
                 L'
               with starting value:
                y);a]
            = g[accumulate (with value x and list item a):
                 f[x;a]
                over list:
                  L'
                with starting value:
                 y);a]
            ∈ T)))
     ⇒ (y = z ∈ T)
     ⇒ (accumulate (with value x and list item a):
          f[x;a]
         over list:
           ys
         with starting value:
          y)
        = accumulate (with value x and list item a):
           g[x;a]
          over list:
            ys
          with starting value:
           z)
        ∈ T))
8. y@0 : T
9. z : T
10. ∀L':A List. ∀a:A.
      (L' @ [a] ≤ ys @ [y]
      ⇒ (f[accumulate (with value x and list item a):
             f[x;a]
            over list:
              L'
            with starting value:
             y@0);a]
         = g[accumulate (with value x and list item a):
              f[x;a]
             over list:
               L'
             with starting value:
              y@0);a]
         ∈ T))
11. y@0 = z ∈ T
⊢ f[accumulate (with value x and list item a):
     f[x;a]
    over list:
      ys
    with starting value:
     y@0);y]
= g[accumulate (with value x and list item a):
     g[x;a]
    over list:
      ys
    with starting value:
     z);y]
∈ T
BY
{ (((RevHypSubst (-1) 0) THENA Auto)
   THEN (Thin (-1))
   THEN (Thin (-2))
   THEN Subst ⌜accumulate (with value x and list item a):
                g[x;a]
               over list:
                 ys
               with starting value:
                y@0)
               = accumulate (with value x and list item a):
                  f[x;a]
                 over list:
                   ys
                 with starting value:
                  y@0)
               ∈ T⌝ 0⋅
   THEN Auto) }

1
.....equality..... 
1. T : Type
2. A : Type
3. f : T ⟶ A ⟶ T
4. g : T ⟶ A ⟶ T
5. ys : A List
6. y : A
7. ∀y,z:T.
     ((∀L':A List. ∀a:A.
         (L' @ [a] ≤ ys
         ⇒ (f[accumulate (with value x and list item a):
                f[x;a]
               over list:
                 L'
               with starting value:
                y);a]
            = g[accumulate (with value x and list item a):
                 f[x;a]
                over list:
                  L'
                with starting value:
                 y);a]
            ∈ T)))
     ⇒ (y = z ∈ T)
     ⇒ (accumulate (with value x and list item a):
          f[x;a]
         over list:
           ys
         with starting value:
          y)
        = accumulate (with value x and list item a):
           g[x;a]
          over list:
            ys
          with starting value:
           z)
        ∈ T))
8. y@0 : T
9. ∀L':A List. ∀a:A.
     (L' @ [a] ≤ ys @ [y]
     ⇒ (f[accumulate (with value x and list item a):
            f[x;a]
           over list:
             L'
           with starting value:
            y@0);a]
        = g[accumulate (with value x and list item a):
             f[x;a]
            over list:
              L'
            with starting value:
             y@0);a]
        ∈ T))
⊢ accumulate (with value x and list item a):
   g[x;a]
  over list:
    ys
  with starting value:
   y@0)
= accumulate (with value x and list item a):
   f[x;a]
  over list:
    ys
  with starting value:
   y@0)
∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  A  :  Type
3.  f  :  T  {}\mrightarrow{}  A  {}\mrightarrow{}  T
4.  g  :  T  {}\mrightarrow{}  A  {}\mrightarrow{}  T
5.  ys  :  A  List
6.  y  :  A
7.  \mforall{}y,z:T.
          ((\mforall{}L':A  List.  \mforall{}a:A.
                  (L'  @  [a]  \mleq{}  ys
                  {}\mRightarrow{}  (f[accumulate  (with  value  x  and  list  item  a):
                                f[x;a]
                              over  list:
                                  L'
                              with  starting  value:
                                y);a]
                        =  g[accumulate  (with  value  x  and  list  item  a):
                                  f[x;a]
                                over  list:
                                    L'
                                with  starting  value:
                                  y);a])))
          {}\mRightarrow{}  (y  =  z)
          {}\mRightarrow{}  (accumulate  (with  value  x  and  list  item  a):
                    f[x;a]
                  over  list:
                      ys
                  with  starting  value:
                    y)
                =  accumulate  (with  value  x  and  list  item  a):
                      g[x;a]
                    over  list:
                        ys
                    with  starting  value:
                      z)))
8.  y@0  :  T
9.  z  :  T
10.  \mforall{}L':A  List.  \mforall{}a:A.
            (L'  @  [a]  \mleq{}  ys  @  [y]
            {}\mRightarrow{}  (f[accumulate  (with  value  x  and  list  item  a):
                          f[x;a]
                        over  list:
                            L'
                        with  starting  value:
                          y@0);a]
                  =  g[accumulate  (with  value  x  and  list  item  a):
                            f[x;a]
                          over  list:
                              L'
                          with  starting  value:
                            y@0);a]))
11.  y@0  =  z
\mvdash{}  f[accumulate  (with  value  x  and  list  item  a):
          f[x;a]
        over  list:
            ys
        with  starting  value:
          y@0);y]
=  g[accumulate  (with  value  x  and  list  item  a):
          g[x;a]
        over  list:
            ys
        with  starting  value:
          z);y]


By

---

Latex:
(((RevHypSubst  (-1)  0)  THENA  Auto)
  THEN  (Thin  (-1))
  THEN  (Thin  (-2))
  THEN  Subst  \mkleeneopen{}accumulate  (with  value  x  and  list  item  a):
                            g[x;a]
                          over  list:
                              ys
                          with  starting  value:
                            y@0)
                          =  accumulate  (with  value  x  and  list  item  a):
                                f[x;a]
                              over  list:
                                  ys
                              with  starting  value:
                                y@0)\mkleeneclose{}  0\mcdot{}
  THEN  Auto)

---

Home Index