proposition: Lemma dp0_decreases : forall t1 t2, Rdp0 t2 t1 -> trans_clos (union _ (one_step R) direct_subterm) (projection t2) (projection t1).
proof: Proof. intros t1 t2 H21. inversion H21 as [f l1 l2 v1 Hl21 Hdp2]; subst. inversion Hdp2 as [v2 u2 sigma2 Hdp2' K2 J2]; clear Hdp2. inversion Hdp2'; subst v2 u2. assert (dp_uv0 := cdp_in_dpR _ _ cdp_uv0). destruct dp_uv0 as [dp_uv0 H2]. inversion dp_uv0 as [u0' r0 p0 g0 k0 H1 H3]; clear Hdp2' H21; subst. destruct u0 as [x0 | f0 l0]. apply False_rect; apply (R_var _ _ H1). assert (Sub := projection_one_step_list f _ _ Hl21). assert (Sub' : trans_clos (union term (one_step R) direct_subterm) (projection (apply_subst sigma2 (Term g0 k0))) (projection (Term f l2))). rewrite <- J2. do 2 rewrite subst_projection. revert uv0_strict; apply trans_incl2. intros a1 a2 [Sub'' | Sub'']. left; apply one_step_apply_subst; assumption. right; destruct a2 as [x2 | g2 k2]. contradiction. simpl; rewrite in_map_iff; exists a1; split; trivial. inversion Sub as [u H0 H5 | u1 u2 K1 K2]. subst u; simpl; rewrite <- H5; assumption. subst u1 u2; apply trans_clos_is_trans with (projection (Term f l2)); trivial. apply trans_incl with (one_step R); trivial. intros u1 u2 K; left; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp) CoLoR(NatCompat)