proposition: Lemma dp_criterion_strong_wf : 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 s t, R s t -> well_formed s /\ well_formed t) -> (forall f, {constructor R f} + {defined R f}) -> forall (inject : nat -> variable) (inject_inv : variable -> nat), (forall n : nat, inject_inv (inject n) = n) -> well_founded (ddp_step_min_wf R) -> well_founded (one_step R).
proof: Proof. intros R HR RR WR CD inject inject_inv Hinj W. intro t; apply acc_well_formed_acc_all with inject inject_inv; trivial; clear t. intro t; pattern t; apply term_rec3; clear t. intros x _; apply Acc_var; trivial. intros; apply ddp_criterion_strong_wf_local; trivial. simpl; intros t t_in_l; apply H; trivial. apply (proj1 (well_formed_unfold H0)); assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)