proposition: Lemma mdp_reverted_criterion_local_strong : (forall f, mark (mark f) = f) -> forall (dpR : relation term), (forall u v, dpR v u -> dp R v u) -> forall s, Acc (rest (acc_sub R) (rdp_step (axiom dpR) R)) s -> Acc (rest (acc_sub R) (rdp_step (axiom (mrel dpR)) R)) (mark_term s).
proof: Proof. intros mark_inv dpR dpR_in_dpR t Acc_t. induction Acc_t as [t' Acc_t IH]. apply Acc_intro; intros s H'. rewrite (TT mark_inv); apply IH. destruct H' as [H' Hmin]; split. apply (mrdp_step_rdp_step mark_inv _ dpR_in_dpR); rewrite <- (TT mark_inv s); 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)