---

Step * 1 of Lemma ml-map-sq


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)]
BY
{ (RepeatFor 2 ((CallByValueReduce (-2) THENA Auto)) THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  valueall-type(A)
4.  A
5.  value-type(B)
6.  f  :  A  {}\mrightarrow{}  B
7.  u  :  A
8.  v  :  A  List
9.  let  y  \mleftarrow{}{}  v
      in  let  y  \mleftarrow{}{}  f
            in  fix((\mlambda{}map,f,l.  if  null(l)
                                              then  []
                                              else  let  a,as  =  l 
                                                        in  [let  y  \mleftarrow{}{}  a  in  f  y  /  let  y  \mleftarrow{}{}  as  in  let  y  \mleftarrow{}{}  f  in  map  y  y]
                                              fi  )) 
                  y 
            y  \msim{}  map(f;v)
10.  valueall-type(A  {}\mrightarrow{}  B)
\mvdash{}  [f  u  / 
      (fix((\mlambda{}map,f,l.  if  null(l)
                                    then  []
                                    else  let  a,as  =  l 
                                              in  [let  y  \mleftarrow{}{}  a  in  f  y  /  let  y  \mleftarrow{}{}  as  in  let  y  \mleftarrow{}{}  f  in  map  y  y]
                                    fi  )) 
        f 
        v)]  \msim{}  [f  u  /  map(f;v)]


By

---

Latex:
(RepeatFor  2  ((CallByValueReduce  (-2)  THENA  Auto))  THEN  Auto)

---

Home Index