proposition: Lemma cdp_criterion : forall R, (forall x t, ~ (R t (Var x))) -> (forall s t, R s t -> forall x, In x (var_list s) -> In x (var_list t)) -> (forall f, {constructor R f} + {defined R f}) -> well_founded (cdp_step R) -> well_founded (C_step R).
proof: Proof. intros R HR RR CD Wf t; pattern t; apply term_rec3; clear t. intro x; apply Context_Acc_var; trivial. intros; apply cdp_criterion_local; trivial. simpl; intros s As; apply H. destruct As as [n [_ As]]. revert n As; clear; induction l as [ | t l]; intros [ | n] H. discriminate. discriminate. injection H; intros; left; assumption. right; apply IHl with n; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)