---

Step * 1 1 of Lemma evalall-append-implies-rec-value


1. b : Base
2. (evalall(b))↓
⊢ b ∈ rec-value()
BY
{ (RWO "rec-value-evalall" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  b  :  Base
2.  (evalall(b))\mdownarrow{}
\mvdash{}  b  \mmember{}  rec-value()


By

---

Latex:
(RWO  "rec-value-evalall"  (-1)  THEN  Auto)

---

Home Index