---

Step * 1 1 2 1 of Lemma aa_kleene_fan_contra


1. f :     @i
2. a1,a2:.  (((f a1) = (f a2))  (a1 = a2))@i
3. b:  . a:. ((f a) = b)@i
4. l1 :  List@i
5. l2 :  List@i
6. y:
     ((y < ||l1 @ l2||)
      ((((y < ||l1 @ l2||)  f y y = ff)  l1 @ l2[y] = tt)
         (((y < ||l1 @ l2||)  f y y = tt)  l1 @ l2[y] = ff)))@i
7. y : @i
8. y < ||l1||@i
9. (((y < ||l1 @ l2||)  f y y = ff)  l1[y] = tt)  (((y < ||l1 @ l2||)  f y y = tt)  l1[y] = ff)
10. l1 @ l2[y] = l1[y]
 (((y < ||l1||)  f y y = ff)  l1[y] = tt)  (((y < ||l1||)  f y y = tt)  l1[y] = ff)
BY
{ (Assert y < ||l1 @ l2|| BY
         MaAuto) }

1
1. f :     @i
2. a1,a2:.  (((f a1) = (f a2))  (a1 = a2))@i
3. b:  . a:. ((f a) = b)@i
4. l1 :  List@i
5. l2 :  List@i
6. y:
     ((y < ||l1 @ l2||)
      ((((y < ||l1 @ l2||)  f y y = ff)  l1 @ l2[y] = tt)
         (((y < ||l1 @ l2||)  f y y = tt)  l1 @ l2[y] = ff)))@i
7. y : @i
8. y < ||l1||@i
9. (((y < ||l1 @ l2||)  f y y = ff)  l1[y] = tt)  (((y < ||l1 @ l2||)  f y y = tt)  l1[y] = ff)
10. l1 @ l2[y] = l1[y]
11. y < ||l1 @ l2||
 (((y < ||l1||)  f y y = ff)  l1[y] = tt)  (((y < ||l1||)  f y y = tt)  l1[y] = ff)



1.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}@i
2.  \mforall{}a1,a2:\mBbbN{}.    (((f  a1)  =  (f  a2))  {}\mRightarrow{}  (a1  =  a2))@i
3.  \mforall{}b:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}a:\mBbbN{}.  ((f  a)  =  b)@i
4.  l1  :  \mBbbB{}  List@i
5.  l2  :  \mBbbB{}  List@i
6.  \mforall{}y:\mBbbN{}
          ((y  <  ||l1  @  l2||)
          {}\mRightarrow{}  ((((y  <  ||l1  @  l2||)  \mwedge{}  f  y  y  =  ff)  {}\mRightarrow{}  l1  @  l2[y]  =  tt)
                \mwedge{}  (((y  <  ||l1  @  l2||)  \mwedge{}  f  y  y  =  tt)  {}\mRightarrow{}  l1  @  l2[y]  =  ff)))@i
7.  y  :  \mBbbN{}@i
8.  y  <  ||l1||@i
9.  (((y  <  ||l1  @  l2||)  \mwedge{}  f  y  y  =  ff)  {}\mRightarrow{}  l1[y]  =  tt)
\mwedge{}  (((y  <  ||l1  @  l2||)  \mwedge{}  f  y  y  =  tt)  {}\mRightarrow{}  l1[y]  =  ff)
10.  l1  @  l2[y]  =  l1[y]
\mvdash{}  (((y  <  ||l1||)  \mwedge{}  f  y  y  =  ff)  {}\mRightarrow{}  l1[y]  =  tt)  \mwedge{}  (((y  <  ||l1||)  \mwedge{}  f  y  y  =  tt)  {}\mRightarrow{}  l1[y]  =  ff)


By

(Assert  y  <  ||l1  @  l2||  BY
              MaAuto)



Home Index