Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PALINDROME_nosorts_noand_C)

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(U11(tt))	→	mark(U12(tt))	(4)
active(U12(tt))	→	mark(tt)	(5)
active(isNePal(__(I,__(P,I))))	→	mark(U11(tt))	(6)
active(__(X1,X2))	→	__(active(X1),X2)	(7)
active(__(X1,X2))	→	__(X1,active(X2))	(8)
active(U11(X))	→	U11(active(X))	(9)
active(U12(X))	→	U12(active(X))	(10)
active(isNePal(X))	→	isNePal(active(X))	(11)
__(mark(X1),X2)	→	mark(__(X1,X2))	(12)
__(X1,mark(X2))	→	mark(__(X1,X2))	(13)
U11(mark(X))	→	mark(U11(X))	(14)
U12(mark(X))	→	mark(U12(X))	(15)
isNePal(mark(X))	→	mark(isNePal(X))	(16)
proper(__(X1,X2))	→	__(proper(X1),proper(X2))	(17)
proper(nil)	→	ok(nil)	(18)
proper(U11(X))	→	U11(proper(X))	(19)
proper(tt)	→	ok(tt)	(20)
proper(U12(X))	→	U12(proper(X))	(21)
proper(isNePal(X))	→	isNePal(proper(X))	(22)
__(ok(X1),ok(X2))	→	ok(__(X1,X2))	(23)
U11(ok(X))	→	ok(U11(X))	(24)
U12(ok(X))	→	ok(U12(X))	(25)
isNePal(ok(X))	→	ok(isNePal(X))	(26)
top(mark(X))	→	top(proper(X))	(27)
top(ok(X))	→	top(active(X))	(28)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

__^#(X1,mark(X2))	→	__^#(X1,X2)	(29)
proper^#(U12(X))	→	proper^#(X)	(30)
U12^#(mark(X))	→	U12^#(X)	(31)
active^#(isNePal(X))	→	active^#(X)	(32)
active^#(__(X1,X2))	→	active^#(X1)	(33)
__^#(mark(X1),X2)	→	__^#(X1,X2)	(34)
U12^#(ok(X))	→	U12^#(X)	(35)
proper^#(__(X1,X2))	→	proper^#(X2)	(36)
proper^#(__(X1,X2))	→	proper^#(X1)	(37)
active^#(__(X1,X2))	→	__^#(active(X1),X2)	(38)
active^#(__(__(X,Y),Z))	→	__^#(X,__(Y,Z))	(39)
active^#(U12(X))	→	U12^#(active(X))	(40)
isNePal^#(mark(X))	→	isNePal^#(X)	(41)
proper^#(U11(X))	→	U11^#(proper(X))	(42)
top^#(mark(X))	→	top^#(proper(X))	(43)
U11^#(ok(X))	→	U11^#(X)	(44)
U11^#(mark(X))	→	U11^#(X)	(45)
active^#(__(X1,X2))	→	__^#(X1,active(X2))	(46)
active^#(isNePal(X))	→	isNePal^#(active(X))	(47)
proper^#(U12(X))	→	U12^#(proper(X))	(48)
proper^#(__(X1,X2))	→	__^#(proper(X1),proper(X2))	(49)
active^#(__(X1,X2))	→	active^#(X2)	(50)
isNePal^#(ok(X))	→	isNePal^#(X)	(51)
top^#(ok(X))	→	active^#(X)	(52)
active^#(__(__(X,Y),Z))	→	__^#(Y,Z)	(53)
proper^#(isNePal(X))	→	proper^#(X)	(54)
proper^#(U11(X))	→	proper^#(X)	(55)
active^#(U11(tt))	→	U12^#(tt)	(56)
top^#(mark(X))	→	proper^#(X)	(57)
top^#(ok(X))	→	top^#(active(X))	(58)
active^#(U11(X))	→	U11^#(active(X))	(59)
active^#(isNePal(__(I,__(P,I))))	→	U11^#(tt)	(60)
__^#(ok(X1),ok(X2))	→	__^#(X1,X2)	(61)
active^#(U12(X))	→	active^#(X)	(62)
active^#(U11(X))	→	active^#(X)	(63)
proper^#(isNePal(X))	→	isNePal^#(proper(X))	(64)

1.1 Dependency Graph Processor

The dependency pairs are split into 7 components.

The 1^st component contains the pair

top^#(ok(X))	→	top^#(active(X))	(58)
top^#(mark(X))	→	top^#(proper(X))	(43)

