proposition: Lemma acc_one_step_acc_dp : forall R, (forall x t, ~ (R t (Var x))) -> forall t, Acc (one_step R) t -> Acc (dp_step R) t.
proof: Proof. intros R HR. assert (H : forall s t, axiom (dp R) s t -> trans_clos (@union term (one_step R) direct_subterm) s t). intros s t H'. inversion H' as [s' t' sigma H]; clear H'; subst. inversion H as [t1 t2 p f l H'' H3 Df]; clear H; subst. assert (H4 := subterm_at_pos_apply_subst_apply_subst_subterm_at_pos t2 p sigma); rewrite H3 in H4. destruct (subterm_subterm _ _ H4) as [H1 | H2]. apply t_step; left; apply at_top; rewrite <- H1; apply instance; trivial. apply trans_clos_is_trans with (apply_subst sigma t2). apply trans_incl with direct_subterm; trivial. intros s t H; right; trivial. apply t_step; left; apply at_top; apply instance; trivial. intros t Acc_t; apply Acc_incl with (trans_clos (@union term (one_step R) direct_subterm)). clear t Acc_t; intros s t H'; inversion H' as [f' l1 l2 H1 H2 H3]; clear H'; subst. inversion H2 as [l | k1 k2 K2]; clear H2; subst. apply H; assumption. apply trans_clos_is_trans with (Term f' l2). apply H; trivial. apply trans_incl with (one_step R). intros s' t' H'; left; trivial. apply general_context; trivial. apply acc_trans; trivial. rewrite <- acc_with_subterm; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)