Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PALINDROME_complete_iGM)

The rewrite relation of the following TRS is considered.

There are 155 ruless (increase limit for explicit display).

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the

prec(__)	=	12	stat(__)	=	lex
prec(nil)	=	14	stat(nil)	=	mul
prec(U11)	=	1	stat(U11)	=	mul
prec(tt)	=	13	stat(tt)	=	mul
prec(isNeList)	=	1	stat(isNeList)	=	mul
prec(U21)	=	4	stat(U21)	=	lex
prec(U22)	=	3	stat(U22)	=	mul
prec(isList)	=	2	stat(isList)	=	mul
prec(U31)	=	0	stat(U31)	=	mul
prec(U41)	=	5	stat(U41)	=	lex
prec(U42)	=	1	stat(U42)	=	mul
prec(U51)	=	6	stat(U51)	=	lex
prec(U52)	=	2	stat(U52)	=	mul
prec(U61)	=	7	stat(U61)	=	mul
prec(U71)	=	9	stat(U71)	=	mul
prec(isNePal)	=	8	stat(isNePal)	=	mul
prec(and)	=	10	stat(and)	=	lex
prec(isPal)	=	11	stat(isPal)	=	mul
prec(a)	=	15	stat(a)	=	mul
prec(e)	=	13	stat(e)	=	mul
prec(i)	=	13	stat(i)	=	mul
prec(o)	=	16	stat(o)	=	mul
prec(u)	=	13	stat(u)	=	mul

π(active)	=	1
π(__)	=	[1,2]
π(mark)	=	1
π(nil)	=	[]
π(U11)	=	[1,2]
π(tt)	=	[]
π(U12)	=	1
π(isNeList)	=	[1]
π(U21)	=	[1,2,3]
π(U22)	=	[1,2]
π(isList)	=	[1]
π(U23)	=	1
π(U31)	=	[1,2]
π(U32)	=	1
π(isQid)	=	1
π(U41)	=	[1,3,2]
π(U42)	=	[1,2]
π(U43)	=	1
π(U51)	=	[1,2,3]
π(U52)	=	[1,2]
π(U53)	=	1
π(U61)	=	[1,2]
π(U62)	=	1
π(U71)	=	[1,2]
π(U72)	=	1
π(isNePal)	=	[1]
π(and)	=	[2,1]
π(isPalListKind)	=	1
π(isPal)	=	[1]
π(a)	=	[]
π(e)	=	[]
π(i)	=	[]
π(o)	=	[]
π(u)	=	[]

all of the following rules can be deleted.

