# Library term_algebra.rwr_strategies

``` Add LoadPath "basis". Add LoadPath "list_extensions". Add LoadPath "term_algebra". ```

# strategies for rewriting in a term algebra

``` Require Import List. Require Import Relations. Require Import Wellfounded. Require Import Arith. Require Import closure. Require Import more_list. Require Import term. Require Import equational_theory. Require Import dp. Require Import rpo. Module Make (E : EqTh).   Import E.   Import T. Inductive P_step (R : relation term) (P : term -> Prop) : term -> term -> Prop :=   | P_at_top : forall t s, P t -> axiom R s t -> P_step R P s t   | P_in_context :      forall f lt ls, P_list R P ls lt -> P_step R P (Term f ls) (Term f lt)    with P_list (R : relation term) (P : term -> Prop) : list term -> list term -> Prop :=     | P_head_step : forall t1 t2 l, P_step R P t1 t2 -> P_list R P (t1 :: l) (t2 :: l)     | P_tail_step : forall t l1 l2, P_list R P l1 l2 -> P_list R P (t :: l1) (t :: l2). Lemma P_step_one_step :   forall R P s t, P_step R P s t -> one_step R s t. Proof. intros R P s t; generalize s; clear s; pattern t; apply term_rec3; clear t. intros v s H; inversion H; subst; apply at_top; trivial. intros f l Hl s H; inversion H as [t' s' Hnf H' | f' lt ls H']; clear H; subst. apply at_top; trivial. apply in_context. generalize ls H'; clear ls H'; induction l as [ | t l]; intros ls H'; inversion H' as [t1 t2 l' H'' | t' l1 l2 H'']; clear H'; subst. apply head_step; apply Hl; trivial; left; trivial. apply tail_step; apply IHl; trivial; intros; apply Hl; trivial; right; trivial. Qed. Lemma trans_clos_P_step_P_list :   forall R P t1 t2 l, trans_clos (P_step R P) t1 t2 -> trans_clos (P_list R P) (t1 :: l) (t2 :: l). Proof. intros R P t1 t2 l H; induction H. apply t_step; apply P_head_step; trivial. apply t_trans with (y :: l); trivial. apply P_head_step; trivial. Qed. Lemma trans_clos_P_list_P_list :   forall R P t l1 l2, trans_clos (P_list R P) l1 l2 -> trans_clos (P_list R P) (t :: l1) (t :: l2). Proof. intros R P t l1 l2 H; induction H. apply t_step; apply P_tail_step; trivial. apply t_trans with (t :: y); trivial. apply P_tail_step; trivial. Qed. Lemma P_context_cons :   forall R P f t1 t2 l, trans_clos (P_step R P) t1 t2 ->       trans_clos (P_step R P) (Term f (t1 :: l)) (Term f (t2 :: l)). Proof. intros R P f t1 t2 l H; induction H as [ | t1 t2 t3 Trans1 Trans2]. apply t_step; apply P_in_context; apply P_head_step; trivial. apply t_trans with (Term f (t2 :: l)); trivial. apply P_in_context; apply P_head_step; trivial. Qed. Lemma P_step_context_in :   forall R P t1 t2 f l l', P_step R P t1 t2 ->    P_step R P (Term f (l ++ t1 :: l')) (Term f (l ++ t2 :: l')). Proof. intros R P t1 t2 f l l' H; apply P_in_context; induction l as [ | t l ]; simpl; [ apply P_head_step | apply P_tail_step ]; trivial. Qed. Lemma P_context_in :   forall R P t1 t2, trans_clos (P_step R P) t1 t2 ->   forall f l l', trans_clos (P_step R P) (Term f (l ++ t1 :: l')) (Term f (l ++ t2 :: l')). Proof. intros R P t1 t2 H; induction H as [ t1 t2 Step | t1 t2 t3 Trans1 Trans2]. intros f l l'; apply t_step; apply P_step_context_in; trivial. intros f l l'; apply trans_clos_is_trans with (Term f (l ++ t2 :: l')); trivial. apply t_step; apply P_step_context_in; trivial. Qed. Lemma P_list_length_eq :     forall R P l1 l2, trans_clos (P_list R P) l1 l2 -> length l1 = length l2. Proof. intros R P l1 l2 H. refine (@inv_trans (list term) (P_list R P) (fun l2 => length l1 = length l2) _ _ _ _ H); trivial. clear l2 H; intros l2 l L H. rewrite L; clear l1 L; induction H; simpl; trivial. rewrite IHP_list; trivial. Qed. Lemma P_list_expand :   forall R P l1 l2, P_list R P l1 l2 ->   exists t1, exists l', exists l'', exists t2, l1 = l' ++ t1 :: l'' /\ l2 = l' ++ t2 :: l'' /\ P_step R P t1 t2. Proof. intros R P l1 l2 H; induction H. exists t1; exists (@nil term); exists l; exists t2; repeat split; trivial. destruct IHP_list as [t1 [l' [l'' [t2 [H1 [H2 H3]]]]]]; subst. exists t1; exists (t :: l'); exists l''; exists t2; repeat split; trivial. Qed. Lemma trans_clos_P_list_split :   forall R P a1 a2 l1 l2, trans_clos (P_list R P) (a1 :: l1) (a2 :: l2) ->   (a1 = a2 /\ trans_clos (P_list R P) l1 l2) \/   (trans_clos (P_step R P) a1 a2 /\ l1 = l2) \/   (trans_clos (P_step R P) a1 a2 /\ trans_clos (P_list R P) l1 l2). Proof. intros R P; assert (H : forall k1 k2, trans_clos (P_list R P) k1 k2 ->                    forall a1 a2 l1 l2, k1 = a1 :: l1 -> k2 = a2 :: l2 ->   (a1 = a2 /\ trans_clos (P_list R P) l1 l2) \/   (trans_clos (P_step R P) a1 a2 /\ l1 = l2) \/   (trans_clos (P_step R P) a1 a2 /\ trans_clos (P_list R P) l1 l2)). intros k1 k2 H; induction H; intros a1 a2 l1 l2 H1 H2; subst. inversion H; clear H; subst. right; left; split; trivial; apply t_step; trivial. left; split; trivial; apply t_step; trivial. inversion H; clear H; subst. destruct (IHtrans_clos _ _ _ _ (refl_equal _) (refl_equal _)) as [H | [H | H]]. destruct H as [H1 H2]; subst. right; right; split; trivial; apply t_step; trivial. destruct H as [H1 H2]; subst. right; left; split; trivial; apply t_trans with t2; trivial. destruct H as [H1 H2]; subst. right; right; split; trivial; apply t_trans with t2; trivial. destruct (IHtrans_clos _ _ _ _ (refl_equal _) (refl_equal _)) as [H | [H | H]]. destruct H as [H1 H2]; subst. left; split; trivial; apply t_trans with l3; trivial. destruct H as [H1 H2]; subst. right; right; split; trivial; apply t_step; trivial. destruct H as [H1 H2]; subst. right; right; split; trivial; apply t_trans with l3; trivial. intros a1 a2 l1 l2 H'; apply (H (a1 :: l1) (a2 :: l2)); trivial. Qed. Lemma trans_clos_P_list_expand :   forall R P l1 l2, trans_clos (P_list R P) l1 l2 <->   exists t1, exists l1', exists l1'', exists t2, exists l2', exists l2'',   l1 = l1' ++ t1 :: l1'' /\ l2 = l2' ++ t2 :: l2'' /\   (l1' = l2' \/ trans_clos (P_list R P) l1' l2') /\   trans_clos (P_step R P) t1 t2 /\   (l1'' = l2'' \/ trans_clos (P_list R P) l1'' l2''). Proof. intros R P l1 l2; split; intro H. induction H. destruct (P_list_expand _ _ _ _ H) as [t1 [l' [l'' [t2 [H1 [H2 H3]]]]]]; subst. exists t1; exists l'; exists l''; exists t2; exists l'; exists l''; repeat split; trivial. left; trivial. apply t_step; trivial. left; trivial. destruct IHtrans_clos as [t1 [l1' [l1'' [t2 [l2' [l2'' [H1 [H2 [H3 [H4 H5]]]]]]]]]]; subst. destruct (P_list_expand _ _ _ _ H) as [u1 [k [k'' [u2 [K1 [K2 K3]]]]]]; subst. destruct (in_in_split_set _ _ _ _ _ _ K2) as [[K | K] | K]; clear K2. destruct K as [l [K K']]; subst. exists t1; exists (k ++ u1 :: l); exists l1''; exists t2; exists l2'; exists l2''; repeat split; trivial. rewrite <- ass_app; simpl; trivial. right; destruct H3 as [H3 | H3]. subst; clear H H0; apply t_step; induction k as [ | a k]; simpl. apply P_head_step; trivial. apply P_tail_step; trivial. apply trans_clos_is_trans with (k ++ u2 :: l); trivial. clear H H0 H3; apply t_step; induction k as [ | a k]; simpl. apply P_head_step; trivial. apply P_tail_step; trivial. destruct K as [l [K K']]; subst. exists t1; exists l1'; exists (l ++ u1 :: k''); exists t2; exists l2'; exists l2''; repeat split; trivial. rewrite <- ass_app; simpl; trivial. right; destruct H5 as [H5 | H5]. subst; clear H H0; apply t_step; induction l as [ | a l]; simpl. apply P_head_step; trivial. apply P_tail_step; trivial. apply trans_clos_is_trans with (l ++ u2 :: k''); trivial. clear H H5 H0; apply t_step; induction l as [ | a l]; simpl. apply P_head_step; trivial. apply P_tail_step; trivial. destruct K as [K [K' K'']]; subst. exists u1; exists k; exists k''; exists t2; exists l2'; exists l2''; repeat split; trivial. apply trans_clos_is_trans with u2; trivial. apply t_step; trivial. generalize l2 H; clear l2 H; induction l1 as [ | a1 l1]; intros l2 H; destruct H as [t1 [l1' [l1'' [t2 [l2' [l2'' [H1 [H2 [H3 [H4 H5]]]]]]]]]]; subst. destruct l1' as [ | a1' l1']; discriminate. destruct l1' as [ | a1' l1']. simpl in H1; injection H1; clear H1; intros; subst. destruct H3 as [H3 | H3]; subst. destruct H5 as [H5 | H5]; subst. simpl; apply trans_clos_P_step_P_list; trivial. simpl; apply trans_clos_is_trans with (t1 :: l2''). apply trans_clos_P_list_P_list; trivial. apply trans_clos_P_step_P_list; trivial. assert (L' := P_list_length_eq _ _ _ _ H3). destruct l2' as [ | a2' l2']. destruct H5 as [H5 | H5]; subst. simpl; apply trans_clos_P_step_P_list; trivial. simpl; apply trans_clos_is_trans with (t1 :: l2''). apply trans_clos_P_list_P_list; trivial. apply trans_clos_P_step_P_list; trivial. simpl in L'; discriminate. simpl in H1; injection H1; clear H1; intros; subst. destruct H3 as [H3 | H3]; subst; simpl. apply trans_clos_P_list_P_list; apply IHl1; trivial. exists t1; exists l1'; exists l1''; exists t2; exists l1'; exists l2''; split; trivial. do 2 (split; trivial). left; trivial. split; trivial. assert (L' := P_list_length_eq _ _ _ _ H3). destruct l2' as [ | a2' l2']. simpl in L'; discriminate. destruct (trans_clos_P_list_split _ _ _ _ _ _ H3) as [H6 | [H6 | H6]]. destruct H6 as [H6 H7]; subst. simpl; apply trans_clos_P_list_P_list; apply IHl1. exists t1; exists l1'; exists l1''; exists t2; exists l2'; exists l2''; split; trivial. do 2 (split; trivial). right; trivial. split; trivial. destruct H6 as [H6 H7]; subst. apply trans_clos_is_trans with (a2' :: l2' ++ t1 :: l1''). apply trans_clos_P_step_P_list; trivial. simpl; apply trans_clos_P_list_P_list; apply IHl1. exists t1; exists l2'; exists l1''; exists t2; exists l2'; exists l2''; split; trivial. do 2 (split; trivial). left; trivial. split; trivial. destruct H6 as [H6 H7]; subst. apply trans_clos_is_trans with (a2' :: l1' ++ t1 :: l1''). apply trans_clos_P_step_P_list; trivial. simpl; apply trans_clos_P_list_P_list; apply IHl1. exists t1; exists l1'; exists l1''; exists t2; exists l2'; exists l2''; split; trivial. do 2 (split; trivial). right; trivial. split; trivial. Qed. Lemma P_general_context_aux :   forall R P f l1 l2 l' l'', trans_clos (P_list R P) l1 l2 ->   trans_clos (P_step R P) (Term f (l' ++ l1 ++ l'')) (Term f (l' ++ l2 ++ l'')). Proof. intros R P f l1 l2 l' l'' H; generalize l' l''; clear l' l''; induction H; intros l' l''. apply t_step; apply P_in_context; generalize l'; clear l'; induction H; intros l'. induction l' as [ | a' l']; simpl. apply P_head_step; trivial. apply P_tail_step; trivial. replace (l' ++ (t :: l1) ++ l'') with ((l' ++ t :: nil) ++ l1 ++ l''). replace (l' ++ (t :: l2) ++ l'') with ((l' ++ t :: nil) ++ l2 ++ l''). apply IHP_list. rewrite <- ass_app; simpl; trivial. rewrite <- ass_app; simpl; trivial. apply trans_clos_is_trans with (Term f (l' ++ y ++ l'')); trivial. apply t_step; apply P_in_context; generalize l'; clear l' H0 IHtrans_clos; induction H; intros l'. induction l' as [ | a' l']; simpl. apply P_head_step; trivial. apply P_tail_step; trivial. replace (l' ++ (t :: l1) ++ l'') with ((l' ++ t :: nil) ++ l1 ++ l''). replace (l' ++ (t :: l2) ++ l'') with ((l' ++ t :: nil) ++ l2 ++ l''). apply IHP_list. rewrite <- ass_app; simpl; trivial. rewrite <- ass_app; simpl; trivial. Qed. Lemma P_general_context :   forall R P f l1 l2, trans_clos (P_list R P) l1 l2 -> trans_clos (P_step R P) (Term f l1) (Term f l2). Proof. intros R P f l1 l2 l1_R_l2; assert (H:= P_general_context_aux R P f l1 l2 nil nil l1_R_l2); simpl in H; do 2 rewrite <- app_nil_end in H; exact H. Qed. Lemma nf_P_step_subterm:   forall R P t, nf (P_step R P) t -> forall s, direct_subterm s t -> nf (P_step R P) s. Proof. intros R P t; pattern t; apply term_rec3; clear t. intros v _ s H; contradiction. simpl; intros f l IH Hnf s s_in_l u H. destruct (In_split _ _ s_in_l) as [l' [l'' H']]; subst. apply (Hnf (Term f (l' ++ u :: l''))). apply P_in_context; clear IH Hnf s_in_l; induction l' as [ | s' l']; simpl. apply P_head_step; trivial. apply P_tail_step; apply IHl'. Qed. Lemma acc_P_list :  forall R P l, (forall t, In t l -> Acc (P_step R P) t) <-> Acc (P_list R P) l. Proof. assert (H : forall R P t, Acc (P_step R P) t ->                       (forall l, Acc (P_list R P) l -> Acc (P_list R P) (t :: l))). intros R P t Acc_t; pattern t; refine (@Acc_ind _ (P_step R P) _ _ t Acc_t). clear t Acc_t; intros t Acc_t IHt l Acc_l. pattern l; refine (@Acc_ind _ (P_list R P) _ _ l Acc_l). clear l Acc_l; intros l Acc_l IHl. apply Acc_intro; intros [ | t' l'] H. inversion H. inversion H as [u' u l'' | u k k'' ]; subst. apply IHt; trivial; apply Acc_intro; assumption. apply IHl; trivial. intros R P l; split. induction l as [ | t l]. intros _; apply Acc_intro; intros [ | t' l'] H'; inversion H'. intros H'; apply H. apply H'; left; trivial. apply IHl; intros; apply H'; right; trivial. intros Acc_l; induction Acc_l as [l Acc_l IH]. intros t t_in_l; apply Acc_intro; intros s H'; destruct (In_split _ _ t_in_l) as [l' [l'' H'']]; subst l; apply (IH (l' ++ s :: l'')). clear Acc_l IH t_in_l; induction l' as [ | s' l']. simpl; apply P_head_step; trivial. simpl; apply P_tail_step; trivial. apply in_or_app; right; left; trivial. Qed. Lemma P_acc_subterms :   forall R P, (forall x t, ~ (R t (Var x))) ->   forall f l, (forall t, In t l -> Acc (P_step R P) t) -> constructor R f ->                    Acc (P_step R P) (Term f l). Proof. intros R P HR f l Acc_l Cf'; inversion Cf' as [f' Cf]; clear Cf'; subst f'; rewrite acc_P_list in Acc_l. pattern l; refine (@Acc_ind _ (P_list R P) _ _ l Acc_l). clear l Acc_l; intros l Acc_l IH. apply Acc_intro. intros t H; inversion H as [t' s Hnf H' | f' l1 l2 H']; subst. inversion H' as [t1 t2 sigma H'' H3 H''']; subst; destruct t2 as [x2 | f2 l2]. absurd (R t1 (Var x2)); trivial; apply HR. simpl in H'''; injection H'''; clear H'''; intros; subst; absurd (R t1 (Term f l2)); trivial; apply Cf. apply IH. generalize l2 l H'. intro k; induction k as [ | s k]; intros k' K; inversion K; subst. apply P_head_step; trivial. apply P_tail_step; trivial. Qed. Lemma P_acc_subterms_1 :    forall R P t s, Acc (P_step R P) t -> direct_subterm s t -> Acc (P_step R P) s. Proof. intros R P t s Acc_t; generalize s; clear s; pattern t; refine (@Acc_ind _ (P_step R P) _ _ t Acc_t). clear t Acc_t; intros t Acc_t IH s H; destruct t as [ x | f l]; simpl in H. contradiction. apply Acc_intro; intros u H'; destruct (In_split _ _ H) as [l1 [l2 H'']]; subst l; apply (IH (Term f (l1 ++ u :: l2))). apply P_step_context_in; trivial. simpl; apply in_or_app; right; left; trivial. Qed. Lemma P_acc_subterms_3 :    forall R P p t s, Acc (P_step R P) t -> subterm_at_pos t p = Some s -> Acc (P_step R P) s. Proof. intros R P p; induction p as [ | i p]; intros t s Acc_t H; simpl in H. injection H; intro; subst; trivial. destruct t as [ x | f l]. discriminate. assert (H' := nth_error_ok_in i l); destruct (nth_error l i) as [ s' | ]. generalize (H' _ (refl_equal _)); clear H'; intro s'_in_l. apply (IHp s'); trivial; apply (P_acc_subterms_1 R P (Term f l)); trivial. destruct s'_in_l as [l1 [l2 [_ H']]]; subst l; simpl; apply in_or_app; right; left; trivial. discriminate. Qed. Lemma var_P_acc :    forall R P l x sigma, In x (var_list_list l) ->    (forall t, In t (map (apply_subst sigma) l) -> Acc (P_step R P) t) ->    Acc (P_step R P) (apply_subst sigma (Var x)). Proof. intros R P l; pattern l; apply (list_rec3 size); clear l; intro n; induction n as [ | n]; intros [ | t l] Sl x sigma H Acc_l. simpl in H; contradiction. simpl in Sl; absurd (1 <= 0); auto with arith. apply le_trans with (size t). apply size_ge_one. refine (le_trans _ _ _ _ Sl); auto with arith. simpl in H; contradiction. assert (Sl' : list_size size l <= n). apply le_S_n; refine (le_trans _ _ _ _ Sl); simpl; apply (plus_le_compat_r 1 (size t) (list_size size l)); apply size_ge_one. destruct t as [y | g k]. simpl in H; destruct H as [y_eq_x | x_in_l]. subst y; apply Acc_l; simpl map; left; trivial. apply (IHn l); trivial; intros; apply Acc_l; simpl map; right; trivial. assert (Sk : list_size size k <= n). apply le_S_n; refine (le_trans _ _ _ _ Sl); simpl; rewrite (list_size_fold size k); apply le_n_S; apply le_plus_l. assert (Acc_k : forall t, In t (map (apply_subst sigma) k) -> Acc (P_step R P) t). intros t H'; apply P_acc_subterms_1 with (Term g (map (apply_subst sigma) k)). apply Acc_l; simpl map; left; trivial. trivial. replace (var_list_list (Term g k :: l)) with (var_list (Term g k) ++ var_list_list l) in H; trivial. rewrite var_list_unfold in H. generalize (IHn _ Sk x sigma). destruct (in_app_or _ _ _ H) as [x_in_k | x_in_l]. clear H; intro H; generalize (H x_in_k); clear H; intro H; apply H. intros t H'; apply Acc_k; trivial. simpl in H; intros _; apply (IHn l); trivial. intros t H'; apply Acc_l; right; trivial. Qed. Lemma P_acc_with_subterm_subterms :   forall R P t, Acc (union _ (P_step R P) direct_subterm) t ->                  forall s, direct_subterm s t -> Acc (union _ (P_step R P) direct_subterm) s. Proof. intros R P t Acc_t; induction Acc_t as [t Acc_t IH]. intros s H; apply Acc_t; right; trivial. Qed. Lemma P_acc_with_subterm :   forall R P t, Acc (P_step R P) t <-> Acc (union _ (P_step R P) direct_subterm) t. Proof. intros R P t; split. intro Acc_t; induction Acc_t as [t Acc_t IH]. generalize Acc_t IH; clear Acc_t IH; pattern t; apply term_rec2; clear t. intro n; induction n as [ | n]; intros t size_t Acc_t IH. absurd (1 <= 0); auto with arith; apply le_trans with (size t); trivial; apply size_ge_one. apply Acc_intro. intros u H; destruct H as [H | H]. apply IH; trivial. apply IHn. apply le_S_n; apply le_trans with (size t); trivial. apply size_direct_subterm; trivial. assert (H' : Acc (P_step R P) u). apply P_acc_subterms_1 with t; trivial. apply Acc_intro; apply Acc_t. inversion H'; trivial. intros v v_R_u. destruct t as [ x | f l]. contradiction. destruct (In_split _ _ H) as [l' [l'' H'']]; clear H; subst l. apply (P_acc_with_subterm_subterms R P (Term f (l' ++ v :: l''))). apply IH; apply P_step_context_in; trivial. simpl; apply in_or_app; right; left; trivial. apply Acc_incl; intros t1 t2 H; left; trivial. Qed. Lemma P_step_in_list :   forall R P l l', P_list R P l' l ->   exists t, exists t', exists l1, exists l2, P_step R P t' t /\ l = l1 ++ t :: l2 /\ l' = l1 ++ t' :: l2. Proof. intros R P l l' H'; induction H'. exists t2; exists t1; exists (@nil term); exists l; repeat split; trivial. destruct IHH' as [u [u' [l3 [l4 [H1 [H2 H3]]]]]]; subst. exists u; exists u'; exists (t :: l3); exists l4; repeat split; trivial. Qed. Definition inner (R : relation term) (t : term) :=   forall s, direct_subterm s t -> nf (one_step R) s. Lemma one_step_nf_inner_step_nf :   forall (R : relation term), (forall t v, R t (Var v) -> False) ->   forall t, nf (one_step R) t <-> nf (P_step R (inner R)) t. Proof. intros R Rvar t; split. intros H s H'; apply (H s); apply (P_step_one_step R (inner R)); trivial. pattern t; apply term_rec3; clear t. intros v _ s H'; inversion H' as [t1 t2 H'' | f' l1 l2 H'']; clear H'; subst. inversion H''; clear H''; subst. destruct t2 as [v2 | f2 l2]. apply (Rvar t1 v2); trivial. discriminate. intros f l IH H s H'. apply (H s); apply P_at_top. intros t t_in_l; apply IH; trivial. apply nf_P_step_subterm with (Term f l); trivial. inversion H' as [t1 t2 H'' | f' l1 l2 H'']; clear H'; subst; trivial. assert (H' : forall t, In t l -> nf (one_step R) t). intros t t_in_l; apply IH; trivial. apply nf_P_step_subterm with (Term f l); trivial. assert False. generalize l1 H'' H'; clear IH H l1 H'' H'; induction l as [ | t l]; intros l1 H'' H'; inversion H'' as [t1 t2' l' H3 | t' l1' l2' H3]; clear H''; subst. apply (H' t (or_introl _ (refl_equal _)) t1); trivial. apply (IHl l1'); trivial. intros s s_in_l; apply H'; right; trivial. contradiction. Qed. Lemma nf_dec_inner_dec :   forall R, (forall t, {nf (one_step R) t}+{~ nf (one_step R) t}) ->   forall t, {inner R t}+{~inner R t}. Proof. intros R nf_dec [v | f l]. left; intro s; simpl; contradiction. unfold inner; simpl; induction l as [ | t l]. left; intro s; simpl; contradiction. destruct (nf_dec t) as [nf_t | red_t]. destruct IHl as [nf_l | red_l]. left; intros s [s_eq_t | s_in_l]; [subst | apply nf_l]; trivial. right; intro nf_tl; apply red_l; intros s s_in_l; apply nf_tl; right; trivial. right; intro nf_tl; apply red_t; apply nf_tl; left; trivial. Defined. Lemma rwr_inner_or_eq :   forall R ll, (forall s t, In (s,t) ll -> s = t \/ trans_clos (P_step R (inner R)) s t) ->             map (@fst term term) ll = map (@snd term term) ll \/             trans_clos (P_list R (inner R)) (map (@fst term term) ll) (map (@snd term term) ll). Proof. intros R ll; induction ll as [ | [s t] ll]; intro H. left; trivial. destruct (H s t (or_introl _ (refl_equal _))) as [H1 | H1]. simpl; subst s; destruct IHll as [H2 | H2]. intros; apply H; right; trivial. left; rewrite H2; trivial. right; apply trans_clos_P_list_P_list; trivial. destruct IHll as [H2 | H2]. intros; apply H; right; trivial. right; simpl; rewrite H2; apply trans_clos_P_step_P_list; trivial. right; apply trans_clos_is_trans with (t :: map (@fst term term) ll). simpl; apply trans_clos_P_step_P_list; trivial. simpl; apply trans_clos_P_list_P_list; trivial. Qed. Lemma rwr_inner_or_eq_bis :   forall R l (f g : term -> term),     (forall s, In s l -> g s = f s \/ trans_clos (P_step R (inner R)) (g s) (f s)) ->             map g l = map f l \/             trans_clos (P_list R (inner R)) (map g l) (map f l). Proof. intros R l f g; induction l as [ | s l]; intro H. left; trivial. destruct (H s (or_introl _ (refl_equal _))) as [H1 | H1]. simpl; rewrite H1; destruct IHl as [H2 | H2]. intros; apply H; right; trivial. left; rewrite H2; trivial. right; apply trans_clos_P_list_P_list; trivial. destruct IHl as [H2 | H2]. intros; apply H; right; trivial. right; simpl; rewrite H2; apply trans_clos_P_step_P_list; trivial. right; apply trans_clos_is_trans with (f s :: map g l). simpl; apply trans_clos_P_step_P_list; trivial. simpl; apply trans_clos_P_list_P_list; trivial. Qed. Lemma rwr_inner_or_eq_subst :   forall R t sigma tau, (forall x, In x (var_list t) ->                                apply_subst sigma (Var x) = apply_subst tau (Var x) \/                                trans_clos (P_step R (inner R)) (apply_subst sigma (Var x)) (apply_subst tau (Var x))) ->             apply_subst sigma t = apply_subst tau t \/             trans_clos (P_step R (inner R)) (apply_subst sigma t) (apply_subst tau t). Proof. intros R t; pattern t; apply term_rec3; clear t. intros v sigma tau H; apply H; left; trivial. intros f l IH sigma tau H; simpl. assert (H' : map (apply_subst sigma) l = map (apply_subst tau) l \/             trans_clos (P_list R (inner R)) (map (apply_subst sigma) l) (map (apply_subst tau) l)). rewrite var_list_unfold in H. induction l as [ | t l]. left; trivial. simpl; destruct (IH t (or_introl _ (refl_equal _)) sigma tau) as [H1 | H1]. intros x x_in_t; apply H; simpl; apply in_or_app; left; trivial. destruct IHl as [H2 | H2]. intros s s_in_t sigma' tau' H'; apply IH; trivial; right; trivial. intros x x_in_l; apply H; simpl; apply in_or_app; right; trivial. left; rewrite H1; rewrite H2; trivial. right; rewrite H1; apply trans_clos_P_list_P_list; trivial. destruct IHl as [H2 | H2]. intros s s_in_t sigma' tau' H'; apply IH; trivial; right; trivial. intros x x_in_l; apply H; simpl; apply in_or_app; right; trivial. right; rewrite H2; apply trans_clos_P_step_P_list; trivial. right; apply trans_clos_is_trans with (apply_subst tau t :: map (apply_subst sigma) l). apply trans_clos_P_step_P_list; trivial. apply trans_clos_P_list_P_list; trivial. destruct H' as [H' | H']. left; rewrite H'; trivial. right; apply P_general_context; trivial. Qed. End Make. ```