proposition: Lemma mdp_criterion_local_strong : forall (dpR : relation term), (forall u v, dpR v u -> dp R v u) -> forall s, Acc (rest (acc_sub R) (rdp_step (axiom (mrel dpR)) R)) (mark_term s) -> Acc (rest (acc_sub R) (rdp_step (axiom dpR) R)) s.
proof: Proof. intros dpR dpR_in_dpR t Acc_t. set (t' := mark_term t) in *; assert (Tt := eq_refl t'); unfold t' at 2 in Tt; clearbody t'. revert t Tt; induction Acc_t as [t' Acc_t IH]. intros t H. apply Acc_intro; intros s H'. apply IH with (mark_term s); [ | apply eq_refl]. subst t'; destruct H' as [H' Hmin]; split. apply rdp_step_rmdp_step; trivial. destruct s; destruct t; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)