---

Step * 1 1 1 of Lemma ml-maprevappend-sq


1. T : Type
2. A : Type
3. f : A ⟶ T
4. valueall-type(T)
5. valueall-type(A)
6. A
7. valueall-type(A ⟶ T)
8. u : A
9. v : A List
10. ∀bs:T List. (ml-maprevappend(f;v;bs) ~ map(f;rev(v)) @ bs)
11. bs : T List
12. ml-maprevappend(f;v;[f u / bs]) ~ map(f;rev(v)) @ [f u / bs]
⊢ let y ⟵ f
  in fix((λrevappend,f,l,x. if null(l)
                           then x
                           else let a.b = l 
                                in let y ⟵ [let y ⟵ a in f y / x]
                                   in let y ⟵ b in let y ⟵ f in revappend y y y
                           fi )) 
     y 
  v 
  [f u / bs] ~ ml-maprevappend(f;v;[f u / bs])
BY
{ (RepUR ``ml-maprevappend ml_apply`` 0
   THEN (CallByValueReduceOn ⌜[f u / bs]⌝0⋅ THENA Auto)
   THEN (CallByValueReduceOn ⌜v⌝0⋅ THENA Auto)
   THEN CallByValueReduceOn ⌜f⌝0⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  A  :  Type
3.  f  :  A  {}\mrightarrow{}  T
4.  valueall-type(T)
5.  valueall-type(A)
6.  A
7.  valueall-type(A  {}\mrightarrow{}  T)
8.  u  :  A
9.  v  :  A  List
10.  \mforall{}bs:T  List.  (ml-maprevappend(f;v;bs)  \msim{}  map(f;rev(v))  @  bs)
11.  bs  :  T  List
12.  ml-maprevappend(f;v;[f  u  /  bs])  \msim{}  map(f;rev(v))  @  [f  u  /  bs]
\mvdash{}  let  y  \mleftarrow{}{}  f
    in  fix((\mlambda{}revappend,f,l,x.  if  null(l)
                                                      then  x
                                                      else  let  a.b  =  l 
                                                                in  let  y  \mleftarrow{}{}  [let  y  \mleftarrow{}{}  a  in  f  y  /  x]
                                                                      in  let  y  \mleftarrow{}{}  b  in  let  y  \mleftarrow{}{}  f  in  revappend  y  y  y
                                                      fi  )) 
          y 
    v 
    [f  u  /  bs]  \msim{}  ml-maprevappend(f;v;[f  u  /  bs])


By

---

Latex:
(RepUR  ``ml-maprevappend  ml\_apply``  0
  THEN  (CallByValueReduceOn  \mkleeneopen{}[f  u  /  bs]\mkleeneclose{}0\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduceOn  \mkleeneopen{}v\mkleeneclose{}0\mcdot{}  THENA  Auto)
  THEN  CallByValueReduceOn  \mkleeneopen{}f\mkleeneclose{}0\mcdot{}
  THEN  Auto)

---

Home Index