---

Step * of Lemma brouwer_prin_27_2_imp_27_5

brouwer_prin_for_num_27_2{i:l}()  brouwer_prin_27_5{i:l}()
BY
{ ((Unfold `brouwer_prin_27_5` 0 THEN Auto) THEN Unfold `brouwer_prin_for_num_27_2` 1 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
 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))))))


brouwer\_prin\_for\_num\_27\_2\{i:l\}()  {}\mRightarrow{}  brouwer\_prin\_27\_5\{i:l\}()


By

((Unfold  `brouwer\_prin\_27\_5`  0  THEN  Auto)  THEN  Unfold  `brouwer\_prin\_for\_num\_27\_2`  1  THEN  Auto)



Home Index