---

Step * 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
⊢ 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] ~ map(f;rev([u / v])) @ bs
BY
{ ((InstHyp [⌜[f u / bs]⌝] (-2)⋅ THENA Auto) THEN NthHypSq (-1) THEN EqCD) }

1
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])

2
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]
⊢ map(f;rev([u / v])) @ bs ~ map(f;rev(v)) @ [f u / bs]

---

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
\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{}  map(f;rev([u  /  v]))  @  bs


By

---

Latex:
((InstHyp  [\mkleeneopen{}[f  u  /  bs]\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)  THEN  NthHypSq  (-1)  THEN  EqCD)

---

Home Index