---

Step * of Lemma enum_not_fan

(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)  (R (l1 @ l2))))  (A:  . n:. (R mklist(n;A))))
         (n:. A:  . (R mklist(n;A))))))
BY
{ (RepUR ``surject`` 0 THEN Auto THEN (D 0 THENA Auto) THEN (InstLemma `aa_kleene_fan_contra_partial` [] THENA Auto)) }

1
.....antecedent..... 
1. f:    bar()
    ((b:  bar(). a:. ((f a) = b))
     (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)))))))@i
2. R: List  
     (((l1,l2: List.  ((R l1)  (R (l1 @ l2))))  (A:  . n:. (R mklist(n;A))))
      (n:. A:  . (R mklist(n;A))))@i'
 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)))))))

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


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


By

(RepUR  ``surject``  0
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  (InstLemma  `aa\_kleene\_fan\_contra\_partial`  []\mcdot{}  THENA  Auto))



Home Index