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_g2 *) | id_g2 : symb (* id_g1 *) | id_g1 : symb (* id_h *) | id_h : symb . Definition symb_eq_bool (f1 f2:symb) : bool := match f1,f2 with | id_f,id_f => true | id_g2,id_g2 => true | id_g1,id_g1 => true | id_h,id_h => 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_g2,id_g2 => refl_equal _ | id_g1,id_g1 => refl_equal _ | id_h,id_h => refl_equal _ | _,_ => _ end;intros abs;discriminate. Defined. Definition arity (f:symb) := match f with | id_f => term.Free 2 | id_g2 => term.Free 3 | id_g1 => term.Free 3 | id_h => term.Free 2 end. Definition symb_order (f1 f2:symb) : bool := match f1,f2 with | id_f,id_f => true | id_f,id_g2 => false | id_f,id_g1 => false | id_f,id_h => false | id_g2,id_f => true | id_g2,id_g2 => true | id_g2,id_g1 => false | id_g2,id_h => false | id_g1,id_f => true | id_g1,id_g2 => true | id_g1,id_g1 => true | id_g1,id_h => false | id_h,id_f => true | id_h,id_g2 => true | id_h,id_g1 => true | id_h,id_h => 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(x_,y_) -> g1(x_,x_,y_) *) | R_xml_0_rule_0 : R_xml_0_rules (algebra.Alg.Term algebra.F.id_g1 ((algebra.Alg.Var 1):: (algebra.Alg.Var 1)::(algebra.Alg.Var 2)::nil)) (algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Var 1):: (algebra.Alg.Var 2)::nil)) (* f(x_,y_) -> g1(y_,x_,x_) *) | R_xml_0_rule_1 : R_xml_0_rules (algebra.Alg.Term algebra.F.id_g1 ((algebra.Alg.Var 2):: (algebra.Alg.Var 1)::(algebra.Alg.Var 1)::nil)) (algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Var 1):: (algebra.Alg.Var 2)::nil)) (* f(x_,y_) -> g2(x_,y_,y_) *) | R_xml_0_rule_2 : R_xml_0_rules (algebra.Alg.Term algebra.F.id_g2 ((algebra.Alg.Var 1):: (algebra.Alg.Var 2)::(algebra.Alg.Var 2)::nil)) (algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Var 1):: (algebra.Alg.Var 2)::nil)) (* f(x_,y_) -> g2(y_,y_,x_) *) | R_xml_0_rule_3 : R_xml_0_rules (algebra.Alg.Term algebra.F.id_g2 ((algebra.Alg.Var 2):: (algebra.Alg.Var 2)::(algebra.Alg.Var 1)::nil)) (algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Var 1):: (algebra.Alg.Var 2)::nil)) (* g1(x_,x_,y_) -> h(x_,y_) *) | R_xml_0_rule_4 : R_xml_0_rules (algebra.Alg.Term algebra.F.id_h ((algebra.Alg.Var 1):: (algebra.Alg.Var 2)::nil)) (algebra.Alg.Term algebra.F.id_g1 ((algebra.Alg.Var 1):: (algebra.Alg.Var 1)::(algebra.Alg.Var 2)::nil)) (* g1(y_,x_,x_) -> h(x_,y_) *) | R_xml_0_rule_5 : R_xml_0_rules (algebra.Alg.Term algebra.F.id_h ((algebra.Alg.Var 1):: (algebra.Alg.Var 2)::nil)) (algebra.Alg.Term algebra.F.id_g1 ((algebra.Alg.Var 2):: (algebra.Alg.Var 1)::(algebra.Alg.Var 1)::nil)) (* g2(x_,y_,y_) -> h(x_,y_) *) | R_xml_0_rule_6 : R_xml_0_rules (algebra.Alg.Term algebra.F.id_h ((algebra.Alg.Var 1):: (algebra.Alg.Var 2)::nil)) (algebra.Alg.Term algebra.F.id_g2 ((algebra.Alg.Var 1):: (algebra.Alg.Var 2)::(algebra.Alg.Var 2)::nil)) (* g2(y_,y_,x_) -> h(x_,y_) *) | R_xml_0_rule_7 : R_xml_0_rules (algebra.Alg.Term algebra.F.id_h ((algebra.Alg.Var 1):: (algebra.Alg.Var 2)::nil)) (algebra.Alg.Term algebra.F.id_g2 ((algebra.Alg.Var 2):: (algebra.Alg.Var 2)::(algebra.Alg.Var 1)::nil)) (* h(x_,x_) -> x_ *) | R_xml_0_rule_8 : R_xml_0_rules (algebra.Alg.Var 1) (algebra.Alg.Term algebra.F.id_h ((algebra.Alg.Var 1):: (algebra.Alg.Var 1)::nil)) . Definition R_xml_0_rule_as_list_0 := ((algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Var 1):: (algebra.Alg.Var 2)::nil)), (algebra.Alg.Term algebra.F.id_g1 ((algebra.Alg.Var 1):: (algebra.Alg.Var 1)::(algebra.Alg.Var 2)::nil)))::nil. Definition R_xml_0_rule_as_list_1 := ((algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Var 1):: (algebra.Alg.Var 2)::nil)), (algebra.Alg.Term algebra.F.id_g1 ((algebra.Alg.Var 2):: (algebra.Alg.Var 1)::(algebra.Alg.Var 1)::nil)))::R_xml_0_rule_as_list_0 . Definition R_xml_0_rule_as_list_2 := ((algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Var 1):: (algebra.Alg.Var 2)::nil)), (algebra.Alg.Term algebra.F.id_g2 ((algebra.Alg.Var 1):: (algebra.Alg.Var 2)::(algebra.Alg.Var 2)::nil)))::R_xml_0_rule_as_list_1 . Definition R_xml_0_rule_as_list_3 := ((algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Var 1):: (algebra.Alg.Var 2)::nil)), (algebra.Alg.Term algebra.F.id_g2 ((algebra.Alg.Var 2):: (algebra.Alg.Var 2)::(algebra.Alg.Var 1)::nil)))::R_xml_0_rule_as_list_2 . Definition R_xml_0_rule_as_list_4 := ((algebra.Alg.Term algebra.F.id_g1 ((algebra.Alg.Var 1):: (algebra.Alg.Var 1)::(algebra.Alg.Var 2)::nil)), (algebra.Alg.Term algebra.F.id_h ((algebra.Alg.Var 1):: (algebra.Alg.Var 2)::nil)))::R_xml_0_rule_as_list_3. Definition R_xml_0_rule_as_list_5 := ((algebra.Alg.Term algebra.F.id_g1 ((algebra.Alg.Var 2):: (algebra.Alg.Var 1)::(algebra.Alg.Var 1)::nil)), (algebra.Alg.Term algebra.F.id_h ((algebra.Alg.Var 1):: (algebra.Alg.Var 2)::nil)))::R_xml_0_rule_as_list_4. Definition R_xml_0_rule_as_list_6 := ((algebra.Alg.Term algebra.F.id_g2 ((algebra.Alg.Var 1):: (algebra.Alg.Var 2)::(algebra.Alg.Var 2)::nil)), (algebra.Alg.Term algebra.F.id_h ((algebra.Alg.Var 1):: (algebra.Alg.Var 2)::nil)))::R_xml_0_rule_as_list_5. Definition R_xml_0_rule_as_list_7 := ((algebra.Alg.Term algebra.F.id_g2 ((algebra.Alg.Var 2):: (algebra.Alg.Var 2)::(algebra.Alg.Var 1)::nil)), (algebra.Alg.Term algebra.F.id_h ((algebra.Alg.Var 1):: (algebra.Alg.Var 2)::nil)))::R_xml_0_rule_as_list_6. Definition R_xml_0_rule_as_list_8 := ((algebra.Alg.Term algebra.F.id_h ((algebra.Alg.Var 1):: (algebra.Alg.Var 1)::nil)),(algebra.Alg.Var 1))::R_xml_0_rule_as_list_7. Definition R_xml_0_rule_as_list := R_xml_0_rule_as_list_8. Lemma R_xml_0_rules_included : forall l r, R_xml_0_rules r l <-> In (l,r) R_xml_0_rule_as_list. Proof. intros l r. constructor. intros H. case H;clear H; (apply (more_list.mem_impl_in (@eq (algebra.Alg.term*algebra.Alg.term))); [tauto|idtac]); match goal with | |- _ _ _ ?t ?l => let u := fresh "u" in (generalize (more_list.mem_bool_ok _ _ algebra.Alg_ext.eq_term_term_bool_ok t l); set (u:=more_list.mem_bool algebra.Alg_ext.eq_term_term_bool t l) in *; vm_compute in u|-;unfold u in *;clear u;intros H;refine H) end . intros H. vm_compute in H|-. rewrite <- or_ext_generated.or10_equiv in H|-. case H;clear H;intros H. injection H;intros ;subst;constructor 9. injection H;intros ;subst;constructor 8. injection H;intros ;subst;constructor 7. injection H;intros ;subst;constructor 6. injection H;intros ;subst;constructor 5. injection H;intros ;subst;constructor 4. injection H;intros ;subst;constructor 3. injection H;intros ;subst;constructor 2. injection H;intros ;subst;constructor 1. elim H. Qed. Lemma R_xml_0_non_var : forall x t, ~R_xml_0_rules t (algebra.EQT.T.Var x). Proof. intros x t H. inversion H. Qed. Lemma R_xml_0_reg : forall s t, (R_xml_0_rules s t) -> forall x, In x (algebra.Alg.var_list s) ->In x (algebra.Alg.var_list t). Proof. intros s t H. inversion H;intros x Hx; (apply (more_list.mem_impl_in (@eq algebra.Alg.variable));[tauto|idtac]); apply (more_list.in_impl_mem (@eq algebra.Alg.variable)) in Hx; vm_compute in Hx|-*;tauto. Qed. Ltac impossible_star_reduction_R_xml_0 := fail. Ltac simplify_star_reduction_R_xml_0 := fail. 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 x4 x2 x1 x5, (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x1 x5) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x2 x4) -> DP_R_xml_0 (algebra.Alg.Term algebra.F.id_g1 (x1::x1::x2::nil)) (algebra.Alg.Term algebra.F.id_f (x5::x4::nil)) (* *) | DP_R_xml_0_1 : forall x4 x2 x1 x5, (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x1 x5) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x2 x4) -> DP_R_xml_0 (algebra.Alg.Term algebra.F.id_g1 (x2::x1::x1::nil)) (algebra.Alg.Term algebra.F.id_f (x5::x4::nil)) (* *) | DP_R_xml_0_2 : forall x4 x2 x1 x5, (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x1 x5) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x2 x4) -> DP_R_xml_0 (algebra.Alg.Term algebra.F.id_g2 (x1::x2::x2::nil)) (algebra.Alg.Term algebra.F.id_f (x5::x4::nil)) (* *) | DP_R_xml_0_3 : forall x4 x2 x1 x5, (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x1 x5) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x2 x4) -> DP_R_xml_0 (algebra.Alg.Term algebra.F.id_g2 (x2::x2::x1::nil)) (algebra.Alg.Term algebra.F.id_f (x5::x4::nil)) (* *) | DP_R_xml_0_4 : forall x4 x2 x6 x1 x5, (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x1 x6) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x1 x5) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x2 x4) -> DP_R_xml_0 (algebra.Alg.Term algebra.F.id_h (x1::x2::nil)) (algebra.Alg.Term algebra.F.id_g1 (x6::x5::x4::nil)) (* *) | DP_R_xml_0_5 : forall x4 x2 x6 x1 x5, (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x2 x6) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x1 x5) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x1 x4) -> DP_R_xml_0 (algebra.Alg.Term algebra.F.id_h (x1::x2::nil)) (algebra.Alg.Term algebra.F.id_g1 (x6::x5::x4::nil)) (* *) | DP_R_xml_0_6 : forall x4 x2 x6 x1 x5, (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x1 x6) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x2 x5) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x2 x4) -> DP_R_xml_0 (algebra.Alg.Term algebra.F.id_h (x1::x2::nil)) (algebra.Alg.Term algebra.F.id_g2 (x6::x5::x4::nil)) (* *) | DP_R_xml_0_7 : forall x4 x2 x6 x1 x5, (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x2 x6) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x2 x5) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x1 x4) -> DP_R_xml_0 (algebra.Alg.Term algebra.F.id_h (x1::x2::nil)) (algebra.Alg.Term algebra.F.id_g2 (x6::x5::x4::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 x4 x2 x6 x1 x5, (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x2 x6) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x2 x5) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x1 x4) -> DP_R_xml_0_non_scc_1 (algebra.Alg.Term algebra.F.id_h (x1::x2::nil)) (algebra.Alg.Term algebra.F.id_g2 (x6::x5::x4::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 x4 x2 x6 x1 x5, (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x1 x6) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x2 x5) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x2 x4) -> DP_R_xml_0_non_scc_2 (algebra.Alg.Term algebra.F.id_h (x1::x2::nil)) (algebra.Alg.Term algebra.F.id_g2 (x6::x5::x4::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 x4 x2 x6 x1 x5, (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x2 x6) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x1 x5) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x1 x4) -> DP_R_xml_0_non_scc_3 (algebra.Alg.Term algebra.F.id_h (x1::x2::nil)) (algebra.Alg.Term algebra.F.id_g1 (x6::x5::x4::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 x4 x2 x6 x1 x5, (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x1 x6) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x1 x5) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x2 x4) -> DP_R_xml_0_non_scc_4 (algebra.Alg.Term algebra.F.id_h (x1::x2::nil)) (algebra.Alg.Term algebra.F.id_g1 (x6::x5::x4::nil)) . Lemma acc_DP_R_xml_0_non_scc_4 : forall x y, (DP_R_xml_0_non_scc_4 x y) ->Acc WF_R_xml_0_deep_rew.DP_R_xml_0 x. Proof. intros x y h. inversion h;clear h;subst; constructor;intros _y _h;inversion _h;clear _h;subst; (R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 )|| (eapply Hrec;econstructor (eassumption)||(algebra.Alg_ext.star_refl' )). Qed. Inductive DP_R_xml_0_non_scc_5 : algebra.Alg.term ->algebra.Alg.term ->Prop := (* *) | DP_R_xml_0_non_scc_5_0 : forall x4 x2 x1 x5, (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x1 x5) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x2 x4) -> DP_R_xml_0_non_scc_5 (algebra.Alg.Term algebra.F.id_g2 (x2::x2:: x1::nil)) (algebra.Alg.Term algebra.F.id_f (x5::x4::nil)) . Lemma acc_DP_R_xml_0_non_scc_5 : forall x y, (DP_R_xml_0_non_scc_5 x y) ->Acc WF_R_xml_0_deep_rew.DP_R_xml_0 x. Proof. intros x y h. inversion h;clear h;subst; constructor;intros _y _h;inversion _h;clear _h;subst; (eapply acc_DP_R_xml_0_non_scc_2; econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))|| ((eapply acc_DP_R_xml_0_non_scc_1; econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))|| ((R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 )|| (eapply Hrec; econstructor (eassumption)||(algebra.Alg_ext.star_refl' )))). Qed. Inductive DP_R_xml_0_non_scc_6 : algebra.Alg.term ->algebra.Alg.term ->Prop := (* *) | DP_R_xml_0_non_scc_6_0 : forall x4 x2 x1 x5, (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x1 x5) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x2 x4) -> DP_R_xml_0_non_scc_6 (algebra.Alg.Term algebra.F.id_g2 (x1::x2:: x2::nil)) (algebra.Alg.Term algebra.F.id_f (x5::x4::nil)) . Lemma acc_DP_R_xml_0_non_scc_6 : forall x y, (DP_R_xml_0_non_scc_6 x y) ->Acc WF_R_xml_0_deep_rew.DP_R_xml_0 x. Proof. intros x y h. inversion h;clear h;subst; constructor;intros _y _h;inversion _h;clear _h;subst; (eapply acc_DP_R_xml_0_non_scc_2; econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))|| ((eapply acc_DP_R_xml_0_non_scc_1; econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))|| ((R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 )|| (eapply Hrec; econstructor (eassumption)||(algebra.Alg_ext.star_refl' )))). Qed. Inductive DP_R_xml_0_non_scc_7 : algebra.Alg.term ->algebra.Alg.term ->Prop := (* *) | DP_R_xml_0_non_scc_7_0 : forall x4 x2 x1 x5, (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x1 x5) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x2 x4) -> DP_R_xml_0_non_scc_7 (algebra.Alg.Term algebra.F.id_g1 (x2::x1:: x1::nil)) (algebra.Alg.Term algebra.F.id_f (x5::x4::nil)) . Lemma acc_DP_R_xml_0_non_scc_7 : forall x y, (DP_R_xml_0_non_scc_7 x y) ->Acc WF_R_xml_0_deep_rew.DP_R_xml_0 x. Proof. intros x y h. inversion h;clear h;subst; constructor;intros _y _h;inversion _h;clear _h;subst; (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' ))|| ((R_xml_0_deep_rew.impossible_star_reduction_R_xml_0 )|| (eapply Hrec; econstructor (eassumption)||(algebra.Alg_ext.star_refl' )))). Qed. Inductive DP_R_xml_0_non_scc_8 : algebra.Alg.term ->algebra.Alg.term ->Prop := (* *) | DP_R_xml_0_non_scc_8_0 : forall x4 x2 x1 x5, (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x1 x5) -> (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) x2 x4) -> DP_R_xml_0_non_scc_8 (algebra.Alg.Term algebra.F.id_g1 (x1::x1:: x2::nil)) (algebra.Alg.Term algebra.F.id_f (x5::x4::nil)) . Lemma acc_DP_R_xml_0_non_scc_8 : forall x y, (DP_R_xml_0_non_scc_8 x y) ->Acc WF_R_xml_0_deep_rew.DP_R_xml_0 x. Proof. intros x y h. inversion h;clear h;subst; constructor;intros _y _h;inversion _h;clear _h;subst; (eapply acc_DP_R_xml_0_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' ))|| ((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_8; econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))|| ((eapply acc_DP_R_xml_0_non_scc_7; econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))|| ((eapply acc_DP_R_xml_0_non_scc_6; econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))|| ((eapply acc_DP_R_xml_0_non_scc_5; econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))|| ((eapply acc_DP_R_xml_0_non_scc_4; econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))|| ((eapply acc_DP_R_xml_0_non_scc_3; econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))|| ((eapply acc_DP_R_xml_0_non_scc_2; econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))|| ((eapply acc_DP_R_xml_0_non_scc_1; econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))|| ((eapply acc_DP_R_xml_0_non_scc_0; econstructor (eassumption)||(algebra.Alg_ext.star_refl' ))|| ((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___various___06.trs/a3pat.v" *** *** End: *** *)