Step
*
1
2
1
1
of Lemma
not_total_enumerable_inc
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
7. 
(d (a + 1))
 False
BY
{ (Assert 

(f a (a + 1)) BY
         (InstHyp [
a
] 4
 THEN Auto))
 }
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
7. 
(d (a + 1))
8. 

(f a (a + 1))
 False
1.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}  {}\mrightarrow{}  \mBbbB{}@i
2.  \mforall{}b:\mBbbZ{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}a:\mBbbZ{}.  ((f  a)  =  b)@i
3.  d  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbB{}
4.  \mforall{}n:\mBbbZ{}.  (\muparrow{}(d  (n  +  1))  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}\mneg{}\msubb{}(f  n  (n  +  1)))
5.  a  :  \mBbbZ{}
6.  (f  a)  =  d
7.  \muparrow{}(d  (a  +  1))
\mvdash{}  False
By
(Assert  \muparrow{}\mneg{}\msubb{}(f  a  (a  +  1))  BY
              (InstHyp  [\mkleeneopen{}a\mkleeneclose{}]  4\mcdot{}  THEN  Auto))\mcdot{}
Home
Index