---

Step * 1 1 of Lemma not_total_enumerable_inc

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

1
1. f :     @i
2. b:  . a:. ((f a) = b)@i
3. n : @i
4. ((n.((f (n - 1) n))) (n + 1))@i
 (f n (n + 1))

2
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))


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


By

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



Home Index