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 :=
  | _if_1 : symb
  | cons : symb
  | iff : symb
  | intersect'ii'in : symb
  | intersect'ii'out : symb
  | nil : symb
  | p : symb
  | reduce'ii'in : symb
  | reduce'ii'out : symb
  | sequent : symb
  | tautology'i'in : symb
  | tautology'i'out : symb
  | u'1'1 : symb
  | u'10'1 : symb
  | u'11'1 : symb
  | u'12'1 : symb
  | u'12'2 : symb
  | u'13'1 : symb
  | u'14'1 : symb
  | u'15'1 : symb
  | u'16'1 : symb
  | u'2'1 : symb
  | u'3'1 : symb
  | u'4'1 : symb
  | u'5'1 : symb
  | u'6'1 : symb
  | u'6'2 : symb
  | u'7'1 : symb
  | u'8'1 : symb
  | u'9'1 : symb
  | x'2a : symb
  | x'2b : symb
  | x'2d : 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._if_1 => 2
  | M.cons => 2
  | M.iff => 2
  | M.intersect'ii'in => 2
  | M.intersect'ii'out => 0
  | M.nil => 0
  | M.p => 1
  | M.reduce'ii'in => 2
  | M.reduce'ii'out => 0
  | M.sequent => 2
  | M.tautology'i'in => 1
  | M.tautology'i'out => 0
  | M.u'1'1 => 1
  | M.u'10'1 => 1
  | M.u'11'1 => 1
  | M.u'12'1 => 5
  | M.u'12'2 => 1
  | M.u'13'1 => 1
  | M.u'14'1 => 1
  | M.u'15'1 => 1
  | M.u'16'1 => 1
  | M.u'2'1 => 1
  | M.u'3'1 => 1
  | M.u'4'1 => 1
  | M.u'5'1 => 1
  | M.u'6'1 => 5
  | M.u'6'2 => 1
  | M.u'7'1 => 1
  | M.u'8'1 => 1
  | M.u'9'1 => 1
  | M.x'2a => 2
  | M.x'2b => 2
  | M.x'2d => 1
  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 _if_1 x2 x1 := F0 M._if_1 (Vcons x2 (Vcons x1 Vnil)).
  Definition cons x2 x1 := F0 M.cons (Vcons x2 (Vcons x1 Vnil)).
  Definition iff x2 x1 := F0 M.iff (Vcons x2 (Vcons x1 Vnil)).
  Definition intersect'ii'in x2 x1 := F0 M.intersect'ii'in (Vcons x2 (Vcons x1 Vnil)).
  Definition intersect'ii'out := F0 M.intersect'ii'out Vnil.
  Definition nil := F0 M.nil Vnil.
  Definition p x1 := F0 M.p (Vcons x1 Vnil).
  Definition reduce'ii'in x2 x1 := F0 M.reduce'ii'in (Vcons x2 (Vcons x1 Vnil)).
  Definition reduce'ii'out := F0 M.reduce'ii'out Vnil.
  Definition sequent x2 x1 := F0 M.sequent (Vcons x2 (Vcons x1 Vnil)).
  Definition tautology'i'in x1 := F0 M.tautology'i'in (Vcons x1 Vnil).
  Definition tautology'i'out := F0 M.tautology'i'out Vnil.
  Definition u'1'1 x1 := F0 M.u'1'1 (Vcons x1 Vnil).
  Definition u'10'1 x1 := F0 M.u'10'1 (Vcons x1 Vnil).
  Definition u'11'1 x1 := F0 M.u'11'1 (Vcons x1 Vnil).
  Definition u'12'1 x5 x4 x3 x2 x1 := F0 M.u'12'1 (Vcons x5 (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil))))).
  Definition u'12'2 x1 := F0 M.u'12'2 (Vcons x1 Vnil).
  Definition u'13'1 x1 := F0 M.u'13'1 (Vcons x1 Vnil).
  Definition u'14'1 x1 := F0 M.u'14'1 (Vcons x1 Vnil).
  Definition u'15'1 x1 := F0 M.u'15'1 (Vcons x1 Vnil).
  Definition u'16'1 x1 := F0 M.u'16'1 (Vcons x1 Vnil).
  Definition u'2'1 x1 := F0 M.u'2'1 (Vcons x1 Vnil).
  Definition u'3'1 x1 := F0 M.u'3'1 (Vcons x1 Vnil).
  Definition u'4'1 x1 := F0 M.u'4'1 (Vcons x1 Vnil).
  Definition u'5'1 x1 := F0 M.u'5'1 (Vcons x1 Vnil).
  Definition u'6'1 x5 x4 x3 x2 x1 := F0 M.u'6'1 (Vcons x5 (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil))))).
  Definition u'6'2 x1 := F0 M.u'6'2 (Vcons x1 Vnil).
  Definition u'7'1 x1 := F0 M.u'7'1 (Vcons x1 Vnil).
  Definition u'8'1 x1 := F0 M.u'8'1 (Vcons x1 Vnil).
  Definition u'9'1 x1 := F0 M.u'9'1 (Vcons x1 Vnil).
  Definition x'2a x2 x1 := F0 M.x'2a (Vcons x2 (Vcons x1 Vnil)).
  Definition x'2b x2 x1 := F0 M.x'2b (Vcons x2 (Vcons x1 Vnil)).
  Definition x'2d x1 := F0 M.x'2d (Vcons x1 Vnil).
End S0.

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

Definition R :=
   R0 (S0.intersect'ii'in (S0.cons (V0 0) (V0 1)) (S0.cons (V0 0) (V0 3)))
      S0.intersect'ii'out
:: R0 (S0.intersect'ii'in (V0 0) (S0.cons (V0 1) (V0 2)))
      (S0.u'1'1 (S0.intersect'ii'in (V0 0) (V0 2)))
:: R0 (S0.u'1'1 S0.intersect'ii'out)
      S0.intersect'ii'out
:: R0 (S0.intersect'ii'in (S0.cons (V0 0) (V0 1)) (V0 2))
      (S0.u'2'1 (S0.intersect'ii'in (V0 1) (V0 2)))
:: R0 (S0.u'2'1 S0.intersect'ii'out)
      S0.intersect'ii'out
:: R0 (S0.reduce'ii'in (S0.sequent (S0.cons (S0._if_1 (V0 0) (V0 1)) (V0 2)) (V0 3)) (V0 4))
      (S0.u'3'1 (S0.reduce'ii'in (S0.sequent (S0.cons (S0.x'2b (S0.x'2d (V0 1)) (V0 0)) (V0 2)) (V0 3)) (V0 4)))
:: R0 (S0.u'3'1 S0.reduce'ii'out)
      S0.reduce'ii'out
