---

Step * 1 of Lemma aa_kleene_fan_contra4


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))))
BY
{ (InstConcl [l.y:
                    ((y < ||l||)
                     ((((nsteps:. ((nsteps < ||l||)  ((T y nsteps))))  f y y = ff)  l[y] = tt)
                        (((nsteps:. ((nsteps < ||l||)  ((T y nsteps))))  f y y = tt)  l[y] = ff)))]
   THEN Auto
   THEN Try (Complete ((RepeatFor 2 (D (-1)) THEN Termination THEN Auto)))) }

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
6. l1 :  List@i
7. l2 :  List@i
8. (l.y:
         ((y < ||l||)
          ((((nsteps:. ((nsteps < ||l||)  ((T y nsteps))))  f y y = ff)  l[y] = tt)
             (((nsteps:. ((nsteps < ||l||)  ((T y nsteps))))  f y y = tt)  l[y] = ff)))) 
   (l1 @ l2)@i
 (l.y:
        ((y < ||l||)
         ((((nsteps:. ((nsteps < ||l||)  ((T y nsteps))))  f y y = ff)  l[y] = tt)
            (((nsteps:. ((nsteps < ||l||)  ((T y nsteps))))  f y y = tt)  l[y] = ff)))) 
  l1

2
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
6. A :   @i
 x:
   (((l.y:
            ((y < ||l||)
             ((((nsteps:. ((nsteps < ||l||)  ((T y nsteps))))  f y y = ff)  l[y] = tt)
                (((nsteps:. ((nsteps < ||l||)  ((T y nsteps))))  f y y = tt)  l[y] = ff)))) 
      mklist(x;A)))

3
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
6. x : @i
 l: List
   ((x = ||l||)
    ((l.y:
            ((y < ||l||)
             ((((nsteps:. ((nsteps < ||l||)  ((T y nsteps))))  f y y = ff)  l[y] = tt)
                (((nsteps:. ((nsteps < ||l||)  ((T y nsteps))))  f y y = tt)  l[y] = ff)))) 
      l))



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{}  \mBbbB{}@i
4.  \mforall{}i,nsteps:\mBbbN{}.    ((\muparrow{}(T  i  nsteps))  {}\mRightarrow{}  (f  i  i)\mdownarrow{})@i
5.  \mforall{}i:\mBbbN{}.  ((f  i  i)\mdownarrow{}  {}\mRightarrow{}  (\mexists{}nsteps:\mBbbN{}.  (\muparrow{}(T  i  nsteps))))@i
\mvdash{}  \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

(InstConcl  [\mkleeneopen{}\mlambda{}l.\mforall{}y:\mBbbN{}
                                    ((y  <  ||l||)
                                    {}\mRightarrow{}  ((((\mexists{}nsteps:\mBbbN{}.  ((nsteps  <  ||l||)  \mwedge{}  (\muparrow{}(T  y  nsteps))))  \mwedge{}  f  y  y  =  ff)
                                          {}\mRightarrow{}  l[y]  =  tt)
                                          \mwedge{}  (((\mexists{}nsteps:\mBbbN{}.  ((nsteps  <  ||l||)  \mwedge{}  (\muparrow{}(T  y  nsteps))))  \mwedge{}  f  y  y  =  tt)
                                              {}\mRightarrow{}  l[y]  =  ff)))\mkleeneclose{}]\mcdot{}\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  ((RepeatFor  2  (D  (-1))  THEN  Termination  THEN  Auto\mcdot{}))))\mcdot{}



Home Index