Require Import ADPUnif.
Require Import ADecomp.
Require Import ADuplicateSymb.
Require Import AGraph.
Require Import APolyInt_MA.
Require Import ATrs.
Require Import List.
Require Import LogicUtil.
Require Import MonotonePolynom.
Require Import Polynom.
Require Import SN.
Require Import VecUtil.

Open Scope nat_scope.
(* termination problem *)

Module M.
  Inductive symb : Type :=
  | _0_1 : symb
  | edge : symb
  | empty : symb
  | eq : symb
  | false : symb
  | if_reach_1 : symb
  | if_reach_2 : symb
  | or : symb
  | reach : symb
  | s : symb
  | true : symb
  | union : symb.
End M.

Lemma eq_symb_dec : forall f g : M.symb, {f=g}+{~f=g}.

Proof.
decide equality.
Defined.

Open Scope nat_scope.
Definition ar (s : M.symb) : nat :=
  match s with
  | M._0_1 => 0
  | M.edge => 3
  | M.empty => 0
  | M.eq => 2
  | M.false => 0
  | M.if_reach_1 => 5
  | M.if_reach_2 => 5
  | M.or => 2
  | M.reach => 4
  | M.s => 1
  | M.true => 0
  | M.union => 2
  end.

Definition s0 := ASignature.mkSignature ar eq_symb_dec.
Definition s0_p := s0.
Definition V0 := @ATerm.Var s0.
Definition F0 := @ATerm.Fun s0.
Definition R0 := @ATrs.mkRule s0.

Module S0.
  Definition _0_1 := F0 M._0_1 Vnil.
  Definition edge x3 x2 x1 := F0 M.edge (Vcons x3 (Vcons x2 (Vcons x1 Vnil))).
  Definition empty := F0 M.empty Vnil.
  Definition eq x2 x1 := F0 M.eq (Vcons x2 (Vcons x1 Vnil)).
  Definition false := F0 M.false Vnil.
  Definition if_reach_1 x5 x4 x3 x2 x1 := F0 M.if_reach_1 (Vcons x5 (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil))))).
  Definition if_reach_2 x5 x4 x3 x2 x1 := F0 M.if_reach_2 (Vcons x5 (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil))))).
  Definition or x2 x1 := F0 M.or (Vcons x2 (Vcons x1 Vnil)).
  Definition reach x4 x3 x2 x1 := F0 M.reach (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))).
  Definition s x1 := F0 M.s (Vcons x1 Vnil).
  Definition true := F0 M.true Vnil.
  Definition union x2 x1 := F0 M.union (Vcons x2 (Vcons x1 Vnil)).
End S0.

Definition E :=
   @nil (@ATrs.rule s0).

Definition R :=
   R0 (S0.eq S0._0_1 S0._0_1)
      S0.true
:: R0 (S0.eq S0._0_1 (S0.s (V0 0)))
      S0.false
:: R0 (S0.eq (S0.s (V0 0)) S0._0_1)
      S0.false
:: R0 (S0.eq (S0.s (V0 0)) (S0.s (V0 1)))
      (S0.eq (V0 0) (V0 1))
:: R0 (S0.or S0.true (V0 0))
      S0.true
:: R0 (S0.or S0.false (V0 0))
      (V0 0)
:: R0 (S0.union S0.empty (V0 0))
      (V0 0)
:: R0 (S0.union (S0.edge (V0 0) (V0 1) (V0 2)) (V0 3))
      (S0.edge (V0 0) (V0 1) (S0.union (V0 2) (V0 3)))
:: R0 (S0.reach (V0 0) (V0 1) S0.empty (V0 2))
      S0.false
:: R0 (S0.reach (V0 0) (V0 1) (S0.edge (V0 2) (V0 3) (V0 4)) (V0 5))
      (S0.if_reach_1 (S0.eq (V0 0) (V0 2)) (V0 0) (V0 1) (S0.edge (V0 2) (V0 3) (V0 4)) (V0 5))
:: R0 (S0.if_reach_1 S0.true (V0 0) (V0 1) (S0.edge (V0 2) (V0 3) (V0 4)) (V0 5))
      (S0.if_reach_2 (S0.eq (V0 1) (V0 3)) (V0 0) (V0 1) (S0.edge (V0 2) (V0 3) (V0 4)) (V0 5))
:: R0 (S0.if_reach_2 S0.true (V0 0) (V0 1) (S0.edge (V0 2) (V0 3) (V0 4)) (V0 5))
      S0.true