1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(top^#)	=	1
π(__^#)	=	1
π(isNePal)	=	1
π(U12^#)	=	1
π(proper)	=	1
π(ok)	=	1
π(active)	=	1

in combination with the following Weighted Path Order with the following precedence and status

prec(U11)	=	2	status(U11)	=	[1]	list-extension(U11)	=	Lex
prec(top)	=	0	status(top)	=	[]	list-extension(top)	=	Lex
prec(U12)	=	1	status(U12)	=	[1]	list-extension(U12)	=	Lex
prec(isNePal^#)	=	0	status(isNePal^#)	=	[]	list-extension(isNePal^#)	=	Lex
prec(nil)	=	0	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(mark)	=	1	status(mark)	=	[1]	list-extension(mark)	=	Lex
prec(proper^#)	=	0	status(proper^#)	=	[]	list-extension(proper^#)	=	Lex
prec(U11^#)	=	0	status(U11^#)	=	[]	list-extension(U11^#)	=	Lex
prec(active^#)	=	0	status(active^#)	=	[]	list-extension(active^#)	=	Lex
prec(tt)	=	3	status(tt)	=	[]	list-extension(tt)	=	Lex
prec(__)	=	5	status(__)	=	[1, 2]	list-extension(__)	=	Lex

and the following Max-polynomial interpretation

[U11(x₁)]	=	x₁ + 0
[top(x₁)]	=	0
[U12(x₁)]	=	x₁ + 0
[isNePal^#(x₁)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 0
[proper^#(x₁)]	=	0
[U11^#(x₁)]	=	0
[active^#(x₁)]	=	0
[tt]	=	0
[__(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)

together with the usable rules

proper(nil)	→	ok(nil)	(18)
active(U11(tt))	→	mark(U12(tt))	(4)
U12(mark(X))	→	mark(U12(X))	(15)
active(__(X1,X2))	→	__(X1,active(X2))	(8)
active(__(__(X,Y),Z))	→	mark(__(X,__(Y,Z)))	(1)
active(__(nil,X))	→	mark(X)	(3)
isNePal(mark(X))	→	mark(isNePal(X))	(16)
proper(U12(X))	→	U12(proper(X))	(21)
isNePal(ok(X))	→	ok(isNePal(X))	(26)
proper(U11(X))	→	U11(proper(X))	(19)
proper(__(X1,X2))	→	__(proper(X1),proper(X2))	(17)
proper(isNePal(X))	→	isNePal(proper(X))	(22)
active(U12(tt))	→	mark(tt)	(5)
active(U12(X))	→	U12(active(X))	(10)
active(__(X1,X2))	→	__(active(X1),X2)	(7)
proper(tt)	→	ok(tt)	(20)
U12(ok(X))	→	ok(U12(X))	(25)
U11(mark(X))	→	mark(U11(X))	(14)
__(mark(X1),X2)	→	mark(__(X1,X2))	(12)
__(ok(X1),ok(X2))	→	ok(__(X1,X2))	(23)
U11(ok(X))	→	ok(U11(X))	(24)
active(isNePal(X))	→	isNePal(active(X))	(11)
active(U11(X))	→	U11(active(X))	(9)
__(X1,mark(X2))	→	mark(__(X1,X2))	(13)
active(isNePal(__(I,__(P,I))))	→	mark(U11(tt))	(6)
active(__(X,nil))	→	mark(X)	(2)

(w.r.t. the implicit argument filter of the reduction pair), the pair

top^#(mark(X))

→

top^#(proper(X))

(43)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

top^#(ok(X))

→

top^#(active(X))

(58)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁)]	=	x₁ + 0
[top(x₁)]	=	0
[top^#(x₁)]	=	x₁ + 0
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	x₁ + 0
[U12(x₁)]	=	x₁ + 0
[U12^#(x₁)]	=	0
[proper(x₁)]	=	48699
[ok(x₁)]	=	x₁ + 30802
[isNePal^#(x₁)]	=	0
[nil]	=	15261
[mark(x₁)]	=	0
[proper^#(x₁)]	=	0
[U11^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 30801
[active^#(x₁)]	=	0
[tt]	=	17897
[__(x₁, x₂)]	=	x₂ + 0

together with the usable rules

proper(nil)	→	ok(nil)	(18)
active(U11(tt))	→	mark(U12(tt))	(4)
U12(mark(X))	→	mark(U12(X))	(15)
active(__(X1,X2))	→	__(X1,active(X2))	(8)
active(__(__(X,Y),Z))	→	mark(__(X,__(Y,Z)))	(1)
active(__(nil,X))	→	mark(X)	(3)
isNePal(mark(X))	→	mark(isNePal(X))	(16)
proper(U12(X))	→	U12(proper(X))	(21)
isNePal(ok(X))	→	ok(isNePal(X))	(26)
proper(U11(X))	→	U11(proper(X))	(19)
proper(__(X1,X2))	→	__(proper(X1),proper(X2))	(17)
proper(isNePal(X))	→	isNePal(proper(X))	(22)
active(U12(tt))	→	mark(tt)	(5)
active(U12(X))	→	U12(active(X))	(10)
active(__(X1,X2))	→	__(active(X1),X2)	(7)
proper(tt)	→	ok(tt)	(20)
U12(ok(X))	→	ok(U12(X))	(25)
U11(mark(X))	→	mark(U11(X))	(14)
__(mark(X1),X2)	→	mark(__(X1,X2))	(12)
__(ok(X1),ok(X2))	→	ok(__(X1,X2))	(23)
U11(ok(X))	→	ok(U11(X))	(24)
active(isNePal(X))	→	isNePal(active(X))	(11)
active(U11(X))	→	U11(active(X))	(9)
__(X1,mark(X2))	→	mark(__(X1,X2))	(13)
active(isNePal(__(I,__(P,I))))	→	mark(U11(tt))	(6)
active(__(X,nil))	→	mark(X)	(2)

(w.r.t. the implicit argument filter of the reduction pair), the pair

top^#(ok(X))

→

top^#(active(X))

(58)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

active^#(U11(X))	→	active^#(X)	(63)
active^#(U12(X))	→	active^#(X)	(62)
active^#(__(X1,X2))	→	active^#(X1)	(33)
active^#(isNePal(X))	→	active^#(X)	(32)
active^#(__(X1,X2))	→	active^#(X2)	(50)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	x₁ + 1
[U12(x₁)]	=	x₁ + 1
[U12^#(x₁)]	=	0
[proper(x₁)]	=	899
[ok(x₁)]	=	x₁ + 24198
[isNePal^#(x₁)]	=	0
[nil]	=	28938
[mark(x₁)]	=	x₁ + 19045
[proper^#(x₁)]	=	0
[U11^#(x₁)]	=	0
[active(x₁)]	=	19044
[active^#(x₁)]	=	x₁ + 0
[tt]	=	1
[__(x₁, x₂)]	=	x₁ + x₂ + 1

together with the usable rules

U12(mark(X))	→	mark(U12(X))	(15)
U12(ok(X))	→	ok(U12(X))	(25)
__(mark(X1),X2)	→	mark(__(X1,X2))	(12)
__(ok(X1),ok(X2))	→	ok(__(X1,X2))	(23)
__(X1,mark(X2))	→	mark(__(X1,X2))	(13)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

active^#(U11(X))	→	active^#(X)	(63)
active^#(U12(X))	→	active^#(X)	(62)
active^#(__(X1,X2))	→	active^#(X1)	(33)
active^#(isNePal(X))	→	active^#(X)	(32)
active^#(__(X1,X2))	→	active^#(X2)	(50)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

proper^#(__(X1,X2))	→	proper^#(X1)	(37)
proper^#(__(X1,X2))	→	proper^#(X2)	(36)
proper^#(U11(X))	→	proper^#(X)	(55)
proper^#(isNePal(X))	→	proper^#(X)	(54)
proper^#(U12(X))	→	proper^#(X)	(30)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	x₁ + 1
[U12(x₁)]	=	x₁ + 1
[U12^#(x₁)]	=	0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 1
[isNePal^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 2
[proper^#(x₁)]	=	x₁ + 0
[U11^#(x₁)]	=	0
[active(x₁)]	=	1
[active^#(x₁)]	=	0
[tt]	=	1
[__(x₁, x₂)]	=	x₁ + x₂ + 1

together with the usable rules

U12(mark(X))	→	mark(U12(X))	(15)
U12(ok(X))	→	ok(U12(X))	(25)
__(mark(X1),X2)	→	mark(__(X1,X2))	(12)
__(ok(X1),ok(X2))	→	ok(__(X1,X2))	(23)
__(X1,mark(X2))	→	mark(__(X1,X2))	(13)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

proper^#(__(X1,X2))	→	proper^#(X1)	(37)
proper^#(__(X1,X2))	→	proper^#(X2)	(36)
proper^#(U11(X))	→	proper^#(X)	(55)
proper^#(isNePal(X))	→	proper^#(X)	(54)
proper^#(U12(X))	→	proper^#(X)	(30)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 4^th component contains the pair

isNePal^#(mark(X))	→	isNePal^#(X)	(41)
isNePal^#(ok(X))	→	isNePal^#(X)	(51)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁)]	=	x₁ + 15620
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	x₁ + 24168
[U12(x₁)]	=	x₁ + 1
[U12^#(x₁)]	=	0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 12237
[isNePal^#(x₁)]	=	x₁ + 0
[nil]	=	54886
[mark(x₁)]	=	x₁ + 2
[proper^#(x₁)]	=	0
[U11^#(x₁)]	=	0
[active(x₁)]	=	1
[active^#(x₁)]	=	0
[tt]	=	1
[__(x₁, x₂)]	=	x₁ + x₂ + 1

together with the usable rules

U12(mark(X))	→	mark(U12(X))	(15)
U12(ok(X))	→	ok(U12(X))	(25)
__(mark(X1),X2)	→	mark(__(X1,X2))	(12)
__(ok(X1),ok(X2))	→	ok(__(X1,X2))	(23)
__(X1,mark(X2))	→	mark(__(X1,X2))	(13)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

isNePal^#(mark(X))	→	isNePal^#(X)	(41)
isNePal^#(ok(X))	→	isNePal^#(X)	(51)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 5^th component contains the pair

__^#(ok(X1),ok(X2))	→	__^#(X1,X2)	(61)
__^#(mark(X1),X2)	→	__^#(X1,X2)	(34)
__^#(X1,mark(X2))	→	__^#(X1,X2)	(29)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[__^#(x₁, x₂)]	=	x₁ + x₂ + 0
[isNePal(x₁)]	=	x₁ + 24168
[U12(x₁)]	=	x₁ + 1
[U12^#(x₁)]	=	0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 3566
[isNePal^#(x₁)]	=	0
[nil]	=	3247
[mark(x₁)]	=	x₁ + 2
[proper^#(x₁)]	=	0
[U11^#(x₁)]	=	0
[active(x₁)]	=	1
[active^#(x₁)]	=	0
[tt]	=	1
[__(x₁, x₂)]	=	x₁ + x₂ + 1

together with the usable rules

U12(mark(X))	→	mark(U12(X))	(15)
U12(ok(X))	→	ok(U12(X))	(25)
__(mark(X1),X2)	→	mark(__(X1,X2))	(12)
__(ok(X1),ok(X2))	→	ok(__(X1,X2))	(23)
__(X1,mark(X2))	→	mark(__(X1,X2))	(13)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

__^#(ok(X1),ok(X2))	→	__^#(X1,X2)	(61)
__^#(mark(X1),X2)	→	__^#(X1,X2)	(34)
__^#(X1,mark(X2))	→	__^#(X1,X2)	(29)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 6^th component contains the pair

U11^#(mark(X))	→	U11^#(X)	(45)
U11^#(ok(X))	→	U11^#(X)	(44)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁)]	=	x₁ + 19621
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	x₁ + 24168
[U12(x₁)]	=	x₁ + 1
[U12^#(x₁)]	=	0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 3566
[isNePal^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 3
[proper^#(x₁)]	=	0
[U11^#(x₁)]	=	x₁ + 0
[active(x₁)]	=	1
[active^#(x₁)]	=	0
[tt]	=	1
[__(x₁, x₂)]	=	x₁ + x₂ + 1

together with the usable rules

U12(mark(X))	→	mark(U12(X))	(15)
U12(ok(X))	→	ok(U12(X))	(25)
__(mark(X1),X2)	→	mark(__(X1,X2))	(12)
__(ok(X1),ok(X2))	→	ok(__(X1,X2))	(23)
__(X1,mark(X2))	→	mark(__(X1,X2))	(13)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

U11^#(mark(X))	→	U11^#(X)	(45)
U11^#(ok(X))	→	U11^#(X)	(44)

could be deleted.

1.1.6.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 7^th component contains the pair

U12^#(ok(X))	→	U12^#(X)	(35)
U12^#(mark(X))	→	U12^#(X)	(31)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁)]	=	x₁ + 1
[top(x₁)]	=	0
[top^#(x₁)]	=	0
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	x₁ + 24168
[U12(x₁)]	=	x₁ + 3578
[U12^#(x₁)]	=	x₁ + 0
[proper(x₁)]	=	1
[ok(x₁)]	=	x₁ + 3566
[isNePal^#(x₁)]	=	0
[nil]	=	1
[mark(x₁)]	=	x₁ + 2
[proper^#(x₁)]	=	0
[U11^#(x₁)]	=	0
[active(x₁)]	=	1
[active^#(x₁)]	=	0
[tt]	=	1
[__(x₁, x₂)]	=	x₁ + x₂ + 1

together with the usable rules

U12(mark(X))	→	mark(U12(X))	(15)
U12(ok(X))	→	ok(U12(X))	(25)
__(mark(X1),X2)	→	mark(__(X1,X2))	(12)
__(ok(X1),ok(X2))	→	ok(__(X1,X2))	(23)
__(X1,mark(X2))	→	mark(__(X1,X2))	(13)

(w.r.t. the implicit argument filter of the reduction pair), the pairs

U12^#(ok(X))	→	U12^#(X)	(35)
U12^#(mark(X))	→	U12^#(X)	(31)

could be deleted.

1.1.7.1 Dependency Graph Processor

The dependency pairs are split into 0 components.