Certification Problem

Input (TPDB TRS_Standard/Secret_07_TRS/secret5)

The rewrite relation of the following TRS is considered.

t(N)	→	cs(r(q(N)),nt(ns(N)))	(1)
q(0)	→	0	(2)
q(s(X))	→	s(p(q(X),d(X)))	(3)
d(0)	→	0	(4)
d(s(X))	→	s(s(d(X)))	(5)
p(0,X)	→	X	(6)
p(X,0)	→	X	(7)
p(s(X),s(Y))	→	s(s(p(X,Y)))	(8)
f(0,X)	→	nil	(9)
f(s(X),cs(Y,Z))	→	cs(Y,nf(X,a(Z)))	(10)
t(X)	→	nt(X)	(11)
s(X)	→	ns(X)	(12)
f(X1,X2)	→	nf(X1,X2)	(13)
a(nt(X))	→	t(a(X))	(14)
a(ns(X))	→	s(a(X))	(15)
a(nf(X1,X2))	→	f(a(X1),a(X2))	(16)
a(X)	→	X	(17)

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^#(nt(X))	→	a^#(X)	(18)
d^#(s(X))	→	d^#(X)	(19)
q^#(s(X))	→	d^#(X)	(20)
a^#(nf(X1,X2))	→	a^#(X2)	(21)
q^#(s(X))	→	p^#(q(X),d(X))	(22)
q^#(s(X))	→	q^#(X)	(23)
t^#(N)	→	q^#(N)	(24)
a^#(nf(X1,X2))	→	f^#(a(X1),a(X2))	(25)
q^#(s(X))	→	s^#(p(q(X),d(X)))	(26)
d^#(s(X))	→	s^#(d(X))	(27)
p^#(s(X),s(Y))	→	p^#(X,Y)	(28)
a^#(ns(X))	→	a^#(X)	(29)
p^#(s(X),s(Y))	→	s^#(p(X,Y))	(30)
f^#(s(X),cs(Y,Z))	→	a^#(Z)	(31)
a^#(nt(X))	→	t^#(a(X))	(32)
a^#(nf(X1,X2))	→	a^#(X1)	(33)
p^#(s(X),s(Y))	→	s^#(s(p(X,Y)))	(34)
d^#(s(X))	→	s^#(s(d(X)))	(35)
a^#(ns(X))	→	s^#(a(X))	(36)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.

The 1^st component contains the pair

