Certification Problem

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

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.

mark^#(__(X1,X2))	→	active^#(__(mark(X1),mark(X2)))	(21)
and^#(X1,active(X2))	→	and^#(X1,X2)	(22)
__^#(active(X1),X2)	→	__^#(X1,X2)	(23)
mark^#(isNePal(X))	→	active^#(isNePal(mark(X)))	(24)
__^#(X1,mark(X2))	→	__^#(X1,X2)	(25)
isNePal^#(active(X))	→	isNePal^#(X)	(26)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(27)
active^#(__(__(X,Y),Z))	→	__^#(Y,Z)	(28)
mark^#(nil)	→	active^#(nil)	(29)
mark^#(isNePal(X))	→	isNePal^#(mark(X))	(30)
mark^#(and(X1,X2))	→	and^#(mark(X1),X2)	(31)
active^#(__(nil,X))	→	mark^#(X)	(32)
mark^#(tt)	→	active^#(tt)	(33)
__^#(X1,active(X2))	→	__^#(X1,X2)	(34)
mark^#(__(X1,X2))	→	mark^#(X2)	(35)
active^#(and(tt,X))	→	mark^#(X)	(36)
active^#(__(__(X,Y),Z))	→	__^#(X,__(Y,Z))	(37)
and^#(mark(X1),X2)	→	and^#(X1,X2)	(38)
and^#(active(X1),X2)	→	and^#(X1,X2)	(39)
and^#(X1,mark(X2))	→	and^#(X1,X2)	(40)
mark^#(and(X1,X2))	→	mark^#(X1)	(41)
active^#(__(__(X,Y),Z))	→	mark^#(__(X,__(Y,Z)))	(42)
active^#(isNePal(__(I,__(P,I))))	→	mark^#(tt)	(43)
mark^#(__(X1,X2))	→	__^#(mark(X1),mark(X2))	(44)
active^#(__(X,nil))	→	mark^#(X)	(45)
__^#(mark(X1),X2)	→	__^#(X1,X2)	(46)
mark^#(isNePal(X))	→	mark^#(X)	(47)
mark^#(__(X1,X2))	→	mark^#(X1)	(48)
isNePal^#(mark(X))	→	isNePal^#(X)	(49)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.

The 1^st component contains the pair

