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 := (* *) | 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)) (* *) | 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)) (* *) | 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)) (* *) | 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 := (* *) | 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 := (* *) | 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 := (* *) | 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 := (* *) | 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: *** *)