---

Step * 1 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. spr(g)@i
5. f:  . ((f  spr(g))  (b:. (A f b)))@i
6. (g []) = 0
 T: List  
   f:  
     ((f  spr(g))  (!y:. (T mklist(y;f)) > 0  (y:. (((T mklist(y;f)) > 0)  (A f (T mklist(y;f)--1))))))
BY
{ ((FLemma `spr_choice_fun` [4] THENA Auto)
   THEN D (-1)
   THEN InstHyp [f,b. (A (n.gammaFIM(mklist(n + 1;f);g;h)[n]) b)] 1
   THEN All Reduce
   THEN Auto
   THEN Try ((RWO "gammaFIM_equi_length_mklist<" 0 THEN Auto))) }

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. spr(g)@i
5. f:  . ((f  spr(g))  (b:. (A f b)))@i
6. (g []) = 0
7. h :  List  
8. a: List. (((g a) = 0)  ((g (a @ [h a])) = 0))
9. f :   @i
 b:. (A (n.gammaFIM(mklist(n + 1;f);g;h)[n]) b)

2
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. spr(g)@i
5. f:  . ((f  spr(g))  (b:. (A f b)))@i
6. (g []) = 0
7. h :  List  
8. a: List. (((g a) = 0)  ((g (a @ [h a])) = 0))
9. T: List  
    f:  
      (!y:. (T mklist(y;f)) > 0
       (y:. (((T mklist(y;f)) > 0)  (A (n.gammaFIM(mklist(n + 1;f);g;h)[n]) (T mklist(y;f)--1)))))
 T: List  
   f:  
     ((f  spr(g))  (!y:. (T mklist(y;f)) > 0  (y:. (((T mklist(y;f)) > 0)  (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{}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.  spr(g)@i
5.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((f  \mmember{}  spr(g))  {}\mRightarrow{}  (\mexists{}b:\mBbbN{}.  (A  f  b)))@i
6.  (g  [])  =  0
\mvdash{}  \mexists{}T:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}
      \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
          ((f  \mmember{}  spr(g))
          {}\mRightarrow{}  (\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))))))


By

((FLemma  `spr\_choice\_fun`  [4]  THENA  Auto)
  THEN  D  (-1)
  THEN  InstHyp  [\mkleeneopen{}\mlambda{}f,b.  (A  (\mlambda{}n.gammaFIM(mklist(n  +  1;f);g;h)[n])  b)\mkleeneclose{}]  1\mcdot{}
  THEN  All  Reduce
  THEN  Auto
  THEN  Try  ((RWO  "gammaFIM\_equi\_length\_mklist<"  0  THEN  Auto)))\mcdot{}



Home Index