---

Step * 1 2 of Lemma aa_kleene_fan_contra2


1. f :     @i
2. a1,a2:.  (((f a1) = (f a2))  (a1 = a2))@i
3. b:  . a:. ((f a) = b)@i
4. A :   @i
 x:. (((l.y:. ((y < ||l||)  ((f y y = ff  l[y] = tt)  (f y y = tt  l[y] = ff)))) mklist(x;A)))
BY
{ ((((Reduce 0 THEN InstHyp [A] 3)
     THENA Auto
     THENA skip{use the bijection to invert the function and get index as a})
    THEN D (-1)
    THEN (InstConcl [a + 1] THENA Auto THENA skip{anything > a works}))
   THEN D 0
   THEN Auto
   THEN InstLemma `mklist_length` [A;a + 1]
   THEN Auto
   THEN (Assert ||mklist(a + 1;A)|| = (a + 1) BY
               MaAuto)) }

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)||)
      ((f y y = ff  mklist(a + 1;A)[y] = tt)  (f y y = tt  mklist(a + 1;A)[y] = ff)))@i
8. ||mklist(a + 1;A)|| ~ a + 1
9. ||mklist(a + 1;A)|| = (a + 1)
 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
\mvdash{}  \mexists{}x:\mBbbN{}
      (\mneg{}((\mlambda{}l.\mforall{}y:\mBbbN{}.  ((y  <  ||l||)  {}\mRightarrow{}  ((f  y  y  =  ff  {}\mRightarrow{}  l[y]  =  tt)  \mwedge{}  (f  y  y  =  tt  {}\mRightarrow{}  l[y]  =  ff)))) 
            mklist(x;A)))


By

((((Reduce  0  THEN  InstHyp  [\mkleeneopen{}A\mkleeneclose{}]  3\mcdot{})
      THENA  Auto
      THENA  skip\{use  the  bijection  to  invert  the  function  and  get  index  as  a\})
    THEN  D  (-1)
    THEN  (InstConcl  [\mkleeneopen{}a  +  1\mkleeneclose{}]\mcdot{}  THENA  Auto  THENA  skip\{anything  >  a  works\}))
  THEN  D  0
  THEN  Auto
  THEN  InstLemma  `mklist\_length`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}a  +  1\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (Assert  ||mklist(a  +  1;A)||  =  (a  +  1)  BY
                          MaAuto))



Home Index