Step * 2 1 1 of Lemma eager-map-append-sq


1. Type
2. value-type(T)
3. Type
4. A ⟶ T
5. A
6. List
7. ∀[bs:T List]. (eager-map-append(f;v;bs) map(f;rev(v)) bs)
8. bs List
⊢ map(f;rev(v)) eval in eval L' bs in   [x L'] map(f;rev(v) [u]) bs
BY
RepeatFor ((CallByValueReduce THENA Auto)) }

1
1. Type
2. value-type(T)
3. Type
4. A ⟶ T
5. A
6. List
7. ∀[bs:T List]. (eager-map-append(f;v;bs) map(f;rev(v)) bs)
8. bs List
⊢ map(f;rev(v)) [f bs] map(f;rev(v) [u]) bs


Latex:


Latex:

1.  T  :  Type
2.  value-type(T)
3.  A  :  Type
4.  f  :  A  {}\mrightarrow{}  T
5.  u  :  A
6.  v  :  A  List
7.  \mforall{}[bs:T  List].  (eager-map-append(f;v;bs)  \msim{}  map(f;rev(v))  @  bs)
8.  bs  :  T  List
\mvdash{}  map(f;rev(v))  @  eval  x  =  f  u  in  eval  L'  =  bs  in      [x  /  L']  \msim{}  map(f;rev(v)  @  [u])  @  bs


By


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




Home Index