:: R0 (S0.if_reach_2 S0.false (V0 0) (V0 1) (S0.edge (V0 2) (V0 3) (V0 4)) (V0 5))
      (S0.or (S0.reach (V0 0) (V0 1) (V0 4) (V0 5)) (S0.reach (V0 3) (V0 1) (S0.union (V0 4) (V0 5)) S0.empty))
:: R0 (S0.if_reach_1 S0.false (V0 0) (V0 1) (S0.edge (V0 2) (V0 3) (V0 4)) (V0 5))
      (S0.reach (V0 0) (V0 1) (V0 4) (S0.edge (V0 2) (V0 3) (V0 5)))
:: @nil (@ATrs.rule s0).

Definition rel := ATrs.red_mod E R.

(* symbol marking *)

Definition s1 := dup_sig s0.
Definition s1_p := s0.
Definition V1 := @ATerm.Var s1.
Definition F1 := @ATerm.Fun s1.
Definition R1 := @ATrs.mkRule s1.

Module S1.
  Definition h_0_1 := F1 (hd_symb s1_p M._0_1) Vnil.
  Definition _0_1 := F1 (int_symb s1_p M._0_1) Vnil.
  Definition hedge x3 x2 x1 := F1 (hd_symb s1_p M.edge) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))).
  Definition edge x3 x2 x1 := F1 (int_symb s1_p M.edge) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))).
  Definition hempty := F1 (hd_symb s1_p M.empty) Vnil.
  Definition empty := F1 (int_symb s1_p M.empty) Vnil.
  Definition heq x2 x1 := F1 (hd_symb s1_p M.eq) (Vcons x2 (Vcons x1 Vnil)).
  Definition eq x2 x1 := F1 (int_symb s1_p M.eq) (Vcons x2 (Vcons x1 Vnil)).
  Definition hfalse := F1 (hd_symb s1_p M.false) Vnil.
  Definition false := F1 (int_symb s1_p M.false) Vnil.
  Definition hif_reach_1 x5 x4 x3 x2 x1 := F1 (hd_symb s1_p M.if_reach_1) (Vcons x5 (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil))))).
  Definition if_reach_1 x5 x4 x3 x2 x1 := F1 (int_symb s1_p M.if_reach_1) (Vcons x5 (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil))))).
  Definition hif_reach_2 x5 x4 x3 x2 x1 := F1 (hd_symb s1_p M.if_reach_2) (Vcons x5 (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil))))).
  Definition if_reach_2 x5 x4 x3 x2 x1 := F1 (int_symb s1_p M.if_reach_2) (Vcons x5 (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil))))).
  Definition hor x2 x1 := F1 (hd_symb s1_p M.or) (Vcons x2 (Vcons x1 Vnil)).
  Definition or x2 x1 := F1 (int_symb s1_p M.or) (Vcons x2 (Vcons x1 Vnil)).
  Definition hreach x4 x3 x2 x1 := F1 (hd_symb s1_p M.reach) (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))).
  Definition reach x4 x3 x2 x1 := F1 (int_symb s1_p M.reach) (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))).
  Definition hs x1 := F1 (hd_symb s1_p M.s) (Vcons x1 Vnil).
  Definition s x1 := F1 (int_symb s1_p M.s) (Vcons x1 Vnil).
  Definition htrue := F1 (hd_symb s1_p M.true) Vnil.
  Definition true := F1 (int_symb s1_p M.true) Vnil.
  Definition hunion x2 x1 := F1 (hd_symb s1_p M.union) (Vcons x2 (Vcons x1 Vnil)).
  Definition union x2 x1 := F1 (int_symb s1_p M.union) (Vcons x2 (Vcons x1 Vnil)).
End S1.

(* graph decomposition 1 *)

Definition cs1 : list (list (@ATrs.rule s1)) :=

   (  R1 (S1.hif_reach_2 (S1.false) (V1 0) (V1 1) (S1.edge (V1 2) (V1 3) (V1 4)) (V1 5))
         (S1.hor (S1.reach (V1 0) (V1 1) (V1 4) (V1 5)) (S1.reach (V1 3) (V1 1) (S1.union (V1 4) (V1 5)) (S1.empty)))
   :: nil)

:: (  R1 (S1.hunion (S1.edge (V1 0) (V1 1) (V1 2)) (V1 3))
         (S1.hunion (V1 2) (V1 3))
   :: nil)

