proposition: Lemma between_dp0_aux2 : (forall n u v, strong_connect_approx n (u0,v0) (u,v) -> refl_trans_clos (union _ (one_step R) direct_subterm) (projection v) (projection u)) -> forall t1 t2 t3 t4 t5 t6, Rdp0 t2 t1 -> refl_trans_clos Rdp' t3 t2 -> Rdp' t4 t3 -> refl_trans_clos Rdp' t5 t4 -> Rdp0 t6 t5 -> refl_trans_clos (union _ (one_step R) direct_subterm) (projection t4) (projection t3).
proof: Proof. intros Hdp t1 t2 t3 t4 t5 t6 H21 H32 H43 H54 H65. inversion H43 as [h l3 l4 v3 Hl43 Hdp4]; subst. inversion Hdp4 as [v4 u4 sigma4 Hdp4' K4 J4]; clear Hdp4. inversion Hdp4' as [v4' u4' Hdp4'']; subst u4' v4'. assert (E4 : extract_dp u4 v4 t4 (Term h l3)). unfold extract_dp; split; trivial. exists h; exists l3; exists l4; exists sigma4; repeat split; trivial. apply sym_eq; assumption. apply sym_eq; assumption. destruct (between_dp0_aux1 t1 t2 (Term h l3) t4 t5 t6 H21 H32 H43 H54 H65 _ _ E4) as [K1 K2]. apply refl_trans_clos_is_trans with (projection (Term h l4)). rewrite <- J4. assert (Hdp4''' := cdp_in_dpR _ _ Hdp4''). destruct Hdp4''' as [Hdp4''' Sub4]. inversion Hdp4''' as [u4' r4 p4 g4 k4 R4 Sub4' D4]; subst. destruct u4 as [x4 | f4 ll4]. apply False_rect; apply (R_var _ _ R4). do 2 rewrite subst_projection. apply one_step_subterm_subst. clear Hdp4' H65 H54 H32 H43 H21. inversion K1 as [[u v] | uv0 uv4 K1']. subst u v u0 v0. right; assumption. subst uv0 uv4. inversion K2 as [[u v] | uv4 uv0 K2']. subst u v u0 v0. right; assumption. subst uv0 uv4. destruct (comp_def _ _ Hdp4'') as [n4 K4]. apply Hdp with n4; split; [ | assumption]. destruct (comp_def _ _ cdp_uv0) as [n0 K0]. replace n4 with n0. assumption. apply Nat.le_antisymm. apply (trans_comp_ok _ _ K1'); assumption. apply (trans_comp_ok _ _ K2'); assumption. apply refl_trans_incl with (one_step R). intros u1 u2 K; left; assumption. apply projection_one_step_list; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp)