---

Step * 2 1 1 of Lemma list_accum_functionality

.....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
BY
{ (Symmetry
   THEN (BHyp (-3))
   THEN Auto
   THEN BackThruSomeHyp
   THEN Auto
   THEN Try ((BLemma `iseg_append` THEN Auto))
   THEN Try ((RWO "length_append" 0 THEN Auto'))) }

---

Latex:

---

Latex:
.....equality..... 
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.  \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]))
\mvdash{}  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)


By

---

Latex:
(Symmetry
  THEN  (BHyp  (-3))
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  Auto
  THEN  Try  ((BLemma  `iseg\_append`  THEN  Auto))
  THEN  Try  ((RWO  "length\_append"  0  THEN  Auto')))

---

Home Index