# Library term_orderings.rpo

``` Add LoadPath "basis". Add LoadPath "list_extensions". Add LoadPath "term_algebra". Require Import Bool. Require Import List. Require Import closure. Require Import more_list. Require Import equiv_list. Require Import list_permut. Require Import dickson. Require Import Relations. Require Import Wellfounded. Require Import Arith. Require Import Wf_nat. Require Import term. Require Import ordered_set. Require Import Recdef. Require Import Coq.subtac.Utils. ```
A non-dependant version of lexicographic extension.
``` Definition lex (A B : Set) (eq_A_dec : forall a1 a2, {a1=a2}+{a1<>a2}) (o1 : relation A) (o2 : relation B) (s t : _ * _) :=   match s with   | (s1,s2) =>     match t with     | (t1,t2) =>        if eq_A_dec s1 t1        then o2 s2 t2        else o1 s1 t1      end    end. ```
Transitivity of lexicographic extension.
``` Lemma lex_trans :  forall (A B : Set) eq_A_dec o1 o2,  antisymmetric A o1 -> transitive A o1 -> transitive B o2 ->  transitive _ (lex _ _ eq_A_dec o1 o2). Proof. unfold transitive, lex; intros A B eq_A_dec o1 o2 A1 T1 T2 p1 p2 p3; destruct p1 as [a1 b1]; destruct p2 as [a2 b2]; destruct p3 as [a3 b3]; elim (eq_A_dec a1 a2); intro eq1. subst a2; elim (eq_A_dec a1 a3); intro eq2; trivial; apply T2. intro lt1; elim (eq_A_dec a1 a3); intro eq3. subst a3; elim (eq_A_dec a2 a1); intro eq2. subst a2; absurd (a1=a1); trivial. intro lt2; generalize (A1 _ _ lt1 lt2); contradiction. elim (eq_A_dec a2 a3); intro eq4. subst a3; trivial. intro lt2; apply T1 with a2; trivial. Qed. ```
Well-foundedness of lexicographic extension.
``` Lemma acc_lex :    forall A B eq_A_dec o1 o2, well_founded o2 ->    forall a, Acc o1 a -> forall b, Acc (lex A B eq_A_dec o1 o2) (a,b). Proof. intros A B eq_A_dec o1 o2 W2 a Acc_a; induction Acc_a as [a Acc_a IHa]. intro b; pattern b; refine (well_founded_ind W2 _ _ b); clear b. intros b IHb; apply Acc_intro. intros [a' b'] H; simpl in H. destruct (eq_A_dec a' a) as [a'_eq_a | a'_diff_a]. subst a'; apply IHb; trivial. apply IHa; trivial. Qed. Lemma wf_lex :   forall A B eq_A_dec o1 o2, well_founded o1 -> well_founded o2 ->   well_founded (lex A B eq_A_dec o1 o2). Proof. intros A B eq_A_dec o1 o2 W1 W2 [a b]. apply acc_lex; trivial. Qed. ```

## Definition of a precedence.

``` Inductive status_type : Set :=   | Lex : status_type   | Mul : status_type. Module Type Precedence. Parameter A : Set. Parameter prec : relation A. Parameter status : A -> status_type. Axiom prec_dec : forall a1 a2 : A, {prec a1 a2} + {~ prec a1 a2}. Axiom prec_antisym : forall s, prec s s -> False. Axiom prec_transitive : transitive A prec. End Precedence. ```

## Definition of RPO from a precedence on symbols.

``` Module Type RPO. Declare Module Import T : term.Term. Declare Module Import P : Precedence with Definition A:= T.symbol. ```

## Definition of rpo.

``` Inductive equiv : term -> term -> Prop :=   | Eq : forall t, equiv t t   | Eq_lex :      forall f l1 l2, status f = Lex -> equiv_list_lex l1 l2 ->      equiv (Term f l1) (Term f l2)   | Eq_mul :      forall f l1 l2, status f = Mul -> permut equiv l1 l2 ->      equiv (Term f l1) (Term f l2) with equiv_list_lex : list term -> list term -> Prop :=    | Eq_list_nil : equiv_list_lex nil nil    | Eq_list_cons :        forall t1 t2 l1 l2, equiv t1 t2 -> equiv_list_lex l1 l2 ->        equiv_list_lex (t1 :: l1) (t2 :: l2). Axiom equiv_equiv : equivalence term equiv. Axiom equiv_dec : forall t1 t2, {equiv t1 t2}+{~equiv t1 t2}. Declare Module Import LP :     list_permut.S with Definition EDS.A:=term                         with Definition EDS.eq_A := equiv. Inductive rpo : term -> term -> Prop :=   | Subterm : forall f l t s, mem s l -> rpo_eq t s -> rpo t (Term f l)   | Top_gt :        forall f g l l', prec g f -> (forall s', mem s' l' -> rpo s' (Term f l)) ->        rpo (Term g l') (Term f l)   | Top_eq_lex :         forall f l l', status f = Lex -> rpo_lex l' l ->         (forall s', mem s' l' -> rpo s' (Term f l)) ->         rpo (Term f l') (Term f l)   | Top_eq_mul :         forall f l l', status f = Mul -> rpo_mul l' l ->         rpo (Term f l') (Term f l) with rpo_eq : term -> term -> Prop :=   | Equiv : forall t t', equiv t t' -> rpo_eq t t'   | Lt : forall s t, rpo s t -> rpo_eq s t with rpo_lex : list term -> list term -> Prop :=   | List_gt : forall s t l l', rpo s t -> length l = length l' -> rpo_lex (s :: l) (t :: l')   | List_eq : forall s s' l l', equiv s s' -> rpo_lex l l' -> rpo_lex (s :: l) (s' :: l') with rpo_mul : list term -> list term -> Prop :=   | List_mul : forall a lg ls lc l l',        permut l' (ls ++ lc) -> permut l (a :: lg ++ lc) ->        (forall b, mem b ls -> exists a', mem a' (a :: lg) /\ rpo b a') ->        rpo_mul l' l. Axiom equiv_rpo_equiv_1 :   forall t t', equiv t t' -> (forall s, rpo s t <-> rpo s t'). Axiom equiv_rpo_equiv_2 :   forall t t', equiv t t' -> (forall s, rpo t s <-> rpo t' s). Axiom equiv_rpo_equiv_3 :   forall t t', equiv t t' -> (forall s, rpo_eq s t <-> rpo_eq s t'). Axiom equiv_rpo_equiv_4 :   forall t t', equiv t t' -> (forall s, rpo_eq t s <-> rpo_eq t' s). ```

## rpo is a preorder, and its reflexive closure is an ordering.

``` Axiom rpo_closure :   forall s t u,   (rpo t s -> rpo u t -> rpo u s) /\   (rpo s t -> rpo t s -> False) /\   (rpo s s -> False) /\   (rpo_eq s t -> rpo_eq t s -> equiv s t). Axiom rpo_trans : forall s t u, rpo s t -> rpo t u -> rpo s u. ```

## Main theorem: when the precedence is well-founded, so is the rpo.

``` Axiom wf_rpo : well_founded prec -> well_founded rpo. ```

## RPO is compatible with the instanciation by a substitution.

``` Axiom equiv_subst :   forall s t, equiv s t ->   forall sigma, equiv (apply_subst sigma s) (apply_subst sigma t). Axiom rpo_subst :   forall s t, rpo s t ->   forall sigma, rpo (apply_subst sigma s) (apply_subst sigma t). ```

## RPO is compatible with adding context.

``` Axiom equiv_add_context :  forall p ctx s t, equiv s t -> is_a_pos ctx p = true ->   equiv (replace_at_pos ctx s p) (replace_at_pos ctx t p). Axiom rpo_add_context :  forall p ctx s t, rpo s t -> is_a_pos ctx p = true ->   rpo (replace_at_pos ctx s p) (replace_at_pos ctx t p). Axiom rpo_dec : forall t1 t2, {rpo t1 t2}+{~rpo t1 t2}. End RPO. Module Make (T1: term.Term)                     (P1 : Precedence with Definition A := T1.symbol) <: RPO with Module T := T1 with Module P:=P1. Module Import T := T1. Module Import P := P1. ```

## Definition of size-based well-founded orderings for induction.

``` Definition o_size s t := size s < size t. Lemma wf_size : well_founded o_size. Proof. generalize (well_founded_ltof _ size); unfold ltof; trivial. Qed. Definition size2 s := match s with (s1,s2) => (size s1, size s2) end. Definition o_size2 s t := lex _ _ eq_nat_dec lt lt (size2 s) (size2 t). Lemma wf_size2 : well_founded o_size2. Proof. refine (wf_inverse_image _ _ (lex _ _ eq_nat_dec lt lt) size2 _); apply wf_lex; apply lt_wf. Qed. Lemma size2_lex1 :  forall s f l t1 t2, In s l -> o_size2 (s,t1) (Term f l,t2). Proof. intros s f l t1 t2 s_in_l; unfold o_size2, size2, lex; destruct (eq_nat_dec (size s) (size (Term f l))) as [s_eq_t | s_lt_t]. absurd (size (Term f l) < size (Term f l)); auto with arith; generalize (size_direct_subterm s (Term f l) s_in_l); rewrite s_eq_t; trivial. apply (size_direct_subterm s (Term f l) s_in_l). Qed. Lemma size2_lex1_bis :  forall a f l t1 t2, o_size2 (Term f l, t1) (Term f (a::l), t2). Proof. intros a f l t1 t2; unfold o_size2, size2, lex; destruct (eq_nat_dec (size (Term f l)) (size (Term f (a :: l)))) as [s_eq_t | s_lt_t]. do 2 rewrite size_unfold in s_eq_t; injection s_eq_t; clear s_eq_t; intro s_eq_t; absurd (list_size size l < list_size size l); auto with arith; generalize (plus_le_compat_r _ _ (list_size size l) (size_ge_one a)); rewrite <- s_eq_t; trivial. do 2 rewrite size_unfold; simpl; apply lt_n_S; apply lt_le_trans with (1 + list_size size l); auto with arith; apply plus_le_compat_r; apply size_ge_one. Qed. Lemma size2_lex2 :   forall t f l s, In t l -> o_size2 (s,t) (s, Term f l). Proof. intros t f l s t_in_l; unfold o_size2, size2, lex; destruct (eq_nat_dec (size s) (size s)) as [_ | s_diff_s]. apply size_direct_subterm; trivial. absurd (size s = size s); trivial. Qed. Lemma size2_lex2_bis :   forall t f l s, o_size2 (s,Term f l) (s, Term f (t :: l)). Proof. intros a f l s; unfold o_size2, size2, lex; destruct (eq_nat_dec (size s) (size s)) as [_ | s_diff_s]. destruct (eq_nat_dec (size (Term f l)) (size (Term f (a :: l)))) as [s_eq_t | s_lt_t]. do 2 rewrite size_unfold in s_eq_t; injection s_eq_t; clear s_eq_t; intro s_eq_t; absurd (list_size size l < list_size size l); auto with arith; generalize (plus_le_compat_r _ _ (list_size size l) (size_ge_one a)); rewrite <- s_eq_t; trivial. do 2 rewrite size_unfold; simpl; apply lt_n_S; apply lt_le_trans with (1 + list_size size l); auto with arith; apply plus_le_compat_r; apply size_ge_one. absurd (size s = size s); trivial. Qed. Lemma o_size2_trans : transitive _ o_size2. Proof. generalize (lex_trans _ _ eq_nat_dec lt lt). unfold transitive, o_size2, size2. intros H [x1 x2] [y1 y2] [z1 z2]; apply H. unfold antisymmetric; intros n m n_lt_m m_lt_n; generalize (lt_asym n m n_lt_m m_lt_n); contradiction. apply lt_trans. apply lt_trans. Qed. Definition size3 s := match s with (s1,s2) => (size s1, size2 s2) end. Definition o_size3 s t :=   lex _ _ eq_nat_dec lt (lex _ _ eq_nat_dec lt lt) (size3 s) (size3 t). Lemma wf_size3 : well_founded o_size3. Proof. refine (wf_inverse_image _ _   (lex _ _ eq_nat_dec lt (lex _ _ eq_nat_dec lt lt)) size3 _). apply wf_lex; [ idtac | apply wf_lex ]; apply lt_wf. Qed. Lemma size3_lex1 :  forall s f l t1 u1 t2 u2, In s l -> o_size3 (s,(t1,u1)) (Term f l,(t2,u2)). Proof. intros s f l t1 u1 t2 u2 s_in_l; unfold o_size3, size3, size2, lex; destruct (eq_nat_dec (size s) (size (Term f l))) as [s_eq_t | s_lt_t]. absurd (size (Term f l) < size (Term f l)); auto with arith; generalize (size_direct_subterm s (Term f l) s_in_l); rewrite s_eq_t; trivial. intros; apply (size_direct_subterm s (Term f l) s_in_l). Qed. Lemma size3_lex1_bis :  forall a f l t1 u1 t2 u2, o_size3 (Term f l,(t1,u1)) (Term f (a::l),(t2,u2)). Proof. intros a f l t1 u1 t2 u2; unfold o_size3, size3, size2, lex; destruct (eq_nat_dec (size (Term f l)) (size (Term f (a :: l)))) as [s_eq_t | s_lt_t]. do 2 rewrite size_unfold in s_eq_t; injection s_eq_t; clear s_eq_t; intro s_eq_t; absurd (list_size size l < list_size size l); auto with arith; generalize (plus_le_compat_r _ _ (list_size size l) (size_ge_one a)); rewrite <- s_eq_t; trivial. do 2 rewrite size_unfold; simpl; apply lt_n_S; apply lt_le_trans with (1 + list_size size l); auto with arith; apply plus_le_compat_r; apply size_ge_one. Qed. Lemma size3_lex2 :   forall t f l s u1 u2, In t l -> o_size3 (s,(t,u1)) (s,(Term f l, u2)). Proof. intros t f l s u1 u2 t_in_l; unfold o_size3, size3, size2, lex; destruct (eq_nat_dec (size s) (size s)) as [_ | s_diff_s]. destruct (eq_nat_dec (size t) (size (Term f l))) as [t_eq_t' | t_lt_t']. absurd (size (Term f l) < size (Term f l)); auto with arith; generalize (size_direct_subterm t (Term f l) t_in_l); rewrite t_eq_t'; trivial. apply (size_direct_subterm t (Term f l) t_in_l). absurd (size s = size s); trivial. Qed. Lemma size3_lex3 :   forall u f l s t, In u l -> o_size3 (s,(t,u)) (s,(t,Term f l)). Proof. intros u f l s t u_in_l; unfold o_size3, size3, size2, lex; destruct (eq_nat_dec (size s) (size s)) as [_ | s_diff_s]. destruct (eq_nat_dec (size t) (size t)) as [_ | t_diff_t]. apply (size_direct_subterm u (Term f l) u_in_l). absurd (size t = size t); trivial. absurd (size s = size s); trivial. Qed. Lemma o_size3_trans : transitive _ o_size3. Proof. generalize (lex_trans _ _ eq_nat_dec lt (lex _ _ eq_nat_dec lt lt)); unfold transitive, o_size3, size3, o_size2. intros H [x1 [x2 x3]] [y1 [y2 y3]] [z1 [z2 z3]]; apply H. unfold antisymmetric; intros n m n_lt_m m_lt_n; generalize (lt_asym n m n_lt_m m_lt_n); contradiction. apply lt_trans. apply lex_trans. unfold antisymmetric; intros n m n_lt_m m_lt_n; generalize (lt_asym n m n_lt_m m_lt_n); contradiction. unfold transitive; apply lt_trans. unfold transitive; apply lt_trans. Qed. ```

## Definition of rpo.

``` ```

### Equivalence modulo rpo

``` Inductive equiv : term -> term -> Prop :=   | Eq : forall t, equiv t t   | Eq_lex :      forall f l1 l2, status f = Lex -> equiv_list_lex l1 l2 ->      equiv (Term f l1) (Term f l2)   | Eq_mul :      forall f l1 l2, status f = Mul -> permut equiv l1 l2 ->      equiv (Term f l1) (Term f l2) with equiv_list_lex : list term -> list term -> Prop :=    | Eq_list_nil : equiv_list_lex nil nil    | Eq_list_cons :        forall t1 t2 l1 l2, equiv t1 t2 -> equiv_list_lex l1 l2 ->        equiv_list_lex (t1 :: l1) (t2 :: l2). Lemma equiv_same_top :   forall f g l l', equiv (Term f l) (Term g l') -> f = g. Proof. intros f g l l' H; inversion H; subst; trivial. Qed. Lemma equiv_same_length :   forall f1 f2 l1 l2, equiv (Term f1 l1) (Term f2 l2) -> length l1 = length l2. Proof. intros f1 f2 l1 l2 t1_eq_t2; inversion t1_eq_t2 as [ | f l1' l2' _ l1_eq_l2 | f l1' l2' _ P]; clear t1_eq_t2; subst. trivial. generalize l2 l1_eq_l2; clear l2 l1_eq_l2; induction l1 as [ | t1 l1]; intros l2 l1_eq_l2; inversion l1_eq_l2 as [ | s1 s2 l1' l2' _ l1'_eq_l2']; subst; trivial. simpl; rewrite (IHl1 l2'); trivial. apply (@permut_length _ equiv); trivial. Qed. Lemma equiv_same_size :   forall t t', equiv t t' -> size t = size t'. Proof. intros t; pattern t; apply term_rec2; clear t. intro n; induction n as [ | n]; intros t1 St1 t2 t1_eq_t2. absurd (1 <= 0); auto with arith; apply le_trans with (size t1); trivial; apply size_ge_one. inversion t1_eq_t2 as [ | f l1' l2' _ l1_eq_l2 | f l1' l2' _ P]; clear t1_eq_t2; subst. trivial. do 2 rewrite size_unfold; apply (f_equal (fun n => 1 + n)). generalize l2' l1_eq_l2; clear l2' l1_eq_l2; induction l1' as [ | t1 l1]; intros l2 l1_eq_l2; inversion l1_eq_l2 as [ | s1 s2 l1' l2' s1_eq_s2 l1'_eq_l2']; subst; trivial. simpl. assert (St1' : size t1 <= n). apply le_S_n; apply le_trans with (size (Term f (t1 :: l1))); trivial. apply size_direct_subterm; left; trivial. rewrite (IHn t1 St1' s2); trivial. assert (Sl1 : size (Term f l1) <= S n). apply le_trans with (size (Term f (t1 :: l1))); trivial. do 2 rewrite size_unfold. simpl; apply le_n_S. apply (plus_le_compat_r 0 (size t1) (list_size size l1)). apply lt_le_weak; apply (size_ge_one t1). rewrite (IHl1 Sl1 l2'); trivial. subst; do 2 rewrite size_unfold; apply (f_equal (fun n => 1 + n)). apply (@permut_size _ _ equiv); trivial. intros a a' a_in_l1 _ a_eq_a'; apply IHn; trivial. apply le_S_n. apply le_trans with (size (Term f l1')); trivial. apply size_direct_subterm; trivial. Qed. Lemma equiv_equiv : equivalence term equiv. Proof. split. intro t; apply Eq. intros t1; pattern t1; apply term_rec3. intros v t2 t3 t1_eq_t2 t2_eq_t3; inversion t1_eq_t2; subst; trivial. intros f l1 E_l1 t2 t3 t1_eq_t2 t2_eq_t3; inversion t1_eq_t2 as [ | f' l1' l2 Sf l1_eq_l2 H2 H' | f' l1' l2 Sf P]; subst; trivial; inversion t2_eq_t3 as [ | f' l2' l3 Sf' l2_eq_l3 H2 H'' | f' l2' l3 Sf' P' ]; subst; trivial. apply Eq_lex; trivial. generalize l2 l3 l1_eq_l2 l2_eq_l3; clear t1_eq_t2 t2_eq_t3 l2 l3 l1_eq_l2 l2_eq_l3; induction l1 as [ |s1 l1]; intros l2 l3 l1_eq_l2 l2_eq_l3. inversion l1_eq_l2; subst; trivial. inversion l1_eq_l2 as [ | s1' s2 l1' l2' s1_eq_s2 l1'_eq_l2']; subst. inversion l2_eq_l3 as [ | s2' s3 l2'' l3' s2_eq_s3 l2''_eq_l3']; subst. apply Eq_list_cons. apply E_l1 with s2; trivial; left; trivial. apply IHl1 with l2'; trivial. intros t t_in_l1; apply E_l1; right; trivial. rewrite Sf in Sf'; discriminate. rewrite Sf in Sf'; discriminate. apply Eq_mul; trivial. apply permut_trans with l2; trivial. intros a b c a_in_l1 _ _; apply E_l1; trivial. intros t1; pattern t1; apply term_rec3; clear t1. intros v t2 t1_eq_t2; inversion t1_eq_t2; subst; trivial. intros f l1 IHl t2 t1_eq_t2; inversion t1_eq_t2 as   [ | f' l1' l2 Sf l1_eq_l2 | f' l1' l2 Sf P]; clear t1_eq_t2; subst. apply Eq. apply Eq_lex; trivial. generalize l2 l1_eq_l2; clear l2 l1_eq_l2; induction l1 as [ | t1 l1]; intros l2 l1_eq_l2; inversion l1_eq_l2 as [ | s1 s2 l1' l2' s1_eq_s2 l1'_eq_l2']; subst; trivial. apply Eq_list_cons. apply IHl; trivial; left; trivial. apply IHl1; trivial. intros t t_in_l1; apply IHl; right; trivial. apply Eq_mul; trivial. apply permut_sym; trivial. intros a b a_in_l1 _; apply IHl; trivial. Qed.   Add Relation term equiv   reflexivity proved by (equiv_refl _ _ equiv_equiv)     symmetry proved by (equiv_sym _ _ equiv_equiv)       transitivity proved by (equiv_trans _ _ equiv_equiv) as EQUIV_RPO. Lemma equiv_dec :   forall t1 t2, {equiv t1 t2}+{~equiv t1 t2}. Proof. intro t1; pattern t1; apply term_rec3; clear t1. intros v1 [v2 | f2 l2]. destruct (X.eq_dec v1 v2) as [v1_eq_v2 | v1_diff_v2]. left; subst; apply Eq. right; intro v1_eq_v2; inversion v1_eq_v2; subst; apply v1_diff_v2; trivial. right; intro v1_eq_t2; inversion v1_eq_t2. intros f1 l1 IH [v2 | f2 l2]. right; intro t1_eq_v2; inversion t1_eq_v2. destruct (F.Symb.eq_dec f1 f2) as [f1_eq_f2 | f1_diff_f2]. assert (Stat : status f1 = status f2). subst; trivial. destruct (status f2); subst f2. assert (Case : {equiv_list_lex l1 l2}+{~equiv_list_lex l1 l2}). generalize l2; clear l2 Stat; induction l1 as [ | t1 l1]; intros [ | t2 l2]. left; apply Eq_list_nil. right; intro l1_eq_l2; inversion l1_eq_l2. right; intro l1_eq_l2; inversion l1_eq_l2. destruct (IH t1 (or_introl _ (refl_equal _)) t2) as [t1_eq_t2 | t1_diff_t2]. assert (IH' : forall t, In t l1 -> forall t2 : term, {equiv t t2} + {~ equiv t t2}). intros t t_in_l1; apply IH; right; trivial. destruct (IHl1 IH' l2) as [l1_eq_l2 | l1_diff_l2]. left; apply Eq_list_cons; trivial. right; intro l1_eq_l2; inversion l1_eq_l2; subst. apply l1_diff_l2; trivial. right; intro l1_eq_l2; inversion l1_eq_l2; subst. apply t1_diff_t2; trivial. destruct Case as [l1_eq_l2 | l1_diff_l2]. left; apply Eq_lex; trivial. right; intro t1_eq_t2; inversion t1_eq_t2; subst. apply l1_diff_l2; generalize l2; intro l; induction l as [ | t l]. apply Eq_list_nil. apply Eq_list_cons; trivial; apply Eq. apply l1_diff_l2; trivial. rewrite Stat in H2; discriminate. assert (Case : {permut equiv l1 l2}+{~permut equiv l1 l2}). apply permut_dec. intros a1 a2 a1_in_l1 a2_in_l2; apply IH; trivial. destruct Case as [l1_eq_l2 | l1_diff_l2]. left; apply Eq_mul; trivial. right; intro t1_eq_t2; inversion t1_eq_t2; subst. apply l1_diff_l2; apply permut_refl; intros a _; apply equiv_refl; apply equiv_equiv. rewrite Stat in H2; discriminate. apply l1_diff_l2; trivial. right; intro t1_eq_t2; apply f1_diff_f2. apply (equiv_same_top _ _ _ _ t1_eq_t2). Defined. Module Term_equiv_dec :    decidable_set.ES with Definition A:= term                              with Definition eq_A := equiv                              with Definition eq_dec := equiv_dec. Definition A := term. Definition eq_A := equiv. Definition eq_dec := equiv_dec. Definition eq_proof := equiv_equiv.   Add Relation A eq_A   reflexivity proved by (equiv_refl _ _ eq_proof)     symmetry proved by (equiv_sym _ _ eq_proof)       transitivity proved by (equiv_trans _ _ eq_proof) as EQA. End Term_equiv_dec. Module Import LP := list_permut.Make (Term_equiv_dec). Lemma term_rec3_mem :    forall P : term -> Type,        (forall v : variable, P (Var v)) ->        (forall (f : symbol) (l : list term),         (forall t : term, mem t l -> P t) -> P (Term f l)) ->        forall t : term, P t. Proof. intros P Hvar Hterm. apply term_rec2; induction n; intros t Size_t. absurd (1 <= 0); auto with arith; apply le_trans with (size t); trivial; apply size_ge_one. destruct t as [ x | f l ]; trivial; apply Hterm; intros; apply IHn; apply lt_n_Sm_le. apply lt_le_trans with (size (Term f l)); trivial. destruct (mem_split_set _ _ H) as [t' [l1 [l2 [t_eq_t' H']]]]. simpl in t_eq_t'; simpl in H'; subst l. rewrite (equiv_same_size _ _ t_eq_t'). apply size_direct_subterm; simpl; apply in_or_app; right; left; trivial. Qed. Inductive rpo : term -> term -> Prop :=   | Subterm : forall f l t s, mem s l -> rpo_eq t s -> rpo t (Term f l)   | Top_gt :        forall f g l l', prec g f -> (forall s', mem s' l' -> rpo s' (Term f l)) ->        rpo (Term g l') (Term f l)   | Top_eq_lex :         forall f l l', status f = Lex -> rpo_lex l' l ->         (forall s', mem s' l' -> rpo s' (Term f l)) ->         rpo (Term f l') (Term f l)   | Top_eq_mul :         forall f l l', status f = Mul -> rpo_mul l' l ->         rpo (Term f l') (Term f l) with rpo_eq : term -> term -> Prop :=   | Equiv : forall t t', equiv t t' -> rpo_eq t t'   | Lt : forall s t, rpo s t -> rpo_eq s t with rpo_lex : list term -> list term -> Prop :=   | List_gt : forall s t l l', rpo s t -> length l = length l' -> rpo_lex (s :: l) (t :: l')   | List_eq : forall s s' l l', equiv s s' -> rpo_lex l l' -> rpo_lex (s :: l) (s' :: l') with rpo_mul : list term -> list term -> Prop :=   | List_mul : forall a lg ls lc l l',        permut l' (ls ++ lc) -> permut l (a :: lg ++ lc) ->        (forall b, mem b ls -> exists a', mem a' (a :: lg) /\ rpo b a') ->        rpo_mul l' l. Lemma size_direct_subterm_mem :   forall n t f l, size (Term f l) <= S n -> mem t l -> size t <= n. Proof. intros n t f l Sfl t_mem_l; apply le_S_n. apply le_trans with (size (Term f l)); trivial. destruct (mem_split_set _ _ t_mem_l) as [t' [l1 [l2 [t_eq_t' H]]]]. simpl in t_eq_t'; simpl in H; subst l. rewrite (equiv_same_size _ _ t_eq_t'). apply size_direct_subterm; simpl; apply in_or_app; right; left; trivial. Qed. Lemma size2_lex1_mem :  forall s f l t1 t2, mem s l -> o_size2 (s,t1) (Term f l,t2). Proof. intros s f l t1 t2 s_mem_l; destruct (mem_split_set _ _ s_mem_l) as [s' [l1 [l2 [s_eq_s' H]]]]. simpl in s_eq_s'; simpl in H. unfold o_size2, size2; rewrite (equiv_same_size _ _ s_eq_s'). apply (size2_lex1 s' f l t1 t2). subst l; apply in_or_app; right; left; trivial. Qed. Lemma size2_lex2_mem :   forall t f l s, mem t l -> o_size2 (s,t) (s, Term f l). Proof. intros t f l s t_mem_l; destruct (mem_split_set _ _ t_mem_l) as [t' [l1 [l2 [t_eq_t' H]]]]. simpl in t_eq_t'; simpl in H. unfold o_size2, size2; rewrite (equiv_same_size _ _ t_eq_t'). apply (size2_lex2 t' f l s). subst l; apply in_or_app; right; left; trivial. Qed. Lemma size3_lex1_mem :  forall s f l t1 u1 t2 u2, mem s l -> o_size3 (s,(t1,u1)) (Term f l,(t2,u2)). Proof. intros s f l t1 u1 t2 u2 s_mem_l; destruct (mem_split_set _ _ s_mem_l) as [s' [l1 [l2 [s_eq_s' H]]]]. simpl in s_eq_s'; simpl in H. unfold o_size3, size3; rewrite (equiv_same_size _ _ s_eq_s'). apply (size3_lex1 s' f l t1 u1 t2 u2). subst l; apply in_or_app; right; left; trivial. Qed. Lemma size3_lex2_mem :   forall t f l s u1 u2, mem t l -> o_size3 (s,(t,u1)) (s,(Term f l, u2)). Proof. intros t f l s u1 u2 t_mem_l; destruct (mem_split_set _ _ t_mem_l) as [t' [l1 [l2 [t_eq_t' H]]]]. simpl in t_eq_t'; simpl in H. unfold o_size3, size3, size2; rewrite (equiv_same_size _ _ t_eq_t'). apply (size3_lex2 t' f l s u1 u2). subst l; apply in_or_app; right; left; trivial. Qed. Lemma size3_lex3_mem :   forall u f l s t, mem u l -> o_size3 (s,(t,u)) (s,(t,Term f l)). Proof. intros u f l s t u_mem_l; destruct (mem_split_set _ _ u_mem_l) as [u' [l1 [l2 [u_eq_u' H]]]]. simpl in u_eq_u'; simpl in H. unfold o_size3, size3, size2; rewrite (equiv_same_size _ _ u_eq_u'). apply (size3_lex3 u' f l s t). subst l; apply in_or_app; right; left; trivial. Qed. Lemma mem_mem :  forall t l1 l2, equiv_list_lex l1 l2 -> (mem t l1 <-> mem t l2). Proof. intros t l1 l2 l1_eq_l2; split. generalize t l2 l1_eq_l2; clear t l2 l1_eq_l2; induction l1 as [ | t1 l1]; intros t l2 l1_eq_l2 t_mem_l1. contradiction. inversion l1_eq_l2 as [ | s1 s2 l1' l2' s1_eq_s2 l1_eq_l2']; subst. destruct t_mem_l1 as [ t_eq_t1 | t_mem_l1]. left; transitivity t1; trivial. right; apply IHl1; trivial. generalize t l2 l1_eq_l2; clear t l2 l1_eq_l2; induction l1 as [ | t1 l1]; intros t l2 l1_eq_l2 t_mem_l2; inversion l1_eq_l2 as [ | s1 s2 l1' l2' s1_eq_s2 l1_eq_l2']; subst. trivial. destruct t_mem_l2 as [ t_eq_t2 | t_mem_l2]. left; transitivity s2; trivial. symmetry; trivial. right; apply IHl1 with l2'; trivial. Qed. Lemma equiv_rpo_equiv_1 :   forall t t', equiv t t' -> (forall s, rpo s t <-> rpo s t'). Proof. assert (H : forall p, match p with (s,t) =>                               forall t', equiv t t' -> rpo s t -> rpo s t'                  end). intro p; pattern p; refine (well_founded_ind wf_size2 _ _ _); clear p. intros [s t] IH t' t_eq_t' s_lt_t. inversion t_eq_t' as [ t'' | f l1 l2 Stat H | f l1 l2 Stat P]; subst. trivial. inversion s_lt_t as [g l t'' t' t'_mem_l t''_le_t' | g g' l l' g_prec_f l'_lt_t | g l l' Stat' l'_lt_ll1 l'_lt_t | g l l' Stat' l'_lt_ll1 ]; subst. destruct t''_le_t' as [t'' t' t''_eq_t' | t'' t' t''_lt_t']; apply Subterm with t'; trivial. setoid_rewrite <- (mem_mem t' _ _ H); trivial. apply Equiv; trivial. setoid_rewrite <- (mem_mem t' _ _ H); trivial. apply Lt; trivial. apply Top_gt; trivial. intros s' s'_mem_l'. apply (IH (s',(Term f l1))); trivial. apply size2_lex1_mem; trivial. apply l'_lt_t; trivial. apply Top_eq_lex; trivial. assert ( L := equiv_same_length _ _ _ _ t_eq_t'). generalize l2 L l' l'_lt_ll1 IH H ; clear l2 L l' l'_lt_ll1 IH H l'_lt_t t_eq_t' s_lt_t. induction l1 as [ | t1 l1]; intros l2 L l' l'_lt_l1 IH l1_eq_l2; inversion l'_lt_l1 as [ s t1' l'' l1' s_lt_t1' L_eq | t1' t1'' l'' l1' t1'_eq_t1'' l''_lt_l1' ]; subst; inversion l1_eq_l2 as [ | t1'' t2 l1' l2' t1''_eq_t2 l1_eq_l2']; subst. simpl; apply List_gt. apply (IH (s,t1)); trivial. apply size2_lex1; left; trivial. simpl in L; injection L; clear L; intro L; rewrite <- L; trivial. apply List_eq. transitivity t1; trivial. apply IHl1; trivial. simpl in L; injection L; trivial. intros y H; apply IH. refine (o_size2_trans _ _ _ H _). apply size2_lex1_bis. intros s' s'_mem_l'. apply (IH (s', Term f l1)); trivial. apply size2_lex1_mem; trivial. apply l'_lt_t; trivial. rewrite Stat in Stat'; discriminate. inversion s_lt_t as [g l t'' t' t'_mem_l t''_le_t' | g g' l l' g_prec_f l'_lt_t | g l l' Stat' l'_lt_l1 l'_lt_t | g l l' Stat' l'_lt_l1 ]; subst. destruct t''_le_t' as [t'' t' t''_eq_t' | t'' t' t''_lt_t']; apply Subterm with t'; trivial. setoid_rewrite <- (mem_permut_mem t' P); trivial. apply Equiv; trivial. setoid_rewrite <- (mem_permut_mem t' P); trivial. apply Lt; trivial. apply Top_gt; trivial. intros s' s'_mem_l2. apply (IH (s', Term f l1)); trivial. apply size2_lex1_mem; trivial. apply l'_lt_t; trivial. rewrite Stat in Stat'; discriminate. apply Top_eq_mul; trivial. inversion l'_lt_l1 as [a lg ls lc l'' l''' Q1 Q2 ls_lt_alg]; subst. apply (List_mul a lg ls lc); trivial. setoid_rewrite <- Q2; symmetry; trivial. intros t t' t_eq_t' s; split. apply (H (s,t)); trivial. apply (H (s,t')); trivial. apply (equiv_sym _ _ equiv_equiv); trivial. Qed. Lemma equiv_rpo_equiv_2 :   forall t t', equiv t t' -> (forall s, rpo t s <-> rpo t' s). Proof. assert (H : forall p, match p with (s,t) =>                               forall t', equiv t t' -> rpo t s -> rpo t' s                  end). intro p; pattern p; refine (well_founded_ind wf_size2 _ _ _); clear p. intros [s t] IH t' t_eq_t' t_lt_s. inversion t_eq_t' as [ t'' | g l1 l2 Stat l1_eq_l2 | g l1 l2 Stat P]; subst. trivial. inversion t_lt_s as [f l t'' t' t'_mem_l t''_le_t' | f f' l l' g_prec_f l'_lt_s | f l l' Stat' ll1_lt_l ll_lt_s | f l l' Stat' ll1_lt_l ]; subst. destruct t''_le_t' as [t'' t' t''_eq_t' | t'' t' t''_lt_t']; apply Subterm with t'; trivial. apply Equiv. transitivity t''; trivial. symmetry; trivial. apply Lt. apply (IH (t',t'')); trivial. apply size2_lex1_mem; trivial. apply Top_gt; trivial. intros s' s'_mem_l2; apply l'_lt_s. setoid_rewrite (mem_mem s' l1 l2); trivial. apply Top_eq_lex; trivial. assert (L := equiv_same_length _ _ _ _ t_eq_t'). generalize l2 l L l1_eq_l2 ll1_lt_l IH; clear l2 l L l1_eq_l2 ll1_lt_l IH ll_lt_s t_eq_t' t_lt_s; induction l1 as [ | t1 l1]; intros l2 l L l1_eq_l2 l1_lt_l IH; inversion l1_lt_l as [ t1' s l1' l' t1'_lt_s L_eq | t1' s l1' l'' t1'_eq_s l1'_lt_l'']; subst; inversion l1_eq_l2 as [ | t1'' t2 l1' l2' t1''_eq_t2 l1_eq_l2']; subst. simpl; apply List_gt. apply (IH (s,t1)); trivial. apply size2_lex1; left; trivial. simpl in L; injection L; clear L; intro L; rewrite <- L; trivial. simpl; apply List_eq. transitivity t1; trivial. symmetry; trivial. apply IHl1; trivial. simpl in L; injection L; trivial. intros y H; apply IH. refine (o_size2_trans _ _ _ H _). apply size2_lex1_bis. intros s' s'_in_l2; apply ll_lt_s. setoid_rewrite (mem_mem s' l1 l2); trivial. rewrite Stat in Stat'; discriminate. inversion t_lt_s as [f l t'' t' t'_mem_l t''_le_t' | f f' l l' g_prec_f l'_lt_s | f l l' Stat' ll1_lt_l ll_lt_s | f l l' Stat' ll1_lt_l ]; subst. destruct t''_le_t' as [t'' t' t''_eq_t' | t'' t' t''_lt_t']; apply Subterm with t'; trivial. apply Equiv. transitivity t''; trivial. symmetry; trivial. apply Lt. apply (IH (t',t'')); trivial. apply size2_lex1_mem; trivial. apply Top_gt; trivial. intros s' s'_mem_l2; apply l'_lt_s. setoid_rewrite (mem_permut_mem s' P); trivial. rewrite Stat in Stat'; discriminate. apply Top_eq_mul; trivial. inversion ll1_lt_l as [a lg ls lc l' l'' Q1 Q2 ls_lt_alg]; subst. apply (List_mul a lg ls lc); trivial. setoid_rewrite <- Q1; symmetry; trivial. intros t t' t_eq_t' s; split. apply (H (s,t)); trivial. apply (H (s,t')); trivial. apply (equiv_sym _ _ equiv_equiv); trivial. Qed. Lemma equiv_rpo_equiv_3 :   forall t t', equiv t t' -> (forall s, rpo_eq s t <-> rpo_eq s t'). Proof. assert (H: forall t t', equiv t t' -> (forall s, rpo_eq s t -> rpo_eq s t')). intros t t' t_eq_t' s s_le_t; inversion s_le_t; subst. apply Equiv; apply (equiv_trans _ _ equiv_equiv) with t; trivial. apply Lt; setoid_rewrite <- (equiv_rpo_equiv_1 _ _ t_eq_t'); trivial. intros t t' t_eq_t' s; split; apply H; trivial. apply (equiv_sym _ _ equiv_equiv); trivial. Qed. Lemma equiv_rpo_equiv_4 :   forall t t', equiv t t' -> (forall s, rpo_eq t s <-> rpo_eq t' s). assert (H: forall t t', equiv t t' -> (forall s, rpo_eq t s -> rpo_eq t' s)). intros t t' t_eq_t' s t_le_s; inversion t_le_s; subst. apply Equiv; apply (equiv_trans _ _ equiv_equiv) with t; trivial; apply (equiv_sym _ _ equiv_equiv); trivial. apply Lt; setoid_rewrite <- (equiv_rpo_equiv_2 _ _ t_eq_t'); trivial. intros t t' t_eq_t' s; split; apply H; trivial. apply (equiv_sym _ _ equiv_equiv); trivial. Qed. ```

