---

Step * of Lemma evalall-int

∀[x:ℤ]. (evalall(x) ~ x)
BY
{ (Auto
   THEN RW (AddrC [2] (RecUnfoldC `evalall`)) 0
   THEN (CallByValueReduce 0 THENA (Auto THEN Unfold `has-value` 0 THEN Refine_callbyvalueInt THEN Auto))) }

1
1. x : ℤ
⊢ if x is a pair then let a,b = x 
                      in eval a' = evalall(a) in
                         eval b' = evalall(b) in
                           <a', b'> otherwise if x is inl then eval y = evalall(outl(x)) in
                                                               inl y
                                              else if x is inr then eval y = evalall(outr(x)) in
                                                                    inr y 
                                                   else x
= x
∈ ℤ

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  (evalall(x)  \msim{}  x)


By

---

Latex:
(Auto
  THEN  RW  (AddrC  [2]  (RecUnfoldC  `evalall`))  0
  THEN  (CallByValueReduce  0
              THENA  (Auto  THEN  Unfold  `has-value`  0  THEN  Refine\_callbyvalueInt  THEN  Auto)
              ))

---

Home Index