---

Step * of Lemma reduce-as-accum

∀[T,A:Type]. ∀[f:T ⟶ A ⟶ A].
  ∀[L:T List]. ∀[a:A].
    (reduce(f;a;L) = accumulate (with value p and list item x): f x pover list:  Lwith starting value: a) ∈ A) 
  supposing ∀x,y:T. ∀a:A.  ((f x (f y a)) = (f y (f x a)) ∈ A)
BY
{ ((UnivCD THENA Auto)
   THEN MoveToConcl (-1)
   THEN ListInd (-1)
   THEN Reduce 0
   THEN Auto
   THEN RWO "-2" 0
   THEN Auto
   THEN Thin (-2)
   THEN MoveToConcl (-1)
   THEN ListInd (-1)
   THEN Reduce 0
   THEN Auto
   THEN RWO "-2" 0
   THEN Auto
   THEN Thin (-2)
   THEN EqCD
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[f:T  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
    \mforall{}[L:T  List].  \mforall{}[a:A].
        (reduce(f;a;L)
        =  accumulate  (with  value  p  and  list  item  x):
              f  x  p
            over  list:
                L
            with  starting  value:
              a)) 
    supposing  \mforall{}x,y:T.  \mforall{}a:A.    ((f  x  (f  y  a))  =  (f  y  (f  x  a)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  Auto
  THEN  RWO  "-2"  0
  THEN  Auto
  THEN  Thin  (-2)
  THEN  MoveToConcl  (-1)
  THEN  ListInd  (-1)
  THEN  Reduce  0
  THEN  Auto
  THEN  RWO  "-2"  0
  THEN  Auto
  THEN  Thin  (-2)
  THEN  EqCD
  THEN  Auto)

---

Home Index