---

Step * of Lemma bar_bwd_implies_fwd

R: List  . ((A: List  . bar_bwd_fim(R;A))  bar_fwd_fim(R))
BY
{ Auto }

1
1. R :  List  @i'
2. A: List  . bar_bwd_fim(R;A)@i'
 bar_fwd_fim(R)


\mforall{}R:\mBbbN{}  List  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}A:\mBbbN{}  List  {}\mrightarrow{}  \mBbbP{}.  bar\_bwd\_fim(R;A))  {}\mRightarrow{}  bar\_fwd\_fim(R))


By

Auto



Home Index