---

Step * 1 2 1 1 of Lemma aa_kleene_fan_contra_partial_imax

.....wf..... 
1. f :     bar()@i
2. b:  bar(). a:. ((f a) = b)@i
3. T :       @i
4. indx,input:.
     ((nsteps:. (((T indx input nsteps))  (f indx input)))
      ((f indx input)  (nsteps:. ((T indx input nsteps))))
      (n1,n2:.  (((n1  n2)  ((T indx input n1)))  ((T indx input n2)))))@i
5. A :   @i
6. a : 
7. (f a) = A
8. z :   bar()
9. z = A
 z = A  
BY
{ ((MemCD THEN Try (Complete (Auto))) THEN ExtWith [`n'] [  bar()] THEN Try (Complete (Auto))) }

1
1. f :     bar()@i
2. b:  bar(). a:. ((f a) = b)@i
3. T :       @i
4. indx,input:.
     ((nsteps:. (((T indx input nsteps))  (f indx input)))
      ((f indx input)  (nsteps:. ((T indx input nsteps))))
      (n1,n2:.  (((n1  n2)  ((T indx input n1)))  ((T indx input n2)))))@i
5. A :   @i
6. a : 
7. (f a) = A
8. z :   bar()
9. z = A
10. n : 
 z n  


.....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{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}@i
4.  \mforall{}indx,input:\mBbbN{}.
          ((\mforall{}nsteps:\mBbbN{}.  ((\muparrow{}(T  indx  input  nsteps))  {}\mRightarrow{}  (f  indx  input)\mdownarrow{}))
          \mwedge{}  ((f  indx  input)\mdownarrow{}  {}\mRightarrow{}  (\mexists{}nsteps:\mBbbN{}.  (\muparrow{}(T  indx  input  nsteps))))
          \mwedge{}  (\mforall{}n1,n2:\mBbbN{}.    (((n1  \mleq{}  n2)  \mwedge{}  (\muparrow{}(T  indx  input  n1)))  {}\mRightarrow{}  (\muparrow{}(T  indx  input  n2)))))@i
5.  A  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}@i
6.  a  :  \mBbbN{}
7.  (f  a)  =  A
8.  z  :  \mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{})
9.  z  =  A
\mvdash{}  z  =  A  \mmember{}  \mBbbP{}


By

((MemCD  THEN  Try  (Complete  (Auto)))  THEN  ExtWith  [`n']  [\mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{})]\mcdot{}  THEN  Try  (Complete  (Auto)))\mcdot{}



Home Index