---

Step * of Lemma ml-map-sq

∀[A,B:Type].  ∀[f:A ⟶ B]. ∀[l:A List].  (ml-map(f;l) ~ map(f;l)) supposing (valueall-type(A) ∧ A) ∧ value-type(B)
BY
{ (InductionOnList
   THEN All (RepUR ``ml-map spreadcons ml_apply``)
   THEN (Assert ⌜valueall-type(A ⟶ B)⌝⋅ THENA Auto)
   THEN CallByValueReduceOn ⌜f⌝ 0⋅
   THEN Auto
   THEN RW (AddrC [1] (SweepUpC UnrollRecursionC)) 0
   THEN Reduce 0
   THEN (Trivial ORELSE RepeatFor 3 (((CallByValueReduce 0 THENA Auto) THEN Reduce 0)))) }

1
1. A : Type
2. B : Type
3. valueall-type(A)
4. A
5. value-type(B)
6. f : A ⟶ B
7. u : A
8. v : A List
9. let y ⟵ v
   in let y ⟵ f
      in fix((λmap,f,l. if null(l)
                       then []
                       else let a,as = l 
                            in [let y ⟵ a in f y / let y ⟵ as in let y ⟵ f in map y y]
                       fi )) 
         y 
      y ~ map(f;v)
10. valueall-type(A ⟶ B)
⊢ [f u / 
   (fix((λmap,f,l. if null(l)
                  then []
                  else let a,as = l 
                       in [let y ⟵ a in f y / let y ⟵ as in let y ⟵ f in map y y]
                  fi )) 
    f 
    v)] ~ [f u / map(f;v)]

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[l:A  List].    (ml-map(f;l)  \msim{}  map(f;l)) 
    supposing  (valueall-type(A)  \mwedge{}  A)  \mwedge{}  value-type(B)


By

---

Latex:
(InductionOnList
  THEN  All  (RepUR  ``ml-map  spreadcons  ml\_apply``)
  THEN  (Assert  \mkleeneopen{}valueall-type(A  {}\mrightarrow{}  B)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  CallByValueReduceOn  \mkleeneopen{}f\mkleeneclose{}  0\mcdot{}
  THEN  Auto
  THEN  RW  (AddrC  [1]  (SweepUpC  UnrollRecursionC))  0
  THEN  Reduce  0
  THEN  (Trivial  ORELSE  RepeatFor  3  (((CallByValueReduce  0  THENA  Auto)  THEN  Reduce  0))))

---

Home Index