---

Step * 1 of Lemma list_accum_functionality


1. T : Type
2. A : Type
3. f : T ⟶ A ⟶ T
4. g : T ⟶ A ⟶ T
⊢ ∀y,z:T.
    ((∀L':A List. ∀a:A.
        (L' @ [a] ≤ []
        ⇒ (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:
          []
        with starting value:
         y)
       = accumulate (with value x and list item a):
          g[x;a]
         over list:
           []
         with starting value:
          z)
       ∈ T))
BY
{ (Reduce 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  A  :  Type
3.  f  :  T  {}\mrightarrow{}  A  {}\mrightarrow{}  T
4.  g  :  T  {}\mrightarrow{}  A  {}\mrightarrow{}  T
\mvdash{}  \mforall{}y,z:T.
        ((\mforall{}L':A  List.  \mforall{}a:A.
                (L'  @  [a]  \mleq{}  []
                {}\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:
                    []
                with  starting  value:
                  y)
              =  accumulate  (with  value  x  and  list  item  a):
                    g[x;a]
                  over  list:
                      []
                  with  starting  value:
                    z)))


By

---

Latex:
(Reduce  0  THEN  Auto)\mcdot{}

---

Home Index