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 := | __ : symb | a : symb | activate : symb | and : symb | e : symb | i : symb | isList : symb | isNeList : symb | isNePal : symb | isPal : symb | isQid : symb | n____ : symb | n__a : symb | n__e : symb | n__i : symb | n__isList : symb | n__isNeList : symb | n__isPal : symb | n__nil : symb | n__o : symb | n__u : symb | nil : symb | o : symb | tt : symb | u : 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.__ => 2 | M.a => 0 | M.activate => 1 | M.and => 2 | M.e => 0 | M.i => 0 | M.isList => 1 | M.isNeList => 1 | M.isNePal => 1 | M.isPal => 1 | M.isQid => 1 | M.n____ => 2 | M.n__a => 0 | M.n__e => 0 | M.n__i => 0 | M.n__isList => 1 | M.n__isNeList => 1 | M.n__isPal => 1 | M.n__nil => 0 | M.n__o => 0 | M.n__u => 0 | M.nil => 0 | M.o => 0 | M.tt => 0 | M.u => 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 __ x2 x1 := F0 M.__ (Vcons x2 (Vcons x1 Vnil)). Definition a := F0 M.a Vnil. Definition activate x1 := F0 M.activate (Vcons x1 Vnil). Definition and x2 x1 := F0 M.and (Vcons x2 (Vcons x1 Vnil)). Definition e := F0 M.e Vnil. Definition i := F0 M.i Vnil. Definition isList x1 := F0 M.isList (Vcons x1 Vnil). Definition isNeList x1 := F0 M.isNeList (Vcons x1 Vnil). Definition isNePal x1 := F0 M.isNePal (Vcons x1 Vnil). Definition isPal x1 := F0 M.isPal (Vcons x1 Vnil). Definition isQid x1 := F0 M.isQid (Vcons x1 Vnil). Definition n____ x2 x1 := F0 M.n____ (Vcons x2 (Vcons x1 Vnil)). Definition n__a := F0 M.n__a Vnil. Definition n__e := F0 M.n__e Vnil. Definition n__i := F0 M.n__i Vnil. Definition n__isList x1 := F0 M.n__isList (Vcons x1 Vnil). Definition n__isNeList x1 := F0 M.n__isNeList (Vcons x1 Vnil). Definition n__isPal x1 := F0 M.n__isPal (Vcons x1 Vnil). Definition n__nil := F0 M.n__nil Vnil. Definition n__o := F0 M.n__o Vnil. Definition n__u := F0 M.n__u Vnil. Definition nil := F0 M.nil Vnil. Definition o := F0 M.o Vnil. Definition tt := F0 M.tt Vnil. Definition u := F0 M.u Vnil. End S0. Definition E := @nil (@ATrs.rule s0). Definition R := R0 (S0.__ (S0.__ (V0 0) (V0 1)) (V0 2)) (S0.__ (V0 0) (S0.__ (V0 1) (V0 2))) :: R0 (S0.__ (V0 0) S0.nil) (V0 0) :: R0 (S0.__ S0.nil (V0 0)) (V0 0) :: R0 (S0.and S0.tt (V0 0)) (S0.activate (V0 0)) :: R0 (S0.isList (V0 0)) (S0.isNeList (S0.activate (V0 0))) :: R0 (S0.isList S0.n__nil) S0.tt :: R0 (S0.isList (S0.n____ (V0 0) (V0 1))) (S0.and (S0.isList (S0.activate (V0 0))) (S0.n__isList (S0.activate (V0 1)))) :: R0 (S0.isNeList (V0 0)) (S0.isQid (S0.activate (V0 0))) :: R0 (S0.isNeList (S0.n____ (V0 0) (V0 1))) (S0.and (S0.isList (S0.activate (V0 0))) (S0.n__isNeList (S0.activate (V0 1)))) :: R0 (S0.isNeList (S0.n____ (V0 0) (V0 1))) (S0.and (S0.isNeList (S0.activate (V0 0))) (S0.n__isList (S0.activate (V0 1)))) :: R0 (S0.isNePal (V0 0)) (S0.isQid (S0.activate (V0 0))) :: R0 (S0.isNePal (S0.n____ (V0 0) (S0.n____ (V0 1) (V0 0)))) (S0.and (S0.isQid (S0.activate (V0 0))) (S0.n__isPal (S0.activate (V0 1)))) :: R0 (S0.isPal (V0 0)) (S0.isNePal (S0.activate (V0 0))) :: R0 (S0.isPal S0.n__nil) S0.tt :: R0 (S0.isQid S0.n__a) S0.tt :: R0 (S0.isQid S0.n__e) S0.tt :: R0 (S0.isQid S0.n__i) S0.tt :: R0 (S0.isQid S0.n__o) S0.tt :: R0 (S0.isQid S0.n__u) S0.tt :: R0 S0.nil S0.n__nil :: R0 (S0.__ (V0 0) (V0 1)) (S0.n____ (V0 0) (V0 1)) :: R0 (S0.isList (V0 0)) (S0.n__isList (V0 0)) :: R0 (S0.isNeList (V0 0)) (S0.n__isNeList (V0 0)) :: R0 (S0.isPal (V0 0)) (S0.n__isPal (V0 0)) :: R0 S0.a S0.n__a :: R0 S0.e S0.n__e :: R0 S0.i S0.n__i :: R0 S0.o S0.n__o :: R0 S0.u S0.n__u :: R0 (S0.activate S0.n__nil) S0.nil :: R0 (S0.activate (S0.n____ (V0 0) (V0 1))) (S0.__ (S0.activate (V0 0)) (S0.activate (V0 1))) :: R0 (S0.activate (S0.n__isList (V0 0))) (S0.isList (V0 0)) :: R0 (S0.activate (S0.n__isNeList (V0 0))) (S0.isNeList (V0 0)) :: R0 (S0.activate (S0.n__isPal (V0 0))) (S0.isPal (V0 0)) :: R0 (S0.activate S0.n__a) S0.a :: R0 (S0.activate S0.n__e) S0.e :: R0 (S0.activate S0.n__i) S0.i :: R0 (S0.activate S0.n__o) S0.o :: R0 (S0.activate S0.n__u) S0.u :: R0 (S0.activate (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__ x2 x1 := F1 (hd_symb s1_p M.__) (Vcons x2 (Vcons x1 Vnil)). Definition __ x2 x1 := F1 (int_symb s1_p M.__) (Vcons x2 (Vcons x1 Vnil)). Definition ha := F1 (hd_symb s1_p M.a) Vnil. Definition a := F1 (int_symb s1_p M.a) Vnil. Definition hactivate x1 := F1 (hd_symb s1_p M.activate) (Vcons x1 Vnil). Definition activate x1 := F1 (int_symb s1_p M.activate) (Vcons x1 Vnil). Definition hand x2 x1 := F1 (hd_symb s1_p M.and) (Vcons x2 (Vcons x1 Vnil)). Definition and x2 x1 := F1 (int_symb s1_p M.and) (Vcons x2 (Vcons x1 Vnil)). Definition he := F1 (hd_symb s1_p M.e) Vnil. Definition e := F1 (int_symb s1_p M.e) Vnil. Definition hi := F1 (hd_symb s1_p M.i) Vnil. Definition i := F1 (int_symb s1_p M.i) Vnil. Definition hisList x1 := F1 (hd_symb s1_p M.isList) (Vcons x1 Vnil). Definition isList x1 := F1 (int_symb s1_p M.isList) (Vcons x1 Vnil). Definition hisNeList x1 := F1 (hd_symb s1_p M.isNeList) (Vcons x1 Vnil). Definition isNeList x1 := F1 (int_symb s1_p M.isNeList) (Vcons x1 Vnil). Definition hisNePal x1 := F1 (hd_symb s1_p M.isNePal) (Vcons x1 Vnil). Definition isNePal x1 := F1 (int_symb s1_p M.isNePal) (Vcons x1 Vnil). Definition hisPal x1 := F1 (hd_symb s1_p M.isPal) (Vcons x1 Vnil). Definition isPal x1 := F1 (int_symb s1_p M.isPal) (Vcons x1 Vnil). Definition hisQid x1 := F1 (hd_symb s1_p M.isQid) (Vcons x1 Vnil). Definition isQid x1 := F1 (int_symb s1_p M.isQid) (Vcons x1 Vnil). Definition hn____ x2 x1 := F1 (hd_symb s1_p M.n____) (Vcons x2 (Vcons x1 Vnil)). Definition n____ x2 x1 := F1 (int_symb s1_p M.n____) (Vcons x2 (Vcons x1 Vnil)). Definition hn__a := F1 (hd_symb s1_p M.n__a) Vnil. Definition n__a := F1 (int_symb s1_p M.n__a) Vnil. Definition hn__e := F1 (hd_symb s1_p M.n__e) Vnil. Definition n__e := F1 (int_symb s1_p M.n__e) Vnil. Definition hn__i := F1 (hd_symb s1_p M.n__i) Vnil. Definition n__i := F1 (int_symb s1_p M.n__i) Vnil. Definition hn__isList x1 := F1 (hd_symb s1_p M.n__isList) (Vcons x1 Vnil). Definition n__isList x1 := F1 (int_symb s1_p M.n__isList) (Vcons x1 Vnil). Definition hn__isNeList x1 := F1 (hd_symb s1_p M.n__isNeList) (Vcons x1 Vnil). Definition n__isNeList x1 := F1 (int_symb s1_p M.n__isNeList) (Vcons x1 Vnil). Definition hn__isPal x1 := F1 (hd_symb s1_p M.n__isPal) (Vcons x1 Vnil). Definition n__isPal x1 := F1 (int_symb s1_p M.n__isPal) (Vcons x1 Vnil). Definition hn__nil := F1 (hd_symb s1_p M.n__nil) Vnil. Definition n__nil := F1 (int_symb s1_p M.n__nil) Vnil. Definition hn__o := F1 (hd_symb s1_p M.n__o) Vnil. Definition n__o := F1 (int_symb s1_p M.n__o) Vnil. Definition hn__u := F1 (hd_symb s1_p M.n__u) Vnil. Definition n__u := F1 (int_symb s1_p M.n__u) Vnil. Definition hnil := F1 (hd_symb s1_p M.nil) Vnil. Definition nil := F1 (int_symb s1_p M.nil) Vnil. Definition ho := F1 (hd_symb s1_p M.o) Vnil. Definition o := F1 (int_symb s1_p M.o) Vnil. Definition htt := F1 (hd_symb s1_p M.tt) Vnil. Definition tt := F1 (int_symb s1_p M.tt) Vnil. Definition hu := F1 (hd_symb s1_p M.u) Vnil. Definition u := F1 (int_symb s1_p M.u) Vnil. End S1. (* graph decomposition 1 *) Definition cs1 : list (list (@ATrs.rule s1)) := ( R1 (S1.hactivate (S1.n__u)) (S1.hu) :: nil) :: ( R1 (S1.hactivate (S1.n__o)) (S1.ho) :: nil) :: ( R1 (S1.hactivate (S1.n__i)) (S1.hi) :: nil) :: ( R1 (S1.hactivate (S1.n__e)) (S1.he) :: nil) :: ( R1 (S1.hactivate (S1.n__a)) (S1.ha) :: nil) :: ( R1 (S1.hactivate (S1.n__nil)) (S1.hnil) :: nil) :: ( R1 (S1.hisNePal (S1.n____ (V1 0) (S1.n____ (V1 1) (V1 0)))) (S1.hisQid (S1.activate (V1 0))) :: nil) :: ( R1 (S1.hisNePal (V1 0)) (S1.hisQid (S1.activate (V1 0))) :: nil) :: ( R1 (S1.hisNeList (V1 0)) (S1.hisQid (S1.activate (V1 0))) :: nil) :: ( R1 (S1.h__ (S1.__ (V1 0) (V1 1)) (V1 2)) (S1.h__ (V1 1) (V1 2)) :: R1 (S1.h__ (S1.__ (V1 0) (V1 1)) (V1 2)) (S1.h__ (V1 0) (S1.__ (V1 1) (V1 2))) :: nil) :: ( R1 (S1.hactivate (S1.n____ (V1 0) (V1 1))) (S1.h__ (S1.activate (V1 0)) (S1.activate (V1 1))) :: nil) :: ( R1 (S1.hactivate (S1.n____ (V1 0) (V1 1))) (S1.hactivate (V1 0)) :: R1 (S1.hactivate (S1.n____ (V1 0) (V1 1))) (S1.hactivate (V1 1)) :: R1 (S1.hactivate (S1.n__isList (V1 0))) (S1.hisList (V1 0)) :: R1 (S1.hisList (V1 0)) (S1.hisNeList (S1.activate (V1 0))) :: R1 (S1.hisNeList (V1 0)) (S1.hactivate (V1 0)) :: R1 (S1.hactivate (S1.n__isNeList (V1 0))) (S1.hisNeList (V1 0)) :: R1 (S1.hisNeList (S1.n____ (V1 0) (V1 1))) (S1.hand (S1.isList (S1.activate (V1 0))) (S1.n__isNeList (S1.activate (V1 1)))) :: R1 (S1.hand (S1.tt) (V1 0)) (S1.hactivate (V1 0)) :: R1 (S1.hactivate (S1.n__isPal (V1 0))) (S1.hisPal (V1 0)) :: R1 (S1.hisPal (V1 0)) (S1.hisNePal (S1.activate (V1 0))) :: R1 (S1.hisNePal (V1 0)) (S1.hactivate (V1 0)) :: R1 (S1.hisNePal (S1.n____ (V1 0) (S1.n____ (V1 1) (V1 0)))) (S1.hand (S1.isQid (S1.activate (V1 0))) (S1.n__isPal (S1.activate (V1 1)))) :: R1 (S1.hisNePal (S1.n____ (V1 0) (S1.n____ (V1 1) (V1 0)))) (S1.hactivate (V1 0)) :: R1 (S1.hisNePal (S1.n____ (V1 0) (S1.n____ (V1 1) (V1 0)))) (S1.hactivate (V1 1)) :: R1 (S1.hisPal (V1 0)) (S1.hactivate (V1 0)) :: R1 (S1.hisNeList (S1.n____ (V1 0) (V1 1))) (S1.hisList (S1.activate (V1 0))) :: R1 (S1.hisList (V1 0)) (S1.hactivate (V1 0)) :: R1 (S1.hisList (S1.n____ (V1 0) (V1 1))) (S1.hand (S1.isList (S1.activate (V1 0))) (S1.n__isList (S1.activate (V1 1)))) :: R1 (S1.hisList (S1.n____ (V1 0) (V1 1))) (S1.hisList (S1.activate (V1 0))) :: R1 (S1.hisList (S1.n____ (V1 0) (V1 1))) (S1.hactivate (V1 0)) :: R1 (S1.hisList (S1.n____ (V1 0) (V1 1))) (S1.hactivate (V1 1)) :: R1 (S1.hisNeList (S1.n____ (V1 0) (V1 1))) (S1.hactivate (V1 0)) :: R1 (S1.hisNeList (S1.n____ (V1 0) (V1 1))) (S1.hactivate (V1 1)) :: R1 (S1.hisNeList (S1.n____ (V1 0) (V1 1))) (S1.hand (S1.isNeList (S1.activate (V1 0))) (S1.n__isList (S1.activate (V1 1)))) :: R1 (S1.hisNeList (S1.n____ (V1 0) (V1 1))) (S1.hisNeList (S1.activate (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.__) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.__) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => (2%Z, Vnil) :: nil | (hd_symb M.and) => nil | (int_symb M.and) => (3%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tt) => nil | (int_symb M.tt) => nil | (hd_symb M.activate) => nil | (int_symb M.activate) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isList) => nil | (int_symb M.isList) => nil | (hd_symb M.isNeList) => nil | (int_symb M.isNeList) => nil | (hd_symb M.n__nil) => nil | (int_symb M.n__nil) => (2%Z, Vnil) :: nil | (hd_symb M.n____) => nil | (int_symb M.n____) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.n__isList) => nil | (int_symb M.n__isList) => nil | (hd_symb M.isQid) => nil | (int_symb M.isQid) => nil | (hd_symb M.n__isNeList) => nil | (int_symb M.n__isNeList) => nil | (hd_symb M.isNePal) => nil | (int_symb M.isNePal) => nil | (hd_symb M.n__isPal) => nil | (int_symb M.n__isPal) => nil | (hd_symb M.isPal) => nil | (int_symb M.isPal) => nil | (hd_symb M.n__a) => nil | (int_symb M.n__a) => nil | (hd_symb M.n__e) => nil | (int_symb M.n__e) => nil | (hd_symb M.n__i) => nil | (int_symb M.n__i) => (1%Z, Vnil) :: nil | (hd_symb M.n__o) => nil | (int_symb M.n__o) => nil | (hd_symb M.n__u) => nil | (int_symb M.n__u) => nil | (hd_symb M.a) => nil | (int_symb M.a) => nil | (hd_symb M.e) => nil | (int_symb M.e) => nil | (hd_symb M.i) => nil | (int_symb M.i) => (2%Z, Vnil) :: nil | (hd_symb M.o) => nil | (int_symb M.o) => nil | (hd_symb M.u) => nil | (int_symb M.u) => 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.__) => nil | (int_symb M.__) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => (1%Z, Vnil) :: nil | (hd_symb M.and) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.and) => (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.tt) => nil | (int_symb M.tt) => nil | (hd_symb M.activate) => (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.activate) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isList) => (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.isList) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isNeList) => (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.isNeList) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.n__nil) => nil | (int_symb M.n__nil) => (1%Z, Vnil) :: nil | (hd_symb M.n____) => nil | (int_symb M.n____) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.n__isList) => nil | (int_symb M.n__isList) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isQid) => nil | (int_symb M.isQid) => nil | (hd_symb M.n__isNeList) => nil | (int_symb M.n__isNeList) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isNePal) => (2%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.isNePal) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.n__isPal) => nil | (int_symb M.n__isPal) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isPal) => (2%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.isPal) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.n__a) => nil | (int_symb M.n__a) => nil | (hd_symb M.n__e) => nil | (int_symb M.n__e) => (1%Z, Vnil) :: nil | (hd_symb M.n__i) => nil | (int_symb M.n__i) => nil | (hd_symb M.n__o) => nil | (int_symb M.n__o) => nil | (hd_symb M.n__u) => nil | (int_symb M.n__u) => nil | (hd_symb M.a) => nil | (int_symb M.a) => nil | (hd_symb M.e) => nil | (int_symb M.e) => (1%Z, Vnil) :: nil | (hd_symb M.i) => nil | (int_symb M.i) => nil | (hd_symb M.o) => nil | (int_symb M.o) => nil | (hd_symb M.u) => nil | (int_symb M.u) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS2. Module PI2 := PolyInt PIS2. (* graph decomposition 2 *) Definition cs2 : list (list (@ATrs.rule s1)) := ( R1 (S1.hisList (V1 0)) (S1.hisNeList (S1.activate (V1 0))) :: R1 (S1.hisNeList (V1 0)) (S1.hactivate (V1 0)) :: R1 (S1.hactivate (S1.n__isList (V1 0))) (S1.hisList (V1 0)) :: R1 (S1.hisList (V1 0)) (S1.hactivate (V1 0)) :: R1 (S1.hactivate (S1.n__isNeList (V1 0))) (S1.hisNeList (V1 0)) :: R1 (S1.hactivate (S1.n__isPal (V1 0))) (S1.hisPal (V1 0)) :: R1 (S1.hisPal (V1 0)) (S1.hisNePal (S1.activate (V1 0))) :: R1 (S1.hisNePal (V1 0)) (S1.hactivate (V1 0)) :: R1 (S1.hisPal (V1 0)) (S1.hactivate (V1 0)) :: nil) :: ( R1 (S1.hand (S1.tt) (V1 0)) (S1.hactivate (V1 0)) :: nil) :: nil. (* 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.__) => nil | (int_symb M.__) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tt) => nil | (int_symb M.tt) => nil | (hd_symb M.activate) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.activate) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isList) => (2%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.isList) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isNeList) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.isNeList) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.n__nil) => nil | (int_symb M.n__nil) => nil | (hd_symb M.n____) => nil | (int_symb M.n____) => (3%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.n__isList) => nil | (int_symb M.n__isList) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isQid) => nil | (int_symb M.isQid) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.n__isNeList) => nil | (int_symb M.n__isNeList) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isNePal) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.isNePal) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.n__isPal) => nil | (int_symb M.n__isPal) => (3%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isPal) => (2%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.isPal) => (3%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.n__a) => nil | (int_symb M.n__a) => nil | (hd_symb M.n__e) => nil | (int_symb M.n__e) => nil | (hd_symb M.n__i) => nil | (int_symb M.n__i) => nil | (hd_symb M.n__o) => nil | (int_symb M.n__o) => nil | (hd_symb M.n__u) => nil | (int_symb M.n__u) => nil | (hd_symb M.a) => nil | (int_symb M.a) => nil | (hd_symb M.e) => nil | (int_symb M.e) => nil | (hd_symb M.i) => nil | (int_symb M.i) => nil | (hd_symb M.o) => nil | (int_symb M.o) => nil | (hd_symb M.u) => nil | (int_symb M.u) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS3. Module PI3 := PolyInt PIS3. (* graph decomposition 3 *) Definition cs3 : list (list (@ATrs.rule s1)) := ( R1 (S1.hactivate (S1.n__isList (V1 0))) (S1.hisList (V1 0)) :: nil) :: ( R1 (S1.hisNePal (V1 0)) (S1.hactivate (V1 0)) :: nil) :: ( R1 (S1.hisNeList (V1 0)) (S1.hactivate (V1 0)) :: 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. left. co_scc. right. PI1.prove_termination. termination_trivial. left. co_scc. right. PI2.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. 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) cs3; subst D; subst R. dpg_unif_N_correct. left. co_scc. left. co_scc. left. co_scc. left. co_scc. Qed.