---

Step * 1 3 2 2 1 1 of Lemma aa_kleene_fan_contra4


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. x : @i
7. y,m:.  Dec(nsteps:m. ((T y nsteps)))
8. halt :     
9. y,m:.  (nsteps:m. ((T y nsteps))  (halt y m))
10. y : @i
11. m : @i
12. (halt y m)@i
 (f y y)
BY
{ (RWO "-4<" (-1) THENA Auto) }

1
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. x : @i
7. y,m:.  Dec(nsteps:m. ((T y nsteps)))
8. halt :     
9. y,m:.  (nsteps:m. ((T y nsteps))  (halt y m))
10. y : @i
11. m : @i
12. nsteps:m. ((T y nsteps))
 (f y y)



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.  x  :  \mBbbN{}@i
7.  \mforall{}y,m:\mBbbN{}.    Dec(\mexists{}nsteps:\mBbbN{}m.  (\muparrow{}(T  y  nsteps)))
8.  halt  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
9.  \mforall{}y,m:\mBbbN{}.    (\mexists{}nsteps:\mBbbN{}m.  (\muparrow{}(T  y  nsteps))  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(halt  y  m))
10.  y  :  \mBbbN{}@i
11.  m  :  \mBbbN{}@i
12.  \muparrow{}(halt  y  m)@i
\mvdash{}  (f  y  y)\mdownarrow{}


By

(RWO  "-4<"  (-1)  THENA  Auto)



Home Index