---

Step * of Lemma reduce-map

∀[f,g,as,x:Top].  (reduce(λa,b. g[a;b];x;map(f;as)) ~ reduce(λa,b. g[f a;b];x;as))
BY
{ (RepUR ``map reduce`` 0
   THEN MutualFixpointInduction1 `as'
   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 Repeat ((SqLeCD THEN Try (BackThruSomeHyp)))) }

---

Latex:

---

Latex:
\mforall{}[f,g,as,x:Top].    (reduce(\mlambda{}a,b.  g[a;b];x;map(f;as))  \msim{}  reduce(\mlambda{}a,b.  g[f  a;b];x;as))


By

---

Latex:
(RepUR  ``map  reduce``  0
  THEN  MutualFixpointInduction1  `as'
  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  Repeat  ((SqLeCD  THEN  Try  (BackThruSomeHyp))))

---

Home Index