---

Step * 1 1 of Lemma atomic-values-evalall


1. v : Base
2. (v)↓
3. ↑if v is a pair then ff otherwise if v is inl then ff
                                     else if v is inr then ff
                                          else tt
⊢ (evalall(v))↓
BY
{ (RecUnfold `evalall` 0 THEN (CallByValueReduce 0 THENA Auto) THEN Repeat (HVimplies2 3 [1])) }

---

Latex:

---

Latex:

1.  v  :  Base
2.  (v)\mdownarrow{}
3.  \muparrow{}if  v  is  a  pair  then  ff  otherwise  if  v  is  inl  then  ff
                                                                          else  if  v  is  inr  then  ff
                                                                                    else  tt
\mvdash{}  (evalall(v))\mdownarrow{}


By

---

Latex:
(RecUnfold  `evalall`  0  THEN  (CallByValueReduce  0  THENA  Auto)  THEN  Repeat  (HVimplies2  3  [1]))

---

Home Index