proposition: Lemma connect_extract_dp : forall u1 v1 s1 t1 un vn sn tn, Rcdp s1 t1 -> refl_trans_clos Rcdp tn s1 -> Rcdp sn tn -> extract_dp u1 v1 s1 t1 -> extract_dp un vn sn tn -> trans_clos (are_connected cdp R) (un,vn) (u1,v1).
proof: Proof. intros u1 v1 s1 t1 un vn sn tn H1 H; revert u1 v1 t1 un vn sn H1. inversion H as [u | tn' s1' H']; clear H. subst u tn. intros u1 v1 t1 un vn sn H1 Hn E1 En; left; apply connect_extract_dp_aux with s1 t1 sn; trivial. subst s1' tn'. induction H' as [tn s1 H | tn t s1 H1 H2]. assert (H_save := H). inversion H as [f l1 l2 tn' H21 H']. inversion H' as [v2 u2 sigma2]. intros u1 v1 t1 un vn sn Dp1 Dpn E1 En. assert (E2 : extract_dp u2 v2 tn (Term f l1)). split. trivial. exists f; exists l1; exists l2; exists sigma2; repeat split; trivial. apply sym_eq; assumption. apply sym_eq; assumption. rewrite H3 in En, Dpn. rewrite H1 in E1, Dp1. apply trans_clos_is_trans with (u2,v2); left. subst; refine (connect_extract_dp_aux _ _ _ _ _ _ _ _ _ E2 En); trivial. subst; refine (connect_extract_dp_aux _ _ _ _ _ _ _ _ _ E1 E2); trivial. intros u1 v1 t1 un vn sn Dp1 Dpn E1 En. assert (H1_save := H1). inversion H1 as [f l1 l2 tn' K1 K2]; subst tn' t. inversion K2 as [v u sigma]. assert (E : extract_dp u v tn (Term f l1)). split; trivial. exists f; exists l1; exists l2; exists sigma; repeat split; trivial. apply sym_eq; assumption. apply sym_eq; assumption. apply trans_clos_is_trans with (u,v). left; refine (connect_extract_dp_aux _ _ _ _ _ _ _ _ _ E En); trivial. apply (IHH2 u1 v1 t1 u v tn Dp1 H1_save E1 E). Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp) CoLoR(NatCompat)