---

Step * 1 1 1 1 of Lemma bar_bwd_implies_fwd


1. R :  List  @i'
2. A: List  . bar_bwd_fim(R;A)@i'
3. a :  List@i
4. R a@i
5. c :   @i
 x:. (R (a @ mklist(x;c)))
BY
{ (((InstConcl [0] THEN Auto) THEN RepUR ``mklist`` 0)
   THEN (Assert R a BY
               Auto)
   THEN Auto
   THEN RWO "append-nil" 0
   THEN Auto) }



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


By

(((InstConcl  [\mkleeneopen{}0\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  RepUR  ``mklist``  0)
  THEN  (Assert  R  a  BY
                          Auto)
  THEN  Auto
  THEN  RWO  "append-nil"  0
  THEN  Auto)\mcdot{}



Home Index