---

Step * 1 of Lemma brouwer_prin_fun_imp_num


1. brouwer_prin_for_fun_27_1ax{i:l}()@i'
2. A :       @i'
3. f:  . b:. (A f b)@i
 T: List  . f:  . !y:. ((T mklist(y;f)) > 0)  (A f (T mklist(y;f)--1))
BY
{ Unfold `brouwer_prin_for_fun_27_1ax` 1 }

1
1. A:        
     ((f:  . B:  . (A f B))
      (T: List  
          f:  
            ((t:. !y:. (T [t / mklist(y;f)]) > 0)
             (B:  . ((t:. y:. ((T [t / mklist(y;f)]) = ((B t) + 1)))  (A f B))))))@i'
2. A :       @i'
3. f:  . b:. (A f b)@i
 T: List  . f:  . !y:. ((T mklist(y;f)) > 0)  (A f (T mklist(y;f)--1))



1.  brouwer\_prin\_for\_fun\_27\_1ax\{i:l\}()@i'
2.  A  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}@i'
3.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}b:\mBbbN{}.  (A  f  b)@i
\mvdash{}  \mexists{}T:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}!y:\mBbbN{}.  ((T  mklist(y;f))  >  0)  \mwedge{}  (A  f  (T  mklist(y;f)--1))


By

Unfold  `brouwer\_prin\_for\_fun\_27\_1ax`  1



Home Index