---

Step * 1 of Lemma bar_bwd_implies_fwd


1. R :  List  @i'
2. A: List  . bar_bwd_fim(R;A)@i'
 bar_fwd_fim(R)
BY
{ (InstHyp [a.c:  . x:. (R (a @ mklist(x;c)))] (-1) THEN Auto) }

1
1. R :  List  @i'
2. A: List  . bar_bwd_fim(R;A)@i'
3. bar_bwd_fim(R;a.c:  . x:. (R (a @ mklist(x;c))))
 bar_fwd_fim(R)



1.  R  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbP{}@i'
2.  \mforall{}A:\mBbbN{}  List  {}\mrightarrow{}  \mBbbP{}.  bar\_bwd\_fim(R;A)@i'
\mvdash{}  bar\_fwd\_fim(R)


By

(InstHyp  [\mkleeneopen{}\mlambda{}a.\mforall{}c:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}x:\mBbbN{}.  (R  (a  @  mklist(x;c)))\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)



Home Index