Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PALINDROME_nokinds_iGM)

The rewrite relation of the following TRS is considered.

active(__(__(X,Y),Z))	→	mark(__(X,__(Y,Z)))	(1)
active(__(X,nil))	→	mark(X)	(2)
active(__(nil,X))	→	mark(X)	(3)
active(and(tt,X))	→	mark(X)	(4)
active(isList(V))	→	mark(isNeList(V))	(5)
active(isList(nil))	→	mark(tt)	(6)
active(isList(__(V1,V2)))	→	mark(and(isList(V1),isList(V2)))	(7)
active(isNeList(V))	→	mark(isQid(V))	(8)
active(isNeList(__(V1,V2)))	→	mark(and(isList(V1),isNeList(V2)))	(9)
active(isNeList(__(V1,V2)))	→	mark(and(isNeList(V1),isList(V2)))	(10)
active(isNePal(V))	→	mark(isQid(V))	(11)
active(isNePal(__(I,__(P,I))))	→	mark(and(isQid(I),isPal(P)))	(12)
active(isPal(V))	→	mark(isNePal(V))	(13)
active(isPal(nil))	→	mark(tt)	(14)
active(isQid(a))	→	mark(tt)	(15)
active(isQid(e))	→	mark(tt)	(16)
active(isQid(i))	→	mark(tt)	(17)
active(isQid(o))	→	mark(tt)	(18)
active(isQid(u))	→	mark(tt)	(19)
mark(__(X1,X2))	→	active(__(mark(X1),mark(X2)))	(20)
mark(nil)	→	active(nil)	(21)
mark(and(X1,X2))	→	active(and(mark(X1),X2))	(22)
mark(tt)	→	active(tt)	(23)
mark(isList(X))	→	active(isList(X))	(24)
mark(isNeList(X))	→	active(isNeList(X))	(25)
mark(isQid(X))	→	active(isQid(X))	(26)
mark(isNePal(X))	→	active(isNePal(X))	(27)
mark(isPal(X))	→	active(isPal(X))	(28)
mark(a)	→	active(a)	(29)
mark(e)	→	active(e)	(30)
mark(i)	→	active(i)	(31)
mark(o)	→	active(o)	(32)
mark(u)	→	active(u)	(33)
__(mark(X1),X2)	→	__(X1,X2)	(34)
__(X1,mark(X2))	→	__(X1,X2)	(35)
__(active(X1),X2)	→	__(X1,X2)	(36)
__(X1,active(X2))	→	__(X1,X2)	(37)
and(mark(X1),X2)	→	and(X1,X2)	(38)
and(X1,mark(X2))	→	and(X1,X2)	(39)
and(active(X1),X2)	→	and(X1,X2)	(40)
and(X1,active(X2))	→	and(X1,X2)	(41)
isList(mark(X))	→	isList(X)	(42)
isList(active(X))	→	isList(X)	(43)
isNeList(mark(X))	→	isNeList(X)	(44)
isNeList(active(X))	→	isNeList(X)	(45)
isQid(mark(X))	→	isQid(X)	(46)
isQid(active(X))	→	isQid(X)	(47)
isNePal(mark(X))	→	isNePal(X)	(48)
isNePal(active(X))	→	isNePal(X)	(49)
isPal(mark(X))	→	isPal(X)	(50)
isPal(active(X))	→	isPal(X)	(51)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over the naturals

