---

Step * 1 of Lemma peval-unroll


1. z : Top
2. v0 : Top
⊢ peval(v0;z) ~ extend-val(v0;fix((λ%,a. extend-val(v0;%;a)));z)
BY
{ (Unfold `peval` 0⋅
   THEN RW (SweepDnC AnyExtractC) 0
   THEN Reduce 0
   THEN RW (AddrC [1] UnrollRecursionC) 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  z  :  Top
2.  v0  :  Top
\mvdash{}  peval(v0;z)  \msim{}  extend-val(v0;fix((\mlambda{}\%,a.  extend-val(v0;\%;a)));z)


By

---

Latex:
(Unfold  `peval`  0\mcdot{}
  THEN  RW  (SweepDnC  AnyExtractC)  0
  THEN  Reduce  0
  THEN  RW  (AddrC  [1]  UnrollRecursionC)  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index