proposition: Lemma ddp_simple_criterion_local : 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}) -> forall t, Acc (ddp_step R) t -> (forall s, direct_subterm s t -> Acc (one_step R) s) -> Acc (one_step R) t.
proof: Proof. intros R HR RR CD. intros t Acc_t IH. apply ddp_criterion_local; trivial. apply Acc_incl with (ddp_step R); trivial. clear; intros s t [H _]; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)