---

Step * of Lemma aa_kleene_fan_contra4

(f:    bar()
  (Surj(;  bar();f)
   (T:    
      ((i,nsteps:.  (((T i nsteps))  (f i i)))  (i:. ((f i i)  (nsteps:. ((T i nsteps)))))))))
 (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 D 1) THEN Unfold `surject` 2) THEN D 2 THEN D 3 THEN D 4) }

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
 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{}  \mBbbB{}
            ((\mforall{}i,nsteps:\mBbbN{}.    ((\muparrow{}(T  i  nsteps))  {}\mRightarrow{}  (f  i  i)\mdownarrow{}))
            \mwedge{}  (\mforall{}i:\mBbbN{}.  ((f  i  i)\mdownarrow{}  {}\mRightarrow{}  (\mexists{}nsteps:\mBbbN{}.  (\muparrow{}(T  i  nsteps)))))))))
{}\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  D  1)  THEN  Unfold  `surject`  2)  THEN  D  2  THEN  D  3  THEN  D  4)



Home Index