---

Step * 1 2 1 1 2 of Lemma aa_not_total_enumerable


1. f :     @i
2. b:  . a:. ((f a) = b)@i
3. d :   
4. n:. ((d n)  (f n n))
5. a : 
6. (f a) = d
7. (d a)
 False
BY
{ (Assert (f a a) BY
         ((InstHyp [a] 4 THENA Auto) THEN (Assert (d a)  (f a a) BY MaAuto) THEN MaAuto)) }

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



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


By

(Assert  \muparrow{}(f  a  a)  BY
              ((InstHyp  [\mkleeneopen{}a\mkleeneclose{}]  4\mcdot{}  THENA  Auto)  THEN  (Assert  \muparrow{}\mneg{}\msubb{}(d  a)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(f  a  a)  BY  MaAuto)  THEN  MaAuto))



Home Index