---

Step * 1 2 2 1 1 2 of Lemma aa_kleene_fan_contra4

.....wf..... 
1. f :     bar()@i
2. b:  bar(). a:. ((f a) = b)@i
3. T :     @i
4. i,nsteps:.  (((T i nsteps))  (f i i))@i
5. i:. ((f i i)  (nsteps:. ((T i nsteps))))@i
6. A :   @i
7. a : 
8. (f a) = A
9. (f a) = A
10. (A a)
11. (f a a)
12. nsteps : 
13. (T a nsteps)
14. x : 
15. y : @i
16. y < ||mklist(x;A)||
17. nsteps:. ((nsteps < ||mklist(x;A)||)  ((T y nsteps)))
 f y y  
BY
{ (RepeatFor 2 (D (-1)) THEN Termination THEN Auto) }


.....wf..... 
1.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{})@i
2.  \mforall{}b:\mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{}).  \mexists{}a:\mBbbN{}.  ((f  a)  =  b)@i
3.  T  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}@i
4.  \mforall{}i,nsteps:\mBbbN{}.    ((\muparrow{}(T  i  nsteps))  {}\mRightarrow{}  (f  i  i)\mdownarrow{})@i
5.  \mforall{}i:\mBbbN{}.  ((f  i  i)\mdownarrow{}  {}\mRightarrow{}  (\mexists{}nsteps:\mBbbN{}.  (\muparrow{}(T  i  nsteps))))@i
6.  A  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}@i
7.  a  :  \mBbbN{}
8.  (f  a)  =  A
9.  (f  a)  =  A
10.  (A  a)\mdownarrow{}
11.  (f  a  a)\mdownarrow{}
12.  nsteps  :  \mBbbN{}
13.  \muparrow{}(T  a  nsteps)
14.  x  :  \mBbbN{}
15.  y  :  \mBbbN{}@i
16.  y  <  ||mklist(x;A)||
17.  \mexists{}nsteps:\mBbbN{}.  ((nsteps  <  ||mklist(x;A)||)  \mwedge{}  (\muparrow{}(T  y  nsteps)))
\mvdash{}  f  y  y  \mmember{}  \mBbbB{}


By

(RepeatFor  2  (D  (-1))  THEN  Termination  THEN  Auto\mcdot{})\mcdot{}



Home Index