---

Step * of Lemma test-cbv-normalize

∀[a,B:Top].  (eval x = a in <let y ⟵ x in B[y], eval z = a in B[z] + 22, eval w = a in B[w] + 3 + 1> ~ eval x = a in <l\000Cet y ⟵ x in B[y], B[x] + 22, (B[x] + 3) + 1>)
BY
{ (NormalizeCbv 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,B:Top].
    (eval  x  =  a  in
      <let  y  \mleftarrow{}{}  x  in  B[y],  eval  z  =  a  in  B[z]  +  22,  eval  w  =  a  in  B[w]  +  3  +  1>  \msim{}  eval  x  =  a  in
                                                                <let  y  \mleftarrow{}{}  x  in  B[y],  B[x]  +  22,  (B[x]  +  3)  +  1>)


By

---

Latex:
(NormalizeCbv  0  THEN  Auto)

---

Home Index