:: (  R1 (S1.hif_reach_2 (S1.false) (V1 0) (V1 1) (S1.edge (V1 2) (V1 3) (V1 4)) (V1 5))
         (S1.hunion (V1 4) (V1 5))
   :: nil)

:: (  R1 (S1.heq (S1.s (V1 0)) (S1.s (V1 1)))
         (S1.heq (V1 0) (V1 1))
   :: nil)

:: (  R1 (S1.hif_reach_1 (S1.true) (V1 0) (V1 1) (S1.edge (V1 2) (V1 3) (V1 4)) (V1 5))
         (S1.heq (V1 1) (V1 3))
   :: nil)

:: (  R1 (S1.hreach (V1 0) (V1 1) (S1.edge (V1 2) (V1 3) (V1 4)) (V1 5))
         (S1.heq (V1 0) (V1 2))
   :: nil)

:: (  R1 (S1.hreach (V1 0) (V1 1) (S1.edge (V1 2) (V1 3) (V1 4)) (V1 5))
         (S1.hif_reach_1 (S1.eq (V1 0) (V1 2)) (V1 0) (V1 1) (S1.edge (V1 2) (V1 3) (V1 4)) (V1 5))
   :: R1 (S1.hif_reach_1 (S1.true) (V1 0) (V1 1) (S1.edge (V1 2) (V1 3) (V1 4)) (V1 5))
         (S1.hif_reach_2 (S1.eq (V1 1) (V1 3)) (V1 0) (V1 1) (S1.edge (V1 2) (V1 3) (V1 4)) (V1 5))
   :: R1 (S1.hif_reach_2 (S1.false) (V1 0) (V1 1) (S1.edge (V1 2) (V1 3) (V1 4)) (V1 5))
         (S1.hreach (V1 0) (V1 1) (V1 4) (V1 5))
   :: R1 (S1.hif_reach_2 (S1.false) (V1 0) (V1 1) (S1.edge (V1 2) (V1 3) (V1 4)) (V1 5))
         (S1.hreach (V1 3) (V1 1) (S1.union (V1 4) (V1 5)) (S1.empty))
   :: R1 (S1.hif_reach_1 (S1.false) (V1 0) (V1 1) (S1.edge (V1 2) (V1 3) (V1 4)) (V1 5))
         (S1.hreach (V1 0) (V1 1) (V1 4) (S1.edge (V1 2) (V1 3) (V1 5)))
   :: nil)

:: nil.

(* polynomial interpretation 1 *)

Module PIS1 (*<: TPolyInt*).

  Definition sig := s1.

  Definition trsInt f :=
    match f as f return poly (@ASignature.arity s1 f) with
    | (hd_symb M.eq) =>
         nil
    | (int_symb M.eq) =>
         (3%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M._0_1) =>
         nil
    | (int_symb M._0_1) =>
         nil
    | (hd_symb M.true) =>
         nil
    | (int_symb M.true) =>
         nil
    | (hd_symb M.s) =>
         nil
    | (int_symb M.s) =>
         (1%Z, (Vcons 0 Vnil))
      :: (2%Z, (Vcons 1 Vnil))
      :: nil
    | (hd_symb M.false) =>
         nil
    | (int_symb M.false) =>
         nil
    | (hd_symb M.or) =>
         nil
    | (int_symb M.or) =>
         (2%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.union) =>
         (2%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: nil
    | (int_symb M.union) =>
         (3%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: (1%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.empty) =>
         nil
    | (int_symb M.empty) =>
         nil
    | (hd_symb M.edge) =>
         nil
    | (int_symb M.edge) =>
         (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))
      :: (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))
      :: (3%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))
      :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))
      :: nil
    | (hd_symb M.reach) =>
         nil
    | (int_symb M.reach) =>
         nil
    | (hd_symb M.if_reach_1) =>
         nil
    | (int_symb M.if_reach_1) =>
         nil
    | (hd_symb M.if_reach_2) =>
         nil
    | (int_symb M.if_reach_2) =>
         nil
    end.

  Lemma trsInt_wm : forall f, pweak_monotone (trsInt f).
  Proof.
    pmonotone.
  Qed.

End PIS1.

Module PI1 := PolyInt PIS1.

(* polynomial interpretation 2 *)

