---

Step * 1 1 of Lemma fan_26_6a_imp_fan_26_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. g :  List  @i
3. R :  List  @i'
4. gen_fin_spr(g)@i
5. a: List. (((g a) = 0)  Dec(R a))@i
6. f:  . ((x:. ((g mklist(x;f)) = 0))  (x:. (R mklist(x;f))))@i
 z:. f:  . ((x:. ((g mklist(x;f)) = 0))  (x:. ((R mklist(x;f))  (x  z))))
BY
{ ((Assert Dec((g []) = 0) BY Auto) THEN D (-1) 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. g :  List  @i
3. R :  List  @i'
4. gen_fin_spr(g)@i
5. a: List. (((g a) = 0)  Dec(R a))@i
6. f:  . ((x:. ((g mklist(x;f)) = 0))  (x:. (R mklist(x;f))))@i
7. (g []) = 0
 z:. f:  . ((x:. ((g mklist(x;f)) = 0))  (x:. ((R mklist(x;f))  (x  z))))

2
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. g :  List  @i
3. R :  List  @i'
4. gen_fin_spr(g)@i
5. a: List. (((g a) = 0)  Dec(R a))@i
6. f:  . ((x:. ((g mklist(x;f)) = 0))  (x:. (R mklist(x;f))))@i
7. ((g []) = 0)
 z:. f:  . ((x:. ((g mklist(x;f)) = 0))  (x:. ((R mklist(x;f))  (x  z))))



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.  g  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
3.  R  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbP{}@i'
4.  gen\_fin\_spr(g)@i
5.  \mforall{}a:\mBbbN{}  List.  (((g  a)  =  0)  {}\mRightarrow{}  Dec(R  a))@i
6.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((\mforall{}x:\mBbbN{}.  ((g  mklist(x;f))  =  0))  {}\mRightarrow{}  (\mexists{}x:\mBbbN{}.  (R  mklist(x;f))))@i
\mvdash{}  \mexists{}z:\mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  ((\mforall{}x:\mBbbN{}.  ((g  mklist(x;f))  =  0))  {}\mRightarrow{}  (\mexists{}x:\mBbbN{}.  ((R  mklist(x;f))  \mwedge{}  (x  \mleq{}  z))))


By

((Assert  Dec((g  [])  =  0)  BY  Auto)  THEN  D  (-1)  THEN  Auto)



Home Index