---

Step * 1 1 1 of Lemma aa_kleene_fan_contra_partial


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. y:
     ((y < ||l1 @ l2||)
      (((((T y y ||l1 @ l2||))  f y y = ff)  l1 @ l2[y] = tt)
         ((((T y y ||l1 @ l2||))  f y y = tt)  l1 @ l2[y] = ff)))@i
8. ||l1||  ||l1 @ l2||
9. y : @i
10. y < ||l1||@i
11. ((((T y y ||l1 @ l2||))  f y y = ff)  l1 @ l2[y] = tt)
 ((((T y y ||l1 @ l2||))  f y y = tt)  l1 @ l2[y] = ff)
 ((((T y y ||l1||))  f y y = ff)  l1[y] = tt)  ((((T y y ||l1||))  f y y = tt)  l1[y] = ff)
BY
{ (Assert ((T y y ||l1||))  ((T y y ||l1 @ l2||)) BY
         ((InstHyp  [y;y] 4 THEN Auto) THEN InstHyp [||l1||;||l1 @ l2||] (-2) 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. y:
     ((y < ||l1 @ l2||)
      (((((T y y ||l1 @ l2||))  f y y = ff)  l1 @ l2[y] = tt)
         ((((T y y ||l1 @ l2||))  f y y = tt)  l1 @ l2[y] = ff)))@i
8. ||l1||  ||l1 @ l2||
9. y : @i
10. y < ||l1||@i
11. ((((T y y ||l1 @ l2||))  f y y = ff)  l1 @ l2[y] = tt)
 ((((T y y ||l1 @ l2||))  f y y = tt)  l1 @ l2[y] = ff)
12. ((T y y ||l1||))  ((T y y ||l1 @ l2||))
 ((((T y y ||l1||))  f y y = ff)  l1[y] = tt)  ((((T y y ||l1||))  f y y = tt)  l1[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{}  \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
5.  l1  :  \mBbbB{}  List@i
6.  l2  :  \mBbbB{}  List@i
7.  \mforall{}y:\mBbbN{}
          ((y  <  ||l1  @  l2||)
          {}\mRightarrow{}  ((((\muparrow{}(T  y  y  ||l1  @  l2||))  \mwedge{}  f  y  y  =  ff)  {}\mRightarrow{}  l1  @  l2[y]  =  tt)
                \mwedge{}  (((\muparrow{}(T  y  y  ||l1  @  l2||))  \mwedge{}  f  y  y  =  tt)  {}\mRightarrow{}  l1  @  l2[y]  =  ff)))@i
8.  ||l1||  \mleq{}  ||l1  @  l2||
9.  y  :  \mBbbN{}@i
10.  y  <  ||l1||@i
11.  (((\muparrow{}(T  y  y  ||l1  @  l2||))  \mwedge{}  f  y  y  =  ff)  {}\mRightarrow{}  l1  @  l2[y]  =  tt)
\mwedge{}  (((\muparrow{}(T  y  y  ||l1  @  l2||))  \mwedge{}  f  y  y  =  tt)  {}\mRightarrow{}  l1  @  l2[y]  =  ff)
\mvdash{}  (((\muparrow{}(T  y  y  ||l1||))  \mwedge{}  f  y  y  =  ff)  {}\mRightarrow{}  l1[y]  =  tt)
\mwedge{}  (((\muparrow{}(T  y  y  ||l1||))  \mwedge{}  f  y  y  =  tt)  {}\mRightarrow{}  l1[y]  =  ff)


By

(Assert  (\muparrow{}(T  y  y  ||l1||))  {}\mRightarrow{}  (\muparrow{}(T  y  y  ||l1  @  l2||))  BY
              ((InstHyp    [\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  4\mcdot{}  THEN  Auto)  THEN  InstHyp  [\mkleeneopen{}||l1||\mkleeneclose{};\mkleeneopen{}||l1  @  l2||\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto))



Home Index