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_p *) | id_p : symb (* id_q *) | id_q : symb (* id_f *) | id_f : symb (* id_g *) | id_g : symb . Definition symb_eq_bool (f1 f2:symb) : bool := match f1,f2 with | id_p,id_p => true | id_q,id_q => true | id_f,id_f => true | id_g,id_g => 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_p,id_p => refl_equal _ | id_q,id_q => refl_equal _ | id_f,id_f => refl_equal _ | id_g,id_g => refl_equal _ | _,_ => _ end;intros abs;discriminate. Defined. Definition arity (f:symb) := match f with | id_p => term.Free 1 | id_q => term.Free 1 | id_f => term.Free 1 | id_g => term.Free 1 end. Definition symb_order (f1 f2:symb) : bool := match f1,f2 with | id_p,id_p => true | id_p,id_q => false | id_p,id_f => false | id_p,id_g => false | id_q,id_p => true | id_q,id_q => true | id_q,id_f => false | id_q,id_g => false | id_f,id_p => true | id_f,id_q => true | id_f,id_f => true | id_f,id_g => false | id_g,id_p => true | id_g,id_q => true | id_g,id_f => true | id_g,id_g => 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 := (* p(f(f(x_))) -> q(f(g(x_))) *) | R_xml_0_rule_0 : R_xml_0_rules (algebra.Alg.Term algebra.F.id_q ((algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Var 1)::nil))::nil))::nil)) (algebra.Alg.Term algebra.F.id_p ((algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Var 1)::nil))::nil))::nil)) (* p(g(g(x_))) -> q(g(f(x_))) *) | R_xml_0_rule_1 : R_xml_0_rules (algebra.Alg.Term algebra.F.id_q ((algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Var 1)::nil))::nil))::nil)) (algebra.Alg.Term algebra.F.id_p ((algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Var 1)::nil))::nil))::nil)) (* q(f(f(x_))) -> p(f(g(x_))) *) | R_xml_0_rule_2 : R_xml_0_rules (algebra.Alg.Term algebra.F.id_p ((algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Var 1)::nil))::nil))::nil)) (algebra.Alg.Term algebra.F.id_q ((algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Var 1)::nil))::nil))::nil)) (* q(g(g(x_))) -> p(g(f(x_))) *) | R_xml_0_rule_3 : R_xml_0_rules (algebra.Alg.Term algebra.F.id_p ((algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Var 1)::nil))::nil))::nil)) (algebra.Alg.Term algebra.F.id_q ((algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Var 1)::nil))::nil))::nil)) . Definition R_xml_0_rule_as_list_0 := ((algebra.Alg.Term algebra.F.id_p ((algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Var 1)::nil))::nil))::nil)), (algebra.Alg.Term algebra.F.id_q ((algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Var 1)::nil))::nil))::nil)))::nil. Definition R_xml_0_rule_as_list_1 := ((algebra.Alg.Term algebra.F.id_p ((algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Var 1)::nil))::nil))::nil)), (algebra.Alg.Term algebra.F.id_q ((algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Var 1)::nil))::nil))::nil)))::R_xml_0_rule_as_list_0. Definition R_xml_0_rule_as_list_2 := ((algebra.Alg.Term algebra.F.id_q ((algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Var 1)::nil))::nil))::nil)), (algebra.Alg.Term algebra.F.id_p ((algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Var 1)::nil))::nil))::nil)))::R_xml_0_rule_as_list_1. Definition R_xml_0_rule_as_list_3 := ((algebra.Alg.Term algebra.F.id_q ((algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Var 1)::nil))::nil))::nil)), (algebra.Alg.Term algebra.F.id_p ((algebra.Alg.Term algebra.F.id_g ((algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Var 1)::nil))::nil))::nil)))::R_xml_0_rule_as_list_2. Definition R_xml_0_rule_as_list := R_xml_0_rule_as_list_3. 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.or5_equiv in H|-. case H;clear H;intros H. injection H;intros ;subst;constructor 4. injection H;intros ;subst;constructor 3. injection H;intros ;subst;constructor 2. injection H;intros ;subst;constructor 1. elim H. Qed. Lemma R_xml_0_non_var : forall x t, ~R_xml_0_rules t (algebra.EQT.T.Var x). Proof. intros x t H. inversion H. Qed. Lemma R_xml_0_reg : forall s t, (R_xml_0_rules s t) -> forall x, In x (algebra.Alg.var_list s) ->In x (algebra.Alg.var_list t). Proof. intros s t H. inversion H;intros x Hx; (apply (more_list.mem_impl_in (@eq algebra.Alg.variable));[tauto|idtac]); apply (more_list.in_impl_mem (@eq algebra.Alg.variable)) in Hx; vm_compute in Hx|-*;tauto. Qed. Inductive and_2 (x3 x4:Prop) : Prop := | conj_2 : x3->x4->and_2 x3 x4 . 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_2 (forall x4, t = (algebra.Alg.Term algebra.F.id_f (x4::nil)) -> exists x3, t' = (algebra.Alg.Term algebra.F.id_f (x3::nil))/\ (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x3 x4)) (forall x4, t = (algebra.Alg.Term algebra.F.id_g (x4::nil)) -> exists x3, t' = (algebra.Alg.Term algebra.F.id_g (x3::nil))/\ (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x3 x4)). Proof. intros t t' H. induction H as [|y IH z z_to_y] using closure_extension.refl_trans_clos_ind2. constructor 1. intros x4 H;exists x4;intuition;constructor 1. intros x4 H;exists x4;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_f H_id_g]. constructor. clear H_id_g;intros x4 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 x4 |- _ => destruct (H_id_f y (refl_equal _)) as [x3];intros ;intuition;exists x3; intuition;eapply closure_extension.refl_trans_clos_R;eassumption end . clear H_id_f;intros x4 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 x4 |- _ => destruct (H_id_g y (refl_equal _)) as [x3];intros ;intuition;exists x3; intuition;eapply closure_extension.refl_trans_clos_R;eassumption end . Qed. Lemma id_f_is_R_xml_0_constructor : forall t t', (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) -> forall x4, t = (algebra.Alg.Term algebra.F.id_f (x4::nil)) -> exists x3, t' = (algebra.Alg.Term algebra.F.id_f (x3::nil))/\ (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x3 x4). 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 x4, t = (algebra.Alg.Term algebra.F.id_g (x4::nil)) -> exists x3, t' = (algebra.Alg.Term algebra.F.id_g (x3::nil))/\ (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) x3 x4). 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_f (?x3::nil)) |- _ => let x3 := fresh "x" in (let Heq := fresh "Heq" in (let Hred1 := fresh "Hred" in (destruct (id_f_is_R_xml_0_constructor H (refl_equal _)) as [x3 [Heq Hred1]]; (discriminate Heq)|| (injection Heq;intros ;subst;clear Heq;clear H; impossible_star_reduction_R_xml_0 )))) | H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) _ (algebra.Alg.Term algebra.F.id_g (?x3::nil)) |- _ => let x3 := fresh "x" in (let Heq := fresh "Heq" in (let Hred1 := fresh "Hred" in (destruct (id_g_is_R_xml_0_constructor H (refl_equal _)) as [x3 [Heq Hred1]]; (discriminate Heq)|| (injection Heq;intros ;subst;clear Heq;clear H; impossible_star_reduction_R_xml_0 )))) end . Ltac simplify_star_reduction_R_xml_0 := match goal with | H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) _ (algebra.Alg.Term algebra.F.id_f (?x3::nil)) |- _ => let x3 := fresh "x" in (let Heq := fresh "Heq" in (let Hred1 := fresh "Hred" in (destruct (id_f_is_R_xml_0_constructor H (refl_equal _)) as [x3 [Heq Hred1]]; (discriminate Heq)|| (injection Heq;intros ;subst;clear Heq;clear H; try (simplify_star_reduction_R_xml_0 ))))) | H:closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) _ (algebra.Alg.Term algebra.F.id_g (?x3::nil)) |- _ => let x3 := fresh "x" in (let Heq := fresh "Heq" in (let Hred1 := fresh "Hred" in (destruct (id_g_is_R_xml_0_constructor H (refl_equal _)) as [x3 [Heq Hred1]]; (discriminate Heq)|| (injection Heq;intros ;subst;clear Heq;clear H; try (simplify_star_reduction_R_xml_0 ))))) end . End R_xml_0_deep_rew. Module WF_R_xml_0_deep_rew. Inductive DP_R_xml_0 : algebra.Alg.term ->algebra.Alg.term ->Prop := (*
*) | DP_R_xml_0_0 : forall x1 x3, (closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules) (algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term algebra.F.id_f (x1::nil))::nil)) x3) -> DP_R_xml_0 (algebra.Alg.Term algebra.F.id_q ((algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term algebra.F.id_g (x1::nil))::nil))::nil)) (algebra.Alg.Term algebra.F.id_p (x3::nil)) (*
*)
| DP_R_xml_0_1 :
forall x1 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_g
(x1::nil))::nil)) x3) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_q ((algebra.Alg.Term
algebra.F.id_g ((algebra.Alg.Term algebra.F.id_f
(x1::nil))::nil))::nil))
(algebra.Alg.Term algebra.F.id_p (x3::nil))
(* *)
| DP_R_xml_0_non_scc_3_0 :
forall x1 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_g
(x1::nil))::nil)) x3) ->
DP_R_xml_0_non_scc_3 (algebra.Alg.Term algebra.F.id_q
((algebra.Alg.Term algebra.F.id_g
((algebra.Alg.Term algebra.F.id_f
(x1::nil))::nil))::nil))
(algebra.Alg.Term algebra.F.id_p (x3::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 x1 x3,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term algebra.F.id_f
(x1::nil))::nil)) x3) ->
DP_R_xml_0_non_scc_4 (algebra.Alg.Term algebra.F.id_q
((algebra.Alg.Term algebra.F.id_f
((algebra.Alg.Term algebra.F.id_g
(x1::nil))::nil))::nil))
(algebra.Alg.Term algebra.F.id_p (x3::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___AG01___3.33.trs/a3pat.v" ***
*** End: ***
*)
*)
| DP_R_xml_0_2 :
forall x1 x3,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term algebra.F.id_f
(x1::nil))::nil)) x3) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_p ((algebra.Alg.Term
algebra.F.id_f ((algebra.Alg.Term algebra.F.id_g
(x1::nil))::nil))::nil))
(algebra.Alg.Term algebra.F.id_q (x3::nil))
(*
*)
| DP_R_xml_0_3 :
forall x1 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_g
(x1::nil))::nil)) x3) ->
DP_R_xml_0 (algebra.Alg.Term algebra.F.id_p ((algebra.Alg.Term
algebra.F.id_g ((algebra.Alg.Term algebra.F.id_f
(x1::nil))::nil))::nil))
(algebra.Alg.Term algebra.F.id_q (x3::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 x1 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_g
(x1::nil))::nil)) x3) ->
DP_R_xml_0_non_scc_1 (algebra.Alg.Term algebra.F.id_p
((algebra.Alg.Term algebra.F.id_g
((algebra.Alg.Term algebra.F.id_f
(x1::nil))::nil))::nil))
(algebra.Alg.Term algebra.F.id_q (x3::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 x1 x3,
(closure.refl_trans_clos (algebra.EQT.one_step R_xml_0_deep_rew.R_xml_0_rules)
(algebra.Alg.Term algebra.F.id_f ((algebra.Alg.Term algebra.F.id_f
(x1::nil))::nil)) x3) ->
DP_R_xml_0_non_scc_2 (algebra.Alg.Term algebra.F.id_p
((algebra.Alg.Term algebra.F.id_f
((algebra.Alg.Term algebra.F.id_g
(x1::nil))::nil))::nil))
(algebra.Alg.Term algebra.F.id_q (x3::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 :=
(*