proposition: Lemma split_rdp_step : forall R s t, rdp_step (axiom (ddp (@union _ (@union _ (@union _ R1 R2) R3) (Pi pi V0 V1)))) R s t -> (rdp_step (axiom (ddp (@union _ R1 R2))) R s t \/ rdp_step (axiom (ddp R3)) R s t \/ (exists t1, exists f3, exists l2, exists p, exists f1, exists l1, exists sigma, exists l3, R3 t1 (Term f3 l2) /\ subterm_at_pos t1 p = Some (Term f1 l1) /\ defined R1 f1 /\ (rwr_list (one_step R) (map (apply_subst sigma) l2) l3 \/ map (apply_subst sigma) l2 = l3) /\ t = Term f3 l3 /\ s = apply_subst sigma (Term f1 l1))).
proof: Proof. intros R s t H. destruct H as [f l1 l2 t3 H' H'']. destruct (split_dp _ _ H'') as [H1 | [H2 | H2]]; clear H''. left; apply Rdp_step with l2; trivial. right; left; apply Rdp_step with l2; trivial. right; right. destruct H2 as [t3' [t1 [p [f1 [l2' [sigma [K3 [Sub' [Df1 [K1 K2]]]]]]]]]]. destruct t3' as [v3 | f3 l3]. absurd (R3 t1 (Var v3)); trivial; apply R3_var. exists t1; exists f3; exists l3; exists p; exists f1. exists l2'; exists sigma. exists l1; split; trivial. split; trivial. split; trivial. simpl in K1; injection K1; clear K1; intros K1 f_eq_f3. split. subst l2. destruct H'; [right | left]; trivial. split; trivial. subst f; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)