---

Step * 2 of Lemma enum_not_fan2


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
BY
{ (D (-1) THEN InstHyp [l.((R l))] 2 THEN Auto THEN MaAuto) }

1
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  
4. l1,l2: List.  ((R (l1 @ l2))  (R l1))
5. A:  . x:. ((R mklist(x;A)))
6. x:. l: List. ((x = ||l||)  (R l))
7. l1 :  List@i
8. l2 :  List@i
9. (l.((R l))) l1@i
 (R (l1 @ l2))

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  
4. l1,l2: List.  ((R (l1 @ l2))  (R l1))
5. A:  . x:. ((R mklist(x;A)))
6. x:. l: List. ((x = ||l||)  (R l))
7. A :   @i
 n:. ((l.((R l))) mklist(n;A))

3
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  
4. l1,l2: List.  ((R (l1 @ l2))  (R l1))
5. A:  . x:. ((R mklist(x;A)))
6. x:. l: List. ((x = ||l||)  (R l))
7. n:. A:  . ((l.((R l))) mklist(n;A))
 False



1.  \mexists{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{})
        ((\mforall{}b:\mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{}).  \mexists{}a:\mBbbN{}.  ((f  a)  =  b))
        \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)))))))@i
2.  \mforall{}R:\mBbbB{}  List  {}\mrightarrow{}  \mBbbP{}
          ((\mforall{}l1,l2:\mBbbB{}  List.    ((R  l1)  {}\mRightarrow{}  (R  (l1  @  l2))))
          {}\mRightarrow{}  (\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))))@i'
3.  \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))))
\mvdash{}  False


By

(D  (-1)  THEN  InstHyp  [\mkleeneopen{}\mlambda{}l.(\mneg{}(R  l))\mkleeneclose{}]  2\mcdot{}  THEN  Auto  THEN  MaAuto)



Home Index