active(__(__(X,Y),Z))	→	mark(__(X,__(Y,Z)))	(1)
active(__(X,nil))	→	mark(X)	(2)
active(__(nil,X))	→	mark(X)	(3)
active(U11(tt,V))	→	mark(U12(isNeList(V)))	(4)
active(U21(tt,V1,V2))	→	mark(U22(isList(V1),V2))	(6)
active(U22(tt,V2))	→	mark(U23(isList(V2)))	(7)
active(U31(tt,V))	→	mark(U32(isQid(V)))	(9)
active(U41(tt,V1,V2))	→	mark(U42(isList(V1),V2))	(11)
active(U42(tt,V2))	→	mark(U43(isNeList(V2)))	(12)
active(U51(tt,V1,V2))	→	mark(U52(isNeList(V1),V2))	(14)
active(U52(tt,V2))	→	mark(U53(isList(V2)))	(15)
active(U61(tt,V))	→	mark(U62(isQid(V)))	(17)
active(U71(tt,V))	→	mark(U72(isNePal(V)))	(19)
active(and(tt,X))	→	mark(X)	(21)
active(isList(V))	→	mark(U11(isPalListKind(V),V))	(22)
active(isList(nil))	→	mark(tt)	(23)
active(isList(__(V1,V2)))	→	mark(U21(and(isPalListKind(V1),isPalListKind(V2)),V1,V2))	(24)
active(isNeList(V))	→	mark(U31(isPalListKind(V),V))	(25)
active(isNeList(__(V1,V2)))	→	mark(U41(and(isPalListKind(V1),isPalListKind(V2)),V1,V2))	(26)
active(isNeList(__(V1,V2)))	→	mark(U51(and(isPalListKind(V1),isPalListKind(V2)),V1,V2))	(27)
active(isNePal(V))	→	mark(U61(isPalListKind(V),V))	(28)
active(isNePal(__(I,__(P,I))))	→	mark(and(and(isQid(I),isPalListKind(I)),and(isPal(P),isPalListKind(P))))	(29)
active(isPal(V))	→	mark(U71(isPalListKind(V),V))	(30)
active(isPal(nil))	→	mark(tt)	(31)
active(isPalListKind(a))	→	mark(tt)	(32)
active(isPalListKind(nil))	→	mark(tt)	(35)
active(isPalListKind(o))	→	mark(tt)	(36)
active(isPalListKind(__(V1,V2)))	→	mark(and(isPalListKind(V1),isPalListKind(V2)))	(38)
active(isQid(a))	→	mark(tt)	(39)
active(isQid(o))	→	mark(tt)	(42)

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[active(x₁)]	=	1 · x₁
[U12(x₁)]	=	1 + 1 · x₁
[tt]	=	1
[mark(x₁)]	=	2 · x₁
[U23(x₁)]	=	1 + 2 · x₁
[U32(x₁)]	=	1 + 2 · x₁
[U43(x₁)]	=	1 + 1 · x₁
[U53(x₁)]	=	1 + 2 · x₁
[U62(x₁)]	=	1 + 2 · x₁
[U72(x₁)]	=	1 + 2 · x₁
[isPalListKind(x₁)]	=	1 + 2 · x₁
[e]	=	1
[i]	=	1
[u]	=	1
[isQid(x₁)]	=	1 + 2 · x₁
[__(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[nil]	=	2
[U11(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[isNeList(x₁)]	=	1 + 2 · x₁
[U21(x₁, x₂, x₃)]	=	1 + 2 · x₁ + 2 · x₂ + 2 · x₃
[U22(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[isList(x₁)]	=	1 + 2 · x₁
[U31(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[U41(x₁, x₂, x₃)]	=	1 + 2 · x₁ + 2 · x₂ + 2 · x₃
[U42(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[U51(x₁, x₂, x₃)]	=	1 + 2 · x₁ + 2 · x₂ + 2 · x₃
[U52(x₁, x₂)]	=	2 + 1 · x₁ + 2 · x₂
[U61(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[U71(x₁, x₂)]	=	1 + 1 · x₁ + 2 · x₂
[isNePal(x₁)]	=	1 + 2 · x₁
[and(x₁, x₂)]	=	1 + 2 · x₁ + 2 · x₂
[isPal(x₁)]	=	1 + 2 · x₁
[a]	=	1
[o]	=	1

all of the following rules can be deleted.

active(U23(tt))	→	mark(tt)	(8)
active(U32(tt))	→	mark(tt)	(10)
active(U53(tt))	→	mark(tt)	(16)
active(U62(tt))	→	mark(tt)	(18)
active(U72(tt))	→	mark(tt)	(20)
active(isPalListKind(e))	→	mark(tt)	(33)
active(isPalListKind(i))	→	mark(tt)	(34)
active(isPalListKind(u))	→	mark(tt)	(37)
active(isQid(e))	→	mark(tt)	(40)
active(isQid(i))	→	mark(tt)	(41)
active(isQid(u))	→	mark(tt)	(43)
mark(__(X1,X2))	→	active(__(mark(X1),mark(X2)))	(44)
mark(nil)	→	active(nil)	(45)
mark(U11(X1,X2))	→	active(U11(mark(X1),X2))	(46)
mark(tt)	→	active(tt)	(47)
mark(U12(X))	→	active(U12(mark(X)))	(48)
mark(isNeList(X))	→	active(isNeList(X))	(49)
mark(U21(X1,X2,X3))	→	active(U21(mark(X1),X2,X3))	(50)
mark(U22(X1,X2))	→	active(U22(mark(X1),X2))	(51)
mark(isList(X))	→	active(isList(X))	(52)
mark(U23(X))	→	active(U23(mark(X)))	(53)
mark(U31(X1,X2))	→	active(U31(mark(X1),X2))	(54)
mark(U32(X))	→	active(U32(mark(X)))	(55)
mark(isQid(X))	→	active(isQid(X))	(56)
mark(U41(X1,X2,X3))	→	active(U41(mark(X1),X2,X3))	(57)
mark(U42(X1,X2))	→	active(U42(mark(X1),X2))	(58)
mark(U43(X))	→	active(U43(mark(X)))	(59)
mark(U51(X1,X2,X3))	→	active(U51(mark(X1),X2,X3))	(60)
mark(U52(X1,X2))	→	active(U52(mark(X1),X2))	(61)
mark(U53(X))	→	active(U53(mark(X)))	(62)
mark(U61(X1,X2))	→	active(U61(mark(X1),X2))	(63)
mark(U62(X))	→	active(U62(mark(X)))	(64)
mark(U71(X1,X2))	→	active(U71(mark(X1),X2))	(65)
mark(U72(X))	→	active(U72(mark(X)))	(66)
mark(isNePal(X))	→	active(isNePal(X))	(67)
mark(and(X1,X2))	→	active(and(mark(X1),X2))	(68)
mark(isPalListKind(X))	→	active(isPalListKind(X))	(69)
mark(isPal(X))	→	active(isPal(X))	(70)
mark(a)	→	active(a)	(71)
mark(e)	→	active(e)	(72)
mark(i)	→	active(i)	(73)
mark(o)	→	active(o)	(74)
mark(u)	→	active(u)	(75)

1.1.1 Rule Removal

Using the Knuth Bendix order with w0 = 1 and the following precedence and weight functions

prec(tt)	=	1	weight(tt)	=	1
prec(active)	=	27	weight(active)	=	0
prec(U12)	=	0	weight(U12)	=	1
prec(mark)	=	2	weight(mark)	=	1
prec(U43)	=	3	weight(U43)	=	1
prec(isNeList)	=	6	weight(isNeList)	=	1
prec(isList)	=	9	weight(isList)	=	1
prec(U23)	=	10	weight(U23)	=	1
prec(U32)	=	12	weight(U32)	=	1
prec(isQid)	=	13	weight(isQid)	=	1
prec(U53)	=	18	weight(U53)	=	1
prec(U62)	=	20	weight(U62)	=	1
prec(U72)	=	22	weight(U72)	=	1
prec(isNePal)	=	23	weight(isNePal)	=	1
prec(isPalListKind)	=	25	weight(isPalListKind)	=	1
prec(isPal)	=	26	weight(isPal)	=	1
prec(__)	=	4	weight(__)	=	0
prec(U11)	=	5	weight(U11)	=	0
prec(U21)	=	7	weight(U21)	=	0
prec(U22)	=	8	weight(U22)	=	0
prec(U31)	=	11	weight(U31)	=	0
prec(U41)	=	14	weight(U41)	=	0
prec(U42)	=	15	weight(U42)	=	0
prec(U51)	=	16	weight(U51)	=	0
prec(U52)	=	17	weight(U52)	=	0
prec(U61)	=	19	weight(U61)	=	0
prec(U71)	=	21	weight(U71)	=	0
prec(and)	=	24	weight(and)	=	0

all of the following rules can be deleted.

active(U12(tt))	→	mark(tt)	(5)
active(U43(tt))	→	mark(tt)	(13)
__(mark(X1),X2)	→	__(X1,X2)	(76)
__(X1,mark(X2))	→	__(X1,X2)	(77)
__(active(X1),X2)	→	__(X1,X2)	(78)
__(X1,active(X2))	→	__(X1,X2)	(79)
U11(mark(X1),X2)	→	U11(X1,X2)	(80)
U11(X1,mark(X2))	→	U11(X1,X2)	(81)
U11(active(X1),X2)	→	U11(X1,X2)	(82)
U11(X1,active(X2))	→	U11(X1,X2)	(83)
U12(mark(X))	→	U12(X)	(84)
U12(active(X))	→	U12(X)	(85)
isNeList(mark(X))	→	isNeList(X)	(86)
isNeList(active(X))	→	isNeList(X)	(87)
U21(mark(X1),X2,X3)	→	U21(X1,X2,X3)	(88)
U21(X1,mark(X2),X3)	→	U21(X1,X2,X3)	(89)
U21(X1,X2,mark(X3))	→	U21(X1,X2,X3)	(90)
U21(active(X1),X2,X3)	→	U21(X1,X2,X3)	(91)
U21(X1,active(X2),X3)	→	U21(X1,X2,X3)	(92)
U21(X1,X2,active(X3))	→	U21(X1,X2,X3)	(93)
U22(mark(X1),X2)	→	U22(X1,X2)	(94)
U22(X1,mark(X2))	→	U22(X1,X2)	(95)
U22(active(X1),X2)	→	U22(X1,X2)	(96)
U22(X1,active(X2))	→	U22(X1,X2)	(97)
isList(mark(X))	→	isList(X)	(98)
isList(active(X))	→	isList(X)	(99)
U23(mark(X))	→	U23(X)	(100)
U23(active(X))	→	U23(X)	(101)
U31(mark(X1),X2)	→	U31(X1,X2)	(102)
U31(X1,mark(X2))	→	U31(X1,X2)	(103)
U31(active(X1),X2)	→	U31(X1,X2)	(104)
U31(X1,active(X2))	→	U31(X1,X2)	(105)
U32(mark(X))	→	U32(X)	(106)
U32(active(X))	→	U32(X)	(107)
isQid(mark(X))	→	isQid(X)	(108)
isQid(active(X))	→	isQid(X)	(109)
U41(mark(X1),X2,X3)	→	U41(X1,X2,X3)	(110)
U41(X1,mark(X2),X3)	→	U41(X1,X2,X3)	(111)
U41(X1,X2,mark(X3))	→	U41(X1,X2,X3)	(112)
U41(active(X1),X2,X3)	→	U41(X1,X2,X3)	(113)
U41(X1,active(X2),X3)	→	U41(X1,X2,X3)	(114)
U41(X1,X2,active(X3))	→	U41(X1,X2,X3)	(115)
U42(mark(X1),X2)	→	U42(X1,X2)	(116)
U42(X1,mark(X2))	→	U42(X1,X2)	(117)
U42(active(X1),X2)	→	U42(X1,X2)	(118)
U42(X1,active(X2))	→	U42(X1,X2)	(119)
U43(mark(X))	→	U43(X)	(120)
U43(active(X))	→	U43(X)	(121)
U51(mark(X1),X2,X3)	→	U51(X1,X2,X3)	(122)
U51(X1,mark(X2),X3)	→	U51(X1,X2,X3)	(123)
U51(X1,X2,mark(X3))	→	U51(X1,X2,X3)	(124)
U51(active(X1),X2,X3)	→	U51(X1,X2,X3)	(125)
U51(X1,active(X2),X3)	→	U51(X1,X2,X3)	(126)
U51(X1,X2,active(X3))	→	U51(X1,X2,X3)	(127)
U52(mark(X1),X2)	→	U52(X1,X2)	(128)
U52(X1,mark(X2))	→	U52(X1,X2)	(129)
U52(active(X1),X2)	→	U52(X1,X2)	(130)
U52(X1,active(X2))	→	U52(X1,X2)	(131)
U53(mark(X))	→	U53(X)	(132)
U53(active(X))	→	U53(X)	(133)
U61(mark(X1),X2)	→	U61(X1,X2)	(134)
U61(X1,mark(X2))	→	U61(X1,X2)	(135)
U61(active(X1),X2)	→	U61(X1,X2)	(136)
U61(X1,active(X2))	→	U61(X1,X2)	(137)
U62(mark(X))	→	U62(X)	(138)
U62(active(X))	→	U62(X)	(139)
U71(mark(X1),X2)	→	U71(X1,X2)	(140)
U71(X1,mark(X2))	→	U71(X1,X2)	(141)
U71(active(X1),X2)	→	U71(X1,X2)	(142)
U71(X1,active(X2))	→	U71(X1,X2)	(143)
U72(mark(X))	→	U72(X)	(144)
U72(active(X))	→	U72(X)	(145)
isNePal(mark(X))	→	isNePal(X)	(146)
isNePal(active(X))	→	isNePal(X)	(147)
and(mark(X1),X2)	→	and(X1,X2)	(148)
and(X1,mark(X2))	→	and(X1,X2)	(149)
and(active(X1),X2)	→	and(X1,X2)	(150)
and(X1,active(X2))	→	and(X1,X2)	(151)
isPalListKind(mark(X))	→	isPalListKind(X)	(152)
isPalListKind(active(X))	→	isPalListKind(X)	(153)
isPal(mark(X))	→	isPal(X)	(154)
isPal(active(X))	→	isPal(X)	(155)

1.1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.