---

Step * 1 2 of Lemma not_total_enumerable_inc


1. f :     @i
2. b:  . a:. ((f a) = b)@i
3. d:  . n:. ((d (n + 1))  (f n (n + 1)))
 False
BY
{ (D (-1) THEN (InstHyp [d] 2 THEN Auto) THEN D (-1)) }

1
1. f :     @i
2. b:  . a:. ((f a) = b)@i
3. d :   
4. n:. ((d (n + 1))  (f n (n + 1)))
5. a : 
6. (f a) = d
 False



1.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbB{}@i
2.  \mforall{}b:\mBbbZ{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}a:\mBbbZ{}.  ((f  a)  =  b)@i
3.  \mexists{}d:\mBbbZ{}  {}\mrightarrow{}  \mBbbB{}.  \mforall{}n:\mBbbZ{}.  (\muparrow{}(d  (n  +  1))  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}\mneg{}\msubb{}(f  n  (n  +  1)))
\mvdash{}  False


By

(D  (-1)  THEN  (InstHyp  [\mkleeneopen{}d\mkleeneclose{}]  2\mcdot{}\mcdot{}  THEN  Auto)  THEN  D  (-1))\mcdot{}



Home Index