proposition: Lemma between_dp0_aux1 : forall t1 t2 t3 t4 t5 t6, Rdp0 t2 t1 -> refl_trans_clos Rdp' t3 t2 -> rdp_step (axiom dp') R t4 t3 -> refl_trans_clos Rdp' t5 t4 -> Rdp0 t6 t5 -> forall u v, extract_dp u v t4 t3 -> refl_trans_clos (are_connected cdp R) (u0,v0) (u,v) /\ refl_trans_clos (are_connected cdp R) (u,v) (u0,v0).
proof: Proof. intros t1 t2 t3 t4 t5 t6 H21 H32 H43 H54 H65 u v E. assert (E1 : extract_dp u0 v0 t2 t1). split; trivial. 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. exists f; exists l1; exists l2; exists sigma2; repeat split; trivial. apply sym_eq; assumption. assert (E6 : extract_dp u0 v0 t6 t5). split; trivial. inversion H65 as [f l1 l2 v1 Hl21 Hdp2]; subst. inversion Hdp2 as [v2 u2 sigma2 Hdp2' K2 J2]; clear Hdp2. inversion Hdp2'; subst v2 u2. exists f; exists l1; exists l2; exists sigma2; repeat split; trivial. apply sym_eq; assumption. split. right; apply (connect_extract_dp u v t4 t3 u0 v0 t6 t5); trivial. apply dp'_is_dp; trivial. apply refl_trans_incl with (rdp_step (axiom dp') R); trivial. intros u1 u2 H; apply dp'_is_dp; trivial. apply dp0_is_dp; trivial. right; apply (connect_extract_dp u0 v0 t2 t1 u v t4 t3); trivial. apply dp0_is_dp; trivial. apply refl_trans_incl with (rdp_step (axiom dp') R); trivial. intros u1 u2 H; apply dp'_is_dp; trivial. apply dp'_is_dp; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp) CoLoR(NatCompat)