---

Step * 1 1 of Lemma aa_not_total_enumerable

.....assertion..... 
1. f :     @i
2. b:  . a:. ((f a) = b)@i
 d:  . n:. ((d n)  (f n n))
BY
{ (InstConcl [n.((f n n))] THEN Auto) }


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


By

(InstConcl  [\mkleeneopen{}\mlambda{}n.(\mneg{}\msubb{}(f  n  n))\mkleeneclose{}]\mcdot{}  THEN  Auto)



Home Index