---

Step * 1 3 2 2 2 2 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,m:.  (((halt y m))  (f y y  ))
11. y.if halt y x then (f y y) else ff fi     
 l: List
   ((x = ||l||)
    ((l.y:
            ((y < ||l||)
             ((((nsteps:. ((nsteps < ||l||)  ((T y nsteps))))  f y y = ff)  l[y] = tt)
                (((nsteps:. ((nsteps < ||l||)  ((T y nsteps))))  f y y = tt)  l[y] = ff)))) 
      l))
BY
{ (Reduce 0 THEN InstConcl [mklist(x;y.if halt y x then (f y y) else ff fi )] THEN Try (Complete (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,m:.  (((halt y m))  (f y y  ))
11. y.if halt y x then (f y y) else ff fi     
 (x = ||mklist(x;y.if halt y x then (f y y) else ff fi )||)
 (y:
     ((y < ||mklist(x;y.if halt y x then (f y y) else ff fi )||)
      ((((nsteps:. ((nsteps < ||mklist(x;y.if halt y x then (f y y) else ff fi )||)  ((T y nsteps))))
         f y y = ff)
         mklist(x;y.if halt y x then (f y y) else ff fi )[y] = tt)
         (((nsteps:. ((nsteps < ||mklist(x;y.if halt y x then (f y y) else ff fi )||)  ((T y nsteps))))
           f y y = tt)
           mklist(x;y.if halt y x then (f y y) else ff fi )[y] = ff))))

2
.....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. 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,m:.  (((halt y m))  (f y y  ))
11. y.if halt y x then (f y y) else ff fi     
12. l :  List
 (x = ||l||)
   (y:
       ((y < ||l||)
        ((((nsteps:. ((nsteps < ||l||)  ((T y nsteps))))  f y y = ff)  l[y] = tt)
           (((nsteps:. ((nsteps < ||l||)  ((T y nsteps))))  f y y = tt)  l[y] = ff))))  



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.  \mforall{}y,m:\mBbbN{}.    ((\muparrow{}(halt  y  m))  {}\mRightarrow{}  (f  y  y  \mmember{}  \mBbbB{}))
11.  \mlambda{}y.if  halt  y  x  then  \mneg{}\msubb{}(f  y  y)  else  ff  fi    \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  \mexists{}l:\mBbbB{}  List
      ((x  =  ||l||)
      \mwedge{}  ((\mlambda{}l.\mforall{}y:\mBbbN{}
                        ((y  <  ||l||)
                        {}\mRightarrow{}  ((((\mexists{}nsteps:\mBbbN{}.  ((nsteps  <  ||l||)  \mwedge{}  (\muparrow{}(T  y  nsteps))))  \mwedge{}  f  y  y  =  ff)  {}\mRightarrow{}  l[y]  =  tt)
                              \mwedge{}  (((\mexists{}nsteps:\mBbbN{}.  ((nsteps  <  ||l||)  \mwedge{}  (\muparrow{}(T  y  nsteps))))  \mwedge{}  f  y  y  =  tt)  {}\mRightarrow{}  l[y]  =  ff)))) 
            l))


By

(Reduce  0
  THEN  InstConcl  [\mkleeneopen{}mklist(x;\mlambda{}y.if  halt  y  x  then  \mneg{}\msubb{}(f  y  y)  else  ff  fi  )\mkleeneclose{}]\mcdot{}
  THEN  Try  (Complete  (Auto)))



Home Index