---

Step * 1 1 2 1 of Lemma brouwer_prin_fun_imp_num


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
4. T :  List  
5. f:  
     ((t:. !y:. (T [t / mklist(y;f)]) > 0)
      (B:  . ((t:. y:. ((T [t / mklist(y;f)]) = ((B t) + 1)))  (A f (B 0)))))
6. f :   @i
 !y:. ((T [0 / mklist(y;f)]) > 0)  (A f (T [0 / mklist(y;f)]--1))
BY
{ (InstHyp [f] (-2) THEN Auto) }

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
4. T :  List  
5. f:  
     ((t:. !y:. (T [t / mklist(y;f)]) > 0)
      (B:  . ((t:. y:. ((T [t / mklist(y;f)]) = ((B t) + 1)))  (A f (B 0)))))
6. f :   @i
7. t:. !y:. (T [t / mklist(y;f)]) > 0
8. B:  . ((t:. y:. ((T [t / mklist(y;f)]) = ((B t) + 1)))  (A f (B 0)))
 !y:. ((T [0 / mklist(y;f)]) > 0)  (A f (T [0 / mklist(y;f)]--1))



1.  \mforall{}A:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
          ((\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}B:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  (A  f  B))
          {}\mRightarrow{}  (\mexists{}T:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}
                    \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
                        ((\mforall{}t:\mBbbN{}.  \mexists{}!y:\mBbbN{}.  (T  [t  /  mklist(y;f)])  >  0)
                        \mwedge{}  (\mforall{}B:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((\mforall{}t:\mBbbN{}.  \mexists{}y:\mBbbN{}.  ((T  [t  /  mklist(y;f)])  =  ((B  t)  +  1)))  {}\mRightarrow{}  (A  f  B))))))@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{}
          ((\mforall{}t:\mBbbN{}.  \mexists{}!y:\mBbbN{}.  (T  [t  /  mklist(y;f)])  >  0)
          \mwedge{}  (\mforall{}B:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((\mforall{}t:\mBbbN{}.  \mexists{}y:\mBbbN{}.  ((T  [t  /  mklist(y;f)])  =  ((B  t)  +  1)))  {}\mRightarrow{}  (A  f  (B  0)))))
6.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}@i
\mvdash{}  \mexists{}!y:\mBbbN{}.  ((T  [0  /  mklist(y;f)])  >  0)  \mwedge{}  (A  f  (T  [0  /  mklist(y;f)]--1))


By

(InstHyp  [\mkleeneopen{}f\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto)



Home Index