## rpo is a preorder, and its reflexive closure is an ordering.

``` Lemma rpo_subterm_equiv :  forall s t, equiv t s -> forall tj, direct_subterm tj t -> rpo tj s. Proof. intros s [ | f l] fl_eq_s tj; simpl. contradiction. intro tj_in_l; setoid_rewrite <- (equiv_rpo_equiv_1 _ _ fl_eq_s). apply Subterm with tj. apply in_impl_mem; trivial. apply Equiv; apply Eq. Qed. Lemma rpo_subterm :  forall s t, rpo t s -> forall tj, direct_subterm tj t -> rpo tj s. Proof. intros s t; cut (forall p : term * term,              match p with               | (s,t) => rpo t s -> forall tj, direct_subterm tj t -> rpo tj s              end). intro H; apply (H (s,t)). clear s t; intro p; pattern p; refine (well_founded_ind wf_size2 _ _ _); clear p. intros [s [ v | f l]] IH t_lt_s tj tj_in_l; simpl in tj_in_l; [ contradiction | idtac]. inversion t_lt_s as [ f' l' t' s' s'_in_l' t'_le_s' | f' g' k k' g'_prec_f' H | f' k k' Sf' k'_lt_k H | f' k k' Sf' k'_lt_k ]. subst; inversion t'_le_s' as [ t'' s'' t'_eq_s' | t'' s'' t'_lt_s']; clear t'_le_s'; subst. apply (Subterm f' l' tj s'); trivial; apply Lt; apply rpo_subterm_equiv with (Term f l); trivial. apply (Subterm f' l' tj s'); trivial. apply Lt; apply (IH (s', Term f l)); trivial. apply size2_lex1_mem; trivial. subst; apply H2; apply in_impl_mem; trivial. subst; apply H2; apply in_impl_mem; trivial. inversion k'_lt_k as [a lg ls lc l1 l2 P1 P2 H]; subst. assert (tj_mem_l := in_impl_mem tj l tj_in_l). setoid_rewrite (mem_permut_mem tj P1) in tj_mem_l. setoid_rewrite <- mem_or_app in tj_mem_l. destruct tj_mem_l as [tj_mem_ls | tj_mem_llc]. destruct (H _ tj_mem_ls) as [a' [a'_mem_a_lg tj_lt_a']]. apply (Subterm f k tj a'). setoid_rewrite (mem_permut_mem a' P2); rewrite app_comm_cons. setoid_rewrite <- mem_or_app; left; trivial. apply Lt; trivial. apply (Subterm f k tj tj). setoid_rewrite (mem_permut_mem tj P2). right; setoid_rewrite <- mem_or_app; right; trivial. apply Equiv; apply Eq. Qed. Lemma rpo_subterm_mem :  forall s f l, rpo (Term f l) s -> forall tj, mem tj l -> rpo tj s. Proof. intros s f l fl_lt_s tj tj_mem_l. destruct (mem_split_set _ _ tj_mem_l) as [tj' [l1 [l2 [tj_eq_tj' H]]]]. simpl in tj_eq_tj'; simpl in H. setoid_rewrite (equiv_rpo_equiv_2 _ _ tj_eq_tj'). apply rpo_subterm with (Term f l); trivial. subst l; simpl; apply in_or_app; right; left; trivial. Qed. Lemma rpo_lex_same_length :   forall l l', rpo_lex l l' -> length l = length l'. Proof. induction l; intros l' rpo_lex_l; inversion rpo_lex_l. simpl; rewrite H3; trivial. simpl; rewrite (IHl l'0); trivial. Qed. Lemma rpo_trans : forall u t s, rpo u t -> rpo t s -> rpo u s. Proof. intros u t s; cut (forall triple : term * (term * term),        match triple with        | (s,(t,u)) => rpo t s -> rpo u t -> rpo u s        end). intros H u_lt_t t_lt_s; apply (H (s,(t,u))); trivial. clear s t u; intro triple; pattern triple; refine (well_founded_ind wf_size3 _ _ triple); clear triple. intros [[v | f l] [t u]] IH. intros t_lt_v; inversion t_lt_v. intros t_lt_fl u_lt_t; inversion t_lt_fl as [ f'' l' s' t' t'_in_l' t_le_t' | f'' f' k'' l' f'_prec_f H'' | f'' k'' l' Sf l'_lt_l H H1 H2 | f'' k'' l' Sf l'_lt_l ]; subst. apply Subterm with t'; trivial; apply Lt; inversion t_le_t' as [t'' t''' t_eq_t' | t'' t''' t_lt_t']; subst. setoid_rewrite <- (equiv_rpo_equiv_1 _ _ t_eq_t'); trivial. apply (IH (t',(t,u))); trivial. apply size3_lex1_mem; trivial. inversion u_lt_t as [ f'' l'' s' t' t'_in_l' u_le_t' | g'' f'' k'' l'' f''_prec_f' H''' | g'' k'' l'' Sf' l''_lt_l' H H1 H2 | g'' k'' l'' Sf' l''_lt_l' ]; subst. inversion u_le_t' as [t'' t''' u_eq_t' | t'' t''' u_lt_t']; subst. setoid_rewrite (equiv_rpo_equiv_2 _ _ u_eq_t'); trivial; apply H''; trivial. apply (IH (Term f l,(t',u))); trivial. apply size3_lex2_mem; trivial. apply H''; trivial. apply Top_gt. apply prec_transitive with f'; trivial. intros u u_in_l''; apply (IH (Term f l, (Term f' l', u))); trivial. apply size3_lex3_mem; trivial. apply H'''; trivial. apply Top_gt; trivial. intros u u_in_l''; apply (IH (Term f l, (Term f' l', u))); trivial. apply size3_lex3_mem; trivial. apply H0; trivial. apply Top_gt; trivial. intros u u_in_l''; apply (IH (Term f l, (Term f' l', u))); trivial. apply size3_lex3_mem; trivial. apply rpo_subterm_mem with f' l''; trivial. inversion u_lt_t as [ f'' l'' s' t' t'_in_l' u_le_t' | g'' f'' k'' l'' f''_prec_f' H''' | g'' k'' l'' Sf' l''_lt_l' H H1 H2 | g'' k'' l'' Sf' l''_lt_l' ]; subst. inversion u_le_t' as [t'' t''' u_eq_t' | t'' t''' u_lt_t']; subst. setoid_rewrite (equiv_rpo_equiv_2 _ _ u_eq_t'); apply rpo_subterm_mem with f l'; trivial. apply (IH (Term f l, (t', u))); trivial. apply size3_lex2_mem; trivial. apply H0; trivial. apply Top_gt; trivial. intros u u_in_l''; apply (IH (Term f l, (Term f l', u))); trivial. apply size3_lex3_mem; trivial. apply H'''; trivial. apply Top_eq_lex; trivial. generalize l' l'' l'_lt_l l''_lt_l' IH; clear l' l'' l'_lt_l l''_lt_l' IH H0 H3 t_lt_fl u_lt_t; induction l as [ | s l]; intros l' l'' l'_lt_l l''_lt_l' IH. inversion l'_lt_l. inversion l'_lt_l as [ t s' k' k t_lt_s L | t s' k' k t_eq_s k'_lt_k]; inversion l''_lt_l' as [ u t' k'' h' u_lt_t L' | u t' k'' h' u_eq_t k''_lt_k']. subst; injection H3; intros; subst; apply List_gt. apply (IH (s,(t,u))); trivial. apply size3_lex1; left; trivial. rewrite L'; trivial. subst; injection H3; intros; subst; apply List_gt. setoid_rewrite (equiv_rpo_equiv_2 _ _ u_eq_t); trivial. rewrite (rpo_lex_same_length _ _ k''_lt_k'); trivial. subst; injection H3; intros; subst; apply List_gt. setoid_rewrite <- (equiv_rpo_equiv_1 _ _ t_eq_s); trivial. rewrite <- (rpo_lex_same_length _ _ k'_lt_k); trivial. subst; injection H3; intros; subst; apply List_eq. transitivity t; trivial. apply IHl with k'; trivial. intros; apply IH; apply o_size3_trans with (Term f l, (Term f k', Term f k'')); trivial. apply size3_lex1_bis. intros u u_in_l''; apply (IH (Term f l, (Term f l', u))); trivial. apply size3_lex3_mem; trivial. apply H3; trivial. rewrite Sf in Sf'; discriminate. inversion u_lt_t as [ f'' l'' s' t' t'_in_l' u_le_t' | g'' f'' k'' l'' f''_prec_f' H''' | g'' k'' l'' Sf' l''_lt_l' H H1 H2 | g'' k'' l'' Sf' l''_lt_l' ]; subst. inversion u_le_t' as [t'' t''' u_eq_t' | t'' t''' u_lt_t']; subst. setoid_rewrite (equiv_rpo_equiv_2 _ _ u_eq_t'); apply rpo_subterm_mem with f l'; trivial. apply (IH (Term f l, (t', u))); trivial. apply size3_lex2_mem; trivial. apply rpo_subterm_mem with f l'; trivial. apply Top_gt; trivial. intros u u_in_l''; apply (IH (Term f l, (Term f l', u))); trivial. apply size3_lex3_mem; trivial. apply H'''; trivial. rewrite Sf in Sf'; discriminate. apply Top_eq_mul; trivial. destruct l'_lt_l as [a lg ls lc l l' P' P ls_lt_alg]. destruct l''_lt_l' as [a' lg' ls' lc' l' l'' Q' Q ls'_lt_alg']. setoid_rewrite P' in Q; rewrite app_comm_cons in Q. destruct (ac_syntactic _ _ _ _ Q) as [k1 [k2 [k3 [k4 [P1 [P2 [P3 P4]]]]]]]. apply (List_mul a (lg ++ k2) (ls' ++ k3) k1). setoid_rewrite Q'. rewrite <- ass_app. setoid_rewrite <- permut_app1. setoid_rewrite list_permut_app_app; trivial. setoid_rewrite P. setoid_rewrite <- permut_cons. reflexivity. rewrite <- ass_app. setoid_rewrite <- permut_app1. setoid_rewrite list_permut_app_app; trivial. intros b b_mem_ls'_k3; setoid_rewrite <- mem_or_app in b_mem_ls'_k3. destruct b_mem_ls'_k3 as [b_mem_ls' | b_mem_k3]. destruct (ls'_lt_alg' _ b_mem_ls') as [a'' [a''_in_a'lg' b_lt_a'']]. setoid_rewrite (mem_permut_mem a'' P4) in a''_in_a'lg'. setoid_rewrite <- mem_or_app in a''_in_a'lg'. destruct a''_in_a'lg' as [a''_mem_k2 | a''_mem_k4]. exists a''; split; trivial. rewrite app_comm_cons; setoid_rewrite <- mem_or_app; right; trivial. destruct (ls_lt_alg a'') as [a3 [a3_in_alg a''_lt_a3]]. setoid_rewrite (mem_permut_mem a'' P2). setoid_rewrite <- mem_or_app; right; trivial. exists a3; split. rewrite app_comm_cons; setoid_rewrite <- mem_or_app; left; trivial. apply (IH (a3,(a'',b))); trivial. apply size3_lex1_mem. setoid_rewrite (mem_permut_mem a3 P). rewrite app_comm_cons; setoid_rewrite <- mem_or_app; left; trivial. destruct (ls_lt_alg b) as [a'' [a''_in_alg b_lt_a'']]. setoid_rewrite (mem_permut_mem b P2); setoid_rewrite <- mem_or_app; left; trivial. exists a''; split; trivial. rewrite app_comm_cons; setoid_rewrite <- mem_or_app; left; trivial. Qed. Lemma rpo_mul_remove_equiv_aux :   forall l l' s s', (forall t, mem t (s :: l) -> rpo t t -> False) ->                       equiv s s' -> rpo_mul (s :: l) (s' :: l') -> rpo_mul l l'. Proof. intros l l' s s' Antirefl s_eq_s' sl_lt_s'l'; inversion sl_lt_s'l' as [a lg ls lc k' k P P' ls_lt_alg]; subst. assert (s_mem_ls_lc : mem s (ls ++ lc)). setoid_rewrite <- (mem_permut_mem s P); left; reflexivity. setoid_rewrite <- mem_or_app in s_mem_ls_lc. destruct s_mem_ls_lc as [s_mem_ls | s_mem_lc]. assert (s'_mem_alg_lc : mem s' (a :: lg ++ lc)). setoid_rewrite <- (mem_permut_mem s' P'); left; reflexivity. rewrite app_comm_cons in s'_mem_alg_lc. setoid_rewrite <- mem_or_app in s'_mem_alg_lc. destruct s'_mem_alg_lc as [s'_mem_alg | s'_mem_lc]. destruct lg as [ | g lg]. assert (s'_eq_a : equiv s' a). destruct s'_mem_alg; trivial; contradiction. destruct (ls_lt_alg _ s_mem_ls) as [a' [[a_eq_a' | a'_mem_nil] b_lt_a']]. assert False. apply (Antirefl s). left; reflexivity. setoid_rewrite (equiv_rpo_equiv_1 _ _ s_eq_s'). setoid_rewrite (equiv_rpo_equiv_1 _ _ s'_eq_a). setoid_rewrite <- (equiv_rpo_equiv_1 _ _ a_eq_a'); trivial. contradiction. contradiction. destruct (mem_split_set _ _ s'_mem_alg) as [u' [alg' [alg'' [s'_eq_u' H]]]]; simpl in s'_eq_u'; simpl in H; subst. assert (P'' : permut l' ((alg' ++ alg'') ++ lc)). rewrite app_comm_cons in P'; rewrite H in P'. rewrite <- ass_app in P'; simpl in P'. rewrite <- ass_app; setoid_rewrite <- permut_cons_inside in P'; trivial. destruct (mem_split_set _ _ s_mem_ls) as [u [ls' [ls'' [s_eq_u H']]]]; simpl in s_eq_u; simpl in H'; subst. assert (ls'ls''_lt_alg'alg'' : forall b : EDS.A,             mem b (ls' ++ ls'') -> exists a' : EDS.A, mem a' (alg' ++ alg'') /\ rpo b a'). intros b b_in_ls'ls''; destruct (ls_lt_alg b) as [a' [a'_mem_aglg b_lt_a']]. apply mem_insert; trivial. rewrite H in a'_mem_aglg. setoid_rewrite <- mem_or_app in a'_mem_aglg. destruct a'_mem_aglg as [a'_mem_alg' | [u'_eq_a' | a'_mem_alg'']]. exists a'; split; trivial. setoid_rewrite <- mem_or_app; left; trivial. destruct (ls_lt_alg a') as [a'' [a''_mem_aglg a'_lt_a'']]. setoid_rewrite <- mem_or_app; right; left. transitivity u'; trivial. transitivity s; trivial. symmetry. transitivity s'; trivial. exists a''; split. apply diff_mem_remove with u'. intro a''_eq_u'. destruct (mem_split_set u (s :: l)) as [u'' [l1 [l2 [u_eq_u'' H']]]]. left; symmetry; trivial. simpl in u_eq_u''; simpl in H'. apply (Antirefl u''). setoid_rewrite (mem_permut_mem u'' P). setoid_rewrite <- mem_or_app; left. setoid_rewrite <- mem_or_app; right; left; symmetry; trivial. assert (u''_eq_u' : equiv u'' u'). transitivity s'; trivial. transitivity s; trivial. transitivity u. symmetry; trivial. symmetry; trivial. setoid_rewrite (equiv_rpo_equiv_2 _ _ u''_eq_u'). setoid_rewrite <- (equiv_rpo_equiv_2 _ _ u'_eq_a'). setoid_rewrite (equiv_rpo_equiv_1 _ _ u''_eq_u'). setoid_rewrite <- (equiv_rpo_equiv_1 _ _ a''_eq_u'); trivial. rewrite <- H; trivial. apply rpo_trans with a'; trivial. exists a'; split; trivial. setoid_rewrite <- mem_or_app; right; trivial. assert (L : length (alg' ++ alg'') = S (length lg)). assert (L' := f_equal (fun l => length l) H). simpl in L'; rewrite length_app in L'; simpl in L'. rewrite plus_comm in L'; simpl in L'; rewrite plus_comm in L'. rewrite <- length_app in L'; injection L'; intro L''; rewrite L''; trivial. destruct (alg' ++ alg'') as [ | a' lg']. discriminate. apply (List_mul a' lg' (ls' ++ ls'') lc); trivial. rewrite <- ass_app in P; simpl in P. setoid_rewrite <- permut_cons_inside in P; trivial. rewrite <- ass_app; trivial. destruct (mem_split_set _ _ s'_mem_lc) as [s'' [lc' [lc'' [s_eq_s'' H]]]]. simpl in s_eq_s''; simpl in H. apply (List_mul a lg ls (lc' ++ lc'')); trivial. rewrite H in P. rewrite ass_app in P. setoid_rewrite <- permut_cons_inside in P. rewrite ass_app; trivial. transitivity s'; trivial. rewrite H in P'. rewrite app_comm_cons in P'. rewrite ass_app in P'. setoid_rewrite <- permut_cons_inside in P'; trivial. rewrite app_comm_cons; rewrite ass_app; trivial. destruct (mem_split_set _ _ s_mem_lc) as [s'' [lc' [lc'' [s_eq_s'' H]]]]. simpl in s_eq_s''; simpl in H. apply (List_mul a lg ls (lc' ++ lc'')); trivial. rewrite H in P. rewrite ass_app in P. setoid_rewrite <- permut_cons_inside in P; trivial. rewrite ass_app; trivial. rewrite H in P'. rewrite app_comm_cons in P'. rewrite ass_app in P'. setoid_rewrite <- permut_cons_inside in P'. rewrite app_comm_cons; rewrite ass_app; trivial. transitivity s; trivial. symmetry; trivial. Qed. Lemma rpo_antirefl :   forall s, rpo s s -> False. Proof. intro s; pattern s; apply term_rec3_mem; clear s. intros v v_lt_v; inversion v_lt_v. intros f l IHl t_lt_t; inversion t_lt_t as [ f' l' s'' s' s'_mem_l s_le_s' | f' f'' l' l'' f_prec_f H' H1 H2 | f' l' l'' Sf l_lt_l H H1 H2 | f' l' l'' Sf l_lt_l ]; clear t_lt_t; subst. apply (IHl s'); trivial. inversion s_le_s' as [u u' s_eq_s' | u u' s_lt_s']; subst. setoid_rewrite <- (equiv_rpo_equiv_1 _ _ s_eq_s'). apply Subterm with s'; trivial; apply Equiv; apply Eq. apply rpo_trans with (Term f l); trivial. apply Subterm with s'; trivial; apply Equiv; apply Eq. apply prec_antisym with f; trivial. clear H0; induction l as [ | t l]; inversion l_lt_l as [ s t' l' l'' s_lt_t | s t' l' l'' s_eq_t l'_lt_l'']; subst. apply IHl with t; trivial; left; reflexivity. apply IHl0; trivial; intros s s_in_l; apply IHl; right; trivial. clear f Sf; induction l as [ | s l]. inversion l_lt_l as [a lg ls lc l' l'' ls_lt_alg]; subst. assert (L := permut_length H); discriminate. apply IHl0. intros t t_mem_l; apply IHl; right; trivial. apply rpo_mul_remove_equiv_aux with s s; trivial. apply Eq. Qed. Lemma rpo_closure :   forall s t u,   (rpo t s -> rpo u t -> rpo u s) /\   (rpo s t -> rpo t s -> False) /\   (rpo s s -> False) /\   (rpo_eq s t -> rpo_eq t s -> equiv s t). Proof. intros s t u; repeat split. intros; apply (rpo_trans u t s); trivial. intros; apply (rpo_antirefl s); apply rpo_trans with t; trivial. apply rpo_antirefl. intros s_le_t t_le_s; destruct s_le_t as [s t s_eq_t | s t s_lt_t]; trivial. destruct t_le_s as [t s t_eq_s | t s t_lt_s]. apply (equiv_sym _ _ equiv_equiv); trivial. assert False; [idtac | contradiction]. apply (rpo_antirefl s); apply rpo_trans with t; trivial. Qed. ```

## Well-foundedness of rpo.

