---

Step * of Lemma brouwer_prin_for_num27_2_equiv

brouwer_prin_for_num_27_2{i:l}()  brouwer_prin_for_num_27_2_orig{i:l}()
BY
{ (RepUR ``brouwer_prin_for_num_27_2_orig brouwer_prin_for_num_27_2`` 0
   THEN Auto
   THEN InstHyp [A] 1
   THEN Auto
   THEN D (-1)
   THEN InstConcl [T] 
   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. f:  . b:. (A f b)@i
4. T :  List  
5. f:  . (!y:. (T mklist(y;f)) > 0  (y:. (((T mklist(y;f)) > 0)  (A f (T mklist(y;f)--1)))))
6. f :   @i
 y:. (((T mklist(y;f)) > 0)  (x:. (((T mklist(x;f)) > 0)  (y = x)))  (A f (T mklist(y;f)--1)))

2
1. A:      
     ((f:  . b:. (A f b))
      (T: List  
          f:  
            y:. (((T mklist(y;f)) > 0)  (x:. (((T mklist(x;f)) > 0)  (y = x)))  (A f (T mklist(y;f)--1)))))@i'
2. A :       @i'
3. f:  . b:. (A f b)@i
4. T :  List  
5. f:  . y:. (((T mklist(y;f)) > 0)  (x:. (((T mklist(x;f)) > 0)  (y = x)))  (A f (T mklist(y;f)--1)))
6. f :   @i
 !y:. (T mklist(y;f)) > 0

3
1. A:      
     ((f:  . b:. (A f b))
      (T: List  
          f:  
            y:. (((T mklist(y;f)) > 0)  (x:. (((T mklist(x;f)) > 0)  (y = x)))  (A f (T mklist(y;f)--1)))))@i'
2. A :       @i'
3. f:  . b:. (A f b)@i
4. T :  List  
5. f:  . y:. (((T mklist(y;f)) > 0)  (x:. (((T mklist(x;f)) > 0)  (y = x)))  (A f (T mklist(y;f)--1)))
6. f :   @i
7. y : @i
8. (T mklist(y;f)) > 0@i
 A f (T mklist(y;f)--1)


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


By

(RepUR  ``brouwer\_prin\_for\_num\_27\_2\_orig  brouwer\_prin\_for\_num\_27\_2``  0\mcdot{}
  THEN  Auto
  THEN  InstHyp  [\mkleeneopen{}A\mkleeneclose{}]  1\mcdot{}
  THEN  Auto
  THEN  D  (-1)
  THEN  InstConcl  [\mkleeneopen{}T\mkleeneclose{}]  \mcdot{}
  THEN  Auto)



Home Index