---

Step * 1 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
 R: List  
   ((l1,l2: List.  ((R (l1 @ l2))  (R l1)))
    (A:  . x:. ((R mklist(x;A))))
    (x:. l: List. ((x = ||l||)  (R l))))
BY
{ (InstConcl [l.y:. ((y < ||l||)  ((f y y = ff  l[y] = tt)  (f y y = tt  l[y] = ff)))] THEN Auto) }

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. (l.y:. ((y < ||l||)  ((f y y = ff  l[y] = tt)  (f y y = tt  l[y] = ff)))) (l1 @ l2)@i
 (l.y:. ((y < ||l||)  ((f y y = ff  l[y] = tt)  (f y y = tt  l[y] = ff)))) l1

2
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)))

3
1. f :     @i
2. a1,a2:.  (((f a1) = (f a2))  (a1 = a2))@i
3. b:  . a:. ((f a) = b)@i
4. x : @i
 l: List. ((x = ||l||)  ((l.y:. ((y < ||l||)  ((f y y = ff  l[y] = tt)  (f y y = tt  l[y] = ff)))) l))



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
\mvdash{}  \mexists{}R:\mBbbB{}  List  {}\mrightarrow{}  \mBbbP{}
      ((\mforall{}l1,l2:\mBbbB{}  List.    ((R  (l1  @  l2))  {}\mRightarrow{}  (R  l1)))
      \mwedge{}  (\mforall{}A:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}x:\mBbbN{}.  (\mneg{}(R  mklist(x;A))))
      \mwedge{}  (\mforall{}x:\mBbbN{}.  \mexists{}l:\mBbbB{}  List.  ((x  =  ||l||)  \mwedge{}  (R  l))))


By

(InstConcl  [\mkleeneopen{}\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)))\mkleeneclose{}]\mcdot{}\mcdot{}
  THEN  Auto
  )\mcdot{}



Home Index