---

Step * of Lemma bar_26_3a_imp_26_3b

(R: List  . bar_26_3a{i:l}(R))  bar_26_3b{i:l}()
BY
{ (Auto THEN RepUR ``bar_26_3b bar_26_1`` 0 THEN RepUR ``bar_26_3a`` (-1)) }

1
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)))


(\mforall{}R:\mBbbN{}  List  {}\mrightarrow{}  \mBbbP{}.  bar\_26\_3a\{i:l\}(R))  {}\mRightarrow{}  bar\_26\_3b\{i:l\}()


By

(Auto  THEN  RepUR  ``bar\_26\_3b  bar\_26\_1``  0  THEN  RepUR  ``bar\_26\_3a``  (-1))



Home Index