proposition: Lemma split_rel : forall dpR R (comp : (term * term) -> nat -> Prop) (comp_approx : forall uv uv', are_connected dpR R uv uv' -> forall n n', comp uv n -> comp uv' n' -> n <= n') (comp_def_on_dps : forall u v, (exists n, comp (u,v) n) <-> dpR v u) (split_graph : exists n0, forall uv n, comp uv n -> n <= n0), forall P, well_founded (rest P (rdp_step (axiom dpR) R)) <-> (forall n, well_founded (rest P (rdp_step (axiom (fun v u => comp (u,v) n)) R))).
proof: Proof. intros dpR R comp comp_approx comp_def_on_dps split_graph P. split; intro W. intros n; revert W; apply wf_incl; intros s t [K [As At]]. inversion K as [f l1 l2 s' H1 H2]; subst. inversion H2 as [t1 t2 sigma H3 H4 H5]; subst. split; [ | split; assumption]. constructor 1 with l2; trivial. rewrite <- H5; constructor. rewrite <- comp_def_on_dps; exists n; assumption. destruct split_graph as [n G]. revert comp comp_approx comp_def_on_dps G W. induction n as [ | n]; intros comp comp_approx comp_def_on_dps G W. apply wf_incl with (rest P (rdp_step (axiom (fun v u : term => comp (u, v) 0)) R)). intros s t [K [As At]]; split; [ | split; assumption]. inversion K as [f l1 l2 s' H1 H2]; subst. inversion H2 as [t1 t2 sigma H3 H4 H5]; subst. constructor 1 with l2. assumption. rewrite <- H5; apply instance. rewrite <- comp_def_on_dps in H3. destruct H3 as [n H3]. assert (H6 := G _ _ H3); inversion H6; subst n; assumption. apply (W 0). set (comp' := fun uv m => match m with 0 => comp uv 0 \/ comp uv 1 | S n => comp uv (S m) end). apply (IHn comp'); clear IHn. intros uv uv' H; assert (K := comp_approx _ _ H); unfold comp'. intros [ | c] [ | c']. intros _ _; apply le_n. intros _ _; apply Nat.le_0_l. intros J [J' | J']. assert (J'' := K _ _ J J'); inversion J''. apply (le_S_n _ _ (K _ _ J J')). intros J J'; apply (le_S_n _ _ (K _ _ J J')). intros u v; rewrite <- (comp_def_on_dps u v). unfold comp'; split. intros [[ | n0] H]. destruct H as [H | H]; [exists 0 | exists 1]; assumption. exists (S (S n0)); assumption. intros [[ | [ | n0]] H]. exists 0; left; assumption. exists 0; right; assumption. exists (S n0); assumption. unfold comp'; intros [u v] [ | n0]. intros _; apply Nat.le_0_l. intro K; apply le_S_n; apply (G _ _ K). intros [ | n0]. apply wf_incl with (union _ (rest P (rdp_step (axiom (fun v u : term => comp (u, v) 1)) R)) (rest P (rdp_step (axiom (fun v u : term => comp (u, v) 0)) R))). intros s t [K [As At]]; inversion K as [f l1 l2 s' H1 H2]; subst; inversion H2 as [t1 t2 sigma H3 H4 H5]; subst. unfold comp' in H3; destruct H3 as [H3 | H3]. right; split; [ | split; assumption]. constructor 1 with l2. assumption. rewrite <- H5; constructor; assumption. left; split; [ | split; assumption]. constructor 1 with l2. assumption. rewrite <- H5; constructor; assumption. clear comp'. intro a; rewrite <- (acc_union_alt _ (W 1)). intros t _; clear a. pattern t; apply (well_founded_ind (W 0)); clear t; intro t. set (R0 := rest P (rdp_step (axiom (fun v u : term => comp (u, v) 0)) R)) in *. set (R1 := rest P (rdp_step (axiom (fun v u : term => comp (u, v) 1)) R)) in *. intros IH0. rewrite accR2; apply Acc_intro; intros s H; rewrite <- accR2. inversion H as [a1 a3 a5 H13 H35]; clear H; subst s t. inversion H35 as [a3' a4 a5' H34 H45]; subst a3' a5'. inversion H34 as [a34 | a3' a4' K34]; clear H34. subst a3 a4. apply Acc_inv with a34; [ apply IH0 | ]; assumption. subst a3' a4'. assert (H : exists a, R1 a a4). rewrite trans_clos_trans_clos_alt in K34; inversion K34 as [a3' a4' H34 | a3' a a4' H3 H4]; clear K34; subst a3' a4'. exists a3; assumption. exists a; assumption. destruct H as [a H]; apply False_rect. destruct H45 as [H45 _]; destruct H as [H _]. inversion H45 as [f l5 l4 t4 H5 H4]; subst a4 a5; inversion H4 as [v4 u4 sigma4]; subst t4. inversion H as [g k4 l t K4 K]; subst a; inversion K as [v u sigma]; subst t. assert (C : are_connected dpR R (u,v) (u4,v4)). exists sigma4; exists sigma. split. rewrite <- comp_def_on_dps; exists 0; assumption. split. rewrite <- comp_def_on_dps; exists 1; assumption. rewrite H7; rewrite <- H3; split; trivial. assert (Abs := comp_approx _ _ C _ _ H1 H0); inversion Abs. apply wf_incl with (rest P (rdp_step (axiom (fun v u : term => comp (u, v) (S (S n0)))) R)). intros s t [K [As At]]; split; [ | split; assumption]. inversion K as [f l1 l2 s' H1 H2]; subst. inversion H2 as [t1 t2 sigma H3 H4 H5]; subst. constructor 1 with l2; trivial. apply W. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec)