---

Step * 1 1 1 of Lemma bar26_4a_imp_fan26_6a


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
 spr(a.if (a  fspr(B)) then 0 else 1 fi )
BY
{ (BLemma `fin_spr_is_spr` THEN Auto) }



1.  \mforall{}g:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}.  \mforall{}R,A:\mBbbN{}  List  {}\mrightarrow{}  \mBbbP{}.
          (spr(g)
          {}\mRightarrow{}  ((g  [])  =  0)
          {}\mRightarrow{}  (\mforall{}a:\mBbbN{}  List.  (((g  a)  =  0)  {}\mRightarrow{}  Dec(R  a)))
          {}\mRightarrow{}  (\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((\mforall{}x:\mBbbN{}.  ((g  mklist(x;f))  =  0))  {}\mRightarrow{}  (\mexists{}x:\mBbbN{}.  (R  mklist(x;f)))))
          {}\mRightarrow{}  (\mforall{}a:\mBbbN{}  List.  (((g  a)  =  0)  {}\mRightarrow{}  (R  a)  {}\mRightarrow{}  (A  a)))
          {}\mRightarrow{}  (\mforall{}a:\mBbbN{}  List.  (((g  a)  =  0)  {}\mRightarrow{}  (\mforall{}s:\mBbbN{}.  (((g  (a  @  [s]))  =  0)  {}\mRightarrow{}  (A  (a  @  [s]))))  {}\mRightarrow{}  (A  a)))
          {}\mRightarrow{}  (A  []))@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{}  spr(\mlambda{}a.if  (a  \mmember{}  fspr(B))  then  0  else  1  fi  )


By

(BLemma  `fin\_spr\_is\_spr`  THEN  Auto)



Home Index