---

Step * 3 1 of Lemma brouwer_prin_for_num27_2_equiv


1. A:      
     ((f:  . b:. (A f b))
      (T: List  
          f:  
            y:. (((T mklist(y;f)) > 0)  (x:. (((T mklist(x;f)) > 0)  (y = x)))  (A f (T mklist(y;f)--1)))))@i'
2. A :       @i'
3. f:  . b:. (A f b)@i
4. T :  List  
5. f:  . y:. (((T mklist(y;f)) > 0)  (x:. (((T mklist(x;f)) > 0)  (y = x)))  (A f (T mklist(y;f)--1)))
6. f :   @i
7. y : @i
8. (T mklist(y;f)) > 0@i
9. y:. (((T mklist(y;f)) > 0)  (x:. (((T mklist(x;f)) > 0)  (y = x)))  (A f (T mklist(y;f)--1)))
 A f (T mklist(y;f)--1)
BY
{ RepeatFor 3 (D (-1)) }

1
1. A:      
     ((f:  . b:. (A f b))
      (T: List  
          f:  
            y:. (((T mklist(y;f)) > 0)  (x:. (((T mklist(x;f)) > 0)  (y = x)))  (A f (T mklist(y;f)--1)))))@i'
2. A :       @i'
3. f:  . b:. (A f b)@i
4. T :  List  
5. f:  . y:. (((T mklist(y;f)) > 0)  (x:. (((T mklist(x;f)) > 0)  (y = x)))  (A f (T mklist(y;f)--1)))
6. f :   @i
7. y : @i
8. (T mklist(y;f)) > 0@i
9. y1 : 
10. (T mklist(y1;f)) > 0
11. x:. (((T mklist(x;f)) > 0)  (y1 = x))
12. A f (T mklist(y1;f)--1)
 A f (T mklist(y;f)--1)



1.  \mforall{}A:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
          ((\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}b:\mBbbN{}.  (A  f  b))
          {}\mRightarrow{}  (\mexists{}T:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}
                    \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
                        \mexists{}y:\mBbbN{}
                          (((T  mklist(y;f))  >  0)
                          \mwedge{}  (\mforall{}x:\mBbbN{}.  (((T  mklist(x;f))  >  0)  {}\mRightarrow{}  (y  =  x)))
                          \mwedge{}  (A  f  (T  mklist(y;f)--1)))))@i'
2.  A  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}@i'
3.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}b:\mBbbN{}.  (A  f  b)@i
4.  T  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}
5.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
          \mexists{}y:\mBbbN{}
            (((T  mklist(y;f))  >  0)
            \mwedge{}  (\mforall{}x:\mBbbN{}.  (((T  mklist(x;f))  >  0)  {}\mRightarrow{}  (y  =  x)))
            \mwedge{}  (A  f  (T  mklist(y;f)--1)))
6.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}@i
7.  y  :  \mBbbN{}@i
8.  (T  mklist(y;f))  >  0@i
9.  \mexists{}y:\mBbbN{}
        (((T  mklist(y;f))  >  0)  \mwedge{}  (\mforall{}x:\mBbbN{}.  (((T  mklist(x;f))  >  0)  {}\mRightarrow{}  (y  =  x)))  \mwedge{}  (A  f  (T  mklist(y;f)--1)))
\mvdash{}  A  f  (T  mklist(y;f)--1)


By

RepeatFor  3  (D  (-1))



Home Index