API tools faq
paste
Advertisement
Guest User

Untitled

a guest
Jul 19th, 2017
76
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
COBOL 124.11 KB | None | 0 0
raw download clone embed print report
  1. Require terminaison.
  2.  
  3. Require Relations.
  4.  
  5. Require term.
  6.  
  7. Require List.
  8.  
  9. Require equational_theory.
  10.  
  11. Require rpo_extension.
  12.  
  13. Require equational_extension.
  14.  
  15. Require closure_extension.
  16.  
  17. Require term_extension.
  18.  
  19. Require dp.
  20.  
  21. Require Inclusion.
  22.  
  23. Require or_ext_generated.
  24.  
  25. Require ZArith.
  26.  
  27. Require ring_extention.
  28.  
  29. Require ring_extention2.
  30.  
  31. Require Zwf.
  32.  
  33. Require Inverse_Image.
  34.  
  35. Require matrix.
  36.  
  37. Require more_list_extention.
  38.  
  39. Require graph_dp.
  40.  
  41. Require subterm_dp.
  42.  
  43. Import List.
  44.  
  45. Import ZArith.
  46.  
  47. Set Implicit Arguments.
  48.  
  49. Module algebra.
  50.  Module F
  51.   <:term_spec.Signature.
  52.   Inductive symb  :
  53.    Set :=
  54.      (* id_u22 *)
  55.     | id_u22 : symb
  56.      (* id_ack_in *)
  57.     | id_ack_in : symb
  58.      (* id_0 *)
  59.     | id_0 : symb
  60.      (* id_ack_out *)
  61.     | id_ack_out : symb
  62.      (* id_s *)
  63.     | id_s : symb
  64.      (* id_u21 *)
  65.     | id_u21 : symb
  66.      (* id_u11 *)
  67.     | id_u11 : symb
  68.   .
  69.  
  70.  
  71.   Definition symb_eq_bool (f1 f2:symb) : bool :=
  72.     match f1,f2 with
  73.       | id_u22,id_u22 => true
  74.       | id_ack_in,id_ack_in => true
  75.       | id_0,id_0 => true
  76.       | id_ack_out,id_ack_out => true
  77.       | id_s,id_s => true
  78.       | id_u21,id_u21 => true
  79.       | id_u11,id_u11 => true
  80.       | _,_ => false
  81.       end.
  82.  
  83.  
  84.    (* Proof of decidability of equality over symb *)
  85.   Definition symb_eq_bool_ok(f1 f2:symb) :
  86.    match symb_eq_bool f1 f2 with
  87.      | true => f1 = f2
  88.      | false => f1 <> f2
  89.      end.
  90.   Proof.
  91.     intros f1 f2.
  92.    
  93.     refine match f1 as u1,f2 as u2 return
  94.              match symb_eq_bool u1 u2 return
  95.                Prop with
  96.                | true => u1 = u2
  97.                | false => u1 <> u2
  98.                end with
  99.              | id_u22,id_u22 => refl_equal _
  100.              | id_ack_in,id_ack_in => refl_equal _
  101.              | id_0,id_0 => refl_equal _
  102.              | id_ack_out,id_ack_out => refl_equal _
  103.              | id_s,id_s => refl_equal _
  104.              | id_u21,id_u21 => refl_equal _
  105.              | id_u11,id_u11 => refl_equal _
  106.              | _,_ => _
  107.              end;intros abs;discriminate.
  108.   Defined.
  109.  
  110.  
  111.   Definition arity (f:symb) :=
  112.     match f with
  113.       | id_u22 => term_spec.Free 1
  114.       | id_ack_in => term_spec.Free 2
  115.       | id_0 => term_spec.Free 0
  116.       | id_ack_out => term_spec.Free 1
  117.       | id_s => term_spec.Free 1
  118.       | id_u21 => term_spec.Free 2
  119.       | id_u11 => term_spec.Free 1
  120.       end.
  121.  
  122.  
  123.   Definition symb_order (f1 f2:symb) : bool :=
  124.     match f1,f2 with
  125.       | id_u22,id_u22 => true
  126.       | id_u22,id_ack_in => false
  127.       | id_u22,id_0 => false
  128.       | id_u22,id_ack_out => false
  129.       | id_u22,id_s => false
  130.       | id_u22,id_u21 => false
  131.       | id_u22,id_u11 => false
  132.       | id_ack_in,id_u22 => true
  133.       | id_ack_in,id_ack_in => true
  134.       | id_ack_in,id_0 => false
  135.       | id_ack_in,id_ack_out => false
  136.       | id_ack_in,id_s => false
  137.       | id_ack_in,id_u21 => false
  138.       | id_ack_in,id_u11 => false
  139.       | id_0,id_u22 => true
  140.       | id_0,id_ack_in => true
  141.       | id_0,id_0 => true
  142.       | id_0,id_ack_out => false
  143.       | id_0,id_s => false
  144.       | id_0,id_u21 => false
  145.       | id_0,id_u11 => false
  146.       | id_ack_out,id_u22 => true
  147.       | id_ack_out,id_ack_in => true
  148.       | id_ack_out,id_0 => true
  149.       | id_ack_out,id_ack_out => true
  150.       | id_ack_out,id_s => false
  151.       | id_ack_out,id_u21 => false
  152.       | id_ack_out,id_u11 => false
  153.       | id_s,id_u22 => true
  154.       | id_s,id_ack_in => true
  155.       | id_s,id_0 => true
  156.       | id_s,id_ack_out => true
  157.       | id_s,id_s => true
  158.       | id_s,id_u21 => false
  159.       | id_s,id_u11 => false
  160.       | id_u21,id_u22 => true
  161.       | id_u21,id_ack_in => true
  162.       | id_u21,id_0 => true
  163.       | id_u21,id_ack_out => true
  164.       | id_u21,id_s => true
  165.       | id_u21,id_u21 => true
  166.       | id_u21,id_u11 => false
  167.       | id_u11,id_u22 => true
  168.       | id_u11,id_ack_in => true
  169.       | id_u11,id_0 => true
  170.       | id_u11,id_ack_out => true
  171.       | id_u11,id_s => true
  172.       | id_u11,id_u21 => true
  173.       | id_u11,id_u11 => true
  174.       end.
  175.  
  176.  
  177.   Module Symb.
  178.    Definition A  := symb.
  179.    
  180.    Definition eq_A  := @eq A.
  181.    
  182.    
  183.    Definition eq_proof : equivalence A eq_A.
  184.    Proof.
  185.      constructor.
  186.      red ;reflexivity .
  187.      red ;intros ;transitivity y ;assumption.
  188.      red ;intros ;symmetry ;assumption.
  189.    Defined.
  190.    
  191.    
  192.    Add Relation A eq_A
  193.   reflexivity proved by (@equiv_refl _ _ eq_proof)
  194.     symmetry proved by (@equiv_sym _ _ eq_proof)
  195.       transitivity proved by (@equiv_trans _ _ eq_proof) as EQA
  196. .
  197.    
  198.    Definition eq_bool  := symb_eq_bool.
  199.    
  200.    Definition eq_bool_ok  := symb_eq_bool_ok.
  201.   End Symb.
  202.  
  203.   Export Symb.
  204.  End F.
  205.  
  206.  Module Alg := term.Make'(F)(term_extension.IntVars).
  207.  
  208. Module Alg_ext := term_extension.Make(Alg).
  209.  
  210. Module EQT := equational_theory.Make(Alg).
  211.  
  212. Module EQT_ext := equational_extension.Make(EQT).
  213. End algebra.
  214.  
  215. Inductive R_xml_0_rules  :
  216. algebra.Alg.term ->algebra.Alg.term ->Prop :=
  217.   (* ack_in(0,n) -> ack_out(s(n)) *)
  218.  | R_xml_0_rule_0 :
  219.   R_xml_0_rules (algebra.Alg.Term algebra.F.id_ack_out ((algebra.Alg.Term
  220.                  algebra.F.id_s ((algebra.Alg.Var 1)::nil))::nil))
  221.    (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term algebra.F.id_0
  222.     nil)::(algebra.Alg.Var 1)::nil))
  223.   (* ack_in(s(m),0) -> u11(ack_in(m,s(0))) *)
  224.  | R_xml_0_rule_1 :
  225.   R_xml_0_rules (algebra.Alg.Term algebra.F.id_u11 ((algebra.Alg.Term
  226.                  algebra.F.id_ack_in ((algebra.Alg.Var 2)::
  227.                  (algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Term
  228.                  algebra.F.id_0 nil)::nil))::nil))::nil))
  229.    (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term algebra.F.id_s
  230.     ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Term algebra.F.id_0
  231.     nil)::nil))
  232.   (* u11(ack_out(n)) -> ack_out(n) *)
  233.  | R_xml_0_rule_2 :
  234.   R_xml_0_rules (algebra.Alg.Term algebra.F.id_ack_out
  235.                  ((algebra.Alg.Var 1)::nil))
  236.    (algebra.Alg.Term algebra.F.id_u11 ((algebra.Alg.Term
  237.     algebra.F.id_ack_out ((algebra.Alg.Var 1)::nil))::nil))
  238.   (* ack_in(s(m),s(n)) -> u21(ack_in(s(m),n),m) *)
  239.  | R_xml_0_rule_3 :
  240.   R_xml_0_rules (algebra.Alg.Term algebra.F.id_u21 ((algebra.Alg.Term
  241.                  algebra.F.id_ack_in ((algebra.Alg.Term algebra.F.id_s
  242.                  ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Var 1)::nil))::
  243.                  (algebra.Alg.Var 2)::nil))
  244.    (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term algebra.F.id_s
  245.     ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Term algebra.F.id_s
  246.     ((algebra.Alg.Var 1)::nil))::nil))
  247.   (* u21(ack_out(n),m) -> u22(ack_in(m,n)) *)
  248.  | R_xml_0_rule_4 :
  249.   R_xml_0_rules (algebra.Alg.Term algebra.F.id_u22 ((algebra.Alg.Term
  250.                  algebra.F.id_ack_in ((algebra.Alg.Var 2)::
  251.                  (algebra.Alg.Var 1)::nil))::nil))
  252.    (algebra.Alg.Term algebra.F.id_u21 ((algebra.Alg.Term
  253.     algebra.F.id_ack_out ((algebra.Alg.Var 1)::nil))::
  254.     (algebra.Alg.Var 2)::nil))
  255.   (* u22(ack_out(n)) -> ack_out(n) *)
  256.  | R_xml_0_rule_5 :
  257.   R_xml_0_rules (algebra.Alg.Term algebra.F.id_ack_out
  258.                  ((algebra.Alg.Var 1)::nil))
  259.    (algebra.Alg.Term algebra.F.id_u22 ((algebra.Alg.Term
  260.     algebra.F.id_ack_out ((algebra.Alg.Var 1)::nil))::nil))
  261. .
  262.  
  263. Module WF_R_xml_0.
  264. Definition R_xml_0_rule_as_list_0  :=
  265.   ((algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term algebra.F.id_0
  266.     nil)::(algebra.Alg.Var 1)::nil)),
  267.    (algebra.Alg.Term algebra.F.id_ack_out ((algebra.Alg.Term algebra.F.id_s
  268.     ((algebra.Alg.Var 1)::nil))::nil)))::nil.
  269.  
  270. Definition R_xml_0_rule_as_list_1  :=
  271.   ((algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term algebra.F.id_s
  272.     ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Term algebra.F.id_0
  273.     nil)::nil)),
  274.    (algebra.Alg.Term algebra.F.id_u11 ((algebra.Alg.Term
  275.     algebra.F.id_ack_in ((algebra.Alg.Var 2)::(algebra.Alg.Term
  276.     algebra.F.id_s ((algebra.Alg.Term algebra.F.id_0
  277.     nil)::nil))::nil))::nil)))::R_xml_0_rule_as_list_0.
  278.  
  279. Definition R_xml_0_rule_as_list_2  :=
  280.   ((algebra.Alg.Term algebra.F.id_u11 ((algebra.Alg.Term
  281.     algebra.F.id_ack_out ((algebra.Alg.Var 1)::nil))::nil)),
  282.    (algebra.Alg.Term algebra.F.id_ack_out ((algebra.Alg.Var 1)::nil)))::
  283.    R_xml_0_rule_as_list_1.
  284.  
  285. Definition R_xml_0_rule_as_list_3  :=
  286.   ((algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term algebra.F.id_s
  287.     ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Term algebra.F.id_s
  288.     ((algebra.Alg.Var 1)::nil))::nil)),
  289.    (algebra.Alg.Term algebra.F.id_u21 ((algebra.Alg.Term
  290.     algebra.F.id_ack_in ((algebra.Alg.Term algebra.F.id_s
  291.     ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Var 1)::nil))::
  292.     (algebra.Alg.Var 2)::nil)))::R_xml_0_rule_as_list_2.
  293.  
  294. Definition R_xml_0_rule_as_list_4  :=
  295.   ((algebra.Alg.Term algebra.F.id_u21 ((algebra.Alg.Term
  296.     algebra.F.id_ack_out ((algebra.Alg.Var 1)::nil))::
  297.     (algebra.Alg.Var 2)::nil)),
  298.    (algebra.Alg.Term algebra.F.id_u22 ((algebra.Alg.Term
  299.     algebra.F.id_ack_in ((algebra.Alg.Var 2)::
  300.     (algebra.Alg.Var 1)::nil))::nil)))::R_xml_0_rule_as_list_3.
  301.  
  302. Definition R_xml_0_rule_as_list_5  :=
  303.   ((algebra.Alg.Term algebra.F.id_u22 ((algebra.Alg.Term
  304.     algebra.F.id_ack_out ((algebra.Alg.Var 1)::nil))::nil)),
  305.    (algebra.Alg.Term algebra.F.id_ack_out ((algebra.Alg.Var 1)::nil)))::
  306.    R_xml_0_rule_as_list_4.
  307.  
  308. Definition R_xml_0_rule_as_list  := R_xml_0_rule_as_list_5.
  309.  
  310. Lemma R_xml_0_rules_included :
  311.  forall l r, R_xml_0_rules r l <-> In (l,r) R_xml_0_rule_as_list.
  312. Proof.
  313.   intros l r.
  314.   constructor.
  315.   intros H.
  316.  
  317.   case H;clear H;
  318.    (apply (more_list.mem_impl_in (@eq (algebra.Alg.term*algebra.Alg.term)));
  319.     [tauto|idtac]);
  320.    match goal with
  321.      |  |- _ _ _ ?t ?l =>
  322.       let u := fresh "u" in
  323.        (generalize (more_list.mem_bool_ok _ _
  324.                      algebra.Alg_ext.eq_term_term_bool_ok t l);
  325.          set (u:=more_list.mem_bool algebra.Alg_ext.eq_term_term_bool t l) in *;
  326.          vm_compute in u|-;unfold u in *;clear u;intros H;refine H)
  327.      end
  328.    .
  329.   intros H.
  330.   vm_compute in H|-.
  331.   rewrite  <- or_ext_generated.or7_equiv in H|-.
  332.   case H;clear H;intros H.
  333.   injection H;intros ;subst;constructor 6.
  334.   injection H;intros ;subst;constructor 5.
  335.   injection H;intros ;subst;constructor 4.
  336.   injection H;intros ;subst;constructor 3.
  337.   injection H;intros ;subst;constructor 2.
  338.   injection H;intros ;subst;constructor 1.
  339.   elim H.
  340. Qed.
  341.  
  342. Lemma R_xml_0_non_var : forall x t, ~R_xml_0_rules t (algebra.EQT.T.Var x).
  343. Proof.
  344.   intros x t H.
  345.   inversion H.
  346. Qed.
  347.  
  348. Lemma R_xml_0_reg :
  349.  forall s t,
  350.   (R_xml_0_rules s t) ->
  351.    forall x, In x (algebra.Alg.var_list s) ->In x (algebra.Alg.var_list t).
  352. Proof.
  353.   intros s t H.
  354.  
  355.   inversion H;intros x Hx;
  356.    (apply (more_list.mem_impl_in (@eq algebra.Alg.variable));[tauto|idtac]);
  357.    apply (more_list.in_impl_mem (@eq algebra.Alg.variable)) in Hx;
  358.    vm_compute in Hx|-*;tauto.
  359. Qed.
  360.  
  361. Inductive and_3 (x4 x5 x6:Prop) :
  362.  Prop :=
  363.   | conj_3 : x4->x5->x6->and_3 x4 x5 x6
  364. .
  365.  
  366. Lemma are_constuctors_of_R_xml_0 :
  367.  forall t t',
  368.    (TransClosure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
  369.    and_3 (t = (algebra.Alg.Term algebra.F.id_0 nil) ->
  370.           t' = (algebra.Alg.Term algebra.F.id_0 nil))
  371.      (forall x5,
  372.       t = (algebra.Alg.Term algebra.F.id_ack_out (x5::nil)) ->
  373.        exists x4,
  374.          t' = (algebra.Alg.Term algebra.F.id_ack_out (x4::nil))/\
  375.         (TransClosure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
  376.           x4 x5))
  377.     (forall x5,
  378.      t = (algebra.Alg.Term algebra.F.id_s (x5::nil)) ->
  379.       exists x4,
  380.         t' = (algebra.Alg.Term algebra.F.id_s (x4::nil))/\
  381.          (TransClosure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
  382.            x4 x5)).
  383.  Proof.
  384.    intros t t' H.
  385.  
  386.   induction H as [|y IH z z_to_y] using
  387.   closure_extension.refl_trans_clos_ind2.
  388.   constructor 1.
  389.   intros H;intuition;constructor 1.
  390.   intros x5 H;exists x5;intuition;constructor 1.
  391.   intros x5 H;exists x5;intuition;constructor 1.
  392.   inversion z_to_y as [t1 t2 H H0 H1|f l1 l2 H0 H H2];clear z_to_y;subst.
  393.  
  394.   inversion H as [t1 t2 sigma H2 H1 H0];clear H IH;subst;inversion H2;
  395.    clear ;constructor;try (intros until 0 );clear ;intros abs;
  396.    discriminate abs.
  397.   destruct IH as [H_id_0 H_id_ack_out H_id_s].
  398.   constructor.
  399.  
  400.   clear H_id_ack_out H_id_s;intros H;injection H;clear H;intros ;subst;
  401.    repeat (
  402.    match goal with
  403.      | H:weaved_relation.one_step_list (algebra.EQT.one_step _) _ _ |-
  404.      _ => inversion H;clear H;subst
  405.      end
  406.    ).
  407.  
  408.   clear H_id_0 H_id_s;intros x5 H;injection H;clear H;intros ;subst;
  409.    repeat (
  410.    match goal with
  411.      | H:weaved_relation.one_step_list (algebra.EQT.one_step _) _ _ |-
  412.      _ => inversion H;clear H;subst
  413.      end
  414.    ).
  415.  
  416.   match goal with
  417.     | H:algebra.EQT.one_step _ ?y x5 |- _ =>
  418.      destruct (H_id_ack_out y (refl_equal _)) as [x4];intros ;intuition;
  419.       exists x4;intuition;eapply closure_extension.refl_trans_clos_R;
  420.       eassumption
  421.     end
  422.   .
  423.  
  424.   clear H_id_0 H_id_ack_out;intros x5 H;injection H;clear H;intros ;
  425.    subst;
  426.    repeat (
  427.    match goal with
  428.      | H:weaved_relation.one_step_list (algebra.EQT.one_step _) _ _ |-
  429.      _ => inversion H;clear H;subst
  430.      end
  431.    ).
  432.  
  433.   match goal with
  434.     | H:algebra.EQT.one_step _ ?y x5 |- _ =>
  435.      destruct (H_id_s y (refl_equal _)) as [x4];intros ;intuition;exists x4;
  436.       intuition;eapply closure_extension.refl_trans_clos_R;eassumption
  437.     end
  438.   .
  439. Qed.
  440.  
  441. Lemma id_0_is_R_xml_0_constructor :
  442.  forall t t',
  443.    (TransClosure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
  444.    t = (algebra.Alg.Term algebra.F.id_0 nil) ->
  445.     t' = (algebra.Alg.Term algebra.F.id_0 nil).
  446.  Proof.
  447.    intros t t' H.
  448.   destruct (are_constuctors_of_R_xml_0 H).
  449.   assumption.
  450. Qed.
  451.  
  452. Lemma id_ack_out_is_R_xml_0_constructor :
  453.  forall t t',
  454.    (TransClosure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
  455.    forall x5,
  456.     t = (algebra.Alg.Term algebra.F.id_ack_out (x5::nil)) ->
  457.      exists x4,
  458.        t' = (algebra.Alg.Term algebra.F.id_ack_out (x4::nil))/\
  459.         (TransClosure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
  460.           x4 x5).
  461.  Proof.
  462.    intros t t' H.
  463.   destruct (are_constuctors_of_R_xml_0 H).
  464.   assumption.
  465. Qed.
  466.  
  467. Lemma id_s_is_R_xml_0_constructor :
  468.  forall t t',
  469.    (TransClosure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) t' t) ->
  470.    forall x5,
  471.     t = (algebra.Alg.Term algebra.F.id_s (x5::nil)) ->
  472.      exists x4,
  473.        t' = (algebra.Alg.Term algebra.F.id_s (x4::nil))/\
  474.         (TransClosure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
  475.           x4 x5).
  476.  Proof.
  477.    intros t t' H.
  478.   destruct (are_constuctors_of_R_xml_0 H).
  479.   assumption.
  480. Qed.
  481.  
  482. Ltac impossible_star_reduction_R_xml_0  :=
  483.  match goal with
  484.    | H:TransClosure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
  485.         _ (algebra.Alg.Term algebra.F.id_0 nil) |- _ =>
  486.     let Heq := fresh "Heq" in
  487.      (set (Heq:=id_0_is_R_xml_0_constructor H (refl_equal _)) in *;
  488.        (discriminate Heq)||
  489.        (clearbody Heq;try (subst);try (clear Heq);clear H;
  490.          impossible_star_reduction_R_xml_0 ))
  491.    | H:TransClosure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
  492.         _ (algebra.Alg.Term algebra.F.id_ack_out (?x4::nil)) |- _ =>
  493.     let x4 := fresh "x" in
  494.      (let Heq := fresh "Heq" in
  495.        (let Hred1 := fresh "Hred" in
  496.          (destruct (id_ack_out_is_R_xml_0_constructor H (refl_equal _)) as
  497.           [x4 [Heq Hred1]];
  498.            (discriminate Heq)||
  499.            (injection Heq;intros ;subst;clear Heq;clear H;
  500.              impossible_star_reduction_R_xml_0 ))))
  501.    | H:TransClosure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
  502.         _ (algebra.Alg.Term algebra.F.id_s (?x4::nil)) |- _ =>
  503.     let x4 := fresh "x" in
  504.      (let Heq := fresh "Heq" in
  505.        (let Hred1 := fresh "Hred" in
  506.          (destruct (id_s_is_R_xml_0_constructor H (refl_equal _)) as
  507.           [x4 [Heq Hred1]];
  508.            (discriminate Heq)||
  509.            (injection Heq;intros ;subst;clear Heq;clear H;
  510.              impossible_star_reduction_R_xml_0 ))))
  511.    end
  512.  .
  513.  
  514. Ltac simplify_star_reduction_R_xml_0  :=
  515.  match goal with
  516.    | H:TransClosure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
  517.         _ (algebra.Alg.Term algebra.F.id_0 nil) |- _ =>
  518.     let Heq := fresh "Heq" in
  519.      (set (Heq:=id_0_is_R_xml_0_constructor H (refl_equal _)) in *;
  520.        (discriminate Heq)||
  521.        (clearbody Heq;try (subst);try (clear Heq);clear H;
  522.          try (simplify_star_reduction_R_xml_0 )))
  523.    | H:TransClosure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
  524.         _ (algebra.Alg.Term algebra.F.id_ack_out (?x4::nil)) |- _ =>
  525.     let x4 := fresh "x" in
  526.      (let Heq := fresh "Heq" in
  527.        (let Hred1 := fresh "Hred" in
  528.          (destruct (id_ack_out_is_R_xml_0_constructor H (refl_equal _)) as
  529.           [x4 [Heq Hred1]];
  530.            (discriminate Heq)||
  531.            (injection Heq;intros ;subst;clear Heq;clear H;
  532.              try (simplify_star_reduction_R_xml_0 )))))
  533.    | H:TransClosure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules)
  534.         _ (algebra.Alg.Term algebra.F.id_s (?x4::nil)) |- _ =>
  535.     let x4 := fresh "x" in
  536.      (let Heq := fresh "Heq" in
  537.        (let Hred1 := fresh "Hred" in
  538.          (destruct (id_s_is_R_xml_0_constructor H (refl_equal _)) as
  539.           [x4 [Heq Hred1]];
  540.            (discriminate Heq)||
  541.            (injection Heq;intros ;subst;clear Heq;clear H;
  542.              try (simplify_star_reduction_R_xml_0 )))))
  543.    end
  544.  .
  545.  
  546. Module InterpGen := interp.Interp(algebra.EQT).
  547.  
  548. Module ddp := dp.MakeDP(algebra.EQT).
  549.  
  550. Module subdp := subterm_dp.MakeSubDP(algebra.EQT).
  551.  
  552. Module SymbType. Definition A := algebra.Alg.F.Symb.A. End SymbType.
  553.  
  554.  
  555. Module Symb_more_list := more_list_extention.Make(SymbType)(algebra.Alg.F.Symb).
  556.  
  557. Module SymbSet := list_set.Make(algebra.F.Symb).
  558.  
  559.  
  560. Module Interp.
  561.  Section S.
  562.    Require Import interp.
  563.    
  564.    Hypothesis A : Type.
  565.    
  566.    Hypothesis Ale Alt Aeq : A -> A -> Prop.
  567.    
  568.    Hypothesis Aop : interp.ordering_pair Aeq Alt Ale.
  569.    
  570.    Hypothesis A0 : A.
  571.    
  572.    Notation Local "a <= b" := (Ale a b).
  573.    
  574.    Hypothesis P_id_u22 : A ->A.
  575.    
  576.    Hypothesis P_id_ack_in : A ->A ->A.
  577.    
  578.    Hypothesis P_id_0 : A.
  579.    
  580.    Hypothesis P_id_ack_out : A ->A.
  581.    
  582.    Hypothesis P_id_s : A ->A.
  583.    
  584.    Hypothesis P_id_u21 : A ->A ->A.
  585.    
  586.    Hypothesis P_id_u11 : A ->A.
  587.    
  588.    Hypothesis P_id_u22_monotonic :
  589.     forall x4 x5, (A0 <= x5)/\ (x5 <= x4) ->P_id_u22 x5 <= P_id_u22 x4.
  590.    
  591.    Hypothesis P_id_ack_in_monotonic :
  592.     forall x4 x6 x5 x7,
  593.      (A0 <= x7)/\ (x7 <= x6) ->
  594.       (A0 <= x5)/\ (x5 <= x4) ->P_id_ack_in x5 x7 <= P_id_ack_in x4 x6.
  595.    
  596.    Hypothesis P_id_ack_out_monotonic :
  597.     forall x4 x5,
  598.      (A0 <= x5)/\ (x5 <= x4) ->P_id_ack_out x5 <= P_id_ack_out x4.
  599.    
  600.    Hypothesis P_id_s_monotonic :
  601.     forall x4 x5, (A0 <= x5)/\ (x5 <= x4) ->P_id_s x5 <= P_id_s x4.
  602.    
  603.    Hypothesis P_id_u21_monotonic :
  604.     forall x4 x6 x5 x7,
  605.      (A0 <= x7)/\ (x7 <= x6) ->
  606.       (A0 <= x5)/\ (x5 <= x4) ->P_id_u21 x5 x7 <= P_id_u21 x4 x6.
  607.    
  608.    Hypothesis P_id_u11_monotonic :
  609.     forall x4 x5, (A0 <= x5)/\ (x5 <= x4) ->P_id_u11 x5 <= P_id_u11 x4.
  610.    
  611.    Hypothesis P_id_u22_bounded : forall x4, (A0 <= x4) ->A0 <= P_id_u22 x4.
  612.    
  613.    Hypothesis P_id_ack_in_bounded :
  614.     forall x4 x5, (A0 <= x4) ->(A0 <= x5) ->A0 <= P_id_ack_in x5 x4.
  615.    
  616.    Hypothesis P_id_0_bounded : A0 <= P_id_0 .
  617.    
  618.    Hypothesis P_id_ack_out_bounded :
  619.     forall x4, (A0 <= x4) ->A0 <= P_id_ack_out x4.
  620.    
  621.    Hypothesis P_id_s_bounded : forall x4, (A0 <= x4) ->A0 <= P_id_s x4.
  622.    
  623.    Hypothesis P_id_u21_bounded :
  624.     forall x4 x5, (A0 <= x4) ->(A0 <= x5) ->A0 <= P_id_u21 x5 x4.
  625.    
  626.    Hypothesis P_id_u11_bounded : forall x4, (A0 <= x4) ->A0 <= P_id_u11 x4.
  627.    
  628.    Fixpoint measure t { struct t }  :=
  629.      match t with
  630.        | (algebra.Alg.Term algebra.F.id_u22 (x4::nil)) =>
  631.         P_id_u22 (measure x4)
  632.        | (algebra.Alg.Term algebra.F.id_ack_in (x5::x4::nil)) =>
  633.         P_id_ack_in (measure x5) (measure x4)
  634.        | (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0
  635.        | (algebra.Alg.Term algebra.F.id_ack_out (x4::nil)) =>
  636.         P_id_ack_out (measure x4)
  637.        | (algebra.Alg.Term algebra.F.id_s (x4::nil)) => P_id_s (measure x4)
  638.        | (algebra.Alg.Term algebra.F.id_u21 (x5::x4::nil)) =>
  639.         P_id_u21 (measure x5) (measure x4)
  640.        | (algebra.Alg.Term algebra.F.id_u11 (x4::nil)) =>
  641.         P_id_u11 (measure x4)
  642.        | _ => A0
  643.        end.
  644.    
  645.    Lemma measure_equation :
  646.     forall t,
  647.      measure t = match t with
  648.                    | (algebra.Alg.Term algebra.F.id_u22 (x4::nil)) =>
  649.                     P_id_u22 (measure x4)
  650.                    | (algebra.Alg.Term algebra.F.id_ack_in (x5::x4::nil)) =>
  651.                     P_id_ack_in (measure x5) (measure x4)
  652.                    | (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0
  653.                    | (algebra.Alg.Term algebra.F.id_ack_out (x4::nil)) =>
  654.                     P_id_ack_out (measure x4)
  655.                    | (algebra.Alg.Term algebra.F.id_s (x4::nil)) =>
  656.                     P_id_s (measure x4)
  657.                    | (algebra.Alg.Term algebra.F.id_u21 (x5::x4::nil)) =>
  658.                     P_id_u21 (measure x5) (measure x4)
  659.                    | (algebra.Alg.Term algebra.F.id_u11 (x4::nil)) =>
  660.                     P_id_u11 (measure x4)
  661.                    | _ => A0
  662.                    end.
  663.    Proof.
  664.      intros t;
  665.       refine match t with
  666.                | (algebra.Alg.Term algebra.F.id_u22 (x4::nil)) => _
  667.                | (algebra.Alg.Term algebra.F.id_ack_in (x5::x4::nil)) =>
  668.                _
  669.                | (algebra.Alg.Term algebra.F.id_0 nil) => _
  670.                | (algebra.Alg.Term algebra.F.id_ack_out (x4::nil)) =>
  671.                _
  672.                | (algebra.Alg.Term algebra.F.id_s (x4::nil)) => _
  673.                | (algebra.Alg.Term algebra.F.id_u21 (x5::x4::nil)) =>
  674.                _
  675.                | (algebra.Alg.Term algebra.F.id_u11 (x4::nil)) => _
  676.                | _ => _
  677.                end;apply refl_equal.
  678.    Qed.
  679.    
  680.    Definition Pols f : InterpGen.Pol_type A (InterpGen.get_arity f) :=
  681.      match f with
  682.        | algebra.F.id_u22 => P_id_u22
  683.        | algebra.F.id_ack_in => P_id_ack_in
  684.        | algebra.F.id_0 => P_id_0
  685.        | algebra.F.id_ack_out => P_id_ack_out
  686.        | algebra.F.id_s => P_id_s
  687.        | algebra.F.id_u21 => P_id_u21
  688.        | algebra.F.id_u11 => P_id_u11
  689.        end.
  690.    
  691.    Lemma same_measure : forall t, measure t = InterpGen.measure A0 Pols t.
  692.    Proof.
  693.      fix 1 .
  694.      intros [a| f l].
  695.      simpl in |-*.
  696.      unfold eq_rect_r, eq_rect, sym_eq in |-*.
  697.      reflexivity .
  698.      
  699.      refine match f with
  700.               | algebra.F.id_u22 =>
  701.                match l with
  702.                  | nil => _
  703.                  | _::nil => _
  704.                  | _::_::_ => _
  705.                  end
  706.               | algebra.F.id_ack_in =>
  707.                match l with
  708.                  | nil => _
  709.                  | _::nil => _
  710.                  | _::_::nil => _
  711.                  | _::_::_::_ => _
  712.                  end
  713.               | algebra.F.id_0 => match l with
  714.                                     | nil => _
  715.                                     | _::_ => _
  716.                                     end
  717.               | algebra.F.id_ack_out =>
  718.                match l with
  719.                  | nil => _
  720.                  | _::nil => _
  721.                  | _::_::_ => _
  722.                  end
  723.               | algebra.F.id_s =>
  724.                match l with
  725.                  | nil => _
  726.                  | _::nil => _
  727.                  | _::_::_ => _
  728.                  end
  729.               | algebra.F.id_u21 =>
  730.                match l with
  731.                  | nil => _
  732.                  | _::nil => _
  733.                  | _::_::nil => _
  734.                  | _::_::_::_ => _
  735.                  end
  736.               | algebra.F.id_u11 =>
  737.                match l with
  738.                  | nil => _
  739.                  | _::nil => _
  740.                  | _::_::_ => _
  741.                  end
  742.               end;simpl in |-*;unfold eq_rect_r, eq_rect, sym_eq in |-*;
  743.       try (reflexivity );f_equal ;auto.
  744.    Qed.
  745.    
  746.    Lemma measure_bounded : forall t, A0 <= measure t.
  747.    Proof.
  748.      intros t.
  749.      rewrite same_measure in |-*.
  750.      apply (InterpGen.measure_bounded Aop).
  751.      intros f.
  752.      case f.
  753.      vm_compute in |-*;intros ;apply P_id_u22_bounded;assumption.
  754.      vm_compute in |-*;intros ;apply P_id_ack_in_bounded;assumption.
  755.      vm_compute in |-*;intros ;apply P_id_0_bounded;assumption.
  756.      vm_compute in |-*;intros ;apply P_id_ack_out_bounded;assumption.
  757.      vm_compute in |-*;intros ;apply P_id_s_bounded;assumption.
  758.      vm_compute in |-*;intros ;apply P_id_u21_bounded;assumption.
  759.      vm_compute in |-*;intros ;apply P_id_u11_bounded;assumption.
  760.    Qed.
  761.    
  762.    Ltac generate_pos_hyp  :=
  763.     match goal with
  764.       | H:context [measure ?x] |- _ =>
  765.        let v := fresh "v" in
  766.         (let H := fresh "h" in
  767.           (set (H:=measure_bounded x) in *;set (v:=measure x) in *;
  768.             clearbody H;clearbody v))
  769.       |  |- context [measure ?x] =>
  770.        let v := fresh "v" in
  771.         (let H := fresh "h" in
  772.           (set (H:=measure_bounded x) in *;set (v:=measure x) in *;
  773.             clearbody H;clearbody v))
  774.       end
  775.     .
  776.    
  777.    Hypothesis rules_monotonic :
  778.     forall l r,
  779.      (algebra.EQT.axiom R_xml_0_rules r l) ->measure r <= measure l.
  780.    
  781.    Lemma measure_star_monotonic :
  782.     forall l r,
  783.      (TransClosure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) r l) ->
  784.       measure r <= measure l.
  785.    Proof.
  786.      intros .
  787.      do 2 (rewrite same_measure in |-*).
  788.      
  789.      apply InterpGen.measure_star_monotonic with (1:=Aop) (Pols:=Pols)
  790.      (rules:=R_xml_0_rules).
  791.      intros f.
  792.      case f.
  793.      vm_compute in |-*;intros ;apply P_id_u22_monotonic;assumption.
  794.      vm_compute in |-*;intros ;apply P_id_ack_in_monotonic;assumption.
  795.      vm_compute in |-*;apply (Aop.(le_refl)).
  796.      vm_compute in |-*;intros ;apply P_id_ack_out_monotonic;assumption.
  797.      vm_compute in |-*;intros ;apply P_id_s_monotonic;assumption.
  798.      vm_compute in |-*;intros ;apply P_id_u21_monotonic;assumption.
  799.      vm_compute in |-*;intros ;apply P_id_u11_monotonic;assumption.
  800.      intros f.
  801.      case f.
  802.      vm_compute in |-*;intros ;apply P_id_u22_bounded;assumption.
  803.      vm_compute in |-*;intros ;apply P_id_ack_in_bounded;assumption.
  804.      vm_compute in |-*;intros ;apply P_id_0_bounded;assumption.
  805.      vm_compute in |-*;intros ;apply P_id_ack_out_bounded;assumption.
  806.      vm_compute in |-*;intros ;apply P_id_s_bounded;assumption.
  807.      vm_compute in |-*;intros ;apply P_id_u21_bounded;assumption.
  808.      vm_compute in |-*;intros ;apply P_id_u11_bounded;assumption.
  809.      intros .
  810.      do 2 (rewrite  <- same_measure in |-*).
  811.      apply rules_monotonic;assumption.
  812.      assumption.
  813.    Qed.
  814.    
  815.    Hypothesis P_id_Marked_u11 : A ->A.
  816.    
  817.    Hypothesis P_id_Marked_u22 : A ->A.
  818.    
  819.    Hypothesis P_id_Marked_u21 : A ->A ->A.
  820.    
  821.    Hypothesis P_id_Marked_ack_in : A ->A ->A.
  822.    
  823.    Hypothesis P_id_Marked_u11_monotonic :
  824.     forall x4 x5,
  825.      (A0 <= x5)/\ (x5 <= x4) ->P_id_Marked_u11 x5 <= P_id_Marked_u11 x4.
  826.    
  827.    Hypothesis P_id_Marked_u22_monotonic :
  828.     forall x4 x5,
  829.      (A0 <= x5)/\ (x5 <= x4) ->P_id_Marked_u22 x5 <= P_id_Marked_u22 x4.
  830.    
  831.    Hypothesis P_id_Marked_u21_monotonic :
  832.     forall x4 x6 x5 x7,
  833.      (A0 <= x7)/\ (x7 <= x6) ->
  834.       (A0 <= x5)/\ (x5 <= x4) ->
  835.        P_id_Marked_u21 x5 x7 <= P_id_Marked_u21 x4 x6.
  836.    
  837.    Hypothesis P_id_Marked_ack_in_monotonic :
  838.     forall x4 x6 x5 x7,
  839.      (A0 <= x7)/\ (x7 <= x6) ->
  840.       (A0 <= x5)/\ (x5 <= x4) ->
  841.        P_id_Marked_ack_in x5 x7 <= P_id_Marked_ack_in x4 x6.
  842.    
  843.    Definition marked_measure t :=
  844.      match t with
  845.        | (algebra.Alg.Term algebra.F.id_u11 (x4::nil)) =>
  846.         P_id_Marked_u11 (measure x4)
  847.        | (algebra.Alg.Term algebra.F.id_u22 (x4::nil)) =>
  848.         P_id_Marked_u22 (measure x4)
  849.        | (algebra.Alg.Term algebra.F.id_u21 (x5::x4::nil)) =>
  850.         P_id_Marked_u21 (measure x5) (measure x4)
  851.        | (algebra.Alg.Term algebra.F.id_ack_in (x5::x4::nil)) =>
  852.         P_id_Marked_ack_in (measure x5) (measure x4)
  853.        | _ => measure t
  854.        end.
  855.    
  856.    Definition  Marked_pols :
  857.     forall f,
  858.      (algebra.EQT.defined R_xml_0_rules f) ->
  859.       InterpGen.Pol_type A (InterpGen.get_arity f).
  860.    Proof.
  861.      intros f H.
  862.      apply ddp.defined_list_complete with (1:=R_xml_0_rules_included) in H .
  863.      apply (Symb_more_list.change_in algebra.F.symb_order) in H .
  864.      
  865.      set (u := (Symb_more_list.qs algebra.F.symb_order
  866.           (Symb_more_list.XSet.remove_red
  867.              (ddp.defined_list R_xml_0_rule_as_list nil) ))) in * .
  868.      vm_compute in u .
  869.      unfold u in * .
  870.      clear u .
  871.      unfold more_list.mem_bool in H .
  872.      
  873.      match type of H with
  874.       | orb ?a ?b = true =>
  875.         assert (H':{a = true}+{b = true});[
  876.            revert H;case a;[left;reflexivity|simpl;intros h;right;exact h]|
  877.              clear H;destruct H' as [H|H]]
  878.     end .
  879.      
  880.      match type of H with
  881.       | _ _ ?t = true =>
  882.         generalize (algebra.F.symb_eq_bool_ok f t);
  883.           unfold algebra.Alg.eq_symb_bool in H;
  884.           rewrite H;clear H;intros ;subst
  885.     end .
  886.      vm_compute in |-*;intros x4;apply (P_id_Marked_u11 x4).
  887.      
  888.      match type of H with
  889.       | orb ?a ?b = true =>
  890.         assert (H':{a = true}+{b = true});[
  891.            revert H;case a;[left;reflexivity|simpl;intros h;right;exact h]|
  892.              clear H;destruct H' as [H|H]]
  893.     end .
  894.      
  895.      match type of H with
  896.       | _ _ ?t = true =>
  897.         generalize (algebra.F.symb_eq_bool_ok f t);
  898.           unfold algebra.Alg.eq_symb_bool in H;
  899.           rewrite H;clear H;intros ;subst
  900.     end .
  901.      vm_compute in |-*;intros x5 x4;apply (P_id_Marked_u21 x5 x4).
  902.      
  903.      match type of H with
  904.       | orb ?a ?b = true =>
  905.         assert (H':{a = true}+{b = true});[
  906.            revert H;case a;[left;reflexivity|simpl;intros h;right;exact h]|
  907.              clear H;destruct H' as [H|H]]
  908.     end .
  909.      
  910.      match type of H with
  911.       | _ _ ?t = true =>
  912.         generalize (algebra.F.symb_eq_bool_ok f t);
  913.           unfold algebra.Alg.eq_symb_bool in H;
  914.           rewrite H;clear H;intros ;subst
  915.     end .
  916.      vm_compute in |-*;intros x5 x4;apply (P_id_Marked_ack_in x5 x4).
  917.      
  918.      match type of H with
  919.       | orb ?a ?b = true =>
  920.         assert (H':{a = true}+{b = true});[
  921.            revert H;case a;[left;reflexivity|simpl;intros h;right;exact h]|
  922.              clear H;destruct H' as [H|H]]
  923.     end .
  924.      
  925.      match type of H with
  926.       | _ _ ?t = true =>
  927.         generalize (algebra.F.symb_eq_bool_ok f t);
  928.           unfold algebra.Alg.eq_symb_bool in H;
  929.           rewrite H;clear H;intros ;subst
  930.     end .
  931.      vm_compute in |-*;intros x4;apply (P_id_Marked_u22 x4).
  932.      discriminate H.
  933.    Defined.
  934.    
  935.    Lemma same_marked_measure :
  936.     forall t,
  937.      marked_measure t = InterpGen.marked_measure A0 Pols Marked_pols
  938.                          (ddp.defined_dec _ _ R_xml_0_rules_included)
  939.                          t.
  940.    Proof.
  941.      intros [a| f l].
  942.      simpl in |-*.
  943.      unfold eq_rect_r, eq_rect, sym_eq in |-*.
  944.      reflexivity .
  945.      
  946.      refine match f with
  947.               | algebra.F.id_u22 =>
  948.                match l with
  949.                  | nil => _
  950.                  | _::nil => _
  951.                  | _::_::_ => _
  952.                  end
  953.               | algebra.F.id_ack_in =>
  954.                match l with
  955.                  | nil => _
  956.                  | _::nil => _
  957.                  | _::_::nil => _
  958.                  | _::_::_::_ => _
  959.                  end
  960.               | algebra.F.id_0 => match l with
  961.                                     | nil => _
  962.                                     | _::_ => _
  963.                                     end
  964.               | algebra.F.id_ack_out =>
  965.                match l with
  966.                  | nil => _
  967.                  | _::nil => _
  968.                  | _::_::_ => _
  969.                  end
  970.               | algebra.F.id_s =>
  971.                match l with
  972.                  | nil => _
  973.                  | _::nil => _
  974.                  | _::_::_ => _
  975.                  end
  976.               | algebra.F.id_u21 =>
  977.                match l with
  978.                  | nil => _
  979.                  | _::nil => _
  980.                  | _::_::nil => _
  981.                  | _::_::_::_ => _
  982.                  end
  983.               | algebra.F.id_u11 =>
  984.                match l with
  985.                  | nil => _
  986.                  | _::nil => _
  987.                  | _::_::_ => _
  988.                  end
  989.               end.
  990.      vm_compute in |-*;reflexivity .
  991.      
  992.      lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
  993.       apply same_measure.
  994.      vm_compute in |-*;reflexivity .
  995.      vm_compute in |-*;reflexivity .
  996.      vm_compute in |-*;reflexivity .
  997.      
  998.      lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
  999.       apply same_measure.
  1000.      vm_compute in |-*;reflexivity .
  1001.      vm_compute in |-*;reflexivity .
  1002.      vm_compute in |-*;reflexivity .
  1003.      vm_compute in |-*;reflexivity .
  1004.      
  1005.      lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
  1006.       apply same_measure.
  1007.      vm_compute in |-*;reflexivity .
  1008.      vm_compute in |-*;reflexivity .
  1009.      
  1010.      lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
  1011.       apply same_measure.
  1012.      vm_compute in |-*;reflexivity .
  1013.      vm_compute in |-*;reflexivity .
  1014.      vm_compute in |-*;reflexivity .
  1015.      
  1016.      lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
  1017.       apply same_measure.
  1018.      vm_compute in |-*;reflexivity .
  1019.      vm_compute in |-*;reflexivity .
  1020.      
  1021.      lazy - [measure InterpGen.measure Pols] in |-* ;f_equal ;
  1022.       apply same_measure.
  1023.      vm_compute in |-*;reflexivity .
  1024.    Qed.
  1025.    
  1026.    Lemma marked_measure_equation :
  1027.     forall t,
  1028.      marked_measure t = match t with
  1029.                           | (algebra.Alg.Term algebra.F.id_u11 (x4::nil)) =>
  1030.                            P_id_Marked_u11 (measure x4)
  1031.                           | (algebra.Alg.Term algebra.F.id_u22 (x4::nil)) =>
  1032.                            P_id_Marked_u22 (measure x4)
  1033.                           | (algebra.Alg.Term algebra.F.id_u21 (x5::
  1034.                              x4::nil)) =>
  1035.                            P_id_Marked_u21 (measure x5) (measure x4)
  1036.                           | (algebra.Alg.Term algebra.F.id_ack_in (x5::
  1037.                              x4::nil)) =>
  1038.                            P_id_Marked_ack_in (measure x5) (measure x4)
  1039.                           | _ => measure t
  1040.                           end.
  1041.    Proof.
  1042.      reflexivity .
  1043.    Qed.
  1044.    
  1045.    Lemma marked_measure_star_monotonic :
  1046.     forall f l1 l2,
  1047.      (TransClosure.refl_trans_clos (weaved_relation.one_step_list (algebra.EQT.one_step
  1048.                                                                    R_xml_0_rules)
  1049.                                                                    )
  1050.        l1 l2) ->
  1051.       marked_measure (algebra.Alg.Term f l1) <= marked_measure (algebra.Alg.Term
  1052.                                                                  f l2).
  1053.    Proof.
  1054.      intros .
  1055.      do 2 (rewrite same_marked_measure in |-*).
  1056.      
  1057.      apply InterpGen.marked_measure_star_monotonic with
  1058.       (1:=Aop) (Pols:=Pols) (rules:=R_xml_0_rules).
  1059.      clear f.
  1060.      intros f.
  1061.      case f.
  1062.      vm_compute in |-*;intros ;apply P_id_u22_monotonic;assumption.
  1063.      vm_compute in |-*;intros ;apply P_id_ack_in_monotonic;assumption.
  1064.      vm_compute in |-*;apply (Aop.(le_refl)).
  1065.      vm_compute in |-*;intros ;apply P_id_ack_out_monotonic;assumption.
  1066.      vm_compute in |-*;intros ;apply P_id_s_monotonic;assumption.
  1067.      vm_compute in |-*;intros ;apply P_id_u21_monotonic;assumption.
  1068.      vm_compute in |-*;intros ;apply P_id_u11_monotonic;assumption.
  1069.      clear f.
  1070.      intros f.
  1071.      case f.
  1072.      vm_compute in |-*;intros ;apply P_id_u22_bounded;assumption.
  1073.      vm_compute in |-*;intros ;apply P_id_ack_in_bounded;assumption.
  1074.      vm_compute in |-*;intros ;apply P_id_0_bounded;assumption.
  1075.      vm_compute in |-*;intros ;apply P_id_ack_out_bounded;assumption.
  1076.      vm_compute in |-*;intros ;apply P_id_s_bounded;assumption.
  1077.      vm_compute in |-*;intros ;apply P_id_u21_bounded;assumption.
  1078.      vm_compute in |-*;intros ;apply P_id_u11_bounded;assumption.
  1079.      intros .
  1080.      do 2 (rewrite  <- same_measure in |-*).
  1081.      apply rules_monotonic;assumption.
  1082.      clear f.
  1083.      intros f.
  1084.      clear H.
  1085.      intros H.
  1086.      generalize H.
  1087.      apply ddp.defined_list_complete with (1:=R_xml_0_rules_included) in H .
  1088.      apply (Symb_more_list.change_in algebra.F.symb_order) in H .
  1089.      
  1090.      set (u := (Symb_more_list.qs algebra.F.symb_order
  1091.           (Symb_more_list.XSet.remove_red
  1092.              (ddp.defined_list R_xml_0_rule_as_list nil)))) in * .
  1093.      vm_compute in u .
  1094.      unfold u in * .
  1095.      clear u .
  1096.      unfold more_list.mem_bool in H .
  1097.      
  1098.      match type of H with
  1099.       | orb ?a ?b = true =>
  1100.         assert (H':{a = true}+{b = true});[
  1101.            revert H;case a;[left;reflexivity|simpl;intros h;right;exact h]|
  1102.              clear H;destruct H' as [H|H]]
  1103.     end .
  1104.      
  1105.      match type of H with
  1106.       | _ _ ?t = true =>
  1107.         generalize (algebra.F.symb_eq_bool_ok f t);
  1108.           unfold algebra.Alg.eq_symb_bool in H;
  1109.           rewrite H;clear H;intros ;subst
  1110.     end .
  1111.      vm_compute in |-*;intros ;apply P_id_Marked_u11_monotonic;assumption.
  1112.      
  1113.      match type of H with
  1114.       | orb ?a ?b = true =>
  1115.         assert (H':{a = true}+{b = true});[
  1116.            revert H;case a;[left;reflexivity|simpl;intros h;right;exact h]|
  1117.              clear H;destruct H' as [H|H]]
  1118.     end .
  1119.      
  1120.      match type of H with
  1121.       | _ _ ?t = true =>
  1122.         generalize (algebra.F.symb_eq_bool_ok f t);
  1123.           unfold algebra.Alg.eq_symb_bool in H;
  1124.           rewrite H;clear H;intros ;subst
  1125.     end .
  1126.      vm_compute in |-*;intros ;apply P_id_Marked_u21_monotonic;assumption.
  1127.      
  1128.      match type of H with
  1129.       | orb ?a ?b = true =>
  1130.         assert (H':{a = true}+{b = true});[
  1131.            revert H;case a;[left;reflexivity|simpl;intros h;right;exact h]|
  1132.              clear H;destruct H' as [H|H]]
  1133.     end .
  1134.      
  1135.      match type of H with
  1136.       | _ _ ?t = true =>
  1137.         generalize (algebra.F.symb_eq_bool_ok f t);
  1138.           unfold algebra.Alg.eq_symb_bool in H;
  1139.           rewrite H;clear H;intros ;subst
  1140.     end .
  1141.      
  1142.      vm_compute in |-*;intros ;apply P_id_Marked_ack_in_monotonic;assumption.
  1143.      
  1144.      match type of H with
  1145.       | orb ?a ?b = true =>
  1146.         assert (H':{a = true}+{b = true});[
  1147.            revert H;case a;[left;reflexivity|simpl;intros h;right;exact h]|
  1148.              clear H;destruct H' as [H|H]]
  1149.     end .
  1150.      
  1151.      match type of H with
  1152.       | _ _ ?t = true =>
  1153.         generalize (algebra.F.symb_eq_bool_ok f t);
  1154.           unfold algebra.Alg.eq_symb_bool in H;
  1155.           rewrite H;clear H;intros ;subst
  1156.     end .
  1157.      vm_compute in |-*;intros ;apply P_id_Marked_u22_monotonic;assumption.
  1158.      discriminate H.
  1159.      assumption.
  1160.    Qed.
  1161.    
  1162.    End S.
  1163. End Interp.
  1164.  
  1165.  
  1166. Module InterpZ.
  1167.  Section S.
  1168.    Open Scope Z_scope.
  1169.    
  1170.    Hypothesis min_value : Z.
  1171.    
  1172.    Import ring_extention.
  1173.    
  1174.    Notation Local "'Alt'" := (Zwf.Zwf min_value).
  1175.    
  1176.    Notation Local "'Ale'" := Zle.
  1177.    
  1178.    Notation Local "'Aeq'" := (@eq Z).
  1179.    
  1180.    Notation Local "a <= b" := (Ale a b).
  1181.    
  1182.    Notation Local "a < b" := (Alt a b).
  1183.    
  1184.    Hypothesis P_id_u22 : Z ->Z.
  1185.    
  1186.    Hypothesis P_id_ack_in : Z ->Z ->Z.
  1187.    
  1188.    Hypothesis P_id_0 : Z.
  1189.    
  1190.    Hypothesis P_id_ack_out : Z ->Z.
  1191.    
  1192.    Hypothesis P_id_s : Z ->Z.
  1193.    
  1194.    Hypothesis P_id_u21 : Z ->Z ->Z.
  1195.    
  1196.    Hypothesis P_id_u11 : Z ->Z.
  1197.    
  1198.    Hypothesis P_id_u22_monotonic :
  1199.     forall x4 x5,
  1200.      (min_value <= x5)/\ (x5 <= x4) ->P_id_u22 x5 <= P_id_u22 x4.
  1201.    
  1202.    Hypothesis P_id_ack_in_monotonic :
  1203.     forall x4 x6 x5 x7,
  1204.      (min_value <= x7)/\ (x7 <= x6) ->
  1205.       (min_value <= x5)/\ (x5 <= x4) ->
  1206.        P_id_ack_in x5 x7 <= P_id_ack_in x4 x6.
  1207.    
  1208.    Hypothesis P_id_ack_out_monotonic :
  1209.     forall x4 x5,
  1210.      (min_value <= x5)/\ (x5 <= x4) ->P_id_ack_out x5 <= P_id_ack_out x4.
  1211.    
  1212.    Hypothesis P_id_s_monotonic :
  1213.     forall x4 x5, (min_value <= x5)/\ (x5 <= x4) ->P_id_s x5 <= P_id_s x4.
  1214.    
  1215.    Hypothesis P_id_u21_monotonic :
  1216.     forall x4 x6 x5 x7,
  1217.      (min_value <= x7)/\ (x7 <= x6) ->
  1218.       (min_value <= x5)/\ (x5 <= x4) ->P_id_u21 x5 x7 <= P_id_u21 x4 x6.
  1219.    
  1220.    Hypothesis P_id_u11_monotonic :
  1221.     forall x4 x5,
  1222.      (min_value <= x5)/\ (x5 <= x4) ->P_id_u11 x5 <= P_id_u11 x4.
  1223.    
  1224.    Hypothesis P_id_u22_bounded :
  1225.     forall x4, (min_value <= x4) ->min_value <= P_id_u22 x4.
  1226.    
  1227.    Hypothesis P_id_ack_in_bounded :
  1228.     forall x4 x5,
  1229.      (min_value <= x4) ->(min_value <= x5) ->min_value <= P_id_ack_in x5 x4.
  1230.    
  1231.    Hypothesis P_id_0_bounded : min_value <= P_id_0 .
  1232.    
  1233.    Hypothesis P_id_ack_out_bounded :
  1234.     forall x4, (min_value <= x4) ->min_value <= P_id_ack_out x4.
  1235.    
  1236.    Hypothesis P_id_s_bounded :
  1237.     forall x4, (min_value <= x4) ->min_value <= P_id_s x4.
  1238.    
  1239.    Hypothesis P_id_u21_bounded :
  1240.     forall x4 x5,
  1241.      (min_value <= x4) ->(min_value <= x5) ->min_value <= P_id_u21 x5 x4.
  1242.    
  1243.    Hypothesis P_id_u11_bounded :
  1244.     forall x4, (min_value <= x4) ->min_value <= P_id_u11 x4.
  1245.    
  1246.    Definition measure  :=
  1247.      Interp.measure min_value P_id_u22 P_id_ack_in P_id_0 P_id_ack_out
  1248.       P_id_s P_id_u21 P_id_u11.
  1249.    
  1250.    Lemma measure_equation :
  1251.     forall t,
  1252.      measure t = match t with
  1253.                    | (algebra.Alg.Term algebra.F.id_u22 (x4::nil)) =>
  1254.                     P_id_u22 (measure x4)
  1255.                    | (algebra.Alg.Term algebra.F.id_ack_in (x5::x4::nil)) =>
  1256.                     P_id_ack_in (measure x5) (measure x4)
  1257.                    | (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0
  1258.                    | (algebra.Alg.Term algebra.F.id_ack_out (x4::nil)) =>
  1259.                     P_id_ack_out (measure x4)
  1260.                    | (algebra.Alg.Term algebra.F.id_s (x4::nil)) =>
  1261.                     P_id_s (measure x4)
  1262.                    | (algebra.Alg.Term algebra.F.id_u21 (x5::x4::nil)) =>
  1263.                     P_id_u21 (measure x5) (measure x4)
  1264.                    | (algebra.Alg.Term algebra.F.id_u11 (x4::nil)) =>
  1265.                     P_id_u11 (measure x4)
  1266.                    | _ => min_value
  1267.                    end.
  1268.    Proof.
  1269.      intros t;
  1270.       refine match t with
  1271.                | (algebra.Alg.Term algebra.F.id_u22 (x4::nil)) => _
  1272.                | (algebra.Alg.Term algebra.F.id_ack_in (x5::x4::nil)) =>
  1273.                _
  1274.                | (algebra.Alg.Term algebra.F.id_0 nil) => _
  1275.                | (algebra.Alg.Term algebra.F.id_ack_out (x4::nil)) =>
  1276.                _
  1277.                | (algebra.Alg.Term algebra.F.id_s (x4::nil)) => _
  1278.                | (algebra.Alg.Term algebra.F.id_u21 (x5::x4::nil)) =>
  1279.                _
  1280.                | (algebra.Alg.Term algebra.F.id_u11 (x4::nil)) => _
  1281.                | _ => _
  1282.                end;apply refl_equal.
  1283.    Qed.
  1284.    
  1285.    Lemma measure_bounded : forall t, min_value <= measure t.
  1286.    Proof.
  1287.      unfold measure in |-*.
  1288.      
  1289.      apply Interp.measure_bounded with Alt Aeq;
  1290.       (apply interp.o_Z)||
  1291.       (cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;auto with zarith).
  1292.    Qed.
  1293.    
  1294.    Ltac generate_pos_hyp  :=
  1295.     match goal with
  1296.       | H:context [measure ?x] |- _ =>
  1297.        let v := fresh "v" in
  1298.         (let H := fresh "h" in
  1299.           (set (H:=measure_bounded x) in *;set (v:=measure x) in *;
  1300.             clearbody H;clearbody v))
  1301.       |  |- context [measure ?x] =>
  1302.        let v := fresh "v" in
  1303.         (let H := fresh "h" in
  1304.           (set (H:=measure_bounded x) in *;set (v:=measure x) in *;
  1305.             clearbody H;clearbody v))
  1306.       end
  1307.     .
  1308.    
  1309.    Hypothesis rules_monotonic :
  1310.     forall l r,
  1311.      (algebra.EQT.axiom R_xml_0_rules r l) ->measure r <= measure l.
  1312.    
  1313.    Lemma measure_star_monotonic :
  1314.     forall l r,
  1315.      (TransClosure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) r l) ->
  1316.       measure r <= measure l.
  1317.    Proof.
  1318.      unfold measure in *.
  1319.      apply Interp.measure_star_monotonic with Alt Aeq.
  1320.      
  1321.      (apply interp.o_Z)||
  1322.      (cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;auto with zarith).
  1323.      intros ;apply P_id_u22_monotonic;assumption.
  1324.      intros ;apply P_id_ack_in_monotonic;assumption.
  1325.      intros ;apply P_id_ack_out_monotonic;assumption.
  1326.      intros ;apply P_id_s_monotonic;assumption.
  1327.      intros ;apply P_id_u21_monotonic;assumption.
  1328.      intros ;apply P_id_u11_monotonic;assumption.
  1329.      intros ;apply P_id_u22_bounded;assumption.
  1330.      intros ;apply P_id_ack_in_bounded;assumption.
  1331.      intros ;apply P_id_0_bounded;assumption.
  1332.      intros ;apply P_id_ack_out_bounded;assumption.
  1333.      intros ;apply P_id_s_bounded;assumption.
  1334.      intros ;apply P_id_u21_bounded;assumption.
  1335.      intros ;apply P_id_u11_bounded;assumption.
  1336.      apply rules_monotonic.
  1337.    Qed.
  1338.    
  1339.    Hypothesis P_id_Marked_u11 : Z ->Z.
  1340.    
  1341.    Hypothesis P_id_Marked_u22 : Z ->Z.
  1342.    
  1343.    Hypothesis P_id_Marked_u21 : Z ->Z ->Z.
  1344.    
  1345.    Hypothesis P_id_Marked_ack_in : Z ->Z ->Z.
  1346.    
  1347.    Hypothesis P_id_Marked_u11_monotonic :
  1348.     forall x4 x5,
  1349.      (min_value <= x5)/\ (x5 <= x4) ->
  1350.       P_id_Marked_u11 x5 <= P_id_Marked_u11 x4.
  1351.    
  1352.    Hypothesis P_id_Marked_u22_monotonic :
  1353.     forall x4 x5,
  1354.      (min_value <= x5)/\ (x5 <= x4) ->
  1355.       P_id_Marked_u22 x5 <= P_id_Marked_u22 x4.
  1356.    
  1357.    Hypothesis P_id_Marked_u21_monotonic :
  1358.     forall x4 x6 x5 x7,
  1359.      (min_value <= x7)/\ (x7 <= x6) ->
  1360.       (min_value <= x5)/\ (x5 <= x4) ->
  1361.        P_id_Marked_u21 x5 x7 <= P_id_Marked_u21 x4 x6.
  1362.    
  1363.    Hypothesis P_id_Marked_ack_in_monotonic :
  1364.     forall x4 x6 x5 x7,
  1365.      (min_value <= x7)/\ (x7 <= x6) ->
  1366.       (min_value <= x5)/\ (x5 <= x4) ->
  1367.        P_id_Marked_ack_in x5 x7 <= P_id_Marked_ack_in x4 x6.
  1368.    
  1369.    Definition marked_measure  :=
  1370.      Interp.marked_measure min_value P_id_u22 P_id_ack_in P_id_0
  1371.       P_id_ack_out P_id_s P_id_u21 P_id_u11 P_id_Marked_u11 P_id_Marked_u22
  1372.       P_id_Marked_u21 P_id_Marked_ack_in.
  1373.    
  1374.    Lemma marked_measure_equation :
  1375.     forall t,
  1376.      marked_measure t = match t with
  1377.                           | (algebra.Alg.Term algebra.F.id_u11 (x4::nil)) =>
  1378.                            P_id_Marked_u11 (measure x4)
  1379.                           | (algebra.Alg.Term algebra.F.id_u22 (x4::nil)) =>
  1380.                            P_id_Marked_u22 (measure x4)
  1381.                           | (algebra.Alg.Term algebra.F.id_u21 (x5::
  1382.                              x4::nil)) =>
  1383.                            P_id_Marked_u21 (measure x5) (measure x4)
  1384.                           | (algebra.Alg.Term algebra.F.id_ack_in (x5::
  1385.                              x4::nil)) =>
  1386.                            P_id_Marked_ack_in (measure x5) (measure x4)
  1387.                           | _ => measure t
  1388.                           end.
  1389.    Proof.
  1390.      reflexivity .
  1391.    Qed.
  1392.    
  1393.    Lemma marked_measure_star_monotonic :
  1394.     forall f l1 l2,
  1395.      (TransClosure.refl_trans_clos (weaved_relation.one_step_list (algebra.EQT.one_step
  1396.                                                                    R_xml_0_rules)
  1397.                                                                    )
  1398.        l1 l2) ->
  1399.       marked_measure (algebra.Alg.Term f l1) <= marked_measure (algebra.Alg.Term
  1400.                                                                  f l2).
  1401.    Proof.
  1402.      unfold marked_measure in *.
  1403.      apply Interp.marked_measure_star_monotonic with Alt Aeq.
  1404.      
  1405.      (apply interp.o_Z)||
  1406.      (cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;auto with zarith).
  1407.      intros ;apply P_id_u22_monotonic;assumption.
  1408.      intros ;apply P_id_ack_in_monotonic;assumption.
  1409.      intros ;apply P_id_ack_out_monotonic;assumption.
  1410.      intros ;apply P_id_s_monotonic;assumption.
  1411.      intros ;apply P_id_u21_monotonic;assumption.
  1412.      intros ;apply P_id_u11_monotonic;assumption.
  1413.      intros ;apply P_id_u22_bounded;assumption.
  1414.      intros ;apply P_id_ack_in_bounded;assumption.
  1415.      intros ;apply P_id_0_bounded;assumption.
  1416.      intros ;apply P_id_ack_out_bounded;assumption.
  1417.      intros ;apply P_id_s_bounded;assumption.
  1418.      intros ;apply P_id_u21_bounded;assumption.
  1419.      intros ;apply P_id_u11_bounded;assumption.
  1420.      apply rules_monotonic.
  1421.      intros ;apply P_id_Marked_u11_monotonic;assumption.
  1422.      intros ;apply P_id_Marked_u22_monotonic;assumption.
  1423.      intros ;apply P_id_Marked_u21_monotonic;assumption.
  1424.      intros ;apply P_id_Marked_ack_in_monotonic;assumption.
  1425.    Qed.
  1426.    
  1427.    End S.
  1428. End InterpZ.
  1429.  
  1430.  
  1431. Inductive DP_R_xml_0  :
  1432.  algebra.Alg.term ->algebra.Alg.term ->Prop :=
  1433.    (* <ack_in(s(m),0),u11(ack_in(m,s(0)))> *)
  1434.   | DP_R_xml_0_0 :
  1435.    DP_R_xml_0 (algebra.Alg.Term algebra.F.id_u11 ((algebra.Alg.Term
  1436.                algebra.F.id_ack_in ((algebra.Alg.Var 2)::(algebra.Alg.Term
  1437.                algebra.F.id_s ((algebra.Alg.Term algebra.F.id_0
  1438.                nil)::nil))::nil))::nil))
  1439.     (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term algebra.F.id_s
  1440.      ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Term algebra.F.id_0
  1441.      nil)::nil))
  1442.    (* <ack_in(s(m),0),ack_in(m,s(0))> *)
  1443.   | DP_R_xml_0_1 :
  1444.    DP_R_xml_0 (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Var 2)::
  1445.                (algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Term
  1446.                algebra.F.id_0 nil)::nil))::nil))
  1447.     (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term algebra.F.id_s
  1448.      ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Term algebra.F.id_0
  1449.      nil)::nil))
  1450.    (* <ack_in(s(m),s(n)),u21(ack_in(s(m),n),m)> *)
  1451.   | DP_R_xml_0_2 :
  1452.    DP_R_xml_0 (algebra.Alg.Term algebra.F.id_u21 ((algebra.Alg.Term
  1453.                algebra.F.id_ack_in ((algebra.Alg.Term algebra.F.id_s
  1454.                ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Var 1)::nil))::
  1455.                (algebra.Alg.Var 2)::nil))
  1456.     (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term algebra.F.id_s
  1457.      ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Term algebra.F.id_s
  1458.      ((algebra.Alg.Var 1)::nil))::nil))
  1459.    (* <ack_in(s(m),s(n)),ack_in(s(m),n)> *)
  1460.   | DP_R_xml_0_3 :
  1461.    DP_R_xml_0 (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term
  1462.                algebra.F.id_s ((algebra.Alg.Var 2)::nil))::
  1463.                (algebra.Alg.Var 1)::nil))
  1464.     (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term algebra.F.id_s
  1465.      ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Term algebra.F.id_s
  1466.      ((algebra.Alg.Var 1)::nil))::nil))
  1467.    (* <u21(ack_out(n),m),u22(ack_in(m,n))> *)
  1468.   | DP_R_xml_0_4 :
  1469.    DP_R_xml_0 (algebra.Alg.Term algebra.F.id_u22 ((algebra.Alg.Term
  1470.                algebra.F.id_ack_in ((algebra.Alg.Var 2)::
  1471.                (algebra.Alg.Var 1)::nil))::nil))
  1472.     (algebra.Alg.Term algebra.F.id_u21 ((algebra.Alg.Term
  1473.      algebra.F.id_ack_out ((algebra.Alg.Var 1)::nil))::
  1474.      (algebra.Alg.Var 2)::nil))
  1475.    (* <u21(ack_out(n),m),ack_in(m,n)> *)
  1476.   | DP_R_xml_0_5 :
  1477.    DP_R_xml_0 (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Var 2)::
  1478.                (algebra.Alg.Var 1)::nil))
  1479.     (algebra.Alg.Term algebra.F.id_u21 ((algebra.Alg.Term
  1480.      algebra.F.id_ack_out ((algebra.Alg.Var 1)::nil))::
  1481.      (algebra.Alg.Var 2)::nil))
  1482. .
  1483.  
  1484. Module sdp :=  subterm_dp.MakeSubDP(algebra.EQT).
  1485.  
  1486.  
  1487.  
  1488. Ltac cdp_incl_dp_tac ind :=
  1489.  let H := fresh "H" in
  1490.  intros ?x ?y H;
  1491.  destruct H;
  1492.  match goal with
  1493.  |- sdp.Dp.dp _ ?t ?r =>
  1494.    match type of ind with
  1495.    | context f [_ ?l r -> _] =>
  1496.      match l with
  1497.      | context g [t] =>
  1498.        match eval vm_compute in
  1499.            (algebra.Alg.is_subterm_ok_true t l (refl_equal true)) with
  1500.        | exist _ ?pos ?Hpos =>
  1501.          constructor 1 with (p := pos) (t2 := l);
  1502.          [ constructor | exact Hpos | econstructor econstructor ]
  1503.        end
  1504.      end
  1505.    end
  1506.  end.
  1507.  
  1508.  
  1509. Ltac destruct_nth_error_nth_subterm :=
  1510.  match goal with
  1511.    | H: context [List.nth_error _ ?i ] |- _ =>
  1512.      destruct i; simpl in *
  1513.    | H: context [algebra.Alg.subterm_at_pos _ ?p ] |- _ =>
  1514.      destruct p; simpl in *
  1515.    | H: Some _ = Some _ |- _ =>
  1516.      inversion H; clear H; subst; simpl in *
  1517.    | H: None = Some _ |- _ =>
  1518.      inversion H
  1519.    | H: Some _ <> None |- _ =>
  1520.      inversion H
  1521.    | H:algebra.EQT.defined _ ?f  |- _ => (* cons pas defini *)
  1522.      solve [
  1523.        let f := fresh "f" in
  1524.          let l := fresh "l" in
  1525.            let h1 := fresh "h" in
  1526.              let h2 := fresh "h" in
  1527.                inversion H as [f l h1 h2] ; subst;  inversion h2 ]
  1528.  end.
  1529.  
  1530.  
  1531. Ltac destruct_until_absurd :=
  1532.  match goal with
  1533.    | |- context [List.nth_error _ ?i ] =>
  1534.      destruct i; simpl
  1535.    | |- context [algebra.Alg.subterm_at_pos _ ?p ] =>
  1536.      destruct p; simpl
  1537.    | |- Some _ <> Some _ =>
  1538.      let abs := fresh "abs" in
  1539.        solve [intro abs; inversion abs]
  1540.    | |- None <> Some _ =>
  1541.      let abs := fresh "abs" in
  1542.        solve [intro abs; inversion abs]
  1543.    | |- Some _ <> None =>
  1544.      let abs := fresh "abs" in
  1545.        solve [intro abs; inversion abs]
  1546.  end.
  1547.  
  1548.  
  1549.  
  1550.      Lemma are_connected_incl : forall (R DP1 DP2:relation algebra.Alg.term) x y,
  1551.  (forall x y,DP1 x y -> DP2 x y) ->
  1552.  sdp.Dp.are_connected DP1 R x y
  1553. -> sdp.Dp.are_connected DP2 R x y.
  1554. Proof.
  1555.  intros R DP1 DP2 x y H.
  1556.  destruct x; destruct y.
  1557.  unfold sdp.Dp.are_connected.
  1558.  intros [sigma [sigma' [hdp1 [hdp2 h]]]] .
  1559.   exists sigma; exists sigma';intros.
  1560.  split.
  1561.  apply H;assumption.
  1562.  split.
  1563.  apply H;assumption.
  1564.  assumption.  
  1565. Qed.
  1566.  
  1567.  
  1568. Module WF_DP_R_xml_0.
  1569.  Inductive DP_R_xml_0_non_scc_1  :
  1570.   algebra.Alg.term ->algebra.Alg.term ->Prop :=
  1571.     (* <ack_in(s(m),0),u11(ack_in(m,s(0)))> *)
  1572.    | DP_R_xml_0_non_scc_1_0 :
  1573.     DP_R_xml_0_non_scc_1 (algebra.Alg.Term algebra.F.id_u11
  1574.                           ((algebra.Alg.Term algebra.F.id_ack_in
  1575.                           ((algebra.Alg.Var 2)::(algebra.Alg.Term
  1576.                           algebra.F.id_s ((algebra.Alg.Term algebra.F.id_0
  1577.                           nil)::nil))::nil))::nil))
  1578.      (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term
  1579.       algebra.F.id_s ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Term
  1580.       algebra.F.id_0 nil)::nil))
  1581.  .
  1582.  
  1583.  
  1584.  Lemma acc_DP_R_xml_0_non_scc_1 :
  1585.   forall x sigma,
  1586.    In x (List.map (algebra.Alg.apply_subst sigma)
  1587.           ((algebra.Alg.Term algebra.F.id_u11 ((algebra.Alg.Term
  1588.             algebra.F.id_ack_in ((algebra.Alg.Var 2)::(algebra.Alg.Term
  1589.             algebra.F.id_s ((algebra.Alg.Term algebra.F.id_0
  1590.             nil)::nil))::nil))::nil))::nil)) ->
  1591.     Acc (sdp.Rcdp_min R_xml_0_rules DP_R_xml_0) x.
  1592.  Proof.
  1593.    intros x sigma H0.
  1594.    simpl in H0|-.
  1595.    
  1596.    constructor;intros y Hy;inversion Hy;clear Hy;subst;destruct H;
  1597.     inversion H2;clear H2;subst;revert H3 H1;destruct H5;intros H3 H1;
  1598.     match goal with
  1599.       |  |- _ =>
  1600.        simpl in H0|-;injection H3;clear H3;intros ;subst;
  1601.         repeat (
  1602.         match type of H0 with
  1603.           | or _ _ => destruct H0 as [H0| H0]
  1604.           | False => elim H0
  1605.           end
  1606.         );
  1607.         (discriminate H0)||
  1608.         (injection H0;clear H0;intros ;subst;
  1609.           repeat (
  1610.           match goal with
  1611.             | H:TransClosure.refl_trans_clos (weaved_relation.one_step_list _) _ _
  1612.                   |- _ =>
  1613.              destruct (algebra.EQT_ext.cons_star _ _ _ _ _ H) ;clear H
  1614.             end
  1615.           );
  1616.           (impossible_star_reduction_R_xml_0 )||
  1617.           (repeat (
  1618.            match goal with
  1619.              | H:TransClosure.refl_trans_clos (weaved_relation.one_step_list _) _ _
  1620.                    |- _ =>
  1621.               destruct (algebra.EQT_ext.cons_star _ _ _ _ _ H) ;clear H
  1622.              | H:TransClosure.refl_trans_clos (algebra.EQT.one_step _) (algebra.Alg.Term ?f1 ?l1) (algebra.Alg.Term ?f2 ?l2)
  1623.                    |- _ =>
  1624.               match f1 with
  1625.                 | f2 => fail 1
  1626.                 | _ =>  destruct (algebra.EQT_ext.trans_at_top _  f1 l1 f2 l2 _ _ H (refl_equal _) (refl_equal _) ) as [l [u [h1 [h2 h3]]]];clear H;[
  1627.                     intros;discriminate|]
  1628.                 end
  1629.              
  1630.              | H:algebra.EQT.axiom _ _ _ |- _ => inversion H;clear H;subst
  1631.              | H:R_xml_0_rules  _ _ |- _ => inversion H;clear H;subst
  1632.              | H:_ = _ |- _ =>
  1633.               discriminate H || (simpl in H;injection H;clear H;intros;subst) ||fail 0
  1634.              end
  1635.            );impossible_star_reduction_R_xml_0 ))
  1636.       end
  1637.     .
  1638.  Qed.
  1639.  
  1640.  
  1641.  Inductive DP_R_xml_0_non_scc_2  :
  1642.   algebra.Alg.term ->algebra.Alg.term ->Prop :=
  1643.     (* <u21(ack_out(n),m),u22(ack_in(m,n))> *)
  1644.    | DP_R_xml_0_non_scc_2_0 :
  1645.     DP_R_xml_0_non_scc_2 (algebra.Alg.Term algebra.F.id_u22
  1646.                           ((algebra.Alg.Term algebra.F.id_ack_in
  1647.                           ((algebra.Alg.Var 2)::
  1648.                           (algebra.Alg.Var 1)::nil))::nil))
  1649.      (algebra.Alg.Term algebra.F.id_u21 ((algebra.Alg.Term
  1650.       algebra.F.id_ack_out ((algebra.Alg.Var 1)::nil))::
  1651.       (algebra.Alg.Var 2)::nil))
  1652.  .
  1653.  
  1654.  
  1655.  Lemma acc_DP_R_xml_0_non_scc_2 :
  1656.   forall x sigma,
  1657.    In x (List.map (algebra.Alg.apply_subst sigma)
  1658.           ((algebra.Alg.Term algebra.F.id_u22 ((algebra.Alg.Term
  1659.             algebra.F.id_ack_in ((algebra.Alg.Var 2)::
  1660.             (algebra.Alg.Var 1)::nil))::nil))::nil)) ->
  1661.     Acc (sdp.Rcdp_min R_xml_0_rules DP_R_xml_0) x.
  1662.  Proof.
  1663.    intros x sigma H0.
  1664.    simpl in H0|-.
  1665.    
  1666.    constructor;intros y Hy;inversion Hy;clear Hy;subst;destruct H;
  1667.     inversion H2;clear H2;subst;revert H3 H1;destruct H5;intros H3 H1;
  1668.     match goal with
  1669.       |  |- _ =>
  1670.        simpl in H0|-;injection H3;clear H3;intros ;subst;
  1671.         repeat (
  1672.         match type of H0 with
  1673.           | or _ _ => destruct H0 as [H0| H0]
  1674.           | False => elim H0
  1675.           end
  1676.         );
  1677.         (discriminate H0)||
  1678.         (injection H0;clear H0;intros ;subst;
  1679.           repeat (
  1680.           match goal with
  1681.             | H:TransClosure.refl_trans_clos (weaved_relation.one_step_list _) _ _
  1682.                   |- _ =>
  1683.              destruct (algebra.EQT_ext.cons_star _ _ _ _ _ H) ;clear H
  1684.             end
  1685.           );
  1686.           (impossible_star_reduction_R_xml_0 )||
  1687.           (repeat (
  1688.            match goal with
  1689.              | H:TransClosure.refl_trans_clos (weaved_relation.one_step_list _) _ _
  1690.                    |- _ =>
  1691.               destruct (algebra.EQT_ext.cons_star _ _ _ _ _ H) ;clear H
  1692.              | H:TransClosure.refl_trans_clos (algebra.EQT.one_step _) (algebra.Alg.Term ?f1 ?l1) (algebra.Alg.Term ?f2 ?l2)
  1693.                    |- _ =>
  1694.               match f1 with
  1695.                 | f2 => fail 1
  1696.                 | _ =>  destruct (algebra.EQT_ext.trans_at_top _  f1 l1 f2 l2 _ _ H (refl_equal _) (refl_equal _) ) as [l [u [h1 [h2 h3]]]];clear H;[
  1697.                     intros;discriminate|]
  1698.                 end
  1699.              
  1700.              | H:algebra.EQT.axiom _ _ _ |- _ => inversion H;clear H;subst
  1701.              | H:R_xml_0_rules  _ _ |- _ => inversion H;clear H;subst
  1702.              | H:_ = _ |- _ =>
  1703.               discriminate H || (simpl in H;injection H;clear H;intros;subst) ||fail 0
  1704.              end
  1705.            );impossible_star_reduction_R_xml_0 ))
  1706.       end
  1707.     .
  1708.  Qed.
  1709.  
  1710.  
  1711.  Inductive DP_R_xml_0_scc_0  :
  1712.   algebra.Alg.term ->algebra.Alg.term ->Prop :=
  1713.     (* <ack_in(s(m),0),ack_in(m,s(0))> *)
  1714.    | DP_R_xml_0_scc_0_0 :
  1715.     DP_R_xml_0_scc_0 (algebra.Alg.Term algebra.F.id_ack_in
  1716.                       ((algebra.Alg.Var 2)::(algebra.Alg.Term
  1717.                       algebra.F.id_s ((algebra.Alg.Term algebra.F.id_0
  1718.                       nil)::nil))::nil))
  1719.      (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term
  1720.       algebra.F.id_s ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Term
  1721.       algebra.F.id_0 nil)::nil))
  1722.     (* <ack_in(s(m),s(n)),u21(ack_in(s(m),n),m)> *)
  1723.    | DP_R_xml_0_scc_0_1 :
  1724.     DP_R_xml_0_scc_0 (algebra.Alg.Term algebra.F.id_u21 ((algebra.Alg.Term
  1725.                       algebra.F.id_ack_in ((algebra.Alg.Term algebra.F.id_s
  1726.                       ((algebra.Alg.Var 2)::nil))::
  1727.                       (algebra.Alg.Var 1)::nil))::(algebra.Alg.Var 2)::nil))
  1728.      (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term
  1729.       algebra.F.id_s ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Term
  1730.       algebra.F.id_s ((algebra.Alg.Var 1)::nil))::nil))
  1731.     (* <ack_in(s(m),s(n)),ack_in(s(m),n)> *)
  1732.    | DP_R_xml_0_scc_0_2 :
  1733.     DP_R_xml_0_scc_0 (algebra.Alg.Term algebra.F.id_ack_in
  1734.                       ((algebra.Alg.Term algebra.F.id_s
  1735.                       ((algebra.Alg.Var 2)::nil))::
  1736.                       (algebra.Alg.Var 1)::nil))
  1737.      (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term
  1738.       algebra.F.id_s ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Term
  1739.       algebra.F.id_s ((algebra.Alg.Var 1)::nil))::nil))
  1740.     (* <u21(ack_out(n),m),ack_in(m,n)> *)
  1741.    | DP_R_xml_0_scc_0_3 :
  1742.     DP_R_xml_0_scc_0 (algebra.Alg.Term algebra.F.id_ack_in
  1743.                       ((algebra.Alg.Var 2)::(algebra.Alg.Var 1)::nil))
  1744.      (algebra.Alg.Term algebra.F.id_u21 ((algebra.Alg.Term
  1745.       algebra.F.id_ack_out ((algebra.Alg.Var 1)::nil))::
  1746.       (algebra.Alg.Var 2)::nil))
  1747.  .
  1748.  
  1749.  
  1750.  Module WF_DP_R_xml_0_scc_0.
  1751.   Inductive DP_R_xml_0_scc_0_large  :
  1752.    algebra.Alg.term ->algebra.Alg.term ->Prop :=
  1753.      (* <ack_in(s(m),s(n)),u21(ack_in(s(m),n),m)> *)
  1754.     | DP_R_xml_0_scc_0_large_0 :
  1755.      DP_R_xml_0_scc_0_large (algebra.Alg.Term algebra.F.id_u21
  1756.                              ((algebra.Alg.Term algebra.F.id_ack_in
  1757.                              ((algebra.Alg.Term algebra.F.id_s
  1758.                              ((algebra.Alg.Var 2)::nil))::
  1759.                              (algebra.Alg.Var 1)::nil))::
  1760.                              (algebra.Alg.Var 2)::nil))
  1761.       (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term
  1762.        algebra.F.id_s ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Term
  1763.        algebra.F.id_s ((algebra.Alg.Var 1)::nil))::nil))
  1764.      (* <ack_in(s(m),s(n)),ack_in(s(m),n)> *)
  1765.     | DP_R_xml_0_scc_0_large_1 :
  1766.      DP_R_xml_0_scc_0_large (algebra.Alg.Term algebra.F.id_ack_in
  1767.                              ((algebra.Alg.Term algebra.F.id_s
  1768.                              ((algebra.Alg.Var 2)::nil))::
  1769.                              (algebra.Alg.Var 1)::nil))
  1770.       (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term
  1771.        algebra.F.id_s ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Term
  1772.        algebra.F.id_s ((algebra.Alg.Var 1)::nil))::nil))
  1773.   .
  1774.  
  1775.  
  1776.   Inductive DP_R_xml_0_scc_0_strict  :
  1777.    algebra.Alg.term ->algebra.Alg.term ->Prop :=
  1778.      (* <ack_in(s(m),0),ack_in(m,s(0))> *)
  1779.     | DP_R_xml_0_scc_0_strict_0 :
  1780.      DP_R_xml_0_scc_0_strict (algebra.Alg.Term algebra.F.id_ack_in
  1781.                               ((algebra.Alg.Var 2)::(algebra.Alg.Term
  1782.                               algebra.F.id_s ((algebra.Alg.Term
  1783.                               algebra.F.id_0 nil)::nil))::nil))
  1784.       (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term
  1785.        algebra.F.id_s ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Term
  1786.        algebra.F.id_0 nil)::nil))
  1787.      (* <u21(ack_out(n),m),ack_in(m,n)> *)
  1788.     | DP_R_xml_0_scc_0_strict_1 :
  1789.      DP_R_xml_0_scc_0_strict (algebra.Alg.Term algebra.F.id_ack_in
  1790.                               ((algebra.Alg.Var 2)::
  1791.                               (algebra.Alg.Var 1)::nil))
  1792.       (algebra.Alg.Term algebra.F.id_u21 ((algebra.Alg.Term
  1793.        algebra.F.id_ack_out ((algebra.Alg.Var 1)::nil))::
  1794.        (algebra.Alg.Var 2)::nil))
  1795.   .
  1796.  
  1797.  
  1798.   Module WF_DP_R_xml_0_scc_0_large.
  1799.    Inductive DP_R_xml_0_scc_0_large_non_scc_1  :
  1800.     algebra.Alg.term ->algebra.Alg.term ->Prop :=
  1801.       (* <ack_in(s(m),s(n)),u21(ack_in(s(m),n),m)> *)
  1802.      | DP_R_xml_0_scc_0_large_non_scc_1_0 :
  1803.       DP_R_xml_0_scc_0_large_non_scc_1 (algebra.Alg.Term algebra.F.id_u21
  1804.                                         ((algebra.Alg.Term
  1805.                                         algebra.F.id_ack_in
  1806.                                         ((algebra.Alg.Term algebra.F.id_s
  1807.                                         ((algebra.Alg.Var 2)::nil))::
  1808.                                         (algebra.Alg.Var 1)::nil))::
  1809.                                         (algebra.Alg.Var 2)::nil))
  1810.        (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term
  1811.         algebra.F.id_s ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Term
  1812.         algebra.F.id_s ((algebra.Alg.Var 1)::nil))::nil))
  1813.    .
  1814.    
  1815.    
  1816.    Lemma acc_DP_R_xml_0_scc_0_large_non_scc_1 :
  1817.     forall x sigma,
  1818.      In x (List.map (algebra.Alg.apply_subst sigma)
  1819.             ((algebra.Alg.Term algebra.F.id_u21 ((algebra.Alg.Term
  1820.               algebra.F.id_ack_in ((algebra.Alg.Term algebra.F.id_s
  1821.               ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Var 1)::nil))::
  1822.               (algebra.Alg.Var 2)::nil))::nil)) ->
  1823.       Acc (sdp.Rcdp_min R_xml_0_rules DP_R_xml_0_scc_0_large) x.
  1824.    Proof.
  1825.      intros x sigma H0.
  1826.      simpl in H0|-.
  1827.      
  1828.      constructor;intros y Hy;inversion Hy;clear Hy;subst;destruct H;
  1829.       inversion H2;clear H2;subst;revert H3 H1;destruct H5;intros H3 H1;
  1830.       match goal with
  1831.         |  |- _ =>
  1832.          simpl in H0|-;injection H3;clear H3;intros ;subst;
  1833.           repeat (
  1834.           match type of H0 with
  1835.             | or _ _ => destruct H0 as [H0| H0]
  1836.             | False => elim H0
  1837.             end
  1838.           );
  1839.           (discriminate H0)||
  1840.           (injection H0;clear H0;intros ;subst;
  1841.             repeat (
  1842.             match goal with
  1843.               | H:TransClosure.refl_trans_clos (weaved_relation.one_step_list _) _ _
  1844.                     |- _ =>
  1845.                destruct (algebra.EQT_ext.cons_star _ _ _ _ _ H) ;clear H
  1846.               end
  1847.             );
  1848.             (impossible_star_reduction_R_xml_0 )||
  1849.             (repeat (
  1850.              match goal with
  1851.                | H:TransClosure.refl_trans_clos (weaved_relation.one_step_list _) _ _
  1852.                      |- _ =>
  1853.                 destruct (algebra.EQT_ext.cons_star _ _ _ _ _ H) ;clear H
  1854.                | H:TransClosure.refl_trans_clos (algebra.EQT.one_step _) (algebra.Alg.Term ?f1 ?l1) (algebra.Alg.Term ?f2 ?l2)
  1855.                      |- _ =>
  1856.                 match f1 with
  1857.                   | f2 => fail 1
  1858.                   | _ =>  destruct (algebra.EQT_ext.trans_at_top _  f1 l1 f2 l2 _ _ H (refl_equal _) (refl_equal _) ) as [l [u [h1 [h2 h3]]]];clear H;[
  1859.                     intros;discriminate|]
  1860.                   end
  1861.                
  1862.                | H:algebra.EQT.axiom _ _ _ |- _ =>
  1863.                 inversion H;clear H;subst
  1864.                | H:R_xml_0_rules  _ _ |- _ => inversion H;clear H;subst
  1865.                | H:_ = _ |- _ =>
  1866.                 discriminate H || (simpl in H;injection H;clear H;intros;subst) ||fail 0
  1867.                end
  1868.              );impossible_star_reduction_R_xml_0 ))
  1869.         end
  1870.       .
  1871.    Qed.
  1872.    
  1873.    
  1874.    Inductive DP_R_xml_0_scc_0_large_scc_0  :
  1875.     algebra.Alg.term ->algebra.Alg.term ->Prop :=
  1876.       (* <ack_in(s(m),s(n)),ack_in(s(m),n)> *)
  1877.      | DP_R_xml_0_scc_0_large_scc_0_0 :
  1878.       DP_R_xml_0_scc_0_large_scc_0 (algebra.Alg.Term algebra.F.id_ack_in
  1879.                                     ((algebra.Alg.Term algebra.F.id_s
  1880.                                     ((algebra.Alg.Var 2)::nil))::
  1881.                                     (algebra.Alg.Var 1)::nil))
  1882.        (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term
  1883.         algebra.F.id_s ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Term
  1884.         algebra.F.id_s ((algebra.Alg.Var 1)::nil))::nil))
  1885.    .
  1886.    
  1887.    
  1888.    Module WF_DP_R_xml_0_scc_0_large_scc_0.
  1889.     Open Scope Z_scope.
  1890.    
  1891.     Import ring_extention.
  1892.    
  1893.     Notation Local "a <= b" := (Zle a b).
  1894.    
  1895.     Notation Local "a < b" := (Zlt a b).
  1896.    
  1897.     Definition P_id_u22 (x4:Z) := 0.
  1898.    
  1899.     Definition P_id_ack_in (x4:Z) (x5:Z) := 0.
  1900.    
  1901.     Definition P_id_0  := 0.
  1902.    
  1903.     Definition P_id_ack_out (x4:Z) := 0.
  1904.    
  1905.     Definition P_id_s (x4:Z) := 1 + 1* x4 + 0.
  1906.    
  1907.     Definition P_id_u21 (x4:Z) (x5:Z) := 0.
  1908.    
  1909.     Definition P_id_u11 (x4:Z) := 0.
  1910.    
  1911.     Lemma P_id_u22_monotonic :
  1912.      forall x4 x5, (0 <= x5)/\ (x5 <= x4) ->P_id_u22 x5 <= P_id_u22 x4.
  1913.     Proof.
  1914.       intros x5 x4.
  1915.       intros [H_1 H_0].
  1916.      
  1917.       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  1918.        ring_simplify ;
  1919.        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  1920.     Qed.
  1921.    
  1922.     Lemma P_id_ack_in_monotonic :
  1923.      forall x4 x6 x5 x7,
  1924.       (0 <= x7)/\ (x7 <= x6) ->
  1925.        (0 <= x5)/\ (x5 <= x4) ->P_id_ack_in x5 x7 <= P_id_ack_in x4 x6.
  1926.     Proof.
  1927.       intros x7 x6 x5 x4.
  1928.       intros [H_1 H_0].
  1929.       intros [H_3 H_2].
  1930.      
  1931.       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  1932.        ring_simplify ;
  1933.        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  1934.     Qed.
  1935.    
  1936.     Lemma P_id_ack_out_monotonic :
  1937.      forall x4 x5,
  1938.       (0 <= x5)/\ (x5 <= x4) ->P_id_ack_out x5 <= P_id_ack_out x4.
  1939.     Proof.
  1940.       intros x5 x4.
  1941.       intros [H_1 H_0].
  1942.      
  1943.       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  1944.        ring_simplify ;
  1945.        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  1946.     Qed.
  1947.    
  1948.     Lemma P_id_s_monotonic :
  1949.      forall x4 x5, (0 <= x5)/\ (x5 <= x4) ->P_id_s x5 <= P_id_s x4.
  1950.     Proof.
  1951.       intros x5 x4.
  1952.       intros [H_1 H_0].
  1953.      
  1954.       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  1955.        ring_simplify ;
  1956.        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  1957.     Qed.
  1958.    
  1959.     Lemma P_id_u21_monotonic :
  1960.      forall x4 x6 x5 x7,
  1961.       (0 <= x7)/\ (x7 <= x6) ->
  1962.        (0 <= x5)/\ (x5 <= x4) ->P_id_u21 x5 x7 <= P_id_u21 x4 x6.
  1963.     Proof.
  1964.       intros x7 x6 x5 x4.
  1965.       intros [H_1 H_0].
  1966.       intros [H_3 H_2].
  1967.      
  1968.       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  1969.        ring_simplify ;
  1970.        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  1971.     Qed.
  1972.    
  1973.     Lemma P_id_u11_monotonic :
  1974.      forall x4 x5, (0 <= x5)/\ (x5 <= x4) ->P_id_u11 x5 <= P_id_u11 x4.
  1975.     Proof.
  1976.       intros x5 x4.
  1977.       intros [H_1 H_0].
  1978.      
  1979.       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  1980.        ring_simplify ;
  1981.        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  1982.     Qed.
  1983.    
  1984.     Lemma P_id_u22_bounded : forall x4, (0 <= x4) ->0 <= P_id_u22 x4.
  1985.     Proof.
  1986.       intros .
  1987.      
  1988.       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  1989.        ring_simplify ;
  1990.        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  1991.     Qed.
  1992.    
  1993.     Lemma P_id_ack_in_bounded :
  1994.      forall x4 x5, (0 <= x4) ->(0 <= x5) ->0 <= P_id_ack_in x5 x4.
  1995.     Proof.
  1996.       intros .
  1997.      
  1998.       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  1999.        ring_simplify ;
  2000.        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2001.     Qed.
  2002.    
  2003.     Lemma P_id_0_bounded : 0 <= P_id_0 .
  2004.     Proof.
  2005.       intros .
  2006.      
  2007.       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2008.        ring_simplify ;
  2009.        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2010.     Qed.
  2011.    
  2012.     Lemma P_id_ack_out_bounded :
  2013.      forall x4, (0 <= x4) ->0 <= P_id_ack_out x4.
  2014.     Proof.
  2015.       intros .
  2016.      
  2017.       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2018.        ring_simplify ;
  2019.        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2020.     Qed.
  2021.    
  2022.     Lemma P_id_s_bounded : forall x4, (0 <= x4) ->0 <= P_id_s x4.
  2023.     Proof.
  2024.       intros .
  2025.      
  2026.       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2027.        ring_simplify ;
  2028.        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2029.     Qed.
  2030.    
  2031.     Lemma P_id_u21_bounded :
  2032.      forall x4 x5, (0 <= x4) ->(0 <= x5) ->0 <= P_id_u21 x5 x4.
  2033.     Proof.
  2034.       intros .
  2035.      
  2036.       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2037.        ring_simplify ;
  2038.        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2039.     Qed.
  2040.    
  2041.     Lemma P_id_u11_bounded : forall x4, (0 <= x4) ->0 <= P_id_u11 x4.
  2042.     Proof.
  2043.       intros .
  2044.      
  2045.       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2046.        ring_simplify ;
  2047.        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2048.     Qed.
  2049.    
  2050.     Definition measure  :=
  2051.       InterpZ.measure 0 P_id_u22 P_id_ack_in P_id_0 P_id_ack_out P_id_s
  2052.        P_id_u21 P_id_u11.
  2053.    
  2054.     Lemma measure_equation :
  2055.      forall t,
  2056.       measure t = match t with
  2057.                     | (algebra.Alg.Term algebra.F.id_u22 (x4::nil)) =>
  2058.                      P_id_u22 (measure x4)
  2059.                     | (algebra.Alg.Term algebra.F.id_ack_in (x5::x4::nil)) =>
  2060.                      P_id_ack_in (measure x5) (measure x4)
  2061.                     | (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0
  2062.                     | (algebra.Alg.Term algebra.F.id_ack_out (x4::nil)) =>
  2063.                      P_id_ack_out (measure x4)
  2064.                     | (algebra.Alg.Term algebra.F.id_s (x4::nil)) =>
  2065.                      P_id_s (measure x4)
  2066.                     | (algebra.Alg.Term algebra.F.id_u21 (x5::x4::nil)) =>
  2067.                      P_id_u21 (measure x5) (measure x4)
  2068.                     | (algebra.Alg.Term algebra.F.id_u11 (x4::nil)) =>
  2069.                      P_id_u11 (measure x4)
  2070.                     | _ => 0
  2071.                     end.
  2072.     Proof.
  2073.       intros t;
  2074.        refine match t with
  2075.                 | (algebra.Alg.Term algebra.F.id_u22 (x4::nil)) => _
  2076.                 | (algebra.Alg.Term algebra.F.id_ack_in (x5::x4::nil)) =>
  2077.                 _
  2078.                 | (algebra.Alg.Term algebra.F.id_0 nil) => _
  2079.                 | (algebra.Alg.Term algebra.F.id_ack_out (x4::nil)) =>
  2080.                 _
  2081.                 | (algebra.Alg.Term algebra.F.id_s (x4::nil)) => _
  2082.                 | (algebra.Alg.Term algebra.F.id_u21 (x5::x4::nil)) =>
  2083.                 _
  2084.                 | (algebra.Alg.Term algebra.F.id_u11 (x4::nil)) => _
  2085.                 | _ => _
  2086.                 end;apply refl_equal.
  2087.     Qed.
  2088.    
  2089.     Lemma measure_bounded : forall t, 0 <= measure t.
  2090.     Proof.
  2091.       unfold measure in |-*.
  2092.      
  2093.       apply InterpZ.measure_bounded;
  2094.        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2095.         ring_simplify ;
  2096.         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2097.     Qed.
  2098.    
  2099.     Ltac generate_pos_hyp  :=
  2100.      match goal with
  2101.        | H:context [measure ?x] |- _ =>
  2102.         let v := fresh "v" in
  2103.          (let H := fresh "h" in
  2104.            (set (H:=measure_bounded x) in *;set (v:=measure x) in *;
  2105.              clearbody H;clearbody v))
  2106.        |  |- context [measure ?x] =>
  2107.         let v := fresh "v" in
  2108.          (let H := fresh "h" in
  2109.            (set (H:=measure_bounded x) in *;set (v:=measure x) in *;
  2110.              clearbody H;clearbody v))
  2111.        end
  2112.      .
  2113.    
  2114.     Lemma rules_monotonic :
  2115.      forall l r,
  2116.       (algebra.EQT.axiom R_xml_0_rules r l) ->measure r <= measure l.
  2117.     Proof.
  2118.       intros l r H.
  2119.       fold measure in |-*.
  2120.      
  2121.       inversion H;clear H;subst;inversion H0;clear H0;subst;
  2122.        simpl algebra.EQT.T.apply_subst in |-*;
  2123.        repeat (
  2124.        match goal with
  2125.          |  |- context [measure (algebra.Alg.Term ?f ?t)] =>
  2126.           rewrite (measure_equation (algebra.Alg.Term f t))
  2127.          end
  2128.        );repeat (generate_pos_hyp );
  2129.        cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2130.         ring_simplify ;
  2131.         (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2132.     Qed.
  2133.    
  2134.     Lemma measure_star_monotonic :
  2135.      forall l r,
  2136.       (TransClosure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) r l) ->
  2137.        measure r <= measure l.
  2138.     Proof.
  2139.       unfold measure in *.
  2140.       apply InterpZ.measure_star_monotonic.
  2141.       intros ;apply P_id_u22_monotonic;assumption.
  2142.       intros ;apply P_id_ack_in_monotonic;assumption.
  2143.       intros ;apply P_id_ack_out_monotonic;assumption.
  2144.       intros ;apply P_id_s_monotonic;assumption.
  2145.       intros ;apply P_id_u21_monotonic;assumption.
  2146.       intros ;apply P_id_u11_monotonic;assumption.
  2147.       intros ;apply P_id_u22_bounded;assumption.
  2148.       intros ;apply P_id_ack_in_bounded;assumption.
  2149.       intros ;apply P_id_0_bounded;assumption.
  2150.       intros ;apply P_id_ack_out_bounded;assumption.
  2151.       intros ;apply P_id_s_bounded;assumption.
  2152.       intros ;apply P_id_u21_bounded;assumption.
  2153.       intros ;apply P_id_u11_bounded;assumption.
  2154.       apply rules_monotonic.
  2155.     Qed.
  2156.    
  2157.     Definition P_id_Marked_u11 (x4:Z) := 1* x4 + 0.
  2158.    
  2159.     Definition P_id_Marked_u22 (x4:Z) := 1* x4 + 0.
  2160.    
  2161.     Definition P_id_Marked_u21 (x4:Z) (x5:Z) := 1* x5 + 1* x4 + 0.
  2162.    
  2163.     Definition P_id_Marked_ack_in (x4:Z) (x5:Z) := 1* x5 + 0.
  2164.    
  2165.     Lemma P_id_Marked_u11_monotonic :
  2166.      forall x4 x5,
  2167.       (0 <= x5)/\ (x5 <= x4) ->P_id_Marked_u11 x5 <= P_id_Marked_u11 x4.
  2168.     Proof.
  2169.       intros x5 x4.
  2170.       intros [H_1 H_0].
  2171.      
  2172.       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2173.        ring_simplify ;
  2174.        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2175.     Qed.
  2176.    
  2177.     Lemma P_id_Marked_u22_monotonic :
  2178.      forall x4 x5,
  2179.       (0 <= x5)/\ (x5 <= x4) ->P_id_Marked_u22 x5 <= P_id_Marked_u22 x4.
  2180.     Proof.
  2181.       intros x5 x4.
  2182.       intros [H_1 H_0].
  2183.      
  2184.       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2185.        ring_simplify ;
  2186.        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2187.     Qed.
  2188.    
  2189.     Lemma P_id_Marked_u21_monotonic :
  2190.      forall x4 x6 x5 x7,
  2191.       (0 <= x7)/\ (x7 <= x6) ->
  2192.        (0 <= x5)/\ (x5 <= x4) ->
  2193.         P_id_Marked_u21 x5 x7 <= P_id_Marked_u21 x4 x6.
  2194.     Proof.
  2195.       intros x7 x6 x5 x4.
  2196.       intros [H_1 H_0].
  2197.       intros [H_3 H_2].
  2198.      
  2199.       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2200.        ring_simplify ;
  2201.        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2202.     Qed.
  2203.    
  2204.     Lemma P_id_Marked_ack_in_monotonic :
  2205.      forall x4 x6 x5 x7,
  2206.       (0 <= x7)/\ (x7 <= x6) ->
  2207.        (0 <= x5)/\ (x5 <= x4) ->
  2208.         P_id_Marked_ack_in x5 x7 <= P_id_Marked_ack_in x4 x6.
  2209.     Proof.
  2210.       intros x7 x6 x5 x4.
  2211.       intros [H_1 H_0].
  2212.       intros [H_3 H_2].
  2213.      
  2214.       cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2215.        ring_simplify ;
  2216.        (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2217.     Qed.
  2218.    
  2219.     Definition marked_measure  :=
  2220.       InterpZ.marked_measure 0 P_id_u22 P_id_ack_in P_id_0 P_id_ack_out
  2221.        P_id_s P_id_u21 P_id_u11 P_id_Marked_u11 P_id_Marked_u22
  2222.        P_id_Marked_u21 P_id_Marked_ack_in.
  2223.    
  2224.     Lemma marked_measure_equation :
  2225.      forall t,
  2226.       marked_measure t = match t with
  2227.                            | (algebra.Alg.Term algebra.F.id_u11 (x4::nil)) =>
  2228.                             P_id_Marked_u11 (measure x4)
  2229.                            | (algebra.Alg.Term algebra.F.id_u22 (x4::nil)) =>
  2230.                             P_id_Marked_u22 (measure x4)
  2231.                            | (algebra.Alg.Term algebra.F.id_u21 (x5::
  2232.                               x4::nil)) =>
  2233.                             P_id_Marked_u21 (measure x5) (measure x4)
  2234.                            | (algebra.Alg.Term algebra.F.id_ack_in (x5::
  2235.                               x4::nil)) =>
  2236.                             P_id_Marked_ack_in (measure x5) (measure x4)
  2237.                            | _ => measure t
  2238.                            end.
  2239.     Proof.
  2240.       reflexivity .
  2241.     Qed.
  2242.    
  2243.     Lemma marked_measure_star_monotonic :
  2244.      forall f l1 l2,
  2245.       (TransClosure.refl_trans_clos (weaved_relation.one_step_list (algebra.EQT.one_step
  2246.                                                                    R_xml_0_rules)
  2247.                                                                    )
  2248.         l1 l2) ->
  2249.        marked_measure (algebra.Alg.Term f l1) <= marked_measure (algebra.Alg.Term
  2250.                                                                   f
  2251.                                                                   l2).
  2252.     Proof.
  2253.       unfold marked_measure in *.
  2254.       apply InterpZ.marked_measure_star_monotonic.
  2255.       intros ;apply P_id_u22_monotonic;assumption.
  2256.       intros ;apply P_id_ack_in_monotonic;assumption.
  2257.       intros ;apply P_id_ack_out_monotonic;assumption.
  2258.       intros ;apply P_id_s_monotonic;assumption.
  2259.       intros ;apply P_id_u21_monotonic;assumption.
  2260.       intros ;apply P_id_u11_monotonic;assumption.
  2261.       intros ;apply P_id_u22_bounded;assumption.
  2262.       intros ;apply P_id_ack_in_bounded;assumption.
  2263.       intros ;apply P_id_0_bounded;assumption.
  2264.       intros ;apply P_id_ack_out_bounded;assumption.
  2265.       intros ;apply P_id_s_bounded;assumption.
  2266.       intros ;apply P_id_u21_bounded;assumption.
  2267.       intros ;apply P_id_u11_bounded;assumption.
  2268.       apply rules_monotonic.
  2269.       intros ;apply P_id_Marked_u11_monotonic;assumption.
  2270.       intros ;apply P_id_Marked_u22_monotonic;assumption.
  2271.       intros ;apply P_id_Marked_u21_monotonic;assumption.
  2272.       intros ;apply P_id_Marked_ack_in_monotonic;assumption.
  2273.     Qed.
  2274.    
  2275.     Ltac rewrite_and_unfold  :=
  2276.      do 2 (rewrite marked_measure_equation);
  2277.       repeat (
  2278.       match goal with
  2279.         |  |- context [measure (algebra.Alg.Term ?f ?t)] =>
  2280.          rewrite (measure_equation (algebra.Alg.Term f t))
  2281.         | H:context [measure (algebra.Alg.Term ?f ?t)] |- _ =>
  2282.          rewrite (measure_equation (algebra.Alg.Term f t)) in H|-
  2283.         end
  2284.       ).
  2285.    
  2286.    
  2287.     Lemma wf :
  2288.      well_founded (sdp.Rcdp_min R_xml_0_rules DP_R_xml_0_scc_0_large_scc_0).
  2289.     Proof.
  2290.       intros x.
  2291.      
  2292.       apply well_founded_ind with
  2293.         (R:=fun x y => (Zwf.Zwf 0) (marked_measure x) (marked_measure y)).
  2294.       apply Inverse_Image.wf_inverse_image with  (B:=Z).
  2295.       apply Zwf.Zwf_well_founded.
  2296.       clear x.
  2297.       intros x IHx.
  2298.      
  2299.       repeat (
  2300.       constructor;intros y H;
  2301.        repeat progress
  2302.       match goal with
  2303.         | H: _ = _ |- _ => (injection H;clear H;intros;subst)||discriminate H || fail 0
  2304.         | H : sdp.Rcdp _ _ _ _ |- _ => inversion H;clear H; subst
  2305.         | H : DP_R_xml_0_scc_0_large_scc_0 _ _ |- _ => inversion H;clear H; subst
  2306.         | H : algebra.EQT.axiom _ _ _ |- _ => inversion H;clear H; subst
  2307.         | H : sdp.Rcdp_min _ _ _ _ |- _ => destruct H as [H _]
  2308.         | H : TransClosure.refl_trans_clos (weaved_relation.one_step_list _) (_::_) _ |- _ =>
  2309.           apply algebra.EQT_ext.one_step_list_star_decompose_cons in H;
  2310.               let x := fresh "x" in
  2311.               let l := fresh "l" in
  2312.               let h1 := fresh "h" in
  2313.               let h2 := fresh "h" in
  2314.                 destruct H as [ x [ l [ h1 [ h2 H ]]]]
  2315.         | H : TransClosure.refl_trans_clos (weaved_relation.one_step_list _) nil _  |- _ =>
  2316.           apply algebra.EQT_ext.one_step_list_star_decompose_nil in H;
  2317.             subst
  2318.       end ;
  2319.        simpl algebra.Alg.apply_subst in |-*;
  2320.        full_prove_ineq algebra.Alg.Term
  2321.        ltac:(algebra.Alg_ext.find_replacement )
  2322.        algebra.EQT_ext.one_step_list_refl_trans_clos marked_measure
  2323.        marked_measure_star_monotonic (Zwf.Zwf 0) (interp.o_Z 0)
  2324.        ltac:(fun _ => impossible_star_reduction_R_xml_0 )
  2325.        ltac:(fun _ => rewrite_and_unfold ) ltac:(fun _ => generate_pos_hyp )
  2326.        
  2327.        ltac:(fun _ => cbv beta iota zeta delta - [Zplus Zmult Zle Zlt] in * ;
  2328.                        try (constructor))
  2329.         IHx algebra.Alg.apply_subst
  2330.       ).
  2331.     Qed.
  2332.    End WF_DP_R_xml_0_scc_0_large_scc_0.
  2333.    
  2334.    Definition wf_DP_R_xml_0_scc_0_large_scc_0  :=
  2335.      WF_DP_R_xml_0_scc_0_large_scc_0.wf.
  2336.    
  2337.    
  2338.    Lemma acc_DP_R_xml_0_scc_0_large_scc_0 :
  2339.     forall x sigma,
  2340.      In x (List.map (algebra.Alg.apply_subst sigma)
  2341.             ((algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term
  2342.               algebra.F.id_s ((algebra.Alg.Var 2)::nil))::
  2343.               (algebra.Alg.Var 1)::nil))::nil)) ->
  2344.       Acc (sdp.Rcdp_min R_xml_0_rules DP_R_xml_0_scc_0_large) x.
  2345.    Proof.
  2346.      intros x.
  2347.      pattern x.
  2348.      
  2349.      apply well_founded_induction with (1:=wf_DP_R_xml_0_scc_0_large_scc_0) .
  2350.      clear .
  2351.      intros x IH sigma H0.
  2352.      simpl in H0|-.
  2353.      
  2354.      constructor;intros y Hy;inversion Hy;clear Hy;subst;destruct H;
  2355.       inversion H2;clear H2;subst;revert H3 H1;destruct H5;intros H3 H1;
  2356.       match goal with
  2357.         |  |- Acc _
  2358.                (algebra.Alg.apply_subst ?sigma
  2359.                  (algebra.Alg.Term algebra.F.id_u21 ((algebra.Alg.Term
  2360.                   algebra.F.id_ack_in ((algebra.Alg.Term algebra.F.id_s
  2361.                   ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Var 1)::nil))::
  2362.                   (algebra.Alg.Var 2)::nil))) =>
  2363.          apply acc_DP_R_xml_0_scc_0_large_non_scc_1 with sigma;apply in_map;
  2364.           (rewrite (algebra.EQT_ext.inb_equiv _ algebra.Alg.eq_bool);
  2365.            [vm_compute in |-*;refine (refl_equal _)|
  2366.            apply algebra.Alg_ext.term_eq_bool_equiv])
  2367.         |  |- Acc _
  2368.                (algebra.Alg.apply_subst ?sigma
  2369.                  (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term
  2370.                   algebra.F.id_s ((algebra.Alg.Var 2)::nil))::
  2371.                   (algebra.Alg.Var 1)::nil))) =>
  2372.          (apply IH with sigma;
  2373.           [(constructor;
  2374.             [(constructor 1 with l2;[assumption|rewrite  <- H3]);
  2375.               constructor constructor|assumption])|
  2376.           apply in_map;
  2377.            (rewrite (algebra.EQT_ext.inb_equiv _ algebra.Alg.eq_bool);
  2378.             [vm_compute in |-*;refine (refl_equal _)|
  2379.             apply algebra.Alg_ext.term_eq_bool_equiv])])
  2380.         |  |- _ =>
  2381.          simpl in H0|-;injection H3;clear H3;intros ;subst;
  2382.           repeat (
  2383.           match type of H0 with
  2384.             | or _ _ => destruct H0 as [H0| H0]
  2385.             | False => elim H0
  2386.             end
  2387.           );
  2388.           (discriminate H0)||
  2389.           (injection H0;clear H0;intros ;subst;
  2390.             repeat (
  2391.             match goal with
  2392.               | H:TransClosure.refl_trans_clos (weaved_relation.one_step_list _) _ _
  2393.                     |- _ =>
  2394.                destruct (algebra.EQT_ext.cons_star _ _ _ _ _ H) ;clear H
  2395.               end
  2396.             );
  2397.             (impossible_star_reduction_R_xml_0 )||
  2398.             (repeat (
  2399.              match goal with
  2400.                | H:TransClosure.refl_trans_clos (weaved_relation.one_step_list _) _ _
  2401.                      |- _ =>
  2402.                 destruct (algebra.EQT_ext.cons_star _ _ _ _ _ H) ;clear H
  2403.                | H:TransClosure.refl_trans_clos (algebra.EQT.one_step _) (algebra.Alg.Term ?f1 ?l1) (algebra.Alg.Term ?f2 ?l2)
  2404.                      |- _ =>
  2405.                 match f1 with
  2406.                   | f2 => fail 1
  2407.                   | _ =>  destruct (algebra.EQT_ext.trans_at_top _  f1 l1 f2 l2 _ _ H (refl_equal _) (refl_equal _) ) as [l [u [h1 [h2 h3]]]];clear H;[
  2408.                     intros;discriminate|]
  2409.                   end
  2410.                
  2411.                | H:algebra.EQT.axiom _ _ _ |- _ =>
  2412.                 inversion H;clear H;subst
  2413.                | H:R_xml_0_rules  _ _ |- _ => inversion H;clear H;subst
  2414.                | H:_ = _ |- _ =>
  2415.                 discriminate H || (simpl in H;injection H;clear H;intros;subst) ||fail 0
  2416.                end
  2417.              );impossible_star_reduction_R_xml_0 ))
  2418.         end
  2419.       .
  2420.    Qed.
  2421.    
  2422.    
  2423.    Lemma wf :
  2424.     well_founded (sdp.Rcdp_min R_xml_0_rules DP_R_xml_0_scc_0_large).
  2425.    Proof.
  2426.      constructor;intros y Hy;inversion Hy;clear Hy;subst;destruct H;
  2427.       inversion H1;clear H1;subst;revert H2 H0;case H4;intros H2 H0;
  2428.       match goal with
  2429.         |  |- Acc _
  2430.                (algebra.Alg.apply_subst ?sigma
  2431.                  (algebra.Alg.Term algebra.F.id_u21 ((algebra.Alg.Term
  2432.                   algebra.F.id_ack_in ((algebra.Alg.Term algebra.F.id_s
  2433.                   ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Var 1)::nil))::
  2434.                   (algebra.Alg.Var 2)::nil))) =>
  2435.          apply acc_DP_R_xml_0_scc_0_large_non_scc_1 with sigma;apply in_map;
  2436.           (rewrite (algebra.EQT_ext.inb_equiv _ algebra.Alg.eq_bool);
  2437.            [vm_compute in |-*;refine (refl_equal _)|
  2438.            apply algebra.Alg_ext.term_eq_bool_equiv])
  2439.         |  |- Acc _
  2440.                (algebra.Alg.apply_subst ?sigma
  2441.                  (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term
  2442.                   algebra.F.id_s ((algebra.Alg.Var 2)::nil))::
  2443.                   (algebra.Alg.Var 1)::nil))) =>
  2444.          apply acc_DP_R_xml_0_scc_0_large_scc_0 with sigma;apply in_map;
  2445.           (rewrite (algebra.EQT_ext.inb_equiv _ algebra.Alg.eq_bool);
  2446.            [vm_compute in |-*;refine (refl_equal _)|
  2447.            apply algebra.Alg_ext.term_eq_bool_equiv])
  2448.         |  |- _ =>
  2449.          injection H;clear H;intros ;subst;
  2450.           repeat (
  2451.           match goal with
  2452.             | H:TransClosure.refl_trans_clos (weaved_relation.one_step_list _) _ _
  2453.                   |- _ =>
  2454.              destruct (algebra.EQT_ext.cons_star _ _ _ _ _ H) ;clear H
  2455.             end
  2456.           );
  2457.           (impossible_star_reduction_R_xml_0 )||
  2458.           (repeat (
  2459.            match goal with
  2460.              | H:TransClosure.refl_trans_clos (weaved_relation.one_step_list _) _ _
  2461.                    |- _ =>
  2462.               destruct (algebra.EQT_ext.cons_star _ _ _ _ _ H) ;clear H
  2463.              | H:TransClosure.refl_trans_clos (algebra.EQT.one_step _) (algebra.Alg.Term ?f1 ?l1) (algebra.Alg.Term ?f2 ?l2)
  2464.                    |- _ =>
  2465.               match f1 with
  2466.                 | f2 => fail 1
  2467.                 | _ =>  destruct (algebra.EQT_ext.trans_at_top _  f1 l1 f2 l2 _ _ H (refl_equal _) (refl_equal _) ) as [l [u [h1 [h2 h3]]]];clear H;[
  2468.                     intros;discriminate|]
  2469.                 end
  2470.              
  2471.              | H:algebra.EQT.axiom _ _ _ |- _ => inversion H;clear H;subst
  2472.              | H:R_xml_0_rules  _ _ |- _ => inversion H;clear H;subst
  2473.              | H:_ = _ |- _ =>
  2474.               discriminate H || (simpl in H;injection H;clear H;intros;subst) ||fail 0
  2475.              end
  2476.            );impossible_star_reduction_R_xml_0 )
  2477.         end
  2478.       .
  2479.    Qed.
  2480.   End WF_DP_R_xml_0_scc_0_large.
  2481.  
  2482.   Open Scope Z_scope.
  2483.  
  2484.   Import ring_extention.
  2485.  
  2486.   Notation Local "a <= b" := (Zle a b).
  2487.  
  2488.   Notation Local "a < b" := (Zlt a b).
  2489.  
  2490.   Definition P_id_u22 (x4:Z) := 0.
  2491.  
  2492.   Definition P_id_ack_in (x4:Z) (x5:Z) := 0.
  2493.  
  2494.   Definition P_id_0  := 0.
  2495.  
  2496.   Definition P_id_ack_out (x4:Z) := 0.
  2497.  
  2498.   Definition P_id_s (x4:Z) := 1 + 1* x4 + 0.
  2499.  
  2500.   Definition P_id_u21 (x4:Z) (x5:Z) := 0.
  2501.  
  2502.   Definition P_id_u11 (x4:Z) := 0.
  2503.  
  2504.   Lemma P_id_u22_monotonic :
  2505.    forall x4 x5, (0 <= x5)/\ (x5 <= x4) ->P_id_u22 x5 <= P_id_u22 x4.
  2506.   Proof.
  2507.     intros x5 x4.
  2508.     intros [H_1 H_0].
  2509.    
  2510.     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2511.      ring_simplify ;
  2512.      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2513.   Qed.
  2514.  
  2515.   Lemma P_id_ack_in_monotonic :
  2516.    forall x4 x6 x5 x7,
  2517.     (0 <= x7)/\ (x7 <= x6) ->
  2518.      (0 <= x5)/\ (x5 <= x4) ->P_id_ack_in x5 x7 <= P_id_ack_in x4 x6.
  2519.   Proof.
  2520.     intros x7 x6 x5 x4.
  2521.     intros [H_1 H_0].
  2522.     intros [H_3 H_2].
  2523.    
  2524.     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2525.      ring_simplify ;
  2526.      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2527.   Qed.
  2528.  
  2529.   Lemma P_id_ack_out_monotonic :
  2530.    forall x4 x5, (0 <= x5)/\ (x5 <= x4) ->P_id_ack_out x5 <= P_id_ack_out x4.
  2531.   Proof.
  2532.     intros x5 x4.
  2533.     intros [H_1 H_0].
  2534.    
  2535.     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2536.      ring_simplify ;
  2537.      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2538.   Qed.
  2539.  
  2540.   Lemma P_id_s_monotonic :
  2541.    forall x4 x5, (0 <= x5)/\ (x5 <= x4) ->P_id_s x5 <= P_id_s x4.
  2542.   Proof.
  2543.     intros x5 x4.
  2544.     intros [H_1 H_0].
  2545.    
  2546.     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2547.      ring_simplify ;
  2548.      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2549.   Qed.
  2550.  
  2551.   Lemma P_id_u21_monotonic :
  2552.    forall x4 x6 x5 x7,
  2553.     (0 <= x7)/\ (x7 <= x6) ->
  2554.      (0 <= x5)/\ (x5 <= x4) ->P_id_u21 x5 x7 <= P_id_u21 x4 x6.
  2555.   Proof.
  2556.     intros x7 x6 x5 x4.
  2557.     intros [H_1 H_0].
  2558.     intros [H_3 H_2].
  2559.    
  2560.     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2561.      ring_simplify ;
  2562.      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2563.   Qed.
  2564.  
  2565.   Lemma P_id_u11_monotonic :
  2566.    forall x4 x5, (0 <= x5)/\ (x5 <= x4) ->P_id_u11 x5 <= P_id_u11 x4.
  2567.   Proof.
  2568.     intros x5 x4.
  2569.     intros [H_1 H_0].
  2570.    
  2571.     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2572.      ring_simplify ;
  2573.      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2574.   Qed.
  2575.  
  2576.   Lemma P_id_u22_bounded : forall x4, (0 <= x4) ->0 <= P_id_u22 x4.
  2577.   Proof.
  2578.     intros .
  2579.    
  2580.     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2581.      ring_simplify ;
  2582.      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2583.   Qed.
  2584.  
  2585.   Lemma P_id_ack_in_bounded :
  2586.    forall x4 x5, (0 <= x4) ->(0 <= x5) ->0 <= P_id_ack_in x5 x4.
  2587.   Proof.
  2588.     intros .
  2589.    
  2590.     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2591.      ring_simplify ;
  2592.      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2593.   Qed.
  2594.  
  2595.   Lemma P_id_0_bounded : 0 <= P_id_0 .
  2596.   Proof.
  2597.     intros .
  2598.    
  2599.     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2600.      ring_simplify ;
  2601.      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2602.   Qed.
  2603.  
  2604.   Lemma P_id_ack_out_bounded : forall x4, (0 <= x4) ->0 <= P_id_ack_out x4.
  2605.   Proof.
  2606.     intros .
  2607.    
  2608.     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2609.      ring_simplify ;
  2610.      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2611.   Qed.
  2612.  
  2613.   Lemma P_id_s_bounded : forall x4, (0 <= x4) ->0 <= P_id_s x4.
  2614.   Proof.
  2615.     intros .
  2616.    
  2617.     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2618.      ring_simplify ;
  2619.      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2620.   Qed.
  2621.  
  2622.   Lemma P_id_u21_bounded :
  2623.    forall x4 x5, (0 <= x4) ->(0 <= x5) ->0 <= P_id_u21 x5 x4.
  2624.   Proof.
  2625.     intros .
  2626.    
  2627.     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2628.      ring_simplify ;
  2629.      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2630.   Qed.
  2631.  
  2632.   Lemma P_id_u11_bounded : forall x4, (0 <= x4) ->0 <= P_id_u11 x4.
  2633.   Proof.
  2634.     intros .
  2635.    
  2636.     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2637.      ring_simplify ;
  2638.      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2639.   Qed.
  2640.  
  2641.   Definition measure  :=
  2642.     InterpZ.measure 0 P_id_u22 P_id_ack_in P_id_0 P_id_ack_out P_id_s
  2643.      P_id_u21 P_id_u11.
  2644.  
  2645.   Lemma measure_equation :
  2646.    forall t,
  2647.     measure t = match t with
  2648.                   | (algebra.Alg.Term algebra.F.id_u22 (x4::nil)) =>
  2649.                    P_id_u22 (measure x4)
  2650.                   | (algebra.Alg.Term algebra.F.id_ack_in (x5::x4::nil)) =>
  2651.                    P_id_ack_in (measure x5) (measure x4)
  2652.                   | (algebra.Alg.Term algebra.F.id_0 nil) => P_id_0
  2653.                   | (algebra.Alg.Term algebra.F.id_ack_out (x4::nil)) =>
  2654.                    P_id_ack_out (measure x4)
  2655.                   | (algebra.Alg.Term algebra.F.id_s (x4::nil)) =>
  2656.                    P_id_s (measure x4)
  2657.                   | (algebra.Alg.Term algebra.F.id_u21 (x5::x4::nil)) =>
  2658.                    P_id_u21 (measure x5) (measure x4)
  2659.                   | (algebra.Alg.Term algebra.F.id_u11 (x4::nil)) =>
  2660.                    P_id_u11 (measure x4)
  2661.                   | _ => 0
  2662.                   end.
  2663.   Proof.
  2664.     intros t;
  2665.      refine match t with
  2666.               | (algebra.Alg.Term algebra.F.id_u22 (x4::nil)) => _
  2667.               | (algebra.Alg.Term algebra.F.id_ack_in (x5::x4::nil)) =>
  2668.               _
  2669.               | (algebra.Alg.Term algebra.F.id_0 nil) => _
  2670.               | (algebra.Alg.Term algebra.F.id_ack_out (x4::nil)) =>
  2671.               _
  2672.               | (algebra.Alg.Term algebra.F.id_s (x4::nil)) => _
  2673.               | (algebra.Alg.Term algebra.F.id_u21 (x5::x4::nil)) =>
  2674.               _
  2675.               | (algebra.Alg.Term algebra.F.id_u11 (x4::nil)) => _
  2676.               | _ => _
  2677.               end;apply refl_equal.
  2678.   Qed.
  2679.  
  2680.   Lemma measure_bounded : forall t, 0 <= measure t.
  2681.   Proof.
  2682.     unfold measure in |-*.
  2683.    
  2684.     apply InterpZ.measure_bounded;
  2685.      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2686.       ring_simplify ;
  2687.       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2688.   Qed.
  2689.  
  2690.   Ltac generate_pos_hyp  :=
  2691.    match goal with
  2692.      | H:context [measure ?x] |- _ =>
  2693.       let v := fresh "v" in
  2694.        (let H := fresh "h" in
  2695.          (set (H:=measure_bounded x) in *;set (v:=measure x) in *;
  2696.            clearbody H;clearbody v))
  2697.      |  |- context [measure ?x] =>
  2698.       let v := fresh "v" in
  2699.        (let H := fresh "h" in
  2700.          (set (H:=measure_bounded x) in *;set (v:=measure x) in *;
  2701.            clearbody H;clearbody v))
  2702.      end
  2703.    .
  2704.  
  2705.   Lemma rules_monotonic :
  2706.    forall l r,
  2707.     (algebra.EQT.axiom R_xml_0_rules r l) ->measure r <= measure l.
  2708.   Proof.
  2709.     intros l r H.
  2710.     fold measure in |-*.
  2711.    
  2712.     inversion H;clear H;subst;inversion H0;clear H0;subst;
  2713.      simpl algebra.EQT.T.apply_subst in |-*;
  2714.      repeat (
  2715.      match goal with
  2716.        |  |- context [measure (algebra.Alg.Term ?f ?t)] =>
  2717.         rewrite (measure_equation (algebra.Alg.Term f t))
  2718.        end
  2719.      );repeat (generate_pos_hyp );
  2720.      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2721.       ring_simplify ;
  2722.       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2723.   Qed.
  2724.  
  2725.   Lemma measure_star_monotonic :
  2726.    forall l r,
  2727.     (TransClosure.refl_trans_clos (algebra.EQT.one_step R_xml_0_rules) r l) ->
  2728.      measure r <= measure l.
  2729.   Proof.
  2730.     unfold measure in *.
  2731.     apply InterpZ.measure_star_monotonic.
  2732.     intros ;apply P_id_u22_monotonic;assumption.
  2733.     intros ;apply P_id_ack_in_monotonic;assumption.
  2734.     intros ;apply P_id_ack_out_monotonic;assumption.
  2735.     intros ;apply P_id_s_monotonic;assumption.
  2736.     intros ;apply P_id_u21_monotonic;assumption.
  2737.     intros ;apply P_id_u11_monotonic;assumption.
  2738.     intros ;apply P_id_u22_bounded;assumption.
  2739.     intros ;apply P_id_ack_in_bounded;assumption.
  2740.     intros ;apply P_id_0_bounded;assumption.
  2741.     intros ;apply P_id_ack_out_bounded;assumption.
  2742.     intros ;apply P_id_s_bounded;assumption.
  2743.     intros ;apply P_id_u21_bounded;assumption.
  2744.     intros ;apply P_id_u11_bounded;assumption.
  2745.     apply rules_monotonic.
  2746.   Qed.
  2747.  
  2748.   Definition P_id_Marked_u11 (x4:Z) := 1* x4 + 0.
  2749.  
  2750.   Definition P_id_Marked_u22 (x4:Z) := 1* x4 + 0.
  2751.  
  2752.   Definition P_id_Marked_u21 (x4:Z) (x5:Z) := 1 + 1* x5 + 0.
  2753.  
  2754.   Definition P_id_Marked_ack_in (x4:Z) (x5:Z) := 1* x4 + 0.
  2755.  
  2756.   Lemma P_id_Marked_u11_monotonic :
  2757.    forall x4 x5,
  2758.     (0 <= x5)/\ (x5 <= x4) ->P_id_Marked_u11 x5 <= P_id_Marked_u11 x4.
  2759.   Proof.
  2760.     intros x5 x4.
  2761.     intros [H_1 H_0].
  2762.    
  2763.     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2764.      ring_simplify ;
  2765.      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2766.   Qed.
  2767.  
  2768.   Lemma P_id_Marked_u22_monotonic :
  2769.    forall x4 x5,
  2770.     (0 <= x5)/\ (x5 <= x4) ->P_id_Marked_u22 x5 <= P_id_Marked_u22 x4.
  2771.   Proof.
  2772.     intros x5 x4.
  2773.     intros [H_1 H_0].
  2774.    
  2775.     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2776.      ring_simplify ;
  2777.      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2778.   Qed.
  2779.  
  2780.   Lemma P_id_Marked_u21_monotonic :
  2781.    forall x4 x6 x5 x7,
  2782.     (0 <= x7)/\ (x7 <= x6) ->
  2783.      (0 <= x5)/\ (x5 <= x4) ->P_id_Marked_u21 x5 x7 <= P_id_Marked_u21 x4 x6.
  2784.   Proof.
  2785.     intros x7 x6 x5 x4.
  2786.     intros [H_1 H_0].
  2787.     intros [H_3 H_2].
  2788.    
  2789.     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2790.      ring_simplify ;
  2791.      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2792.   Qed.
  2793.  
  2794.   Lemma P_id_Marked_ack_in_monotonic :
  2795.    forall x4 x6 x5 x7,
  2796.     (0 <= x7)/\ (x7 <= x6) ->
  2797.      (0 <= x5)/\ (x5 <= x4) ->
  2798.       P_id_Marked_ack_in x5 x7 <= P_id_Marked_ack_in x4 x6.
  2799.   Proof.
  2800.     intros x7 x6 x5 x4.
  2801.     intros [H_1 H_0].
  2802.     intros [H_3 H_2].
  2803.    
  2804.     cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2805.      ring_simplify ;
  2806.      (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2807.   Qed.
  2808.  
  2809.   Definition marked_measure  :=
  2810.     InterpZ.marked_measure 0 P_id_u22 P_id_ack_in P_id_0 P_id_ack_out
  2811.      P_id_s P_id_u21 P_id_u11 P_id_Marked_u11 P_id_Marked_u22
  2812.      P_id_Marked_u21 P_id_Marked_ack_in.
  2813.  
  2814.   Lemma marked_measure_equation :
  2815.    forall t,
  2816.     marked_measure t = match t with
  2817.                          | (algebra.Alg.Term algebra.F.id_u11 (x4::nil)) =>
  2818.                           P_id_Marked_u11 (measure x4)
  2819.                          | (algebra.Alg.Term algebra.F.id_u22 (x4::nil)) =>
  2820.                           P_id_Marked_u22 (measure x4)
  2821.                          | (algebra.Alg.Term algebra.F.id_u21 (x5::x4::nil)) =>
  2822.                           P_id_Marked_u21 (measure x5) (measure x4)
  2823.                          | (algebra.Alg.Term algebra.F.id_ack_in (x5::
  2824.                             x4::nil)) =>
  2825.                           P_id_Marked_ack_in (measure x5) (measure x4)
  2826.                          | _ => measure t
  2827.                          end.
  2828.   Proof.
  2829.     reflexivity .
  2830.   Qed.
  2831.  
  2832.   Lemma marked_measure_star_monotonic :
  2833.    forall f l1 l2,
  2834.     (TransClosure.refl_trans_clos (weaved_relation.one_step_list (algebra.EQT.one_step
  2835.                                                                    R_xml_0_rules)
  2836.                                                                   )
  2837.       l1 l2) ->
  2838.      marked_measure (algebra.Alg.Term f l1) <= marked_measure (algebra.Alg.Term
  2839.                                                                 f l2).
  2840.   Proof.
  2841.     unfold marked_measure in *.
  2842.     apply InterpZ.marked_measure_star_monotonic.
  2843.     intros ;apply P_id_u22_monotonic;assumption.
  2844.     intros ;apply P_id_ack_in_monotonic;assumption.
  2845.     intros ;apply P_id_ack_out_monotonic;assumption.
  2846.     intros ;apply P_id_s_monotonic;assumption.
  2847.     intros ;apply P_id_u21_monotonic;assumption.
  2848.     intros ;apply P_id_u11_monotonic;assumption.
  2849.     intros ;apply P_id_u22_bounded;assumption.
  2850.     intros ;apply P_id_ack_in_bounded;assumption.
  2851.     intros ;apply P_id_0_bounded;assumption.
  2852.     intros ;apply P_id_ack_out_bounded;assumption.
  2853.     intros ;apply P_id_s_bounded;assumption.
  2854.     intros ;apply P_id_u21_bounded;assumption.
  2855.     intros ;apply P_id_u11_bounded;assumption.
  2856.     apply rules_monotonic.
  2857.     intros ;apply P_id_Marked_u11_monotonic;assumption.
  2858.     intros ;apply P_id_Marked_u22_monotonic;assumption.
  2859.     intros ;apply P_id_Marked_u21_monotonic;assumption.
  2860.     intros ;apply P_id_Marked_ack_in_monotonic;assumption.
  2861.   Qed.
  2862.  
  2863.   Ltac rewrite_and_unfold  :=
  2864.    do 2 (rewrite marked_measure_equation);
  2865.     repeat (
  2866.     match goal with
  2867.       |  |- context [measure (algebra.Alg.Term ?f ?t)] =>
  2868.        rewrite (measure_equation (algebra.Alg.Term f t))
  2869.       | H:context [measure (algebra.Alg.Term ?f ?t)] |- _ =>
  2870.        rewrite (measure_equation (algebra.Alg.Term f t)) in H|-
  2871.       end
  2872.     ).
  2873.  
  2874.   Definition lt a b := (Zwf.Zwf 0) (marked_measure a) (marked_measure b).
  2875.  
  2876.   Definition le a b := marked_measure a <= marked_measure b.
  2877.  
  2878.   Lemma lt_le_compat : forall a b c, (lt a b) ->(le b c) ->lt a c.
  2879.   Proof.
  2880.     unfold lt, le in *.
  2881.     intros a b c.
  2882.     apply (interp.le_lt_compat_right (interp.o_Z 0)).
  2883.   Qed.
  2884.  
  2885.   Lemma wf_lt : well_founded lt.
  2886.   Proof.
  2887.     unfold lt in *.
  2888.     apply Inverse_Image.wf_inverse_image with  (B:=Z).
  2889.     apply Zwf.Zwf_well_founded.
  2890.   Qed.
  2891.  
  2892.   Lemma DP_R_xml_0_scc_0_strict_in_lt :
  2893.    Relation_Definitions.inclusion _
  2894.     (sdp.Rcdp_min R_xml_0_rules DP_R_xml_0_scc_0_strict) lt.
  2895.   Proof.
  2896.     unfold Relation_Definitions.inclusion, lt in *.
  2897.    
  2898.     intros a b H;destruct H;clear H0;destruct H;inversion H0;clear H0;
  2899.      subst;destruct H3;injection H1;clear H1;intros ;subst;
  2900.      repeat (
  2901. match goal with
  2902.     | H:TransClosure.refl_trans_clos (weaved_relation.one_step_list _) (_::_) ?l1
  2903.     |- _ =>
  2904.     let x := fresh "x" in
  2905.     let l := fresh "l" in
  2906.     let heq := fresh "heq" in
  2907.     let h1 := fresh "h" in
  2908.     let h2:= fresh "h" in
  2909.     destruct (algebra.EQT_ext.one_step_list_star_decompose_cons _ _ _ _ H) as
  2910.      [x [ l [ heq [h1 h2]]]];
  2911.    clear H;subst l1
  2912.     | H:TransClosure.refl_trans_clos (weaved_relation.one_step_list _)  nil ?l1 |- _ =>
  2913.         let heq := fresh "heq" in
  2914.         set (heq := algebra.EQT_ext.one_step_list_star_decompose_nil _ _ H);
  2915.         clearbody heq; clear H;subst l1
  2916. end) ;
  2917.      
  2918.      match goal with
  2919.        |  |- (Zwf.Zwf 0) _ (marked_measure (algebra.Alg.Term ?f ?l)) =>
  2920.         let l'' := algebra.Alg_ext.find_replacement l  in
  2921.          ((apply (interp.le_lt_compat_right (interp.o_Z 0)) with
  2922.             (marked_measure (algebra.Alg.Term f l''));[idtac|
  2923.            apply marked_measure_star_monotonic;
  2924.             repeat (apply algebra.EQT_ext.one_step_list_refl_trans_clos);
  2925.             (assumption)||(constructor 1)]))
  2926.        end
  2927.      ;clear ;simpl algebra.Alg.apply_subst in *;rewrite_and_unfold ;
  2928.      repeat (generate_pos_hyp );
  2929.      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2930.       ring_simplify ;
  2931.       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2932.   Qed.
  2933.  
  2934.   Lemma DP_R_xml_0_scc_0_large_in_le :
  2935.    Relation_Definitions.inclusion _
  2936.     (sdp.Rcdp_min R_xml_0_rules DP_R_xml_0_scc_0_large) le.
  2937.   Proof.
  2938.     unfold Relation_Definitions.inclusion, le, Zwf.Zwf in *.
  2939.    
  2940.     intros a b H;destruct H;clear H0;destruct H;inversion H0;clear H0;
  2941.      subst;destruct H3;injection H1;clear H1;intros ;subst;
  2942.      repeat (
  2943. match goal with
  2944.     | H:TransClosure.refl_trans_clos (weaved_relation.one_step_list _) (_::_) ?l1
  2945.     |- _ =>
  2946.     let x := fresh "x" in
  2947.     let l := fresh "l" in
  2948.     let heq := fresh "heq" in
  2949.     let h1 := fresh "h" in
  2950.     let h2:= fresh "h" in
  2951.     destruct (algebra.EQT_ext.one_step_list_star_decompose_cons _ _ _ _ H) as
  2952.      [x [ l [ heq [h1 h2]]]];
  2953.    clear H;subst l1
  2954.     | H:TransClosure.refl_trans_clos (weaved_relation.one_step_list _)  nil ?l1 |- _ =>
  2955.         let heq := fresh "heq" in
  2956.         set (heq := algebra.EQT_ext.one_step_list_star_decompose_nil _ _ H);
  2957.         clearbody heq; clear H;subst l1
  2958. end) ;
  2959.      
  2960.      match goal with
  2961.        |  |- _ <= marked_measure (algebra.Alg.Term ?f ?l) =>
  2962.         let l'' := algebra.Alg_ext.find_replacement l  in
  2963.          ((apply (interp.le_trans (interp.o_Z 0)) with
  2964.             (marked_measure (algebra.Alg.Term f l''));[idtac|
  2965.            apply marked_measure_star_monotonic;
  2966.             repeat (apply algebra.EQT_ext.one_step_list_refl_trans_clos);
  2967.             (assumption)||(constructor 1)]))
  2968.        end
  2969.      ;clear ;simpl algebra.Alg.apply_subst in *;rewrite_and_unfold ;
  2970.      repeat (generate_pos_hyp );
  2971.      cbv beta iota zeta delta - [Zle Zlt Zplus Zmult] ;intuition;
  2972.       ring_simplify ;
  2973.       (auto with zarith)||(repeat (translate_vars );prove_ineq ).
  2974.   Qed.
  2975.  
  2976.   Definition wf_DP_R_xml_0_scc_0_large  := WF_DP_R_xml_0_scc_0_large.wf.
  2977.  
  2978.  
  2979.   Lemma wf : well_founded (sdp.Rcdp_min R_xml_0_rules DP_R_xml_0_scc_0).
  2980.   Proof.
  2981.     intros x.
  2982.     apply (well_founded_ind wf_lt).
  2983.     clear x.
  2984.     intros x.
  2985.     pattern x.
  2986.     apply (@Acc_ind _ (sdp.Rcdp_min R_xml_0_rules DP_R_xml_0_scc_0_large)).
  2987.     clear x.
  2988.     intros x _ IHx IHx'.
  2989.      constructor.
  2990.      intros y H.
  2991.      destruct H.
  2992.      destruct H.
  2993.      inversion H1;clear H1;subst.
  2994.      destruct H4;injection H2;intros .
  2995.      
  2996.      apply IHx';apply DP_R_xml_0_scc_0_strict_in_lt;
  2997.      (constructor;
  2998.       [(constructor 1 with l2;[refine H|
  2999.         subst;rewrite  <- H2;constructor;constructor])|assumption]).
  3000.    
  3001.     (apply IHx;
  3002.      [(constructor;
  3003.        [(constructor 1 with l2;[refine H|
  3004.          subst;rewrite  <- H2;constructor;constructor])|assumption])|
  3005.      intros y' Hlt;apply IHx';apply lt_le_compat with (1:=Hlt) ;
  3006.       apply DP_R_xml_0_scc_0_large_in_le;
  3007.       (constructor;
  3008.        [(constructor 1 with l2;[refine H|
  3009.          subst;rewrite  <- H2;constructor;constructor])|assumption])]).
  3010.    
  3011.     (apply IHx;
  3012.      [(constructor;
  3013.        [(constructor 1 with l2;[refine H|
  3014.          subst;rewrite  <- H2;constructor;constructor])|assumption])|
  3015.      intros y' Hlt;apply IHx';apply lt_le_compat with (1:=Hlt) ;
  3016.       apply DP_R_xml_0_scc_0_large_in_le;
  3017.       (constructor;
  3018.        [(constructor 1 with l2;[refine H|
  3019.          subst;rewrite  <- H2;constructor;constructor])|assumption])]).
  3020.    
  3021.     apply IHx';apply DP_R_xml_0_scc_0_strict_in_lt;
  3022.       (constructor;
  3023.        [(constructor 1 with l2;[refine H|
  3024.          subst;rewrite  <- H2;constructor;constructor])|assumption]).
  3025.      apply wf_DP_R_xml_0_scc_0_large.
  3026.    Qed.
  3027.   End WF_DP_R_xml_0_scc_0.
  3028.  
  3029.   Definition wf_DP_R_xml_0_scc_0  := WF_DP_R_xml_0_scc_0.wf.
  3030.  
  3031.  
  3032.   Lemma acc_DP_R_xml_0_scc_0 :
  3033.    forall x sigma,
  3034.     In x (List.map (algebra.Alg.apply_subst sigma)
  3035.            ((algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Var 2)::
  3036.              (algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Term
  3037.              algebra.F.id_0 nil)::nil))::nil))::
  3038.             (algebra.Alg.Term algebra.F.id_u21 ((algebra.Alg.Term
  3039.              algebra.F.id_ack_in ((algebra.Alg.Term algebra.F.id_s
  3040.              ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Var 1)::nil))::
  3041.              (algebra.Alg.Var 2)::nil))::
  3042.              (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term
  3043.               algebra.F.id_s ((algebra.Alg.Var 2)::nil))::
  3044.               (algebra.Alg.Var 1)::nil))::
  3045.               (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Var 2)::
  3046.                (algebra.Alg.Var 1)::nil))::nil)) ->
  3047.      Acc (sdp.Rcdp_min R_xml_0_rules DP_R_xml_0) x.
  3048.   Proof.
  3049.     intros x.
  3050.     pattern x.
  3051.     apply well_founded_induction with (1:=wf_DP_R_xml_0_scc_0) .
  3052.     clear .
  3053.     intros x IH sigma H0.
  3054.     simpl in H0|-.
  3055.    
  3056.     constructor;intros y Hy;inversion Hy;clear Hy;subst;destruct H;
  3057.      inversion H2;clear H2;subst;revert H3 H1;destruct H5;intros H3 H1;
  3058.      match goal with
  3059.        |  |- Acc _
  3060.               (algebra.Alg.apply_subst ?sigma
  3061.                 (algebra.Alg.Term algebra.F.id_u22 ((algebra.Alg.Term
  3062.                  algebra.F.id_ack_in ((algebra.Alg.Var 2)::
  3063.                  (algebra.Alg.Var 1)::nil))::nil))) =>
  3064.         apply acc_DP_R_xml_0_non_scc_2 with sigma;apply in_map;
  3065.          (rewrite (algebra.EQT_ext.inb_equiv _ algebra.Alg.eq_bool);
  3066.           [vm_compute in |-*;refine (refl_equal _)|
  3067.           apply algebra.Alg_ext.term_eq_bool_equiv])
  3068.        |  |- Acc _
  3069.               (algebra.Alg.apply_subst ?sigma
  3070.                 (algebra.Alg.Term algebra.F.id_u11 ((algebra.Alg.Term
  3071.                  algebra.F.id_ack_in ((algebra.Alg.Var 2)::(algebra.Alg.Term
  3072.                  algebra.F.id_s ((algebra.Alg.Term algebra.F.id_0
  3073.                  nil)::nil))::nil))::nil))) =>
  3074.         apply acc_DP_R_xml_0_non_scc_1 with sigma;apply in_map;
  3075.          (rewrite (algebra.EQT_ext.inb_equiv _ algebra.Alg.eq_bool);
  3076.           [vm_compute in |-*;refine (refl_equal _)|
  3077.           apply algebra.Alg_ext.term_eq_bool_equiv])
  3078.        |  |- Acc _
  3079.               (algebra.Alg.apply_subst ?sigma
  3080.                 (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Var 2)::
  3081.                  (algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Term
  3082.                  algebra.F.id_0 nil)::nil))::nil))) =>
  3083.         (apply IH with sigma;
  3084.          [(constructor;
  3085.            [(constructor 1 with l2;[assumption|rewrite  <- H3]);
  3086.              constructor constructor|assumption])|
  3087.          apply in_map;
  3088.           (rewrite (algebra.EQT_ext.inb_equiv _ algebra.Alg.eq_bool);
  3089.            [vm_compute in |-*;refine (refl_equal _)|
  3090.            apply algebra.Alg_ext.term_eq_bool_equiv])])
  3091.        |  |- Acc _
  3092.               (algebra.Alg.apply_subst ?sigma
  3093.                 (algebra.Alg.Term algebra.F.id_u21 ((algebra.Alg.Term
  3094.                  algebra.F.id_ack_in ((algebra.Alg.Term algebra.F.id_s
  3095.                  ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Var 1)::nil))::
  3096.                  (algebra.Alg.Var 2)::nil))) =>
  3097.         (apply IH with sigma;
  3098.          [(constructor;
  3099.            [(constructor 1 with l2;[assumption|rewrite  <- H3]);
  3100.              constructor constructor|assumption])|
  3101.          apply in_map;
  3102.           (rewrite (algebra.EQT_ext.inb_equiv _ algebra.Alg.eq_bool);
  3103.            [vm_compute in |-*;refine (refl_equal _)|
  3104.            apply algebra.Alg_ext.term_eq_bool_equiv])])
  3105.        |  |- Acc _
  3106.               (algebra.Alg.apply_subst ?sigma
  3107.                 (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term
  3108.                  algebra.F.id_s ((algebra.Alg.Var 2)::nil))::
  3109.                  (algebra.Alg.Var 1)::nil))) =>
  3110.         (apply IH with sigma;
  3111.          [(constructor;
  3112.            [(constructor 1 with l2;[assumption|rewrite  <- H3]);
  3113.              constructor constructor|assumption])|
  3114.          apply in_map;
  3115.           (rewrite (algebra.EQT_ext.inb_equiv _ algebra.Alg.eq_bool);
  3116.            [vm_compute in |-*;refine (refl_equal _)|
  3117.            apply algebra.Alg_ext.term_eq_bool_equiv])])
  3118.        |  |- Acc _
  3119.               (algebra.Alg.apply_subst ?sigma
  3120.                 (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Var 2)::
  3121.                  (algebra.Alg.Var 1)::nil))) =>
  3122.         (apply IH with sigma;
  3123.          [(constructor;
  3124.            [(constructor 1 with l2;[assumption|rewrite  <- H3]);
  3125.              constructor constructor|assumption])|
  3126.          apply in_map;
  3127.           (rewrite (algebra.EQT_ext.inb_equiv _ algebra.Alg.eq_bool);
  3128.            [vm_compute in |-*;refine (refl_equal _)|
  3129.            apply algebra.Alg_ext.term_eq_bool_equiv])])
  3130.        |  |- _ =>
  3131.         simpl in H0|-;injection H3;clear H3;intros ;subst;
  3132.          repeat (
  3133.          match type of H0 with
  3134.            | or _ _ => destruct H0 as [H0| H0]
  3135.            | False => elim H0
  3136.            end
  3137.          );
  3138.          (discriminate H0)||
  3139.          (injection H0;clear H0;intros ;subst;
  3140.            repeat (
  3141.            match goal with
  3142.              | H:TransClosure.refl_trans_clos (weaved_relation.one_step_list _) _ _
  3143.                    |- _ =>
  3144.               destruct (algebra.EQT_ext.cons_star _ _ _ _ _ H) ;clear H
  3145.              end
  3146.            );
  3147.            (impossible_star_reduction_R_xml_0 )||
  3148.            (repeat (
  3149.             match goal with
  3150.               | H:TransClosure.refl_trans_clos (weaved_relation.one_step_list _) _ _
  3151.                     |- _ =>
  3152.                destruct (algebra.EQT_ext.cons_star _ _ _ _ _ H) ;clear H
  3153.               | H:TransClosure.refl_trans_clos (algebra.EQT.one_step _) (algebra.Alg.Term ?f1 ?l1) (algebra.Alg.Term ?f2 ?l2)
  3154.                     |- _ =>
  3155.                match f1 with
  3156.                  | f2 => fail 1
  3157.                  | _ =>  destruct (algebra.EQT_ext.trans_at_top _  f1 l1 f2 l2 _ _ H (refl_equal _) (refl_equal _) ) as [l [u [h1 [h2 h3]]]];clear H;[
  3158.                      intros;discriminate|]
  3159.                  end
  3160.                
  3161.               | H:algebra.EQT.axiom _ _ _ |- _ => inversion H;clear H;subst
  3162.               | H:R_xml_0_rules  _ _ |- _ => inversion H;clear H;subst
  3163.               | H:_ = _ |- _ =>
  3164.                discriminate H || (simpl in H;injection H;clear H;intros;subst) ||fail 0
  3165.               end
  3166.             );impossible_star_reduction_R_xml_0 ))
  3167.        end
  3168.      .
  3169.   Qed.
  3170.  
  3171.  
  3172.   Lemma wf : well_founded (sdp.Rcdp_min R_xml_0_rules DP_R_xml_0).
  3173.   Proof.
  3174.     constructor;intros y Hy;inversion Hy;clear Hy;subst;destruct H;
  3175.      inversion H1;clear H1;subst;revert H2 H0;case H4;intros H2 H0;
  3176.      match goal with
  3177.        |  |- Acc _
  3178.               (algebra.Alg.apply_subst ?sigma
  3179.                 (algebra.Alg.Term algebra.F.id_u22 ((algebra.Alg.Term
  3180.                  algebra.F.id_ack_in ((algebra.Alg.Var 2)::
  3181.                  (algebra.Alg.Var 1)::nil))::nil))) =>
  3182.         apply acc_DP_R_xml_0_non_scc_2 with sigma;apply in_map;
  3183.          (rewrite (algebra.EQT_ext.inb_equiv _ algebra.Alg.eq_bool);
  3184.           [vm_compute in |-*;refine (refl_equal _)|
  3185.           apply algebra.Alg_ext.term_eq_bool_equiv])
  3186.        |  |- Acc _
  3187.               (algebra.Alg.apply_subst ?sigma
  3188.                 (algebra.Alg.Term algebra.F.id_u11 ((algebra.Alg.Term
  3189.                  algebra.F.id_ack_in ((algebra.Alg.Var 2)::(algebra.Alg.Term
  3190.                  algebra.F.id_s ((algebra.Alg.Term algebra.F.id_0
  3191.                  nil)::nil))::nil))::nil))) =>
  3192.         apply acc_DP_R_xml_0_non_scc_1 with sigma;apply in_map;
  3193.          (rewrite (algebra.EQT_ext.inb_equiv _ algebra.Alg.eq_bool);
  3194.           [vm_compute in |-*;refine (refl_equal _)|
  3195.           apply algebra.Alg_ext.term_eq_bool_equiv])
  3196.        |  |- Acc _
  3197.               (algebra.Alg.apply_subst ?sigma
  3198.                 (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Var 2)::
  3199.                  (algebra.Alg.Term algebra.F.id_s ((algebra.Alg.Term
  3200.                  algebra.F.id_0 nil)::nil))::nil))) =>
  3201.         apply acc_DP_R_xml_0_scc_0 with sigma;apply in_map;
  3202.          (rewrite (algebra.EQT_ext.inb_equiv _ algebra.Alg.eq_bool);
  3203.           [vm_compute in |-*;refine (refl_equal _)|
  3204.           apply algebra.Alg_ext.term_eq_bool_equiv])
  3205.        |  |- Acc _
  3206.               (algebra.Alg.apply_subst ?sigma
  3207.                 (algebra.Alg.Term algebra.F.id_u21 ((algebra.Alg.Term
  3208.                  algebra.F.id_ack_in ((algebra.Alg.Term algebra.F.id_s
  3209.                  ((algebra.Alg.Var 2)::nil))::(algebra.Alg.Var 1)::nil))::
  3210.                  (algebra.Alg.Var 2)::nil))) =>
  3211.         apply acc_DP_R_xml_0_scc_0 with sigma;apply in_map;
  3212.          (rewrite (algebra.EQT_ext.inb_equiv _ algebra.Alg.eq_bool);
  3213.           [vm_compute in |-*;refine (refl_equal _)|
  3214.           apply algebra.Alg_ext.term_eq_bool_equiv])
  3215.        |  |- Acc _
  3216.               (algebra.Alg.apply_subst ?sigma
  3217.                 (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Term
  3218.                  algebra.F.id_s ((algebra.Alg.Var 2)::nil))::
  3219.                  (algebra.Alg.Var 1)::nil))) =>
  3220.         apply acc_DP_R_xml_0_scc_0 with sigma;apply in_map;
  3221.          (rewrite (algebra.EQT_ext.inb_equiv _ algebra.Alg.eq_bool);
  3222.           [vm_compute in |-*;refine (refl_equal _)|
  3223.           apply algebra.Alg_ext.term_eq_bool_equiv])
  3224.        |  |- Acc _
  3225.               (algebra.Alg.apply_subst ?sigma
  3226.                 (algebra.Alg.Term algebra.F.id_ack_in ((algebra.Alg.Var 2)::
  3227.                  (algebra.Alg.Var 1)::nil))) =>
  3228.         apply acc_DP_R_xml_0_scc_0 with sigma;apply in_map;
  3229.          (rewrite (algebra.EQT_ext.inb_equiv _ algebra.Alg.eq_bool);
  3230.           [vm_compute in |-*;refine (refl_equal _)|
  3231.           apply algebra.Alg_ext.term_eq_bool_equiv])
  3232.        |  |- _ =>
  3233.         injection H;clear H;intros ;subst;
  3234.          repeat (
  3235.          match goal with
  3236.            | H:TransClosure.refl_trans_clos (weaved_relation.one_step_list _) _ _
  3237.                  |- _ =>
  3238.             destruct (algebra.EQT_ext.cons_star _ _ _ _ _ H) ;clear H
  3239.            end
  3240.          );
  3241.          (impossible_star_reduction_R_xml_0 )||
  3242.          (repeat (
  3243.           match goal with
  3244.             | H:TransClosure.refl_trans_clos (weaved_relation.one_step_list _) _ _
  3245.                   |- _ =>
  3246.              destruct (algebra.EQT_ext.cons_star _ _ _ _ _ H) ;clear H
  3247.             | H:TransClosure.refl_trans_clos (algebra.EQT.one_step _) (algebra.Alg.Term ?f1 ?l1) (algebra.Alg.Term ?f2 ?l2)
  3248.                   |- _ =>
  3249.              match f1 with
  3250.                | f2 => fail 1
  3251.                | _ =>  destruct (algebra.EQT_ext.trans_at_top _  f1 l1 f2 l2 _ _ H (refl_equal _) (refl_equal _) ) as [l [u [h1 [h2 h3]]]];clear H;[
  3252.                      intros;discriminate|]
  3253.                end
  3254.              
  3255.             | H:algebra.EQT.axiom _ _ _ |- _ => inversion H;clear H;subst
  3256.             | H:R_xml_0_rules  _ _ |- _ => inversion H;clear H;subst
  3257.             | H:_ = _ |- _ =>
  3258.              discriminate H || (simpl in H;injection H;clear H;intros;subst) ||fail 0
  3259.             end
  3260.           );impossible_star_reduction_R_xml_0 )
  3261.        end
  3262.      .
  3263.   Qed.
  3264.  End WF_DP_R_xml_0.
  3265.  
  3266.  Ltac destruct_until_cdp_or_notdefined :=
  3267.   match goal with
  3268.     | H: None = Some _ |- _ => inversion H
  3269.     | H:algebra.EQT.defined _ ?f |- _ =>
  3270.       solve [inversion H;
  3271.         match goal with
  3272.           H': R_xml_0_rules _ _ |- _ =>
  3273.            inversion H'
  3274.         end
  3275.         | solve
  3276.           [constructor; constructor |
  3277.             constructor 2; constructor ; constructor |
  3278.               constructor 2 ;constructor 2; constructor |
  3279.               constructor 2 ;constructor 2; constructor 2 ]
  3280.       ]
  3281.     | H: Some _ = Some _ |- _ =>
  3282.       inversion H; clear H;subst
  3283.     | H: (match (nth_error _ ?n) with
  3284.             Some _ => _
  3285.             | None => _ end) = Some _ |- _  =>
  3286.     destruct n;simpl in *
  3287.     | H: algebra.Alg.subterm_at_pos _ ?p = Some _ |- _ => destruct p;simpl in *
  3288.   end.
  3289.  
  3290.  Definition wf_H  := WF_DP_R_xml_0.wf.
  3291.  
  3292.  Lemma wf : well_founded (algebra.EQT.one_step R_xml_0_rules).
  3293.  Proof.
  3294.    apply sdp.Dp.ddp_criterion.
  3295.   intros x t .
  3296.    apply R_xml_0_non_var.
  3297.    apply R_xml_0_reg.
  3298.    intros ;apply (ddp.constructor_defined_dec _ _ R_xml_0_rules_included).
  3299.    
  3300.    
  3301.   apply Inclusion.wf_incl with (2:=wf_H).
  3302.   intros x y.
  3303.   clear;intros H;destruct H;constructor;[|assumption].
  3304.     inversion H. econstructor; try eassumption;subst.
  3305.   inversion H2. constructor.
  3306.  clear -H5.
  3307.   apply sdp.Dp.ddp_list_is_complete with (is_def := algebra.EQT_ext.is_def (sdp.Dp.defined_list R_xml_0_rule_as_list nil)) (1:=R_xml_0_rules_included) in H5.
  3308.   vm_compute in H5;
  3309.   repeat (destruct H5 as [H5|H5]; [ injection H5;clear H5;intros;subst;constructor|]);
  3310.     elim H5.
  3311.  
  3312.   apply algebra.EQT_ext.is_def_equiv.
  3313.   split.
  3314.   apply sdp.Dp.defined_list_sound with (1:=R_xml_0_rules_included).
  3315.   apply sdp.Dp.defined_list_complete with (1:=R_xml_0_rules_included)
  3316.  .
  3317.  Qed.
  3318. End WF_R_xml_0.
  3319.  
  3320.  
  3321. (*
  3322. *** Local Variables: ***
  3323. *** coq-prog-name: "coqtop" ***
  3324. *** 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/") ***
  3325. *** 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/  certificate.v" ***
  3326. *** End: ***
  3327.  *)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!