---

Step * 1 of Lemma bar26_4a_imp_fan26_6a


1. bar_26_4a{i:l}()@i'
2. B :  List  @i
3. R :  List  @i'
4. a: List. Dec(R a)@i
5. f:fin_spr(B). x:. (R mklist(x;f))@i
 z:. f:fin_spr(B). x:. ((x  z)  (R mklist(x;f)))
BY
{ Unfold `bar_26_4a` 1 }

1
1. g: List  . R,A: List  .
     (spr(g)
      ((g []) = 0)
      (a: List. (((g a) = 0)  Dec(R a)))
      (f:  . ((x:. ((g mklist(x;f)) = 0))  (x:. (R mklist(x;f)))))
      (a: List. (((g a) = 0)  (R a)  (A a)))
      (a: List. (((g a) = 0)  (s:. (((g (a @ [s])) = 0)  (A (a @ [s]))))  (A a)))
      (A []))@i'
2. B :  List  @i
3. R :  List  @i'
4. a: List. Dec(R a)@i
5. f:fin_spr(B). x:. (R mklist(x;f))@i
 z:. f:fin_spr(B). x:. ((x  z)  (R mklist(x;f)))



1.  bar\_26\_4a\{i:l\}()@i'
2.  B  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
3.  R  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbP{}@i'
4.  \mforall{}a:\mBbbN{}  List.  Dec(R  a)@i
5.  \mforall{}f:fin\_spr(B).  \mexists{}x:\mBbbN{}.  (R  mklist(x;f))@i
\mvdash{}  \mexists{}z:\mBbbN{}.  \mforall{}f:fin\_spr(B).  \mexists{}x:\mBbbN{}.  ((x  \mleq{}  z)  \mwedge{}  (R  mklist(x;f)))


By

Unfold  `bar\_26\_4a`  1



Home Index