``` Lemma equiv_acc_rpo :   forall t t', equiv t t' -> Acc rpo t -> Acc rpo t'. Proof. intros t t' t_eq_t' Acc_t; apply Acc_intro. intro s; setoid_rewrite <- (equiv_rpo_equiv_1 _ _ t_eq_t'). inversion Acc_t as [H]; apply (H s); trivial. Qed. Inductive rpo_lex_rest : list term -> list term -> Prop := | Rpo_lex_rest :      forall l l', (forall s, mem s l -> Acc rpo s) -> (forall s, mem s l' -> Acc rpo s) ->      rpo_lex l' l -> rpo_lex_rest l' l. Lemma wf_rpo_lex_rest : well_founded rpo_lex_rest. Proof. unfold well_founded; intro l; pattern l; apply list_rec2; clear l; induction n; intros [ | t l ] L. apply Acc_intro; intros l' H; inversion H as [ k k' Acc_l Acc_l' H' H1 H2]; subst; inversion H'. simpl in L; absurd (S (length l) <= 0); auto with arith. apply Acc_intro; intros l' H; inversion H as [ k k' Acc_l Acc_l' H' H1 H2]; subst; inversion H'. simpl in L; generalize (le_S_n _ _ L); clear L; intro L. assert (H : Acc rpo t -> Acc rpo_lex_rest (t :: l)). intro Acc_t; generalize l L; clear l L; induction Acc_t as [ s Acc_s IHs]. intros l L; assert (Acc_l := IHn _ L); generalize s Acc_s IHs; clear s Acc_s IHs; induction Acc_l as [l' Acc_l' IHl']. intros s Acc_s IHs; apply Acc_intro. intros l'' H; inversion H as [k' k'' Acc_s_l Acc_l'' H']; subst. inversion H' as [u s' k' k'' u_lt_s L' | s' s'' k' k'' s'_eq_s k'_lt_l H1 H2]. subst; apply IHs; trivial; rewrite L'; trivial. subst; apply IHl'. apply Rpo_lex_rest; trivial. intros; apply Acc_s_l; right; trivial. intros; apply Acc_l''; right; trivial. rewrite (rpo_lex_same_length k' l'); trivial. intros u u_lt_s'; apply (Acc_s u); setoid_rewrite <- (equiv_rpo_equiv_1 _ _ s'_eq_s); trivial. intros u u_lt_s' l Ll; apply IHs; trivial; setoid_rewrite <- (equiv_rpo_equiv_1 _ _ s'_eq_s); trivial. apply Acc_intro; intros l' H'; inversion H' as [H1 H2 Acc_t_l]; subst. assert (wf_t : Acc rpo t). apply Acc_t_l; left; reflexivity. apply (Acc_inv (H wf_t)); trivial. Qed. ```
Definition of a finer grain for multiset extension.
``` Inductive rpo_mul_step : list term -> list term -> Prop :=   | List_mul_step :        forall a ls lc l l',         permut l' (ls ++ lc) -> permut l (a :: lc) ->        (forall b, mem b ls -> rpo b a) ->        rpo_mul_step l' l. ```
The plain multiset extension is in the transitive closure of the finer grain extension.
``` Lemma rpo_mul_trans_clos :   inclusion _ rpo_mul (clos_trans _ rpo_mul_step). Proof. unfold inclusion; intros l' l H; inversion H as [a lg ls lc k k' P' P ls_lt_alg]; subst. generalize l' l a ls lc P P' ls_lt_alg; clear l' l a ls lc P P' ls_lt_alg H; induction lg as [ | g lg]; intros l' l a ls lc P P' ls_lt_alg. apply t_step; apply (List_mul_step a ls lc); trivial. intros b b_in_ls; destruct (ls_lt_alg b b_in_ls) as [a' [[a'_eq_a | a'_in_nil] b_lt_a']]. setoid_rewrite <- (equiv_rpo_equiv_1 _ _ a'_eq_a); trivial. contradiction. assert (H: exists ls1, exists ls2,  permut ls (ls1 ++ ls2) /\  (forall b, mem b ls1 -> rpo b g) /\  (forall b, mem b ls2 -> exists a', mem a' (a :: lg) /\ rpo b a')). clear P'; induction ls as [ | s ls]. exists (nil : list term); exists (nil : list term); intuition. contradiction. contradiction. destruct IHls as [ls1 [ls2 [P' [ls1_lt_g ls2_lt_alg]]]]. intros b b_in_ls; apply ls_lt_alg; right; trivial. destruct (ls_lt_alg s) as [a' [[a'_eq_a | [a'_eq_g | a'_in_lg]] b_lt_a']]. left; reflexivity. exists ls1; exists (s :: ls2); repeat split; trivial. setoid_rewrite <- permut_cons_inside; trivial. reflexivity. intros b [b_eq_s | b_in_ls2]. exists a; split. left; reflexivity. setoid_rewrite (equiv_rpo_equiv_2 _ _ b_eq_s). setoid_rewrite <- (equiv_rpo_equiv_1 _ _ a'_eq_a); trivial. apply ls2_lt_alg; trivial. exists (s :: ls1); exists ls2; repeat split; trivial. simpl; setoid_rewrite <- permut_cons; trivial. reflexivity. intros b [b_eq_s | b_in_ls1]. setoid_rewrite (equiv_rpo_equiv_2 _ _ b_eq_s). setoid_rewrite <- (equiv_rpo_equiv_1 _ _ a'_eq_g); trivial. apply ls1_lt_g; trivial. exists ls1; exists (s :: ls2); repeat split; trivial. setoid_rewrite <- permut_cons_inside; trivial. reflexivity. intros b [b_eq_s | b_in_ls2]. exists a'; split. right; trivial. setoid_rewrite (equiv_rpo_equiv_2 _ _ b_eq_s); trivial. apply ls2_lt_alg; trivial. destruct H as [ls1 [ls2 [Pls [ls1_lt_g ls2_lt_alg]]]]. apply t_trans with (g :: ls2 ++ lc). apply t_step; apply (List_mul_step g ls1 (ls2 ++ lc)); auto. setoid_rewrite P'. rewrite ass_app; setoid_rewrite <- permut_app2; trivial. apply (IHlg (g :: ls2 ++ lc) l a ls2 (g :: lc)); trivial. setoid_rewrite P. simpl; setoid_rewrite <- permut_cons. reflexivity. setoid_rewrite <- permut_cons_inside; reflexivity. setoid_rewrite <- permut_cons_inside; reflexivity. Qed. Inductive rpo_mul_rest : list term -> list term -> Prop := | Rpo_mul_rest :      forall l l', (forall s, mem s l -> Acc rpo s) ->                   (forall s, mem s l' -> Acc rpo s) ->      rpo_mul l' l -> rpo_mul_rest l' l. Inductive rpo_mul_step_rest : list term -> list term -> Prop := | Rpo_mul_step_rest :      forall l l', (forall s, mem s l -> Acc rpo s) ->                   (forall s, mem s l' -> Acc rpo s) ->      rpo_mul_step l' l -> rpo_mul_step_rest l' l. Lemma rpo_mul_rest_trans_clos :   inclusion _ rpo_mul_rest (clos_trans _ rpo_mul_step_rest). Proof. unfold inclusion; intros l' l H; inversion H as [k k' Acc_l Acc_l' H' H1 H2 ]; subst. inversion H' as [a lg ls lc k k' P' P ls_lt_alg]; subst. generalize l' l a ls lc P' P ls_lt_alg Acc_l Acc_l'; clear l' l a ls lc P' P ls_lt_alg H Acc_l Acc_l' H'; induction lg as [ | g lg]; intros l' l a ls lc P' P ls_lt_alg Acc_l Acc_l'. apply t_step; apply Rpo_mul_step_rest; trivial; apply (List_mul_step a ls lc); trivial. intros b b_in_ls; destruct (ls_lt_alg b b_in_ls) as [a' [[a'_eq_a | a'_in_nil] b_lt_a']]. setoid_rewrite <- (equiv_rpo_equiv_1 _ _ a'_eq_a); trivial. contradiction. assert (H: exists ls1, exists ls2,  permut ls (ls1 ++ ls2) /\  (forall b, mem b ls1 -> rpo b g) /\  (forall b, mem b ls2 -> exists a', mem a' (a :: lg) /\ rpo b a')). clear P'; induction ls as [ | s ls]. exists (nil : list term); exists (nil : list term); intuition. contradiction. contradiction. destruct IHls as [ls1 [ls2 [P' [ls1_lt_g ls2_lt_alg]]]]. intros b b_in_ls; apply ls_lt_alg; right; trivial. destruct (ls_lt_alg s) as [a' [[a'_eq_a | [a'_eq_g | a'_in_lg]] b_lt_a']]. left; reflexivity. exists ls1; exists (s :: ls2); repeat split; trivial. setoid_rewrite <- permut_cons_inside; trivial. reflexivity. intros b [b_eq_s | b_in_ls2]. exists a; split. left; reflexivity. setoid_rewrite (equiv_rpo_equiv_2 _ _ b_eq_s). setoid_rewrite <- (equiv_rpo_equiv_1 _ _ a'_eq_a); trivial. apply ls2_lt_alg; trivial. exists (s :: ls1); exists ls2; repeat split; trivial. simpl; setoid_rewrite <- permut_cons; trivial. reflexivity. intros b [b_eq_s | b_in_ls1]. setoid_rewrite (equiv_rpo_equiv_2 _ _ b_eq_s). setoid_rewrite <- (equiv_rpo_equiv_1 _ _ a'_eq_g); trivial. apply ls1_lt_g; trivial. exists ls1; exists (s :: ls2); repeat split; trivial. setoid_rewrite <- permut_cons_inside; trivial. reflexivity. intros b [b_eq_s | b_in_ls2]. exists a'; split. right; trivial. setoid_rewrite (equiv_rpo_equiv_2 _ _ b_eq_s); trivial. apply ls2_lt_alg; trivial. destruct H as [ls1 [ls2 [Pls [ls1_lt_g ls2_lt_alg]]]]. apply t_trans with (g :: ls2 ++ lc). apply t_step; apply Rpo_mul_step_rest; trivial. intros s [g_eq_s | s_mem_ls2lc]. apply Acc_l. setoid_rewrite P; right; left; trivial. apply Acc_l'. setoid_rewrite P'; setoid_rewrite <- mem_or_app. setoid_rewrite <- mem_or_app in s_mem_ls2lc. destruct s_mem_ls2lc as [s_mem_ls2 | s_mem_lc]. left; setoid_rewrite Pls; setoid_rewrite <- mem_or_app; right; trivial. right; trivial. apply (List_mul_step g ls1 (ls2 ++ lc)); auto. setoid_rewrite P'; setoid_rewrite Pls; rewrite ass_app; auto. apply (IHlg (g :: ls2 ++ lc) l a ls2 (g :: lc)); trivial. setoid_rewrite <- permut_cons_inside; reflexivity. setoid_rewrite P. setoid_rewrite <- permut_cons. reflexivity. simpl; setoid_rewrite <- permut_cons_inside; reflexivity. intros s [g_eq_s | s_mem_ls2lc]. apply Acc_l. setoid_rewrite P; right; left; trivial. apply Acc_l'. setoid_rewrite P'; setoid_rewrite <- mem_or_app. setoid_rewrite <- mem_or_app in s_mem_ls2lc. destruct s_mem_ls2lc as [s_mem_ls2 | s_mem_lc]. left; setoid_rewrite Pls; setoid_rewrite <- mem_or_app; right; trivial. right; trivial. Qed. ```
Splitting in two disjoint cases.
``` Lemma two_cases_rpo :  forall a m n,  rpo_mul_step n (a :: m) ->  (exists a', exists n', equiv a a' /\ permut n (a' :: n') /\                                                            rpo_mul_step n' m) \/  (exists ls, (forall b, mem b ls -> rpo b a) /\ permut n (ls ++ m)). Proof. intros b m n M; inversion M as [a ls lc l l' P' P ls_lt_a]; subst. assert (b_mem_a_lc : mem b (a :: lc)). setoid_rewrite <- (mem_permut_mem b P); left; reflexivity. simpl in b_mem_a_lc; destruct b_mem_a_lc as [b_eq_a | b_mem_lc]. right; exists ls; repeat split; trivial. intros c c_mem_ls; setoid_rewrite (equiv_rpo_equiv_1 _ _ b_eq_a). apply ls_lt_a; trivial. setoid_rewrite P'; setoid_rewrite <- permut_app1. setoid_rewrite <- permut_cons in P; symmetry; trivial. symmetry; trivial. destruct (mem_split_set _ _ b_mem_lc) as [b' [lc1 [lc2 [b_eq_b' H]]]]; simpl in b_eq_b'; simpl in H. left; exists b'; exists (ls ++ (lc1 ++ lc2)); repeat split; trivial. setoid_rewrite P'; subst lc. rewrite ass_app; apply permut_sym. setoid_rewrite <- permut_cons_inside. reflexivity. rewrite ass_app; auto. apply (List_mul_step a ls (lc1 ++ lc2)); auto. rewrite app_comm_cons. setoid_rewrite (permut_cons_inside m (a :: lc1) lc2 b_eq_b'). setoid_rewrite P. simpl; subst lc; auto. Qed. Lemma list_permut_map_acc :  forall l l', permut l l' ->  Acc rpo_mul_step_rest l -> Acc rpo_mul_step_rest l'. Proof. intros l l' P A1; apply Acc_intro; intros l'' M2. inversion A1 as [H]; apply H; inversion M2 as [k' k'' Acc_l' Acc_l'' H']; subst. inversion H' as [a ls lc k' k'' P'' P' ls_lt_a]; subst. apply Rpo_mul_step_rest; trivial. intros s s_in_l; apply Acc_l'; setoid_rewrite <- (mem_permut_mem s P); trivial. apply (List_mul_step a ls lc); trivial; apply permut_trans with l'; trivial. Qed. ```
Multiset extension of rpo on accessible terms lists is well-founded.
``` Lemma wf_rpo_mul_rest : well_founded rpo_mul_rest. Proof. apply wf_incl with (clos_trans _ rpo_mul_step_rest). unfold inclusion; apply rpo_mul_rest_trans_clos. apply wf_clos_trans. unfold well_founded; intro l; induction l as [ | s l]. apply Acc_intro; intros m H; inversion H as [l l' Acc_l Acc_l' H']; subst; inversion H' as [a ls lc l l' P P']; subst. assert (L := permut_length P'); discriminate. assert (Acc rpo s -> Acc rpo_mul_step_rest (s :: l)). intro Acc_s; generalize l IHl; clear l IHl; pattern s; apply Acc_ind with term rpo; trivial; clear s Acc_s. intros s Acc_s IHs l Acc_l; pattern l; apply Acc_ind with (list term) rpo_mul_step_rest; trivial; clear l Acc_l. intros l Acc_l IHl; apply Acc_intro. intros l' H; inversion H as [s_k k' Acc_s_l Acc_l' H']; subst. destruct (two_cases_rpo s l l' H') as [[s' [n' [s_eq_s' [P H'']]]] | [ls [ls_lt_s P]]]. apply (list_permut_map_acc (s :: n')). setoid_rewrite P; setoid_rewrite <- permut_cons; auto. apply Acc_intro; intros l'' l''_lt_s'_n; apply Acc_inv with (s :: n'). apply IHl; apply Rpo_mul_step_rest; trivial. intros; apply Acc_s_l; right; trivial. intros s'' s''_in_n'; apply Acc_l'; setoid_rewrite (mem_permut_mem s'' P); right; trivial. trivial. apply (list_permut_map_acc (ls ++ l)). apply permut_sym; trivial. clear P; induction ls as [ | b ls]. simpl; apply Acc_intro; trivial. simpl; apply IHs. apply ls_lt_s; left; reflexivity. apply IHls; intros; apply ls_lt_s; right; trivial. apply Acc_intro. intros l' H'. apply Acc_inv with (s :: l); trivial. inversion H' as [k k' Acc_s_l Acc_l']; subst; apply H; apply Acc_s_l; left; reflexivity. Qed. Inductive rpo_rest : (symbol * list term) -> (symbol * list term) -> Prop :=  | Top_gt_rest :        forall f g l l', prec g f ->        (forall s, mem s l -> Acc rpo s) -> (forall s, mem s l' -> Acc rpo s) ->        rpo_rest (g, l') (f, l)   | Top_eq_lex_rest :         forall f l l', status f = Lex -> rpo_lex l' l ->         (forall s, mem s l -> Acc rpo s) -> (forall s, mem s l' -> Acc rpo s) ->         rpo_rest (f, l') (f, l)   | Top_eq_mul_rest :         forall f l l', status f = Mul -> rpo_mul l' l ->         (forall s, mem s l -> Acc rpo s) -> (forall s, mem s l' -> Acc rpo s) ->         rpo_rest (f, l') (f, l). Lemma wf_rpo_rest : well_founded prec -> well_founded rpo_rest. Proof. intros wf_prec; unfold well_founded; intros [f l]; generalize l; clear l; pattern f; apply (well_founded_induction_type wf_prec); clear f. intros f IHf l; assert (Sf : forall f', f' = f -> status f' = status f). intros; subst; trivial. destruct (status f); generalize (Sf _ (refl_equal _)); clear Sf; intro Sf. pattern l; apply (well_founded_induction_type wf_rpo_lex_rest); clear l. intros l IHl; apply Acc_intro; intros [g l'] H. inversion H as [ f' g' k k' g_prec_f Acc_l Acc_l' | f' k k' Sf' H' Acc_l Acc_l' | f' k k' Sf' H' Acc_l Acc_l' ]; subst. apply IHf; trivial. apply IHl; apply Rpo_lex_rest; trivial. absurd (Lex = Mul); [discriminate | apply trans_eq with (status f); auto]. pattern l; apply (well_founded_induction_type wf_rpo_mul_rest); clear l. intros l IHl; apply Acc_intro; intros [g l'] H; inversion H as [ f' g' k k' g_prec_f Acc_l Acc_l' | f' k k' Sf' H' Acc_l Acc_l' | f' k k' Sf' H' Acc_l Acc_l' ]; subst. apply IHf; trivial. absurd (Lex = Mul); [discriminate | apply trans_eq with (status f); auto]. apply IHl; apply Rpo_mul_rest; trivial. Qed. Lemma acc_build :   well_founded prec -> forall f_l,   match f_l with (f, l) =>   (forall t, mem t l -> Acc rpo t) -> Acc rpo (Term f l)   end. Proof. intros wf_prec f_l; pattern f_l; apply (well_founded_induction_type (wf_rpo_rest wf_prec)); clear f_l. intros [f l] IH Acc_l; apply Acc_intro; intros s; pattern s; apply term_rec3_mem; clear s. intros v _; apply Acc_intro. intros t t_lt_v; inversion t_lt_v. intros g k IHl gk_lt_fl; inversion gk_lt_fl as [ f' l' s' t t_in_l H' | f' g' k' l' g_prec_f | f' k' l' Sf H' H'' | f' k' l' Sf H']; subst. assert (Acc_t := Acc_l _ t_in_l). subst; inversion H' as [s' t' s_eq_t | s' t' s_lt_t ]; subst s' t'; [idtac | apply Acc_inv with t; trivial ]. apply Acc_intro; intro u. setoid_rewrite (equiv_rpo_equiv_1 (Term g k) t); trivial; intro; apply Acc_inv with t; trivial. assert (Acc_k : forall s, mem s k -> Acc rpo s). intros s s_mem_k; apply IHl; trivial. apply H0; trivial. apply (IH (g,k)); trivial. apply Top_gt_rest; trivial. assert (Acc_k : forall s, mem s k -> Acc rpo s). intros s s_mem_k; apply IHl; trivial. apply H''; trivial. apply (IH (f,k)); trivial. apply Top_eq_lex_rest; trivial. assert (Acc_k : forall s, mem s k -> Acc rpo s). intros s s_mem_k; apply IHl; trivial. apply rpo_trans with (Term f k); trivial; apply Subterm with s; trivial; apply Equiv; apply Eq. apply (IH (f,k)); trivial. apply Top_eq_mul_rest; trivial. Qed. ```

## Main theorem: when the precedence is well-founded, so is the rpo.

``` Lemma wf_rpo : well_founded prec -> well_founded rpo. Proof. intro wf_prec; unfold well_founded; intro t; pattern t; apply term_rec3_mem; clear t. intro v; apply Acc_intro; intros s s_lt_t; inversion s_lt_t. intros f l Acc_l; apply (acc_build wf_prec (f,l)); trivial. Qed. ```

## RPO is compatible with the instanciation by a substitution.

``` Lemma equiv_subst :   forall s t, equiv s t ->   forall sigma, equiv (apply_subst sigma s) (apply_subst sigma t). Proof. intros s t; generalize s; clear s. pattern t; apply term_rec3_mem; clear t. intros v s v_eq_s; inversion v_eq_s; subst; intro sigma; apply Eq. intros f l IHl s fl_eq_s sigma; inversion fl_eq_s as [ s' | f' l1 l2 Sf l1_eq_l2 | f' l1 l2 Sf P ]; subst. apply Eq. simpl; apply Eq_lex; trivial. generalize l1 l1_eq_l2; clear fl_eq_s l1 l1_eq_l2; induction l as [ | s l]; intros l1 l1_eq_l2; inversion l1_eq_l2 as [ | s1 s' l1' l' s1_eq_s' l1'_eq_l']; subst. simpl; apply Eq_list_nil. simpl; apply Eq_list_cons. apply IHl; trivial; left; reflexivity. apply IHl0; trivial. intros t t_in_l; apply IHl; right; trivial. simpl; apply Eq_mul; trivial. apply (permut_map (A := term) (B := term) (A' := term) (B' := term) (R := equiv)). intros a1 a2 a1_in_l1 _ a1_eq_a2; symmetry; apply IHl. setoid_rewrite <- (mem_permut_mem a1 P). apply in_impl_mem; trivial. symmetry; trivial. trivial. Qed. Lemma rpo_subst :   forall s t, rpo s t ->   forall sigma, rpo (apply_subst sigma s) (apply_subst sigma t). Proof. cut (forall p, match p with             (s,t) => rpo s t ->               forall sigma, rpo (apply_subst sigma s) (apply_subst sigma t)         end). intros H s t s_lt_t sigma; apply (H (s,t)); trivial. intro p; pattern p; refine (well_founded_ind wf_size2 _ _ _); clear p. intros [s t] IH s_lt_t sigma. inversion s_lt_t as [ f l s' t' t'_mem_l R' | f g l l' R' R'' | f l l' f_lex Rlex R' H2 H3 | f l l' f_mul Rmul R' H2 ]; subst. simpl; apply Subterm with (apply_subst sigma t'). destruct (mem_split_set _ _ t'_mem_l) as [t'' [l1 [l2 [t'_eq_t'' H]]]]; simpl in t'_eq_t''; simpl in H; subst l. rewrite map_app; setoid_rewrite <- mem_or_app. right; left; apply equiv_subst; trivial. inversion R' as [ s' R'' | s' t'' R'' ]; subst. apply Equiv; apply equiv_subst; trivial. apply Lt; apply (IH (s,t')); trivial. apply size2_lex2_mem; trivial. simpl; apply Top_gt; trivial. intros s' s'_mem_l'_sigma; destruct (mem_split_set _ _ s'_mem_l'_sigma) as [s'' [l1 [l2 [s'_eq_s'' H]]]]; simpl in s'_eq_s''; simpl in H. setoid_rewrite (equiv_rpo_equiv_2 _ _ s'_eq_s''). assert (s''_in_l'_sigma : In s'' (map (apply_subst sigma) l')). rewrite H; apply in_or_app; right; left; trivial. setoid_rewrite in_map_iff in s''_in_l'_sigma. destruct s''_in_l'_sigma as [u [s_eq_u_sigma u_in_l']]. subst s''; replace (Term f (map (apply_subst sigma) l)) with               (apply_subst sigma (Term f l)); trivial. apply (IH (u, Term f l)). apply size2_lex1; trivial. apply rpo_trans with (Term g l'); trivial. apply Subterm with u. apply in_impl_mem; trivial. apply Equiv; apply Eq. simpl; apply Top_eq_lex; trivial. generalize l Rlex IH; clear l s_lt_t Rlex R' IH; induction l' as [ | s' l' ]; intros l Rlex IH; inversion Rlex as [s'' t' k k' s'_lt_t' L | s'' t' k k' s'_eq_t' k_lt_k']; subst; simpl. apply List_gt. apply (IH (s',t')); trivial. apply size2_lex1; left; trivial. do 2 rewrite length_map; trivial. apply List_eq. apply equiv_subst; trivial. apply IHl'; trivial. intros [s t] S s_lt_t tau; apply (IH (s,t)); trivial. apply o_size2_trans with (Term f l', Term f k'); trivial. apply size2_lex1_bis. intros s' s'_mem_l'_sigma; destruct (mem_split_set _ _ s'_mem_l'_sigma) as [s'' [l1 [l2 [s'_eq_s'' H]]]]; simpl in s'_eq_s''; simpl in H. setoid_rewrite (equiv_rpo_equiv_2 _ _ s'_eq_s''). assert (s''_in_l'_sigma : In s'' (map (apply_subst sigma) l')). rewrite H; apply in_or_app; right; left; trivial. setoid_rewrite in_map_iff in s''_in_l'_sigma. destruct s''_in_l'_sigma as [u [s_eq_u_sigma u_in_l']]. subst s''; replace (Term f (map (apply_subst sigma) l)) with               (apply_subst sigma (Term f l)); trivial. apply (IH (u, Term f l)). apply size2_lex1; trivial. apply rpo_trans with (Term f l'); trivial. apply Subterm with u. apply in_impl_mem; trivial. apply Equiv; apply Eq. simpl; apply Top_eq_mul; trivial; inversion Rmul as [ a lg ls lc l0 k0 Pk Pl ls_lt_alg]; subst. apply (List_mul (apply_subst sigma a) (map (apply_subst sigma) lg) (map (apply_subst sigma) ls) (map (apply_subst sigma) lc)). rewrite <- map_app; apply permut_map with equiv; trivial. intros b b' _ _ b_eq_b'; apply equiv_subst; trivial. rewrite <- map_app. refine (@permut_map term term term term equiv                     equiv (apply_subst sigma) _ _ (a :: lg ++ lc) _ _); trivial. intros b b' b_in_l _ b_eq_b'; apply equiv_subst; trivial. intros b b_mem_ls_sigma; destruct (mem_split_set _ _ b_mem_ls_sigma) as [b' [ls1 [ls2 [b_eq_b' H]]]]; simpl in b_eq_b'; simpl in H. assert (b'_in_ls_sigma : In b' (map (apply_subst sigma) ls)). rewrite H; apply in_or_app; right; left; trivial. setoid_rewrite in_map_iff in b'_in_ls_sigma. destruct b'_in_ls_sigma as [b'' [b''_sigma_eq_b' b''_in_ls]]. destruct (ls_lt_alg b'') as [a' [a'_mem_alg b''_lt_a']]. apply in_impl_mem; trivial. destruct (mem_split_set _ _ a'_mem_alg) as [a'' [alg' [alg'' [a'_eq_a'' H']]]]; simpl in a'_eq_a''; simpl in H'. exists (apply_subst sigma a''); split; trivial. apply in_impl_mem. setoid_rewrite (in_map_iff (apply_subst sigma) (a :: lg)). exists a''; split; trivial. rewrite H'; apply in_or_app; right; left; trivial. setoid_rewrite (equiv_rpo_equiv_2 _ _ b_eq_b'). subst b'; apply (IH (b'',a'')). apply size2_lex1_mem. setoid_rewrite Pk; setoid_rewrite <- mem_or_app; left; apply in_impl_mem; trivial. setoid_rewrite <- (equiv_rpo_equiv_1 _ _ a'_eq_a''); trivial. Qed. ```

## RPO is compatible with adding context.

