---

Step * 1 of Lemma bar_26_3a_imp_26_3b


1. R: List  . ((a: List. Dec(R a))  bar_fwd_fim(R)  (A: List  . bar_bwd_fim(R;A)))@i'
 c: List  . (bar_fwd_fim(l.((c l) = 0))  (A: List  . bar_bwd_fim(l.((c l) = 0);A)))
BY
{ Auto }

1
1. R: List  . ((a: List. Dec(R a))  bar_fwd_fim(R)  (A: List  . bar_bwd_fim(R;A)))@i'
2. c :  List  @i
3. bar_fwd_fim(l.((c l) = 0))@i
4. A :  List  @i'
 bar_bwd_fim(l.((c l) = 0);A)



1.  \mforall{}R:\mBbbN{}  List  {}\mrightarrow{}  \mBbbP{}
          ((\mforall{}a:\mBbbN{}  List.  Dec(R  a))  {}\mRightarrow{}  bar\_fwd\_fim(R)  {}\mRightarrow{}  (\mforall{}A:\mBbbN{}  List  {}\mrightarrow{}  \mBbbP{}.  bar\_bwd\_fim(R;A)))@i'
\mvdash{}  \mforall{}c:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}.  (bar\_fwd\_fim(\mlambda{}l.((c  l)  =  0))  {}\mRightarrow{}  (\mforall{}A:\mBbbN{}  List  {}\mrightarrow{}  \mBbbP{}.  bar\_bwd\_fim(\mlambda{}l.((c  l)  =  0);A)))


By

Auto



Home Index