---

Step * 1 2 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. A :   @i
5. a : 
6. (f a) = A
7. y:
     ((y < ||mklist(a + 1;A)||)
      ((((y < ||mklist(a + 1;A)||)  f y y = ff)  mklist(a + 1;A)[y] = tt)
         (((y < ||mklist(a + 1;A)||)  f y y = tt)  mklist(a + 1;A)[y] = ff)))@i
8. (((a < ||mklist(a + 1;A)||)  A a = ff)  mklist(a + 1;A)[a] = tt)
 (((a < ||mklist(a + 1;A)||)  A a = tt)  mklist(a + 1;A)[a] = ff)
 False
BY
{ ((D (-1) THEN BoolCase A a) THENA Auto) }

1
1. f :     @i
2. a1,a2:.  (((f a1) = (f a2))  (a1 = a2))@i
3. b:  . a:. ((f a) = b)@i
4. A :   @i
5. a : 
6. (f a) = A
7. y:
     ((y < ||mklist(a + 1;A)||)
      ((((y < ||mklist(a + 1;A)||)  f y y = ff)  mklist(a + 1;A)[y] = tt)
         (((y < ||mklist(a + 1;A)||)  f y y = tt)  mklist(a + 1;A)[y] = ff)))@i
8. ((a < ||mklist(a + 1;A)||)  A a = ff)  mklist(a + 1;A)[a] = tt
9. ((a < ||mklist(a + 1;A)||)  A a = tt)  mklist(a + 1;A)[a] = ff
10. (A a)
 False

2
1. f :     @i
2. a1,a2:.  (((f a1) = (f a2))  (a1 = a2))@i
3. b:  . a:. ((f a) = b)@i
4. A :   @i
5. a : 
6. (f a) = A
7. y:
     ((y < ||mklist(a + 1;A)||)
      ((((y < ||mklist(a + 1;A)||)  f y y = ff)  mklist(a + 1;A)[y] = tt)
         (((y < ||mklist(a + 1;A)||)  f y y = tt)  mklist(a + 1;A)[y] = ff)))@i
8. ((a < ||mklist(a + 1;A)||)  A a = ff)  mklist(a + 1;A)[a] = tt
9. ((a < ||mklist(a + 1;A)||)  A a = tt)  mklist(a + 1;A)[a] = ff
10. (A a)
 False



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.  A  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}@i
5.  a  :  \mBbbN{}
6.  (f  a)  =  A
7.  \mforall{}y:\mBbbN{}
          ((y  <  ||mklist(a  +  1;A)||)
          {}\mRightarrow{}  ((((y  <  ||mklist(a  +  1;A)||)  \mwedge{}  f  y  y  =  ff)  {}\mRightarrow{}  mklist(a  +  1;A)[y]  =  tt)
                \mwedge{}  (((y  <  ||mklist(a  +  1;A)||)  \mwedge{}  f  y  y  =  tt)  {}\mRightarrow{}  mklist(a  +  1;A)[y]  =  ff)))@i
8.  (((a  <  ||mklist(a  +  1;A)||)  \mwedge{}  A  a  =  ff)  {}\mRightarrow{}  mklist(a  +  1;A)[a]  =  tt)
\mwedge{}  (((a  <  ||mklist(a  +  1;A)||)  \mwedge{}  A  a  =  tt)  {}\mRightarrow{}  mklist(a  +  1;A)[a]  =  ff)
\mvdash{}  False


By

((D  (-1)  THEN  BoolCase  \mkleeneopen{}A  a\mkleeneclose{}\mcdot{})  THENA  Auto)



Home Index