---

Step * 1 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. l1 :  List@i
7. l2 :  List@i
8. y:
     ((y < ||l1 @ l2||)
      ((((nsteps:. ((nsteps < ||l1 @ l2||)  ((T y nsteps))))  f y y = ff)  l1 @ l2[y] = tt)
         (((nsteps:. ((nsteps < ||l1 @ l2||)  ((T y nsteps))))  f y y = tt)  l1 @ l2[y] = ff)))@i
9. y : @i
10. y < ||l1||@i
11. (((nsteps:. ((nsteps < ||l1 @ l2||)  ((T y nsteps))))  f y y = ff)  l1 @ l2[y] = tt)
 (((nsteps:. ((nsteps < ||l1 @ l2||)  ((T y nsteps))))  f y y = tt)  l1 @ l2[y] = ff)
 (((nsteps:. ((nsteps < ||l1||)  ((T y nsteps))))  f y y = ff)  l1[y] = tt)
 (((nsteps:. ((nsteps < ||l1||)  ((T y nsteps))))  f y y = tt)  l1[y] = ff)
BY
{ (RWO "select_append_front" (-1) 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. y:
     ((y < ||l1 @ l2||)
      ((((nsteps:. ((nsteps < ||l1 @ l2||)  ((T y nsteps))))  f y y = ff)  l1 @ l2[y] = tt)
         (((nsteps:. ((nsteps < ||l1 @ l2||)  ((T y nsteps))))  f y y = tt)  l1 @ l2[y] = ff)))@i
9. y : @i
10. y < ||l1||@i
11. ((nsteps:. ((nsteps < ||l1 @ l2||)  ((T y nsteps))))  f y y = ff)  l1[y] = tt
12. ((nsteps:. ((nsteps < ||l1 @ l2||)  ((T y nsteps))))  f y y = tt)  l1[y] = ff
13. nsteps:. ((nsteps < ||l1||)  ((T y nsteps)))@i
14. f y y = ff@i
 l1[y] = tt

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. l1 :  List@i
7. l2 :  List@i
8. y:
     ((y < ||l1 @ l2||)
      ((((nsteps:. ((nsteps < ||l1 @ l2||)  ((T y nsteps))))  f y y = ff)  l1 @ l2[y] = tt)
         (((nsteps:. ((nsteps < ||l1 @ l2||)  ((T y nsteps))))  f y y = tt)  l1 @ l2[y] = ff)))@i
9. y : @i
10. y < ||l1||@i
11. ((nsteps:. ((nsteps < ||l1 @ l2||)  ((T y nsteps))))  f y y = ff)  l1[y] = tt
12. ((nsteps:. ((nsteps < ||l1 @ l2||)  ((T y nsteps))))  f y y = tt)  l1[y] = ff
13. nsteps:. ((nsteps < ||l1||)  ((T y nsteps)))@i
14. f y y = tt@i
 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{}  \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.  l1  :  \mBbbB{}  List@i
7.  l2  :  \mBbbB{}  List@i
8.  \mforall{}y:\mBbbN{}
          ((y  <  ||l1  @  l2||)
          {}\mRightarrow{}  ((((\mexists{}nsteps:\mBbbN{}.  ((nsteps  <  ||l1  @  l2||)  \mwedge{}  (\muparrow{}(T  y  nsteps))))  \mwedge{}  f  y  y  =  ff)  {}\mRightarrow{}  l1  @  l2[y]  =  tt)
                \mwedge{}  (((\mexists{}nsteps:\mBbbN{}.  ((nsteps  <  ||l1  @  l2||)  \mwedge{}  (\muparrow{}(T  y  nsteps))))  \mwedge{}  f  y  y  =  tt)
                    {}\mRightarrow{}  l1  @  l2[y]  =  ff)))@i
9.  y  :  \mBbbN{}@i
10.  y  <  ||l1||@i
11.  (((\mexists{}nsteps:\mBbbN{}.  ((nsteps  <  ||l1  @  l2||)  \mwedge{}  (\muparrow{}(T  y  nsteps))))  \mwedge{}  f  y  y  =  ff)  {}\mRightarrow{}  l1  @  l2[y]  =  tt)
\mwedge{}  (((\mexists{}nsteps:\mBbbN{}.  ((nsteps  <  ||l1  @  l2||)  \mwedge{}  (\muparrow{}(T  y  nsteps))))  \mwedge{}  f  y  y  =  tt)  {}\mRightarrow{}  l1  @  l2[y]  =  ff)
\mvdash{}  (((\mexists{}nsteps:\mBbbN{}.  ((nsteps  <  ||l1||)  \mwedge{}  (\muparrow{}(T  y  nsteps))))  \mwedge{}  f  y  y  =  ff)  {}\mRightarrow{}  l1[y]  =  tt)
\mwedge{}  (((\mexists{}nsteps:\mBbbN{}.  ((nsteps  <  ||l1||)  \mwedge{}  (\muparrow{}(T  y  nsteps))))  \mwedge{}  f  y  y  =  tt)  {}\mRightarrow{}  l1[y]  =  ff)


By

(RWO  "select\_append\_front"  (-1)
  THEN  Auto
  THEN  Try  (Complete  ((RepeatFor  2  (D  (-1))  THEN  Termination  THEN  Auto\mcdot{}))))



Home Index