---

Step * of Lemma aa_fib_count_wf

n:. (aa_fib_count(n)    )
BY
{ ((D 0 THENA Auto) THEN CompNatInd 1) }

1
1. n : @i
2. n1:. aa_fib_count(n1)     supposing n1 < n
 aa_fib_count(n)    


\mforall{}n:\mBbbN{}.  (aa\_fib\_count(n)  \mmember{}  \mBbbN{}  \mtimes{}  \mBbbN{})


By

((D  0  THENA  Auto)  THEN  CompNatInd  1)



Home Index