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_terms *)
    | id_terms : symb
     (* id_first *)
    | id_first : symb
     (* id_0 *)
    | id_0 : symb
     (* id_recip *)
    | id_recip : symb
     (* id_dbl *)
    | id_dbl : symb
     (* id_cons *)
    | id_cons : symb
     (* id_nil *)
    | id_nil : symb
     (* id_s *)
    | id_s : symb
     (* id_sqr *)
    | id_sqr : symb
     (* id_add *)
    | id_add : symb
  .
  
  
  Definition symb_eq_bool (f1 f2:symb) : bool := 
    match f1,f2 with
      | id_terms,id_terms => true
      | id_first,id_first => true
      | id_0,id_0 => true
      | id_recip,id_recip => true
      | id_dbl,id_dbl => true
      | id_cons,id_cons => true
      | id_nil,id_nil => true
      | id_s,id_s => true
      | id_sqr,id_sqr => true
      | id_add,id_add => 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_terms,id_terms => refl_equal _
             | id_first,id_first => refl_equal _
             | id_0,id_0 => refl_equal _
             | id_recip,id_recip => refl_equal _
             | id_dbl,id_dbl => refl_equal _
             | id_cons,id_cons => refl_equal _
             | id_nil,id_nil => refl_equal _
             | id_s,id_s => refl_equal _
             | id_sqr,id_sqr => refl_equal _
             | id_add,id_add => refl_equal _
             | _,_ => _
             end;intros abs;discriminate.
  Defined.
  
  
  Definition arity (f:symb) := 
    match f with
      | id_terms => term.Free 1
      | id_first => term.Free 2
      | id_0 => term.Free 0
      | id_recip => term.Free 1
      | id_dbl => term.Free 1
      | id_cons => term.Free 1
      | id_nil => term.Free 0
      | id_s => term.Free 0
      | id_sqr => term.Free 1
      | id_add => term.Free 2
      end.
  
  
  Definition symb_order (f1 f2:symb) : bool := 
    match f1,f2 with
      | id_terms,id_terms => true
      | id_terms,id_first => false
      | id_terms,id_0 => false
      | id_terms,id_recip => false
      | id_terms,id_dbl => false
      | id_terms,id_cons => false
      | id_terms,id_nil => false
      | id_terms,id_s => false
      | id_terms,id_sqr => false
      | id_terms,id_add => false
      | id_first,id_terms => true
      | id_first,id_first => true
      | id_first,id_0 => false
      | id_first,id_recip => false
      | id_first,id_dbl => false
      | id_first,id_cons => false
      | id_first,id_nil => false
      | id_first,id_s => false
      | id_first,id_sqr => false
      | id_first,id_add => false
      | id_0,id_terms => true
      | id_0,id_first => true
      | id_0,id_0 => true
      | id_0,id_recip => false
      | id_0,id_dbl => false
      | id_0,id_cons => false
      | id_0,id_nil => false
      | id_0,id_s => false
      | id_0,id_sqr => false
      | id_0,id_add => false
      | id_recip,id_terms => true
      | id_recip,id_first => true
      | id_recip,id_0 => true
      | id_recip,id_recip => true
      | id_recip,id_dbl => false
      | id_recip,id_cons => false
      | id_recip,id_nil => false
      | id_recip,id_s => false
      | id_recip,id_sqr => false
      | id_recip,id_add => false
      | id_dbl,id_terms => true
      | id_dbl,id_first => true
      | id_dbl,id_0 => true
      | id_dbl,id_recip => true
      | id_dbl,id_dbl => true
      | id_dbl,id_cons => false
      | id_dbl,id_nil => false
      | id_dbl,id_s => false
      | id_dbl,id_sqr => false
      | id_dbl,id_add => false
      | id_cons,id_terms => true
      | id_cons,id_first => true
      | id_cons,id_0 => true
      | id_cons,id_recip => true
      | id_cons,id_dbl => true
      | id_cons,id_cons => true
      | id_cons,id_nil => false
      | id_cons,id_s => false
      | id_cons,id_sqr => false
      | id_cons,id_add => false
      | id_nil,id_terms => true
      | id_nil,id_first => true
      | id_nil,id_0 => true
      | id_nil,id_recip => true
      | id_nil,id_dbl => true
      | id_nil,id_cons => true
      | id_nil,id_nil => true
      | id_nil,id_s => false
      | id_nil,id_sqr => false
      | id_nil,id_add => false
      | id_s,id_terms => true
      | id_s,id_first => true
      | id_s,id_0 => true
      | id_s,id_recip => true
      | id_s,id_dbl => true
      | id_s,id_cons => true
      | id_s,id_nil => true
      | id_s,id_s => true
      | id_s,id_sqr => false
      | id_s,id_add => false
      | id_sqr,id_terms => true
      | id_sqr,id_first => true
      | id_sqr,id_0 => true
      | id_sqr,id_recip => true
      | id_sqr,id_dbl => true
      | id_sqr,id_cons => true
      | id_sqr,id_nil => true
      | id_sqr,id_s => true
      | id_sqr,id_sqr => true
      | id_sqr,id_add => false
      | id_add,id_terms => true
      | id_add,id_first => true
      | id_add,id_0 => true
      | id_add,id_recip => true
      | id_add,id_dbl => true
      | id_add,id_cons => true
      | id_add,id_nil => true
      | id_add,id_s => true
      | id_add,id_sqr => true
      | id_add,id_add => 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 := 
    (* terms(N_) -> cons(recip(sqr(N_))) *)
   | R_xml_0_rule_0 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_cons ((algebra.Alg.Term 
                   algebra.F.id_recip ((algebra.Alg.Term algebra.F.id_sqr 
                   ((algebra.Alg.Var 1)::nil))::nil))::nil)) 
     (algebra.Alg.Term algebra.F.id_terms ((algebra.Alg.Var 1)::nil))
    (* sqr(0) -> 0 *)
   | R_xml_0_rule_1 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_0 nil) 
     (algebra.Alg.Term algebra.F.id_sqr ((algebra.Alg.Term algebra.F.id_0 
      nil)::nil))
    (* sqr(s) -> s *)
   | R_xml_0_rule_2 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_s nil) 
     (algebra.Alg.Term algebra.F.id_sqr ((algebra.Alg.Term algebra.F.id_s 
      nil)::nil))
    (* dbl(0) -> 0 *)
   | R_xml_0_rule_3 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_0 nil) 
     (algebra.Alg.Term algebra.F.id_dbl ((algebra.Alg.Term algebra.F.id_0 
      nil)::nil))
    (* dbl(s) -> s *)
   | R_xml_0_rule_4 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_s nil) 
     (algebra.Alg.Term algebra.F.id_dbl ((algebra.Alg.Term algebra.F.id_s 
      nil)::nil))
    (* add(0,X_) -> X_ *)
   | R_xml_0_rule_5 :
    R_xml_0_rules (algebra.Alg.Var 2) 
     (algebra.Alg.Term algebra.F.id_add ((algebra.Alg.Term algebra.F.id_0 
      nil)::(algebra.Alg.Var 2)::nil))
    (* add(s,Y_) -> s *)
   | R_xml_0_rule_6 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_s nil) 
     (algebra.Alg.Term algebra.F.id_add ((algebra.Alg.Term algebra.F.id_s 
      nil)::(algebra.Alg.Var 3)::nil))
    (* first(0,X_) -> nil *)
   | R_xml_0_rule_7 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_nil nil) 
     (algebra.Alg.Term algebra.F.id_first ((algebra.Alg.Term algebra.F.id_0 
      nil)::(algebra.Alg.Var 2)::nil))
    (* first(s,cons(Y_)) -> cons(Y_) *)
   | R_xml_0_rule_8 :
    R_xml_0_rules (algebra.Alg.Term algebra.F.id_cons 
                   ((algebra.Alg.Var 3)::nil)) 
     (algebra.Alg.Term algebra.F.id_first ((algebra.Alg.Term algebra.F.id_s 
      nil)::(algebra.Alg.Term algebra.F.id_cons 
      ((algebra.Alg.Var 3)::nil))::nil))
 .
 
 
 Definition R_xml_0_rule_as_list_0  := 
   ((algebra.Alg.Term algebra.F.id_terms ((algebra.Alg.Var 1)::nil)),
    (algebra.Alg.Term algebra.F.id_cons ((algebra.Alg.Term 
     algebra.F.id_recip ((algebra.Alg.Term algebra.F.id_sqr 
     ((algebra.Alg.Var 1)::nil))::nil))::nil)))::nil.
 
 
 Definition R_xml_0_rule_as_list_1  := 
   ((algebra.Alg.Term algebra.F.id_sqr ((algebra.Alg.Term algebra.F.id_0 
     nil)::nil)),(algebra.Alg.Term algebra.F.id_0 nil))::
    R_xml_0_rule_as_list_0.
 
 
 Definition R_xml_0_rule_as_list_2  := 
   ((algebra.Alg.Term algebra.F.id_sqr ((algebra.Alg.Term algebra.F.id_s 
     nil)::nil)),(algebra.Alg.Term algebra.F.id_s nil))::
    R_xml_0_rule_as_list_1.
 
 
 Definition R_xml_0_rule_as_list_3  := 
   ((algebra.Alg.Term algebra.F.id_dbl ((algebra.Alg.Term algebra.F.id_0 
     nil)::nil)),(algebra.Alg.Term algebra.F.id_0 nil))::
    R_xml_0_rule_as_list_2.
 
 
 Definition R_xml_0_rule_as_list_4  := 
   ((algebra.Alg.Term algebra.F.id_dbl ((algebra.Alg.Term algebra.F.id_s 
     nil)::nil)),(algebra.Alg.Term algebra.F.id_s nil))::
    R_xml_0_rule_as_list_3.
 
 
 Definition R_xml_0_rule_as_list_5  := 
   ((algebra.Alg.Term algebra.F.id_add ((algebra.Alg.Term algebra.F.id_0 
     nil)::(algebra.Alg.Var 2)::nil)),(algebra.Alg.Var 2))::
    R_xml_0_rule_as_list_4.
 
 
 Definition R_xml_0_rule_as_list_6  := 
   ((algebra.Alg.Term algebra.F.id_add ((algebra.Alg.Term algebra.F.id_s 
     nil)::(algebra.Alg.Var 3)::nil)),(algebra.Alg.Term algebra.F.id_s nil))::
    R_xml_0_rule_as_list_5.
 
 
 Definition R_xml_0_rule_as_list_7  := 
   ((algebra.Alg.Term algebra.F.id_first ((algebra.Alg.Term algebra.F.id_0 
     nil)::(algebra.Alg.Var 2)::nil)),
    (algebra.Alg.Term algebra.F.id_nil nil))::R_xml_0_rule_as_list_6.
 
 
 Definition R_xml_0_rule_as_list_8  := 
   ((algebra.Alg.Term algebra.F.id_first ((algebra.Alg.Term algebra.F.id_s 
     nil)::(algebra.Alg.Term algebra.F.id_cons 
     ((algebra.Alg.Var 3)::nil))::nil)),
    (algebra.Alg.Term algebra.F.id_cons ((algebra.Alg.Var 3)::nil)))::
    R_xml_0_rule_as_list_7.
 
 Definition R_xml_0_rule_as_list  := R_xml_0_rule_as_list_8.
 
 
 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.or10_equiv in H|-.
   case H;clear H;intros H.
   injection H;intros ;subst;constructor 9.
   injection H;intros ;subst;constructor 8.
   injection H;intros ;subst;constructor 7.
   injection H;intros ;subst;constructor 6.
   injection H;intros ;subst;constructor 5.
   injection H;intros ;subst;constructor 4.
   injection H;intros ;subst;constructor 3.
   injection H;intros ;subst;constructor 2.
   injection H;intros ;subst;constructor 1.
   elim H.
 Qed.
 
 
 Lemma R_xml_0_non_var : forall x t, ~R_xml_0_rules t (algebra.EQT.T.Var x).
 Proof.
   intros x t H.
   inversion H.
 Qed.
 
 
 Lemma R_xml_0_reg :
  forall s t, 
   (R_xml_0_rules s t) ->
    forall x, In x (algebra.Alg.var_list s) ->In x (algebra.Alg.var_list t).
 Proof.
   intros s t H.
   
   inversion H;intros x Hx;
    (apply (more_list.mem_impl_in (@eq algebra.Alg.variable));[tauto|idtac]);
    apply (more_list.in_impl_mem (@eq algebra.Alg.variable)) in Hx;
    vm_compute in Hx|-*;tauto.
 Qed.
 
 
 Inductive and_5 (x5 x6 x7 x8 x9:Prop) :
  Prop := 
   | conj_5 : x5->x6->x7->x8->x9->and_5 x5 x6 x7 x8 x9
 .
 
 
 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_5 (t = (algebra.Alg.Term algebra.F.id_0 nil) ->
           t' = (algebra.Alg.Term algebra.F.id_0 nil)) 
     (forall x6, 
      t = (algebra.Alg.Term algebra.F.id_recip (x6::nil)) ->
       exists x5,
         t' = (algebra.Alg.Term algebra.F.id_recip (x5::nil))/\ 
         (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x5 x6)) 
     
     (forall x6, 
      t = (algebra.Alg.Term algebra.F.id_cons (x6::nil)) ->
       exists x5,
         t' = (algebra.Alg.Term algebra.F.id_cons (x5::nil))/\ 
         (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x5 x6)) 
     
     (t = (algebra.Alg.Term algebra.F.id_nil nil) ->
      t' = (algebra.Alg.Term algebra.F.id_nil nil)) 
     (t = (algebra.Alg.Term algebra.F.id_s nil) ->
      t' = (algebra.Alg.Term algebra.F.id_s nil)).
 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 x6 H;exists x6;intuition;constructor 1.
   intros x6 H;exists x6;intuition;constructor 1.
   intros H;intuition;constructor 1.
   intros H;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_0 H_id_recip H_id_cons H_id_nil H_id_s].
   constructor.
   
   clear H_id_recip H_id_cons H_id_nil H_id_s;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_0 H_id_cons H_id_nil H_id_s;intros x6 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 x6 |- _ =>
      destruct (H_id_recip y (refl_equal _)) as [x5];intros ;intuition;
       exists x5;intuition;eapply closure_extension.refl_trans_clos_R;
       eassumption
     end
   .
   
   clear H_id_0 H_id_recip H_id_nil H_id_s;intros x6 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 x6 |- _ =>
      destruct (H_id_cons y (refl_equal _)) as [x5];intros ;intuition;
       exists x5;intuition;eapply closure_extension.refl_trans_clos_R;
       eassumption
     end
   .
   
   clear H_id_0 H_id_recip H_id_cons H_id_s;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_0 H_id_recip H_id_cons H_id_nil;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
    ).
 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_recip_is_R_xml_0_constructor :
  forall t t', 
   (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
    forall x6, 
     t = (algebra.Alg.Term algebra.F.id_recip (x6::nil)) ->
      exists x5,
        t' = (algebra.Alg.Term algebra.F.id_recip (x5::nil))/\ 
        (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x5 x6).
 Proof.
   intros t t' H.
   destruct (are_constuctors_of_R_xml_0 H).
   assumption.
 Qed.
 
 
 Lemma id_cons_is_R_xml_0_constructor :
  forall t t', 
   (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
    forall x6, 
     t = (algebra.Alg.Term algebra.F.id_cons (x6::nil)) ->
      exists x5,
        t' = (algebra.Alg.Term algebra.F.id_cons (x5::nil))/\ 
        (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x5 x6).
 Proof.
   intros t t' H.
   destruct (are_constuctors_of_R_xml_0 H).
   assumption.
 Qed.
 
 
 Lemma id_nil_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_nil nil) ->
     t' = (algebra.Alg.Term algebra.F.id_nil 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) ->
    t = (algebra.Alg.Term algebra.F.id_s nil) ->
     t' = (algebra.Alg.Term algebra.F.id_s nil).
 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_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_recip (?x5::nil)) |- _ =>
     let x5 := fresh "x" in 
      (let Heq := fresh "Heq" in 
        (let Hred1 := fresh "Hred" in 
          (destruct (id_recip_is_R_xml_0_constructor H (refl_equal _)) as 
           [x5 [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_cons (?x5::nil)) |- _ =>
     let x5 := fresh "x" in 
      (let Heq := fresh "Heq" in 
        (let Hred1 := fresh "Hred" in 
          (destruct (id_cons_is_R_xml_0_constructor H (refl_equal _)) as 
           [x5 [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_nil nil) |- _ =>
     let Heq := fresh "Heq" in 
      (set (Heq:=id_nil_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 nil) |- _ =>
     let Heq := fresh "Heq" in 
      (set (Heq:=id_s_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 ))
    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_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_recip (?x5::nil)) |- _ =>
     let x5 := fresh "x" in 
      (let Heq := fresh "Heq" in 
        (let Hred1 := fresh "Hred" in 
          (destruct (id_recip_is_R_xml_0_constructor H (refl_equal _)) as 
           [x5 [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_cons (?x5::nil)) |- _ =>
     let x5 := fresh "x" in 
      (let Heq := fresh "Heq" in 
        (let Hred1 := fresh "Hred" in 
          (destruct (id_cons_is_R_xml_0_constructor H (refl_equal _)) as 
           [x5 [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_nil nil) |- _ =>
     let Heq := fresh "Heq" in 
      (set (Heq:=id_nil_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 nil) |- _ =>
     let Heq := fresh "Heq" in 
      (set (Heq:=id_s_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 )))
    end
  .
End R_xml_0_deep_rew.

Module WF_R_xml_0_deep_rew.
 Inductive DP_R_xml_0  :
  algebra.Alg.term ->algebra.Alg.term ->Prop := 
    (* <terms(N_),sqr(N_)> *)
   | DP_R_xml_0_0 :
    forall x1 x5, 
     (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                x1 x5) ->
      DP_R_xml_0 (algebra.Alg.Term algebra.F.id_sqr (x1::nil)) 
       (algebra.Alg.Term algebra.F.id_terms (x5::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 := 
     (* <terms(N_),sqr(N_)> *)
    | DP_R_xml_0_non_scc_1_0 :
     forall x1 x5, 
      (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
                                 x1 x5) ->
       DP_R_xml_0_non_scc_1 (algebra.Alg.Term algebra.F.id_sqr (x1::nil)) 
        (algebra.Alg.Term algebra.F.id_terms (x5::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.
  
  
  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_1;
       econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
     ((eapply acc_DP_R_xml_0_non_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___TRCSR___Ex26_Luc03b_L.trs/a3pat.v" ***
*** End: ***
 *)