mark^#(__(X1,X2))	→	mark^#(X1)	(48)
mark^#(isNePal(X))	→	mark^#(X)	(47)
active^#(__(X,nil))	→	mark^#(X)	(45)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(27)
active^#(__(__(X,Y),Z))	→	mark^#(__(X,__(Y,Z)))	(42)
mark^#(and(X1,X2))	→	mark^#(X1)	(41)
mark^#(isNePal(X))	→	active^#(isNePal(mark(X)))	(24)
active^#(and(tt,X))	→	mark^#(X)	(36)
mark^#(__(X1,X2))	→	mark^#(X2)	(35)
mark^#(__(X1,X2))	→	active^#(__(mark(X1),mark(X2)))	(21)
active^#(__(nil,X))	→	mark^#(X)	(32)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[and(x₁, x₂)]	=	8368
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	8366
[mark^#(x₁)]	=	8368
[isNePal^#(x₁)]	=	0
[nil]	=	8368
[mark(x₁)]	=	8367
[active(x₁)]	=	x₁ + 0
[active^#(x₁)]	=	x₁ + 0
[tt]	=	20165
[and^#(x₁, x₂)]	=	0
[__(x₁, x₂)]	=	8368

together with the usable rules

and(X1,active(X2))	→	and(X1,X2)	(18)
and(mark(X1),X2)	→	and(X1,X2)	(15)
and(X1,mark(X2))	→	and(X1,X2)	(16)
isNePal(mark(X))	→	isNePal(X)	(19)
and(active(X1),X2)	→	and(X1,X2)	(17)
isNePal(active(X))	→	isNePal(X)	(20)
__(X1,active(X2))	→	__(X1,X2)	(14)
__(X1,mark(X2))	→	__(X1,X2)	(12)
__(mark(X1),X2)	→	__(X1,X2)	(11)
__(active(X1),X2)	→	__(X1,X2)	(13)

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

mark^#(isNePal(X))

→

active^#(isNePal(mark(X)))

(24)

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^#(and(tt,X))	→	mark^#(X)	(36)
mark^#(and(X1,X2))	→	mark^#(X1)	(41)
mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(27)
active^#(__(__(X,Y),Z))	→	mark^#(__(X,__(Y,Z)))	(42)
active^#(__(nil,X))	→	mark^#(X)	(32)
mark^#(isNePal(X))	→	mark^#(X)	(47)
mark^#(__(X1,X2))	→	mark^#(X2)	(35)
mark^#(__(X1,X2))	→	mark^#(X1)	(48)
mark^#(__(X1,X2))	→	active^#(__(mark(X1),mark(X2)))	(21)
active^#(__(X,nil))	→	mark^#(X)	(45)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[and(x₁, x₂)]	=	x₁ + x₂ + 2998
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	x₁ + 23046
[mark^#(x₁)]	=	x₁ + 0
[isNePal^#(x₁)]	=	0
[nil]	=	41514
[mark(x₁)]	=	x₁ + 0
[active(x₁)]	=	x₁ + 0
[active^#(x₁)]	=	x₁ + 0
[tt]	=	28
[and^#(x₁, x₂)]	=	0
[__(x₁, x₂)]	=	x₁ + x₂ + 8946

together with the usable rules

and(X1,active(X2))	→	and(X1,X2)	(18)
active(and(tt,X))	→	mark(X)	(4)
and(mark(X1),X2)	→	and(X1,X2)	(15)
mark(and(X1,X2))	→	active(and(mark(X1),X2))	(8)
active(__(__(X,Y),Z))	→	mark(__(X,__(Y,Z)))	(1)
active(__(nil,X))	→	mark(X)	(3)
and(X1,mark(X2))	→	and(X1,X2)	(16)
isNePal(mark(X))	→	isNePal(X)	(19)
and(active(X1),X2)	→	and(X1,X2)	(17)
active(isNePal(__(I,__(P,I))))	→	mark(tt)	(5)
mark(isNePal(X))	→	active(isNePal(mark(X)))	(10)
mark(nil)	→	active(nil)	(7)
isNePal(active(X))	→	isNePal(X)	(20)
__(X1,active(X2))	→	__(X1,X2)	(14)
__(X1,mark(X2))	→	__(X1,X2)	(12)
__(mark(X1),X2)	→	__(X1,X2)	(11)
mark(tt)	→	active(tt)	(9)
__(active(X1),X2)	→	__(X1,X2)	(13)
mark(__(X1,X2))	→	active(__(mark(X1),mark(X2)))	(6)
active(__(X,nil))	→	mark(X)	(2)

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

active^#(and(tt,X))	→	mark^#(X)	(36)
mark^#(and(X1,X2))	→	mark^#(X1)	(41)
active^#(__(nil,X))	→	mark^#(X)	(32)
mark^#(isNePal(X))	→	mark^#(X)	(47)
mark^#(__(X1,X2))	→	mark^#(X2)	(35)
mark^#(__(X1,X2))	→	mark^#(X1)	(48)
active^#(__(X,nil))	→	mark^#(X)	(45)

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

mark^#(and(X1,X2))	→	active^#(and(mark(X1),X2))	(27)
active^#(__(__(X,Y),Z))	→	mark^#(__(X,__(Y,Z)))	(42)
mark^#(__(X1,X2))	→	active^#(__(mark(X1),mark(X2)))	(21)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[and(x₁, x₂)]	=	28882
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	2241
[mark^#(x₁)]	=	28883
[isNePal^#(x₁)]	=	0
[nil]	=	9726
[mark(x₁)]	=	x₁ + 1
[active(x₁)]	=	28885
[active^#(x₁)]	=	x₁ + 0
[tt]	=	28885
[and^#(x₁, x₂)]	=	0
[__(x₁, x₂)]	=	28883

together with the usable rules

and(X1,active(X2))	→	and(X1,X2)	(18)
and(mark(X1),X2)	→	and(X1,X2)	(15)
and(X1,mark(X2))	→	and(X1,X2)	(16)
isNePal(mark(X))	→	isNePal(X)	(19)
and(active(X1),X2)	→	and(X1,X2)	(17)
isNePal(active(X))	→	isNePal(X)	(20)
__(X1,active(X2))	→	__(X1,X2)	(14)
__(X1,mark(X2))	→	__(X1,X2)	(12)
__(mark(X1),X2)	→	__(X1,X2)	(11)
__(active(X1),X2)	→	__(X1,X2)	(13)

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

mark^#(and(X1,X2))

→

active^#(and(mark(X1),X2))

(27)

could be deleted.

1.1.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)))	(21)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(mark^#)	=	1
π(isNePal^#)	=	1
π(mark)	=	1
π(active)	=	1
π(active^#)	=	1

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

prec(and)	=	1	status(and)	=	[1, 2]	list-extension(and)	=	Lex
prec(__^#)	=	0	status(__^#)	=	[1, 2]	list-extension(__^#)	=	Lex
prec(isNePal)	=	1	status(isNePal)	=	[]	list-extension(isNePal)	=	Lex
prec(nil)	=	2	status(nil)	=	[]	list-extension(nil)	=	Lex
prec(tt)	=	0	status(tt)	=	[]	list-extension(tt)	=	Lex
prec(and^#)	=	0	status(and^#)	=	[2, 1]	list-extension(and^#)	=	Lex
prec(__)	=	1	status(__)	=	[1, 2]	list-extension(__)	=	Lex

and the following Max-polynomial interpretation

[and(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[__^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[isNePal(x₁)]	=	0
[nil]	=	0
[tt]	=	0
[and^#(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)
[__(x₁, x₂)]	=	max(x₁ + 0, x₂ + 0, 0)

together with the usable rules

and(X1,active(X2))	→	and(X1,X2)	(18)
active(and(tt,X))	→	mark(X)	(4)
and(mark(X1),X2)	→	and(X1,X2)	(15)
mark(and(X1,X2))	→	active(and(mark(X1),X2))	(8)
active(__(__(X,Y),Z))	→	mark(__(X,__(Y,Z)))	(1)
active(__(nil,X))	→	mark(X)	(3)
and(X1,mark(X2))	→	and(X1,X2)	(16)
isNePal(mark(X))	→	isNePal(X)	(19)
and(active(X1),X2)	→	and(X1,X2)	(17)
active(isNePal(__(I,__(P,I))))	→	mark(tt)	(5)
mark(isNePal(X))	→	active(isNePal(mark(X)))	(10)
mark(nil)	→	active(nil)	(7)
isNePal(active(X))	→	isNePal(X)	(20)
__(X1,active(X2))	→	__(X1,X2)	(14)
__(X1,mark(X2))	→	__(X1,X2)	(12)
__(mark(X1),X2)	→	__(X1,X2)	(11)
mark(tt)	→	active(tt)	(9)
__(active(X1),X2)	→	__(X1,X2)	(13)
mark(__(X1,X2))	→	active(__(mark(X1),mark(X2)))	(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.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

__^#(mark(X1),X2)	→	__^#(X1,X2)	(46)
__^#(X1,mark(X2))	→	__^#(X1,X2)	(25)
__^#(active(X1),X2)	→	__^#(X1,X2)	(23)
__^#(X1,active(X2))	→	__^#(X1,X2)	(34)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[and(x₁, x₂)]	=	x₁ + x₂ + 1
[__^#(x₁, x₂)]	=	x₁ + x₂ + 0
[isNePal(x₁)]	=	x₁ + 2
[mark^#(x₁)]	=	0
[isNePal^#(x₁)]	=	0
[nil]	=	42910
[mark(x₁)]	=	x₁ + 4
[active(x₁)]	=	x₁ + 1
[active^#(x₁)]	=	0
[tt]	=	1
[and^#(x₁, x₂)]	=	0
[__(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)	(46)
__^#(X1,mark(X2))	→	__^#(X1,X2)	(25)
__^#(active(X1),X2)	→	__^#(X1,X2)	(23)
__^#(X1,active(X2))	→	__^#(X1,X2)	(34)

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

isNePal^#(mark(X))	→	isNePal^#(X)	(49)
isNePal^#(active(X))	→	isNePal^#(X)	(26)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[and(x₁, x₂)]	=	x₁ + x₂ + 1
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	x₁ + 1
[mark^#(x₁)]	=	0
[isNePal^#(x₁)]	=	x₁ + 0
[nil]	=	42910
[mark(x₁)]	=	x₁ + 4
[active(x₁)]	=	x₁ + 1
[active^#(x₁)]	=	0
[tt]	=	1
[and^#(x₁, x₂)]	=	0
[__(x₁, x₂)]	=	1

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

isNePal^#(mark(X))	→	isNePal^#(X)	(49)
isNePal^#(active(X))	→	isNePal^#(X)	(26)

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

and^#(X1,mark(X2))	→	and^#(X1,X2)	(40)
and^#(active(X1),X2)	→	and^#(X1,X2)	(39)
and^#(mark(X1),X2)	→	and^#(X1,X2)	(38)
and^#(X1,active(X2))	→	and^#(X1,X2)	(22)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[and(x₁, x₂)]	=	x₁ + x₂ + 1
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	x₁ + 1
[mark^#(x₁)]	=	0
[isNePal^#(x₁)]	=	0
[nil]	=	41065
[mark(x₁)]	=	x₁ + 4
[active(x₁)]	=	x₁ + 1
[active^#(x₁)]	=	0
[tt]	=	1
[and^#(x₁, x₂)]	=	x₁ + 0
[__(x₁, x₂)]	=	1

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

and^#(active(X1),X2)	→	and^#(X1,X2)	(39)
and^#(mark(X1),X2)	→	and^#(X1,X2)	(38)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

and^#(X1,active(X2))	→	and^#(X1,X2)	(22)
and^#(X1,mark(X2))	→	and^#(X1,X2)	(40)

1.1.4.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[and(x₁, x₂)]	=	x₁ + x₂ + 1
[__^#(x₁, x₂)]	=	0
[isNePal(x₁)]	=	x₁ + 1
[mark^#(x₁)]	=	0
[isNePal^#(x₁)]	=	0
[nil]	=	52629
[mark(x₁)]	=	x₁ + 4
[active(x₁)]	=	x₁ + 1
[active^#(x₁)]	=	0
[tt]	=	1
[and^#(x₁, x₂)]	=	x₂ + 0
[__(x₁, x₂)]	=	2

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

and^#(X1,active(X2))	→	and^#(X1,X2)	(22)
and^#(X1,mark(X2))	→	and^#(X1,X2)	(40)

could be deleted.

1.1.4.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.