proposition: Lemma acc_R_acc_dp_sub : forall t, Acc (one_step R) t -> Acc (union _ Rcdp (trans_clos direct_subterm)) t.
proof: Proof. intros t Acc_t; apply Acc_incl with (trans_clos (union _ (one_step R) direct_subterm)). clear t Acc_t; intros s t [H1 | H2]. inversion H1; clear H1; subst. inversion H0; clear H0; subst. assert (H4 := cdp_in_dpR _ _ H3); clear H3. destruct H4 as [H4 Sub]. inversion H4; clear H4; subst. destruct (subterm_subterm _ _ H2) as [H4 | H4]; subst; inversion H; clear H; subst. do 3 left; rewrite <- H1; apply instance; assumption. apply trans_clos_is_trans with (Term f l2). apply trans_incl with (one_step R). do 3 intro; left; assumption. do 2 left; rewrite <- H1; apply instance; assumption. apply trans_incl with (one_step R). do 3 intro; left; assumption. apply general_context; assumption. apply trans_clos_is_trans with (apply_subst sigma t3). apply trans_incl with direct_subterm. do 3 intro; right; assumption. apply instantiated_subterm; assumption. do 3 left; rewrite <- H1; apply instance; assumption. apply trans_clos_is_trans with (apply_subst sigma t3). apply trans_incl with direct_subterm. do 3 intro; right; assumption. apply instantiated_subterm; assumption. apply trans_clos_is_trans with (Term f l2). do 3 left; rewrite <- H1; apply instance; assumption. apply trans_incl with (one_step R). do 3 intro; left; assumption. apply general_context; assumption. apply trans_incl with direct_subterm; trivial. do 3 intro; right; assumption. apply acc_trans; rewrite <- acc_with_subterm; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp) CoLoR(NatCompat)