Step
*
1
of Lemma
evalall-append-implies-rec-value
1. b : Base
2. v : rec-value() List
⊢ (evalall(v @ b))↓ 
⇒ (b ∈ rec-value())
BY
{ (ListInd (-1) THEN Reduce 0 THEN Auto) }
1
1. b : Base
2. (evalall(b))↓
⊢ b ∈ rec-value()
2
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()
Latex:
Latex:
1.  b  :  Base
2.  v  :  rec-value()  List
\mvdash{}  (evalall(v  @  b))\mdownarrow{}  {}\mRightarrow{}  (b  \mmember{}  rec-value())
By
Latex:
(ListInd  (-1)  THEN  Reduce  0  THEN  Auto)
Home
Index