Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/PALINDROME_nokinds_GM)

The rewrite relation of the following TRS is considered.

a____(__(X,Y),Z)	→	a____(mark(X),a____(mark(Y),mark(Z)))	(1)
a____(X,nil)	→	mark(X)	(2)
a____(nil,X)	→	mark(X)	(3)
a__and(tt,X)	→	mark(X)	(4)
a__isList(V)	→	a__isNeList(V)	(5)
a__isList(nil)	→	tt	(6)
a__isList(__(V1,V2))	→	a__and(a__isList(V1),isList(V2))	(7)
a__isNeList(V)	→	a__isQid(V)	(8)
a__isNeList(__(V1,V2))	→	a__and(a__isList(V1),isNeList(V2))	(9)
a__isNeList(__(V1,V2))	→	a__and(a__isNeList(V1),isList(V2))	(10)
a__isNePal(V)	→	a__isQid(V)	(11)
a__isNePal(__(I,__(P,I)))	→	a__and(a__isQid(I),isPal(P))	(12)
a__isPal(V)	→	a__isNePal(V)	(13)
a__isPal(nil)	→	tt	(14)
a__isQid(a)	→	tt	(15)
a__isQid(e)	→	tt	(16)
a__isQid(i)	→	tt	(17)
a__isQid(o)	→	tt	(18)
a__isQid(u)	→	tt	(19)
mark(__(X1,X2))	→	a____(mark(X1),mark(X2))	(20)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(21)
mark(isList(X))	→	a__isList(X)	(22)
mark(isNeList(X))	→	a__isNeList(X)	(23)
mark(isQid(X))	→	a__isQid(X)	(24)
mark(isNePal(X))	→	a__isNePal(X)	(25)
mark(isPal(X))	→	a__isPal(X)	(26)
mark(nil)	→	nil	(27)
mark(tt)	→	tt	(28)
mark(a)	→	a	(29)
mark(e)	→	e	(30)
mark(i)	→	i	(31)
mark(o)	→	o	(32)
mark(u)	→	u	(33)
a____(X1,X2)	→	__(X1,X2)	(34)
a__and(X1,X2)	→	and(X1,X2)	(35)
a__isList(X)	→	isList(X)	(36)
a__isNeList(X)	→	isNeList(X)	(37)
a__isQid(X)	→	isQid(X)	(38)
a__isNePal(X)	→	isNePal(X)	(39)
a__isPal(X)	→	isPal(X)	(40)

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.

a__isPal^#(V)	→	a__isNePal^#(V)	(41)
a__isNeList^#(V)	→	a__isQid^#(V)	(42)
mark^#(isQid(X))	→	a__isQid^#(X)	(43)
mark^#(__(X1,X2))	→	mark^#(X2)	(44)
a__isNePal^#(__(I,__(P,I)))	→	a__isQid^#(I)	(45)
mark^#(__(X1,X2))	→	a____^#(mark(X1),mark(X2))	(46)
a____^#(__(X,Y),Z)	→	a____^#(mark(X),a____(mark(Y),mark(Z)))	(47)
a____^#(nil,X)	→	mark^#(X)	(48)
mark^#(__(X1,X2))	→	mark^#(X1)	(49)
a__isList^#(__(V1,V2))	→	a__and^#(a__isList(V1),isList(V2))	(50)
a__and^#(tt,X)	→	mark^#(X)	(51)
a____^#(__(X,Y),Z)	→	mark^#(X)	(52)
mark^#(isPal(X))	→	a__isPal^#(X)	(53)
mark^#(isNeList(X))	→	a__isNeList^#(X)	(54)
mark^#(isNePal(X))	→	a__isNePal^#(X)	(55)
a__isNePal^#(V)	→	a__isQid^#(V)	(56)
a____^#(__(X,Y),Z)	→	mark^#(Z)	(57)
mark^#(and(X1,X2))	→	mark^#(X1)	(58)
a____^#(__(X,Y),Z)	→	mark^#(Y)	(59)
a__isNeList^#(__(V1,V2))	→	a__isNeList^#(V1)	(60)
mark^#(isList(X))	→	a__isList^#(X)	(61)
a____^#(__(X,Y),Z)	→	a____^#(mark(Y),mark(Z))	(62)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(63)
a__isNeList^#(__(V1,V2))	→	a__and^#(a__isNeList(V1),isList(V2))	(64)
a__isNeList^#(__(V1,V2))	→	a__and^#(a__isList(V1),isNeList(V2))	(65)
a____^#(X,nil)	→	mark^#(X)	(66)
a__isNePal^#(__(I,__(P,I)))	→	a__and^#(a__isQid(I),isPal(P))	(67)
a__isList^#(__(V1,V2))	→	a__isList^#(V1)	(68)
a__isNeList^#(__(V1,V2))	→	a__isList^#(V1)	(69)
a__isList^#(V)	→	a__isNeList^#(V)	(70)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

