proposition: Lemma dp_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 (dp_step R) -> well_founded (one_step R).
proof: Proof. intros R HR RR CD Wf t; pattern t; apply term_rec3; clear t. intro x; apply Acc_var; trivial. intros; apply dp_criterion_local; trivial. Defined.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)