(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA                        ENS-CNRS                *)
(*              Rocquencourt                        Lyon                    *)
(*                                                                          *)
(*                                Coq V5.10                                 *)
(*                              Nov 25th 1994                               *)
(*                                                                          *)
(****************************************************************************)
(*                             terminaison_SL.v                             *)
(****************************************************************************)

(*****************************************************************************)
(*          Projet Coq  - Calculus of Inductive Constructions V5.8           *)
(*****************************************************************************)
(*                                                                           *)
(*      Meta-theory of the explicit substitution calculus lambda-env         *)
(*      Amokrane Saibi                                                       *)
(*                                                                           *)
(*      September 1993                                                       *)
(*                                                                           *)
(*****************************************************************************)


              (* Preuve de terminaison *)  


Require Import Le.
Require Import Lt.
Require Import Plus.
Require Import Gt.
Require Import Minus.
Require Import Mult.
Require Import sur_les_relations.
Require Import TS. 
Require Import sigma_lift.  
Require Import comparith.
Require Import Pol1.
Require Import Pol2.

Section ordre.

Variable A : Set.
Variable f g : A -> nat.

Definition e_lexfg (a b : A) := f a > f b \/ f a = f b /\ g a > g b.

Lemma lexfg_notherian : explicit_noetherian _ e_lexfg. 
Proof.
unfold explicit_noetherian in |- *; unfold universal in |- *;
 unfold hereditary in |- *; unfold adjoint in |- *; 
 unfold sub in |- *; unfold a_set in |- *.
