---

Step * of Lemma list_accum-map

∀[L,y,f,g:Top].
  (accumulate (with value x and list item a):
    f[x;a]
   over list:
     map(g;L)
   with starting value:
    y) ~ accumulate (with value x and list item a):
          f[x;g a]
         over list:
           L
         with starting value:
          y))
BY
{ (RepUR ``map reduce`` 0
   THEN MutualFixpointInduction1 `L'
   THEN Reduce 0
   THEN RW (SubC (TryC RecUnfoldTopAbC)) 0
   THEN RW (SubC (SubC (TryC RecUnfoldTopAbC))) 0
   THEN RW (SubC (TryC (LiftC true))) 0
   THEN UseCbvSqle
   THEN RW (SubC (TryC (LiftC true))) 0
   THEN HVimplies2 0 [1]
   THEN Try (((RWO "-1" 0 THENA Auto)
              THEN RW (SubC (LiftC true)) 0
              THEN HVimplies2 0 [1]
              THEN RW (SubC (TryC RecUnfoldTopAbC)) 0
              THEN Auto))
   THEN BackThruSomeHyp) }

---

Latex:

---

Latex:
\mforall{}[L,y,f,g:Top].
    (accumulate  (with  value  x  and  list  item  a):
        f[x;a]
      over  list:
          map(g;L)
      with  starting  value:
        y)  \msim{}  accumulate  (with  value  x  and  list  item  a):
                    f[x;g  a]
                  over  list:
                      L
                  with  starting  value:
                    y))


By

---

Latex:
(RepUR  ``map  reduce``  0
  THEN  MutualFixpointInduction1  `L'
  THEN  Reduce  0
  THEN  RW  (SubC  (TryC  RecUnfoldTopAbC))  0
  THEN  RW  (SubC  (SubC  (TryC  RecUnfoldTopAbC)))  0
  THEN  RW  (SubC  (TryC  (LiftC  true)))  0
  THEN  UseCbvSqle
  THEN  RW  (SubC  (TryC  (LiftC  true)))  0
  THEN  HVimplies2  0  [1]
  THEN  Try  (((RWO  "-1"  0  THENA  Auto)
                        THEN  RW  (SubC  (LiftC  true))  0
                        THEN  HVimplies2  0  [1]
                        THEN  RW  (SubC  (TryC  RecUnfoldTopAbC))  0
                        THEN  Auto))
  THEN  BackThruSomeHyp)

---

Home Index