---

Step * of Lemma eager_map_cons_lemma

∀v,u,f:Top.  (eager-map(f;[u / v]) ~ eval x = f u in eval r = eager-map(f;v) in   [x / r])
BY
{ (Auto
   THEN (RW  (AddrC [1] UnfoldTopAbC) 0 THEN Reduce 0 THEN Auto)
   THEN RW  (AddrC [2] UnfoldTopAbC) 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}v,u,f:Top.    (eager-map(f;[u  /  v])  \msim{}  eval  x  =  f  u  in  eval  r  =  eager-map(f;v)  in      [x  /  r])


By

---

Latex:
(Auto
  THEN  (RW    (AddrC  [1]  UnfoldTopAbC)  0  THEN  Reduce  0  THEN  Auto)
  THEN  RW    (AddrC  [2]  UnfoldTopAbC)  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index