``` Lemma equiv_add_context :  forall p ctx s t, equiv s t -> is_a_pos ctx p = true ->   equiv (replace_at_pos ctx s p) (replace_at_pos ctx t p). Proof. intro p; induction p as [ | i p ]; intros ctx s t R H; trivial; destruct ctx as [ v | f l ]. discriminate. assert (Status : forall g, g = f -> status g = status f). intros; subst; trivial. do 2 (rewrite replace_at_pos_unfold); destruct (status f); generalize (Status f (refl_equal _)); clear Status; intro Status. apply Eq_lex; trivial. generalize i H; clear i H; induction l as [ | u l]; intros i H; simpl. apply Eq_list_nil. destruct i as [ | i]. apply Eq_list_cons. simpl in H; apply IHp; trivial. generalize l; intro l'; induction l' as [ | u' l']. apply Eq_list_nil. apply Eq_list_cons; trivial; reflexivity. apply Eq_list_cons. reflexivity. apply IHl; trivial. apply Eq_mul; trivial. generalize i H; clear i H; induction l as [ | u l]; intros i H; simpl; auto. destruct i as [ | i]. setoid_rewrite <- permut_cons. simpl in H; apply IHp; trivial. reflexivity. setoid_rewrite <- permut_cons. reflexivity. apply IHl; trivial. Qed. Lemma rpo_add_context :  forall p ctx s t, rpo s t -> is_a_pos ctx p = true ->   rpo (replace_at_pos ctx s p) (replace_at_pos ctx t p). Proof. intro p; induction p as [ | i p ]; intros ctx s t R H; trivial; destruct ctx as [ v | f l ]. discriminate. assert (Status : forall g, g = f -> status g = status f). intros; subst; trivial. do 2 (rewrite replace_at_pos_unfold); destruct (status f); generalize (Status f (refl_equal _)); clear Status; intro Status. apply Top_eq_lex; trivial. generalize i H; clear i H; induction l as [ | u l]; intros i H; simpl. simpl in H; destruct i; discriminate. destruct i as [ | i]. apply List_gt; trivial. simpl in H; apply IHp; trivial. apply List_eq. reflexivity. apply IHl; trivial. intros s' s'_mem_ls; assert (H' : exists s'', rpo_eq s' s'' /\ mem s'' (replace_at_pos_list l t i p)). generalize i H s' s'_mem_ls; clear i H s' s'_mem_ls; induction l as [ | u l]; intros i H; simpl. intros; contradiction. destruct i as [ | i]. intros s' [s'_eq_s'' | s'_mem_l]. exists (replace_at_pos u t p); split. apply Lt; setoid_rewrite (equiv_rpo_equiv_2 _ _ s'_eq_s''). apply IHp; trivial. left; reflexivity. exists s'; split. apply Equiv; apply Eq. right; trivial. intros s' [s'_eq_u | s'_mem_l]. exists u; split. apply Equiv; trivial. left; reflexivity. simpl in IHl; simpl in H. destruct (IHl i H s' s'_mem_l) as [s'' [s'_le_s'' s''_mem_l']]. exists s''; split; trivial. right; trivial. destruct H' as [s'' [s'_le_s'' s''_mem_l']]. apply Subterm with s''; trivial. apply Top_eq_mul; trivial. generalize i H; clear i H; induction l as [ | u l]; intros i H; simpl. simpl in H; destruct i; discriminate. destruct i as [ | i]. apply (List_mul (replace_at_pos u t p) nil (replace_at_pos u s p :: nil) l); auto. intros b [b_eq_s' | b_mem_nil]. exists (replace_at_pos u t p); split. left; reflexivity. setoid_rewrite (equiv_rpo_equiv_2 _ _ b_eq_s'). apply IHp; trivial. contradiction. simpl in IHl; simpl in H; assert (H' := IHl i H). inversion H' as [a lg ls lc l' l'' ls_lt_alg P1 P2]; subst. apply (List_mul a lg ls (u :: lc)); trivial. setoid_rewrite <- permut_cons_inside; trivial; reflexivity. rewrite app_comm_cons. setoid_rewrite <- permut_cons_inside; trivial; reflexivity. Qed. Function remove_equiv (t : term) (l : list term) {struct l} : option (list term) :=   match l with      | nil => @None _      | a :: l =>          if equiv_dec t a          then Some l          else             match remove_equiv t l with             | None => @ None _             | Some l' => Some (a :: l')             end     end. Function remove_equiv_list (l1 l2 : list term) {struct l1} : (list term) * (list term) :=     match l1, l2 with     | _, nil => (l1,l2)     | nil, _ => (l1,l2)     | a1 :: l1, l2 =>           match remove_equiv a1 l2 with           | Some l2' => remove_equiv_list l1 l2'           | None =>                match remove_equiv_list l1 l2 with                       | (l1',l2') => (a1 :: l1', l2')                end           end    end. Lemma remove_equiv_is_sound_some :   forall t l l', remove_equiv t l = Some l' ->     {t' | equiv t t' /\ permut l (t' :: l')}. Proof. intros t l; induction l as [ | a l]; intros l' R; simpl in R. discriminate. destruct (equiv_dec t a) as [t_eq_a | t_diff_a]. injection R; intro; subst l'; clear R; exists a; split; auto. destruct (remove_equiv t l) as [ l'' | ]. injection R; intro; subst l'; clear R. destruct (IHl l'' (refl_equal _)) as [t' [t_eq_t' P]]. exists t'; split; trivial. setoid_rewrite <- (@permut_cons_inside a a l (t' :: nil) l''); trivial. reflexivity. discriminate. Qed. Lemma remove_equiv_is_sound_none :   forall t l, remove_equiv t l = None -> forall t', mem t' l -> ~ (equiv t t'). Proof. intros t l; functional induction (remove_equiv t l) as   [ | H1 a l t' t_eq_a _ | H1 a l t' t_diff_a _ IH H | H1 a l t' t_diff_a _ IH l' H ]. simpl; intros; contradiction. intros; discriminate. intros _; rewrite H in IH; intros t' [a_eq_t' | t'_mem_l]. intro t_eq_t'; apply t_diff_a. transitivity t'; trivial. apply IH; trivial. intros; discriminate. Qed. Lemma remove_equiv_list_is_sound :   forall l1 l2,     match remove_equiv_list l1 l2 with          | (l1',l2') =>              {lc | permut l1 (l1' ++ lc) /\ permut l2 (l2' ++ lc) /\                            (forall t1 t2, mem t1 l1' -> mem t2 l2' -> ~ equiv t1 t2)}    end. Proof. intros l1 l2; functional induction (remove_equiv_list l1 l2) as [ l1 | H1 l2 H2 H3 H4 H' | H1 l2 t1 l1 H2 H3 H4 _ l2' H IH | H1 l2 t1 l1 H2 H3 H4 H' H IH l1' l2' R]. exists (@nil term); simpl; repeat split; auto. rewrite <- app_nil_end; auto. destruct l2 as [ | t2 l2]. contradiction. exists (@nil term); simpl; repeat split; auto. rewrite <- app_nil_end; auto. destruct (remove_equiv_is_sound_some t1 l2 l2' H) as [t2 [t1_eq_t2 P2]]. destruct (remove_equiv_list l1 l2') as [l1'' l2'']. destruct IH as [lc [P1 [P2' D]]]. exists (t1 :: lc); repeat split; auto. setoid_rewrite <- permut_cons_inside; trivial. reflexivity. setoid_rewrite P2; setoid_rewrite <- permut_cons_inside; trivial. symmetry; trivial. rewrite R in IH. destruct IH as [lc [P1 [P2 D]]]. exists lc; repeat split; auto. simpl; setoid_rewrite <- permut_cons; trivial. reflexivity. intros u1 u2 [t1_eq_u1 | u1_mem_l1'] u2_mem_u2'. assert (H'' := remove_equiv_is_sound_none t1 l2 H). intro u1_eq_u2; apply (H'' u2). setoid_rewrite P2; setoid_rewrite <- mem_or_app; left; trivial. transitivity u1; trivial. symmetry; trivial. apply D; trivial. Qed. Lemma rpo_dec : forall t1 t2, {rpo t1 t2}+{~rpo t1 t2}. Proof. cut (forall p, match p with (t2,t1) =>                               {rpo t1 t2}+{~rpo t1 t2}                  end). intros H t1 t2; apply (H (t2,t1)). intro p; pattern p; refine (well_founded_induction wf_size2 _ _ _); clear p. intros [[v | f l] t1] IH. right; intro t1_lt_t2; inversion t1_lt_t2. assert (H : {t | mem t l /\ rpo_eq t1 t}+{~exists t, mem t l /\ rpo_eq t1 t}). induction l as [ | s l]. right; intros [t [t_mem_nil _]]; contradiction. destruct (equiv_dec t1 s) as [t1_eq_s | t1_diff_s]. left; exists s; split. left; reflexivity. apply Equiv; trivial. destruct (IH (s,t1)) as [t1_lt_s | not_t1_lt_s]. apply size2_lex1; left; trivial. left; exists s; split. left; reflexivity. apply Lt; trivial. destruct IHl as [Ok | Ko]. intros [t2 t1'] H; apply (IH (t2,t1')). apply o_size2_trans with (Term f l, t1); trivial. apply size2_lex1_bis. destruct Ok as [t [t_mem_l t1_le_t]]. left; exists t; split; trivial. right; trivial. right; intros [t [[s_eq_t | t_mem_l] t1_le_t]]. destruct t1_le_t. apply t1_diff_s; transitivity t'; trivial; symmetry; trivial. apply not_t1_lt_s; setoid_rewrite <- (equiv_rpo_equiv_1 _ _ s_eq_t); trivial. apply Ko; exists t; split; trivial. destruct H as [[t [t_mem_l t1_le_t]] | H]. left; apply Subterm with t; trivial. destruct t1 as [v | g k]. right; intro v_lt_fl; inversion v_lt_fl; subst. apply H; exists s; split; trivial. destruct (F.Symb.eq_dec g f) as [g_eq_f | g_diff_f]. assert (Sf := f_equal (fun h => status h) g_eq_f); simpl in Sf. destruct (status f); subst g. assert (H' : {rpo_lex k l}+{~rpo_lex k l}). generalize k IH; clear k IH H; induction l as [ | t l]; intros k IH. right; intro k_lt_nil; inversion k_lt_nil. destruct k as [ | s k]. right; intro nil_lt_tl; inversion nil_lt_tl. destruct (IH (t,s)) as [s_lt_t | not_s_lt_t]. apply size2_lex1; left; trivial. destruct (eq_nat_dec (length k) (length l)) as [L | L]. left; apply List_gt; trivial. right; intro sk_lt_tl; apply L; assert (L' := rpo_lex_same_length _ _ sk_lt_tl); simpl in L'; injection L'; trivial. destruct (equiv_dec s t) as [s_eq_t | s_diff_t]. destruct (IHl k) as [k_lt_l | not_k_lt_l]. intros [t2 t1] H; apply (IH (t2,t1)). apply o_size2_trans with (Term f l, Term f k); trivial. apply size2_lex1_bis. left; apply List_eq; trivial. right; intro sk_lt_tl; inversion sk_lt_tl; subst. absurd (rpo s t); trivial. absurd (rpo_lex k l); trivial. right; intro sk_lt_tl; inversion sk_lt_tl; subst. absurd (rpo s t); trivial. absurd (equiv s t); trivial. destruct H' as [k_lt_l | not_k_lt_l]. assert (H'' : {forall s, mem s k -> rpo s (Term f l)}+{~(forall s, mem s k -> rpo s (Term f l))}). clear k_lt_l H; induction k as [ | s k]. left; intros s s_mem_nil; contradiction. destruct (IH (Term f l, s)) as [s_lt_fl | not_s_lt_fl]. apply size2_lex2; left; trivial. destruct IHk as [Ok | Ko]. intros [t2 t1] H'; apply (IH (t2,t1)). apply o_size2_trans with (Term f l, Term f k); trivial. apply size2_lex2_bis. left; intros s' [s_eq_s' | s'_mem_k]. setoid_rewrite (equiv_rpo_equiv_2 _ _ s_eq_s'); trivial. apply Ok; trivial. right; intro H; apply Ko. intros s' s'_mem_k; apply H; right; trivial. right; intro H; apply not_s_lt_fl; apply H; left; reflexivity. destruct H'' as [Ok | Ko]. left; apply Top_eq_lex; trivial. right; intro fk_lt_fl; inversion fk_lt_fl; subst. apply Ko; intros s' s'_mem_k; apply rpo_trans with (Term f k); trivial. apply Subterm with s'; trivial. apply Equiv; reflexivity. apply (prec_antisym f); trivial. apply Ko; trivial. rewrite H3 in Sf; discriminate. right ; intro fk_lt_fl; inversion fk_lt_fl; subst. apply H; exists s; split; trivial. apply (prec_antisym f); trivial. apply not_k_lt_l; trivial. rewrite H3 in Sf; discriminate. assert (H' := remove_equiv_list_is_sound k l). destruct (remove_equiv_list k l) as [k' l']; destruct H' as [lc [Pk [Pl D]]]. assert (Rem : rpo_mul k l -> rpo_mul k' l'). generalize l k l' k' Pk Pl; clear l k l' k' Pk Pl D IH H. induction lc as [ | c lc]; intros l k l' k' Pk Pl k_lt_l. inversion k_lt_l as [a lg ls lc' k'' l'' Rk Rl ls_lt_alg]; subst. apply (List_mul a lg ls lc'); trivial. transitivity k; trivial; symmetry; rewrite <- app_nil_end in Pk; trivial. transitivity l; trivial; symmetry; rewrite <- app_nil_end in Pl; trivial. assert (H := IHlc l k (l' ++ c :: nil) (k' ++ c :: nil)). do 2 rewrite <- ass_app in H; simpl in H. generalize (H Pk Pl k_lt_l); clear H; intro H. apply (rpo_mul_remove_equiv_aux k' l' c c). intros t _; apply rpo_antirefl. reflexivity. inversion H as [a lg ls lc' k'' l'' Rk Rl ls_lt_alg]; subst. apply (List_mul a lg ls lc'); trivial. setoid_rewrite <- Rk; setoid_rewrite <- permut_cons_inside. reflexivity. rewrite <- app_nil_end; auto. setoid_rewrite <- Rl; setoid_rewrite <- permut_cons_inside. reflexivity. rewrite <- app_nil_end; auto. assert (H' : {forall u, mem u k' -> exists v, mem v l' /\ rpo u v} +                  {~ forall u, mem u k' -> exists v, mem v l' /\ rpo u v}). assert (IH' : forall u v, mem u k' -> mem v l' -> {rpo u v}+{~rpo u v}). intros u v u_mem_k' v_mem_l'; apply (IH (v,u)). apply size2_lex1_mem. setoid_rewrite Pl; setoid_rewrite <- mem_or_app; left; trivial. generalize l' IH'; clear l k IH H l' lc Pk Pl D IH' Rem. induction k' as [ | u' k']; intros l' IH'. left; intros; contradiction. assert (H : {v | mem v l' /\ rpo u' v}+{forall v, mem v l' -> ~rpo u' v}). assert (IH'' : forall v, mem v l' -> {rpo u' v}+{~rpo u' v}). intros v v_mem_l'; apply (IH' u' v); trivial. left; reflexivity. clear IHk' IH'; induction l' as [ | v' l']. right; intros; contradiction. destruct IHl' as [Ok | Ko]. intros; apply IH''; right; trivial. destruct Ok as [v [v_mem_l' u'_lt_v]]; left; exists v; split; trivial. right; trivial. destruct (IH'' v') as [Ok' | Ko']. left; reflexivity. left; exists v'; split; trivial. left; reflexivity. right; intros v [v'_eq_v | v_mem_l']. intros u'_lt_v; apply Ko'. setoid_rewrite <- (equiv_rpo_equiv_1 _ _ v'_eq_v); trivial. apply Ko; trivial. destruct H as [[v [v_mem_l' u'_lt_v]] | Ko]. destruct (IHk' l') as [Ok' | Ko']. intros u v' u_mem_k' v'_mem_l'; apply IH'; trivial; right; trivial. left; intros u [u'_eq_u | u_mem_k']. exists v; split; trivial. setoid_rewrite (equiv_rpo_equiv_2 _ _ u'_eq_u); trivial. apply Ok'; trivial. right; intro H; apply Ko'. intros u u_mem_k'; apply H; right; trivial. right; intro H. destruct (H u') as [v [v_mem_l' u'_lt_v]]. left; reflexivity. apply (Ko v); trivial. destruct l' as [ | v' l']. right; intro fk_lt_fl. inversion fk_lt_fl as [f' l' t'' t' t'_mem_l fk_le_t' | f' f'' k'' l'' f_prec_f k''_lt_fl | f' k'' l'' Sf' k''_lt_l'' l'_lt_t | f' k'' l'' Sf' k_lt_l ]; subst. apply H; exists t'; split; trivial. apply (prec_antisym f f_prec_f). rewrite Sf in Sf'; discriminate. assert (k'_lt_nil := Rem k_lt_l). inversion k'_lt_nil as [a lg ls lc' k'' l'' Rk Rl ls_lt_alg]; subst. assert (L := permut_length Rl); discriminate. destruct H' as [Ok | Ko]. left; apply Top_eq_mul; trivial. apply (List_mul v' l' k' lc); trivial. right; intro fk_lt_fl. inversion fk_lt_fl as [f' l'' t'' t' t'_mem_l fk_le_t' | f' f'' k'' l'' f_prec_f k''_lt_fl | f' k'' l'' Sf' k''_lt_l'' l'_lt_t | f' k'' l'' Sf' k_lt_l ]; subst. setoid_rewrite Pl in t'_mem_l; setoid_rewrite <- mem_or_app in t'_mem_l. destruct t'_mem_l as [t'_mem_vl' | t'_mem_lc]. apply Ko; intros u u_mem_k'; exists t'; split; trivial. inversion fk_le_t'; subst. setoid_rewrite <- (equiv_rpo_equiv_1 (Term f k) t'); trivial. apply Subterm with u. setoid_rewrite Pk; setoid_rewrite <- mem_or_app; left; trivial. apply Equiv; apply Eq. apply rpo_trans with (Term f k); trivial. apply Subterm with u. setoid_rewrite Pk; setoid_rewrite <- mem_or_app; left; trivial. apply Equiv; apply Eq. apply (rpo_antirefl (Term f k)). inversion fk_le_t'; subst. setoid_rewrite (equiv_rpo_equiv_2 (Term f k) t'); trivial. apply Subterm with t'. setoid_rewrite Pk; setoid_rewrite <- mem_or_app; right; trivial. apply Equiv; apply Eq. apply rpo_trans with t'; trivial. apply Subterm with t'. setoid_rewrite Pk; setoid_rewrite <- mem_or_app; right; trivial. apply Equiv; apply Eq. apply (prec_antisym f); trivial. rewrite Sf in Sf'; discriminate. assert (k'_lt_vl' := Rem k_lt_l). apply Ko. inversion k'_lt_vl' as [a lg ls lc' k'' l'' Rk Rl ls_lt_alg]; subst. intro u; setoid_rewrite Rk; setoid_rewrite <- mem_or_app. intros [u_mem_ls | u_mem_lc']. destruct (ls_lt_alg _ u_mem_ls) as [a' [a'_mem_alg u_lt_a']]; exists a'; split; trivial. setoid_rewrite Rl; rewrite app_comm_cons; setoid_rewrite <- mem_or_app; left; trivial. assert False. apply (D u u). setoid_rewrite Rk; setoid_rewrite <- mem_or_app; right; trivial. setoid_rewrite Rl; rewrite app_comm_cons; setoid_rewrite <- mem_or_app; right; trivial. reflexivity. contradiction. destruct (prec_dec g f) as [g_prec_f | not_g_prec_f]. assert (H' : {forall t, mem t k -> rpo t (Term f l)}+{~forall t, mem t k -> rpo t (Term f l)}). clear H; induction k as [ | s k]. left; intros; contradiction. destruct (IH (Term f l,s)) as [s_lt_fl | not_s_lt_fl]. apply size2_lex2; left; trivial. destruct IHk as [Ok | Ko]. intros [t2 t1] St; apply (IH (t2,t1)). apply o_size2_trans with (Term f l, Term g k); trivial. apply size2_lex2_bis. left; intros t [t_eq_s | t_mem_k]. setoid_rewrite (equiv_rpo_equiv_2 _ _ t_eq_s); trivial. apply Ok; trivial. right; intro sk_lt_fl; apply Ko; intros; apply sk_lt_fl; right; trivial. right; intro sk_lt_fl; apply not_s_lt_fl; intros; apply sk_lt_fl; left; reflexivity. destruct H' as [Ok | Ko]. left; apply Top_gt; trivial. right; intro gk_lt_fl; inversion gk_lt_fl as [f' l'' t'' t' t'_mem_l fk_le_t' | f' f'' k'' l'' f_prec_f k''_lt_fl | f' k'' l'' Sf' k''_lt_l'' l'_lt_t | f' k'' l'' Sf' k_lt_l ]; subst. apply H; exists t'; split; trivial. apply Ko; trivial. apply (prec_antisym f); trivial. apply (prec_antisym f); trivial. right; intro gk_lt_fl; inversion gk_lt_fl as [f' l'' t'' t' t'_mem_l fk_le_t' | f' f'' k'' l'' f_prec_f k''_lt_fl | f' k'' l'' Sf' k''_lt_l'' l'_lt_t | f' k'' l'' Sf' k_lt_l ]; subst. apply H; exists t'; split; trivial. absurd (prec g f); trivial. absurd (f=f); trivial. absurd (f=f); trivial. Defined. Function var_in_term_list (x : variable) (l : list term) { measure (list_size size) l } : bool :=   match l with     | nil => false     | (Var y) :: l => if (X.eq_dec x y) then true else (var_in_term_list x l)     | (Term _ ll) :: l => Bool.orb (var_in_term_list x ll) (var_in_term_list x l) end. Proof. intros x t_l t l t_l_eq_t_l y t_eq_y x_eq_y _; subst; simpl; auto with arith. intros _ t_l t l t_l_eq_t_l f ll t_eq_f_ll; subst; simpl; auto with arith. intros _ t_l t l t_l_eq_t_l f ll t_eq_f_ll; subst; apply lt_le_trans with (size (Term f ll)). rewrite size_unfold; simpl; auto with arith. simpl; auto with arith. Defined. Lemma trans_clos_subterm_rpo:   forall s t, trans_clos direct_subterm s t -> rpo s t. Proof. intros s t H; induction H as [ s [ v | f l ] H | s t u H1 H2]. inversion H. apply (Subterm f l s s); trivial. simpl in H; apply in_impl_mem; trivial. apply Equiv; apply Eq. apply (rpo_subterm u t); trivial. Qed. Definition prec_eval f1 f2 :=   if (F.Symb.eq_dec f1 f2)   then Equivalent   else      if prec_dec f1 f2 then Less_than      else         if prec_dec f2 f1 then Greater_than         else Uncomparable. Lemma prec_eval_is_sound :   forall f1 f2,   match prec_eval f1 f2 with   | Equivalent => f1 = f2   | Less_than => prec f1 f2   | Greater_than => prec f2 f1   | Uncomparable => f1 <> f2 /\ ~prec f1 f2 /\ ~prec f2 f1   end. Proof. intros f1 f2; unfold prec_eval; destruct (F.Symb.eq_dec f1 f2) as [f1_eq_f2 | f1_diff_f2]; trivial. destruct (prec_dec f1 f2) as [f1_lt_f2 | not_f1_lt_f2]; trivial. destruct (prec_dec f2 f1) as [f2_lt_f1 | not_f2_lt_f1]; trivial. repeat split; trivial. Qed. Inductive result (A : Set) : Set :=   | Not_found : result A   | Not_finished : result A   | Found : A -> result A. Record rpo_inf : Set :=   { rpo_l : list (term*term);     rpo_eq_l : list (term*term);     equiv_l : list (term*term);     rpo_l_valid : forall t t', In (t,t') rpo_l -> rpo t t';     rpo_eq_valid : forall t t', In (t,t') rpo_eq_l -> rpo_eq t t';     equiv_l_valid : forall t t', In (t,t') equiv_l -> equiv t t'   }. Function remove_equiv_eval (p : term -> term -> option bool)     (t : term) (l : list term) {struct l} : result (list term) :=      match l with      | nil => @Not_found _      | a :: l =>             match p t a with             | Some true => (Found _ l)             | Some false =>                match remove_equiv_eval p t l with                | Found l' => Found _ (a :: l')                | Not_found => @Not_found _                | Not_finished => @Not_finished _                end              | None => @Not_finished _              end             end. Function remove_equiv_eval_list (p : term -> term -> option bool) (l1 l2 : list term)   {struct l1} : option ((list term) * (list term)):=     match l1, l2 with     | _, nil => Some (l1,l2)     | nil, _ => Some (l1,l2)     | a1 :: l1, l2 =>           match remove_equiv_eval p a1 l2 with           | Found l2' => remove_equiv_eval_list p l1 l2'           | Not_found =>                       match remove_equiv_eval_list p l1 l2 with                       | Some (l1',l2') => Some (a1 :: l1', l2')                       | None => None                       end           | Not_finished => None           end      end. Function equiv_eval_list (p : term -> term -> option bool) (l1 l2 : list term) {struct l1} : option bool :=      match l1, l2 with     | nil, nil => Some true     | (a :: l), (b :: l') =>               match p a b with               | Some true => equiv_eval_list p l l'               | Some false => Some false               | None => None               end          | _, _ => Some false     end. Function find (t1 t2:term) (l:list (term*term)) {struct l} : bool :=   match l with     | nil => false     | (t1',t2')::l =>       if eq_term_dec t1' t1         then if eq_term_dec t2' t2           then true           else find t1 t2 l         else find t1 t2 l   end. Fixpoint equiv_eval rpo_infos (n : nat) (t1 t2 : term) {struct n} : option bool :=    match n with    | 0 => None    | S m =>      match t1, t2 with      | Var v1, Var v2 =>          if X.eq_dec v1 v2 then Some true else Some false      | Term f1 l1, Term f2 l2 =>        if find t1 t2 rpo_infos.(equiv_l)          then Some true          else            if F.Symb.eq_dec f1 f2              then                match status f1 with                  | Lex => equiv_eval_list (equiv_eval rpo_infos m) l1 l2                  | Mul =>                    match remove_equiv_eval_list (equiv_eval rpo_infos m) l1 l2 with                      | Some (nil,nil) => Some true                      | Some _ => Some false                      | None => None                    end                end              else Some false        | _, _ => Some false      end    end. Lemma equiv_eval_equation :   forall rpo_infos n t1 t2, equiv_eval rpo_infos n t1 t2 =    match n with    | 0 => None    | S m =>      match t1, t2 with      | Var v1, Var v2 =>          if X.eq_dec v1 v2 then Some true else Some false      | Term f1 l1, Term f2 l2 =>        if find t1 t2 rpo_infos.(equiv_l)          then Some true          else            if F.Symb.eq_dec f1 f2              then                match status f1 with                  | Lex => equiv_eval_list (equiv_eval rpo_infos m) l1 l2                  | Mul =>                    match remove_equiv_eval_list (equiv_eval rpo_infos m) l1 l2 with                      | Some (nil,nil) => Some true                      | Some _ => Some false                      | None => None                    end                end              else Some false        | _, _ => Some false      end    end. Proof. intros rpo_infos [ | n] [v1 | f1 l1] [v2 | f2 l2]; unfold equiv_eval; simpl; trivial. Qed. Lemma equiv_eval_list_is_sound :   forall p l1 l2, match equiv_eval_list p l1 l2 with       | Some true => length l1 = length l2 /\                               (forall t1 t2, In (t1,t2) (combine l1 l2) -> p t1 t2 = Some true)       | Some false => length l1 <> length l2 \/                                (exists t1, exists t2,                                  In (t1,t2) (combine l1 l2) /\ p t1 t2 = Some false)       | None => exists t1, exists t2, In (t1,t2) (combine l1 l2) /\                             p t1 t2 = None       end. Proof. intros p l1; induction l1 as [ | t1 l1]; intros [ | t2 l2]; simpl. split; trivial; intros; contradiction. left; discriminate. left; discriminate. assert (H : forall u2, u2 = t2 -> p t1 u2 = p t1 t2). intros; subst; trivial. destruct (p t1 t2) as [ [ | ] | ]; generalize (H _ (refl_equal _)); clear H; intro H. generalize (IHl1 l2); destruct (equiv_eval_list p l1 l2) as [ [ | ] | ]. intros [L H']; repeat split. rewrite L; trivial. intros t3 t4 [t3t4_eq_t1t2 | t3t4_in_ll]. injection t3t4_eq_t1t2; intros; subst; trivial. apply H'; trivial. intros [L | [t3 [t4 [H' H'']]]]. left; intros H''; apply L; injection H''; intros; trivial. right; exists t3; exists t4; split; trivial; right; trivial. intros [t3 [t4 [H' H'']]]; exists t3; exists t4; split; trivial; right; trivial. right; exists t1; exists t2; split; trivial; left; trivial. exists t1; exists t2; split; trivial; left; trivial. Qed. Lemma remove_equiv_eval_is_sound :   forall p t l,       match remove_equiv_eval p t l with       | Found l' =>                 exists t', p t t' = Some true /\                    list_permut.permut (@eq term) l (t' :: l')       | Not_found => forall t', In t' l -> p t t' = Some false       | Not_finished => exists t', In t' l /\ p t t' = None       end. intros p t l; functional induction (remove_equiv_eval p t l) as   [ | H1 a l t' H | H1 a l t' H IH l' H' | H1 a l t' H IH H' | H1 a l t' H IH H' | H1 a l t' H]. simpl; intros; contradiction. exists a; split; auto. apply list_permut.permut_refl; intro; trivial. rewrite H' in IH; destruct IH as [t' [H'' P]]; exists t'; split; trivial. apply (Pcons (R := @eq term) a a (l := l) (t' :: nil) l'); trivial. rewrite H' in IH; intros t' [a_eq_t' | t'_in_l]; [subst | apply IH]; trivial. rewrite H' in IH; destruct IH as [t' [t'_in_l ptt'_eq_none]]; exists t'; split; trivial; right; trivial. exists a; split; trivial; left; trivial. Qed. Lemma remove_equiv_eval_list_is_sound :   forall p l1 l2,     match remove_equiv_eval_list p l1 l2 with          | Some (l1',l2') =>               exists ll, (forall t1 t2, In (t1,t2) ll -> p t1 t2 = Some true) /\                 list_permut.permut (@eq term) l1 (l1' ++ (map (fun st => fst st) ll)) /\                 list_permut.permut (@eq term) l2 (l2' ++ (map (fun st => snd st) ll)) /\                 (forall t1 t2, In t1 l1' -> In t2 l2' -> p t1 t2 = Some false)          | None => exists t1, exists t2, In t1 l1 /\ In t2 l2 /\ p t1 t2 = None     end. Proof. intros p l1 l2; functional induction (remove_equiv_eval_list p l1 l2) as [ l1 | H1 l2 H2 H3 H4 H' | H1 l2 t1 l1 H2 H3 H4 H' l2' H IH | H1 l2 t1 l1 H2 H3 H4 H' H IH l1' l2' R | H1 l2 t1 l1 H2 H3 H4 H' H IH R | H1 l2 t1 l1 H2 H3 H4 H' H]. exists (@nil (term * term)); simpl; intuition; intros. rewrite <- app_nil_end; apply list_permut.permut_refl; intro; trivial. apply list_permut.permut_refl; intro; trivial. destruct l2 as [ | t2 l2]. contradiction. exists (@nil (term * term)); simpl; intuition; intros. apply list_permut.permut_refl; intro; trivial. rewrite <- app_nil_end; apply list_permut.permut_refl; intro; trivial. assert (K := remove_equiv_eval_is_sound p t1 l2); rewrite H in K. destruct K as [t2' [pt1t2_eq_true P]]. destruct (remove_equiv_eval_list p l1 l2') as [ [l1'' l2''] | ]. destruct IH as [ll [E_ll [P1 [P2 F]]]]; exists ((t1,t2') :: ll); repeat split; trivial. intros u1 u2 [u1u2_eq_t1t2' | u1u2_in_ll]. injection u1u2_eq_t1t2'; intros; subst; apply pt1t2_eq_true. apply E_ll; trivial. simpl; apply Pcons; trivial. apply list_permut.permut_trans with (t2' :: l2'); trivial. intros a b c _ a_eq_b b_eq_c; transitivity b; trivial. simpl; apply Pcons; trivial. destruct IH as [t1' [t2 [t1_in_l1 [t2_in_l2 p1p2_eq_none]]]]; exists t1'; exists t2; repeat split; trivial. right; trivial. destruct (list_permut.permut_inv_right P) as [t2'' [k2 [k2' [t2''_eq_t2' [H'' P']]]]]. subst l2; apply in_insert. generalize (k2 ++ k2') l2' t2_in_l2 P'; intro k; induction k as [ | u k]; intros l t2_in_l Q; inversion Q as [ | a b k' l1' l2]; subst; trivial. destruct (in_app_or _ _ _ t2_in_l) as [t2_in_l1' | [t2_eq_b | t2_in_l2']]. right; apply (IHk (l1' ++ l2)); trivial; apply in_or_app; left; trivial. left; subst; trivial. right; apply (IHk (l1' ++ l2)); trivial; apply in_or_app; right; trivial. assert (K := remove_equiv_eval_is_sound p t1 l2); rewrite H in K. rewrite R in IH; destruct IH as [ll [E_ll [P1 [P2 F]]]]; exists ll; repeat split; auto. simpl; apply (Pcons (R := @eq term) t1 t1 (l := l1) nil                        (l1' ++ map (fun st : term * term => fst st) ll)); trivial. simpl; intros u1 u2 [u1_eq_t1 | u1_in_l1'] u2_in_l2'. subst u1; apply K; setoid_rewrite (in_permut_in P2); apply in_or_app; left; trivial. apply F; trivial. rewrite R in IH; destruct IH as [u1 [u2 [u1_in_l1 [u2_in_l2 pu1u2_eq_none]]]]; exists u1; exists u2; repeat split; trivial; right; trivial. assert (K := remove_equiv_eval_is_sound p t1 l2); rewrite H in K. destruct K as [t2 [t2_in_l2 pt1t2_eq_none]]; exists t1; exists t2; repeat split; trivial; left; trivial. Qed. Lemma find_is_sound :   forall (I: term -> term -> Prop) l (l_sound: forall t t', In (t,t') l -> I t t') t1 t2,     find t1 t2 l = true ->     I t1 t2. Proof.   intros I l l_sound t1 t2.   functional induction (find t1 t2 l)     as [ | xx t1' t2' l xxx Heq _ Heq' _ | xx t1' t2' l xxx Heq _ Heq' _ IH | xx t1' t2' l xxx Heq _ IH ]. intros;discriminate. intros _; apply l_sound;simpl;auto. simpl in l_sound;intros Hrec. apply IH;auto. simpl in l_sound;intros Hrec;apply IH;auto. Qed. Lemma equiv_eval_is_sound_weak :   forall rpo_infos n t1 t2, equiv_eval rpo_infos n t1 t2 = Some true -> equiv t1 t2. intros rpo_infos n; induction n as [ | n]. intros; discriminate. destruct t1 as [v1 | f1 l1]; destruct t2 as [v2 | f2 l2]; simpl. destruct (X.eq_dec v1 v2) as [v1_eq_v2 | v1_diff_v2]. subst; intuition; apply Eq. intro; discriminate. intro; discriminate. intro; discriminate. case_eq (find (Term f1 l1) (Term f2 l2) (equiv_l rpo_infos));simpl. intros H _ ;eapply find_is_sound with (1:=equiv_l_valid rpo_infos);auto. intros _. destruct (F.Symb.eq_dec f1 f2) as [f1_eq_f2 | f1_diff_f2]. assert (Sf1 := f_equal status f1_eq_f2); destruct (status f2); subst f2; rewrite Sf1. intro H; apply Eq_lex; trivial. generalize l1 l2 H; clear l1 l2 H; intro l; induction l as [ | t l]; intros [ | t' l'] H. apply Eq_list_nil. discriminate. discriminate. simpl in H; apply Eq_list_cons. apply IHn; destruct (equiv_eval rpo_infos n t t') as [ [ | ] | ]; trivial; discriminate. apply IHl; destruct (equiv_eval rpo_infos n t t') as [ [ | ] | ]; trivial; discriminate. intro H; assert (H' := remove_equiv_eval_list_is_sound (equiv_eval rpo_infos n) l1 l2); destruct (remove_equiv_eval_list (equiv_eval rpo_infos n) l1 l2) as [ [l1' l2'] | ]. destruct H' as [ll [E_ll [P1 [P2 H']]]]; apply Eq_mul; trivial. destruct l1'; destruct l2'; try discriminate; simpl in P1; trivial. generalize l1 l2 P1 P2; clear l1 l2 P1 P2; induction ll as [ | [t1 t2] ll]; intros l1 l2 P1 P2. rewrite (permut_nil P1); rewrite (permut_nil P2); apply Pnil. destruct (permut_inv_right P1) as [t1' [l1' [l1'' [t1_eq_t1' [H'' Q1]]]]]; subst l1 t1'. destruct (permut_inv_right P2) as [t2' [l2' [l2'' [t2_eq_t2' [H'' Q2]]]]]; subst l2 t2'. simpl; apply permut_strong. apply IHn; apply E_ll; left; trivial. apply IHll; trivial. intros; apply E_ll; right; trivial. discriminate. intro; discriminate. Qed. Lemma equiv_eval_list_fully_evaluates :   forall p l1 l2, (forall t1 t2, In t1 l1 -> In t2 l2 -> p t1 t2 <> None) ->   equiv_eval_list p l1 l2 <> None. Proof. intros p l1 l2 E; functional induction (equiv_eval_list p l1 l2) as [ | H1 H2 t1 l1 H3 t2 l2 H4 H IH | H1 H2 t1 l1 H3 t2 l2 H4 H IH | H1 H2 t1 l1 H3 t2 l2 H4 H IH | l1 l2 H1 H2 H3 H4 H]. discriminate. apply IH; intros u1 u2 u1_in_l1 u2_in_l2; apply E; right; trivial. discriminate. assert (E' := E t1 t2); rewrite H in E'; apply E'; left; trivial. discriminate. Qed. Lemma remove_equiv_eval_fully_evaluates :   forall p t l, (forall t', In t' l -> p t t' <> None) ->   remove_equiv_eval p t l <> @Not_finished _. Proof. intros p t l E; functional induction (remove_equiv_eval p t l) as   [ | H1 a l t' H | H1 a l t' H IH l' H' | H1 a l t' H IH H' | H1 a l t' H IH H' | H1 a l t' H]. discriminate. discriminate. discriminate. discriminate. rewrite H' in IH; apply IH; intros; apply E; right; trivial. assert (H' := E _ (or_introl _ (refl_equal _)) H); contradiction. Qed. Lemma remove_equiv_eval_list_fully_evaluates :   forall p l1 l2, (forall t1 t2, In t1 l1 -> In t2 l2 -> p t1 t2 <> None) ->   remove_equiv_eval_list p l1 l2 <> None. Proof. intros p l1 l2 E; functional induction (remove_equiv_eval_list p l1 l2) as [ l1 | H1 l2 H2 H3 H4 H' | H1 l2 t1 l1 H2 H3 H4 H' l2' H IH | H1 l2 t1 l1 H2 H3 H4 H' H IH l1' l2' R | H1 l2 t1 l1 H2 H3 H4 H' H IH R | H1 l2 t1 l1 H2 H3 H4 H' H]. discriminate. discriminate. assert (K := remove_equiv_eval_is_sound p t1 l2); rewrite H in K; destruct K as [t2 [t2_in_l2 P2]]; apply IH; intros u1 u2 u1_in_l1 u2_in_l2'; apply E; trivial. right; trivial. setoid_rewrite (in_permut_in P2); right; trivial. discriminate. rewrite R in IH; apply IH; intros u1 u2 u1_in_l1 u2_in_l2; apply E; trivial; right; trivial. assert (K := remove_equiv_eval_fully_evaluates p t1 l2); rewrite H in K; intros _; apply K; trivial. intros t2 t2_in_l2; apply E; trivial; left; trivial. Qed. Lemma equiv_eval_terminates :   forall rpo_infos n t1 t2, size t1 + size t2 <= n -> equiv_eval rpo_infos n t1 t2 <> None. Proof. intros rpo_infos n; induction n as [ | n]. intros t1 t2 St1; absurd (1 <= 0); auto with arith; apply le_trans with (size t1 + size t2); trivial; apply le_trans with (1 + size t2); [apply le_plus_l | apply plus_le_compat_r; apply size_ge_one]. intros t1 t2 St; rewrite equiv_eval_equation. destruct t1 as [ v1 | f1 l1]; destruct t2 as [ v2 | f2 l2]. destruct (X.eq_dec v1 v2); intros; discriminate. intros; discriminate. intros; discriminate. destruct (find (Term f1 l1) (Term f2 l2) (equiv_l rpo_infos)). intro;discriminate. destruct (F.Symb.eq_dec f1 f2) as [f1_eq_f2 | f1_diff_f2]; [idtac | intros; discriminate]. assert (H : forall t1 t2 : term, In t1 l1 -> In t2 l2 -> equiv_eval rpo_infos n t1 t2 <> None). intros t1 t2 t1_in_l1 t2_in_l2; apply IHn. rewrite size_unfold in St; rewrite <- plus_assoc in St. rewrite size_unfold in St; simpl in St. refine (le_trans _ _ _ _ (le_S_n _ _ St)); apply plus_le_compat. generalize (size_direct_subterm t1 (Term f1 l1) t1_in_l1); rewrite (size_unfold (Term f1 l1)); simpl; auto with arith. generalize (size_direct_subterm t2 (Term f1 l2) t2_in_l2); rewrite (size_unfold (Term f1 l2)); simpl; auto with arith. assert (Sf1 := f_equal status f1_eq_f2); destruct (status f2); subst f2; rewrite Sf1. apply equiv_eval_list_fully_evaluates; trivial. assert (H':= remove_equiv_eval_list_fully_evaluates (equiv_eval rpo_infos n) l1 l2 H); destruct (remove_equiv_eval_list (equiv_eval rpo_infos n) l1 l2) as [ [[ | t1' l1'] [ | t2' l2']] | ]; try discriminate. intros _; apply H'; trivial. Qed. Lemma equiv_eval_is_complete_true :   forall rpo_infos n t1 t2, size t1 + size t2 <= n -> equiv t1 t2 ->      equiv_eval rpo_infos n t1 t2 = Some true. Proof. intros rpo_infos n; induction n as [ | n ]. intros t1 t2 St; absurd (1 <= 0); auto with arith. refine (le_trans _ _ _ _ St); apply le_trans with (size t1); [ apply size_ge_one | apply le_plus_l]. intros t1 t2 St t1_eq_t2; inversion t1_eq_t2 as [ t | f l1 l2 Sf | f l1 l2 Sf P1 P2]; subst. destruct t2 as [v2 | f2 l2]; simpl. destruct (X.eq_dec v2 v2) as [v2_eq_v2 | v2_diff_v2]; trivial. absurd (v2 = v2); trivial. destruct (find (Term f2 l2) (Term f2 l2) (equiv_l rpo_infos)). trivial. destruct (F.Symb.eq_dec f2 f2) as [f2_eq_f2 | f2_diff_f2]. assert (H : forall t2, In t2 l2 -> equiv_eval rpo_infos n t2 t2 = Some true). intros t2 t2_in_l2; apply IHn. apply le_S_n; refine (le_trans _ _ _ _ St); replace (S (size t2 + size t2)) with (S (size t2) + size t2); trivial; apply plus_le_compat; [idtac | apply lt_le_weak]; apply size_direct_subterm; trivial. apply Eq. destruct (status f2). clear St t1_eq_t2; induction l2 as [ | t2 l2]; simpl; trivial. rewrite (H t2); [rewrite IHl2 | left]; trivial; intros; apply H; right; trivial. assert (H' : remove_equiv_eval_list (equiv_eval rpo_infos n) l2 l2 = Some (nil,nil)). clear St t1_eq_t2; induction l2 as [ | t2 l2]; simpl; trivial. rewrite (H t2); [rewrite IHl2 | left]; trivial; intros; apply H; right; trivial. rewrite H'; trivial. absurd (f2 = f2); trivial. rewrite equiv_eval_equation. destruct (find (Term f l1) (Term f l2) (equiv_l rpo_infos)). trivial. rewrite Sf; destruct (F.Symb.eq_dec f f) as [_ | f_diff_f]. assert (Size : forall t1 t2, In t1 l1 -> In t2 l2 -> size t1 + size t2 <= n). intros t1 t2 t1_in_l1 t2_in_l2; apply le_S_n; refine (le_trans _ _ _ _ St); replace (S (size t1 + size t2)) with (S (size t1) + size t2); trivial; apply plus_le_compat; [idtac | apply lt_le_weak]; apply size_direct_subterm; trivial. generalize l2 H Size; clear l2 H Size St t1_eq_t2; induction l1 as [ | t1 l1]; intros l2 H Size; inversion H as [ | s t2 l l2' t1_eq_t2 l1_eq_l2']; subst; simpl. trivial. rewrite (IHn t1 t2); trivial. apply IHl1; trivial. intros; apply Size; right; trivial. apply Size; left; trivial. absurd (f = f); trivial. assert (St' : forall t1 t2, In t1 l1 -> In t2 l2 -> size t1 + size t2 <= n). intros t1 t2 t1_in_l1 t2_in_l2; apply le_S_n; refine (le_trans _ _ _ _ St); replace (S (size t1 + size t2)) with (S (size t1) + size t2); trivial; apply plus_le_compat; [idtac | apply lt_le_weak]; apply size_direct_subterm; trivial. assert (T : forall t1 t2, In t1 l1 -> In t2 l2 -> equiv_eval rpo_infos n t1 t2 <> None). intros t1 t2 t1_in_l1 t2_in_l2; apply equiv_eval_terminates; apply St'; trivial. assert (H' : remove_equiv_eval_list (equiv_eval rpo_infos n) l1 l2 = Some (nil,nil)). generalize l2 P1 St' T; clear l2 P1 St t1_eq_t2 St' T; induction l1 as [ | t1 l1]; intros l2 P1 St' T; inversion P1 as [ | t1' t2 l1' l2' l2'' t1_eq_t2 l1_eq_l2]; trivial. assert (H' := remove_equiv_eval_is_sound (equiv_eval rpo_infos n) t1 l2). subst; simpl. destruct (remove_equiv_eval (equiv_eval rpo_infos n) t1 (l2' ++ t2 :: l2''))   as [ | | l']. assert (H'' := H' t2); rewrite (IHn t1 t2) in H''; trivial. assert (H''' : Some true = Some false). apply H''; apply in_or_app; right; left; trivial. discriminate. apply St'. left; trivial. apply in_or_app; right; left; trivial. assert False. destruct H' as [t' [t'_in_l2 H'']]. apply (T t1 t'); trivial; left; trivial. contradiction. destruct H' as [t' [t1_eq_t' P2]]. assert (H : l2' ++ t2 :: l2'' <> nil). destruct l2' as [ | t2' l2']; simpl; discriminate. assert (Q : list_permut.permut (eq (A:=term)) (t2 :: l2' ++ l2'') (l2' ++ t2 :: l2'')). apply Pcons; trivial. apply list_permut.permut_refl; intro; trivial. destruct (l2' ++ t2 :: l2'') as [ | t2' k2]. absurd (@nil term = nil); trivial. apply IHl1; trivial. apply permut_trans with (l2' ++ l2''); trivial. assert (t1_eq_t'' : equiv t1 t'). apply (equiv_eval_is_sound_weak _ _ _ _ t1_eq_t'). assert (t2_eq_t' : equiv t2 t'). transitivity t1; trivial; symmetry; trivial. setoid_rewrite (permut_cons (l2' ++ l2'') l' t2_eq_t'). apply permut_impl with (@eq term); trivial. intros; subst; apply Eq. apply list_permut.permut_trans with (t2' :: k2); trivial. intros a b c _ _ _ a_eq_b b_eq_c; subst; trivial. intros; apply St'. right; trivial. setoid_rewrite (in_permut_in P2); right; trivial. intros; apply T. right; trivial. setoid_rewrite (in_permut_in P2); right; trivial. rewrite equiv_eval_equation; rewrite Sf; rewrite H'. destruct (find (Term f l1) (Term f l2) (equiv_l rpo_infos)). trivial. destruct (F.Symb.eq_dec f f) as [f_eq_f | f_diff_f]; trivial; absurd (f = f); trivial. Qed. Lemma equiv_eval_is_sound :   forall rpo_infos n t1 t2, size t1 + size t2 <= n ->      match equiv_eval rpo_infos n t1 t2 with      | Some true => equiv t1 t2      | Some false => ~equiv t1 t2      | None => False      end. Proof. intros rpo_infos n t1 t2 St; assert (H := equiv_eval_is_sound_weak rpo_infos n t1 t2); assert (T := equiv_eval_terminates rpo_infos n t1 t2 St); assert (H' := equiv_eval_is_complete_true rpo_infos n t1 t2 St); destruct (equiv_eval rpo_infos n t1 t2) as [ [ | ] | ]. apply H; trivial. intro t1_eq_t2; assert (H'' := H' t1_eq_t2); discriminate. apply T; trivial. Qed. Fixpoint lexico_eval (p : term -> term -> option comp) (s1 s2 : term)    (l1 l2 : list term) {struct l1} : option comp :=     match l1, l2 with     | nil, nil => Some Equivalent     | (t1 :: l1'), (t2 :: l2') =>           match p t1 t2 with           | Some Equivalent => lexico_eval p s1 s2 l1' l2'           | Some Greater_than =>              let check_s1_gt_l2 :=               list_forall_option                 (fun t2 =>                    match p s1 t2 with                      | Some Greater_than => Some true                      | Some _ => Some false                      | None => None                     end) l2 in             match check_s1_gt_l2 with             | Some true => Some Greater_than             | Some false => Some Uncomparable             | None => None             end           | Some Less_than =>               let check_s2_gt_l1 :=                 list_forall_option                 (fun t1 =>                    match p t1 s2 with                      | Some Less_than => Some true                      | Some _ => Some false                      | None => None                     end) l1 in               match check_s2_gt_l1 with               | Some true => Some Less_than               | Some false => Some Uncomparable               | None => None               end          | Some Uncomparable => Some Uncomparable          | None => None      end    | _, _ => Some Uncomparable end. Lemma lexico_eval_equation :   forall p s1 s2 l1 l2, lexico_eval p s1 s2 l1 l2 =     match l1, l2 with     | nil, nil => Some Equivalent     | (t1 :: l1'), (t2 :: l2') =>           match p t1 t2 with           | Some Equivalent => lexico_eval p s1 s2 l1' l2'           | Some Greater_than =>              let check_s1_gt_l2 :=               list_forall_option                 (fun t2 =>                    match p s1 t2 with                      | Some Greater_than => Some true                      | Some _ => Some false                      | None => None                     end) l2 in             match check_s1_gt_l2 with             | Some true => Some Greater_than             | Some false => Some Uncomparable             | None => None             end           | Some Less_than =>               let check_s2_gt_l1 :=                 list_forall_option                 (fun t1 =>                    match p t1 s2 with                      | Some Less_than => Some true                      | Some _ => Some false                      | None => None                     end) l1 in               match check_s2_gt_l1 with               | Some true => Some Less_than               | Some false => Some Uncomparable               | None => None               end          | Some Uncomparable => Some Uncomparable          | None => None      end    | _, _ => Some Uncomparable end. Proof. intros p s1 s2 [ | t1 l1] [ | t2 l2]; apply refl_equal. Qed. Definition mult_eval (p : term -> term -> option comp) (l1 l2 : list term) : option comp :=          let check_l1_gt_l2 :=            list_forall_option               (fun t2 =>                  list_exists_option                    (fun t1 =>                       match p t1 t2 with                         | Some Greater_than => Some true                         | Some _ => Some false                         | None => None                       end) l1) l2 in          match check_l1_gt_l2 with          | None => None         | Some true => Some Greater_than         | Some false =>           let check_l1_lt_l2 :=              list_forall_option                 (fun t1 =>                    list_exists_option                      (fun t2 =>                         match p t1 t2 with                           | Some Less_than => Some true                           | Some _ => Some false                           | None => None                          end) l2) l1 in           match check_l1_lt_l2 with           | Some true => Some Less_than           | Some false => Some Uncomparable           | None => None           end end. Fixpoint rpo_eval rpo_infos (n : nat) (t1 t2 : term) {struct n} : option comp :=     if find t1 t2 (rpo_l rpo_infos)       then Some Less_than       else if find t2 t1 (rpo_l rpo_infos)         then Some Greater_than         else if find t1 t2 (equiv_l rpo_infos)           then Some Equivalent           else if find t2 t1 (equiv_l rpo_infos)             then Some Equivalent             else              (match equiv_eval rpo_infos n t1 t2 with   | None => None   | Some true => Some Equivalent   | Some false =>      (match t1, t2 with      | Var _, Var _ => Some Uncomparable      | Var x, (Term _ l) =>             if var_in_term_list x l             then Some Less_than             else Some Uncomparable      | (Term _ l), Var x =>             if var_in_term_list x l             then Some Greater_than             else Some Uncomparable      | (Term f1 l1), (Term f2 l2) =>        (match n with        | 0 => None        | S m =>          let check_l1_gt_t2 :=                      list_exists_option                           (fun t => match rpo_eval rpo_infos m t t2 with                                     | Some Equivalent                                     | Some Greater_than => Some true                                     | Some _ => Some false                                     | None => None                                    end) l1 in           (match check_l1_gt_t2 with           | None => None           | Some true => Some Greater_than           | Some false =>             let check_l2_gt_t1 :=                    list_exists_option                         (fun t => match rpo_eval rpo_infos m t1 t with                                        | Some Equivalent                                        | Some Less_than => Some true                                        | Some _ => Some false                                        | None => None                                      end) l2 in           (match check_l2_gt_t1 with           | None => None           | Some true => Some Less_than           | Some false =>              (match prec_eval f1 f2 with                   | Uncomparable => Some Uncomparable                   | Greater_than =>                        let check_l2_lt_t1 :=                           list_forall_option                               (fun t => match rpo_eval rpo_infos m t1 t with                                                | Some Greater_than => Some true                                                | Some _ => Some false                                                | None => None                                                end) l2 in                      (match check_l2_lt_t1 with                      | None => None                      | Some true => Some Greater_than                      | Some false => Some Uncomparable                     end)                   | Less_than =>                       let check_l1_lt_t2 :=                           list_forall_option                             (fun t => match rpo_eval rpo_infos m t t2 with                                                | Some Less_than => Some true                                                | Some _ => Some false                                                | None => None                                                end) l1 in                       (match check_l1_lt_t2 with                       | None => None                       | Some true => Some Less_than                       | Some false => Some Uncomparable                     end)                   | Equivalent =>                         (match status f1 with                           | Mul =>                                 match remove_equiv_eval_list (equiv_eval rpo_infos m) l1 l2 with                                 | None => None                                 | Some (nil, nil) => Some Equivalent                                 | Some (nil, _ :: _) => Some Less_than                                 | Some (_ :: _,nil) => Some Greater_than                                 | Some (l1, l2) => mult_eval (rpo_eval rpo_infos m) l1 l2                                 end                           | Lex => lexico_eval (rpo_eval rpo_infos m) t1 t2 l1 l2                        end)           end)         end)       end)     end)   end) end). Lemma rpo_eval_equation :   forall rpo_infos n t1 t2, rpo_eval rpo_infos n t1 t2 =     if find t1 t2 (rpo_l rpo_infos)       then Some Less_than       else if find t2 t1 (rpo_l rpo_infos)         then Some Greater_than         else if find t1 t2 (equiv_l rpo_infos)           then Some Equivalent           else if find t2 t1 (equiv_l rpo_infos)             then Some Equivalent             else              (match equiv_eval rpo_infos n t1 t2 with   | None => None   | Some true => Some Equivalent   | Some false =>      (match t1, t2 with      | Var _, Var _ => Some Uncomparable      | Var x, (Term _ l) =>             if var_in_term_list x l             then Some Less_than             else Some Uncomparable      | (Term _ l), Var x =>             if var_in_term_list x l             then Some Greater_than             else Some Uncomparable      | (Term f1 l1), (Term f2 l2) =>        (match n with        | 0 => None        | S m =>          let check_l1_gt_t2 :=                      list_exists_option                           (fun t => match rpo_eval rpo_infos m t t2 with                                     | Some Equivalent                                     | Some Greater_than => Some true                                     | Some _ => Some false                                     | None => None                                    end) l1 in           (match check_l1_gt_t2 with           | None => None           | Some true => Some Greater_than           | Some false =>             let check_l2_gt_t1 :=                    list_exists_option                         (fun t => match rpo_eval rpo_infos m t1 t with                                        | Some Equivalent                                        | Some Less_than => Some true                                        | Some _ => Some false                                        | None => None                                      end) l2 in           (match check_l2_gt_t1 with           | None => None           | Some true => Some Less_than           | Some false =>              (match prec_eval f1 f2 with                   | Uncomparable => Some Uncomparable                   | Greater_than =>                        let check_l2_lt_t1 :=                           list_forall_option                               (fun t => match rpo_eval rpo_infos m t1 t with                                                | Some Greater_than => Some true                                                | Some _ => Some false                                                | None => None                                                end) l2 in                      (match check_l2_lt_t1 with                      | None => None                      | Some true => Some Greater_than                      | Some false => Some Uncomparable                     end)                   | Less_than =>                       let check_l1_lt_t2 :=                           list_forall_option                             (fun t => match rpo_eval rpo_infos m t t2 with                                                | Some Less_than => Some true                                                | Some _ => Some false                                                | None => None                                                end) l1 in                       (match check_l1_lt_t2 with                       | None => None                       | Some true => Some Less_than                       | Some false => Some Uncomparable                     end)                   | Equivalent =>                         (match status f1 with                           | Mul =>                                 match remove_equiv_eval_list (equiv_eval rpo_infos m) l1 l2 with                                 | None => None                                 | Some (nil, nil) => Some Equivalent                                 | Some (nil, _ :: _) => Some Less_than                                 | Some (_ :: _,nil) => Some Greater_than                                 | Some (l1, l2) => mult_eval (rpo_eval rpo_infos m) l1 l2                                 end                           | Lex => lexico_eval (rpo_eval rpo_infos m) t1 t2 l1 l2                        end)           end)         end)       end)     end)   end) end). Proof. intros rpo_infos [ | n] [v1 | f1 l1] [v2 | f2 l2]; unfold rpo_eval; simpl; trivial. Qed. Lemma lexico_eval_is_sound :   forall (p : term -> term -> option comp) s1 s2 l1 l2,            length l1 = length l2 ->            match lexico_eval p s1 s2 l1 l2 with            | Some Equivalent =>              (exists ll, (forall t1 t2, In (t1,t2) ll -> p t1 t2 = Some Equivalent) /\                             l1 = map (fun st => fst st) ll /\                             l2 = map (fun st => snd st) ll)              | Some Less_than =>                  (exists ll, exists t1, exists t2, exists l1', exists l2',                    (forall t1 t2, In (t1,t2) ll -> p t1 t2 = Some Equivalent) /\                    p t1 t2 = Some Less_than /\                    (forall t1, In t1 l1 ->                    ((exists t2, In t2 l2 /\ (p t1 t2 = Some Equivalent \/                                                      p t1 t2 = Some Less_than)) \/                                                   p t1 s2 = Some Less_than)) /\                    l1 = map (fun st => fst st) ll ++ t1 :: l1' /\                    l2 = map (fun st => snd st) ll ++ t2 :: l2')              | Some Greater_than =>                  (exists ll, exists t1, exists t2, exists l1', exists l2',                    (forall t1 t2, In (t1,t2) ll -> p t1 t2 = Some Equivalent) /\                    p t1 t2 = Some Greater_than /\                    (forall t2, In t2 l2 ->                    ((exists t1, In t1 l1 /\ (p t1 t2 = Some Equivalent \/                                                      p t1 t2 = Some Greater_than)) \/                                                   p s1 t2 = Some Greater_than)) /\                    l1 = map (fun st => fst st) ll ++ t1 :: l1' /\                    l2 = map (fun st => snd st) ll ++ t2 :: l2')             | _ => True end. Proof. intros p s1 s2 l1; induction l1 as [ | t1 l1]; intros [ | t2 l2] L. simpl; exists (@nil (term * term)); simpl; intuition. simpl; trivial. simpl; trivial. simpl in L; injection L; clear L; intro L; simpl. assert (P : forall u1, u1 = t1 -> p u1 t2 = p t1 t2). intros; subst; trivial. destruct (p t1 t2) as [ [ | | | ] | ]; generalize (P _ (refl_equal _)); clear P; intro P. generalize (IHl1 _ L); destruct (lexico_eval p s1 s2 l1 l2) as [ [ | | | ] | ]. intros [ll [E_ll [H1 H2]]]. exists ((t1,t2) :: ll); simpl; repeat split. intros t3 t4 [H | H]. injection H; intros; subst; trivial. apply E_ll; trivial. rewrite H1; trivial. rewrite H2; trivial. intros [ll [u1 [u2 [l1' [l2' [E_ll [P' [H [H1 H2]]]]]]]]]. exists ((t1,t2) :: ll); exists u1; exists u2; exists l1'; exists l2'; repeat split; trivial. intros t3 t4 [H' | H']. injection H'; intros; subst; trivial. apply E_ll; trivial. intros t3 [t1_eq_t3 | t3_in_l1]. subst t3. left; exists t2; split; trivial; left; trivial. destruct (H _ t3_in_l1) as [[t4 [t4_in_l2 H']] | H']. left; exists t4; split; trivial; right; trivial. right; trivial. simpl; rewrite H1; trivial. simpl; rewrite H2; trivial. intros [ll [u1 [u2 [l1' [l2' [E_ll [P' [H [H1 H2]]]]]]]]]. exists ((t1,t2) :: ll); exists u1; exists u2; exists l1'; exists l2'; repeat split; trivial. intros t3 t4 [H' | H']. injection H'; intros; subst; trivial. apply E_ll; trivial. intros t3 [t1_eq_t3 | t3_in_l1]. subst t3. left; exists t1; split; trivial; left; trivial. destruct (H _ t3_in_l1) as [[t4 [t4_in_l2 H']] | H']. left; exists t4; split; trivial; right; trivial. right; trivial. simpl; rewrite H1; trivial. simpl; rewrite H2; trivial. trivial. trivial. assert (P' : forall u1, u1 = t1 -> p u1 s2 = p t1 s2). intros; subst; trivial. destruct (p t1 s2) as [ [ | | | ] | ]; generalize (P' _ (refl_equal _)); clear P'; intro P'; generalize (list_forall_option_is_sound         (fun t3 : term =>          match p t3 s2 with          | Some Equivalent => Some false          | Some Less_than => Some true          | Some Greater_than => Some false          | Some Uncomparable => Some false          | None => None (A:=bool)          end) l1); destruct (list_forall_option         (fun t3 : term =>          match p t3 s2 with          | Some Equivalent => Some false          | Some Less_than => Some true          | Some Greater_than => Some false          | Some Uncomparable => Some false          | None => None (A:=bool)          end) l1) as [ [ | ] | ]; trivial. intros H. exists (@nil (term * term)); exists t1; exists t2; exists l1; exists l2; repeat split; trivial. simpl; tauto. intros u1 [u1_eq_t1 | u1_in_l1]. left; exists t2; split. left; trivial. subst; right; trivial. right; generalize (H _ u1_in_l1); destruct (p u1 s2) as [ [ | | | ] | ]; trivial; intros; discriminate. assert (P' : forall u2, u2 = t2 -> p s1 u2 = p s1 t2). intros; subst; trivial. destruct (p s1 t2) as [ [ | | | ] | ]; generalize (P' _ (refl_equal _)); clear P'; intro P'; generalize (list_forall_option_is_sound         (fun t3 : term =>          match p s1 t3 with          | Some Equivalent => Some false          | Some Less_than => Some false          | Some Greater_than => Some true          | Some Uncomparable => Some false          | None => None (A:=bool)          end) l2); destruct (list_forall_option         (fun t3 : term =>          match p s1 t3 with          | Some Equivalent => Some false          | Some Less_than => Some false          | Some Greater_than => Some true          | Some Uncomparable => Some false          | None => None (A:=bool)          end) l2) as [ [ | ] | ]; trivial. intros H. exists (@nil (term * term)); exists t1; exists t2; exists l1; exists l2; repeat split; trivial. simpl; tauto. intros u2 [u2_eq_t2 | u2_in_l2]. left; exists t1; split. left; trivial. subst; right; trivial. right; generalize (H _ u2_in_l2); destruct (p s1 u2) as [ [ | | | ] | ]; trivial; intros; discriminate. trivial. trivial. Qed. Lemma mult_eval_is_sound_weak :   forall p l1 l2,    match mult_eval p l1 l2 with      | Some Equivalent => False      | Some Less_than =>        forall t1, In t1 l1 -> exists t2, In t2 l2 /\ p t1 t2 = Some Less_than      | Some Greater_than =>        forall t2, In t2 l2 -> exists t1, In t1 l1 /\ p t1 t2 = Some Greater_than      | _ => True      end. Proof. intros p l1 l2; unfold mult_eval. generalize (list_forall_option_is_sound       (fun t2 : term =>        list_exists_option          (fun t1 : term =>           match p t1 t2 with           | Some Equivalent => Some false           | Some Less_than => Some false           | Some Greater_than => Some true           | Some Uncomparable => Some false           | None => None (A:=bool)           end) l1) l2); destruct (list_forall_option       (fun t2 : term =>        list_exists_option          (fun t1 : term =>           match p t1 t2 with           | Some Equivalent => Some false           | Some Less_than => Some false           | Some Greater_than => Some true           | Some Uncomparable => Some false           | None => None (A:=bool)           end) l1) l2) as [ [ | ] | ]. intros H t2 t2_in_l2; generalize (H _ t2_in_l2) (list_exists_option_is_sound    (fun t1 : term =>     match p t1 t2 with     | Some Equivalent => Some false     | Some Less_than => Some false     | Some Greater_than => Some true     | Some Uncomparable => Some false     | None => None (A:=bool)     end) l1); destruct (list_exists_option    (fun t1 : term =>     match p t1 t2 with     | Some Equivalent => Some false     | Some Less_than => Some false     | Some Greater_than => Some true     | Some Uncomparable => Some false     | None => None (A:=bool)     end) l1) as [ [ | ] | ]. intros _ [t1 [t1_in_l1 H']]; exists t1; split; trivial. destruct (p t1 t2) as [ [ | | | ] | ]; trivial; discriminate. intros; discriminate. intros; discriminate. intros _; generalize (list_forall_option_is_sound       (fun t1 : term =>        list_exists_option          (fun t2 : term =>           match p t1 t2 with           | Some Equivalent => Some false           | Some Less_than => Some true           | Some Greater_than => Some false           | Some Uncomparable => Some false           | None => None (A:=bool)           end) l2) l1); destruct (list_forall_option       (fun t1 : term =>        list_exists_option          (fun t2 : term =>           match p t1 t2 with           | Some Equivalent => Some false           | Some Less_than => Some true           | Some Greater_than => Some false           | Some Uncomparable => Some false           | None => None (A:=bool)           end) l2) l1) as [ [ | ] | ]. intros H t1 t1_in_l1; generalize (H _ t1_in_l1) (list_exists_option_is_sound    (fun t2 : term =>     match p t1 t2 with     | Some Equivalent => Some false     | Some Less_than => Some true     | Some Greater_than => Some false     | Some Uncomparable => Some false     | None => None (A:=bool)     end) l2); destruct (list_exists_option    (fun t2 : term =>     match p t1 t2 with     | Some Equivalent => Some false     | Some Less_than => Some true     | Some Greater_than => Some false     | Some Uncomparable => Some false     | None => None (A:=bool)     end) l2) as [ [ | ] | ]. intros _ [t2 [t2_in_l2 H']]; exists t2; split; trivial. destruct (p t1 t2) as [ [ | | | ] | ]; trivial; discriminate. intros; discriminate. intros; discriminate. trivial. trivial. trivial. Qed. Lemma well_formed_equiv :   forall t1 t2, well_formed t1 -> equiv t1 t2 -> well_formed t2. Proof. intro t1; pattern t1; apply term_rec3; clear t1. intros v t2 _ v_eq_t2; inversion v_eq_t2; subst; simpl; trivial. intros f l IH t2 Wfl fl_eq_t2; inversion fl_eq_t2; subst; trivial. assert (L' := equiv_same_length _ _ _ _ fl_eq_t2). destruct (well_formed_unfold _ Wfl) as [Wl L]. apply well_formed_fold; split. assert (IH' : forall t t2, In t l -> equiv t t2 -> well_formed t2). intros t t2 t_in_l; apply IH; trivial. apply Wl; trivial. generalize l2 H3; clear l2 IH H3 H1 L' L fl_eq_t2 Wfl; induction l as [ | t l]; intros l2 l_eq_l2; inversion l_eq_l2; subst. contradiction. intros u [u_eq_t2 | u_in_l2]; subst. apply IH' with t; trivial. left; trivial. apply IHl with l0; trivial. intros; apply Wl; right; trivial. intros u1 u2 u1_in_l; apply IH'; right; trivial. rewrite <- L'; trivial. assert (L' := equiv_same_length _ _ _ _ fl_eq_t2). destruct (well_formed_unfold _ Wfl) as [Wl L]. apply well_formed_fold; split. assert (IH' : forall t t2, In t l -> equiv t t2 -> well_formed t2). intros t t2 t_in_l; apply IH; trivial. apply Wl; trivial. generalize l2 H3; clear l2 IH H3 H1 L' L fl_eq_t2 Wfl; induction l as [ | t l]; intros l2 l_eq_l2; inversion l_eq_l2; subst. contradiction. intros u u_in_l2; destruct (in_app_or _ _ _ u_in_l2) as [u_in_l1 | [u_eq_b | u_in_l3]]. apply IHl with (l1 ++ l3); trivial. intros; apply Wl; right; trivial. intros u1 u2 u1_in_l; apply IH'; right; trivial. apply in_or_app; left; trivial. subst u; apply IH' with t; trivial; left; trivial. apply IHl with (l1 ++ l3); trivial. intros; apply Wl; right; trivial. intros u1 u2 u1_in_l; apply IH'; right; trivial. apply in_or_app; right; trivial. rewrite <- L'; trivial. Qed. Lemma well_formed_list_is_well_formed_list :   forall l, well_formed_list l -> (forall t, mem t l -> well_formed t). Proof. intro l; induction l as [ | t l]. intros; contradiction. simpl; intros [Wt Wl] u [u_eq_t | u_in_l]. apply well_formed_equiv with t; trivial. symmetry; trivial. apply IHl; trivial. Qed. Lemma rpo_eval_is_sound_weak :   forall rpo_infos n t1 t2, well_formed t1 -> well_formed t2 ->                 match rpo_eval rpo_infos n t1 t2 with                      | Some Equivalent => equiv t1 t2                      | Some Greater_than => rpo t2 t1                      | Some Less_than => rpo t1 t2                      | _ => True                      end. Proof. intros rpo_infos n; induction n as [ | n]. intros t1 t2 _ _. simpl. case_eq (find t1 t2 (rpo_l rpo_infos)). intros Hfind;apply (find_is_sound rpo _ (rpo_l_valid rpo_infos) _ _ (Hfind)). intro; case_eq (find t2 t1 (rpo_l rpo_infos)). intros Hfind;apply (find_is_sound rpo _ (rpo_l_valid rpo_infos) _ _ (Hfind)). intro. case_eq (find t1 t2 (equiv_l rpo_infos)). intros Hfind;apply (find_is_sound equiv _ (equiv_l_valid rpo_infos) _ _ (Hfind)). intro; case_eq (find t2 t1 (equiv_l rpo_infos)). intros Hfind;apply equiv_sym. apply equiv_equiv. apply (find_is_sound equiv _ (equiv_l_valid rpo_infos) _ _ (Hfind)). tauto. intros t1 t2 W1 W2; rewrite rpo_eval_equation. case_eq (find t1 t2 (rpo_l rpo_infos)). intros Hfind;apply (find_is_sound rpo _ (rpo_l_valid rpo_infos) _ _ (Hfind)). intros _; case_eq (find t2 t1 (rpo_l rpo_infos)). intros Hfind;apply (find_is_sound rpo _ (rpo_l_valid rpo_infos) _ _ (Hfind)). intros _. case_eq (find t1 t2 (equiv_l rpo_infos)). intros Hfind;apply (find_is_sound equiv _ (equiv_l_valid rpo_infos) _ _ (Hfind)). intros _; case_eq (find t2 t1 (equiv_l rpo_infos)). intros Hfind;apply equiv_sym. apply equiv_equiv. apply (find_is_sound equiv _ (equiv_l_valid rpo_infos) _ _ (Hfind)). intros _. assert (E1 := equiv_eval_is_sound_weak rpo_infos (S n) t1 t2); destruct (equiv_eval rpo_infos (S n) t1 t2) as [ [ | ] | ]. apply E1; trivial. clear E1; assert (H : forall v f l, var_in_term_list v l = true -> rpo (Var v) (Term f l)). intros v f l H; apply trans_clos_subterm_rpo; trivial. assert (H' : (In (Var v) l \/                   (exists t, In t l /\ trans_clos direct_subterm (Var v) t)) ->                      trans_clos direct_subterm (Var v) (Term f l)). intros [v_in_l | [t [t_in_l H']]]. apply closure.t_step; trivial. apply trans_clos_is_trans with t; trivial; apply closure.t_step; trivial. apply H'; clear H'. generalize H; clear H; pattern l; refine (list_rec3 size _ _ _); clear l. intros m; induction m as [ | m]; intros [ | t l] L. intros; discriminate. simpl in L; absurd (1 <= 0); auto with arith; refine (le_trans _ _ _ _ L); apply le_trans with (size t); auto with arith; apply size_ge_one. intros; discriminate. simpl in L; assert (Sl : list_size size l <= m). apply le_S_n; refine (le_trans _ _ _ _ L); apply (plus_le_compat_r 1 (size t) (list_size size l)); apply size_ge_one. destruct t as [v' | f' l']; rewrite var_in_term_list_equation. destruct (X.eq_dec v v') as [v_eq_v' | v_diff_v']. intros _; left; subst; left; trivial. intro H; destruct (IHm _ Sl H) as [v_in_l | [t [t_in_l H']]]. left; right; trivial. right; exists t; split; trivial; right; trivial. assert (Sl' : list_size size l' <= m). apply le_S_n; refine (le_trans _ _ _ _ L); rewrite size_unfold; simpl; apply le_n_S; auto with arith. generalize (IHm _ Sl'); destruct (var_in_term_list v l'). intro H; destruct (H (refl_equal _)) as [v_in_l' | [t [t_in_l' H']]]. right; exists (Term f' l'); split. left; trivial. apply closure.t_step; trivial. right; exists (Term f' l'); split. left; trivial. apply trans_clos_is_trans with t; trivial; apply closure.t_step; trivial. intros _; generalize (IHm _ Sl); destruct (var_in_term_list v l). intro H; destruct (H (refl_equal _)) as [v_in_l' | [t [t_in_l' H']]]. left; right; trivial. right; exists t; split; trivial; right; trivial. intros; discriminate. destruct t1 as [v1 | f1 l1]; destruct t2 as [v2 | f2 l2]; trivial. generalize (H v1 f2 l2); destruct (var_in_term_list v1 l2); intro H'; trivial; apply H'; trivial. generalize (H v2 f1 l1); destruct (var_in_term_list v2 l1); intro H'; trivial; apply H'; trivial. generalize (list_exists_option_is_sound   (fun t : term =>         match rpo_eval rpo_infos n t (Term f2 l2) with         | Some Equivalent => Some true         | Some Less_than => Some false         | Some Greater_than => Some true         | Some Uncomparable => Some false         | None => None (A:=bool)         end) l1); destruct (list_exists_option      (fun t : term =>       match rpo_eval rpo_infos n t (Term f2 l2) with       | Some Equivalent => Some true       | Some Less_than => Some false       | Some Greater_than => Some true       | Some Uncomparable => Some false       | None => None (A:=bool)       end) l1) as [ [ | ] | ]. intros [t1 [t1_in_l1 t1_gt_f2l2]]; simpl; apply Subterm with t1; trivial. apply in_impl_mem; trivial. assert (Wt1 : well_formed t1). destruct (well_formed_unfold _ W1) as [W _]; apply W; trivial. generalize (IHn t1 (Term f2 l2) Wt1 W2); destruct (rpo_eval rpo_infos n t1 (Term f2 l2)) as [ [ | | | ] | ]; try discriminate. intro H1; apply Equiv; apply (equiv_sym _ _ equiv_equiv); trivial. intro H1; apply Lt; trivial. intros _; generalize (list_exists_option_is_sound   (fun t : term =>         match rpo_eval rpo_infos n (Term f1 l1) t with         | Some Equivalent => Some true         | Some Less_than => Some true         | Some Greater_than => Some false         | Some Uncomparable => Some false         | None => None (A:=bool)         end) l2); destruct (list_exists_option      (fun t : term =>       match rpo_eval rpo_infos n (Term f1 l1) t with       | Some Equivalent => Some true       | Some Less_than => Some true       | Some Greater_than => Some false       | Some Uncomparable => Some false       | None => None (A:=bool)       end) l2) as [ [ | ] | ]. intros [t2 [t2_in_l2 t2_gt_f1l1]]; simpl; apply Subterm with t2; trivial. apply in_impl_mem; trivial. assert (Wt2 : well_formed t2). destruct (well_formed_unfold _ W2) as [W _]; apply W; trivial. generalize (IHn (Term f1 l1) t2 W1 Wt2); destruct (rpo_eval rpo_infos n (Term f1 l1) t2) as [ [ | | | ] | ]; try discriminate. intro; apply Equiv; trivial. intro; apply Lt; trivial. assert (Wl1 : well_formed_list l1). destruct W1; trivial. assert (Wl2 : well_formed_list l2). destruct W2; trivial. intros _; generalize (prec_eval_is_sound f1 f2); destruct (prec_eval f1 f2). intro f1_eq_f2; assert (Sf1 := f_equal status f1_eq_f2); destruct (status f2); subst f2; rewrite Sf1. assert (L : length l1 = length l2). destruct (well_formed_unfold _ W1) as [_ Ll1]; destruct (well_formed_unfold _ W2) as [_ Ll2]; destruct (F.arity f1) as [ | | m]; rewrite Ll1; rewrite Ll2; trivial. simpl; assert (H' := lexico_eval_is_sound (rpo_eval rpo_infos n) (Term f1 l1)                                 (Term f1 l2) l1 l2 L); destruct (lexico_eval (rpo_eval rpo_infos n) (Term f1 l1) (Term f1 l2) l1 l2) as [ [ | | | ] | ]. destruct H' as [ll [E_ll [H1 H2]]]; trivial. apply (Eq_lex f1 l1 l2 Sf1); trivial. assert (E_ll' : forall t1 t2, In (t1,t2) ll -> equiv t1 t2). intros t1 t2 t1t2_in_ll; assert (Wt1 : well_formed t1). apply (well_formed_list_is_well_formed_list _ (proj1 W1)). rewrite H1; apply in_impl_mem; setoid_rewrite in_map_iff; exists (t1,t2); simpl; split; trivial. assert (Wt2 : well_formed t2). apply (well_formed_list_is_well_formed_list _ (proj1 W2)). rewrite H2; apply in_impl_mem; setoid_rewrite in_map_iff; exists (t1,t2); simpl; split; trivial. assert (H' := IHn t1 t2 Wt1 Wt2). rewrite (E_ll t1 t2 t1t2_in_ll) in H'; trivial. rewrite H1; rewrite H2; clear E_ll H1 H2; induction ll as [ | [t1 t2] ll]. apply Eq_list_nil. simpl; apply Eq_list_cons. apply E_ll'; left; trivial. apply IHll; intros; apply E_ll'; right; trivial. destruct H' as [ll [t1 [t2 [l1' [l2' [E_ll [t1_lt_t2 [H'' [H1 H2]]]]]]]]]; apply Top_eq_lex; trivial. subst l1 l2; generalize t1 t2 l1' l2' E_ll t1_lt_t2 Wl1 Wl2 L; clear H'' t1 t2 l1' l2' E_ll t1_lt_t2 Wl1 Wl2 W1 W2 L; induction ll as [ | [u1 u2]]; intros t1 t2 l1' l2' E_ll t1_lt_t2 Wl1 Wl2 L. subst; simpl; apply List_gt. assert (Wt1 : well_formed t1). apply (well_formed_list_is_well_formed_list _ Wl1); simpl; left; reflexivity. assert (Wt2 : well_formed t2). apply (well_formed_list_is_well_formed_list _ Wl2); simpl; left; reflexivity. assert (H'' := IHn t1 t2 Wt1 Wt2). rewrite t1_lt_t2 in H''; trivial. simpl in L; injection L; trivial. simpl; apply List_eq. assert (Wu1 : well_formed u1). apply (well_formed_list_is_well_formed_list _ Wl1). simpl; left; reflexivity. assert (Wu2 : well_formed u2). apply (well_formed_list_is_well_formed_list _ Wl2). simpl; left; reflexivity. assert (H'' := IHn u1 u2 Wu1 Wu2). rewrite (E_ll u1 u2) in H''; trivial; left; trivial. apply IHll; trivial. intros; apply E_ll; right; trivial. destruct Wl1; trivial. destruct Wl2; trivial. simpl in L; injection L; trivial. intros u1 u1_mem_l1; destruct (mem_split_set _ _ u1_mem_l1) as [u1' [k1' [k1'' [u1_eq_u1' H']]]]. simpl in u1_eq_u1'; setoid_rewrite (equiv_rpo_equiv_2 _ _ u1_eq_u1'). assert (u1'_in_l1 : In u1' l1). simpl in H'; rewrite H'; apply in_or_app; right; left; trivial. assert (Wu1 : well_formed u1'). apply (well_formed_list_is_well_formed_list _ Wl1); apply in_impl_mem; trivial. destruct (H'' u1' u1'_in_l1) as [[u2 [u2_in_l2 u1_le_u2]] | u1_lt_s2]. assert (Wu2 : well_formed u2). apply (well_formed_list_is_well_formed_list _ Wl2); apply in_impl_mem; trivial. apply Subterm with u2. apply in_impl_mem; trivial. assert (H''' := IHn u1' u2 Wu1 Wu2). destruct u1_le_u2 as [u1_eq_u2 | u1_lt_u2]. rewrite u1_eq_u2 in H'''; apply Equiv; trivial. rewrite u1_lt_u2 in H'''; apply Lt; trivial. assert (H''' := IHn u1' _ Wu1 W2); rewrite u1_lt_s2 in H'''; trivial. destruct H' as [ll [t1 [t2 [l1' [l2' [E_ll [t1_lt_t2 [H'' [H1 H2]]]]]]]]]; apply Top_eq_lex; trivial. subst l1 l2; generalize t1 t2 l1' l2' E_ll t1_lt_t2 Wl1 Wl2 L; clear H'' t1 t2 l1' l2' E_ll t1_lt_t2 Wl1 Wl2 W1 W2 L; induction ll as [ | [u1 u2]]; intros t1 t2 l1' l2' E_ll t1_lt_t2 Wl1 Wl2 L. subst; simpl; apply List_gt. assert (Wt1 : well_formed t1). apply (well_formed_list_is_well_formed_list _ Wl1); simpl; left; reflexivity. assert (Wt2 : well_formed t2). apply (well_formed_list_is_well_formed_list _ Wl2); simpl; left; reflexivity. assert (H'' := IHn t1 t2 Wt1 Wt2). rewrite t1_lt_t2 in H''; trivial. simpl in L; injection L; intro; apply sym_eq; trivial. simpl; apply List_eq. apply (equiv_sym _ _ equiv_equiv); assert (Wu1 : well_formed u1). apply (well_formed_list_is_well_formed_list _ Wl1). simpl; left; reflexivity. assert (Wu2 : well_formed u2). apply (well_formed_list_is_well_formed_list _ Wl2). simpl; left; reflexivity. assert (H'' := IHn u1 u2 Wu1 Wu2). rewrite (E_ll u1 u2) in H''; trivial; left; trivial. apply IHll; trivial. intros; apply E_ll; right; trivial. destruct Wl1; trivial. destruct Wl2; trivial. simpl in L; injection L; trivial. intros u2 u2_mem_l2; destruct (mem_split_set _ _ u2_mem_l2) as [u2' [k2' [k2'' [u2_eq_u2' H']]]]. simpl in u2_eq_u2'; setoid_rewrite (equiv_rpo_equiv_2 _ _ u2_eq_u2'). assert (u2'_in_l2 : In u2' l2). simpl in H'; rewrite H'; apply in_or_app; right; left; trivial. assert (Wu2 : well_formed u2'). apply (well_formed_list_is_well_formed_list _ Wl2); apply in_impl_mem; trivial. destruct (H'' u2' u2'_in_l2) as [[u1 [u1_in_l1 u2_le_u1]] | u2_lt_s1]. assert (Wu1 : well_formed u1). apply (well_formed_list_is_well_formed_list _ Wl1); apply in_impl_mem; trivial. apply Subterm with u1; trivial. apply in_impl_mem; trivial. assert (H''' := IHn u1 u2' Wu1 Wu2). destruct u2_le_u1 as [u2_eq_u1 | u2_lt_u1]. rewrite u2_eq_u1 in H'''; apply Equiv; apply (equiv_sym _ _ equiv_equiv); trivial. rewrite u2_lt_u1 in H'''; apply Lt; trivial. assert (H''' := IHn _ u2' W1 Wu2); rewrite u2_lt_s1 in H'''; trivial. trivial. trivial. simpl; assert (H' := remove_equiv_eval_list_is_sound (equiv_eval rpo_infos n) l1 l2); destruct (remove_equiv_eval_list (equiv_eval rpo_infos n) l1 l2) as [ [[ | t1' l1'] [ | t2' l2']] | ]. destruct H' as [ll [E_ll [P1 [P2 _]]]]; apply (Eq_mul f1 l1 l2 Sf1); trivial. simpl in P1; simpl in P2. apply permut_trans with (map (fun st : term * term => fst st) ll); trivial. apply permut_impl with (@eq term); trivial; intros; subst; reflexivity. apply permut_trans with (map (fun st : term * term => snd st) ll); trivial. assert (E_ll' : forall t1 t2, In (t1,t2) ll -> equiv t1 t2). intros t1 t2 t1t2_in_ll; assert (Wt1 : well_formed t1). apply (well_formed_list_is_well_formed_list _ (proj1 W1)). apply in_impl_mem; setoid_rewrite (in_permut_in P1). setoid_rewrite in_map_iff; exists (t1,t2); simpl; split; trivial. assert (Wt2 : well_formed t2). apply (well_formed_list_is_well_formed_list _ (proj1 W2)). apply in_impl_mem; setoid_rewrite (in_permut_in P2). setoid_rewrite in_map_iff; exists (t1,t2); simpl; split; trivial. assert (H' := equiv_eval_is_sound_weak rpo_infos n t1 t2); rewrite (E_ll t1 t2 t1t2_in_ll) in H'; apply H'; trivial. clear E_ll P1 P2; induction ll as [ | [t1 t2] ll]. reflexivity. simpl; setoid_rewrite <- permut_cons. apply E_ll'; left; trivial. apply IHll. intros; apply E_ll'; right; trivial. symmetry; apply permut_impl with (@eq term); trivial; intros; subst; reflexivity. destruct H' as [ll [E_ll [P1 [P2 _]]]]. apply Top_eq_mul; trivial. apply (List_mul t2' l2' nil l1); trivial. reflexivity. transitivity ((t2' :: l2') ++ (map (fun st : term * term => snd st) ll)). apply permut_impl with (@eq term); trivial; intros; subst; reflexivity. rewrite app_comm_cons; setoid_rewrite <- permut_app1. transitivity (map (fun st : term * term => fst st) ll). symmetry. assert (E_ll' : forall t1 t2, In (t1,t2) ll -> equiv t1 t2). intros t1 t2 t1t2_in_ll; assert (Wt1 : well_formed t1). apply (well_formed_list_is_well_formed_list _ (proj1 W1)). apply in_impl_mem; setoid_rewrite (in_permut_in P1). simpl; setoid_rewrite in_map_iff; exists (t1,t2); simpl; split; trivial. assert (Wt2 : well_formed t2). apply (well_formed_list_is_well_formed_list _ (proj1 W2)). apply in_impl_mem; setoid_rewrite (in_permut_in P2). apply in_or_app; right; setoid_rewrite in_map_iff; exists (t1,t2); simpl; split; trivial. assert (H' := equiv_eval_is_sound_weak rpo_infos n t1 t2); rewrite (E_ll t1 t2 t1t2_in_ll) in H'; apply H'; trivial. clear E_ll P1 P2; induction ll as [ | [t1 t2] ll]. reflexivity. simpl; setoid_rewrite <- permut_cons. apply E_ll'; left; trivial. apply IHll. intros; apply E_ll'; right; trivial. symmetry; apply permut_impl with (@eq term); trivial; intros; subst; reflexivity. intros; contradiction. destruct H' as [ll [E_ll [P1 [P2 _]]]]. apply Top_eq_mul; trivial. apply (List_mul t1' l1' nil l2); trivial. reflexivity. transitivity ((t1' :: l1') ++ (map (fun st : term * term => fst st) ll)). apply permut_impl with (@eq term); trivial; intros; subst; reflexivity. rewrite app_comm_cons; setoid_rewrite <- permut_app1. transitivity (map (fun st : term * term => snd st) ll). assert (E_ll' : forall t1 t2, In (t1,t2) ll -> equiv t1 t2). intros t1 t2 t1t2_in_ll; assert (Wt1 : well_formed t1). apply (well_formed_list_is_well_formed_list _ (proj1 W1)). apply in_impl_mem; setoid_rewrite (in_permut_in P1). apply in_or_app; right; setoid_rewrite in_map_iff; exists (t1,t2); simpl; split; trivial. assert (Wt2 : well_formed t2). apply (well_formed_list_is_well_formed_list _ (proj1 W2)). apply in_impl_mem; setoid_rewrite (in_permut_in P2). simpl; setoid_rewrite in_map_iff; exists (t1,t2); simpl; split; trivial. assert (H' := equiv_eval_is_sound_weak rpo_infos n t1 t2); rewrite (E_ll t1 t2 t1t2_in_ll) in H'; apply H'; trivial. clear E_ll P1 P2; induction ll as [ | [t1 t2] ll]. reflexivity. simpl; setoid_rewrite <- permut_cons. apply E_ll'; left; trivial. apply IHll. intros; apply E_ll'; right; trivial. symmetry; apply permut_impl with (@eq term); trivial; intros; subst; reflexivity. intros; contradiction. assert (H'' := mult_eval_is_sound_weak (rpo_eval rpo_infos n) (t1' :: l1') (t2' :: l2')). destruct (mult_eval (rpo_eval rpo_infos n) (t1' :: l1') (t2' :: l2')) as [ [ | | | ] | ]. contradiction. destruct H' as [ll [E_ll [P1 [P2 _]]]]. assert (E_ll' : forall t1 t2, In (t1,t2) ll -> equiv t1 t2). intros t1 t2 t1t2_in_ll; assert (H' := equiv_eval_is_sound_weak rpo_infos n t1 t2); rewrite (E_ll t1 t2 t1t2_in_ll) in H'; apply H'; trivial. apply Top_eq_mul; trivial. apply (List_mul t2' l2' (t1' :: l1') (map (fun st : term * term => fst st) ll)); trivial. apply permut_impl with (@eq term); trivial; intros; subst; reflexivity. transitivity ((t2' :: l2') ++ map (fun st : term * term => snd st) ll). apply permut_impl with (@eq term); trivial; intros; subst; reflexivity. rewrite app_comm_cons; setoid_rewrite <- permut_app1. clear E_ll P1 P2; induction ll as [ | [t1 t2] ll]. reflexivity. simpl; setoid_rewrite <- permut_cons. symmetry; apply E_ll'; left; trivial. apply IHll. intros; apply E_ll'; right; trivial. intros u1 u1_mem_l1'. destruct (mem_split_set _ _ u1_mem_l1') as [u1' [k1 [k1' [u1_eq_u1' H']]]]. simpl in u1_eq_u1'; simpl in H'. assert (u1'_in_l1' : In u1' (t1' :: l1')). rewrite H'; apply in_or_app; right; left; trivial. destruct (H'' _ u1'_in_l1') as [u2 [u2_in_l2' u1_lt_u2]]; exists u2; split. apply in_impl_mem; trivial. assert (Wu1 : well_formed u1'). apply (well_formed_list_is_well_formed_list _ Wl1). apply in_impl_mem; setoid_rewrite (in_permut_in P1); apply in_or_app; left; trivial. assert (Wu2 : well_formed u2). apply (well_formed_list_is_well_formed_list _ Wl2); apply in_impl_mem; setoid_rewrite (in_permut_in P2); apply in_or_app; left; trivial. assert (H''' := IHn u1' u2 Wu1 Wu2). rewrite u1_lt_u2 in H'''. setoid_rewrite (equiv_rpo_equiv_2 _ _ u1_eq_u1'); trivial. destruct H' as [ll [E_ll [P1 [P2 _]]]]. assert (E_ll' : forall t1 t2, In (t1,t2) ll -> equiv t1 t2). intros t1 t2 t1t2_in_ll; assert (H' := equiv_eval_is_sound_weak rpo_infos n t1 t2); rewrite (E_ll t1 t2 t1t2_in_ll) in H'; apply H'; trivial. apply Top_eq_mul; trivial. apply (List_mul t1' l1' (t2' :: l2') (map (fun st : term * term => fst st) ll)); trivial. transitivity ((t2' :: l2') ++ map (fun st : term * term => snd st) ll). apply permut_impl with (@eq term); trivial; intros; subst; reflexivity. setoid_rewrite <- permut_app1. clear E_ll P1 P2; induction ll as [ | [t1 t2] ll]. reflexivity. simpl; setoid_rewrite <- permut_cons. symmetry; apply E_ll'; left; trivial. apply IHll. intros; apply E_ll'; right; trivial. apply permut_impl with (@eq term); trivial; intros; subst; reflexivity. intros u2 u2_mem_l2'. destruct (mem_split_set _ _ u2_mem_l2') as [u2' [k2 [k2' [u2_eq_u2' H']]]]. simpl in u2_eq_u2'; simpl in H'. assert (u2'_in_l2' : In u2' (t2' :: l2')). rewrite H'; apply in_or_app; right; left; trivial. destruct (H'' _ u2'_in_l2') as [u1 [u1_in_l1' u2_lt_u1]]; exists u1; split. apply in_impl_mem; trivial. assert (Wu2 : well_formed u2'). apply (well_formed_list_is_well_formed_list _ Wl2). apply in_impl_mem; setoid_rewrite (in_permut_in P2); apply in_or_app; left; trivial. assert (Wu1 : well_formed u1). apply (well_formed_list_is_well_formed_list _ Wl1); apply in_impl_mem; setoid_rewrite (in_permut_in P1); apply in_or_app; left; trivial. assert (H''' := IHn u1 u2' Wu1 Wu2). rewrite u2_lt_u1 in H'''. setoid_rewrite (equiv_rpo_equiv_2 _ _ u2_eq_u2'); trivial. trivial. trivial. trivial. intro f1_lt_f2; simpl. generalize (list_forall_option_is_sound       (fun t : term =>        match rpo_eval rpo_infos n t (Term f2 l2) with        | Some Equivalent => Some false        | Some Less_than => Some true        | Some Greater_than => Some false        | Some Uncomparable => Some false        | None => None (A:=bool)        end) l1); destruct (list_forall_option       (fun t : term =>        match rpo_eval rpo_infos n t (Term f2 l2) with        | Some Equivalent => Some false        | Some Less_than => Some true        | Some Greater_than => Some false        | Some Uncomparable => Some false        | None => None (A:=bool)        end) l1) as [ [ | ] | ]. intros l1_lt_s2; apply Top_gt; trivial. intros t1 t1_mem_l1; destruct (mem_split_set _ _ t1_mem_l1) as [t1' [k1 [k1' [t1_eq_t1' H']]]]. simpl in t1_eq_t1'; simpl in H'. assert (t1'_in_l1 : In t1' l1). rewrite H'; apply in_or_app; right; left; trivial. assert (Wt1 : well_formed t1'). apply (well_formed_list_is_well_formed_list _ Wl1); apply in_impl_mem; trivial. setoid_rewrite (equiv_rpo_equiv_2 _ _ t1_eq_t1'). assert (H'' := l1_lt_s2 t1' t1'_in_l1); assert (H''' := IHn _ _ Wt1 W2); destruct (rpo_eval rpo_infos n t1' (Term f2 l2)) as [ [ | | | ] | ]; trivial; discriminate. trivial. trivial. intro f2_lt_f1; simpl. generalize (list_forall_option_is_sound       (fun t : term =>        match rpo_eval rpo_infos n (Term f1 l1) t with        | Some Equivalent => Some false        | Some Less_than => Some false        | Some Greater_than => Some true        | Some Uncomparable => Some false        | None => None (A:=bool)        end) l2); destruct (list_forall_option       (fun t : term =>        match rpo_eval rpo_infos n (Term f1 l1) t with        | Some Equivalent => Some false        | Some Less_than => Some false        | Some Greater_than => Some true        | Some Uncomparable => Some false        | None => None (A:=bool)        end) l2) as [ [ | ] | ]. intros s1_gt_l2; apply Top_gt; trivial. intros t2 t2_mem_l2; destruct (mem_split_set _ _ t2_mem_l2) as [t2' [k2 [k2' [t2_eq_t2' H']]]]. simpl in t2_eq_t2'; simpl in H'. assert (t2'_in_l2 : In t2' l2). rewrite H'; apply in_or_app; right; left; trivial. assert (Wt2 : well_formed t2'). apply (well_formed_list_is_well_formed_list _ Wl2); apply in_impl_mem; trivial. setoid_rewrite (equiv_rpo_equiv_2 _ _ t2_eq_t2'). assert (H'' := s1_gt_l2 t2' t2'_in_l2); assert (H''' := IHn _ _ W1 Wt2); destruct (rpo_eval rpo_infos n (Term f1 l1) t2') as [ [ | | | ] | ]; trivial; discriminate. trivial. trivial. simpl; trivial. simpl; trivial. simpl; trivial. trivial. Qed. Lemma lexico_eval_fully_evaluates :   forall p s1 s2 l1 l2,   (forall t1, In t1 l1 -> p t1 s2 <> None) ->   (forall t2, In t2 l2 -> p s1 t2 <> None) ->   (forall t1 t2, In t1 l1 -> In t2 l2 -> p t1 t2 <> None) ->   lexico_eval p s1 s2 l1 l2 <> None. Proof. intros p s1 s2 l1; induction l1 as [ | t1 l1]; intros [ | t2 l2] Es2 Es1 E; simpl; try discriminate. assert (H := E t1 t2 (or_introl _ (refl_equal _)) (or_introl _ (refl_equal _))); destruct (p t1 t2) as [ [ | | | ] | ]. apply IHl1; intros; [apply Es2 | apply Es1 | apply E]; right; trivial. generalize (list_forall_option_is_sound       (fun t3 : term =>        match p t3 s2 with        | Some Equivalent => Some false        | Some Less_than => Some true        | Some Greater_than => Some false        | Some Uncomparable => Some false        | None => None (A:=bool)        end) l1); destruct (list_forall_option       (fun t3 : term =>        match p t3 s2 with        | Some Equivalent => Some false        | Some Less_than => Some true        | Some Greater_than => Some false        | Some Uncomparable => Some false        | None => None (A:=bool)        end) l1) as [ [ | ] | ]. clear H; assert (H := Es2 t1 (or_introl _ (refl_equal _))); destruct (p t1 s2) as [ [ | | | ] | ]. intros _; discriminate. intros _; discriminate. intros _; discriminate. intros _; discriminate. intros _; apply H; trivial. clear H; assert (H := Es2 t1 (or_introl _ (refl_equal _))); destruct (p t1 s2) as [ [ | | | ] | ]. intros _; discriminate. intros _; discriminate. intros _; discriminate. intros _; discriminate. intros _; apply H; trivial. intros [u1 [u1_in_l1 pt1s2_eq_none]]; assert (H' := Es2 _ (or_intror _ u1_in_l1)); destruct (p u1 s2) as [ [ | | | ] | ]; trivial. discriminate. discriminate. discriminate. discriminate. absurd (@None comp = None); trivial. generalize (list_forall_option_is_sound         (fun t3 : term =>          match p s1 t3 with          | Some Equivalent => Some false          | Some Less_than => Some false          | Some Greater_than => Some true          | Some Uncomparable => Some false          | None => None (A:=bool)          end) l2); destruct (list_forall_option         (fun t3 : term =>          match p s1 t3 with          | Some Equivalent => Some false          | Some Less_than => Some false          | Some Greater_than => Some true          | Some Uncomparable => Some false          | None => None (A:=bool)          end) l2) as [ [ | ] | ]. clear H; assert (H := Es1 t2 (or_introl _ (refl_equal _))); destruct (p s1 t2) as [ [ | | | ] | ]. intros _; discriminate. intros _; discriminate. intros _; discriminate. intros _; discriminate. intros _; apply H; trivial. clear H; assert (H := Es1 t2 (or_introl _ (refl_equal _))); destruct (p s1 t2) as [ [ | | | ] | ]. intros _; discriminate. intros _; discriminate. intros _; discriminate. intros _; discriminate. intros _; apply H; trivial. intros [u2 [u2_in_l2 ps1u2_eq_none]]; assert (H' := Es1 _ (or_intror _ u2_in_l2)); destruct (p s1 u2) as [ [ | | | ] | ]; trivial. discriminate. discriminate. discriminate. discriminate. absurd (@None comp = None); trivial. discriminate. trivial. Qed. Lemma mult_eval_fully_evaluates :   forall p l1 l2,   (forall t1 t2, In t1 l1 -> In t2 l2 -> p t1 t2 <> None) ->   mult_eval p l1 l2 <> None. Proof. intros p [ | t1 l1] l2 E; unfold mult_eval. simpl; clear E; induction l2 as [ | t2 l2]; simpl. discriminate. destruct (list_forall_option (fun _ : term => Some false) l2) as [ [ | ] | ]; trivial; discriminate. generalize (list_forall_option_is_sound     (fun t2 : term =>      list_exists_option        (fun t3 : term =>         match p t3 t2 with         | Some Equivalent => Some false         | Some Less_than => Some false         | Some Greater_than => Some true         | Some Uncomparable => Some false         | None => None (A:=bool)         end) (t1 :: l1)) l2); destruct (list_forall_option     (fun t2 : term =>      list_exists_option        (fun t3 : term =>         match p t3 t2 with         | Some Equivalent => Some false         | Some Less_than => Some false         | Some Greater_than => Some true         | Some Uncomparable => Some false         | None => None (A:=bool)         end) (t1 :: l1)) l2) as [ [ | ] | ]. intros _; discriminate. intros _; generalize (list_forall_option_is_sound     (fun t2 : term =>      list_exists_option        (fun t3 : term =>         match p t2 t3 with         | Some Equivalent => Some false         | Some Less_than => Some true         | Some Greater_than => Some false         | Some Uncomparable => Some false         | None => None (A:=bool)         end) l2) (t1 :: l1)); destruct (list_forall_option     (fun t2 : term =>      list_exists_option        (fun t3 : term =>         match p t2 t3 with         | Some Equivalent => Some false         | Some Less_than => Some true         | Some Greater_than => Some false         | Some Uncomparable => Some false         | None => None (A:=bool)         end) l2) (t1 :: l1)) as [ [ | ] | ]. intros _; discriminate. intros _; discriminate. intros [u1 [u1_in_l1 H]]. assert (H' := list_exists_option_is_sound       (fun t3 : term =>        match p u1 t3 with        | Some Equivalent => Some false        | Some Less_than => Some true        | Some Greater_than => Some false        | Some Uncomparable => Some false        | None => None (A:=bool)        end) l2); rewrite H in H'. destruct H' as [ [u2 [u2_in_l2 pu1u2_eq_none]] _]. assert (H' := E u1 u2 u1_in_l1 u2_in_l2); destruct (p u1 u2) as [ [ | | | ] | ]; trivial; discriminate. intros [u2 [u2_in_l2 H]]. assert (H' := list_exists_option_is_sound       (fun t3 : term =>        match p t3 u2 with        | Some Equivalent => Some false        | Some Less_than => Some false        | Some Greater_than => Some true        | Some Uncomparable => Some false        | None => None (A:=bool)        end) (t1 :: l1)); rewrite H in H'. destruct H' as [ [u1 [u1_in_l1 pu1u2_eq_none]] _]. assert (H' := E u1 u2 u1_in_l1 u2_in_l2); destruct (p u1 u2) as [ [ | | | ] | ]; trivial; discriminate. Qed. Lemma rpo_eval_terminates :   forall rpo_infos n t1 t2, size t1 + size t2 <= n -> rpo_eval rpo_infos n t1 t2 <> None. Proof. intros rpo_infos n; induction n as [ | n]. intros t1 t2 St1; absurd (1 <= 0); auto with arith; apply le_trans with (size t1 + size t2); trivial; apply le_trans with (1 + size t2); [apply le_plus_l | apply plus_le_compat_r; apply size_ge_one]. intros t1 t2 St; rewrite rpo_eval_equation. case (find t1 t2 (rpo_l rpo_infos)). intro;discriminate. case (find t2 t1 (rpo_l rpo_infos)). intro;discriminate. case (find t1 t2 (equiv_l rpo_infos)). intro;discriminate. case (find t2 t1 (equiv_l rpo_infos)). intro;discriminate. assert (T := equiv_eval_terminates rpo_infos (S n) t1 t2 St); destruct (equiv_eval rpo_infos (S n) t1 t2) as [ [ | ] | ]; try discriminate. destruct t1 as [v1 | f1 l1]; destruct t2 as [v2 | f2 l2]. discriminate. destruct (var_in_term_list v1 l2); discriminate. destruct (var_in_term_list v2 l1); discriminate. generalize (list_exists_option_is_sound (fun t : term =>       match rpo_eval rpo_infos n t (Term f2 l2) with       | Some Equivalent => Some true       | Some Less_than => Some false       | Some Greater_than => Some true       | Some Uncomparable => Some false       | None => None (A:=bool)       end) l1); destruct (list_exists_option     (fun t : term =>      match rpo_eval rpo_infos n t (Term f2 l2) with      | Some Equivalent => Some true      | Some Less_than => Some false      | Some Greater_than => Some true      | Some Uncomparable => Some false      | None => None (A:=bool)      end) l1) as [ [ | ] | ]. intros _; simpl; discriminate. intros _; generalize (list_exists_option_is_sound (fun t : term =>          match rpo_eval rpo_infos n (Term f1 l1) t with          | Some Equivalent => Some true          | Some Less_than => Some true          | Some Greater_than => Some false          | Some Uncomparable => Some false          | None => None (A:=bool)          end) l2); destruct (list_exists_option         (fun t : term =>          match rpo_eval rpo_infos n (Term f1 l1) t with          | Some Equivalent => Some true          | Some Less_than => Some true          | Some Greater_than => Some false          | Some Uncomparable => Some false          | None => None (A:=bool)          end) l2) as [ [ | ] | ]. intros _; simpl; discriminate. intros _; simpl; destruct (prec_eval f1 f2); try discriminate. destruct (status f1). apply lexico_eval_fully_evaluates. intros t1 t1_in_l1; apply IHn. apply le_S_n; refine (le_trans _ _ _ _ St); replace (S (size t1 + size (Term f2 l2))) with                 (S (size t1) + size (Term f2 l2)); trivial; apply plus_le_compat_r; apply size_direct_subterm; trivial. intros t2 t2_in_l2; apply IHn. apply le_S_n; refine (le_trans _ _ _ _ St); rewrite plus_comm; replace (S (size t2 + size (Term f1 l1))) with                 (S (size t2) + size (Term f1 l1)); trivial; rewrite plus_comm; apply plus_le_compat_l; apply size_direct_subterm; trivial. intros t1 t2 t1_in_l1 t2_in_l2; apply IHn. apply le_S_n; refine (le_trans _ _ _ _ St); replace (S (size t1 + size t2)) with (S (size t1) + size t2); trivial; apply plus_le_compat. apply size_direct_subterm; trivial. apply lt_le_weak; apply size_direct_subterm; trivial. generalize (remove_equiv_eval_list_is_sound (equiv_eval rpo_infos n) l1 l2); destruct (remove_equiv_eval_list (equiv_eval rpo_infos n) l1 l2) as [ [[ | t1' l1'] [ | t2' l2']] | ]. intros; discriminate. intros; discriminate. intros; discriminate. intros [ll [_ [P1 [P2 _]]]]; apply mult_eval_fully_evaluates. intros t1 t2 t1_in_l1' t2_in_l2'; apply IHn. apply le_S_n; refine (le_trans _ _ _ _ St); replace (S (size t1 + size t2)) with (S (size t1) + size t2); trivial; apply plus_le_compat. apply size_direct_subterm; simpl; setoid_rewrite (in_permut_in P1); apply in_or_app; left; trivial. apply lt_le_weak; apply size_direct_subterm; simpl; setoid_rewrite (in_permut_in P2); apply in_or_app; left; trivial. intros [t1 [t2 [t1_in_l1 [t2_in_l2 H]]]]; assert (H' := equiv_eval_terminates rpo_infos n t1 t2); destruct (equiv_eval rpo_infos n t1 t2) as [ [ | ] | ]. discriminate. discriminate. intros _; apply H'; trivial. apply le_S_n; refine (le_trans _ _ _ _ St); replace (S (size t1 + size t2)) with (S (size t1) + size t2); trivial; apply plus_le_compat. apply size_direct_subterm; trivial. apply lt_le_weak; apply size_direct_subterm; trivial. generalize (list_forall_option_is_sound     (fun t : term =>      match rpo_eval rpo_infos n t (Term f2 l2) with      | Some Equivalent => Some false      | Some Less_than => Some true      | Some Greater_than => Some false      | Some Uncomparable => Some false      | None => None (A:=bool)      end) l1); destruct (list_forall_option     (fun t : term =>      match rpo_eval rpo_infos n t (Term f2 l2) with      | Some Equivalent => Some false      | Some Less_than => Some true      | Some Greater_than => Some false      | Some Uncomparable => Some false      | None => None (A:=bool)      end) l1) as [ [ | ] | ]. intros _; discriminate. intros _; discriminate. intros [u1 [u1_in_l1 H]]; assert (H' := IHn u1 (Term f2 l2)); destruct (rpo_eval rpo_infos n u1 (Term f2 l2)) as [ [ | | | ] | ]. discriminate. discriminate. discriminate. discriminate. apply H'. apply le_S_n; refine (le_trans _ _ _ _ St); replace (S (size u1 + size (Term f2 l2))) with                 (S (size u1) + size (Term f2 l2)); trivial; apply plus_le_compat_r; apply size_direct_subterm; trivial. generalize (list_forall_option_is_sound     (fun t : term =>      match rpo_eval rpo_infos n (Term f1 l1) t with      | Some Equivalent => Some false      | Some Less_than => Some false      | Some Greater_than => Some true      | Some Uncomparable => Some false      | None => None (A:=bool)      end) l2); destruct (list_forall_option     (fun t : term =>      match rpo_eval rpo_infos n (Term f1 l1) t with      | Some Equivalent => Some false      | Some Less_than => Some false      | Some Greater_than => Some true      | Some Uncomparable => Some false      | None => None (A:=bool)      end) l2) as [ [ | ] | ]. intros _; discriminate. intros _; discriminate. intros [u2 [u2_in_l2 H]]; assert (H' := IHn (Term f1 l1) u2); destruct (rpo_eval rpo_infos n (Term f1 l1) u2) as [ [ | | | ] | ]. discriminate. discriminate. discriminate. discriminate. apply H'. apply le_S_n; refine (le_trans _ _ _ _ St); rewrite plus_comm; replace (S (size u2 + size (Term f1 l1))) with                 (S (size u2) + size (Term f1 l1)); trivial; rewrite plus_comm; apply plus_le_compat_l; apply size_direct_subterm; trivial. intros [[u2 [u2_in_l2 H]] _]; assert (H' := IHn (Term f1 l1) u2); destruct (rpo_eval rpo_infos n (Term f1 l1) u2) as [ [ | | | ] | ]. discriminate. discriminate. discriminate. discriminate. apply H'. apply le_S_n; refine (le_trans _ _ _ _ St); rewrite plus_comm; replace (S (size u2 + size (Term f1 l1))) with                 (S (size u2) + size (Term f1 l1)); trivial; rewrite plus_comm; apply plus_le_compat_l; apply size_direct_subterm; trivial. intros [[u1 [u1_in_l1 H]] _]; assert (H' := IHn u1 (Term f2 l2)); destruct (rpo_eval rpo_infos n u1 (Term f2 l2)) as [ [ | | | ] | ]. discriminate. discriminate. discriminate. discriminate. apply H'. apply le_S_n; refine (le_trans _ _ _ _ St); replace (S (size u1 + size (Term f2 l2))) with                 (S (size u1) + size (Term f2 l2)); trivial; apply plus_le_compat_r; apply size_direct_subterm; trivial. intros _; apply T; trivial. Qed. Lemma rpo_eval_is_complete_equivalent :   forall rpo_infos n t1 t2, size t1 + size t2 <= n -> equiv t1 t2 ->         rpo_eval rpo_infos n t1 t2 = Some Equivalent. Proof. intros rpo_infos n t1 t2 St t1_eq_t2; rewrite rpo_eval_equation. case_eq (find t1 t2 (rpo_l rpo_infos)). intro abs. generalize (find_is_sound rpo _ (rpo_l_valid rpo_infos) _ _ abs). intro h;absurd (rpo t1 t1). intro;apply rpo_antirefl with (1:=H). rewrite <- (equiv_rpo_equiv_1 _ _ t1_eq_t2) in h. assumption. intro h1. case_eq (find t2 t1 (rpo_l rpo_infos)). intro abs. generalize (find_is_sound rpo _ (rpo_l_valid rpo_infos) _ _ abs). intro h;absurd (rpo t2 t2). intro;apply rpo_antirefl with (1:=H). rewrite (equiv_rpo_equiv_1 _ _ t1_eq_t2) in h. assumption. intro h2. case_eq (find t1 t2 (equiv_l rpo_infos)). trivial. intro h3. case_eq (find t2 t1 (equiv_l rpo_infos)). trivial. intro h4. assert (H := equiv_eval_is_sound rpo_infos _ _ _ St). destruct (equiv_eval rpo_infos n t1 t2) as [ [ | ] | ]. trivial. absurd (equiv t1 t2); trivial. contradiction. Qed. Lemma var_case2 :   forall v f l, rpo (Var v) (Term f l) -> var_in_term_list v l = true . Proof. intros v f l v_lt_t; inversion v_lt_t as [ f2 l2 u s s_in_l v_le_s | | | ]; subst. generalize s s_in_l v_le_s; clear v_lt_t s s_in_l v_le_s; pattern l; apply (list_rec3 size); clear l. intro n; induction n as [ | n]; intros [ | t l] Sl s s_in_l v_le_s. contradiction. simpl in Sl; absurd (1 <= 0); auto with arith. refine (le_trans _ _ _ _ Sl); apply le_trans with (size t). apply size_ge_one. apply le_plus_l. contradiction. simpl in s_in_l; destruct s_in_l as [s_eq_t | s_in_l]. setoid_rewrite (equiv_rpo_equiv_3 _ _ s_eq_t) in v_le_s. inversion v_le_s; subst. inversion H; subst; rewrite var_in_term_list_equation; simpl; destruct (X.eq_dec v v) as [_ | v_diff_v]; trivial; absurd (v = v); trivial. inversion H as [g k u1 s' s'_in_k v_le_s' | | |]; subst; rewrite var_in_term_list_equation; simpl. assert (Sk : list_size size k <= n). apply le_S_n; refine (le_trans _ _ _ _ Sl); simpl; apply le_n_S; rewrite (list_size_fold size k); auto with arith. rewrite (IHn k Sk s' s'_in_k v_le_s'); simpl; trivial. 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. rewrite var_in_term_list_equation; rewrite (IHn l Sl' s s_in_l v_le_s); destruct t as [v' | g k]. destruct (X.eq_dec v v'); trivial. destruct (var_in_term_list v k); trivial. Qed. Lemma rpo_eval_is_complete_less_greater :   forall rpo_infos n t1 t2, size t1 + size t2 <= n ->         well_formed t1 -> well_formed t2 -> rpo t1 t2 ->         rpo_eval rpo_infos n t1 t2 = Some Less_than /\         rpo_eval rpo_infos n t2 t1 = Some Greater_than. Proof. intros rpo_infos n; induction n as [ | n]; intros t1 t2 St W1 W2 t1_lt_t2. absurd (1 <= 0); auto with arith; apply le_trans with (size t1 + size t2); trivial; apply le_trans with (1 + size t2); [apply le_plus_l | apply plus_le_compat_r; apply size_ge_one]. assert (TE := equiv_eval_terminates rpo_infos _ _ _ St); assert (R := rpo_eval_is_sound_weak rpo_infos (S n) t1 t2 W1 W2); assert (T := rpo_eval_terminates rpo_infos (S n) t1 t2 St). rewrite plus_comm in St; assert (TE' := equiv_eval_terminates rpo_infos _ _ _ St); assert (R' := rpo_eval_is_sound_weak rpo_infos (S n) t2 t1 W2 W1); assert (T' := rpo_eval_terminates rpo_infos (S n) t2 t1 St). do 2 rewrite rpo_eval_equation; rewrite rpo_eval_equation in R; rewrite rpo_eval_equation in T; rewrite rpo_eval_equation in R'; rewrite rpo_eval_equation in T'. revert R T R' T'. case_eq (find t1 t2 (rpo_l rpo_infos));intro Heq_1; case_eq (find t2 t1 (rpo_l rpo_infos));intro Heq_2; case_eq (find t1 t2 (equiv_l rpo_infos));intro Heq_3; case_eq (find t2 t1 (equiv_l rpo_infos));intro Heq_4; intros R T R' T';try (absurd (rpo t1 t1);[ intro; apply (rpo_antirefl t1); trivial| apply rpo_trans with t2;assumption]);try complete intuition; try (absurd (rpo t1 t1); [intro; apply (rpo_antirefl t1); trivial| setoid_rewrite (equiv_rpo_equiv_1 _ _ R') in t1_lt_t2; trivial]). destruct (equiv_eval rpo_infos (S n) t1 t2) as [ [ | ] | ]; destruct (equiv_eval rpo_infos (S n) t2 t1) as [ [ | ] | ]; try (absurd (rpo t1 t1);[ intro; apply (rpo_antirefl t1); trivial| setoid_rewrite <- (equiv_rpo_equiv_1 _ _ R) in t1_lt_t2; trivial]);try complete intuition; try (absurd (rpo t1 t1); [intro; apply (rpo_antirefl t1); trivial| setoid_rewrite (equiv_rpo_equiv_1 _ _ R') in t1_lt_t2; trivial]). clear TE TE'. destruct t1 as [v1 | f1 l1]; destruct t2 as [v2 | f2 l2]. inversion t1_lt_t2. rewrite (var_case2 _ _ _ t1_lt_t2); split; trivial. inversion t1_lt_t2. assert (Sl : forall t1 t2, In t1 l1 -> In t2 l2 -> size t1 + size t2 <= n). intros t1 t2 t1_in_l1 t2_in_l2; apply le_S_n; refine (le_trans _ _ _ _ St); replace (S (size t1 + size t2)) with (S (size t1) + size t2); trivial; rewrite plus_comm; apply plus_le_compat. apply lt_le_weak; apply size_direct_subterm; trivial. apply size_direct_subterm; trivial. destruct (well_formed_unfold (Term f1 l1) W1) as [Wl1 _]. destruct (well_formed_unfold (Term f2 l2) W2) as [Wl2 _]. assert (IHl1l2 : forall t1 t2, In t1 l1 -> In t2 l2 -> rpo t1 t2 ->      rpo_eval rpo_infos n t1 t2 = Some Less_than /\       rpo_eval rpo_infos n t2 t1 = Some Greater_than). intros; apply IHn; trivial. apply Sl; trivial. apply Wl1; trivial. apply Wl2; trivial. assert (IHl2l1 : forall t1 t2, In t1 l1 -> In t2 l2 -> rpo t2 t1 ->      rpo_eval rpo_infos n t2 t1 = Some Less_than /\       rpo_eval rpo_infos n t1 t2 = Some Greater_than). intros; apply IHn; trivial. rewrite plus_comm; apply Sl; trivial. apply Wl2; trivial. apply Wl1; trivial. assert (IHl1s2 : forall t1, In t1 l1 -> rpo t1 (Term f2 l2) ->      rpo_eval rpo_infos n t1 (Term f2 l2) = Some Less_than /\       rpo_eval rpo_infos n (Term f2 l2) t1 = Some Greater_than). intros; apply IHn; trivial. apply le_S_n; refine (le_trans _ _ _ _ St); replace (S (size t1 + size (Term f2 l2))) with (S (size t1) + size (Term f2 l2)); trivial; rewrite plus_comm; apply plus_le_compat_l. apply size_direct_subterm; trivial. apply Wl1; trivial. assert (IHs2l1 : forall t1, In t1 l1 -> rpo (Term f2 l2) t1 ->      rpo_eval rpo_infos n (Term f2 l2) t1 = Some Less_than /\       rpo_eval rpo_infos n t1 (Term f2 l2) = Some Greater_than). intros; apply IHn; trivial. rewrite plus_comm; apply le_S_n; refine (le_trans _ _ _ _ St); replace (S (size t1 + size (Term f2 l2))) with (S (size t1) + size (Term f2 l2)); trivial; rewrite plus_comm; apply plus_le_compat_l. apply size_direct_subterm; trivial. apply Wl1; trivial. assert (IHs1l2 : forall t2, In t2 l2 -> rpo (Term f1 l1) t2 ->      rpo_eval rpo_infos n (Term f1 l1) t2 = Some Less_than /\       rpo_eval rpo_infos n t2 (Term f1 l1) = Some Greater_than). intros; apply IHn; trivial. rewrite plus_comm; apply le_S_n; refine (le_trans _ _ _ _ St); replace (S (size t2 + size (Term f1 l1))) with (S (size t2) + size (Term f1 l1)); trivial; apply plus_le_compat_r. apply size_direct_subterm; trivial. apply Wl2; trivial. assert (IHl2s1 : forall t2, In t2 l2 -> rpo t2 (Term f1 l1) ->      rpo_eval rpo_infos n t2 (Term f1 l1) = Some Less_than /\       rpo_eval rpo_infos n (Term f1 l1) t2 = Some Greater_than). intros; apply IHn; trivial. apply le_S_n; refine (le_trans _ _ _ _ St); replace (S (size t2 + size (Term f1 l1))) with (S (size t2) + size (Term f1 l1)); trivial; apply plus_le_compat_r. apply size_direct_subterm; trivial. apply Wl2; trivial. inversion t1_lt_t2 as [ f2' l2' u1 s2 s2_in_l2 u1_le_s2 | f2' f1' l2' l1' f1_lt_f2 H | f l2' l1' Sf l1_lt_l2 H | f l2' l1' Sf l1_lt_l2]; subst. split. destruct (list_exists_option            (fun t : term =>             match rpo_eval rpo_infos n t (Term f2 l2) with             | Some Equivalent => Some true             | Some Less_than => Some false             | Some Greater_than => Some true             | Some Uncomparable => Some false             | None => None (A:=bool)             end) l1) as [ [ | ] | ]. simpl in R; destruct (rpo_closure (Term f1 l1) (Term f2 l2) (Term f2 l2)) as [_ [Antisym _]]. assert False; [apply Antisym; trivial | contradiction]. assert (t1_lt_l2 : list_exists_option           (fun t : term =>            match rpo_eval rpo_infos n (Term f1 l1) t with            | Some Equivalent => Some true            | Some Less_than => Some true            | Some Greater_than => Some false            | Some Uncomparable => Some false            | None => None (A:=bool)            end) l2 = Some true). apply list_exists_option_is_complete_true. destruct (mem_split_set _ _ s2_in_l2) as [s2' [l2' [l2'' [s2_eq_s2' H]]]]. simpl in s2_eq_s2'; simpl in H. assert (s2'_in_l2 : In s2' l2). subst l2; apply in_or_app; right; left; trivial. exists s2'; split; trivial. setoid_rewrite (equiv_rpo_equiv_3 _ _ s2_eq_s2') in u1_le_s2. inversion u1_le_s2; subst. rewrite (rpo_eval_is_complete_equivalent rpo_infos n (Term f1 l1) s2'); trivial. rewrite plus_comm; apply le_S_n; refine (le_trans _ _ _ _ St); replace (S (size s2' + size (Term f1 l1))) with (S (size s2') + size (Term f1 l1)); trivial; apply plus_le_compat_r. apply size_direct_subterm; simpl; trivial. destruct (IHs1l2 s2' s2'_in_l2 H0) as [H1 _]; rewrite H1; trivial. rewrite t1_lt_l2; simpl; trivial. simpl in T; absurd (@None comp = None); trivial. assert (l2_gt_t1 : list_exists_option             (fun t : term =>              match rpo_eval rpo_infos n t (Term f1 l1) with              | Some Equivalent => Some true              | Some Less_than => Some false              | Some Greater_than => Some true              | Some Uncomparable => Some false              | None => None (A:=bool)              end) l2 = Some true). apply list_exists_option_is_complete_true. destruct (mem_split_set _ _ s2_in_l2) as [s2' [l2' [l2'' [s2_eq_s2' H]]]]. simpl in s2_eq_s2'; simpl in H. assert (s2'_in_l2 : In s2' l2). subst l2; apply in_or_app; right; left; trivial. exists s2'; split; trivial. inversion u1_le_s2; subst. rewrite (rpo_eval_is_complete_equivalent rpo_infos n s2' (Term f1 l1)); trivial. apply le_S_n; refine (le_trans _ _ _ _ St); replace (S (size s2' + size (Term f1 l1))) with (S (size s2') + size (Term f1 l1)); trivial; apply plus_le_compat_r. apply size_direct_subterm; trivial. symmetry; transitivity s2; trivial. setoid_rewrite (equiv_rpo_equiv_1 _ _ s2_eq_s2') in H0. destruct (IHs1l2 s2' s2'_in_l2 H0) as [_ H2]; rewrite H2; trivial. rewrite l2_gt_t1; simpl; trivial. split. destruct (list_exists_option            (fun t : term =>             match rpo_eval rpo_infos n t (Term f2 l2) with             | Some Equivalent => Some true             | Some Less_than => Some false             | Some Greater_than => Some true             | Some Uncomparable => Some false             | None => None (A:=bool)             end) l1) as [ [ | ] | ]. simpl in R. destruct (rpo_closure (Term f1 l1) (Term f2 l2) (Term f2 l2)) as [_ [Antisym _]]. assert False; [apply Antisym; trivial | contradiction]. destruct (list_exists_option                (fun t : term =>                 match rpo_eval rpo_infos n (Term f1 l1) t with                 | Some Equivalent => Some true                 | Some Less_than => Some true                 | Some Greater_than => Some false                 | Some Uncomparable => Some false                 | None => None (A:=bool)                 end) l2) as [ [ | ] | ]. trivial. generalize (prec_eval_is_sound f1 f2); destruct (prec_eval f1 f2). intro; subst f2; assert False; [apply (prec_antisym f1); trivial | contradiction]. intros _; assert (H' : list_forall_option     (fun t : term =>      match rpo_eval rpo_infos n t (Term f2 l2) with      | Some Equivalent => Some false      | Some Less_than => Some true      | Some Greater_than => Some false      | Some Uncomparable => Some false      | None => None (A:=bool)      end) l1 = Some true). apply list_forall_option_is_complete_true. intros u1 u1_in_l1; destruct (IHl1s2 u1 u1_in_l1) as [H1 _]. apply H0; apply in_impl_mem; trivial. rewrite H1; trivial. rewrite H'; trivial. intro f2_lt_f1; assert False; [apply (prec_antisym f1); apply prec_transitive with f2; trivial | contradiction]. intros [_ [not_f1_lt_f2 _]]; absurd (prec f1 f2); trivial. simpl in T; absurd (@None comp = None); trivial. simpl in T; absurd (@None comp = None); trivial. clear R T; destruct (list_exists_option              (fun t : term =>              match rpo_eval rpo_infos n t (Term f1 l1) with              | Some Equivalent => Some true              | Some Less_than => Some false              | Some Greater_than => Some true              | Some Uncomparable => Some false              | None => None (A:=bool)              end) l2) as [ [ | ] | ]. trivial. destruct (list_exists_option          (fun t : term =>           match rpo_eval rpo_infos n (Term f2 l2) t with           | Some Equivalent => Some true           | Some Less_than => Some true           | Some Greater_than => Some false           | Some Uncomparable => Some false           | None => None (A:=bool)           end) l1) as [ [ | ] | ]. simpl in R'. destruct (rpo_closure (Term f1 l1) (Term f2 l2) (Term f2 l2)) as [_ [Antisym _]]. assert False; [apply Antisym; trivial | contradiction]. generalize (prec_eval_is_sound f2 f1); destruct (prec_eval f2 f1). intro; subst f2; assert False; [apply (prec_antisym f1); trivial | contradiction]. intro f2_lt_f1; assert False; [apply (prec_antisym f1); apply prec_transitive with f2; trivial | contradiction]. intros _; assert (H' : list_forall_option     (fun t : term =>      match rpo_eval rpo_infos n (Term f2 l2) t with      | Some Equivalent => Some false      | Some Less_than => Some false      | Some Greater_than => Some true      | Some Uncomparable => Some false      | None => None (A:=bool)      end) l1 = Some true). apply list_forall_option_is_complete_true. intros u1 u1_in_l1; destruct (IHl1s2 u1 u1_in_l1) as [_ H2]. apply H0; apply in_impl_mem; trivial. rewrite H2; trivial. rewrite H'; trivial. intros [_ [_ not_f1_lt_f2]]; absurd (prec f1 f2); trivial. simpl in T'; absurd (@None comp = None); trivial. simpl in T'; absurd (@None comp = None); trivial. split. destruct (list_exists_option      (fun t : term =>       match rpo_eval rpo_infos n t (Term f2 l2) with       | Some Equivalent => Some true       | Some Less_than => Some false       | Some Greater_than => Some true       | Some Uncomparable => Some false       | None => None (A:=bool)       end) l1) as [ [ | ] | ]. simpl in R. destruct (rpo_closure (Term f2 l1) (Term f2 l2) (Term f2 l2)) as [_ [Antisym _]]. assert False; [apply Antisym; trivial | contradiction]. destruct (list_exists_option          (fun t : term =>           match rpo_eval rpo_infos n (Term f2 l1) t with           | Some Equivalent => Some true           | Some Less_than => Some true           | Some Greater_than => Some false           | Some Uncomparable => Some false           | None => None (A:=bool)           end) l2) as [ [ | ] | ]. trivial. simpl; generalize (prec_eval_is_sound f2 f2); destruct (prec_eval f2 f2). intros _; rewrite Sf; rewrite Sf in R; rewrite Sf in T; simpl in R; simpl in T. assert (L : length l1 = length l2). destruct W1 as [_ L1]; destruct W2 as [_ L2]; destruct (F.arity f2) as [ | | m]; rewrite L1; rewrite L2; trivial. generalize (Term f2 l1) (Term f2 l2) t1_lt_t2 H0 St IHl1s2 IHs2l1 IHs1l2 IHl2s1 R T. clear W1 W2 H0 St IHl1s2 IHs2l1 IHs1l2 IHl2s1 R T R' T'. generalize l2 L l1_lt_l2 IHl1l2 IHl2l1 Sl; clear l2 L l1_lt_l2 IHl1l2 IHl2l1 Sl Wl1 Wl2 t1_lt_t2 Heq_1 Heq_2 Heq_3 Heq_4. induction l1 as [ | t1 l1]; intros [ | t2 l2] L l1_lt_l2 IHl1l2 IHl2l1 Sl; intros s1 s2 s1_lt_s2 H0 St IHl1s2 IHs2l1 IHs1l2 IHl2s1 R T. simpl in R; absurd (rpo s1 s1). intro; apply (rpo_antirefl s1); trivial. setoid_rewrite <- (equiv_rpo_equiv_1 _ _ R) in s1_lt_s2; trivial. discriminate. discriminate. inversion l1_lt_l2; subst. simpl; destruct (IHl1l2 t1 t2 (or_introl _ (refl_equal _))                  (or_introl _ (refl_equal _)) H3) as [H1 _]; rewrite H1; clear H1. destruct (IHl1s2 t1 (or_introl _ (refl_equal _))                   (H0 t1 (or_introl _ (equiv_refl _ _ equiv_equiv _)))) as [H1 _]; rewrite H1; clear H1. assert (H' : list_forall_option     (fun t3 : term =>      match rpo_eval rpo_infos n t3 s2 with      | Some Equivalent => Some false      | Some Less_than => Some true      | Some Greater_than => Some false      | Some Uncomparable => Some false      | None => None (A:=bool)      end) l1 = Some true). apply list_forall_option_is_complete_true. intros u1 u1_in_l1; destruct (IHl1s2 u1 (or_intror _ u1_in_l1)                   (H0 u1 (or_intror _ (in_impl_mem _ _ u1_in_l1)))) as [H1 _]; rewrite H1; trivial. rewrite H'; trivial. simpl; assert (H' := rpo_eval_is_complete_equivalent rpo_infos n t1 t2). generalize (H' (Sl _ _ (or_introl _ (refl_equal _))                         (or_introl _ (refl_equal _))) H3); clear H'; intro H'; rewrite H'. apply IHl1; trivial. injection L; intros; trivial. intros; apply IHl1l2; trivial; right; trivial. intros; apply IHl2l1; trivial; right; trivial. intros; apply Sl; right; trivial. intros; apply H0; right; trivial. intros; apply IHl1s2; trivial; right; trivial. intros; apply IHs2l1; trivial; right; trivial. intros; apply IHs1l2; trivial; right; trivial. intros; apply IHl2s1; trivial; right; trivial. simpl in R; rewrite H' in R; trivial. simpl in T; rewrite H' in T; trivial. intro; assert False; [apply (prec_antisym f2); trivial | contradiction]. intro; assert False; [apply (prec_antisym f2); trivial | contradiction]. intros [f2_diff_f2 _]; absurd (f2 = f2); trivial. simpl in T; absurd (@None comp = None); trivial. simpl in T; absurd (@None comp = None); trivial. destruct (list_exists_option      (fun t : term =>       match rpo_eval rpo_infos n t (Term f2 l1) with       | Some Equivalent => Some true       | Some Less_than => Some false       | Some Greater_than => Some true       | Some Uncomparable => Some false       | None => None (A:=bool)       end) l2) as [ [ | ] | ]. trivial. destruct (list_exists_option          (fun t : term =>           match rpo_eval rpo_infos n (Term f2 l2) t with           | Some Equivalent => Some true           | Some Less_than => Some true           | Some Greater_than => Some false           | Some Uncomparable => Some false           | None => None (A:=bool)           end) l1) as [ [ | ] | ]. simpl in R'. destruct (rpo_closure (Term f2 l1) (Term f2 l2) (Term f2 l2)) as [_ [Antisym _]]. assert False; [apply Antisym; trivial | contradiction]. simpl; generalize (prec_eval_is_sound f2 f2); destruct (prec_eval f2 f2). intros _; rewrite Sf; rewrite Sf in R'; rewrite Sf in T'; simpl in R'; simpl in T'. assert (L : length l1 = length l2). destruct W1 as [_ L1]; destruct W2 as [_ L2]; destruct (F.arity f2) as [ | | m]; rewrite L1; rewrite L2; trivial. generalize (Term f2 l1) (Term f2 l2) t1_lt_t2 H0 St IHl1s2 IHs2l1 IHs1l2 IHl2s1 R' T'. clear W1 W2 H0 St IHl1s2 IHs2l1 IHs1l2 IHl2s1 R T R' T'. generalize l2 L l1_lt_l2 IHl1l2 IHl2l1 Sl; clear l2 L l1_lt_l2 IHl1l2 IHl2l1 Sl Wl1 Wl2 t1_lt_t2 Heq_1 Heq_2 Heq_3 Heq_4. induction l1 as [ | t1 l1]; intros [ | t2 l2] L l1_lt_l2 IHl1l2 IHl2l1 Sl; intros s1 s2 s1_lt_s2 H0 St IHl1s2 IHs2l1 IHs1l2 IHl2s1 R' T'. simpl in R'; absurd (rpo s1 s1). intro; apply (rpo_antirefl s1); trivial. setoid_rewrite (equiv_rpo_equiv_1 _ _ R') in s1_lt_s2; trivial. discriminate. discriminate. inversion l1_lt_l2; subst. simpl; destruct (IHl1l2 t1 t2 (or_introl _ (refl_equal _))                  (or_introl _ (refl_equal _)) H3) as [_ H2]; rewrite H2; clear H2. destruct (IHl1s2 t1 (or_introl _ (refl_equal _))                   (H0 t1 (or_introl _ (equiv_refl _ _ equiv_equiv _)))) as [_ H2]; rewrite H2; clear H2. assert (H' : list_forall_option     (fun t3 : term =>      match rpo_eval rpo_infos n s2 t3 with      | Some Equivalent => Some false      | Some Less_than => Some false      | Some Greater_than => Some true      | Some Uncomparable => Some false      | None => None (A:=bool)      end) l1 = Some true). apply list_forall_option_is_complete_true. intros u1 u1_in_l1; destruct (IHl1s2 u1 (or_intror _ u1_in_l1)                   (H0 u1 (or_intror _ (in_impl_mem _ _ u1_in_l1)))) as [_ H2]; rewrite H2; trivial. rewrite H'; trivial. simpl; assert (H' := rpo_eval_is_complete_equivalent rpo_infos n t2 t1). rewrite plus_comm in H'; generalize (H' (Sl _ _ (or_introl _ (refl_equal _))                         (or_introl _ (refl_equal _)))                       (equiv_sym _ _ equiv_equiv _ _ H3)); clear H'; intro H'; rewrite H'. apply IHl1; trivial. injection L; intros; trivial. intros; apply IHl1l2; trivial; right; trivial. intros; apply IHl2l1; trivial; right; trivial. intros; apply Sl; right; trivial. intros; apply H0; right; trivial. intros; apply IHl1s2; trivial; right; trivial. intros; apply IHs2l1; trivial; right; trivial. intros; apply IHs1l2; trivial; right; trivial. intros; apply IHl2s1; trivial; right; trivial. simpl in R'; rewrite H' in R'; trivial. simpl in T'; rewrite H' in T'; trivial. intro; assert False; [apply (prec_antisym f2); trivial | contradiction]. intro; assert False; [apply (prec_antisym f2); trivial | contradiction]. intros [f2_diff_f2 _]; absurd (f2 = f2); trivial. simpl in T; absurd (@None comp = None); trivial. simpl in T; absurd (@None comp = None); trivial. split. destruct (list_exists_option      (fun t : term =>       match rpo_eval rpo_infos n t (Term f2 l2) with       | Some Equivalent => Some true       | Some Less_than => Some false       | Some Greater_than => Some true       | Some Uncomparable => Some false       | None => None (A:=bool)       end) l1) as [ [ | ] | ]. simpl in R. destruct (rpo_closure (Term f2 l1) (Term f2 l2) (Term f2 l2)) as [_ [Antisym _]]. assert False; [apply Antisym; trivial | contradiction]. destruct (list_exists_option          (fun t : term =>           match rpo_eval rpo_infos n (Term f2 l1) t with           | Some Equivalent => Some true           | Some Less_than => Some true           | Some Greater_than => Some false           | Some Uncomparable => Some false           | None => None (A:=bool)           end) l2) as [ [ | ] | ]. trivial. simpl; generalize (prec_eval_is_sound f2 f2); destruct (prec_eval f2 f2). intros _; rewrite Sf; rewrite Sf in R; rewrite Sf in T; simpl in R; simpl in T. case_eq (remove_equiv_eval_list (equiv_eval rpo_infos n) l1 l2). intros [[ | t1' l1'] [ | t2' l2']] H. rewrite H in R; absurd (rpo (Term f2 l1) (Term f2 l1)). intro; apply (rpo_antirefl (Term f2 l1)); trivial. setoid_rewrite <- (equiv_rpo_equiv_1 _ _ R) in t1_lt_t2; trivial. trivial. rewrite H in R; absurd (rpo (Term f2 l1) (Term f2 l1)). intro; apply (rpo_antirefl (Term f2 l1)); trivial. apply rpo_trans with (Term f2 l2); trivial. assert (H' := remove_equiv_eval_list_is_sound (equiv_eval rpo_infos n) l1 l2); rewrite H in H'; destruct H' as [ll [E_ll [P1 [P2 F]]]]. assert (H' : rpo_mul (t1' :: l1') (t2' :: l2')). assert (E_ll' : forall t1 t2, In (t1,t2) ll -> equiv t1 t2). intros t1 t2 t1t2_in_ll; apply (equiv_eval_is_sound_weak rpo_infos n); apply E_ll; trivial. generalize ll l1 l2 t1' l1' t2' l2' l1_lt_l2 E_ll' P1 P2; clear t1' l1' t2' l2' l1_lt_l2 ll E_ll' E_ll P1 P2 F H; induction ll as [ | [u1 u2] ll]; intros k1 k2 t1' l1' t2' l2' k1_lt_k2 E_ll P1 P2. inversion k1_lt_k2; subst. apply (List_mul a lg ls lc); trivial. simpl in P1; rewrite <- app_nil_end in P1. transitivity k1; trivial. symmetry; apply permut_impl with (@eq term); trivial; intros; subst; reflexivity. simpl in P2; rewrite <- app_nil_end in P2. transitivity k2; trivial. symmetry; apply permut_impl with (@eq term); trivial; intros; subst; reflexivity. apply (rpo_mul_remove_equiv_aux (t1' :: l1') (t2' :: l2') u1 u2). intros t _ t_lt_t; apply (rpo_antirefl t); trivial. apply E_ll; left; trivial. apply (IHll k1 k2 u1 (t1' :: l1') u2 (t2' :: l2') k1_lt_k2). intros; apply E_ll; right; trivial. apply list_permut.permut_trans with    ((t1' :: l1') ++ map (fun st : term * term => fst st) ((u1, u2) :: ll)); trivial. intros; subst; trivial. apply list_permut.permut_sym. intros; subst; trivial. simpl map; rewrite <- app_comm_cons; apply Pcons; trivial. apply list_permut.permut_refl; intro; trivial. apply list_permut.permut_trans with ((t2' :: l2') ++ map (fun st : term * term => snd st) ((u1, u2) :: ll)); trivial. intros; subst; trivial. apply list_permut.permut_sym. intros; subst; trivial. simpl map; rewrite <- app_comm_cons; apply Pcons; trivial. apply list_permut.permut_refl; intro; trivial. rewrite H in R; rewrite H in T; unfold mult_eval; unfold mult_eval in R; unfold mult_eval in T; destruct (list_forall_option           (fun t2 : term =>            list_exists_option              (fun t1 : term =>               match rpo_eval rpo_infos n t1 t2 with               | Some Equivalent => Some false               | Some Less_than => Some false               | Some Greater_than => Some true               | Some Uncomparable => Some false               | None => None (A:=bool)               end) (t1' :: l1')) (t2' :: l2')) as [ [ | ] | ]. absurd (rpo (Term f2 l1) (Term f2 l1)). intro; apply (rpo_antirefl (Term f2 l1)); trivial. apply rpo_trans with (Term f2 l2); trivial. assert (list_forall_option     (fun t1 : term =>      list_exists_option        (fun t2 : term =>         match rpo_eval rpo_infos n t1 t2 with         | Some Equivalent => Some false         | Some Less_than => Some true         | Some Greater_than => Some false         | Some Uncomparable => Some false         | None => None (A:=bool)         end) (t2' :: l2')) (t1' :: l1') = Some true). apply list_forall_option_is_complete_true. intros u1 u1_in_l1'; apply list_exists_option_is_complete_true. inversion H'; subst. assert (u1_mem_ls_lc : mem u1 (ls ++ lc)). setoid_rewrite <- (mem_permut_mem u1 H0); apply in_impl_mem; trivial. setoid_rewrite <- mem_or_app in u1_mem_ls_lc. destruct u1_mem_ls_lc as [u1_mem_ls | u1_mem_lc]. destruct (H2 _ u1_mem_ls) as [a' [a'_in_lg u1_lt_a']]. destruct (mem_split_set _ _ a'_in_lg) as [a'' [lg' [lg'' [a''_eq_a' H'']]]]. simpl in a''_eq_a'; simpl in H''. destruct (mem_split_set a'' (t2' :: l2')) as [a3 [k2' [k2'' [a''_eq_a3 H''']]]]. setoid_rewrite H1; rewrite app_comm_cons. setoid_rewrite <- mem_or_app; left. rewrite H''; apply in_impl_mem; apply in_or_app; right; left; trivial. simpl in a''_eq_a3; simpl in H'''. exists a3; split. rewrite H'''; apply in_or_app; right; left; trivial. destruct (IHl1l2 u1 a3) as [H1' _]; trivial. setoid_rewrite (in_permut_in P1); apply in_or_app; left; trivial. setoid_rewrite (in_permut_in P2); apply in_or_app; left; rewrite H'''. apply in_or_app; right; left; trivial. setoid_rewrite <- (equiv_rpo_equiv_1 _ _ a''_eq_a3). setoid_rewrite <- (equiv_rpo_equiv_1 _ _ a''_eq_a'); trivial. rewrite H1'; trivial. assert (u1_mem_l2' : mem u1 (t2' :: l2')). setoid_rewrite H1; right; setoid_rewrite <- mem_or_app; right; trivial. destruct (mem_split_set _ _ u1_mem_l2') as [u2 [k2' [k2'' [u1_eq_u2 H'']]]]. simpl in u1_eq_u2; simpl in H''. assert (u2_in_l2' : In u2 (t2' :: l2')). rewrite H''; apply in_or_app; right; left; trivial. generalize (equiv_eval_is_sound rpo_infos n u1 u2); rewrite (F u1 u2 u1_in_l1' u2_in_l2'); intro; absurd (equiv u1 u2); trivial; apply H3. apply le_S_n; refine (le_trans _ _ _ _ St); replace (S (size u1 + size u2)) with (S (size u1) + size u2); trivial; rewrite plus_comm; apply plus_le_compat. apply le_trans with (size (Term f2 (t2' :: l2'))). apply lt_le_weak; apply size_direct_subterm; simpl; trivial. do 2 rewrite size_unfold. assert (Dummy : forall a0 a' : term,   In a0 l2 -> In a' ((t2' :: l2') ++ map (fun st : term * term => snd st) ll) ->    a0 = a' -> size a0 = size a'). intros; subst; trivial. rewrite (permut_size size size Dummy P2). apply plus_le_compat_l. rewrite list_size_app; apply le_plus_trans; apply le_n. apply le_trans with (size (Term f2 (t1' :: l1'))). apply size_direct_subterm; simpl; trivial. do 2 rewrite size_unfold. assert (Dummy : forall a0 a' : term,   In a0 l1 -> In a' ((t1' :: l1') ++ map (fun st : term * term => fst st) ll) ->    a0 = a' -> size a0 = size a'). intros; subst; trivial. rewrite (permut_size size size Dummy P1). apply plus_le_compat_l. rewrite list_size_app; apply le_plus_trans; apply le_n. rewrite H0; trivial. assert False; [apply T; trivial | contradiction]. intro H; rewrite H in T; assert False; [apply T; trivial | contradiction]. intro; assert False; [apply (prec_antisym f2); trivial | contradiction]. intro; assert False; [apply (prec_antisym f2); trivial | contradiction]. intros [f2_diff_f2 _]; absurd (f2 = f2); trivial. assert False; [apply T; trivial | contradiction]. assert False; [apply T; trivial | contradiction]. destruct (list_exists_option      (fun t : term =>       match rpo_eval rpo_infos n t (Term f2 l1) with       | Some Equivalent => Some true       | Some Less_than => Some false       | Some Greater_than => Some true       | Some Uncomparable => Some false       | None => None (A:=bool)       end) l2) as [ [ | ] | ]. trivial. destruct (list_exists_option          (fun t : term =>           match rpo_eval rpo_infos n (Term f2 l2) t with           | Some Equivalent => Some true           | Some Less_than => Some true           | Some Greater_than => Some false           | Some Uncomparable => Some false           | None => None (A:=bool)           end) l1) as [ [ | ] | ]. simpl in R. destruct (rpo_closure (Term f2 l1) (Term f2 l2) (Term f2 l2)) as [_ [Antisym _]]. assert False; [apply Antisym; trivial | contradiction]. simpl; generalize (prec_eval_is_sound f2 f2); destruct (prec_eval f2 f2). intros _; rewrite Sf; rewrite Sf in R'; rewrite Sf in T'; simpl in R'; simpl in T'. case_eq (remove_equiv_eval_list (equiv_eval rpo_infos n) l2 l1). intros [[ | t2' l2'] [ | t1' l1']] H. rewrite H in R'; absurd (rpo (Term f2 l1) (Term f2 l1)). intro; apply (rpo_antirefl (Term f2 l1)); trivial. setoid_rewrite (equiv_rpo_equiv_1 _ _ R') in t1_lt_t2; trivial. rewrite H in R'; absurd (rpo (Term f2 l1) (Term f2 l1)). intro; apply (rpo_antirefl (Term f2 l1)); trivial. apply rpo_trans with (Term f2 l2); trivial. trivial. assert (H' := remove_equiv_eval_list_is_sound (equiv_eval rpo_infos n) l2 l1); rewrite H in H'; destruct H' as [ll [E_ll [P2 [P1 F]]]]. assert (H' : rpo_mul (t1' :: l1') (t2' :: l2')). assert (E_ll' : forall t1 t2, In (t1,t2) ll -> equiv t1 t2). intros t1 t2 t1t2_in_ll; apply (equiv_eval_is_sound_weak rpo_infos n); apply E_ll; trivial. generalize ll l1 l2 t1' l1' t2' l2' l1_lt_l2 E_ll' P1 P2; clear t1' l1' t2' l2' l1_lt_l2 ll E_ll' E_ll P1 P2 F H; induction ll as [ | [u1 u2] ll]; intros k1 k2 t1' l1' t2' l2' k1_lt_k2 E_ll P1 P2. inversion k1_lt_k2; subst. apply (List_mul a lg ls lc); trivial. transitivity k1; trivial; symmetry. simpl in P1; rewrite <- app_nil_end in P1. apply permut_impl with (@eq term); trivial. intros; subst; reflexivity. transitivity k2; trivial; symmetry. simpl in P2; rewrite <- app_nil_end in P2. apply permut_impl with (@eq term); trivial. intros; subst; reflexivity. apply (rpo_mul_remove_equiv_aux (t1' :: l1') (t2' :: l2') u2 u1). intros t _ t_lt_t; apply (rpo_antirefl t); trivial. apply (equiv_sym _ _ equiv_equiv); apply E_ll; left; trivial. apply (IHll k1 k2 u2 (t1' :: l1') u1 (t2' :: l2') k1_lt_k2). intros; apply E_ll; right; trivial. apply list_permut.permut_trans with   ((t1' :: l1') ++ map (fun st : term * term => snd st) ((u1, u2) :: ll)); trivial. intros; subst; trivial. simpl; rewrite app_comm_cons; apply list_permut.permut_sym. intros; subst; trivial. apply Pcons; trivial. simpl; apply list_permut.permut_refl; intro; trivial. apply list_permut.permut_trans with   ((t2' :: l2') ++ map (fun st : term * term => fst st) ((u1, u2) :: ll)); trivial. intros; subst; trivial. simpl; rewrite app_comm_cons; apply list_permut.permut_sym. intros; subst; trivial. apply Pcons; trivial. simpl; apply list_permut.permut_refl; intro; trivial. rewrite H in R'; rewrite H in T'; unfold mult_eval; unfold mult_eval in R'; unfold mult_eval in T'. assert (list_forall_option     (fun t2 : term =>      list_exists_option        (fun t1 : term =>         match rpo_eval rpo_infos n t1 t2 with         | Some Equivalent => Some false         | Some Less_than => Some false         | Some Greater_than => Some true         | Some Uncomparable => Some false         | None => None (A:=bool)         end) (t2' :: l2')) (t1' :: l1') = Some true). apply list_forall_option_is_complete_true. intros u1 u1_in_l1'; apply list_exists_option_is_complete_true. inversion H'; subst. assert (u1_mem_ls_lc : mem u1 (ls ++ lc)). setoid_rewrite <- (mem_permut_mem u1 H0); apply in_impl_mem; trivial. setoid_rewrite <- mem_or_app in u1_mem_ls_lc. destruct u1_mem_ls_lc as [u1_mem_ls | u1_mem_lc]. destruct (H2 _ u1_mem_ls) as [a' [a'_in_lg u1_lt_a']]. destruct (mem_split_set _ _ a'_in_lg) as [a'' [lg' [lg'' [a''_eq_a' H'']]]]. simpl in a''_eq_a'; simpl in H''. destruct (mem_split_set a'' (t2' :: l2')) as [a3 [k2' [k2'' [a''_eq_a3 H''']]]]. setoid_rewrite H1; rewrite app_comm_cons. setoid_rewrite <- mem_or_app; left. rewrite H''; apply in_impl_mem; apply in_or_app; right; left; trivial. simpl in a''_eq_a3; simpl in H'''. exists a3; split. rewrite H'''; apply in_or_app; right; left; trivial. destruct (IHl1l2 u1 a3) as [_ H2']; trivial. setoid_rewrite (in_permut_in P1); apply in_or_app; left; trivial. setoid_rewrite (in_permut_in P2); apply in_or_app; left; rewrite H'''. apply in_or_app; right; left; trivial. setoid_rewrite <- (equiv_rpo_equiv_1 _ _ a''_eq_a3). setoid_rewrite <- (equiv_rpo_equiv_1 _ _ a''_eq_a'); trivial. rewrite H2'; trivial. assert (u1_mem_l2' : mem u1 (t2' :: l2')). setoid_rewrite H1; right; setoid_rewrite <- mem_or_app; right; trivial. destruct (mem_split_set _ _ u1_mem_l2') as [u2 [k2' [k2'' [u1_eq_u2 H'']]]]. simpl in u1_eq_u2; simpl in H''. assert (u2_in_l2' : In u2 (t2' :: l2')). rewrite H''; apply in_or_app; right; left; trivial. generalize (equiv_eval_is_sound rpo_infos n u2 u1); rewrite (F u2 u1 u2_in_l2' u1_in_l1'). intro; absurd (equiv u2 u1). apply H3. rewrite plus_comm. apply le_S_n; refine (le_trans _ _ _ _ St); replace (S (size u1 + size u2)) with (S (size u1) + size u2); trivial; rewrite plus_comm; apply plus_le_compat. apply le_trans with (size (Term f2 (t2' :: l2'))). apply lt_le_weak; apply size_direct_subterm; simpl; trivial. do 2 rewrite size_unfold. assert (Dummy : forall a0 a' : term,   In a0 l2 -> In a' ((t2' :: l2') ++ map (fun st : term * term => fst st) ll) ->    a0 = a' -> size a0 = size a'). intros; subst; trivial. rewrite (permut_size size size Dummy P2). apply plus_le_compat_l. rewrite list_size_app; apply le_plus_trans; apply le_n. apply le_trans with (size (Term f2 (t1' :: l1'))). apply size_direct_subterm; simpl; trivial. do 2 rewrite size_unfold. assert (Dummy : forall a0 a' : term,   In a0 l1 -> In a' ((t1' :: l1') ++ map (fun st : term * term => snd st) ll) ->    a0 = a' -> size a0 = size a'). intros; subst; trivial. rewrite (permut_size size size Dummy P1). apply plus_le_compat_l. rewrite list_size_app; apply le_plus_trans; apply le_n. symmetry; trivial. rewrite H0; trivial. intro H; rewrite H in T'; assert False; [apply T'; trivial | contradiction]. intro; assert False; [apply (prec_antisym f2); trivial | contradiction]. intro; assert False; [apply (prec_antisym f2); trivial | contradiction]. intros [f2_diff_f2 _]; absurd (f2 = f2); trivial. assert False; [apply T'; trivial | contradiction]. assert False; [apply T'; trivial | contradiction]. Qed. Lemma rpo_eval_is_complete :   forall rpo_infos n t1 t2, size t1 + size t2 <= n ->         well_formed t1 -> well_formed t2 ->         match rpo_eval rpo_infos n t1 t2 with         | Some Equivalent => equiv t1 t2         | Some Less_than => rpo t1 t2         | Some Greater_than => rpo t2 t1         | Some Uncomparable => ~equiv t1 t2 /\ ~ rpo t1 t2 /\ ~rpo t2 t1         | None => False         end. intros rpo_infos n t1 t2 St W1 W2; generalize (rpo_eval_is_sound_weak rpo_infos n t1 t2 W1 W2) (rpo_eval_is_complete_equivalent rpo_infos n t1 t2 St) (rpo_eval_is_complete_less_greater rpo_infos n t1 t2 St W1 W2) (rpo_eval_terminates rpo_infos n t1 t2 St); rewrite plus_comm in St; generalize (rpo_eval_is_complete_less_greater rpo_infos n t2 t1 St W2 W1). destruct (rpo_eval rpo_infos n t1 t2) as [ [ | | | ] | ]; trivial. intros not_t2_lt_t1 _ t1_diff_t2 not_t1_lt_t2 T; repeat split; intro H. generalize (t1_diff_t2 H); discriminate. destruct (not_t1_lt_t2 H); discriminate. destruct (not_t2_lt_t1 H); discriminate. intros _ _ _ _ H; apply H; trivial. Qed. Definition empty_rpo_infos : rpo_inf. Proof.   constructor 1 with (@nil (term*term)) (@nil (term*term)) (@nil (term*term));simpl;tauto. Defined. Definition add_equiv (rpo_infos:rpo_inf) t1 t2 (H:equiv t1 t2) : rpo_inf. Proof.   intros rpo_infos t1 t2 H.   case rpo_infos.   clear rpo_infos.   intros rpo_l0 rpo_eq_l0 equiv_l0 rpo_l_valid0 rpo_eq_valid0 equiv_l_valid0.   constructor 1 with rpo_l0 rpo_eq_l0 ((t1,t2)::equiv_l0).   exact rpo_l_valid0.   exact rpo_eq_valid0.   simpl.   intros t t' H0.   case H0; intros H1.   injection H1.   intros H2 H3.   rewrite <- H2;rewrite <- H3;exact H.   exact (equiv_l_valid0 _ _ H1). Defined. End Make. ```