---

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


1. b : Base
2. u : rec-value()
3. v : rec-value() List
4. (evalall(v @ b))↓ ⇒ (b ∈ rec-value())
5. (evalall([u / (v @ b)]))↓
⊢ b ∈ rec-value()
BY
{ (RWO "evalall-cons" (-1) THEN Auto THEN HasValueD (-1) THEN HasValueD (-2) THEN Auto) }

---

Latex:

---

Latex:

1.  b  :  Base
2.  u  :  rec-value()
3.  v  :  rec-value()  List
4.  (evalall(v  @  b))\mdownarrow{}  {}\mRightarrow{}  (b  \mmember{}  rec-value())
5.  (evalall([u  /  (v  @  b)]))\mdownarrow{}
\mvdash{}  b  \mmember{}  rec-value()


By

---

Latex:
(RWO  "evalall-cons"  (-1)  THEN  Auto  THEN  HasValueD  (-1)  THEN  HasValueD  (-2)  THEN  Auto)

---

Home Index