Module PIS2 (*<: TPolyInt*).

  Definition sig := s1.

  Definition trsInt f :=
    match f as f return poly (@ASignature.arity s1 f) with
    | (hd_symb M.eq) =>
         (1%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: nil
    | (int_symb M.eq) =>
         nil
    | (hd_symb M._0_1) =>
         nil
    | (int_symb M._0_1) =>
         nil
    | (hd_symb M.true) =>
         nil
    | (int_symb M.true) =>
         nil
    | (hd_symb M.s) =>
         nil
    | (int_symb M.s) =>
         (1%Z, (Vcons 0 Vnil))
      :: (2%Z, (Vcons 1 Vnil))
      :: nil
    | (hd_symb M.false) =>
         nil
    | (int_symb M.false) =>
         nil
    | (hd_symb M.or) =>
         nil
    | (int_symb M.or) =>
         (2%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.union) =>
         nil
    | (int_symb M.union) =>
         (2%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: (2%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.empty) =>
         nil
    | (int_symb M.empty) =>
         nil
    | (hd_symb M.edge) =>
         nil
    | (int_symb M.edge) =>
         (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))
      :: nil
    | (hd_symb M.reach) =>
         nil
    | (int_symb M.reach) =>
         nil
    | (hd_symb M.if_reach_1) =>
         nil
    | (int_symb M.if_reach_1) =>
         nil
    | (hd_symb M.if_reach_2) =>
         nil
    | (int_symb M.if_reach_2) =>
         nil
    end.

  Lemma trsInt_wm : forall f, pweak_monotone (trsInt f).
  Proof.
    pmonotone.
  Qed.

End PIS2.

Module PI2 := PolyInt PIS2.

(* polynomial interpretation 3 *)

Module PIS3 (*<: TPolyInt*).

  Definition sig := s1.

  Definition trsInt f :=
    match f as f return poly (@ASignature.arity s1 f) with
    | (hd_symb M.eq) =>
         nil
    | (int_symb M.eq) =>
         nil
    | (hd_symb M._0_1) =>
         nil
    | (int_symb M._0_1) =>
         nil
    | (hd_symb M.true) =>
         nil
    | (int_symb M.true) =>
         nil
    | (hd_symb M.s) =>
         nil
    | (int_symb M.s) =>
         nil
    | (hd_symb M.false) =>
         nil
    | (int_symb M.false) =>
         nil
    | (hd_symb M.or) =>
         nil
    | (int_symb M.or) =>
         (2%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.union) =>
         nil
    | (int_symb M.union) =>
         (1%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: (1%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.empty) =>
         nil
    | (int_symb M.empty) =>
         (1%Z, Vnil)
      :: nil
    | (hd_symb M.edge) =>
         nil
    | (int_symb M.edge) =>
         (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))
      :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))
      :: nil
    | (hd_symb M.reach) =>
         (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))))
      :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))))
      :: nil
    | (int_symb M.reach) =>
         nil
    | (hd_symb M.if_reach_1) =>
         (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))))
      :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))))
      :: nil
    | (int_symb M.if_reach_1) =>
         nil
    | (hd_symb M.if_reach_2) =>
         (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))))
      :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))))
      :: nil
    | (int_symb M.if_reach_2) =>
         nil
    end.

  Lemma trsInt_wm : forall f, pweak_monotone (trsInt f).
  Proof.
    pmonotone.
  Qed.

End PIS3.

Module PI3 := PolyInt PIS3.

(* polynomial interpretation 4 *)

Module PIS4 (*<: TPolyInt*).

  Definition sig := s1.

  Definition trsInt f :=
    match f as f return poly (@ASignature.arity s1 f) with
    | (hd_symb M.eq) =>
         nil
    | (int_symb M.eq) =>
         nil
    | (hd_symb M._0_1) =>
         nil
    | (int_symb M._0_1) =>
         nil
    | (hd_symb M.true) =>
         nil
    | (int_symb M.true) =>
         nil
    | (hd_symb M.s) =>
         nil
    | (int_symb M.s) =>
         nil
    | (hd_symb M.false) =>
         nil
    | (int_symb M.false) =>
         nil
    | (hd_symb M.or) =>
         nil
    | (int_symb M.or) =>
         (2%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.union) =>
         nil
    | (int_symb M.union) =>
         (1%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: (1%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.empty) =>
         nil
    | (int_symb M.empty) =>
         nil
    | (hd_symb M.edge) =>
         nil
    | (int_symb M.edge) =>
         (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))
      :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))
      :: nil
    | (hd_symb M.reach) =>
         (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))))
      :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))))
      :: nil
    | (int_symb M.reach) =>
         nil
    | (hd_symb M.if_reach_1) =>
         (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))))
      :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))))
      :: nil
    | (int_symb M.if_reach_1) =>
         nil
    | (hd_symb M.if_reach_2) =>
         (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))))
      :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))))
      :: nil
    | (int_symb M.if_reach_2) =>
         nil
    end.

  Lemma trsInt_wm : forall f, pweak_monotone (trsInt f).
  Proof.
    pmonotone.
  Qed.

