---

Step * of Lemma aa_kleene_fan_contra_partial_imax

(f:    bar()
  (Surj(;  bar();f)
   (T:      
      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))))))))
 (R: List  
     ((l1,l2: List.  ((R (l1 @ l2))  (R l1)))
      (A:  . x:. ((R mklist(x;A))))
      (x:. l: List. ((x = ||l||)  (R l)))))
BY
{ (Auto THEN RepeatFor 3 (D (-1))) }

1
1. f :     bar()@i
2. Surj(;  bar();f)@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
 R: List  
   ((l1,l2: List.  ((R (l1 @ l2))  (R l1)))
    (A:  . x:. ((R mklist(x;A))))
    (x:. l: List. ((x = ||l||)  (R l))))


(\mexists{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{})
    (Surj(\mBbbN{};\mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{});f)
    \mwedge{}  (\mexists{}T:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
            \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))))))))
{}\mRightarrow{}  (\mexists{}R:\mBbbB{}  List  {}\mrightarrow{}  \mBbbP{}
          ((\mforall{}l1,l2:\mBbbB{}  List.    ((R  (l1  @  l2))  {}\mRightarrow{}  (R  l1)))
          \mwedge{}  (\mforall{}A:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}x:\mBbbN{}.  (\mneg{}(R  mklist(x;A))))
          \mwedge{}  (\mforall{}x:\mBbbN{}.  \mexists{}l:\mBbbB{}  List.  ((x  =  ||l||)  \mwedge{}  (R  l)))))


By

(Auto  THEN  RepeatFor  3  (D  (-1)))



Home Index