---

Step * of Lemma ml-prodmap-sq

∀[T,A,B:Type].
  ∀[f:A ⟶ B ⟶ T]. ∀[as:A List]. ∀[bs:B List].  (ml-prodmap(f;as;bs) ~ eager-product-map(f;as;bs)) 
  supposing valueall-type(T) ∧ valueall-type(A) ∧ valueall-type(B) ∧ A ∧ B
BY
{ (InductionOnList
   THEN ((UnivCD THENA Auto) THEN (Assert ↓∃:A. value-type(B ⟶ T) BY (RepeatFor 2 ((D 0 THEN Auto)) THEN EAuto 1)))
   THEN RepUR ``ml-prodmap`` 0
   THEN (RW (AddrC [1] (LemmaC `ml_apply-sq`)) 0 THEN Auto)
   THEN (RW (AddrC [1;1] (LemmaC `ml_apply-sq`)) 0 THEN Auto)
   THEN RW (AddrC [1;1;1] (LemmaC `ml_apply-sq`)) 0
   THEN Auto
   THEN RW (SweepUpC UnrollRecursionC) 0
   THEN Reduce 0
   THEN Try (Fold `ml-prodmap` 0)
   THEN RepUR ``eager-product-map`` 0
   THEN Try (Fold `eager-product-map` 0)
   THEN (Trivial ORELSE RepUR ``spreadcons`` 0)) }

1
1. T : Type
2. A : Type
3. B : Type
4. valueall-type(T)
5. valueall-type(A)
6. valueall-type(B)
7. A
8. B
9. f : A ⟶ B ⟶ T
10. u : A
11. v : A List
12. ∀[bs:B List]. (ml-prodmap(f;v;bs) ~ eager-product-map(f;v;bs))
13. bs : B List
14. ↓∃:A. value-type(B ⟶ T)
⊢ ml-maprevappend(f(u);bs;ml-prodmap(f;v;bs)) ~ eager-map-append(f u;bs;eager-product-map(f;v;bs))

---

Latex:

---

Latex:
\mforall{}[T,A,B:Type].
    \mforall{}[f:A  {}\mrightarrow{}  B  {}\mrightarrow{}  T].  \mforall{}[as:A  List].  \mforall{}[bs:B  List].    (ml-prodmap(f;as;bs)  \msim{}  eager-product-map(f;as;bs)) 
    supposing  valueall-type(T)  \mwedge{}  valueall-type(A)  \mwedge{}  valueall-type(B)  \mwedge{}  A  \mwedge{}  B


By

---

Latex:
(InductionOnList
  THEN  ((UnivCD  THENA  Auto)
              THEN  (Assert  \mdownarrow{}\mexists{}:A.  value-type(B  {}\mrightarrow{}  T)  BY
                                      (RepeatFor  2  ((D  0  THEN  Auto))  THEN  EAuto  1))
              )
  THEN  RepUR  ``ml-prodmap``  0
  THEN  (RW  (AddrC  [1]  (LemmaC  `ml\_apply-sq`))  0  THEN  Auto)
  THEN  (RW  (AddrC  [1;1]  (LemmaC  `ml\_apply-sq`))  0  THEN  Auto)
  THEN  RW  (AddrC  [1;1;1]  (LemmaC  `ml\_apply-sq`))  0
  THEN  Auto
  THEN  RW  (SweepUpC  UnrollRecursionC)  0
  THEN  Reduce  0
  THEN  Try  (Fold  `ml-prodmap`  0)
  THEN  RepUR  ``eager-product-map``  0
  THEN  Try  (Fold  `eager-product-map`  0)
  THEN  (Trivial  ORELSE  RepUR  ``spreadcons``  0))

---

Home Index