---

Step * 1 of Lemma ml-reduce-sq


1. A : Type
2. B : Type
3. valueall-type(B)
4. valueall-type(A) ∧ A
5. f : A ⟶ B ⟶ B
6. u : A
7. v : A List
8. ∀[b:B]
     (let y ⟵ v
      in let y ⟵ b
         in fix((λreduce,f,b,l. if null(l)
                               then b
                               else let a,as = l 
                                    in let y ⟵ let y ⟵ as
                                                in let y ⟵ b in let y ⟵ f in reduce y y y
                                       in let y ⟵ a in f y y
                               fi )) 
            f 
            y 
         y ~ reduce(f;b;v))
9. [b] : B
10. value-type(B ⟶ B)
11. valueall-type(A ⟶ B ⟶ B)
⊢ let y@0 ⟵ reduce(f;b;v)
  in let y@0 ⟵ u in f y@0 y@0 ~ f u reduce(f;b;v)
BY
{ RepeatFor 2 ((CallByValueReduce 0 THEN Auto)) }

---

Latex:

---

Latex:

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


By

---

Latex:
RepeatFor  2  ((CallByValueReduce  0  THEN  Auto))

---

Home Index