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

Open Scope nat_scope.
(* termination problem *)

Module M.
  Inductive symb : Type :=
  | _0_1 : symb
  | _lt__eq__2 : symb
  | f : symb
  | false : symb
  | g : symb
  | p : symb
  | s : symb
  | true : 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._lt__eq__2 => 2
  | M.f => 3
  | M.false => 0
  | M.g => 4
  | M.p => 1
  | M.s => 1
  | M.true => 0
  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 _lt__eq__2 x2 x1 := F0 M._lt__eq__2 (Vcons x2 (Vcons x1 Vnil)).
  Definition f x3 x2 x1 := F0 M.f (Vcons x3 (Vcons x2 (Vcons x1 Vnil))).
  Definition false := F0 M.false Vnil.
  Definition g x4 x3 x2 x1 := F0 M.g (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))).
  Definition p x1 := F0 M.p (Vcons x1 Vnil).
  Definition s x1 := F0 M.s (Vcons x1 Vnil).
  Definition true := F0 M.true Vnil.
End S0.

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

Definition R :=
   R0 (S0.f (V0 0) (V0 1) (V0 2))
      (S0.g (S0._lt__eq__2 (V0 0) (V0 1)) (V0 0) (V0 1) (V0 2))
:: R0 (S0.g S0.true (V0 0) (V0 1) (V0 2))
      (V0 2)
:: R0 (S0.g S0.false (V0 0) (V0 1) (V0 2))
      (S0.f (S0.f (S0.p (V0 0)) (V0 1) (V0 2)) (S0.f (S0.p (V0 1)) (V0 2) (V0 0)) (S0.f (S0.p (V0 2)) (V0 0) (V0 1)))
:: R0 (S0.p S0._0_1)
      S0._0_1
:: R0 (S0.p (S0.s (V0 0)))
      (V0 0)
:: @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 h_lt__eq__2 x2 x1 := F1 (hd_symb s1_p M._lt__eq__2) (Vcons x2 (Vcons x1 Vnil)).
  Definition _lt__eq__2 x2 x1 := F1 (int_symb s1_p M._lt__eq__2) (Vcons x2 (Vcons x1 Vnil)).
  Definition hf x3 x2 x1 := F1 (hd_symb s1_p M.f) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))).
  Definition f x3 x2 x1 := F1 (int_symb s1_p M.f) (Vcons x3 (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 hg x4 x3 x2 x1 := F1 (hd_symb s1_p M.g) (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))).
  Definition g x4 x3 x2 x1 := F1 (int_symb s1_p M.g) (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil)))).
  Definition hp x1 := F1 (hd_symb s1_p M.p) (Vcons x1 Vnil).
  Definition p x1 := F1 (int_symb s1_p M.p) (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.
End S1.

(* graph decomposition 1 *)

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

   (  R1 (S1.hg (S1.false) (V1 0) (V1 1) (V1 2))
         (S1.hp (V1 2))
   :: nil)

:: (  R1 (S1.hg (S1.false) (V1 0) (V1 1) (V1 2))
         (S1.hp (V1 1))
   :: nil)

:: (  R1 (S1.hg (S1.false) (V1 0) (V1 1) (V1 2))
         (S1.hp (V1 0))
   :: nil)

:: (  R1 (S1.hf (V1 0) (V1 1) (V1 2))
         (S1.hg (S1._lt__eq__2 (V1 0) (V1 1)) (V1 0) (V1 1) (V1 2))
   :: nil)

:: (  R1 (S1.hg (S1.false) (V1 0) (V1 1) (V1 2))
         (S1.hf (S1.p (V1 2)) (V1 0) (V1 1))
   :: nil)

:: (  R1 (S1.hg (S1.false) (V1 0) (V1 1) (V1 2))
         (S1.hf (S1.p (V1 1)) (V1 2) (V1 0))
   :: nil)

:: (  R1 (S1.hg (S1.false) (V1 0) (V1 1) (V1 2))
         (S1.hf (S1.p (V1 0)) (V1 1) (V1 2))
   :: nil)

:: (  R1 (S1.hg (S1.false) (V1 0) (V1 1) (V1 2))
         (S1.hf (S1.f (S1.p (V1 0)) (V1 1) (V1 2)) (S1.f (S1.p (V1 1)) (V1 2) (V1 0)) (S1.f (S1.p (V1 2)) (V1 0) (V1 1)))
   :: nil)

:: nil.

(* 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.
left. co_scc.
left. co_scc.
left. co_scc.
left. co_scc.
left. co_scc.
left. co_scc.
left. co_scc.
Qed.