Step
*
1
1
of Lemma
data-stream-cons
.....wf..... 
1. L : Top List
2. a : Top
3. P : Top
⊢ ||[a / L]|| ∈ ℕ+
BY
{ (Auto THEN Auto') }
Latex:
Latex:
.....wf..... 
1.  L  :  Top  List
2.  a  :  Top
3.  P  :  Top
\mvdash{}  ||[a  /  L]||  \mmember{}  \mBbbN{}\msupplus{}
By
Latex:
(Auto  THEN  Auto')
Home
Index