---

Step * of Lemma list_accum_functionality

∀[T,A:Type]. ∀[f,g:T ⟶ A ⟶ T]. ∀[L:A List]. ∀[y,z:T].
  (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):
        g[x;a]
       over list:
         L
       with starting value:
        z)
     ∈ T) supposing 
     ((y = z ∈ T) and 
     (∀L':A List. ∀a:A.
        (L' @ [a] ≤ L
        ⇒ (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))))
BY
{ (Auto THEN RepeatFor 5 (MoveToConcl (-1)) THEN (BLemma `last_induction` THENA Auto)) }

1
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))

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  RepeatFor  5  (MoveToConcl  (-1))  THEN  (BLemma  `last\_induction`  THENA  Auto))

---

Home Index