proposition: Lemma dp_subterm_criterion_gen : forall R : relation term, (forall (v : variable) (t : term), ~ R t (Var v)) -> forall (l0 : list (term * term)) (cdp cdp': term -> term -> Prop), (forall u v : term, cdp v u -> ddp R v u) -> forall (P : symbol -> nat), (forall u v, cdp v u <-> (cdp' v u \/ In (u,v) l0)) -> (forall u0 v0, In (u0,v0) l0 -> u0 <> v0) -> (forall u0 v0, In (u0,v0) l0 -> cdp v0 u0) -> (forall u0 v0, In (u0,v0) l0 -> match v0 with | Var _ => True | Term f _ => match F.arity f with | AC => P f < 2 | C => P f < 2 | Free n => P f < n end end) -> (forall u0 v0, In (u0,v0) l0 -> trans_clos (union term (one_step R) direct_subterm) (projection P v0) (projection P u0)) -> forall comp : term * term -> nat -> Prop, (forall u v : term, cdp v u -> exists n : nat, comp (u, v) n) -> (forall uv n n', comp uv n -> comp uv n' -> n = n') -> (forall uv uv' : term * term, are_connected cdp R uv uv' -> forall n n' : nat, comp uv n -> comp uv' n' -> n <= n') -> forall n0, (forall uv0, In uv0 l0 -> comp uv0 n0) -> (forall u0 v0, In (u0,v0) l0 -> 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 : term, comp (u, v) n0 -> refl_trans_clos (union term (one_step R) direct_subterm) (projection P v) (projection P u)) -> well_founded (rest (acc_sub R) (rdp_step (axiom cdp') R)) -> well_founded (rest (acc_sub R) (rdp_step (axiom cdp) R)).
proof: Proof. intros R R_var l0; induction l0 as [ | [u0 v0] l0]; intros cdp cdp' cdp_in_dpR P split_cdp l0_diff l0_in_dpR P_ok l0_decr comp comp_def comp_fonc comp_ok n0 l0_in_comp_n0 Wl0 cdp_decr W'. apply wf_incl with (rest (acc_sub R) (rdp_step (axiom cdp') R)); [ | assumption]. intros x y [H Hmin]; split; [ | assumption]. inversion H as [f l1 l2 t3 H1 H2]; clear H; subst. constructor 1 with l2. assumption. inversion H2 as [t1 t2 sigma H3 H4]; clear H2; subst. constructor 1. rewrite split_cdp in H3; destruct H3 as [H3 | H3]; [assumption | contradiction]. apply (dp_subterm_criterion R R_var _ cdp_in_dpR P u0 v0) with comp. apply l0_diff; left; apply eq_refl. rewrite split_cdp; right; left; apply eq_refl. apply P_ok with u0; left; apply eq_refl. apply l0_decr; left; apply eq_refl. assumption. assumption. apply Wl0 with u0; left; apply eq_refl. unfold strong_connect_approx; intros n u v [H1 H2]; apply cdp_decr. replace n0 with n. assumption. apply comp_fonc with (u0,v0). assumption. apply l0_in_comp_n0; left; apply eq_refl. apply wf_incl with (rest (acc_sub R) (rdp_step (axiom (fun v u => cdp' v u \/ In (u, v) l0)) R)). intros x y [H Hmin]; split; [ | assumption]. inversion H as [f l1 l2 t3 H1 H2]; clear H; subst. constructor 1 with l2. assumption. inversion H2 as [t1 t2 sigma H3 H4]; clear H2; subst. constructor 1. inversion H3 as [u v K1 K2]; clear H3; subst. rewrite split_cdp in K1; simpl in K1; destruct K1 as [K1 | [K1 | K1]]. left; assumption. apply False_rect; apply K2; apply sym_eq; assumption. right; assumption. apply IHl0 with cdp' P comp n0. intros u v [H | H]; apply cdp_in_dpR; rewrite split_cdp; [left | do 2 right]; assumption. intros u v; split; intro H; assumption. intros; apply l0_diff; right; assumption. intros; right; assumption. intros u1 v1 uv1_in_l0; apply P_ok with u1; right; assumption. intros u1 v1 uv1_in_l0; apply l0_decr; right; assumption. intros u v [H | H]; apply comp_def. rewrite split_cdp; left; assumption. rewrite split_cdp; do 2 right; assumption. assumption. intros [u v] [u' v'] H; apply comp_ok. destruct H as [sigma [sigma' [H1 [H2 H3]]]]. exists sigma; exists sigma'; split; [ | split]. rewrite split_cdp; destruct H1 as [H1 | H1]; [left | do 2 right]; assumption. rewrite split_cdp; destruct H2 as [H2 | H2]; [left | do 2 right]; assumption. assumption. intros; apply l0_in_comp_n0; right; assumption. intros u1 v1 uv1_in_l0; apply Wl0 with u1; right; assumption. apply cdp_decr. assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp)