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 := | U11 : symb | U12 : symb | U21 : symb | U22 : symb | U23 : symb | U31 : symb | U32 : symb | U41 : symb | U42 : symb | U43 : symb | U51 : symb | U52 : symb | U53 : symb | U61 : symb | U62 : symb | U71 : symb | U72 : symb | __ : symb | a : symb | a__U11 : symb | a__U12 : symb | a__U21 : symb | a__U22 : symb | a__U23 : symb | a__U31 : symb | a__U32 : symb | a__U41 : symb | a__U42 : symb | a__U43 : symb | a__U51 : symb | a__U52 : symb | a__U53 : symb | a__U61 : symb | a__U62 : symb | a__U71 : symb | a__U72 : symb | a____ : symb | a__and : symb | a__isList : symb | a__isNeList : symb | a__isNePal : symb | a__isPal : symb | a__isPalListKind : symb | a__isQid : symb | and : symb | e : symb | i : symb | isList : symb | isNeList : symb | isNePal : symb | isPal : symb | isPalListKind : symb | isQid : symb | mark : 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.U11 => 2 | M.U12 => 1 | M.U21 => 3 | M.U22 => 2 | M.U23 => 1 | M.U31 => 2 | M.U32 => 1 | M.U41 => 3 | M.U42 => 2 | M.U43 => 1 | M.U51 => 3 | M.U52 => 2 | M.U53 => 1 | M.U61 => 2 | M.U62 => 1 | M.U71 => 2 | M.U72 => 1 | M.__ => 2 | M.a => 0 | M.a__U11 => 2 | M.a__U12 => 1 | M.a__U21 => 3 | M.a__U22 => 2 | M.a__U23 => 1 | M.a__U31 => 2 | M.a__U32 => 1 | M.a__U41 => 3 | M.a__U42 => 2 | M.a__U43 => 1 | M.a__U51 => 3 | M.a__U52 => 2 | M.a__U53 => 1 | M.a__U61 => 2 | M.a__U62 => 1 | M.a__U71 => 2 | M.a__U72 => 1 | M.a____ => 2 | M.a__and => 2 | M.a__isList => 1 | M.a__isNeList => 1 | M.a__isNePal => 1 | M.a__isPal => 1 | M.a__isPalListKind => 1 | M.a__isQid => 1 | M.and => 2 | M.e => 0 | M.i => 0 | M.isList => 1 | M.isNeList => 1 | M.isNePal => 1 | M.isPal => 1 | M.isPalListKind => 1 | M.isQid => 1 | M.mark => 1 | 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 U11 x2 x1 := F0 M.U11 (Vcons x2 (Vcons x1 Vnil)). Definition U12 x1 := F0 M.U12 (Vcons x1 Vnil). Definition U21 x3 x2 x1 := F0 M.U21 (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition U22 x2 x1 := F0 M.U22 (Vcons x2 (Vcons x1 Vnil)). Definition U23 x1 := F0 M.U23 (Vcons x1 Vnil). Definition U31 x2 x1 := F0 M.U31 (Vcons x2 (Vcons x1 Vnil)). Definition U32 x1 := F0 M.U32 (Vcons x1 Vnil). Definition U41 x3 x2 x1 := F0 M.U41 (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition U42 x2 x1 := F0 M.U42 (Vcons x2 (Vcons x1 Vnil)). Definition U43 x1 := F0 M.U43 (Vcons x1 Vnil). Definition U51 x3 x2 x1 := F0 M.U51 (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition U52 x2 x1 := F0 M.U52 (Vcons x2 (Vcons x1 Vnil)). Definition U53 x1 := F0 M.U53 (Vcons x1 Vnil). Definition U61 x2 x1 := F0 M.U61 (Vcons x2 (Vcons x1 Vnil)). Definition U62 x1 := F0 M.U62 (Vcons x1 Vnil). Definition U71 x2 x1 := F0 M.U71 (Vcons x2 (Vcons x1 Vnil)). Definition U72 x1 := F0 M.U72 (Vcons x1 Vnil). Definition __ x2 x1 := F0 M.__ (Vcons x2 (Vcons x1 Vnil)). Definition a := F0 M.a Vnil. Definition a__U11 x2 x1 := F0 M.a__U11 (Vcons x2 (Vcons x1 Vnil)). Definition a__U12 x1 := F0 M.a__U12 (Vcons x1 Vnil). Definition a__U21 x3 x2 x1 := F0 M.a__U21 (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition a__U22 x2 x1 := F0 M.a__U22 (Vcons x2 (Vcons x1 Vnil)). Definition a__U23 x1 := F0 M.a__U23 (Vcons x1 Vnil). Definition a__U31 x2 x1 := F0 M.a__U31 (Vcons x2 (Vcons x1 Vnil)). Definition a__U32 x1 := F0 M.a__U32 (Vcons x1 Vnil). Definition a__U41 x3 x2 x1 := F0 M.a__U41 (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition a__U42 x2 x1 := F0 M.a__U42 (Vcons x2 (Vcons x1 Vnil)). Definition a__U43 x1 := F0 M.a__U43 (Vcons x1 Vnil). Definition a__U51 x3 x2 x1 := F0 M.a__U51 (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition a__U52 x2 x1 := F0 M.a__U52 (Vcons x2 (Vcons x1 Vnil)). Definition a__U53 x1 := F0 M.a__U53 (Vcons x1 Vnil). Definition a__U61 x2 x1 := F0 M.a__U61 (Vcons x2 (Vcons x1 Vnil)). Definition a__U62 x1 := F0 M.a__U62 (Vcons x1 Vnil). Definition a__U71 x2 x1 := F0 M.a__U71 (Vcons x2 (Vcons x1 Vnil)). Definition a__U72 x1 := F0 M.a__U72 (Vcons x1 Vnil). Definition a____ x2 x1 := F0 M.a____ (Vcons x2 (Vcons x1 Vnil)). Definition a__and x2 x1 := F0 M.a__and (Vcons x2 (Vcons x1 Vnil)). Definition a__isList x1 := F0 M.a__isList (Vcons x1 Vnil). Definition a__isNeList x1 := F0 M.a__isNeList (Vcons x1 Vnil). Definition a__isNePal x1 := F0 M.a__isNePal (Vcons x1 Vnil). Definition a__isPal x1 := F0 M.a__isPal (Vcons x1 Vnil). Definition a__isPalListKind x1 := F0 M.a__isPalListKind (Vcons x1 Vnil). Definition a__isQid x1 := F0 M.a__isQid (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 isPalListKind x1 := F0 M.isPalListKind (Vcons x1 Vnil). Definition isQid x1 := F0 M.isQid (Vcons x1 Vnil). Definition mark x1 := F0 M.mark (Vcons x1 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.a____ (S0.__ (V0 0) (V0 1)) (V0 2)) (S0.a____ (S0.mark (V0 0)) (S0.a____ (S0.mark (V0 1)) (S0.mark (V0 2)))) :: R0 (S0.a____ (V0 0) S0.nil) (S0.mark (V0 0)) :: R0 (S0.a____ S0.nil (V0 0)) (S0.mark (V0 0)) :: R0 (S0.a__U11 S0.tt (V0 0)) (S0.a__U12 (S0.a__isNeList (V0 0))) :: R0 (S0.a__U12 S0.tt) S0.tt :: R0 (S0.a__U21 S0.tt (V0 0) (V0 1)) (S0.a__U22 (S0.a__isList (V0 0)) (V0 1)) :: R0 (S0.a__U22 S0.tt (V0 0)) (S0.a__U23 (S0.a__isList (V0 0))) :: R0 (S0.a__U23 S0.tt) S0.tt :: R0 (S0.a__U31 S0.tt (V0 0)) (S0.a__U32 (S0.a__isQid (V0 0))) :: R0 (S0.a__U32 S0.tt) S0.tt :: R0 (S0.a__U41 S0.tt (V0 0) (V0 1)) (S0.a__U42 (S0.a__isList (V0 0)) (V0 1)) :: R0 (S0.a__U42 S0.tt (V0 0)) (S0.a__U43 (S0.a__isNeList (V0 0))) :: R0 (S0.a__U43 S0.tt) S0.tt :: R0 (S0.a__U51 S0.tt (V0 0) (V0 1)) (S0.a__U52 (S0.a__isNeList (V0 0)) (V0 1)) :: R0 (S0.a__U52 S0.tt (V0 0)) (S0.a__U53 (S0.a__isList (V0 0))) :: R0 (S0.a__U53 S0.tt) S0.tt :: R0 (S0.a__U61 S0.tt (V0 0)) (S0.a__U62 (S0.a__isQid (V0 0))) :: R0 (S0.a__U62 S0.tt) S0.tt :: R0 (S0.a__U71 S0.tt (V0 0)) (S0.a__U72 (S0.a__isNePal (V0 0))) :: R0 (S0.a__U72 S0.tt) S0.tt :: R0 (S0.a__and S0.tt (V0 0)) (S0.mark (V0 0)) :: R0 (S0.a__isList (V0 0)) (S0.a__U11 (S0.a__isPalListKind (V0 0)) (V0 0)) :: R0 (S0.a__isList S0.nil) S0.tt :: R0 (S0.a__isList (S0.__ (V0 0) (V0 1))) (S0.a__U21 (S0.a__and (S0.a__isPalListKind (V0 0)) (S0.isPalListKind (V0 1))) (V0 0) (V0 1)) :: R0 (S0.a__isNeList (V0 0)) (S0.a__U31 (S0.a__isPalListKind (V0 0)) (V0 0)) :: R0 (S0.a__isNeList (S0.__ (V0 0) (V0 1))) (S0.a__U41 (S0.a__and (S0.a__isPalListKind (V0 0)) (S0.isPalListKind (V0 1))) (V0 0) (V0 1)) :: R0 (S0.a__isNeList (S0.__ (V0 0) (V0 1))) (S0.a__U51 (S0.a__and (S0.a__isPalListKind (V0 0)) (S0.isPalListKind (V0 1))) (V0 0) (V0 1)) :: R0 (S0.a__isNePal (V0 0)) (S0.a__U61 (S0.a__isPalListKind (V0 0)) (V0 0)) :: R0 (S0.a__isNePal (S0.__ (V0 0) (S0.__ (V0 1) (V0 0)))) (S0.a__and (S0.a__and (S0.a__isQid (V0 0)) (S0.isPalListKind (V0 0))) (S0.and (S0.isPal (V0 1)) (S0.isPalListKind (V0 1)))) :: R0 (S0.a__isPal (V0 0)) (S0.a__U71 (S0.a__isPalListKind (V0 0)) (V0 0)) :: R0 (S0.a__isPal S0.nil) S0.tt :: R0 (S0.a__isPalListKind S0.a) S0.tt :: R0 (S0.a__isPalListKind S0.e) S0.tt :: R0 (S0.a__isPalListKind S0.i) S0.tt :: R0 (S0.a__isPalListKind S0.nil) S0.tt :: R0 (S0.a__isPalListKind S0.o) S0.tt :: R0 (S0.a__isPalListKind S0.u) S0.tt :: R0 (S0.a__isPalListKind (S0.__ (V0 0) (V0 1))) (S0.a__and (S0.a__isPalListKind (V0 0)) (S0.isPalListKind (V0 1))) :: R0 (S0.a__isQid S0.a) S0.tt :: R0 (S0.a__isQid S0.e) S0.tt :: R0 (S0.a__isQid S0.i) S0.tt :: R0 (S0.a__isQid S0.o) S0.tt :: R0 (S0.a__isQid S0.u) S0.tt :: R0 (S0.mark (S0.__ (V0 0) (V0 1))) (S0.a____ (S0.mark (V0 0)) (S0.mark (V0 1))) :: R0 (S0.mark (S0.U11 (V0 0) (V0 1))) (S0.a__U11 (S0.mark (V0 0)) (V0 1)) :: R0 (S0.mark (S0.U12 (V0 0))) (S0.a__U12 (S0.mark (V0 0))) :: R0 (S0.mark (S0.isNeList (V0 0))) (S0.a__isNeList (V0 0)) :: R0 (S0.mark (S0.U21 (V0 0) (V0 1) (V0 2))) (S0.a__U21 (S0.mark (V0 0)) (V0 1) (V0 2)) :: R0 (S0.mark (S0.U22 (V0 0) (V0 1))) (S0.a__U22 (S0.mark (V0 0)) (V0 1)) :: R0 (S0.mark (S0.isList (V0 0))) (S0.a__isList (V0 0)) :: R0 (S0.mark (S0.U23 (V0 0))) (S0.a__U23 (S0.mark (V0 0))) :: R0 (S0.mark (S0.U31 (V0 0) (V0 1))) (S0.a__U31 (S0.mark (V0 0)) (V0 1)) :: R0 (S0.mark (S0.U32 (V0 0))) (S0.a__U32 (S0.mark (V0 0))) :: R0 (S0.mark (S0.isQid (V0 0))) (S0.a__isQid (V0 0)) :: R0 (S0.mark (S0.U41 (V0 0) (V0 1) (V0 2))) (S0.a__U41 (S0.mark (V0 0)) (V0 1) (V0 2)) :: R0 (S0.mark (S0.U42 (V0 0) (V0 1))) (S0.a__U42 (S0.mark (V0 0)) (V0 1)) :: R0 (S0.mark (S0.U43 (V0 0))) (S0.a__U43 (S0.mark (V0 0))) :: R0 (S0.mark (S0.U51 (V0 0) (V0 1) (V0 2))) (S0.a__U51 (S0.mark (V0 0)) (V0 1) (V0 2)) :: R0 (S0.mark (S0.U52 (V0 0) (V0 1))) (S0.a__U52 (S0.mark (V0 0)) (V0 1)) :: R0 (S0.mark (S0.U53 (V0 0))) (S0.a__U53 (S0.mark (V0 0))) :: R0 (S0.mark (S0.U61 (V0 0) (V0 1))) (S0.a__U61 (S0.mark (V0 0)) (V0 1)) :: R0 (S0.mark (S0.U62 (V0 0))) (S0.a__U62 (S0.mark (V0 0))) :: R0 (S0.mark (S0.U71 (V0 0) (V0 1))) (S0.a__U71 (S0.mark (V0 0)) (V0 1)) :: R0 (S0.mark (S0.U72 (V0 0))) (S0.a__U72 (S0.mark (V0 0))) :: R0 (S0.mark (S0.isNePal (V0 0))) (S0.a__isNePal (V0 0)) :: R0 (S0.mark (S0.and (V0 0) (V0 1))) (S0.a__and (S0.mark (V0 0)) (V0 1)) :: R0 (S0.mark (S0.isPalListKind (V0 0))) (S0.a__isPalListKind (V0 0)) :: R0 (S0.mark (S0.isPal (V0 0))) (S0.a__isPal (V0 0)) :: R0 (S0.mark S0.nil) S0.nil :: R0 (S0.mark S0.tt) S0.tt :: R0 (S0.mark S0.a) S0.a :: R0 (S0.mark S0.e) S0.e :: R0 (S0.mark S0.i) S0.i :: R0 (S0.mark S0.o) S0.o :: R0 (S0.mark S0.u) S0.u :: R0 (S0.a____ (V0 0) (V0 1)) (S0.__ (V0 0) (V0 1)) :: R0 (S0.a__U11 (V0 0) (V0 1)) (S0.U11 (V0 0) (V0 1)) :: R0 (S0.a__U12 (V0 0)) (S0.U12 (V0 0)) :: R0 (S0.a__isNeList (V0 0)) (S0.isNeList (V0 0)) :: R0 (S0.a__U21 (V0 0) (V0 1) (V0 2)) (S0.U21 (V0 0) (V0 1) (V0 2)) :: R0 (S0.a__U22 (V0 0) (V0 1)) (S0.U22 (V0 0) (V0 1)) :: R0 (S0.a__isList (V0 0)) (S0.isList (V0 0)) :: R0 (S0.a__U23 (V0 0)) (S0.U23 (V0 0)) :: R0 (S0.a__U31 (V0 0) (V0 1)) (S0.U31 (V0 0) (V0 1)) :: R0 (S0.a__U32 (V0 0)) (S0.U32 (V0 0)) :: R0 (S0.a__isQid (V0 0)) (S0.isQid (V0 0)) :: R0 (S0.a__U41 (V0 0) (V0 1) (V0 2)) (S0.U41 (V0 0) (V0 1) (V0 2)) :: R0 (S0.a__U42 (V0 0) (V0 1)) (S0.U42 (V0 0) (V0 1)) :: R0 (S0.a__U43 (V0 0)) (S0.U43 (V0 0)) :: R0 (S0.a__U51 (V0 0) (V0 1) (V0 2)) (S0.U51 (V0 0) (V0 1) (V0 2)) :: R0 (S0.a__U52 (V0 0) (V0 1)) (S0.U52 (V0 0) (V0 1)) :: R0 (S0.a__U53 (V0 0)) (S0.U53 (V0 0)) :: R0 (S0.a__U61 (V0 0) (V0 1)) (S0.U61 (V0 0) (V0 1)) :: R0 (S0.a__U62 (V0 0)) (S0.U62 (V0 0)) :: R0 (S0.a__U71 (V0 0) (V0 1)) (S0.U71 (V0 0) (V0 1)) :: R0 (S0.a__U72 (V0 0)) (S0.U72 (V0 0)) :: R0 (S0.a__isNePal (V0 0)) (S0.isNePal (V0 0)) :: R0 (S0.a__and (V0 0) (V0 1)) (S0.and (V0 0) (V0 1)) :: R0 (S0.a__isPalListKind (V0 0)) (S0.isPalListKind (V0 0)) :: R0 (S0.a__isPal (V0 0)) (S0.isPal (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 hU11 x2 x1 := F1 (hd_symb s1_p M.U11) (Vcons x2 (Vcons x1 Vnil)). Definition U11 x2 x1 := F1 (int_symb s1_p M.U11) (Vcons x2 (Vcons x1 Vnil)). Definition hU12 x1 := F1 (hd_symb s1_p M.U12) (Vcons x1 Vnil). Definition U12 x1 := F1 (int_symb s1_p M.U12) (Vcons x1 Vnil). Definition hU21 x3 x2 x1 := F1 (hd_symb s1_p M.U21) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition U21 x3 x2 x1 := F1 (int_symb s1_p M.U21) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition hU22 x2 x1 := F1 (hd_symb s1_p M.U22) (Vcons x2 (Vcons x1 Vnil)). Definition U22 x2 x1 := F1 (int_symb s1_p M.U22) (Vcons x2 (Vcons x1 Vnil)). Definition hU23 x1 := F1 (hd_symb s1_p M.U23) (Vcons x1 Vnil). Definition U23 x1 := F1 (int_symb s1_p M.U23) (Vcons x1 Vnil). Definition hU31 x2 x1 := F1 (hd_symb s1_p M.U31) (Vcons x2 (Vcons x1 Vnil)). Definition U31 x2 x1 := F1 (int_symb s1_p M.U31) (Vcons x2 (Vcons x1 Vnil)). Definition hU32 x1 := F1 (hd_symb s1_p M.U32) (Vcons x1 Vnil). Definition U32 x1 := F1 (int_symb s1_p M.U32) (Vcons x1 Vnil). Definition hU41 x3 x2 x1 := F1 (hd_symb s1_p M.U41) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition U41 x3 x2 x1 := F1 (int_symb s1_p M.U41) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition hU42 x2 x1 := F1 (hd_symb s1_p M.U42) (Vcons x2 (Vcons x1 Vnil)). Definition U42 x2 x1 := F1 (int_symb s1_p M.U42) (Vcons x2 (Vcons x1 Vnil)). Definition hU43 x1 := F1 (hd_symb s1_p M.U43) (Vcons x1 Vnil). Definition U43 x1 := F1 (int_symb s1_p M.U43) (Vcons x1 Vnil). Definition hU51 x3 x2 x1 := F1 (hd_symb s1_p M.U51) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition U51 x3 x2 x1 := F1 (int_symb s1_p M.U51) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition hU52 x2 x1 := F1 (hd_symb s1_p M.U52) (Vcons x2 (Vcons x1 Vnil)). Definition U52 x2 x1 := F1 (int_symb s1_p M.U52) (Vcons x2 (Vcons x1 Vnil)). Definition hU53 x1 := F1 (hd_symb s1_p M.U53) (Vcons x1 Vnil). Definition U53 x1 := F1 (int_symb s1_p M.U53) (Vcons x1 Vnil). Definition hU61 x2 x1 := F1 (hd_symb s1_p M.U61) (Vcons x2 (Vcons x1 Vnil)). Definition U61 x2 x1 := F1 (int_symb s1_p M.U61) (Vcons x2 (Vcons x1 Vnil)). Definition hU62 x1 := F1 (hd_symb s1_p M.U62) (Vcons x1 Vnil). Definition U62 x1 := F1 (int_symb s1_p M.U62) (Vcons x1 Vnil). Definition hU71 x2 x1 := F1 (hd_symb s1_p M.U71) (Vcons x2 (Vcons x1 Vnil)). Definition U71 x2 x1 := F1 (int_symb s1_p M.U71) (Vcons x2 (Vcons x1 Vnil)). Definition hU72 x1 := F1 (hd_symb s1_p M.U72) (Vcons x1 Vnil). Definition U72 x1 := F1 (int_symb s1_p M.U72) (Vcons x1 Vnil). 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 ha__U11 x2 x1 := F1 (hd_symb s1_p M.a__U11) (Vcons x2 (Vcons x1 Vnil)). Definition a__U11 x2 x1 := F1 (int_symb s1_p M.a__U11) (Vcons x2 (Vcons x1 Vnil)). Definition ha__U12 x1 := F1 (hd_symb s1_p M.a__U12) (Vcons x1 Vnil). Definition a__U12 x1 := F1 (int_symb s1_p M.a__U12) (Vcons x1 Vnil). Definition ha__U21 x3 x2 x1 := F1 (hd_symb s1_p M.a__U21) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition a__U21 x3 x2 x1 := F1 (int_symb s1_p M.a__U21) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition ha__U22 x2 x1 := F1 (hd_symb s1_p M.a__U22) (Vcons x2 (Vcons x1 Vnil)). Definition a__U22 x2 x1 := F1 (int_symb s1_p M.a__U22) (Vcons x2 (Vcons x1 Vnil)). Definition ha__U23 x1 := F1 (hd_symb s1_p M.a__U23) (Vcons x1 Vnil). Definition a__U23 x1 := F1 (int_symb s1_p M.a__U23) (Vcons x1 Vnil). Definition ha__U31 x2 x1 := F1 (hd_symb s1_p M.a__U31) (Vcons x2 (Vcons x1 Vnil)). Definition a__U31 x2 x1 := F1 (int_symb s1_p M.a__U31) (Vcons x2 (Vcons x1 Vnil)). Definition ha__U32 x1 := F1 (hd_symb s1_p M.a__U32) (Vcons x1 Vnil). Definition a__U32 x1 := F1 (int_symb s1_p M.a__U32) (Vcons x1 Vnil). Definition ha__U41 x3 x2 x1 := F1 (hd_symb s1_p M.a__U41) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition a__U41 x3 x2 x1 := F1 (int_symb s1_p M.a__U41) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition ha__U42 x2 x1 := F1 (hd_symb s1_p M.a__U42) (Vcons x2 (Vcons x1 Vnil)). Definition a__U42 x2 x1 := F1 (int_symb s1_p M.a__U42) (Vcons x2 (Vcons x1 Vnil)). Definition ha__U43 x1 := F1 (hd_symb s1_p M.a__U43) (Vcons x1 Vnil). Definition a__U43 x1 := F1 (int_symb s1_p M.a__U43) (Vcons x1 Vnil). Definition ha__U51 x3 x2 x1 := F1 (hd_symb s1_p M.a__U51) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition a__U51 x3 x2 x1 := F1 (int_symb s1_p M.a__U51) (Vcons x3 (Vcons x2 (Vcons x1 Vnil))). Definition ha__U52 x2 x1 := F1 (hd_symb s1_p M.a__U52) (Vcons x2 (Vcons x1 Vnil)). Definition a__U52 x2 x1 := F1 (int_symb s1_p M.a__U52) (Vcons x2 (Vcons x1 Vnil)). Definition ha__U53 x1 := F1 (hd_symb s1_p M.a__U53) (Vcons x1 Vnil). Definition a__U53 x1 := F1 (int_symb s1_p M.a__U53) (Vcons x1 Vnil). Definition ha__U61 x2 x1 := F1 (hd_symb s1_p M.a__U61) (Vcons x2 (Vcons x1 Vnil)). Definition a__U61 x2 x1 := F1 (int_symb s1_p M.a__U61) (Vcons x2 (Vcons x1 Vnil)). Definition ha__U62 x1 := F1 (hd_symb s1_p M.a__U62) (Vcons x1 Vnil). Definition a__U62 x1 := F1 (int_symb s1_p M.a__U62) (Vcons x1 Vnil). Definition ha__U71 x2 x1 := F1 (hd_symb s1_p M.a__U71) (Vcons x2 (Vcons x1 Vnil)). Definition a__U71 x2 x1 := F1 (int_symb s1_p M.a__U71) (Vcons x2 (Vcons x1 Vnil)). Definition ha__U72 x1 := F1 (hd_symb s1_p M.a__U72) (Vcons x1 Vnil). Definition a__U72 x1 := F1 (int_symb s1_p M.a__U72) (Vcons x1 Vnil). Definition ha____ x2 x1 := F1 (hd_symb s1_p M.a____) (Vcons x2 (Vcons x1 Vnil)). Definition a____ x2 x1 := F1 (int_symb s1_p M.a____) (Vcons x2 (Vcons x1 Vnil)). Definition ha__and x2 x1 := F1 (hd_symb s1_p M.a__and) (Vcons x2 (Vcons x1 Vnil)). Definition a__and x2 x1 := F1 (int_symb s1_p M.a__and) (Vcons x2 (Vcons x1 Vnil)). Definition ha__isList x1 := F1 (hd_symb s1_p M.a__isList) (Vcons x1 Vnil). Definition a__isList x1 := F1 (int_symb s1_p M.a__isList) (Vcons x1 Vnil). Definition ha__isNeList x1 := F1 (hd_symb s1_p M.a__isNeList) (Vcons x1 Vnil). Definition a__isNeList x1 := F1 (int_symb s1_p M.a__isNeList) (Vcons x1 Vnil). Definition ha__isNePal x1 := F1 (hd_symb s1_p M.a__isNePal) (Vcons x1 Vnil). Definition a__isNePal x1 := F1 (int_symb s1_p M.a__isNePal) (Vcons x1 Vnil). Definition ha__isPal x1 := F1 (hd_symb s1_p M.a__isPal) (Vcons x1 Vnil). Definition a__isPal x1 := F1 (int_symb s1_p M.a__isPal) (Vcons x1 Vnil). Definition ha__isPalListKind x1 := F1 (hd_symb s1_p M.a__isPalListKind) (Vcons x1 Vnil). Definition a__isPalListKind x1 := F1 (int_symb s1_p M.a__isPalListKind) (Vcons x1 Vnil). Definition ha__isQid x1 := F1 (hd_symb s1_p M.a__isQid) (Vcons x1 Vnil). Definition a__isQid x1 := F1 (int_symb s1_p M.a__isQid) (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 hisPalListKind x1 := F1 (hd_symb s1_p M.isPalListKind) (Vcons x1 Vnil). Definition isPalListKind x1 := F1 (int_symb s1_p M.isPalListKind) (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 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 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.hmark (S1.U72 (V1 0))) (S1.ha__U72 (S1.mark (V1 0))) :: nil) :: ( R1 (S1.hmark (S1.U62 (V1 0))) (S1.ha__U62 (S1.mark (V1 0))) :: nil) :: ( R1 (S1.hmark (S1.U53 (V1 0))) (S1.ha__U53 (S1.mark (V1 0))) :: nil) :: ( R1 (S1.hmark (S1.U43 (V1 0))) (S1.ha__U43 (S1.mark (V1 0))) :: nil) :: ( R1 (S1.hmark (S1.isQid (V1 0))) (S1.ha__isQid (V1 0)) :: nil) :: ( R1 (S1.hmark (S1.U32 (V1 0))) (S1.ha__U32 (S1.mark (V1 0))) :: nil) :: ( R1 (S1.hmark (S1.U23 (V1 0))) (S1.ha__U23 (S1.mark (V1 0))) :: nil) :: ( R1 (S1.hmark (S1.U12 (V1 0))) (S1.ha__U12 (S1.mark (V1 0))) :: nil) :: ( R1 (S1.ha__isNePal (S1.__ (V1 0) (S1.__ (V1 1) (V1 0)))) (S1.ha__isQid (V1 0)) :: nil) :: ( R1 (S1.ha__U71 (S1.tt) (V1 0)) (S1.ha__U72 (S1.a__isNePal (V1 0))) :: nil) :: ( R1 (S1.ha__U61 (S1.tt) (V1 0)) (S1.ha__isQid (V1 0)) :: nil) :: ( R1 (S1.ha__U61 (S1.tt) (V1 0)) (S1.ha__U62 (S1.a__isQid (V1 0))) :: nil) :: ( R1 (S1.hmark (S1.U61 (V1 0) (V1 1))) (S1.ha__U61 (S1.mark (V1 0)) (V1 1)) :: nil) :: ( R1 (S1.ha__isNePal (V1 0)) (S1.ha__U61 (S1.a__isPalListKind (V1 0)) (V1 0)) :: nil) :: ( R1 (S1.ha__U52 (S1.tt) (V1 0)) (S1.ha__U53 (S1.a__isList (V1 0))) :: nil) :: ( R1 (S1.ha__U42 (S1.tt) (V1 0)) (S1.ha__U43 (S1.a__isNeList (V1 0))) :: nil) :: ( R1 (S1.ha__U31 (S1.tt) (V1 0)) (S1.ha__isQid (V1 0)) :: nil) :: ( R1 (S1.ha__U31 (S1.tt) (V1 0)) (S1.ha__U32 (S1.a__isQid (V1 0))) :: nil) :: ( R1 (S1.hmark (S1.U31 (V1 0) (V1 1))) (S1.ha__U31 (S1.mark (V1 0)) (V1 1)) :: nil) :: ( R1 (S1.ha__isNeList (V1 0)) (S1.ha__U31 (S1.a__isPalListKind (V1 0)) (V1 0)) :: nil) :: ( R1 (S1.ha__U22 (S1.tt) (V1 0)) (S1.ha__U23 (S1.a__isList (V1 0))) :: nil) :: ( R1 (S1.ha__U11 (S1.tt) (V1 0)) (S1.ha__U12 (S1.a__isNeList (V1 0))) :: nil) :: ( R1 (S1.ha____ (S1.__ (V1 0) (V1 1)) (V1 2)) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.__ (V1 0) (V1 1))) (S1.ha____ (S1.mark (V1 0)) (S1.mark (V1 1))) :: R1 (S1.ha____ (S1.__ (V1 0) (V1 1)) (V1 2)) (S1.ha____ (S1.mark (V1 0)) (S1.a____ (S1.mark (V1 1)) (S1.mark (V1 2)))) :: R1 (S1.ha____ (S1.__ (V1 0) (V1 1)) (V1 2)) (S1.ha____ (S1.mark (V1 1)) (S1.mark (V1 2))) :: R1 (S1.ha____ (S1.__ (V1 0) (V1 1)) (V1 2)) (S1.hmark (V1 1)) :: R1 (S1.hmark (S1.__ (V1 0) (V1 1))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.__ (V1 0) (V1 1))) (S1.hmark (V1 1)) :: R1 (S1.hmark (S1.U11 (V1 0) (V1 1))) (S1.ha__U11 (S1.mark (V1 0)) (V1 1)) :: R1 (S1.ha__U11 (S1.tt) (V1 0)) (S1.ha__isNeList (V1 0)) :: R1 (S1.ha__isNeList (V1 0)) (S1.ha__isPalListKind (V1 0)) :: R1 (S1.ha__isPalListKind (S1.__ (V1 0) (V1 1))) (S1.ha__and (S1.a__isPalListKind (V1 0)) (S1.isPalListKind (V1 1))) :: R1 (S1.ha__and (S1.tt) (V1 0)) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U11 (V1 0) (V1 1))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U12 (V1 0))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.isNeList (V1 0))) (S1.ha__isNeList (V1 0)) :: R1 (S1.ha__isNeList (S1.__ (V1 0) (V1 1))) (S1.ha__U41 (S1.a__and (S1.a__isPalListKind (V1 0)) (S1.isPalListKind (V1 1))) (V1 0) (V1 1)) :: R1 (S1.ha__U41 (S1.tt) (V1 0) (V1 1)) (S1.ha__U42 (S1.a__isList (V1 0)) (V1 1)) :: R1 (S1.ha__U42 (S1.tt) (V1 0)) (S1.ha__isNeList (V1 0)) :: R1 (S1.ha__isNeList (S1.__ (V1 0) (V1 1))) (S1.ha__and (S1.a__isPalListKind (V1 0)) (S1.isPalListKind (V1 1))) :: R1 (S1.ha__isNeList (S1.__ (V1 0) (V1 1))) (S1.ha__isPalListKind (V1 0)) :: R1 (S1.ha__isPalListKind (S1.__ (V1 0) (V1 1))) (S1.ha__isPalListKind (V1 0)) :: R1 (S1.ha__isNeList (S1.__ (V1 0) (V1 1))) (S1.ha__U51 (S1.a__and (S1.a__isPalListKind (V1 0)) (S1.isPalListKind (V1 1))) (V1 0) (V1 1)) :: R1 (S1.ha__U51 (S1.tt) (V1 0) (V1 1)) (S1.ha__U52 (S1.a__isNeList (V1 0)) (V1 1)) :: R1 (S1.ha__U52 (S1.tt) (V1 0)) (S1.ha__isList (V1 0)) :: R1 (S1.ha__isList (V1 0)) (S1.ha__U11 (S1.a__isPalListKind (V1 0)) (V1 0)) :: R1 (S1.ha__isList (V1 0)) (S1.ha__isPalListKind (V1 0)) :: R1 (S1.ha__isList (S1.__ (V1 0) (V1 1))) (S1.ha__U21 (S1.a__and (S1.a__isPalListKind (V1 0)) (S1.isPalListKind (V1 1))) (V1 0) (V1 1)) :: R1 (S1.ha__U21 (S1.tt) (V1 0) (V1 1)) (S1.ha__U22 (S1.a__isList (V1 0)) (V1 1)) :: R1 (S1.ha__U22 (S1.tt) (V1 0)) (S1.ha__isList (V1 0)) :: R1 (S1.ha__isList (S1.__ (V1 0) (V1 1))) (S1.ha__and (S1.a__isPalListKind (V1 0)) (S1.isPalListKind (V1 1))) :: R1 (S1.ha__isList (S1.__ (V1 0) (V1 1))) (S1.ha__isPalListKind (V1 0)) :: R1 (S1.ha__U21 (S1.tt) (V1 0) (V1 1)) (S1.ha__isList (V1 0)) :: R1 (S1.ha__U51 (S1.tt) (V1 0) (V1 1)) (S1.ha__isNeList (V1 0)) :: R1 (S1.ha__U41 (S1.tt) (V1 0) (V1 1)) (S1.ha__isList (V1 0)) :: R1 (S1.hmark (S1.U21 (V1 0) (V1 1) (V1 2))) (S1.ha__U21 (S1.mark (V1 0)) (V1 1) (V1 2)) :: R1 (S1.hmark (S1.U21 (V1 0) (V1 1) (V1 2))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U22 (V1 0) (V1 1))) (S1.ha__U22 (S1.mark (V1 0)) (V1 1)) :: R1 (S1.hmark (S1.U22 (V1 0) (V1 1))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.isList (V1 0))) (S1.ha__isList (V1 0)) :: R1 (S1.hmark (S1.U23 (V1 0))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U31 (V1 0) (V1 1))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U32 (V1 0))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U41 (V1 0) (V1 1) (V1 2))) (S1.ha__U41 (S1.mark (V1 0)) (V1 1) (V1 2)) :: R1 (S1.hmark (S1.U41 (V1 0) (V1 1) (V1 2))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U42 (V1 0) (V1 1))) (S1.ha__U42 (S1.mark (V1 0)) (V1 1)) :: R1 (S1.hmark (S1.U42 (V1 0) (V1 1))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U43 (V1 0))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U51 (V1 0) (V1 1) (V1 2))) (S1.ha__U51 (S1.mark (V1 0)) (V1 1) (V1 2)) :: R1 (S1.hmark (S1.U51 (V1 0) (V1 1) (V1 2))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U52 (V1 0) (V1 1))) (S1.ha__U52 (S1.mark (V1 0)) (V1 1)) :: R1 (S1.hmark (S1.U52 (V1 0) (V1 1))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U53 (V1 0))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U61 (V1 0) (V1 1))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U62 (V1 0))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U71 (V1 0) (V1 1))) (S1.ha__U71 (S1.mark (V1 0)) (V1 1)) :: R1 (S1.ha__U71 (S1.tt) (V1 0)) (S1.ha__isNePal (V1 0)) :: R1 (S1.ha__isNePal (V1 0)) (S1.ha__isPalListKind (V1 0)) :: R1 (S1.ha__isNePal (S1.__ (V1 0) (S1.__ (V1 1) (V1 0)))) (S1.ha__and (S1.a__and (S1.a__isQid (V1 0)) (S1.isPalListKind (V1 0))) (S1.and (S1.isPal (V1 1)) (S1.isPalListKind (V1 1)))) :: R1 (S1.ha__isNePal (S1.__ (V1 0) (S1.__ (V1 1) (V1 0)))) (S1.ha__and (S1.a__isQid (V1 0)) (S1.isPalListKind (V1 0))) :: R1 (S1.hmark (S1.U71 (V1 0) (V1 1))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U72 (V1 0))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.isNePal (V1 0))) (S1.ha__isNePal (V1 0)) :: R1 (S1.hmark (S1.and (V1 0) (V1 1))) (S1.ha__and (S1.mark (V1 0)) (V1 1)) :: R1 (S1.hmark (S1.and (V1 0) (V1 1))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.isPalListKind (V1 0))) (S1.ha__isPalListKind (V1 0)) :: R1 (S1.hmark (S1.isPal (V1 0))) (S1.ha__isPal (V1 0)) :: R1 (S1.ha__isPal (V1 0)) (S1.ha__U71 (S1.a__isPalListKind (V1 0)) (V1 0)) :: R1 (S1.ha__isPal (V1 0)) (S1.ha__isPalListKind (V1 0)) :: R1 (S1.ha____ (S1.__ (V1 0) (V1 1)) (V1 2)) (S1.hmark (V1 2)) :: R1 (S1.ha____ (V1 0) (S1.nil)) (S1.hmark (V1 0)) :: R1 (S1.ha____ (S1.nil) (V1 0)) (S1.hmark (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.a____) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a____) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.__) => nil | (int_symb M.__) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.mark) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: 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.a__U11) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (int_symb M.a__U11) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.tt) => nil | (int_symb M.tt) => nil | (hd_symb M.a__U12) => nil | (int_symb M.a__U12) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__isNeList) => (1%Z, (Vcons 0 Vnil)) :: nil | (int_symb M.a__isNeList) => nil | (hd_symb M.a__U21) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (int_symb M.a__U21) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.a__U22) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (int_symb M.a__U22) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__isList) => (1%Z, (Vcons 0 Vnil)) :: nil | (int_symb M.a__isList) => nil | (hd_symb M.a__U23) => nil | (int_symb M.a__U23) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U31) => nil | (int_symb M.a__U31) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U32) => nil | (int_symb M.a__U32) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__isQid) => nil | (int_symb M.a__isQid) => nil | (hd_symb M.a__U41) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (int_symb M.a__U41) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.a__U42) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (int_symb M.a__U42) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U43) => nil | (int_symb M.a__U43) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U51) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (int_symb M.a__U51) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.a__U52) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (int_symb M.a__U52) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U53) => nil | (int_symb M.a__U53) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U61) => nil | (int_symb M.a__U61) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U62) => nil | (int_symb M.a__U62) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U71) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (int_symb M.a__U71) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U72) => nil | (int_symb M.a__U72) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__isNePal) => (1%Z, (Vcons 0 Vnil)) :: nil | (int_symb M.a__isNePal) => nil | (hd_symb M.a__and) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a__and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__isPalListKind) => (1%Z, (Vcons 0 Vnil)) :: nil | (int_symb M.a__isPalListKind) => nil | (hd_symb M.isPalListKind) => nil | (int_symb M.isPalListKind) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.isPal) => nil | (int_symb M.isPal) => nil | (hd_symb M.a__isPal) => (1%Z, (Vcons 0 Vnil)) :: nil | (int_symb M.a__isPal) => 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) => (3%Z, Vnil) :: nil | (hd_symb M.o) => nil | (int_symb M.o) => (1%Z, Vnil) :: nil | (hd_symb M.u) => nil | (int_symb M.u) => nil | (hd_symb M.U11) => nil | (int_symb M.U11) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U12) => nil | (int_symb M.U12) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isNeList) => nil | (int_symb M.isNeList) => nil | (hd_symb M.U21) => nil | (int_symb M.U21) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.U22) => nil | (int_symb M.U22) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.isList) => nil | (int_symb M.isList) => nil | (hd_symb M.U23) => nil | (int_symb M.U23) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U31) => nil | (int_symb M.U31) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U32) => nil | (int_symb M.U32) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isQid) => nil | (int_symb M.isQid) => nil | (hd_symb M.U41) => nil | (int_symb M.U41) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.U42) => nil | (int_symb M.U42) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U43) => nil | (int_symb M.U43) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U51) => nil | (int_symb M.U51) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.U52) => nil | (int_symb M.U52) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U53) => nil | (int_symb M.U53) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U61) => nil | (int_symb M.U61) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U62) => nil | (int_symb M.U62) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U71) => nil | (int_symb M.U71) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U72) => nil | (int_symb M.U72) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isNePal) => nil | (int_symb M.isNePal) => 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.a____) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a____) => (2%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 | (int_symb M.__) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.mark) => (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.mark) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.a__U11) => nil | (int_symb M.a__U11) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.tt) => nil | (int_symb M.tt) => nil | (hd_symb M.a__U12) => nil | (int_symb M.a__U12) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__isNeList) => nil | (int_symb M.a__isNeList) => nil | (hd_symb M.a__U21) => nil | (int_symb M.a__U21) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.a__U22) => nil | (int_symb M.a__U22) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__isList) => nil | (int_symb M.a__isList) => nil | (hd_symb M.a__U23) => nil | (int_symb M.a__U23) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U31) => nil | (int_symb M.a__U31) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U32) => nil | (int_symb M.a__U32) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__isQid) => nil | (int_symb M.a__isQid) => nil | (hd_symb M.a__U41) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (int_symb M.a__U41) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.a__U42) => nil | (int_symb M.a__U42) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U43) => nil | (int_symb M.a__U43) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U51) => nil | (int_symb M.a__U51) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.a__U52) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (int_symb M.a__U52) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U53) => nil | (int_symb M.a__U53) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U61) => nil | (int_symb M.a__U61) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U62) => nil | (int_symb M.a__U62) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U71) => nil | (int_symb M.a__U71) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U72) => nil | (int_symb M.a__U72) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__isNePal) => nil | (int_symb M.a__isNePal) => nil | (hd_symb M.a__and) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a__and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__isPalListKind) => nil | (int_symb M.a__isPalListKind) => nil | (hd_symb M.isPalListKind) => nil | (int_symb M.isPalListKind) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.isPal) => nil | (int_symb M.isPal) => nil | (hd_symb M.a__isPal) => nil | (int_symb M.a__isPal) => 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) => (1%Z, Vnil) :: nil | (hd_symb M.U11) => nil | (int_symb M.U11) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U12) => nil | (int_symb M.U12) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isNeList) => nil | (int_symb M.isNeList) => nil | (hd_symb M.U21) => nil | (int_symb M.U21) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.U22) => nil | (int_symb M.U22) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.isList) => nil | (int_symb M.isList) => nil | (hd_symb M.U23) => nil | (int_symb M.U23) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U31) => nil | (int_symb M.U31) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U32) => nil | (int_symb M.U32) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isQid) => nil | (int_symb M.isQid) => nil | (hd_symb M.U41) => nil | (int_symb M.U41) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.U42) => nil | (int_symb M.U42) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U43) => nil | (int_symb M.U43) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U51) => nil | (int_symb M.U51) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.U52) => nil | (int_symb M.U52) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U53) => nil | (int_symb M.U53) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U61) => nil | (int_symb M.U61) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U62) => nil | (int_symb M.U62) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U71) => nil | (int_symb M.U71) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U72) => nil | (int_symb M.U72) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isNePal) => nil | (int_symb M.isNePal) => 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.a____) => nil | (int_symb M.a____) => (2%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 | (int_symb M.__) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.mark) => (2%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.mark) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => (1%Z, Vnil) :: nil | (hd_symb M.a__U11) => nil | (int_symb M.a__U11) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.tt) => nil | (int_symb M.tt) => nil | (hd_symb M.a__U12) => nil | (int_symb M.a__U12) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__isNeList) => nil | (int_symb M.a__isNeList) => nil | (hd_symb M.a__U21) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (int_symb M.a__U21) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.a__U22) => nil | (int_symb M.a__U22) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__isList) => nil | (int_symb M.a__isList) => nil | (hd_symb M.a__U23) => nil | (int_symb M.a__U23) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U31) => nil | (int_symb M.a__U31) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U32) => nil | (int_symb M.a__U32) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__isQid) => nil | (int_symb M.a__isQid) => nil | (hd_symb M.a__U41) => nil | (int_symb M.a__U41) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.a__U42) => nil | (int_symb M.a__U42) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U43) => nil | (int_symb M.a__U43) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U51) => nil | (int_symb M.a__U51) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.a__U52) => nil | (int_symb M.a__U52) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U53) => nil | (int_symb M.a__U53) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U61) => nil | (int_symb M.a__U61) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__U62) => nil | (int_symb M.a__U62) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U71) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a__U71) => (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.a__U72) => nil | (int_symb M.a__U72) => (2%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__isNePal) => (2%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.a__isNePal) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__and) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a__and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__isPalListKind) => nil | (int_symb M.a__isPalListKind) => nil | (hd_symb M.isPalListKind) => nil | (int_symb M.isPalListKind) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.isPal) => nil | (int_symb M.isPal) => (2%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__isPal) => (3%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.a__isPal) => (2%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: 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) => (1%Z, Vnil) :: nil | (hd_symb M.o) => nil | (int_symb M.o) => nil | (hd_symb M.u) => nil | (int_symb M.u) => nil | (hd_symb M.U11) => nil | (int_symb M.U11) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U12) => nil | (int_symb M.U12) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isNeList) => nil | (int_symb M.isNeList) => nil | (hd_symb M.U21) => nil | (int_symb M.U21) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.U22) => nil | (int_symb M.U22) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.isList) => nil | (int_symb M.isList) => nil | (hd_symb M.U23) => nil | (int_symb M.U23) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U31) => nil | (int_symb M.U31) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U32) => nil | (int_symb M.U32) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isQid) => nil | (int_symb M.isQid) => nil | (hd_symb M.U41) => nil | (int_symb M.U41) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.U42) => nil | (int_symb M.U42) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U43) => nil | (int_symb M.U43) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U51) => nil | (int_symb M.U51) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.U52) => nil | (int_symb M.U52) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U53) => nil | (int_symb M.U53) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U61) => nil | (int_symb M.U61) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.U62) => nil | (int_symb M.U62) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U71) => nil | (int_symb M.U71) => (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.U72) => nil | (int_symb M.U72) => (2%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isNePal) => nil | (int_symb M.isNePal) => (1%Z, (Vcons 1 Vnil)) :: 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.a____) => nil | (int_symb M.a____) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.__) => nil | (int_symb M.__) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.mark) => (1%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.mark) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.a__U11) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (int_symb M.a__U11) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.tt) => nil | (int_symb M.tt) => nil | (hd_symb M.a__U12) => nil | (int_symb M.a__U12) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__isNeList) => (1%Z, (Vcons 0 Vnil)) :: nil | (int_symb M.a__isNeList) => nil | (hd_symb M.a__U21) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (int_symb M.a__U21) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.a__U22) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (int_symb M.a__U22) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__isList) => (1%Z, (Vcons 0 Vnil)) :: nil | (int_symb M.a__isList) => nil | (hd_symb M.a__U23) => nil | (int_symb M.a__U23) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U31) => nil | (int_symb M.a__U31) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U32) => nil | (int_symb M.a__U32) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__isQid) => nil | (int_symb M.a__isQid) => nil | (hd_symb M.a__U41) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (int_symb M.a__U41) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.a__U42) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (int_symb M.a__U42) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U43) => nil | (int_symb M.a__U43) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U51) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (int_symb M.a__U51) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.a__U52) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (int_symb M.a__U52) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U53) => nil | (int_symb M.a__U53) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U61) => nil | (int_symb M.a__U61) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U62) => nil | (int_symb M.a__U62) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U71) => nil | (int_symb M.a__U71) => nil | (hd_symb M.a__U72) => nil | (int_symb M.a__U72) => nil | (hd_symb M.a__isNePal) => (2%Z, (Vcons 0 Vnil)) :: nil | (int_symb M.a__isNePal) => (1%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M.a__and) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a__and) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__isPalListKind) => (1%Z, (Vcons 0 Vnil)) :: nil | (int_symb M.a__isPalListKind) => nil | (hd_symb M.isPalListKind) => nil | (int_symb M.isPalListKind) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.isPal) => nil | (int_symb M.isPal) => nil | (hd_symb M.a__isPal) => nil | (int_symb M.a__isPal) => 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) => (3%Z, Vnil) :: nil | (hd_symb M.o) => nil | (int_symb M.o) => nil | (hd_symb M.u) => nil | (int_symb M.u) => nil | (hd_symb M.U11) => nil | (int_symb M.U11) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U12) => nil | (int_symb M.U12) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isNeList) => nil | (int_symb M.isNeList) => nil | (hd_symb M.U21) => nil | (int_symb M.U21) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.U22) => nil | (int_symb M.U22) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.isList) => nil | (int_symb M.isList) => nil | (hd_symb M.U23) => nil | (int_symb M.U23) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U31) => nil | (int_symb M.U31) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U32) => nil | (int_symb M.U32) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isQid) => nil | (int_symb M.isQid) => nil | (hd_symb M.U41) => nil | (int_symb M.U41) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.U42) => nil | (int_symb M.U42) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U43) => nil | (int_symb M.U43) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U51) => nil | (int_symb M.U51) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.U52) => nil | (int_symb M.U52) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U53) => nil | (int_symb M.U53) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U61) => nil | (int_symb M.U61) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U62) => nil | (int_symb M.U62) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U71) => nil | (int_symb M.U71) => nil | (hd_symb M.U72) => nil | (int_symb M.U72) => nil | (hd_symb M.isNePal) => nil | (int_symb M.isNePal) => (1%Z, (Vcons 0 Vnil)) :: 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.a____) => nil | (int_symb M.a____) => (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 | (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.mark) => (2%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.mark) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.a__U11) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a__U11) => (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.a__U12) => nil | (int_symb M.a__U12) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__isNeList) => (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.a__isNeList) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U21) => (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (int_symb M.a__U21) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.a__U22) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a__U22) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__isList) => (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.a__isList) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U23) => nil | (int_symb M.a__U23) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U31) => nil | (int_symb M.a__U31) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U32) => nil | (int_symb M.a__U32) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__isQid) => nil | (int_symb M.a__isQid) => nil | (hd_symb M.a__U41) => (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (int_symb M.a__U41) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.a__U42) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a__U42) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__U43) => nil | (int_symb M.a__U43) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U51) => (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (int_symb M.a__U51) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.a__U52) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a__U52) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__U53) => nil | (int_symb M.a__U53) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U61) => nil | (int_symb M.a__U61) => nil | (hd_symb M.a__U62) => nil | (int_symb M.a__U62) => nil | (hd_symb M.a__U71) => nil | (int_symb M.a__U71) => nil | (hd_symb M.a__U72) => nil | (int_symb M.a__U72) => nil | (hd_symb M.a__isNePal) => nil | (int_symb M.a__isNePal) => nil | (hd_symb M.a__and) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a__and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__isPalListKind) => nil | (int_symb M.a__isPalListKind) => nil | (hd_symb M.isPalListKind) => nil | (int_symb M.isPalListKind) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.isPal) => nil | (int_symb M.isPal) => nil | (hd_symb M.a__isPal) => nil | (int_symb M.a__isPal) => 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) => (1%Z, Vnil) :: nil | (hd_symb M.u) => nil | (int_symb M.u) => nil | (hd_symb M.U11) => nil | (int_symb M.U11) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.U12) => nil | (int_symb M.U12) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isNeList) => nil | (int_symb M.isNeList) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U21) => nil | (int_symb M.U21) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.U22) => nil | (int_symb M.U22) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.isList) => nil | (int_symb M.isList) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U23) => nil | (int_symb M.U23) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U31) => nil | (int_symb M.U31) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U32) => nil | (int_symb M.U32) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isQid) => nil | (int_symb M.isQid) => nil | (hd_symb M.U41) => nil | (int_symb M.U41) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.U42) => nil | (int_symb M.U42) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.U43) => nil | (int_symb M.U43) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U51) => nil | (int_symb M.U51) => (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.U52) => nil | (int_symb M.U52) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.U53) => nil | (int_symb M.U53) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U61) => nil | (int_symb M.U61) => nil | (hd_symb M.U62) => nil | (int_symb M.U62) => nil | (hd_symb M.U71) => nil | (int_symb M.U71) => nil | (hd_symb M.U72) => nil | (int_symb M.U72) => nil | (hd_symb M.isNePal) => nil | (int_symb M.isNePal) => 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.a____) => nil | (int_symb M.a____) => (2%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 | (int_symb M.__) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.mark) => (2%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.mark) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.a__U11) => nil | (int_symb M.a__U11) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.tt) => nil | (int_symb M.tt) => nil | (hd_symb M.a__U12) => nil | (int_symb M.a__U12) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__isNeList) => nil | (int_symb M.a__isNeList) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U21) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (int_symb M.a__U21) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.a__U22) => nil | (int_symb M.a__U22) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__isList) => nil | (int_symb M.a__isList) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U23) => nil | (int_symb M.a__U23) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U31) => nil | (int_symb M.a__U31) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U32) => nil | (int_symb M.a__U32) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__isQid) => nil | (int_symb M.a__isQid) => nil | (hd_symb M.a__U41) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (int_symb M.a__U41) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.a__U42) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a__U42) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__U43) => nil | (int_symb M.a__U43) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U51) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (3%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (int_symb M.a__U51) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.a__U52) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a__U52) => (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.a__U53) => nil | (int_symb M.a__U53) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U61) => nil | (int_symb M.a__U61) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U62) => nil | (int_symb M.a__U62) => nil | (hd_symb M.a__U71) => nil | (int_symb M.a__U71) => nil | (hd_symb M.a__U72) => nil | (int_symb M.a__U72) => nil | (hd_symb M.a__isNePal) => nil | (int_symb M.a__isNePal) => (1%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M.a__and) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a__and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__isPalListKind) => nil | (int_symb M.a__isPalListKind) => nil | (hd_symb M.isPalListKind) => nil | (int_symb M.isPalListKind) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.isPal) => nil | (int_symb M.isPal) => nil | (hd_symb M.a__isPal) => nil | (int_symb M.a__isPal) => 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) => (1%Z, Vnil) :: nil | (hd_symb M.u) => nil | (int_symb M.u) => nil | (hd_symb M.U11) => nil | (int_symb M.U11) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.U12) => nil | (int_symb M.U12) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isNeList) => nil | (int_symb M.isNeList) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U21) => nil | (int_symb M.U21) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.U22) => nil | (int_symb M.U22) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.isList) => nil | (int_symb M.isList) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U23) => nil | (int_symb M.U23) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U31) => nil | (int_symb M.U31) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U32) => nil | (int_symb M.U32) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isQid) => nil | (int_symb M.isQid) => nil | (hd_symb M.U41) => nil | (int_symb M.U41) => (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.U42) => nil | (int_symb M.U42) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.U43) => nil | (int_symb M.U43) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U51) => nil | (int_symb M.U51) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.U52) => nil | (int_symb M.U52) => (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.U53) => nil | (int_symb M.U53) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U61) => nil | (int_symb M.U61) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.U62) => nil | (int_symb M.U62) => nil | (hd_symb M.U71) => nil | (int_symb M.U71) => nil | (hd_symb M.U72) => nil | (int_symb M.U72) => nil | (hd_symb M.isNePal) => nil | (int_symb M.isNePal) => (1%Z, (Vcons 0 Vnil)) :: nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS6. Module PI6 := PolyInt PIS6. (* graph decomposition 2 *) Definition cs2 : list (list (@ATrs.rule s1)) := ( R1 (S1.ha__U51 (S1.tt) (V1 0) (V1 1)) (S1.ha__U52 (S1.a__isNeList (V1 0)) (V1 1)) :: nil) :: ( R1 (S1.ha__U11 (S1.tt) (V1 0)) (S1.ha__isNeList (V1 0)) :: R1 (S1.ha__isNeList (V1 0)) (S1.ha__isPalListKind (V1 0)) :: R1 (S1.ha__isPalListKind (S1.__ (V1 0) (V1 1))) (S1.ha__and (S1.a__isPalListKind (V1 0)) (S1.isPalListKind (V1 1))) :: R1 (S1.ha__and (S1.tt) (V1 0)) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U11 (V1 0) (V1 1))) (S1.ha__U11 (S1.mark (V1 0)) (V1 1)) :: R1 (S1.hmark (S1.U11 (V1 0) (V1 1))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U12 (V1 0))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.isNeList (V1 0))) (S1.ha__isNeList (V1 0)) :: R1 (S1.hmark (S1.U22 (V1 0) (V1 1))) (S1.ha__U22 (S1.mark (V1 0)) (V1 1)) :: R1 (S1.ha__U22 (S1.tt) (V1 0)) (S1.ha__isList (V1 0)) :: R1 (S1.ha__isList (V1 0)) (S1.ha__U11 (S1.a__isPalListKind (V1 0)) (V1 0)) :: R1 (S1.ha__isList (V1 0)) (S1.ha__isPalListKind (V1 0)) :: R1 (S1.ha__isPalListKind (S1.__ (V1 0) (V1 1))) (S1.ha__isPalListKind (V1 0)) :: R1 (S1.hmark (S1.U22 (V1 0) (V1 1))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.isList (V1 0))) (S1.ha__isList (V1 0)) :: R1 (S1.hmark (S1.U23 (V1 0))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U31 (V1 0) (V1 1))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U32 (V1 0))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U41 (V1 0) (V1 1) (V1 2))) (S1.ha__U41 (S1.mark (V1 0)) (V1 1) (V1 2)) :: R1 (S1.ha__U41 (S1.tt) (V1 0) (V1 1)) (S1.ha__U42 (S1.a__isList (V1 0)) (V1 1)) :: R1 (S1.ha__U42 (S1.tt) (V1 0)) (S1.ha__isNeList (V1 0)) :: R1 (S1.ha__U41 (S1.tt) (V1 0) (V1 1)) (S1.ha__isList (V1 0)) :: R1 (S1.hmark (S1.U41 (V1 0) (V1 1) (V1 2))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U42 (V1 0) (V1 1))) (S1.ha__U42 (S1.mark (V1 0)) (V1 1)) :: R1 (S1.hmark (S1.U42 (V1 0) (V1 1))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U43 (V1 0))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U53 (V1 0))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.and (V1 0) (V1 1))) (S1.ha__and (S1.mark (V1 0)) (V1 1)) :: R1 (S1.hmark (S1.and (V1 0) (V1 1))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.isPalListKind (V1 0))) (S1.ha__isPalListKind (V1 0)) :: nil) :: nil. (* 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.a____) => nil | (int_symb M.a____) => (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 | (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.mark) => (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.mark) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.a__U11) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a__U11) => (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.a__U12) => nil | (int_symb M.a__U12) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__isNeList) => (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.a__isNeList) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U21) => nil | (int_symb M.a__U21) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.a__U22) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a__U22) => (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.a__isList) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.a__isList) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U23) => nil | (int_symb M.a__U23) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U31) => nil | (int_symb M.a__U31) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U32) => nil | (int_symb M.a__U32) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__isQid) => nil | (int_symb M.a__isQid) => nil | (hd_symb M.a__U41) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (int_symb M.a__U41) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.a__U42) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a__U42) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__U43) => nil | (int_symb M.a__U43) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U51) => nil | (int_symb M.a__U51) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.a__U52) => nil | (int_symb M.a__U52) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__U53) => nil | (int_symb M.a__U53) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U61) => nil | (int_symb M.a__U61) => nil | (hd_symb M.a__U62) => nil | (int_symb M.a__U62) => nil | (hd_symb M.a__U71) => nil | (int_symb M.a__U71) => nil | (hd_symb M.a__U72) => nil | (int_symb M.a__U72) => nil | (hd_symb M.a__isNePal) => nil | (int_symb M.a__isNePal) => nil | (hd_symb M.a__and) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a__and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__isPalListKind) => nil | (int_symb M.a__isPalListKind) => nil | (hd_symb M.isPalListKind) => nil | (int_symb M.isPalListKind) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.isPal) => nil | (int_symb M.isPal) => nil | (hd_symb M.a__isPal) => nil | (int_symb M.a__isPal) => 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) => (2%Z, Vnil) :: nil | (hd_symb M.u) => nil | (int_symb M.u) => nil | (hd_symb M.U11) => nil | (int_symb M.U11) => (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.U12) => nil | (int_symb M.U12) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isNeList) => nil | (int_symb M.isNeList) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U21) => nil | (int_symb M.U21) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.U22) => nil | (int_symb M.U22) => (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.isList) => nil | (int_symb M.isList) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U23) => nil | (int_symb M.U23) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U31) => nil | (int_symb M.U31) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U32) => nil | (int_symb M.U32) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isQid) => nil | (int_symb M.isQid) => nil | (hd_symb M.U41) => nil | (int_symb M.U41) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.U42) => nil | (int_symb M.U42) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.U43) => nil | (int_symb M.U43) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U51) => nil | (int_symb M.U51) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.U52) => nil | (int_symb M.U52) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.U53) => nil | (int_symb M.U53) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U61) => nil | (int_symb M.U61) => nil | (hd_symb M.U62) => nil | (int_symb M.U62) => nil | (hd_symb M.U71) => nil | (int_symb M.U71) => nil | (hd_symb M.U72) => nil | (int_symb M.U72) => nil | (hd_symb M.isNePal) => nil | (int_symb M.isNePal) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS7. Module PI7 := PolyInt PIS7. (* graph decomposition 3 *) Definition cs3 : list (list (@ATrs.rule s1)) := ( R1 (S1.ha__isList (V1 0)) (S1.ha__U11 (S1.a__isPalListKind (V1 0)) (V1 0)) :: nil) :: ( R1 (S1.ha__U41 (S1.tt) (V1 0) (V1 1)) (S1.ha__isList (V1 0)) :: nil) :: ( R1 (S1.hmark (S1.isList (V1 0))) (S1.ha__isList (V1 0)) :: nil) :: ( R1 (S1.ha__U22 (S1.tt) (V1 0)) (S1.ha__isList (V1 0)) :: nil) :: ( R1 (S1.hmark (S1.U22 (V1 0) (V1 1))) (S1.ha__U22 (S1.mark (V1 0)) (V1 1)) :: nil) :: ( R1 (S1.hmark (S1.U11 (V1 0) (V1 1))) (S1.ha__U11 (S1.mark (V1 0)) (V1 1)) :: nil) :: ( R1 (S1.ha__isPalListKind (S1.__ (V1 0) (V1 1))) (S1.ha__and (S1.a__isPalListKind (V1 0)) (S1.isPalListKind (V1 1))) :: R1 (S1.ha__and (S1.tt) (V1 0)) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.isNeList (V1 0))) (S1.ha__isNeList (V1 0)) :: R1 (S1.ha__isNeList (V1 0)) (S1.ha__isPalListKind (V1 0)) :: R1 (S1.ha__isPalListKind (S1.__ (V1 0) (V1 1))) (S1.ha__isPalListKind (V1 0)) :: R1 (S1.hmark (S1.U23 (V1 0))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U31 (V1 0) (V1 1))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U32 (V1 0))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U41 (V1 0) (V1 1) (V1 2))) (S1.ha__U41 (S1.mark (V1 0)) (V1 1) (V1 2)) :: R1 (S1.ha__U41 (S1.tt) (V1 0) (V1 1)) (S1.ha__U42 (S1.a__isList (V1 0)) (V1 1)) :: R1 (S1.ha__U42 (S1.tt) (V1 0)) (S1.ha__isNeList (V1 0)) :: R1 (S1.hmark (S1.U42 (V1 0) (V1 1))) (S1.ha__U42 (S1.mark (V1 0)) (V1 1)) :: R1 (S1.hmark (S1.U42 (V1 0) (V1 1))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U43 (V1 0))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U53 (V1 0))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.and (V1 0) (V1 1))) (S1.ha__and (S1.mark (V1 0)) (V1 1)) :: R1 (S1.hmark (S1.and (V1 0) (V1 1))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.isPalListKind (V1 0))) (S1.ha__isPalListKind (V1 0)) :: nil) :: nil. (* 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.a____) => nil | (int_symb M.a____) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.__) => nil | (int_symb M.__) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.mark) => (2%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.mark) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.a__U11) => nil | (int_symb M.a__U11) => nil | (hd_symb M.tt) => nil | (int_symb M.tt) => nil | (hd_symb M.a__U12) => nil | (int_symb M.a__U12) => nil | (hd_symb M.a__isNeList) => (1%Z, (Vcons 0 Vnil)) :: nil | (int_symb M.a__isNeList) => (1%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M.a__U21) => nil | (int_symb M.a__U21) => nil | (hd_symb M.a__U22) => nil | (int_symb M.a__U22) => nil | (hd_symb M.a__isList) => nil | (int_symb M.a__isList) => nil | (hd_symb M.a__U23) => nil | (int_symb M.a__U23) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U31) => nil | (int_symb M.a__U31) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U32) => nil | (int_symb M.a__U32) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__isQid) => nil | (int_symb M.a__isQid) => nil | (hd_symb M.a__U41) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (int_symb M.a__U41) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.a__U42) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (int_symb M.a__U42) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U43) => nil | (int_symb M.a__U43) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U51) => nil | (int_symb M.a__U51) => nil | (hd_symb M.a__U52) => nil | (int_symb M.a__U52) => nil | (hd_symb M.a__U53) => nil | (int_symb M.a__U53) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U61) => nil | (int_symb M.a__U61) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U62) => nil | (int_symb M.a__U62) => nil | (hd_symb M.a__U71) => nil | (int_symb M.a__U71) => nil | (hd_symb M.a__U72) => nil | (int_symb M.a__U72) => nil | (hd_symb M.a__isNePal) => nil | (int_symb M.a__isNePal) => nil | (hd_symb M.a__and) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a__and) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__isPalListKind) => nil | (int_symb M.a__isPalListKind) => nil | (hd_symb M.isPalListKind) => nil | (int_symb M.isPalListKind) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.isPal) => nil | (int_symb M.isPal) => nil | (hd_symb M.a__isPal) => nil | (int_symb M.a__isPal) => 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) => (1%Z, Vnil) :: nil | (hd_symb M.U11) => nil | (int_symb M.U11) => nil | (hd_symb M.U12) => nil | (int_symb M.U12) => nil | (hd_symb M.isNeList) => nil | (int_symb M.isNeList) => (1%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M.U21) => nil | (int_symb M.U21) => nil | (hd_symb M.U22) => nil | (int_symb M.U22) => nil | (hd_symb M.isList) => nil | (int_symb M.isList) => nil | (hd_symb M.U23) => nil | (int_symb M.U23) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U31) => nil | (int_symb M.U31) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U32) => nil | (int_symb M.U32) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isQid) => nil | (int_symb M.isQid) => nil | (hd_symb M.U41) => nil | (int_symb M.U41) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.U42) => nil | (int_symb M.U42) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U43) => nil | (int_symb M.U43) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U51) => nil | (int_symb M.U51) => nil | (hd_symb M.U52) => nil | (int_symb M.U52) => nil | (hd_symb M.U53) => nil | (int_symb M.U53) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U61) => nil | (int_symb M.U61) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U62) => nil | (int_symb M.U62) => nil | (hd_symb M.U71) => nil | (int_symb M.U71) => nil | (hd_symb M.U72) => nil | (int_symb M.U72) => nil | (hd_symb M.isNePal) => nil | (int_symb M.isNePal) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS8. Module PI8 := PolyInt PIS8. (* graph decomposition 4 *) Definition cs4 : list (list (@ATrs.rule s1)) := ( R1 (S1.hmark (S1.U42 (V1 0) (V1 1))) (S1.ha__U42 (S1.mark (V1 0)) (V1 1)) :: nil) :: ( R1 (S1.ha__U41 (S1.tt) (V1 0) (V1 1)) (S1.ha__U42 (S1.a__isList (V1 0)) (V1 1)) :: nil) :: ( R1 (S1.hmark (S1.U41 (V1 0) (V1 1) (V1 2))) (S1.ha__U41 (S1.mark (V1 0)) (V1 1) (V1 2)) :: nil) :: ( R1 (S1.ha__and (S1.tt) (V1 0)) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U23 (V1 0))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U43 (V1 0))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.U53 (V1 0))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.and (V1 0) (V1 1))) (S1.ha__and (S1.mark (V1 0)) (V1 1)) :: R1 (S1.hmark (S1.and (V1 0) (V1 1))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.isPalListKind (V1 0))) (S1.ha__isPalListKind (V1 0)) :: R1 (S1.ha__isPalListKind (S1.__ (V1 0) (V1 1))) (S1.ha__and (S1.a__isPalListKind (V1 0)) (S1.isPalListKind (V1 1))) :: R1 (S1.ha__isPalListKind (S1.__ (V1 0) (V1 1))) (S1.ha__isPalListKind (V1 0)) :: nil) :: nil. (* 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.a____) => nil | (int_symb M.a____) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.__) => nil | (int_symb M.__) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.mark) => (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.mark) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => (1%Z, Vnil) :: nil | (hd_symb M.a__U11) => nil | (int_symb M.a__U11) => nil | (hd_symb M.tt) => nil | (int_symb M.tt) => nil | (hd_symb M.a__U12) => nil | (int_symb M.a__U12) => nil | (hd_symb M.a__isNeList) => nil | (int_symb M.a__isNeList) => (2%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M.a__U21) => nil | (int_symb M.a__U21) => nil | (hd_symb M.a__U22) => nil | (int_symb M.a__U22) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__isList) => nil | (int_symb M.a__isList) => nil | (hd_symb M.a__U23) => nil | (int_symb M.a__U23) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U31) => nil | (int_symb M.a__U31) => nil | (hd_symb M.a__U32) => nil | (int_symb M.a__U32) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__isQid) => nil | (int_symb M.a__isQid) => nil | (hd_symb M.a__U41) => nil | (int_symb M.a__U41) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.a__U42) => nil | (int_symb M.a__U42) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U43) => nil | (int_symb M.a__U43) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U51) => nil | (int_symb M.a__U51) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.a__U52) => nil | (int_symb M.a__U52) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U53) => nil | (int_symb M.a__U53) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U61) => nil | (int_symb M.a__U61) => nil | (hd_symb M.a__U62) => nil | (int_symb M.a__U62) => nil | (hd_symb M.a__U71) => nil | (int_symb M.a__U71) => nil | (hd_symb M.a__U72) => nil | (int_symb M.a__U72) => nil | (hd_symb M.a__isNePal) => nil | (int_symb M.a__isNePal) => nil | (hd_symb M.a__and) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a__and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__isPalListKind) => nil | (int_symb M.a__isPalListKind) => nil | (hd_symb M.isPalListKind) => nil | (int_symb M.isPalListKind) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.isPal) => nil | (int_symb M.isPal) => nil | (hd_symb M.a__isPal) => nil | (int_symb M.a__isPal) => 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 | (hd_symb M.U11) => nil | (int_symb M.U11) => nil | (hd_symb M.U12) => nil | (int_symb M.U12) => nil | (hd_symb M.isNeList) => nil | (int_symb M.isNeList) => (2%Z, (Vcons 0 Vnil)) :: nil | (hd_symb M.U21) => nil | (int_symb M.U21) => nil | (hd_symb M.U22) => nil | (int_symb M.U22) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.isList) => nil | (int_symb M.isList) => nil | (hd_symb M.U23) => nil | (int_symb M.U23) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U31) => nil | (int_symb M.U31) => nil | (hd_symb M.U32) => nil | (int_symb M.U32) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isQid) => nil | (int_symb M.isQid) => nil | (hd_symb M.U41) => nil | (int_symb M.U41) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.U42) => nil | (int_symb M.U42) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.U43) => nil | (int_symb M.U43) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U51) => nil | (int_symb M.U51) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 1 (Vcons 0 (Vcons 0 Vnil)))) :: nil | (hd_symb M.U52) => nil | (int_symb M.U52) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: nil | (hd_symb M.U53) => nil | (int_symb M.U53) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U61) => nil | (int_symb M.U61) => nil | (hd_symb M.U62) => nil | (int_symb M.U62) => nil | (hd_symb M.U71) => nil | (int_symb M.U71) => nil | (hd_symb M.U72) => nil | (int_symb M.U72) => nil | (hd_symb M.isNePal) => nil | (int_symb M.isNePal) => 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.a____) => nil | (int_symb M.a____) => (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.__) => nil | (int_symb M.__) => (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.mark) => (2%Z, (Vcons 1 Vnil)) :: 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.a__U11) => nil | (int_symb M.a__U11) => nil | (hd_symb M.tt) => nil | (int_symb M.tt) => nil | (hd_symb M.a__U12) => nil | (int_symb M.a__U12) => nil | (hd_symb M.a__isNeList) => nil | (int_symb M.a__isNeList) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U21) => nil | (int_symb M.a__U21) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.a__U22) => nil | (int_symb M.a__U22) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__isList) => nil | (int_symb M.a__isList) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U23) => nil | (int_symb M.a__U23) => (2%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U31) => nil | (int_symb M.a__U31) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__U32) => nil | (int_symb M.a__U32) => nil | (hd_symb M.a__isQid) => nil | (int_symb M.a__isQid) => nil | (hd_symb M.a__U41) => nil | (int_symb M.a__U41) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.a__U42) => nil | (int_symb M.a__U42) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__U43) => nil | (int_symb M.a__U43) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U51) => nil | (int_symb M.a__U51) => nil | (hd_symb M.a__U52) => nil | (int_symb M.a__U52) => nil | (hd_symb M.a__U53) => nil | (int_symb M.a__U53) => nil | (hd_symb M.a__U61) => nil | (int_symb M.a__U61) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.a__U62) => nil | (int_symb M.a__U62) => nil | (hd_symb M.a__U71) => nil | (int_symb M.a__U71) => nil | (hd_symb M.a__U72) => nil | (int_symb M.a__U72) => nil | (hd_symb M.a__isNePal) => nil | (int_symb M.a__isNePal) => nil | (hd_symb M.a__and) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a__and) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__isPalListKind) => nil | (int_symb M.a__isPalListKind) => nil | (hd_symb M.isPalListKind) => nil | (int_symb M.isPalListKind) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (1%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.isPal) => nil | (int_symb M.isPal) => nil | (hd_symb M.a__isPal) => nil | (int_symb M.a__isPal) => 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 | (hd_symb M.U11) => nil | (int_symb M.U11) => nil | (hd_symb M.U12) => nil | (int_symb M.U12) => nil | (hd_symb M.isNeList) => nil | (int_symb M.isNeList) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U21) => nil | (int_symb M.U21) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.U22) => nil | (int_symb M.U22) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.isList) => nil | (int_symb M.isList) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U23) => nil | (int_symb M.U23) => (2%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U31) => nil | (int_symb M.U31) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.U32) => nil | (int_symb M.U32) => nil | (hd_symb M.isQid) => nil | (int_symb M.isQid) => nil | (hd_symb M.U41) => nil | (int_symb M.U41) => (2%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (1%Z, (Vcons 0 (Vcons 1 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.U42) => nil | (int_symb M.U42) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.U43) => nil | (int_symb M.U43) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U51) => nil | (int_symb M.U51) => nil | (hd_symb M.U52) => nil | (int_symb M.U52) => nil | (hd_symb M.U53) => nil | (int_symb M.U53) => nil | (hd_symb M.U61) => nil | (int_symb M.U61) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: nil | (hd_symb M.U62) => nil | (int_symb M.U62) => nil | (hd_symb M.U71) => nil | (int_symb M.U71) => nil | (hd_symb M.U72) => nil | (int_symb M.U72) => nil | (hd_symb M.isNePal) => nil | (int_symb M.isNePal) => 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.a____) => nil | (int_symb M.a____) => (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.__) => nil | (int_symb M.__) => (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.mark) => (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.mark) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.a__U11) => nil | (int_symb M.a__U11) => nil | (hd_symb M.tt) => nil | (int_symb M.tt) => nil | (hd_symb M.a__U12) => nil | (int_symb M.a__U12) => nil | (hd_symb M.a__isNeList) => nil | (int_symb M.a__isNeList) => nil | (hd_symb M.a__U21) => nil | (int_symb M.a__U21) => nil | (hd_symb M.a__U22) => nil | (int_symb M.a__U22) => nil | (hd_symb M.a__isList) => nil | (int_symb M.a__isList) => nil | (hd_symb M.a__U23) => nil | (int_symb M.a__U23) => nil | (hd_symb M.a__U31) => nil | (int_symb M.a__U31) => nil | (hd_symb M.a__U32) => nil | (int_symb M.a__U32) => nil | (hd_symb M.a__isQid) => nil | (int_symb M.a__isQid) => nil | (hd_symb M.a__U41) => nil | (int_symb M.a__U41) => nil | (hd_symb M.a__U42) => nil | (int_symb M.a__U42) => nil | (hd_symb M.a__U43) => nil | (int_symb M.a__U43) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U51) => nil | (int_symb M.a__U51) => nil | (hd_symb M.a__U52) => nil | (int_symb M.a__U52) => nil | (hd_symb M.a__U53) => nil | (int_symb M.a__U53) => nil | (hd_symb M.a__U61) => nil | (int_symb M.a__U61) => nil | (hd_symb M.a__U62) => nil | (int_symb M.a__U62) => nil | (hd_symb M.a__U71) => nil | (int_symb M.a__U71) => nil | (hd_symb M.a__U72) => nil | (int_symb M.a__U72) => nil | (hd_symb M.a__isNePal) => nil | (int_symb M.a__isNePal) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__and) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a__and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__isPalListKind) => (2%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.a__isPalListKind) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isPalListKind) => nil | (int_symb M.isPalListKind) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.and) => nil | (int_symb M.and) => (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.isPal) => nil | (int_symb M.isPal) => nil | (hd_symb M.a__isPal) => nil | (int_symb M.a__isPal) => nil | (hd_symb M.a) => nil | (int_symb M.a) => nil | (hd_symb M.e) => nil | (int_symb M.e) => (2%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) => (2%Z, Vnil) :: nil | (hd_symb M.U11) => nil | (int_symb M.U11) => nil | (hd_symb M.U12) => nil | (int_symb M.U12) => nil | (hd_symb M.isNeList) => nil | (int_symb M.isNeList) => nil | (hd_symb M.U21) => nil | (int_symb M.U21) => nil | (hd_symb M.U22) => nil | (int_symb M.U22) => nil | (hd_symb M.isList) => nil | (int_symb M.isList) => nil | (hd_symb M.U23) => nil | (int_symb M.U23) => nil | (hd_symb M.U31) => nil | (int_symb M.U31) => nil | (hd_symb M.U32) => nil | (int_symb M.U32) => nil | (hd_symb M.isQid) => nil | (int_symb M.isQid) => nil | (hd_symb M.U41) => nil | (int_symb M.U41) => nil | (hd_symb M.U42) => nil | (int_symb M.U42) => nil | (hd_symb M.U43) => nil | (int_symb M.U43) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U51) => nil | (int_symb M.U51) => nil | (hd_symb M.U52) => nil | (int_symb M.U52) => nil | (hd_symb M.U53) => nil | (int_symb M.U53) => nil | (hd_symb M.U61) => nil | (int_symb M.U61) => nil | (hd_symb M.U62) => nil | (int_symb M.U62) => nil | (hd_symb M.U71) => nil | (int_symb M.U71) => nil | (hd_symb M.U72) => nil | (int_symb M.U72) => nil | (hd_symb M.isNePal) => nil | (int_symb M.isNePal) => (1%Z, (Vcons 1 Vnil)) :: nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS11. Module PI11 := PolyInt PIS11. (* graph decomposition 5 *) Definition cs5 : list (list (@ATrs.rule s1)) := ( R1 (S1.hmark (S1.isPalListKind (V1 0))) (S1.ha__isPalListKind (V1 0)) :: nil) :: ( R1 (S1.hmark (S1.U43 (V1 0))) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.and (V1 0) (V1 1))) (S1.ha__and (S1.mark (V1 0)) (V1 1)) :: R1 (S1.ha__and (S1.tt) (V1 0)) (S1.hmark (V1 0)) :: R1 (S1.hmark (S1.and (V1 0) (V1 1))) (S1.hmark (V1 0)) :: nil) :: nil. (* 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.a____) => nil | (int_symb M.a____) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.__) => nil | (int_symb M.__) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (3%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.mark) => (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.mark) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.a__U11) => nil | (int_symb M.a__U11) => nil | (hd_symb M.tt) => nil | (int_symb M.tt) => nil | (hd_symb M.a__U12) => nil | (int_symb M.a__U12) => nil | (hd_symb M.a__isNeList) => nil | (int_symb M.a__isNeList) => nil | (hd_symb M.a__U21) => nil | (int_symb M.a__U21) => nil | (hd_symb M.a__U22) => nil | (int_symb M.a__U22) => nil | (hd_symb M.a__isList) => nil | (int_symb M.a__isList) => nil | (hd_symb M.a__U23) => nil | (int_symb M.a__U23) => nil | (hd_symb M.a__U31) => nil | (int_symb M.a__U31) => nil | (hd_symb M.a__U32) => nil | (int_symb M.a__U32) => nil | (hd_symb M.a__isQid) => nil | (int_symb M.a__isQid) => nil | (hd_symb M.a__U41) => nil | (int_symb M.a__U41) => nil | (hd_symb M.a__U42) => nil | (int_symb M.a__U42) => nil | (hd_symb M.a__U43) => nil | (int_symb M.a__U43) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U51) => nil | (int_symb M.a__U51) => nil | (hd_symb M.a__U52) => nil | (int_symb M.a__U52) => nil | (hd_symb M.a__U53) => nil | (int_symb M.a__U53) => nil | (hd_symb M.a__U61) => nil | (int_symb M.a__U61) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__U62) => nil | (int_symb M.a__U62) => nil | (hd_symb M.a__U71) => nil | (int_symb M.a__U71) => nil | (hd_symb M.a__U72) => nil | (int_symb M.a__U72) => nil | (hd_symb M.a__isNePal) => nil | (int_symb M.a__isNePal) => (2%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__and) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (int_symb M.a__and) => (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.a__isPalListKind) => nil | (int_symb M.a__isPalListKind) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.isPalListKind) => nil | (int_symb M.isPalListKind) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.and) => nil | (int_symb M.and) => (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.isPal) => nil | (int_symb M.isPal) => (1%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__isPal) => nil | (int_symb M.a__isPal) => (1%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: 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) => (3%Z, Vnil) :: nil | (hd_symb M.U11) => nil | (int_symb M.U11) => nil | (hd_symb M.U12) => nil | (int_symb M.U12) => nil | (hd_symb M.isNeList) => nil | (int_symb M.isNeList) => nil | (hd_symb M.U21) => nil | (int_symb M.U21) => nil | (hd_symb M.U22) => nil | (int_symb M.U22) => nil | (hd_symb M.isList) => nil | (int_symb M.isList) => nil | (hd_symb M.U23) => nil | (int_symb M.U23) => nil | (hd_symb M.U31) => nil | (int_symb M.U31) => nil | (hd_symb M.U32) => nil | (int_symb M.U32) => nil | (hd_symb M.isQid) => nil | (int_symb M.isQid) => nil | (hd_symb M.U41) => nil | (int_symb M.U41) => nil | (hd_symb M.U42) => nil | (int_symb M.U42) => nil | (hd_symb M.U43) => nil | (int_symb M.U43) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U51) => nil | (int_symb M.U51) => nil | (hd_symb M.U52) => nil | (int_symb M.U52) => nil | (hd_symb M.U53) => nil | (int_symb M.U53) => nil | (hd_symb M.U61) => nil | (int_symb M.U61) => (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.U62) => nil | (int_symb M.U62) => nil | (hd_symb M.U71) => nil | (int_symb M.U71) => nil | (hd_symb M.U72) => nil | (int_symb M.U72) => nil | (hd_symb M.isNePal) => nil | (int_symb M.isNePal) => (2%Z, (Vcons 0 Vnil)) :: (2%Z, (Vcons 1 Vnil)) :: nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS12. Module PI12 := PolyInt PIS12. (* graph decomposition 6 *) Definition cs6 : list (list (@ATrs.rule s1)) := ( R1 (S1.hmark (S1.U43 (V1 0))) (S1.hmark (V1 0)) :: nil) :: ( R1 (S1.ha__and (S1.tt) (V1 0)) (S1.hmark (V1 0)) :: nil) :: nil. (* 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.a____) => nil | (int_symb M.a____) => (2%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 | (int_symb M.__) => (2%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 1 (Vcons 0 Vnil))) :: (1%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.mark) => (1%Z, (Vcons 1 Vnil)) :: nil | (int_symb M.mark) => (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.nil) => nil | (int_symb M.nil) => nil | (hd_symb M.a__U11) => nil | (int_symb M.a__U11) => nil | (hd_symb M.tt) => nil | (int_symb M.tt) => nil | (hd_symb M.a__U12) => nil | (int_symb M.a__U12) => nil | (hd_symb M.a__isNeList) => nil | (int_symb M.a__isNeList) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U21) => nil | (int_symb M.a__U21) => nil | (hd_symb M.a__U22) => nil | (int_symb M.a__U22) => nil | (hd_symb M.a__isList) => nil | (int_symb M.a__isList) => nil | (hd_symb M.a__U23) => nil | (int_symb M.a__U23) => nil | (hd_symb M.a__U31) => nil | (int_symb M.a__U31) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__U32) => nil | (int_symb M.a__U32) => nil | (hd_symb M.a__isQid) => nil | (int_symb M.a__isQid) => nil | (hd_symb M.a__U41) => nil | (int_symb M.a__U41) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.a__U42) => nil | (int_symb M.a__U42) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__U43) => nil | (int_symb M.a__U43) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.a__U51) => nil | (int_symb M.a__U51) => nil | (hd_symb M.a__U52) => nil | (int_symb M.a__U52) => nil | (hd_symb M.a__U53) => nil | (int_symb M.a__U53) => nil | (hd_symb M.a__U61) => nil | (int_symb M.a__U61) => nil | (hd_symb M.a__U62) => nil | (int_symb M.a__U62) => nil | (hd_symb M.a__U71) => nil | (int_symb M.a__U71) => nil | (hd_symb M.a__U72) => nil | (int_symb M.a__U72) => nil | (hd_symb M.a__isNePal) => nil | (int_symb M.a__isNePal) => nil | (hd_symb M.a__and) => nil | (int_symb M.a__and) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.a__isPalListKind) => nil | (int_symb M.a__isPalListKind) => nil | (hd_symb M.isPalListKind) => nil | (int_symb M.isPalListKind) => nil | (hd_symb M.and) => nil | (int_symb M.and) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.isPal) => nil | (int_symb M.isPal) => nil | (hd_symb M.a__isPal) => nil | (int_symb M.a__isPal) => 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 | (hd_symb M.U11) => nil | (int_symb M.U11) => nil | (hd_symb M.U12) => nil | (int_symb M.U12) => nil | (hd_symb M.isNeList) => nil | (int_symb M.isNeList) => (2%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U21) => nil | (int_symb M.U21) => nil | (hd_symb M.U22) => nil | (int_symb M.U22) => nil | (hd_symb M.isList) => nil | (int_symb M.isList) => nil | (hd_symb M.U23) => nil | (int_symb M.U23) => nil | (hd_symb M.U31) => nil | (int_symb M.U31) => (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.U32) => nil | (int_symb M.U32) => nil | (hd_symb M.isQid) => nil | (int_symb M.isQid) => nil | (hd_symb M.U41) => nil | (int_symb M.U41) => (1%Z, (Vcons 0 (Vcons 0 (Vcons 0 Vnil)))) :: (2%Z, (Vcons 0 (Vcons 0 (Vcons 1 Vnil)))) :: nil | (hd_symb M.U42) => nil | (int_symb M.U42) => (1%Z, (Vcons 0 (Vcons 0 Vnil))) :: (2%Z, (Vcons 0 (Vcons 1 Vnil))) :: nil | (hd_symb M.U43) => nil | (int_symb M.U43) => (1%Z, (Vcons 0 Vnil)) :: (1%Z, (Vcons 1 Vnil)) :: nil | (hd_symb M.U51) => nil | (int_symb M.U51) => nil | (hd_symb M.U52) => nil | (int_symb M.U52) => nil | (hd_symb M.U53) => nil | (int_symb M.U53) => nil | (hd_symb M.U61) => nil | (int_symb M.U61) => nil | (hd_symb M.U62) => nil | (int_symb M.U62) => nil | (hd_symb M.U71) => nil | (int_symb M.U71) => nil | (hd_symb M.U72) => nil | (int_symb M.U72) => nil | (hd_symb M.isNePal) => nil | (int_symb M.isNePal) => nil end. Lemma trsInt_wm : forall f, pweak_monotone (trsInt f). Proof. pmonotone. Qed. End PIS13. Module PI13 := PolyInt PIS13. (* 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. left. co_scc. left. co_scc. left. co_scc. left. co_scc. left. co_scc. left. co_scc. right. PI1.prove_termination. PI2.prove_termination. PI3.prove_termination. PI4.prove_termination. PI5.prove_termination. PI6.prove_termination. let D := fresh "D" in let R := fresh "R" in set_rules_to D; set_mod_rules_to R; graph_decomp (dpg_unif_N 100 R D) cs2; subst D; subst R. dpg_unif_N_correct. left. co_scc. right. PI7.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. left. co_scc. left. co_scc. right. PI8.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) cs4; subst D; subst R. dpg_unif_N_correct. left. co_scc. left. co_scc. left. co_scc. right. PI9.prove_termination. PI10.prove_termination. PI11.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) cs5; subst D; subst R. dpg_unif_N_correct. left. co_scc. right. PI12.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) cs6; subst D; subst R. dpg_unif_N_correct. right. PI13.prove_termination. termination_trivial. left. co_scc. Qed.