Require terminaison.

Require Relations.

Require term.

Require List.

Require equational_theory.

Require rpo_extension.

Require equational_extension.

Require closure_extension.

Require term_extension.

Require dp.

Require Inclusion.

Require or_ext_generated.

Require ZArith.

Require ring_extention.

Require Zwf.

Require Inverse_Image.

Require matrix.

Require more_list_extention.

Import List.

Import ZArith.

Set Implicit Arguments.

Module algebra.
 Module F
  <:term.Signature.
  Inductive symb  :
   Set := 
     (* id_a__filter *)
    | id_a__filter : symb
     (* id_a__nats *)
    | id_a__nats : symb
     (* id_s *)
    | id_s : symb
     (* id_0 *)
    | id_0 : symb
     (* id_a__zprimes *)
    | id_a__zprimes : symb
     (* id_a__sieve *)
    | id_a__sieve : symb
     (* id_cons *)
    | id_cons : symb
     (* id_nats *)
    | id_nats : symb
     (* id_mark *)
    | id_mark : symb
     (* id_filter *)
    | id_filter : symb
     (* id_zprimes *)
    | id_zprimes : symb
     (* id_sieve *)
    | id_sieve : symb
  .
  
  
  Definition symb_eq_bool (f1 f2:symb) : bool := 
    match f1,f2 with
      | id_a__filter,id_a__filter => true
      | id_a__nats,id_a__nats => true
      | id_s,id_s => true
      | id_0,id_0 => true
      | id_a__zprimes,id_a__zprimes => true
      | id_a__sieve,id_a__sieve => true
      | id_cons,id_cons => true
      | id_nats,id_nats => true
      | id_mark,id_mark => true
      | id_filter,id_filter => true
      | id_zprimes,id_zprimes => true
      | id_sieve,id_sieve => true
      | _,_ => false
      end.
  
  
   (* Proof of decidability of equality over symb *)
  Definition symb_eq_bool_ok(f1 f2:symb) :
   match symb_eq_bool f1 f2 with
     | true => f1 = f2
     | false => f1 <> f2
     end.
  Proof.
    intros f1 f2.
    
    refine match f1 as u1,f2 as u2 return 
             match symb_eq_bool u1 u2 return 
               Prop with
               | true => u1 = u2
               | false => u1 <> u2
               end with
             | id_a__filter,id_a__filter => refl_equal _
             | id_a__nats,id_a__nats => refl_equal _
             | id_s,id_s => refl_equal _
             | id_0,id_0 => refl_equal _
             | id_a__zprimes,id_a__zprimes => refl_equal _
             | id_a__sieve,id_a__sieve => refl_equal _
             | id_cons,id_cons => refl_equal _
             | id_nats,id_nats => refl_equal _
             | id_mark,id_mark => refl_equal _
             | id_filter,id_filter => refl_equal _
             | id_zprimes,id_zprimes => refl_equal _
             | id_sieve,id_sieve => refl_equal _
             | _,_ => _
             end;intros abs;discriminate.
  Defined.
  
  
  Definition arity (f:symb) := 
    match f with
      | id_a__filter => term.Free 3
      | id_a__nats => term.Free 1
      | id_s => term.Free 1
      | id_0 => term.Free 0
      | id_a__zprimes => term.Free 0
      | id_a__sieve => term.Free 1
      | id_cons => term.Free 2
      | id_nats => term.Free 1
      | id_mark => term.Free 1
      | id_filter => term.Free 3
      | id_zprimes => term.Free 0
      | id_sieve => term.Free 1
      end.
  
  
  Definition symb_order (f1 f2:symb) : bool := 
    match f1,f2 with
      | id_a__filter,id_a__filter => true
      | id_a__filter,id_a__nats => false
      | id_a__filter,id_s => false
      | id_a__filter,id_0 => false
      | id_a__filter,id_a__zprimes => false
      | id_a__filter,id_a__sieve => false
      | id_a__filter,id_cons => false
      | id_a__filter,id_nats => false
      | id_a__filter,id_mark => false
      | id_a__filter,id_filter => false
      | id_a__filter,id_zprimes => false
      | id_a__filter,id_sieve => false
      | id_a__nats,id_a__filter => true
      | id_a__nats,id_a__nats => true
      | id_a__nats,id_s => false
      | id_a__nats,id_0 => false
      | id_a__nats,id_a__zprimes => false
      | id_a__nats,id_a__sieve => false
      | id_a__nats,id_cons => false
      | id_a__nats,id_nats => false
      | id_a__nats,id_mark => false
      | id_a__nats,id_filter => false
      | id_a__nats,id_zprimes => false
      | id_a__nats,id_sieve => false
      | id_s,id_a__filter => true
      | id_s,id_a__nats => true
      | id_s,id_s => true
      | id_s,id_0 => false
      | id_s,id_a__zprimes => false
      | id_s,id_a__sieve => false
      | id_s,id_cons => false
      | id_s,id_nats => false
      | id_s,id_mark => false
      | id_s,id_filter => false
      | id_s,id_zprimes => false
      | id_s,id_sieve => false
      | id_0,id_a__filter => true
      | id_0,id_a__nats => true
      | id_0,id_s => true
      | id_0,id_0 => true
      | id_0,id_a__zprimes => false
      | id_0,id_a__sieve => false
      | id_0,id_cons => false
      | id_0,id_nats => false
      | id_0,id_mark => false
      | id_0,id_filter => false
      | id_0,id_zprimes => false
      | id_0,id_sieve => false
      | id_a__zprimes,id_a__filter => true
      | id_a__zprimes,id_a__nats => true
      | id_a__zprimes,id_s => true
      | id_a__zprimes,id_0 => true
      | id_a__zprimes,id_a__zprimes => true
      | id_a__zprimes,id_a__sieve => false
      | id_a__zprimes,id_cons => false
      | id_a__zprimes,id_nats => false
      | id_a__zprimes,id_mark => false
      | id_a__zprimes,id_filter => false
      | id_a__zprimes,id_zprimes => false
      | id_a__zprimes,id_sieve => false
      | id_a__sieve,id_a__filter => true
      | id_a__sieve,id_a__nats => true
      | id_a__sieve,id_s => true
      | id_a__sieve,id_0 => true
      | id_a__sieve,id_a__zprimes => true
      | id_a__sieve,id_a__sieve => true
      | id_a__sieve,id_cons => false
      | id_a__sieve,id_nats => false
      | id_a__sieve,id_mark => false
      | id_a__sieve,id_filter => false
      | id_a__sieve,id_zprimes => false
      | id_a__sieve,id_sieve => false
      | id_cons,id_a__filter => true
      | id_cons,id_a__nats => true
      | id_cons,id_s => true
      | id_cons,id_0 => true
      | id_cons,id_a__zprimes => true
      | id_cons,id_a__sieve => true
      | id_cons,id_cons => true
      | id_cons,id_nats => false
      | id_cons,id_mark => false
      | id_cons,id_filter => false
      | id_cons,id_zprimes => false
      | id_cons,id_sieve => false
      | id_nats,id_a__filter => true
      | id_nats,id_a__nats => true
      | id_nats,id_s => true
      | id_nats,id_0 => true
      | id_nats,id_a__zprimes => true
      | id_nats,id_a__sieve => true
      | id_nats,id_cons => true
      | id_nats,id_nats => true
      | id_nats,id_mark => false
      | id_nats,id_filter => false
      | id_nats,id_zprimes => false
      | id_nats,id_sieve => false
      | id_mark,id_a__filter => true
      | id_mark,id_a__nats => true
      | id_mark,id_s => true
      | id_mark,id_0 => true
      | id_mark,id_a__zprimes => true
      | id_mark,id_a__sieve => true
      | id_mark,id_cons => true
      | id_mark,id_nats => true
      | id_mark,id_mark => true
      | id_mark,id_filter => false
      | id_mark,id_zprimes => false
      | id_mark,id_sieve => false
      | id_filter,id_a__filter => true
      | id_filter,id_a__nats => true
      | id_filter,id_s => true
      | id_filter,id_0 => true
      | id_filter,id_a__zprimes => true
      | id_filter,id_a__sieve => true
      | id_filter,id_cons => true
      | id_filter,id_nats => true
      | id_filter,id_mark => true
      | id_filter,id_filter => true
      | id_filter,id_zprimes => false
      | id_filter,id_sieve => false
      | id_zprimes,id_a__filter => true
      | id_zprimes,id_a__nats => true
      | id_zprimes,id_s => true
      | id_zprimes,id_0 => true
      | id_zprimes,id_a__zprimes => true
      | id_zprimes,id_a__sieve => true
      | id_zprimes,id_cons => true
      | id_zprimes,id_nats => true
      | id_zprimes,id_mark => true
      | id_zprimes,id_filter => true
      | id_zprimes,id_zprimes => true
      | id_zprimes,id_sieve => false
      | id_sieve,id_a__filter => true
      | id_sieve,id_a__nats => true
      | id_sieve,id_s => true
      | id_sieve,id_0 => true
      | id_sieve,id_a__zprimes => true
      | id_sieve,id_a__sieve => true
      | id_sieve,id_cons => true
      | id_sieve,id_nats => true
      | id_sieve,id_mark => true
      | id_sieve,id_filter => true
      | id_sieve,id_zprimes => true
      | id_sieve,id_sieve => true
      end.
  
  
  Module Symb.
   Definition A  := symb.
   
   Definition eq_A  := @eq A.
   
   
   Definition eq_proof : equivalence A eq_A.
   Proof.
     constructor.
     red ;reflexivity .
     red ;intros ;transitivity y ;assumption.
     red ;intros ;symmetry ;assumption.
   Defined.
   
   
   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
.
   
   Definition eq_bool  := symb_eq_bool.
   
   Definition eq_bool_ok  := symb_eq_bool_ok.
  End Symb.
  
  Export Symb.
 End F.
 
 Module Alg := term.Make'(F)(term_extension.IntVars).
 
 Module Alg_ext := term_extension.Make(Alg).
 
 Module EQT := equational_theory.Make(Alg).
 
 Module EQT_ext := equational_extension.Make(EQT).
End algebra.

