---

Step * 1 1 2 2 of Lemma aa_fib_count_wf


1. n : @i
2. n1:. aa_fib_count(n1)     supposing n1 < n
3. ((n = 0)  (n = 1))
 (n = 1)
BY
{ (((D 0 THENA Auto) THEN (D 3 THENA Auto)) THEN OrRight THEN Auto) }



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


By

(((D  0  THENA  Auto)  THEN  (D  3  THENA  Auto))  THEN  OrRight  THEN  Auto)\mcdot{}



Home Index