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 | active : symb | add : symb | cons : symb | from : symb | fst : symb | len : symb | mark : symb | nil : symb | ok : symb | proper : symb | s : symb | top : 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.active => 1 | M.add => 2 | M.cons => 2 | M.from => 1 | M.fst => 2 | M.len => 1 | M.mark => 1 | M.nil => 0 | M.ok => 1 | M.proper => 1 | M.s => 1 | M.top => 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 _0_1 := F0 M._0_1 Vnil. Definition active x1 := F0 M.active (Vcons x1 Vnil). Definition add x2 x1 := F0 M.add (Vcons x2 (Vcons x1 Vnil)). Definition cons x2 x1 := F0 M.cons (Vcons x2 (Vcons x1 Vnil)). Definition from x1 := F0 M.from (Vcons x1 Vnil). Definition fst x2 x1 := F0 M.fst (Vcons x2 (Vcons x1 Vnil)). Definition len x1 := F0 M.len (Vcons x1 Vnil). Definition mark x1 := F0 M.mark (Vcons x1 Vnil). Definition nil := F0 M.nil Vnil. Definition ok x1 := F0 M.ok (Vcons x1 Vnil). Definition proper x1 := F0 M.proper (Vcons x1 Vnil). Definition s x1 := F0 M.s (Vcons x1 Vnil). Definition top x1 := F0 M.top (Vcons x1 Vnil). End S0. Definition E := @nil (@ATrs.rule s0). Definition R := R0 (S0.active (S0.fst S0._0_1 (V0 0))) (S0.mark S0.nil) :: R0 (S0.active (S0.fst (S0.s (V0 0)) (S0.cons (V0 1) (V0 2)))) (S0.mark (S0.cons (V0 1) (S0.fst (V0 0) (V0 2)))) :: R0 (S0.active (S0.from (V0 0))) (S0.mark (S0.cons (V0 0) (S0.from (S0.s (V0 0))))) :: R0 (S0.active (S0.add S0._0_1 (V0 0))) (S0.mark (V0 0)) :: R0 (S0.active (S0.add (S0.s (V0 0)) (V0 1))) (S0.mark (S0.s (S0.add (V0 0) (V0 1)))) :: R0 (S0.active (S0.len S0.nil)) (S0.mark S0._0_1) :: R0 (S0.active (S0.len (S0.cons (V0 0) (V0 1)))) (S0.mark (S0.s (S0.len (V0 1)))) :: R0 (S0.active (S0.cons (V0 0) (V0 1))) (S0.cons (S0.active (V0 0)) (V0 1)) :: R0 (S0.active (S0.fst (V0 0) (V0 1))) (S0.fst (S0.active (V0 0)) (V0 1)) :: R0 (S0.active (S0.fst (V0 0) (V0 1))) (S0.fst (V0 0) (S0.active (V0 1))) :: R0 (S0.active (S0.from (V0 0))) (S0.from (S0.active (V0 0))) :: R0 (S0.active (S0.add (V0 0) (V0 1))) (S0.add (S0.active (V0 0)) (V0 1)) :: R0 (S0.active (S0.add (V0 0) (V0 1))) (S0.add (V0 0) (S0.active (V0 1))) :: R0 (S0.active (S0.len (V0 0))) (S0.len (S0.active (V0 0))) :: R0 (S0.cons (S0.mark (V0 0)) (V0 1)) (S0.mark (S0.cons (V0 0) (V0 1))) :: R0 (S0.fst (S0.mark (V0 0)) (V0 1)) (S0.mark (S0.fst (V0 0) (V0 1))) :: R0 (S0.fst (V0 0) (S0.mark (V0 1))) (S0.mark (S0.fst (V0 0) (V0 1))) :: R0 (S0.from (S0.mark (V0 0))) (S0.mark (S0.from (V0 0))) :: R0 (S0.add (S0.mark (V0 0)) (V0 1)) (S0.mark (S0.add (V0 0) (V0 1))) :: R0 (S0.add (V0 0) (S0.mark (V0 1))) (S0.mark (S0.add (V0 0) (V0 1))) :: R0 (S0.len (S0.mark (V0 0))) (S0.mark (S0.len (V0 0))) :: R0 (S0.proper S0._0_1) (S0.ok S0._0_1) :: R0 (S0.proper (S0.s (V0 0))) (S0.s (S0.proper (V0 0))) :: R0 (S0.proper S0.nil) (S0.ok S0.nil) :: R0 (S0.proper (S0.cons (V0 0) (V0 1))) (S0.cons (S0.proper (V0 0)) (S0.proper (V0 1))) :: R0 (S0.proper (S0.fst (V0 0) (V0 1))) (S0.fst (S0.proper (V0 0)) (S0.proper (V0 1))) :: R0 (S0.proper (S0.from (V0 0))) (S0.from (S0.proper (V0 0))) :: R0 (S0.proper (S0.add (V0 0) (V0 1))) (S0.add (S0.proper (V0 0)) (S0.proper (V0 1))) :: R0 (S0.proper (S0.len (V0 0))) (S0.len (S0.proper (V0 0))) :: R0 (S0.s (S0.ok (V0 0))) (S0.ok (S0.s (V0 0))) :: R0 (S0.cons (S0.ok (V0 0)) (S0.ok (V0 1))) (S0.ok (S0.cons (V0 0) (V0 1))) :: R0 (S0.fst (S0.ok (V0 0)) (S0.ok (V0 1))) (S0.ok (S0.fst (V0 0) (V0 1))) :: R0 (S0.from (S0.ok (V0 0))) (S0.ok (S0.from (V0 0))) :: R0 (S0.add (S0.ok (V0 0)) (S0.ok (V0 1))) (S0.ok (S0.add (V0 0) (V0 1))) :: R0 (S0.len (S0.ok (V0 0))) (S0.ok (S0.len (V0 0))) :: R0 (S0.top (S0.mark (V0 0))) (S0.top (S0.proper (V0 0))) :: R0 (S0.top (S0.ok (V0 0))) (S0.top (S0.active (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 hactive x1 := F1 (hd_symb s1_p M.active) (Vcons x1 Vnil). Definition active x1 := F1 (int_symb s1_p M.active) (Vcons x1 Vnil). Definition hadd x2 x1 := F1 (hd_symb s1_p M.add) (Vcons x2 (Vcons x1 Vnil)). Definition add x2 x1 := F1 (int_symb s1_p M.add) (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 hfrom x1 := F1 (hd_symb s1_p M.from) (Vcons x1 Vnil). Definition from x1 := F1 (int_symb s1_p M.from) (Vcons x1 Vnil). Definition hfst x2 x1 := F1 (hd_symb s1_p M.fst) (Vcons x2 (Vcons x1 Vnil)). Definition fst x2 x1 := F1 (int_symb s1_p M.fst) (Vcons x2 (Vcons x1 Vnil)). Definition hlen x1 := F1 (hd_symb s1_p M.len) (Vcons x1 Vnil). Definition len x1 := F1 (int_symb s1_p M.len) (Vcons x1 Vnil). Definition hmark x1 := F1 (hd_symb s1_p M.mark) (Vcons x1 Vnil). Definition mark x1 := F1 (int_symb s1_p M.mark) (Vcons x1 Vnil). Definition hnil := F1 (hd_symb s1_p M.nil) Vnil. Definition nil := F1 (int_symb s1_p M.nil) Vnil. Definition hok x1 := F1 (hd_symb s1_p M.ok) (Vcons x1 Vnil). Definition ok x1 := F1 (int_symb s1_p M.ok) (Vcons x1 Vnil). Definition hproper x1 := F1 (hd_symb s1_p M.proper) (Vcons x1 Vnil). Definition proper x1 := F1 (int_symb s1_p M.proper) (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 htop x1 := F1 (hd_symb s1_p M.top) (Vcons x1 Vnil). Definition top x1 := F1 (int_symb s1_p M.top) (Vcons x1 Vnil). End S1. (* graph decomposition 1 *) Definition cs1 : list (list (@ATrs.rule s1)) := ( R1 (S1.hs (S1.ok (V1 0))) (S1.hs (V1 0)) :: nil) :: ( R1 (S1.hproper (S1.s (V1 0))) (S1.hs (S1.proper (V1 0))) :: nil) :: ( R1 (S1.hlen (S1.ok (V1 0))) (S1.hlen (V1 0)) :: R1 (S1.hlen (S1.mark (V1 0))) (S1.hlen (V1 0)) :: nil) :: ( R1 (S1.hproper (S1.len (V1 0))) (S1.hlen (S1.proper (V1 0))) :: nil) :: ( R1 (S1.hadd (V1 0) (S1.mark (V1 1))) (S1.hadd (V1 0) (V1 1)) :: R1 (S1.hadd (S1.mark (V1 0)) (V1 1)) (S1.hadd (V1 0) (V1 1)) :: R1 (S1.hadd (S1.ok (V1 0)) (S1.ok (V1 1))) (S1.hadd (V1 0) (V1 1)) :: nil) :: ( R1 (S1.hproper (S1.add (V1 0) (V1 1))) (S1.hadd (S1.proper (V1 0)) (S1.proper (V1 1))) :: nil) :: ( R1 (S1.hfrom (S1.ok (V1 0))) (S1.hfrom (V1 0)) :: R1 (S1.hfrom (S1.mark (V1 0))) (S1.hfrom (V1 0)) :: nil) :: ( R1 (S1.hproper (S1.from (V1 0))) (S1.hfrom (S1.proper (V1 0))) :: nil) :: ( R1 (S1.hfst (V1 0) (S1.mark (V1 1))) (S1.hfst (V1 0) (V1 1)) :: R1 (S1.hfst (S1.mark (V1 0)) (V1 1)) (S1.hfst (V1 0) (V1 1)) :: R1 (S1.hfst (S1.ok (V1 0)) (S1.ok (V1 1))) (S1.hfst (V1 0) (V1 1)) :: nil) :: ( R1 (S1.hproper (S1.fst (V1 0) (V1 1))) (S1.hfst (S1.proper (V1 0)) (S1.proper (V1 1))) :: nil) :: ( R1 (S1.hcons (S1.ok (V1 0)) (S1.ok (V1 1))) (S1.hcons (V1 0) (V1 1)) :: R1 (S1.hcons (S1.mark (V1 0)) (V1 1)) (S1.hcons (V1 0) (V1 1)) :: nil) :: ( R1 (S1.hproper (S1.cons (V1 0) (V1 1))) (S1.hcons (S1.proper (V1 0)) (S1.proper (V1 1))) :: nil) :: ( R1 (S1.hproper (S1.cons (V1 0) (V1 1))) (S1.hproper (V1 0)) :: R1 (S1.hproper (S1.s (V1 0))) (S1.hproper (V1 0)) :: R1 (S1.hproper (S1.cons (V1 0) (V1 1))) (S1.hproper (V1 1)) :: R1 (S1.hproper (S1.fst (V1 0) (V1 1))) (S1.hproper (V1 0)) :: R1 (S1.hproper (S1.fst (V1 0) (V1 1))) (S1.hproper (V1 1)) :: R1 (S1.hproper (S1.from (V1 0))) (S1.hproper (V1 0)) :: R1 (S1.hproper (S1.add (V1 0) (V1 1))) (S1.hproper (V1 0)) :: R1 (S1.hproper (S1.add (V1 0) (V1 1))) (S1.hproper (V1 1)) :: R1 (S1.hproper (S1.len (V1 0))) (S1.hproper (V1 0)) :: nil) :: ( R1 (S1.htop (S1.mark (V1 0))) (S1.hproper (V1 0)) :: nil) :: ( R1 (S1.hactive (S1.len (V1 0))) (S1.hlen (S1.active (V1 0))) :: nil) :: ( R1 (S1.hactive (S1.add (V1 0) (V1 1))) (S1.hadd (V1 0) (S1.active (V1 1))) :: nil) :: ( R1 (S1.hactive (S1.add (V1 0) (V1 1))) (S1.hadd (S1.active (V1 0)) (V1 1)) :: nil) :: ( R1 (S1.hactive (S1.from (V1 0))) (S1.hfrom (S1.active (V1 0))) :: nil) :: ( R1 (S1.hactive (S1.fst (V1 0) (V1 1))) (S1.hfst (V1 0) (S1.active (V1 1))) :: nil) :: ( R1 (S1.hactive (S1.fst (V1 0) (V1 1))) (S1.hfst (S1.active (V1 0)) (V1 1)) :: nil) :: ( R1 (S1.hactive (S1.cons (V1 0) (V1 1))) (S1.hcons (S1.active (V1 0)) (V1 1)) :: nil) :: ( R1 (S1.hactive (S1.len (S1.cons (V1 0) (V1 1)))) (S1.hlen (V1 1)) :: nil) :: ( R1 (S1.hactive (S1.len (S1.cons (V1 0) (V1 1)))) (S1.hs (S1.len (V1 1))) :: nil) :: ( R1 (S1.hactive (S1.add (S1.s (V1 0)) (V1 1))) (S1.hadd (V1 0) (V1 1)) :: nil) :: ( R1 (S1.hactive (S1.add (S1.s (V1 0)) (V1 1))) (S1.hs (S1.add (V1 0) (V1 1))) :: nil) :: ( R1 (S1.hactive (S1.from (V1 0))) (S1.hs (V1 0)) :: nil) :: ( R1 (S1.hactive (S1.from (V1 0))) (S1.hfrom (S1.s (V1 0))) :: nil) :: ( R1 (S1.hactive (S1.from (V1 0))) (S1.hcons (V1 0) (S1.from (S1.s (V1 0)))) :: nil) :: ( R1 (S1.hactive (S1.fst (S1.s (V1 0)) (S1.cons (V1 1) (V1 2)))) (S1.hfst (V1 0) (V1 2)) :: nil) :: ( R1 (S1.hactive (S1.fst (S1.s (V1 0)) (S1.cons (V1 1) (V1 2)))) (S1.hcons (V1 1) (S1.fst (V1 0) (V1 2))) :: nil) :: ( R1 (S1.hactive (S1.fst (V1 0) (V1 1))) (S1.hactive (V1 0)) :: R1 (S1.hactive (S1.cons (V1 0) (V1 1))) (S1.hactive (V1 0)) :: R1 (S1.hactive (S1.fst (V1 0) (V1 1))) (S1.hactive (V1 1)) :: R1 (S1.hactive (S1.from (V1 0))) (S1.hactive (V1 0)) :: R1 (S1.hactive (S1.add (V1 0) (V1 1))) (S1.hactive (V1 0)) :: R1 (S1.hactive (S1.add (V1 0) (V1 1))) (S1.hactive (V1 1)) :: R1 (S1.hactive (S1.len (V1 0))) (S1.hactive (V1 0)) :: nil) :: ( R1 (S1.htop (S1.ok (V1 0))) (S1.hactive (V1 0)) :: nil) :: ( R1 (S1.htop (S1.ok (V1 0))) (S1.htop (S1.active (V1 0))) :: R1 (S1.htop (S1.mark (V1 0))) (S1.htop (S1.proper (V1 0))) :: 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.active) => nil | (int_symb M.active) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.fst) => nil | (int_symb M.fst) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.mark) => nil | (int_symb M.mark) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.s) => (2%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.s) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.from) => nil | (int_symb M.from) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.add) => nil | (int_symb M.add) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.len) => nil | (int_symb M.len) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.proper) => nil | (int_symb M.proper) => (2%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M.ok) => nil | (int_symb M.ok) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.top) => nil | (int_symb M.top) => 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.active) => nil | (int_symb M.active) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.fst) => nil | (int_symb M.fst) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => (3%Z, Vnil) :: nil | (hd_symb M.mark) => nil | (int_symb M.mark) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => (2%Z, Vnil) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.from) => nil | (int_symb M.from) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.add) => nil | (int_symb M.add) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.len) => (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.len) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.proper) => nil | (int_symb M.proper) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.ok) => nil | (int_symb M.ok) => (2%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.top) => nil | (int_symb M.top) => 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.active) => nil | (int_symb M.active) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.fst) => nil | (int_symb M.fst) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => (3%Z, Vnil) :: nil | (hd_symb M.mark) => nil | (int_symb M.mark) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => (3%Z, Vnil) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => (2%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.from) => nil | (int_symb M.from) => (2%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.add) => nil | (int_symb M.add) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.len) => (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.len) => (2%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.proper) => nil | (int_symb M.proper) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.ok) => nil | (int_symb M.ok) => nil | (hd_symb M.top) => nil | (int_symb M.top) => 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.active) => nil | (int_symb M.active) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.fst) => nil | (int_symb M.fst) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => (2%Z, Vnil) :: nil | (hd_symb M.mark) => nil | (int_symb M.mark) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => (2%Z, Vnil) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.from) => nil | (int_symb M.from) => (3%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.add) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (int_symb M.add) => (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.len) => nil | (int_symb M.len) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.proper) => nil | (int_symb M.proper) => (3%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.ok) => nil | (int_symb M.ok) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.top) => nil | (int_symb M.top) => 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.active) => nil | (int_symb M.active) => (1%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.fst) => nil | (int_symb M.fst) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.mark) => nil | (int_symb M.mark) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.s) => nil | (int_symb M.s) => nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.from) => nil | (int_symb M.from) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.add) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.add) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.len) => nil | (int_symb M.len) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.proper) => nil | (int_symb M.proper) => nil | (hd_symb M.ok) => nil | (int_symb M.ok) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.top) => nil | (int_symb M.top) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS5. Module PI5 := PolyInt PIS5. (* polynomial interpretation 6 *) Module PIS6 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.active) => nil | (int_symb M.active) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.fst) => nil | (int_symb M.fst) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => (2%Z, Vnil) :: nil | (hd_symb M.mark) => nil | (int_symb M.mark) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => (2%Z, Vnil) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => (2%Z, (Vcons 0 Vnil)) :: (3%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.from) => nil | (int_symb M.from) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.add) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.add) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.len) => nil | (int_symb M.len) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.proper) => nil | (int_symb M.proper) => (3%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.ok) => nil | (int_symb M.ok) => (2%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.top) => nil | (int_symb M.top) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS6. Module PI6 := PolyInt PIS6. (* polynomial interpretation 7 *) Module PIS7 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.active) => nil | (int_symb M.active) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.fst) => nil | (int_symb M.fst) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => (3%Z, Vnil) :: nil | (hd_symb M.mark) => nil | (int_symb M.mark) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => (2%Z, Vnil) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.from) => (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.from) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.add) => nil | (int_symb M.add) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.len) => nil | (int_symb M.len) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.proper) => nil | (int_symb M.proper) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.ok) => nil | (int_symb M.ok) => (2%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.top) => nil | (int_symb M.top) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS7. Module PI7 := PolyInt PIS7. (* polynomial interpretation 8 *) Module PIS8 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.active) => nil | (int_symb M.active) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.fst) => nil | (int_symb M.fst) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => (3%Z, Vnil) :: nil | (hd_symb M.mark) => nil | (int_symb M.mark) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => (3%Z, Vnil) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => (2%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.from) => (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.from) => (2%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.add) => nil | (int_symb M.add) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.len) => nil | (int_symb M.len) => (2%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.proper) => nil | (int_symb M.proper) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.ok) => nil | (int_symb M.ok) => nil | (hd_symb M.top) => nil | (int_symb M.top) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS8. Module PI8 := PolyInt PIS8. (* polynomial interpretation 9 *) Module PIS9 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.active) => nil | (int_symb M.active) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.fst) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (int_symb M.fst) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => (2%Z, Vnil) :: nil | (hd_symb M.mark) => nil | (int_symb M.mark) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => (2%Z, Vnil) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.from) => nil | (int_symb M.from) => (3%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.add) => nil | (int_symb M.add) => (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.len) => nil | (int_symb M.len) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.proper) => nil | (int_symb M.proper) => (3%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.ok) => nil | (int_symb M.ok) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.top) => nil | (int_symb M.top) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS9. Module PI9 := PolyInt PIS9. (* polynomial interpretation 10 *) Module PIS10 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.active) => nil | (int_symb M.active) => (1%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.fst) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.fst) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.mark) => nil | (int_symb M.mark) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.s) => nil | (int_symb M.s) => nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.from) => nil | (int_symb M.from) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.add) => nil | (int_symb M.add) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.len) => nil | (int_symb M.len) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.proper) => nil | (int_symb M.proper) => nil | (hd_symb M.ok) => nil | (int_symb M.ok) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.top) => nil | (int_symb M.top) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS10. Module PI10 := PolyInt PIS10. (* polynomial interpretation 11 *) Module PIS11 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.active) => nil | (int_symb M.active) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.fst) => (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.fst) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => (2%Z, Vnil) :: nil | (hd_symb M.mark) => nil | (int_symb M.mark) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => (2%Z, Vnil) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => (2%Z, (Vcons 0 Vnil)) :: (3%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.from) => nil | (int_symb M.from) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.add) => nil | (int_symb M.add) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.len) => nil | (int_symb M.len) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.proper) => nil | (int_symb M.proper) => (3%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.ok) => nil | (int_symb M.ok) => (2%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.top) => nil | (int_symb M.top) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS11. Module PI11 := PolyInt PIS11. (* polynomial interpretation 12 *) Module PIS12 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.active) => nil | (int_symb M.active) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.fst) => nil | (int_symb M.fst) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => (2%Z, Vnil) :: nil | (hd_symb M.mark) => nil | (int_symb M.mark) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => (2%Z, Vnil) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => (2%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.cons) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.cons) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.from) => nil | (int_symb M.from) => (1%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.add) => nil | (int_symb M.add) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.len) => nil | (int_symb M.len) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.proper) => nil | (int_symb M.proper) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.ok) => nil | (int_symb M.ok) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.top) => nil | (int_symb M.top) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS12. Module PI12 := PolyInt PIS12. (* polynomial interpretation 13 *) Module PIS13 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.active) => nil | (int_symb M.active) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.fst) => nil | (int_symb M.fst) => (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._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.mark) => nil | (int_symb M.mark) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => (1%Z, Vnil) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => nil | (hd_symb M.cons) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (int_symb M.cons) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.from) => nil | (int_symb M.from) => (2%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.add) => nil | (int_symb M.add) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.len) => nil | (int_symb M.len) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.proper) => nil | (int_symb M.proper) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.ok) => nil | (int_symb M.ok) => nil | (hd_symb M.top) => nil | (int_symb M.top) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS13. Module PI13 := PolyInt PIS13. (* polynomial interpretation 14 *) Module PIS14 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.active) => nil | (int_symb M.active) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.fst) => nil | (int_symb M.fst) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => (1%Z, Vnil) :: nil | (hd_symb M.mark) => nil | (int_symb M.mark) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => (1%Z, Vnil) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => (2%Z, (Vcons 1 Vnil)) :: 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.from) => nil | (int_symb M.from) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.add) => nil | (int_symb M.add) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.len) => nil | (int_symb M.len) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.proper) => (2%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.proper) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.ok) => nil | (int_symb M.ok) => nil | (hd_symb M.top) => nil | (int_symb M.top) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS14. Module PI14 := PolyInt PIS14. (* polynomial interpretation 15 *) Module PIS15 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.active) => nil | (int_symb M.active) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.fst) => nil | (int_symb M.fst) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => (2%Z, Vnil) :: nil | (hd_symb M.mark) => nil | (int_symb M.mark) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => (3%Z, Vnil) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.from) => nil | (int_symb M.from) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.add) => nil | (int_symb M.add) => nil | (hd_symb M.len) => nil | (int_symb M.len) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.proper) => (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.proper) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.ok) => nil | (int_symb M.ok) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.top) => nil | (int_symb M.top) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS15. Module PI15 := PolyInt PIS15. (* polynomial interpretation 16 *) Module PIS16 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.active) => nil | (int_symb M.active) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.fst) => nil | (int_symb M.fst) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.mark) => nil | (int_symb M.mark) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.s) => nil | (int_symb M.s) => (3%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.from) => nil | (int_symb M.from) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.add) => nil | (int_symb M.add) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.len) => nil | (int_symb M.len) => nil | (hd_symb M.proper) => (2%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.proper) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.ok) => nil | (int_symb M.ok) => nil | (hd_symb M.top) => nil | (int_symb M.top) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS16. Module PI16 := PolyInt PIS16. (* polynomial interpretation 17 *) Module PIS17 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.active) => nil | (int_symb M.active) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.fst) => nil | (int_symb M.fst) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.mark) => nil | (int_symb M.mark) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.s) => nil | (int_symb M.s) => (1%Z, (Vcons 0 Vnil)) :: (2%Z, (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))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.from) => nil | (int_symb M.from) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.add) => nil | (int_symb M.add) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.len) => nil | (int_symb M.len) => nil | (hd_symb M.proper) => (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.proper) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.ok) => nil | (int_symb M.ok) => nil | (hd_symb M.top) => nil | (int_symb M.top) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS17. Module PI17 := PolyInt PIS17. (* polynomial interpretation 18 *) Module PIS18 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.active) => nil | (int_symb M.active) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.fst) => nil | (int_symb M.fst) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => (1%Z, Vnil) :: nil | (hd_symb M.mark) => nil | (int_symb M.mark) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => (1%Z, Vnil) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.from) => nil | (int_symb M.from) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.add) => nil | (int_symb M.add) => (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.len) => nil | (int_symb M.len) => nil | (hd_symb M.proper) => (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.proper) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.ok) => nil | (int_symb M.ok) => nil | (hd_symb M.top) => nil | (int_symb M.top) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS18. Module PI18 := PolyInt PIS18. (* polynomial interpretation 19 *) Module PIS19 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.active) => (2%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.active) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.fst) => nil | (int_symb M.fst) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.mark) => nil | (int_symb M.mark) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.s) => nil | (int_symb M.s) => nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.from) => nil | (int_symb M.from) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.add) => nil | (int_symb M.add) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.len) => nil | (int_symb M.len) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.proper) => nil | (int_symb M.proper) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.ok) => nil | (int_symb M.ok) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.top) => nil | (int_symb M.top) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS19. Module PI19 := PolyInt PIS19. (* polynomial interpretation 20 *) Module PIS20 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.active) => (2%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.active) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.fst) => nil | (int_symb M.fst) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => (3%Z, Vnil) :: nil | (hd_symb M.mark) => nil | (int_symb M.mark) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.s) => nil | (int_symb M.s) => (2%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M.cons) => nil | (int_symb M.cons) => nil | (hd_symb M.from) => nil | (int_symb M.from) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.add) => nil | (int_symb M.add) => (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.len) => nil | (int_symb M.len) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.proper) => nil | (int_symb M.proper) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.ok) => nil | (int_symb M.ok) => nil | (hd_symb M.top) => nil | (int_symb M.top) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS20. Module PI20 := PolyInt PIS20. (* polynomial interpretation 21 *) Module PIS21 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.active) => (2%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.active) => (2%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.fst) => nil | (int_symb M.fst) => (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._0_1) => nil | (int_symb M._0_1) => (1%Z, Vnil) :: nil | (hd_symb M.mark) => nil | (int_symb M.mark) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => (2%Z, Vnil) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.from) => nil | (int_symb M.from) => (2%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.add) => nil | (int_symb M.add) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.len) => nil | (int_symb M.len) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.proper) => nil | (int_symb M.proper) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.ok) => nil | (int_symb M.ok) => (1%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M.top) => nil | (int_symb M.top) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS21. Module PI21 := PolyInt PIS21. (* polynomial interpretation 22 *) Module PIS22 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.active) => nil | (int_symb M.active) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.fst) => nil | (int_symb M.fst) => (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._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.mark) => nil | (int_symb M.mark) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => (2%Z, Vnil) :: nil | (hd_symb M.s) => nil | (int_symb M.s) => nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.from) => nil | (int_symb M.from) => (2%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.add) => nil | (int_symb M.add) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.len) => nil | (int_symb M.len) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.proper) => nil | (int_symb M.proper) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.ok) => nil | (int_symb M.ok) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.top) => (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.top) => (2%Z, (Vcons 1 Vnil)) :: nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS22. Module PI22 := PolyInt PIS22. (* polynomial interpretation 23 *) Module PIS23 (*<: TPolyInt*). Definition sig := s1. Definition trsInt f := match f as f return poly (@ASignature.arity s1 f) with | (hd_symb M.active) => nil | (int_symb M.active) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.fst) => nil | (int_symb M.fst) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M._0_1) => nil | (int_symb M._0_1) => nil | (hd_symb M.mark) => nil | (int_symb M.mark) => nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.s) => nil | (int_symb M.s) => (2%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.cons) => nil | (int_symb M.cons) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.from) => nil | (int_symb M.from) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.add) => nil | (int_symb M.add) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.len) => nil | (int_symb M.len) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.proper) => nil | (int_symb M.proper) => (3%Z, (Vcons 0 Vnil)) :: (3%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.ok) => nil | (int_symb M.ok) => (3%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.top) => (3%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.top) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS23. Module PI23 := PolyInt PIS23. (* 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. right. PI1.prove_termination. termination_trivial. left. co_scc. right. PI2.prove_termination. PI3.prove_termination. termination_trivial. left. co_scc. right. PI4.prove_termination. PI5.prove_termination. PI6.prove_termination. termination_trivial. left. co_scc. right. PI7.prove_termination. PI8.prove_termination. termination_trivial. left. co_scc. right. PI9.prove_termination. PI10.prove_termination. PI11.prove_termination. termination_trivial. left. co_scc. right. PI12.prove_termination. PI13.prove_termination. termination_trivial. left. co_scc. right. PI14.prove_termination. PI15.prove_termination. PI16.prove_termination. PI17.prove_termination. PI18.prove_termination. termination_trivial. 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. left. co_scc. right. PI19.prove_termination. PI20.prove_termination. PI21.prove_termination. termination_trivial. left. co_scc. right. PI22.prove_termination. PI23.prove_termination. termination_trivial. Qed.