proposition: Lemma split_dps : forall t1 t2, Rcdp t1 t2 <-> union _ Rdp' Rdp0 t1 t2.
proof: Proof. intros u1 u2; split; intro H. inversion H as [f' l1 l2 H1 H2 H']; clear H; subst. inversion H' as [t1 t2 sigma H'' H3 H''']; clear H'; subst. generalize (T.eq_bool_ok t2 u0); case (T.eq_bool t2 u0); [intro t2_eq_u0 | intro t2_diff_u0]. generalize (T.eq_bool_ok t1 v0); case (T.eq_bool t1 v0); [intro t1_eq_v0 | intro t1_diff_v0]. subst t1 t2; right. apply Rdp_step with l2; trivial. rewrite <- H'''; apply instance; apply Dp0. left; apply Rdp_step with l2; trivial. rewrite <- H'''; apply instance; apply Dp'; trivial. intro H; apply t1_diff_v0; injection H; intros; assumption. left; apply Rdp_step with l2; trivial. rewrite <- H'''; apply instance; apply Dp'; trivial. intro H; apply t2_diff_u0; injection H; intros; assumption. destruct H as [H | H]. inversion H as [f' l1 l2 H1 H2 H']; clear H; subst. inversion H' as [t1 t2 sigma H'' H3 H''']; clear H'; subst. inversion H'' as [v u]; clear H''; subst t1 t2. apply Rdp_step with l2; trivial. rewrite <- H'''; apply instance; assumption. inversion H as [f' l1 l2 H1 H2 H']; clear H; subst. inversion H' as [t1 t2 sigma H'' H3 H''']; clear H'; subst. inversion H'' as [v u]; clear H''; subst t1 t2. apply Rdp_step with l2; trivial. rewrite <- H'''; apply instance; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp) CoLoR(NatCompat)