a__isList^#(V)	→	a__isNeList^#(V)	(70)
a____^#(__(X,Y),Z)	→	mark^#(X)	(52)
a__isNeList^#(__(V1,V2))	→	a__isList^#(V1)	(69)
a__and^#(tt,X)	→	mark^#(X)	(51)
a__isList^#(__(V1,V2))	→	a__and^#(a__isList(V1),isList(V2))	(50)
a__isList^#(__(V1,V2))	→	a__isList^#(V1)	(68)
mark^#(__(X1,X2))	→	mark^#(X1)	(49)
a__isNePal^#(__(I,__(P,I)))	→	a__and^#(a__isQid(I),isPal(P))	(67)
a____^#(X,nil)	→	mark^#(X)	(66)
a____^#(nil,X)	→	mark^#(X)	(48)
a__isNeList^#(__(V1,V2))	→	a__and^#(a__isList(V1),isNeList(V2))	(65)
a____^#(__(X,Y),Z)	→	a____^#(mark(X),a____(mark(Y),mark(Z)))	(47)
a__isNeList^#(__(V1,V2))	→	a__and^#(a__isNeList(V1),isList(V2))	(64)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(63)
a____^#(__(X,Y),Z)	→	a____^#(mark(Y),mark(Z))	(62)
mark^#(__(X1,X2))	→	a____^#(mark(X1),mark(X2))	(46)
mark^#(__(X1,X2))	→	mark^#(X2)	(44)
mark^#(isList(X))	→	a__isList^#(X)	(61)
a__isNeList^#(__(V1,V2))	→	a__isNeList^#(V1)	(60)
a____^#(__(X,Y),Z)	→	mark^#(Y)	(59)
mark^#(and(X1,X2))	→	mark^#(X1)	(58)
a____^#(__(X,Y),Z)	→	mark^#(Z)	(57)
mark^#(isNePal(X))	→	a__isNePal^#(X)	(55)
mark^#(isNeList(X))	→	a__isNeList^#(X)	(54)
a__isPal^#(V)	→	a__isNePal^#(V)	(41)
mark^#(isPal(X))	→	a__isPal^#(X)	(53)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	1
[a__isNePal^#(x₁)]	=	x₁ + 0
[a__isNeList^#(x₁)]	=	x₁ + 0
[isNeList(x₁)]	=	x₁ + 1
[isPal(x₁)]	=	x₁ + 1
[u]	=	51150
[and(x₁, x₂)]	=	x₁ + x₂ + 283
[a__isPal^#(x₁)]	=	x₁ + 1
[isNePal(x₁)]	=	x₁ + 1
[a____^#(x₁, x₂)]	=	x₁ + x₂ + 285
[isQid(x₁)]	=	x₁ + 1
[a____(x₁, x₂)]	=	x₁ + x₂ + 285
[a__isList(x₁)]	=	x₁ + 1
[a__isNeList(x₁)]	=	x₁ + 1
[o]	=	1
[mark^#(x₁)]	=	x₁ + 1
[isList(x₁)]	=	x₁ + 1
[a__and^#(x₁, x₂)]	=	x₂ + 283
[nil]	=	1
[a__isQid^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[a__isNePal(x₁)]	=	x₁ + 1
[i]	=	21775
[e]	=	1
[a__isPal(x₁)]	=	x₁ + 1
[tt]	=	1
[a__isQid(x₁)]	=	x₁ + 1
[a__isList^#(x₁)]	=	x₁ + 1
[a__and(x₁, x₂)]	=	x₁ + x₂ + 283
[__(x₁, x₂)]	=	x₁ + x₂ + 285

together with the usable rules

a__isQid(o)	→	tt	(18)
a__and(tt,X)	→	mark(X)	(4)
a__isQid(a)	→	tt	(15)
a__isNeList(V)	→	a__isQid(V)	(8)
a____(__(X,Y),Z)	→	a____(mark(X),a____(mark(Y),mark(Z)))	(1)
a____(nil,X)	→	mark(X)	(3)
a__isQid(e)	→	tt	(16)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(21)
a__isList(X)	→	isList(X)	(36)
mark(isPal(X))	→	a__isPal(X)	(26)
a__isQid(u)	→	tt	(19)
mark(o)	→	o	(32)
a__isQid(i)	→	tt	(17)
mark(nil)	→	nil	(27)
a____(X1,X2)	→	__(X1,X2)	(34)
mark(isList(X))	→	a__isList(X)	(22)
mark(tt)	→	tt	(28)
a__isList(V)	→	a__isNeList(V)	(5)
mark(u)	→	u	(33)
a__isNeList(__(V1,V2))	→	a__and(a__isNeList(V1),isList(V2))	(10)
a__isNePal(X)	→	isNePal(X)	(39)
a__isList(__(V1,V2))	→	a__and(a__isList(V1),isList(V2))	(7)
mark(__(X1,X2))	→	a____(mark(X1),mark(X2))	(20)
mark(isNePal(X))	→	a__isNePal(X)	(25)
mark(e)	→	e	(30)
a__isPal(nil)	→	tt	(14)
mark(i)	→	i	(31)
a__isNePal(__(I,__(P,I)))	→	a__and(a__isQid(I),isPal(P))	(12)
mark(isNeList(X))	→	a__isNeList(X)	(23)
mark(isQid(X))	→	a__isQid(X)	(24)
a__isNePal(V)	→	a__isQid(V)	(11)
a__isNeList(__(V1,V2))	→	a__and(a__isList(V1),isNeList(V2))	(9)
a__isPal(V)	→	a__isNePal(V)	(13)
a__isPal(X)	→	isPal(X)	(40)
a__isList(nil)	→	tt	(6)
a__isQid(X)	→	isQid(X)	(38)
a__isNeList(X)	→	isNeList(X)	(37)
a__and(X1,X2)	→	and(X1,X2)	(35)
mark(a)	→	a	(29)
a____(X,nil)	→	mark(X)	(2)

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

a__isList^#(V)	→	a__isNeList^#(V)	(70)
a____^#(__(X,Y),Z)	→	mark^#(X)	(52)
a__isNeList^#(__(V1,V2))	→	a__isList^#(V1)	(69)
a__and^#(tt,X)	→	mark^#(X)	(51)
a__isList^#(__(V1,V2))	→	a__and^#(a__isList(V1),isList(V2))	(50)
a__isList^#(__(V1,V2))	→	a__isList^#(V1)	(68)
mark^#(__(X1,X2))	→	mark^#(X1)	(49)
a__isNePal^#(__(I,__(P,I)))	→	a__and^#(a__isQid(I),isPal(P))	(67)
a____^#(X,nil)	→	mark^#(X)	(66)
a____^#(nil,X)	→	mark^#(X)	(48)
a__isNeList^#(__(V1,V2))	→	a__and^#(a__isList(V1),isNeList(V2))	(65)
a__isNeList^#(__(V1,V2))	→	a__and^#(a__isNeList(V1),isList(V2))	(64)
mark^#(and(X1,X2))	→	a__and^#(mark(X1),X2)	(63)
a____^#(__(X,Y),Z)	→	a____^#(mark(Y),mark(Z))	(62)
mark^#(__(X1,X2))	→	a____^#(mark(X1),mark(X2))	(46)
mark^#(__(X1,X2))	→	mark^#(X2)	(44)
mark^#(isList(X))	→	a__isList^#(X)	(61)
a__isNeList^#(__(V1,V2))	→	a__isNeList^#(V1)	(60)
a____^#(__(X,Y),Z)	→	mark^#(Y)	(59)
mark^#(and(X1,X2))	→	mark^#(X1)	(58)
a____^#(__(X,Y),Z)	→	mark^#(Z)	(57)
mark^#(isNePal(X))	→	a__isNePal^#(X)	(55)
mark^#(isNeList(X))	→	a__isNeList^#(X)	(54)
a__isPal^#(V)	→	a__isNePal^#(V)	(41)
mark^#(isPal(X))	→	a__isPal^#(X)	(53)

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

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

→

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

(47)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a]	=	1
[a__isNePal^#(x₁)]	=	0
[a__isNeList^#(x₁)]	=	0
[isNeList(x₁)]	=	x₁ + 1
[isPal(x₁)]	=	x₁ + 21238
[u]	=	1
[and(x₁, x₂)]	=	x₁ + x₂ + 1
[a__isPal^#(x₁)]	=	1
[isNePal(x₁)]	=	x₁ + 21238
[a____^#(x₁, x₂)]	=	x₁ + 285
[isQid(x₁)]	=	x₁ + 1
[a____(x₁, x₂)]	=	x₁ + x₂ + 2
[a__isList(x₁)]	=	x₁ + 1
[a__isNeList(x₁)]	=	x₁ + 1
[o]	=	1
[mark^#(x₁)]	=	1
[isList(x₁)]	=	x₁ + 1
[a__and^#(x₁, x₂)]	=	283
[nil]	=	1
[a__isQid^#(x₁)]	=	0
[mark(x₁)]	=	x₁ + 0
[a__isNePal(x₁)]	=	x₁ + 21238
[i]	=	1
[e]	=	1
[a__isPal(x₁)]	=	x₁ + 21238
[tt]	=	2
[a__isQid(x₁)]	=	x₁ + 1
[a__isList^#(x₁)]	=	1
[a__and(x₁, x₂)]	=	x₁ + x₂ + 1
[__(x₁, x₂)]	=	x₁ + x₂ + 2

together with the usable rules

a__isQid(o)	→	tt	(18)
a__and(tt,X)	→	mark(X)	(4)
a__isQid(a)	→	tt	(15)
a__isNeList(V)	→	a__isQid(V)	(8)
a____(__(X,Y),Z)	→	a____(mark(X),a____(mark(Y),mark(Z)))	(1)
a____(nil,X)	→	mark(X)	(3)
a__isQid(e)	→	tt	(16)
mark(and(X1,X2))	→	a__and(mark(X1),X2)	(21)
a__isList(X)	→	isList(X)	(36)
mark(isPal(X))	→	a__isPal(X)	(26)
a__isQid(u)	→	tt	(19)
mark(o)	→	o	(32)
a__isQid(i)	→	tt	(17)
mark(nil)	→	nil	(27)
a____(X1,X2)	→	__(X1,X2)	(34)
mark(isList(X))	→	a__isList(X)	(22)
mark(tt)	→	tt	(28)
a__isList(V)	→	a__isNeList(V)	(5)
mark(u)	→	u	(33)
a__isNeList(__(V1,V2))	→	a__and(a__isNeList(V1),isList(V2))	(10)
a__isNePal(X)	→	isNePal(X)	(39)
a__isList(__(V1,V2))	→	a__and(a__isList(V1),isList(V2))	(7)
mark(__(X1,X2))	→	a____(mark(X1),mark(X2))	(20)
mark(isNePal(X))	→	a__isNePal(X)	(25)
mark(e)	→	e	(30)
a__isPal(nil)	→	tt	(14)
mark(i)	→	i	(31)
a__isNePal(__(I,__(P,I)))	→	a__and(a__isQid(I),isPal(P))	(12)
mark(isNeList(X))	→	a__isNeList(X)	(23)
mark(isQid(X))	→	a__isQid(X)	(24)
a__isNePal(V)	→	a__isQid(V)	(11)
a__isNeList(__(V1,V2))	→	a__and(a__isList(V1),isNeList(V2))	(9)
a__isPal(V)	→	a__isNePal(V)	(13)
a__isPal(X)	→	isPal(X)	(40)
a__isList(nil)	→	tt	(6)
a__isQid(X)	→	isQid(X)	(38)
a__isNeList(X)	→	isNeList(X)	(37)
a__and(X1,X2)	→	and(X1,X2)	(35)
mark(a)	→	a	(29)
a____(X,nil)	→	mark(X)	(2)

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

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

→

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

(47)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.