proposition: Lemma dp_subterm_criterion: (match v0 with | Var _ => True | Term f l => match F.arity f with | AC => length l = 2 | C => length l = 2 | Free n => length l = n end end) -> (forall u v, cdp v u -> connect_approx (u0,v0) (u,v) -> connect_approx (u,v) (u0,v0) -> refl_trans_clos (union _ (one_step R) direct_subterm) (projection v) (projection u)) -> well_founded Rdp_min' -> well_founded Rcdp_min.
proof: Proof. intros L Hdp W' t; apply (well_founded_ind W'); clear t. intros t IH; apply Acc_intro; intros s [H [Ms Mt]]. rewrite split_dps in H; destruct H as [H | H]. apply IH. split; [ | split ]; assumption. apply Acc_incl with (union _ Rdp_min' Rdp0_min). do 2 intro; intros [K [MW1 MW2]]; rewrite split_dps in K; destruct K as [K | K]; [left | right]; split; trivial. split; assumption. split; assumption. apply acc_union_weak. apply acc_inv_im2 with term (trans_clos (union term (one_step R) direct_subterm)) projection. intros a1 a2 a3 H32 H21 H10. assert (B := between_dp0 Hdp). assert (H0 : exists a0, Rdp0 a1 a0). inversion H10 as [a | a1' b1 K10]; clear H10; subst. exists t; assumption. inversion K10 as [a1' b1' H10 | a1' b1 c1' J10 K0]; clear K10. subst a1' b1'. inversion H10 as [a1' b1 c1' K1 K10]; clear H10. subst a1' c1'. exists b1; destruct K1; assumption. subst a1' c1'. inversion J10 as [a1' b1' c1 J1 J0]; clear J10. subst a1' c1. exists b1'; destruct J1; assumption. destruct H0 as [a0 H0]. inversion H21 as [a2' b2 c2' K2 K1]; clear H21. subst a2' c2'. assert (K1' : refl_trans_clos Rdp' b2 a1). apply refl_trans_incl with Rdp_min'; trivial. do 2 intro; intros [K _]; assumption. assert (K2' := proj1 K2). assert (B' := B _ _ _ _ H0 K1' K2'). inversion B' as [p J1 J2 | pb2 pa1 B'']. apply dp0_decreases; assumption. subst pb2 pa1. apply trans_clos_is_trans with (projection b2); trivial. apply dp0_decreases; assumption. apply acc_trans; rewrite <- acc_with_subterm. destruct s as [v | f l]. simpl; apply Acc_var; trivial. apply Ms; apply (projection_is_subterm t). assumption. inversion H as [g l1 l2 t3 H1 H2]; clear H; subst. inversion H2 as [t1 t2 sigma]; clear H2; subst. inversion H; clear H; subst t1 t2. assert (H4 := cdp_in_dpR _ _ cdp_uv0). destruct H4 as [H4 _]. inversion H4; clear IH W'; subst. injection H0; intros; subst f2 l; rewrite length_map. assumption. intros b _; apply W'. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp) CoLoR(NatCompat)