Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PALINDROME_nosorts_noand_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(U11(tt))	→	mark(U12(tt))	(4)
active(U12(tt))	→	mark(tt)	(5)
active(isNePal(__(I,__(P,I))))	→	mark(U11(tt))	(6)
mark(__(X1,X2))	→	active(__(mark(X1),mark(X2)))	(7)
mark(nil)	→	active(nil)	(8)
mark(U11(X))	→	active(U11(mark(X)))	(9)
mark(tt)	→	active(tt)	(10)
mark(U12(X))	→	active(U12(mark(X)))	(11)
mark(isNePal(X))	→	active(isNePal(mark(X)))	(12)
__(mark(X1),X2)	→	__(X1,X2)	(13)
__(X1,mark(X2))	→	__(X1,X2)	(14)
__(active(X1),X2)	→	__(X1,X2)	(15)
__(X1,active(X2))	→	__(X1,X2)	(16)
U11(mark(X))	→	U11(X)	(17)
U11(active(X))	→	U11(X)	(18)
U12(mark(X))	→	U12(X)	(19)
U12(active(X))	→	U12(X)	(20)
isNePal(mark(X))	→	isNePal(X)	(21)
isNePal(active(X))	→	isNePal(X)	(22)

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.

active^#(isNePal(__(I,__(P,I))))	→	mark^#(U11(tt))	(23)
active^#(__(__(X,Y),Z))	→	__^#(X,__(Y,Z))	(24)
U11^#(active(X))	→	U11^#(X)	(25)
mark^#(U11(X))	→	U11^#(mark(X))	(26)
mark^#(isNePal(X))	→	mark^#(X)	(27)
mark^#(U12(X))	→	U12^#(mark(X))	(28)
mark^#(isNePal(X))	→	active^#(isNePal(mark(X)))	(29)
U12^#(mark(X))	→	U12^#(X)	(30)
U11^#(mark(X))	→	U11^#(X)	(31)
mark^#(isNePal(X))	→	isNePal^#(mark(X))	(32)
mark^#(nil)	→	active^#(nil)	(33)
__^#(X1,mark(X2))	→	__^#(X1,X2)	(34)
active^#(__(__(X,Y),Z))	→	__^#(Y,Z)	(35)
isNePal^#(mark(X))	→	isNePal^#(X)	(36)
mark^#(tt)	→	active^#(tt)	(37)
mark^#(U11(X))	→	mark^#(X)	(38)
mark^#(U12(X))	→	mark^#(X)	(39)
active^#(U11(tt))	→	mark^#(U12(tt))	(40)
mark^#(U11(X))	→	active^#(U11(mark(X)))	(41)
active^#(__(__(X,Y),Z))	→	mark^#(__(X,__(Y,Z)))	(42)
isNePal^#(active(X))	→	isNePal^#(X)	(43)
active^#(U11(tt))	→	U12^#(tt)	(44)
active^#(__(nil,X))	→	mark^#(X)	(45)
mark^#(__(X1,X2))	→	__^#(mark(X1),mark(X2))	(46)
__^#(active(X1),X2)	→	__^#(X1,X2)	(47)
mark^#(__(X1,X2))	→	mark^#(X2)	(48)
__^#(X1,active(X2))	→	__^#(X1,X2)	(49)
active^#(U12(tt))	→	mark^#(tt)	(50)
mark^#(__(X1,X2))	→	active^#(__(mark(X1),mark(X2)))	(51)
active^#(isNePal(__(I,__(P,I))))	→	U11^#(tt)	(52)
active^#(__(X,nil))	→	mark^#(X)	(53)
mark^#(U12(X))	→	active^#(U12(mark(X)))	(54)
U12^#(active(X))	→	U12^#(X)	(55)
__^#(mark(X1),X2)	→	__^#(X1,X2)	(56)
mark^#(__(X1,X2))	→	mark^#(X1)	(57)

1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.

The 1^st component contains the pair

