---

Step * 1 1 2 1 of Lemma aa_fib_count_wf


1. n : @i
2. n1:. aa_fib_count(n1)     supposing n1 < n
3. ((n = 0)  (n = 1))
 (n = 0)
BY
{ (((D 0 THENA Auto) THEN (D 3 THENA Auto)) THEN OrLeft 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  =  0)


By

(((D  0  THENA  Auto)  THEN  (D  3  THENA  Auto))  THEN  OrLeft  THEN  Auto)



Home Index