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_f *)
| id_f : symb
(* id_if *)
| id_if : symb
(* id_b *)
| id_b : symb
(* id_h *)
| id_h : symb
(* id_i *)
| id_i : symb
(* id__dot_ *)
| id__dot_ : symb
(* id_c *)
| id_c : symb
(* id_g *)
| id_g : symb
(* id_e *)
| id_e : symb
(* id_b' *)
| id_b' : symb
(* id_a *)
| id_a : symb
(* id_d' *)
| id_d' : symb
(* id_d *)
| id_d : symb
.
Definition symb_eq_bool (f1 f2:symb) : bool :=
match f1,f2 with
| id_f,id_f => true
| id_if,id_if => true
| id_b,id_b => true
| id_h,id_h => true
| id_i,id_i => true
| id__dot_,id__dot_ => true
| id_c,id_c => true
| id_g,id_g => true
| id_e,id_e => true
| id_b',id_b' => true
| id_a,id_a => true
| id_d',id_d' => true
| id_d,id_d => 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_f,id_f => refl_equal _
| id_if,id_if => refl_equal _
| id_b,id_b => refl_equal _
| id_h,id_h => refl_equal _
| id_i,id_i => refl_equal _
| id__dot_,id__dot_ => refl_equal _
| id_c,id_c => refl_equal _
| id_g,id_g => refl_equal _
| id_e,id_e => refl_equal _
| id_b',id_b' => refl_equal _
| id_a,id_a => refl_equal _
| id_d',id_d' => refl_equal _
| id_d,id_d => refl_equal _
| _,_ => _
end;intros abs;discriminate.
Defined.
Definition arity (f:symb) :=
match f with
| id_f => term.Free 2
| id_if => term.Free 3
| id_b => term.Free 0
| id_h => term.Free 2
| id_i => term.Free 3
| id__dot_ => term.Free 2
| id_c => term.Free 0
| id_g => term.Free 2
| id_e => term.Free 0
| id_b' => term.Free 0
| id_a => term.Free 0
| id_d' => term.Free 0
| id_d => term.Free 0
end.
Definition symb_order (f1 f2:symb) : bool :=
match f1,f2 with
| id_f,id_f => true
| id_f,id_if => false
| id_f,id_b => false
| id_f,id_h => false
| id_f,id_i => false
| id_f,id__dot_ => false
| id_f,id_c => false
| id_f,id_g => false
| id_f,id_e => false
| id_f,id_b' => false
| id_f,id_a => false
| id_f,id_d' => false
| id_f,id_d => false
| id_if,id_f => true
| id_if,id_if => true
| id_if,id_b => false
| id_if,id_h => false
| id_if,id_i => false
| id_if,id__dot_ => false
| id_if,id_c => false
| id_if,id_g => false
| id_if,id_e => false
| id_if,id_b' => false
| id_if,id_a => false
| id_if,id_d' => false
| id_if,id_d => false
| id_b,id_f => true
| id_b,id_if => true
| id_b,id_b => true
| id_b,id_h => false
| id_b,id_i => false
| id_b,id__dot_ => false
| id_b,id_c => false
| id_b,id_g => false
| id_b,id_e => false
| id_b,id_b' => false
| id_b,id_a => false
| id_b,id_d' => false
| id_b,id_d => false
| id_h,id_f => true
| id_h,id_if => true
| id_h,id_b => true
| id_h,id_h => true
| id_h,id_i => false
| id_h,id__dot_ => false
| id_h,id_c => false
| id_h,id_g => false
| id_h,id_e => false
| id_h,id_b' => false
| id_h,id_a => false
| id_h,id_d' => false
| id_h,id_d => false
| id_i,id_f => true
| id_i,id_if => true
| id_i,id_b => true
| id_i,id_h => true
| id_i,id_i => true
| id_i,id__dot_ => false
| id_i,id_c => false
| id_i,id_g => false
| id_i,id_e => false
| id_i,id_b' => false
| id_i,id_a => false
| id_i,id_d' => false
| id_i,id_d => false
| id__dot_,id_f => true
| id__dot_,id_if => true
| id__dot_,id_b => true
| id__dot_,id_h => true
| id__dot_,id_i => true
| id__dot_,id__dot_ => true
| id__dot_,id_c => false
| id__dot_,id_g => false
| id__dot_,id_e => false
| id__dot_,id_b' => false
| id__dot_,id_a => false
| id__dot_,id_d' => false
| id__dot_,id_d => false
| id_c,id_f => true
| id_c,id_if => true
| id_c,id_b => true
| id_c,id_h => true
| id_c,id_i => true
| id_c,id__dot_ => true
| id_c,id_c => true
| id_c,id_g => false
| id_c,id_e => false
| id_c,id_b' => false
| id_c,id_a => false
| id_c,id_d' => false
| id_c,id_d => false
| id_g,id_f => true
| id_g,id_if => true
| id_g,id_b => true
| id_g,id_h => true
| id_g,id_i => true
| id_g,id__dot_ => true
| id_g,id_c => true
| id_g,id_g => true
| id_g,id_e => false
| id_g,id_b' => false
| id_g,id_a => false
| id_g,id_d' => false
| id_g,id_d => false
| id_e,id_f => true
| id_e,id_if => true
| id_e,id_b => true
| id_e,id_h => true
| id_e,id_i => true
| id_e,id__dot_ => true
| id_e,id_c => true
| id_e,id_g => true
| id_e,id_e => true
| id_e,id_b' => false
| id_e,id_a => false
| id_e,id_d' => false
| id_e,id_d => false
| id_b',id_f => true
| id_b',id_if => true
| id_b',id_b => true
| id_b',id_h => true
| id_b',id_i => true
| id_b',id__dot_ => true
| id_b',id_c => true
| id_b',id_g => true
| id_b',id_e => true
| id_b',id_b' => true
| id_b',id_a => false
| id_b',id_d' => false
| id_b',id_d => false
| id_a,id_f => true
| id_a,id_if => true
| id_a,id_b => true
| id_a,id_h => true
| id_a,id_i => true
| id_a,id__dot_ => true
| id_a,id_c => true
| id_a,id_g => true
| id_a,id_e => true
| id_a,id_b' => true
| id_a,id_a => true
| id_a,id_d' => false
| id_a,id_d => false
| id_d',id_f => true
| id_d',id_if => true
| id_d',id_b => true
| id_d',id_h => true
| id_d',id_i => true
| id_d',id__dot_ => true
| id_d',id_c => true
| id_d',id_g => true
| id_d',id_e => true
| id_d',id_b' => true
| id_d',id_a => true
| id_d',id_d' => true
| id_d',id_d => false
| id_d,id_f => true
| id_d,id_if => true
| id_d,id_b => true
| id_d,id_h => true
| id_d,id_i => true
| id_d,id__dot_ => true
| id_d,id_c => true
| id_d,id_g => true
| id_d,id_e => true
| id_d,id_b' => true
| id_d,id_a => true
| id_d,id_d' => true
| id_d,id_d => 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 :=
(* f(g(i(a,b,b'),c),d) -> if(e,f(.(b,c),d'),f(.(b',c),d')) *)
| R_xml_0_rule_0 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_if ((algebra.Alg.Term
algebra.F.id_e nil)::(algebra.Alg.Term algebra.F.id_f
((algebra.Alg.Term algebra.F.id__dot_ ((algebra.Alg.Term
algebra.F.id_b nil)::(algebra.Alg.Term algebra.F.id_c
nil)::nil))::(algebra.Alg.Term algebra.F.id_d'
nil)::nil))::(algebra.Alg.Term algebra.F.id_f
((algebra.Alg.Term algebra.F.id__dot_ ((algebra.Alg.Term
algebra.F.id_b' nil)::(algebra.Alg.Term algebra.F.id_c
nil)::nil))::(algebra.Alg.Term algebra.F.id_d'
nil)::nil))::nil))
(algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term algebra.F.id_g
((algebra.Alg.Term algebra.F.id_i ((algebra.Alg.Term algebra.F.id_a
nil)::(algebra.Alg.Term algebra.F.id_b nil)::(algebra.Alg.Term
algebra.F.id_b' nil)::nil))::(algebra.Alg.Term algebra.F.id_c
nil)::nil))::(algebra.Alg.Term algebra.F.id_d nil)::nil))
(* f(g(h(a,b),c),d) -> if(e,f(.(b,g(h(a,b),c)),d),f(c,d')) *)
| R_xml_0_rule_1 :
R_xml_0_rules (algebra.Alg.Term algebra.F.id_if ((algebra.Alg.Term
algebra.F.id_e nil)::(algebra.Alg.Term algebra.F.id_f
((algebra.Alg.Term algebra.F.id__dot_ ((algebra.Alg.Term
algebra.F.id_b nil)::(algebra.Alg.Term algebra.F.id_g
((algebra.Alg.Term algebra.F.id_h ((algebra.Alg.Term
algebra.F.id_a nil)::(algebra.Alg.Term algebra.F.id_b
nil)::nil))::(algebra.Alg.Term algebra.F.id_c
nil)::nil))::nil))::(algebra.Alg.Term algebra.F.id_d
nil)::nil))::(algebra.Alg.Term algebra.F.id_f
((algebra.Alg.Term algebra.F.id_c nil)::(algebra.Alg.Term
algebra.F.id_d' nil)::nil))::nil))
(algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term algebra.F.id_g
((algebra.Alg.Term algebra.F.id_h ((algebra.Alg.Term algebra.F.id_a
nil)::(algebra.Alg.Term algebra.F.id_b nil)::nil))::(algebra.Alg.Term
algebra.F.id_c nil)::nil))::(algebra.Alg.Term algebra.F.id_d
nil)::nil))
.
Definition R_xml_0_rule_as_list_0 :=
((algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term algebra.F.id_g
((algebra.Alg.Term algebra.F.id_i ((algebra.Alg.Term algebra.F.id_a
nil)::(algebra.Alg.Term algebra.F.id_b nil)::(algebra.Alg.Term
algebra.F.id_b' nil)::nil))::(algebra.Alg.Term algebra.F.id_c
nil)::nil))::(algebra.Alg.Term algebra.F.id_d nil)::nil)),
(algebra.Alg.Term algebra.F.id_if ((algebra.Alg.Term algebra.F.id_e
nil)::(algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term
algebra.F.id__dot_ ((algebra.Alg.Term algebra.F.id_b nil)::
(algebra.Alg.Term algebra.F.id_c nil)::nil))::(algebra.Alg.Term
algebra.F.id_d' nil)::nil))::(algebra.Alg.Term algebra.F.id_f
((algebra.Alg.Term algebra.F.id__dot_ ((algebra.Alg.Term
algebra.F.id_b' nil)::(algebra.Alg.Term algebra.F.id_c nil)::nil))::
(algebra.Alg.Term algebra.F.id_d' nil)::nil))::nil)))::nil.
Definition R_xml_0_rule_as_list_1 :=
((algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term algebra.F.id_g
((algebra.Alg.Term algebra.F.id_h ((algebra.Alg.Term algebra.F.id_a
nil)::(algebra.Alg.Term algebra.F.id_b nil)::nil))::(algebra.Alg.Term
algebra.F.id_c nil)::nil))::(algebra.Alg.Term algebra.F.id_d nil)::nil)),
(algebra.Alg.Term algebra.F.id_if ((algebra.Alg.Term algebra.F.id_e
nil)::(algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term
algebra.F.id__dot_ ((algebra.Alg.Term algebra.F.id_b nil)::
(algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Term algebra.F.id_h
((algebra.Alg.Term algebra.F.id_a nil)::(algebra.Alg.Term
algebra.F.id_b nil)::nil))::(algebra.Alg.Term algebra.F.id_c
nil)::nil))::nil))::(algebra.Alg.Term algebra.F.id_d nil)::nil))::
(algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term algebra.F.id_c
nil)::(algebra.Alg.Term algebra.F.id_d' nil)::nil))::nil)))::
R_xml_0_rule_as_list_0.
Definition R_xml_0_rule_as_list := R_xml_0_rule_as_list_1.
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.or3_equiv in H|-.
case H;clear H;intros H.
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_12 (x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13:Prop) :
Prop :=
| conj_12 :
x2->x3->x4->x5->x6->x7->x8->x9->x10->x11->x12->x13->
and_12 x2 x3 x4 x5 x6 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_12 (forall x3 x5 x7,
t = (algebra.Alg.Term algebra.F.id_if (x3::x5::x7::nil)) ->
exists x2,
exists x4,
exists x6,
t' = (algebra.Alg.Term algebra.F.id_if (x2::x4::x6::nil))/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x2 x3)/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x4 x5)/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x6 x7))
(t = (algebra.Alg.Term algebra.F.id_b nil) ->
t' = (algebra.Alg.Term algebra.F.id_b nil))
(forall x3 x5,
t = (algebra.Alg.Term algebra.F.id_h (x3::x5::nil)) ->
exists x2,
exists x4,
t' = (algebra.Alg.Term algebra.F.id_h (x2::x4::nil))/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x2 x3)/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x4 x5))
(forall x3 x5 x7,
t = (algebra.Alg.Term algebra.F.id_i (x3::x5::x7::nil)) ->
exists x2,
exists x4,
exists x6,
t' = (algebra.Alg.Term algebra.F.id_i (x2::x4::x6::nil))/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x2 x3)/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x4 x5)/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x6 x7))
(forall x3 x5,
t = (algebra.Alg.Term algebra.F.id__dot_ (x3::x5::nil)) ->
exists x2,
exists x4,
t' = (algebra.Alg.Term algebra.F.id__dot_ (x2::x4::nil))/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x2 x3)/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x4 x5))
(t = (algebra.Alg.Term algebra.F.id_c nil) ->
t' = (algebra.Alg.Term algebra.F.id_c nil))
(forall x3 x5,
t = (algebra.Alg.Term algebra.F.id_g (x3::x5::nil)) ->
exists x2,
exists x4,
t' = (algebra.Alg.Term algebra.F.id_g (x2::x4::nil))/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x2 x3)/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x4 x5))
(t = (algebra.Alg.Term algebra.F.id_e nil) ->
t' = (algebra.Alg.Term algebra.F.id_e nil))
(t = (algebra.Alg.Term algebra.F.id_b' nil) ->
t' = (algebra.Alg.Term algebra.F.id_b' nil))
(t = (algebra.Alg.Term algebra.F.id_a nil) ->
t' = (algebra.Alg.Term algebra.F.id_a nil))
(t = (algebra.Alg.Term algebra.F.id_d' nil) ->
t' = (algebra.Alg.Term algebra.F.id_d' nil))
(t = (algebra.Alg.Term algebra.F.id_d nil) ->
t' = (algebra.Alg.Term algebra.F.id_d nil)).
Proof.
intros t t' H.
induction H as [|y IH z z_to_y] using
closure_extension.refl_trans_clos_ind2.
constructor 1.
intros x3 x5 x7 H;exists x3;exists x5;exists x7;intuition;constructor 1.
intros H;intuition;constructor 1.
intros x3 x5 H;exists x3;exists x5;intuition;constructor 1.
intros x3 x5 x7 H;exists x3;exists x5;exists x7;intuition;constructor 1.
intros x3 x5 H;exists x3;exists x5;intuition;constructor 1.
intros H;intuition;constructor 1.
intros x3 x5 H;exists x3;exists x5;intuition;constructor 1.
intros H;intuition;constructor 1.
intros H;intuition;constructor 1.
intros H;intuition;constructor 1.
intros H;intuition;constructor 1.
intros H;intuition;constructor 1.
inversion z_to_y as [t1 t2 H H0 H1|f l1 l2 H0 H H2];clear z_to_y;subst.
inversion H as [t1 t2 sigma H2 H1 H0];clear H IH;subst;inversion H2;
clear ;constructor;try (intros until 0 );clear ;intros abs;
discriminate abs.
destruct IH as
[H_id_if H_id_b H_id_h H_id_i H_id__dot_ H_id_c H_id_g H_id_e H_id_b'
H_id_a H_id_d' H_id_d].
constructor.
clear H_id_b H_id_h H_id_i H_id__dot_ H_id_c H_id_g H_id_e H_id_b'
H_id_a H_id_d' H_id_d;intros x3 x5 x7 H;injection H;clear H;intros ;
subst;
repeat (
match goal with
| H:closure.one_step_list (algebra.EQT.one_step _) _ _ |- _ =>
inversion H;clear H;subst
end
).
match goal with
| H:algebra.EQT.one_step _ ?y x3 |- _ =>
destruct (H_id_if y x5 x7 (refl_equal _)) as [x2 [x4 [x6]]];intros ;
intuition;exists x2;exists x4;exists x6;intuition;
eapply closure_extension.refl_trans_clos_R;eassumption
end
.
match goal with
| H:algebra.EQT.one_step _ ?y x5 |- _ =>
destruct (H_id_if x3 y x7 (refl_equal _)) as [x2 [x4 [x6]]];intros ;
intuition;exists x2;exists x4;exists x6;intuition;
eapply closure_extension.refl_trans_clos_R;eassumption
end
.
match goal with
| H:algebra.EQT.one_step _ ?y x7 |- _ =>
destruct (H_id_if x3 x5 y (refl_equal _)) as [x2 [x4 [x6]]];intros ;
intuition;exists x2;exists x4;exists x6;intuition;
eapply closure_extension.refl_trans_clos_R;eassumption
end
.
clear H_id_if H_id_h H_id_i H_id__dot_ H_id_c H_id_g H_id_e H_id_b'
H_id_a H_id_d' H_id_d;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_if H_id_b H_id_i H_id__dot_ H_id_c H_id_g H_id_e H_id_b'
H_id_a H_id_d' H_id_d;intros x3 x5 H;injection H;clear H;intros ;subst;
repeat (
match goal with
| H:closure.one_step_list (algebra.EQT.one_step _) _ _ |- _ =>
inversion H;clear H;subst
end
).
match goal with
| H:algebra.EQT.one_step _ ?y x3 |- _ =>
destruct (H_id_h y x5 (refl_equal _)) as [x2 [x4]];intros ;intuition;
exists x2;exists x4;intuition;
eapply closure_extension.refl_trans_clos_R;eassumption
end
.
match goal with
| H:algebra.EQT.one_step _ ?y x5 |- _ =>
destruct (H_id_h x3 y (refl_equal _)) as [x2 [x4]];intros ;intuition;
exists x2;exists x4;intuition;
eapply closure_extension.refl_trans_clos_R;eassumption
end
.
clear H_id_if H_id_b H_id_h H_id__dot_ H_id_c H_id_g H_id_e H_id_b'
H_id_a H_id_d' H_id_d;intros x3 x5 x7 H;injection H;clear H;intros ;
subst;
repeat (
match goal with
| H:closure.one_step_list (algebra.EQT.one_step _) _ _ |- _ =>
inversion H;clear H;subst
end
).
match goal with
| H:algebra.EQT.one_step _ ?y x3 |- _ =>
destruct (H_id_i y x5 x7 (refl_equal _)) as [x2 [x4 [x6]]];intros ;
intuition;exists x2;exists x4;exists x6;intuition;
eapply closure_extension.refl_trans_clos_R;eassumption
end
.
match goal with
| H:algebra.EQT.one_step _ ?y x5 |- _ =>
destruct (H_id_i x3 y x7 (refl_equal _)) as [x2 [x4 [x6]]];intros ;
intuition;exists x2;exists x4;exists x6;intuition;
eapply closure_extension.refl_trans_clos_R;eassumption
end
.
match goal with
| H:algebra.EQT.one_step _ ?y x7 |- _ =>
destruct (H_id_i x3 x5 y (refl_equal _)) as [x2 [x4 [x6]]];intros ;
intuition;exists x2;exists x4;exists x6;intuition;
eapply closure_extension.refl_trans_clos_R;eassumption
end
.
clear H_id_if H_id_b H_id_h H_id_i H_id_c H_id_g H_id_e H_id_b' H_id_a
H_id_d' H_id_d;intros x3 x5 H;injection H;clear H;intros ;subst;
repeat (
match goal with
| H:closure.one_step_list (algebra.EQT.one_step _) _ _ |- _ =>
inversion H;clear H;subst
end
).
match goal with
| H:algebra.EQT.one_step _ ?y x3 |- _ =>
destruct (H_id__dot_ y x5 (refl_equal _)) as [x2 [x4]];intros ;
intuition;exists x2;exists x4;intuition;
eapply closure_extension.refl_trans_clos_R;eassumption
end
.
match goal with
| H:algebra.EQT.one_step _ ?y x5 |- _ =>
destruct (H_id__dot_ x3 y (refl_equal _)) as [x2 [x4]];intros ;
intuition;exists x2;exists x4;intuition;
eapply closure_extension.refl_trans_clos_R;eassumption
end
.
clear H_id_if H_id_b H_id_h H_id_i H_id__dot_ H_id_g H_id_e H_id_b'
H_id_a H_id_d' H_id_d;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_if H_id_b H_id_h H_id_i H_id__dot_ H_id_c H_id_e H_id_b'
H_id_a H_id_d' H_id_d;intros x3 x5 H;injection H;clear H;intros ;subst;
repeat (
match goal with
| H:closure.one_step_list (algebra.EQT.one_step _) _ _ |- _ =>
inversion H;clear H;subst
end
).
match goal with
| H:algebra.EQT.one_step _ ?y x3 |- _ =>
destruct (H_id_g y x5 (refl_equal _)) as [x2 [x4]];intros ;intuition;
exists x2;exists x4;intuition;
eapply closure_extension.refl_trans_clos_R;eassumption
end
.
match goal with
| H:algebra.EQT.one_step _ ?y x5 |- _ =>
destruct (H_id_g x3 y (refl_equal _)) as [x2 [x4]];intros ;intuition;
exists x2;exists x4;intuition;
eapply closure_extension.refl_trans_clos_R;eassumption
end
.
clear H_id_if H_id_b H_id_h H_id_i H_id__dot_ H_id_c H_id_g H_id_b'
H_id_a H_id_d' H_id_d;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_if H_id_b H_id_h H_id_i H_id__dot_ H_id_c H_id_g H_id_e
H_id_a H_id_d' H_id_d;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_if H_id_b H_id_h H_id_i H_id__dot_ H_id_c H_id_g H_id_e
H_id_b' H_id_d' H_id_d;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_if H_id_b H_id_h H_id_i H_id__dot_ H_id_c H_id_g H_id_e
H_id_b' H_id_a H_id_d;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_if H_id_b H_id_h H_id_i H_id__dot_ H_id_c H_id_g H_id_e
H_id_b' H_id_a H_id_d';intros H;injection H;clear H;intros ;subst;
repeat (
match goal with
| H:closure.one_step_list (algebra.EQT.one_step _) _ _ |- _ =>
inversion H;clear H;subst
end
).
Qed.
Lemma id_if_is_R_xml_0_constructor :
forall t t',
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
forall x3 x5 x7,
t = (algebra.Alg.Term algebra.F.id_if (x3::x5::x7::nil)) ->
exists x2,
exists x4,
exists x6,
t' = (algebra.Alg.Term algebra.F.id_if (x2::x4::x6::nil))/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x2 x3)/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x4 x5)/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x6 x7).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Lemma id_b_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_b nil) ->
t' = (algebra.Alg.Term algebra.F.id_b nil).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Lemma id_h_is_R_xml_0_constructor :
forall t t',
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
forall x3 x5,
t = (algebra.Alg.Term algebra.F.id_h (x3::x5::nil)) ->
exists x2,
exists x4,
t' = (algebra.Alg.Term algebra.F.id_h (x2::x4::nil))/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x2 x3)/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x4 x5).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Lemma id_i_is_R_xml_0_constructor :
forall t t',
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
forall x3 x5 x7,
t = (algebra.Alg.Term algebra.F.id_i (x3::x5::x7::nil)) ->
exists x2,
exists x4,
exists x6,
t' = (algebra.Alg.Term algebra.F.id_i (x2::x4::x6::nil))/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x2 x3)/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x4 x5)/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
x6 x7).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Lemma id__dot__is_R_xml_0_constructor :
forall t t',
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
forall x3 x5,
t = (algebra.Alg.Term algebra.F.id__dot_ (x3::x5::nil)) ->
exists x2,
exists x4,
t' = (algebra.Alg.Term algebra.F.id__dot_ (x2::x4::nil))/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x2 x3)/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x4 x5).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Lemma id_c_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_c nil) ->
t' = (algebra.Alg.Term algebra.F.id_c nil).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Lemma id_g_is_R_xml_0_constructor :
forall t t',
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
forall x3 x5,
t = (algebra.Alg.Term algebra.F.id_g (x3::x5::nil)) ->
exists x2,
exists x4,
t' = (algebra.Alg.Term algebra.F.id_g (x2::x4::nil))/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x2 x3)/\
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x4 x5).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Lemma id_e_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_e nil) ->
t' = (algebra.Alg.Term algebra.F.id_e nil).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Lemma id_b'_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_b' nil) ->
t' = (algebra.Alg.Term algebra.F.id_b' nil).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Lemma id_a_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_a nil) ->
t' = (algebra.Alg.Term algebra.F.id_a nil).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Lemma id_d'_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_d' nil) ->
t' = (algebra.Alg.Term algebra.F.id_d' nil).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Lemma id_d_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_d nil) ->
t' = (algebra.Alg.Term algebra.F.id_d nil).
Proof.
intros t t' H.
destruct (are_constuctors_of_R_xml_0 H).
assumption.
Qed.
Ltac impossible_star_reduction_R_xml_0 :=
match goal with
| H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
_ (algebra.Alg.Term algebra.F.id_if (?x4::?x3::?x2::nil)) |-
_ =>
let x4 := fresh "x" in
(let x3 := fresh "x" in
(let x2 := fresh "x" in
(let Heq := fresh "Heq" in
(let Hred1 := fresh "Hred" in
(let Hred2 := fresh "Hred" in
(let Hred3 := fresh "Hred" in
(destruct (id_if_is_R_xml_0_constructor H (refl_equal _))
as [x4 [x3 [x2 [Heq [Hred3 [Hred2 Hred1]]]]]];
(discriminate Heq)||
(injection Heq;intros ;subst;clear Heq;clear H;
impossible_star_reduction_R_xml_0 ))))))))
| H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
_ (algebra.Alg.Term algebra.F.id_b nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_b_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_h (?x3::?x2::nil)) |- _ =>
let x3 := fresh "x" in
(let x2 := fresh "x" in
(let Heq := fresh "Heq" in
(let Hred1 := fresh "Hred" in
(let Hred2 := fresh "Hred" in
(destruct (id_h_is_R_xml_0_constructor H (refl_equal _)) as
[x3 [x2 [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_i (?x4::?x3::?x2::nil)) |-
_ =>
let x4 := fresh "x" in
(let x3 := fresh "x" in
(let x2 := fresh "x" in
(let Heq := fresh "Heq" in
(let Hred1 := fresh "Hred" in
(let Hred2 := fresh "Hred" in
(let Hred3 := fresh "Hred" in
(destruct (id_i_is_R_xml_0_constructor H (refl_equal _))
as [x4 [x3 [x2 [Heq [Hred3 [Hred2 Hred1]]]]]];
(discriminate Heq)||
(injection Heq;intros ;subst;clear Heq;clear H;
impossible_star_reduction_R_xml_0 ))))))))
| H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
_ (algebra.Alg.Term algebra.F.id__dot_ (?x3::?x2::nil)) |- _ =>
let x3 := fresh "x" in
(let x2 := fresh "x" in
(let Heq := fresh "Heq" in
(let Hred1 := fresh "Hred" in
(let Hred2 := fresh "Hred" in
(destruct (id__dot__is_R_xml_0_constructor H (refl_equal _))
as [x3 [x2 [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_c nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_c_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_g (?x3::?x2::nil)) |- _ =>
let x3 := fresh "x" in
(let x2 := fresh "x" in
(let Heq := fresh "Heq" in
(let Hred1 := fresh "Hred" in
(let Hred2 := fresh "Hred" in
(destruct (id_g_is_R_xml_0_constructor H (refl_equal _)) as
[x3 [x2 [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_e nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_e_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_b' nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_b'_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_a nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_a_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_d' nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_d'_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_d nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_d_is_R_xml_0_constructor H (refl_equal _)) in *;
(discriminate Heq)||
(clearbody Heq;try (subst);try (clear Heq);clear H;
impossible_star_reduction_R_xml_0 ))
end
.
Ltac simplify_star_reduction_R_xml_0 :=
match goal with
| H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
_ (algebra.Alg.Term algebra.F.id_if (?x4::?x3::?x2::nil)) |-
_ =>
let x4 := fresh "x" in
(let x3 := fresh "x" in
(let x2 := fresh "x" in
(let Heq := fresh "Heq" in
(let Hred1 := fresh "Hred" in
(let Hred2 := fresh "Hred" in
(let Hred3 := fresh "Hred" in
(destruct (id_if_is_R_xml_0_constructor H (refl_equal _))
as [x4 [x3 [x2 [Heq [Hred3 [Hred2 Hred1]]]]]];
(discriminate Heq)||
(injection Heq;intros ;subst;clear Heq;clear H;
try (simplify_star_reduction_R_xml_0 )))))))))
| H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
_ (algebra.Alg.Term algebra.F.id_b nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_b_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_h (?x3::?x2::nil)) |- _ =>
let x3 := fresh "x" in
(let x2 := fresh "x" in
(let Heq := fresh "Heq" in
(let Hred1 := fresh "Hred" in
(let Hred2 := fresh "Hred" in
(destruct (id_h_is_R_xml_0_constructor H (refl_equal _)) as
[x3 [x2 [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_i (?x4::?x3::?x2::nil)) |-
_ =>
let x4 := fresh "x" in
(let x3 := fresh "x" in
(let x2 := fresh "x" in
(let Heq := fresh "Heq" in
(let Hred1 := fresh "Hred" in
(let Hred2 := fresh "Hred" in
(let Hred3 := fresh "Hred" in
(destruct (id_i_is_R_xml_0_constructor H (refl_equal _))
as [x4 [x3 [x2 [Heq [Hred3 [Hred2 Hred1]]]]]];
(discriminate Heq)||
(injection Heq;intros ;subst;clear Heq;clear H;
try (simplify_star_reduction_R_xml_0 )))))))))
| H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
_ (algebra.Alg.Term algebra.F.id__dot_ (?x3::?x2::nil)) |- _ =>
let x3 := fresh "x" in
(let x2 := fresh "x" in
(let Heq := fresh "Heq" in
(let Hred1 := fresh "Hred" in
(let Hred2 := fresh "Hred" in
(destruct (id__dot__is_R_xml_0_constructor H (refl_equal _))
as [x3 [x2 [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_c nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_c_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_g (?x3::?x2::nil)) |- _ =>
let x3 := fresh "x" in
(let x2 := fresh "x" in
(let Heq := fresh "Heq" in
(let Hred1 := fresh "Hred" in
(let Hred2 := fresh "Hred" in
(destruct (id_g_is_R_xml_0_constructor H (refl_equal _)) as
[x3 [x2 [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_e nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_e_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_b' nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_b'_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_a nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_a_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_d' nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_d'_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_d nil) |- _ =>
let Heq := fresh "Heq" in
(set (Heq:=id_d_is_R_xml_0_constructor H (refl_equal _)) in *;
(discriminate Heq)||
(clearbody Heq;try (subst);try (clear Heq);clear H;
try (simplify_star_reduction_R_xml_0 )))
end
.
End R_xml_0_deep_rew.
Module WF_R_xml_0_deep_rew.
Inductive DP_R_xml_0 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <f(g(i(a,b,b'),c),d),f(.(b,c),d')> *)
| DP_R_xml_0_0 :
forall x2 x3,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Term algebra.F.id_i
((algebra.Alg.Term algebra.F.id_a nil)::(algebra.Alg.Term
algebra.F.id_b nil)::(algebra.Alg.Term algebra.F.id_b' nil)::nil))::
(algebra.Alg.Term algebra.F.id_c nil)::nil)) x3) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_d nil)
x2) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term
algebra.F.id__dot_ ((algebra.Alg.Term algebra.F.id_b
nil)::(algebra.Alg.Term algebra.F.id_c nil)::nil))::
(algebra.Alg.Term algebra.F.id_d' nil)::nil))
(algebra.Alg.Term algebra.F.id_f (x3::x2::nil))
(* <f(g(i(a,b,b'),c),d),f(.(b',c),d')> *)
| DP_R_xml_0_1 :
forall x2 x3,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Term algebra.F.id_i
((algebra.Alg.Term algebra.F.id_a nil)::(algebra.Alg.Term
algebra.F.id_b nil)::(algebra.Alg.Term algebra.F.id_b' nil)::nil))::
(algebra.Alg.Term algebra.F.id_c nil)::nil)) x3) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_d nil)
x2) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term
algebra.F.id__dot_ ((algebra.Alg.Term algebra.F.id_b'
nil)::(algebra.Alg.Term algebra.F.id_c nil)::nil))::
(algebra.Alg.Term algebra.F.id_d' nil)::nil))
(algebra.Alg.Term algebra.F.id_f (x3::x2::nil))
(* <f(g(h(a,b),c),d),f(.(b,g(h(a,b),c)),d)> *)
| DP_R_xml_0_2 :
forall x2 x3,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Term algebra.F.id_h
((algebra.Alg.Term algebra.F.id_a nil)::(algebra.Alg.Term
algebra.F.id_b nil)::nil))::(algebra.Alg.Term algebra.F.id_c
nil)::nil)) x3) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_d nil)
x2) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term
algebra.F.id__dot_ ((algebra.Alg.Term algebra.F.id_b
nil)::(algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Term
algebra.F.id_h ((algebra.Alg.Term algebra.F.id_a nil)::
(algebra.Alg.Term algebra.F.id_b nil)::nil))::
(algebra.Alg.Term algebra.F.id_c nil)::nil))::nil))::
(algebra.Alg.Term algebra.F.id_d nil)::nil))
(algebra.Alg.Term algebra.F.id_f (x3::x2::nil))
(* <f(g(h(a,b),c),d),f(c,d')> *)
| DP_R_xml_0_3 :
forall x2 x3,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Term algebra.F.id_h
((algebra.Alg.Term algebra.F.id_a nil)::(algebra.Alg.Term
algebra.F.id_b nil)::nil))::(algebra.Alg.Term algebra.F.id_c
nil)::nil)) x3) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_d nil)
x2) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term
algebra.F.id_c nil)::(algebra.Alg.Term algebra.F.id_d'
nil)::nil))
(algebra.Alg.Term algebra.F.id_f (x3::x2::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(g(h(a,b),c),d),f(c,d')> *)
| DP_R_xml_0_non_scc_1_0 :
forall x2 x3,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Term algebra.F.id_h
((algebra.Alg.Term algebra.F.id_a nil)::(algebra.Alg.Term
algebra.F.id_b nil)::nil))::(algebra.Alg.Term algebra.F.id_c
nil)::nil)) x3) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_d nil)
x2) ->
DP_R_xml_0_non_scc_1 (algebra.Alg.Term algebra.F.id_f
((algebra.Alg.Term algebra.F.id_c nil)::
(algebra.Alg.Term algebra.F.id_d' nil)::nil))
(algebra.Alg.Term algebra.F.id_f (x3::x2::nil))
.
Lemma acc_DP_R_xml_0_non_scc_1 :
forall x y,
(DP_R_xml_0_non_scc_1 x y) ->Acc WF_R_xml_0_deep_rew.DP_R_xml_0 x.
Proof.
intros x y h.
inversion h;clear h;subst;
constructor;intros _y _h;inversion _h;clear _h;subst;
(R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 )||
(eapply Hrec;econstructor (eassumption)||(algebra.Alg_ext.star_refl' )).
Qed.
Inductive DP_R_xml_0_non_scc_2 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <f(g(h(a,b),c),d),f(.(b,g(h(a,b),c)),d)> *)
| DP_R_xml_0_non_scc_2_0 :
forall x2 x3,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Term algebra.F.id_h
((algebra.Alg.Term algebra.F.id_a nil)::(algebra.Alg.Term
algebra.F.id_b nil)::nil))::(algebra.Alg.Term algebra.F.id_c
nil)::nil)) x3) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_d nil)
x2) ->
DP_R_xml_0_non_scc_2 (algebra.Alg.Term algebra.F.id_f
((algebra.Alg.Term algebra.F.id__dot_
((algebra.Alg.Term algebra.F.id_b nil)::
(algebra.Alg.Term algebra.F.id_g
((algebra.Alg.Term algebra.F.id_h
((algebra.Alg.Term algebra.F.id_a nil)::
(algebra.Alg.Term algebra.F.id_b nil)::nil))::
(algebra.Alg.Term algebra.F.id_c
nil)::nil))::nil))::(algebra.Alg.Term
algebra.F.id_d nil)::nil))
(algebra.Alg.Term algebra.F.id_f (x3::x2::nil))
.
Lemma acc_DP_R_xml_0_non_scc_2 :
forall x y,
(DP_R_xml_0_non_scc_2 x y) ->Acc WF_R_xml_0_deep_rew.DP_R_xml_0 x.
Proof.
intros x y h.
inversion h;clear h;subst;
constructor;intros _y _h;inversion _h;clear _h;subst;
(R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 )||
(eapply Hrec;econstructor (eassumption)||(algebra.Alg_ext.star_refl' )).
Qed.
Inductive DP_R_xml_0_non_scc_3 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <f(g(i(a,b,b'),c),d),f(.(b',c),d')> *)
| DP_R_xml_0_non_scc_3_0 :
forall x2 x3,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Term algebra.F.id_i
((algebra.Alg.Term algebra.F.id_a nil)::(algebra.Alg.Term
algebra.F.id_b nil)::(algebra.Alg.Term algebra.F.id_b' nil)::nil))::
(algebra.Alg.Term algebra.F.id_c nil)::nil)) x3) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_d nil)
x2) ->
DP_R_xml_0_non_scc_3 (algebra.Alg.Term algebra.F.id_f
((algebra.Alg.Term algebra.F.id__dot_
((algebra.Alg.Term algebra.F.id_b' nil)::
(algebra.Alg.Term algebra.F.id_c nil)::nil))::
(algebra.Alg.Term algebra.F.id_d' nil)::nil))
(algebra.Alg.Term algebra.F.id_f (x3::x2::nil))
.
Lemma acc_DP_R_xml_0_non_scc_3 :
forall x y,
(DP_R_xml_0_non_scc_3 x y) ->Acc WF_R_xml_0_deep_rew.DP_R_xml_0 x.
Proof.
intros x y h.
inversion h;clear h;subst;
constructor;intros _y _h;inversion _h;clear _h;subst;
(R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 )||
(eapply Hrec;econstructor (eassumption)||(algebra.Alg_ext.star_refl' )).
Qed.
Inductive DP_R_xml_0_non_scc_4 :
algebra.Alg.term ->algebra.Alg.term ->Prop :=
(* <f(g(i(a,b,b'),c),d),f(.(b,c),d')> *)
| DP_R_xml_0_non_scc_4_0 :
forall x2 x3,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Term algebra.F.id_i
((algebra.Alg.Term algebra.F.id_a nil)::(algebra.Alg.Term
algebra.F.id_b nil)::(algebra.Alg.Term algebra.F.id_b' nil)::nil))::
(algebra.Alg.Term algebra.F.id_c nil)::nil)) x3) ->
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_d nil)
x2) ->
DP_R_xml_0_non_scc_4 (algebra.Alg.Term algebra.F.id_f
((algebra.Alg.Term algebra.F.id__dot_
((algebra.Alg.Term algebra.F.id_b nil)::
(algebra.Alg.Term algebra.F.id_c nil)::nil))::
(algebra.Alg.Term algebra.F.id_d' nil)::nil))
(algebra.Alg.Term algebra.F.id_f (x3::x2::nil))
.
Lemma acc_DP_R_xml_0_non_scc_4 :
forall x y,
(DP_R_xml_0_non_scc_4 x y) ->Acc WF_R_xml_0_deep_rew.DP_R_xml_0 x.
Proof.
intros x y h.
inversion h;clear h;subst;
constructor;intros _y _h;inversion _h;clear _h;subst;
(R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 )||
(eapply Hrec;econstructor (eassumption)||(algebra.Alg_ext.star_refl' )).
Qed.
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_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' ))||
((R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 )||(fail)))))).
Qed.
End WF_DP_R_xml_0.
Definition wf_H := WF_DP_R_xml_0.wf.
Lemma wf :
well_founded (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules).
Proof.
apply ddp.dp_criterion.
apply R_xml_0_deep_rew.R_xml_0_non_var.
apply R_xml_0_deep_rew.R_xml_0_reg.
intros ;
apply (ddp.constructor_defined_dec _ _
R_xml_0_deep_rew.R_xml_0_rules_included).
refine (Inclusion.wf_incl _ _ _ _ wf_H).
intros x y H.
destruct (R_xml_0_dp_step_spec H) as [f [l1 [l2 [H1 [H2 H3]]]]].
destruct (ddp.dp_list_complete _ _
R_xml_0_deep_rew.R_xml_0_rules_included _ _ H3)
as [x' [y' [sigma [h1 [h2 h3]]]]].
clear H3.
subst.
vm_compute in h3|-.
let e := type of h3 in (dp_concl_tac h2 h3 ltac:(fun _ => idtac) e).
Qed.
End WF_R_xml_0_deep_rew.
(*
*** Local Variables: ***
*** coq-prog-name: "coqtop" ***
*** coq-prog-args: ("-emacs-U" "-I" "$COCCINELLE/examples" "-I" "$COCCINELLE/term_algebra" "-I" "$COCCINELLE/term_orderings" "-I" "$COCCINELLE/basis" "-I" "$COCCINELLE/list_extensions" "-I" "$COCCINELLE/examples/cime_trace/") ***
*** compile-command: "coqc -I $COCCINELLE/term_algebra -I $COCCINELLE/term_orderings -I $COCCINELLE/basis -I $COCCINELLE/list_extensions -I $COCCINELLE/examples/cime_trace/ -I $COCCINELLE/examples/ c_output/strat/tpdb-5.0___TRS___SK90___4.47.trs/a3pat.v" ***
*** End: ***
*)