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


1. Base
2. rec-value() List
⊢ (evalall(v b))↓  (b ∈ rec-value())
BY
(ListInd (-1) THEN Reduce THEN Auto) }

1
1. Base
2. (evalall(b))↓
⊢ b ∈ rec-value()

2
1. Base
2. rec-value()
3. 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