(* Goal: forall (A0 : forall _ : A, Prop) (_ : forall (x : A) (_ : forall (x0 : A) (_ : e_lexfg x x0), A0 x0), A0 x) (x : A), A0 x *)
intros P H.
(* Goal: forall x : A, P x *)
cut (forall (n m : nat) (a : A), n > f a \/ n = f a /\ m > g a -> P a).
(* Goal: forall (_ : forall (n m : nat) (a : A) (_ : or (gt n (f a)) (and (@eq nat n (f a)) (gt m (g a)))), P a) (x : A), P x *)
(* Goal: forall (n m : nat) (a : A) (_ : or (gt n (f a)) (and (@eq nat n (f a)) (gt m (g a)))), P a *)
intros H0 x; apply (H0 (S (f x)) 0).
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
auto with arith.
(* Goal: forall (n m : nat) (a : A) (_ : or (gt n (f a)) (and (@eq nat n (f a)) (gt m (g a)))), P a *)
simple induction n; simple induction m.
(* m=n=0 *)
(* Goal: forall (a : A) (_ : or (gt O (f a)) (and (@eq nat O (f a)) (gt O (g a)))), P a *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt O (f a)) (and (@eq nat O (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt O (f a)) (and (@eq nat O (f a)) (gt (S n) (g a)))), P a *)
(* Goal: forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt O (g a)))), P a *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt (S n) (g a)))), P a *)
simple induction 1; intro H1.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
absurd (0 > f a); auto with arith.
(* Goal: P a *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt O (f a)) (and (@eq nat O (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt O (f a)) (and (@eq nat O (f a)) (gt (S n) (g a)))), P a *)
(* Goal: forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt O (g a)))), P a *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt (S n) (g a)))), P a *)
elim H1; intros.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
absurd (0 > g a); auto with arith.
(* n=0, m=(S y) *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt O (f a)) (and (@eq nat O (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt O (f a)) (and (@eq nat O (f a)) (gt (S n) (g a)))), P a *)
(* Goal: forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt O (g a)))), P a *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt (S n) (g a)))), P a *)
intros y H' a H0.
(* Goal: P a *)
(* Goal: forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt O (g a)))), P a *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt (S n) (g a)))), P a *)
apply H; intros b lexfgab. 
(* Goal: P b *)
(* Goal: forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt O (g a)))), P a *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt (S n) (g a)))), P a *)
apply H'; right.
(* Goal: and (@eq nat O (f b)) (gt y (g b)) *)
(* Goal: forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt O (g a)))), P a *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt (S n) (g a)))), P a *)
elim H0; intro H1.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
absurd (0 > f a); auto with arith.
(* Goal: and (@eq nat O (f b)) (gt y (g b)) *)
(* Goal: forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt O (g a)))), P a *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt (S n) (g a)))), P a *)
elim H1; intros H2 H3; elim lexfgab; intro H4.
(* Goal: and (@eq nat O (f b)) (gt y (g b)) *)
(* Goal: and (@eq nat O (f b)) (gt y (g b)) *)
(* Goal: forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt O (g a)))), P a *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt (S n) (g a)))), P a *)
absurd (0 > f b).
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
auto with arith.
(* Goal: @eq nat O (f b) *)
(* Goal: gt y (g b) *)
(* Goal: forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt O (g a)))), P a *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt (S n) (g a)))), P a *)
rewrite H2; assumption.
(* Goal: and (@eq nat O (f b)) (gt y (g b)) *)
(* Goal: forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt O (g a)))), P a *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt (S n) (g a)))), P a *)
elim H4; intros.
(* Goal: and (@eq nat O (f b)) (gt y (g b)) *)
(* Goal: forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt O (g a)))), P a *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt (S n) (g a)))), P a *)
split.
(* Goal: @eq nat O (f b) *)
(* Goal: gt y (g b) *)
(* Goal: forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt O (g a)))), P a *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt (S n) (g a)))), P a *)
rewrite H2; assumption.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
apply le_gt_trans with (g a); auto with arith.
(* n=(S y), m=0 *)
(* Goal: P a *)
(* Goal: forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt O (g a)))), P a *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt (S n) (g a)))), P a *)
intros a H0'; apply H; intros b lexfgab.
(* Goal: P b *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt (S n) (g a)))), P a *)
apply (H0 (g a) b); elim H0'; intro H1.
(* Goal: or (gt n0 (f b)) (and (@eq nat n0 (f b)) (gt (g a) (g b))) *)
(* Goal: or (gt n0 (f b)) (and (@eq nat n0 (f b)) (gt (g a) (g b))) *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt (S n) (g a)))), P a *)
elim lexfgab; intro H2.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
left; apply le_gt_trans with (f a); auto with arith.
(* Goal: or (gt n0 (f b)) (and (@eq nat n0 (f b)) (gt (g a) (g b))) *)
(* Goal: or (gt n0 (f b)) (and (@eq nat n0 (f b)) (gt (g a) (g b))) *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt (S n) (g a)))), P a *)
elim H2; intros H3 H4; elim (gt_S n0 (f a) H1); intro H5.
(* Goal: or (gt n0 (f b)) (and (@eq nat n0 (f b)) (gt (g a) (g b))) *)
(* Goal: or (gt n0 (f b)) (and (@eq nat n0 (f b)) (gt (g a) (g b))) *)
(* Goal: or (gt n0 (f b)) (and (@eq nat n0 (f b)) (gt (g a) (g b))) *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt (S n) (g a)))), P a *)
left; elim H3; assumption.
(* Goal: and (@eq nat O (f b)) (gt y (g b)) *)
(* Goal: forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt O (g a)))), P a *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt (S n) (g a)))), P a *)
right; split.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
elim H3; auto with arith.
(* Goal: @eq nat (e_P1 ws s) (e_P1 ws s') *)
(* Goal: gt (Nat.add (e_P2 ws s) (Nat.add (e_P2 ws s) (Nat.add (e_P2 ws s) (Nat.add (e_P2 ws s) O)))) (Nat.add (e_P2 ws s') (Nat.add (e_P2 ws s') (Nat.add (e_P2 ws s') (Nat.add (e_P2 ws s') O)))) *)
assumption.
(* Goal: or (gt n0 (f b)) (and (@eq nat n0 (f b)) (gt (g a) (g b))) *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt (S n) (g a)))), P a *)
elim H1; intros H2 H3.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
absurd (0 > g a); auto with arith.
(* n=(S y), m=(S y0) *)
(* Goal: P a *)
(* Goal: forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt O (g a)))), P a *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt (S n) (g a)))), P a *)
intros y0 H0' a H1; apply H; intros b lexfgab.
(* Goal: P b *)
apply H0'; elim H1; elim lexfgab; intros H2 H3.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
left; apply le_gt_trans with (f a); auto with arith.
(* Goal: @eq nat (e_P1 ws s) (e_P1 ws s') *)
(* Goal: gt (Nat.add (e_P2 ws s) (Nat.add (e_P2 ws s) (Nat.add (e_P2 ws s) (Nat.add (e_P2 ws s) O)))) (Nat.add (e_P2 ws s') (Nat.add (e_P2 ws s') (Nat.add (e_P2 ws s') (Nat.add (e_P2 ws s') O)))) *)
elim H2; intros H4 H5; left; elim H4; assumption.
(* Goal: @eq nat (e_P1 ws s) (e_P1 ws s') *)
(* Goal: gt (Nat.add (e_P2 ws s) (Nat.add (e_P2 ws s) (Nat.add (e_P2 ws s) (Nat.add (e_P2 ws s) O)))) (Nat.add (e_P2 ws s') (Nat.add (e_P2 ws s') (Nat.add (e_P2 ws s') (Nat.add (e_P2 ws s') O)))) *)
elim H3; intros H4 H5; left; rewrite H4; assumption.
(* Goal: or (gt (S n0) (f b)) (and (@eq nat (S n0) (f b)) (gt y0 (g b))) *)
elim H2; intros H4 H5; elim H3; intros H6 H7.
(* Goal: and (@eq nat O (f b)) (gt y (g b)) *)
(* Goal: forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt O (g a)))), P a *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt (S n) (g a)))), P a *)
right; split.
(* Goal: @eq nat (e_P1 ws s) (e_P1 ws s') *)
(* Goal: gt (Nat.add (e_P2 ws s) (Nat.add (e_P2 ws s) (Nat.add (e_P2 ws s) (Nat.add (e_P2 ws s) O)))) (Nat.add (e_P2 ws s') (Nat.add (e_P2 ws s') (Nat.add (e_P2 ws s') (Nat.add (e_P2 ws s') O)))) *)
apply trans_equal with (f a); assumption.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
apply le_gt_trans with (g a); auto with arith.
Qed.