Module R_xml_0_deep_rew.
 Inductive R_xml_0_rules  :
  algebra.Alg.term ->algebra.Alg.term ->Prop := 
    (* a__filter(cons(X_,Y_),0,M_) -> cons(0,filter(Y_,M_,M_)) *)
   | R_xml_0_rule_0 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_cons ((algebra.Alg.Term 
                   algebra.F.id_0 nil)::(algebra.Alg.Term 
                   algebra.F.id_filter ((algebra.Alg.Var 2)::
                   (algebra.Alg.Var 3)::(algebra.Alg.Var 3)::nil))::nil)) 
     (algebra.Alg.Term algebra.F.id_a__filter ((algebra.Alg.Term 
      algebra.F.id_cons ((algebra.Alg.Var 1)::(algebra.Alg.Var 2)::nil))::
      (algebra.Alg.Term algebra.F.id_0 nil)::(algebra.Alg.Var 3)::nil))
   
    (* a__filter(cons(X_,Y_),s(N_),M_) -> cons(mark(X_),filter(Y_,N_,M_)) *)
   | R_xml_0_rule_1 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_cons ((algebra.Alg.Term 
                   algebra.F.id_mark ((algebra.Alg.Var 1)::nil))::
                   (algebra.Alg.Term algebra.F.id_filter 
                   ((algebra.Alg.Var 2)::(algebra.Alg.Var 4)::
                   (algebra.Alg.Var 3)::nil))::nil)) 
     (algebra.Alg.Term algebra.F.id_a__filter ((algebra.Alg.Term 
      algebra.F.id_cons ((algebra.Alg.Var 1)::(algebra.Alg.Var 2)::nil))::
      (algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Var 4)::nil))::
      (algebra.Alg.Var 3)::nil))
    (* a__sieve(cons(0,Y_)) -> cons(0,sieve(Y_)) *)
   | R_xml_0_rule_2 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_cons ((algebra.Alg.Term 
                   algebra.F.id_0 nil)::(algebra.Alg.Term algebra.F.id_sieve 
                   ((algebra.Alg.Var 2)::nil))::nil)) 
     (algebra.Alg.Term algebra.F.id_a__sieve ((algebra.Alg.Term 
      algebra.F.id_cons ((algebra.Alg.Term algebra.F.id_0 nil)::
      (algebra.Alg.Var 2)::nil))::nil))
   
    (* a__sieve(cons(s(N_),Y_)) -> cons(s(mark(N_)),sieve(filter(Y_,N_,N_))) *)
   | R_xml_0_rule_3 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_cons ((algebra.Alg.Term 
                   algebra.F.id_s ((algebra.Alg.Term algebra.F.id_mark 
                   ((algebra.Alg.Var 4)::nil))::nil))::(algebra.Alg.Term 
                   algebra.F.id_sieve ((algebra.Alg.Term algebra.F.id_filter 
                   ((algebra.Alg.Var 2)::(algebra.Alg.Var 4)::
                   (algebra.Alg.Var 4)::nil))::nil))::nil)) 
     (algebra.Alg.Term algebra.F.id_a__sieve ((algebra.Alg.Term 
      algebra.F.id_cons ((algebra.Alg.Term algebra.F.id_s 
      ((algebra.Alg.Var 4)::nil))::(algebra.Alg.Var 2)::nil))::nil))
    (* a__nats(N_) -> cons(mark(N_),nats(s(N_))) *)
   | R_xml_0_rule_4 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_cons ((algebra.Alg.Term 
                   algebra.F.id_mark ((algebra.Alg.Var 4)::nil))::
                   (algebra.Alg.Term algebra.F.id_nats ((algebra.Alg.Term 
                   algebra.F.id_s ((algebra.Alg.Var 4)::nil))::nil))::nil)) 
     (algebra.Alg.Term algebra.F.id_a__nats ((algebra.Alg.Var 4)::nil))
    (* a__zprimes -> a__sieve(a__nats(s(s(0)))) *)
   | R_xml_0_rule_5 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_a__sieve ((algebra.Alg.Term 
                   algebra.F.id_a__nats ((algebra.Alg.Term algebra.F.id_s 
                   ((algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Term 
                   algebra.F.id_0 nil)::nil))::nil))::nil))::nil)) 
     (algebra.Alg.Term algebra.F.id_a__zprimes nil)
   
    (* mark(filter(X1_,X2_,X3_)) -> a__filter(mark(X1_),mark(X2_),mark(X3_)) *)
   | R_xml_0_rule_6 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_a__filter 
                   ((algebra.Alg.Term algebra.F.id_mark 
                   ((algebra.Alg.Var 5)::nil))::(algebra.Alg.Term 
                   algebra.F.id_mark ((algebra.Alg.Var 6)::nil))::
                   (algebra.Alg.Term algebra.F.id_mark 
                   ((algebra.Alg.Var 7)::nil))::nil)) 
     (algebra.Alg.Term algebra.F.id_mark ((algebra.Alg.Term 
      algebra.F.id_filter ((algebra.Alg.Var 5)::(algebra.Alg.Var 6)::
      (algebra.Alg.Var 7)::nil))::nil))
    (* mark(sieve(X_)) -> a__sieve(mark(X_)) *)
   | R_xml_0_rule_7 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_a__sieve ((algebra.Alg.Term 
                   algebra.F.id_mark ((algebra.Alg.Var 1)::nil))::nil)) 
     (algebra.Alg.Term algebra.F.id_mark ((algebra.Alg.Term 
      algebra.F.id_sieve ((algebra.Alg.Var 1)::nil))::nil))
    (* mark(nats(X_)) -> a__nats(mark(X_)) *)
   | R_xml_0_rule_8 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_a__nats ((algebra.Alg.Term 
                   algebra.F.id_mark ((algebra.Alg.Var 1)::nil))::nil)) 
     (algebra.Alg.Term algebra.F.id_mark ((algebra.Alg.Term 
      algebra.F.id_nats ((algebra.Alg.Var 1)::nil))::nil))
    (* mark(zprimes) -> a__zprimes *)
   | R_xml_0_rule_9 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_a__zprimes nil) 
     (algebra.Alg.Term algebra.F.id_mark ((algebra.Alg.Term 
      algebra.F.id_zprimes nil)::nil))
    (* mark(cons(X1_,X2_)) -> cons(mark(X1_),X2_) *)
   | R_xml_0_rule_10 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_cons ((algebra.Alg.Term 
                   algebra.F.id_mark ((algebra.Alg.Var 5)::nil))::
                   (algebra.Alg.Var 6)::nil)) 
     (algebra.Alg.Term algebra.F.id_mark ((algebra.Alg.Term 
      algebra.F.id_cons ((algebra.Alg.Var 5)::
      (algebra.Alg.Var 6)::nil))::nil))
    (* mark(0) -> 0 *)
   | R_xml_0_rule_11 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_0 nil) 
     (algebra.Alg.Term algebra.F.id_mark ((algebra.Alg.Term algebra.F.id_0 
      nil)::nil))
    (* mark(s(X_)) -> s(mark(X_)) *)
   | R_xml_0_rule_12 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Term 
                   algebra.F.id_mark ((algebra.Alg.Var 1)::nil))::nil)) 
     (algebra.Alg.Term algebra.F.id_mark ((algebra.Alg.Term algebra.F.id_s 
      ((algebra.Alg.Var 1)::nil))::nil))
    (* a__filter(X1_,X2_,X3_) -> filter(X1_,X2_,X3_) *)
   | R_xml_0_rule_13 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_filter 
                   ((algebra.Alg.Var 5)::(algebra.Alg.Var 6)::
                   (algebra.Alg.Var 7)::nil)) 
     (algebra.Alg.Term algebra.F.id_a__filter ((algebra.Alg.Var 5)::
      (algebra.Alg.Var 6)::(algebra.Alg.Var 7)::nil))
    (* a__sieve(X_) -> sieve(X_) *)
   | R_xml_0_rule_14 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_sieve 
                   ((algebra.Alg.Var 1)::nil)) 
     (algebra.Alg.Term algebra.F.id_a__sieve ((algebra.Alg.Var 1)::nil))
    (* a__nats(X_) -> nats(X_) *)
   | R_xml_0_rule_15 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_nats 
                   ((algebra.Alg.Var 1)::nil)) 
     (algebra.Alg.Term algebra.F.id_a__nats ((algebra.Alg.Var 1)::nil))
    (* a__zprimes -> zprimes *)
   | R_xml_0_rule_16 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_zprimes nil) 
     (algebra.Alg.Term algebra.F.id_a__zprimes nil)
 .
 
 
 Definition R_xml_0_rule_as_list_0  := 
   ((algebra.Alg.Term algebra.F.id_a__filter ((algebra.Alg.Term 
     algebra.F.id_cons ((algebra.Alg.Var 1)::(algebra.Alg.Var 2)::nil))::
     (algebra.Alg.Term algebra.F.id_0 nil)::(algebra.Alg.Var 3)::nil)),
    (algebra.Alg.Term algebra.F.id_cons ((algebra.Alg.Term algebra.F.id_0 
     nil)::(algebra.Alg.Term algebra.F.id_filter ((algebra.Alg.Var 2)::
     (algebra.Alg.Var 3)::(algebra.Alg.Var 3)::nil))::nil)))::nil.
 
 
 Definition R_xml_0_rule_as_list_1  := 
   ((algebra.Alg.Term algebra.F.id_a__filter ((algebra.Alg.Term 
     algebra.F.id_cons ((algebra.Alg.Var 1)::(algebra.Alg.Var 2)::nil))::
     (algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Var 4)::nil))::
     (algebra.Alg.Var 3)::nil)),
    (algebra.Alg.Term algebra.F.id_cons ((algebra.Alg.Term algebra.F.id_mark 
     ((algebra.Alg.Var 1)::nil))::(algebra.Alg.Term algebra.F.id_filter 
     ((algebra.Alg.Var 2)::(algebra.Alg.Var 4)::
     (algebra.Alg.Var 3)::nil))::nil)))::R_xml_0_rule_as_list_0.
 
 
 Definition R_xml_0_rule_as_list_2  := 
   ((algebra.Alg.Term algebra.F.id_a__sieve ((algebra.Alg.Term 
     algebra.F.id_cons ((algebra.Alg.Term algebra.F.id_0 nil)::
     (algebra.Alg.Var 2)::nil))::nil)),
    (algebra.Alg.Term algebra.F.id_cons ((algebra.Alg.Term algebra.F.id_0 
     nil)::(algebra.Alg.Term algebra.F.id_sieve 
     ((algebra.Alg.Var 2)::nil))::nil)))::R_xml_0_rule_as_list_1.
 
 
 Definition R_xml_0_rule_as_list_3  := 
   ((algebra.Alg.Term algebra.F.id_a__sieve ((algebra.Alg.Term 
     algebra.F.id_cons ((algebra.Alg.Term algebra.F.id_s 
     ((algebra.Alg.Var 4)::nil))::(algebra.Alg.Var 2)::nil))::nil)),
    (algebra.Alg.Term algebra.F.id_cons ((algebra.Alg.Term algebra.F.id_s 
     ((algebra.Alg.Term algebra.F.id_mark 
     ((algebra.Alg.Var 4)::nil))::nil))::(algebra.Alg.Term 
     algebra.F.id_sieve ((algebra.Alg.Term algebra.F.id_filter 
     ((algebra.Alg.Var 2)::(algebra.Alg.Var 4)::
     (algebra.Alg.Var 4)::nil))::nil))::nil)))::R_xml_0_rule_as_list_2.
 
 
 Definition R_xml_0_rule_as_list_4  := 
   ((algebra.Alg.Term algebra.F.id_a__nats ((algebra.Alg.Var 4)::nil)),
    (algebra.Alg.Term algebra.F.id_cons ((algebra.Alg.Term algebra.F.id_mark 
     ((algebra.Alg.Var 4)::nil))::(algebra.Alg.Term algebra.F.id_nats 
     ((algebra.Alg.Term algebra.F.id_s 
     ((algebra.Alg.Var 4)::nil))::nil))::nil)))::R_xml_0_rule_as_list_3.
 
 
 Definition R_xml_0_rule_as_list_5  := 
   ((algebra.Alg.Term algebra.F.id_a__zprimes nil),
    (algebra.Alg.Term algebra.F.id_a__sieve ((algebra.Alg.Term 
     algebra.F.id_a__nats ((algebra.Alg.Term algebra.F.id_s 
     ((algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Term algebra.F.id_0 
     nil)::nil))::nil))::nil))::nil)))::R_xml_0_rule_as_list_4.
 
 
 Definition R_xml_0_rule_as_list_6  := 
   ((algebra.Alg.Term algebra.F.id_mark ((algebra.Alg.Term 
     algebra.F.id_filter ((algebra.Alg.Var 5)::(algebra.Alg.Var 6)::
     (algebra.Alg.Var 7)::nil))::nil)),
    (algebra.Alg.Term algebra.F.id_a__filter ((algebra.Alg.Term 
     algebra.F.id_mark ((algebra.Alg.Var 5)::nil))::(algebra.Alg.Term 
     algebra.F.id_mark ((algebra.Alg.Var 6)::nil))::(algebra.Alg.Term 
     algebra.F.id_mark ((algebra.Alg.Var 7)::nil))::nil)))::
    R_xml_0_rule_as_list_5.
 
 
 Definition R_xml_0_rule_as_list_7  := 
   ((algebra.Alg.Term algebra.F.id_mark ((algebra.Alg.Term 
     algebra.F.id_sieve ((algebra.Alg.Var 1)::nil))::nil)),
    (algebra.Alg.Term algebra.F.id_a__sieve ((algebra.Alg.Term 
     algebra.F.id_mark ((algebra.Alg.Var 1)::nil))::nil)))::
    R_xml_0_rule_as_list_6.
 
 
 Definition R_xml_0_rule_as_list_8  := 
   ((algebra.Alg.Term algebra.F.id_mark ((algebra.Alg.Term algebra.F.id_nats 
     ((algebra.Alg.Var 1)::nil))::nil)),
    (algebra.Alg.Term algebra.F.id_a__nats ((algebra.Alg.Term 
     algebra.F.id_mark ((algebra.Alg.Var 1)::nil))::nil)))::
    R_xml_0_rule_as_list_7.
 
 
 Definition R_xml_0_rule_as_list_9  := 
   ((algebra.Alg.Term algebra.F.id_mark ((algebra.Alg.Term 
     algebra.F.id_zprimes nil)::nil)),
    (algebra.Alg.Term algebra.F.id_a__zprimes nil))::R_xml_0_rule_as_list_8.
 
 
 Definition R_xml_0_rule_as_list_10  := 
   ((algebra.Alg.Term algebra.F.id_mark ((algebra.Alg.Term algebra.F.id_cons 
     ((algebra.Alg.Var 5)::(algebra.Alg.Var 6)::nil))::nil)),
    (algebra.Alg.Term algebra.F.id_cons ((algebra.Alg.Term algebra.F.id_mark 
     ((algebra.Alg.Var 5)::nil))::(algebra.Alg.Var 6)::nil)))::
    R_xml_0_rule_as_list_9.
 
 
 Definition R_xml_0_rule_as_list_11  := 
   ((algebra.Alg.Term algebra.F.id_mark ((algebra.Alg.Term algebra.F.id_0 
     nil)::nil)),(algebra.Alg.Term algebra.F.id_0 nil))::
    R_xml_0_rule_as_list_10.
 
 
 Definition R_xml_0_rule_as_list_12  := 
   ((algebra.Alg.Term algebra.F.id_mark ((algebra.Alg.Term algebra.F.id_s 
     ((algebra.Alg.Var 1)::nil))::nil)),
    (algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Term algebra.F.id_mark 
     ((algebra.Alg.Var 1)::nil))::nil)))::R_xml_0_rule_as_list_11.
 
 
 Definition R_xml_0_rule_as_list_13  := 
   ((algebra.Alg.Term algebra.F.id_a__filter ((algebra.Alg.Var 5)::
     (algebra.Alg.Var 6)::(algebra.Alg.Var 7)::nil)),
    (algebra.Alg.Term algebra.F.id_filter ((algebra.Alg.Var 5)::
     (algebra.Alg.Var 6)::(algebra.Alg.Var 7)::nil)))::
    R_xml_0_rule_as_list_12.
 
 
 Definition R_xml_0_rule_as_list_14  := 
   ((algebra.Alg.Term algebra.F.id_a__sieve ((algebra.Alg.Var 1)::nil)),
    (algebra.Alg.Term algebra.F.id_sieve ((algebra.Alg.Var 1)::nil)))::
    R_xml_0_rule_as_list_13.
 
 
 Definition R_xml_0_rule_as_list_15  := 
   ((algebra.Alg.Term algebra.F.id_a__nats ((algebra.Alg.Var 1)::nil)),
    (algebra.Alg.Term algebra.F.id_nats ((algebra.Alg.Var 1)::nil)))::
    R_xml_0_rule_as_list_14.
 
 
 Definition R_xml_0_rule_as_list_16  := 
   ((algebra.Alg.Term algebra.F.id_a__zprimes nil),
    (algebra.Alg.Term algebra.F.id_zprimes nil))::R_xml_0_rule_as_list_15.
 
 Definition R_xml_0_rule_as_list  := R_xml_0_rule_as_list_16.
 
 
 Lemma R_xml_0_rules_included :
  forall l r, R_xml_0_rules r l <-> In (l,r) R_xml_0_rule_as_list.
 Proof.
   intros l r.
   constructor.
   intros H.
   
   case H;clear H;
    (apply (more_list.mem_impl_in (@eq (algebra.Alg.term*algebra.Alg.term)));
     [tauto|idtac]);
    match goal with
      |  |- _ _ _ ?t ?l =>
       let u := fresh "u" in 
        (generalize (more_list.mem_bool_ok _ _ 
                      algebra.Alg_ext.eq_term_term_bool_ok t l);
          set (u:=more_list.mem_bool algebra.Alg_ext.eq_term_term_bool t l) in *;
          vm_compute in u|-;unfold u in *;clear u;intros H;refine H)
      end
    .
   intros H.
   vm_compute in H|-.
   rewrite  <- or_ext_generated.or18_equiv in H|-.
   case H;clear H;intros H.
   injection H;intros ;subst;constructor 17.
   injection H;intros ;subst;constructor 16.
   injection H;intros ;subst;constructor 15.
   injection H;intros ;subst;constructor 14.
   injection H;intros ;subst;constructor 13.
   injection H;intros ;subst;constructor 12.
   injection H;intros ;subst;constructor 11.
   injection H;intros ;subst;constructor 10.
   injection H;intros ;subst;constructor 9.
   injection H;intros ;subst;constructor 8.
   injection H;intros ;subst;constructor 7.
   injection H;intros ;subst;constructor 6.
   injection H;intros ;subst;constructor 5.
   injection H;intros ;subst;constructor 4.
   injection H;intros ;subst;constructor 3.
   injection H;intros ;subst;constructor 2.
   injection H;intros ;subst;constructor 1.
   elim H.
 Qed.
 
 
 Lemma R_xml_0_non_var : forall x t, ~R_xml_0_rules t (algebra.EQT.T.Var x).
 Proof.
   intros x t H.
   inversion H.
 Qed.
 
 
 Lemma R_xml_0_reg :
  forall s t, 
   (R_xml_0_rules s t) ->
    forall x, In x (algebra.Alg.var_list s) ->In x (algebra.Alg.var_list t).
 Proof.
   intros s t H.
   
   inversion H;intros x Hx;
    (apply (more_list.mem_impl_in (@eq algebra.Alg.variable));[tauto|idtac]);
    apply (more_list.in_impl_mem (@eq algebra.Alg.variable)) in Hx;
    vm_compute in Hx|-*;tauto.
 Qed.
 
 
 Inductive and_7 (x9 x10 x11 x12 x13 x14 x15:Prop) :
  Prop := 
   | conj_7 :
    x9->x10->x11->x12->x13->x14->x15->and_7 x9 x10 x11 x12 x13 x14 x15
 .
 
 
 Lemma are_constuctors_of_R_xml_0 :
  forall t t', 
   (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
    and_7 (forall x10, 
           t = (algebra.Alg.Term algebra.F.id_s (x10::nil)) ->
            exists x9,
              t' = (algebra.Alg.Term algebra.F.id_s (x9::nil))/\ 
              (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
                x9 x10)) 
     (t = (algebra.Alg.Term algebra.F.id_0 nil) ->
      t' = (algebra.Alg.Term algebra.F.id_0 nil)) 
     (forall x10 x12, 
      t = (algebra.Alg.Term algebra.F.id_cons (x10::x12::nil)) ->
       exists x9,
         exists x11,
           t' = (algebra.Alg.Term algebra.F.id_cons (x9::x11::nil))/\ 
           (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
             x9 x10)/\ 
           (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
             x11 x12)) 
     (forall x10, 
      t = (algebra.Alg.Term algebra.F.id_nats (x10::nil)) ->
       exists x9,
         t' = (algebra.Alg.Term algebra.F.id_nats (x9::nil))/\ 
         (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x9 x10))
       
     (forall x10 x12 x14, 
      t = (algebra.Alg.Term algebra.F.id_filter (x10::x12::x14::nil)) ->
       exists x9,
         exists x11,
           exists x13,
             t' = (algebra.Alg.Term algebra.F.id_filter (x9::x11::x13::nil))/\
              
             (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
               x9 x10)/\ 
             (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
               x11 x12)/\ 
             (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
               x13 x14)) 
     (t = (algebra.Alg.Term algebra.F.id_zprimes nil) ->
      t' = (algebra.Alg.Term algebra.F.id_zprimes nil)) 
     (forall x10, 
      t = (algebra.Alg.Term algebra.F.id_sieve (x10::nil)) ->
       exists x9,
         t' = (algebra.Alg.Term algebra.F.id_sieve (x9::nil))/\ 
         (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x9 x10))
      .
 Proof.
   intros t t' H.
   
   induction H as [|y IH z z_to_y] using 
   closure_extension.refl_trans_clos_ind2.
   constructor 1.
   intros x10 H;exists x10;intuition;constructor 1.
   intros H;intuition;constructor 1.
   intros x10 x12 H;exists x10;exists x12;intuition;constructor 1.
   intros x10 H;exists x10;intuition;constructor 1.
   
   intros x10 x12 x14 H;exists x10;exists x12;exists x14;intuition;
    constructor 1.
   intros H;intuition;constructor 1.
   intros x10 H;exists x10;intuition;constructor 1.
   inversion z_to_y as [t1 t2 H H0 H1|f l1 l2 H0 H H2];clear z_to_y;subst.
   
   inversion H as [t1 t2 sigma H2 H1 H0];clear H IH;subst;inversion H2;
    clear ;constructor;try (intros until 0 );clear ;intros abs;
    discriminate abs.
   
   destruct IH as 
   [H_id_s H_id_0 H_id_cons H_id_nats H_id_filter H_id_zprimes H_id_sieve].
   constructor.
   
   clear H_id_0 H_id_cons H_id_nats H_id_filter H_id_zprimes H_id_sieve;
    intros x10 H;injection H;clear H;intros ;subst;
    repeat (
    match goal with
      | H:closure.one_step_list (algebra.EQT.one_step _) _ _ |- _ =>
       inversion H;clear H;subst
      end
    ).
   
   match goal with
     | H:algebra.EQT.one_step _ ?y x10 |- _ =>
      destruct (H_id_s y (refl_equal _)) as [x9];intros ;intuition;exists x9;
       intuition;eapply closure_extension.refl_trans_clos_R;eassumption
     end
   .
   
   clear H_id_s H_id_cons H_id_nats H_id_filter H_id_zprimes H_id_sieve;
    intros H;injection H;clear H;intros ;subst;
    repeat (
    match goal with
      | H:closure.one_step_list (algebra.EQT.one_step _) _ _ |- _ =>
       inversion H;clear H;subst
      end
    ).
   
   clear H_id_s H_id_0 H_id_nats H_id_filter H_id_zprimes H_id_sieve;
    intros x10 x12 H;injection H;clear H;intros ;subst;
    repeat (
    match goal with
      | H:closure.one_step_list (algebra.EQT.one_step _) _ _ |- _ =>
       inversion H;clear H;subst
      end
    ).
   
   match goal with
     | H:algebra.EQT.one_step _ ?y x10 |- _ =>
      destruct (H_id_cons y x12 (refl_equal _)) as [x9 [x11]];intros ;
       intuition;exists x9;exists x11;intuition;
       eapply closure_extension.refl_trans_clos_R;eassumption
     end
   .
   
   match goal with
     | H:algebra.EQT.one_step _ ?y x12 |- _ =>
      destruct (H_id_cons x10 y (refl_equal _)) as [x9 [x11]];intros ;
       intuition;exists x9;exists x11;intuition;
       eapply closure_extension.refl_trans_clos_R;eassumption
     end
   .
   
   clear H_id_s H_id_0 H_id_cons H_id_filter H_id_zprimes H_id_sieve;
    intros x10 H;injection H;clear H;intros ;subst;
    repeat (
    match goal with
      | H:closure.one_step_list (algebra.EQT.one_step _) _ _ |- _ =>
       inversion H;clear H;subst
      end
    ).
   
   match goal with
     | H:algebra.EQT.one_step _ ?y x10 |- _ =>
      destruct (H_id_nats y (refl_equal _)) as [x9];intros ;intuition;
       exists x9;intuition;eapply closure_extension.refl_trans_clos_R;
       eassumption
     end
   .
   
   clear H_id_s H_id_0 H_id_cons H_id_nats H_id_zprimes H_id_sieve;
    intros x10 x12 x14 H;injection H;clear H;intros ;subst;
    repeat (
    match goal with
      | H:closure.one_step_list (algebra.EQT.one_step _) _ _ |- _ =>
       inversion H;clear H;subst
      end
    ).
   
   match goal with
     | H:algebra.EQT.one_step _ ?y x10 |- _ =>
      destruct (H_id_filter y x12 x14 (refl_equal _)) as [x9 [x11 [x13]]];
       intros ;intuition;exists x9;exists x11;exists x13;intuition;
       eapply closure_extension.refl_trans_clos_R;eassumption
     end
   .
   
   match goal with
     | H:algebra.EQT.one_step _ ?y x12 |- _ =>
      destruct (H_id_filter x10 y x14 (refl_equal _)) as [x9 [x11 [x13]]];
       intros ;intuition;exists x9;exists x11;exists x13;intuition;
       eapply closure_extension.refl_trans_clos_R;eassumption
     end
   .
   
   match goal with
     | H:algebra.EQT.one_step _ ?y x14 |- _ =>
      destruct (H_id_filter x10 x12 y (refl_equal _)) as [x9 [x11 [x13]]];
       intros ;intuition;exists x9;exists x11;exists x13;intuition;
       eapply closure_extension.refl_trans_clos_R;eassumption
     end
   .
   
   clear H_id_s H_id_0 H_id_cons H_id_nats H_id_filter H_id_sieve;intros H;
    injection H;clear H;intros ;subst;
    repeat (
    match goal with
      | H:closure.one_step_list (algebra.EQT.one_step _) _ _ |- _ =>
       inversion H;clear H;subst
      end
    ).
   
   clear H_id_s H_id_0 H_id_cons H_id_nats H_id_filter H_id_zprimes;
    intros x10 H;injection H;clear H;intros ;subst;
    repeat (
    match goal with
      | H:closure.one_step_list (algebra.EQT.one_step _) _ _ |- _ =>
       inversion H;clear H;subst
      end
    ).
   
   match goal with
     | H:algebra.EQT.one_step _ ?y x10 |- _ =>
      destruct (H_id_sieve y (refl_equal _)) as [x9];intros ;intuition;
       exists x9;intuition;eapply closure_extension.refl_trans_clos_R;
       eassumption
     end
   .
 Qed.
 
 
 Lemma id_s_is_R_xml_0_constructor :
  forall t t', 
   (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
    forall x10, 
     t = (algebra.Alg.Term algebra.F.id_s (x10::nil)) ->
      exists x9,
        t' = (algebra.Alg.Term algebra.F.id_s (x9::nil))/\ 
        (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x9 x10).
 Proof.
   intros t t' H.
   destruct (are_constuctors_of_R_xml_0 H).
   assumption.
 Qed.
 
 
 Lemma id_0_is_R_xml_0_constructor :
  forall t t', 
   (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
    t = (algebra.Alg.Term algebra.F.id_0 nil) ->
     t' = (algebra.Alg.Term algebra.F.id_0 nil).
 Proof.
   intros t t' H.
   destruct (are_constuctors_of_R_xml_0 H).
   assumption.
 Qed.
 
 
 Lemma id_cons_is_R_xml_0_constructor :
  forall t t', 
   (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
    forall x10 x12, 
     t = (algebra.Alg.Term algebra.F.id_cons (x10::x12::nil)) ->
      exists x9,
        exists x11,
          t' = (algebra.Alg.Term algebra.F.id_cons (x9::x11::nil))/\ 
          (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
            x9 x10)/\ 
          (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
            x11 x12).
 Proof.
   intros t t' H.
   destruct (are_constuctors_of_R_xml_0 H).
   assumption.
 Qed.
 
 
 Lemma id_nats_is_R_xml_0_constructor :
  forall t t', 
   (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
    forall x10, 
     t = (algebra.Alg.Term algebra.F.id_nats (x10::nil)) ->
      exists x9,
        t' = (algebra.Alg.Term algebra.F.id_nats (x9::nil))/\ 
        (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x9 x10).
 Proof.
   intros t t' H.
   destruct (are_constuctors_of_R_xml_0 H).
   assumption.
 Qed.
 
 
 Lemma id_filter_is_R_xml_0_constructor :
  forall t t', 
   (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
    forall x10 x12 x14, 
     t = (algebra.Alg.Term algebra.F.id_filter (x10::x12::x14::nil)) ->
      exists x9,
        exists x11,
          exists x13,
            t' = (algebra.Alg.Term algebra.F.id_filter (x9::x11::x13::nil))/\
             
            (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
              x9 x10)/\ 
            (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
              x11 x12)/\ 
            (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
              x13 x14).
 Proof.
   intros t t' H.
   destruct (are_constuctors_of_R_xml_0 H).
   assumption.
 Qed.
 
 
 Lemma id_zprimes_is_R_xml_0_constructor :
  forall t t', 
   (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
    t = (algebra.Alg.Term algebra.F.id_zprimes nil) ->
     t' = (algebra.Alg.Term algebra.F.id_zprimes nil).
 Proof.
   intros t t' H.
   destruct (are_constuctors_of_R_xml_0 H).
   assumption.
 Qed.
 
 
 Lemma id_sieve_is_R_xml_0_constructor :
  forall t t', 
   (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
    forall x10, 
     t = (algebra.Alg.Term algebra.F.id_sieve (x10::nil)) ->
      exists x9,
        t' = (algebra.Alg.Term algebra.F.id_sieve (x9::nil))/\ 
        (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x9 x10).
 Proof.
   intros t t' H.
   destruct (are_constuctors_of_R_xml_0 H).
   assumption.
 Qed.
 
 
 Ltac impossible_star_reduction_R_xml_0  :=
  match goal with
    | H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
         _ (algebra.Alg.Term algebra.F.id_s (?x9::nil)) |- _ =>
     let x9 := fresh "x" in 
      (let Heq := fresh "Heq" in 
        (let Hred1 := fresh "Hred" in 
          (destruct (id_s_is_R_xml_0_constructor H (refl_equal _)) as 
           [x9 [Heq Hred1]];
            (discriminate Heq)||
            (injection Heq;intros ;subst;clear Heq;clear H;
              impossible_star_reduction_R_xml_0 ))))
    | H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
         _ (algebra.Alg.Term algebra.F.id_0 nil) |- _ =>
     let Heq := fresh "Heq" in 
      (set (Heq:=id_0_is_R_xml_0_constructor H (refl_equal _)) in *;
        (discriminate Heq)||
        (clearbody Heq;try (subst);try (clear Heq);clear H;
          impossible_star_reduction_R_xml_0 ))
    | H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
         _ (algebra.Alg.Term algebra.F.id_cons (?x10::?x9::nil)) |- _ =>
     let x10 := fresh "x" in 
      (let x9 := fresh "x" in 
        (let Heq := fresh "Heq" in 
          (let Hred1 := fresh "Hred" in 
            (let Hred2 := fresh "Hred" in 
              (destruct (id_cons_is_R_xml_0_constructor H (refl_equal _)) as 
               [x10 [x9 [Heq [Hred2 Hred1]]]];
                (discriminate Heq)||
                (injection Heq;intros ;subst;clear Heq;clear H;
                  impossible_star_reduction_R_xml_0 ))))))
    | H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
         _ (algebra.Alg.Term algebra.F.id_nats (?x9::nil)) |- _ =>
     let x9 := fresh "x" in 
      (let Heq := fresh "Heq" in 
        (let Hred1 := fresh "Hred" in 
          (destruct (id_nats_is_R_xml_0_constructor H (refl_equal _)) as 
           [x9 [Heq Hred1]];
            (discriminate Heq)||
            (injection Heq;intros ;subst;clear Heq;clear H;
              impossible_star_reduction_R_xml_0 ))))
    | H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
         _ (algebra.Alg.Term algebra.F.id_filter (?x11::?x10::?x9::nil)) |- 
    _ =>
     let x11 := fresh "x" in 
      (let x10 := fresh "x" in 
        (let x9 := fresh "x" in 
          (let Heq := fresh "Heq" in 
            (let Hred1 := fresh "Hred" in 
              (let Hred2 := fresh "Hred" in 
                (let Hred3 := fresh "Hred" in 
                  (destruct (id_filter_is_R_xml_0_constructor H 
                              (refl_equal _))
                    as [x11 [x10 [x9 [Heq [Hred3 [Hred2 Hred1]]]]]];
                    (discriminate Heq)||
                    (injection Heq;intros ;subst;clear Heq;clear H;
                      impossible_star_reduction_R_xml_0 ))))))))
    | H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
         _ (algebra.Alg.Term algebra.F.id_zprimes nil) |- _ =>
     let Heq := fresh "Heq" in 
      (set (Heq:=id_zprimes_is_R_xml_0_constructor H (refl_equal _)) in *;
        (discriminate Heq)||
        (clearbody Heq;try (subst);try (clear Heq);clear H;
          impossible_star_reduction_R_xml_0 ))
    | H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
         _ (algebra.Alg.Term algebra.F.id_sieve (?x9::nil)) |- _ =>
     let x9 := fresh "x" in 
      (let Heq := fresh "Heq" in 
        (let Hred1 := fresh "Hred" in 
          (destruct (id_sieve_is_R_xml_0_constructor H (refl_equal _)) as 
           [x9 [Heq Hred1]];
            (discriminate Heq)||
            (injection Heq;intros ;subst;clear Heq;clear H;
              impossible_star_reduction_R_xml_0 ))))
    end
  .
 
 
 Ltac simplify_star_reduction_R_xml_0  :=
  match goal with
    | H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
         _ (algebra.Alg.Term algebra.F.id_s (?x9::nil)) |- _ =>
     let x9 := fresh "x" in 
      (let Heq := fresh "Heq" in 
        (let Hred1 := fresh "Hred" in 
          (destruct (id_s_is_R_xml_0_constructor H (refl_equal _)) as 
           [x9 [Heq Hred1]];
            (discriminate Heq)||
            (injection Heq;intros ;subst;clear Heq;clear H;
              try (simplify_star_reduction_R_xml_0 )))))
    | H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
         _ (algebra.Alg.Term algebra.F.id_0 nil) |- _ =>
     let Heq := fresh "Heq" in 
      (set (Heq:=id_0_is_R_xml_0_constructor H (refl_equal _)) in *;
        (discriminate Heq)||
        (clearbody Heq;try (subst);try (clear Heq);clear H;
          try (simplify_star_reduction_R_xml_0 )))
    | H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
         _ (algebra.Alg.Term algebra.F.id_cons (?x10::?x9::nil)) |- _ =>
     let x10 := fresh "x" in 
      (let x9 := fresh "x" in 
        (let Heq := fresh "Heq" in 
          (let Hred1 := fresh "Hred" in 
            (let Hred2 := fresh "Hred" in 
              (destruct (id_cons_is_R_xml_0_constructor H (refl_equal _)) as 
               [x10 [x9 [Heq [Hred2 Hred1]]]];
                (discriminate Heq)||
                (injection Heq;intros ;subst;clear Heq;clear H;
                  try (simplify_star_reduction_R_xml_0 )))))))
    | H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
         _ (algebra.Alg.Term algebra.F.id_nats (?x9::nil)) |- _ =>
     let x9 := fresh "x" in 
      (let Heq := fresh "Heq" in 
        (let Hred1 := fresh "Hred" in 
          (destruct (id_nats_is_R_xml_0_constructor H (refl_equal _)) as 
           [x9 [Heq Hred1]];
            (discriminate Heq)||
            (injection Heq;intros ;subst;clear Heq;clear H;
              try (simplify_star_reduction_R_xml_0 )))))
    | H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
         _ (algebra.Alg.Term algebra.F.id_filter (?x11::?x10::?x9::nil)) |- 
    _ =>
     let x11 := fresh "x" in 
      (let x10 := fresh "x" in 
        (let x9 := fresh "x" in 
          (let Heq := fresh "Heq" in 
            (let Hred1 := fresh "Hred" in 
              (let Hred2 := fresh "Hred" in 
                (let Hred3 := fresh "Hred" in 
                  (destruct (id_filter_is_R_xml_0_constructor H 
                              (refl_equal _))
                    as [x11 [x10 [x9 [Heq [Hred3 [Hred2 Hred1]]]]]];
                    (discriminate Heq)||
                    (injection Heq;intros ;subst;clear Heq;clear H;
                      try (simplify_star_reduction_R_xml_0 )))))))))
    | H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
         _ (algebra.Alg.Term algebra.F.id_zprimes nil) |- _ =>
     let Heq := fresh "Heq" in 
      (set (Heq:=id_zprimes_is_R_xml_0_constructor H (refl_equal _)) in *;
        (discriminate Heq)||
        (clearbody Heq;try (subst);try (clear Heq);clear H;
          try (simplify_star_reduction_R_xml_0 )))
    | H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
         _ (algebra.Alg.Term algebra.F.id_sieve (?x9::nil)) |- _ =>
     let x9 := fresh "x" in 
      (let Heq := fresh "Heq" in 
        (let Hred1 := fresh "Hred" in 
          (destruct (id_sieve_is_R_xml_0_constructor H (refl_equal _)) as 
           [x9 [Heq Hred1]];
            (discriminate Heq)||
            (injection Heq;intros ;subst;clear Heq;clear H;
              try (simplify_star_reduction_R_xml_0 )))))
    end
  .
End R_xml_0_deep_rew.

Module InterpGen := interp.Interp(algebra.EQT).

Module ddp := dp.MakeDP(algebra.EQT).

Module SymbType. Definition A := algebra.Alg.F.Symb.A. End SymbType.

Module Symb_more_list := more_list_extention.Make(SymbType)(algebra.Alg.F.Symb).

Module SymbSet := list_set.Make(algebra.F.Symb).

Module Interp.
 Section S.
   Require Import interp.
   
   Hypothesis A : Type.
   
   Hypothesis Ale Alt Aeq : A -> A -> Prop.
   
   Hypothesis Aop : interp.ordering_pair Aeq Alt Ale.
   
   Hypothesis A0 : A.
   
   Notation Local "a <= b" := (Ale a b).
   
   Hypothesis P_id_a__filter : A ->A ->A ->A.
   
   Hypothesis P_id_a__nats : A ->A.
   
   Hypothesis P_id_s : A ->A.
   
   Hypothesis P_id_0 : A.
   
   Hypothesis P_id_a__zprimes : A.
   
   Hypothesis P_id_a__sieve : A ->A.
   
   Hypothesis P_id_cons : A ->A ->A.
   
   Hypothesis P_id_nats : A ->A.
   
   Hypothesis P_id_mark : A ->A.
   
   Hypothesis P_id_filter : A ->A ->A ->A.
   
   Hypothesis P_id_zprimes : A.
   
   Hypothesis P_id_sieve : A ->A.
   
   Hypothesis P_id_a__filter_monotonic :
    forall x12 x10 x14 x9 x13 x11, 
     (A0 <= x14)/\ (x14 <= x13) ->
      (A0 <= x12)/\ (x12 <= x11) ->
       (A0 <= x10)/\ (x10 <= x9) ->
        P_id_a__filter x10 x12 x14 <= P_id_a__filter x9 x11 x13.
   
   Hypothesis P_id_a__nats_monotonic :
    forall x10 x9, 
     (A0 <= x10)/\ (x10 <= x9) ->P_id_a__nats x10 <= P_id_a__nats x9.
   
   Hypothesis P_id_s_monotonic :
    forall x10 x9, (A0 <= x10)/\ (x10 <= x9) ->P_id_s x10 <= P_id_s x9.
   
   Hypothesis P_id_a__sieve_monotonic :
    forall x10 x9, 
     (A0 <= x10)/\ (x10 <= x9) ->P_id_a__sieve x10 <= P_id_a__sieve x9.
   
   Hypothesis P_id_cons_monotonic :
    forall x12 x10 x9 x11, 
     (A0 <= x12)/\ (x12 <= x11) ->
      (A0 <= x10)/\ (x10 <= x9) ->P_id_cons x10 x12 <= P_id_cons x9 x11.
   
   Hypothesis P_id_nats_monotonic :
    forall x10 x9, (A0 <= x10)/\ (x10 <= x9) ->P_id_nats x10 <= P_id_nats x9.
   
   Hypothesis P_id_mark_monotonic :
    forall x10 x9, (A0 <= x10)/\ (x10 <= x9) ->P_id_mark x10 <= P_id_mark x9.
   
   Hypothesis P_id_filter_monotonic :
    forall x12 x10 x14 x9 x13 x11, 
     (A0 <= x14)/\ (x14 <= x13) ->
      (A0 <= x12)/\ (x12 <= x11) ->
       (A0 <= x10)/\ (x10 <= x9) ->
        P_id_filter x10 x12 x14 <= P_id_filter x9 x11 x13.
   
   Hypothesis P_id_sieve_monotonic :
    forall x10 x9, 
     (A0 <= x10)/\ (x10 <= x9) ->P_id_sieve x10 <= P_id_sieve x9.
   
   Hypothesis P_id_a__filter_bounded :
    forall x10 x9 x11, 
     (A0 <= x9) ->(A0 <= x10) ->(A0 <= x11) ->A0 <= P_id_a__filter x11 x10 x9.
   
   Hypothesis P_id_a__nats_bounded :
    forall x9, (A0 <= x9) ->A0 <= P_id_a__nats x9.
   
   Hypothesis P_id_s_bounded : forall x9, (A0 <= x9) ->A0 <= P_id_s x9.
   
   Hypothesis P_id_0_bounded : A0 <= P_id_0 .
   
   Hypothesis P_id_a__zprimes_bounded : A0 <= P_id_a__zprimes .
   
   Hypothesis P_id_a__sieve_bounded :
    forall x9, (A0 <= x9) ->A0 <= P_id_a__sieve x9.
   
   Hypothesis P_id_cons_bounded :
    forall x10 x9, (A0 <= x9) ->(A0 <= x10) ->A0 <= P_id_cons x10 x9.
   
   Hypothesis P_id_nats_bounded : forall x9, (A0 <= x9) ->A0 <= P_id_nats x9.
   
   Hypothesis P_id_mark_bounded : forall x9, (A0 <= x9) ->A0 <= P_id_mark x9.
   
   Hypothesis P_id_filter_bounded :
    forall x10 x9 x11, 
     (A0 <= x9) ->(A0 <= x10) ->(A0 <= x11) ->A0 <= P_id_filter x11 x10 x9.
   
   Hypothesis P_id_zprimes_bounded : A0 <= P_id_zprimes .
   
   Hypothesis P_id_sieve_bounded :
    forall x9, (A0 <= x9) ->A0 <= P_id_sieve x9.
   
   Fixpoint measure t { struct t }  := 
     match t with
       | (algebra.Alg.Term algebra.F.id_a__filter (x11::x10::x9::nil)) =>
        P_id_a__filter (measure x11) (measure x10) (measure x9)
       | (algebra.Alg.Term algebra.F.id_a__nats (x9::nil)) =>
        P_id_a__nats (measure x9)
       | (algebra.Alg.Term algebra.F.id_s (x9::nil)) => P_id_s (measure x9)
       | (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0 
       | (algebra.Alg.Term algebra.F.id_a__zprimes nil) => P_id_a__zprimes 
       | (algebra.Alg.Term algebra.F.id_a__sieve (x9::nil)) =>
        P_id_a__sieve (measure x9)
       | (algebra.Alg.Term algebra.F.id_cons (x10::x9::nil)) =>
        P_id_cons (measure x10) (measure x9)
       | (algebra.Alg.Term algebra.F.id_nats (x9::nil)) =>
        P_id_nats (measure x9)
       | (algebra.Alg.Term algebra.F.id_mark (x9::nil)) =>
        P_id_mark (measure x9)
       | (algebra.Alg.Term algebra.F.id_filter (x11::x10::x9::nil)) =>
        P_id_filter (measure x11) (measure x10) (measure x9)
       | (algebra.Alg.Term algebra.F.id_zprimes nil) => P_id_zprimes 
       | (algebra.Alg.Term algebra.F.id_sieve (x9::nil)) =>
        P_id_sieve (measure x9)
       | _ => A0
       end.
   
   Lemma measure_equation :
    forall t, 
     measure t = match t with
                   | (algebra.Alg.Term algebra.F.id_a__filter (x11::x10::
                      x9::nil)) =>
                    P_id_a__filter (measure x11) (measure x10) (measure x9)
                   | (algebra.Alg.Term algebra.F.id_a__nats (x9::nil)) =>
                    P_id_a__nats (measure x9)
                   | (algebra.Alg.Term algebra.F.id_s (x9::nil)) =>
                    P_id_s (measure x9)
                   | (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0 
                   | (algebra.Alg.Term algebra.F.id_a__zprimes nil) =>
                    P_id_a__zprimes 
                   | (algebra.Alg.Term algebra.F.id_a__sieve (x9::nil)) =>
                    P_id_a__sieve (measure x9)
                   | (algebra.Alg.Term algebra.F.id_cons (x10::x9::nil)) =>
                    P_id_cons (measure x10) (measure x9)
                   | (algebra.Alg.Term algebra.F.id_nats (x9::nil)) =>
                    P_id_nats (measure x9)
                   | (algebra.Alg.Term algebra.F.id_mark (x9::nil)) =>
                    P_id_mark (measure x9)
                   | (algebra.Alg.Term algebra.F.id_filter (x11::x10::
                      x9::nil)) =>
                    P_id_filter (measure x11) (measure x10) (measure x9)
                   | (algebra.Alg.Term algebra.F.id_zprimes nil) =>
                    P_id_zprimes 
                   | (algebra.Alg.Term algebra.F.id_sieve (x9::nil)) =>
                    P_id_sieve (measure x9)
                   | _ => A0
                   end.
   Proof.
     intros t;case t;intros ;apply refl_equal.
   Qed.
   
   Definition Pols f : InterpGen.Pol_type A (InterpGen.get_arity f) := 
     match f with
       | algebra.F.id_a__filter => P_id_a__filter
       | algebra.F.id_a__nats => P_id_a__nats
       | algebra.F.id_s => P_id_s
       | algebra.F.id_0 => P_id_0
       | algebra.F.id_a__zprimes => P_id_a__zprimes
       | algebra.F.id_a__sieve => P_id_a__sieve
       | algebra.F.id_cons => P_id_cons
       | algebra.F.id_nats => P_id_nats
       | algebra.F.id_mark => P_id_mark
       | algebra.F.id_filter => P_id_filter
       | algebra.F.id_zprimes => P_id_zprimes
       | algebra.F.id_sieve => P_id_sieve
       end.
   
   Lemma same_measure : forall t, measure t = InterpGen.measure A0 Pols t.
   Proof.
     fix 1 .
     intros [a| f l].
     simpl in |-*.
     unfold eq_rect_r, eq_rect, sym_eq in |-*.
     reflexivity .
     
     refine match f with
              | algebra.F.id_a__filter =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::nil => _
                 | _::_::_::nil => _
                 | _::_::_::_::_ => _
                 end
              | algebra.F.id_a__nats =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::_ => _
                 end
              | algebra.F.id_s =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::_ => _
                 end
              | algebra.F.id_0 => match l with
                                    | nil => _
                                    | _::_ => _
                                    end
              | algebra.F.id_a__zprimes =>
               match l with
                 | nil => _
                 | _::_ => _
                 end
              | algebra.F.id_a__sieve =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::_ => _
                 end
              | algebra.F.id_cons =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::nil => _
                 | _::_::_::_ => _
                 end
              | algebra.F.id_nats =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::_ => _
                 end
              | algebra.F.id_mark =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::_ => _
                 end
              | algebra.F.id_filter =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::nil => _
                 | _::_::_::nil => _
                 | _::_::_::_::_ => _
                 end
              | algebra.F.id_zprimes => match l with
                                          | nil => _
                                          | _::_ => _
                                          end
              | algebra.F.id_sieve =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::_ => _
                 end
              end;simpl in |-*;unfold eq_rect_r, eq_rect, sym_eq in |-*;
      try (reflexivity );f_equal ;auto.
   Qed.
   
   Lemma measure_bounded : forall t, A0 <= measure t.
   Proof.
     intros t.
     rewrite same_measure in |-*.
     apply (InterpGen.measure_bounded Aop).
     intros f.
     case f.
     vm_compute in |-*;intros ;apply P_id_a__filter_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_a__nats_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_s_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_0_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_a__zprimes_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_a__sieve_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_cons_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_nats_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_mark_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_filter_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_zprimes_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_sieve_bounded;assumption.
   Qed.
   
   Ltac generate_pos_hyp  :=
    match goal with
      | H:context [measure ?x] |- _ =>
       let v := fresh "v" in 
        (let H := fresh "h" in 
          (set (H:=measure_bounded x) in *;set (v:=measure x) in *;
            clearbody H;clearbody v))
      |  |- context [measure ?x] =>
       let v := fresh "v" in 
        (let H := fresh "h" in 
          (set (H:=measure_bounded x) in *;set (v:=measure x) in *;
            clearbody H;clearbody v))
      end
    .
   
   Hypothesis rules_monotonic :
    forall l r, 
     (algebra.EQT.axiom R_xml_0_deep_rew.R_xml_0_rules r l) ->
      measure r <= measure l.
   
   Lemma measure_star_monotonic :
    forall l r, 
     (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                r l) ->measure r <= measure l.
   Proof.
     intros .
     do 2 (rewrite same_measure in |-*).
     
     apply InterpGen.measure_star_monotonic with (1:=Aop) (Pols:=Pols) 
     (rules:=R_xml_0_deep_rew.R_xml_0_rules).
     intros f.
     case f.
     vm_compute in |-*;intros ;apply P_id_a__filter_monotonic;assumption.
     vm_compute in |-*;intros ;apply P_id_a__nats_monotonic;assumption.
     vm_compute in |-*;intros ;apply P_id_s_monotonic;assumption.
     vm_compute in |-*;apply (Aop.(le_refl)).
     vm_compute in |-*;apply (Aop.(le_refl)).
     vm_compute in |-*;intros ;apply P_id_a__sieve_monotonic;assumption.
     vm_compute in |-*;intros ;apply P_id_cons_monotonic;assumption.
     vm_compute in |-*;intros ;apply P_id_nats_monotonic;assumption.
     vm_compute in |-*;intros ;apply P_id_mark_monotonic;assumption.
     vm_compute in |-*;intros ;apply P_id_filter_monotonic;assumption.
     vm_compute in |-*;apply (Aop.(le_refl)).
     vm_compute in |-*;intros ;apply P_id_sieve_monotonic;assumption.
     intros f.
     case f.
     vm_compute in |-*;intros ;apply P_id_a__filter_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_a__nats_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_s_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_0_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_a__zprimes_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_a__sieve_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_cons_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_nats_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_mark_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_filter_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_zprimes_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_sieve_bounded;assumption.
     intros .
     do 2 (rewrite  <- same_measure in |-*).
     apply rules_monotonic;assumption.
     assumption.
   Qed.
   
   Hypothesis P_id_A__ZPRIMES : A.
   
   Hypothesis P_id_A__FILTER : A ->A ->A ->A.
   
   Hypothesis P_id_A__SIEVE : A ->A.
   
   Hypothesis P_id_MARK : A ->A.
   
   Hypothesis P_id_A__NATS : A ->A.
   
   Hypothesis P_id_A__FILTER_monotonic :
    forall x12 x10 x14 x9 x13 x11, 
     (A0 <= x14)/\ (x14 <= x13) ->
      (A0 <= x12)/\ (x12 <= x11) ->
       (A0 <= x10)/\ (x10 <= x9) ->
        P_id_A__FILTER x10 x12 x14 <= P_id_A__FILTER x9 x11 x13.
   
   Hypothesis P_id_A__SIEVE_monotonic :
    forall x10 x9, 
     (A0 <= x10)/\ (x10 <= x9) ->P_id_A__SIEVE x10 <= P_id_A__SIEVE x9.
   
   Hypothesis P_id_MARK_monotonic :
    forall x10 x9, (A0 <= x10)/\ (x10 <= x9) ->P_id_MARK x10 <= P_id_MARK x9.
   
   Hypothesis P_id_A__NATS_monotonic :
    forall x10 x9, 
     (A0 <= x10)/\ (x10 <= x9) ->P_id_A__NATS x10 <= P_id_A__NATS x9.
   
   Definition marked_measure t := 
     match t with
       | (algebra.Alg.Term algebra.F.id_a__zprimes nil) => P_id_A__ZPRIMES 
       | (algebra.Alg.Term algebra.F.id_a__filter (x11::x10::x9::nil)) =>
        P_id_A__FILTER (measure x11) (measure x10) (measure x9)
       | (algebra.Alg.Term algebra.F.id_a__sieve (x9::nil)) =>
        P_id_A__SIEVE (measure x9)
       | (algebra.Alg.Term algebra.F.id_mark (x9::nil)) =>
        P_id_MARK (measure x9)
       | (algebra.Alg.Term algebra.F.id_a__nats (x9::nil)) =>
        P_id_A__NATS (measure x9)
       | _ => measure t
       end.
   
   Definition  Marked_pols :
    forall f, 
     (algebra.EQT.defined R_xml_0_deep_rew.R_xml_0_rules f) ->
      InterpGen.Pol_type A (InterpGen.get_arity f).
   Proof.
     intros f H.
     
     apply ddp.defined_list_complete with (1:=R_xml_0_deep_rew.R_xml_0_rules_included) in H .
     apply (Symb_more_list.change_in algebra.F.symb_order) in H .
     
     set (u := (Symb_more_list.qs algebra.F.symb_order
           (Symb_more_list.XSet.remove_red
              (ddp.defined_list R_xml_0_deep_rew.R_xml_0_rule_as_list)))) in * .
     vm_compute in u .
     unfold u in * .
     clear u .
     unfold more_list.mem_bool in H .
     
     match type of H with 
       | orb ?a ?b = true => 
         assert (H':{a = true}+{b = true});[
           revert H;case a;[left;reflexivity|simpl;intros h;right;exact h]|
             clear H;destruct H' as [H|H]]
     end .
     
     match type of H with 
       | _ _ ?t = true =>
         generalize (algebra.F.symb_eq_bool_ok f t);
           unfold algebra.Alg.eq_symb_bool in H;
           rewrite H;clear H;intros ;subst
     end .
     vm_compute in |-*;intros x9;apply (P_id_MARK x9).
     
     match type of H with 
       | orb ?a ?b = true => 
         assert (H':{a = true}+{b = true});[
           revert H;case a;[left;reflexivity|simpl;intros h;right;exact h]|
             clear H;destruct H' as [H|H]]
     end .
     
     match type of H with 
       | _ _ ?t = true =>
         generalize (algebra.F.symb_eq_bool_ok f t);
           unfold algebra.Alg.eq_symb_bool in H;
           rewrite H;clear H;intros ;subst
     end .
     vm_compute in |-*;intros x9;apply (P_id_A__SIEVE x9).
     
     match type of H with 
       | orb ?a ?b = true => 
         assert (H':{a = true}+{b = true});[
           revert H;case a;[left;reflexivity|simpl;intros h;right;exact h]|
             clear H;destruct H' as [H|H]]
     end .
     
     match type of H with 
       | _ _ ?t = true =>
         generalize (algebra.F.symb_eq_bool_ok f t);
           unfold algebra.Alg.eq_symb_bool in H;
           rewrite H;clear H;intros ;subst
     end .
     vm_compute in |-*;intros ;apply (P_id_A__ZPRIMES ).
     
     match type of H with 
       | orb ?a ?b = true => 
         assert (H':{a = true}+{b = true});[
           revert H;case a;[left;reflexivity|simpl;intros h;right;exact h]|
             clear H;destruct H' as [H|H]]
     end .
     
     match type of H with 
       | _ _ ?t = true =>
         generalize (algebra.F.symb_eq_bool_ok f t);
           unfold algebra.Alg.eq_symb_bool in H;
           rewrite H;clear H;intros ;subst
     end .
     vm_compute in |-*;intros x9;apply (P_id_A__NATS x9).
     
     match type of H with 
       | orb ?a ?b = true => 
         assert (H':{a = true}+{b = true});[
           revert H;case a;[left;reflexivity|simpl;intros h;right;exact h]|
             clear H;destruct H' as [H|H]]
     end .
     
     match type of H with 
       | _ _ ?t = true =>
         generalize (algebra.F.symb_eq_bool_ok f t);
           unfold algebra.Alg.eq_symb_bool in H;
           rewrite H;clear H;intros ;subst
     end .
     vm_compute in |-*;intros x11 x10 x9;apply (P_id_A__FILTER x11 x10 x9).
     discriminate H.
   Defined.
   
   Lemma same_marked_measure :
    forall t, 
     marked_measure t = InterpGen.marked_measure A0 Pols Marked_pols 
                         (ddp.defined_dec _ _ 
                           R_xml_0_deep_rew.R_xml_0_rules_included) t.
   Proof.
     intros [a| f l].
     simpl in |-*.
     unfold eq_rect_r, eq_rect, sym_eq in |-*.
     reflexivity .
     
     refine match f with
              | algebra.F.id_a__filter =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::nil => _
                 | _::_::_::nil => _
                 | _::_::_::_::_ => _
                 end
              | algebra.F.id_a__nats =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::_ => _
                 end
              | algebra.F.id_s =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::_ => _
                 end
              | algebra.F.id_0 => match l with
                                    | nil => _
                                    | _::_ => _
                                    end
              | algebra.F.id_a__zprimes =>
               match l with
                 | nil => _
                 | _::_ => _
                 end
              | algebra.F.id_a__sieve =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::_ => _
                 end
              | algebra.F.id_cons =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::nil => _
                 | _::_::_::_ => _
                 end
              | algebra.F.id_nats =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::_ => _
                 end
              | algebra.F.id_mark =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::_ => _
                 end
              | algebra.F.id_filter =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::nil => _
                 | _::_::_::nil => _
                 | _::_::_::_::_ => _
                 end
              | algebra.F.id_zprimes => match l with
                                          | nil => _
                                          | _::_ => _
                                          end
              | algebra.F.id_sieve =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::_ => _
                 end
              end.
     vm_compute in |-*;reflexivity .
     vm_compute in |-*;reflexivity .
     vm_compute in |-*;reflexivity .
     
     lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
      apply same_measure.
     vm_compute in |-*;reflexivity .
     vm_compute in |-*;reflexivity .
     
     lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
      apply same_measure.
     vm_compute in |-*;reflexivity .
     vm_compute in |-*;reflexivity .
     
     lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
      apply same_measure.
     vm_compute in |-*;reflexivity .
     vm_compute in |-*;reflexivity .
     vm_compute in |-*;reflexivity .
     vm_compute in |-*;reflexivity .
     vm_compute in |-*;reflexivity .
     vm_compute in |-*;reflexivity .
     
     lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
      apply same_measure.
     vm_compute in |-*;reflexivity .
     vm_compute in |-*;reflexivity .
     vm_compute in |-*;reflexivity .
     
     lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
      apply same_measure.
     vm_compute in |-*;reflexivity .
     vm_compute in |-*;reflexivity .
     
     lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
      apply same_measure.
     vm_compute in |-*;reflexivity .
     vm_compute in |-*;reflexivity .
     
     lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
      apply same_measure.
     vm_compute in |-*;reflexivity .
     vm_compute in |-*;reflexivity .
     vm_compute in |-*;reflexivity .
     vm_compute in |-*;reflexivity .
     
     lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
      apply same_measure.
     vm_compute in |-*;reflexivity .
     vm_compute in |-*;reflexivity .
     vm_compute in |-*;reflexivity .
     vm_compute in |-*;reflexivity .
     
     lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
      apply same_measure.
     vm_compute in |-*;reflexivity .
   Qed.
   
   Lemma marked_measure_equation :
    forall t, 
     marked_measure t = match t with
                          | (algebra.Alg.Term algebra.F.id_a__zprimes nil) =>
                           P_id_A__ZPRIMES 
                          | (algebra.Alg.Term algebra.F.id_a__filter (x11::
                             x10::x9::nil)) =>
                           P_id_A__FILTER (measure x11) (measure x10) 
                            (measure x9)
                          | (algebra.Alg.Term algebra.F.id_a__sieve 
                             (x9::nil)) =>
                           P_id_A__SIEVE (measure x9)
                          | (algebra.Alg.Term algebra.F.id_mark (x9::nil)) =>
                           P_id_MARK (measure x9)
                          | (algebra.Alg.Term algebra.F.id_a__nats (x9::nil)) =>
                           P_id_A__NATS (measure x9)
                          | _ => measure t
                          end.
   Proof.
     reflexivity .
   Qed.
   
   Lemma marked_measure_star_monotonic :
    forall f l1 l2, 
     (closure.refl_trans_clos (closure.one_step_list (algebra.EQT.one_step 
                                                       R_xml_0_deep_rew.R_xml_0_rules)
                                                      ) l1 l2) ->
      marked_measure (algebra.Alg.Term f l1) <= marked_measure (algebra.Alg.Term 
                                                                 f l2).
   Proof.
     intros .
     do 2 (rewrite same_marked_measure in |-*).
     
     apply InterpGen.marked_measure_star_monotonic with (1:=Aop) (Pols:=
     Pols) (rules:=R_xml_0_deep_rew.R_xml_0_rules).
     clear f.
     intros f.
     case f.
     vm_compute in |-*;intros ;apply P_id_a__filter_monotonic;assumption.
     vm_compute in |-*;intros ;apply P_id_a__nats_monotonic;assumption.
     vm_compute in |-*;intros ;apply P_id_s_monotonic;assumption.
     vm_compute in |-*;apply (Aop.(le_refl)).
     vm_compute in |-*;apply (Aop.(le_refl)).
     vm_compute in |-*;intros ;apply P_id_a__sieve_monotonic;assumption.
     vm_compute in |-*;intros ;apply P_id_cons_monotonic;assumption.
     vm_compute in |-*;intros ;apply P_id_nats_monotonic;assumption.
     vm_compute in |-*;intros ;apply P_id_mark_monotonic;assumption.
     vm_compute in |-*;intros ;apply P_id_filter_monotonic;assumption.
     vm_compute in |-*;apply (Aop.(le_refl)).
     vm_compute in |-*;intros ;apply P_id_sieve_monotonic;assumption.
     clear f.
     intros f.
     case f.
     vm_compute in |-*;intros ;apply P_id_a__filter_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_a__nats_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_s_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_0_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_a__zprimes_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_a__sieve_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_cons_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_nats_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_mark_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_filter_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_zprimes_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_sieve_bounded;assumption.
     intros .
     do 2 (rewrite  <- same_measure in |-*).
     apply rules_monotonic;assumption.
     clear f.
     intros f.
     clear H.
     intros H.
     generalize H.
     
     apply ddp.defined_list_complete with (1:=R_xml_0_deep_rew.R_xml_0_rules_included) in H .
     apply (Symb_more_list.change_in algebra.F.symb_order) in H .
     
     set (u := (Symb_more_list.qs algebra.F.symb_order
           (Symb_more_list.XSet.remove_red
              (ddp.defined_list R_xml_0_deep_rew.R_xml_0_rule_as_list)))) in * .
     vm_compute in u .
     unfold u in * .
     clear u .
     unfold more_list.mem_bool in H .
     
     match type of H with 
       | orb ?a ?b = true => 
         assert (H':{a = true}+{b = true});[
           revert H;case a;[left;reflexivity|simpl;intros h;right;exact h]|
             clear H;destruct H' as [H|H]]
     end .
     
     match type of H with 
       | _ _ ?t = true =>
         generalize (algebra.F.symb_eq_bool_ok f t);
           unfold algebra.Alg.eq_symb_bool in H;
           rewrite H;clear H;intros ;subst
     end .
     vm_compute in |-*;intros ;apply P_id_MARK_monotonic;assumption.
     
     match type of H with 
       | orb ?a ?b = true => 
         assert (H':{a = true}+{b = true});[
           revert H;case a;[left;reflexivity|simpl;intros h;right;exact h]|
             clear H;destruct H' as [H|H]]
     end .
     
     match type of H with 
       | _ _ ?t = true =>
         generalize (algebra.F.symb_eq_bool_ok f t);
           unfold algebra.Alg.eq_symb_bool in H;
           rewrite H;clear H;intros ;subst
     end .
     vm_compute in |-*;intros ;apply P_id_A__SIEVE_monotonic;assumption.
     
     match type of H with 
       | orb ?a ?b = true => 
         assert (H':{a = true}+{b = true});[
           revert H;case a;[left;reflexivity|simpl;intros h;right;exact h]|
             clear H;destruct H' as [H|H]]
     end .
     
     match type of H with 
       | _ _ ?t = true =>
         generalize (algebra.F.symb_eq_bool_ok f t);
           unfold algebra.Alg.eq_symb_bool in H;
           rewrite H;clear H;intros ;subst
     end .
     vm_compute in |-*;intros ;apply (Aop.(le_refl)).
     
     match type of H with 
       | orb ?a ?b = true => 
         assert (H':{a = true}+{b = true});[
           revert H;case a;[left;reflexivity|simpl;intros h;right;exact h]|
             clear H;destruct H' as [H|H]]
     end .
     
     match type of H with 
       | _ _ ?t = true =>
         generalize (algebra.F.symb_eq_bool_ok f t);
           unfold algebra.Alg.eq_symb_bool in H;
           rewrite H;clear H;intros ;subst
     end .
     vm_compute in |-*;intros ;apply P_id_A__NATS_monotonic;assumption.
     
     match type of H with 
       | orb ?a ?b = true => 
         assert (H':{a = true}+{b = true});[
           revert H;case a;[left;reflexivity|simpl;intros h;right;exact h]|
             clear H;destruct H' as [H|H]]
     end .
     
     match type of H with 
       | _ _ ?t = true =>
         generalize (algebra.F.symb_eq_bool_ok f t);
           unfold algebra.Alg.eq_symb_bool in H;
           rewrite H;clear H;intros ;subst
     end .
     vm_compute in |-*;intros ;apply P_id_A__FILTER_monotonic;assumption.
     discriminate H.
     assumption.
   Qed.
   
   End S.
End Interp.

Module InterpZ.
 Section S.
   Open Scope Z_scope.
   
   Hypothesis min_value : Z.
   
   Import ring_extention.
   
   Notation Local "'Alt'" := (Zwf.Zwf min_value).
   
   Notation Local "'Ale'" := Zle.
   
   Notation Local "'Aeq'" := (@eq Z).
   
   Notation Local "a <= b" := (Ale a b).
   
   Notation Local "a < b" := (Alt a b).
   
   Hypothesis P_id_a__filter : Z ->Z ->Z ->Z.
   
   Hypothesis P_id_a__nats : Z ->Z.
   
   Hypothesis P_id_s : Z ->Z.
   
   Hypothesis P_id_0 : Z.
   
   Hypothesis P_id_a__zprimes : Z.
   
   Hypothesis P_id_a__sieve : Z ->Z.
   
   Hypothesis P_id_cons : Z ->Z ->Z.
   
   Hypothesis P_id_nats : Z ->Z.
   
   Hypothesis P_id_mark : Z ->Z.
   
   Hypothesis P_id_filter : Z ->Z ->Z ->Z.
   
   Hypothesis P_id_zprimes : Z.
   
   Hypothesis P_id_sieve : Z ->Z.
   
   Hypothesis P_id_a__filter_monotonic :
    forall x12 x10 x14 x9 x13 x11, 
     (min_value <= x14)/\ (x14 <= x13) ->
      (min_value <= x12)/\ (x12 <= x11) ->
       (min_value <= x10)/\ (x10 <= x9) ->
        P_id_a__filter x10 x12 x14 <= P_id_a__filter x9 x11 x13.
   
   Hypothesis P_id_a__nats_monotonic :
    forall x10 x9, 
     (min_value <= x10)/\ (x10 <= x9) ->P_id_a__nats x10 <= P_id_a__nats x9.
   
   Hypothesis P_id_s_monotonic :
    forall x10 x9, (min_value <= x10)/\ (x10 <= x9) ->P_id_s x10 <= P_id_s x9.
   
   Hypothesis P_id_a__sieve_monotonic :
    forall x10 x9, 
     (min_value <= x10)/\ (x10 <= x9) ->P_id_a__sieve x10 <= P_id_a__sieve x9.
   
   Hypothesis P_id_cons_monotonic :
    forall x12 x10 x9 x11, 
     (min_value <= x12)/\ (x12 <= x11) ->
      (min_value <= x10)/\ (x10 <= x9) ->
       P_id_cons x10 x12 <= P_id_cons x9 x11.
   
   Hypothesis P_id_nats_monotonic :
    forall x10 x9, 
     (min_value <= x10)/\ (x10 <= x9) ->P_id_nats x10 <= P_id_nats x9.
   
   Hypothesis P_id_mark_monotonic :
    forall x10 x9, 
     (min_value <= x10)/\ (x10 <= x9) ->P_id_mark x10 <= P_id_mark x9.
   
   Hypothesis P_id_filter_monotonic :
    forall x12 x10 x14 x9 x13 x11, 
     (min_value <= x14)/\ (x14 <= x13) ->
      (min_value <= x12)/\ (x12 <= x11) ->
       (min_value <= x10)/\ (x10 <= x9) ->
        P_id_filter x10 x12 x14 <= P_id_filter x9 x11 x13.
   
   Hypothesis P_id_sieve_monotonic :
    forall x10 x9, 
     (min_value <= x10)/\ (x10 <= x9) ->P_id_sieve x10 <= P_id_sieve x9.
   
   Hypothesis P_id_a__filter_bounded :
    forall x10 x9 x11, 
     (min_value <= x9) ->
      (min_value <= x10) ->
       (min_value <= x11) ->min_value <= P_id_a__filter x11 x10 x9.
   
   Hypothesis P_id_a__nats_bounded :
    forall x9, (min_value <= x9) ->min_value <= P_id_a__nats x9.
   
   Hypothesis P_id_s_bounded :
    forall x9, (min_value <= x9) ->min_value <= P_id_s x9.
   
   Hypothesis P_id_0_bounded : min_value <= P_id_0 .
   
   Hypothesis P_id_a__zprimes_bounded : min_value <= P_id_a__zprimes .
   
   Hypothesis P_id_a__sieve_bounded :
    forall x9, (min_value <= x9) ->min_value <= P_id_a__sieve x9.
   
   Hypothesis P_id_cons_bounded :
    forall x10 x9, 
     (min_value <= x9) ->(min_value <= x10) ->min_value <= P_id_cons x10 x9.
   
   Hypothesis P_id_nats_bounded :
    forall x9, (min_value <= x9) ->min_value <= P_id_nats x9.
   
   Hypothesis P_id_mark_bounded :
    forall x9, (min_value <= x9) ->min_value <= P_id_mark x9.
   
   Hypothesis P_id_filter_bounded :
    forall x10 x9 x11, 
     (min_value <= x9) ->
      (min_value <= x10) ->
       (min_value <= x11) ->min_value <= P_id_filter x11 x10 x9.
   
   Hypothesis P_id_zprimes_bounded : min_value <= P_id_zprimes .
   
   Hypothesis P_id_sieve_bounded :
    forall x9, (min_value <= x9) ->min_value <= P_id_sieve x9.
   
   Definition measure  := 
     Interp.measure min_value P_id_a__filter P_id_a__nats P_id_s P_id_0 
      P_id_a__zprimes P_id_a__sieve P_id_cons P_id_nats P_id_mark 
      P_id_filter P_id_zprimes P_id_sieve.
   
   Lemma measure_equation :
    forall t, 
     measure t = match t with
                   | (algebra.Alg.Term algebra.F.id_a__filter (x11::x10::
                      x9::nil)) =>
                    P_id_a__filter (measure x11) (measure x10) (measure x9)
                   | (algebra.Alg.Term algebra.F.id_a__nats (x9::nil)) =>
                    P_id_a__nats (measure x9)
                   | (algebra.Alg.Term algebra.F.id_s (x9::nil)) =>
                    P_id_s (measure x9)
                   | (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0 
                   | (algebra.Alg.Term algebra.F.id_a__zprimes nil) =>
                    P_id_a__zprimes 
                   | (algebra.Alg.Term algebra.F.id_a__sieve (x9::nil)) =>
                    P_id_a__sieve (measure x9)
                   | (algebra.Alg.Term algebra.F.id_cons (x10::x9::nil)) =>
                    P_id_cons (measure x10) (measure x9)
                   | (algebra.Alg.Term algebra.F.id_nats (x9::nil)) =>
                    P_id_nats (measure x9)
                   | (algebra.Alg.Term algebra.F.id_mark (x9::nil)) =>
                    P_id_mark (measure x9)
                   | (algebra.Alg.Term algebra.F.id_filter (x11::x10::
                      x9::nil)) =>
                    P_id_filter (measure x11) (measure x10) (measure x9)
                   | (algebra.Alg.Term algebra.F.id_zprimes nil) =>
                    P_id_zprimes 
                   | (algebra.Alg.Term algebra.F.id_sieve (x9::nil)) =>
                    P_id_sieve (measure x9)
                   | _ => min_value
                   end.
   Proof.
     intros t;case t;intros ;apply refl_equal.
   Qed.
   
   Lemma measure_bounded : forall t, min_value <= measure t.
   Proof.
     unfold measure in |-*.
     
     apply Interp.measure_bounded with Alt Aeq;
      (apply interp.o_Z)||
      (cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;auto with zarith).
   Qed.
   
   Ltac generate_pos_hyp  :=
    match goal with
      | H:context [measure ?x] |- _ =>
       let v := fresh "v" in 
        (let H := fresh "h" in 
          (set (H:=measure_bounded x) in *;set (v:=measure x) in *;
            clearbody H;clearbody v))
      |  |- context [measure ?x] =>
       let v := fresh "v" in 
        (let H := fresh "h" in 
          (set (H:=measure_bounded x) in *;set (v:=measure x) in *;
            clearbody H;clearbody v))
      end
    .
   
   Hypothesis rules_monotonic :
    forall l r, 
     (algebra.EQT.axiom R_xml_0_deep_rew.R_xml_0_rules r l) ->
      measure r <= measure l.
   
   Lemma measure_star_monotonic :
    forall l r, 
     (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                r l) ->measure r <= measure l.
   Proof.
     unfold measure in *.
     apply Interp.measure_star_monotonic with Alt Aeq.
     
     (apply interp.o_Z)||
     (cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;auto with zarith).
     intros ;apply P_id_a__filter_monotonic;assumption.
     intros ;apply P_id_a__nats_monotonic;assumption.
     intros ;apply P_id_s_monotonic;assumption.
     intros ;apply P_id_a__sieve_monotonic;assumption.
     intros ;apply P_id_cons_monotonic;assumption.
     intros ;apply P_id_nats_monotonic;assumption.
     intros ;apply P_id_mark_monotonic;assumption.
     intros ;apply P_id_filter_monotonic;assumption.
     intros ;apply P_id_sieve_monotonic;assumption.
     intros ;apply P_id_a__filter_bounded;assumption.
     intros ;apply P_id_a__nats_bounded;assumption.
     intros ;apply P_id_s_bounded;assumption.
     intros ;apply P_id_0_bounded;assumption.
     intros ;apply P_id_a__zprimes_bounded;assumption.
     intros ;apply P_id_a__sieve_bounded;assumption.
     intros ;apply P_id_cons_bounded;assumption.
     intros ;apply P_id_nats_bounded;assumption.
     intros ;apply P_id_mark_bounded;assumption.
     intros ;apply P_id_filter_bounded;assumption.
     intros ;apply P_id_zprimes_bounded;assumption.
     intros ;apply P_id_sieve_bounded;assumption.
     apply rules_monotonic.
   Qed.
   
   Hypothesis P_id_A__ZPRIMES : Z.
   
   Hypothesis P_id_A__FILTER : Z ->Z ->Z ->Z.
   
   Hypothesis P_id_A__SIEVE : Z ->Z.
   
   Hypothesis P_id_MARK : Z ->Z.
   
   Hypothesis P_id_A__NATS : Z ->Z.
   
   Hypothesis P_id_A__FILTER_monotonic :
    forall x12 x10 x14 x9 x13 x11, 
     (min_value <= x14)/\ (x14 <= x13) ->
      (min_value <= x12)/\ (x12 <= x11) ->
       (min_value <= x10)/\ (x10 <= x9) ->
        P_id_A__FILTER x10 x12 x14 <= P_id_A__FILTER x9 x11 x13.
   
   Hypothesis P_id_A__SIEVE_monotonic :
    forall x10 x9, 
     (min_value <= x10)/\ (x10 <= x9) ->P_id_A__SIEVE x10 <= P_id_A__SIEVE x9.
   
   Hypothesis P_id_MARK_monotonic :
    forall x10 x9, 
     (min_value <= x10)/\ (x10 <= x9) ->P_id_MARK x10 <= P_id_MARK x9.
   
   Hypothesis P_id_A__NATS_monotonic :
    forall x10 x9, 
     (min_value <= x10)/\ (x10 <= x9) ->P_id_A__NATS x10 <= P_id_A__NATS x9.
   
   Definition marked_measure  := 
     Interp.marked_measure min_value P_id_a__filter P_id_a__nats P_id_s 
      P_id_0 P_id_a__zprimes P_id_a__sieve P_id_cons P_id_nats P_id_mark 
      P_id_filter P_id_zprimes P_id_sieve P_id_A__ZPRIMES P_id_A__FILTER 
      P_id_A__SIEVE P_id_MARK P_id_A__NATS.
   
   Lemma marked_measure_equation :
    forall t, 
     marked_measure t = match t with
                          | (algebra.Alg.Term algebra.F.id_a__zprimes nil) =>
                           P_id_A__ZPRIMES 
                          | (algebra.Alg.Term algebra.F.id_a__filter (x11::
                             x10::x9::nil)) =>
                           P_id_A__FILTER (measure x11) (measure x10) 
                            (measure x9)
                          | (algebra.Alg.Term algebra.F.id_a__sieve 
                             (x9::nil)) =>
                           P_id_A__SIEVE (measure x9)
                          | (algebra.Alg.Term algebra.F.id_mark (x9::nil)) =>
                           P_id_MARK (measure x9)
                          | (algebra.Alg.Term algebra.F.id_a__nats (x9::nil)) =>
                           P_id_A__NATS (measure x9)
                          | _ => measure t
                          end.
   Proof.
     reflexivity .
   Qed.
   
   Lemma marked_measure_star_monotonic :
    forall f l1 l2, 
     (closure.refl_trans_clos (closure.one_step_list (algebra.EQT.one_step 
                                                       R_xml_0_deep_rew.R_xml_0_rules)
                                                      ) l1 l2) ->
      marked_measure (algebra.Alg.Term f l1) <= marked_measure (algebra.Alg.Term 
                                                                 f l2).
   Proof.
     unfold marked_measure in *.
     apply Interp.marked_measure_star_monotonic with Alt Aeq.
     
     (apply interp.o_Z)||
     (cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;auto with zarith).
     intros ;apply P_id_a__filter_monotonic;assumption.
     intros ;apply P_id_a__nats_monotonic;assumption.
     intros ;apply P_id_s_monotonic;assumption.
     intros ;apply P_id_a__sieve_monotonic;assumption.
     intros ;apply P_id_cons_monotonic;assumption.
     intros ;apply P_id_nats_monotonic;assumption.
     intros ;apply P_id_mark_monotonic;assumption.
     intros ;apply P_id_filter_monotonic;assumption.
     intros ;apply P_id_sieve_monotonic;assumption.
     intros ;apply P_id_a__filter_bounded;assumption.
     intros ;apply P_id_a__nats_bounded;assumption.
     intros ;apply P_id_s_bounded;assumption.
     intros ;apply P_id_0_bounded;assumption.
     intros ;apply P_id_a__zprimes_bounded;assumption.
     intros ;apply P_id_a__sieve_bounded;assumption.
     intros ;apply P_id_cons_bounded;assumption.
     intros ;apply P_id_nats_bounded;assumption.
     intros ;apply P_id_mark_bounded;assumption.
     intros ;apply P_id_filter_bounded;assumption.
     intros ;apply P_id_zprimes_bounded;assumption.
     intros ;apply P_id_sieve_bounded;assumption.
     apply rules_monotonic.
     intros ;apply P_id_A__FILTER_monotonic;assumption.
     intros ;apply P_id_A__SIEVE_monotonic;assumption.
     intros ;apply P_id_MARK_monotonic;assumption.
     intros ;apply P_id_A__NATS_monotonic;assumption.
   Qed.
   
   End S.
End InterpZ.

Module WF_R_xml_0_deep_rew.
 Inductive DP_R_xml_0  :
  algebra.Alg.term ->algebra.Alg.term ->Prop := 
    (* <a__filter(cons(X_,Y_),s(N_),M_),mark(X_)> *)
   | DP_R_xml_0_0 :
    forall x4 x2 x10 x1 x9 x3 x11, 
     (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                
       (algebra.Alg.Term algebra.F.id_cons (x1::x2::nil)) x11) ->
      (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                 (algebra.Alg.Term algebra.F.id_s (x4::nil)) 
        x10) ->
       (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                  x3 x9) ->
        DP_R_xml_0 (algebra.Alg.Term algebra.F.id_mark (x1::nil)) 
         (algebra.Alg.Term algebra.F.id_a__filter (x11::x10::x9::nil))
    (* <a__sieve(cons(s(N_),Y_)),mark(N_)> *)
   | DP_R_xml_0_1 :
    forall x4 x2 x9, 
     (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                
       (algebra.Alg.Term algebra.F.id_cons ((algebra.Alg.Term algebra.F.id_s 
        (x4::nil))::x2::nil)) x9) ->
      DP_R_xml_0 (algebra.Alg.Term algebra.F.id_mark (x4::nil)) 
       (algebra.Alg.Term algebra.F.id_a__sieve (x9::nil))
    (* <a__nats(N_),mark(N_)> *)
   | DP_R_xml_0_2 :
    forall x4 x9, 
     (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                x4 x9) ->
      DP_R_xml_0 (algebra.Alg.Term algebra.F.id_mark (x4::nil)) 
       (algebra.Alg.Term algebra.F.id_a__nats (x9::nil))
    (* <a__zprimes,a__sieve(a__nats(s(s(0))))> *)
   | DP_R_xml_0_3 :
    DP_R_xml_0 (algebra.Alg.Term algebra.F.id_a__sieve ((algebra.Alg.Term 
                algebra.F.id_a__nats ((algebra.Alg.Term algebra.F.id_s 
                ((algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Term 
                algebra.F.id_0 nil)::nil))::nil))::nil))::nil)) 
     (algebra.Alg.Term algebra.F.id_a__zprimes nil)
    (* <a__zprimes,a__nats(s(s(0)))> *)
   | DP_R_xml_0_4 :
    DP_R_xml_0 (algebra.Alg.Term algebra.F.id_a__nats ((algebra.Alg.Term 
                algebra.F.id_s ((algebra.Alg.Term algebra.F.id_s 
                ((algebra.Alg.Term algebra.F.id_0 nil)::nil))::nil))::nil)) 
     (algebra.Alg.Term algebra.F.id_a__zprimes nil)
   
    (* <mark(filter(X1_,X2_,X3_)),a__filter(mark(X1_),mark(X2_),mark(X3_))> *)
   | DP_R_xml_0_5 :
    forall x6 x9 x5 x7, 
     (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                
       (algebra.Alg.Term algebra.F.id_filter (x5::x6::x7::nil)) x9) ->
      DP_R_xml_0 (algebra.Alg.Term algebra.F.id_a__filter ((algebra.Alg.Term 
                  algebra.F.id_mark (x5::nil))::(algebra.Alg.Term 
                  algebra.F.id_mark (x6::nil))::(algebra.Alg.Term 
                  algebra.F.id_mark (x7::nil))::nil)) 
       (algebra.Alg.Term algebra.F.id_mark (x9::nil))
    (* <mark(filter(X1_,X2_,X3_)),mark(X1_)> *)
   | DP_R_xml_0_6 :
    forall x6 x9 x5 x7, 
     (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                
       (algebra.Alg.Term algebra.F.id_filter (x5::x6::x7::nil)) x9) ->
      DP_R_xml_0 (algebra.Alg.Term algebra.F.id_mark (x5::nil)) 
       (algebra.Alg.Term algebra.F.id_mark (x9::nil))
    (* <mark(filter(X1_,X2_,X3_)),mark(X2_)> *)
   | DP_R_xml_0_7 :
    forall x6 x9 x5 x7, 
     (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                
       (algebra.Alg.Term algebra.F.id_filter (x5::x6::x7::nil)) x9) ->
      DP_R_xml_0 (algebra.Alg.Term algebra.F.id_mark (x6::nil)) 
       (algebra.Alg.Term algebra.F.id_mark (x9::nil))
    (* <mark(filter(X1_,X2_,X3_)),mark(X3_)> *)
   | DP_R_xml_0_8 :
    forall x6 x9 x5 x7, 
     (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                
       (algebra.Alg.Term algebra.F.id_filter (x5::x6::x7::nil)) x9) ->
      DP_R_xml_0 (algebra.Alg.Term algebra.F.id_mark (x7::nil)) 
       (algebra.Alg.Term algebra.F.id_mark (x9::nil))
    (* <mark(sieve(X_)),a__sieve(mark(X_))> *)
   | DP_R_xml_0_9 :
    forall x1 x9, 
     (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                
       (algebra.Alg.Term algebra.F.id_sieve (x1::nil)) x9) ->
      DP_R_xml_0 (algebra.Alg.Term algebra.F.id_a__sieve ((algebra.Alg.Term 
                  algebra.F.id_mark (x1::nil))::nil)) 
       (algebra.Alg.Term algebra.F.id_mark (x9::nil))
    (* <mark(sieve(X_)),mark(X_)> *)
   | DP_R_xml_0_10 :
    forall x1 x9, 
     (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                
       (algebra.Alg.Term algebra.F.id_sieve (x1::nil)) x9) ->
      DP_R_xml_0 (algebra.Alg.Term algebra.F.id_mark (x1::nil)) 
       (algebra.Alg.Term algebra.F.id_mark (x9::nil))
    (* <mark(nats(X_)),a__nats(mark(X_))> *)
   | DP_R_xml_0_11 :
    forall x1 x9, 
     (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                
       (algebra.Alg.Term algebra.F.id_nats (x1::nil)) x9) ->
      DP_R_xml_0 (algebra.Alg.Term algebra.F.id_a__nats ((algebra.Alg.Term 
                  algebra.F.id_mark (x1::nil))::nil)) 
       (algebra.Alg.Term algebra.F.id_mark (x9::nil))
    (* <mark(nats(X_)),mark(X_)> *)
   | DP_R_xml_0_12 :
    forall x1 x9, 
     (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                
       (algebra.Alg.Term algebra.F.id_nats (x1::nil)) x9) ->
      DP_R_xml_0 (algebra.Alg.Term algebra.F.id_mark (x1::nil)) 
       (algebra.Alg.Term algebra.F.id_mark (x9::nil))
    (* <mark(zprimes),a__zprimes> *)
   | DP_R_xml_0_13 :
    forall x9, 
     (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                (algebra.Alg.Term algebra.F.id_zprimes nil) 
       x9) ->
      DP_R_xml_0 (algebra.Alg.Term algebra.F.id_a__zprimes nil) 
       (algebra.Alg.Term algebra.F.id_mark (x9::nil))
    (* <mark(cons(X1_,X2_)),mark(X1_)> *)
   | DP_R_xml_0_14 :
    forall x6 x9 x5, 
     (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                
       (algebra.Alg.Term algebra.F.id_cons (x5::x6::nil)) x9) ->
      DP_R_xml_0 (algebra.Alg.Term algebra.F.id_mark (x5::nil)) 
       (algebra.Alg.Term algebra.F.id_mark (x9::nil))
    (* <mark(s(X_)),mark(X_)> *)
   | DP_R_xml_0_15 :
    forall x1 x9, 
     (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                (algebra.Alg.Term algebra.F.id_s (x1::nil)) 
       x9) ->
      DP_R_xml_0 (algebra.Alg.Term algebra.F.id_mark (x1::nil)) 
       (algebra.Alg.Term algebra.F.id_mark (x9::nil))
 .
 
 Module ddp := dp.MakeDP(algebra.EQT).
 
 
 Lemma R_xml_0_dp_step_spec :
  forall x y, 
   (ddp.dp_step R_xml_0_deep_rew.R_xml_0_rules x y) ->
    exists f,
      exists l1,
        exists l2,
          y = algebra.Alg.Term f l2/\ 
          (closure.refl_trans_clos (closure.one_step_list (algebra.EQT.one_step 
                                                            R_xml_0_deep_rew.R_xml_0_rules)
                                                           ) l1 l2)/\ 
          (ddp.dp R_xml_0_deep_rew.R_xml_0_rules x (algebra.Alg.Term f l1)).
 Proof.
   intros x y H.
   induction H.
   inversion H.
   subst.
   destruct t0.
   refine ((False_ind) _ _).
   refine (R_xml_0_deep_rew.R_xml_0_non_var H0).
   simpl in H|-*.
   exists a.
   exists ((List.map) (algebra.Alg.apply_subst sigma) l).
   exists ((List.map) (algebra.Alg.apply_subst sigma) l).
   repeat (constructor).
   assumption.
   exists f.
   exists l2.
   exists l1.
   constructor.
   constructor.
   constructor.
   constructor.
   rewrite  <- closure.rwr_list_trans_clos_one_step_list.
   assumption.
   assumption.
 Qed.
 
 
 Ltac included_dp_tac H :=
  injection H;clear H;intros;subst;
  repeat (match goal with 
  | H: closure.refl_trans_clos (closure.one_step_list _) (_::_) _ |- _=>           
  let x := fresh "x" in 
  let l := fresh "l" in 
  let h1 := fresh "h" in 
  let h2 := fresh "h" in 
  let h3 := fresh "h" in 
  destruct (@algebra.EQT_ext.one_step_list_star_decompose_cons _ _ _ _  H) as [x [l[h1[h2 h3]]]];clear H;subst
  | H: closure.refl_trans_clos (closure.one_step_list _) nil _ |- _ => 
  rewrite (@algebra.EQT_ext.one_step_list_star_decompose_nil _ _ H) in *;clear H
  end
  );simpl;
  econstructor eassumption
 .
 
 
 Ltac dp_concl_tac h2 h cont_tac 
  t :=
  match t with
    | False => let h' := fresh "a" in 
                (set (h':=t) in *;cont_tac h';
                  repeat (
                  let e := type of h in 
                   (match e with
                      | ?t => unfold t in h|-;
                               (case h;
                                [abstract (clear h;intros h;injection h;
                                            clear h;intros ;subst;
                                            included_dp_tac h2)|
                                clear h;intros h;clear t])
                      | ?t => unfold t in h|-;elim h
                      end
                    )
                  ))
    | or ?a ?b => let cont_tac 
                   h' := let h'' := fresh "a" in 
                          (set (h'':=or a h') in *;cont_tac h'') in 
                   (dp_concl_tac h2 h cont_tac b)
    end
  .
 
 
 Module WF_DP_R_xml_0.
  Inductive DP_R_xml_0_large  :
   algebra.Alg.term ->algebra.Alg.term ->Prop := 
     (* <a__sieve(cons(s(N_),Y_)),mark(N_)> *)
    | DP_R_xml_0_large_0 :
     forall x4 x2 x9, 
      (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                 
        (algebra.Alg.Term algebra.F.id_cons ((algebra.Alg.Term 
         algebra.F.id_s (x4::nil))::x2::nil)) x9) ->
       DP_R_xml_0_large (algebra.Alg.Term algebra.F.id_mark (x4::nil)) 
        (algebra.Alg.Term algebra.F.id_a__sieve (x9::nil))
     (* <a__nats(N_),mark(N_)> *)
    | DP_R_xml_0_large_1 :
     forall x4 x9, 
      (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                 x4 x9) ->
       DP_R_xml_0_large (algebra.Alg.Term algebra.F.id_mark (x4::nil)) 
        (algebra.Alg.Term algebra.F.id_a__nats (x9::nil))
     (* <a__zprimes,a__sieve(a__nats(s(s(0))))> *)
    | DP_R_xml_0_large_2 :
     DP_R_xml_0_large (algebra.Alg.Term algebra.F.id_a__sieve 
                       ((algebra.Alg.Term algebra.F.id_a__nats 
                       ((algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Term 
                       algebra.F.id_s ((algebra.Alg.Term algebra.F.id_0 
                       nil)::nil))::nil))::nil))::nil)) 
      (algebra.Alg.Term algebra.F.id_a__zprimes nil)
     (* <a__zprimes,a__nats(s(s(0)))> *)
    | DP_R_xml_0_large_3 :
     DP_R_xml_0_large (algebra.Alg.Term algebra.F.id_a__nats 
                       ((algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Term 
                       algebra.F.id_s ((algebra.Alg.Term algebra.F.id_0 
                       nil)::nil))::nil))::nil)) 
      (algebra.Alg.Term algebra.F.id_a__zprimes nil)
     (* <mark(nats(X_)),a__nats(mark(X_))> *)
    | DP_R_xml_0_large_4 :
     forall x1 x9, 
      (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                 
        (algebra.Alg.Term algebra.F.id_nats (x1::nil)) x9) ->
       DP_R_xml_0_large (algebra.Alg.Term algebra.F.id_a__nats 
                         ((algebra.Alg.Term algebra.F.id_mark 
                         (x1::nil))::nil)) 
        (algebra.Alg.Term algebra.F.id_mark (x9::nil))
     (* <mark(nats(X_)),mark(X_)> *)
    | DP_R_xml_0_large_5 :
     forall x1 x9, 
      (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                 
        (algebra.Alg.Term algebra.F.id_nats (x1::nil)) x9) ->
       DP_R_xml_0_large (algebra.Alg.Term algebra.F.id_mark (x1::nil)) 
        (algebra.Alg.Term algebra.F.id_mark (x9::nil))
     (* <mark(cons(X1_,X2_)),mark(X1_)> *)
    | DP_R_xml_0_large_6 :
     forall x6 x9 x5, 
      (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                 
        (algebra.Alg.Term algebra.F.id_cons (x5::x6::nil)) x9) ->
       DP_R_xml_0_large (algebra.Alg.Term algebra.F.id_mark (x5::nil)) 
        (algebra.Alg.Term algebra.F.id_mark (x9::nil))
     (* <mark(s(X_)),mark(X_)> *)
    | DP_R_xml_0_large_7 :
     forall x1 x9, 
      (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                 (algebra.Alg.Term algebra.F.id_s (x1::nil)) 
        x9) ->
       DP_R_xml_0_large (algebra.Alg.Term algebra.F.id_mark (x1::nil)) 
        (algebra.Alg.Term algebra.F.id_mark (x9::nil))
  .
  
  
  Inductive DP_R_xml_0_strict  :
   algebra.Alg.term ->algebra.Alg.term ->Prop := 
     (* <a__filter(cons(X_,Y_),s(N_),M_),mark(X_)> *)
    | DP_R_xml_0_strict_0 :
     forall x4 x2 x10 x1 x9 x3 x11, 
      (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                 
        (algebra.Alg.Term algebra.F.id_cons (x1::x2::nil)) x11) ->
       (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                  
         (algebra.Alg.Term algebra.F.id_s (x4::nil)) x10) ->
        (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                   x3 x9) ->
         DP_R_xml_0_strict (algebra.Alg.Term algebra.F.id_mark (x1::nil)) 
          (algebra.Alg.Term algebra.F.id_a__filter (x11::x10::x9::nil))
    
     (* <mark(filter(X1_,X2_,X3_)),a__filter(mark(X1_),mark(X2_),mark(X3_))> *)
    | DP_R_xml_0_strict_1 :
     forall x6 x9 x5 x7, 
      (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                 
        (algebra.Alg.Term algebra.F.id_filter (x5::x6::x7::nil)) x9) ->
       DP_R_xml_0_strict (algebra.Alg.Term algebra.F.id_a__filter 
                          ((algebra.Alg.Term algebra.F.id_mark (x5::nil))::
                          (algebra.Alg.Term algebra.F.id_mark (x6::nil))::
                          (algebra.Alg.Term algebra.F.id_mark 
                          (x7::nil))::nil)) 
        (algebra.Alg.Term algebra.F.id_mark (x9::nil))
     (* <mark(filter(X1_,X2_,X3_)),mark(X1_)> *)
    | DP_R_xml_0_strict_2 :
     forall x6 x9 x5 x7, 
      (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                 
        (algebra.Alg.Term algebra.F.id_filter (x5::x6::x7::nil)) x9) ->
       DP_R_xml_0_strict (algebra.Alg.Term algebra.F.id_mark (x5::nil)) 
        (algebra.Alg.Term algebra.F.id_mark (x9::nil))
     (* <mark(filter(X1_,X2_,X3_)),mark(X2_)> *)
    | DP_R_xml_0_strict_3 :
     forall x6 x9 x5 x7, 
      (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                 
        (algebra.Alg.Term algebra.F.id_filter (x5::x6::x7::nil)) x9) ->
       DP_R_xml_0_strict (algebra.Alg.Term algebra.F.id_mark (x6::nil)) 
        (algebra.Alg.Term algebra.F.id_mark (x9::nil))
     (* <mark(filter(X1_,X2_,X3_)),mark(X3_)> *)
    | DP_R_xml_0_strict_4 :
     forall x6 x9 x5 x7, 
      (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                 
        (algebra.Alg.Term algebra.F.id_filter (x5::x6::x7::nil)) x9) ->
       DP_R_xml_0_strict (algebra.Alg.Term algebra.F.id_mark (x7::nil)) 
        (algebra.Alg.Term algebra.F.id_mark (x9::nil))
     (* <mark(sieve(X_)),a__sieve(mark(X_))> *)
    | DP_R_xml_0_strict_5 :
     forall x1 x9, 
      (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                 
        (algebra.Alg.Term algebra.F.id_sieve (x1::nil)) x9) ->
       DP_R_xml_0_strict (algebra.Alg.Term algebra.F.id_a__sieve 
                          ((algebra.Alg.Term algebra.F.id_mark 
                          (x1::nil))::nil)) 
        (algebra.Alg.Term algebra.F.id_mark (x9::nil))
     (* <mark(sieve(X_)),mark(X_)> *)
    | DP_R_xml_0_strict_6 :
     forall x1 x9, 
      (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                 
        (algebra.Alg.Term algebra.F.id_sieve (x1::nil)) x9) ->
       DP_R_xml_0_strict (algebra.Alg.Term algebra.F.id_mark (x1::nil)) 
        (algebra.Alg.Term algebra.F.id_mark (x9::nil))
     (* <mark(zprimes),a__zprimes> *)
    | DP_R_xml_0_strict_7 :
     forall x9, 
      (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                 (algebra.Alg.Term algebra.F.id_zprimes nil) 
        x9) ->
       DP_R_xml_0_strict (algebra.Alg.Term algebra.F.id_a__zprimes nil) 
        (algebra.Alg.Term algebra.F.id_mark (x9::nil))
  .
  
  
  Module WF_DP_R_xml_0_large.
   Inductive DP_R_xml_0_large_scc_1  :
    algebra.Alg.term ->algebra.Alg.term ->Prop := 
      (* <mark(nats(X_)),a__nats(mark(X_))> *)
     | DP_R_xml_0_large_scc_1_0 :
      forall x1 x9, 
       (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                  
         (algebra.Alg.Term algebra.F.id_nats (x1::nil)) x9) ->
        DP_R_xml_0_large_scc_1 (algebra.Alg.Term algebra.F.id_a__nats 
                                ((algebra.Alg.Term algebra.F.id_mark 
                                (x1::nil))::nil)) 
         (algebra.Alg.Term algebra.F.id_mark (x9::nil))
      (* <a__nats(N_),mark(N_)> *)
     | DP_R_xml_0_large_scc_1_1 :
      forall x4 x9, 
       (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                  x4 x9) ->
        DP_R_xml_0_large_scc_1 (algebra.Alg.Term algebra.F.id_mark (x4::nil)) 
         (algebra.Alg.Term algebra.F.id_a__nats (x9::nil))
      (* <mark(nats(X_)),mark(X_)> *)
     | DP_R_xml_0_large_scc_1_2 :
      forall x1 x9, 
       (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                  
         (algebra.Alg.Term algebra.F.id_nats (x1::nil)) x9) ->
        DP_R_xml_0_large_scc_1 (algebra.Alg.Term algebra.F.id_mark (x1::nil)) 
         (algebra.Alg.Term algebra.F.id_mark (x9::nil))
      (* <mark(cons(X1_,X2_)),mark(X1_)> *)
     | DP_R_xml_0_large_scc_1_3 :
      forall x6 x9 x5, 
       (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                  
         (algebra.Alg.Term algebra.F.id_cons (x5::x6::nil)) x9) ->
        DP_R_xml_0_large_scc_1 (algebra.Alg.Term algebra.F.id_mark (x5::nil)) 
         (algebra.Alg.Term algebra.F.id_mark (x9::nil))
      (* <mark(s(X_)),mark(X_)> *)
     | DP_R_xml_0_large_scc_1_4 :
      forall x1 x9, 
       (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                  
         (algebra.Alg.Term algebra.F.id_s (x1::nil)) x9) ->
        DP_R_xml_0_large_scc_1 (algebra.Alg.Term algebra.F.id_mark (x1::nil)) 
         (algebra.Alg.Term algebra.F.id_mark (x9::nil))
   .
   
   
   Module WF_DP_R_xml_0_large_scc_1.
    Inductive DP_R_xml_0_large_scc_1_large  :
     algebra.Alg.term ->algebra.Alg.term ->Prop := 
       (* <mark(cons(X1_,X2_)),mark(X1_)> *)
      | DP_R_xml_0_large_scc_1_large_0 :
       forall x6 x9 x5, 
        (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                   
          (algebra.Alg.Term algebra.F.id_cons (x5::x6::nil)) x9) ->
         DP_R_xml_0_large_scc_1_large (algebra.Alg.Term algebra.F.id_mark 
                                       (x5::nil)) 
          (algebra.Alg.Term algebra.F.id_mark (x9::nil))
       (* <mark(s(X_)),mark(X_)> *)
      | DP_R_xml_0_large_scc_1_large_1 :
       forall x1 x9, 
        (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                   
          (algebra.Alg.Term algebra.F.id_s (x1::nil)) x9) ->
         DP_R_xml_0_large_scc_1_large (algebra.Alg.Term algebra.F.id_mark 
                                       (x1::nil)) 
          (algebra.Alg.Term algebra.F.id_mark (x9::nil))
    .
    
    
    Inductive DP_R_xml_0_large_scc_1_strict  :
     algebra.Alg.term ->algebra.Alg.term ->Prop := 
       (* <mark(nats(X_)),a__nats(mark(X_))> *)
      | DP_R_xml_0_large_scc_1_strict_0 :
       forall x1 x9, 
        (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                   
          (algebra.Alg.Term algebra.F.id_nats (x1::nil)) x9) ->
         DP_R_xml_0_large_scc_1_strict (algebra.Alg.Term 
                                        algebra.F.id_a__nats 
                                        ((algebra.Alg.Term algebra.F.id_mark 
                                        (x1::nil))::nil)) 
          (algebra.Alg.Term algebra.F.id_mark (x9::nil))
       (* <a__nats(N_),mark(N_)> *)
      | DP_R_xml_0_large_scc_1_strict_1 :
       forall x4 x9, 
        (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                   x4 x9) ->
         DP_R_xml_0_large_scc_1_strict (algebra.Alg.Term algebra.F.id_mark 
                                        (x4::nil)) 
          (algebra.Alg.Term algebra.F.id_a__nats (x9::nil))
       (* <mark(nats(X_)),mark(X_)> *)
      | DP_R_xml_0_large_scc_1_strict_2 :
       forall x1 x9, 
        (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                   
          (algebra.Alg.Term algebra.F.id_nats (x1::nil)) x9) ->
         DP_R_xml_0_large_scc_1_strict (algebra.Alg.Term algebra.F.id_mark 
                                        (x1::nil)) 
          (algebra.Alg.Term algebra.F.id_mark (x9::nil))
    .
    
    
    Module WF_DP_R_xml_0_large_scc_1_large.
     Inductive DP_R_xml_0_large_scc_1_large_large  :
      algebra.Alg.term ->algebra.Alg.term ->Prop := 
        (* <mark(cons(X1_,X2_)),mark(X1_)> *)
       | DP_R_xml_0_large_scc_1_large_large_0 :
        forall x6 x9 x5, 
         (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                    
           (algebra.Alg.Term algebra.F.id_cons (x5::x6::nil)) x9) ->
          DP_R_xml_0_large_scc_1_large_large (algebra.Alg.Term 
                                              algebra.F.id_mark (x5::nil)) 
           (algebra.Alg.Term algebra.F.id_mark (x9::nil))
     .
     
     
     Inductive DP_R_xml_0_large_scc_1_large_strict  :
      algebra.Alg.term ->algebra.Alg.term ->Prop := 
        (* <mark(s(X_)),mark(X_)> *)
       | DP_R_xml_0_large_scc_1_large_strict_0 :
        forall x1 x9, 
         (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                    
           (algebra.Alg.Term algebra.F.id_s (x1::nil)) x9) ->
          DP_R_xml_0_large_scc_1_large_strict (algebra.Alg.Term 
                                               algebra.F.id_mark (x1::nil)) 
           (algebra.Alg.Term algebra.F.id_mark (x9::nil))
     .
     
     
     Module WF_DP_R_xml_0_large_scc_1_large_large.
      Open Scope Z_scope.
      
      Import ring_extention.
      
      Notation Local "a <= b" := (Zle a b).
      
      Notation Local "a < b" := (Zlt a b).
      
      Definition P_id_a__filter (x9:Z) (x10:Z) (x11:Z) := 2 + 2* x9 + 2* x10.
      
      Definition P_id_a__nats (x9:Z) := 2 + 2* x9.
      
      Definition P_id_s (x9:Z) := 1.
      
      Definition P_id_0  := 1.
      
      Definition P_id_a__zprimes  := 2.
      
      Definition P_id_a__sieve (x9:Z) := 2.
      
      Definition P_id_cons (x9:Z) (x10:Z) := 1 + 1* x9.
      
      Definition P_id_nats (x9:Z) := 2 + 2* x9.
      
      Definition P_id_mark (x9:Z) := 2* x9.
      
      Definition P_id_filter (x9:Z) (x10:Z) (x11:Z) := 1 + 2* x9 + 2* x10.
      
      Definition P_id_zprimes  := 2.
      
      Definition P_id_sieve (x9:Z) := 1.
      
      Lemma P_id_a__filter_monotonic :
       forall x12 x10 x14 x9 x13 x11, 
        (1 <= x14)/\ (x14 <= x13) ->
         (1 <= x12)/\ (x12 <= x11) ->
          (1 <= x10)/\ (x10 <= x9) ->
           P_id_a__filter x10 x12 x14 <= P_id_a__filter x9 x11 x13.
      Proof.
        intros x14 x13 x12 x11 x10 x9.
        intros [H_1 H_0].
        intros [H_3 H_2].
        intros [H_5 H_4].
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma P_id_a__nats_monotonic :
       forall x10 x9, 
        (1 <= x10)/\ (x10 <= x9) ->P_id_a__nats x10 <= P_id_a__nats x9.
      Proof.
        intros x10 x9.
        intros [H_1 H_0].
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma P_id_s_monotonic :
       forall x10 x9, (1 <= x10)/\ (x10 <= x9) ->P_id_s x10 <= P_id_s x9.
      Proof.
        intros x10 x9.
        intros [H_1 H_0].
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma P_id_a__sieve_monotonic :
       forall x10 x9, 
        (1 <= x10)/\ (x10 <= x9) ->P_id_a__sieve x10 <= P_id_a__sieve x9.
      Proof.
        intros x10 x9.
        intros [H_1 H_0].
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma P_id_cons_monotonic :
       forall x12 x10 x9 x11, 
        (1 <= x12)/\ (x12 <= x11) ->
         (1 <= x10)/\ (x10 <= x9) ->P_id_cons x10 x12 <= P_id_cons x9 x11.
      Proof.
        intros x12 x11 x10 x9.
        intros [H_1 H_0].
        intros [H_3 H_2].
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma P_id_nats_monotonic :
       forall x10 x9, 
        (1 <= x10)/\ (x10 <= x9) ->P_id_nats x10 <= P_id_nats x9.
      Proof.
        intros x10 x9.
        intros [H_1 H_0].
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma P_id_mark_monotonic :
       forall x10 x9, 
        (1 <= x10)/\ (x10 <= x9) ->P_id_mark x10 <= P_id_mark x9.
      Proof.
        intros x10 x9.
        intros [H_1 H_0].
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma P_id_filter_monotonic :
       forall x12 x10 x14 x9 x13 x11, 
        (1 <= x14)/\ (x14 <= x13) ->
         (1 <= x12)/\ (x12 <= x11) ->
          (1 <= x10)/\ (x10 <= x9) ->
           P_id_filter x10 x12 x14 <= P_id_filter x9 x11 x13.
      Proof.
        intros x14 x13 x12 x11 x10 x9.
        intros [H_1 H_0].
        intros [H_3 H_2].
        intros [H_5 H_4].
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma P_id_sieve_monotonic :
       forall x10 x9, 
        (1 <= x10)/\ (x10 <= x9) ->P_id_sieve x10 <= P_id_sieve x9.
      Proof.
        intros x10 x9.
        intros [H_1 H_0].
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma P_id_a__filter_bounded :
       forall x10 x9 x11, 
        (1 <= x9) ->(1 <= x10) ->(1 <= x11) ->1 <= P_id_a__filter x11 x10 x9.
      Proof.
        intros .
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma P_id_a__nats_bounded :
       forall x9, (1 <= x9) ->1 <= P_id_a__nats x9.
      Proof.
        intros .
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma P_id_s_bounded : forall x9, (1 <= x9) ->1 <= P_id_s x9.
      Proof.
        intros .
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma P_id_0_bounded : 1 <= P_id_0 .
      Proof.
        intros .
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma P_id_a__zprimes_bounded : 1 <= P_id_a__zprimes .
      Proof.
        intros .
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma P_id_a__sieve_bounded :
       forall x9, (1 <= x9) ->1 <= P_id_a__sieve x9.
      Proof.
        intros .
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma P_id_cons_bounded :
       forall x10 x9, (1 <= x9) ->(1 <= x10) ->1 <= P_id_cons x10 x9.
      Proof.
        intros .
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma P_id_nats_bounded : forall x9, (1 <= x9) ->1 <= P_id_nats x9.
      Proof.
        intros .
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma P_id_mark_bounded : forall x9, (1 <= x9) ->1 <= P_id_mark x9.
      Proof.
        intros .
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma P_id_filter_bounded :
       forall x10 x9 x11, 
        (1 <= x9) ->(1 <= x10) ->(1 <= x11) ->1 <= P_id_filter x11 x10 x9.
      Proof.
        intros .
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma P_id_zprimes_bounded : 1 <= P_id_zprimes .
      Proof.
        intros .
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma P_id_sieve_bounded : forall x9, (1 <= x9) ->1 <= P_id_sieve x9.
      Proof.
        intros .
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Definition measure  := 
        InterpZ.measure 1 P_id_a__filter P_id_a__nats P_id_s P_id_0 
         P_id_a__zprimes P_id_a__sieve P_id_cons P_id_nats P_id_mark 
         P_id_filter P_id_zprimes P_id_sieve.
      
      Lemma measure_equation :
       forall t, 
        measure t = match t with
                      | (algebra.Alg.Term algebra.F.id_a__filter (x11::x10::
                         x9::nil)) =>
                       P_id_a__filter (measure x11) (measure x10) 
                        (measure x9)
                      | (algebra.Alg.Term algebra.F.id_a__nats (x9::nil)) =>
                       P_id_a__nats (measure x9)
                      | (algebra.Alg.Term algebra.F.id_s (x9::nil)) =>
                       P_id_s (measure x9)
                      | (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0 
                      | (algebra.Alg.Term algebra.F.id_a__zprimes nil) =>
                       P_id_a__zprimes 
                      | (algebra.Alg.Term algebra.F.id_a__sieve (x9::nil)) =>
                       P_id_a__sieve (measure x9)
                      | (algebra.Alg.Term algebra.F.id_cons (x10::x9::nil)) =>
                       P_id_cons (measure x10) (measure x9)
                      | (algebra.Alg.Term algebra.F.id_nats (x9::nil)) =>
                       P_id_nats (measure x9)
                      | (algebra.Alg.Term algebra.F.id_mark (x9::nil)) =>
                       P_id_mark (measure x9)
                      | (algebra.Alg.Term algebra.F.id_filter (x11::x10::
                         x9::nil)) =>
                       P_id_filter (measure x11) (measure x10) (measure x9)
                      | (algebra.Alg.Term algebra.F.id_zprimes nil) =>
                       P_id_zprimes 
                      | (algebra.Alg.Term algebra.F.id_sieve (x9::nil)) =>
                       P_id_sieve (measure x9)
                      | _ => 1
                      end.
      Proof.
        intros t;case t;intros ;apply refl_equal.
      Qed.
      
      Lemma measure_bounded : forall t, 1 <= measure t.
      Proof.
        unfold measure in |-*.
        
        apply InterpZ.measure_bounded;
         cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
          (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Ltac generate_pos_hyp  :=
       match goal with
         | H:context [measure ?x] |- _ =>
          let v := fresh "v" in 
           (let H := fresh "h" in 
             (set (H:=measure_bounded x) in *;set (v:=measure x) in *;
               clearbody H;clearbody v))
         |  |- context [measure ?x] =>
          let v := fresh "v" in 
           (let H := fresh "h" in 
             (set (H:=measure_bounded x) in *;set (v:=measure x) in *;
               clearbody H;clearbody v))
         end
       .
      
      Lemma rules_monotonic :
       forall l r, 
        (algebra.EQT.axiom R_xml_0_deep_rew.R_xml_0_rules r l) ->
         measure r <= measure l.
      Proof.
        intros l r H.
        fold measure in |-*.
        
        inversion H;clear H;subst;inversion H0;clear H0;subst;
         simpl algebra.EQT.T.apply_subst in |-*;
         repeat (
         match goal with
           |  |- context [measure (algebra.Alg.Term ?f ?t)] =>
            rewrite (measure_equation (algebra.Alg.Term f t))
           end
         );repeat (generate_pos_hyp );
         cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
          (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma measure_star_monotonic :
       forall l r, 
        (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                   r l) ->measure r <= measure l.
      Proof.
        unfold measure in *.
        apply InterpZ.measure_star_monotonic.
        intros ;apply P_id_a__filter_monotonic;assumption.
        intros ;apply P_id_a__nats_monotonic;assumption.
        intros ;apply P_id_s_monotonic;assumption.
        intros ;apply P_id_a__sieve_monotonic;assumption.
        intros ;apply P_id_cons_monotonic;assumption.
        intros ;apply P_id_nats_monotonic;assumption.
        intros ;apply P_id_mark_monotonic;assumption.
        intros ;apply P_id_filter_monotonic;assumption.
        intros ;apply P_id_sieve_monotonic;assumption.
        intros ;apply P_id_a__filter_bounded;assumption.
        intros ;apply P_id_a__nats_bounded;assumption.
        intros ;apply P_id_s_bounded;assumption.
        intros ;apply P_id_0_bounded;assumption.
        intros ;apply P_id_a__zprimes_bounded;assumption.
        intros ;apply P_id_a__sieve_bounded;assumption.
        intros ;apply P_id_cons_bounded;assumption.
        intros ;apply P_id_nats_bounded;assumption.
        intros ;apply P_id_mark_bounded;assumption.
        intros ;apply P_id_filter_bounded;assumption.
        intros ;apply P_id_zprimes_bounded;assumption.
        intros ;apply P_id_sieve_bounded;assumption.
        apply rules_monotonic.
      Qed.
      
      Definition P_id_A__ZPRIMES  := 0.
      
      Definition P_id_A__FILTER (x9:Z) (x10:Z) (x11:Z) := 0.
      
      Definition P_id_A__SIEVE (x9:Z) := 0.
      
      Definition P_id_MARK (x9:Z) := 2* x9.
      
      Definition P_id_A__NATS (x9:Z) := 0.
      
      Lemma P_id_A__FILTER_monotonic :
       forall x12 x10 x14 x9 x13 x11, 
        (1 <= x14)/\ (x14 <= x13) ->
         (1 <= x12)/\ (x12 <= x11) ->
          (1 <= x10)/\ (x10 <= x9) ->
           P_id_A__FILTER x10 x12 x14 <= P_id_A__FILTER x9 x11 x13.
      Proof.
        intros x14 x13 x12 x11 x10 x9.
        intros [H_1 H_0].
        intros [H_3 H_2].
        intros [H_5 H_4].
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma P_id_A__SIEVE_monotonic :
       forall x10 x9, 
        (1 <= x10)/\ (x10 <= x9) ->P_id_A__SIEVE x10 <= P_id_A__SIEVE x9.
      Proof.
        intros x10 x9.
        intros [H_1 H_0].
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma P_id_MARK_monotonic :
       forall x10 x9, 
        (1 <= x10)/\ (x10 <= x9) ->P_id_MARK x10 <= P_id_MARK x9.
      Proof.
        intros x10 x9.
        intros [H_1 H_0].
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Lemma P_id_A__NATS_monotonic :
       forall x10 x9, 
        (1 <= x10)/\ (x10 <= x9) ->P_id_A__NATS x10 <= P_id_A__NATS x9.
      Proof.
        intros x10 x9.
        intros [H_1 H_0].
        
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
      Qed.
      
      Definition marked_measure  := 
        InterpZ.marked_measure 1 P_id_a__filter P_id_a__nats P_id_s P_id_0 
         P_id_a__zprimes P_id_a__sieve P_id_cons P_id_nats P_id_mark 
         P_id_filter P_id_zprimes P_id_sieve P_id_A__ZPRIMES P_id_A__FILTER 
         P_id_A__SIEVE P_id_MARK P_id_A__NATS.
      
      Lemma marked_measure_equation :
       forall t, 
        marked_measure t = match t with
                             | (algebra.Alg.Term algebra.F.id_a__zprimes nil) =>
                              P_id_A__ZPRIMES 
                             | (algebra.Alg.Term algebra.F.id_a__filter 
                                (x11::x10::x9::nil)) =>
                              P_id_A__FILTER (measure x11) (measure x10) 
                               (measure x9)
                             | (algebra.Alg.Term algebra.F.id_a__sieve 
                                (x9::nil)) =>
                              P_id_A__SIEVE (measure x9)
                             | (algebra.Alg.Term algebra.F.id_mark (x9::nil)) =>
                              P_id_MARK (measure x9)
                             | (algebra.Alg.Term algebra.F.id_a__nats 
                                (x9::nil)) =>
                              P_id_A__NATS (measure x9)
                             | _ => measure t
                             end.
      Proof.
        reflexivity .
      Qed.
      
      Lemma marked_measure_star_monotonic :
       forall f l1 l2, 
        (closure.refl_trans_clos (closure.one_step_list (algebra.EQT.one_step 
                                                          R_xml_0_deep_rew.R_xml_0_rules)
                                                         ) l1 l2) ->
         marked_measure (algebra.Alg.Term f l1) <= marked_measure (algebra.Alg.Term 
                                                                    f 
                                                                    l2).
      Proof.
        unfold marked_measure in *.
        apply InterpZ.marked_measure_star_monotonic.
        intros ;apply P_id_a__filter_monotonic;assumption.
        intros ;apply P_id_a__nats_monotonic;assumption.
        intros ;apply P_id_s_monotonic;assumption.
        intros ;apply P_id_a__sieve_monotonic;assumption.
        intros ;apply P_id_cons_monotonic;assumption.
        intros ;apply P_id_nats_monotonic;assumption.
        intros ;apply P_id_mark_monotonic;assumption.
        intros ;apply P_id_filter_monotonic;assumption.
        intros ;apply P_id_sieve_monotonic;assumption.
        intros ;apply P_id_a__filter_bounded;assumption.
        intros ;apply P_id_a__nats_bounded;assumption.
        intros ;apply P_id_s_bounded;assumption.
        intros ;apply P_id_0_bounded;assumption.
        intros ;apply P_id_a__zprimes_bounded;assumption.
        intros ;apply P_id_a__sieve_bounded;assumption.
        intros ;apply P_id_cons_bounded;assumption.
        intros ;apply P_id_nats_bounded;assumption.
        intros ;apply P_id_mark_bounded;assumption.
        intros ;apply P_id_filter_bounded;assumption.
        intros ;apply P_id_zprimes_bounded;assumption.
        intros ;apply P_id_sieve_bounded;assumption.
        apply rules_monotonic.
        intros ;apply P_id_A__FILTER_monotonic;assumption.
        intros ;apply P_id_A__SIEVE_monotonic;assumption.
        intros ;apply P_id_MARK_monotonic;assumption.
        intros ;apply P_id_A__NATS_monotonic;assumption.
      Qed.
      
      Ltac rewrite_and_unfold  :=
       do 2 (rewrite marked_measure_equation);
        repeat (
        match goal with
          |  |- context [measure (algebra.Alg.Term ?f ?t)] =>
           rewrite (measure_equation (algebra.Alg.Term f t))
          | H:context [measure (algebra.Alg.Term ?f ?t)] |- _ =>
           rewrite (measure_equation (algebra.Alg.Term f t)) in H|-
          end
        ).
      
      
      Lemma wf :
       well_founded WF_DP_R_xml_0_large_scc_1_large.DP_R_xml_0_large_scc_1_large_large
        .
      Proof.
        intros x.
        
        apply well_founded_ind with
          (R:=fun x y => (Zwf.Zwf 1) (marked_measure x) (marked_measure y)).
        apply Inverse_Image.wf_inverse_image with  (B:=Z).
        apply Zwf.Zwf_well_founded.
        clear x.
        intros x IHx.
        
        repeat (
        constructor;inversion 1;subst;
         full_prove_ineq algebra.Alg.Term 
         ltac:(algebra.Alg_ext.find_replacement ) 
         algebra.EQT_ext.one_step_list_refl_trans_clos marked_measure 
         marked_measure_star_monotonic (Zwf.Zwf 1) (interp.o_Z 1) 
         ltac:(fun _ => R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 ) 
         ltac:(fun _ => rewrite_and_unfold ) 
         ltac:(fun _ => generate_pos_hyp ) 
         ltac:(fun _ => cbv beta iota zeta delta - [Zplus Zmult Zle Zlt] in * ;
                         try (constructor))
          IHx
        ).
      Qed.
     End WF_DP_R_xml_0_large_scc_1_large_large.
     
     Open Scope Z_scope.
     
     Import ring_extention.
     
     Notation Local "a <= b" := (Zle a b).
     
     Notation Local "a < b" := (Zlt a b).
     
     Definition P_id_a__filter (x9:Z) (x10:Z) (x11:Z) := 1* x9.
     
     Definition P_id_a__nats (x9:Z) := 1* x9.
     
     Definition P_id_s (x9:Z) := 1 + 2* x9.
     
     Definition P_id_0  := 0.
     
     Definition P_id_a__zprimes  := 3.
     
     Definition P_id_a__sieve (x9:Z) := 1* x9.
     
     Definition P_id_cons (x9:Z) (x10:Z) := 1* x9.
     
     Definition P_id_nats (x9:Z) := 1* x9.
     
     Definition P_id_mark (x9:Z) := 1* x9.
     
     Definition P_id_filter (x9:Z) (x10:Z) (x11:Z) := 1* x9.
     
     Definition P_id_zprimes  := 3.
     
     Definition P_id_sieve (x9:Z) := 1* x9.
     
     Lemma P_id_a__filter_monotonic :
      forall x12 x10 x14 x9 x13 x11, 
       (0 <= x14)/\ (x14 <= x13) ->
        (0 <= x12)/\ (x12 <= x11) ->
         (0 <= x10)/\ (x10 <= x9) ->
          P_id_a__filter x10 x12 x14 <= P_id_a__filter x9 x11 x13.
     Proof.
       intros x14 x13 x12 x11 x10 x9.
       intros [H_1 H_0].
       intros [H_3 H_2].
       intros [H_5 H_4].
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma P_id_a__nats_monotonic :
      forall x10 x9, 
       (0 <= x10)/\ (x10 <= x9) ->P_id_a__nats x10 <= P_id_a__nats x9.
     Proof.
       intros x10 x9.
       intros [H_1 H_0].
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma P_id_s_monotonic :
      forall x10 x9, (0 <= x10)/\ (x10 <= x9) ->P_id_s x10 <= P_id_s x9.
     Proof.
       intros x10 x9.
       intros [H_1 H_0].
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma P_id_a__sieve_monotonic :
      forall x10 x9, 
       (0 <= x10)/\ (x10 <= x9) ->P_id_a__sieve x10 <= P_id_a__sieve x9.
     Proof.
       intros x10 x9.
       intros [H_1 H_0].
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma P_id_cons_monotonic :
      forall x12 x10 x9 x11, 
       (0 <= x12)/\ (x12 <= x11) ->
        (0 <= x10)/\ (x10 <= x9) ->P_id_cons x10 x12 <= P_id_cons x9 x11.
     Proof.
       intros x12 x11 x10 x9.
       intros [H_1 H_0].
       intros [H_3 H_2].
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma P_id_nats_monotonic :
      forall x10 x9, (0 <= x10)/\ (x10 <= x9) ->P_id_nats x10 <= P_id_nats x9.
     Proof.
       intros x10 x9.
       intros [H_1 H_0].
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma P_id_mark_monotonic :
      forall x10 x9, (0 <= x10)/\ (x10 <= x9) ->P_id_mark x10 <= P_id_mark x9.
     Proof.
       intros x10 x9.
       intros [H_1 H_0].
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma P_id_filter_monotonic :
      forall x12 x10 x14 x9 x13 x11, 
       (0 <= x14)/\ (x14 <= x13) ->
        (0 <= x12)/\ (x12 <= x11) ->
         (0 <= x10)/\ (x10 <= x9) ->
          P_id_filter x10 x12 x14 <= P_id_filter x9 x11 x13.
     Proof.
       intros x14 x13 x12 x11 x10 x9.
       intros [H_1 H_0].
       intros [H_3 H_2].
       intros [H_5 H_4].
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma P_id_sieve_monotonic :
      forall x10 x9, 
       (0 <= x10)/\ (x10 <= x9) ->P_id_sieve x10 <= P_id_sieve x9.
     Proof.
       intros x10 x9.
       intros [H_1 H_0].
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma P_id_a__filter_bounded :
      forall x10 x9 x11, 
       (0 <= x9) ->(0 <= x10) ->(0 <= x11) ->0 <= P_id_a__filter x11 x10 x9.
     Proof.
       intros .
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma P_id_a__nats_bounded :
      forall x9, (0 <= x9) ->0 <= P_id_a__nats x9.
     Proof.
       intros .
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma P_id_s_bounded : forall x9, (0 <= x9) ->0 <= P_id_s x9.
     Proof.
       intros .
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma P_id_0_bounded : 0 <= P_id_0 .
     Proof.
       intros .
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma P_id_a__zprimes_bounded : 0 <= P_id_a__zprimes .
     Proof.
       intros .
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma P_id_a__sieve_bounded :
      forall x9, (0 <= x9) ->0 <= P_id_a__sieve x9.
     Proof.
       intros .
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma P_id_cons_bounded :
      forall x10 x9, (0 <= x9) ->(0 <= x10) ->0 <= P_id_cons x10 x9.
     Proof.
       intros .
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma P_id_nats_bounded : forall x9, (0 <= x9) ->0 <= P_id_nats x9.
     Proof.
       intros .
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma P_id_mark_bounded : forall x9, (0 <= x9) ->0 <= P_id_mark x9.
     Proof.
       intros .
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma P_id_filter_bounded :
      forall x10 x9 x11, 
       (0 <= x9) ->(0 <= x10) ->(0 <= x11) ->0 <= P_id_filter x11 x10 x9.
     Proof.
       intros .
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma P_id_zprimes_bounded : 0 <= P_id_zprimes .
     Proof.
       intros .
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma P_id_sieve_bounded : forall x9, (0 <= x9) ->0 <= P_id_sieve x9.
     Proof.
       intros .
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Definition measure  := 
       InterpZ.measure 0 P_id_a__filter P_id_a__nats P_id_s P_id_0 
        P_id_a__zprimes P_id_a__sieve P_id_cons P_id_nats P_id_mark 
        P_id_filter P_id_zprimes P_id_sieve.
     
     Lemma measure_equation :
      forall t, 
       measure t = match t with
                     | (algebra.Alg.Term algebra.F.id_a__filter (x11::x10::
                        x9::nil)) =>
                      P_id_a__filter (measure x11) (measure x10) (measure x9)
                     | (algebra.Alg.Term algebra.F.id_a__nats (x9::nil)) =>
                      P_id_a__nats (measure x9)
                     | (algebra.Alg.Term algebra.F.id_s (x9::nil)) =>
                      P_id_s (measure x9)
                     | (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0 
                     | (algebra.Alg.Term algebra.F.id_a__zprimes nil) =>
                      P_id_a__zprimes 
                     | (algebra.Alg.Term algebra.F.id_a__sieve (x9::nil)) =>
                      P_id_a__sieve (measure x9)
                     | (algebra.Alg.Term algebra.F.id_cons (x10::x9::nil)) =>
                      P_id_cons (measure x10) (measure x9)
                     | (algebra.Alg.Term algebra.F.id_nats (x9::nil)) =>
                      P_id_nats (measure x9)
                     | (algebra.Alg.Term algebra.F.id_mark (x9::nil)) =>
                      P_id_mark (measure x9)
                     | (algebra.Alg.Term algebra.F.id_filter (x11::x10::
                        x9::nil)) =>
                      P_id_filter (measure x11) (measure x10) (measure x9)
                     | (algebra.Alg.Term algebra.F.id_zprimes nil) =>
                      P_id_zprimes 
                     | (algebra.Alg.Term algebra.F.id_sieve (x9::nil)) =>
                      P_id_sieve (measure x9)
                     | _ => 0
                     end.
     Proof.
       intros t;case t;intros ;apply refl_equal.
     Qed.
     
     Lemma measure_bounded : forall t, 0 <= measure t.
     Proof.
       unfold measure in |-*.
       
       apply InterpZ.measure_bounded;
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Ltac generate_pos_hyp  :=
      match goal with
        | H:context [measure ?x] |- _ =>
         let v := fresh "v" in 
          (let H := fresh "h" in 
            (set (H:=measure_bounded x) in *;set (v:=measure x) in *;
              clearbody H;clearbody v))
        |  |- context [measure ?x] =>
         let v := fresh "v" in 
          (let H := fresh "h" in 
            (set (H:=measure_bounded x) in *;set (v:=measure x) in *;
              clearbody H;clearbody v))
        end
      .
     
     Lemma rules_monotonic :
      forall l r, 
       (algebra.EQT.axiom R_xml_0_deep_rew.R_xml_0_rules r l) ->
        measure r <= measure l.
     Proof.
       intros l r H.
       fold measure in |-*.
       
       inversion H;clear H;subst;inversion H0;clear H0;subst;
        simpl algebra.EQT.T.apply_subst in |-*;
        repeat (
        match goal with
          |  |- context [measure (algebra.Alg.Term ?f ?t)] =>
           rewrite (measure_equation (algebra.Alg.Term f t))
          end
        );repeat (generate_pos_hyp );
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma measure_star_monotonic :
      forall l r, 
       (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                  r l) ->measure r <= measure l.
     Proof.
       unfold measure in *.
       apply InterpZ.measure_star_monotonic.
       intros ;apply P_id_a__filter_monotonic;assumption.
       intros ;apply P_id_a__nats_monotonic;assumption.
       intros ;apply P_id_s_monotonic;assumption.
       intros ;apply P_id_a__sieve_monotonic;assumption.
       intros ;apply P_id_cons_monotonic;assumption.
       intros ;apply P_id_nats_monotonic;assumption.
       intros ;apply P_id_mark_monotonic;assumption.
       intros ;apply P_id_filter_monotonic;assumption.
       intros ;apply P_id_sieve_monotonic;assumption.
       intros ;apply P_id_a__filter_bounded;assumption.
       intros ;apply P_id_a__nats_bounded;assumption.
       intros ;apply P_id_s_bounded;assumption.
       intros ;apply P_id_0_bounded;assumption.
       intros ;apply P_id_a__zprimes_bounded;assumption.
       intros ;apply P_id_a__sieve_bounded;assumption.
       intros ;apply P_id_cons_bounded;assumption.
       intros ;apply P_id_nats_bounded;assumption.
       intros ;apply P_id_mark_bounded;assumption.
       intros ;apply P_id_filter_bounded;assumption.
       intros ;apply P_id_zprimes_bounded;assumption.
       intros ;apply P_id_sieve_bounded;assumption.
       apply rules_monotonic.
     Qed.
     
     Definition P_id_A__ZPRIMES  := 0.
     
     Definition P_id_A__FILTER (x9:Z) (x10:Z) (x11:Z) := 0.
     
     Definition P_id_A__SIEVE (x9:Z) := 0.
     
     Definition P_id_MARK (x9:Z) := 2* x9.
     
     Definition P_id_A__NATS (x9:Z) := 0.
     
     Lemma P_id_A__FILTER_monotonic :
      forall x12 x10 x14 x9 x13 x11, 
       (0 <= x14)/\ (x14 <= x13) ->
        (0 <= x12)/\ (x12 <= x11) ->
         (0 <= x10)/\ (x10 <= x9) ->
          P_id_A__FILTER x10 x12 x14 <= P_id_A__FILTER x9 x11 x13.
     Proof.
       intros x14 x13 x12 x11 x10 x9.
       intros [H_1 H_0].
       intros [H_3 H_2].
       intros [H_5 H_4].
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma P_id_A__SIEVE_monotonic :
      forall x10 x9, 
       (0 <= x10)/\ (x10 <= x9) ->P_id_A__SIEVE x10 <= P_id_A__SIEVE x9.
     Proof.
       intros x10 x9.
       intros [H_1 H_0].
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma P_id_MARK_monotonic :
      forall x10 x9, (0 <= x10)/\ (x10 <= x9) ->P_id_MARK x10 <= P_id_MARK x9.
     Proof.
       intros x10 x9.
       intros [H_1 H_0].
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma P_id_A__NATS_monotonic :
      forall x10 x9, 
       (0 <= x10)/\ (x10 <= x9) ->P_id_A__NATS x10 <= P_id_A__NATS x9.
     Proof.
       intros x10 x9.
       intros [H_1 H_0].
       
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Definition marked_measure  := 
       InterpZ.marked_measure 0 P_id_a__filter P_id_a__nats P_id_s P_id_0 
        P_id_a__zprimes P_id_a__sieve P_id_cons P_id_nats P_id_mark 
        P_id_filter P_id_zprimes P_id_sieve P_id_A__ZPRIMES P_id_A__FILTER 
        P_id_A__SIEVE P_id_MARK P_id_A__NATS.
     
     Lemma marked_measure_equation :
      forall t, 
       marked_measure t = match t with
                            | (algebra.Alg.Term algebra.F.id_a__zprimes nil) =>
                             P_id_A__ZPRIMES 
                            | (algebra.Alg.Term algebra.F.id_a__filter (x11::
                               x10::x9::nil)) =>
                             P_id_A__FILTER (measure x11) (measure x10) 
                              (measure x9)
                            | (algebra.Alg.Term algebra.F.id_a__sieve 
                               (x9::nil)) =>
                             P_id_A__SIEVE (measure x9)
                            | (algebra.Alg.Term algebra.F.id_mark (x9::nil)) =>
                             P_id_MARK (measure x9)
                            | (algebra.Alg.Term algebra.F.id_a__nats 
                               (x9::nil)) =>
                             P_id_A__NATS (measure x9)
                            | _ => measure t
                            end.
     Proof.
       reflexivity .
     Qed.
     
     Lemma marked_measure_star_monotonic :
      forall f l1 l2, 
       (closure.refl_trans_clos (closure.one_step_list (algebra.EQT.one_step 
                                                         R_xml_0_deep_rew.R_xml_0_rules)
                                                        ) l1 l2) ->
        marked_measure (algebra.Alg.Term f l1) <= marked_measure (algebra.Alg.Term 
                                                                   f 
                                                                   l2).
     Proof.
       unfold marked_measure in *.
       apply InterpZ.marked_measure_star_monotonic.
       intros ;apply P_id_a__filter_monotonic;assumption.
       intros ;apply P_id_a__nats_monotonic;assumption.
       intros ;apply P_id_s_monotonic;assumption.
       intros ;apply P_id_a__sieve_monotonic;assumption.
       intros ;apply P_id_cons_monotonic;assumption.
       intros ;apply P_id_nats_monotonic;assumption.
       intros ;apply P_id_mark_monotonic;assumption.
       intros ;apply P_id_filter_monotonic;assumption.
       intros ;apply P_id_sieve_monotonic;assumption.
       intros ;apply P_id_a__filter_bounded;assumption.
       intros ;apply P_id_a__nats_bounded;assumption.
       intros ;apply P_id_s_bounded;assumption.
       intros ;apply P_id_0_bounded;assumption.
       intros ;apply P_id_a__zprimes_bounded;assumption.
       intros ;apply P_id_a__sieve_bounded;assumption.
       intros ;apply P_id_cons_bounded;assumption.
       intros ;apply P_id_nats_bounded;assumption.
       intros ;apply P_id_mark_bounded;assumption.
       intros ;apply P_id_filter_bounded;assumption.
       intros ;apply P_id_zprimes_bounded;assumption.
       intros ;apply P_id_sieve_bounded;assumption.
       apply rules_monotonic.
       intros ;apply P_id_A__FILTER_monotonic;assumption.
       intros ;apply P_id_A__SIEVE_monotonic;assumption.
       intros ;apply P_id_MARK_monotonic;assumption.
       intros ;apply P_id_A__NATS_monotonic;assumption.
     Qed.
     
     Ltac rewrite_and_unfold  :=
      do 2 (rewrite marked_measure_equation);
       repeat (
       match goal with
         |  |- context [measure (algebra.Alg.Term ?f ?t)] =>
          rewrite (measure_equation (algebra.Alg.Term f t))
         | H:context [measure (algebra.Alg.Term ?f ?t)] |- _ =>
          rewrite (measure_equation (algebra.Alg.Term f t)) in H|-
         end
       ).
     
     Definition lt a b := (Zwf.Zwf 0) (marked_measure a) (marked_measure b).
     
     Definition le a b := marked_measure a <= marked_measure b.
     
     Lemma lt_le_compat : forall a b c, (lt a b) ->(le b c) ->lt a c.
     Proof.
       unfold lt, le in *.
       intros a b c.
       apply (interp.le_lt_compat_right (interp.o_Z 0)).
     Qed.
     
     Lemma wf_lt : well_founded lt.
     Proof.
       unfold lt in *.
       apply Inverse_Image.wf_inverse_image with  (B:=Z).
       apply Zwf.Zwf_well_founded.
     Qed.
     
     Lemma DP_R_xml_0_large_scc_1_large_strict_in_lt :
      Relation_Definitions.inclusion _ DP_R_xml_0_large_scc_1_large_strict lt.
     Proof.
       unfold Relation_Definitions.inclusion, lt in *.
       
       intros a b H;destruct H;
        match goal with
          |  |- (Zwf.Zwf 0) _ (marked_measure (algebra.Alg.Term ?f ?l)) =>
           let l'' := algebra.Alg_ext.find_replacement l  in 
            ((apply (interp.le_lt_compat_right (interp.o_Z 0)) with
               (marked_measure (algebra.Alg.Term f l''));[idtac|
              apply marked_measure_star_monotonic;
               repeat (apply algebra.EQT_ext.one_step_list_refl_trans_clos);
               (assumption)||(constructor 1)]))
          end
        ;clear ;rewrite_and_unfold ;repeat (generate_pos_hyp );
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Lemma DP_R_xml_0_large_scc_1_large_large_in_le :
      Relation_Definitions.inclusion _ DP_R_xml_0_large_scc_1_large_large le.
     Proof.
       unfold Relation_Definitions.inclusion, le, Zwf.Zwf in *.
       
       intros a b H;destruct H;
        match goal with
          |  |- _ <= marked_measure (algebra.Alg.Term ?f ?l) =>
           let l'' := algebra.Alg_ext.find_replacement l  in 
            ((apply (interp.le_trans (interp.o_Z 0)) with
               (marked_measure (algebra.Alg.Term f l''));[idtac|
              apply marked_measure_star_monotonic;
               repeat (apply algebra.EQT_ext.one_step_list_refl_trans_clos);
               (assumption)||(constructor 1)]))
          end
        ;clear ;rewrite_and_unfold ;repeat (generate_pos_hyp );
        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
     Qed.
     
     Definition wf_DP_R_xml_0_large_scc_1_large_large  := 
       WF_DP_R_xml_0_large_scc_1_large_large.wf.
     
     
     Lemma wf :
      well_founded WF_DP_R_xml_0_large_scc_1.DP_R_xml_0_large_scc_1_large.
     Proof.
       intros x.
       apply (well_founded_ind wf_lt).
       clear x.
       intros x.
       pattern x.
       apply (@Acc_ind _ DP_R_xml_0_large_scc_1_large_large).
       clear x.
       intros x _ IHx IHx'.
       constructor.
       intros y H.
       
       destruct H;
        (apply IHx';apply DP_R_xml_0_large_scc_1_large_strict_in_lt;
          econstructor eassumption)||
        ((apply IHx;[econstructor eassumption|
          intros y' Hlt;apply IHx';apply lt_le_compat with (1:=Hlt) ;
           apply DP_R_xml_0_large_scc_1_large_large_in_le;
           econstructor eassumption])).
       apply wf_DP_R_xml_0_large_scc_1_large_large.
     Qed.
    End WF_DP_R_xml_0_large_scc_1_large.
    
    Open Scope Z_scope.
    
    Import ring_extention.
    
    Notation Local "a <= b" := (Zle a b).
    
    Notation Local "a < b" := (Zlt a b).
    
    Definition P_id_a__filter (x9:Z) (x10:Z) (x11:Z) := 1* x9 + 1* x11.
    
    Definition P_id_a__nats (x9:Z) := 2 + 1* x9.
    
    Definition P_id_s (x9:Z) := 2* x9.
    
    Definition P_id_0  := 0.
    
    Definition P_id_a__zprimes  := 2.
    
    Definition P_id_a__sieve (x9:Z) := 1* x9.
    
    Definition P_id_cons (x9:Z) (x10:Z) := 1* x9.
    
    Definition P_id_nats (x9:Z) := 2 + 1* x9.
    
    Definition P_id_mark (x9:Z) := 1* x9.
    
    Definition P_id_filter (x9:Z) (x10:Z) (x11:Z) := 1* x9 + 1* x11.
    
    Definition P_id_zprimes  := 2.
    
    Definition P_id_sieve (x9:Z) := 1* x9.
    
    Lemma P_id_a__filter_monotonic :
     forall x12 x10 x14 x9 x13 x11, 
      (0 <= x14)/\ (x14 <= x13) ->
       (0 <= x12)/\ (x12 <= x11) ->
        (0 <= x10)/\ (x10 <= x9) ->
         P_id_a__filter x10 x12 x14 <= P_id_a__filter x9 x11 x13.
    Proof.
      intros x14 x13 x12 x11 x10 x9.
      intros [H_1 H_0].
      intros [H_3 H_2].
      intros [H_5 H_4].
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma P_id_a__nats_monotonic :
     forall x10 x9, 
      (0 <= x10)/\ (x10 <= x9) ->P_id_a__nats x10 <= P_id_a__nats x9.
    Proof.
      intros x10 x9.
      intros [H_1 H_0].
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma P_id_s_monotonic :
     forall x10 x9, (0 <= x10)/\ (x10 <= x9) ->P_id_s x10 <= P_id_s x9.
    Proof.
      intros x10 x9.
      intros [H_1 H_0].
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma P_id_a__sieve_monotonic :
     forall x10 x9, 
      (0 <= x10)/\ (x10 <= x9) ->P_id_a__sieve x10 <= P_id_a__sieve x9.
    Proof.
      intros x10 x9.
      intros [H_1 H_0].
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma P_id_cons_monotonic :
     forall x12 x10 x9 x11, 
      (0 <= x12)/\ (x12 <= x11) ->
       (0 <= x10)/\ (x10 <= x9) ->P_id_cons x10 x12 <= P_id_cons x9 x11.
    Proof.
      intros x12 x11 x10 x9.
      intros [H_1 H_0].
      intros [H_3 H_2].
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma P_id_nats_monotonic :
     forall x10 x9, (0 <= x10)/\ (x10 <= x9) ->P_id_nats x10 <= P_id_nats x9.
    Proof.
      intros x10 x9.
      intros [H_1 H_0].
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma P_id_mark_monotonic :
     forall x10 x9, (0 <= x10)/\ (x10 <= x9) ->P_id_mark x10 <= P_id_mark x9.
    Proof.
      intros x10 x9.
      intros [H_1 H_0].
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma P_id_filter_monotonic :
     forall x12 x10 x14 x9 x13 x11, 
      (0 <= x14)/\ (x14 <= x13) ->
       (0 <= x12)/\ (x12 <= x11) ->
        (0 <= x10)/\ (x10 <= x9) ->
         P_id_filter x10 x12 x14 <= P_id_filter x9 x11 x13.
    Proof.
      intros x14 x13 x12 x11 x10 x9.
      intros [H_1 H_0].
      intros [H_3 H_2].
      intros [H_5 H_4].
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma P_id_sieve_monotonic :
     forall x10 x9, 
      (0 <= x10)/\ (x10 <= x9) ->P_id_sieve x10 <= P_id_sieve x9.
    Proof.
      intros x10 x9.
      intros [H_1 H_0].
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma P_id_a__filter_bounded :
     forall x10 x9 x11, 
      (0 <= x9) ->(0 <= x10) ->(0 <= x11) ->0 <= P_id_a__filter x11 x10 x9.
    Proof.
      intros .
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma P_id_a__nats_bounded : forall x9, (0 <= x9) ->0 <= P_id_a__nats x9.
    Proof.
      intros .
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma P_id_s_bounded : forall x9, (0 <= x9) ->0 <= P_id_s x9.
    Proof.
      intros .
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma P_id_0_bounded : 0 <= P_id_0 .
    Proof.
      intros .
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma P_id_a__zprimes_bounded : 0 <= P_id_a__zprimes .
    Proof.
      intros .
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma P_id_a__sieve_bounded :
     forall x9, (0 <= x9) ->0 <= P_id_a__sieve x9.
    Proof.
      intros .
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma P_id_cons_bounded :
     forall x10 x9, (0 <= x9) ->(0 <= x10) ->0 <= P_id_cons x10 x9.
    Proof.
      intros .
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma P_id_nats_bounded : forall x9, (0 <= x9) ->0 <= P_id_nats x9.
    Proof.
      intros .
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma P_id_mark_bounded : forall x9, (0 <= x9) ->0 <= P_id_mark x9.
    Proof.
      intros .
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma P_id_filter_bounded :
     forall x10 x9 x11, 
      (0 <= x9) ->(0 <= x10) ->(0 <= x11) ->0 <= P_id_filter x11 x10 x9.
    Proof.
      intros .
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma P_id_zprimes_bounded : 0 <= P_id_zprimes .
    Proof.
      intros .
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma P_id_sieve_bounded : forall x9, (0 <= x9) ->0 <= P_id_sieve x9.
    Proof.
      intros .
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Definition measure  := 
      InterpZ.measure 0 P_id_a__filter P_id_a__nats P_id_s P_id_0 
       P_id_a__zprimes P_id_a__sieve P_id_cons P_id_nats P_id_mark 
       P_id_filter P_id_zprimes P_id_sieve.
    
    Lemma measure_equation :
     forall t, 
      measure t = match t with
                    | (algebra.Alg.Term algebra.F.id_a__filter (x11::x10::
                       x9::nil)) =>
                     P_id_a__filter (measure x11) (measure x10) (measure x9)
                    | (algebra.Alg.Term algebra.F.id_a__nats (x9::nil)) =>
                     P_id_a__nats (measure x9)
                    | (algebra.Alg.Term algebra.F.id_s (x9::nil)) =>
                     P_id_s (measure x9)
                    | (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0 
                    | (algebra.Alg.Term algebra.F.id_a__zprimes nil) =>
                     P_id_a__zprimes 
                    | (algebra.Alg.Term algebra.F.id_a__sieve (x9::nil)) =>
                     P_id_a__sieve (measure x9)
                    | (algebra.Alg.Term algebra.F.id_cons (x10::x9::nil)) =>
                     P_id_cons (measure x10) (measure x9)
                    | (algebra.Alg.Term algebra.F.id_nats (x9::nil)) =>
                     P_id_nats (measure x9)
                    | (algebra.Alg.Term algebra.F.id_mark (x9::nil)) =>
                     P_id_mark (measure x9)
                    | (algebra.Alg.Term algebra.F.id_filter (x11::x10::
                       x9::nil)) =>
                     P_id_filter (measure x11) (measure x10) (measure x9)
                    | (algebra.Alg.Term algebra.F.id_zprimes nil) =>
                     P_id_zprimes 
                    | (algebra.Alg.Term algebra.F.id_sieve (x9::nil)) =>
                     P_id_sieve (measure x9)
                    | _ => 0
                    end.
    Proof.
      intros t;case t;intros ;apply refl_equal.
    Qed.
    
    Lemma measure_bounded : forall t, 0 <= measure t.
    Proof.
      unfold measure in |-*.
      
      apply InterpZ.measure_bounded;
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Ltac generate_pos_hyp  :=
     match goal with
       | H:context [measure ?x] |- _ =>
        let v := fresh "v" in 
         (let H := fresh "h" in 
           (set (H:=measure_bounded x) in *;set (v:=measure x) in *;
             clearbody H;clearbody v))
       |  |- context [measure ?x] =>
        let v := fresh "v" in 
         (let H := fresh "h" in 
           (set (H:=measure_bounded x) in *;set (v:=measure x) in *;
             clearbody H;clearbody v))
       end
     .
    
    Lemma rules_monotonic :
     forall l r, 
      (algebra.EQT.axiom R_xml_0_deep_rew.R_xml_0_rules r l) ->
       measure r <= measure l.
    Proof.
      intros l r H.
      fold measure in |-*.
      
      inversion H;clear H;subst;inversion H0;clear H0;subst;
       simpl algebra.EQT.T.apply_subst in |-*;
       repeat (
       match goal with
         |  |- context [measure (algebra.Alg.Term ?f ?t)] =>
          rewrite (measure_equation (algebra.Alg.Term f t))
         end
       );repeat (generate_pos_hyp );
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma measure_star_monotonic :
     forall l r, 
      (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                 r l) ->measure r <= measure l.
    Proof.
      unfold measure in *.
      apply InterpZ.measure_star_monotonic.
      intros ;apply P_id_a__filter_monotonic;assumption.
      intros ;apply P_id_a__nats_monotonic;assumption.
      intros ;apply P_id_s_monotonic;assumption.
      intros ;apply P_id_a__sieve_monotonic;assumption.
      intros ;apply P_id_cons_monotonic;assumption.
      intros ;apply P_id_nats_monotonic;assumption.
      intros ;apply P_id_mark_monotonic;assumption.
      intros ;apply P_id_filter_monotonic;assumption.
      intros ;apply P_id_sieve_monotonic;assumption.
      intros ;apply P_id_a__filter_bounded;assumption.
      intros ;apply P_id_a__nats_bounded;assumption.
      intros ;apply P_id_s_bounded;assumption.
      intros ;apply P_id_0_bounded;assumption.
      intros ;apply P_id_a__zprimes_bounded;assumption.
      intros ;apply P_id_a__sieve_bounded;assumption.
      intros ;apply P_id_cons_bounded;assumption.
      intros ;apply P_id_nats_bounded;assumption.
      intros ;apply P_id_mark_bounded;assumption.
      intros ;apply P_id_filter_bounded;assumption.
      intros ;apply P_id_zprimes_bounded;assumption.
      intros ;apply P_id_sieve_bounded;assumption.
      apply rules_monotonic.
    Qed.
    
    Definition P_id_A__ZPRIMES  := 0.
    
    Definition P_id_A__FILTER (x9:Z) (x10:Z) (x11:Z) := 0.
    
    Definition P_id_A__SIEVE (x9:Z) := 0.
    
    Definition P_id_MARK (x9:Z) := 2* x9.
    
    Definition P_id_A__NATS (x9:Z) := 1 + 2* x9.
    
    Lemma P_id_A__FILTER_monotonic :
     forall x12 x10 x14 x9 x13 x11, 
      (0 <= x14)/\ (x14 <= x13) ->
       (0 <= x12)/\ (x12 <= x11) ->
        (0 <= x10)/\ (x10 <= x9) ->
         P_id_A__FILTER x10 x12 x14 <= P_id_A__FILTER x9 x11 x13.
    Proof.
      intros x14 x13 x12 x11 x10 x9.
      intros [H_1 H_0].
      intros [H_3 H_2].
      intros [H_5 H_4].
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma P_id_A__SIEVE_monotonic :
     forall x10 x9, 
      (0 <= x10)/\ (x10 <= x9) ->P_id_A__SIEVE x10 <= P_id_A__SIEVE x9.
    Proof.
      intros x10 x9.
      intros [H_1 H_0].
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma P_id_MARK_monotonic :
     forall x10 x9, (0 <= x10)/\ (x10 <= x9) ->P_id_MARK x10 <= P_id_MARK x9.
    Proof.
      intros x10 x9.
      intros [H_1 H_0].
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma P_id_A__NATS_monotonic :
     forall x10 x9, 
      (0 <= x10)/\ (x10 <= x9) ->P_id_A__NATS x10 <= P_id_A__NATS x9.
    Proof.
      intros x10 x9.
      intros [H_1 H_0].
      
      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Definition marked_measure  := 
      InterpZ.marked_measure 0 P_id_a__filter P_id_a__nats P_id_s P_id_0 
       P_id_a__zprimes P_id_a__sieve P_id_cons P_id_nats P_id_mark 
       P_id_filter P_id_zprimes P_id_sieve P_id_A__ZPRIMES P_id_A__FILTER 
       P_id_A__SIEVE P_id_MARK P_id_A__NATS.
    
    Lemma marked_measure_equation :
     forall t, 
      marked_measure t = match t with
                           | (algebra.Alg.Term algebra.F.id_a__zprimes nil) =>
                            P_id_A__ZPRIMES 
                           | (algebra.Alg.Term algebra.F.id_a__filter (x11::
                              x10::x9::nil)) =>
                            P_id_A__FILTER (measure x11) (measure x10) 
                             (measure x9)
                           | (algebra.Alg.Term algebra.F.id_a__sieve 
                              (x9::nil)) =>
                            P_id_A__SIEVE (measure x9)
                           | (algebra.Alg.Term algebra.F.id_mark (x9::nil)) =>
                            P_id_MARK (measure x9)
                           | (algebra.Alg.Term algebra.F.id_a__nats 
                              (x9::nil)) =>
                            P_id_A__NATS (measure x9)
                           | _ => measure t
                           end.
    Proof.
      reflexivity .
    Qed.
    
    Lemma marked_measure_star_monotonic :
     forall f l1 l2, 
      (closure.refl_trans_clos (closure.one_step_list (algebra.EQT.one_step 
                                                        R_xml_0_deep_rew.R_xml_0_rules)
                                                       ) l1 l2) ->
       marked_measure (algebra.Alg.Term f l1) <= marked_measure (algebra.Alg.Term 
                                                                  f l2).
    Proof.
      unfold marked_measure in *.
      apply InterpZ.marked_measure_star_monotonic.
      intros ;apply P_id_a__filter_monotonic;assumption.
      intros ;apply P_id_a__nats_monotonic;assumption.
      intros ;apply P_id_s_monotonic;assumption.
      intros ;apply P_id_a__sieve_monotonic;assumption.
      intros ;apply P_id_cons_monotonic;assumption.
      intros ;apply P_id_nats_monotonic;assumption.
      intros ;apply P_id_mark_monotonic;assumption.
      intros ;apply P_id_filter_monotonic;assumption.
      intros ;apply P_id_sieve_monotonic;assumption.
      intros ;apply P_id_a__filter_bounded;assumption.
      intros ;apply P_id_a__nats_bounded;assumption.
      intros ;apply P_id_s_bounded;assumption.
      intros ;apply P_id_0_bounded;assumption.
      intros ;apply P_id_a__zprimes_bounded;assumption.
      intros ;apply P_id_a__sieve_bounded;assumption.
      intros ;apply P_id_cons_bounded;assumption.
      intros ;apply P_id_nats_bounded;assumption.
      intros ;apply P_id_mark_bounded;assumption.
      intros ;apply P_id_filter_bounded;assumption.
      intros ;apply P_id_zprimes_bounded;assumption.
      intros ;apply P_id_sieve_bounded;assumption.
      apply rules_monotonic.
      intros ;apply P_id_A__FILTER_monotonic;assumption.
      intros ;apply P_id_A__SIEVE_monotonic;assumption.
      intros ;apply P_id_MARK_monotonic;assumption.
      intros ;apply P_id_A__NATS_monotonic;assumption.
    Qed.
    
    Ltac rewrite_and_unfold  :=
     do 2 (rewrite marked_measure_equation);
      repeat (
      match goal with
        |  |- context [measure (algebra.Alg.Term ?f ?t)] =>
         rewrite (measure_equation (algebra.Alg.Term f t))
        | H:context [measure (algebra.Alg.Term ?f ?t)] |- _ =>
         rewrite (measure_equation (algebra.Alg.Term f t)) in H|-
        end
      ).
    
    Definition lt a b := (Zwf.Zwf 0) (marked_measure a) (marked_measure b).
    
    Definition le a b := marked_measure a <= marked_measure b.
    
    Lemma lt_le_compat : forall a b c, (lt a b) ->(le b c) ->lt a c.
    Proof.
      unfold lt, le in *.
      intros a b c.
      apply (interp.le_lt_compat_right (interp.o_Z 0)).
    Qed.
    
    Lemma wf_lt : well_founded lt.
    Proof.
      unfold lt in *.
      apply Inverse_Image.wf_inverse_image with  (B:=Z).
      apply Zwf.Zwf_well_founded.
    Qed.
    
    Lemma DP_R_xml_0_large_scc_1_strict_in_lt :
     Relation_Definitions.inclusion _ DP_R_xml_0_large_scc_1_strict lt.
    Proof.
      unfold Relation_Definitions.inclusion, lt in *.
      
      intros a b H;destruct H;
       match goal with
         |  |- (Zwf.Zwf 0) _ (marked_measure (algebra.Alg.Term ?f ?l)) =>
          let l'' := algebra.Alg_ext.find_replacement l  in 
           ((apply (interp.le_lt_compat_right (interp.o_Z 0)) with
              (marked_measure (algebra.Alg.Term f l''));[idtac|
             apply marked_measure_star_monotonic;
              repeat (apply algebra.EQT_ext.one_step_list_refl_trans_clos);
              (assumption)||(constructor 1)]))
         end
       ;clear ;rewrite_and_unfold ;repeat (generate_pos_hyp );
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Lemma DP_R_xml_0_large_scc_1_large_in_le :
     Relation_Definitions.inclusion _ DP_R_xml_0_large_scc_1_large le.
    Proof.
      unfold Relation_Definitions.inclusion, le, Zwf.Zwf in *.
      
      intros a b H;destruct H;
       match goal with
         |  |- _ <= marked_measure (algebra.Alg.Term ?f ?l) =>
          let l'' := algebra.Alg_ext.find_replacement l  in 
           ((apply (interp.le_trans (interp.o_Z 0)) with
              (marked_measure (algebra.Alg.Term f l''));[idtac|
             apply marked_measure_star_monotonic;
              repeat (apply algebra.EQT_ext.one_step_list_refl_trans_clos);
              (assumption)||(constructor 1)]))
         end
       ;clear ;rewrite_and_unfold ;repeat (generate_pos_hyp );
       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
    Qed.
    
    Definition wf_DP_R_xml_0_large_scc_1_large  := 
      WF_DP_R_xml_0_large_scc_1_large.wf.
    
    
    Lemma wf : well_founded WF_DP_R_xml_0_large.DP_R_xml_0_large_scc_1.
    Proof.
      intros x.
      apply (well_founded_ind wf_lt).
      clear x.
      intros x.
      pattern x.
      apply (@Acc_ind _ DP_R_xml_0_large_scc_1_large).
      clear x.
      intros x _ IHx IHx'.
      constructor.
      intros y H.
      
      destruct H;
       (apply IHx';apply DP_R_xml_0_large_scc_1_strict_in_lt;
         econstructor eassumption)||
       ((apply IHx;[econstructor eassumption|
         intros y' Hlt;apply IHx';apply lt_le_compat with (1:=Hlt) ;
          apply DP_R_xml_0_large_scc_1_large_in_le;econstructor eassumption])).
      apply wf_DP_R_xml_0_large_scc_1_large.
    Qed.
   End WF_DP_R_xml_0_large_scc_1.
   
   Definition wf_DP_R_xml_0_large_scc_1  := WF_DP_R_xml_0_large_scc_1.wf.
   
   
   Lemma acc_DP_R_xml_0_large_scc_1 :
    forall x y, 
     (DP_R_xml_0_large_scc_1 x y) ->Acc WF_DP_R_xml_0.DP_R_xml_0_large x.
   Proof.
     intros x.
     pattern x.
     apply (@Acc_ind _ DP_R_xml_0_large_scc_1).
     intros x' _ Hrec y h.
     
     inversion h;clear h;subst;
      constructor;intros _y _h;inversion _h;clear _h;subst;
       (eapply Hrec;econstructor eassumption)||
       ((R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 )||
        (eapply Hrec;
          econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))).
     apply wf_DP_R_xml_0_large_scc_1.
   Qed.
   
   
   Inductive DP_R_xml_0_large_non_scc_2  :
    algebra.Alg.term ->algebra.Alg.term ->Prop := 
      (* <a__zprimes,a__nats(s(s(0)))> *)
     | DP_R_xml_0_large_non_scc_2_0 :
      DP_R_xml_0_large_non_scc_2 (algebra.Alg.Term algebra.F.id_a__nats 
                                  ((algebra.Alg.Term algebra.F.id_s 
                                  ((algebra.Alg.Term algebra.F.id_s 
                                  ((algebra.Alg.Term algebra.F.id_0 
                                  nil)::nil))::nil))::nil)) 
       (algebra.Alg.Term algebra.F.id_a__zprimes nil)
   .
   
   
   Lemma acc_DP_R_xml_0_large_non_scc_2 :
    forall x y, 
     (DP_R_xml_0_large_non_scc_2 x y) ->Acc WF_DP_R_xml_0.DP_R_xml_0_large x.
   Proof.
     intros x y h.
     
     inversion h;clear h;subst;
      constructor;intros _y _h;inversion _h;clear _h;subst;
       (eapply acc_DP_R_xml_0_large_scc_1;
         econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
       ((R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 )||
        (eapply Hrec;
          econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))).
   Qed.
   
   
   Inductive DP_R_xml_0_large_non_scc_3  :
    algebra.Alg.term ->algebra.Alg.term ->Prop := 
      (* <a__sieve(cons(s(N_),Y_)),mark(N_)> *)
     | DP_R_xml_0_large_non_scc_3_0 :
      forall x4 x2 x9, 
       (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                  
         (algebra.Alg.Term algebra.F.id_cons ((algebra.Alg.Term 
          algebra.F.id_s (x4::nil))::x2::nil)) x9) ->
        DP_R_xml_0_large_non_scc_3 (algebra.Alg.Term algebra.F.id_mark 
                                    (x4::nil)) 
         (algebra.Alg.Term algebra.F.id_a__sieve (x9::nil))
   .
   
   
   Lemma acc_DP_R_xml_0_large_non_scc_3 :
    forall x y, 
     (DP_R_xml_0_large_non_scc_3 x y) ->Acc WF_DP_R_xml_0.DP_R_xml_0_large x.
   Proof.
     intros x y h.
     
     inversion h;clear h;subst;
      constructor;intros _y _h;inversion _h;clear _h;subst;
       (eapply acc_DP_R_xml_0_large_scc_1;
         econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
       ((R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 )||
        (eapply Hrec;
          econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))).
   Qed.
   
   
   Inductive DP_R_xml_0_large_non_scc_4  :
    algebra.Alg.term ->algebra.Alg.term ->Prop := 
      (* <a__zprimes,a__sieve(a__nats(s(s(0))))> *)
     | DP_R_xml_0_large_non_scc_4_0 :
      DP_R_xml_0_large_non_scc_4 (algebra.Alg.Term algebra.F.id_a__sieve 
                                  ((algebra.Alg.Term algebra.F.id_a__nats 
                                  ((algebra.Alg.Term algebra.F.id_s 
                                  ((algebra.Alg.Term algebra.F.id_s 
                                  ((algebra.Alg.Term algebra.F.id_0 
                                  nil)::nil))::nil))::nil))::nil)) 
       (algebra.Alg.Term algebra.F.id_a__zprimes nil)
   .
   
   
   Lemma acc_DP_R_xml_0_large_non_scc_4 :
    forall x y, 
     (DP_R_xml_0_large_non_scc_4 x y) ->Acc WF_DP_R_xml_0.DP_R_xml_0_large x.
   Proof.
     intros x y h.
     
     inversion h;clear h;subst;
      constructor;intros _y _h;inversion _h;clear _h;subst;
       (eapply acc_DP_R_xml_0_large_non_scc_3;
         econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
       ((R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 )||
        (eapply Hrec;
          econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))).
   Qed.
   
   
   Lemma wf : well_founded WF_DP_R_xml_0.DP_R_xml_0_large.
   Proof.
     constructor;intros _y _h;inversion _h;clear _h;subst;
      (eapply acc_DP_R_xml_0_large_non_scc_4;
        econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
      ((eapply acc_DP_R_xml_0_large_non_scc_3;
         econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
       ((eapply acc_DP_R_xml_0_large_non_scc_2;
          econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
        ((eapply acc_DP_R_xml_0_large_non_scc_1;
           econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
         ((eapply acc_DP_R_xml_0_large_non_scc_0;
            econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
          ((eapply acc_DP_R_xml_0_large_scc_1;
             econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
           ((eapply acc_DP_R_xml_0_large_scc_0;
              econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
            ((R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 )||(fail)))))))).
   Qed.
  End WF_DP_R_xml_0_large.
  
  Open Scope Z_scope.
  
  Import ring_extention.
  
  Notation Local "a <= b" := (Zle a b).
  
  Notation Local "a < b" := (Zlt a b).
  
  Definition P_id_a__filter (x9:Z) (x10:Z) (x11:Z) := 
    2 + 1* x9 + 1* x10 + 1* x11.
  
  Definition P_id_a__nats (x9:Z) := 2* x9.
  
  Definition P_id_s (x9:Z) := 2* x9.
  
  Definition P_id_0  := 0.
  
  Definition P_id_a__zprimes  := 2.
  
  Definition P_id_a__sieve (x9:Z) := 2 + 2* x9.
  
  Definition P_id_cons (x9:Z) (x10:Z) := 2* x9.
  
  Definition P_id_nats (x9:Z) := 2* x9.
  
  Definition P_id_mark (x9:Z) := 1* x9.
  
  Definition P_id_filter (x9:Z) (x10:Z) (x11:Z) := 
    2 + 1* x9 + 1* x10 + 1* x11.
  
  Definition P_id_zprimes  := 2.
  
  Definition P_id_sieve (x9:Z) := 2 + 2* x9.
  
  Lemma P_id_a__filter_monotonic :
   forall x12 x10 x14 x9 x13 x11, 
    (0 <= x14)/\ (x14 <= x13) ->
     (0 <= x12)/\ (x12 <= x11) ->
      (0 <= x10)/\ (x10 <= x9) ->
       P_id_a__filter x10 x12 x14 <= P_id_a__filter x9 x11 x13.
  Proof.
    intros x14 x13 x12 x11 x10 x9.
    intros [H_1 H_0].
    intros [H_3 H_2].
    intros [H_5 H_4].
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma P_id_a__nats_monotonic :
   forall x10 x9, 
    (0 <= x10)/\ (x10 <= x9) ->P_id_a__nats x10 <= P_id_a__nats x9.
  Proof.
    intros x10 x9.
    intros [H_1 H_0].
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma P_id_s_monotonic :
   forall x10 x9, (0 <= x10)/\ (x10 <= x9) ->P_id_s x10 <= P_id_s x9.
  Proof.
    intros x10 x9.
    intros [H_1 H_0].
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma P_id_a__sieve_monotonic :
   forall x10 x9, 
    (0 <= x10)/\ (x10 <= x9) ->P_id_a__sieve x10 <= P_id_a__sieve x9.
  Proof.
    intros x10 x9.
    intros [H_1 H_0].
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma P_id_cons_monotonic :
   forall x12 x10 x9 x11, 
    (0 <= x12)/\ (x12 <= x11) ->
     (0 <= x10)/\ (x10 <= x9) ->P_id_cons x10 x12 <= P_id_cons x9 x11.
  Proof.
    intros x12 x11 x10 x9.
    intros [H_1 H_0].
    intros [H_3 H_2].
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma P_id_nats_monotonic :
   forall x10 x9, (0 <= x10)/\ (x10 <= x9) ->P_id_nats x10 <= P_id_nats x9.
  Proof.
    intros x10 x9.
    intros [H_1 H_0].
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma P_id_mark_monotonic :
   forall x10 x9, (0 <= x10)/\ (x10 <= x9) ->P_id_mark x10 <= P_id_mark x9.
  Proof.
    intros x10 x9.
    intros [H_1 H_0].
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma P_id_filter_monotonic :
   forall x12 x10 x14 x9 x13 x11, 
    (0 <= x14)/\ (x14 <= x13) ->
     (0 <= x12)/\ (x12 <= x11) ->
      (0 <= x10)/\ (x10 <= x9) ->
       P_id_filter x10 x12 x14 <= P_id_filter x9 x11 x13.
  Proof.
    intros x14 x13 x12 x11 x10 x9.
    intros [H_1 H_0].
    intros [H_3 H_2].
    intros [H_5 H_4].
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma P_id_sieve_monotonic :
   forall x10 x9, (0 <= x10)/\ (x10 <= x9) ->P_id_sieve x10 <= P_id_sieve x9.
  Proof.
    intros x10 x9.
    intros [H_1 H_0].
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma P_id_a__filter_bounded :
   forall x10 x9 x11, 
    (0 <= x9) ->(0 <= x10) ->(0 <= x11) ->0 <= P_id_a__filter x11 x10 x9.
  Proof.
    intros .
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma P_id_a__nats_bounded : forall x9, (0 <= x9) ->0 <= P_id_a__nats x9.
  Proof.
    intros .
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma P_id_s_bounded : forall x9, (0 <= x9) ->0 <= P_id_s x9.
  Proof.
    intros .
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma P_id_0_bounded : 0 <= P_id_0 .
  Proof.
    intros .
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma P_id_a__zprimes_bounded : 0 <= P_id_a__zprimes .
  Proof.
    intros .
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma P_id_a__sieve_bounded : forall x9, (0 <= x9) ->0 <= P_id_a__sieve x9.
  Proof.
    intros .
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma P_id_cons_bounded :
   forall x10 x9, (0 <= x9) ->(0 <= x10) ->0 <= P_id_cons x10 x9.
  Proof.
    intros .
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma P_id_nats_bounded : forall x9, (0 <= x9) ->0 <= P_id_nats x9.
  Proof.
    intros .
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma P_id_mark_bounded : forall x9, (0 <= x9) ->0 <= P_id_mark x9.
  Proof.
    intros .
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma P_id_filter_bounded :
   forall x10 x9 x11, 
    (0 <= x9) ->(0 <= x10) ->(0 <= x11) ->0 <= P_id_filter x11 x10 x9.
  Proof.
    intros .
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma P_id_zprimes_bounded : 0 <= P_id_zprimes .
  Proof.
    intros .
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma P_id_sieve_bounded : forall x9, (0 <= x9) ->0 <= P_id_sieve x9.
  Proof.
    intros .
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Definition measure  := 
    InterpZ.measure 0 P_id_a__filter P_id_a__nats P_id_s P_id_0 
     P_id_a__zprimes P_id_a__sieve P_id_cons P_id_nats P_id_mark P_id_filter 
     P_id_zprimes P_id_sieve.
  
  Lemma measure_equation :
   forall t, 
    measure t = match t with
                  | (algebra.Alg.Term algebra.F.id_a__filter (x11::x10::
                     x9::nil)) =>
                   P_id_a__filter (measure x11) (measure x10) (measure x9)
                  | (algebra.Alg.Term algebra.F.id_a__nats (x9::nil)) =>
                   P_id_a__nats (measure x9)
                  | (algebra.Alg.Term algebra.F.id_s (x9::nil)) =>
                   P_id_s (measure x9)
                  | (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0 
                  | (algebra.Alg.Term algebra.F.id_a__zprimes nil) =>
                   P_id_a__zprimes 
                  | (algebra.Alg.Term algebra.F.id_a__sieve (x9::nil)) =>
                   P_id_a__sieve (measure x9)
                  | (algebra.Alg.Term algebra.F.id_cons (x10::x9::nil)) =>
                   P_id_cons (measure x10) (measure x9)
                  | (algebra.Alg.Term algebra.F.id_nats (x9::nil)) =>
                   P_id_nats (measure x9)
                  | (algebra.Alg.Term algebra.F.id_mark (x9::nil)) =>
                   P_id_mark (measure x9)
                  | (algebra.Alg.Term algebra.F.id_filter (x11::x10::
                     x9::nil)) =>
                   P_id_filter (measure x11) (measure x10) (measure x9)
                  | (algebra.Alg.Term algebra.F.id_zprimes nil) =>
                   P_id_zprimes 
                  | (algebra.Alg.Term algebra.F.id_sieve (x9::nil)) =>
                   P_id_sieve (measure x9)
                  | _ => 0
                  end.
  Proof.
    intros t;case t;intros ;apply refl_equal.
  Qed.
  
  Lemma measure_bounded : forall t, 0 <= measure t.
  Proof.
    unfold measure in |-*.
    
    apply InterpZ.measure_bounded;
     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Ltac generate_pos_hyp  :=
   match goal with
     | H:context [measure ?x] |- _ =>
      let v := fresh "v" in 
       (let H := fresh "h" in 
         (set (H:=measure_bounded x) in *;set (v:=measure x) in *;
           clearbody H;clearbody v))
     |  |- context [measure ?x] =>
      let v := fresh "v" in 
       (let H := fresh "h" in 
         (set (H:=measure_bounded x) in *;set (v:=measure x) in *;
           clearbody H;clearbody v))
     end
   .
  
  Lemma rules_monotonic :
   forall l r, 
    (algebra.EQT.axiom R_xml_0_deep_rew.R_xml_0_rules r l) ->
     measure r <= measure l.
  Proof.
    intros l r H.
    fold measure in |-*.
    
    inversion H;clear H;subst;inversion H0;clear H0;subst;
     simpl algebra.EQT.T.apply_subst in |-*;
     repeat (
     match goal with
       |  |- context [measure (algebra.Alg.Term ?f ?t)] =>
        rewrite (measure_equation (algebra.Alg.Term f t))
       end
     );repeat (generate_pos_hyp );
     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma measure_star_monotonic :
   forall l r, 
    (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                               r l) ->measure r <= measure l.
  Proof.
    unfold measure in *.
    apply InterpZ.measure_star_monotonic.
    intros ;apply P_id_a__filter_monotonic;assumption.
    intros ;apply P_id_a__nats_monotonic;assumption.
    intros ;apply P_id_s_monotonic;assumption.
    intros ;apply P_id_a__sieve_monotonic;assumption.
    intros ;apply P_id_cons_monotonic;assumption.
    intros ;apply P_id_nats_monotonic;assumption.
    intros ;apply P_id_mark_monotonic;assumption.
    intros ;apply P_id_filter_monotonic;assumption.
    intros ;apply P_id_sieve_monotonic;assumption.
    intros ;apply P_id_a__filter_bounded;assumption.
    intros ;apply P_id_a__nats_bounded;assumption.
    intros ;apply P_id_s_bounded;assumption.
    intros ;apply P_id_0_bounded;assumption.
    intros ;apply P_id_a__zprimes_bounded;assumption.
    intros ;apply P_id_a__sieve_bounded;assumption.
    intros ;apply P_id_cons_bounded;assumption.
    intros ;apply P_id_nats_bounded;assumption.
    intros ;apply P_id_mark_bounded;assumption.
    intros ;apply P_id_filter_bounded;assumption.
    intros ;apply P_id_zprimes_bounded;assumption.
    intros ;apply P_id_sieve_bounded;assumption.
    apply rules_monotonic.
  Qed.
  
  Definition P_id_A__ZPRIMES  := 0.
  
  Definition P_id_A__FILTER (x9:Z) (x10:Z) (x11:Z) := 3 + 1* x9.
  
  Definition P_id_A__SIEVE (x9:Z) := 1* x9.
  
  Definition P_id_MARK (x9:Z) := 2* x9.
  
  Definition P_id_A__NATS (x9:Z) := 2* x9.
  
  Lemma P_id_A__FILTER_monotonic :
   forall x12 x10 x14 x9 x13 x11, 
    (0 <= x14)/\ (x14 <= x13) ->
     (0 <= x12)/\ (x12 <= x11) ->
      (0 <= x10)/\ (x10 <= x9) ->
       P_id_A__FILTER x10 x12 x14 <= P_id_A__FILTER x9 x11 x13.
  Proof.
    intros x14 x13 x12 x11 x10 x9.
    intros [H_1 H_0].
    intros [H_3 H_2].
    intros [H_5 H_4].
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma P_id_A__SIEVE_monotonic :
   forall x10 x9, 
    (0 <= x10)/\ (x10 <= x9) ->P_id_A__SIEVE x10 <= P_id_A__SIEVE x9.
  Proof.
    intros x10 x9.
    intros [H_1 H_0].
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma P_id_MARK_monotonic :
   forall x10 x9, (0 <= x10)/\ (x10 <= x9) ->P_id_MARK x10 <= P_id_MARK x9.
  Proof.
    intros x10 x9.
    intros [H_1 H_0].
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma P_id_A__NATS_monotonic :
   forall x10 x9, 
    (0 <= x10)/\ (x10 <= x9) ->P_id_A__NATS x10 <= P_id_A__NATS x9.
  Proof.
    intros x10 x9.
    intros [H_1 H_0].
    
    cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
     (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Definition marked_measure  := 
    InterpZ.marked_measure 0 P_id_a__filter P_id_a__nats P_id_s P_id_0 
     P_id_a__zprimes P_id_a__sieve P_id_cons P_id_nats P_id_mark P_id_filter 
     P_id_zprimes P_id_sieve P_id_A__ZPRIMES P_id_A__FILTER P_id_A__SIEVE 
     P_id_MARK P_id_A__NATS.
  
  Lemma marked_measure_equation :
   forall t, 
    marked_measure t = match t with
                         | (algebra.Alg.Term algebra.F.id_a__zprimes nil) =>
                          P_id_A__ZPRIMES 
                         | (algebra.Alg.Term algebra.F.id_a__filter (x11::
                            x10::x9::nil)) =>
                          P_id_A__FILTER (measure x11) (measure x10) 
                           (measure x9)
                         | (algebra.Alg.Term algebra.F.id_a__sieve (x9::nil)) =>
                          P_id_A__SIEVE (measure x9)
                         | (algebra.Alg.Term algebra.F.id_mark (x9::nil)) =>
                          P_id_MARK (measure x9)
                         | (algebra.Alg.Term algebra.F.id_a__nats (x9::nil)) =>
                          P_id_A__NATS (measure x9)
                         | _ => measure t
                         end.
  Proof.
    reflexivity .
  Qed.
  
  Lemma marked_measure_star_monotonic :
   forall f l1 l2, 
    (closure.refl_trans_clos (closure.one_step_list (algebra.EQT.one_step 
                                                      R_xml_0_deep_rew.R_xml_0_rules)
                                                     ) l1 l2) ->
     marked_measure (algebra.Alg.Term f l1) <= marked_measure (algebra.Alg.Term 
                                                                f l2).
  Proof.
    unfold marked_measure in *.
    apply InterpZ.marked_measure_star_monotonic.
    intros ;apply P_id_a__filter_monotonic;assumption.
    intros ;apply P_id_a__nats_monotonic;assumption.
    intros ;apply P_id_s_monotonic;assumption.
    intros ;apply P_id_a__sieve_monotonic;assumption.
    intros ;apply P_id_cons_monotonic;assumption.
    intros ;apply P_id_nats_monotonic;assumption.
    intros ;apply P_id_mark_monotonic;assumption.
    intros ;apply P_id_filter_monotonic;assumption.
    intros ;apply P_id_sieve_monotonic;assumption.
    intros ;apply P_id_a__filter_bounded;assumption.
    intros ;apply P_id_a__nats_bounded;assumption.
    intros ;apply P_id_s_bounded;assumption.
    intros ;apply P_id_0_bounded;assumption.
    intros ;apply P_id_a__zprimes_bounded;assumption.
    intros ;apply P_id_a__sieve_bounded;assumption.
    intros ;apply P_id_cons_bounded;assumption.
    intros ;apply P_id_nats_bounded;assumption.
    intros ;apply P_id_mark_bounded;assumption.
    intros ;apply P_id_filter_bounded;assumption.
    intros ;apply P_id_zprimes_bounded;assumption.
    intros ;apply P_id_sieve_bounded;assumption.
    apply rules_monotonic.
    intros ;apply P_id_A__FILTER_monotonic;assumption.
    intros ;apply P_id_A__SIEVE_monotonic;assumption.
    intros ;apply P_id_MARK_monotonic;assumption.
    intros ;apply P_id_A__NATS_monotonic;assumption.
  Qed.
  
  Ltac rewrite_and_unfold  :=
   do 2 (rewrite marked_measure_equation);
    repeat (
    match goal with
      |  |- context [measure (algebra.Alg.Term ?f ?t)] =>
       rewrite (measure_equation (algebra.Alg.Term f t))
      | H:context [measure (algebra.Alg.Term ?f ?t)] |- _ =>
       rewrite (measure_equation (algebra.Alg.Term f t)) in H|-
      end
    ).
  
  Definition lt a b := (Zwf.Zwf 0) (marked_measure a) (marked_measure b).
  
  Definition le a b := marked_measure a <= marked_measure b.
  
  Lemma lt_le_compat : forall a b c, (lt a b) ->(le b c) ->lt a c.
  Proof.
    unfold lt, le in *.
    intros a b c.
    apply (interp.le_lt_compat_right (interp.o_Z 0)).
  Qed.
  
  Lemma wf_lt : well_founded lt.
  Proof.
    unfold lt in *.
    apply Inverse_Image.wf_inverse_image with  (B:=Z).
    apply Zwf.Zwf_well_founded.
  Qed.
  
  Lemma DP_R_xml_0_strict_in_lt :
   Relation_Definitions.inclusion _ DP_R_xml_0_strict lt.
  Proof.
    unfold Relation_Definitions.inclusion, lt in *.
    
    intros a b H;destruct H;
     match goal with
       |  |- (Zwf.Zwf 0) _ (marked_measure (algebra.Alg.Term ?f ?l)) =>
        let l'' := algebra.Alg_ext.find_replacement l  in 
         ((apply (interp.le_lt_compat_right (interp.o_Z 0)) with
            (marked_measure (algebra.Alg.Term f l''));[idtac|
           apply marked_measure_star_monotonic;
            repeat (apply algebra.EQT_ext.one_step_list_refl_trans_clos);
            (assumption)||(constructor 1)]))
       end
     ;clear ;rewrite_and_unfold ;repeat (generate_pos_hyp );
     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Lemma DP_R_xml_0_large_in_le :
   Relation_Definitions.inclusion _ DP_R_xml_0_large le.
  Proof.
    unfold Relation_Definitions.inclusion, le, Zwf.Zwf in *.
    
    intros a b H;destruct H;
     match goal with
       |  |- _ <= marked_measure (algebra.Alg.Term ?f ?l) =>
        let l'' := algebra.Alg_ext.find_replacement l  in 
         ((apply (interp.le_trans (interp.o_Z 0)) with
            (marked_measure (algebra.Alg.Term f l''));[idtac|
           apply marked_measure_star_monotonic;
            repeat (apply algebra.EQT_ext.one_step_list_refl_trans_clos);
            (assumption)||(constructor 1)]))
       end
     ;clear ;rewrite_and_unfold ;repeat (generate_pos_hyp );
     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  Qed.
  
  Definition wf_DP_R_xml_0_large  := WF_DP_R_xml_0_large.wf.
  
  
  Lemma wf : well_founded WF_R_xml_0_deep_rew.DP_R_xml_0.
  Proof.
    intros x.
    apply (well_founded_ind wf_lt).
    clear x.
    intros x.
    pattern x.
    apply (@Acc_ind _ DP_R_xml_0_large).
    clear x.
    intros x _ IHx IHx'.
    constructor.
    intros y H.
    
    destruct H;
     (apply IHx';apply DP_R_xml_0_strict_in_lt;econstructor eassumption)||
     ((apply IHx;[econstructor eassumption|
       intros y' Hlt;apply IHx';apply lt_le_compat with (1:=Hlt) ;
        apply DP_R_xml_0_large_in_le;econstructor eassumption])).
    apply wf_DP_R_xml_0_large.
  Qed.
 End WF_DP_R_xml_0.
 
 Definition wf_H  := WF_DP_R_xml_0.wf.
 
 Lemma wf :
  well_founded (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules).
 Proof.
   apply ddp.dp_criterion.
   apply R_xml_0_deep_rew.R_xml_0_non_var.
   apply R_xml_0_deep_rew.R_xml_0_reg.
   
   intros ;
    apply (ddp.constructor_defined_dec _ _ 
            R_xml_0_deep_rew.R_xml_0_rules_included).
   refine (Inclusion.wf_incl _ _ _ _ wf_H).
   intros x y H.
   destruct (R_xml_0_dp_step_spec H) as [f [l1 [l2 [H1 [H2 H3]]]]].
   
   destruct (ddp.dp_list_complete _ _ 
              R_xml_0_deep_rew.R_xml_0_rules_included _ _ H3)
    as [x' [y' [sigma [h1 [h2 h3]]]]].
   clear H3.
   subst.
   vm_compute in h3|-.
   let e := type of h3 in (dp_concl_tac h2 h3 ltac:(fun _ => idtac) e).
 Qed.
End WF_R_xml_0_deep_rew.


(* 
*** Local Variables: ***
*** coq-prog-name: "coqtop" ***
*** coq-prog-args: ("-emacs-U" "-I" "$COCCINELLE/examples" "-I" "$COCCINELLE/term_algebra" "-I" "$COCCINELLE/term_orderings" "-I" "$COCCINELLE/basis" "-I" "$COCCINELLE/list_extensions" "-I" "$COCCINELLE/examples/cime_trace/") ***
*** compile-command: "coqc -I $COCCINELLE/term_algebra -I $COCCINELLE/term_orderings -I $COCCINELLE/basis -I $COCCINELLE/list_extensions -I $COCCINELLE/examples/cime_trace/ -I $COCCINELLE/examples/  c_output/strat/tpdb-5.0___TRS___TRCSR___Ex9_BLR02_GM.trs/a3pat.v" ***
*** End: ***
 *)