proposition: Lemma ddp_criterion_strong_wf_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 r l : term, R r l -> well_formed r /\ well_formed l) -> (forall f, {constructor R f} + {defined R f}) -> forall t, Acc (ddp_step_min_wf R) t -> (forall s, direct_subterm s t -> Acc (one_step R) s) -> well_formed t -> Acc (one_step R) t.
proof: Proof. intros R HR RR WR CD. intros t Acc_t Hl Wt; apply ddp_criterion_local; trivial. revert Hl Wt; induction Acc_t as [t Acc_t IH]. intros Hl Wt; apply Acc_intro. intros s [H [Hs Ht]]; assert (Ws : well_formed s). apply well_formed_rdp_step_inv with (ddp R) R t; trivial. clear Hs Ht; inversion H; clear H; subst. intros u v H; apply well_formed_dp with R; [apply WR | apply ddp_is_dp; trivial]. intros u v H'; apply reg_dp with R; [apply RR | apply ddp_is_dp; trivial]. apply IH; trivial. split; [idtac | split; split]; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)