---

Step * of Lemma fan_26_6a_prin27_5_imp_fan27_7a

fan_26_6a{i:l}()  brouwer_prin_27_5{i:l}()  fan_27_7a{i:l}()
BY
{ ((Auto THEN Unfold `fan_27_7a` 0) THEN Unfold `fan_26_6a` 1 THEN Unfold `brouwer_prin_27_5` 2 THEN Auto) }

1
1. B: List  . R: List  .
     ((a: List. Dec(R a))
      (f:fin_spr(B). x:. (R mklist(x;f)))
      (z:. f:fin_spr(B). x:. ((x  z)  (R mklist(x;f)))))@i'
2. A:      . g: List  .
     (spr(g)
      (f:  . ((f  spr(g))  (b:. (A f b))))
      (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))))))))@i'
3. A :       @i'
4. B :  List  @i
5. f:  . ((f  fspr(B))  (b:. (A f b)))@i
 z:. f:  . ((f  fspr(B))  (b:. G:  . ((G  fspr(B))  equal_upto(z;f;G)  (A G b))))


fan\_26\_6a\{i:l\}()  {}\mRightarrow{}  brouwer\_prin\_27\_5\{i:l\}()  {}\mRightarrow{}  fan\_27\_7a\{i:l\}()


By

((Auto  THEN  Unfold  `fan\_27\_7a`  0)
  THEN  Unfold  `fan\_26\_6a`  1
  THEN  Unfold  `brouwer\_prin\_27\_5`  2
  THEN  Auto)



Home Index