---

Step * 1 1 1 of Lemma aa_fib_count_wf

.....truecase..... 
1. n : @i
2. n1:. aa_fib_count(n1)     supposing n1 < n
3. (n = 0)  (n = 1)
 <1, 0>    
BY
{ Auto' }


.....truecase..... 
1.  n  :  \mBbbN{}@i
2.  \mforall{}n1:\mBbbN{}.  aa\_fib\_count(n1)  \mmember{}  \mBbbN{}  \mtimes{}  \mBbbN{}  supposing  n1  <  n
3.  (n  =  0)  \mvee{}  (n  =  1)
\mvdash{}  ə,  0>  \mmember{}  \mBbbN{}  \mtimes{}  \mBbbN{}


By

Auto'



Home Index