proposition: Lemma split_rel : forall R1 R2 s t, one_step (union _ R1 R2) t s <-> (one_step R1 t s \/ one_step R2 t s).
proof: Proof. intros R1 R2 s; pattern s; apply term_rec2; clear s. intro n; induction n as [ | n]; intros s Size_s. absurd (1 <= 0); auto with arith; apply Nat.le_trans with (size s); trivial; apply size_ge_one. intros t; split; intro H. inversion H as [s' t' H' | f' lt ls H']; subst. inversion H' as [t' s' sigma H'']; subst. destruct H'' as [K1 | K2]. left; apply at_top; apply instance; trivial. right; apply at_top; apply instance; trivial. assert (Size_ls : forall s, In s ls -> size s <= n). intros s s_in_ls; apply le_S_n. apply Nat.le_trans with (size (Term f' ls)); trivial. apply size_direct_subterm; trivial. clear H Size_s; assert (H'' : one_step_list (one_step R1) lt ls \/ one_step_list (one_step R2) lt ls). induction H' as [t' s' l H'' | s lt' ls' H'']; subst. rewrite (IHn s' (Size_ls s' (or_introl _ (eq_refl _))) t') in H''. destruct H'' as [H1 | H2]. left; apply head_step; trivial. right; apply head_step; trivial. destruct IHH'' as [H1 | H2]. intros; apply Size_ls; right; trivial. left; apply tail_step; trivial. right; apply tail_step; trivial. destruct H'' as [H1 | H2]; [left | right]; apply in_context; trivial. destruct H as [H1 | H2]. apply one_step_incl with R1; trivial. intros; left; trivial. apply one_step_incl with R2; trivial. intros; right; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)