---

Step * 1 2 1 of Lemma brouwer_prin_27_2_imp_27_5


1. A:      
     ((f:  . b:. (A f b))
      (T: List  
          f:  . (!y:. (T mklist(y;f)) > 0  (y:. (((T mklist(y;f)) > 0)  (A f (T mklist(y;f)--1)))))))@i'
2. A :       @i'
3. g :  List  @i
4. g []  0
5. spr(g)@i
6. f:  . ((f  spr(g))  (b:. (A f b)))@i
7. f :   @i
8. (f  spr(g))@i
 !y:. 0 > 0
BY
{ (InstLemma `empty_spr` [g] THEN MaAuto) }

1
1. A:      
     ((f:  . b:. (A f b))
      (T: List  
          f:  . (!y:. (T mklist(y;f)) > 0  (y:. (((T mklist(y;f)) > 0)  (A f (T mklist(y;f)--1)))))))@i'
2. A :       @i'
3. g :  List  @i
4. g []  0
5. spr(g)@i
6. f:  . ((f  spr(g))  (b:. (A f b)))@i
7. f :   @i
8. (f  spr(g))@i
9. a: List. ((g a) > 0)
 !y:. 0 > 0



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{}y:\mBbbN{}.  (((T  mklist(y;f))  >  0)  {}\mRightarrow{}  (A  f  (T  mklist(y;f)--1)))))))@i'
2.  A  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}@i'
3.  g  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
4.  g  []  \mneq{}  0
5.  spr(g)@i
6.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((f  \mmember{}  spr(g))  {}\mRightarrow{}  (\mexists{}b:\mBbbN{}.  (A  f  b)))@i
7.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}@i
8.  (f  \mmember{}  spr(g))@i
\mvdash{}  \mexists{}!y:\mBbbN{}.  0  >  0


By

(InstLemma  `empty\_spr`  [\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THEN  MaAuto)



Home Index