---

Step * 1 1 1 2 2 of Lemma bar_bwd_implies_fwd


1. R :  List  @i'
2. A: List  . bar_bwd_fim(R;A)@i'
3. f :   @i
4. c:  . x:. (R mklist(x;c))
 x:. (R mklist(x;f))
BY
{ (MoveToConcl (-2) THEN Trivial) }



1.  R  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbP{}@i'
2.  \mforall{}A:\mBbbN{}  List  {}\mrightarrow{}  \mBbbP{}.  bar\_bwd\_fim(R;A)@i'
3.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}@i
4.  \mforall{}c:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}x:\mBbbN{}.  (R  mklist(x;c))
\mvdash{}  \mexists{}x:\mBbbN{}.  (R  mklist(x;f))


By

(MoveToConcl  (-2)  THEN  Trivial)



Home Index