---

Step * 2 of Lemma real-list-has-valueall


1. u : ℝ
2. v : ℝ List
3. has-valueall(v)
⊢ has-valueall([u / v])
BY
{ (RepUR ``has-valueall cons`` 0
   THEN RecUnfold `evalall` 0
   THEN Reduce 0
   THEN (CallByValueReduce 0 THENA (Fold `has-valueall` 0 THEN BLemma `real-has-valueall` THEN Auto))
   THEN (CallByValueReduce 0 THENA (Fold `has-valueall` 0 THEN Auto))) }

1
1. u : ℝ
2. v : ℝ List
3. has-valueall(v)
⊢ (<evalall(u), evalall(v)>)↓

---

Latex:

---

Latex:

1.  u  :  \mBbbR{}
2.  v  :  \mBbbR{}  List
3.  has-valueall(v)
\mvdash{}  has-valueall([u  /  v])


By

---

Latex:
(RepUR  ``has-valueall  cons``  0
  THEN  RecUnfold  `evalall`  0
  THEN  Reduce  0
  THEN  (CallByValueReduce  0  THENA  (Fold  `has-valueall`  0  THEN  BLemma  `real-has-valueall`  THEN  Auto))
  THEN  (CallByValueReduce  0  THENA  (Fold  `has-valueall`  0  THEN  Auto)))

---

Home Index