---

Step * 2 of Lemma list_accum_functionality


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))))
BY
{ ((((UnivCD THENA Auto) THEN RWO "list_accum_append" 0) THENM Reduce 0) THENA Auto) }

1
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

---

Latex:

---

Latex:

1.  T  :  Type
2.  A  :  Type
3.  f  :  T  {}\mrightarrow{}  A  {}\mrightarrow{}  T
4.  g  :  T  {}\mrightarrow{}  A  {}\mrightarrow{}  T
\mvdash{}  \mforall{}ys:A  List.  \mforall{}y:A.
        ((\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))))
        {}\mRightarrow{}  (\mforall{}y@0,z:T.
                    ((\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])))
                    {}\mRightarrow{}  (y@0  =  z)
                    {}\mRightarrow{}  (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)))))


By

---

Latex:
((((UnivCD  THENA  Auto)  THEN  RWO  "list\_accum\_append"  0)  THENM  Reduce  0)  THENA  Auto)

---

Home Index