a^#(nf(X1,X2))	→	a^#(X1)	(33)
f^#(s(X),cs(Y,Z))	→	a^#(Z)	(31)
a^#(nf(X1,X2))	→	a^#(X2)	(21)
a^#(ns(X))	→	a^#(X)	(29)
a^#(nf(X1,X2))	→	f^#(a(X1),a(X2))	(25)
a^#(nt(X))	→	a^#(X)	(18)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a(x₁)]	=	x₁ + 0
[nf(x₁, x₂)]	=	x₁ + x₂ + 28883
[q(x₁)]	=	1
[d(x₁)]	=	x₁ + 33215
[s(x₁)]	=	x₁ + 0
[r(x₁)]	=	x₁ + 0
[t(x₁)]	=	x₁ + 18458
[ns(x₁)]	=	x₁ + 0
[p^#(x₁, x₂)]	=	0
[cs(x₁, x₂)]	=	x₂ + 0
[f(x₁, x₂)]	=	x₁ + x₂ + 28883
[p(x₁, x₂)]	=	21657
[0]	=	25908
[s^#(x₁)]	=	0
[nil]	=	0
[d^#(x₁)]	=	0
[f^#(x₁, x₂)]	=	x₂ + 1
[nt(x₁)]	=	x₁ + 18458
[a^#(x₁)]	=	x₁ + 0
[q^#(x₁)]	=	0
[t^#(x₁)]	=	0

together with the usable rules

d(0)	→	0	(4)
a(ns(X))	→	s(a(X))	(15)
t(N)	→	cs(r(q(N)),nt(ns(N)))	(1)
a(nf(X1,X2))	→	f(a(X1),a(X2))	(16)
a(X)	→	X	(17)
d(s(X))	→	s(s(d(X)))	(5)
f(s(X),cs(Y,Z))	→	cs(Y,nf(X,a(Z)))	(10)
a(nt(X))	→	t(a(X))	(14)
s(X)	→	ns(X)	(12)
t(X)	→	nt(X)	(11)
f(0,X)	→	nil	(9)
f(X1,X2)	→	nf(X1,X2)	(13)

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

a^#(nf(X1,X2))	→	a^#(X1)	(33)
f^#(s(X),cs(Y,Z))	→	a^#(Z)	(31)
a^#(nf(X1,X2))	→	a^#(X2)	(21)
a^#(nf(X1,X2))	→	f^#(a(X1),a(X2))	(25)
a^#(nt(X))	→	a^#(X)	(18)

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^#(ns(X))

→

a^#(X)

(29)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a(x₁)]	=	x₁ + 2
[nf(x₁, x₂)]	=	x₁ + 25074
[q(x₁)]	=	1
[d(x₁)]	=	1
[s(x₁)]	=	0
[r(x₁)]	=	x₁ + 0
[t(x₁)]	=	x₁ + 24480
[ns(x₁)]	=	x₁ + 1
[p^#(x₁, x₂)]	=	0
[cs(x₁, x₂)]	=	x₂ + 24480
[f(x₁, x₂)]	=	x₁ + x₂ + 25073
[p(x₁, x₂)]	=	21657
[0]	=	25908
[s^#(x₁)]	=	0
[nil]	=	50982
[d^#(x₁)]	=	0
[f^#(x₁, x₂)]	=	1
[nt(x₁)]	=	1
[a^#(x₁)]	=	x₁ + 0
[q^#(x₁)]	=	0
[t^#(x₁)]	=	0

together with the usable rule

a(X)

→

(17)

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

a^#(ns(X))

→

a^#(X)

(29)

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

q^#(s(X))

→

q^#(X)

(23)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a(x₁)]	=	x₁ + 0
[nf(x₁, x₂)]	=	x₁ + 25074
[q(x₁)]	=	x₁ + 1
[d(x₁)]	=	43324
[s(x₁)]	=	x₁ + 1
[r(x₁)]	=	x₁ + 0
[t(x₁)]	=	x₁ + 24480
[ns(x₁)]	=	x₁ + 2
[p^#(x₁, x₂)]	=	0
[cs(x₁, x₂)]	=	x₂ + 24480
[f(x₁, x₂)]	=	x₂ + 25073
[p(x₁, x₂)]	=	0
[0]	=	43325
[s^#(x₁)]	=	0
[nil]	=	25074
[d^#(x₁)]	=	0
[f^#(x₁, x₂)]	=	1
[nt(x₁)]	=	1
[a^#(x₁)]	=	0
[q^#(x₁)]	=	x₁ + 0
[t^#(x₁)]	=	0

together with the usable rule

a(X)

→

(17)

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

q^#(s(X))

→

q^#(X)

(23)

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

p^#(s(X),s(Y))

→

p^#(X,Y)

(28)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a(x₁)]	=	x₁ + 0
[nf(x₁, x₂)]	=	x₁ + 25074
[q(x₁)]	=	x₁ + 1
[d(x₁)]	=	43324
[s(x₁)]	=	x₁ + 1
[r(x₁)]	=	x₁ + 0
[t(x₁)]	=	x₁ + 24480
[ns(x₁)]	=	x₁ + 2
[p^#(x₁, x₂)]	=	x₁ + 0
[cs(x₁, x₂)]	=	x₂ + 24480
[f(x₁, x₂)]	=	x₂ + 25073
[p(x₁, x₂)]	=	0
[0]	=	43325
[s^#(x₁)]	=	0
[nil]	=	25074
[d^#(x₁)]	=	0
[f^#(x₁, x₂)]	=	1
[nt(x₁)]	=	1
[a^#(x₁)]	=	0
[q^#(x₁)]	=	0
[t^#(x₁)]	=	0

together with the usable rule

a(X)

→

(17)

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

p^#(s(X),s(Y))

→

p^#(X,Y)

(28)

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

d^#(s(X))

→

d^#(X)

(19)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[a(x₁)]	=	x₁ + 0
[nf(x₁, x₂)]	=	x₁ + 25074
[q(x₁)]	=	x₁ + 1
[d(x₁)]	=	53793
[s(x₁)]	=	x₁ + 1
[r(x₁)]	=	x₁ + 0
[t(x₁)]	=	x₁ + 49765
[ns(x₁)]	=	2
[p^#(x₁, x₂)]	=	0
[cs(x₁, x₂)]	=	x₂ + 23929
[f(x₁, x₂)]	=	x₂ + 25073
[p(x₁, x₂)]	=	0
[0]	=	53794
[s^#(x₁)]	=	0
[nil]	=	25074
[d^#(x₁)]	=	x₁ + 0
[f^#(x₁, x₂)]	=	1
[nt(x₁)]	=	x₁ + 25835
[a^#(x₁)]	=	0
[q^#(x₁)]	=	0
[t^#(x₁)]	=	0

together with the usable rule

a(X)

→

(17)

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

d^#(s(X))

→

d^#(X)

(19)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 0 components.