---

Step * 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)
⊢ ∀as:A List. ∀bs:T List.  (ml-maprevappend(f;as;bs) ~ map(f;rev(as)) @ bs)
BY
{ (InductionOnList
   THEN Intro
   THEN RepUR ``ml-maprevappend ml_apply`` 0
   THEN RW (SweepUpC UnrollRecursionC) 0
   THEN Reduce 0
   THEN RepeatFor 2 ((CallByValueReduce 0⋅ THENA Auto))
   THEN Reduce 0
   THEN (Trivial
   ORELSE ((CallByValueReduce 0⋅ THENA Auto)
           THEN RepUR ``spreadcons`` 0
           THEN Fold `spreadcons` 0
           THEN RepeatFor 2 ((CallByValueReduce 0⋅ THENA Auto)))
   )) }

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
⊢ 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

---

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)
\mvdash{}  \mforall{}as:A  List.  \mforall{}bs:T  List.    (ml-maprevappend(f;as;bs)  \msim{}  map(f;rev(as))  @  bs)


By

---

Latex:
(InductionOnList
  THEN  Intro
  THEN  RepUR  ``ml-maprevappend  ml\_apply``  0
  THEN  RW  (SweepUpC  UnrollRecursionC)  0
  THEN  Reduce  0
  THEN  RepeatFor  2  ((CallByValueReduce  0\mcdot{}  THENA  Auto))
  THEN  Reduce  0
  THEN  (Trivial
  ORELSE  ((CallByValueReduce  0\mcdot{}  THENA  Auto)
                  THEN  RepUR  ``spreadcons``  0
                  THEN  Fold  `spreadcons`  0
                  THEN  RepeatFor  2  ((CallByValueReduce  0\mcdot{}  THENA  Auto)))
  ))

---

Home Index