proposition: Lemma dp_criterion_lift : forall R rule_list, (forall l r, R r l <-> In (l,r) rule_list) -> (forall l r, In (l,r) rule_list -> forall v, l <> Var v) -> (forall l r, In (l,r) rule_list -> forall v, In v (var_list r) -> In v (var_list l)) -> well_founded (ddp_step_min R) -> well_founded (one_step R).
proof: Proof. intros R rule_list Equiv R_var R_reg Wf; apply ddp_criterion; trivial. intros x t H; rewrite Equiv in H. apply (R_var (Var x) t H x); trivial. intros s t H; rewrite Equiv in H. apply (R_reg t s H). apply constructor_defined_dec with rule_list; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)