---

Step * 1 1 2 of Lemma not_total_enumerable_inc


1. f :     @i
2. b:  . a:. ((f a) = b)@i
3. n : @i
4. (f n (n + 1))@i
 ((n.((f (n - 1) n))) (n + 1))
BY
{ (Reduce 0 THEN Auto) }



1.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbB{}@i
2.  \mforall{}b:\mBbbZ{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}a:\mBbbZ{}.  ((f  a)  =  b)@i
3.  n  :  \mBbbZ{}@i
4.  \muparrow{}\mneg{}\msubb{}(f  n  (n  +  1))@i
\mvdash{}  \muparrow{}((\mlambda{}n.(\mneg{}\msubb{}(f  (n  -  1)  n)))  (n  +  1))


By

(Reduce  0  THEN  Auto)



Home Index