End ordre.

Notation lexfg := (e_lexfg _) (only parsing).
(* <Warning> : Syntax is discontinued *)

Theorem lexfg_systemSL :
 forall (b : wsort) (M N : TS b),
 e_systemSL _ M N -> e_lexfg _ (e_P1 b) (e_P2 b) M N.
Proof.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
red in |- *; simple induction 1; auto with arith.
Qed.
Hint Resolve lexfg_systemSL.
 
Theorem lexfg_app_l :
 forall a a' b : terms,
 e_lexfg _ (e_P1 wt) (e_P2 wt) a a' ->
 e_lexfg _ (e_P1 wt) (e_P2 wt) (app a b) (app a' b).
Proof.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
unfold e_lexfg in |- *; simple induction 1; simpl in |- *; auto with arith.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
intros; elim H0; auto with arith.
Qed.
Hint Resolve lexfg_app_l.

Theorem lexfg_app_r :
 forall a b b' : terms,
 e_lexfg _ (e_P1 wt) (e_P2 wt) b b' ->
 e_lexfg _ (e_P1 wt) (e_P2 wt) (app a b) (app a b').
Proof.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
unfold e_lexfg in |- *; simple induction 1; simpl in |- *; auto with arith.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
intros; elim H0; auto with arith.
Qed.
Hint Resolve lexfg_app_r.

Theorem lexfg_lambda :
 forall a a' : terms,
 e_lexfg _ (e_P1 wt) (e_P2 wt) a a' ->
 e_lexfg _ (e_P1 wt) (e_P2 wt) (lambda a) (lambda a').
Proof.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
unfold e_lexfg in |- *; simple induction 1; simpl in |- *; auto with arith.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
intros; elim H0; auto with arith.
Qed.
Hint Resolve lexfg_lambda.

Theorem lexfg_env_t :
 forall (a a' : terms) (s : sub_explicits),
 e_lexfg _ (e_P1 wt) (e_P2 wt) a a' ->
 e_lexfg _ (e_P1 wt) (e_P2 wt) (env a s) (env a' s).
Proof.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
unfold e_lexfg in |- *; simple induction 1; simpl in |- *; auto with arith.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
intros; elim H0; auto with arith.
Qed.
Hint Resolve lexfg_env_t.

Theorem lexfg_env_s :
 forall (a : terms) (s s' : sub_explicits),
 e_lexfg _ (e_P1 ws) (e_P2 ws) s s' ->
 e_lexfg _ (e_P1 wt) (e_P2 wt) (env a s) (env a s').
Proof.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
unfold e_lexfg in |- *; simple induction 1; simpl in |- *; auto with arith.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
intros; elim H0; auto with arith.
Qed.
Hint Resolve lexfg_env_s.

Theorem lexfg_cons_t :
 forall (a a' : terms) (s : sub_explicits),
 e_lexfg _ (e_P1 wt) (e_P2 wt) a a' ->
 e_lexfg _ (e_P1 ws) (e_P2 ws) (cons a s) (cons a' s).
Proof.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
unfold e_lexfg in |- *; simple induction 1; simpl in |- *; auto with arith.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
intros; elim H0; auto with arith.
Qed.
Hint Resolve lexfg_cons_t.

Theorem lexfg_cons_s :
 forall (a : terms) (s s' : sub_explicits),
 e_lexfg _ (e_P1 ws) (e_P2 ws) s s' ->
 e_lexfg _ (e_P1 ws) (e_P2 ws) (cons a s) (cons a s').
Proof.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
unfold e_lexfg in |- *; simple induction 1; simpl in |- *; auto with arith.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
intros; elim H0; auto with arith.
Qed.
Hint Resolve lexfg_cons_s.

Theorem lexfg_comp_l :
 forall s s' t : sub_explicits,
 e_lexfg _ (e_P1 ws) (e_P2 ws) s s' ->
 e_lexfg _ (e_P1 ws) (e_P2 ws) (comp s t) (comp s' t).
Proof.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
unfold e_lexfg in |- *; simple induction 1; simpl in |- *; auto with arith.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
intros; elim H0; auto with arith.
Qed.
Hint Resolve lexfg_comp_l.

Theorem lexfg_comp_r :
 forall s t t' : sub_explicits,
 e_lexfg _ (e_P1 ws) (e_P2 ws) t t' ->
 e_lexfg _ (e_P1 ws) (e_P2 ws) (comp s t) (comp s t').
Proof.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
unfold e_lexfg in |- *; simple induction 1; simpl in |- *; auto with arith.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
intros; elim H0; auto with arith.
Qed.
Hint Resolve lexfg_comp_r.

Theorem lexfg_lift :
 forall s s' : sub_explicits,
 e_lexfg _ (e_P1 ws) (e_P2 ws) s s' ->
 e_lexfg _ (e_P1 ws) (e_P2 ws) (lift s) (lift s').
Proof.
(* Goal: forall (s s' : sub_explicits) (_ : e_lexfg (TS ws) (e_P1 ws) (e_P2 ws) s s'), e_lexfg (TS ws) (e_P1 ws) (e_P2 ws) (lift s) (lift s') *)
unfold e_lexfg in |- *; simple induction 1; simpl in |- *; intros.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
auto with arith.
(* Goal: and (@eq nat O (f b)) (gt y (g b)) *)
(* Goal: forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt O (g a)))), P a *)
(* Goal: forall (n : nat) (_ : forall (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt n (g a)))), P a) (a : A) (_ : or (gt (S n0) (f a)) (and (@eq nat (S n0) (f a)) (gt (S n) (g a)))), P a *)
elim H0; intros; right; split.
(* Goal: @eq nat (e_P1 ws s) (e_P1 ws s') *)
(* Goal: gt (Nat.add (e_P2 ws s) (Nat.add (e_P2 ws s) (Nat.add (e_P2 ws s) (Nat.add (e_P2 ws s) O)))) (Nat.add (e_P2 ws s') (Nat.add (e_P2 ws s') (Nat.add (e_P2 ws s') (Nat.add (e_P2 ws s') O)))) *)
assumption.
(* Goal: gt (Nat.add (e_P2 ws s) (Nat.add (e_P2 ws s) (Nat.add (e_P2 ws s) (Nat.add (e_P2 ws s) O)))) (Nat.add (e_P2 ws s') (Nat.add (e_P2 ws s') (Nat.add (e_P2 ws s') (Nat.add (e_P2 ws s') O)))) *)
change (4 * e_P2 _ s > 4 * e_P2 _ s') in |- *.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
auto with arith.
Qed.
Hint Resolve lexfg_lift.

Theorem lexfg_relSL :
 forall (b : wsort) (M N : TS b),
 e_relSL _ M N -> e_lexfg _ (e_P1 b) (e_P2 b) M N.
Proof.
(* Goal: gt (Nat.mul (S (S (S (S O)))) (e_P2 ws s)) (Nat.mul (S (S (S (S O)))) (e_P2 ws s')) *)
simple induction 1; auto with arith.
Qed.


(***************************************************)
(*   la relation sigma-lift (SL) est noetherienne  *)
(***************************************************)

Theorem relSL_noetherian :
 forall b : wsort, explicit_noetherian _ (e_relSL b).
Proof.
(* Goal: forall b : wsort, explicit_noetherian (TS b) (e_relSL b) *)
intro b; apply noether_inclus with (e_lexfg _ (e_P1 b) (e_P2 b)).
(* Goal: explicit_noetherian (TS b) (e_lexfg (TS b) (e_P1 b) (e_P2 b)) *)
(* Goal: forall (x y : TS b) (_ : e_relSL b x y), e_lexfg (TS b) (e_P1 b) (e_P2 b) x y *)
apply lexfg_notherian.
(* Goal: forall (x y : TS b) (_ : e_relSL b x y), e_lexfg (TS b) (e_P1 b) (e_P2 b) x y *)
exact (lexfg_relSL b).
Qed.

