---

Step * 1 of Lemma fan_26_6a_prin27_5_imp_fan27_7a


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))))
BY
{ (InstLemma `fin_spr_is_spr` [B] THENA 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
6. spr(a.if (a  fspr(B)) then 0 else 1 fi )
 z:. f:  . ((f  fspr(B))  (b:. G:  . ((G  fspr(B))  equal_upto(z;f;G)  (A G b))))



1.  \mforall{}B:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}.  \mforall{}R:\mBbbN{}  List  {}\mrightarrow{}  \mBbbP{}.
          ((\mforall{}a:\mBbbN{}  List.  Dec(R  a))
          {}\mRightarrow{}  (\mforall{}f:fin\_spr(B).  \mexists{}x:\mBbbN{}.  (R  mklist(x;f)))
          {}\mRightarrow{}  (\mexists{}z:\mBbbN{}.  \mforall{}f:fin\_spr(B).  \mexists{}x:\mBbbN{}.  ((x  \mleq{}  z)  \mwedge{}  (R  mklist(x;f)))))@i'
2.  \mforall{}A:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}.  \mforall{}g:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}.
          (spr(g)
          {}\mRightarrow{}  (\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((f  \mmember{}  spr(g))  {}\mRightarrow{}  (\mexists{}b:\mBbbN{}.  (A  f  b))))
          {}\mRightarrow{}  (\mexists{}T:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}
                    \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
                        ((f  \mmember{}  spr(g))
                        {}\mRightarrow{}  (\mexists{}!y:\mBbbN{}.  (T  mklist(y;f))  >  0
                              \mwedge{}  (\mforall{}y:\mBbbN{}.  (((T  mklist(y;f))  >  0)  {}\mRightarrow{}  (A  f  (T  mklist(y;f)--1))))))))@i'
3.  A  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}@i'
4.  B  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
5.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((f  \mmember{}  fspr(B))  {}\mRightarrow{}  (\mexists{}b:\mBbbN{}.  (A  f  b)))@i
\mvdash{}  \mexists{}z:\mBbbN{}
      \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((f  \mmember{}  fspr(B))  {}\mRightarrow{}  (\mexists{}b:\mBbbN{}.  \mforall{}G:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((G  \mmember{}  fspr(B))  {}\mRightarrow{}  equal\_upto(z;f;G)  {}\mRightarrow{}  (A  G  b))))


By

(InstLemma  `fin\_spr\_is\_spr`  [\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto)



Home Index