---

Step * of Lemma aa_kleene_fan_contra

(f:    . Bij(;  ;f))
 (R: List  
     ((l1,l2: List.  ((R (l1 @ l2))  (R l1)))
      (A:  . x:. ((R mklist(x;A))))
      (x:. l: List. ((x = ||l||)  (R l)))))
BY
{ ((Auto THEN D 1) THEN Unfold `biject` 2 THEN Unfold `inject` 2 THEN Unfold `surject` 2 THEN D 2) }

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


(\mexists{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  Bij(\mBbbN{};\mBbbN{}  {}\mrightarrow{}  \mBbbB{};f))
{}\mRightarrow{}  (\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

((Auto  THEN  D  1)  THEN  Unfold  `biject`  2  THEN  Unfold  `inject`  2  THEN  Unfold  `surject`  2  THEN  D  2)



Home Index