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_lt *)
| id_lt : symb
(* id_split *)
| id_split : symb
(* id_false *)
| id_false : symb
(* id_qsort *)
| id_qsort : symb
(* id_s *)
| id_s : symb
(* id_f_1 *)
| id_f_1 : symb
(* id_nil *)
| id_nil : symb
(* id_0 *)
| id_0 : symb
(* id_pair *)
| id_pair : symb
(* id_append *)
| id_append : symb
(* id_f_3 *)
| id_f_3 : symb
(* id_true *)
| id_true : symb
(* id_f_2 *)
| id_f_2 : symb
(* id_add *)
| id_add : symb
.
Definition symb_eq_bool (f1 f2:symb) : bool :=
match f1,f2 with
| id_lt,id_lt => true
| id_split,id_split => true
| id_false,id_false => true
| id_qsort,id_qsort => true
| id_s,id_s => true
| id_f_1,id_f_1 => true
| id_nil,id_nil => true
| id_0,id_0 => true
| id_pair,id_pair => true
| id_append,id_append => true
| id_f_3,id_f_3 => true
| id_true,id_true => true
| id_f_2,id_f_2 => true
| id_add,id_add => true
| _,_ => false
end.
(* Proof of decidability of equality over symb *)
Definition symb_eq_bool_ok(f1 f2:symb) :
match symb_eq_bool f1 f2 with
| true => f1 = f2
| false => f1 <> f2
end.
Proof.
intros f1 f2.
refine match f1 as u1,f2 as u2 return
match symb_eq_bool u1 u2 return
Prop with
| true => u1 = u2
| false => u1 <> u2
end with
| id_lt,id_lt => refl_equal _
| id_split,id_split => refl_equal _
| id_false,id_false => refl_equal _
| id_qsort,id_qsort => refl_equal _
| id_s,id_s => refl_equal _
| id_f_1,id_f_1 => refl_equal _
| id_nil,id_nil => refl_equal _
| id_0,id_0 => refl_equal _
| id_pair,id_pair => refl_equal _
| id_append,id_append => refl_equal _
| id_f_3,id_f_3 => refl_equal _
| id_true,id_true => refl_equal _
| id_f_2,id_f_2 => refl_equal _
| id_add,id_add => refl_equal _
| _,_ => _
end;intros abs;discriminate.
Defined.
Definition arity (f:symb) :=
match f with
| id_lt => term.Free 2
| id_split => term.Free 2
| id_false => term.Free 0
| id_qsort => term.Free 1
| id_s => term.Free 1
| id_f_1 => term.Free 4
| id_nil => term.Free 0
| id_0 => term.Free 0
| id_pair => term.Free 2
| id_append => term.Free 2
| id_f_3 => term.Free 3
| id_true => term.Free 0
| id_f_2 => term.Free 6
| id_add => term.Free 2
end.
Definition symb_order (f1 f2:symb) : bool :=
match f1,f2 with
| id_lt,id_lt => true
| id_lt,id_split => false
| id_lt,id_false => false
| id_lt,id_qsort => false
| id_lt,id_s => false
| id_lt,id_f_1 => false
| id_lt,id_nil => false
| id_lt,id_0 => false
| id_lt,id_pair => false
| id_lt,id_append => false
| id_lt,id_f_3 => false
| id_lt,id_true => false
| id_lt,id_f_2 => false
| id_lt,id_add => false
| id_split,id_lt => true
| id_split,id_split => true
| id_split,id_false => false
| id_split,id_qsort => false
| id_split,id_s => false
| id_split,id_f_1 => false
| id_split,id_nil => false
| id_split,id_0 => false
| id_split,id_pair => false
| id_split,id_append => false
| id_split,id_f_3 => false
| id_split,id_true => false
| id_split,id_f_2 => false
| id_split,id_add => false
| id_false,id_lt => true
| id_false,id_split => true
| id_false,id_false => true
| id_false,id_qsort => false
| id_false,id_s => false
| id_false,id_f_1 => false
| id_false,id_nil => false
| id_false,id_0 => false
| id_false,id_pair => false
| id_false,id_append => false
| id_false,id_f_3 => false
| id_false,id_true => false
| id_false,id_f_2 => false
| id_false,id_add => false
| id_qsort,id_lt => true
| id_qsort,id_split => true
| id_qsort,id_false => true
| id_qsort,id_qsort => true
| id_qsort,id_s => false
| id_qsort,id_f_1 => false
| id_qsort,id_nil => false
| id_qsort,id_0 => false
| id_qsort,id_pair => false
| id_qsort,id_append => false
| id_qsort,id_f_3 => false
| id_qsort,id_true => false
| id_qsort,id_f_2 => false
| id_qsort,id_add => false
| id_s,id_lt => true
| id_s,id_split => true
| id_s,id_false => true
| id_s,id_qsort => true
| id_s,id_s => true
| id_s,id_f_1 => false
| id_s,id_nil => false
| id_s,id_0 => false
| id_s,id_pair => false
| id_s,id_append => false
| id_s,id_f_3 => false
| id_s,id_true => false
| id_s,id_f_2 => false
| id_s,id_add => false
| id_f_1,id_lt => true
| id_f_1,id_split => true
| id_f_1,id_false => true
| id_f_1,id_qsort => true
| id_f_1,id_s => true
| id_f_1,id_f_1 => true
| id_f_1,id_nil => false
| id_f_1,id_0 => false
| id_f_1,id_pair => false
| id_f_1,id_append => false
| id_f_1,id_f_3 => false
| id_f_1,id_true => false
| id_f_1,id_f_2 => false
| id_f_1,id_add => false
| id_nil,id_lt => true
| id_nil,id_split => true
| id_nil,id_false => true
| id_nil,id_qsort => true
| id_nil,id_s => true
| id_nil,id_f_1 => true
| id_nil,id_nil => true
| id_nil,id_0 => false
| id_nil,id_pair => false
| id_nil,id_append => false
| id_nil,id_f_3 => false
| id_nil,id_true => false
| id_nil,id_f_2 => false
| id_nil,id_add => false
| id_0,id_lt => true
| id_0,id_split => true
| id_0,id_false => true
| id_0,id_qsort => true
| id_0,id_s => true
| id_0,id_f_1 => true
| id_0,id_nil => true
| id_0,id_0 => true
| id_0,id_pair => false
| id_0,id_append => false
| id_0,id_f_3 => false
| id_0,id_true => false
| id_0,id_f_2 => false
| id_0,id_add => false
| id_pair,id_lt => true
| id_pair,id_split => true
| id_pair,id_false => true
| id_pair,id_qsort => true
| id_pair,id_s => true
| id_pair,id_f_1 => true
| id_pair,id_nil => true
| id_pair,id_0 => true
| id_pair,id_pair => true
| id_pair,id_append => false
| id_pair,id_f_3 => false
| id_pair,id_true => false
| id_pair,id_f_2 => false
| id_pair,id_add => false
| id_append,id_lt => true
| id_append,id_split => true
| id_append,id_false => true
| id_append,id_qsort => true
| id_append,id_s => true
| id_append,id_f_1 => true
| id_append,id_nil => true
| id_append,id_0 => true
| id_append,id_pair => true
| id_append,id_append => true
| id_append,id_f_3 => false
| id_append,id_true => false
| id_append,id_f_2 => false
| id_append,id_add => false
| id_f_3,id_lt => true
| id_f_3,id_split => true
| id_f_3,id_false => true
| id_f_3,id_qsort => true
| id_f_3,id_s => true
| id_f_3,id_f_1 => true
| id_f_3,id_nil => true
| id_f_3,id_0 => true
| id_f_3,id_pair => true
| id_f_3,id_append => true
| id_f_3,id_f_3 => true
| id_f_3,id_true => false
| id_f_3,id_f_2 => false
| id_f_3,id_add => false
| id_true,id_lt => true
| id_true,id_split => true
| id_true,id_false => true
| id_true,id_qsort => true
| id_true,id_s => true
| id_true,id_f_1 => true
| id_true,id_nil => true
| id_true,id_0 => true
| id_true,id_pair => true
| id_true,id_append => true
| id_true,id_f_3 => true
| id_true,id_true => true
| id_true,id_f_2 => false
| id_true,id_add => false
| id_f_2,id_lt => true
| id_f_2,id_split => true
| id_f_2,id_false => true
| id_f_2,id_qsort => true
| id_f_2,id_s => true
| id_f_2,id_f_1 => true
| id_f_2,id_nil => true
| id_f_2,id_0 => true
| id_f_2,id_pair => true
| id_f_2,id_append => true
| id_f_2,id_f_3 => true
| id_f_2,id_true => true
| id_f_2,id_f_2 => true
| id_f_2,id_add => false
| id_add,id_lt => true
| id_add,id_split => true
| id_add,id_false => true
| id_add,id_qsort => true
| id_add,id_s => true
| id_add,id_f_1 => true
| id_add,id_nil => true
| id_add,id_0 => true
| id_add,id_pair => true
| id_add,id_append => true
| id_add,id_f_3 => true
| id_add,id_true => true
| id_add,id_f_2 => true
| id_add,id_add => true
end.
Module Symb.
Definition A := symb.
Definition eq_A := @eq A.
Definition eq_proof : equivalence A eq_A.
Proof.
constructor.
red ;reflexivity .
red ;intros ;transitivity y ;assumption.
red ;intros ;symmetry ;assumption.
Defined.
Add Relation A eq_A
reflexivity proved by (@equiv_refl _ _ eq_proof)
symmetry proved by (@equiv_sym _ _ eq_proof)
transitivity proved by (@equiv_trans _ _ eq_proof) as EQA
.
Definition eq_bool := symb_eq_bool.
Definition eq_bool_ok := symb_eq_bool_ok.
End Symb.
Export Symb.
End F.
Module Alg := term.Make'(F)(term_extension.IntVars).
Module Alg_ext := term_extension.Make(Alg).
Module EQT := equational_theory.Make(Alg).
Module EQT_ext := equational_extension.Make(EQT).
End algebra.
Module R_xml_0_deep_rew.
Inductive R_xml_0_rules :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* lt(0,s(X_)) -> true *)
| R_xml_0_rule_0 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_true nil)
(algebra.Alg.Term algebra.F.id_lt ((algebra.Alg.Term algebra.F.id_0
nil)::(algebra.Alg.Term algebra.F.id_s
((algebra.Alg.Var 1)::nil))::nil))
(* lt(s(X_),0) -> false *)
| R_xml_0_rule_1 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_false nil)
(algebra.Alg.Term algebra.F.id_lt ((algebra.Alg.Term algebra.F.id_s
((algebra.Alg.Var 1)::nil))::(algebra.Alg.Term algebra.F.id_0
nil)::nil))
(* lt(s(X_),s(Y_)) -> lt(X_,Y_) *)
| R_xml_0_rule_2 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_lt ((algebra.Alg.Var 1)::
(algebra.Alg.Var 2)::nil))
(algebra.Alg.Term algebra.F.id_lt ((algebra.Alg.Term algebra.F.id_s
((algebra.Alg.Var 1)::nil))::(algebra.Alg.Term algebra.F.id_s
((algebra.Alg.Var 2)::nil))::nil))
(* append(nil,Y_) -> Y_ *)
| R_xml_0_rule_3 :
R_xml_0_rules (algebra.Alg.Var 2)
(algebra.Alg.Term algebra.F.id_append ((algebra.Alg.Term
algebra.F.id_nil nil)::(algebra.Alg.Var 2)::nil))
(* append(add(N_,X_),Y_) -> add(N_,append(X_,Y_)) *)
| R_xml_0_rule_4 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_add ((algebra.Alg.Var 3)::
(algebra.Alg.Term algebra.F.id_append
((algebra.Alg.Var 1)::(algebra.Alg.Var 2)::nil))::nil))
(algebra.Alg.Term algebra.F.id_append ((algebra.Alg.Term
algebra.F.id_add ((algebra.Alg.Var 3)::(algebra.Alg.Var 1)::nil))::
(algebra.Alg.Var 2)::nil))
(* split(N_,nil) -> pair(nil,nil) *)
| R_xml_0_rule_5 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_pair ((algebra.Alg.Term
algebra.F.id_nil nil)::(algebra.Alg.Term algebra.F.id_nil
nil)::nil))
(algebra.Alg.Term algebra.F.id_split ((algebra.Alg.Var 3)::
(algebra.Alg.Term algebra.F.id_nil nil)::nil))
(* split(N_,add(M_,Y_)) -> f_1(split(N_,Y_),N_,M_,Y_) *)
| R_xml_0_rule_6 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_f_1 ((algebra.Alg.Term
algebra.F.id_split ((algebra.Alg.Var 3)::
(algebra.Alg.Var 2)::nil))::(algebra.Alg.Var 3)::
(algebra.Alg.Var 4)::(algebra.Alg.Var 2)::nil))
(algebra.Alg.Term algebra.F.id_split ((algebra.Alg.Var 3)::
(algebra.Alg.Term algebra.F.id_add ((algebra.Alg.Var 4)::
(algebra.Alg.Var 2)::nil))::nil))
(* f_1(pair(X_,Z_),N_,M_,Y_) -> f_2(lt(N_,M_),N_,M_,Y_,X_,Z_) *)
| R_xml_0_rule_7 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_f_2 ((algebra.Alg.Term
algebra.F.id_lt ((algebra.Alg.Var 3)::
(algebra.Alg.Var 4)::nil))::(algebra.Alg.Var 3)::
(algebra.Alg.Var 4)::(algebra.Alg.Var 2)::
(algebra.Alg.Var 1)::(algebra.Alg.Var 5)::nil))
(algebra.Alg.Term algebra.F.id_f_1 ((algebra.Alg.Term algebra.F.id_pair
((algebra.Alg.Var 1)::(algebra.Alg.Var 5)::nil))::(algebra.Alg.Var 3)::
(algebra.Alg.Var 4)::(algebra.Alg.Var 2)::nil))
(* f_2(true,N_,M_,Y_,X_,Z_) -> pair(X_,add(M_,Z_)) *)
| R_xml_0_rule_8 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_pair ((algebra.Alg.Var 1)::
(algebra.Alg.Term algebra.F.id_add ((algebra.Alg.Var 4)::
(algebra.Alg.Var 5)::nil))::nil))
(algebra.Alg.Term algebra.F.id_f_2 ((algebra.Alg.Term algebra.F.id_true
nil)::(algebra.Alg.Var 3)::(algebra.Alg.Var 4)::(algebra.Alg.Var 2)::
(algebra.Alg.Var 1)::(algebra.Alg.Var 5)::nil))
(* f_2(false,N_,M_,Y_,X_,Z_) -> pair(add(M_,X_),Z_) *)
| R_xml_0_rule_9 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_pair ((algebra.Alg.Term
algebra.F.id_add ((algebra.Alg.Var 4)::
(algebra.Alg.Var 1)::nil))::(algebra.Alg.Var 5)::nil))
(algebra.Alg.Term algebra.F.id_f_2 ((algebra.Alg.Term
algebra.F.id_false nil)::(algebra.Alg.Var 3)::(algebra.Alg.Var 4)::
(algebra.Alg.Var 2)::(algebra.Alg.Var 1)::(algebra.Alg.Var 5)::nil))
(* qsort(nil) -> nil *)
| R_xml_0_rule_10 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_nil nil)
(algebra.Alg.Term algebra.F.id_qsort ((algebra.Alg.Term
algebra.F.id_nil nil)::nil))
(* qsort(add(N_,X_)) -> f_3(split(N_,X_),N_,X_) *)
| R_xml_0_rule_11 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_f_3 ((algebra.Alg.Term
algebra.F.id_split ((algebra.Alg.Var 3)::
(algebra.Alg.Var 1)::nil))::(algebra.Alg.Var 3)::
(algebra.Alg.Var 1)::nil))
(algebra.Alg.Term algebra.F.id_qsort ((algebra.Alg.Term
algebra.F.id_add ((algebra.Alg.Var 3)::
(algebra.Alg.Var 1)::nil))::nil))
(* f_3(pair(Y_,Z_),N_,X_) -> append(qsort(Y_),add(X_,qsort(Z_))) *)
| R_xml_0_rule_12 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_append ((algebra.Alg.Term
algebra.F.id_qsort ((algebra.Alg.Var 2)::nil))::
(algebra.Alg.Term algebra.F.id_add ((algebra.Alg.Var 1)::
(algebra.Alg.Term algebra.F.id_qsort
((algebra.Alg.Var 5)::nil))::nil))::nil))
(algebra.Alg.Term algebra.F.id_f_3 ((algebra.Alg.Term algebra.F.id_pair
((algebra.Alg.Var 2)::(algebra.Alg.Var 5)::nil))::(algebra.Alg.Var 3)::
(algebra.Alg.Var 1)::nil))
.
Definition R_xml_0_rule_as_list_0 :=
((algebra.Alg.Term algebra.F.id_lt ((algebra.Alg.Term algebra.F.id_0
nil)::(algebra.Alg.Term algebra.F.id_s
((algebra.Alg.Var 1)::nil))::nil)),
(algebra.Alg.Term algebra.F.id_true nil))::nil.
Definition R_xml_0_rule_as_list_1 :=
((algebra.Alg.Term algebra.F.id_lt ((algebra.Alg.Term algebra.F.id_s
((algebra.Alg.Var 1)::nil))::(algebra.Alg.Term algebra.F.id_0
nil)::nil)),(algebra.Alg.Term algebra.F.id_false nil))::
R_xml_0_rule_as_list_0.
Definition R_xml_0_rule_as_list_2 :=
((algebra.Alg.Term algebra.F.id_lt ((algebra.Alg.Term algebra.F.id_s
((algebra.Alg.Var 1)::nil))::(algebra.Alg.Term algebra.F.id_s
((algebra.Alg.Var 2)::nil))::nil)),
(algebra.Alg.Term algebra.F.id_lt ((algebra.Alg.Var 1)::
(algebra.Alg.Var 2)::nil)))::R_xml_0_rule_as_list_1.
Definition R_xml_0_rule_as_list_3 :=
((algebra.Alg.Term algebra.F.id_append ((algebra.Alg.Term
algebra.F.id_nil nil)::(algebra.Alg.Var 2)::nil)),(algebra.Alg.Var 2))::
R_xml_0_rule_as_list_2.
Definition R_xml_0_rule_as_list_4 :=
((algebra.Alg.Term algebra.F.id_append ((algebra.Alg.Term
algebra.F.id_add ((algebra.Alg.Var 3)::(algebra.Alg.Var 1)::nil))::
(algebra.Alg.Var 2)::nil)),
(algebra.Alg.Term algebra.F.id_add ((algebra.Alg.Var 3)::
(algebra.Alg.Term algebra.F.id_append ((algebra.Alg.Var 1)::
(algebra.Alg.Var 2)::nil))::nil)))::R_xml_0_rule_as_list_3.
Definition R_xml_0_rule_as_list_5 :=
((algebra.Alg.Term algebra.F.id_split ((algebra.Alg.Var 3)::
(algebra.Alg.Term algebra.F.id_nil nil)::nil)),
(algebra.Alg.Term algebra.F.id_pair ((algebra.Alg.Term algebra.F.id_nil
nil)::(algebra.Alg.Term algebra.F.id_nil nil)::nil)))::
R_xml_0_rule_as_list_4.
Definition R_xml_0_rule_as_list_6 :=
((algebra.Alg.Term algebra.F.id_split ((algebra.Alg.Var 3)::
(algebra.Alg.Term algebra.F.id_add ((algebra.Alg.Var 4)::
(algebra.Alg.Var 2)::nil))::nil)),
(algebra.Alg.Term algebra.F.id_f_1 ((algebra.Alg.Term algebra.F.id_split
((algebra.Alg.Var 3)::(algebra.Alg.Var 2)::nil))::(algebra.Alg.Var 3)::
(algebra.Alg.Var 4)::(algebra.Alg.Var 2)::nil)))::R_xml_0_rule_as_list_5
.
Definition R_xml_0_rule_as_list_7 :=
((algebra.Alg.Term algebra.F.id_f_1 ((algebra.Alg.Term algebra.F.id_pair
((algebra.Alg.Var 1)::(algebra.Alg.Var 5)::nil))::(algebra.Alg.Var 3)::
(algebra.Alg.Var 4)::(algebra.Alg.Var 2)::nil)),
(algebra.Alg.Term algebra.F.id_f_2 ((algebra.Alg.Term algebra.F.id_lt
((algebra.Alg.Var 3)::(algebra.Alg.Var 4)::nil))::(algebra.Alg.Var 3)::
(algebra.Alg.Var 4)::(algebra.Alg.Var 2)::(algebra.Alg.Var 1)::
(algebra.Alg.Var 5)::nil)))::R_xml_0_rule_as_list_6.
Definition R_xml_0_rule_as_list_8 :=
((algebra.Alg.Term algebra.F.id_f_2 ((algebra.Alg.Term algebra.F.id_true
nil)::(algebra.Alg.Var 3)::(algebra.Alg.Var 4)::(algebra.Alg.Var 2)::
(algebra.Alg.Var 1)::(algebra.Alg.Var 5)::nil)),
(algebra.Alg.Term algebra.F.id_pair ((algebra.Alg.Var 1)::
(algebra.Alg.Term algebra.F.id_add ((algebra.Alg.Var 4)::
(algebra.Alg.Var 5)::nil))::nil)))::R_xml_0_rule_as_list_7.
Definition R_xml_0_rule_as_list_9 :=
((algebra.Alg.Term algebra.F.id_f_2 ((algebra.Alg.Term algebra.F.id_false
nil)::(algebra.Alg.Var 3)::(algebra.Alg.Var 4)::(algebra.Alg.Var 2)::
(algebra.Alg.Var 1)::(algebra.Alg.Var 5)::nil)),
(algebra.Alg.Term algebra.F.id_pair ((algebra.Alg.Term algebra.F.id_add
((algebra.Alg.Var 4)::(algebra.Alg.Var 1)::nil))::
(algebra.Alg.Var 5)::nil)))::R_xml_0_rule_as_list_8.
Definition R_xml_0_rule_as_list_10 :=
((algebra.Alg.Term algebra.F.id_qsort ((algebra.Alg.Term algebra.F.id_nil
nil)::nil)),(algebra.Alg.Term algebra.F.id_nil nil))::
R_xml_0_rule_as_list_9.
Definition R_xml_0_rule_as_list_11 :=
((algebra.Alg.Term algebra.F.id_qsort ((algebra.Alg.Term algebra.F.id_add
((algebra.Alg.Var 3)::(algebra.Alg.Var 1)::nil))::nil)),
(algebra.Alg.Term algebra.F.id_f_3 ((algebra.Alg.Term algebra.F.id_split
((algebra.Alg.Var 3)::(algebra.Alg.Var 1)::nil))::(algebra.Alg.Var 3)::
(algebra.Alg.Var 1)::nil)))::R_xml_0_rule_as_list_10.
Definition R_xml_0_rule_as_list_12 :=
((algebra.Alg.Term algebra.F.id_f_3 ((algebra.Alg.Term algebra.F.id_pair
((algebra.Alg.Var 2)::(algebra.Alg.Var 5)::nil))::(algebra.Alg.Var 3)::
(algebra.Alg.Var 1)::nil)),
(algebra.Alg.Term algebra.F.id_append ((algebra.Alg.Term
algebra.F.id_qsort ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Term
algebra.F.id_add ((algebra.Alg.Var 1)::(algebra.Alg.Term
algebra.F.id_qsort ((algebra.Alg.Var 5)::nil))::nil))::nil)))::
R_xml_0_rule_as_list_11.
Definition R_xml_0_rule_as_list := R_xml_0_rule_as_list_12.
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.or14_equiv in H|-.
case H;clear H;intros H.
injection H;intros ;subst;constructor 13.
injection H;intros ;subst;constructor 12.
injection H;intros ;subst;constructor 11.
injection H;intros ;subst;constructor 10.
injection H;intros ;subst;constructor 9.
injection H;intros ;subst;constructor 8.
injection H;intros ;subst;constructor 7.
injection H;intros ;subst;constructor 6.
injection H;intros ;subst;constructor 5.
injection H;intros ;subst;constructor 4.
injection H;intros ;subst;constructor 3.
injection H;intros ;subst;constructor 2.
injection H;intros ;subst;constructor 1.
elim H.
Qed.
Lemma R_xml_0_non_var : forall x t, ~R_xml_0_rules t (algebra.EQT.T.Var x).
Proof.
intros x t H.
inversion H.
Qed.
Lemma R_xml_0_reg :
forall s t,
(R_xml_0_rules s t) ->
forall x, In x (algebra.Alg.var_list s) ->In x (algebra.Alg.var_list t).
Proof.
intros s t H.
inversion H;intros x Hx;
(apply (more_list.mem_impl_in (@eq algebra.Alg.variable));[tauto|idtac]);
apply (more_list.in_impl_mem (@eq algebra.Alg.variable)) in Hx;
vm_compute in Hx|-*;tauto.
Qed.
Inductive and_7 (x7 x8 x9 x10 x11 x12 x13:Prop) :
Prop :=
| conj_7 : x7->x8->x9->x10->x11->x12->x13->and_7 x7 x8 x9 x10 x11 x12 x13
.
Lemma are_constuctors_of_R_xml_0 :
forall t t',
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
and_7 (t = (algebra.Alg.Term algebra.F.id_false nil) ->
t' = (algebra.Alg.Term algebra.F.id_false nil))
(forall x8,
t = (algebra.Alg.Term algebra.F.id_s (x8::nil)) ->
exists x7,
t' = (algebra.Alg.Term algebra.F.id_s (x7::nil))/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x7 x8))
(t = (algebra.Alg.Term algebra.F.id_nil nil) ->
t' = (algebra.Alg.Term algebra.F.id_nil nil))
(t = (algebra.Alg.Term algebra.F.id_0 nil) ->
t' = (algebra.Alg.Term algebra.F.id_0 nil))
(forall x8 x10,
t = (algebra.Alg.Term algebra.F.id_pair (x8::x10::nil)) ->
exists x7,
exists x9,
t' = (algebra.Alg.Term algebra.F.id_pair (x7::x9::nil))/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x7 x8)/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x9 x10))
(t = (algebra.Alg.Term algebra.F.id_true nil) ->
t' = (algebra.Alg.Term algebra.F.id_true nil))
(forall x8 x10,
t = (algebra.Alg.Term algebra.F.id_add (x8::x10::nil)) ->
exists x7,
exists x9,
t' = (algebra.Alg.Term algebra.F.id_add (x7::x9::nil))/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x7 x8)/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x9 x10)).
Proof.
intros t t' H.
induction H as [|y IH z z_to_y] using
closure_extension.refl_trans_clos_ind2.
constructor 1.
intros H;intuition;constructor 1.
intros x8 H;exists x8;intuition;constructor 1.
intros H;intuition;constructor 1.
intros H;intuition;constructor 1.
intros x8 x10 H;exists x8;exists x10;intuition;constructor 1.
intros H;intuition;constructor 1.
intros x8 x10 H;exists x8;exists x10;intuition;constructor 1.
inversion z_to_y as [t1 t2 H H0 H1|f l1 l2 H0 H H2];clear z_to_y;subst.
inversion H as [t1 t2 sigma H2 H1 H0];clear H IH;subst;inversion H2;
clear ;constructor;try (intros until 0 );clear ;intros abs;
discriminate abs.
destruct IH as
[H_id_false H_id_s H_id_nil H_id_0 H_id_pair H_id_true H_id_add].
constructor.
clear H_id_s H_id_nil H_id_0 H_id_pair H_id_true H_id_add;intros H;
injection H;clear H;intros ;subst;
repeat (
match goal with
| H:closure.one_step_list (algebra.EQT.one_step _) _ _ |- _ =>
inversion H;clear H;subst
end
).
clear H_id_false H_id_nil H_id_0 H_id_pair H_id_true H_id_add;intros x8 H;
injection H;clear H;intros ;subst;
repeat (
match goal with
| H:closure.one_step_list (algebra.EQT.one_step _) _ _ |- _ =>
inversion H;clear H;subst
end
).
match goal with
| H:algebra.EQT.one_step _ ?y x8 |- _ =>
destruct (H_id_s y (refl_equal _)) as [x7];intros ;intuition;exists x7;
intuition;eapply closure_extension.refl_trans_clos_R;eassumption
end
.
clear H_id_false H_id_s H_id_0 H_id_pair H_id_true H_id_add;intros H;
injection H;clear H;intros ;subst;
repeat (
match goal with
| H:closure.one_step_list (algebra.EQT.one_step _) _ _ |- _ =>
inversion H;clear H;subst
end
).
clear H_id_false H_id_s H_id_nil H_id_pair H_id_true H_id_add;intros H;
injection H;clear H;intros ;subst;
repeat (
match goal with
| H:closure.one_step_list (algebra.EQT.one_step _) _ _ |- _ =>
inversion H;clear H;subst
end
).
clear H_id_false H_id_s H_id_nil H_id_0 H_id_true H_id_add;
intros x8 x10 H;injection H;clear H;intros ;subst;
repeat (
match goal with
| H:closure.one_step_list (algebra.EQT.one_step _) _ _ |- _ =>
inversion H;clear H;subst
end
).
match goal with
| H:algebra.EQT.one_step _ ?y x8 |- _ =>
destruct (H_id_pair y x10 (refl_equal _)) as [x7 [x9]];intros ;
intuition;exists x7;exists x9;intuition;
eapply closure_extension.refl_trans_clos_R;eassumption
end
.
match goal with
| H:algebra.EQT.one_step _ ?y x10 |- _ =>
destruct (H_id_pair x8 y (refl_equal _)) as [x7 [x9]];intros ;
intuition;exists x7;exists x9;intuition;
eapply closure_extension.refl_trans_clos_R;eassumption
end
.
clear H_id_false H_id_s H_id_nil H_id_0 H_id_pair H_id_add;intros H;
injection H;clear H;intros ;subst;
repeat (
match goal with
| H:closure.one_step_list (algebra.EQT.one_step _) _ _ |- _ =>
inversion H;clear H;subst
end
).
clear H_id_false H_id_s H_id_nil H_id_0 H_id_pair H_id_true;
intros x8 x10 H;injection H;clear H;intros ;subst;
repeat (
match goal with
| H:closure.one_step_list (algebra.EQT.one_step _) _ _ |- _ =>
inversion H;clear H;subst
end
).
match goal with
| H:algebra.EQT.one_step _ ?y x8 |- _ =>
destruct (H_id_add y x10 (refl_equal _)) as [x7 [x9]];intros ;
intuition;exists x7;exists x9;intuition;
eapply closure_extension.refl_trans_clos_R;eassumption
end
.
match goal with
| H:algebra.EQT.one_step _ ?y x10 |- _ =>
destruct (H_id_add x8 y (refl_equal _)) as [x7 [x9]];intros ;intuition;
exists x7;exists x9;intuition;
eapply closure_extension.refl_trans_clos_R;eassumption
end
.
Qed.
Lemma id_false_is_R_xml_0_constructor :
forall t t',
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
t = (algebra.Alg.Term algebra.F.id_false nil) ->
t' = (algebra.Alg.Term algebra.F.id_false nil).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Lemma id_s_is_R_xml_0_constructor :
forall t t',
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
forall x8,
t = (algebra.Alg.Term algebra.F.id_s (x8::nil)) ->
exists x7,
t' = (algebra.Alg.Term algebra.F.id_s (x7::nil))/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x7 x8).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Lemma id_nil_is_R_xml_0_constructor :
forall t t',
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
t = (algebra.Alg.Term algebra.F.id_nil nil) ->
t' = (algebra.Alg.Term algebra.F.id_nil nil).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Lemma id_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_pair_is_R_xml_0_constructor :
forall t t',
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
forall x8 x10,
t = (algebra.Alg.Term algebra.F.id_pair (x8::x10::nil)) ->
exists x7,
exists x9,
t' = (algebra.Alg.Term algebra.F.id_pair (x7::x9::nil))/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x7 x8)/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x9 x10).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Lemma id_true_is_R_xml_0_constructor :
forall t t',
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
t = (algebra.Alg.Term algebra.F.id_true nil) ->
t' = (algebra.Alg.Term algebra.F.id_true nil).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Lemma id_add_is_R_xml_0_constructor :
forall t t',
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
forall x8 x10,
t = (algebra.Alg.Term algebra.F.id_add (x8::x10::nil)) ->
exists x7,
exists x9,
t' = (algebra.Alg.Term algebra.F.id_add (x7::x9::nil))/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x7 x8)/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x9 x10).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Ltac impossible_star_reduction_R_xml_0 :=
match goal with
| H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
_ (algebra.Alg.Term algebra.F.id_false nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_false_is_R_xml_0_constructor H (refl_equal _)) in *;
(discriminate Heq)||
(clearbody Heq;try (subst);try (clear Heq);clear H;
impossible_star_reduction_R_xml_0 ))
| H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
_ (algebra.Alg.Term algebra.F.id_s (?x7::nil)) |- _ =>
let x7 := fresh "x" in
(let Heq := fresh "Heq" in
(let Hred1 := fresh "Hred" in
(destruct (id_s_is_R_xml_0_constructor H (refl_equal _)) as
[x7 [Heq Hred1]];
(discriminate Heq)||
(injection Heq;intros ;subst;clear Heq;clear H;
impossible_star_reduction_R_xml_0 ))))
| H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
_ (algebra.Alg.Term algebra.F.id_nil nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_nil_is_R_xml_0_constructor H (refl_equal _)) in *;
(discriminate Heq)||
(clearbody Heq;try (subst);try (clear Heq);clear H;
impossible_star_reduction_R_xml_0 ))
| H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
_ (algebra.Alg.Term algebra.F.id_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_pair (?x8::?x7::nil)) |- _ =>
let x8 := fresh "x" in
(let x7 := fresh "x" in
(let Heq := fresh "Heq" in
(let Hred1 := fresh "Hred" in
(let Hred2 := fresh "Hred" in
(destruct (id_pair_is_R_xml_0_constructor H (refl_equal _)) as
[x8 [x7 [Heq [Hred2 Hred1]]]];
(discriminate Heq)||
(injection Heq;intros ;subst;clear Heq;clear H;
impossible_star_reduction_R_xml_0 ))))))
| H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
_ (algebra.Alg.Term algebra.F.id_true nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_true_is_R_xml_0_constructor H (refl_equal _)) in *;
(discriminate Heq)||
(clearbody Heq;try (subst);try (clear Heq);clear H;
impossible_star_reduction_R_xml_0 ))
| H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
_ (algebra.Alg.Term algebra.F.id_add (?x8::?x7::nil)) |- _ =>
let x8 := fresh "x" in
(let x7 := fresh "x" in
(let Heq := fresh "Heq" in
(let Hred1 := fresh "Hred" in
(let Hred2 := fresh "Hred" in
(destruct (id_add_is_R_xml_0_constructor H (refl_equal _)) as
[x8 [x7 [Heq [Hred2 Hred1]]]];
(discriminate Heq)||
(injection Heq;intros ;subst;clear Heq;clear H;
impossible_star_reduction_R_xml_0 ))))))
end
.
Ltac simplify_star_reduction_R_xml_0 :=
match goal with
| H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
_ (algebra.Alg.Term algebra.F.id_false nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_false_is_R_xml_0_constructor H (refl_equal _)) in *;
(discriminate Heq)||
(clearbody Heq;try (subst);try (clear Heq);clear H;
try (simplify_star_reduction_R_xml_0 )))
| H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
_ (algebra.Alg.Term algebra.F.id_s (?x7::nil)) |- _ =>
let x7 := fresh "x" in
(let Heq := fresh "Heq" in
(let Hred1 := fresh "Hred" in
(destruct (id_s_is_R_xml_0_constructor H (refl_equal _)) as
[x7 [Heq Hred1]];
(discriminate Heq)||
(injection Heq;intros ;subst;clear Heq;clear H;
try (simplify_star_reduction_R_xml_0 )))))
| H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
_ (algebra.Alg.Term algebra.F.id_nil nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_nil_is_R_xml_0_constructor H (refl_equal _)) in *;
(discriminate Heq)||
(clearbody Heq;try (subst);try (clear Heq);clear H;
try (simplify_star_reduction_R_xml_0 )))
| H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
_ (algebra.Alg.Term algebra.F.id_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_pair (?x8::?x7::nil)) |- _ =>
let x8 := fresh "x" in
(let x7 := fresh "x" in
(let Heq := fresh "Heq" in
(let Hred1 := fresh "Hred" in
(let Hred2 := fresh "Hred" in
(destruct (id_pair_is_R_xml_0_constructor H (refl_equal _)) as
[x8 [x7 [Heq [Hred2 Hred1]]]];
(discriminate Heq)||
(injection Heq;intros ;subst;clear Heq;clear H;
try (simplify_star_reduction_R_xml_0 )))))))
| H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
_ (algebra.Alg.Term algebra.F.id_true nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_true_is_R_xml_0_constructor H (refl_equal _)) in *;
(discriminate Heq)||
(clearbody Heq;try (subst);try (clear Heq);clear H;
try (simplify_star_reduction_R_xml_0 )))
| H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
_ (algebra.Alg.Term algebra.F.id_add (?x8::?x7::nil)) |- _ =>
let x8 := fresh "x" in
(let x7 := fresh "x" in
(let Heq := fresh "Heq" in
(let Hred1 := fresh "Hred" in
(let Hred2 := fresh "Hred" in
(destruct (id_add_is_R_xml_0_constructor H (refl_equal _)) as
[x8 [x7 [Heq [Hred2 Hred1]]]];
(discriminate Heq)||
(injection Heq;intros ;subst;clear Heq;clear H;
try (simplify_star_reduction_R_xml_0 )))))))
end
.
End R_xml_0_deep_rew.
Module InterpGen := interp.Interp(algebra.EQT).
Module ddp := dp.MakeDP(algebra.EQT).
Module SymbType. Definition A := algebra.Alg.F.Symb.A. End SymbType.
Module Symb_more_list := more_list_extention.Make(SymbType)(algebra.Alg.F.Symb).
Module SymbSet := list_set.Make(algebra.F.Symb).
Module Interp.
Section S.
Require Import interp.
Hypothesis A : Type.
Hypothesis Ale Alt Aeq : A -> A -> Prop.
Hypothesis Aop : interp.ordering_pair Aeq Alt Ale.
Hypothesis A0 : A.
Notation Local "a <= b" := (Ale a b).
Hypothesis P_id_lt : A ->A ->A.
Hypothesis P_id_split : A ->A ->A.
Hypothesis P_id_false : A.
Hypothesis P_id_qsort : A ->A.
Hypothesis P_id_s : A ->A.
Hypothesis P_id_f_1 : A ->A ->A ->A ->A.
Hypothesis P_id_nil : A.
Hypothesis P_id_0 : A.
Hypothesis P_id_pair : A ->A ->A.
Hypothesis P_id_append : A ->A ->A.
Hypothesis P_id_f_3 : A ->A ->A ->A.
Hypothesis P_id_true : A.
Hypothesis P_id_f_2 : A ->A ->A ->A ->A ->A ->A.
Hypothesis P_id_add : A ->A ->A.
Hypothesis P_id_lt_monotonic :
forall x8 x10 x9 x7,
(A0 <= x10)/\ (x10 <= x9) ->
(A0 <= x8)/\ (x8 <= x7) ->P_id_lt x8 x10 <= P_id_lt x7 x9.
Hypothesis P_id_split_monotonic :
forall x8 x10 x9 x7,
(A0 <= x10)/\ (x10 <= x9) ->
(A0 <= x8)/\ (x8 <= x7) ->P_id_split x8 x10 <= P_id_split x7 x9.
Hypothesis P_id_qsort_monotonic :
forall x8 x7, (A0 <= x8)/\ (x8 <= x7) ->P_id_qsort x8 <= P_id_qsort x7.
Hypothesis P_id_s_monotonic :
forall x8 x7, (A0 <= x8)/\ (x8 <= x7) ->P_id_s x8 <= P_id_s x7.
Hypothesis P_id_f_1_monotonic :
forall x8 x12 x10 x14 x9 x13 x11 x7,
(A0 <= x14)/\ (x14 <= x13) ->
(A0 <= x12)/\ (x12 <= x11) ->
(A0 <= x10)/\ (x10 <= x9) ->
(A0 <= x8)/\ (x8 <= x7) ->
P_id_f_1 x8 x10 x12 x14 <= P_id_f_1 x7 x9 x11 x13.
Hypothesis P_id_pair_monotonic :
forall x8 x10 x9 x7,
(A0 <= x10)/\ (x10 <= x9) ->
(A0 <= x8)/\ (x8 <= x7) ->P_id_pair x8 x10 <= P_id_pair x7 x9.
Hypothesis P_id_append_monotonic :
forall x8 x10 x9 x7,
(A0 <= x10)/\ (x10 <= x9) ->
(A0 <= x8)/\ (x8 <= x7) ->P_id_append x8 x10 <= P_id_append x7 x9.
Hypothesis P_id_f_3_monotonic :
forall x8 x12 x10 x9 x11 x7,
(A0 <= x12)/\ (x12 <= x11) ->
(A0 <= x10)/\ (x10 <= x9) ->
(A0 <= x8)/\ (x8 <= x7) ->P_id_f_3 x8 x10 x12 <= P_id_f_3 x7 x9 x11.
Hypothesis P_id_f_2_monotonic :
forall x16 x8 x12 x18 x10 x14 x17 x9 x13 x11 x7 x15,
(A0 <= x18)/\ (x18 <= x17) ->
(A0 <= x16)/\ (x16 <= x15) ->
(A0 <= x14)/\ (x14 <= x13) ->
(A0 <= x12)/\ (x12 <= x11) ->
(A0 <= x10)/\ (x10 <= x9) ->
(A0 <= x8)/\ (x8 <= x7) ->
P_id_f_2 x8 x10 x12 x14 x16 x18 <= P_id_f_2 x7 x9 x11 x13 x15 x17.
Hypothesis P_id_add_monotonic :
forall x8 x10 x9 x7,
(A0 <= x10)/\ (x10 <= x9) ->
(A0 <= x8)/\ (x8 <= x7) ->P_id_add x8 x10 <= P_id_add x7 x9.
Hypothesis P_id_lt_bounded :
forall x8 x7, (A0 <= x7) ->(A0 <= x8) ->A0 <= P_id_lt x8 x7.
Hypothesis P_id_split_bounded :
forall x8 x7, (A0 <= x7) ->(A0 <= x8) ->A0 <= P_id_split x8 x7.
Hypothesis P_id_false_bounded : A0 <= P_id_false .
Hypothesis P_id_qsort_bounded :
forall x7, (A0 <= x7) ->A0 <= P_id_qsort x7.
Hypothesis P_id_s_bounded : forall x7, (A0 <= x7) ->A0 <= P_id_s x7.
Hypothesis P_id_f_1_bounded :
forall x8 x10 x9 x7,
(A0 <= x7) ->
(A0 <= x8) ->(A0 <= x9) ->(A0 <= x10) ->A0 <= P_id_f_1 x10 x9 x8 x7.
Hypothesis P_id_nil_bounded : A0 <= P_id_nil .
Hypothesis P_id_0_bounded : A0 <= P_id_0 .
Hypothesis P_id_pair_bounded :
forall x8 x7, (A0 <= x7) ->(A0 <= x8) ->A0 <= P_id_pair x8 x7.
Hypothesis P_id_append_bounded :
forall x8 x7, (A0 <= x7) ->(A0 <= x8) ->A0 <= P_id_append x8 x7.
Hypothesis P_id_f_3_bounded :
forall x8 x9 x7,
(A0 <= x7) ->(A0 <= x8) ->(A0 <= x9) ->A0 <= P_id_f_3 x9 x8 x7.
Hypothesis P_id_true_bounded : A0 <= P_id_true .
Hypothesis P_id_f_2_bounded :
forall x8 x12 x10 x9 x11 x7,
(A0 <= x7) ->
(A0 <= x8) ->
(A0 <= x9) ->
(A0 <= x10) ->
(A0 <= x11) ->(A0 <= x12) ->A0 <= P_id_f_2 x12 x11 x10 x9 x8 x7.
Hypothesis P_id_add_bounded :
forall x8 x7, (A0 <= x7) ->(A0 <= x8) ->A0 <= P_id_add x8 x7.
Fixpoint measure t { struct t } :=
match t with
| (algebra.Alg.Term algebra.F.id_lt (x8::x7::nil)) =>
P_id_lt (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_split (x8::x7::nil)) =>
P_id_split (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_false nil) => P_id_false
| (algebra.Alg.Term algebra.F.id_qsort (x7::nil)) =>
P_id_qsort (measure x7)
| (algebra.Alg.Term algebra.F.id_s (x7::nil)) => P_id_s (measure x7)
| (algebra.Alg.Term algebra.F.id_f_1 (x10::x9::x8::x7::nil)) =>
P_id_f_1 (measure x10) (measure x9) (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_nil nil) => P_id_nil
| (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0
| (algebra.Alg.Term algebra.F.id_pair (x8::x7::nil)) =>
P_id_pair (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_append (x8::x7::nil)) =>
P_id_append (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_3 (x9::x8::x7::nil)) =>
P_id_f_3 (measure x9) (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_true nil) => P_id_true
| (algebra.Alg.Term algebra.F.id_f_2 (x12::x11::x10::x9::x8::x7::nil)) =>
P_id_f_2 (measure x12) (measure x11) (measure x10) (measure x9)
(measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_add (x8::x7::nil)) =>
P_id_add (measure x8) (measure x7)
| _ => A0
end.
Lemma measure_equation :
forall t,
measure t = match t with
| (algebra.Alg.Term algebra.F.id_lt (x8::x7::nil)) =>
P_id_lt (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_split (x8::x7::nil)) =>
P_id_split (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_false nil) => P_id_false
| (algebra.Alg.Term algebra.F.id_qsort (x7::nil)) =>
P_id_qsort (measure x7)
| (algebra.Alg.Term algebra.F.id_s (x7::nil)) =>
P_id_s (measure x7)
| (algebra.Alg.Term algebra.F.id_f_1 (x10::x9::x8::
x7::nil)) =>
P_id_f_1 (measure x10) (measure x9) (measure x8)
(measure x7)
| (algebra.Alg.Term algebra.F.id_nil nil) => P_id_nil
| (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0
| (algebra.Alg.Term algebra.F.id_pair (x8::x7::nil)) =>
P_id_pair (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_append (x8::x7::nil)) =>
P_id_append (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_3 (x9::x8::x7::nil)) =>
P_id_f_3 (measure x9) (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_true nil) => P_id_true
| (algebra.Alg.Term algebra.F.id_f_2 (x12::x11::x10::x9::
x8::x7::nil)) =>
P_id_f_2 (measure x12) (measure x11) (measure x10)
(measure x9) (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_add (x8::x7::nil)) =>
P_id_add (measure x8) (measure x7)
| _ => 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_lt => P_id_lt
| algebra.F.id_split => P_id_split
| algebra.F.id_false => P_id_false
| algebra.F.id_qsort => P_id_qsort
| algebra.F.id_s => P_id_s
| algebra.F.id_f_1 => P_id_f_1
| algebra.F.id_nil => P_id_nil
| algebra.F.id_0 => P_id_0
| algebra.F.id_pair => P_id_pair
| algebra.F.id_append => P_id_append
| algebra.F.id_f_3 => P_id_f_3
| algebra.F.id_true => P_id_true
| algebra.F.id_f_2 => P_id_f_2
| algebra.F.id_add => P_id_add
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_lt =>
match l with
| nil => _
| _::nil => _
| _::_::nil => _
| _::_::_::_ => _
end
| algebra.F.id_split =>
match l with
| nil => _
| _::nil => _
| _::_::nil => _
| _::_::_::_ => _
end
| algebra.F.id_false => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_qsort =>
match l with
| nil => _
| _::nil => _
| _::_::_ => _
end
| algebra.F.id_s =>
match l with
| nil => _
| _::nil => _
| _::_::_ => _
end
| algebra.F.id_f_1 =>
match l with
| nil => _
| _::nil => _
| _::_::nil => _
| _::_::_::nil => _
| _::_::_::_::nil => _
| _::_::_::_::_::_ => _
end
| algebra.F.id_nil => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_0 => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_pair =>
match l with
| nil => _
| _::nil => _
| _::_::nil => _
| _::_::_::_ => _
end
| algebra.F.id_append =>
match l with
| nil => _
| _::nil => _
| _::_::nil => _
| _::_::_::_ => _
end
| algebra.F.id_f_3 =>
match l with
| nil => _
| _::nil => _
| _::_::nil => _
| _::_::_::nil => _
| _::_::_::_::_ => _
end
| algebra.F.id_true => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_f_2 =>
match l with
| nil => _
| _::nil => _
| _::_::nil => _
| _::_::_::nil => _
| _::_::_::_::nil => _
| _::_::_::_::_::nil => _
| _::_::_::_::_::_::nil => _
| _::_::_::_::_::_::_::_ => _
end
| algebra.F.id_add =>
match l with
| nil => _
| _::nil => _
| _::_::nil => _
| _::_::_::_ => _
end
end;simpl in |-*;unfold eq_rect_r, eq_rect, sym_eq in |-*;
try (reflexivity );f_equal ;auto.
Qed.
Lemma measure_bounded : forall t, A0 <= measure t.
Proof.
intros t.
rewrite same_measure in |-*.
apply (InterpGen.measure_bounded Aop).
intros f.
case f.
vm_compute in |-*;intros ;apply P_id_lt_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_split_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_false_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_qsort_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_s_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_f_1_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_nil_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_0_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_pair_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_append_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_f_3_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_true_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_f_2_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_add_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_lt_monotonic;assumption.
vm_compute in |-*;intros ;apply P_id_split_monotonic;assumption.
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;intros ;apply P_id_qsort_monotonic;assumption.
vm_compute in |-*;intros ;apply P_id_s_monotonic;assumption.
vm_compute in |-*;intros ;apply P_id_f_1_monotonic;assumption.
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;intros ;apply P_id_pair_monotonic;assumption.
vm_compute in |-*;intros ;apply P_id_append_monotonic;assumption.
vm_compute in |-*;intros ;apply P_id_f_3_monotonic;assumption.
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;intros ;apply P_id_f_2_monotonic;assumption.
vm_compute in |-*;intros ;apply P_id_add_monotonic;assumption.
intros f.
case f.
vm_compute in |-*;intros ;apply P_id_lt_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_split_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_false_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_qsort_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_s_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_f_1_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_nil_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_0_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_pair_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_append_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_f_3_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_true_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_f_2_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_add_bounded;assumption.
intros .
do 2 (rewrite <- same_measure in |-*).
apply rules_monotonic;assumption.
assumption.
Qed.
Hypothesis P_id_SPLIT : A ->A ->A.
Hypothesis P_id_F_3 : A ->A ->A ->A.
Hypothesis P_id_F_2 : A ->A ->A ->A ->A ->A ->A.
Hypothesis P_id_LT : A ->A ->A.
Hypothesis P_id_F_1 : A ->A ->A ->A ->A.
Hypothesis P_id_QSORT : A ->A.
Hypothesis P_id_APPEND : A ->A ->A.
Hypothesis P_id_SPLIT_monotonic :
forall x8 x10 x9 x7,
(A0 <= x10)/\ (x10 <= x9) ->
(A0 <= x8)/\ (x8 <= x7) ->P_id_SPLIT x8 x10 <= P_id_SPLIT x7 x9.
Hypothesis P_id_F_3_monotonic :
forall x8 x12 x10 x9 x11 x7,
(A0 <= x12)/\ (x12 <= x11) ->
(A0 <= x10)/\ (x10 <= x9) ->
(A0 <= x8)/\ (x8 <= x7) ->P_id_F_3 x8 x10 x12 <= P_id_F_3 x7 x9 x11.
Hypothesis P_id_F_2_monotonic :
forall x16 x8 x12 x18 x10 x14 x17 x9 x13 x11 x7 x15,
(A0 <= x18)/\ (x18 <= x17) ->
(A0 <= x16)/\ (x16 <= x15) ->
(A0 <= x14)/\ (x14 <= x13) ->
(A0 <= x12)/\ (x12 <= x11) ->
(A0 <= x10)/\ (x10 <= x9) ->
(A0 <= x8)/\ (x8 <= x7) ->
P_id_F_2 x8 x10 x12 x14 x16 x18 <= P_id_F_2 x7 x9 x11 x13 x15 x17.
Hypothesis P_id_LT_monotonic :
forall x8 x10 x9 x7,
(A0 <= x10)/\ (x10 <= x9) ->
(A0 <= x8)/\ (x8 <= x7) ->P_id_LT x8 x10 <= P_id_LT x7 x9.
Hypothesis P_id_F_1_monotonic :
forall x8 x12 x10 x14 x9 x13 x11 x7,
(A0 <= x14)/\ (x14 <= x13) ->
(A0 <= x12)/\ (x12 <= x11) ->
(A0 <= x10)/\ (x10 <= x9) ->
(A0 <= x8)/\ (x8 <= x7) ->
P_id_F_1 x8 x10 x12 x14 <= P_id_F_1 x7 x9 x11 x13.
Hypothesis P_id_QSORT_monotonic :
forall x8 x7, (A0 <= x8)/\ (x8 <= x7) ->P_id_QSORT x8 <= P_id_QSORT x7.
Hypothesis P_id_APPEND_monotonic :
forall x8 x10 x9 x7,
(A0 <= x10)/\ (x10 <= x9) ->
(A0 <= x8)/\ (x8 <= x7) ->P_id_APPEND x8 x10 <= P_id_APPEND x7 x9.
Definition marked_measure t :=
match t with
| (algebra.Alg.Term algebra.F.id_split (x8::x7::nil)) =>
P_id_SPLIT (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_3 (x9::x8::x7::nil)) =>
P_id_F_3 (measure x9) (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_2 (x12::x11::x10::x9::x8::x7::nil)) =>
P_id_F_2 (measure x12) (measure x11) (measure x10) (measure x9)
(measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_lt (x8::x7::nil)) =>
P_id_LT (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_1 (x10::x9::x8::x7::nil)) =>
P_id_F_1 (measure x10) (measure x9) (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_qsort (x7::nil)) =>
P_id_QSORT (measure x7)
| (algebra.Alg.Term algebra.F.id_append (x8::x7::nil)) =>
P_id_APPEND (measure x8) (measure x7)
| _ => 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 x12 x11 x10 x9 x8 x7;
apply (P_id_F_2 x12 x11 x10 x9 x8 x7).
match type of H with
| orb ?a ?b = true =>
assert (H':{a = true}+{b = true});[
revert H;case a;[left;reflexivity|simpl;intros h;right;exact h]|
clear H;destruct H' as [H|H]]
end .
match type of H with
| _ _ ?t = true =>
generalize (algebra.F.symb_eq_bool_ok f t);
unfold algebra.Alg.eq_symb_bool in H;
rewrite H;clear H;intros ;subst
end .
vm_compute in |-*;intros x9 x8 x7;apply (P_id_F_3 x9 x8 x7).
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 x8 x7;apply (P_id_APPEND x8 x7).
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 x10 x9 x8 x7;apply (P_id_F_1 x10 x9 x8 x7).
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 x7;apply (P_id_QSORT x7).
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 x8 x7;apply (P_id_SPLIT x8 x7).
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 x8 x7;apply (P_id_LT x8 x7).
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_lt =>
match l with
| nil => _
| _::nil => _
| _::_::nil => _
| _::_::_::_ => _
end
| algebra.F.id_split =>
match l with
| nil => _
| _::nil => _
| _::_::nil => _
| _::_::_::_ => _
end
| algebra.F.id_false => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_qsort =>
match l with
| nil => _
| _::nil => _
| _::_::_ => _
end
| algebra.F.id_s =>
match l with
| nil => _
| _::nil => _
| _::_::_ => _
end
| algebra.F.id_f_1 =>
match l with
| nil => _
| _::nil => _
| _::_::nil => _
| _::_::_::nil => _
| _::_::_::_::nil => _
| _::_::_::_::_::_ => _
end
| algebra.F.id_nil => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_0 => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_pair =>
match l with
| nil => _
| _::nil => _
| _::_::nil => _
| _::_::_::_ => _
end
| algebra.F.id_append =>
match l with
| nil => _
| _::nil => _
| _::_::nil => _
| _::_::_::_ => _
end
| algebra.F.id_f_3 =>
match l with
| nil => _
| _::nil => _
| _::_::nil => _
| _::_::_::nil => _
| _::_::_::_::_ => _
end
| algebra.F.id_true => match l with
| nil => _
| _::_ => _
end
| algebra.F.id_f_2 =>
match l with
| nil => _
| _::nil => _
| _::_::nil => _
| _::_::_::nil => _
| _::_::_::_::nil => _
| _::_::_::_::_::nil => _
| _::_::_::_::_::_::nil => _
| _::_::_::_::_::_::_::_ => _
end
| algebra.F.id_add =>
match l with
| nil => _
| _::nil => _
| _::_::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 .
lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
apply same_measure.
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
apply same_measure.
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
apply same_measure.
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
apply same_measure.
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
apply same_measure.
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
apply same_measure.
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
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 .
lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
apply same_measure.
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
vm_compute in |-*;reflexivity .
lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
apply same_measure.
vm_compute in |-*;reflexivity .
Qed.
Lemma marked_measure_equation :
forall t,
marked_measure t = match t with
| (algebra.Alg.Term algebra.F.id_split (x8::
x7::nil)) =>
P_id_SPLIT (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_3 (x9::x8::
x7::nil)) =>
P_id_F_3 (measure x9) (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_2 (x12::x11::
x10::x9::x8::x7::nil)) =>
P_id_F_2 (measure x12) (measure x11)
(measure x10) (measure x9) (measure x8)
(measure x7)
| (algebra.Alg.Term algebra.F.id_lt (x8::x7::nil)) =>
P_id_LT (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_1 (x10::x9::x8::
x7::nil)) =>
P_id_F_1 (measure x10) (measure x9) (measure x8)
(measure x7)
| (algebra.Alg.Term algebra.F.id_qsort (x7::nil)) =>
P_id_QSORT (measure x7)
| (algebra.Alg.Term algebra.F.id_append (x8::
x7::nil)) =>
P_id_APPEND (measure x8) (measure x7)
| _ => 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_lt_monotonic;assumption.
vm_compute in |-*;intros ;apply P_id_split_monotonic;assumption.
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;intros ;apply P_id_qsort_monotonic;assumption.
vm_compute in |-*;intros ;apply P_id_s_monotonic;assumption.
vm_compute in |-*;intros ;apply P_id_f_1_monotonic;assumption.
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;intros ;apply P_id_pair_monotonic;assumption.
vm_compute in |-*;intros ;apply P_id_append_monotonic;assumption.
vm_compute in |-*;intros ;apply P_id_f_3_monotonic;assumption.
vm_compute in |-*;apply (Aop.(le_refl)).
vm_compute in |-*;intros ;apply P_id_f_2_monotonic;assumption.
vm_compute in |-*;intros ;apply P_id_add_monotonic;assumption.
clear f.
intros f.
case f.
vm_compute in |-*;intros ;apply P_id_lt_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_split_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_false_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_qsort_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_s_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_f_1_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_nil_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_0_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_pair_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_append_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_f_3_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_true_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_f_2_bounded;assumption.
vm_compute in |-*;intros ;apply P_id_add_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_F_2_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_F_3_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_APPEND_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_F_1_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_QSORT_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_SPLIT_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_LT_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_lt : Z ->Z ->Z.
Hypothesis P_id_split : Z ->Z ->Z.
Hypothesis P_id_false : Z.
Hypothesis P_id_qsort : Z ->Z.
Hypothesis P_id_s : Z ->Z.
Hypothesis P_id_f_1 : Z ->Z ->Z ->Z ->Z.
Hypothesis P_id_nil : Z.
Hypothesis P_id_0 : Z.
Hypothesis P_id_pair : Z ->Z ->Z.
Hypothesis P_id_append : Z ->Z ->Z.
Hypothesis P_id_f_3 : Z ->Z ->Z ->Z.
Hypothesis P_id_true : Z.
Hypothesis P_id_f_2 : Z ->Z ->Z ->Z ->Z ->Z ->Z.
Hypothesis P_id_add : Z ->Z ->Z.
Hypothesis P_id_lt_monotonic :
forall x8 x10 x9 x7,
(min_value <= x10)/\ (x10 <= x9) ->
(min_value <= x8)/\ (x8 <= x7) ->P_id_lt x8 x10 <= P_id_lt x7 x9.
Hypothesis P_id_split_monotonic :
forall x8 x10 x9 x7,
(min_value <= x10)/\ (x10 <= x9) ->
(min_value <= x8)/\ (x8 <= x7) ->P_id_split x8 x10 <= P_id_split x7 x9.
Hypothesis P_id_qsort_monotonic :
forall x8 x7,
(min_value <= x8)/\ (x8 <= x7) ->P_id_qsort x8 <= P_id_qsort x7.
Hypothesis P_id_s_monotonic :
forall x8 x7, (min_value <= x8)/\ (x8 <= x7) ->P_id_s x8 <= P_id_s x7.
Hypothesis P_id_f_1_monotonic :
forall x8 x12 x10 x14 x9 x13 x11 x7,
(min_value <= x14)/\ (x14 <= x13) ->
(min_value <= x12)/\ (x12 <= x11) ->
(min_value <= x10)/\ (x10 <= x9) ->
(min_value <= x8)/\ (x8 <= x7) ->
P_id_f_1 x8 x10 x12 x14 <= P_id_f_1 x7 x9 x11 x13.
Hypothesis P_id_pair_monotonic :
forall x8 x10 x9 x7,
(min_value <= x10)/\ (x10 <= x9) ->
(min_value <= x8)/\ (x8 <= x7) ->P_id_pair x8 x10 <= P_id_pair x7 x9.
Hypothesis P_id_append_monotonic :
forall x8 x10 x9 x7,
(min_value <= x10)/\ (x10 <= x9) ->
(min_value <= x8)/\ (x8 <= x7) ->
P_id_append x8 x10 <= P_id_append x7 x9.
Hypothesis P_id_f_3_monotonic :
forall x8 x12 x10 x9 x11 x7,
(min_value <= x12)/\ (x12 <= x11) ->
(min_value <= x10)/\ (x10 <= x9) ->
(min_value <= x8)/\ (x8 <= x7) ->
P_id_f_3 x8 x10 x12 <= P_id_f_3 x7 x9 x11.
Hypothesis P_id_f_2_monotonic :
forall x16 x8 x12 x18 x10 x14 x17 x9 x13 x11 x7 x15,
(min_value <= x18)/\ (x18 <= x17) ->
(min_value <= x16)/\ (x16 <= x15) ->
(min_value <= x14)/\ (x14 <= x13) ->
(min_value <= x12)/\ (x12 <= x11) ->
(min_value <= x10)/\ (x10 <= x9) ->
(min_value <= x8)/\ (x8 <= x7) ->
P_id_f_2 x8 x10 x12 x14 x16 x18 <= P_id_f_2 x7 x9 x11 x13 x15 x17.
Hypothesis P_id_add_monotonic :
forall x8 x10 x9 x7,
(min_value <= x10)/\ (x10 <= x9) ->
(min_value <= x8)/\ (x8 <= x7) ->P_id_add x8 x10 <= P_id_add x7 x9.
Hypothesis P_id_lt_bounded :
forall x8 x7,
(min_value <= x7) ->(min_value <= x8) ->min_value <= P_id_lt x8 x7.
Hypothesis P_id_split_bounded :
forall x8 x7,
(min_value <= x7) ->(min_value <= x8) ->min_value <= P_id_split x8 x7.
Hypothesis P_id_false_bounded : min_value <= P_id_false .
Hypothesis P_id_qsort_bounded :
forall x7, (min_value <= x7) ->min_value <= P_id_qsort x7.
Hypothesis P_id_s_bounded :
forall x7, (min_value <= x7) ->min_value <= P_id_s x7.
Hypothesis P_id_f_1_bounded :
forall x8 x10 x9 x7,
(min_value <= x7) ->
(min_value <= x8) ->
(min_value <= x9) ->
(min_value <= x10) ->min_value <= P_id_f_1 x10 x9 x8 x7.
Hypothesis P_id_nil_bounded : min_value <= P_id_nil .
Hypothesis P_id_0_bounded : min_value <= P_id_0 .
Hypothesis P_id_pair_bounded :
forall x8 x7,
(min_value <= x7) ->(min_value <= x8) ->min_value <= P_id_pair x8 x7.
Hypothesis P_id_append_bounded :
forall x8 x7,
(min_value <= x7) ->(min_value <= x8) ->min_value <= P_id_append x8 x7.
Hypothesis P_id_f_3_bounded :
forall x8 x9 x7,
(min_value <= x7) ->
(min_value <= x8) ->(min_value <= x9) ->min_value <= P_id_f_3 x9 x8 x7.
Hypothesis P_id_true_bounded : min_value <= P_id_true .
Hypothesis P_id_f_2_bounded :
forall x8 x12 x10 x9 x11 x7,
(min_value <= x7) ->
(min_value <= x8) ->
(min_value <= x9) ->
(min_value <= x10) ->
(min_value <= x11) ->
(min_value <= x12) ->min_value <= P_id_f_2 x12 x11 x10 x9 x8 x7.
Hypothesis P_id_add_bounded :
forall x8 x7,
(min_value <= x7) ->(min_value <= x8) ->min_value <= P_id_add x8 x7.
Definition measure :=
Interp.measure min_value P_id_lt P_id_split P_id_false P_id_qsort
P_id_s P_id_f_1 P_id_nil P_id_0 P_id_pair P_id_append P_id_f_3
P_id_true P_id_f_2 P_id_add.
Lemma measure_equation :
forall t,
measure t = match t with
| (algebra.Alg.Term algebra.F.id_lt (x8::x7::nil)) =>
P_id_lt (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_split (x8::x7::nil)) =>
P_id_split (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_false nil) => P_id_false
| (algebra.Alg.Term algebra.F.id_qsort (x7::nil)) =>
P_id_qsort (measure x7)
| (algebra.Alg.Term algebra.F.id_s (x7::nil)) =>
P_id_s (measure x7)
| (algebra.Alg.Term algebra.F.id_f_1 (x10::x9::x8::
x7::nil)) =>
P_id_f_1 (measure x10) (measure x9) (measure x8)
(measure x7)
| (algebra.Alg.Term algebra.F.id_nil nil) => P_id_nil
| (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0
| (algebra.Alg.Term algebra.F.id_pair (x8::x7::nil)) =>
P_id_pair (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_append (x8::x7::nil)) =>
P_id_append (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_3 (x9::x8::x7::nil)) =>
P_id_f_3 (measure x9) (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_true nil) => P_id_true
| (algebra.Alg.Term algebra.F.id_f_2 (x12::x11::x10::x9::
x8::x7::nil)) =>
P_id_f_2 (measure x12) (measure x11) (measure x10)
(measure x9) (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_add (x8::x7::nil)) =>
P_id_add (measure x8) (measure x7)
| _ => 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_lt_monotonic;assumption.
intros ;apply P_id_split_monotonic;assumption.
intros ;apply P_id_qsort_monotonic;assumption.
intros ;apply P_id_s_monotonic;assumption.
intros ;apply P_id_f_1_monotonic;assumption.
intros ;apply P_id_pair_monotonic;assumption.
intros ;apply P_id_append_monotonic;assumption.
intros ;apply P_id_f_3_monotonic;assumption.
intros ;apply P_id_f_2_monotonic;assumption.
intros ;apply P_id_add_monotonic;assumption.
intros ;apply P_id_lt_bounded;assumption.
intros ;apply P_id_split_bounded;assumption.
intros ;apply P_id_false_bounded;assumption.
intros ;apply P_id_qsort_bounded;assumption.
intros ;apply P_id_s_bounded;assumption.
intros ;apply P_id_f_1_bounded;assumption.
intros ;apply P_id_nil_bounded;assumption.
intros ;apply P_id_0_bounded;assumption.
intros ;apply P_id_pair_bounded;assumption.
intros ;apply P_id_append_bounded;assumption.
intros ;apply P_id_f_3_bounded;assumption.
intros ;apply P_id_true_bounded;assumption.
intros ;apply P_id_f_2_bounded;assumption.
intros ;apply P_id_add_bounded;assumption.
apply rules_monotonic.
Qed.
Hypothesis P_id_SPLIT : Z ->Z ->Z.
Hypothesis P_id_F_3 : Z ->Z ->Z ->Z.
Hypothesis P_id_F_2 : Z ->Z ->Z ->Z ->Z ->Z ->Z.
Hypothesis P_id_LT : Z ->Z ->Z.
Hypothesis P_id_F_1 : Z ->Z ->Z ->Z ->Z.
Hypothesis P_id_QSORT : Z ->Z.
Hypothesis P_id_APPEND : Z ->Z ->Z.
Hypothesis P_id_SPLIT_monotonic :
forall x8 x10 x9 x7,
(min_value <= x10)/\ (x10 <= x9) ->
(min_value <= x8)/\ (x8 <= x7) ->P_id_SPLIT x8 x10 <= P_id_SPLIT x7 x9.
Hypothesis P_id_F_3_monotonic :
forall x8 x12 x10 x9 x11 x7,
(min_value <= x12)/\ (x12 <= x11) ->
(min_value <= x10)/\ (x10 <= x9) ->
(min_value <= x8)/\ (x8 <= x7) ->
P_id_F_3 x8 x10 x12 <= P_id_F_3 x7 x9 x11.
Hypothesis P_id_F_2_monotonic :
forall x16 x8 x12 x18 x10 x14 x17 x9 x13 x11 x7 x15,
(min_value <= x18)/\ (x18 <= x17) ->
(min_value <= x16)/\ (x16 <= x15) ->
(min_value <= x14)/\ (x14 <= x13) ->
(min_value <= x12)/\ (x12 <= x11) ->
(min_value <= x10)/\ (x10 <= x9) ->
(min_value <= x8)/\ (x8 <= x7) ->
P_id_F_2 x8 x10 x12 x14 x16 x18 <= P_id_F_2 x7 x9 x11 x13 x15 x17.
Hypothesis P_id_LT_monotonic :
forall x8 x10 x9 x7,
(min_value <= x10)/\ (x10 <= x9) ->
(min_value <= x8)/\ (x8 <= x7) ->P_id_LT x8 x10 <= P_id_LT x7 x9.
Hypothesis P_id_F_1_monotonic :
forall x8 x12 x10 x14 x9 x13 x11 x7,
(min_value <= x14)/\ (x14 <= x13) ->
(min_value <= x12)/\ (x12 <= x11) ->
(min_value <= x10)/\ (x10 <= x9) ->
(min_value <= x8)/\ (x8 <= x7) ->
P_id_F_1 x8 x10 x12 x14 <= P_id_F_1 x7 x9 x11 x13.
Hypothesis P_id_QSORT_monotonic :
forall x8 x7,
(min_value <= x8)/\ (x8 <= x7) ->P_id_QSORT x8 <= P_id_QSORT x7.
Hypothesis P_id_APPEND_monotonic :
forall x8 x10 x9 x7,
(min_value <= x10)/\ (x10 <= x9) ->
(min_value <= x8)/\ (x8 <= x7) ->
P_id_APPEND x8 x10 <= P_id_APPEND x7 x9.
Definition marked_measure :=
Interp.marked_measure min_value P_id_lt P_id_split P_id_false
P_id_qsort P_id_s P_id_f_1 P_id_nil P_id_0 P_id_pair P_id_append
P_id_f_3 P_id_true P_id_f_2 P_id_add P_id_SPLIT P_id_F_3 P_id_F_2
P_id_LT P_id_F_1 P_id_QSORT P_id_APPEND.
Lemma marked_measure_equation :
forall t,
marked_measure t = match t with
| (algebra.Alg.Term algebra.F.id_split (x8::
x7::nil)) =>
P_id_SPLIT (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_3 (x9::x8::
x7::nil)) =>
P_id_F_3 (measure x9) (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_2 (x12::x11::
x10::x9::x8::x7::nil)) =>
P_id_F_2 (measure x12) (measure x11)
(measure x10) (measure x9) (measure x8)
(measure x7)
| (algebra.Alg.Term algebra.F.id_lt (x8::x7::nil)) =>
P_id_LT (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_1 (x10::x9::x8::
x7::nil)) =>
P_id_F_1 (measure x10) (measure x9) (measure x8)
(measure x7)
| (algebra.Alg.Term algebra.F.id_qsort (x7::nil)) =>
P_id_QSORT (measure x7)
| (algebra.Alg.Term algebra.F.id_append (x8::
x7::nil)) =>
P_id_APPEND (measure x8) (measure x7)
| _ => 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_lt_monotonic;assumption.
intros ;apply P_id_split_monotonic;assumption.
intros ;apply P_id_qsort_monotonic;assumption.
intros ;apply P_id_s_monotonic;assumption.
intros ;apply P_id_f_1_monotonic;assumption.
intros ;apply P_id_pair_monotonic;assumption.
intros ;apply P_id_append_monotonic;assumption.
intros ;apply P_id_f_3_monotonic;assumption.
intros ;apply P_id_f_2_monotonic;assumption.
intros ;apply P_id_add_monotonic;assumption.
intros ;apply P_id_lt_bounded;assumption.
intros ;apply P_id_split_bounded;assumption.
intros ;apply P_id_false_bounded;assumption.
intros ;apply P_id_qsort_bounded;assumption.
intros ;apply P_id_s_bounded;assumption.
intros ;apply P_id_f_1_bounded;assumption.
intros ;apply P_id_nil_bounded;assumption.
intros ;apply P_id_0_bounded;assumption.
intros ;apply P_id_pair_bounded;assumption.
intros ;apply P_id_append_bounded;assumption.
intros ;apply P_id_f_3_bounded;assumption.
intros ;apply P_id_true_bounded;assumption.
intros ;apply P_id_f_2_bounded;assumption.
intros ;apply P_id_add_bounded;assumption.
apply rules_monotonic.
intros ;apply P_id_SPLIT_monotonic;assumption.
intros ;apply P_id_F_3_monotonic;assumption.
intros ;apply P_id_F_2_monotonic;assumption.
intros ;apply P_id_LT_monotonic;assumption.
intros ;apply P_id_F_1_monotonic;assumption.
intros ;apply P_id_QSORT_monotonic;assumption.
intros ;apply P_id_APPEND_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 :=
(* <lt(s(X_),s(Y_)),lt(X_,Y_)> *)
| DP_R_xml_0_0 :
forall x8 x2 x1 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_s (x1::nil))
x8) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_s (x2::nil))
x7) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_lt (x1::x2::nil))
(algebra.Alg.Term algebra.F.id_lt (x8::x7::nil))
(* <append(add(N_,X_),Y_),append(X_,Y_)> *)
| DP_R_xml_0_1 :
forall x8 x2 x1 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_add (x3::x1::nil)) x8) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x2 x7) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_append (x1::x2::nil))
(algebra.Alg.Term algebra.F.id_append (x8::x7::nil))
(* <split(N_,add(M_,Y_)),f_1(split(N_,Y_),N_,M_,Y_)> *)
| DP_R_xml_0_2 :
forall x8 x4 x2 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x3 x8) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_add (x4::x2::nil)) x7) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_f_1 ((algebra.Alg.Term
algebra.F.id_split (x3::x2::nil))::x3::x4::x2::nil))
(algebra.Alg.Term algebra.F.id_split (x8::x7::nil))
(* <split(N_,add(M_,Y_)),split(N_,Y_)> *)
| DP_R_xml_0_3 :
forall x8 x4 x2 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x3 x8) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_add (x4::x2::nil)) x7) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_split (x3::x2::nil))
(algebra.Alg.Term algebra.F.id_split (x8::x7::nil))
(* <f_1(pair(X_,Z_),N_,M_,Y_),f_2(lt(N_,M_),N_,M_,Y_,X_,Z_)> *)
| DP_R_xml_0_4 :
forall x8 x4 x2 x10 x1 x9 x5 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_pair (x1::x5::nil)) x10) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x3 x9) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x4 x8) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x2 x7) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_f_2 ((algebra.Alg.Term
algebra.F.id_lt (x3::x4::nil))::x3::x4::x2::x1::
x5::nil))
(algebra.Alg.Term algebra.F.id_f_1 (x10::x9::x8::x7::nil))
(* <f_1(pair(X_,Z_),N_,M_,Y_),lt(N_,M_)> *)
| DP_R_xml_0_5 :
forall x8 x4 x2 x10 x1 x9 x5 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_pair (x1::x5::nil)) x10) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x3 x9) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x4 x8) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x2 x7) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_lt (x3::x4::nil))
(algebra.Alg.Term algebra.F.id_f_1 (x10::x9::x8::x7::nil))
(* <qsort(add(N_,X_)),f_3(split(N_,X_),N_,X_)> *)
| DP_R_xml_0_6 :
forall x1 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_add (x3::x1::nil)) x7) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_f_3 ((algebra.Alg.Term
algebra.F.id_split (x3::x1::nil))::x3::x1::nil))
(algebra.Alg.Term algebra.F.id_qsort (x7::nil))
(* <qsort(add(N_,X_)),split(N_,X_)> *)
| DP_R_xml_0_7 :
forall x1 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_add (x3::x1::nil)) x7) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_split (x3::x1::nil))
(algebra.Alg.Term algebra.F.id_qsort (x7::nil))
(* <f_3(pair(Y_,Z_),N_,X_),append(qsort(Y_),add(X_,qsort(Z_)))> *)
| DP_R_xml_0_8 :
forall x8 x2 x1 x9 x5 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_pair (x2::x5::nil)) x9) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x3 x8) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x1 x7) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_append ((algebra.Alg.Term
algebra.F.id_qsort (x2::nil))::(algebra.Alg.Term
algebra.F.id_add (x1::(algebra.Alg.Term
algebra.F.id_qsort (x5::nil))::nil))::nil))
(algebra.Alg.Term algebra.F.id_f_3 (x9::x8::x7::nil))
(* <f_3(pair(Y_,Z_),N_,X_),qsort(Y_)> *)
| DP_R_xml_0_9 :
forall x8 x2 x1 x9 x5 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_pair (x2::x5::nil)) x9) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x3 x8) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x1 x7) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_qsort (x2::nil))
(algebra.Alg.Term algebra.F.id_f_3 (x9::x8::x7::nil))
(* <f_3(pair(Y_,Z_),N_,X_),qsort(Z_)> *)
| DP_R_xml_0_10 :
forall x8 x2 x1 x9 x5 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_pair (x2::x5::nil)) x9) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x3 x8) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x1 x7) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_qsort (x5::nil))
(algebra.Alg.Term algebra.F.id_f_3 (x9::x8::x7::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 :=
(* <f_1(pair(X_,Z_),N_,M_,Y_),f_2(lt(N_,M_),N_,M_,Y_,X_,Z_)> *)
| DP_R_xml_0_non_scc_1_0 :
forall x8 x4 x2 x10 x1 x9 x5 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_pair (x1::x5::nil)) x10) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x3 x9) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x4 x8) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x2 x7) ->
DP_R_xml_0_non_scc_1 (algebra.Alg.Term algebra.F.id_f_2
((algebra.Alg.Term algebra.F.id_lt (x3::
x4::nil))::x3::x4::x2::x1::x5::nil))
(algebra.Alg.Term algebra.F.id_f_1 (x10::x9::x8::x7::nil))
.
Lemma acc_DP_R_xml_0_non_scc_1 :
forall x y,
(DP_R_xml_0_non_scc_1 x y) ->Acc WF_R_xml_0_deep_rew.DP_R_xml_0 x.
Proof.
intros x y h.
inversion h;clear h;subst;
constructor;intros _y _h;inversion _h;clear _h;subst;
(R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 )||
(eapply Hrec;econstructor (eassumption)||(algebra.Alg_ext.star_refl' )).
Qed.
Inductive DP_R_xml_0_scc_2 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <append(add(N_,X_),Y_),append(X_,Y_)> *)
| DP_R_xml_0_scc_2_0 :
forall x8 x2 x1 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_add (x3::x1::nil)) x8) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x2 x7) ->
DP_R_xml_0_scc_2 (algebra.Alg.Term algebra.F.id_append (x1::x2::nil))
(algebra.Alg.Term algebra.F.id_append (x8::x7::nil))
.
Module WF_DP_R_xml_0_scc_2.
Open Scope Z_scope.
Import ring_extention.
Notation Local "a <= b" := (Zle a b).
Notation Local "a < b" := (Zlt a b).
Definition P_id_lt (x7:Z) (x8:Z) := 2.
Definition P_id_split (x7:Z) (x8:Z) := 1* x8.
Definition P_id_false := 2.
Definition P_id_qsort (x7:Z) := 1* x7.
Definition P_id_s (x7:Z) := 0.
Definition P_id_f_1 (x7:Z) (x8:Z) (x9:Z) (x10:Z) := 2 + 1* x7.
Definition P_id_nil := 0.
Definition P_id_0 := 0.
Definition P_id_pair (x7:Z) (x8:Z) := 1* x7 + 1* x8.
Definition P_id_append (x7:Z) (x8:Z) := 1* x7 + 1* x8.
Definition P_id_f_3 (x7:Z) (x8:Z) (x9:Z) := 2 + 1* x7.
Definition P_id_true := 2.
Definition P_id_f_2 (x7:Z) (x8:Z) (x9:Z) (x10:Z) (x11:Z) (x12:Z) :=
1* x7 + 1* x11 + 1* x12.
Definition P_id_add (x7:Z) (x8:Z) := 2 + 1* x8.
Lemma P_id_lt_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_lt x8 x10 <= P_id_lt x7 x9.
Proof.
intros x10 x9 x8 x7.
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_split_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_split x8 x10 <= P_id_split x7 x9.
Proof.
intros x10 x9 x8 x7.
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_qsort_monotonic :
forall x8 x7, (0 <= x8)/\ (x8 <= x7) ->P_id_qsort x8 <= P_id_qsort x7.
Proof.
intros x8 x7.
intros [H_1 H_0].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_s_monotonic :
forall x8 x7, (0 <= x8)/\ (x8 <= x7) ->P_id_s x8 <= P_id_s x7.
Proof.
intros x8 x7.
intros [H_1 H_0].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_f_1_monotonic :
forall x8 x12 x10 x14 x9 x13 x11 x7,
(0 <= x14)/\ (x14 <= x13) ->
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->
P_id_f_1 x8 x10 x12 x14 <= P_id_f_1 x7 x9 x11 x13.
Proof.
intros x14 x13 x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
intros [H_7 H_6].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_pair_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_pair x8 x10 <= P_id_pair x7 x9.
Proof.
intros x10 x9 x8 x7.
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_append_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_append x8 x10 <= P_id_append x7 x9.
Proof.
intros x10 x9 x8 x7.
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_f_3_monotonic :
forall x8 x12 x10 x9 x11 x7,
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_f_3 x8 x10 x12 <= P_id_f_3 x7 x9 x11.
Proof.
intros x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_f_2_monotonic :
forall x16 x8 x12 x18 x10 x14 x17 x9 x13 x11 x7 x15,
(0 <= x18)/\ (x18 <= x17) ->
(0 <= x16)/\ (x16 <= x15) ->
(0 <= x14)/\ (x14 <= x13) ->
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->
P_id_f_2 x8 x10 x12 x14 x16 x18 <= P_id_f_2 x7 x9 x11 x13 x15 x17.
Proof.
intros x18 x17 x16 x15 x14 x13 x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
intros [H_7 H_6].
intros [H_9 H_8].
intros [H_11 H_10].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_add_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_add x8 x10 <= P_id_add x7 x9.
Proof.
intros x10 x9 x8 x7.
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_lt_bounded :
forall x8 x7, (0 <= x7) ->(0 <= x8) ->0 <= P_id_lt x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_split_bounded :
forall x8 x7, (0 <= x7) ->(0 <= x8) ->0 <= P_id_split x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_false_bounded : 0 <= P_id_false .
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_qsort_bounded : forall x7, (0 <= x7) ->0 <= P_id_qsort x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_s_bounded : forall x7, (0 <= x7) ->0 <= P_id_s x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_f_1_bounded :
forall x8 x10 x9 x7,
(0 <= x7) ->
(0 <= x8) ->(0 <= x9) ->(0 <= x10) ->0 <= P_id_f_1 x10 x9 x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_nil_bounded : 0 <= P_id_nil .
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_pair_bounded :
forall x8 x7, (0 <= x7) ->(0 <= x8) ->0 <= P_id_pair x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_append_bounded :
forall x8 x7, (0 <= x7) ->(0 <= x8) ->0 <= P_id_append x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_f_3_bounded :
forall x8 x9 x7,
(0 <= x7) ->(0 <= x8) ->(0 <= x9) ->0 <= P_id_f_3 x9 x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_true_bounded : 0 <= P_id_true .
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_f_2_bounded :
forall x8 x12 x10 x9 x11 x7,
(0 <= x7) ->
(0 <= x8) ->
(0 <= x9) ->
(0 <= x10) ->
(0 <= x11) ->(0 <= x12) ->0 <= P_id_f_2 x12 x11 x10 x9 x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_add_bounded :
forall x8 x7, (0 <= x7) ->(0 <= x8) ->0 <= P_id_add x8 x7.
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_lt P_id_split P_id_false P_id_qsort P_id_s
P_id_f_1 P_id_nil P_id_0 P_id_pair P_id_append P_id_f_3 P_id_true
P_id_f_2 P_id_add.
Lemma measure_equation :
forall t,
measure t = match t with
| (algebra.Alg.Term algebra.F.id_lt (x8::x7::nil)) =>
P_id_lt (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_split (x8::x7::nil)) =>
P_id_split (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_false nil) => P_id_false
| (algebra.Alg.Term algebra.F.id_qsort (x7::nil)) =>
P_id_qsort (measure x7)
| (algebra.Alg.Term algebra.F.id_s (x7::nil)) =>
P_id_s (measure x7)
| (algebra.Alg.Term algebra.F.id_f_1 (x10::x9::x8::
x7::nil)) =>
P_id_f_1 (measure x10) (measure x9) (measure x8)
(measure x7)
| (algebra.Alg.Term algebra.F.id_nil nil) => P_id_nil
| (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0
| (algebra.Alg.Term algebra.F.id_pair (x8::x7::nil)) =>
P_id_pair (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_append (x8::x7::nil)) =>
P_id_append (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_3 (x9::x8::x7::nil)) =>
P_id_f_3 (measure x9) (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_true nil) => P_id_true
| (algebra.Alg.Term algebra.F.id_f_2 (x12::x11::x10::x9::
x8::x7::nil)) =>
P_id_f_2 (measure x12) (measure x11) (measure x10)
(measure x9) (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_add (x8::x7::nil)) =>
P_id_add (measure x8) (measure x7)
| _ => 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_lt_monotonic;assumption.
intros ;apply P_id_split_monotonic;assumption.
intros ;apply P_id_qsort_monotonic;assumption.
intros ;apply P_id_s_monotonic;assumption.
intros ;apply P_id_f_1_monotonic;assumption.
intros ;apply P_id_pair_monotonic;assumption.
intros ;apply P_id_append_monotonic;assumption.
intros ;apply P_id_f_3_monotonic;assumption.
intros ;apply P_id_f_2_monotonic;assumption.
intros ;apply P_id_add_monotonic;assumption.
intros ;apply P_id_lt_bounded;assumption.
intros ;apply P_id_split_bounded;assumption.
intros ;apply P_id_false_bounded;assumption.
intros ;apply P_id_qsort_bounded;assumption.
intros ;apply P_id_s_bounded;assumption.
intros ;apply P_id_f_1_bounded;assumption.
intros ;apply P_id_nil_bounded;assumption.
intros ;apply P_id_0_bounded;assumption.
intros ;apply P_id_pair_bounded;assumption.
intros ;apply P_id_append_bounded;assumption.
intros ;apply P_id_f_3_bounded;assumption.
intros ;apply P_id_true_bounded;assumption.
intros ;apply P_id_f_2_bounded;assumption.
intros ;apply P_id_add_bounded;assumption.
apply rules_monotonic.
Qed.
Definition P_id_SPLIT (x7:Z) (x8:Z) := 0.
Definition P_id_F_3 (x7:Z) (x8:Z) (x9:Z) := 0.
Definition P_id_F_2 (x7:Z) (x8:Z) (x9:Z) (x10:Z) (x11:Z) (x12:Z) := 0.
Definition P_id_LT (x7:Z) (x8:Z) := 0.
Definition P_id_F_1 (x7:Z) (x8:Z) (x9:Z) (x10:Z) := 0.
Definition P_id_QSORT (x7:Z) := 0.
Definition P_id_APPEND (x7:Z) (x8:Z) := 1* x7.
Lemma P_id_SPLIT_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_SPLIT x8 x10 <= P_id_SPLIT x7 x9.
Proof.
intros x10 x9 x8 x7.
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_F_3_monotonic :
forall x8 x12 x10 x9 x11 x7,
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_F_3 x8 x10 x12 <= P_id_F_3 x7 x9 x11.
Proof.
intros x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_F_2_monotonic :
forall x16 x8 x12 x18 x10 x14 x17 x9 x13 x11 x7 x15,
(0 <= x18)/\ (x18 <= x17) ->
(0 <= x16)/\ (x16 <= x15) ->
(0 <= x14)/\ (x14 <= x13) ->
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->
P_id_F_2 x8 x10 x12 x14 x16 x18 <= P_id_F_2 x7 x9 x11 x13 x15 x17.
Proof.
intros x18 x17 x16 x15 x14 x13 x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
intros [H_7 H_6].
intros [H_9 H_8].
intros [H_11 H_10].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_LT_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_LT x8 x10 <= P_id_LT x7 x9.
Proof.
intros x10 x9 x8 x7.
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_F_1_monotonic :
forall x8 x12 x10 x14 x9 x13 x11 x7,
(0 <= x14)/\ (x14 <= x13) ->
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->
P_id_F_1 x8 x10 x12 x14 <= P_id_F_1 x7 x9 x11 x13.
Proof.
intros x14 x13 x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
intros [H_7 H_6].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_QSORT_monotonic :
forall x8 x7, (0 <= x8)/\ (x8 <= x7) ->P_id_QSORT x8 <= P_id_QSORT x7.
Proof.
intros x8 x7.
intros [H_1 H_0].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_APPEND_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_APPEND x8 x10 <= P_id_APPEND x7 x9.
Proof.
intros x10 x9 x8 x7.
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_lt P_id_split P_id_false P_id_qsort
P_id_s P_id_f_1 P_id_nil P_id_0 P_id_pair P_id_append P_id_f_3
P_id_true P_id_f_2 P_id_add P_id_SPLIT P_id_F_3 P_id_F_2 P_id_LT
P_id_F_1 P_id_QSORT P_id_APPEND.
Lemma marked_measure_equation :
forall t,
marked_measure t = match t with
| (algebra.Alg.Term algebra.F.id_split (x8::
x7::nil)) =>
P_id_SPLIT (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_3 (x9::x8::
x7::nil)) =>
P_id_F_3 (measure x9) (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_2 (x12::x11::
x10::x9::x8::x7::nil)) =>
P_id_F_2 (measure x12) (measure x11)
(measure x10) (measure x9) (measure x8)
(measure x7)
| (algebra.Alg.Term algebra.F.id_lt (x8::x7::nil)) =>
P_id_LT (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_1 (x10::x9::x8::
x7::nil)) =>
P_id_F_1 (measure x10) (measure x9) (measure x8)
(measure x7)
| (algebra.Alg.Term algebra.F.id_qsort (x7::nil)) =>
P_id_QSORT (measure x7)
| (algebra.Alg.Term algebra.F.id_append (x8::
x7::nil)) =>
P_id_APPEND (measure x8) (measure x7)
| _ => 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_lt_monotonic;assumption.
intros ;apply P_id_split_monotonic;assumption.
intros ;apply P_id_qsort_monotonic;assumption.
intros ;apply P_id_s_monotonic;assumption.
intros ;apply P_id_f_1_monotonic;assumption.
intros ;apply P_id_pair_monotonic;assumption.
intros ;apply P_id_append_monotonic;assumption.
intros ;apply P_id_f_3_monotonic;assumption.
intros ;apply P_id_f_2_monotonic;assumption.
intros ;apply P_id_add_monotonic;assumption.
intros ;apply P_id_lt_bounded;assumption.
intros ;apply P_id_split_bounded;assumption.
intros ;apply P_id_false_bounded;assumption.
intros ;apply P_id_qsort_bounded;assumption.
intros ;apply P_id_s_bounded;assumption.
intros ;apply P_id_f_1_bounded;assumption.
intros ;apply P_id_nil_bounded;assumption.
intros ;apply P_id_0_bounded;assumption.
intros ;apply P_id_pair_bounded;assumption.
intros ;apply P_id_append_bounded;assumption.
intros ;apply P_id_f_3_bounded;assumption.
intros ;apply P_id_true_bounded;assumption.
intros ;apply P_id_f_2_bounded;assumption.
intros ;apply P_id_add_bounded;assumption.
apply rules_monotonic.
intros ;apply P_id_SPLIT_monotonic;assumption.
intros ;apply P_id_F_3_monotonic;assumption.
intros ;apply P_id_F_2_monotonic;assumption.
intros ;apply P_id_LT_monotonic;assumption.
intros ;apply P_id_F_1_monotonic;assumption.
intros ;apply P_id_QSORT_monotonic;assumption.
intros ;apply P_id_APPEND_monotonic;assumption.
Qed.
Ltac rewrite_and_unfold :=
do 2 (rewrite marked_measure_equation);
repeat (
match goal with
| |- context [measure (algebra.Alg.Term ?f ?t)] =>
rewrite (measure_equation (algebra.Alg.Term f t))
| H:context [measure (algebra.Alg.Term ?f ?t)] |- _ =>
rewrite (measure_equation (algebra.Alg.Term f t)) in H|-
end
).
Lemma wf : well_founded WF_DP_R_xml_0.DP_R_xml_0_scc_2.
Proof.
intros x.
apply well_founded_ind with
(R:=fun x y => (Zwf.Zwf 0) (marked_measure x) (marked_measure y)).
apply Inverse_Image.wf_inverse_image with (B:=Z).
apply Zwf.Zwf_well_founded.
clear x.
intros x IHx.
repeat (
constructor;inversion 1;subst;
full_prove_ineq algebra.Alg.Term
ltac:(algebra.Alg_ext.find_replacement )
algebra.EQT_ext.one_step_list_refl_trans_clos marked_measure
marked_measure_star_monotonic (Zwf.Zwf 0) (interp.o_Z 0)
ltac:(fun _ => R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 )
ltac:(fun _ => rewrite_and_unfold ) ltac:(fun _ => generate_pos_hyp )
ltac:(fun _ => cbv beta iota zeta delta - [Zplus Zmult Zle Zlt] in * ;
try (constructor))
IHx
).
Qed.
End WF_DP_R_xml_0_scc_2.
Definition wf_DP_R_xml_0_scc_2 := WF_DP_R_xml_0_scc_2.wf.
Lemma acc_DP_R_xml_0_scc_2 :
forall x y, (DP_R_xml_0_scc_2 x y) ->Acc WF_R_xml_0_deep_rew.DP_R_xml_0 x.
Proof.
intros x.
pattern x.
apply (@Acc_ind _ DP_R_xml_0_scc_2).
intros x' _ Hrec y h.
inversion h;clear h;subst;
constructor;intros _y _h;inversion _h;clear _h;subst;
(eapply Hrec;econstructor eassumption)||
((R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 )||
(eapply Hrec;econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))).
apply wf_DP_R_xml_0_scc_2.
Qed.
Inductive DP_R_xml_0_non_scc_3 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <f_3(pair(Y_,Z_),N_,X_),append(qsort(Y_),add(X_,qsort(Z_)))> *)
| DP_R_xml_0_non_scc_3_0 :
forall x8 x2 x1 x9 x5 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_pair (x2::x5::nil)) x9) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x3 x8) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x1 x7) ->
DP_R_xml_0_non_scc_3 (algebra.Alg.Term algebra.F.id_append
((algebra.Alg.Term algebra.F.id_qsort
(x2::nil))::(algebra.Alg.Term
algebra.F.id_add (x1::(algebra.Alg.Term
algebra.F.id_qsort (x5::nil))::nil))::nil))
(algebra.Alg.Term algebra.F.id_f_3 (x9::x8::x7::nil))
.
Lemma acc_DP_R_xml_0_non_scc_3 :
forall x y,
(DP_R_xml_0_non_scc_3 x y) ->Acc WF_R_xml_0_deep_rew.DP_R_xml_0 x.
Proof.
intros x y h.
inversion h;clear h;subst;
constructor;intros _y _h;inversion _h;clear _h;subst;
(eapply acc_DP_R_xml_0_scc_2;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((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_4 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <lt(s(X_),s(Y_)),lt(X_,Y_)> *)
| DP_R_xml_0_scc_4_0 :
forall x8 x2 x1 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_s (x1::nil))
x8) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_s (x2::nil)) x7) ->
DP_R_xml_0_scc_4 (algebra.Alg.Term algebra.F.id_lt (x1::x2::nil))
(algebra.Alg.Term algebra.F.id_lt (x8::x7::nil))
.
Module WF_DP_R_xml_0_scc_4.
Open Scope Z_scope.
Import ring_extention.
Notation Local "a <= b" := (Zle a b).
Notation Local "a < b" := (Zlt a b).
Definition P_id_lt (x7:Z) (x8:Z) := 1* x7.
Definition P_id_split (x7:Z) (x8:Z) := 0.
Definition P_id_false := 0.
Definition P_id_qsort (x7:Z) := 0.
Definition P_id_s (x7:Z) := 1 + 2* x7.
Definition P_id_f_1 (x7:Z) (x8:Z) (x9:Z) (x10:Z) := 3* x7.
Definition P_id_nil := 0.
Definition P_id_0 := 1.
Definition P_id_pair (x7:Z) (x8:Z) := 2* x7 + 1* x8.
Definition P_id_append (x7:Z) (x8:Z) := 1* x8.
Definition P_id_f_3 (x7:Z) (x8:Z) (x9:Z) := 1* x7.
Definition P_id_true := 0.
Definition P_id_f_2 (x7:Z) (x8:Z) (x9:Z) (x10:Z) (x11:Z) (x12:Z) :=
3* x11 + 2* x12.
Definition P_id_add (x7:Z) (x8:Z) := 0.
Lemma P_id_lt_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_lt x8 x10 <= P_id_lt x7 x9.
Proof.
intros x10 x9 x8 x7.
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_split_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_split x8 x10 <= P_id_split x7 x9.
Proof.
intros x10 x9 x8 x7.
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_qsort_monotonic :
forall x8 x7, (0 <= x8)/\ (x8 <= x7) ->P_id_qsort x8 <= P_id_qsort x7.
Proof.
intros x8 x7.
intros [H_1 H_0].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_s_monotonic :
forall x8 x7, (0 <= x8)/\ (x8 <= x7) ->P_id_s x8 <= P_id_s x7.
Proof.
intros x8 x7.
intros [H_1 H_0].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_f_1_monotonic :
forall x8 x12 x10 x14 x9 x13 x11 x7,
(0 <= x14)/\ (x14 <= x13) ->
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->
P_id_f_1 x8 x10 x12 x14 <= P_id_f_1 x7 x9 x11 x13.
Proof.
intros x14 x13 x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
intros [H_7 H_6].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_pair_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_pair x8 x10 <= P_id_pair x7 x9.
Proof.
intros x10 x9 x8 x7.
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_append_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_append x8 x10 <= P_id_append x7 x9.
Proof.
intros x10 x9 x8 x7.
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_f_3_monotonic :
forall x8 x12 x10 x9 x11 x7,
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_f_3 x8 x10 x12 <= P_id_f_3 x7 x9 x11.
Proof.
intros x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_f_2_monotonic :
forall x16 x8 x12 x18 x10 x14 x17 x9 x13 x11 x7 x15,
(0 <= x18)/\ (x18 <= x17) ->
(0 <= x16)/\ (x16 <= x15) ->
(0 <= x14)/\ (x14 <= x13) ->
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->
P_id_f_2 x8 x10 x12 x14 x16 x18 <= P_id_f_2 x7 x9 x11 x13 x15 x17.
Proof.
intros x18 x17 x16 x15 x14 x13 x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
intros [H_7 H_6].
intros [H_9 H_8].
intros [H_11 H_10].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_add_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_add x8 x10 <= P_id_add x7 x9.
Proof.
intros x10 x9 x8 x7.
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_lt_bounded :
forall x8 x7, (0 <= x7) ->(0 <= x8) ->0 <= P_id_lt x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_split_bounded :
forall x8 x7, (0 <= x7) ->(0 <= x8) ->0 <= P_id_split x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_false_bounded : 0 <= P_id_false .
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_qsort_bounded : forall x7, (0 <= x7) ->0 <= P_id_qsort x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_s_bounded : forall x7, (0 <= x7) ->0 <= P_id_s x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_f_1_bounded :
forall x8 x10 x9 x7,
(0 <= x7) ->
(0 <= x8) ->(0 <= x9) ->(0 <= x10) ->0 <= P_id_f_1 x10 x9 x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_nil_bounded : 0 <= P_id_nil .
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_pair_bounded :
forall x8 x7, (0 <= x7) ->(0 <= x8) ->0 <= P_id_pair x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_append_bounded :
forall x8 x7, (0 <= x7) ->(0 <= x8) ->0 <= P_id_append x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_f_3_bounded :
forall x8 x9 x7,
(0 <= x7) ->(0 <= x8) ->(0 <= x9) ->0 <= P_id_f_3 x9 x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_true_bounded : 0 <= P_id_true .
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_f_2_bounded :
forall x8 x12 x10 x9 x11 x7,
(0 <= x7) ->
(0 <= x8) ->
(0 <= x9) ->
(0 <= x10) ->
(0 <= x11) ->(0 <= x12) ->0 <= P_id_f_2 x12 x11 x10 x9 x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_add_bounded :
forall x8 x7, (0 <= x7) ->(0 <= x8) ->0 <= P_id_add x8 x7.
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_lt P_id_split P_id_false P_id_qsort P_id_s
P_id_f_1 P_id_nil P_id_0 P_id_pair P_id_append P_id_f_3 P_id_true
P_id_f_2 P_id_add.
Lemma measure_equation :
forall t,
measure t = match t with
| (algebra.Alg.Term algebra.F.id_lt (x8::x7::nil)) =>
P_id_lt (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_split (x8::x7::nil)) =>
P_id_split (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_false nil) => P_id_false
| (algebra.Alg.Term algebra.F.id_qsort (x7::nil)) =>
P_id_qsort (measure x7)
| (algebra.Alg.Term algebra.F.id_s (x7::nil)) =>
P_id_s (measure x7)
| (algebra.Alg.Term algebra.F.id_f_1 (x10::x9::x8::
x7::nil)) =>
P_id_f_1 (measure x10) (measure x9) (measure x8)
(measure x7)
| (algebra.Alg.Term algebra.F.id_nil nil) => P_id_nil
| (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0
| (algebra.Alg.Term algebra.F.id_pair (x8::x7::nil)) =>
P_id_pair (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_append (x8::x7::nil)) =>
P_id_append (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_3 (x9::x8::x7::nil)) =>
P_id_f_3 (measure x9) (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_true nil) => P_id_true
| (algebra.Alg.Term algebra.F.id_f_2 (x12::x11::x10::x9::
x8::x7::nil)) =>
P_id_f_2 (measure x12) (measure x11) (measure x10)
(measure x9) (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_add (x8::x7::nil)) =>
P_id_add (measure x8) (measure x7)
| _ => 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_lt_monotonic;assumption.
intros ;apply P_id_split_monotonic;assumption.
intros ;apply P_id_qsort_monotonic;assumption.
intros ;apply P_id_s_monotonic;assumption.
intros ;apply P_id_f_1_monotonic;assumption.
intros ;apply P_id_pair_monotonic;assumption.
intros ;apply P_id_append_monotonic;assumption.
intros ;apply P_id_f_3_monotonic;assumption.
intros ;apply P_id_f_2_monotonic;assumption.
intros ;apply P_id_add_monotonic;assumption.
intros ;apply P_id_lt_bounded;assumption.
intros ;apply P_id_split_bounded;assumption.
intros ;apply P_id_false_bounded;assumption.
intros ;apply P_id_qsort_bounded;assumption.
intros ;apply P_id_s_bounded;assumption.
intros ;apply P_id_f_1_bounded;assumption.
intros ;apply P_id_nil_bounded;assumption.
intros ;apply P_id_0_bounded;assumption.
intros ;apply P_id_pair_bounded;assumption.
intros ;apply P_id_append_bounded;assumption.
intros ;apply P_id_f_3_bounded;assumption.
intros ;apply P_id_true_bounded;assumption.
intros ;apply P_id_f_2_bounded;assumption.
intros ;apply P_id_add_bounded;assumption.
apply rules_monotonic.
Qed.
Definition P_id_SPLIT (x7:Z) (x8:Z) := 0.
Definition P_id_F_3 (x7:Z) (x8:Z) (x9:Z) := 0.
Definition P_id_F_2 (x7:Z) (x8:Z) (x9:Z) (x10:Z) (x11:Z) (x12:Z) := 0.
Definition P_id_LT (x7:Z) (x8:Z) := 1* x7.
Definition P_id_F_1 (x7:Z) (x8:Z) (x9:Z) (x10:Z) := 0.
Definition P_id_QSORT (x7:Z) := 0.
Definition P_id_APPEND (x7:Z) (x8:Z) := 0.
Lemma P_id_SPLIT_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_SPLIT x8 x10 <= P_id_SPLIT x7 x9.
Proof.
intros x10 x9 x8 x7.
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_F_3_monotonic :
forall x8 x12 x10 x9 x11 x7,
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_F_3 x8 x10 x12 <= P_id_F_3 x7 x9 x11.
Proof.
intros x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_F_2_monotonic :
forall x16 x8 x12 x18 x10 x14 x17 x9 x13 x11 x7 x15,
(0 <= x18)/\ (x18 <= x17) ->
(0 <= x16)/\ (x16 <= x15) ->
(0 <= x14)/\ (x14 <= x13) ->
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->
P_id_F_2 x8 x10 x12 x14 x16 x18 <= P_id_F_2 x7 x9 x11 x13 x15 x17.
Proof.
intros x18 x17 x16 x15 x14 x13 x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
intros [H_7 H_6].
intros [H_9 H_8].
intros [H_11 H_10].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_LT_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_LT x8 x10 <= P_id_LT x7 x9.
Proof.
intros x10 x9 x8 x7.
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_F_1_monotonic :
forall x8 x12 x10 x14 x9 x13 x11 x7,
(0 <= x14)/\ (x14 <= x13) ->
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->
P_id_F_1 x8 x10 x12 x14 <= P_id_F_1 x7 x9 x11 x13.
Proof.
intros x14 x13 x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
intros [H_7 H_6].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_QSORT_monotonic :
forall x8 x7, (0 <= x8)/\ (x8 <= x7) ->P_id_QSORT x8 <= P_id_QSORT x7.
Proof.
intros x8 x7.
intros [H_1 H_0].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_APPEND_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_APPEND x8 x10 <= P_id_APPEND x7 x9.
Proof.
intros x10 x9 x8 x7.
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_lt P_id_split P_id_false P_id_qsort
P_id_s P_id_f_1 P_id_nil P_id_0 P_id_pair P_id_append P_id_f_3
P_id_true P_id_f_2 P_id_add P_id_SPLIT P_id_F_3 P_id_F_2 P_id_LT
P_id_F_1 P_id_QSORT P_id_APPEND.
Lemma marked_measure_equation :
forall t,
marked_measure t = match t with
| (algebra.Alg.Term algebra.F.id_split (x8::
x7::nil)) =>
P_id_SPLIT (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_3 (x9::x8::
x7::nil)) =>
P_id_F_3 (measure x9) (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_2 (x12::x11::
x10::x9::x8::x7::nil)) =>
P_id_F_2 (measure x12) (measure x11)
(measure x10) (measure x9) (measure x8)
(measure x7)
| (algebra.Alg.Term algebra.F.id_lt (x8::x7::nil)) =>
P_id_LT (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_1 (x10::x9::x8::
x7::nil)) =>
P_id_F_1 (measure x10) (measure x9) (measure x8)
(measure x7)
| (algebra.Alg.Term algebra.F.id_qsort (x7::nil)) =>
P_id_QSORT (measure x7)
| (algebra.Alg.Term algebra.F.id_append (x8::
x7::nil)) =>
P_id_APPEND (measure x8) (measure x7)
| _ => 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_lt_monotonic;assumption.
intros ;apply P_id_split_monotonic;assumption.
intros ;apply P_id_qsort_monotonic;assumption.
intros ;apply P_id_s_monotonic;assumption.
intros ;apply P_id_f_1_monotonic;assumption.
intros ;apply P_id_pair_monotonic;assumption.
intros ;apply P_id_append_monotonic;assumption.
intros ;apply P_id_f_3_monotonic;assumption.
intros ;apply P_id_f_2_monotonic;assumption.
intros ;apply P_id_add_monotonic;assumption.
intros ;apply P_id_lt_bounded;assumption.
intros ;apply P_id_split_bounded;assumption.
intros ;apply P_id_false_bounded;assumption.
intros ;apply P_id_qsort_bounded;assumption.
intros ;apply P_id_s_bounded;assumption.
intros ;apply P_id_f_1_bounded;assumption.
intros ;apply P_id_nil_bounded;assumption.
intros ;apply P_id_0_bounded;assumption.
intros ;apply P_id_pair_bounded;assumption.
intros ;apply P_id_append_bounded;assumption.
intros ;apply P_id_f_3_bounded;assumption.
intros ;apply P_id_true_bounded;assumption.
intros ;apply P_id_f_2_bounded;assumption.
intros ;apply P_id_add_bounded;assumption.
apply rules_monotonic.
intros ;apply P_id_SPLIT_monotonic;assumption.
intros ;apply P_id_F_3_monotonic;assumption.
intros ;apply P_id_F_2_monotonic;assumption.
intros ;apply P_id_LT_monotonic;assumption.
intros ;apply P_id_F_1_monotonic;assumption.
intros ;apply P_id_QSORT_monotonic;assumption.
intros ;apply P_id_APPEND_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_4.
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_4.
Definition wf_DP_R_xml_0_scc_4 := WF_DP_R_xml_0_scc_4.wf.
Lemma acc_DP_R_xml_0_scc_4 :
forall x y, (DP_R_xml_0_scc_4 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_4).
intros x' _ Hrec y h.
inversion h;clear h;subst;
constructor;intros _y _h;inversion _h;clear _h;subst;
(eapply Hrec;econstructor eassumption)||
((R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 )||
(eapply Hrec;econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))).
apply wf_DP_R_xml_0_scc_4.
Qed.
Inductive DP_R_xml_0_non_scc_5 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <f_1(pair(X_,Z_),N_,M_,Y_),lt(N_,M_)> *)
| DP_R_xml_0_non_scc_5_0 :
forall x8 x4 x2 x10 x1 x9 x5 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_pair (x1::x5::nil)) x10) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x3 x9) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x4 x8) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x2 x7) ->
DP_R_xml_0_non_scc_5 (algebra.Alg.Term algebra.F.id_lt (x3::
x4::nil))
(algebra.Alg.Term algebra.F.id_f_1 (x10::x9::x8::x7::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;
(eapply acc_DP_R_xml_0_scc_4;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 )||
(eapply Hrec;econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))).
Qed.
Inductive DP_R_xml_0_non_scc_6 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <split(N_,add(M_,Y_)),f_1(split(N_,Y_),N_,M_,Y_)> *)
| DP_R_xml_0_non_scc_6_0 :
forall x8 x4 x2 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x3 x8) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_add (x4::x2::nil)) x7) ->
DP_R_xml_0_non_scc_6 (algebra.Alg.Term algebra.F.id_f_1
((algebra.Alg.Term algebra.F.id_split (x3::
x2::nil))::x3::x4::x2::nil))
(algebra.Alg.Term algebra.F.id_split (x8::x7::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;
(eapply acc_DP_R_xml_0_non_scc_5;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_1;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 )||
(eapply Hrec;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' )))).
Qed.
Inductive DP_R_xml_0_scc_7 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <split(N_,add(M_,Y_)),split(N_,Y_)> *)
| DP_R_xml_0_scc_7_0 :
forall x8 x4 x2 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x3 x8) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_add (x4::x2::nil)) x7) ->
DP_R_xml_0_scc_7 (algebra.Alg.Term algebra.F.id_split (x3::x2::nil))
(algebra.Alg.Term algebra.F.id_split (x8::x7::nil))
.
Module WF_DP_R_xml_0_scc_7.
Open Scope Z_scope.
Import ring_extention.
Notation Local "a <= b" := (Zle a b).
Notation Local "a < b" := (Zlt a b).
Definition P_id_lt (x7:Z) (x8:Z) := 2.
Definition P_id_split (x7:Z) (x8:Z) := 1* x8.
Definition P_id_false := 2.
Definition P_id_qsort (x7:Z) := 1* x7.
Definition P_id_s (x7:Z) := 0.
Definition P_id_f_1 (x7:Z) (x8:Z) (x9:Z) (x10:Z) := 2 + 1* x7.
Definition P_id_nil := 0.
Definition P_id_0 := 0.
Definition P_id_pair (x7:Z) (x8:Z) := 1* x7 + 1* x8.
Definition P_id_append (x7:Z) (x8:Z) := 1* x7 + 1* x8.
Definition P_id_f_3 (x7:Z) (x8:Z) (x9:Z) := 2 + 1* x7.
Definition P_id_true := 2.
Definition P_id_f_2 (x7:Z) (x8:Z) (x9:Z) (x10:Z) (x11:Z) (x12:Z) :=
1* x7 + 1* x11 + 1* x12.
Definition P_id_add (x7:Z) (x8:Z) := 2 + 1* x8.
Lemma P_id_lt_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_lt x8 x10 <= P_id_lt x7 x9.
Proof.
intros x10 x9 x8 x7.
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_split_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_split x8 x10 <= P_id_split x7 x9.
Proof.
intros x10 x9 x8 x7.
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_qsort_monotonic :
forall x8 x7, (0 <= x8)/\ (x8 <= x7) ->P_id_qsort x8 <= P_id_qsort x7.
Proof.
intros x8 x7.
intros [H_1 H_0].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_s_monotonic :
forall x8 x7, (0 <= x8)/\ (x8 <= x7) ->P_id_s x8 <= P_id_s x7.
Proof.
intros x8 x7.
intros [H_1 H_0].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_f_1_monotonic :
forall x8 x12 x10 x14 x9 x13 x11 x7,
(0 <= x14)/\ (x14 <= x13) ->
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->
P_id_f_1 x8 x10 x12 x14 <= P_id_f_1 x7 x9 x11 x13.
Proof.
intros x14 x13 x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
intros [H_7 H_6].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_pair_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_pair x8 x10 <= P_id_pair x7 x9.
Proof.
intros x10 x9 x8 x7.
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_append_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_append x8 x10 <= P_id_append x7 x9.
Proof.
intros x10 x9 x8 x7.
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_f_3_monotonic :
forall x8 x12 x10 x9 x11 x7,
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_f_3 x8 x10 x12 <= P_id_f_3 x7 x9 x11.
Proof.
intros x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_f_2_monotonic :
forall x16 x8 x12 x18 x10 x14 x17 x9 x13 x11 x7 x15,
(0 <= x18)/\ (x18 <= x17) ->
(0 <= x16)/\ (x16 <= x15) ->
(0 <= x14)/\ (x14 <= x13) ->
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->
P_id_f_2 x8 x10 x12 x14 x16 x18 <= P_id_f_2 x7 x9 x11 x13 x15 x17.
Proof.
intros x18 x17 x16 x15 x14 x13 x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
intros [H_7 H_6].
intros [H_9 H_8].
intros [H_11 H_10].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_add_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_add x8 x10 <= P_id_add x7 x9.
Proof.
intros x10 x9 x8 x7.
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_lt_bounded :
forall x8 x7, (0 <= x7) ->(0 <= x8) ->0 <= P_id_lt x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_split_bounded :
forall x8 x7, (0 <= x7) ->(0 <= x8) ->0 <= P_id_split x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_false_bounded : 0 <= P_id_false .
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_qsort_bounded : forall x7, (0 <= x7) ->0 <= P_id_qsort x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_s_bounded : forall x7, (0 <= x7) ->0 <= P_id_s x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_f_1_bounded :
forall x8 x10 x9 x7,
(0 <= x7) ->
(0 <= x8) ->(0 <= x9) ->(0 <= x10) ->0 <= P_id_f_1 x10 x9 x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_nil_bounded : 0 <= P_id_nil .
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_pair_bounded :
forall x8 x7, (0 <= x7) ->(0 <= x8) ->0 <= P_id_pair x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_append_bounded :
forall x8 x7, (0 <= x7) ->(0 <= x8) ->0 <= P_id_append x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_f_3_bounded :
forall x8 x9 x7,
(0 <= x7) ->(0 <= x8) ->(0 <= x9) ->0 <= P_id_f_3 x9 x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_true_bounded : 0 <= P_id_true .
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_f_2_bounded :
forall x8 x12 x10 x9 x11 x7,
(0 <= x7) ->
(0 <= x8) ->
(0 <= x9) ->
(0 <= x10) ->
(0 <= x11) ->(0 <= x12) ->0 <= P_id_f_2 x12 x11 x10 x9 x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_add_bounded :
forall x8 x7, (0 <= x7) ->(0 <= x8) ->0 <= P_id_add x8 x7.
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_lt P_id_split P_id_false P_id_qsort P_id_s
P_id_f_1 P_id_nil P_id_0 P_id_pair P_id_append P_id_f_3 P_id_true
P_id_f_2 P_id_add.
Lemma measure_equation :
forall t,
measure t = match t with
| (algebra.Alg.Term algebra.F.id_lt (x8::x7::nil)) =>
P_id_lt (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_split (x8::x7::nil)) =>
P_id_split (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_false nil) => P_id_false
| (algebra.Alg.Term algebra.F.id_qsort (x7::nil)) =>
P_id_qsort (measure x7)
| (algebra.Alg.Term algebra.F.id_s (x7::nil)) =>
P_id_s (measure x7)
| (algebra.Alg.Term algebra.F.id_f_1 (x10::x9::x8::
x7::nil)) =>
P_id_f_1 (measure x10) (measure x9) (measure x8)
(measure x7)
| (algebra.Alg.Term algebra.F.id_nil nil) => P_id_nil
| (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0
| (algebra.Alg.Term algebra.F.id_pair (x8::x7::nil)) =>
P_id_pair (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_append (x8::x7::nil)) =>
P_id_append (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_3 (x9::x8::x7::nil)) =>
P_id_f_3 (measure x9) (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_true nil) => P_id_true
| (algebra.Alg.Term algebra.F.id_f_2 (x12::x11::x10::x9::
x8::x7::nil)) =>
P_id_f_2 (measure x12) (measure x11) (measure x10)
(measure x9) (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_add (x8::x7::nil)) =>
P_id_add (measure x8) (measure x7)
| _ => 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_lt_monotonic;assumption.
intros ;apply P_id_split_monotonic;assumption.
intros ;apply P_id_qsort_monotonic;assumption.
intros ;apply P_id_s_monotonic;assumption.
intros ;apply P_id_f_1_monotonic;assumption.
intros ;apply P_id_pair_monotonic;assumption.
intros ;apply P_id_append_monotonic;assumption.
intros ;apply P_id_f_3_monotonic;assumption.
intros ;apply P_id_f_2_monotonic;assumption.
intros ;apply P_id_add_monotonic;assumption.
intros ;apply P_id_lt_bounded;assumption.
intros ;apply P_id_split_bounded;assumption.
intros ;apply P_id_false_bounded;assumption.
intros ;apply P_id_qsort_bounded;assumption.
intros ;apply P_id_s_bounded;assumption.
intros ;apply P_id_f_1_bounded;assumption.
intros ;apply P_id_nil_bounded;assumption.
intros ;apply P_id_0_bounded;assumption.
intros ;apply P_id_pair_bounded;assumption.
intros ;apply P_id_append_bounded;assumption.
intros ;apply P_id_f_3_bounded;assumption.
intros ;apply P_id_true_bounded;assumption.
intros ;apply P_id_f_2_bounded;assumption.
intros ;apply P_id_add_bounded;assumption.
apply rules_monotonic.
Qed.
Definition P_id_SPLIT (x7:Z) (x8:Z) := 1* x8.
Definition P_id_F_3 (x7:Z) (x8:Z) (x9:Z) := 0.
Definition P_id_F_2 (x7:Z) (x8:Z) (x9:Z) (x10:Z) (x11:Z) (x12:Z) := 0.
Definition P_id_LT (x7:Z) (x8:Z) := 0.
Definition P_id_F_1 (x7:Z) (x8:Z) (x9:Z) (x10:Z) := 0.
Definition P_id_QSORT (x7:Z) := 0.
Definition P_id_APPEND (x7:Z) (x8:Z) := 0.
Lemma P_id_SPLIT_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_SPLIT x8 x10 <= P_id_SPLIT x7 x9.
Proof.
intros x10 x9 x8 x7.
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_F_3_monotonic :
forall x8 x12 x10 x9 x11 x7,
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_F_3 x8 x10 x12 <= P_id_F_3 x7 x9 x11.
Proof.
intros x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_F_2_monotonic :
forall x16 x8 x12 x18 x10 x14 x17 x9 x13 x11 x7 x15,
(0 <= x18)/\ (x18 <= x17) ->
(0 <= x16)/\ (x16 <= x15) ->
(0 <= x14)/\ (x14 <= x13) ->
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->
P_id_F_2 x8 x10 x12 x14 x16 x18 <= P_id_F_2 x7 x9 x11 x13 x15 x17.
Proof.
intros x18 x17 x16 x15 x14 x13 x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
intros [H_7 H_6].
intros [H_9 H_8].
intros [H_11 H_10].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_LT_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_LT x8 x10 <= P_id_LT x7 x9.
Proof.
intros x10 x9 x8 x7.
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_F_1_monotonic :
forall x8 x12 x10 x14 x9 x13 x11 x7,
(0 <= x14)/\ (x14 <= x13) ->
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->
P_id_F_1 x8 x10 x12 x14 <= P_id_F_1 x7 x9 x11 x13.
Proof.
intros x14 x13 x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
intros [H_7 H_6].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_QSORT_monotonic :
forall x8 x7, (0 <= x8)/\ (x8 <= x7) ->P_id_QSORT x8 <= P_id_QSORT x7.
Proof.
intros x8 x7.
intros [H_1 H_0].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_APPEND_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_APPEND x8 x10 <= P_id_APPEND x7 x9.
Proof.
intros x10 x9 x8 x7.
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_lt P_id_split P_id_false P_id_qsort
P_id_s P_id_f_1 P_id_nil P_id_0 P_id_pair P_id_append P_id_f_3
P_id_true P_id_f_2 P_id_add P_id_SPLIT P_id_F_3 P_id_F_2 P_id_LT
P_id_F_1 P_id_QSORT P_id_APPEND.
Lemma marked_measure_equation :
forall t,
marked_measure t = match t with
| (algebra.Alg.Term algebra.F.id_split (x8::
x7::nil)) =>
P_id_SPLIT (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_3 (x9::x8::
x7::nil)) =>
P_id_F_3 (measure x9) (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_2 (x12::x11::
x10::x9::x8::x7::nil)) =>
P_id_F_2 (measure x12) (measure x11)
(measure x10) (measure x9) (measure x8)
(measure x7)
| (algebra.Alg.Term algebra.F.id_lt (x8::x7::nil)) =>
P_id_LT (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_1 (x10::x9::x8::
x7::nil)) =>
P_id_F_1 (measure x10) (measure x9) (measure x8)
(measure x7)
| (algebra.Alg.Term algebra.F.id_qsort (x7::nil)) =>
P_id_QSORT (measure x7)
| (algebra.Alg.Term algebra.F.id_append (x8::
x7::nil)) =>
P_id_APPEND (measure x8) (measure x7)
| _ => 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_lt_monotonic;assumption.
intros ;apply P_id_split_monotonic;assumption.
intros ;apply P_id_qsort_monotonic;assumption.
intros ;apply P_id_s_monotonic;assumption.
intros ;apply P_id_f_1_monotonic;assumption.
intros ;apply P_id_pair_monotonic;assumption.
intros ;apply P_id_append_monotonic;assumption.
intros ;apply P_id_f_3_monotonic;assumption.
intros ;apply P_id_f_2_monotonic;assumption.
intros ;apply P_id_add_monotonic;assumption.
intros ;apply P_id_lt_bounded;assumption.
intros ;apply P_id_split_bounded;assumption.
intros ;apply P_id_false_bounded;assumption.
intros ;apply P_id_qsort_bounded;assumption.
intros ;apply P_id_s_bounded;assumption.
intros ;apply P_id_f_1_bounded;assumption.
intros ;apply P_id_nil_bounded;assumption.
intros ;apply P_id_0_bounded;assumption.
intros ;apply P_id_pair_bounded;assumption.
intros ;apply P_id_append_bounded;assumption.
intros ;apply P_id_f_3_bounded;assumption.
intros ;apply P_id_true_bounded;assumption.
intros ;apply P_id_f_2_bounded;assumption.
intros ;apply P_id_add_bounded;assumption.
apply rules_monotonic.
intros ;apply P_id_SPLIT_monotonic;assumption.
intros ;apply P_id_F_3_monotonic;assumption.
intros ;apply P_id_F_2_monotonic;assumption.
intros ;apply P_id_LT_monotonic;assumption.
intros ;apply P_id_F_1_monotonic;assumption.
intros ;apply P_id_QSORT_monotonic;assumption.
intros ;apply P_id_APPEND_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_7.
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_7.
Definition wf_DP_R_xml_0_scc_7 := WF_DP_R_xml_0_scc_7.wf.
Lemma acc_DP_R_xml_0_scc_7 :
forall x y, (DP_R_xml_0_scc_7 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_7).
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_6;
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_7.
Qed.
Inductive DP_R_xml_0_non_scc_8 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <qsort(add(N_,X_)),split(N_,X_)> *)
| DP_R_xml_0_non_scc_8_0 :
forall x1 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_add (x3::x1::nil)) x7) ->
DP_R_xml_0_non_scc_8 (algebra.Alg.Term algebra.F.id_split (x3::
x1::nil))
(algebra.Alg.Term algebra.F.id_qsort (x7::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;
(eapply acc_DP_R_xml_0_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' ))||
((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_9 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <qsort(add(N_,X_)),f_3(split(N_,X_),N_,X_)> *)
| DP_R_xml_0_scc_9_0 :
forall x1 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_add (x3::x1::nil)) x7) ->
DP_R_xml_0_scc_9 (algebra.Alg.Term algebra.F.id_f_3
((algebra.Alg.Term algebra.F.id_split (x3::
x1::nil))::x3::x1::nil))
(algebra.Alg.Term algebra.F.id_qsort (x7::nil))
(* <f_3(pair(Y_,Z_),N_,X_),qsort(Y_)> *)
| DP_R_xml_0_scc_9_1 :
forall x8 x2 x1 x9 x5 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_pair (x2::x5::nil)) x9) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x3 x8) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x1 x7) ->
DP_R_xml_0_scc_9 (algebra.Alg.Term algebra.F.id_qsort (x2::nil))
(algebra.Alg.Term algebra.F.id_f_3 (x9::x8::x7::nil))
(* <f_3(pair(Y_,Z_),N_,X_),qsort(Z_)> *)
| DP_R_xml_0_scc_9_2 :
forall x8 x2 x1 x9 x5 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_pair (x2::x5::nil)) x9) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x3 x8) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x1 x7) ->
DP_R_xml_0_scc_9 (algebra.Alg.Term algebra.F.id_qsort (x5::nil))
(algebra.Alg.Term algebra.F.id_f_3 (x9::x8::x7::nil))
.
Module WF_DP_R_xml_0_scc_9.
Inductive DP_R_xml_0_scc_9_large :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <qsort(add(N_,X_)),f_3(split(N_,X_),N_,X_)> *)
| DP_R_xml_0_scc_9_large_0 :
forall x1 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_add (x3::x1::nil)) x7) ->
DP_R_xml_0_scc_9_large (algebra.Alg.Term algebra.F.id_f_3
((algebra.Alg.Term algebra.F.id_split (x3::
x1::nil))::x3::x1::nil))
(algebra.Alg.Term algebra.F.id_qsort (x7::nil))
.
Inductive DP_R_xml_0_scc_9_strict :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <f_3(pair(Y_,Z_),N_,X_),qsort(Y_)> *)
| DP_R_xml_0_scc_9_strict_0 :
forall x8 x2 x1 x9 x5 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_pair (x2::x5::nil)) x9) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x3 x8) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x1 x7) ->
DP_R_xml_0_scc_9_strict (algebra.Alg.Term algebra.F.id_qsort
(x2::nil))
(algebra.Alg.Term algebra.F.id_f_3 (x9::x8::x7::nil))
(* <f_3(pair(Y_,Z_),N_,X_),qsort(Z_)> *)
| DP_R_xml_0_scc_9_strict_1 :
forall x8 x2 x1 x9 x5 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_pair (x2::x5::nil)) x9) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x3 x8) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
x1 x7) ->
DP_R_xml_0_scc_9_strict (algebra.Alg.Term algebra.F.id_qsort
(x5::nil))
(algebra.Alg.Term algebra.F.id_f_3 (x9::x8::x7::nil))
.
Module WF_DP_R_xml_0_scc_9_large.
Inductive DP_R_xml_0_scc_9_large_non_scc_1 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <qsort(add(N_,X_)),f_3(split(N_,X_),N_,X_)> *)
| DP_R_xml_0_scc_9_large_non_scc_1_0 :
forall x1 x3 x7,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_add (x3::x1::nil)) x7) ->
DP_R_xml_0_scc_9_large_non_scc_1 (algebra.Alg.Term algebra.F.id_f_3
((algebra.Alg.Term
algebra.F.id_split (x3::
x1::nil))::x3::x1::nil))
(algebra.Alg.Term algebra.F.id_qsort (x7::nil))
.
Lemma acc_DP_R_xml_0_scc_9_large_non_scc_1 :
forall x y,
(DP_R_xml_0_scc_9_large_non_scc_1 x y) ->
Acc WF_DP_R_xml_0_scc_9.DP_R_xml_0_scc_9_large x.
Proof.
intros x y h.
inversion h;clear h;subst;
constructor;intros _y _h;inversion _h;clear _h;subst;
(R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 )||
(eapply Hrec;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' )).
Qed.
Lemma wf : well_founded WF_DP_R_xml_0_scc_9.DP_R_xml_0_scc_9_large.
Proof.
constructor;intros _y _h;inversion _h;clear _h;subst;
(eapply acc_DP_R_xml_0_scc_9_large_non_scc_1;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_scc_9_large_non_scc_0;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 )||(fail))).
Qed.
End WF_DP_R_xml_0_scc_9_large.
Open Scope Z_scope.
Import ring_extention.
Notation Local "a <= b" := (Zle a b).
Notation Local "a < b" := (Zlt a b).
Definition P_id_lt (x7:Z) (x8:Z) := 0.
Definition P_id_split (x7:Z) (x8:Z) := 1* x8.
Definition P_id_false := 0.
Definition P_id_qsort (x7:Z) := 2* x7.
Definition P_id_s (x7:Z) := 0.
Definition P_id_f_1 (x7:Z) (x8:Z) (x9:Z) (x10:Z) := 1 + 1* x7.
Definition P_id_nil := 0.
Definition P_id_0 := 0.
Definition P_id_pair (x7:Z) (x8:Z) := 1* x7 + 1* x8.
Definition P_id_append (x7:Z) (x8:Z) := 1* x7 + 1* x8.
Definition P_id_f_3 (x7:Z) (x8:Z) (x9:Z) := 1 + 2* x7.
Definition P_id_true := 0.
Definition P_id_f_2 (x7:Z) (x8:Z) (x9:Z) (x10:Z) (x11:Z) (x12:Z) :=
1 + 1* x11 + 1* x12.
Definition P_id_add (x7:Z) (x8:Z) := 1 + 1* x8.
Lemma P_id_lt_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_lt x8 x10 <= P_id_lt x7 x9.
Proof.
intros x10 x9 x8 x7.
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_split_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_split x8 x10 <= P_id_split x7 x9.
Proof.
intros x10 x9 x8 x7.
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_qsort_monotonic :
forall x8 x7, (0 <= x8)/\ (x8 <= x7) ->P_id_qsort x8 <= P_id_qsort x7.
Proof.
intros x8 x7.
intros [H_1 H_0].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_s_monotonic :
forall x8 x7, (0 <= x8)/\ (x8 <= x7) ->P_id_s x8 <= P_id_s x7.
Proof.
intros x8 x7.
intros [H_1 H_0].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_f_1_monotonic :
forall x8 x12 x10 x14 x9 x13 x11 x7,
(0 <= x14)/\ (x14 <= x13) ->
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->
P_id_f_1 x8 x10 x12 x14 <= P_id_f_1 x7 x9 x11 x13.
Proof.
intros x14 x13 x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
intros [H_7 H_6].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_pair_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_pair x8 x10 <= P_id_pair x7 x9.
Proof.
intros x10 x9 x8 x7.
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_append_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_append x8 x10 <= P_id_append x7 x9.
Proof.
intros x10 x9 x8 x7.
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_f_3_monotonic :
forall x8 x12 x10 x9 x11 x7,
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_f_3 x8 x10 x12 <= P_id_f_3 x7 x9 x11.
Proof.
intros x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_f_2_monotonic :
forall x16 x8 x12 x18 x10 x14 x17 x9 x13 x11 x7 x15,
(0 <= x18)/\ (x18 <= x17) ->
(0 <= x16)/\ (x16 <= x15) ->
(0 <= x14)/\ (x14 <= x13) ->
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->
P_id_f_2 x8 x10 x12 x14 x16 x18 <= P_id_f_2 x7 x9 x11 x13 x15 x17.
Proof.
intros x18 x17 x16 x15 x14 x13 x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
intros [H_7 H_6].
intros [H_9 H_8].
intros [H_11 H_10].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_add_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_add x8 x10 <= P_id_add x7 x9.
Proof.
intros x10 x9 x8 x7.
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_lt_bounded :
forall x8 x7, (0 <= x7) ->(0 <= x8) ->0 <= P_id_lt x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_split_bounded :
forall x8 x7, (0 <= x7) ->(0 <= x8) ->0 <= P_id_split x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_false_bounded : 0 <= P_id_false .
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_qsort_bounded : forall x7, (0 <= x7) ->0 <= P_id_qsort x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_s_bounded : forall x7, (0 <= x7) ->0 <= P_id_s x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_f_1_bounded :
forall x8 x10 x9 x7,
(0 <= x7) ->
(0 <= x8) ->(0 <= x9) ->(0 <= x10) ->0 <= P_id_f_1 x10 x9 x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_nil_bounded : 0 <= P_id_nil .
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_pair_bounded :
forall x8 x7, (0 <= x7) ->(0 <= x8) ->0 <= P_id_pair x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_append_bounded :
forall x8 x7, (0 <= x7) ->(0 <= x8) ->0 <= P_id_append x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_f_3_bounded :
forall x8 x9 x7,
(0 <= x7) ->(0 <= x8) ->(0 <= x9) ->0 <= P_id_f_3 x9 x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_true_bounded : 0 <= P_id_true .
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_f_2_bounded :
forall x8 x12 x10 x9 x11 x7,
(0 <= x7) ->
(0 <= x8) ->
(0 <= x9) ->
(0 <= x10) ->
(0 <= x11) ->(0 <= x12) ->0 <= P_id_f_2 x12 x11 x10 x9 x8 x7.
Proof.
intros .
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_add_bounded :
forall x8 x7, (0 <= x7) ->(0 <= x8) ->0 <= P_id_add x8 x7.
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_lt P_id_split P_id_false P_id_qsort P_id_s
P_id_f_1 P_id_nil P_id_0 P_id_pair P_id_append P_id_f_3 P_id_true
P_id_f_2 P_id_add.
Lemma measure_equation :
forall t,
measure t = match t with
| (algebra.Alg.Term algebra.F.id_lt (x8::x7::nil)) =>
P_id_lt (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_split (x8::x7::nil)) =>
P_id_split (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_false nil) => P_id_false
| (algebra.Alg.Term algebra.F.id_qsort (x7::nil)) =>
P_id_qsort (measure x7)
| (algebra.Alg.Term algebra.F.id_s (x7::nil)) =>
P_id_s (measure x7)
| (algebra.Alg.Term algebra.F.id_f_1 (x10::x9::x8::
x7::nil)) =>
P_id_f_1 (measure x10) (measure x9) (measure x8)
(measure x7)
| (algebra.Alg.Term algebra.F.id_nil nil) => P_id_nil
| (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0
| (algebra.Alg.Term algebra.F.id_pair (x8::x7::nil)) =>
P_id_pair (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_append (x8::x7::nil)) =>
P_id_append (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_3 (x9::x8::x7::nil)) =>
P_id_f_3 (measure x9) (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_true nil) => P_id_true
| (algebra.Alg.Term algebra.F.id_f_2 (x12::x11::x10::x9::
x8::x7::nil)) =>
P_id_f_2 (measure x12) (measure x11) (measure x10)
(measure x9) (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_add (x8::x7::nil)) =>
P_id_add (measure x8) (measure x7)
| _ => 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_lt_monotonic;assumption.
intros ;apply P_id_split_monotonic;assumption.
intros ;apply P_id_qsort_monotonic;assumption.
intros ;apply P_id_s_monotonic;assumption.
intros ;apply P_id_f_1_monotonic;assumption.
intros ;apply P_id_pair_monotonic;assumption.
intros ;apply P_id_append_monotonic;assumption.
intros ;apply P_id_f_3_monotonic;assumption.
intros ;apply P_id_f_2_monotonic;assumption.
intros ;apply P_id_add_monotonic;assumption.
intros ;apply P_id_lt_bounded;assumption.
intros ;apply P_id_split_bounded;assumption.
intros ;apply P_id_false_bounded;assumption.
intros ;apply P_id_qsort_bounded;assumption.
intros ;apply P_id_s_bounded;assumption.
intros ;apply P_id_f_1_bounded;assumption.
intros ;apply P_id_nil_bounded;assumption.
intros ;apply P_id_0_bounded;assumption.
intros ;apply P_id_pair_bounded;assumption.
intros ;apply P_id_append_bounded;assumption.
intros ;apply P_id_f_3_bounded;assumption.
intros ;apply P_id_true_bounded;assumption.
intros ;apply P_id_f_2_bounded;assumption.
intros ;apply P_id_add_bounded;assumption.
apply rules_monotonic.
Qed.
Definition P_id_SPLIT (x7:Z) (x8:Z) := 0.
Definition P_id_F_3 (x7:Z) (x8:Z) (x9:Z) := 2 + 2* x7.
Definition P_id_F_2 (x7:Z) (x8:Z) (x9:Z) (x10:Z) (x11:Z) (x12:Z) := 0.
Definition P_id_LT (x7:Z) (x8:Z) := 0.
Definition P_id_F_1 (x7:Z) (x8:Z) (x9:Z) (x10:Z) := 0.
Definition P_id_QSORT (x7:Z) := 2* x7.
Definition P_id_APPEND (x7:Z) (x8:Z) := 0.
Lemma P_id_SPLIT_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_SPLIT x8 x10 <= P_id_SPLIT x7 x9.
Proof.
intros x10 x9 x8 x7.
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_F_3_monotonic :
forall x8 x12 x10 x9 x11 x7,
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_F_3 x8 x10 x12 <= P_id_F_3 x7 x9 x11.
Proof.
intros x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_F_2_monotonic :
forall x16 x8 x12 x18 x10 x14 x17 x9 x13 x11 x7 x15,
(0 <= x18)/\ (x18 <= x17) ->
(0 <= x16)/\ (x16 <= x15) ->
(0 <= x14)/\ (x14 <= x13) ->
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->
P_id_F_2 x8 x10 x12 x14 x16 x18 <= P_id_F_2 x7 x9 x11 x13 x15 x17.
Proof.
intros x18 x17 x16 x15 x14 x13 x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
intros [H_7 H_6].
intros [H_9 H_8].
intros [H_11 H_10].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_LT_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_LT x8 x10 <= P_id_LT x7 x9.
Proof.
intros x10 x9 x8 x7.
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_F_1_monotonic :
forall x8 x12 x10 x14 x9 x13 x11 x7,
(0 <= x14)/\ (x14 <= x13) ->
(0 <= x12)/\ (x12 <= x11) ->
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->
P_id_F_1 x8 x10 x12 x14 <= P_id_F_1 x7 x9 x11 x13.
Proof.
intros x14 x13 x12 x11 x10 x9 x8 x7.
intros [H_1 H_0].
intros [H_3 H_2].
intros [H_5 H_4].
intros [H_7 H_6].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_QSORT_monotonic :
forall x8 x7, (0 <= x8)/\ (x8 <= x7) ->P_id_QSORT x8 <= P_id_QSORT x7.
Proof.
intros x8 x7.
intros [H_1 H_0].
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma P_id_APPEND_monotonic :
forall x8 x10 x9 x7,
(0 <= x10)/\ (x10 <= x9) ->
(0 <= x8)/\ (x8 <= x7) ->P_id_APPEND x8 x10 <= P_id_APPEND x7 x9.
Proof.
intros x10 x9 x8 x7.
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_lt P_id_split P_id_false P_id_qsort
P_id_s P_id_f_1 P_id_nil P_id_0 P_id_pair P_id_append P_id_f_3
P_id_true P_id_f_2 P_id_add P_id_SPLIT P_id_F_3 P_id_F_2 P_id_LT
P_id_F_1 P_id_QSORT P_id_APPEND.
Lemma marked_measure_equation :
forall t,
marked_measure t = match t with
| (algebra.Alg.Term algebra.F.id_split (x8::
x7::nil)) =>
P_id_SPLIT (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_3 (x9::x8::
x7::nil)) =>
P_id_F_3 (measure x9) (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_2 (x12::x11::
x10::x9::x8::x7::nil)) =>
P_id_F_2 (measure x12) (measure x11)
(measure x10) (measure x9) (measure x8)
(measure x7)
| (algebra.Alg.Term algebra.F.id_lt (x8::x7::nil)) =>
P_id_LT (measure x8) (measure x7)
| (algebra.Alg.Term algebra.F.id_f_1 (x10::x9::x8::
x7::nil)) =>
P_id_F_1 (measure x10) (measure x9) (measure x8)
(measure x7)
| (algebra.Alg.Term algebra.F.id_qsort (x7::nil)) =>
P_id_QSORT (measure x7)
| (algebra.Alg.Term algebra.F.id_append (x8::
x7::nil)) =>
P_id_APPEND (measure x8) (measure x7)
| _ => 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_lt_monotonic;assumption.
intros ;apply P_id_split_monotonic;assumption.
intros ;apply P_id_qsort_monotonic;assumption.
intros ;apply P_id_s_monotonic;assumption.
intros ;apply P_id_f_1_monotonic;assumption.
intros ;apply P_id_pair_monotonic;assumption.
intros ;apply P_id_append_monotonic;assumption.
intros ;apply P_id_f_3_monotonic;assumption.
intros ;apply P_id_f_2_monotonic;assumption.
intros ;apply P_id_add_monotonic;assumption.
intros ;apply P_id_lt_bounded;assumption.
intros ;apply P_id_split_bounded;assumption.
intros ;apply P_id_false_bounded;assumption.
intros ;apply P_id_qsort_bounded;assumption.
intros ;apply P_id_s_bounded;assumption.
intros ;apply P_id_f_1_bounded;assumption.
intros ;apply P_id_nil_bounded;assumption.
intros ;apply P_id_0_bounded;assumption.
intros ;apply P_id_pair_bounded;assumption.
intros ;apply P_id_append_bounded;assumption.
intros ;apply P_id_f_3_bounded;assumption.
intros ;apply P_id_true_bounded;assumption.
intros ;apply P_id_f_2_bounded;assumption.
intros ;apply P_id_add_bounded;assumption.
apply rules_monotonic.
intros ;apply P_id_SPLIT_monotonic;assumption.
intros ;apply P_id_F_3_monotonic;assumption.
intros ;apply P_id_F_2_monotonic;assumption.
intros ;apply P_id_LT_monotonic;assumption.
intros ;apply P_id_F_1_monotonic;assumption.
intros ;apply P_id_QSORT_monotonic;assumption.
intros ;apply P_id_APPEND_monotonic;assumption.
Qed.
Ltac rewrite_and_unfold :=
do 2 (rewrite marked_measure_equation);
repeat (
match goal with
| |- context [measure (algebra.Alg.Term ?f ?t)] =>
rewrite (measure_equation (algebra.Alg.Term f t))
| H:context [measure (algebra.Alg.Term ?f ?t)] |- _ =>
rewrite (measure_equation (algebra.Alg.Term f t)) in H|-
end
).
Definition lt a b := (Zwf.Zwf 0) (marked_measure a) (marked_measure b).
Definition le a b := marked_measure a <= marked_measure b.
Lemma lt_le_compat : forall a b c, (lt a b) ->(le b c) ->lt a c.
Proof.
unfold lt, le in *.
intros a b c.
apply (interp.le_lt_compat_right (interp.o_Z 0)).
Qed.
Lemma wf_lt : well_founded lt.
Proof.
unfold lt in *.
apply Inverse_Image.wf_inverse_image with (B:=Z).
apply Zwf.Zwf_well_founded.
Qed.
Lemma DP_R_xml_0_scc_9_strict_in_lt :
Relation_Definitions.inclusion _ DP_R_xml_0_scc_9_strict lt.
Proof.
unfold Relation_Definitions.inclusion, lt in *.
intros a b H;destruct H;
match goal with
| |- (Zwf.Zwf 0) _ (marked_measure (algebra.Alg.Term ?f ?l)) =>
let l'' := algebra.Alg_ext.find_replacement l in
((apply (interp.le_lt_compat_right (interp.o_Z 0)) with
(marked_measure (algebra.Alg.Term f l''));[idtac|
apply marked_measure_star_monotonic;
repeat (apply algebra.EQT_ext.one_step_list_refl_trans_clos);
(assumption)||(constructor 1)]))
end
;clear ;rewrite_and_unfold ;repeat (generate_pos_hyp );
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Lemma DP_R_xml_0_scc_9_large_in_le :
Relation_Definitions.inclusion _ DP_R_xml_0_scc_9_large le.
Proof.
unfold Relation_Definitions.inclusion, le, Zwf.Zwf in *.
intros a b H;destruct H;
match goal with
| |- _ <= marked_measure (algebra.Alg.Term ?f ?l) =>
let l'' := algebra.Alg_ext.find_replacement l in
((apply (interp.le_trans (interp.o_Z 0)) with
(marked_measure (algebra.Alg.Term f l''));[idtac|
apply marked_measure_star_monotonic;
repeat (apply algebra.EQT_ext.one_step_list_refl_trans_clos);
(assumption)||(constructor 1)]))
end
;clear ;rewrite_and_unfold ;repeat (generate_pos_hyp );
cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
(auto with zarith)||(repeat (translate_vars );prove_ineq ).
Qed.
Definition wf_DP_R_xml_0_scc_9_large := WF_DP_R_xml_0_scc_9_large.wf.
Lemma wf : well_founded WF_DP_R_xml_0.DP_R_xml_0_scc_9.
Proof.
intros x.
apply (well_founded_ind wf_lt).
clear x.
intros x.
pattern x.
apply (@Acc_ind _ DP_R_xml_0_scc_9_large).
clear x.
intros x _ IHx IHx'.
constructor.
intros y H.
destruct H;
(apply IHx';apply DP_R_xml_0_scc_9_strict_in_lt;
econstructor eassumption)||
((apply IHx;[econstructor eassumption|
intros y' Hlt;apply IHx';apply lt_le_compat with (1:=Hlt) ;
apply DP_R_xml_0_scc_9_large_in_le;econstructor eassumption])).
apply wf_DP_R_xml_0_scc_9_large.
Qed.
End WF_DP_R_xml_0_scc_9.
Definition wf_DP_R_xml_0_scc_9 := WF_DP_R_xml_0_scc_9.wf.
Lemma acc_DP_R_xml_0_scc_9 :
forall x y, (DP_R_xml_0_scc_9 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_9).
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_8;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((eapply acc_DP_R_xml_0_non_scc_3;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))||
((R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 )||
(eapply Hrec;
econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))))).
apply wf_DP_R_xml_0_scc_9.
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_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_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___Rubio___enno.trs/a3pat.v" ***
*** End: ***
*)