---

Step * 1 of Lemma evalall-append-implies-list


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index