---

Step * 1 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'
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)
BY
{ (InstHyp [l.((c l) = 0)] 1 THEN All Reduce THEN Auto) }



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'
2.  c  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
3.  bar\_fwd\_fim(\mlambda{}l.((c  l)  =  0))@i
4.  A  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbP{}@i'
\mvdash{}  bar\_bwd\_fim(\mlambda{}l.((c  l)  =  0);A)


By

(InstHyp  [\mkleeneopen{}\mlambda{}l.((c  l)  =  0)\mkleeneclose{}]  1\mcdot{}  THEN  All  Reduce  THEN  Auto)



Home Index