---

Step * 1 of Lemma aa_kleene_fan_contra_partial_imax


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

1
1. f :     bar()@i
2. b:  bar(). a:. ((f a) = b)@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
5. l1 :  List@i
6. l2 :  List@i
7. (l.y:
         ((y < ||l||)
          (((((T y y ||l||))  f y y = ff)  l[y] = tt)  ((((T y y ||l||))  f y y = tt)  l[y] = ff)))) 
   (l1 @ l2)@i
 (l.y:
        ((y < ||l||)
         (((((T y y ||l||))  f y y = ff)  l[y] = tt)  ((((T y y ||l||))  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. 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
5. A :   @i
 x:
   (((l.y:
            ((y < ||l||)
             (((((T y y ||l||))  f y y = ff)  l[y] = tt)  ((((T y y ||l||))  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. 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
5. x : @i
 l: List
   ((x = ||l||)
    ((l.y:
            ((y < ||l||)
             (((((T y y ||l||))  f y y = ff)  l[y] = tt)  ((((T y y ||l||))  f y y = tt)  l[y] = ff)))) 
      l))



1.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{})@i
2.  Surj(\mBbbN{};\mBbbN{}  {}\mrightarrow{}  bar(\mBbbB{});f)@i
3.  T  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}@i
4.  \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
\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

(Unfold  `surject`  2\mcdot{}
  THEN  InstConcl  [\mkleeneopen{}\mlambda{}l.\mforall{}y:\mBbbN{}
                                              ((y  <  ||l||)
                                              {}\mRightarrow{}  ((((\muparrow{}(T  y  y  ||l||))  \mwedge{}  f  y  y  =  ff)  {}\mRightarrow{}  l[y]  =  tt)
                                                    \mwedge{}  (((\muparrow{}(T  y  y  ||l||))  \mwedge{}  f  y  y  =  tt)  {}\mRightarrow{}  l[y]  =  ff)))\mkleeneclose{}]\mcdot{}\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  (Termination  THEN  Auto\mcdot{})))



Home Index