proposition: Lemma psi_two_cases : forall t, (nf (one_step R) t /\ psi t = t) \/ (~nf (one_step R) t /\ psi t <> t).
proof: Proof. intro t; pattern t; apply term_rec3; clear t. intros v; left; split. apply nf_var. rewrite psi_nf; trivial; apply nf_var. intros f l IH. assert (red_dec :=compute_red_is_correct rule_list Rreg' R Req). assert (nf_dec := dec_nf _ _ red_dec). destruct (nf_dec (Term f l)) as [nf_fl | not_nf_fl]. left; split; trivial; rewrite psi_nf; trivial. right; split; trivial. intro H; destruct (psi_char (Term f l)) as [[H1 H2] | P]. apply not_nf_fl; trivial. apply (Psi_not_refl (Term f l)); rewrite H in P; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure more_list weaved_relation term equational_theory_spec rwr_strategies dp rpo)