[active(x₁)]	=	1 · x₁
[__(x₁, x₂)]	=	2 + 2 · x₁ + 1 · x₂
[mark(x₁)]	=	1 · x₁
[nil]	=	0
[and(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[tt]	=	0
[isList(x₁)]	=	2 + 1 · x₁
[isNeList(x₁)]	=	1 · x₁
[isQid(x₁)]	=	1 · x₁
[isNePal(x₁)]	=	1 · x₁
[isPal(x₁)]	=	2 · x₁
[a]	=	2
[e]	=	0
[i]	=	1
[o]	=	1
[u]	=	0

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(isList(V))	→	mark(isNeList(V))	(5)
active(isList(nil))	→	mark(tt)	(6)
active(isNePal(__(I,__(P,I))))	→	mark(and(isQid(I),isPal(P)))	(12)
active(isQid(a))	→	mark(tt)	(15)
active(isQid(i))	→	mark(tt)	(17)
active(isQid(o))	→	mark(tt)	(18)

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[active(x₁)]	=	1 · x₁
[and(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[tt]	=	0
[mark(x₁)]	=	1 · x₁
[isList(x₁)]	=	1 · x₁
[__(x₁, x₂)]	=	2 · x₁ + 1 · x₂
[isNeList(x₁)]	=	1 · x₁
[isQid(x₁)]	=	1 · x₁
[isNePal(x₁)]	=	2 · x₁
[isPal(x₁)]	=	2 · x₁
[nil]	=	0
[e]	=	2
[u]	=	0
[a]	=	0
[i]	=	0
[o]	=	0

all of the following rules can be deleted.

active(isQid(e))

→

mark(tt)

(16)

1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[active(x₁)]	=	1 · x₁
[and(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[tt]	=	2
[mark(x₁)]	=	1 · x₁
[isList(x₁)]	=	1 + 2 · x₁
[__(x₁, x₂)]	=	2 + 2 · x₁ + 1 · x₂
[isNeList(x₁)]	=	1 + 2 · x₁
[isQid(x₁)]	=	2 · x₁
[isNePal(x₁)]	=	2 + 2 · x₁
[isPal(x₁)]	=	2 + 2 · x₁
[nil]	=	2
[u]	=	2
[a]	=	0
[e]	=	0
[i]	=	0
[o]	=	0

all of the following rules can be deleted.

active(and(tt,X))	→	mark(X)	(4)
active(isList(__(V1,V2)))	→	mark(and(isList(V1),isList(V2)))	(7)
active(isNeList(V))	→	mark(isQid(V))	(8)
active(isNeList(__(V1,V2)))	→	mark(and(isList(V1),isNeList(V2)))	(9)
active(isNeList(__(V1,V2)))	→	mark(and(isNeList(V1),isList(V2)))	(10)
active(isNePal(V))	→	mark(isQid(V))	(11)
active(isPal(nil))	→	mark(tt)	(14)
active(isQid(u))	→	mark(tt)	(19)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[active(x₁)]	=	1 · x₁
[isPal(x₁)]	=	2 + 1 · x₁
[mark(x₁)]	=	1 · x₁
[isNePal(x₁)]	=	1 + 1 · x₁
[__(x₁, x₂)]	=	2 · x₁ + 2 · x₂
[nil]	=	0
[and(x₁, x₂)]	=	1 · x₁ + 1 · x₂
[tt]	=	0
[isList(x₁)]	=	2 · x₁
[isNeList(x₁)]	=	2 · x₁
[isQid(x₁)]	=	2 · x₁
[a]	=	0
[e]	=	0
[i]	=	0
[o]	=	0
[u]	=	0

all of the following rules can be deleted.

active(isPal(V))

→

mark(isNePal(V))

(13)

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals

[mark(x₁)]	=	1 + 2 · x₁
[__(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[active(x₁)]	=	1 · x₁
[nil]	=	2
[and(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[tt]	=	2
[isList(x₁)]	=	2 + 1 · x₁
[isNeList(x₁)]	=	2 + 1 · x₁
[isQid(x₁)]	=	2 + 1 · x₁
[isNePal(x₁)]	=	2 + 1 · x₁
[isPal(x₁)]	=	2 + 1 · x₁
[a]	=	2
[e]	=	2
[i]	=	2
[o]	=	1
[u]	=	2

all of the following rules can be deleted.

mark(__(X1,X2))	→	active(__(mark(X1),mark(X2)))	(20)
mark(nil)	→	active(nil)	(21)
mark(and(X1,X2))	→	active(and(mark(X1),X2))	(22)
mark(tt)	→	active(tt)	(23)
mark(isList(X))	→	active(isList(X))	(24)
mark(isNeList(X))	→	active(isNeList(X))	(25)
mark(isQid(X))	→	active(isQid(X))	(26)
mark(isNePal(X))	→	active(isNePal(X))	(27)
mark(isPal(X))	→	active(isPal(X))	(28)
mark(a)	→	active(a)	(29)
mark(e)	→	active(e)	(30)
mark(i)	→	active(i)	(31)
mark(o)	→	active(o)	(32)
mark(u)	→	active(u)	(33)
__(mark(X1),X2)	→	__(X1,X2)	(34)
__(X1,mark(X2))	→	__(X1,X2)	(35)
and(mark(X1),X2)	→	and(X1,X2)	(38)
and(X1,mark(X2))	→	and(X1,X2)	(39)
isList(mark(X))	→	isList(X)	(42)
isNeList(mark(X))	→	isNeList(X)	(44)
isQid(mark(X))	→	isQid(X)	(46)
isNePal(mark(X))	→	isNePal(X)	(48)
isPal(mark(X))	→	isPal(X)	(50)

1.1.1.1.1.1 Rule Removal

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

prec(active)	=	7	weight(active)	=	0
prec(isList)	=	2	weight(isList)	=	1
prec(isNeList)	=	3	weight(isNeList)	=	1
prec(isQid)	=	4	weight(isQid)	=	1
prec(isNePal)	=	5	weight(isNePal)	=	1
prec(isPal)	=	6	weight(isPal)	=	1
prec(__)	=	0	weight(__)	=	0
prec(and)	=	1	weight(and)	=	0

all of the following rules can be deleted.

__(active(X1),X2)	→	__(X1,X2)	(36)
__(X1,active(X2))	→	__(X1,X2)	(37)
and(active(X1),X2)	→	and(X1,X2)	(40)
and(X1,active(X2))	→	and(X1,X2)	(41)
isList(active(X))	→	isList(X)	(43)
isNeList(active(X))	→	isNeList(X)	(45)
isQid(active(X))	→	isQid(X)	(47)
isNePal(active(X))	→	isNePal(X)	(49)
isPal(active(X))	→	isPal(X)	(51)

1.1.1.1.1.1.1 R is empty

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