End PIS4.

Module PI4 := PolyInt PIS4.

(* graph decomposition 2 *)

Definition cs2 : list (list (@ATrs.rule s1)) :=

   (  R1 (S1.hif_reach_1 (S1.true) (V1 0) (V1 1) (S1.edge (V1 2) (V1 3) (V1 4)) (V1 5))
         (S1.hif_reach_2 (S1.eq (V1 1) (V1 3)) (V1 0) (V1 1) (S1.edge (V1 2) (V1 3) (V1 4)) (V1 5))
   :: nil)

:: (  R1 (S1.hif_reach_1 (S1.false) (V1 0) (V1 1) (S1.edge (V1 2) (V1 3) (V1 4)) (V1 5))
         (S1.hreach (V1 0) (V1 1) (V1 4) (S1.edge (V1 2) (V1 3) (V1 5)))
   :: R1 (S1.hreach (V1 0) (V1 1) (S1.edge (V1 2) (V1 3) (V1 4)) (V1 5))
         (S1.hif_reach_1 (S1.eq (V1 0) (V1 2)) (V1 0) (V1 1) (S1.edge (V1 2) (V1 3) (V1 4)) (V1 5))
   :: nil)

:: nil.

(* polynomial interpretation 5 *)

Module PIS5 (*<: TPolyInt*).

  Definition sig := s1.

  Definition trsInt f :=
    match f as f return poly (@ASignature.arity s1 f) with
    | (hd_symb M.eq) =>
         nil
    | (int_symb M.eq) =>
         (1%Z, (Vcons 0 (Vcons 0 Vnil)))
      :: nil
    | (hd_symb M._0_1) =>
         nil
    | (int_symb M._0_1) =>
         nil
    | (hd_symb M.true) =>
         nil
    | (int_symb M.true) =>
         nil
    | (hd_symb M.s) =>
         nil
    | (int_symb M.s) =>
         nil
    | (hd_symb M.false) =>
         nil
    | (int_symb M.false) =>
         nil
    | (hd_symb M.or) =>
         nil
    | (int_symb M.or) =>
         (2%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.union) =>
         nil
    | (int_symb M.union) =>
         (1%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: (2%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.empty) =>
         nil
    | (int_symb M.empty) =>
         nil
    | (hd_symb M.edge) =>
         nil
    | (int_symb M.edge) =>
         (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))
      :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))
      :: nil
    | (hd_symb M.reach) =>
         (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))))
      :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))))
      :: nil
    | (int_symb M.reach) =>
         nil
    | (hd_symb M.if_reach_1) =>
         (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))))
      :: nil
    | (int_symb M.if_reach_1) =>
         nil
    | (hd_symb M.if_reach_2) =>
         nil
    | (int_symb M.if_reach_2) =>
         nil
    end.

  Lemma trsInt_wm : forall f, pweak_monotone (trsInt f).
  Proof.
    pmonotone.
  Qed.

End PIS5.

Module PI5 := PolyInt PIS5.

(* termination proof *)

Lemma termination : WF rel.

Proof.
unfold rel.
dp_trans.
mark.
let D := fresh "D" in let R := fresh "R" in set_rules_to D; set_mod_rules_to R;
graph_decomp (dpg_unif_N 100 R D) cs1; subst D; subst R.
dpg_unif_N_correct.
left. co_scc.
right. PI1.prove_termination.
termination_trivial.
left. co_scc.
right. PI2.prove_termination.
termination_trivial.
left. co_scc.
left. co_scc.
right. PI3.prove_termination.
PI4.prove_termination.
let D := fresh "D" in let R := fresh "R" in set_rules_to D; set_mod_rules_to R;
graph_decomp (dpg_unif_N 100 R D) cs2; subst D; subst R.
dpg_unif_N_correct.
left. co_scc.
right. PI5.prove_termination.
termination_trivial.
Qed.