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__plus_ *)
| id__plus_ : symb
(* id_7 *)
| id_7 : symb
(* id_3 *)
| id_3 : symb
(* id_1 *)
| id_1 : symb
(* id_9 *)
| id_9 : symb
(* id_5 *)
| id_5 : symb
(* id_0 *)
| id_0 : symb
(* id_8 *)
| id_8 : symb
(* id_4 *)
| id_4 : symb
(* id_2 *)
| id_2 : symb
(* id_c *)
| id_c : symb
(* id_6 *)
| id_6 : symb
.
Definition symb_eq_bool (f1 f2:symb) : bool :=
match f1,f2 with
| id__plus_,id__plus_ => true
| id_7,id_7 => true
| id_3,id_3 => true
| id_1,id_1 => true
| id_9,id_9 => true
| id_5,id_5 => true
| id_0,id_0 => true
| id_8,id_8 => true
| id_4,id_4 => true
| id_2,id_2 => true
| id_c,id_c => true
| id_6,id_6 => 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__plus_,id__plus_ => refl_equal _
| id_7,id_7 => refl_equal _
| id_3,id_3 => refl_equal _
| id_1,id_1 => refl_equal _
| id_9,id_9 => refl_equal _
| id_5,id_5 => refl_equal _
| id_0,id_0 => refl_equal _
| id_8,id_8 => refl_equal _
| id_4,id_4 => refl_equal _
| id_2,id_2 => refl_equal _
| id_c,id_c => refl_equal _
| id_6,id_6 => refl_equal _
| _,_ => _
end;intros abs;discriminate.
Defined.
Definition arity (f:symb) :=
match f with
| id__plus_ => term.Free 2
| id_7 => term.Free 0
| id_3 => term.Free 0
| id_1 => term.Free 0
| id_9 => term.Free 0
| id_5 => term.Free 0
| id_0 => term.Free 0
| id_8 => term.Free 0
| id_4 => term.Free 0
| id_2 => term.Free 0
| id_c => term.Free 2
| id_6 => term.Free 0
end.
Definition symb_order (f1 f2:symb) : bool :=
match f1,f2 with
| id__plus_,id__plus_ => true
| id__plus_,id_7 => false
| id__plus_,id_3 => false
| id__plus_,id_1 => false
| id__plus_,id_9 => false
| id__plus_,id_5 => false
| id__plus_,id_0 => false
| id__plus_,id_8 => false
| id__plus_,id_4 => false
| id__plus_,id_2 => false
| id__plus_,id_c => false
| id__plus_,id_6 => false
| id_7,id__plus_ => true
| id_7,id_7 => true
| id_7,id_3 => false
| id_7,id_1 => false
| id_7,id_9 => false
| id_7,id_5 => false
| id_7,id_0 => false
| id_7,id_8 => false
| id_7,id_4 => false
| id_7,id_2 => false
| id_7,id_c => false
| id_7,id_6 => false
| id_3,id__plus_ => true
| id_3,id_7 => true
| id_3,id_3 => true
| id_3,id_1 => false
| id_3,id_9 => false
| id_3,id_5 => false
| id_3,id_0 => false
| id_3,id_8 => false
| id_3,id_4 => false
| id_3,id_2 => false
| id_3,id_c => false
| id_3,id_6 => false
| id_1,id__plus_ => true
| id_1,id_7 => true
| id_1,id_3 => true
| id_1,id_1 => true
| id_1,id_9 => false
| id_1,id_5 => false
| id_1,id_0 => false
| id_1,id_8 => false
| id_1,id_4 => false
| id_1,id_2 => false
| id_1,id_c => false
| id_1,id_6 => false
| id_9,id__plus_ => true
| id_9,id_7 => true
| id_9,id_3 => true
| id_9,id_1 => true
| id_9,id_9 => true
| id_9,id_5 => false
| id_9,id_0 => false
| id_9,id_8 => false
| id_9,id_4 => false
| id_9,id_2 => false
| id_9,id_c => false
| id_9,id_6 => false
| id_5,id__plus_ => true
| id_5,id_7 => true
| id_5,id_3 => true
| id_5,id_1 => true
| id_5,id_9 => true
| id_5,id_5 => true
| id_5,id_0 => false
| id_5,id_8 => false
| id_5,id_4 => false
| id_5,id_2 => false
| id_5,id_c => false
| id_5,id_6 => false
| id_0,id__plus_ => true
| id_0,id_7 => true
| id_0,id_3 => true
| id_0,id_1 => true
| id_0,id_9 => true
| id_0,id_5 => true
| id_0,id_0 => true
| id_0,id_8 => false
| id_0,id_4 => false
| id_0,id_2 => false
| id_0,id_c => false
| id_0,id_6 => false
| id_8,id__plus_ => true
| id_8,id_7 => true
| id_8,id_3 => true
| id_8,id_1 => true
| id_8,id_9 => true
| id_8,id_5 => true
| id_8,id_0 => true
| id_8,id_8 => true
| id_8,id_4 => false
| id_8,id_2 => false
| id_8,id_c => false
| id_8,id_6 => false
| id_4,id__plus_ => true
| id_4,id_7 => true
| id_4,id_3 => true
| id_4,id_1 => true
| id_4,id_9 => true
| id_4,id_5 => true
| id_4,id_0 => true
| id_4,id_8 => true
| id_4,id_4 => true
| id_4,id_2 => false
| id_4,id_c => false
| id_4,id_6 => false
| id_2,id__plus_ => true
| id_2,id_7 => true
| id_2,id_3 => true
| id_2,id_1 => true
| id_2,id_9 => true
| id_2,id_5 => true
| id_2,id_0 => true
| id_2,id_8 => true
| id_2,id_4 => true
| id_2,id_2 => true
| id_2,id_c => false
| id_2,id_6 => false
| id_c,id__plus_ => true
| id_c,id_7 => true
| id_c,id_3 => true
| id_c,id_1 => true
| id_c,id_9 => true
| id_c,id_5 => true
| id_c,id_0 => true
| id_c,id_8 => true
| id_c,id_4 => true
| id_c,id_2 => true
| id_c,id_c => true
| id_c,id_6 => false
| id_6,id__plus_ => true
| id_6,id_7 => true
| id_6,id_3 => true
| id_6,id_1 => true
| id_6,id_9 => true
| id_6,id_5 => true
| id_6,id_0 => true
| id_6,id_8 => true
| id_6,id_4 => true
| id_6,id_2 => true
| id_6,id_c => true
| id_6,id_6 => 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 :=
(* +(0,0) -> 0 *)
| R_xml_0_rule_0 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_0 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_0
nil)::(algebra.Alg.Term algebra.F.id_0 nil)::nil))
(* +(0,1) -> 1 *)
| R_xml_0_rule_1 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_1 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_0
nil)::(algebra.Alg.Term algebra.F.id_1 nil)::nil))
(* +(0,2) -> 2 *)
| R_xml_0_rule_2 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_2 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_0
nil)::(algebra.Alg.Term algebra.F.id_2 nil)::nil))
(* +(0,3) -> 3 *)
| R_xml_0_rule_3 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_3 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_0
nil)::(algebra.Alg.Term algebra.F.id_3 nil)::nil))
(* +(0,4) -> 4 *)
| R_xml_0_rule_4 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_4 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_0
nil)::(algebra.Alg.Term algebra.F.id_4 nil)::nil))
(* +(0,5) -> 5 *)
| R_xml_0_rule_5 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_5 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_0
nil)::(algebra.Alg.Term algebra.F.id_5 nil)::nil))
(* +(0,6) -> 6 *)
| R_xml_0_rule_6 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_6 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_0
nil)::(algebra.Alg.Term algebra.F.id_6 nil)::nil))
(* +(0,7) -> 7 *)
| R_xml_0_rule_7 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_7 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_0
nil)::(algebra.Alg.Term algebra.F.id_7 nil)::nil))
(* +(0,8) -> 8 *)
| R_xml_0_rule_8 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_8 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_0
nil)::(algebra.Alg.Term algebra.F.id_8 nil)::nil))
(* +(0,9) -> 9 *)
| R_xml_0_rule_9 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_9 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_0
nil)::(algebra.Alg.Term algebra.F.id_9 nil)::nil))
(* +(1,0) -> 1 *)
| R_xml_0_rule_10 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_1 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_1
nil)::(algebra.Alg.Term algebra.F.id_0 nil)::nil))
(* +(1,1) -> 2 *)
| R_xml_0_rule_11 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_2 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_1
nil)::(algebra.Alg.Term algebra.F.id_1 nil)::nil))
(* +(1,2) -> 3 *)
| R_xml_0_rule_12 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_3 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_1
nil)::(algebra.Alg.Term algebra.F.id_2 nil)::nil))
(* +(1,3) -> 4 *)
| R_xml_0_rule_13 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_4 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_1
nil)::(algebra.Alg.Term algebra.F.id_3 nil)::nil))
(* +(1,4) -> 5 *)
| R_xml_0_rule_14 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_5 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_1
nil)::(algebra.Alg.Term algebra.F.id_4 nil)::nil))
(* +(1,5) -> 6 *)
| R_xml_0_rule_15 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_6 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_1
nil)::(algebra.Alg.Term algebra.F.id_5 nil)::nil))
(* +(1,6) -> 7 *)
| R_xml_0_rule_16 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_7 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_1
nil)::(algebra.Alg.Term algebra.F.id_6 nil)::nil))
(* +(1,7) -> 8 *)
| R_xml_0_rule_17 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_8 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_1
nil)::(algebra.Alg.Term algebra.F.id_7 nil)::nil))
(* +(1,8) -> 9 *)
| R_xml_0_rule_18 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_9 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_1
nil)::(algebra.Alg.Term algebra.F.id_8 nil)::nil))
(* +(1,9) -> c(1,0) *)
| R_xml_0_rule_19 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_0
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_1
nil)::(algebra.Alg.Term algebra.F.id_9 nil)::nil))
(* +(2,0) -> 2 *)
| R_xml_0_rule_20 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_2 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_2
nil)::(algebra.Alg.Term algebra.F.id_0 nil)::nil))
(* +(2,1) -> 3 *)
| R_xml_0_rule_21 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_3 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_2
nil)::(algebra.Alg.Term algebra.F.id_1 nil)::nil))
(* +(2,2) -> 4 *)
| R_xml_0_rule_22 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_4 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_2
nil)::(algebra.Alg.Term algebra.F.id_2 nil)::nil))
(* +(2,3) -> 5 *)
| R_xml_0_rule_23 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_5 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_2
nil)::(algebra.Alg.Term algebra.F.id_3 nil)::nil))
(* +(2,4) -> 6 *)
| R_xml_0_rule_24 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_6 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_2
nil)::(algebra.Alg.Term algebra.F.id_4 nil)::nil))
(* +(2,5) -> 7 *)
| R_xml_0_rule_25 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_7 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_2
nil)::(algebra.Alg.Term algebra.F.id_5 nil)::nil))
(* +(2,6) -> 8 *)
| R_xml_0_rule_26 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_8 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_2
nil)::(algebra.Alg.Term algebra.F.id_6 nil)::nil))
(* +(2,7) -> 9 *)
| R_xml_0_rule_27 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_9 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_2
nil)::(algebra.Alg.Term algebra.F.id_7 nil)::nil))
(* +(2,8) -> c(1,0) *)
| R_xml_0_rule_28 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_0
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_2
nil)::(algebra.Alg.Term algebra.F.id_8 nil)::nil))
(* +(2,9) -> c(1,1) *)
| R_xml_0_rule_29 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_1
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_2
nil)::(algebra.Alg.Term algebra.F.id_9 nil)::nil))
(* +(3,0) -> 3 *)
| R_xml_0_rule_30 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_3 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_3
nil)::(algebra.Alg.Term algebra.F.id_0 nil)::nil))
(* +(3,1) -> 4 *)
| R_xml_0_rule_31 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_4 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_3
nil)::(algebra.Alg.Term algebra.F.id_1 nil)::nil))
(* +(3,2) -> 5 *)
| R_xml_0_rule_32 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_5 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_3
nil)::(algebra.Alg.Term algebra.F.id_2 nil)::nil))
(* +(3,3) -> 6 *)
| R_xml_0_rule_33 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_6 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_3
nil)::(algebra.Alg.Term algebra.F.id_3 nil)::nil))
(* +(3,4) -> 7 *)
| R_xml_0_rule_34 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_7 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_3
nil)::(algebra.Alg.Term algebra.F.id_4 nil)::nil))
(* +(3,5) -> 8 *)
| R_xml_0_rule_35 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_8 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_3
nil)::(algebra.Alg.Term algebra.F.id_5 nil)::nil))
(* +(3,6) -> 9 *)
| R_xml_0_rule_36 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_9 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_3
nil)::(algebra.Alg.Term algebra.F.id_6 nil)::nil))
(* +(3,7) -> c(1,0) *)
| R_xml_0_rule_37 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_0
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_3
nil)::(algebra.Alg.Term algebra.F.id_7 nil)::nil))
(* +(3,8) -> c(1,1) *)
| R_xml_0_rule_38 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_1
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_3
nil)::(algebra.Alg.Term algebra.F.id_8 nil)::nil))
(* +(3,9) -> c(1,2) *)
| R_xml_0_rule_39 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_2
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_3
nil)::(algebra.Alg.Term algebra.F.id_9 nil)::nil))
(* +(4,0) -> 4 *)
| R_xml_0_rule_40 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_4 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_4
nil)::(algebra.Alg.Term algebra.F.id_0 nil)::nil))
(* +(4,1) -> 5 *)
| R_xml_0_rule_41 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_5 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_4
nil)::(algebra.Alg.Term algebra.F.id_1 nil)::nil))
(* +(4,2) -> 6 *)
| R_xml_0_rule_42 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_6 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_4
nil)::(algebra.Alg.Term algebra.F.id_2 nil)::nil))
(* +(4,3) -> 7 *)
| R_xml_0_rule_43 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_7 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_4
nil)::(algebra.Alg.Term algebra.F.id_3 nil)::nil))
(* +(4,4) -> 8 *)
| R_xml_0_rule_44 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_8 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_4
nil)::(algebra.Alg.Term algebra.F.id_4 nil)::nil))
(* +(4,5) -> 9 *)
| R_xml_0_rule_45 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_9 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_4
nil)::(algebra.Alg.Term algebra.F.id_5 nil)::nil))
(* +(4,6) -> c(1,0) *)
| R_xml_0_rule_46 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_0
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_4
nil)::(algebra.Alg.Term algebra.F.id_6 nil)::nil))
(* +(4,7) -> c(1,1) *)
| R_xml_0_rule_47 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_1
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_4
nil)::(algebra.Alg.Term algebra.F.id_7 nil)::nil))
(* +(4,8) -> c(1,2) *)
| R_xml_0_rule_48 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_2
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_4
nil)::(algebra.Alg.Term algebra.F.id_8 nil)::nil))
(* +(4,9) -> c(1,3) *)
| R_xml_0_rule_49 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_3
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_4
nil)::(algebra.Alg.Term algebra.F.id_9 nil)::nil))
(* +(5,0) -> 5 *)
| R_xml_0_rule_50 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_5 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_5
nil)::(algebra.Alg.Term algebra.F.id_0 nil)::nil))
(* +(5,1) -> 6 *)
| R_xml_0_rule_51 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_6 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_5
nil)::(algebra.Alg.Term algebra.F.id_1 nil)::nil))
(* +(5,2) -> 7 *)
| R_xml_0_rule_52 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_7 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_5
nil)::(algebra.Alg.Term algebra.F.id_2 nil)::nil))
(* +(5,3) -> 8 *)
| R_xml_0_rule_53 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_8 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_5
nil)::(algebra.Alg.Term algebra.F.id_3 nil)::nil))
(* +(5,4) -> 9 *)
| R_xml_0_rule_54 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_9 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_5
nil)::(algebra.Alg.Term algebra.F.id_4 nil)::nil))
(* +(5,5) -> c(1,0) *)
| R_xml_0_rule_55 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_0
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_5
nil)::(algebra.Alg.Term algebra.F.id_5 nil)::nil))
(* +(5,6) -> c(1,1) *)
| R_xml_0_rule_56 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_1
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_5
nil)::(algebra.Alg.Term algebra.F.id_6 nil)::nil))
(* +(5,7) -> c(1,2) *)
| R_xml_0_rule_57 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_2
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_5
nil)::(algebra.Alg.Term algebra.F.id_7 nil)::nil))
(* +(5,8) -> c(1,3) *)
| R_xml_0_rule_58 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_3
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_5
nil)::(algebra.Alg.Term algebra.F.id_8 nil)::nil))
(* +(5,9) -> c(1,4) *)
| R_xml_0_rule_59 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_4
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_5
nil)::(algebra.Alg.Term algebra.F.id_9 nil)::nil))
(* +(6,0) -> 6 *)
| R_xml_0_rule_60 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_6 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_6
nil)::(algebra.Alg.Term algebra.F.id_0 nil)::nil))
(* +(6,1) -> 7 *)
| R_xml_0_rule_61 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_7 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_6
nil)::(algebra.Alg.Term algebra.F.id_1 nil)::nil))
(* +(6,2) -> 8 *)
| R_xml_0_rule_62 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_8 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_6
nil)::(algebra.Alg.Term algebra.F.id_2 nil)::nil))
(* +(6,3) -> 9 *)
| R_xml_0_rule_63 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_9 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_6
nil)::(algebra.Alg.Term algebra.F.id_3 nil)::nil))
(* +(6,4) -> c(1,0) *)
| R_xml_0_rule_64 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_0
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_6
nil)::(algebra.Alg.Term algebra.F.id_4 nil)::nil))
(* +(6,5) -> c(1,1) *)
| R_xml_0_rule_65 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_1
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_6
nil)::(algebra.Alg.Term algebra.F.id_5 nil)::nil))
(* +(6,6) -> c(1,2) *)
| R_xml_0_rule_66 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_2
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_6
nil)::(algebra.Alg.Term algebra.F.id_6 nil)::nil))
(* +(6,7) -> c(1,3) *)
| R_xml_0_rule_67 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_3
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_6
nil)::(algebra.Alg.Term algebra.F.id_7 nil)::nil))
(* +(6,8) -> c(1,4) *)
| R_xml_0_rule_68 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_4
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_6
nil)::(algebra.Alg.Term algebra.F.id_8 nil)::nil))
(* +(6,9) -> c(1,5) *)
| R_xml_0_rule_69 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_5
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_6
nil)::(algebra.Alg.Term algebra.F.id_9 nil)::nil))
(* +(7,0) -> 7 *)
| R_xml_0_rule_70 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_7 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_7
nil)::(algebra.Alg.Term algebra.F.id_0 nil)::nil))
(* +(7,1) -> 8 *)
| R_xml_0_rule_71 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_8 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_7
nil)::(algebra.Alg.Term algebra.F.id_1 nil)::nil))
(* +(7,2) -> 9 *)
| R_xml_0_rule_72 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_9 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_7
nil)::(algebra.Alg.Term algebra.F.id_2 nil)::nil))
(* +(7,3) -> c(1,0) *)
| R_xml_0_rule_73 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_0
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_7
nil)::(algebra.Alg.Term algebra.F.id_3 nil)::nil))
(* +(7,4) -> c(1,1) *)
| R_xml_0_rule_74 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_1
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_7
nil)::(algebra.Alg.Term algebra.F.id_4 nil)::nil))
(* +(7,5) -> c(1,2) *)
| R_xml_0_rule_75 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_2
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_7
nil)::(algebra.Alg.Term algebra.F.id_5 nil)::nil))
(* +(7,6) -> c(1,3) *)
| R_xml_0_rule_76 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_3
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_7
nil)::(algebra.Alg.Term algebra.F.id_6 nil)::nil))
(* +(7,7) -> c(1,4) *)
| R_xml_0_rule_77 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_4
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_7
nil)::(algebra.Alg.Term algebra.F.id_7 nil)::nil))
(* +(7,8) -> c(1,5) *)
| R_xml_0_rule_78 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_5
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_7
nil)::(algebra.Alg.Term algebra.F.id_8 nil)::nil))
(* +(7,9) -> c(1,6) *)
| R_xml_0_rule_79 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_6
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_7
nil)::(algebra.Alg.Term algebra.F.id_9 nil)::nil))
(* +(8,0) -> 8 *)
| R_xml_0_rule_80 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_8 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_8
nil)::(algebra.Alg.Term algebra.F.id_0 nil)::nil))
(* +(8,1) -> 9 *)
| R_xml_0_rule_81 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_9 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_8
nil)::(algebra.Alg.Term algebra.F.id_1 nil)::nil))
(* +(8,2) -> c(1,0) *)
| R_xml_0_rule_82 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_0
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_8
nil)::(algebra.Alg.Term algebra.F.id_2 nil)::nil))
(* +(8,3) -> c(1,1) *)
| R_xml_0_rule_83 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_1
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_8
nil)::(algebra.Alg.Term algebra.F.id_3 nil)::nil))
(* +(8,4) -> c(1,2) *)
| R_xml_0_rule_84 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_2
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_8
nil)::(algebra.Alg.Term algebra.F.id_4 nil)::nil))
(* +(8,5) -> c(1,3) *)
| R_xml_0_rule_85 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_3
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_8
nil)::(algebra.Alg.Term algebra.F.id_5 nil)::nil))
(* +(8,6) -> c(1,4) *)
| R_xml_0_rule_86 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_4
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_8
nil)::(algebra.Alg.Term algebra.F.id_6 nil)::nil))
(* +(8,7) -> c(1,5) *)
| R_xml_0_rule_87 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_5
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_8
nil)::(algebra.Alg.Term algebra.F.id_7 nil)::nil))
(* +(8,8) -> c(1,6) *)
| R_xml_0_rule_88 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_6
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_8
nil)::(algebra.Alg.Term algebra.F.id_8 nil)::nil))
(* +(8,9) -> c(1,7) *)
| R_xml_0_rule_89 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_7
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_8
nil)::(algebra.Alg.Term algebra.F.id_9 nil)::nil))
(* +(9,0) -> 9 *)
| R_xml_0_rule_90 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_9 nil)
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_9
nil)::(algebra.Alg.Term algebra.F.id_0 nil)::nil))
(* +(9,1) -> c(1,0) *)
| R_xml_0_rule_91 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_0
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_9
nil)::(algebra.Alg.Term algebra.F.id_1 nil)::nil))
(* +(9,2) -> c(1,1) *)
| R_xml_0_rule_92 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_1
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_9
nil)::(algebra.Alg.Term algebra.F.id_2 nil)::nil))
(* +(9,3) -> c(1,2) *)
| R_xml_0_rule_93 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_2
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_9
nil)::(algebra.Alg.Term algebra.F.id_3 nil)::nil))
(* +(9,4) -> c(1,3) *)
| R_xml_0_rule_94 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_3
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_9
nil)::(algebra.Alg.Term algebra.F.id_4 nil)::nil))
(* +(9,5) -> c(1,4) *)
| R_xml_0_rule_95 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_4
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_9
nil)::(algebra.Alg.Term algebra.F.id_5 nil)::nil))
(* +(9,6) -> c(1,5) *)
| R_xml_0_rule_96 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_5
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_9
nil)::(algebra.Alg.Term algebra.F.id_6 nil)::nil))
(* +(9,7) -> c(1,6) *)
| R_xml_0_rule_97 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_6
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_9
nil)::(algebra.Alg.Term algebra.F.id_7 nil)::nil))
(* +(9,8) -> c(1,7) *)
| R_xml_0_rule_98 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_7
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_9
nil)::(algebra.Alg.Term algebra.F.id_8 nil)::nil))
(* +(9,9) -> c(1,8) *)
| R_xml_0_rule_99 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_8
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_9
nil)::(algebra.Alg.Term algebra.F.id_9 nil)::nil))
(* +(x_,c(y_,z_)) -> c(y_,+(x_,z_)) *)
| R_xml_0_rule_100 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Var 2)::
(algebra.Alg.Term algebra.F.id__plus_
((algebra.Alg.Var 1)::(algebra.Alg.Var 3)::nil))::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Var 1)::
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Var 2)::
(algebra.Alg.Var 3)::nil))::nil))
(* +(c(x_,y_),z_) -> c(x_,+(y_,z_)) *)
| R_xml_0_rule_101 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Var 1)::
(algebra.Alg.Term algebra.F.id__plus_
((algebra.Alg.Var 2)::(algebra.Alg.Var 3)::nil))::nil))
(algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Var 1)::(algebra.Alg.Var 2)::nil))::
(algebra.Alg.Var 3)::nil))
(* c(0,x_) -> x_ *)
| R_xml_0_rule_102 :
R_xml_0_rules (algebra.Alg.Var 1)
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_0
nil)::(algebra.Alg.Var 1)::nil))
(* c(x_,c(y_,z_)) -> c(+(x_,y_),z_) *)
| R_xml_0_rule_103 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id__plus_ ((algebra.Alg.Var 1)::
(algebra.Alg.Var 2)::nil))::(algebra.Alg.Var 3)::nil))
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Var 1)::
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Var 2)::
(algebra.Alg.Var 3)::nil))::nil))
.
Definition R_xml_0_rule_as_list_0 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_0
nil)::(algebra.Alg.Term algebra.F.id_0 nil)::nil)),
(algebra.Alg.Term algebra.F.id_0 nil))::nil.
Definition R_xml_0_rule_as_list_1 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_0
nil)::(algebra.Alg.Term algebra.F.id_1 nil)::nil)),
(algebra.Alg.Term algebra.F.id_1 nil))::R_xml_0_rule_as_list_0.
Definition R_xml_0_rule_as_list_2 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_0
nil)::(algebra.Alg.Term algebra.F.id_2 nil)::nil)),
(algebra.Alg.Term algebra.F.id_2 nil))::R_xml_0_rule_as_list_1.
Definition R_xml_0_rule_as_list_3 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_0
nil)::(algebra.Alg.Term algebra.F.id_3 nil)::nil)),
(algebra.Alg.Term algebra.F.id_3 nil))::R_xml_0_rule_as_list_2.
Definition R_xml_0_rule_as_list_4 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_0
nil)::(algebra.Alg.Term algebra.F.id_4 nil)::nil)),
(algebra.Alg.Term algebra.F.id_4 nil))::R_xml_0_rule_as_list_3.
Definition R_xml_0_rule_as_list_5 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_0
nil)::(algebra.Alg.Term algebra.F.id_5 nil)::nil)),
(algebra.Alg.Term algebra.F.id_5 nil))::R_xml_0_rule_as_list_4.
Definition R_xml_0_rule_as_list_6 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_0
nil)::(algebra.Alg.Term algebra.F.id_6 nil)::nil)),
(algebra.Alg.Term algebra.F.id_6 nil))::R_xml_0_rule_as_list_5.
Definition R_xml_0_rule_as_list_7 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_0
nil)::(algebra.Alg.Term algebra.F.id_7 nil)::nil)),
(algebra.Alg.Term algebra.F.id_7 nil))::R_xml_0_rule_as_list_6.
Definition R_xml_0_rule_as_list_8 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_0
nil)::(algebra.Alg.Term algebra.F.id_8 nil)::nil)),
(algebra.Alg.Term algebra.F.id_8 nil))::R_xml_0_rule_as_list_7.
Definition R_xml_0_rule_as_list_9 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_0
nil)::(algebra.Alg.Term algebra.F.id_9 nil)::nil)),
(algebra.Alg.Term algebra.F.id_9 nil))::R_xml_0_rule_as_list_8.
Definition R_xml_0_rule_as_list_10 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_1
nil)::(algebra.Alg.Term algebra.F.id_0 nil)::nil)),
(algebra.Alg.Term algebra.F.id_1 nil))::R_xml_0_rule_as_list_9.
Definition R_xml_0_rule_as_list_11 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_1
nil)::(algebra.Alg.Term algebra.F.id_1 nil)::nil)),
(algebra.Alg.Term algebra.F.id_2 nil))::R_xml_0_rule_as_list_10.
Definition R_xml_0_rule_as_list_12 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_1
nil)::(algebra.Alg.Term algebra.F.id_2 nil)::nil)),
(algebra.Alg.Term algebra.F.id_3 nil))::R_xml_0_rule_as_list_11.
Definition R_xml_0_rule_as_list_13 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_1
nil)::(algebra.Alg.Term algebra.F.id_3 nil)::nil)),
(algebra.Alg.Term algebra.F.id_4 nil))::R_xml_0_rule_as_list_12.
Definition R_xml_0_rule_as_list_14 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_1
nil)::(algebra.Alg.Term algebra.F.id_4 nil)::nil)),
(algebra.Alg.Term algebra.F.id_5 nil))::R_xml_0_rule_as_list_13.
Definition R_xml_0_rule_as_list_15 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_1
nil)::(algebra.Alg.Term algebra.F.id_5 nil)::nil)),
(algebra.Alg.Term algebra.F.id_6 nil))::R_xml_0_rule_as_list_14.
Definition R_xml_0_rule_as_list_16 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_1
nil)::(algebra.Alg.Term algebra.F.id_6 nil)::nil)),
(algebra.Alg.Term algebra.F.id_7 nil))::R_xml_0_rule_as_list_15.
Definition R_xml_0_rule_as_list_17 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_1
nil)::(algebra.Alg.Term algebra.F.id_7 nil)::nil)),
(algebra.Alg.Term algebra.F.id_8 nil))::R_xml_0_rule_as_list_16.
Definition R_xml_0_rule_as_list_18 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_1
nil)::(algebra.Alg.Term algebra.F.id_8 nil)::nil)),
(algebra.Alg.Term algebra.F.id_9 nil))::R_xml_0_rule_as_list_17.
Definition R_xml_0_rule_as_list_19 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_1
nil)::(algebra.Alg.Term algebra.F.id_9 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_0 nil)::nil)))::R_xml_0_rule_as_list_18.
Definition R_xml_0_rule_as_list_20 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_2
nil)::(algebra.Alg.Term algebra.F.id_0 nil)::nil)),
(algebra.Alg.Term algebra.F.id_2 nil))::R_xml_0_rule_as_list_19.
Definition R_xml_0_rule_as_list_21 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_2
nil)::(algebra.Alg.Term algebra.F.id_1 nil)::nil)),
(algebra.Alg.Term algebra.F.id_3 nil))::R_xml_0_rule_as_list_20.
Definition R_xml_0_rule_as_list_22 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_2
nil)::(algebra.Alg.Term algebra.F.id_2 nil)::nil)),
(algebra.Alg.Term algebra.F.id_4 nil))::R_xml_0_rule_as_list_21.
Definition R_xml_0_rule_as_list_23 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_2
nil)::(algebra.Alg.Term algebra.F.id_3 nil)::nil)),
(algebra.Alg.Term algebra.F.id_5 nil))::R_xml_0_rule_as_list_22.
Definition R_xml_0_rule_as_list_24 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_2
nil)::(algebra.Alg.Term algebra.F.id_4 nil)::nil)),
(algebra.Alg.Term algebra.F.id_6 nil))::R_xml_0_rule_as_list_23.
Definition R_xml_0_rule_as_list_25 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_2
nil)::(algebra.Alg.Term algebra.F.id_5 nil)::nil)),
(algebra.Alg.Term algebra.F.id_7 nil))::R_xml_0_rule_as_list_24.
Definition R_xml_0_rule_as_list_26 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_2
nil)::(algebra.Alg.Term algebra.F.id_6 nil)::nil)),
(algebra.Alg.Term algebra.F.id_8 nil))::R_xml_0_rule_as_list_25.
Definition R_xml_0_rule_as_list_27 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_2
nil)::(algebra.Alg.Term algebra.F.id_7 nil)::nil)),
(algebra.Alg.Term algebra.F.id_9 nil))::R_xml_0_rule_as_list_26.
Definition R_xml_0_rule_as_list_28 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_2
nil)::(algebra.Alg.Term algebra.F.id_8 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_0 nil)::nil)))::R_xml_0_rule_as_list_27.
Definition R_xml_0_rule_as_list_29 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_2
nil)::(algebra.Alg.Term algebra.F.id_9 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_1 nil)::nil)))::R_xml_0_rule_as_list_28.
Definition R_xml_0_rule_as_list_30 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_3
nil)::(algebra.Alg.Term algebra.F.id_0 nil)::nil)),
(algebra.Alg.Term algebra.F.id_3 nil))::R_xml_0_rule_as_list_29.
Definition R_xml_0_rule_as_list_31 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_3
nil)::(algebra.Alg.Term algebra.F.id_1 nil)::nil)),
(algebra.Alg.Term algebra.F.id_4 nil))::R_xml_0_rule_as_list_30.
Definition R_xml_0_rule_as_list_32 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_3
nil)::(algebra.Alg.Term algebra.F.id_2 nil)::nil)),
(algebra.Alg.Term algebra.F.id_5 nil))::R_xml_0_rule_as_list_31.
Definition R_xml_0_rule_as_list_33 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_3
nil)::(algebra.Alg.Term algebra.F.id_3 nil)::nil)),
(algebra.Alg.Term algebra.F.id_6 nil))::R_xml_0_rule_as_list_32.
Definition R_xml_0_rule_as_list_34 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_3
nil)::(algebra.Alg.Term algebra.F.id_4 nil)::nil)),
(algebra.Alg.Term algebra.F.id_7 nil))::R_xml_0_rule_as_list_33.
Definition R_xml_0_rule_as_list_35 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_3
nil)::(algebra.Alg.Term algebra.F.id_5 nil)::nil)),
(algebra.Alg.Term algebra.F.id_8 nil))::R_xml_0_rule_as_list_34.
Definition R_xml_0_rule_as_list_36 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_3
nil)::(algebra.Alg.Term algebra.F.id_6 nil)::nil)),
(algebra.Alg.Term algebra.F.id_9 nil))::R_xml_0_rule_as_list_35.
Definition R_xml_0_rule_as_list_37 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_3
nil)::(algebra.Alg.Term algebra.F.id_7 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_0 nil)::nil)))::R_xml_0_rule_as_list_36.
Definition R_xml_0_rule_as_list_38 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_3
nil)::(algebra.Alg.Term algebra.F.id_8 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_1 nil)::nil)))::R_xml_0_rule_as_list_37.
Definition R_xml_0_rule_as_list_39 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_3
nil)::(algebra.Alg.Term algebra.F.id_9 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_2 nil)::nil)))::R_xml_0_rule_as_list_38.
Definition R_xml_0_rule_as_list_40 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_4
nil)::(algebra.Alg.Term algebra.F.id_0 nil)::nil)),
(algebra.Alg.Term algebra.F.id_4 nil))::R_xml_0_rule_as_list_39.
Definition R_xml_0_rule_as_list_41 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_4
nil)::(algebra.Alg.Term algebra.F.id_1 nil)::nil)),
(algebra.Alg.Term algebra.F.id_5 nil))::R_xml_0_rule_as_list_40.
Definition R_xml_0_rule_as_list_42 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_4
nil)::(algebra.Alg.Term algebra.F.id_2 nil)::nil)),
(algebra.Alg.Term algebra.F.id_6 nil))::R_xml_0_rule_as_list_41.
Definition R_xml_0_rule_as_list_43 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_4
nil)::(algebra.Alg.Term algebra.F.id_3 nil)::nil)),
(algebra.Alg.Term algebra.F.id_7 nil))::R_xml_0_rule_as_list_42.
Definition R_xml_0_rule_as_list_44 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_4
nil)::(algebra.Alg.Term algebra.F.id_4 nil)::nil)),
(algebra.Alg.Term algebra.F.id_8 nil))::R_xml_0_rule_as_list_43.
Definition R_xml_0_rule_as_list_45 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_4
nil)::(algebra.Alg.Term algebra.F.id_5 nil)::nil)),
(algebra.Alg.Term algebra.F.id_9 nil))::R_xml_0_rule_as_list_44.
Definition R_xml_0_rule_as_list_46 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_4
nil)::(algebra.Alg.Term algebra.F.id_6 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_0 nil)::nil)))::R_xml_0_rule_as_list_45.
Definition R_xml_0_rule_as_list_47 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_4
nil)::(algebra.Alg.Term algebra.F.id_7 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_1 nil)::nil)))::R_xml_0_rule_as_list_46.
Definition R_xml_0_rule_as_list_48 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_4
nil)::(algebra.Alg.Term algebra.F.id_8 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_2 nil)::nil)))::R_xml_0_rule_as_list_47.
Definition R_xml_0_rule_as_list_49 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_4
nil)::(algebra.Alg.Term algebra.F.id_9 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_3 nil)::nil)))::R_xml_0_rule_as_list_48.
Definition R_xml_0_rule_as_list_50 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_5
nil)::(algebra.Alg.Term algebra.F.id_0 nil)::nil)),
(algebra.Alg.Term algebra.F.id_5 nil))::R_xml_0_rule_as_list_49.
Definition R_xml_0_rule_as_list_51 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_5
nil)::(algebra.Alg.Term algebra.F.id_1 nil)::nil)),
(algebra.Alg.Term algebra.F.id_6 nil))::R_xml_0_rule_as_list_50.
Definition R_xml_0_rule_as_list_52 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_5
nil)::(algebra.Alg.Term algebra.F.id_2 nil)::nil)),
(algebra.Alg.Term algebra.F.id_7 nil))::R_xml_0_rule_as_list_51.
Definition R_xml_0_rule_as_list_53 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_5
nil)::(algebra.Alg.Term algebra.F.id_3 nil)::nil)),
(algebra.Alg.Term algebra.F.id_8 nil))::R_xml_0_rule_as_list_52.
Definition R_xml_0_rule_as_list_54 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_5
nil)::(algebra.Alg.Term algebra.F.id_4 nil)::nil)),
(algebra.Alg.Term algebra.F.id_9 nil))::R_xml_0_rule_as_list_53.
Definition R_xml_0_rule_as_list_55 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_5
nil)::(algebra.Alg.Term algebra.F.id_5 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_0 nil)::nil)))::R_xml_0_rule_as_list_54.
Definition R_xml_0_rule_as_list_56 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_5
nil)::(algebra.Alg.Term algebra.F.id_6 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_1 nil)::nil)))::R_xml_0_rule_as_list_55.
Definition R_xml_0_rule_as_list_57 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_5
nil)::(algebra.Alg.Term algebra.F.id_7 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_2 nil)::nil)))::R_xml_0_rule_as_list_56.
Definition R_xml_0_rule_as_list_58 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_5
nil)::(algebra.Alg.Term algebra.F.id_8 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_3 nil)::nil)))::R_xml_0_rule_as_list_57.
Definition R_xml_0_rule_as_list_59 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_5
nil)::(algebra.Alg.Term algebra.F.id_9 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_4 nil)::nil)))::R_xml_0_rule_as_list_58.
Definition R_xml_0_rule_as_list_60 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_6
nil)::(algebra.Alg.Term algebra.F.id_0 nil)::nil)),
(algebra.Alg.Term algebra.F.id_6 nil))::R_xml_0_rule_as_list_59.
Definition R_xml_0_rule_as_list_61 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_6
nil)::(algebra.Alg.Term algebra.F.id_1 nil)::nil)),
(algebra.Alg.Term algebra.F.id_7 nil))::R_xml_0_rule_as_list_60.
Definition R_xml_0_rule_as_list_62 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_6
nil)::(algebra.Alg.Term algebra.F.id_2 nil)::nil)),
(algebra.Alg.Term algebra.F.id_8 nil))::R_xml_0_rule_as_list_61.
Definition R_xml_0_rule_as_list_63 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_6
nil)::(algebra.Alg.Term algebra.F.id_3 nil)::nil)),
(algebra.Alg.Term algebra.F.id_9 nil))::R_xml_0_rule_as_list_62.
Definition R_xml_0_rule_as_list_64 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_6
nil)::(algebra.Alg.Term algebra.F.id_4 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_0 nil)::nil)))::R_xml_0_rule_as_list_63.
Definition R_xml_0_rule_as_list_65 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_6
nil)::(algebra.Alg.Term algebra.F.id_5 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_1 nil)::nil)))::R_xml_0_rule_as_list_64.
Definition R_xml_0_rule_as_list_66 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_6
nil)::(algebra.Alg.Term algebra.F.id_6 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_2 nil)::nil)))::R_xml_0_rule_as_list_65.
Definition R_xml_0_rule_as_list_67 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_6
nil)::(algebra.Alg.Term algebra.F.id_7 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_3 nil)::nil)))::R_xml_0_rule_as_list_66.
Definition R_xml_0_rule_as_list_68 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_6
nil)::(algebra.Alg.Term algebra.F.id_8 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_4 nil)::nil)))::R_xml_0_rule_as_list_67.
Definition R_xml_0_rule_as_list_69 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_6
nil)::(algebra.Alg.Term algebra.F.id_9 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_5 nil)::nil)))::R_xml_0_rule_as_list_68.
Definition R_xml_0_rule_as_list_70 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_7
nil)::(algebra.Alg.Term algebra.F.id_0 nil)::nil)),
(algebra.Alg.Term algebra.F.id_7 nil))::R_xml_0_rule_as_list_69.
Definition R_xml_0_rule_as_list_71 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_7
nil)::(algebra.Alg.Term algebra.F.id_1 nil)::nil)),
(algebra.Alg.Term algebra.F.id_8 nil))::R_xml_0_rule_as_list_70.
Definition R_xml_0_rule_as_list_72 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_7
nil)::(algebra.Alg.Term algebra.F.id_2 nil)::nil)),
(algebra.Alg.Term algebra.F.id_9 nil))::R_xml_0_rule_as_list_71.
Definition R_xml_0_rule_as_list_73 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_7
nil)::(algebra.Alg.Term algebra.F.id_3 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_0 nil)::nil)))::R_xml_0_rule_as_list_72.
Definition R_xml_0_rule_as_list_74 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_7
nil)::(algebra.Alg.Term algebra.F.id_4 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_1 nil)::nil)))::R_xml_0_rule_as_list_73.
Definition R_xml_0_rule_as_list_75 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_7
nil)::(algebra.Alg.Term algebra.F.id_5 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_2 nil)::nil)))::R_xml_0_rule_as_list_74.
Definition R_xml_0_rule_as_list_76 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_7
nil)::(algebra.Alg.Term algebra.F.id_6 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_3 nil)::nil)))::R_xml_0_rule_as_list_75.
Definition R_xml_0_rule_as_list_77 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_7
nil)::(algebra.Alg.Term algebra.F.id_7 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_4 nil)::nil)))::R_xml_0_rule_as_list_76.
Definition R_xml_0_rule_as_list_78 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_7
nil)::(algebra.Alg.Term algebra.F.id_8 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_5 nil)::nil)))::R_xml_0_rule_as_list_77.
Definition R_xml_0_rule_as_list_79 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_7
nil)::(algebra.Alg.Term algebra.F.id_9 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_6 nil)::nil)))::R_xml_0_rule_as_list_78.
Definition R_xml_0_rule_as_list_80 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_8
nil)::(algebra.Alg.Term algebra.F.id_0 nil)::nil)),
(algebra.Alg.Term algebra.F.id_8 nil))::R_xml_0_rule_as_list_79.
Definition R_xml_0_rule_as_list_81 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_8
nil)::(algebra.Alg.Term algebra.F.id_1 nil)::nil)),
(algebra.Alg.Term algebra.F.id_9 nil))::R_xml_0_rule_as_list_80.
Definition R_xml_0_rule_as_list_82 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_8
nil)::(algebra.Alg.Term algebra.F.id_2 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_0 nil)::nil)))::R_xml_0_rule_as_list_81.
Definition R_xml_0_rule_as_list_83 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_8
nil)::(algebra.Alg.Term algebra.F.id_3 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_1 nil)::nil)))::R_xml_0_rule_as_list_82.
Definition R_xml_0_rule_as_list_84 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_8
nil)::(algebra.Alg.Term algebra.F.id_4 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_2 nil)::nil)))::R_xml_0_rule_as_list_83.
Definition R_xml_0_rule_as_list_85 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_8
nil)::(algebra.Alg.Term algebra.F.id_5 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_3 nil)::nil)))::R_xml_0_rule_as_list_84.
Definition R_xml_0_rule_as_list_86 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_8
nil)::(algebra.Alg.Term algebra.F.id_6 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_4 nil)::nil)))::R_xml_0_rule_as_list_85.
Definition R_xml_0_rule_as_list_87 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_8
nil)::(algebra.Alg.Term algebra.F.id_7 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_5 nil)::nil)))::R_xml_0_rule_as_list_86.
Definition R_xml_0_rule_as_list_88 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_8
nil)::(algebra.Alg.Term algebra.F.id_8 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_6 nil)::nil)))::R_xml_0_rule_as_list_87.
Definition R_xml_0_rule_as_list_89 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_8
nil)::(algebra.Alg.Term algebra.F.id_9 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_7 nil)::nil)))::R_xml_0_rule_as_list_88.
Definition R_xml_0_rule_as_list_90 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_9
nil)::(algebra.Alg.Term algebra.F.id_0 nil)::nil)),
(algebra.Alg.Term algebra.F.id_9 nil))::R_xml_0_rule_as_list_89.
Definition R_xml_0_rule_as_list_91 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_9
nil)::(algebra.Alg.Term algebra.F.id_1 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_0 nil)::nil)))::R_xml_0_rule_as_list_90.
Definition R_xml_0_rule_as_list_92 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_9
nil)::(algebra.Alg.Term algebra.F.id_2 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_1 nil)::nil)))::R_xml_0_rule_as_list_91.
Definition R_xml_0_rule_as_list_93 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_9
nil)::(algebra.Alg.Term algebra.F.id_3 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_2 nil)::nil)))::R_xml_0_rule_as_list_92.
Definition R_xml_0_rule_as_list_94 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_9
nil)::(algebra.Alg.Term algebra.F.id_4 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_3 nil)::nil)))::R_xml_0_rule_as_list_93.
Definition R_xml_0_rule_as_list_95 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_9
nil)::(algebra.Alg.Term algebra.F.id_5 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_4 nil)::nil)))::R_xml_0_rule_as_list_94.
Definition R_xml_0_rule_as_list_96 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_9
nil)::(algebra.Alg.Term algebra.F.id_6 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_5 nil)::nil)))::R_xml_0_rule_as_list_95.
Definition R_xml_0_rule_as_list_97 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_9
nil)::(algebra.Alg.Term algebra.F.id_7 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_6 nil)::nil)))::R_xml_0_rule_as_list_96.
Definition R_xml_0_rule_as_list_98 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_9
nil)::(algebra.Alg.Term algebra.F.id_8 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_7 nil)::nil)))::R_xml_0_rule_as_list_97.
Definition R_xml_0_rule_as_list_99 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_9
nil)::(algebra.Alg.Term algebra.F.id_9 nil)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_8 nil)::nil)))::R_xml_0_rule_as_list_98.
Definition R_xml_0_rule_as_list_100 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Var 1)::
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Var 2)::
(algebra.Alg.Var 3)::nil))::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Var 2)::(algebra.Alg.Term
algebra.F.id__plus_ ((algebra.Alg.Var 1)::
(algebra.Alg.Var 3)::nil))::nil)))::R_xml_0_rule_as_list_99.
Definition R_xml_0_rule_as_list_101 :=
((algebra.Alg.Term algebra.F.id__plus_ ((algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Var 1)::(algebra.Alg.Var 2)::nil))::
(algebra.Alg.Var 3)::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Var 1)::(algebra.Alg.Term
algebra.F.id__plus_ ((algebra.Alg.Var 2)::
(algebra.Alg.Var 3)::nil))::nil)))::R_xml_0_rule_as_list_100.
Definition R_xml_0_rule_as_list_102 :=
((algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id_0 nil)::
(algebra.Alg.Var 1)::nil)),(algebra.Alg.Var 1))::
R_xml_0_rule_as_list_101.
Definition R_xml_0_rule_as_list_103 :=
((algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Var 1)::(algebra.Alg.Term
algebra.F.id_c ((algebra.Alg.Var 2)::(algebra.Alg.Var 3)::nil))::nil)),
(algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term algebra.F.id__plus_
((algebra.Alg.Var 1)::(algebra.Alg.Var 2)::nil))::
(algebra.Alg.Var 3)::nil)))::R_xml_0_rule_as_list_102.
Definition R_xml_0_rule_as_list := R_xml_0_rule_as_list_103.
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.or25_equiv in H|-.
case H;clear H;intros H.
injection H;intros ;subst;constructor 104.
injection H;intros ;subst;constructor 103.
injection H;intros ;subst;constructor 102.
injection H;intros ;subst;constructor 101.
injection H;intros ;subst;constructor 100.
injection H;intros ;subst;constructor 99.
injection H;intros ;subst;constructor 98.
injection H;intros ;subst;constructor 97.
injection H;intros ;subst;constructor 96.
injection H;intros ;subst;constructor 95.
injection H;intros ;subst;constructor 94.
injection H;intros ;subst;constructor 93.
injection H;intros ;subst;constructor 92.
injection H;intros ;subst;constructor 91.
injection H;intros ;subst;constructor 90.
injection H;intros ;subst;constructor 89.
injection H;intros ;subst;constructor 88.
injection H;intros ;subst;constructor 87.
injection H;intros ;subst;constructor 86.
injection H;intros ;subst;constructor 85.
injection H;intros ;subst;constructor 84.
injection H;intros ;subst;constructor 83.
injection H;intros ;subst;constructor 82.
injection H;intros ;subst;constructor 81.
rewrite <- or_ext_generated.or25_equiv in H|-.
case H;clear H;intros H.
injection H;intros ;subst;constructor 80.
injection H;intros ;subst;constructor 79.
injection H;intros ;subst;constructor 78.
injection H;intros ;subst;constructor 77.
injection H;intros ;subst;constructor 76.
injection H;intros ;subst;constructor 75.
injection H;intros ;subst;constructor 74.
injection H;intros ;subst;constructor 73.
injection H;intros ;subst;constructor 72.
injection H;intros ;subst;constructor 71.
injection H;intros ;subst;constructor 70.
injection H;intros ;subst;constructor 69.
injection H;intros ;subst;constructor 68.
injection H;intros ;subst;constructor 67.
injection H;intros ;subst;constructor 66.
injection H;intros ;subst;constructor 65.
injection H;intros ;subst;constructor 64.
injection H;intros ;subst;constructor 63.
injection H;intros ;subst;constructor 62.
injection H;intros ;subst;constructor 61.
injection H;intros ;subst;constructor 60.
injection H;intros ;subst;constructor 59.
injection H;intros ;subst;constructor 58.
injection H;intros ;subst;constructor 57.
rewrite <- or_ext_generated.or25_equiv in H|-.
case H;clear H;intros H.
injection H;intros ;subst;constructor 56.
injection H;intros ;subst;constructor 55.
injection H;intros ;subst;constructor 54.
injection H;intros ;subst;constructor 53.
injection H;intros ;subst;constructor 52.
injection H;intros ;subst;constructor 51.
injection H;intros ;subst;constructor 50.
injection H;intros ;subst;constructor 49.
injection H;intros ;subst;constructor 48.
injection H;intros ;subst;constructor 47.
injection H;intros ;subst;constructor 46.
injection H;intros ;subst;constructor 45.
injection H;intros ;subst;constructor 44.
injection H;intros ;subst;constructor 43.
injection H;intros ;subst;constructor 42.
injection H;intros ;subst;constructor 41.
injection H;intros ;subst;constructor 40.
injection H;intros ;subst;constructor 39.
injection H;intros ;subst;constructor 38.
injection H;intros ;subst;constructor 37.
injection H;intros ;subst;constructor 36.
injection H;intros ;subst;constructor 35.
injection H;intros ;subst;constructor 34.
injection H;intros ;subst;constructor 33.
rewrite <- or_ext_generated.or25_equiv in H|-.
case H;clear H;intros H.
injection H;intros ;subst;constructor 32.
injection H;intros ;subst;constructor 31.
injection H;intros ;subst;constructor 30.
injection H;intros ;subst;constructor 29.
injection H;intros ;subst;constructor 28.
injection H;intros ;subst;constructor 27.
injection H;intros ;subst;constructor 26.
injection H;intros ;subst;constructor 25.
injection H;intros ;subst;constructor 24.
injection H;intros ;subst;constructor 23.
injection H;intros ;subst;constructor 22.
injection H;intros ;subst;constructor 21.
injection H;intros ;subst;constructor 20.
injection H;intros ;subst;constructor 19.
injection H;intros ;subst;constructor 18.
injection H;intros ;subst;constructor 17.
injection H;intros ;subst;constructor 16.
injection H;intros ;subst;constructor 15.
injection H;intros ;subst;constructor 14.
injection H;intros ;subst;constructor 13.
injection H;intros ;subst;constructor 12.
injection H;intros ;subst;constructor 11.
injection H;intros ;subst;constructor 10.
injection H;intros ;subst;constructor 9.
rewrite <- or_ext_generated.or9_equiv in H|-.
case H;clear H;intros H.
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_10 (x5 x6 x7 x8 x9 x10 x11 x12 x13 x14:Prop) :
Prop :=
| conj_10 :
x5->x6->x7->x8->x9->x10->x11->x12->x13->x14->
and_10 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14
.
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_10 (t = (algebra.Alg.Term algebra.F.id_7 nil) ->
t' = (algebra.Alg.Term algebra.F.id_7 nil))
(t = (algebra.Alg.Term algebra.F.id_3 nil) ->
t' = (algebra.Alg.Term algebra.F.id_3 nil))
(t = (algebra.Alg.Term algebra.F.id_1 nil) ->
t' = (algebra.Alg.Term algebra.F.id_1 nil))
(t = (algebra.Alg.Term algebra.F.id_9 nil) ->
t' = (algebra.Alg.Term algebra.F.id_9 nil))
(t = (algebra.Alg.Term algebra.F.id_5 nil) ->
t' = (algebra.Alg.Term algebra.F.id_5 nil))
(t = (algebra.Alg.Term algebra.F.id_0 nil) ->
t' = (algebra.Alg.Term algebra.F.id_0 nil))
(t = (algebra.Alg.Term algebra.F.id_8 nil) ->
t' = (algebra.Alg.Term algebra.F.id_8 nil))
(t = (algebra.Alg.Term algebra.F.id_4 nil) ->
t' = (algebra.Alg.Term algebra.F.id_4 nil))
(t = (algebra.Alg.Term algebra.F.id_2 nil) ->
t' = (algebra.Alg.Term algebra.F.id_2 nil))
(t = (algebra.Alg.Term algebra.F.id_6 nil) ->
t' = (algebra.Alg.Term algebra.F.id_6 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 H;intuition;constructor 1.
intros H;intuition;constructor 1.
intros H;intuition;constructor 1.
intros H;intuition;constructor 1.
intros H;intuition;constructor 1.
intros H;intuition;constructor 1.
intros H;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_7 H_id_3 H_id_1 H_id_9 H_id_5 H_id_0 H_id_8 H_id_4 H_id_2 H_id_6].
constructor.
clear H_id_3 H_id_1 H_id_9 H_id_5 H_id_0 H_id_8 H_id_4 H_id_2 H_id_6;
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_7 H_id_1 H_id_9 H_id_5 H_id_0 H_id_8 H_id_4 H_id_2 H_id_6;
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_7 H_id_3 H_id_9 H_id_5 H_id_0 H_id_8 H_id_4 H_id_2 H_id_6;
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_7 H_id_3 H_id_1 H_id_5 H_id_0 H_id_8 H_id_4 H_id_2 H_id_6;
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_7 H_id_3 H_id_1 H_id_9 H_id_0 H_id_8 H_id_4 H_id_2 H_id_6;
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_7 H_id_3 H_id_1 H_id_9 H_id_5 H_id_8 H_id_4 H_id_2 H_id_6;
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_7 H_id_3 H_id_1 H_id_9 H_id_5 H_id_0 H_id_4 H_id_2 H_id_6;
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_7 H_id_3 H_id_1 H_id_9 H_id_5 H_id_0 H_id_8 H_id_2 H_id_6;
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_7 H_id_3 H_id_1 H_id_9 H_id_5 H_id_0 H_id_8 H_id_4 H_id_6;
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_7 H_id_3 H_id_1 H_id_9 H_id_5 H_id_0 H_id_8 H_id_4 H_id_2;
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_7_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_7 nil) ->
t' = (algebra.Alg.Term algebra.F.id_7 nil).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Lemma id_3_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_3 nil) ->
t' = (algebra.Alg.Term algebra.F.id_3 nil).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Lemma id_1_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_1 nil) ->
t' = (algebra.Alg.Term algebra.F.id_1 nil).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Lemma id_9_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_9 nil) ->
t' = (algebra.Alg.Term algebra.F.id_9 nil).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Lemma id_5_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_5 nil) ->
t' = (algebra.Alg.Term algebra.F.id_5 nil).
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_8_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_8 nil) ->
t' = (algebra.Alg.Term algebra.F.id_8 nil).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Lemma id_4_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_4 nil) ->
t' = (algebra.Alg.Term algebra.F.id_4 nil).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Lemma id_2_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_2 nil) ->
t' = (algebra.Alg.Term algebra.F.id_2 nil).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Lemma id_6_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_6 nil) ->
t' = (algebra.Alg.Term algebra.F.id_6 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_7 nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_7_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_3 nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_3_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_1 nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_1_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_9 nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_9_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_5 nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_5_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_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_8 nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_8_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_4 nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_4_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_2 nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_2_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_6 nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_6_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_7 nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_7_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_3 nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_3_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_1 nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_1_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_9 nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_9_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_5 nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_5_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_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_8 nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_8_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_4 nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_4_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_2 nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_2_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_6 nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_6_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 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__plus_ : A ->A ->A.
Hypothesis P_id_7 : A.
Hypothesis P_id_3 : A.
Hypothesis P_id_1 : A.
Hypothesis P_id_9 : A.
Hypothesis P_id_5 : A.
Hypothesis P_id_0 : A.
Hypothesis P_id_8 : A.
Hypothesis P_id_4 : A.
Hypothesis P_id_2 : A.
Hypothesis P_id_c : A ->A ->A.
Hypothesis P_id_6 : A.
Hypothesis P_id__plus__monotonic :
forall x8 x6 x5 x7,
(A0 <= x8)/\ (x8 <= x7) ->
(A0 <= x6)/\ (x6 <= x5) ->P_id__plus_ x6 x8 <= P_id__plus_ x5 x7.
Hypothesis P_id_c_monotonic :
forall x8 x6 x5 x7,
(A0 <= x8)/\ (x8 <= x7) ->
(A0 <= x6)/\ (x6 <= x5) ->P_id_c x6 x8 <= P_id_c x5 x7.
Hypothesis P_id__plus__bounded :
forall x6 x5, (A0 <= x5) ->(A0 <= x6) ->A0 <= P_id__plus_ x6 x5.
Hypothesis P_id_7_bounded : A0 <= P_id_7 .
Hypothesis P_id_3_bounded : A0 <= P_id_3 .
Hypothesis P_id_1_bounded : A0 <= P_id_1 .
Hypothesis P_id_9_bounded : A0 <= P_id_9 .
Hypothesis P_id_5_bounded : A0 <= P_id_5 .
Hypothesis P_id_0_bounded : A0 <= P_id_0 .
Hypothesis P_id_8_bounded : A0 <= P_id_8 .
Hypothesis P_id_4_bounded : A0 <= P_id_4 .
Hypothesis P_id_2_bounded : A0 <= P_id_2 .
Hypothesis P_id_c_bounded :
forall x6 x5, (A0 <= x5) ->(A0 <= x6) ->A0 <= P_id_c x6 x5.
Hypothesis P_id_6_bounded : A0 <= P_id_6 .
Fixpoint measure t { struct t } :=
match t with
| (algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil)) =>
P_id__plus_ (measure x6) (measure x5)
| (algebra.Alg.Term algebra.F.id_7 nil) => P_id_7
| (algebra.Alg.Term algebra.F.id_3 nil) => P_id_3
| (algebra.Alg.Term algebra.F.id_1 nil) => P_id_1
| (algebra.Alg.Term algebra.F.id_9 nil) => P_id_9
| (algebra.Alg.Term algebra.F.id_5 nil) => P_id_5
| (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0
| (algebra.Alg.Term algebra.F.id_8 nil) => P_id_8
| (algebra.Alg.Term algebra.F.id_4 nil) => P_id_4
| (algebra.Alg.Term algebra.F.id_2 nil) => P_id_2
| (algebra.Alg.Term algebra.F.id_c (x6::x5::nil)) =>
P_id_c (measure x6) (measure x5)
| (algebra.Alg.Term algebra.F.id_6 nil) => P_id_6
| _ => A0
end.
Lemma measure_equation :
forall t,
measure t = match t with
| (algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil)) =>
P_id__plus_ (measure x6) (measure x5)
| (algebra.Alg.Term algebra.F.id_7 nil) => P_id_7
| (algebra.Alg.Term algebra.F.id_3 nil) => P_id_3
| (algebra.Alg.Term algebra.F.id_1 nil) => P_id_1
| (algebra.Alg.Term algebra.F.id_9 nil) => P_id_9
| (algebra.Alg.Term algebra.F.id_5 nil) => P_id_5
| (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0
| (algebra.Alg.Term algebra.F.id_8 nil) => P_id_8
| (algebra.Alg.Term algebra.F.id_4 nil) => P_id_4
| (algebra.Alg.Term algebra.F.id_2 nil) => P_id_2
| (algebra.Alg.Term algebra.F.id_c (x6::x5::nil)) =>
P_id_c (measure x6) (measure x5)
| (algebra.Alg.Term algebra.F.id_6 nil) => P_id_6
| _ => 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__plus_ => P_id__plus_
| algebra.F.id_7 => P_id_7
| algebra.F.id_3 => P_id_3
| algebra.F.id_1 => P_id_1
| algebra.F.id_9 => P_id_9
| algebra.F.id_5 => P_id_5
| algebra.F.id_0 => P_id_0
| algebra.F.id_8 => P_id_8
| algebra.F.id_4 => P_id_4
| algebra.F.id_2 => P_id_2
| algebra.F.id_c => P_id_c
| algebra.F.id_6 => P_id_6
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__plus_ =>
match l with
| nil => _
| _::nil => _
| _::_::nil => _
| _::_::_::_ => _
end
| algebra.F.id_7 => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_3 => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_1 => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_9 => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_5 => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_0 => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_8 => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_4 => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_2 => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_c =>
match l with
| nil => _
| _::nil => _
| _::_::nil => _
| _::_::_::_ => _
end
| algebra.F.id_6 => match l with
| 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__plus__bounded;assumption.
vm_compute in |-*;intros ;apply P_id_7_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_3_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_1_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_9_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_5_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_0_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_8_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_4_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_2_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_c_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_6_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__plus__monotonic;assumption.
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;intros ;apply P_id_c_monotonic;assumption.
vm_compute in |-*;apply (Aop.(le_refl)).
intros f.
case f.
vm_compute in |-*;intros ;apply P_id__plus__bounded;assumption.
vm_compute in |-*;intros ;apply P_id_7_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_3_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_1_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_9_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_5_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_0_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_8_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_4_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_2_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_c_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_6_bounded;assumption.
intros .
do 2 (rewrite <- same_measure in |-*).
apply rules_monotonic;assumption.
assumption.
Qed.
Hypothesis P_id__plus__hat_1 : A ->A ->A.
Hypothesis P_id_C : A ->A ->A.
Hypothesis P_id__plus__hat_1_monotonic :
forall x8 x6 x5 x7,
(A0 <= x8)/\ (x8 <= x7) ->
(A0 <= x6)/\ (x6 <= x5) ->
P_id__plus__hat_1 x6 x8 <= P_id__plus__hat_1 x5 x7.
Hypothesis P_id_C_monotonic :
forall x8 x6 x5 x7,
(A0 <= x8)/\ (x8 <= x7) ->
(A0 <= x6)/\ (x6 <= x5) ->P_id_C x6 x8 <= P_id_C x5 x7.
Definition marked_measure t :=
match t with
| (algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil)) =>
P_id__plus__hat_1 (measure x6) (measure x5)
| (algebra.Alg.Term algebra.F.id_c (x6::x5::nil)) =>
P_id_C (measure x6) (measure x5)
| _ => 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 x6 x5;apply (P_id_C x6 x5).
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 x6 x5;apply (P_id__plus__hat_1 x6 x5).
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__plus_ =>
match l with
| nil => _
| _::nil => _
| _::_::nil => _
| _::_::_::_ => _
end
| algebra.F.id_7 => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_3 => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_1 => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_9 => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_5 => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_0 => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_8 => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_4 => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_2 => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_c =>
match l with
| nil => _
| _::nil => _
| _::_::nil => _
| _::_::_::_ => _
end
| algebra.F.id_6 => match l with
| nil => _
| _::_ => _
end
end.
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
apply same_measure.
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
apply same_measure.
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
Qed.
Lemma marked_measure_equation :
forall t,
marked_measure t = match t with
| (algebra.Alg.Term algebra.F.id__plus_ (x6::
x5::nil)) =>
P_id__plus__hat_1 (measure x6) (measure x5)
| (algebra.Alg.Term algebra.F.id_c (x6::x5::nil)) =>
P_id_C (measure x6) (measure x5)
| _ => 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__plus__monotonic;assumption.
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;intros ;apply P_id_c_monotonic;assumption.
vm_compute in |-*;apply (Aop.(le_refl)).
clear f.
intros f.
case f.
vm_compute in |-*;intros ;apply P_id__plus__bounded;assumption.
vm_compute in |-*;intros ;apply P_id_7_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_3_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_1_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_9_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_5_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_0_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_8_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_4_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_2_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_c_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_6_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_C_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__plus__hat_1_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__plus_ : Z ->Z ->Z.
Hypothesis P_id_7 : Z.
Hypothesis P_id_3 : Z.
Hypothesis P_id_1 : Z.
Hypothesis P_id_9 : Z.
Hypothesis P_id_5 : Z.
Hypothesis P_id_0 : Z.
Hypothesis P_id_8 : Z.
Hypothesis P_id_4 : Z.
Hypothesis P_id_2 : Z.
Hypothesis P_id_c : Z ->Z ->Z.
Hypothesis P_id_6 : Z.
Hypothesis P_id__plus__monotonic :
forall x8 x6 x5 x7,
(min_value <= x8)/\ (x8 <= x7) ->
(min_value <= x6)/\ (x6 <= x5) ->P_id__plus_ x6 x8 <= P_id__plus_ x5 x7.
Hypothesis P_id_c_monotonic :
forall x8 x6 x5 x7,
(min_value <= x8)/\ (x8 <= x7) ->
(min_value <= x6)/\ (x6 <= x5) ->P_id_c x6 x8 <= P_id_c x5 x7.
Hypothesis P_id__plus__bounded :
forall x6 x5,
(min_value <= x5) ->(min_value <= x6) ->min_value <= P_id__plus_ x6 x5.
Hypothesis P_id_7_bounded : min_value <= P_id_7 .
Hypothesis P_id_3_bounded : min_value <= P_id_3 .
Hypothesis P_id_1_bounded : min_value <= P_id_1 .
Hypothesis P_id_9_bounded : min_value <= P_id_9 .
Hypothesis P_id_5_bounded : min_value <= P_id_5 .
Hypothesis P_id_0_bounded : min_value <= P_id_0 .
Hypothesis P_id_8_bounded : min_value <= P_id_8 .
Hypothesis P_id_4_bounded : min_value <= P_id_4 .
Hypothesis P_id_2_bounded : min_value <= P_id_2 .
Hypothesis P_id_c_bounded :
forall x6 x5,
(min_value <= x5) ->(min_value <= x6) ->min_value <= P_id_c x6 x5.
Hypothesis P_id_6_bounded : min_value <= P_id_6 .
Definition measure :=
Interp.measure min_value P_id__plus_ P_id_7 P_id_3 P_id_1 P_id_9
P_id_5 P_id_0 P_id_8 P_id_4 P_id_2 P_id_c P_id_6.
Lemma measure_equation :
forall t,
measure t = match t with
| (algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil)) =>
P_id__plus_ (measure x6) (measure x5)
| (algebra.Alg.Term algebra.F.id_7 nil) => P_id_7
| (algebra.Alg.Term algebra.F.id_3 nil) => P_id_3
| (algebra.Alg.Term algebra.F.id_1 nil) => P_id_1
| (algebra.Alg.Term algebra.F.id_9 nil) => P_id_9
| (algebra.Alg.Term algebra.F.id_5 nil) => P_id_5
| (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0
| (algebra.Alg.Term algebra.F.id_8 nil) => P_id_8
| (algebra.Alg.Term algebra.F.id_4 nil) => P_id_4
| (algebra.Alg.Term algebra.F.id_2 nil) => P_id_2
| (algebra.Alg.Term algebra.F.id_c (x6::x5::nil)) =>
P_id_c (measure x6) (measure x5)
| (algebra.Alg.Term algebra.F.id_6 nil) => P_id_6
| _ => 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__plus__monotonic;assumption.
intros ;apply P_id_c_monotonic;assumption.
intros ;apply P_id__plus__bounded;assumption.
intros ;apply P_id_7_bounded;assumption.
intros ;apply P_id_3_bounded;assumption.
intros ;apply P_id_1_bounded;assumption.
intros ;apply P_id_9_bounded;assumption.
intros ;apply P_id_5_bounded;assumption.
intros ;apply P_id_0_bounded;assumption.
intros ;apply P_id_8_bounded;assumption.
intros ;apply P_id_4_bounded;assumption.
intros ;apply P_id_2_bounded;assumption.
intros ;apply P_id_c_bounded;assumption.
intros ;apply P_id_6_bounded;assumption.
apply rules_monotonic.
Qed.
Hypothesis P_id__plus__hat_1 : Z ->Z ->Z.
Hypothesis P_id_C : Z ->Z ->Z.
Hypothesis P_id__plus__hat_1_monotonic :
forall x8 x6 x5 x7,
(min_value <= x8)/\ (x8 <= x7) ->
(min_value <= x6)/\ (x6 <= x5) ->
P_id__plus__hat_1 x6 x8 <= P_id__plus__hat_1 x5 x7.
Hypothesis P_id_C_monotonic :
forall x8 x6 x5 x7,
(min_value <= x8)/\ (x8 <= x7) ->
(min_value <= x6)/\ (x6 <= x5) ->P_id_C x6 x8 <= P_id_C x5 x7.
Definition marked_measure :=
Interp.marked_measure min_value P_id__plus_ P_id_7 P_id_3 P_id_1
P_id_9 P_id_5 P_id_0 P_id_8 P_id_4 P_id_2 P_id_c P_id_6
P_id__plus__hat_1 P_id_C.
Lemma marked_measure_equation :
forall t,
marked_measure t = match t with
| (algebra.Alg.Term algebra.F.id__plus_ (x6::
x5::nil)) =>
P_id__plus__hat_1 (measure x6) (measure x5)
| (algebra.Alg.Term algebra.F.id_c (x6::x5::nil)) =>
P_id_C (measure x6) (measure x5)
| _ => 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__plus__monotonic;assumption.
intros ;apply P_id_c_monotonic;assumption.
intros ;apply P_id__plus__bounded;assumption.
intros ;apply P_id_7_bounded;assumption.
intros ;apply P_id_3_bounded;assumption.
intros ;apply P_id_1_bounded;assumption.
intros ;apply P_id_9_bounded;assumption.
intros ;apply P_id_5_bounded;assumption.
intros ;apply P_id_0_bounded;assumption.
intros ;apply P_id_8_bounded;assumption.
intros ;apply P_id_4_bounded;assumption.
intros ;apply P_id_2_bounded;assumption.
intros ;apply P_id_c_bounded;assumption.
intros ;apply P_id_6_bounded;assumption.
apply rules_monotonic.
intros ;apply P_id__plus__hat_1_monotonic;assumption.
intros ;apply P_id_C_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 :=
(* <+(1,9),c(1,0)> *)
| DP_R_xml_0_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_1 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_0
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(2,8),c(1,0)> *)
| DP_R_xml_0_1 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_2 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_0
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(2,9),c(1,1)> *)
| DP_R_xml_0_2 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_2 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_1
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(3,7),c(1,0)> *)
| DP_R_xml_0_3 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_3 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_0
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(3,8),c(1,1)> *)
| DP_R_xml_0_4 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_3 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_1
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(3,9),c(1,2)> *)
| DP_R_xml_0_5 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_3 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_2
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(4,6),c(1,0)> *)
| DP_R_xml_0_6 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_4 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_0
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(4,7),c(1,1)> *)
| DP_R_xml_0_7 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_4 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_1
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(4,8),c(1,2)> *)
| DP_R_xml_0_8 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_4 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_2
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(4,9),c(1,3)> *)
| DP_R_xml_0_9 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_4 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_3
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(5,5),c(1,0)> *)
| DP_R_xml_0_10 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_5 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_5 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_0
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(5,6),c(1,1)> *)
| DP_R_xml_0_11 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_5 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_1
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(5,7),c(1,2)> *)
| DP_R_xml_0_12 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_5 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_2
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(5,8),c(1,3)> *)
| DP_R_xml_0_13 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_5 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_3
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(5,9),c(1,4)> *)
| DP_R_xml_0_14 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_5 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_4
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(6,4),c(1,0)> *)
| DP_R_xml_0_15 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_4 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_0
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(6,5),c(1,1)> *)
| DP_R_xml_0_16 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_5 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_1
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(6,6),c(1,2)> *)
| DP_R_xml_0_17 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_2
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(6,7),c(1,3)> *)
| DP_R_xml_0_18 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_3
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(6,8),c(1,4)> *)
| DP_R_xml_0_19 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_4
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(6,9),c(1,5)> *)
| DP_R_xml_0_20 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_5
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(7,3),c(1,0)> *)
| DP_R_xml_0_21 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_3 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_0
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(7,4),c(1,1)> *)
| DP_R_xml_0_22 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_4 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_1
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(7,5),c(1,2)> *)
| DP_R_xml_0_23 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_5 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_2
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(7,6),c(1,3)> *)
| DP_R_xml_0_24 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_3
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(7,7),c(1,4)> *)
| DP_R_xml_0_25 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_4
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(7,8),c(1,5)> *)
| DP_R_xml_0_26 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_5
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(7,9),c(1,6)> *)
| DP_R_xml_0_27 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_6
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(8,2),c(1,0)> *)
| DP_R_xml_0_28 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_2 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_0
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(8,3),c(1,1)> *)
| DP_R_xml_0_29 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_3 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_1
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(8,4),c(1,2)> *)
| DP_R_xml_0_30 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_4 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_2
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(8,5),c(1,3)> *)
| DP_R_xml_0_31 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_5 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_3
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(8,6),c(1,4)> *)
| DP_R_xml_0_32 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_4
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(8,7),c(1,5)> *)
| DP_R_xml_0_33 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_5
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(8,8),c(1,6)> *)
| DP_R_xml_0_34 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_6
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(8,9),c(1,7)> *)
| DP_R_xml_0_35 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_7
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(9,1),c(1,0)> *)
| DP_R_xml_0_36 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_1 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_0
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(9,2),c(1,1)> *)
| DP_R_xml_0_37 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_2 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_1
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(9,3),c(1,2)> *)
| DP_R_xml_0_38 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_3 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_2
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(9,4),c(1,3)> *)
| DP_R_xml_0_39 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_4 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_3
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(9,5),c(1,4)> *)
| DP_R_xml_0_40 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_5 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_4
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(9,6),c(1,5)> *)
| DP_R_xml_0_41 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_5
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(9,7),c(1,6)> *)
| DP_R_xml_0_42 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_6
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(9,8),c(1,7)> *)
| DP_R_xml_0_43 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_7
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(9,9),c(1,8)> *)
| DP_R_xml_0_44 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id_1 nil)::(algebra.Alg.Term algebra.F.id_8
nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(x_,c(y_,z_)),c(y_,+(x_,z_))> *)
| DP_R_xml_0_45 :
forall x2 x6 x1 x5 x3,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x1 x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_c (x2::x3::nil)) x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c (x2::(algebra.Alg.Term
algebra.F.id__plus_ (x1::x3::nil))::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(x_,c(y_,z_)),+(x_,z_)> *)
| DP_R_xml_0_46 :
forall x2 x6 x1 x5 x3,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x1 x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_c (x2::x3::nil)) x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id__plus_ (x1::x3::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(c(x_,y_),z_),c(x_,+(y_,z_))> *)
| DP_R_xml_0_47 :
forall x2 x6 x1 x5 x3,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_c (x1::x2::nil)) x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x3 x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c (x1::(algebra.Alg.Term
algebra.F.id__plus_ (x2::x3::nil))::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(c(x_,y_),z_),+(y_,z_)> *)
| DP_R_xml_0_48 :
forall x2 x6 x1 x5 x3,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_c (x1::x2::nil)) x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x3 x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id__plus_ (x2::x3::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <c(x_,c(y_,z_)),c(+(x_,y_),z_)> *)
| DP_R_xml_0_49 :
forall x2 x6 x1 x5 x3,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x1 x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_c (x2::x3::nil)) x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_c ((algebra.Alg.Term
algebra.F.id__plus_ (x1::x2::nil))::x3::nil))
(algebra.Alg.Term algebra.F.id_c (x6::x5::nil))
(* <c(x_,c(y_,z_)),+(x_,y_)> *)
| DP_R_xml_0_50 :
forall x2 x6 x1 x5 x3,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x1 x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_c (x2::x3::nil)) x5) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id__plus_ (x1::x2::nil))
(algebra.Alg.Term algebra.F.id_c (x6::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 :=
(* <+(9,9),c(1,8)> *)
| DP_R_xml_0_non_scc_1_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x5) ->
DP_R_xml_0_non_scc_1 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_8 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::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.
Inductive DP_R_xml_0_non_scc_2 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(9,8),c(1,7)> *)
| DP_R_xml_0_non_scc_2_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x5) ->
DP_R_xml_0_non_scc_2 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_7 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_2 :
forall x y,
(DP_R_xml_0_non_scc_2 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_non_scc_3 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(9,7),c(1,6)> *)
| DP_R_xml_0_non_scc_3_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x5) ->
DP_R_xml_0_non_scc_3 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_6 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::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;
(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_non_scc_4 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(9,6),c(1,5)> *)
| DP_R_xml_0_non_scc_4_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x5) ->
DP_R_xml_0_non_scc_4 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_5 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_4 :
forall x y,
(DP_R_xml_0_non_scc_4 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_non_scc_5 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(9,5),c(1,4)> *)
| DP_R_xml_0_non_scc_5_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_5 nil)
x5) ->
DP_R_xml_0_non_scc_5 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_4 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_5 :
forall x y,
(DP_R_xml_0_non_scc_5 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_non_scc_6 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(9,4),c(1,3)> *)
| DP_R_xml_0_non_scc_6_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_4 nil)
x5) ->
DP_R_xml_0_non_scc_6 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_3 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_6 :
forall x y,
(DP_R_xml_0_non_scc_6 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_non_scc_7 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(9,3),c(1,2)> *)
| DP_R_xml_0_non_scc_7_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_3 nil)
x5) ->
DP_R_xml_0_non_scc_7 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_2 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_7 :
forall x y,
(DP_R_xml_0_non_scc_7 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_non_scc_8 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(9,2),c(1,1)> *)
| DP_R_xml_0_non_scc_8_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_2 nil)
x5) ->
DP_R_xml_0_non_scc_8 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_1 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_8 :
forall x y,
(DP_R_xml_0_non_scc_8 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_non_scc_9 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(9,1),c(1,0)> *)
| DP_R_xml_0_non_scc_9_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_1 nil)
x5) ->
DP_R_xml_0_non_scc_9 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_0 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_9 :
forall x y,
(DP_R_xml_0_non_scc_9 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_non_scc_10 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(8,9),c(1,7)> *)
| DP_R_xml_0_non_scc_10_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x5) ->
DP_R_xml_0_non_scc_10 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_7 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_10 :
forall x y,
(DP_R_xml_0_non_scc_10 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_non_scc_11 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(8,8),c(1,6)> *)
| DP_R_xml_0_non_scc_11_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x5) ->
DP_R_xml_0_non_scc_11 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_6 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_11 :
forall x y,
(DP_R_xml_0_non_scc_11 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_non_scc_12 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(8,7),c(1,5)> *)
| DP_R_xml_0_non_scc_12_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x5) ->
DP_R_xml_0_non_scc_12 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_5 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_12 :
forall x y,
(DP_R_xml_0_non_scc_12 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_non_scc_13 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(8,6),c(1,4)> *)
| DP_R_xml_0_non_scc_13_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x5) ->
DP_R_xml_0_non_scc_13 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_4 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_13 :
forall x y,
(DP_R_xml_0_non_scc_13 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_non_scc_14 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(8,5),c(1,3)> *)
| DP_R_xml_0_non_scc_14_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_5 nil)
x5) ->
DP_R_xml_0_non_scc_14 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_3 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_14 :
forall x y,
(DP_R_xml_0_non_scc_14 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_non_scc_15 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(8,4),c(1,2)> *)
| DP_R_xml_0_non_scc_15_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_4 nil)
x5) ->
DP_R_xml_0_non_scc_15 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_2 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_15 :
forall x y,
(DP_R_xml_0_non_scc_15 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_non_scc_16 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(8,3),c(1,1)> *)
| DP_R_xml_0_non_scc_16_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_3 nil)
x5) ->
DP_R_xml_0_non_scc_16 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_1 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_16 :
forall x y,
(DP_R_xml_0_non_scc_16 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_non_scc_17 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(8,2),c(1,0)> *)
| DP_R_xml_0_non_scc_17_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_2 nil)
x5) ->
DP_R_xml_0_non_scc_17 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_0 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_17 :
forall x y,
(DP_R_xml_0_non_scc_17 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_non_scc_18 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(7,9),c(1,6)> *)
| DP_R_xml_0_non_scc_18_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x5) ->
DP_R_xml_0_non_scc_18 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_6 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_18 :
forall x y,
(DP_R_xml_0_non_scc_18 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_non_scc_19 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(7,8),c(1,5)> *)
| DP_R_xml_0_non_scc_19_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x5) ->
DP_R_xml_0_non_scc_19 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_5 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_19 :
forall x y,
(DP_R_xml_0_non_scc_19 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_non_scc_20 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(7,7),c(1,4)> *)
| DP_R_xml_0_non_scc_20_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x5) ->
DP_R_xml_0_non_scc_20 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_4 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_20 :
forall x y,
(DP_R_xml_0_non_scc_20 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_non_scc_21 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(7,6),c(1,3)> *)
| DP_R_xml_0_non_scc_21_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x5) ->
DP_R_xml_0_non_scc_21 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_3 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_21 :
forall x y,
(DP_R_xml_0_non_scc_21 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_non_scc_22 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(7,5),c(1,2)> *)
| DP_R_xml_0_non_scc_22_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_5 nil)
x5) ->
DP_R_xml_0_non_scc_22 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_2 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_22 :
forall x y,
(DP_R_xml_0_non_scc_22 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_non_scc_23 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(7,4),c(1,1)> *)
| DP_R_xml_0_non_scc_23_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_4 nil)
x5) ->
DP_R_xml_0_non_scc_23 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_1 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_23 :
forall x y,
(DP_R_xml_0_non_scc_23 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_non_scc_24 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(7,3),c(1,0)> *)
| DP_R_xml_0_non_scc_24_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_3 nil)
x5) ->
DP_R_xml_0_non_scc_24 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_0 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_24 :
forall x y,
(DP_R_xml_0_non_scc_24 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_non_scc_25 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(6,9),c(1,5)> *)
| DP_R_xml_0_non_scc_25_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x5) ->
DP_R_xml_0_non_scc_25 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_5 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_25 :
forall x y,
(DP_R_xml_0_non_scc_25 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_non_scc_26 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(6,8),c(1,4)> *)
| DP_R_xml_0_non_scc_26_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x5) ->
DP_R_xml_0_non_scc_26 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_4 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_26 :
forall x y,
(DP_R_xml_0_non_scc_26 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_non_scc_27 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(6,7),c(1,3)> *)
| DP_R_xml_0_non_scc_27_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x5) ->
DP_R_xml_0_non_scc_27 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_3 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_27 :
forall x y,
(DP_R_xml_0_non_scc_27 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_non_scc_28 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(6,6),c(1,2)> *)
| DP_R_xml_0_non_scc_28_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x5) ->
DP_R_xml_0_non_scc_28 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_2 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_28 :
forall x y,
(DP_R_xml_0_non_scc_28 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_non_scc_29 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(6,5),c(1,1)> *)
| DP_R_xml_0_non_scc_29_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_5 nil)
x5) ->
DP_R_xml_0_non_scc_29 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_1 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_29 :
forall x y,
(DP_R_xml_0_non_scc_29 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_non_scc_30 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(6,4),c(1,0)> *)
| DP_R_xml_0_non_scc_30_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_4 nil)
x5) ->
DP_R_xml_0_non_scc_30 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_0 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_30 :
forall x y,
(DP_R_xml_0_non_scc_30 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_non_scc_31 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(5,9),c(1,4)> *)
| DP_R_xml_0_non_scc_31_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_5 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x5) ->
DP_R_xml_0_non_scc_31 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_4 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_31 :
forall x y,
(DP_R_xml_0_non_scc_31 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_non_scc_32 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(5,8),c(1,3)> *)
| DP_R_xml_0_non_scc_32_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_5 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x5) ->
DP_R_xml_0_non_scc_32 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_3 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_32 :
forall x y,
(DP_R_xml_0_non_scc_32 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_non_scc_33 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(5,7),c(1,2)> *)
| DP_R_xml_0_non_scc_33_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_5 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x5) ->
DP_R_xml_0_non_scc_33 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_2 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_33 :
forall x y,
(DP_R_xml_0_non_scc_33 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_non_scc_34 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(5,6),c(1,1)> *)
| DP_R_xml_0_non_scc_34_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_5 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x5) ->
DP_R_xml_0_non_scc_34 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_1 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_34 :
forall x y,
(DP_R_xml_0_non_scc_34 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_non_scc_35 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(5,5),c(1,0)> *)
| DP_R_xml_0_non_scc_35_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_5 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_5 nil)
x5) ->
DP_R_xml_0_non_scc_35 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_0 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_35 :
forall x y,
(DP_R_xml_0_non_scc_35 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_non_scc_36 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(4,9),c(1,3)> *)
| DP_R_xml_0_non_scc_36_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_4 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x5) ->
DP_R_xml_0_non_scc_36 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_3 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_36 :
forall x y,
(DP_R_xml_0_non_scc_36 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_non_scc_37 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(4,8),c(1,2)> *)
| DP_R_xml_0_non_scc_37_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_4 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x5) ->
DP_R_xml_0_non_scc_37 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_2 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_37 :
forall x y,
(DP_R_xml_0_non_scc_37 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_non_scc_38 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(4,7),c(1,1)> *)
| DP_R_xml_0_non_scc_38_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_4 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x5) ->
DP_R_xml_0_non_scc_38 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_1 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_38 :
forall x y,
(DP_R_xml_0_non_scc_38 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_non_scc_39 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(4,6),c(1,0)> *)
| DP_R_xml_0_non_scc_39_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_4 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_6 nil)
x5) ->
DP_R_xml_0_non_scc_39 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_0 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_39 :
forall x y,
(DP_R_xml_0_non_scc_39 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_non_scc_40 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(3,9),c(1,2)> *)
| DP_R_xml_0_non_scc_40_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_3 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x5) ->
DP_R_xml_0_non_scc_40 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_2 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_40 :
forall x y,
(DP_R_xml_0_non_scc_40 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_non_scc_41 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(3,8),c(1,1)> *)
| DP_R_xml_0_non_scc_41_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_3 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x5) ->
DP_R_xml_0_non_scc_41 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_1 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_41 :
forall x y,
(DP_R_xml_0_non_scc_41 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_non_scc_42 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(3,7),c(1,0)> *)
| DP_R_xml_0_non_scc_42_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_3 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_7 nil)
x5) ->
DP_R_xml_0_non_scc_42 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_0 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_42 :
forall x y,
(DP_R_xml_0_non_scc_42 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_non_scc_43 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(2,9),c(1,1)> *)
| DP_R_xml_0_non_scc_43_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_2 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x5) ->
DP_R_xml_0_non_scc_43 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_1 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_43 :
forall x y,
(DP_R_xml_0_non_scc_43 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_non_scc_44 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(2,8),c(1,0)> *)
| DP_R_xml_0_non_scc_44_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_2 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_8 nil)
x5) ->
DP_R_xml_0_non_scc_44 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_0 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_44 :
forall x y,
(DP_R_xml_0_non_scc_44 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_non_scc_45 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(1,9),c(1,0)> *)
| DP_R_xml_0_non_scc_45_0 :
forall x6 x5,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_1 nil)
x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_9 nil)
x5) ->
DP_R_xml_0_non_scc_45 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id_1 nil)::
(algebra.Alg.Term algebra.F.id_0 nil)::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Lemma acc_DP_R_xml_0_non_scc_45 :
forall x y,
(DP_R_xml_0_non_scc_45 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_46 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <+(x_,c(y_,z_)),c(y_,+(x_,z_))> *)
| DP_R_xml_0_scc_46_0 :
forall x2 x6 x1 x5 x3,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x1 x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_c (x2::x3::nil)) x5) ->
DP_R_xml_0_scc_46 (algebra.Alg.Term algebra.F.id_c (x2::
(algebra.Alg.Term algebra.F.id__plus_ (x1::
x3::nil))::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <c(x_,c(y_,z_)),c(+(x_,y_),z_)> *)
| DP_R_xml_0_scc_46_1 :
forall x2 x6 x1 x5 x3,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x1 x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_c (x2::x3::nil)) x5) ->
DP_R_xml_0_scc_46 (algebra.Alg.Term algebra.F.id_c
((algebra.Alg.Term algebra.F.id__plus_ (x1::
x2::nil))::x3::nil))
(algebra.Alg.Term algebra.F.id_c (x6::x5::nil))
(* <c(x_,c(y_,z_)),+(x_,y_)> *)
| DP_R_xml_0_scc_46_2 :
forall x2 x6 x1 x5 x3,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x1 x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_c (x2::x3::nil)) x5) ->
DP_R_xml_0_scc_46 (algebra.Alg.Term algebra.F.id__plus_ (x1::
x2::nil))
(algebra.Alg.Term algebra.F.id_c (x6::x5::nil))
(* <+(x_,c(y_,z_)),+(x_,z_)> *)
| DP_R_xml_0_scc_46_3 :
forall x2 x6 x1 x5 x3,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x1 x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_c (x2::x3::nil)) x5) ->
DP_R_xml_0_scc_46 (algebra.Alg.Term algebra.F.id__plus_ (x1::
x3::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(c(x_,y_),z_),c(x_,+(y_,z_))> *)
| DP_R_xml_0_scc_46_4 :
forall x2 x6 x1 x5 x3,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_c (x1::x2::nil)) x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x3 x5) ->
DP_R_xml_0_scc_46 (algebra.Alg.Term algebra.F.id_c (x1::
(algebra.Alg.Term algebra.F.id__plus_ (x2::
x3::nil))::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
(* <+(c(x_,y_),z_),+(y_,z_)> *)
| DP_R_xml_0_scc_46_5 :
forall x2 x6 x1 x5 x3,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_c (x1::x2::nil)) x6) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x3 x5) ->
DP_R_xml_0_scc_46 (algebra.Alg.Term algebra.F.id__plus_ (x2::
x3::nil))
(algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil))
.
Module WF_DP_R_xml_0_scc_46.
Open Scope Z_scope.
Import ring_extention.
Notation Local "a <= b" := (Zle a b).
Notation Local "a < b" := (Zlt a b).
Definition P_id__plus_ (x5:Z) (x6:Z) := 1* x5 + 1* x6.
Definition P_id_7 := 2.
Definition P_id_3 := 1.
Definition P_id_1 := 1.
Definition P_id_9 := 2.
Definition P_id_5 := 1.
Definition P_id_0 := 0.
Definition P_id_8 := 2.
Definition P_id_4 := 1.
Definition P_id_2 := 1.
Definition P_id_c (x5:Z) (x6:Z) := 1 + 1* x5 + 1* x6.
Definition P_id_6 := 2.
Lemma P_id__plus__monotonic :
forall x8 x6 x5 x7,
(0 <= x8)/\ (x8 <= x7) ->
(0 <= x6)/\ (x6 <= x5) ->P_id__plus_ x6 x8 <= P_id__plus_ x5 x7.
Proof.
intros x8 x7 x6 x5.
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_c_monotonic :
forall x8 x6 x5 x7,
(0 <= x8)/\ (x8 <= x7) ->
(0 <= x6)/\ (x6 <= x5) ->P_id_c x6 x8 <= P_id_c x5 x7.
Proof.
intros x8 x7 x6 x5.
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__plus__bounded :
forall x6 x5, (0 <= x5) ->(0 <= x6) ->0 <= P_id__plus_ x6 x5.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_7_bounded : 0 <= P_id_7 .
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_3_bounded : 0 <= P_id_3 .
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_1_bounded : 0 <= P_id_1 .
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_9_bounded : 0 <= P_id_9 .
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_5_bounded : 0 <= P_id_5 .
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_8_bounded : 0 <= P_id_8 .
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_4_bounded : 0 <= P_id_4 .
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_2_bounded : 0 <= P_id_2 .
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_c_bounded :
forall x6 x5, (0 <= x5) ->(0 <= x6) ->0 <= P_id_c x6 x5.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_6_bounded : 0 <= P_id_6 .
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__plus_ P_id_7 P_id_3 P_id_1 P_id_9 P_id_5
P_id_0 P_id_8 P_id_4 P_id_2 P_id_c P_id_6.
Lemma measure_equation :
forall t,
measure t = match t with
| (algebra.Alg.Term algebra.F.id__plus_ (x6::x5::nil)) =>
P_id__plus_ (measure x6) (measure x5)
| (algebra.Alg.Term algebra.F.id_7 nil) => P_id_7
| (algebra.Alg.Term algebra.F.id_3 nil) => P_id_3
| (algebra.Alg.Term algebra.F.id_1 nil) => P_id_1
| (algebra.Alg.Term algebra.F.id_9 nil) => P_id_9
| (algebra.Alg.Term algebra.F.id_5 nil) => P_id_5
| (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0
| (algebra.Alg.Term algebra.F.id_8 nil) => P_id_8
| (algebra.Alg.Term algebra.F.id_4 nil) => P_id_4
| (algebra.Alg.Term algebra.F.id_2 nil) => P_id_2
| (algebra.Alg.Term algebra.F.id_c (x6::x5::nil)) =>
P_id_c (measure x6) (measure x5)
| (algebra.Alg.Term algebra.F.id_6 nil) => P_id_6
| _ => 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__plus__monotonic;assumption.
intros ;apply P_id_c_monotonic;assumption.
intros ;apply P_id__plus__bounded;assumption.
intros ;apply P_id_7_bounded;assumption.
intros ;apply P_id_3_bounded;assumption.
intros ;apply P_id_1_bounded;assumption.
intros ;apply P_id_9_bounded;assumption.
intros ;apply P_id_5_bounded;assumption.
intros ;apply P_id_0_bounded;assumption.
intros ;apply P_id_8_bounded;assumption.
intros ;apply P_id_4_bounded;assumption.
intros ;apply P_id_2_bounded;assumption.
intros ;apply P_id_c_bounded;assumption.
intros ;apply P_id_6_bounded;assumption.
apply rules_monotonic.
Qed.
Definition P_id__plus__hat_1 (x5:Z) (x6:Z) := 1* x5 + 1* x6.
Definition P_id_C (x5:Z) (x6:Z) := 1* x5 + 1* x6.
Lemma P_id__plus__hat_1_monotonic :
forall x8 x6 x5 x7,
(0 <= x8)/\ (x8 <= x7) ->
(0 <= x6)/\ (x6 <= x5) ->
P_id__plus__hat_1 x6 x8 <= P_id__plus__hat_1 x5 x7.
Proof.
intros x8 x7 x6 x5.
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_C_monotonic :
forall x8 x6 x5 x7,
(0 <= x8)/\ (x8 <= x7) ->
(0 <= x6)/\ (x6 <= x5) ->P_id_C x6 x8 <= P_id_C x5 x7.
Proof.
intros x8 x7 x6 x5.
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.
Definition marked_measure :=
InterpZ.marked_measure 0 P_id__plus_ P_id_7 P_id_3 P_id_1 P_id_9
P_id_5 P_id_0 P_id_8 P_id_4 P_id_2 P_id_c P_id_6 P_id__plus__hat_1
P_id_C.
Lemma marked_measure_equation :
forall t,
marked_measure t = match t with
| (algebra.Alg.Term algebra.F.id__plus_ (x6::
x5::nil)) =>
P_id__plus__hat_1 (measure x6) (measure x5)
| (algebra.Alg.Term algebra.F.id_c (x6::x5::nil)) =>
P_id_C (measure x6) (measure x5)
| _ => 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__plus__monotonic;assumption.
intros ;apply P_id_c_monotonic;assumption.
intros ;apply P_id__plus__bounded;assumption.
intros ;apply P_id_7_bounded;assumption.
intros ;apply P_id_3_bounded;assumption.
intros ;apply P_id_1_bounded;assumption.
intros ;apply P_id_9_bounded;assumption.
intros ;apply P_id_5_bounded;assumption.
intros ;apply P_id_0_bounded;assumption.
intros ;apply P_id_8_bounded;assumption.
intros ;apply P_id_4_bounded;assumption.
intros ;apply P_id_2_bounded;assumption.
intros ;apply P_id_c_bounded;assumption.
intros ;apply P_id_6_bounded;assumption.
apply rules_monotonic.
intros ;apply P_id__plus__hat_1_monotonic;assumption.
intros ;apply P_id_C_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_46.
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_46.
Definition wf_DP_R_xml_0_scc_46 := WF_DP_R_xml_0_scc_46.wf.
Lemma acc_DP_R_xml_0_scc_46 :
forall x y, (DP_R_xml_0_scc_46 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_46).
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_45;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_44;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_43;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_42;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_41;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_40;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_39;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_38;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_37;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_36;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_35;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_34;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_33;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_32;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_31;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_30;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_29;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_28;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_27;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_26;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_25;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_24;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_23;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_22;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_21;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_20;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_19;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_18;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_17;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_16;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_15;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_14;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_13;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_12;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_11;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_10;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_9;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_8;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_7;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_6;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_5;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_4;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((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' ))||
((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_46.
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_45;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_44;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_43;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_42;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_41;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_40;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_39;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_38;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_37;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_36;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_35;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_34;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_33;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_32;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_31;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_30;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_29;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_28;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_27;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_26;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_25;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_24;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_23;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_22;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_21;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_20;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_19;
econstructor
(eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_18;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_17;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_16;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_15;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_14;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_13;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_12;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_11;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_10;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_9;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_8;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_7;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_6;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_5;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_4;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((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_46;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_scc_45;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_scc_44;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_scc_43;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_scc_42;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_scc_41;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_scc_40;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_scc_39;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_scc_38;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_scc_37;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply
acc_DP_R_xml_0_scc_36;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply
acc_DP_R_xml_0_scc_35;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply
acc_DP_R_xml_0_scc_34;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply
acc_DP_R_xml_0_scc_33;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply
acc_DP_R_xml_0_scc_32;
econstructor
(eassumption)||
(algebra.Alg_ext.star_refl' ))||
((eapply
acc_DP_R_xml_0_scc_31;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
((eapply
acc_DP_R_xml_0_scc_30;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
((
eapply
acc_DP_R_xml_0_scc_29;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_28;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_27;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_26;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_25;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_24;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_23;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_22;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_21;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_20;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_19;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_18;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_17;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_16;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_15;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_14;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_13;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_12;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_11;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_10;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_9;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_8;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_7;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_6;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_5;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_4;
econstructor
(
eassumption)||
(
algebra.Alg_ext.star_refl' ))||
(
(
eapply
acc_DP_R_xml_0_scc_3;
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___HM___t000.trs/a3pat.v" ***
*** End: ***
*)