---

Step * 1 of Lemma atomic-values-evalall


1. x : Base
2. x ∈ atomic-values()
⊢ (evalall(x))↓
BY
{ (GenConclAtAddr [1;1]⋅
   THEN ThinVar `x'
   THEN (D (-1) THEN SqUnhide)
   THEN (D (-2) THEN SqUnhide)
   THEN Unfold `is-atomic` (-1)) }

1
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))↓

---

Latex:

---

Latex:

1.  x  :  Base
2.  x  \mmember{}  atomic-values()
\mvdash{}  (evalall(x))\mdownarrow{}


By

---

Latex:
(GenConclAtAddr  [1;1]\mcdot{}
  THEN  ThinVar  `x'
  THEN  (D  (-1)  THEN  SqUnhide)
  THEN  (D  (-2)  THEN  SqUnhide)
  THEN  Unfold  `is-atomic`  (-1))

---

Home Index