---

Step * of Lemma bar_bwd_fim_wf

R,A: List  .  (bar_bwd_fim(R;A)  )
BY
{ (Unfold `bar_bwd_fim` 0 THEN Auto) }


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


By

(Unfold  `bar\_bwd\_fim`  0  THEN  Auto)



Home Index