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.

Module Type Precedence,

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.

Module Type RPO,

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.