---

Step * 1 2 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
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)))
BY
{ (((Reduce 0 THEN InstHyp [A] 2) THENA Auto)
   THEN skip{use the bijection to invert the function and get index as a}
   THEN D (-1)
   THEN Assert (f a) = A
   THEN skip{need to show that they are equal in non-bar type}) }

1
.....assertion..... 
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
7. a : 
8. (f a) = A
 (f a) = A

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
7. a : 
8. (f a) = A
9. (f a) = A
 x:
   ((y:
        ((y < ||mklist(x;A)||)
         ((((nsteps:. ((nsteps < ||mklist(x;A)||)  ((T y nsteps))))  f y y = ff)  mklist(x;A)[y] = tt)
            (((nsteps:. ((nsteps < ||mklist(x;A)||)  ((T y nsteps))))  f y y = tt)  mklist(x;A)[y] = ff)))))



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
6.  A  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}@i
\mvdash{}  \mexists{}x:\mBbbN{}
      (\mneg{}((\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)))) 
            mklist(x;A)))


By

(((Reduce  0  THEN  InstHyp  [\mkleeneopen{}A\mkleeneclose{}]  2\mcdot{})  THENA  Auto)
  THEN  skip\{use  the  bijection  to  invert  the  function  and  get  index  as  a\}
  THEN  D  (-1)
  THEN  Assert  \mkleeneopen{}(f  a)  =  A\mkleeneclose{}\mcdot{}
  THEN  skip\{need  to  show  that  they  are  equal  in  non-bar  type\})\mcdot{}



Home Index