:: R0 (S0.reduce'ii'in (S0.sequent (S0.cons (S0.iff (V0 0) (V0 1)) (V0 2)) (V0 3)) (V0 4))
      (S0.u'4'1 (S0.reduce'ii'in (S0.sequent (S0.cons (S0.x'2a (S0._if_1 (V0 0) (V0 1)) (S0._if_1 (V0 1) (V0 0))) (V0 2)) (V0 3)) (V0 4)))
:: R0 (S0.u'4'1 S0.reduce'ii'out)
      S0.reduce'ii'out
:: R0 (S0.reduce'ii'in (S0.sequent (S0.cons (S0.x'2a (V0 0) (V0 1)) (V0 2)) (V0 3)) (V0 4))
      (S0.u'5'1 (S0.reduce'ii'in (S0.sequent (S0.cons (V0 0) (S0.cons (V0 1) (V0 2))) (V0 3)) (V0 4)))
:: R0 (S0.u'5'1 S0.reduce'ii'out)
      S0.reduce'ii'out
:: R0 (S0.reduce'ii'in (S0.sequent (S0.cons (S0.x'2b (V0 0) (V0 1)) (V0 2)) (V0 3)) (V0 4))
      (S0.u'6'1 (S0.reduce'ii'in (S0.sequent (S0.cons (V0 0) (V0 2)) (V0 3)) (V0 4)) (V0 1) (V0 2) (V0 3) (V0 4))
:: R0 (S0.u'6'1 S0.reduce'ii'out (V0 0) (V0 1) (V0 2) (V0 3))
      (S0.u'6'2 (S0.reduce'ii'in (S0.sequent (S0.cons (V0 0) (V0 1)) (V0 2)) (V0 3)))
:: R0 (S0.u'6'2 S0.reduce'ii'out)
      S0.reduce'ii'out
:: R0 (S0.reduce'ii'in (S0.sequent (S0.cons (S0.x'2d (V0 0)) (V0 1)) (V0 2)) (V0 3))
      (S0.u'7'1 (S0.reduce'ii'in (S0.sequent (V0 1) (S0.cons (V0 0) (V0 2))) (V0 3)))
:: R0 (S0.u'7'1 S0.reduce'ii'out)
      S0.reduce'ii'out
:: R0 (S0.reduce'ii'in (S0.sequent (V0 0) (S0.cons (S0._if_1 (V0 1) (V0 2)) (V0 3))) (V0 4))
      (S0.u'8'1 (S0.reduce'ii'in (S0.sequent (V0 0) (S0.cons (S0.x'2b (S0.x'2d (V0 2)) (V0 1)) (V0 3))) (V0 4)))
:: R0 (S0.u'8'1 S0.reduce'ii'out)
      S0.reduce'ii'out
:: R0 (S0.reduce'ii'in (S0.sequent (V0 0) (S0.cons (S0.iff (V0 1) (V0 2)) (V0 3))) (V0 4))
      (S0.u'9'1 (S0.reduce'ii'in (S0.sequent (V0 0) (S0.cons (S0.x'2a (S0._if_1 (V0 1) (V0 2)) (S0._if_1 (V0 2) (V0 1))) (V0 3))) (V0 4)))
:: R0 (S0.u'9'1 S0.reduce'ii'out)
      S0.reduce'ii'out
:: R0 (S0.reduce'ii'in (S0.sequent (S0.cons (S0.p (V0 0)) (V0 1)) (V0 2)) (S0.sequent (V0 3) (V0 4)))
      (S0.u'10'1 (S0.reduce'ii'in (S0.sequent (V0 1) (V0 2)) (S0.sequent (S0.cons (S0.p (V0 0)) (V0 3)) (V0 4))))
:: R0 (S0.u'10'1 S0.reduce'ii'out)
      S0.reduce'ii'out
:: R0 (S0.reduce'ii'in (S0.sequent (V0 0) (S0.cons (S0.x'2b (V0 1) (V0 2)) (V0 3))) (V0 4))
      (S0.u'11'1 (S0.reduce'ii'in (S0.sequent (V0 0) (S0.cons (V0 1) (S0.cons (V0 2) (V0 3)))) (V0 4)))
:: R0 (S0.u'11'1 S0.reduce'ii'out)
      S0.reduce'ii'out
:: R0 (S0.reduce'ii'in (S0.sequent (V0 0) (S0.cons (S0.x'2a (V0 1) (V0 2)) (V0 3))) (V0 4))
      (S0.u'12'1 (S0.reduce'ii'in (S0.sequent (V0 0) (S0.cons (V0 1) (V0 3))) (V0 4)) (V0 0) (V0 2) (V0 3) (V0 4))
:: R0 (S0.u'12'1 S0.reduce'ii'out (V0 0) (V0 1) (V0 2) (V0 3))
      (S0.u'12'2 (S0.reduce'ii'in (S0.sequent (V0 0) (S0.cons (V0 1) (V0 2))) (V0 3)))
:: R0 (S0.u'12'2 S0.reduce'ii'out)
      S0.reduce'ii'out
:: R0 (S0.reduce'ii'in (S0.sequent (V0 0) (S0.cons (S0.x'2d (V0 1)) (V0 2))) (V0 3))
      (S0.u'13'1 (S0.reduce'ii'in (S0.sequent (S0.cons (V0 1) (V0 0)) (V0 2)) (V0 3)))
:: R0 (S0.u'13'1 S0.reduce'ii'out)
      S0.reduce'ii'out
:: R0 (S0.reduce'ii'in (S0.sequent S0.nil (S0.cons (S0.p (V0 0)) (V0 1))) (S0.sequent (V0 2) (V0 3)))
      (S0.u'14'1 (S0.reduce'ii'in (S0.sequent S0.nil (V0 1)) (S0.sequent (V0 2) (S0.cons (S0.p (V0 0)) (V0 3)))))
:: R0 (S0.u'14'1 S0.reduce'ii'out)
      S0.reduce'ii'out
:: R0 (S0.reduce'ii'in (S0.sequent S0.nil S0.nil) (S0.sequent (V0 0) (V0 1)))
      (S0.u'15'1 (S0.intersect'ii'in (V0 0) (V0 1)))
:: R0 (S0.u'15'1 S0.intersect'ii'out)
      S0.reduce'ii'out
:: R0 (S0.tautology'i'in (V0 0))
      (S0.u'16'1 (S0.reduce'ii'in (S0.sequent S0.nil (S0.cons (V0 0) S0.nil)) (S0.sequent S0.nil S0.nil)))
:: R0 (S0.u'16'1 S0.reduce'ii'out)
      S0.tautology'i'out
:: @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_if_1 x2 x1 := F1 (hd_symb s1_p M._if_1) (Vcons x2 (Vcons x1 Vnil)).
  Definition _if_1 x2 x1 := F1 (int_symb s1_p M._if_1) (Vcons x2 (Vcons x1 Vnil)).
  Definition hcons x2 x1 := F1 (hd_symb s1_p M.cons) (Vcons x2 (Vcons x1 Vnil)).
  Definition cons x2 x1 := F1 (int_symb s1_p M.cons) (Vcons x2 (Vcons x1 Vnil)).
  Definition hiff x2 x1 := F1 (hd_symb s1_p M.iff) (Vcons x2 (Vcons x1 Vnil)).
  Definition iff x2 x1 := F1 (int_symb s1_p M.iff) (Vcons x2 (Vcons x1 Vnil)).
  Definition hintersect'ii'in x2 x1 := F1 (hd_symb s1_p M.intersect'ii'in) (Vcons x2 (Vcons x1 Vnil)).
  Definition intersect'ii'in x2 x1 := F1 (int_symb s1_p M.intersect'ii'in) (Vcons x2 (Vcons x1 Vnil)).
  Definition hintersect'ii'out := F1 (hd_symb s1_p M.intersect'ii'out) Vnil.
  Definition intersect'ii'out := F1 (int_symb s1_p M.intersect'ii'out) Vnil.
  Definition hnil := F1 (hd_symb s1_p M.nil) Vnil.
  Definition nil := F1 (int_symb s1_p M.nil) 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 hreduce'ii'in x2 x1 := F1 (hd_symb s1_p M.reduce'ii'in) (Vcons x2 (Vcons x1 Vnil)).
  Definition reduce'ii'in x2 x1 := F1 (int_symb s1_p M.reduce'ii'in) (Vcons x2 (Vcons x1 Vnil)).
  Definition hreduce'ii'out := F1 (hd_symb s1_p M.reduce'ii'out) Vnil.
  Definition reduce'ii'out := F1 (int_symb s1_p M.reduce'ii'out) Vnil.
  Definition hsequent x2 x1 := F1 (hd_symb s1_p M.sequent) (Vcons x2 (Vcons x1 Vnil)).
  Definition sequent x2 x1 := F1 (int_symb s1_p M.sequent) (Vcons x2 (Vcons x1 Vnil)).
  Definition htautology'i'in x1 := F1 (hd_symb s1_p M.tautology'i'in) (Vcons x1 Vnil).
  Definition tautology'i'in x1 := F1 (int_symb s1_p M.tautology'i'in) (Vcons x1 Vnil).
  Definition htautology'i'out := F1 (hd_symb s1_p M.tautology'i'out) Vnil.
  Definition tautology'i'out := F1 (int_symb s1_p M.tautology'i'out) Vnil.
  Definition hu'1'1 x1 := F1 (hd_symb s1_p M.u'1'1) (Vcons x1 Vnil).
  Definition u'1'1 x1 := F1 (int_symb s1_p M.u'1'1) (Vcons x1 Vnil).
  Definition hu'10'1 x1 := F1 (hd_symb s1_p M.u'10'1) (Vcons x1 Vnil).
  Definition u'10'1 x1 := F1 (int_symb s1_p M.u'10'1) (Vcons x1 Vnil).
  Definition hu'11'1 x1 := F1 (hd_symb s1_p M.u'11'1) (Vcons x1 Vnil).
  Definition u'11'1 x1 := F1 (int_symb s1_p M.u'11'1) (Vcons x1 Vnil).
  Definition hu'12'1 x5 x4 x3 x2 x1 := F1 (hd_symb s1_p M.u'12'1) (Vcons x5 (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil))))).
  Definition u'12'1 x5 x4 x3 x2 x1 := F1 (int_symb s1_p M.u'12'1) (Vcons x5 (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil))))).
  Definition hu'12'2 x1 := F1 (hd_symb s1_p M.u'12'2) (Vcons x1 Vnil).
  Definition u'12'2 x1 := F1 (int_symb s1_p M.u'12'2) (Vcons x1 Vnil).
  Definition hu'13'1 x1 := F1 (hd_symb s1_p M.u'13'1) (Vcons x1 Vnil).
  Definition u'13'1 x1 := F1 (int_symb s1_p M.u'13'1) (Vcons x1 Vnil).
  Definition hu'14'1 x1 := F1 (hd_symb s1_p M.u'14'1) (Vcons x1 Vnil).
  Definition u'14'1 x1 := F1 (int_symb s1_p M.u'14'1) (Vcons x1 Vnil).
  Definition hu'15'1 x1 := F1 (hd_symb s1_p M.u'15'1) (Vcons x1 Vnil).
  Definition u'15'1 x1 := F1 (int_symb s1_p M.u'15'1) (Vcons x1 Vnil).
  Definition hu'16'1 x1 := F1 (hd_symb s1_p M.u'16'1) (Vcons x1 Vnil).
  Definition u'16'1 x1 := F1 (int_symb s1_p M.u'16'1) (Vcons x1 Vnil).
  Definition hu'2'1 x1 := F1 (hd_symb s1_p M.u'2'1) (Vcons x1 Vnil).
  Definition u'2'1 x1 := F1 (int_symb s1_p M.u'2'1) (Vcons x1 Vnil).
  Definition hu'3'1 x1 := F1 (hd_symb s1_p M.u'3'1) (Vcons x1 Vnil).
  Definition u'3'1 x1 := F1 (int_symb s1_p M.u'3'1) (Vcons x1 Vnil).
  Definition hu'4'1 x1 := F1 (hd_symb s1_p M.u'4'1) (Vcons x1 Vnil).
  Definition u'4'1 x1 := F1 (int_symb s1_p M.u'4'1) (Vcons x1 Vnil).
  Definition hu'5'1 x1 := F1 (hd_symb s1_p M.u'5'1) (Vcons x1 Vnil).
  Definition u'5'1 x1 := F1 (int_symb s1_p M.u'5'1) (Vcons x1 Vnil).
  Definition hu'6'1 x5 x4 x3 x2 x1 := F1 (hd_symb s1_p M.u'6'1) (Vcons x5 (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil))))).
  Definition u'6'1 x5 x4 x3 x2 x1 := F1 (int_symb s1_p M.u'6'1) (Vcons x5 (Vcons x4 (Vcons x3 (Vcons x2 (Vcons x1 Vnil))))).
  Definition hu'6'2 x1 := F1 (hd_symb s1_p M.u'6'2) (Vcons x1 Vnil).
  Definition u'6'2 x1 := F1 (int_symb s1_p M.u'6'2) (Vcons x1 Vnil).
  Definition hu'7'1 x1 := F1 (hd_symb s1_p M.u'7'1) (Vcons x1 Vnil).
  Definition u'7'1 x1 := F1 (int_symb s1_p M.u'7'1) (Vcons x1 Vnil).
  Definition hu'8'1 x1 := F1 (hd_symb s1_p M.u'8'1) (Vcons x1 Vnil).
  Definition u'8'1 x1 := F1 (int_symb s1_p M.u'8'1) (Vcons x1 Vnil).
  Definition hu'9'1 x1 := F1 (hd_symb s1_p M.u'9'1) (Vcons x1 Vnil).
  Definition u'9'1 x1 := F1 (int_symb s1_p M.u'9'1) (Vcons x1 Vnil).
  Definition hx'2a x2 x1 := F1 (hd_symb s1_p M.x'2a) (Vcons x2 (Vcons x1 Vnil)).
  Definition x'2a x2 x1 := F1 (int_symb s1_p M.x'2a) (Vcons x2 (Vcons x1 Vnil)).
  Definition hx'2b x2 x1 := F1 (hd_symb s1_p M.x'2b) (Vcons x2 (Vcons x1 Vnil)).
  Definition x'2b x2 x1 := F1 (int_symb s1_p M.x'2b) (Vcons x2 (Vcons x1 Vnil)).
  Definition hx'2d x1 := F1 (hd_symb s1_p M.x'2d) (Vcons x1 Vnil).
  Definition x'2d x1 := F1 (int_symb s1_p M.x'2d) (Vcons x1 Vnil).
End S1.

(* graph decomposition 1 *)

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

   (  R1 (S1.htautology'i'in (V1 0))
         (S1.hu'16'1 (S1.reduce'ii'in (S1.sequent (S1.nil) (S1.cons (V1 0) (S1.nil))) (S1.sequent (S1.nil) (S1.nil))))
   :: nil)

:: (  R1 (S1.hreduce'ii'in (S1.sequent (S1.nil) (S1.nil)) (S1.sequent (V1 0) (V1 1)))
         (S1.hu'15'1 (S1.intersect'ii'in (V1 0) (V1 1)))
   :: nil)

:: (  R1 (S1.hreduce'ii'in (S1.sequent (S1.nil) (S1.cons (S1.p (V1 0)) (V1 1))) (S1.sequent (V1 2) (V1 3)))
         (S1.hu'14'1 (S1.reduce'ii'in (S1.sequent (S1.nil) (V1 1)) (S1.sequent (V1 2) (S1.cons (S1.p (V1 0)) (V1 3)))))
   :: nil)

:: (  R1 (S1.hreduce'ii'in (S1.sequent (V1 0) (S1.cons (S1.x'2d (V1 1)) (V1 2))) (V1 3))
         (S1.hu'13'1 (S1.reduce'ii'in (S1.sequent (S1.cons (V1 1) (V1 0)) (V1 2)) (V1 3)))
   :: nil)

:: (  R1 (S1.hu'12'1 (S1.reduce'ii'out) (V1 0) (V1 1) (V1 2) (V1 3))
         (S1.hu'12'2 (S1.reduce'ii'in (S1.sequent (V1 0) (S1.cons (V1 1) (V1 2))) (V1 3)))
   :: nil)

:: (  R1 (S1.hreduce'ii'in (S1.sequent (V1 0) (S1.cons (S1.x'2b (V1 1) (V1 2)) (V1 3))) (V1 4))
         (S1.hu'11'1 (S1.reduce'ii'in (S1.sequent (V1 0) (S1.cons (V1 1) (S1.cons (V1 2) (V1 3)))) (V1 4)))
   :: nil)

:: (  R1 (S1.hreduce'ii'in (S1.sequent (S1.cons (S1.p (V1 0)) (V1 1)) (V1 2)) (S1.sequent (V1 3) (V1 4)))
         (S1.hu'10'1 (S1.reduce'ii'in (S1.sequent (V1 1) (V1 2)) (S1.sequent (S1.cons (S1.p (V1 0)) (V1 3)) (V1 4))))
   :: nil)

:: (  R1 (S1.hreduce'ii'in (S1.sequent (V1 0) (S1.cons (S1.iff (V1 1) (V1 2)) (V1 3))) (V1 4))
         (S1.hu'9'1 (S1.reduce'ii'in (S1.sequent (V1 0) (S1.cons (S1.x'2a (S1._if_1 (V1 1) (V1 2)) (S1._if_1 (V1 2) (V1 1))) (V1 3))) (V1 4)))
   :: nil)

:: (  R1 (S1.hreduce'ii'in (S1.sequent (V1 0) (S1.cons (S1._if_1 (V1 1) (V1 2)) (V1 3))) (V1 4))
         (S1.hu'8'1 (S1.reduce'ii'in (S1.sequent (V1 0) (S1.cons (S1.x'2b (S1.x'2d (V1 2)) (V1 1)) (V1 3))) (V1 4)))
   :: nil)

:: (  R1 (S1.hreduce'ii'in (S1.sequent (S1.cons (S1.x'2d (V1 0)) (V1 1)) (V1 2)) (V1 3))
         (S1.hu'7'1 (S1.reduce'ii'in (S1.sequent (V1 1) (S1.cons (V1 0) (V1 2))) (V1 3)))
   :: nil)

:: (  R1 (S1.hu'6'1 (S1.reduce'ii'out) (V1 0) (V1 1) (V1 2) (V1 3))
         (S1.hu'6'2 (S1.reduce'ii'in (S1.sequent (S1.cons (V1 0) (V1 1)) (V1 2)) (V1 3)))
   :: nil)

:: (  R1 (S1.hreduce'ii'in (S1.sequent (S1.cons (S1.x'2a (V1 0) (V1 1)) (V1 2)) (V1 3)) (V1 4))
         (S1.hu'5'1 (S1.reduce'ii'in (S1.sequent (S1.cons (V1 0) (S1.cons (V1 1) (V1 2))) (V1 3)) (V1 4)))
   :: nil)

:: (  R1 (S1.hreduce'ii'in (S1.sequent (S1.cons (S1.iff (V1 0) (V1 1)) (V1 2)) (V1 3)) (V1 4))
         (S1.hu'4'1 (S1.reduce'ii'in (S1.sequent (S1.cons (S1.x'2a (S1._if_1 (V1 0) (V1 1)) (S1._if_1 (V1 1) (V1 0))) (V1 2)) (V1 3)) (V1 4)))
   :: nil)

:: (  R1 (S1.hreduce'ii'in (S1.sequent (S1.cons (S1._if_1 (V1 0) (V1 1)) (V1 2)) (V1 3)) (V1 4))
         (S1.hu'3'1 (S1.reduce'ii'in (S1.sequent (S1.cons (S1.x'2b (S1.x'2d (V1 1)) (V1 0)) (V1 2)) (V1 3)) (V1 4)))
   :: nil)

:: (  R1 (S1.hintersect'ii'in (S1.cons (V1 0) (V1 1)) (V1 2))
         (S1.hu'2'1 (S1.intersect'ii'in (V1 1) (V1 2)))
   :: nil)

:: (  R1 (S1.hintersect'ii'in (V1 0) (S1.cons (V1 1) (V1 2)))
         (S1.hu'1'1 (S1.intersect'ii'in (V1 0) (V1 2)))
   :: nil)

:: (  R1 (S1.hintersect'ii'in (S1.cons (V1 0) (V1 1)) (V1 2))
         (S1.hintersect'ii'in (V1 1) (V1 2))
   :: R1 (S1.hintersect'ii'in (V1 0) (S1.cons (V1 1) (V1 2)))
         (S1.hintersect'ii'in (V1 0) (V1 2))
   :: nil)

:: (  R1 (S1.hreduce'ii'in (S1.sequent (S1.nil) (S1.nil)) (S1.sequent (V1 0) (V1 1)))
         (S1.hintersect'ii'in (V1 0) (V1 1))
   :: nil)

:: (  R1 (S1.hreduce'ii'in (S1.sequent (S1.cons (S1.x'2b (V1 0) (V1 1)) (V1 2)) (V1 3)) (V1 4))
         (S1.hu'6'1 (S1.reduce'ii'in (S1.sequent (S1.cons (V1 0) (V1 2)) (V1 3)) (V1 4)) (V1 1) (V1 2) (V1 3) (V1 4))
   :: R1 (S1.hu'6'1 (S1.reduce'ii'out) (V1 0) (V1 1) (V1 2) (V1 3))
         (S1.hreduce'ii'in (S1.sequent (S1.cons (V1 0) (V1 1)) (V1 2)) (V1 3))
   :: R1 (S1.hreduce'ii'in (S1.sequent (S1.cons (S1._if_1 (V1 0) (V1 1)) (V1 2)) (V1 3)) (V1 4))
         (S1.hreduce'ii'in (S1.sequent (S1.cons (S1.x'2b (S1.x'2d (V1 1)) (V1 0)) (V1 2)) (V1 3)) (V1 4))
   :: R1 (S1.hreduce'ii'in (S1.sequent (S1.cons (S1.x'2b (V1 0) (V1 1)) (V1 2)) (V1 3)) (V1 4))
         (S1.hreduce'ii'in (S1.sequent (S1.cons (V1 0) (V1 2)) (V1 3)) (V1 4))
   :: R1 (S1.hreduce'ii'in (S1.sequent (S1.cons (S1.iff (V1 0) (V1 1)) (V1 2)) (V1 3)) (V1 4))
         (S1.hreduce'ii'in (S1.sequent (S1.cons (S1.x'2a (S1._if_1 (V1 0) (V1 1)) (S1._if_1 (V1 1) (V1 0))) (V1 2)) (V1 3)) (V1 4))
   :: R1 (S1.hreduce'ii'in (S1.sequent (S1.cons (S1.x'2a (V1 0) (V1 1)) (V1 2)) (V1 3)) (V1 4))
         (S1.hreduce'ii'in (S1.sequent (S1.cons (V1 0) (S1.cons (V1 1) (V1 2))) (V1 3)) (V1 4))
   :: R1 (S1.hreduce'ii'in (S1.sequent (S1.cons (S1.x'2d (V1 0)) (V1 1)) (V1 2)) (V1 3))
         (S1.hreduce'ii'in (S1.sequent (V1 1) (S1.cons (V1 0) (V1 2))) (V1 3))
   :: R1 (S1.hreduce'ii'in (S1.sequent (V1 0) (S1.cons (S1._if_1 (V1 1) (V1 2)) (V1 3))) (V1 4))
         (S1.hreduce'ii'in (S1.sequent (V1 0) (S1.cons (S1.x'2b (S1.x'2d (V1 2)) (V1 1)) (V1 3))) (V1 4))
   :: R1 (S1.hreduce'ii'in (S1.sequent (S1.cons (S1.p (V1 0)) (V1 1)) (V1 2)) (S1.sequent (V1 3) (V1 4)))
         (S1.hreduce'ii'in (S1.sequent (V1 1) (V1 2)) (S1.sequent (S1.cons (S1.p (V1 0)) (V1 3)) (V1 4)))
   :: R1 (S1.hreduce'ii'in (S1.sequent (V1 0) (S1.cons (S1.iff (V1 1) (V1 2)) (V1 3))) (V1 4))
         (S1.hreduce'ii'in (S1.sequent (V1 0) (S1.cons (S1.x'2a (S1._if_1 (V1 1) (V1 2)) (S1._if_1 (V1 2) (V1 1))) (V1 3))) (V1 4))
   :: R1 (S1.hreduce'ii'in (S1.sequent (V1 0) (S1.cons (S1.x'2a (V1 1) (V1 2)) (V1 3))) (V1 4))
         (S1.hu'12'1 (S1.reduce'ii'in (S1.sequent (V1 0) (S1.cons (V1 1) (V1 3))) (V1 4)) (V1 0) (V1 2) (V1 3) (V1 4))
   :: R1 (S1.hu'12'1 (S1.reduce'ii'out) (V1 0) (V1 1) (V1 2) (V1 3))
         (S1.hreduce'ii'in (S1.sequent (V1 0) (S1.cons (V1 1) (V1 2))) (V1 3))
   :: R1 (S1.hreduce'ii'in (S1.sequent (V1 0) (S1.cons (S1.x'2b (V1 1) (V1 2)) (V1 3))) (V1 4))
         (S1.hreduce'ii'in (S1.sequent (V1 0) (S1.cons (V1 1) (S1.cons (V1 2) (V1 3)))) (V1 4))
   :: R1 (S1.hreduce'ii'in (S1.sequent (V1 0) (S1.cons (S1.x'2a (V1 1) (V1 2)) (V1 3))) (V1 4))
         (S1.hreduce'ii'in (S1.sequent (V1 0) (S1.cons (V1 1) (V1 3))) (V1 4))
   :: R1 (S1.hreduce'ii'in (S1.sequent (V1 0) (S1.cons (S1.x'2d (V1 1)) (V1 2))) (V1 3))
         (S1.hreduce'ii'in (S1.sequent (S1.cons (V1 1) (V1 0)) (V1 2)) (V1 3))
   :: R1 (S1.hreduce'ii'in (S1.sequent (S1.nil) (S1.cons (S1.p (V1 0)) (V1 1))) (S1.sequent (V1 2) (V1 3)))
         (S1.hreduce'ii'in (S1.sequent (S1.nil) (V1 1)) (S1.sequent (V1 2) (S1.cons (S1.p (V1 0)) (V1 3))))
   :: nil)

:: (  R1 (S1.htautology'i'in (V1 0))
         (S1.hreduce'ii'in (S1.sequent (S1.nil) (S1.cons (V1 0) (S1.nil))) (S1.sequent (S1.nil) (S1.nil)))
   :: 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.intersect'ii'in) =>
         (1%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: (1%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (int_symb M.intersect'ii'in) =>
         (1%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.cons) =>
         nil
    | (int_symb M.cons) =>
         (1%Z, (Vcons 0 (Vcons 0 Vnil)))
      :: (1%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: (2%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.intersect'ii'out) =>
         nil
    | (int_symb M.intersect'ii'out) =>
         nil
    | (hd_symb M.u'1'1) =>
         nil
    | (int_symb M.u'1'1) =>
         (1%Z, (Vcons 0 Vnil))
      :: nil
    | (hd_symb M.u'2'1) =>
         nil
    | (int_symb M.u'2'1) =>
         (1%Z, (Vcons 1 Vnil))
      :: nil
    | (hd_symb M.reduce'ii'in) =>
         nil
    | (int_symb M.reduce'ii'in) =>
         (1%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: nil
    | (hd_symb M.sequent) =>
         nil
    | (int_symb M.sequent) =>
         (1%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: (2%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M._if_1) =>
         nil
    | (int_symb M._if_1) =>
         nil
    | (hd_symb M.u'3'1) =>
         nil
    | (int_symb M.u'3'1) =>
         nil
    | (hd_symb M.x'2b) =>
         nil
    | (int_symb M.x'2b) =>
         nil
    | (hd_symb M.x'2d) =>
         nil
    | (int_symb M.x'2d) =>
         nil
    | (hd_symb M.reduce'ii'out) =>
         nil
    | (int_symb M.reduce'ii'out) =>
         nil
    | (hd_symb M.iff) =>
         nil
    | (int_symb M.iff) =>
         nil
    | (hd_symb M.u'4'1) =>
         nil
    | (int_symb M.u'4'1) =>
         (1%Z, (Vcons 0 Vnil))
      :: nil
    | (hd_symb M.x'2a) =>
         nil
    | (int_symb M.x'2a) =>
         (1%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.u'5'1) =>
         nil
    | (int_symb M.u'5'1) =>
         nil
    | (hd_symb M.u'6'1) =>
         nil
    | (int_symb M.u'6'1) =>
         (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))
      :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))))
      :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))))
      :: nil
    | (hd_symb M.u'6'2) =>
         nil
    | (int_symb M.u'6'2) =>
         (1%Z, (Vcons 0 Vnil))
      :: nil
    | (hd_symb M.u'7'1) =>
         nil
    | (int_symb M.u'7'1) =>
         (1%Z, (Vcons 0 Vnil))
      :: nil
    | (hd_symb M.u'8'1) =>
         nil
    | (int_symb M.u'8'1) =>
         (2%Z, (Vcons 0 Vnil))
      :: nil
    | (hd_symb M.u'9'1) =>
         nil
    | (int_symb M.u'9'1) =>
         nil
    | (hd_symb M.p) =>
         nil
    | (int_symb M.p) =>
         (3%Z, (Vcons 0 Vnil))
      :: (1%Z, (Vcons 1 Vnil))
      :: nil
    | (hd_symb M.u'10'1) =>
         nil
    | (int_symb M.u'10'1) =>
         nil
    | (hd_symb M.u'11'1) =>
         nil
    | (int_symb M.u'11'1) =>
         (2%Z, (Vcons 0 Vnil))
      :: nil
    | (hd_symb M.u'12'1) =>
         nil
    | (int_symb M.u'12'1) =>
         (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))))
      :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))))
      :: nil
    | (hd_symb M.u'12'2) =>
         nil
    | (int_symb M.u'12'2) =>
         nil
    | (hd_symb M.u'13'1) =>
         nil
    | (int_symb M.u'13'1) =>
         (1%Z, (Vcons 0 Vnil))
      :: nil
    | (hd_symb M.nil) =>
         nil
    | (int_symb M.nil) =>
         nil
    | (hd_symb M.u'14'1) =>
         nil
    | (int_symb M.u'14'1) =>
         (3%Z, (Vcons 0 Vnil))
      :: nil
    | (hd_symb M.u'15'1) =>
         nil
    | (int_symb M.u'15'1) =>
         nil
    | (hd_symb M.tautology'i'in) =>
         nil
    | (int_symb M.tautology'i'in) =>
         (2%Z, (Vcons 0 Vnil))
      :: nil
    | (hd_symb M.u'16'1) =>
         nil
    | (int_symb M.u'16'1) =>
         (1%Z, (Vcons 0 Vnil))
      :: nil
    | (hd_symb M.tautology'i'out) =>
         nil
    | (int_symb M.tautology'i'out) =>
         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.intersect'ii'in) =>
         nil
    | (int_symb M.intersect'ii'in) =>
         nil
    | (hd_symb M.cons) =>
         nil
    | (int_symb M.cons) =>
         (1%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: (1%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.intersect'ii'out) =>
         nil
    | (int_symb M.intersect'ii'out) =>
         nil
    | (hd_symb M.u'1'1) =>
         nil
    | (int_symb M.u'1'1) =>
         nil
    | (hd_symb M.u'2'1) =>
         nil
    | (int_symb M.u'2'1) =>
         nil
    | (hd_symb M.reduce'ii'in) =>
         (2%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: (1%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (int_symb M.reduce'ii'in) =>
         nil
    | (hd_symb M.sequent) =>
         nil
    | (int_symb M.sequent) =>
         (1%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: (1%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M._if_1) =>
         nil
    | (int_symb M._if_1) =>
         (1%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: (2%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.u'3'1) =>
         nil
    | (int_symb M.u'3'1) =>
         nil
    | (hd_symb M.x'2b) =>
         nil
    | (int_symb M.x'2b) =>
         (1%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: (1%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.x'2d) =>
         nil
    | (int_symb M.x'2d) =>
         (2%Z, (Vcons 1 Vnil))
      :: nil
    | (hd_symb M.reduce'ii'out) =>
         nil
    | (int_symb M.reduce'ii'out) =>
         nil
    | (hd_symb M.iff) =>
         nil
    | (int_symb M.iff) =>
         (3%Z, (Vcons 0 (Vcons 0 Vnil)))
      :: (3%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: (3%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.u'4'1) =>
         nil
    | (int_symb M.u'4'1) =>
         nil
    | (hd_symb M.x'2a) =>
         nil
    | (int_symb M.x'2a) =>
         (1%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: (1%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.u'5'1) =>
         nil
    | (int_symb M.u'5'1) =>
         nil
    | (hd_symb M.u'6'1) =>
         (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))
      :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))))
      :: (2%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.u'6'1) =>
         nil
    | (hd_symb M.u'6'2) =>
         nil
    | (int_symb M.u'6'2) =>
         nil
    | (hd_symb M.u'7'1) =>
         nil
    | (int_symb M.u'7'1) =>
         nil
    | (hd_symb M.u'8'1) =>
         nil
    | (int_symb M.u'8'1) =>
         nil
    | (hd_symb M.u'9'1) =>
         nil
    | (int_symb M.u'9'1) =>
         nil
    | (hd_symb M.p) =>
         nil
    | (int_symb M.p) =>
         (3%Z, (Vcons 0 Vnil))
      :: nil
    | (hd_symb M.u'10'1) =>
         nil
    | (int_symb M.u'10'1) =>
         nil
    | (hd_symb M.u'11'1) =>
         nil
    | (int_symb M.u'11'1) =>
         nil
    | (hd_symb M.u'12'1) =>
         (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))
      :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))))
      :: (2%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.u'12'1) =>
         nil
    | (hd_symb M.u'12'2) =>
         nil
    | (int_symb M.u'12'2) =>
         nil
    | (hd_symb M.u'13'1) =>
         nil
    | (int_symb M.u'13'1) =>
         nil
    | (hd_symb M.nil) =>
         nil
    | (int_symb M.nil) =>
         nil
    | (hd_symb M.u'14'1) =>
         nil
    | (int_symb M.u'14'1) =>
         nil
    | (hd_symb M.u'15'1) =>
         nil
    | (int_symb M.u'15'1) =>
         nil
    | (hd_symb M.tautology'i'in) =>
         nil
    | (int_symb M.tautology'i'in) =>
         (2%Z, (Vcons 0 Vnil))
      :: (1%Z, (Vcons 1 Vnil))
      :: nil
    | (hd_symb M.u'16'1) =>
         nil
    | (int_symb M.u'16'1) =>
         (1%Z, (Vcons 0 Vnil))
      :: nil
    | (hd_symb M.tautology'i'out) =>
         nil
    | (int_symb M.tautology'i'out) =>
         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.intersect'ii'in) =>
         nil
    | (int_symb M.intersect'ii'in) =>
         nil
    | (hd_symb M.cons) =>
         nil
    | (int_symb M.cons) =>
         (1%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: (1%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.intersect'ii'out) =>
         nil
    | (int_symb M.intersect'ii'out) =>
         nil
    | (hd_symb M.u'1'1) =>
         nil
    | (int_symb M.u'1'1) =>
         nil
    | (hd_symb M.u'2'1) =>
         nil
    | (int_symb M.u'2'1) =>
         nil
    | (hd_symb M.reduce'ii'in) =>
         (2%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: nil
    | (int_symb M.reduce'ii'in) =>
         nil
    | (hd_symb M.sequent) =>
         nil
    | (int_symb M.sequent) =>
         (1%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: (1%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M._if_1) =>
         nil
    | (int_symb M._if_1) =>
         (2%Z, (Vcons 0 (Vcons 0 Vnil)))
      :: (2%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: (2%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.u'3'1) =>
         nil
    | (int_symb M.u'3'1) =>
         nil
    | (hd_symb M.x'2b) =>
         nil
    | (int_symb M.x'2b) =>
         (1%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: (2%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.x'2d) =>
         nil
    | (int_symb M.x'2d) =>
         (1%Z, (Vcons 0 Vnil))
      :: (1%Z, (Vcons 1 Vnil))
      :: nil
    | (hd_symb M.reduce'ii'out) =>
         nil
    | (int_symb M.reduce'ii'out) =>
         nil
    | (hd_symb M.iff) =>
         nil
    | (int_symb M.iff) =>
         nil
    | (hd_symb M.u'4'1) =>
         nil
    | (int_symb M.u'4'1) =>
         nil
    | (hd_symb M.x'2a) =>
         nil
    | (int_symb M.x'2a) =>
         (3%Z, (Vcons 0 (Vcons 0 Vnil)))
      :: (1%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: (1%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.u'5'1) =>
         nil
    | (int_symb M.u'5'1) =>
         nil
    | (hd_symb M.u'6'1) =>
         (3%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))
      :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))))
      :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))))
      :: nil
    | (int_symb M.u'6'1) =>
         nil
    | (hd_symb M.u'6'2) =>
         nil
    | (int_symb M.u'6'2) =>
         nil
    | (hd_symb M.u'7'1) =>
         nil
    | (int_symb M.u'7'1) =>
         nil
    | (hd_symb M.u'8'1) =>
         nil
    | (int_symb M.u'8'1) =>
         nil
    | (hd_symb M.u'9'1) =>
         nil
    | (int_symb M.u'9'1) =>
         nil
    | (hd_symb M.p) =>
         nil
    | (int_symb M.p) =>
         nil
    | (hd_symb M.u'10'1) =>
         nil
    | (int_symb M.u'10'1) =>
         nil
    | (hd_symb M.u'11'1) =>
         nil
    | (int_symb M.u'11'1) =>
         nil
    | (hd_symb M.u'12'1) =>
         (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))
      :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 Vnil))))))
      :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 (Vcons 0 Vnil))))))
      :: nil
    | (int_symb M.u'12'1) =>
         nil
    | (hd_symb M.u'12'2) =>
         nil
    | (int_symb M.u'12'2) =>
         nil
    | (hd_symb M.u'13'1) =>
         nil
    | (int_symb M.u'13'1) =>
         nil
    | (hd_symb M.nil) =>
         nil
    | (int_symb M.nil) =>
         nil
    | (hd_symb M.u'14'1) =>
         nil
    | (int_symb M.u'14'1) =>
         nil
    | (hd_symb M.u'15'1) =>
         nil
    | (int_symb M.u'15'1) =>
         nil
    | (hd_symb M.tautology'i'in) =>
         nil
    | (int_symb M.tautology'i'in) =>
         (2%Z, (Vcons 1 Vnil))
      :: nil
    | (hd_symb M.u'16'1) =>
         nil
    | (int_symb M.u'16'1) =>
         nil
    | (hd_symb M.tautology'i'out) =>
         nil
    | (int_symb M.tautology'i'out) =>
         nil
    end.

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

End PIS3.

Module PI3 := PolyInt PIS3.

(* graph decomposition 2 *)

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

   (  R1 (S1.hu'6'1 (S1.reduce'ii'out) (V1 0) (V1 1) (V1 2) (V1 3))
         (S1.hreduce'ii'in (S1.sequent (S1.cons (V1 0) (V1 1)) (V1 2)) (V1 3))
   :: R1 (S1.hreduce'ii'in (S1.sequent (S1.cons (S1.x'2b (V1 0) (V1 1)) (V1 2)) (V1 3)) (V1 4))
         (S1.hu'6'1 (S1.reduce'ii'in (S1.sequent (S1.cons (V1 0) (V1 2)) (V1 3)) (V1 4)) (V1 1) (V1 2) (V1 3) (V1 4))
   :: R1 (S1.hreduce'ii'in (S1.sequent (S1.cons (S1.x'2b (V1 0) (V1 1)) (V1 2)) (V1 3)) (V1 4))
         (S1.hreduce'ii'in (S1.sequent (S1.cons (V1 0) (V1 2)) (V1 3)) (V1 4))
   :: R1 (S1.hreduce'ii'in (S1.sequent (V1 0) (S1.cons (S1.x'2b (V1 1) (V1 2)) (V1 3))) (V1 4))
         (S1.hreduce'ii'in (S1.sequent (V1 0) (S1.cons (V1 1) (S1.cons (V1 2) (V1 3)))) (V1 4))
   :: nil)

:: (  R1 (S1.hu'12'1 (S1.reduce'ii'out) (V1 0) (V1 1) (V1 2) (V1 3))
         (S1.hreduce'ii'in (S1.sequent (V1 0) (S1.cons (V1 1) (V1 2))) (V1 3))
   :: nil)

:: nil.

(* 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.intersect'ii'in) =>
         nil
    | (int_symb M.intersect'ii'in) =>
         nil
    | (hd_symb M.cons) =>
         nil
    | (int_symb M.cons) =>
         (1%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: nil
    | (hd_symb M.intersect'ii'out) =>
         nil
    | (int_symb M.intersect'ii'out) =>
         nil
    | (hd_symb M.u'1'1) =>
         nil
    | (int_symb M.u'1'1) =>
         nil
    | (hd_symb M.u'2'1) =>
         nil
    | (int_symb M.u'2'1) =>
         nil
    | (hd_symb M.reduce'ii'in) =>
         (2%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: (1%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (int_symb M.reduce'ii'in) =>
         nil
    | (hd_symb M.sequent) =>
         nil
    | (int_symb M.sequent) =>
         (1%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: nil
    | (hd_symb M._if_1) =>
         nil
    | (int_symb M._if_1) =>
         nil
    | (hd_symb M.u'3'1) =>
         nil
    | (int_symb M.u'3'1) =>
         nil
    | (hd_symb M.x'2b) =>
         nil
    | (int_symb M.x'2b) =>
         (2%Z, (Vcons 0 (Vcons 0 Vnil)))
      :: (1%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: (2%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.x'2d) =>
         nil
    | (int_symb M.x'2d) =>
         nil
    | (hd_symb M.reduce'ii'out) =>
         nil
    | (int_symb M.reduce'ii'out) =>
         nil
    | (hd_symb M.iff) =>
         nil
    | (int_symb M.iff) =>
         nil
    | (hd_symb M.u'4'1) =>
         nil
    | (int_symb M.u'4'1) =>
         nil
    | (hd_symb M.x'2a) =>
         nil
    | (int_symb M.x'2a) =>
         nil
    | (hd_symb M.u'5'1) =>
         nil
    | (int_symb M.u'5'1) =>
         nil
    | (hd_symb M.u'6'1) =>
         (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))
      :: (3%Z, (Vcons 0 (Vcons 1 (Vcons 0 (Vcons 0 (Vcons 0 Vnil))))))
      :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))))
      :: nil
    | (int_symb M.u'6'1) =>
         nil
    | (hd_symb M.u'6'2) =>
         nil
    | (int_symb M.u'6'2) =>
         nil
    | (hd_symb M.u'7'1) =>
         nil
    | (int_symb M.u'7'1) =>
         nil
    | (hd_symb M.u'8'1) =>
         nil
    | (int_symb M.u'8'1) =>
         nil
    | (hd_symb M.u'9'1) =>
         nil
    | (int_symb M.u'9'1) =>
         nil
    | (hd_symb M.p) =>
         nil
    | (int_symb M.p) =>
         nil
    | (hd_symb M.u'10'1) =>
         nil
    | (int_symb M.u'10'1) =>
         nil
    | (hd_symb M.u'11'1) =>
         nil
    | (int_symb M.u'11'1) =>
         nil
    | (hd_symb M.u'12'1) =>
         nil
    | (int_symb M.u'12'1) =>
         nil
    | (hd_symb M.u'12'2) =>
         nil
    | (int_symb M.u'12'2) =>
         nil
    | (hd_symb M.u'13'1) =>
         nil
    | (int_symb M.u'13'1) =>
         nil
    | (hd_symb M.nil) =>
         nil
    | (int_symb M.nil) =>
         nil
    | (hd_symb M.u'14'1) =>
         nil
    | (int_symb M.u'14'1) =>
         nil
    | (hd_symb M.u'15'1) =>
         nil
    | (int_symb M.u'15'1) =>
         nil
    | (hd_symb M.tautology'i'in) =>
         nil
    | (int_symb M.tautology'i'in) =>
         (3%Z, (Vcons 0 Vnil))
      :: (3%Z, (Vcons 1 Vnil))
      :: nil
    | (hd_symb M.u'16'1) =>
         nil
    | (int_symb M.u'16'1) =>
         nil
    | (hd_symb M.tautology'i'out) =>
         nil
    | (int_symb M.tautology'i'out) =>
         nil
    end.

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

End PIS4.

Module PI4 := PolyInt PIS4.

(* 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.intersect'ii'in) =>
         nil
    | (int_symb M.intersect'ii'in) =>
         (1%Z, (Vcons 0 (Vcons 0 Vnil)))
      :: nil
    | (hd_symb M.cons) =>
         nil
    | (int_symb M.cons) =>
         (2%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: nil
    | (hd_symb M.intersect'ii'out) =>
         nil
    | (int_symb M.intersect'ii'out) =>
         nil
    | (hd_symb M.u'1'1) =>
         nil
    | (int_symb M.u'1'1) =>
         (1%Z, (Vcons 1 Vnil))
      :: nil
    | (hd_symb M.u'2'1) =>
         nil
    | (int_symb M.u'2'1) =>
         nil
    | (hd_symb M.reduce'ii'in) =>
         (2%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: nil
    | (int_symb M.reduce'ii'in) =>
         (1%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M.sequent) =>
         nil
    | (int_symb M.sequent) =>
         (2%Z, (Vcons 0 (Vcons 1 Vnil)))
      :: nil
    | (hd_symb M._if_1) =>
         nil
    | (int_symb M._if_1) =>
         nil
    | (hd_symb M.u'3'1) =>
         nil
    | (int_symb M.u'3'1) =>
         nil
    | (hd_symb M.x'2b) =>
         nil
    | (int_symb M.x'2b) =>
         (2%Z, (Vcons 0 (Vcons 0 Vnil)))
      :: (2%Z, (Vcons 1 (Vcons 0 Vnil)))
      :: nil
    | (hd_symb M.x'2d) =>
         nil
    | (int_symb M.x'2d) =>
         nil
    | (hd_symb M.reduce'ii'out) =>
         nil
    | (int_symb M.reduce'ii'out) =>
         nil
    | (hd_symb M.iff) =>
         nil
    | (int_symb M.iff) =>
         nil
    | (hd_symb M.u'4'1) =>
         nil
    | (int_symb M.u'4'1) =>
         (1%Z, (Vcons 1 Vnil))
      :: nil
    | (hd_symb M.x'2a) =>
         nil
    | (int_symb M.x'2a) =>
         nil
    | (hd_symb M.u'5'1) =>
         nil
    | (int_symb M.u'5'1) =>
         nil
    | (hd_symb M.u'6'1) =>
         nil
    | (int_symb M.u'6'1) =>
         (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))))
      :: nil
    | (hd_symb M.u'6'2) =>
         nil
    | (int_symb M.u'6'2) =>
         nil
    | (hd_symb M.u'7'1) =>
         nil
    | (int_symb M.u'7'1) =>
         (1%Z, (Vcons 1 Vnil))
      :: nil
    | (hd_symb M.u'8'1) =>
         nil
    | (int_symb M.u'8'1) =>
         (1%Z, (Vcons 1 Vnil))
      :: nil
    | (hd_symb M.u'9'1) =>
         nil
    | (int_symb M.u'9'1) =>
         (1%Z, (Vcons 1 Vnil))
      :: nil
    | (hd_symb M.p) =>
         nil
    | (int_symb M.p) =>
         nil
    | (hd_symb M.u'10'1) =>
         nil
    | (int_symb M.u'10'1) =>
         (1%Z, (Vcons 1 Vnil))
      :: nil
    | (hd_symb M.u'11'1) =>
         nil
    | (int_symb M.u'11'1) =>
         (1%Z, (Vcons 1 Vnil))
      :: nil
    | (hd_symb M.u'12'1) =>
         nil
    | (int_symb M.u'12'1) =>
         (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 0 (Vcons 1 Vnil))))))
      :: nil
    | (hd_symb M.u'12'2) =>
         nil
    | (int_symb M.u'12'2) =>
         nil
    | (hd_symb M.u'13'1) =>
         nil
    | (int_symb M.u'13'1) =>
         nil
    | (hd_symb M.nil) =>
         nil
    | (int_symb M.nil) =>
         nil
    | (hd_symb M.u'14'1) =>
         nil
    | (int_symb M.u'14'1) =>
         nil
    | (hd_symb M.u'15'1) =>
         nil
    | (int_symb M.u'15'1) =>
         nil
    | (hd_symb M.tautology'i'in) =>
         nil
    | (int_symb M.tautology'i'in) =>
         (2%Z, (Vcons 0 Vnil))
      :: (3%Z, (Vcons 1 Vnil))
      :: nil
    | (hd_symb M.u'16'1) =>
         nil
    | (int_symb M.u'16'1) =>
         (1%Z, (Vcons 0 Vnil))
      :: nil
    | (hd_symb M.tautology'i'out) =>
         nil
    | (int_symb M.tautology'i'out) =>
         (1%Z, Vnil)
      :: 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.
left. co_scc.
left. co_scc.
left. co_scc.
left. co_scc.
left. co_scc.
left. co_scc.
left. co_scc.
left. co_scc.
left. co_scc.
left. co_scc.
left. co_scc.
left. co_scc.
left. co_scc.
left. co_scc.
left. co_scc.
right. PI1.prove_termination.
termination_trivial.
left. co_scc.
right. PI2.prove_termination.
PI3.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.
right. PI4.prove_termination.
PI5.prove_termination.
termination_trivial.
left. co_scc.
left. co_scc.
Qed.