mark^#(__(X1,X2))	→	mark^#(X1)	(57)
mark^#(U12(X))	→	active^#(U12(mark(X)))	(54)
active^#(__(X,nil))	→	mark^#(X)	(53)
mark^#(__(X1,X2))	→	active^#(__(mark(X1),mark(X2)))	(51)
mark^#(isNePal(X))	→	active^#(isNePal(mark(X)))	(29)
mark^#(isNePal(X))	→	mark^#(X)	(27)
mark^#(__(X1,X2))	→	mark^#(X2)	(48)
active^#(__(nil,X))	→	mark^#(X)	(45)
active^#(__(__(X,Y),Z))	→	mark^#(__(X,__(Y,Z)))	(42)
mark^#(U11(X))	→	active^#(U11(mark(X)))	(41)
active^#(U11(tt))	→	mark^#(U12(tt))	(40)
mark^#(U12(X))	→	mark^#(X)	(39)
mark^#(U11(X))	→	mark^#(X)	(38)
active^#(isNePal(__(I,__(P,I))))	→	mark^#(U11(tt))	(23)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁)]	=	x₁ + 26634
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	x₁ + 28740
[U12(x₁)]	=	x₁ + 26633
[U12^#(x₁)]	=	0
[mark^#(x₁)]	=	x₁ + 0
[isNePal^#(x₁)]	=	0
[nil]	=	50866
[mark(x₁)]	=	x₁ + 0
[U11^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 0
[active^#(x₁)]	=	x₁ + 0
[tt]	=	3287
[__(x₁, x₂)]	=	x₁ + x₂ + 591

together with the usable rules

U11(active(X))	→	U11(X)	(18)
active(U11(tt))	→	mark(U12(tt))	(4)
__(active(X1),X2)	→	__(X1,X2)	(15)
mark(nil)	→	active(nil)	(8)
active(__(__(X,Y),Z))	→	mark(__(X,__(Y,Z)))	(1)
active(__(nil,X))	→	mark(X)	(3)
__(X1,active(X2))	→	__(X1,X2)	(16)
isNePal(mark(X))	→	isNePal(X)	(21)
U12(mark(X))	→	U12(X)	(19)
U11(mark(X))	→	U11(X)	(17)
isNePal(active(X))	→	isNePal(X)	(22)
active(U12(tt))	→	mark(tt)	(5)
mark(tt)	→	active(tt)	(10)
mark(__(X1,X2))	→	active(__(mark(X1),mark(X2)))	(7)
U12(active(X))	→	U12(X)	(20)
__(X1,mark(X2))	→	__(X1,X2)	(14)
mark(isNePal(X))	→	active(isNePal(mark(X)))	(12)
mark(U12(X))	→	active(U12(mark(X)))	(11)
mark(U11(X))	→	active(U11(mark(X)))	(9)
__(mark(X1),X2)	→	__(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 pairs

mark^#(__(X1,X2))	→	mark^#(X1)	(57)
active^#(__(X,nil))	→	mark^#(X)	(53)
mark^#(isNePal(X))	→	mark^#(X)	(27)
mark^#(__(X1,X2))	→	mark^#(X2)	(48)
active^#(__(nil,X))	→	mark^#(X)	(45)
active^#(U11(tt))	→	mark^#(U12(tt))	(40)
mark^#(U12(X))	→	mark^#(X)	(39)
mark^#(U11(X))	→	mark^#(X)	(38)
active^#(isNePal(__(I,__(P,I))))	→	mark^#(U11(tt))	(23)

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

active^#(__(__(X,Y),Z))	→	mark^#(__(X,__(Y,Z)))	(42)
mark^#(__(X1,X2))	→	active^#(__(mark(X1),mark(X2)))	(51)
mark^#(isNePal(X))	→	active^#(isNePal(mark(X)))	(29)
mark^#(U12(X))	→	active^#(U12(mark(X)))	(54)
mark^#(U11(X))	→	active^#(U11(mark(X)))	(41)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁)]	=	4709
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	1
[U12(x₁)]	=	7630
[U12^#(x₁)]	=	0
[mark^#(x₁)]	=	24697
[isNePal^#(x₁)]	=	0
[nil]	=	51457
[mark(x₁)]	=	1
[U11^#(x₁)]	=	0
[active(x₁)]	=	1
[active^#(x₁)]	=	x₁ + 0
[tt]	=	1
[__(x₁, x₂)]	=	24697

together with the usable rules

U11(active(X))	→	U11(X)	(18)
active(U11(tt))	→	mark(U12(tt))	(4)
__(active(X1),X2)	→	__(X1,X2)	(15)
mark(nil)	→	active(nil)	(8)
active(__(__(X,Y),Z))	→	mark(__(X,__(Y,Z)))	(1)
active(__(nil,X))	→	mark(X)	(3)
__(X1,active(X2))	→	__(X1,X2)	(16)
isNePal(mark(X))	→	isNePal(X)	(21)
U12(mark(X))	→	U12(X)	(19)
U11(mark(X))	→	U11(X)	(17)
isNePal(active(X))	→	isNePal(X)	(22)
active(U12(tt))	→	mark(tt)	(5)
mark(tt)	→	active(tt)	(10)
mark(__(X1,X2))	→	active(__(mark(X1),mark(X2)))	(7)
U12(active(X))	→	U12(X)	(20)
__(X1,mark(X2))	→	__(X1,X2)	(14)
mark(isNePal(X))	→	active(isNePal(mark(X)))	(12)
mark(U12(X))	→	active(U12(mark(X)))	(11)
mark(U11(X))	→	active(U11(mark(X)))	(9)
__(mark(X1),X2)	→	__(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 pairs

mark^#(isNePal(X))	→	active^#(isNePal(mark(X)))	(29)
mark^#(U12(X))	→	active^#(U12(mark(X)))	(54)
mark^#(U11(X))	→	active^#(U11(mark(X)))	(41)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

active^#(__(__(X,Y),Z))	→	mark^#(__(X,__(Y,Z)))	(42)
mark^#(__(X1,X2))	→	active^#(__(mark(X1),mark(X2)))	(51)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(__^#)	=	1
π(U12)	=	1
π(mark)	=	1
π(active)	=	1

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

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

and the following Max-polynomial interpretation

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

together with the usable rules

U11(active(X))	→	U11(X)	(18)
active(U11(tt))	→	mark(U12(tt))	(4)
__(active(X1),X2)	→	__(X1,X2)	(15)
mark(nil)	→	active(nil)	(8)
active(__(__(X,Y),Z))	→	mark(__(X,__(Y,Z)))	(1)
active(__(nil,X))	→	mark(X)	(3)
__(X1,active(X2))	→	__(X1,X2)	(16)
isNePal(mark(X))	→	isNePal(X)	(21)
U12(mark(X))	→	U12(X)	(19)
U11(mark(X))	→	U11(X)	(17)
isNePal(active(X))	→	isNePal(X)	(22)
active(U12(tt))	→	mark(tt)	(5)
mark(tt)	→	active(tt)	(10)
mark(__(X1,X2))	→	active(__(mark(X1),mark(X2)))	(7)
U12(active(X))	→	U12(X)	(20)
__(X1,mark(X2))	→	__(X1,X2)	(14)
mark(isNePal(X))	→	active(isNePal(mark(X)))	(12)
mark(U12(X))	→	active(U12(mark(X)))	(11)
mark(U11(X))	→	active(U11(mark(X)))	(9)
__(mark(X1),X2)	→	__(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

active^#(__(__(X,Y),Z))

→

mark^#(__(X,__(Y,Z)))

(42)

could be deleted.

1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

U11^#(mark(X))	→	U11^#(X)	(31)
U11^#(active(X))	→	U11^#(X)	(25)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁)]	=	x₁ + 15261
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	21387
[U12(x₁)]	=	x₁ + 15263
[U12^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[isNePal^#(x₁)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 1
[U11^#(x₁)]	=	x₁ + 0
[active(x₁)]	=	x₁ + 2
[active^#(x₁)]	=	1
[tt]	=	6128
[__(x₁, x₂)]	=	1

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

U11^#(mark(X))	→	U11^#(X)	(31)
U11^#(active(X))	→	U11^#(X)	(25)

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

U12^#(active(X))	→	U12^#(X)	(55)
U12^#(mark(X))	→	U12^#(X)	(30)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁)]	=	x₁ + 3154
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	3153
[U12(x₁)]	=	x₁ + 3156
[U12^#(x₁)]	=	x₁ + 0
[mark^#(x₁)]	=	0
[isNePal^#(x₁)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 1
[U11^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[active^#(x₁)]	=	1
[tt]	=	1
[__(x₁, x₂)]	=	45545

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

U12^#(active(X))	→	U12^#(X)	(55)
U12^#(mark(X))	→	U12^#(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)	(36)
isNePal^#(active(X))	→	isNePal^#(X)	(43)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁)]	=	x₁ + 4187
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	23744
[U12(x₁)]	=	x₁ + 4189
[U12^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[isNePal^#(x₁)]	=	x₁ + 0
[nil]	=	0
[mark(x₁)]	=	x₁ + 1
[U11^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[active^#(x₁)]	=	1
[tt]	=	19559
[__(x₁, x₂)]	=	45545

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

isNePal^#(mark(X))	→	isNePal^#(X)	(36)
isNePal^#(active(X))	→	isNePal^#(X)	(43)

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

__^#(mark(X1),X2)	→	__^#(X1,X2)	(56)
__^#(X1,mark(X2))	→	__^#(X1,X2)	(34)
__^#(X1,active(X2))	→	__^#(X1,X2)	(49)
__^#(active(X1),X2)	→	__^#(X1,X2)	(47)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁)]	=	x₁ + 10197
[__^#(x₁, x₂)]	=	x₁ + 0
[isNePal(x₁)]	=	31729
[U12(x₁)]	=	x₁ + 10199
[U12^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[isNePal^#(x₁)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 1
[U11^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[active^#(x₁)]	=	1
[tt]	=	21534
[__(x₁, x₂)]	=	1

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

__^#(mark(X1),X2)	→	__^#(X1,X2)	(56)
__^#(active(X1),X2)	→	__^#(X1,X2)	(47)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

__^#(X1,active(X2))	→	__^#(X1,X2)	(49)
__^#(X1,mark(X2))	→	__^#(X1,X2)	(34)

1.1.5.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[U11(x₁)]	=	x₁ + 40401
[__^#(x₁, x₂)]	=	x₂ + 0
[isNePal(x₁)]	=	40400
[U12(x₁)]	=	x₁ + 40403
[U12^#(x₁)]	=	0
[mark^#(x₁)]	=	0
[isNePal^#(x₁)]	=	0
[nil]	=	0
[mark(x₁)]	=	x₁ + 1
[U11^#(x₁)]	=	0
[active(x₁)]	=	x₁ + 2
[active^#(x₁)]	=	1
[tt]	=	1
[__(x₁, x₂)]	=	7690

having no usable rules (w.r.t. the implicit argument filter of the reduction pair), the pairs

__^#(X1,active(X2))	→	__^#(X1,X2)	(49)
__^#(X1,mark(X2))	→	__^#(X1,X2)	(34)

could be deleted.

1.1.5.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.