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_prime *)
    | id_prime : symb
     (* id_divp *)
    | id_divp : symb
     (* id_prime1 *)
    | id_prime1 : symb
     (* id_false *)
    | id_false : symb
     (* id_rem *)
    | id_rem : symb
     (* id_and *)
    | id_and : symb
     (* id_0 *)
    | id_0 : symb
     (* id__equal_ *)
    | id__equal_ : symb
     (* id_true *)
    | id_true : symb
     (* id_s *)
    | id_s : symb
     (* id_not *)
    | id_not : symb
  .
  
  
  Definition symb_eq_bool (f1 f2:symb) : bool := 
    match f1,f2 with
      | id_prime,id_prime => true
      | id_divp,id_divp => true
      | id_prime1,id_prime1 => true
      | id_false,id_false => true
      | id_rem,id_rem => true
      | id_and,id_and => true
      | id_0,id_0 => true
      | id__equal_,id__equal_ => true
      | id_true,id_true => true
      | id_s,id_s => true
      | id_not,id_not => 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_prime,id_prime => refl_equal _
             | id_divp,id_divp => refl_equal _
             | id_prime1,id_prime1 => refl_equal _
             | id_false,id_false => refl_equal _
             | id_rem,id_rem => refl_equal _
             | id_and,id_and => refl_equal _
             | id_0,id_0 => refl_equal _
             | id__equal_,id__equal_ => refl_equal _
             | id_true,id_true => refl_equal _
             | id_s,id_s => refl_equal _
             | id_not,id_not => refl_equal _
             | _,_ => _
             end;intros abs;discriminate.
  Defined.
  
  
  Definition arity (f:symb) := 
    match f with
      | id_prime => term.Free 1
      | id_divp => term.Free 2
      | id_prime1 => term.Free 2
      | id_false => term.Free 0
      | id_rem => term.Free 2
      | id_and => term.Free 2
      | id_0 => term.Free 0
      | id__equal_ => term.Free 2
      | id_true => term.Free 0
      | id_s => term.Free 1
      | id_not => term.Free 1
      end.
  
  
  Definition symb_order (f1 f2:symb) : bool := 
    match f1,f2 with
      | id_prime,id_prime => true
      | id_prime,id_divp => false
      | id_prime,id_prime1 => false
      | id_prime,id_false => false
      | id_prime,id_rem => false
      | id_prime,id_and => false
      | id_prime,id_0 => false
      | id_prime,id__equal_ => false
      | id_prime,id_true => false
      | id_prime,id_s => false
      | id_prime,id_not => false
      | id_divp,id_prime => true
      | id_divp,id_divp => true
      | id_divp,id_prime1 => false
      | id_divp,id_false => false
      | id_divp,id_rem => false
      | id_divp,id_and => false
      | id_divp,id_0 => false
      | id_divp,id__equal_ => false
      | id_divp,id_true => false
      | id_divp,id_s => false
      | id_divp,id_not => false
      | id_prime1,id_prime => true
      | id_prime1,id_divp => true
      | id_prime1,id_prime1 => true
      | id_prime1,id_false => false
      | id_prime1,id_rem => false
      | id_prime1,id_and => false
      | id_prime1,id_0 => false
      | id_prime1,id__equal_ => false
      | id_prime1,id_true => false
      | id_prime1,id_s => false
      | id_prime1,id_not => false
      | id_false,id_prime => true
      | id_false,id_divp => true
      | id_false,id_prime1 => true
      | id_false,id_false => true
      | id_false,id_rem => false
      | id_false,id_and => false
      | id_false,id_0 => false
      | id_false,id__equal_ => false
      | id_false,id_true => false
      | id_false,id_s => false
      | id_false,id_not => false
      | id_rem,id_prime => true
      | id_rem,id_divp => true
      | id_rem,id_prime1 => true
      | id_rem,id_false => true
      | id_rem,id_rem => true
      | id_rem,id_and => false
      | id_rem,id_0 => false
      | id_rem,id__equal_ => false
      | id_rem,id_true => false
      | id_rem,id_s => false
      | id_rem,id_not => false
      | id_and,id_prime => true
      | id_and,id_divp => true
      | id_and,id_prime1 => true
      | id_and,id_false => true
      | id_and,id_rem => true
      | id_and,id_and => true
      | id_and,id_0 => false
      | id_and,id__equal_ => false
      | id_and,id_true => false
      | id_and,id_s => false
      | id_and,id_not => false
      | id_0,id_prime => true
      | id_0,id_divp => true
      | id_0,id_prime1 => true
      | id_0,id_false => true
      | id_0,id_rem => true
      | id_0,id_and => true
      | id_0,id_0 => true
      | id_0,id__equal_ => false
      | id_0,id_true => false
      | id_0,id_s => false
      | id_0,id_not => false
      | id__equal_,id_prime => true
      | id__equal_,id_divp => true
      | id__equal_,id_prime1 => true
      | id__equal_,id_false => true
      | id__equal_,id_rem => true
      | id__equal_,id_and => true
      | id__equal_,id_0 => true
      | id__equal_,id__equal_ => true
      | id__equal_,id_true => false
      | id__equal_,id_s => false
      | id__equal_,id_not => false
      | id_true,id_prime => true
      | id_true,id_divp => true
      | id_true,id_prime1 => true
      | id_true,id_false => true
      | id_true,id_rem => true
      | id_true,id_and => true
      | id_true,id_0 => true
      | id_true,id__equal_ => true
      | id_true,id_true => true
      | id_true,id_s => false
      | id_true,id_not => false
      | id_s,id_prime => true
      | id_s,id_divp => true
      | id_s,id_prime1 => true
      | id_s,id_false => true
      | id_s,id_rem => true
      | id_s,id_and => true
      | id_s,id_0 => true
      | id_s,id__equal_ => true
      | id_s,id_true => true
      | id_s,id_s => true
      | id_s,id_not => false
      | id_not,id_prime => true
      | id_not,id_divp => true
      | id_not,id_prime1 => true
      | id_not,id_false => true
      | id_not,id_rem => true
      | id_not,id_and => true
      | id_not,id_0 => true
      | id_not,id__equal_ => true
      | id_not,id_true => true
      | id_not,id_s => true
      | id_not,id_not => 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 := 
    (* prime(0) -> false *)
   | R_xml_0_rule_0 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_false nil) 
     (algebra.Alg.Term algebra.F.id_prime ((algebra.Alg.Term algebra.F.id_0 
      nil)::nil))
    (* prime(s(0)) -> false *)
   | R_xml_0_rule_1 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_false nil) 
     (algebra.Alg.Term algebra.F.id_prime ((algebra.Alg.Term algebra.F.id_s 
      ((algebra.Alg.Term algebra.F.id_0 nil)::nil))::nil))
    (* prime(s(s(x_))) -> prime1(s(s(x_)),s(x_)) *)
   | R_xml_0_rule_2 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_prime1 ((algebra.Alg.Term 
                   algebra.F.id_s ((algebra.Alg.Term algebra.F.id_s 
                   ((algebra.Alg.Var 1)::nil))::nil))::(algebra.Alg.Term 
                   algebra.F.id_s ((algebra.Alg.Var 1)::nil))::nil)) 
     (algebra.Alg.Term algebra.F.id_prime ((algebra.Alg.Term algebra.F.id_s 
      ((algebra.Alg.Term algebra.F.id_s 
      ((algebra.Alg.Var 1)::nil))::nil))::nil))
    (* prime1(x_,0) -> false *)
   | R_xml_0_rule_3 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_false nil) 
     (algebra.Alg.Term algebra.F.id_prime1 ((algebra.Alg.Var 1)::
      (algebra.Alg.Term algebra.F.id_0 nil)::nil))
    (* prime1(x_,s(0)) -> true *)
   | R_xml_0_rule_4 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_true nil) 
     (algebra.Alg.Term algebra.F.id_prime1 ((algebra.Alg.Var 1)::
      (algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Term algebra.F.id_0 
      nil)::nil))::nil))
   
    (* prime1(x_,s(s(y_))) -> and(not(divp(s(s(y_)),x_)),prime1(x_,s(y_))) *)
   | R_xml_0_rule_5 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_and ((algebra.Alg.Term 
                   algebra.F.id_not ((algebra.Alg.Term algebra.F.id_divp 
                   ((algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Term 
                   algebra.F.id_s ((algebra.Alg.Var 2)::nil))::nil))::
                   (algebra.Alg.Var 1)::nil))::nil))::(algebra.Alg.Term 
                   algebra.F.id_prime1 ((algebra.Alg.Var 1)::
                   (algebra.Alg.Term algebra.F.id_s 
                   ((algebra.Alg.Var 2)::nil))::nil))::nil)) 
     (algebra.Alg.Term algebra.F.id_prime1 ((algebra.Alg.Var 1)::
      (algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Term algebra.F.id_s 
      ((algebra.Alg.Var 2)::nil))::nil))::nil))
    (* divp(x_,y_) -> =(rem(x_,y_),0) *)
   | R_xml_0_rule_6 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id__equal_ ((algebra.Alg.Term 
                   algebra.F.id_rem ((algebra.Alg.Var 1)::
                   (algebra.Alg.Var 2)::nil))::(algebra.Alg.Term 
                   algebra.F.id_0 nil)::nil)) 
     (algebra.Alg.Term algebra.F.id_divp ((algebra.Alg.Var 1)::
      (algebra.Alg.Var 2)::nil))
 .
 
 
 Definition R_xml_0_rule_as_list_0  := 
   ((algebra.Alg.Term algebra.F.id_prime ((algebra.Alg.Term algebra.F.id_0 
     nil)::nil)),(algebra.Alg.Term algebra.F.id_false nil))::nil.
 
 
 Definition R_xml_0_rule_as_list_1  := 
   ((algebra.Alg.Term algebra.F.id_prime ((algebra.Alg.Term algebra.F.id_s 
     ((algebra.Alg.Term algebra.F.id_0 nil)::nil))::nil)),
    (algebra.Alg.Term algebra.F.id_false nil))::R_xml_0_rule_as_list_0.
 
 
 Definition R_xml_0_rule_as_list_2  := 
   ((algebra.Alg.Term algebra.F.id_prime ((algebra.Alg.Term algebra.F.id_s 
     ((algebra.Alg.Term algebra.F.id_s 
     ((algebra.Alg.Var 1)::nil))::nil))::nil)),
    (algebra.Alg.Term algebra.F.id_prime1 ((algebra.Alg.Term algebra.F.id_s 
     ((algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Var 1)::nil))::nil))::
     (algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Var 1)::nil))::nil)))::
    R_xml_0_rule_as_list_1.
 
 
 Definition R_xml_0_rule_as_list_3  := 
   ((algebra.Alg.Term algebra.F.id_prime1 ((algebra.Alg.Var 1)::
     (algebra.Alg.Term algebra.F.id_0 nil)::nil)),
    (algebra.Alg.Term algebra.F.id_false nil))::R_xml_0_rule_as_list_2.
 
 
 Definition R_xml_0_rule_as_list_4  := 
   ((algebra.Alg.Term algebra.F.id_prime1 ((algebra.Alg.Var 1)::
     (algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Term algebra.F.id_0 
     nil)::nil))::nil)),(algebra.Alg.Term algebra.F.id_true nil))::
    R_xml_0_rule_as_list_3.
 
 
 Definition R_xml_0_rule_as_list_5  := 
   ((algebra.Alg.Term algebra.F.id_prime1 ((algebra.Alg.Var 1)::
     (algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Term algebra.F.id_s 
     ((algebra.Alg.Var 2)::nil))::nil))::nil)),
    (algebra.Alg.Term algebra.F.id_and ((algebra.Alg.Term algebra.F.id_not 
     ((algebra.Alg.Term algebra.F.id_divp ((algebra.Alg.Term algebra.F.id_s 
     ((algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Var 2)::nil))::nil))::
     (algebra.Alg.Var 1)::nil))::nil))::(algebra.Alg.Term 
     algebra.F.id_prime1 ((algebra.Alg.Var 1)::(algebra.Alg.Term 
     algebra.F.id_s ((algebra.Alg.Var 2)::nil))::nil))::nil)))::
    R_xml_0_rule_as_list_4.
 
 
 Definition R_xml_0_rule_as_list_6  := 
   ((algebra.Alg.Term algebra.F.id_divp ((algebra.Alg.Var 1)::
     (algebra.Alg.Var 2)::nil)),
    (algebra.Alg.Term algebra.F.id__equal_ ((algebra.Alg.Term 
     algebra.F.id_rem ((algebra.Alg.Var 1)::(algebra.Alg.Var 2)::nil))::
     (algebra.Alg.Term algebra.F.id_0 nil)::nil)))::R_xml_0_rule_as_list_5.
 
 Definition R_xml_0_rule_as_list  := R_xml_0_rule_as_list_6.
 
 
 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.or8_equiv in H|-.
   case H;clear H;intros H.
   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_8 (x4 x5 x6 x7 x8 x9 x10 x11:Prop) :
  Prop := 
   | conj_8 :
    x4->x5->x6->x7->x8->x9->x10->x11->and_8 x4 x5 x6 x7 x8 x9 x10 x11
 .
 
 
 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_8 (t = (algebra.Alg.Term algebra.F.id_false nil) ->
           t' = (algebra.Alg.Term algebra.F.id_false nil)) 
     (forall x5 x7, 
      t = (algebra.Alg.Term algebra.F.id_rem (x5::x7::nil)) ->
       exists x4,
         exists x6,
           t' = (algebra.Alg.Term algebra.F.id_rem (x4::x6::nil))/\ 
           (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
             x4 x5)/\ 
           (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
             x6 x7)) 
     (forall x5 x7, 
      t = (algebra.Alg.Term algebra.F.id_and (x5::x7::nil)) ->
       exists x4,
         exists x6,
           t' = (algebra.Alg.Term algebra.F.id_and (x4::x6::nil))/\ 
           (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
             x4 x5)/\ 
           (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
             x6 x7)) 
     (t = (algebra.Alg.Term algebra.F.id_0 nil) ->
      t' = (algebra.Alg.Term algebra.F.id_0 nil)) 
     (forall x5 x7, 
      t = (algebra.Alg.Term algebra.F.id__equal_ (x5::x7::nil)) ->
       exists x4,
         exists x6,
           t' = (algebra.Alg.Term algebra.F.id__equal_ (x4::x6::nil))/\ 
           (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
             x4 x5)/\ 
           (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) 
             x6 x7)) 
     (t = (algebra.Alg.Term algebra.F.id_true nil) ->
      t' = (algebra.Alg.Term algebra.F.id_true nil)) 
     (forall x5, 
      t = (algebra.Alg.Term algebra.F.id_s (x5::nil)) ->
       exists x4,
         t' = (algebra.Alg.Term algebra.F.id_s (x4::nil))/\ 
         (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x4 x5)) 
     
     (forall x5, 
      t = (algebra.Alg.Term algebra.F.id_not (x5::nil)) ->
       exists x4,
         t' = (algebra.Alg.Term algebra.F.id_not (x4::nil))/\ 
         (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x4 x5)).
 Proof.
   intros t t' H.
   
   induction H as [|y IH z z_to_y] using 
   closure_extension.refl_trans_clos_ind2.
   constructor 1.
   intros H;intuition;constructor 1.
   intros x5 x7 H;exists x5;exists x7;intuition;constructor 1.
   intros x5 x7 H;exists x5;exists x7;intuition;constructor 1.
   intros H;intuition;constructor 1.
   intros x5 x7 H;exists x5;exists x7;intuition;constructor 1.
   intros H;intuition;constructor 1.
   intros x5 H;exists x5;intuition;constructor 1.
   intros x5 H;exists x5;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_false H_id_rem H_id_and H_id_0 H_id__equal_ H_id_true H_id_s 
    H_id_not].
   constructor.
   
   clear H_id_rem H_id_and H_id_0 H_id__equal_ H_id_true H_id_s H_id_not;
    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_false H_id_and H_id_0 H_id__equal_ H_id_true H_id_s H_id_not;
    intros x5 x7 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 x5 |- _ =>
      destruct (H_id_rem y x7 (refl_equal _)) as [x4 [x6]];intros ;intuition;
       exists x4;exists x6;intuition;
       eapply closure_extension.refl_trans_clos_R;eassumption
     end
   .
   
   match goal with
     | H:algebra.EQT.one_step _ ?y x7 |- _ =>
      destruct (H_id_rem x5 y (refl_equal _)) as [x4 [x6]];intros ;intuition;
       exists x4;exists x6;intuition;
       eapply closure_extension.refl_trans_clos_R;eassumption
     end
   .
   
   clear H_id_false H_id_rem H_id_0 H_id__equal_ H_id_true H_id_s H_id_not;
    intros x5 x7 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 x5 |- _ =>
      destruct (H_id_and y x7 (refl_equal _)) as [x4 [x6]];intros ;intuition;
       exists x4;exists x6;intuition;
       eapply closure_extension.refl_trans_clos_R;eassumption
     end
   .
   
   match goal with
     | H:algebra.EQT.one_step _ ?y x7 |- _ =>
      destruct (H_id_and x5 y (refl_equal _)) as [x4 [x6]];intros ;intuition;
       exists x4;exists x6;intuition;
       eapply closure_extension.refl_trans_clos_R;eassumption
     end
   .
   
   clear H_id_false H_id_rem H_id_and H_id__equal_ H_id_true H_id_s H_id_not;
    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_false H_id_rem H_id_and H_id_0 H_id_true H_id_s H_id_not;
    intros x5 x7 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 x5 |- _ =>
      destruct (H_id__equal_ y x7 (refl_equal _)) as [x4 [x6]];intros ;
       intuition;exists x4;exists x6;intuition;
       eapply closure_extension.refl_trans_clos_R;eassumption
     end
   .
   
   match goal with
     | H:algebra.EQT.one_step _ ?y x7 |- _ =>
      destruct (H_id__equal_ x5 y (refl_equal _)) as [x4 [x6]];intros ;
       intuition;exists x4;exists x6;intuition;
       eapply closure_extension.refl_trans_clos_R;eassumption
     end
   .
   
   clear H_id_false H_id_rem H_id_and H_id_0 H_id__equal_ H_id_s H_id_not;
    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_false H_id_rem H_id_and H_id_0 H_id__equal_ H_id_true H_id_not;
    intros x5 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 x5 |- _ =>
      destruct (H_id_s y (refl_equal _)) as [x4];intros ;intuition;exists x4;
       intuition;eapply closure_extension.refl_trans_clos_R;eassumption
     end
   .
   
   clear H_id_false H_id_rem H_id_and H_id_0 H_id__equal_ H_id_true H_id_s;
    intros x5 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 x5 |- _ =>
      destruct (H_id_not y (refl_equal _)) as [x4];intros ;intuition;
       exists x4;intuition;eapply closure_extension.refl_trans_clos_R;
       eassumption
     end
   .
 Qed.
 
 
 Lemma id_false_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_false nil) ->
     t' = (algebra.Alg.Term algebra.F.id_false nil).
 Proof.
   intros t t' H.
   destruct (are_constuctors_of_R_xml_0 H).
   assumption.
 Qed.
 
 
 Lemma id_rem_is_R_xml_0_constructor :
  forall t t', 
   (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
    forall x5 x7, 
     t = (algebra.Alg.Term algebra.F.id_rem (x5::x7::nil)) ->
      exists x4,
        exists x6,
          t' = (algebra.Alg.Term algebra.F.id_rem (x4::x6::nil))/\ 
          (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x4 x5)/\
           
          (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x6 x7).
 Proof.
   intros t t' H.
   destruct (are_constuctors_of_R_xml_0 H).
   assumption.
 Qed.
 
 
 Lemma id_and_is_R_xml_0_constructor :
  forall t t', 
   (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
    forall x5 x7, 
     t = (algebra.Alg.Term algebra.F.id_and (x5::x7::nil)) ->
      exists x4,
        exists x6,
          t' = (algebra.Alg.Term algebra.F.id_and (x4::x6::nil))/\ 
          (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x4 x5)/\
           
          (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x6 x7).
 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__equal__is_R_xml_0_constructor :
  forall t t', 
   (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
    forall x5 x7, 
     t = (algebra.Alg.Term algebra.F.id__equal_ (x5::x7::nil)) ->
      exists x4,
        exists x6,
          t' = (algebra.Alg.Term algebra.F.id__equal_ (x4::x6::nil))/\ 
          (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x4 x5)/\
           
          (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x6 x7).
 Proof.
   intros t t' H.
   destruct (are_constuctors_of_R_xml_0 H).
   assumption.
 Qed.
 
 
 Lemma id_true_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_true nil) ->
     t' = (algebra.Alg.Term algebra.F.id_true nil).
 Proof.
   intros t t' H.
   destruct (are_constuctors_of_R_xml_0 H).
   assumption.
 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 x5, 
     t = (algebra.Alg.Term algebra.F.id_s (x5::nil)) ->
      exists x4,
        t' = (algebra.Alg.Term algebra.F.id_s (x4::nil))/\ 
        (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x4 x5).
 Proof.
   intros t t' H.
   destruct (are_constuctors_of_R_xml_0 H).
   assumption.
 Qed.
 
 
 Lemma id_not_is_R_xml_0_constructor :
  forall t t', 
   (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
    forall x5, 
     t = (algebra.Alg.Term algebra.F.id_not (x5::nil)) ->
      exists x4,
        t' = (algebra.Alg.Term algebra.F.id_not (x4::nil))/\ 
        (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x4 x5).
 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_false nil) |- _ =>
     let Heq := fresh "Heq" in 
      (set (Heq:=id_false_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_rem (?x5::?x4::nil)) |- _ =>
     let x5 := fresh "x" in 
      (let x4 := fresh "x" in 
        (let Heq := fresh "Heq" in 
          (let Hred1 := fresh "Hred" in 
            (let Hred2 := fresh "Hred" in 
              (destruct (id_rem_is_R_xml_0_constructor H (refl_equal _)) as 
               [x5 [x4 [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_and (?x5::?x4::nil)) |- _ =>
     let x5 := fresh "x" in 
      (let x4 := fresh "x" in 
        (let Heq := fresh "Heq" in 
          (let Hred1 := fresh "Hred" in 
            (let Hred2 := fresh "Hred" in 
              (destruct (id_and_is_R_xml_0_constructor H (refl_equal _)) as 
               [x5 [x4 [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_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__equal_ (?x5::?x4::nil)) |- 
    _ =>
     let x5 := fresh "x" in 
      (let x4 := fresh "x" in 
        (let Heq := fresh "Heq" in 
          (let Hred1 := fresh "Hred" in 
            (let Hred2 := fresh "Hred" in 
              (destruct (id__equal__is_R_xml_0_constructor H (refl_equal _))
                as [x5 [x4 [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_true nil) |- _ =>
     let Heq := fresh "Heq" in 
      (set (Heq:=id_true_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_s (?x4::nil)) |- _ =>
     let x4 := 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 
           [x4 [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_not (?x4::nil)) |- _ =>
     let x4 := fresh "x" in 
      (let Heq := fresh "Heq" in 
        (let Hred1 := fresh "Hred" in 
          (destruct (id_not_is_R_xml_0_constructor H (refl_equal _)) as 
           [x4 [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_false nil) |- _ =>
     let Heq := fresh "Heq" in 
      (set (Heq:=id_false_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_rem (?x5::?x4::nil)) |- _ =>
     let x5 := fresh "x" in 
      (let x4 := fresh "x" in 
        (let Heq := fresh "Heq" in 
          (let Hred1 := fresh "Hred" in 
            (let Hred2 := fresh "Hred" in 
              (destruct (id_rem_is_R_xml_0_constructor H (refl_equal _)) as 
               [x5 [x4 [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_and (?x5::?x4::nil)) |- _ =>
     let x5 := fresh "x" in 
      (let x4 := fresh "x" in 
        (let Heq := fresh "Heq" in 
          (let Hred1 := fresh "Hred" in 
            (let Hred2 := fresh "Hred" in 
              (destruct (id_and_is_R_xml_0_constructor H (refl_equal _)) as 
               [x5 [x4 [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_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__equal_ (?x5::?x4::nil)) |- 
    _ =>
     let x5 := fresh "x" in 
      (let x4 := fresh "x" in 
        (let Heq := fresh "Heq" in 
          (let Hred1 := fresh "Hred" in 
            (let Hred2 := fresh "Hred" in 
              (destruct (id__equal__is_R_xml_0_constructor H (refl_equal _))
                as [x5 [x4 [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_true nil) |- _ =>
     let Heq := fresh "Heq" in 
      (set (Heq:=id_true_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_s (?x4::nil)) |- _ =>
     let x4 := 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 
           [x4 [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_not (?x4::nil)) |- _ =>
     let x4 := fresh "x" in 
      (let Heq := fresh "Heq" in 
        (let Hred1 := fresh "Hred" in 
          (destruct (id_not_is_R_xml_0_constructor H (refl_equal _)) as 
           [x4 [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_prime : A ->A.
   
   Hypothesis P_id_divp : A ->A ->A.
   
   Hypothesis P_id_prime1 : A ->A ->A.
   
   Hypothesis P_id_false : A.
   
   Hypothesis P_id_rem : A ->A ->A.
   
   Hypothesis P_id_and : A ->A ->A.
   
   Hypothesis P_id_0 : A.
   
   Hypothesis P_id__equal_ : A ->A ->A.
   
   Hypothesis P_id_true : A.
   
   Hypothesis P_id_s : A ->A.
   
   Hypothesis P_id_not : A ->A.
   
   Hypothesis P_id_prime_monotonic :
    forall x4 x5, (A0 <= x5)/\ (x5 <= x4) ->P_id_prime x5 <= P_id_prime x4.
   
   Hypothesis P_id_divp_monotonic :
    forall x4 x6 x5 x7, 
     (A0 <= x7)/\ (x7 <= x6) ->
      (A0 <= x5)/\ (x5 <= x4) ->P_id_divp x5 x7 <= P_id_divp x4 x6.
   
   Hypothesis P_id_prime1_monotonic :
    forall x4 x6 x5 x7, 
     (A0 <= x7)/\ (x7 <= x6) ->
      (A0 <= x5)/\ (x5 <= x4) ->P_id_prime1 x5 x7 <= P_id_prime1 x4 x6.
   
   Hypothesis P_id_rem_monotonic :
    forall x4 x6 x5 x7, 
     (A0 <= x7)/\ (x7 <= x6) ->
      (A0 <= x5)/\ (x5 <= x4) ->P_id_rem x5 x7 <= P_id_rem x4 x6.
   
   Hypothesis P_id_and_monotonic :
    forall x4 x6 x5 x7, 
     (A0 <= x7)/\ (x7 <= x6) ->
      (A0 <= x5)/\ (x5 <= x4) ->P_id_and x5 x7 <= P_id_and x4 x6.
   
   Hypothesis P_id__equal__monotonic :
    forall x4 x6 x5 x7, 
     (A0 <= x7)/\ (x7 <= x6) ->
      (A0 <= x5)/\ (x5 <= x4) ->P_id__equal_ x5 x7 <= P_id__equal_ x4 x6.
   
   Hypothesis P_id_s_monotonic :
    forall x4 x5, (A0 <= x5)/\ (x5 <= x4) ->P_id_s x5 <= P_id_s x4.
   
   Hypothesis P_id_not_monotonic :
    forall x4 x5, (A0 <= x5)/\ (x5 <= x4) ->P_id_not x5 <= P_id_not x4.
   
   Hypothesis P_id_prime_bounded :
    forall x4, (A0 <= x4) ->A0 <= P_id_prime x4.
   
   Hypothesis P_id_divp_bounded :
    forall x4 x5, (A0 <= x4) ->(A0 <= x5) ->A0 <= P_id_divp x5 x4.
   
   Hypothesis P_id_prime1_bounded :
    forall x4 x5, (A0 <= x4) ->(A0 <= x5) ->A0 <= P_id_prime1 x5 x4.
   
   Hypothesis P_id_false_bounded : A0 <= P_id_false .
   
   Hypothesis P_id_rem_bounded :
    forall x4 x5, (A0 <= x4) ->(A0 <= x5) ->A0 <= P_id_rem x5 x4.
   
   Hypothesis P_id_and_bounded :
    forall x4 x5, (A0 <= x4) ->(A0 <= x5) ->A0 <= P_id_and x5 x4.
   
   Hypothesis P_id_0_bounded : A0 <= P_id_0 .
   
   Hypothesis P_id__equal__bounded :
    forall x4 x5, (A0 <= x4) ->(A0 <= x5) ->A0 <= P_id__equal_ x5 x4.
   
   Hypothesis P_id_true_bounded : A0 <= P_id_true .
   
   Hypothesis P_id_s_bounded : forall x4, (A0 <= x4) ->A0 <= P_id_s x4.
   
   Hypothesis P_id_not_bounded : forall x4, (A0 <= x4) ->A0 <= P_id_not x4.
   
   Fixpoint measure t { struct t }  := 
     match t with
       | (algebra.Alg.Term algebra.F.id_prime (x4::nil)) =>
        P_id_prime (measure x4)
       | (algebra.Alg.Term algebra.F.id_divp (x5::x4::nil)) =>
        P_id_divp (measure x5) (measure x4)
       | (algebra.Alg.Term algebra.F.id_prime1 (x5::x4::nil)) =>
        P_id_prime1 (measure x5) (measure x4)
       | (algebra.Alg.Term algebra.F.id_false nil) => P_id_false 
       | (algebra.Alg.Term algebra.F.id_rem (x5::x4::nil)) =>
        P_id_rem (measure x5) (measure x4)
       | (algebra.Alg.Term algebra.F.id_and (x5::x4::nil)) =>
        P_id_and (measure x5) (measure x4)
       | (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0 
       | (algebra.Alg.Term algebra.F.id__equal_ (x5::x4::nil)) =>
        P_id__equal_ (measure x5) (measure x4)
       | (algebra.Alg.Term algebra.F.id_true nil) => P_id_true 
       | (algebra.Alg.Term algebra.F.id_s (x4::nil)) => P_id_s (measure x4)
       | (algebra.Alg.Term algebra.F.id_not (x4::nil)) =>
        P_id_not (measure x4)
       | _ => A0
       end.
   
   Lemma measure_equation :
    forall t, 
     measure t = match t with
                   | (algebra.Alg.Term algebra.F.id_prime (x4::nil)) =>
                    P_id_prime (measure x4)
                   | (algebra.Alg.Term algebra.F.id_divp (x5::x4::nil)) =>
                    P_id_divp (measure x5) (measure x4)
                   | (algebra.Alg.Term algebra.F.id_prime1 (x5::x4::nil)) =>
                    P_id_prime1 (measure x5) (measure x4)
                   | (algebra.Alg.Term algebra.F.id_false nil) => P_id_false 
                   | (algebra.Alg.Term algebra.F.id_rem (x5::x4::nil)) =>
                    P_id_rem (measure x5) (measure x4)
                   | (algebra.Alg.Term algebra.F.id_and (x5::x4::nil)) =>
                    P_id_and (measure x5) (measure x4)
                   | (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0 
                   | (algebra.Alg.Term algebra.F.id__equal_ (x5::x4::nil)) =>
                    P_id__equal_ (measure x5) (measure x4)
                   | (algebra.Alg.Term algebra.F.id_true nil) => P_id_true 
                   | (algebra.Alg.Term algebra.F.id_s (x4::nil)) =>
                    P_id_s (measure x4)
                   | (algebra.Alg.Term algebra.F.id_not (x4::nil)) =>
                    P_id_not (measure x4)
                   | _ => 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_prime => P_id_prime
       | algebra.F.id_divp => P_id_divp
       | algebra.F.id_prime1 => P_id_prime1
       | algebra.F.id_false => P_id_false
       | algebra.F.id_rem => P_id_rem
       | algebra.F.id_and => P_id_and
       | algebra.F.id_0 => P_id_0
       | algebra.F.id__equal_ => P_id__equal_
       | algebra.F.id_true => P_id_true
       | algebra.F.id_s => P_id_s
       | algebra.F.id_not => P_id_not
       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_prime =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::_ => _
                 end
              | algebra.F.id_divp =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::nil => _
                 | _::_::_::_ => _
                 end
              | algebra.F.id_prime1 =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::nil => _
                 | _::_::_::_ => _
                 end
              | algebra.F.id_false => match l with
                                        | nil => _
                                        | _::_ => _
                                        end
              | algebra.F.id_rem =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::nil => _
                 | _::_::_::_ => _
                 end
              | algebra.F.id_and =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::nil => _
                 | _::_::_::_ => _
                 end
              | algebra.F.id_0 => match l with
                                    | nil => _
                                    | _::_ => _
                                    end
              | algebra.F.id__equal_ =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::nil => _
                 | _::_::_::_ => _
                 end
              | algebra.F.id_true => match l with
                                       | nil => _
                                       | _::_ => _
                                       end
              | algebra.F.id_s =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::_ => _
                 end
              | algebra.F.id_not =>
               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_prime_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_divp_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_prime1_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_false_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_rem_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_and_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_0_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id__equal__bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_true_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_s_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_not_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_prime_monotonic;assumption.
     vm_compute in |-*;intros ;apply P_id_divp_monotonic;assumption.
     vm_compute in |-*;intros ;apply P_id_prime1_monotonic;assumption.
     vm_compute in |-*;apply (Aop.(le_refl)).
     vm_compute in |-*;intros ;apply P_id_rem_monotonic;assumption.
     vm_compute in |-*;intros ;apply P_id_and_monotonic;assumption.
     vm_compute in |-*;apply (Aop.(le_refl)).
     vm_compute in |-*;intros ;apply P_id__equal__monotonic;assumption.
     vm_compute in |-*;apply (Aop.(le_refl)).
     vm_compute in |-*;intros ;apply P_id_s_monotonic;assumption.
     vm_compute in |-*;intros ;apply P_id_not_monotonic;assumption.
     intros f.
     case f.
     vm_compute in |-*;intros ;apply P_id_prime_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_divp_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_prime1_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_false_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_rem_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_and_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_0_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id__equal__bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_true_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_s_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_not_bounded;assumption.
     intros .
     do 2 (rewrite  <- same_measure in |-*).
     apply rules_monotonic;assumption.
     assumption.
   Qed.
   
   Hypothesis P_id_PRIME1 : A ->A ->A.
   
   Hypothesis P_id_DIVP : A ->A ->A.
   
   Hypothesis P_id_PRIME : A ->A.
   
   Hypothesis P_id_PRIME1_monotonic :
    forall x4 x6 x5 x7, 
     (A0 <= x7)/\ (x7 <= x6) ->
      (A0 <= x5)/\ (x5 <= x4) ->P_id_PRIME1 x5 x7 <= P_id_PRIME1 x4 x6.
   
   Hypothesis P_id_DIVP_monotonic :
    forall x4 x6 x5 x7, 
     (A0 <= x7)/\ (x7 <= x6) ->
      (A0 <= x5)/\ (x5 <= x4) ->P_id_DIVP x5 x7 <= P_id_DIVP x4 x6.
   
   Hypothesis P_id_PRIME_monotonic :
    forall x4 x5, (A0 <= x5)/\ (x5 <= x4) ->P_id_PRIME x5 <= P_id_PRIME x4.
   
   Definition marked_measure t := 
     match t with
       | (algebra.Alg.Term algebra.F.id_prime1 (x5::x4::nil)) =>
        P_id_PRIME1 (measure x5) (measure x4)
       | (algebra.Alg.Term algebra.F.id_divp (x5::x4::nil)) =>
        P_id_DIVP (measure x5) (measure x4)
       | (algebra.Alg.Term algebra.F.id_prime (x4::nil)) =>
        P_id_PRIME (measure x4)
       | _ => 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 x5 x4;apply (P_id_PRIME1 x5 x4).
     
     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 x5 x4;apply (P_id_DIVP x5 x4).
     
     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 x4;apply (P_id_PRIME x4).
     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_prime =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::_ => _
                 end
              | algebra.F.id_divp =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::nil => _
                 | _::_::_::_ => _
                 end
              | algebra.F.id_prime1 =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::nil => _
                 | _::_::_::_ => _
                 end
              | algebra.F.id_false => match l with
                                        | nil => _
                                        | _::_ => _
                                        end
              | algebra.F.id_rem =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::nil => _
                 | _::_::_::_ => _
                 end
              | algebra.F.id_and =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::nil => _
                 | _::_::_::_ => _
                 end
              | algebra.F.id_0 => match l with
                                    | nil => _
                                    | _::_ => _
                                    end
              | algebra.F.id__equal_ =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::nil => _
                 | _::_::_::_ => _
                 end
              | algebra.F.id_true => match l with
                                       | nil => _
                                       | _::_ => _
                                       end
              | algebra.F.id_s =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::_ => _
                 end
              | algebra.F.id_not =>
               match l with
                 | nil => _
                 | _::nil => _
                 | _::_::_ => _
                 end
              end.
     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 .
     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 .
     
     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 .
     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 .
     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_prime1 (x5::
                             x4::nil)) =>
                           P_id_PRIME1 (measure x5) (measure x4)
                          | (algebra.Alg.Term algebra.F.id_divp (x5::
                             x4::nil)) =>
                           P_id_DIVP (measure x5) (measure x4)
                          | (algebra.Alg.Term algebra.F.id_prime (x4::nil)) =>
                           P_id_PRIME (measure x4)
                          | _ => 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_prime_monotonic;assumption.
     vm_compute in |-*;intros ;apply P_id_divp_monotonic;assumption.
     vm_compute in |-*;intros ;apply P_id_prime1_monotonic;assumption.
     vm_compute in |-*;apply (Aop.(le_refl)).
     vm_compute in |-*;intros ;apply P_id_rem_monotonic;assumption.
     vm_compute in |-*;intros ;apply P_id_and_monotonic;assumption.
     vm_compute in |-*;apply (Aop.(le_refl)).
     vm_compute in |-*;intros ;apply P_id__equal__monotonic;assumption.
     vm_compute in |-*;apply (Aop.(le_refl)).
     vm_compute in |-*;intros ;apply P_id_s_monotonic;assumption.
     vm_compute in |-*;intros ;apply P_id_not_monotonic;assumption.
     clear f.
     intros f.
     case f.
     vm_compute in |-*;intros ;apply P_id_prime_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_divp_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_prime1_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_false_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_rem_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_and_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_0_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id__equal__bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_true_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_s_bounded;assumption.
     vm_compute in |-*;intros ;apply P_id_not_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_PRIME1_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_DIVP_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_PRIME_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_prime : Z ->Z.
   
   Hypothesis P_id_divp : Z ->Z ->Z.
   
   Hypothesis P_id_prime1 : Z ->Z ->Z.
   
   Hypothesis P_id_false : Z.
   
   Hypothesis P_id_rem : Z ->Z ->Z.
   
   Hypothesis P_id_and : Z ->Z ->Z.
   
   Hypothesis P_id_0 : Z.
   
   Hypothesis P_id__equal_ : Z ->Z ->Z.
   
   Hypothesis P_id_true : Z.
   
   Hypothesis P_id_s : Z ->Z.
   
   Hypothesis P_id_not : Z ->Z.
   
   Hypothesis P_id_prime_monotonic :
    forall x4 x5, 
     (min_value <= x5)/\ (x5 <= x4) ->P_id_prime x5 <= P_id_prime x4.
   
   Hypothesis P_id_divp_monotonic :
    forall x4 x6 x5 x7, 
     (min_value <= x7)/\ (x7 <= x6) ->
      (min_value <= x5)/\ (x5 <= x4) ->P_id_divp x5 x7 <= P_id_divp x4 x6.
   
   Hypothesis P_id_prime1_monotonic :
    forall x4 x6 x5 x7, 
     (min_value <= x7)/\ (x7 <= x6) ->
      (min_value <= x5)/\ (x5 <= x4) ->P_id_prime1 x5 x7 <= P_id_prime1 x4 x6.
   
   Hypothesis P_id_rem_monotonic :
    forall x4 x6 x5 x7, 
     (min_value <= x7)/\ (x7 <= x6) ->
      (min_value <= x5)/\ (x5 <= x4) ->P_id_rem x5 x7 <= P_id_rem x4 x6.
   
   Hypothesis P_id_and_monotonic :
    forall x4 x6 x5 x7, 
     (min_value <= x7)/\ (x7 <= x6) ->
      (min_value <= x5)/\ (x5 <= x4) ->P_id_and x5 x7 <= P_id_and x4 x6.
   
   Hypothesis P_id__equal__monotonic :
    forall x4 x6 x5 x7, 
     (min_value <= x7)/\ (x7 <= x6) ->
      (min_value <= x5)/\ (x5 <= x4) ->
       P_id__equal_ x5 x7 <= P_id__equal_ x4 x6.
   
   Hypothesis P_id_s_monotonic :
    forall x4 x5, (min_value <= x5)/\ (x5 <= x4) ->P_id_s x5 <= P_id_s x4.
   
   Hypothesis P_id_not_monotonic :
    forall x4 x5, (min_value <= x5)/\ (x5 <= x4) ->P_id_not x5 <= P_id_not x4.
   
   Hypothesis P_id_prime_bounded :
    forall x4, (min_value <= x4) ->min_value <= P_id_prime x4.
   
   Hypothesis P_id_divp_bounded :
    forall x4 x5, 
     (min_value <= x4) ->(min_value <= x5) ->min_value <= P_id_divp x5 x4.
   
   Hypothesis P_id_prime1_bounded :
    forall x4 x5, 
     (min_value <= x4) ->(min_value <= x5) ->min_value <= P_id_prime1 x5 x4.
   
   Hypothesis P_id_false_bounded : min_value <= P_id_false .
   
   Hypothesis P_id_rem_bounded :
    forall x4 x5, 
     (min_value <= x4) ->(min_value <= x5) ->min_value <= P_id_rem x5 x4.
   
   Hypothesis P_id_and_bounded :
    forall x4 x5, 
     (min_value <= x4) ->(min_value <= x5) ->min_value <= P_id_and x5 x4.
   
   Hypothesis P_id_0_bounded : min_value <= P_id_0 .
   
   Hypothesis P_id__equal__bounded :
    forall x4 x5, 
     (min_value <= x4) ->(min_value <= x5) ->min_value <= P_id__equal_ x5 x4.
   
   Hypothesis P_id_true_bounded : min_value <= P_id_true .
   
   Hypothesis P_id_s_bounded :
    forall x4, (min_value <= x4) ->min_value <= P_id_s x4.
   
   Hypothesis P_id_not_bounded :
    forall x4, (min_value <= x4) ->min_value <= P_id_not x4.
   
   Definition measure  := 
     Interp.measure min_value P_id_prime P_id_divp P_id_prime1 P_id_false 
      P_id_rem P_id_and P_id_0 P_id__equal_ P_id_true P_id_s P_id_not.
   
   Lemma measure_equation :
    forall t, 
     measure t = match t with
                   | (algebra.Alg.Term algebra.F.id_prime (x4::nil)) =>
                    P_id_prime (measure x4)
                   | (algebra.Alg.Term algebra.F.id_divp (x5::x4::nil)) =>
                    P_id_divp (measure x5) (measure x4)
                   | (algebra.Alg.Term algebra.F.id_prime1 (x5::x4::nil)) =>
                    P_id_prime1 (measure x5) (measure x4)
                   | (algebra.Alg.Term algebra.F.id_false nil) => P_id_false 
                   | (algebra.Alg.Term algebra.F.id_rem (x5::x4::nil)) =>
                    P_id_rem (measure x5) (measure x4)
                   | (algebra.Alg.Term algebra.F.id_and (x5::x4::nil)) =>
                    P_id_and (measure x5) (measure x4)
                   | (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0 
                   | (algebra.Alg.Term algebra.F.id__equal_ (x5::x4::nil)) =>
                    P_id__equal_ (measure x5) (measure x4)
                   | (algebra.Alg.Term algebra.F.id_true nil) => P_id_true 
                   | (algebra.Alg.Term algebra.F.id_s (x4::nil)) =>
                    P_id_s (measure x4)
                   | (algebra.Alg.Term algebra.F.id_not (x4::nil)) =>
                    P_id_not (measure x4)
                   | _ => 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_prime_monotonic;assumption.
     intros ;apply P_id_divp_monotonic;assumption.
     intros ;apply P_id_prime1_monotonic;assumption.
     intros ;apply P_id_rem_monotonic;assumption.
     intros ;apply P_id_and_monotonic;assumption.
     intros ;apply P_id__equal__monotonic;assumption.
     intros ;apply P_id_s_monotonic;assumption.
     intros ;apply P_id_not_monotonic;assumption.
     intros ;apply P_id_prime_bounded;assumption.
     intros ;apply P_id_divp_bounded;assumption.
     intros ;apply P_id_prime1_bounded;assumption.
     intros ;apply P_id_false_bounded;assumption.
     intros ;apply P_id_rem_bounded;assumption.
     intros ;apply P_id_and_bounded;assumption.
     intros ;apply P_id_0_bounded;assumption.
     intros ;apply P_id__equal__bounded;assumption.
     intros ;apply P_id_true_bounded;assumption.
     intros ;apply P_id_s_bounded;assumption.
     intros ;apply P_id_not_bounded;assumption.
     apply rules_monotonic.
   Qed.
   
   Hypothesis P_id_PRIME1 : Z ->Z ->Z.
   
   Hypothesis P_id_DIVP : Z ->Z ->Z.
   
   Hypothesis P_id_PRIME : Z ->Z.
   
   Hypothesis P_id_PRIME1_monotonic :
    forall x4 x6 x5 x7, 
     (min_value <= x7)/\ (x7 <= x6) ->
      (min_value <= x5)/\ (x5 <= x4) ->P_id_PRIME1 x5 x7 <= P_id_PRIME1 x4 x6.
   
   Hypothesis P_id_DIVP_monotonic :
    forall x4 x6 x5 x7, 
     (min_value <= x7)/\ (x7 <= x6) ->
      (min_value <= x5)/\ (x5 <= x4) ->P_id_DIVP x5 x7 <= P_id_DIVP x4 x6.
   
   Hypothesis P_id_PRIME_monotonic :
    forall x4 x5, 
     (min_value <= x5)/\ (x5 <= x4) ->P_id_PRIME x5 <= P_id_PRIME x4.
   
   Definition marked_measure  := 
     Interp.marked_measure min_value P_id_prime P_id_divp P_id_prime1 
      P_id_false P_id_rem P_id_and P_id_0 P_id__equal_ P_id_true P_id_s 
      P_id_not P_id_PRIME1 P_id_DIVP P_id_PRIME.
   
   Lemma marked_measure_equation :
    forall t, 
     marked_measure t = match t with
                          | (algebra.Alg.Term algebra.F.id_prime1 (x5::
                             x4::nil)) =>
                           P_id_PRIME1 (measure x5) (measure x4)
                          | (algebra.Alg.Term algebra.F.id_divp (x5::
                             x4::nil)) =>
                           P_id_DIVP (measure x5) (measure x4)
                          | (algebra.Alg.Term algebra.F.id_prime (x4::nil)) =>
                           P_id_PRIME (measure x4)
                          | _ => 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_prime_monotonic;assumption.
     intros ;apply P_id_divp_monotonic;assumption.
     intros ;apply P_id_prime1_monotonic;assumption.
     intros ;apply P_id_rem_monotonic;assumption.
     intros ;apply P_id_and_monotonic;assumption.
     intros ;apply P_id__equal__monotonic;assumption.
     intros ;apply P_id_s_monotonic;assumption.
     intros ;apply P_id_not_monotonic;assumption.
     intros ;apply P_id_prime_bounded;assumption.
     intros ;apply P_id_divp_bounded;assumption.
     intros ;apply P_id_prime1_bounded;assumption.
     intros ;apply P_id_false_bounded;assumption.
     intros ;apply P_id_rem_bounded;assumption.
     intros ;apply P_id_and_bounded;assumption.
     intros ;apply P_id_0_bounded;assumption.
     intros ;apply P_id__equal__bounded;assumption.
     intros ;apply P_id_true_bounded;assumption.
     intros ;apply P_id_s_bounded;assumption.
     intros ;apply P_id_not_bounded;assumption.
     apply rules_monotonic.
     intros ;apply P_id_PRIME1_monotonic;assumption.
     intros ;apply P_id_DIVP_monotonic;assumption.
     intros ;apply P_id_PRIME_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 := 
    (* <prime(s(s(x_))),prime1(s(s(x_)),s(x_))> *)
   | DP_R_xml_0_0 :
    forall x4 x1, 
     (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                
       (algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Term algebra.F.id_s 
        (x1::nil))::nil)) x4) ->
      DP_R_xml_0 (algebra.Alg.Term algebra.F.id_prime1 ((algebra.Alg.Term 
                  algebra.F.id_s ((algebra.Alg.Term algebra.F.id_s 
                  (x1::nil))::nil))::(algebra.Alg.Term algebra.F.id_s 
                  (x1::nil))::nil)) 
       (algebra.Alg.Term algebra.F.id_prime (x4::nil))
    (* <prime1(x_,s(s(y_))),divp(s(s(y_)),x_)> *)
   | DP_R_xml_0_1 :
    forall x4 x2 x1 x5, 
     (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                x1 x5) ->
      (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                 
        (algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Term algebra.F.id_s 
         (x2::nil))::nil)) x4) ->
       DP_R_xml_0 (algebra.Alg.Term algebra.F.id_divp ((algebra.Alg.Term 
                   algebra.F.id_s ((algebra.Alg.Term algebra.F.id_s 
                   (x2::nil))::nil))::x1::nil)) 
        (algebra.Alg.Term algebra.F.id_prime1 (x5::x4::nil))
    (* <prime1(x_,s(s(y_))),prime1(x_,s(y_))> *)
   | DP_R_xml_0_2 :
    forall x4 x2 x1 x5, 
     (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                x1 x5) ->
      (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                 
        (algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Term algebra.F.id_s 
         (x2::nil))::nil)) x4) ->
       DP_R_xml_0 (algebra.Alg.Term algebra.F.id_prime1 (x1::
                   (algebra.Alg.Term algebra.F.id_s (x2::nil))::nil)) 
        (algebra.Alg.Term algebra.F.id_prime1 (x5::x4::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_non_scc_1  :
   algebra.Alg.term ->algebra.Alg.term ->Prop := 
     (* <prime1(x_,s(s(y_))),divp(s(s(y_)),x_)> *)
    | DP_R_xml_0_non_scc_1_0 :
     forall x4 x2 x1 x5, 
      (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                 x1 x5) ->
       (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                  
         (algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Term algebra.F.id_s 
          (x2::nil))::nil)) x4) ->
        DP_R_xml_0_non_scc_1 (algebra.Alg.Term algebra.F.id_divp 
                              ((algebra.Alg.Term algebra.F.id_s 
                              ((algebra.Alg.Term algebra.F.id_s 
                              (x2::nil))::nil))::x1::nil)) 
         (algebra.Alg.Term algebra.F.id_prime1 (x5::x4::nil))
  .
  
  
  Lemma acc_DP_R_xml_0_non_scc_1 :
   forall x y, 
    (DP_R_xml_0_non_scc_1 x y) ->Acc WF_R_xml_0_deep_rew.DP_R_xml_0 x.
  Proof.
    intros x y h.
    
    inversion h;clear h;subst;
     constructor;intros _y _h;inversion _h;clear _h;subst;
      (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_scc_2  :
   algebra.Alg.term ->algebra.Alg.term ->Prop := 
     (* <prime1(x_,s(s(y_))),prime1(x_,s(y_))> *)
    | DP_R_xml_0_scc_2_0 :
     forall x4 x2 x1 x5, 
      (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                 x1 x5) ->
       (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                  
         (algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Term algebra.F.id_s 
          (x2::nil))::nil)) x4) ->
        DP_R_xml_0_scc_2 (algebra.Alg.Term algebra.F.id_prime1 (x1::
                          (algebra.Alg.Term algebra.F.id_s (x2::nil))::nil)) 
         (algebra.Alg.Term algebra.F.id_prime1 (x5::x4::nil))
  .
  
  
  Module WF_DP_R_xml_0_scc_2.
   Open Scope Z_scope.
   
   Import ring_extention.
   
   Notation Local "a <= b" := (Zle a b).
   
   Notation Local "a < b" := (Zlt a b).
   
   Definition P_id_prime (x4:Z) := 0.
   
   Definition P_id_divp (x4:Z) (x5:Z) := 2 + 2* x4.
   
   Definition P_id_prime1 (x4:Z) (x5:Z) := 0.
   
   Definition P_id_false  := 0.
   
   Definition P_id_rem (x4:Z) (x5:Z) := 1* x4.
   
   Definition P_id_and (x4:Z) (x5:Z) := 0.
   
   Definition P_id_0  := 0.
   
   Definition P_id__equal_ (x4:Z) (x5:Z) := 1 + 1* x4.
   
   Definition P_id_true  := 0.
   
   Definition P_id_s (x4:Z) := 3 + 3* x4.
   
   Definition P_id_not (x4:Z) := 0.
   
   Lemma P_id_prime_monotonic :
    forall x4 x5, (0 <= x5)/\ (x5 <= x4) ->P_id_prime x5 <= P_id_prime x4.
   Proof.
     intros x5 x4.
     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_divp_monotonic :
    forall x4 x6 x5 x7, 
     (0 <= x7)/\ (x7 <= x6) ->
      (0 <= x5)/\ (x5 <= x4) ->P_id_divp x5 x7 <= P_id_divp x4 x6.
   Proof.
     intros x7 x6 x5 x4.
     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_prime1_monotonic :
    forall x4 x6 x5 x7, 
     (0 <= x7)/\ (x7 <= x6) ->
      (0 <= x5)/\ (x5 <= x4) ->P_id_prime1 x5 x7 <= P_id_prime1 x4 x6.
   Proof.
     intros x7 x6 x5 x4.
     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_rem_monotonic :
    forall x4 x6 x5 x7, 
     (0 <= x7)/\ (x7 <= x6) ->
      (0 <= x5)/\ (x5 <= x4) ->P_id_rem x5 x7 <= P_id_rem x4 x6.
   Proof.
     intros x7 x6 x5 x4.
     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_and_monotonic :
    forall x4 x6 x5 x7, 
     (0 <= x7)/\ (x7 <= x6) ->
      (0 <= x5)/\ (x5 <= x4) ->P_id_and x5 x7 <= P_id_and x4 x6.
   Proof.
     intros x7 x6 x5 x4.
     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__equal__monotonic :
    forall x4 x6 x5 x7, 
     (0 <= x7)/\ (x7 <= x6) ->
      (0 <= x5)/\ (x5 <= x4) ->P_id__equal_ x5 x7 <= P_id__equal_ x4 x6.
   Proof.
     intros x7 x6 x5 x4.
     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_s_monotonic :
    forall x4 x5, (0 <= x5)/\ (x5 <= x4) ->P_id_s x5 <= P_id_s x4.
   Proof.
     intros x5 x4.
     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_not_monotonic :
    forall x4 x5, (0 <= x5)/\ (x5 <= x4) ->P_id_not x5 <= P_id_not x4.
   Proof.
     intros x5 x4.
     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_prime_bounded : forall x4, (0 <= x4) ->0 <= P_id_prime x4.
   Proof.
     intros .
     
     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
   Qed.
   
   Lemma P_id_divp_bounded :
    forall x4 x5, (0 <= x4) ->(0 <= x5) ->0 <= P_id_divp x5 x4.
   Proof.
     intros .
     
     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
   Qed.
   
   Lemma P_id_prime1_bounded :
    forall x4 x5, (0 <= x4) ->(0 <= x5) ->0 <= P_id_prime1 x5 x4.
   Proof.
     intros .
     
     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
   Qed.
   
   Lemma P_id_false_bounded : 0 <= P_id_false .
   Proof.
     intros .
     
     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
   Qed.
   
   Lemma P_id_rem_bounded :
    forall x4 x5, (0 <= x4) ->(0 <= x5) ->0 <= P_id_rem x5 x4.
   Proof.
     intros .
     
     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
   Qed.
   
   Lemma P_id_and_bounded :
    forall x4 x5, (0 <= x4) ->(0 <= x5) ->0 <= P_id_and x5 x4.
   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__equal__bounded :
    forall x4 x5, (0 <= x4) ->(0 <= x5) ->0 <= P_id__equal_ x5 x4.
   Proof.
     intros .
     
     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
   Qed.
   
   Lemma P_id_true_bounded : 0 <= P_id_true .
   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 x4, (0 <= x4) ->0 <= P_id_s x4.
   Proof.
     intros .
     
     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
   Qed.
   
   Lemma P_id_not_bounded : forall x4, (0 <= x4) ->0 <= P_id_not x4.
   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_prime P_id_divp P_id_prime1 P_id_false P_id_rem 
      P_id_and P_id_0 P_id__equal_ P_id_true P_id_s P_id_not.
   
   Lemma measure_equation :
    forall t, 
     measure t = match t with
                   | (algebra.Alg.Term algebra.F.id_prime (x4::nil)) =>
                    P_id_prime (measure x4)
                   | (algebra.Alg.Term algebra.F.id_divp (x5::x4::nil)) =>
                    P_id_divp (measure x5) (measure x4)
                   | (algebra.Alg.Term algebra.F.id_prime1 (x5::x4::nil)) =>
                    P_id_prime1 (measure x5) (measure x4)
                   | (algebra.Alg.Term algebra.F.id_false nil) => P_id_false 
                   | (algebra.Alg.Term algebra.F.id_rem (x5::x4::nil)) =>
                    P_id_rem (measure x5) (measure x4)
                   | (algebra.Alg.Term algebra.F.id_and (x5::x4::nil)) =>
                    P_id_and (measure x5) (measure x4)
                   | (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0 
                   | (algebra.Alg.Term algebra.F.id__equal_ (x5::x4::nil)) =>
                    P_id__equal_ (measure x5) (measure x4)
                   | (algebra.Alg.Term algebra.F.id_true nil) => P_id_true 
                   | (algebra.Alg.Term algebra.F.id_s (x4::nil)) =>
                    P_id_s (measure x4)
                   | (algebra.Alg.Term algebra.F.id_not (x4::nil)) =>
                    P_id_not (measure x4)
                   | _ => 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_prime_monotonic;assumption.
     intros ;apply P_id_divp_monotonic;assumption.
     intros ;apply P_id_prime1_monotonic;assumption.
     intros ;apply P_id_rem_monotonic;assumption.
     intros ;apply P_id_and_monotonic;assumption.
     intros ;apply P_id__equal__monotonic;assumption.
     intros ;apply P_id_s_monotonic;assumption.
     intros ;apply P_id_not_monotonic;assumption.
     intros ;apply P_id_prime_bounded;assumption.
     intros ;apply P_id_divp_bounded;assumption.
     intros ;apply P_id_prime1_bounded;assumption.
     intros ;apply P_id_false_bounded;assumption.
     intros ;apply P_id_rem_bounded;assumption.
     intros ;apply P_id_and_bounded;assumption.
     intros ;apply P_id_0_bounded;assumption.
     intros ;apply P_id__equal__bounded;assumption.
     intros ;apply P_id_true_bounded;assumption.
     intros ;apply P_id_s_bounded;assumption.
     intros ;apply P_id_not_bounded;assumption.
     apply rules_monotonic.
   Qed.
   
   Definition P_id_PRIME1 (x4:Z) (x5:Z) := 2* x5.
   
   Definition P_id_DIVP (x4:Z) (x5:Z) := 0.
   
   Definition P_id_PRIME (x4:Z) := 0.
   
   Lemma P_id_PRIME1_monotonic :
    forall x4 x6 x5 x7, 
     (0 <= x7)/\ (x7 <= x6) ->
      (0 <= x5)/\ (x5 <= x4) ->P_id_PRIME1 x5 x7 <= P_id_PRIME1 x4 x6.
   Proof.
     intros x7 x6 x5 x4.
     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_DIVP_monotonic :
    forall x4 x6 x5 x7, 
     (0 <= x7)/\ (x7 <= x6) ->
      (0 <= x5)/\ (x5 <= x4) ->P_id_DIVP x5 x7 <= P_id_DIVP x4 x6.
   Proof.
     intros x7 x6 x5 x4.
     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_PRIME_monotonic :
    forall x4 x5, (0 <= x5)/\ (x5 <= x4) ->P_id_PRIME x5 <= P_id_PRIME x4.
   Proof.
     intros x5 x4.
     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_prime P_id_divp P_id_prime1 P_id_false 
      P_id_rem P_id_and P_id_0 P_id__equal_ P_id_true P_id_s P_id_not 
      P_id_PRIME1 P_id_DIVP P_id_PRIME.
   
   Lemma marked_measure_equation :
    forall t, 
     marked_measure t = match t with
                          | (algebra.Alg.Term algebra.F.id_prime1 (x5::
                             x4::nil)) =>
                           P_id_PRIME1 (measure x5) (measure x4)
                          | (algebra.Alg.Term algebra.F.id_divp (x5::
                             x4::nil)) =>
                           P_id_DIVP (measure x5) (measure x4)
                          | (algebra.Alg.Term algebra.F.id_prime (x4::nil)) =>
                           P_id_PRIME (measure x4)
                          | _ => 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_prime_monotonic;assumption.
     intros ;apply P_id_divp_monotonic;assumption.
     intros ;apply P_id_prime1_monotonic;assumption.
     intros ;apply P_id_rem_monotonic;assumption.
     intros ;apply P_id_and_monotonic;assumption.
     intros ;apply P_id__equal__monotonic;assumption.
     intros ;apply P_id_s_monotonic;assumption.
     intros ;apply P_id_not_monotonic;assumption.
     intros ;apply P_id_prime_bounded;assumption.
     intros ;apply P_id_divp_bounded;assumption.
     intros ;apply P_id_prime1_bounded;assumption.
     intros ;apply P_id_false_bounded;assumption.
     intros ;apply P_id_rem_bounded;assumption.
     intros ;apply P_id_and_bounded;assumption.
     intros ;apply P_id_0_bounded;assumption.
     intros ;apply P_id__equal__bounded;assumption.
     intros ;apply P_id_true_bounded;assumption.
     intros ;apply P_id_s_bounded;assumption.
     intros ;apply P_id_not_bounded;assumption.
     apply rules_monotonic.
     intros ;apply P_id_PRIME1_monotonic;assumption.
     intros ;apply P_id_DIVP_monotonic;assumption.
     intros ;apply P_id_PRIME_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.DP_R_xml_0_scc_2.
   Proof.
     intros x.
     
     apply well_founded_ind with
       (R:=fun x y => (Zwf.Zwf 0) (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 0) (interp.o_Z 0) 
      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_scc_2.
  
  Definition wf_DP_R_xml_0_scc_2  := WF_DP_R_xml_0_scc_2.wf.
  
  
  Lemma acc_DP_R_xml_0_scc_2 :
   forall x y, (DP_R_xml_0_scc_2 x y) ->Acc WF_R_xml_0_deep_rew.DP_R_xml_0 x.
  Proof.
    intros x.
    pattern x.
    apply (@Acc_ind _ DP_R_xml_0_scc_2).
    intros x' _ Hrec y h.
    
    inversion h;clear h;subst;
     constructor;intros _y _h;inversion _h;clear _h;subst;
      (eapply Hrec;econstructor eassumption)||
      ((eapply acc_DP_R_xml_0_non_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' )))).
    apply wf_DP_R_xml_0_scc_2.
  Qed.
  
  
  Inductive DP_R_xml_0_non_scc_3  :
   algebra.Alg.term ->algebra.Alg.term ->Prop := 
     (* <prime(s(s(x_))),prime1(s(s(x_)),s(x_))> *)
    | DP_R_xml_0_non_scc_3_0 :
     forall x4 x1, 
      (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                 
        (algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Term algebra.F.id_s 
         (x1::nil))::nil)) x4) ->
       DP_R_xml_0_non_scc_3 (algebra.Alg.Term algebra.F.id_prime1 
                             ((algebra.Alg.Term algebra.F.id_s 
                             ((algebra.Alg.Term algebra.F.id_s 
                             (x1::nil))::nil))::(algebra.Alg.Term 
                             algebra.F.id_s (x1::nil))::nil)) 
        (algebra.Alg.Term algebra.F.id_prime (x4::nil))
  .
  
  
  Lemma acc_DP_R_xml_0_non_scc_3 :
   forall x y, 
    (DP_R_xml_0_non_scc_3 x y) ->Acc WF_R_xml_0_deep_rew.DP_R_xml_0 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_scc_2;
        econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
      ((eapply acc_DP_R_xml_0_non_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.
  
  
  Lemma wf : well_founded WF_R_xml_0_deep_rew.DP_R_xml_0.
  Proof.
    constructor;intros _y _h;inversion _h;clear _h;subst;
     (eapply acc_DP_R_xml_0_non_scc_3;
       econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
     ((eapply acc_DP_R_xml_0_non_scc_2;
        econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
      ((eapply acc_DP_R_xml_0_non_scc_1;
         econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
       ((eapply acc_DP_R_xml_0_non_scc_0;
          econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
        ((eapply acc_DP_R_xml_0_scc_2;
           econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
         ((eapply acc_DP_R_xml_0_scc_1;
            econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
          ((eapply acc_DP_R_xml_0_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.
 
 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___SK90___2.29.trs/a3pat.v" ***
*** End: ***
 *)