Certification Problem

Input (TPDB TRS_Standard/AProVE_07/wiehe12)

The rewrite relation of the following TRS is considered.

g(s(x),s(y))	→	if(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0))),k(n(s(x),s(y)),s(s(0))))),g(minus(m(x,y),n(x,y)),n(s(x),s(y))))	(1)
n(0,y)	→	0	(2)
n(x,0)	→	0	(3)
n(s(x),s(y))	→	s(n(x,y))	(4)
m(0,y)	→	y	(5)
m(x,0)	→	x	(6)
m(s(x),s(y))	→	s(m(x,y))	(7)
k(0,s(y))	→	0	(8)
k(s(x),s(y))	→	s(k(minus(x,y),s(y)))	(9)
t(x)	→	p(x,x)	(10)
p(s(x),s(y))	→	s(s(p(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))	(11)
p(s(x),x)	→	p(if(gt(x,x),id(x),id(x)),s(x))	(12)
p(0,y)	→	y	(13)
p(id(x),s(y))	→	s(p(x,if(gt(s(y),y),y,s(y))))	(14)
minus(x,0)	→	x	(15)
minus(s(x),s(y))	→	minus(x,y)	(16)
id(x)	→	x	(17)
if(true,x,y)	→	x	(18)
if(false,x,y)	→	y	(19)
not(x)	→	if(x,false,true)	(20)
and(x,false)	→	false	(21)
and(true,true)	→	true	(22)
f(0)	→	true	(23)
f(s(x))	→	h(x)	(24)
h(0)	→	false	(25)
h(s(x))	→	f(x)	(26)
gt(s(x),0)	→	true	(27)
gt(0,y)	→	false	(28)
gt(s(x),s(y))	→	gt(x,y)	(29)

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.

k^#(s(x),s(y))	→	k^#(minus(x,y),s(y))	(30)
n^#(s(x),s(y))	→	n^#(x,y)	(31)
g^#(s(x),s(y))	→	f^#(s(y))	(32)
g^#(s(x),s(y))	→	n^#(x,y)	(33)
g^#(s(x),s(y))	→	n^#(s(x),s(y))	(34)
g^#(s(x),s(y))	→	n^#(x,y)	(33)
g^#(s(x),s(y))	→	n^#(s(x),s(y))	(34)
g^#(s(x),s(y))	→	g^#(minus(m(x,y),n(x,y)),n(s(x),s(y)))	(35)
p^#(s(x),s(y))	→	gt^#(x,y)	(36)
g^#(s(x),s(y))	→	m^#(x,y)	(37)
p^#(s(x),x)	→	p^#(if(gt(x,x),id(x),id(x)),s(x))	(38)
p^#(s(x),s(y))	→	gt^#(x,y)	(36)
p^#(s(x),s(y))	→	id^#(y)	(39)
h^#(s(x))	→	f^#(x)	(40)
t^#(x)	→	p^#(x,x)	(41)
f^#(s(x))	→	h^#(x)	(42)
g^#(s(x),s(y))	→	g^#(k(minus(m(x,y),n(x,y)),s(s(0))),k(n(s(x),s(y)),s(s(0))))	(43)
p^#(s(x),x)	→	if^#(gt(x,x),id(x),id(x))	(44)
g^#(s(x),s(y))	→	t^#(g(k(minus(m(x,y),n(x,y)),s(s(0))),k(n(s(x),s(y)),s(s(0)))))	(45)
minus^#(s(x),s(y))	→	minus^#(x,y)	(46)
p^#(id(x),s(y))	→	gt^#(s(y),y)	(47)
p^#(s(x),s(y))	→	if^#(not(gt(x,y)),id(x),id(y))	(48)
g^#(s(x),s(y))	→	minus^#(m(x,y),n(x,y))	(49)
p^#(s(x),s(y))	→	id^#(x)	(50)
g^#(s(x),s(y))	→	minus^#(m(x,y),n(x,y))	(49)
p^#(s(x),s(y))	→	if^#(gt(x,y),x,y)	(51)
g^#(s(x),s(y))	→	f^#(s(x))	(52)
m^#(s(x),s(y))	→	m^#(x,y)	(53)
g^#(s(x),s(y))	→	m^#(x,y)	(37)
g^#(s(x),s(y))	→	and^#(f(s(x)),f(s(y)))	(54)
p^#(s(x),x)	→	id^#(x)	(55)
g^#(s(x),s(y))	→	k^#(minus(m(x,y),n(x,y)),s(s(0)))	(56)
p^#(id(x),s(y))	→	if^#(gt(s(y),y),y,s(y))	(57)
g^#(s(x),s(y))	→	if^#(and(f(s(x)),f(s(y))),t(g(k(minus(m(x,y),n(x,y)),s(s(0))),k(n(s(x),s(y)),s(s(0))))),g(minus(m(x,y),n(x,y)),n(s(x),s(y))))	(58)
g^#(s(x),s(y))	→	k^#(n(s(x),s(y)),s(s(0)))	(59)
not^#(x)	→	if^#(x,false,true)	(60)
p^#(s(x),x)	→	id^#(x)	(55)
k^#(s(x),s(y))	→	minus^#(x,y)	(61)
gt^#(s(x),s(y))	→	gt^#(x,y)	(62)
p^#(s(x),s(y))	→	not^#(gt(x,y))	(63)
p^#(s(x),x)	→	gt^#(x,x)	(64)
p^#(s(x),s(y))	→	p^#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))	(65)
p^#(id(x),s(y))	→	p^#(x,if(gt(s(y),y),y,s(y)))	(66)

1.1 Dependency Graph Processor

The dependency pairs are split into 8 components.

The 1^st component contains the pair

g^#(s(x),s(y))	→	g^#(k(minus(m(x,y),n(x,y)),s(s(0))),k(n(s(x),s(y)),s(s(0))))	(43)
g^#(s(x),s(y))	→	g^#(minus(m(x,y),n(x,y)),n(s(x),s(y)))	(35)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[h(x₁)]	=	0
[s(x₁)]	=	x₁ + 12461
[n(x₁, x₂)]	=	max(x₁ + 12457, 0)
[gt(x₁, x₂)]	=	max(0)
[minus(x₁, x₂)]	=	max(x₁ + 0, 0)
[and(x₁, x₂)]	=	max(0)
[k(x₁, x₂)]	=	max(x₁ + 1, 0)
[t(x₁)]	=	0
[false]	=	0
[id^#(x₁)]	=	0
[p^#(x₁, x₂)]	=	max(0)
[true]	=	0
[f(x₁)]	=	0
[not^#(x₁)]	=	0
[p(x₁, x₂)]	=	max(0)
[if(x₁, x₂, x₃)]	=	max(0)
[0]	=	4620
[h^#(x₁)]	=	0
[k^#(x₁, x₂)]	=	max(0)
[gt^#(x₁, x₂)]	=	max(0)
[f^#(x₁)]	=	0
[g^#(x₁, x₂)]	=	max(x₁ + 20205, x₂ + 7746, 0)
[minus^#(x₁, x₂)]	=	max(0)
[if^#(x₁, x₂, x₃)]	=	max(0)
[id(x₁)]	=	0
[t^#(x₁)]	=	0
[n^#(x₁, x₂)]	=	max(0)
[m^#(x₁, x₂)]	=	max(0)
[g(x₁, x₂)]	=	max(0)
[and^#(x₁, x₂)]	=	max(0)
[not(x₁)]	=	0
[m(x₁, x₂)]	=	max(x₁ + 3, x₂ + 1, 0)

together with the usable rules

n(s(x),s(y))	→	s(n(x,y))	(4)
minus(x,0)	→	x	(15)
k(0,s(y))	→	0	(8)
n(x,0)	→	0	(3)
minus(s(x),s(y))	→	minus(x,y)	(16)
m(0,y)	→	y	(5)
m(s(x),s(y))	→	s(m(x,y))	(7)
k(s(x),s(y))	→	s(k(minus(x,y),s(y)))	(9)
m(x,0)	→	x	(6)
n(0,y)	→	0	(2)

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

g^#(s(x),s(y))

→

g^#(minus(m(x,y),n(x,y)),n(s(x),s(y)))

(35)

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

g^#(s(x),s(y))

→

g^#(k(minus(m(x,y),n(x,y)),s(s(0))),k(n(s(x),s(y)),s(s(0))))

(43)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[h(x₁)]	=	0
[s(x₁)]	=	x₁ + 37900
[n(x₁, x₂)]	=	max(x₁ + 1, 0)
[gt(x₁, x₂)]	=	max(0)
[minus(x₁, x₂)]	=	max(x₁ + 0, 0)
[and(x₁, x₂)]	=	max(0)
[k(x₁, x₂)]	=	max(x₁ + 1, 0)
[t(x₁)]	=	0
[false]	=	0
[id^#(x₁)]	=	0
[p^#(x₁, x₂)]	=	max(0)
[true]	=	0
[f(x₁)]	=	0
[not^#(x₁)]	=	0
[p(x₁, x₂)]	=	max(0)
[if(x₁, x₂, x₃)]	=	max(0)
[0]	=	1
[h^#(x₁)]	=	0
[k^#(x₁, x₂)]	=	max(0)
[gt^#(x₁, x₂)]	=	max(0)
[f^#(x₁)]	=	0
[g^#(x₁, x₂)]	=	max(x₁ + 23982, x₂ + 23979, 0)
[minus^#(x₁, x₂)]	=	max(0)
[if^#(x₁, x₂, x₃)]	=	max(0)
[id(x₁)]	=	0
[t^#(x₁)]	=	0
[n^#(x₁, x₂)]	=	max(0)
[m^#(x₁, x₂)]	=	max(0)
[g(x₁, x₂)]	=	max(0)
[and^#(x₁, x₂)]	=	max(0)
[not(x₁)]	=	0
[m(x₁, x₂)]	=	max(x₁ + 37895, x₂ + 37894, 0)

together with the usable rules

n(s(x),s(y))	→	s(n(x,y))	(4)
minus(x,0)	→	x	(15)
k(0,s(y))	→	0	(8)
n(x,0)	→	0	(3)
minus(s(x),s(y))	→	minus(x,y)	(16)
m(0,y)	→	y	(5)
m(s(x),s(y))	→	s(m(x,y))	(7)
k(s(x),s(y))	→	s(k(minus(x,y),s(y)))	(9)
m(x,0)	→	x	(6)
n(0,y)	→	0	(2)

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

g^#(s(x),s(y))

→

g^#(k(minus(m(x,y),n(x,y)),s(s(0))),k(n(s(x),s(y)),s(s(0))))

(43)

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

p^#(id(x),s(y))	→	p^#(x,if(gt(s(y),y),y,s(y)))	(66)
p^#(s(x),s(y))	→	p^#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))	(65)
p^#(s(x),x)	→	p^#(if(gt(x,x),id(x),id(x)),s(x))	(38)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[h(x₁)]	=	0
[s(x₁)]	=	x₁ + 3
[n(x₁, x₂)]	=	max(x₁ + 1, 0)
[gt(x₁, x₂)]	=	max(0)
[minus(x₁, x₂)]	=	max(x₁ + 0, 0)
[and(x₁, x₂)]	=	max(0)
[k(x₁, x₂)]	=	max(x₁ + 1, 0)
[t(x₁)]	=	0
[false]	=	0
[id^#(x₁)]	=	0
[p^#(x₁, x₂)]	=	max(x₁ + 17900, x₂ + 17897, 0)
[true]	=	0
[f(x₁)]	=	0
[not^#(x₁)]	=	0
[p(x₁, x₂)]	=	max(0)
[if(x₁, x₂, x₃)]	=	max(x₁ + 1, x₂ + 1, x₃ + 0, 0)
[0]	=	1
[h^#(x₁)]	=	0
[k^#(x₁, x₂)]	=	max(0)
[gt^#(x₁, x₂)]	=	max(0)
[f^#(x₁)]	=	0
[g^#(x₁, x₂)]	=	max(x₁ + 23982, x₂ + 23979, 0)
[minus^#(x₁, x₂)]	=	max(0)
[if^#(x₁, x₂, x₃)]	=	max(0)
[id(x₁)]	=	x₁ + 1
[t^#(x₁)]	=	0
[n^#(x₁, x₂)]	=	max(0)
[m^#(x₁, x₂)]	=	max(0)
[g(x₁, x₂)]	=	max(0)
[and^#(x₁, x₂)]	=	max(0)
[not(x₁)]	=	x₁ + 5
[m(x₁, x₂)]	=	max(x₁ + 2, x₂ + 1, 0)

together with the usable rules

if(true,x,y)	→	x	(18)
n(s(x),s(y))	→	s(n(x,y))	(4)
minus(x,0)	→	x	(15)
k(0,s(y))	→	0	(8)
n(x,0)	→	0	(3)
minus(s(x),s(y))	→	minus(x,y)	(16)
if(false,x,y)	→	y	(19)
id(x)	→	x	(17)
gt(s(x),0)	→	true	(27)
gt(0,y)	→	false	(28)
m(0,y)	→	y	(5)
m(s(x),s(y))	→	s(m(x,y))	(7)
not(x)	→	if(x,false,true)	(20)
k(s(x),s(y))	→	s(k(minus(x,y),s(y)))	(9)
m(x,0)	→	x	(6)
gt(s(x),s(y))	→	gt(x,y)	(29)
n(0,y)	→	0	(2)

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

p^#(s(x),x)

→

p^#(if(gt(x,x),id(x),id(x)),s(x))

(38)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

p^#(id(x),s(y))	→	p^#(x,if(gt(s(y),y),y,s(y)))	(66)
p^#(s(x),s(y))	→	p^#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))	(65)

1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[h(x₁)]	=	0
[s(x₁)]	=	x₁ + 4
[n(x₁, x₂)]	=	max(x₁ + 1, 0)
[gt(x₁, x₂)]	=	max(0)
[minus(x₁, x₂)]	=	max(x₁ + 0, 0)
[and(x₁, x₂)]	=	max(0)
[k(x₁, x₂)]	=	max(x₁ + 1, 0)
[t(x₁)]	=	0
[false]	=	0
[id^#(x₁)]	=	0
[p^#(x₁, x₂)]	=	max(x₁ + 28938, x₂ + 28940, 0)
[true]	=	0
[f(x₁)]	=	0
[not^#(x₁)]	=	0
[p(x₁, x₂)]	=	max(0)
[if(x₁, x₂, x₃)]	=	max(x₁ + 1, x₂ + 1, x₃ + 0, 0)
[0]	=	1
[h^#(x₁)]	=	0
[k^#(x₁, x₂)]	=	max(0)
[gt^#(x₁, x₂)]	=	max(0)
[f^#(x₁)]	=	0
[g^#(x₁, x₂)]	=	max(x₁ + 23982, x₂ + 23979, 0)
[minus^#(x₁, x₂)]	=	max(0)
[if^#(x₁, x₂, x₃)]	=	max(0)
[id(x₁)]	=	x₁ + 0
[t^#(x₁)]	=	0
[n^#(x₁, x₂)]	=	max(0)
[m^#(x₁, x₂)]	=	max(0)
[g(x₁, x₂)]	=	max(0)
[and^#(x₁, x₂)]	=	max(0)
[not(x₁)]	=	x₁ + 2
[m(x₁, x₂)]	=	max(x₁ + 2, x₂ + 1, 0)

together with the usable rules

if(true,x,y)	→	x	(18)
n(s(x),s(y))	→	s(n(x,y))	(4)
minus(x,0)	→	x	(15)
k(0,s(y))	→	0	(8)
n(x,0)	→	0	(3)
minus(s(x),s(y))	→	minus(x,y)	(16)
if(false,x,y)	→	y	(19)
id(x)	→	x	(17)
gt(s(x),0)	→	true	(27)
gt(0,y)	→	false	(28)
m(0,y)	→	y	(5)
m(s(x),s(y))	→	s(m(x,y))	(7)
not(x)	→	if(x,false,true)	(20)
k(s(x),s(y))	→	s(k(minus(x,y),s(y)))	(9)
m(x,0)	→	x	(6)
gt(s(x),s(y))	→	gt(x,y)	(29)
n(0,y)	→	0	(2)

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

p^#(s(x),s(y))

→

p^#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))

(65)

could be deleted.

1.1.2.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

p^#(id(x),s(y))

→

p^#(x,if(gt(s(y),y),y,s(y)))

(66)

1.1.2.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[h(x₁)]	=	0
[s(x₁)]	=	3
[n(x₁, x₂)]	=	1
[gt(x₁, x₂)]	=	1
[minus(x₁, x₂)]	=	1
[and(x₁, x₂)]	=	0
[k(x₁, x₂)]	=	2
[t(x₁)]	=	0
[false]	=	1
[id^#(x₁)]	=	0
[p^#(x₁, x₂)]	=	x₁ + 0
[true]	=	1
[f(x₁)]	=	0
[not^#(x₁)]	=	0
[p(x₁, x₂)]	=	0
[if(x₁, x₂, x₃)]	=	x₂ + x₃ + 0
[0]	=	2
[h^#(x₁)]	=	0
[k^#(x₁, x₂)]	=	0
[gt^#(x₁, x₂)]	=	0
[f^#(x₁)]	=	0
[g^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[id(x₁)]	=	x₁ + 28872
[t^#(x₁)]	=	0
[n^#(x₁, x₂)]	=	0
[m^#(x₁, x₂)]	=	0
[g(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[not(x₁)]	=	0
[m(x₁, x₂)]	=	1

together with the usable rules

if(true,x,y)	→	x	(18)
k(0,s(y))	→	0	(8)
if(false,x,y)	→	y	(19)
id(x)	→	x	(17)
gt(s(x),0)	→	true	(27)
gt(0,y)	→	false	(28)
gt(s(x),s(y))	→	gt(x,y)	(29)

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

p^#(id(x),s(y))

→

p^#(x,if(gt(s(y),y),y,s(y)))

(66)

could be deleted.

1.1.2.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

m^#(s(x),s(y))

→

m^#(x,y)

(53)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[h(x₁)]	=	0
[s(x₁)]	=	x₁ + 1
[n(x₁, x₂)]	=	11820
[gt(x₁, x₂)]	=	23505
[minus(x₁, x₂)]	=	1
[and(x₁, x₂)]	=	0
[k(x₁, x₂)]	=	11821
[t(x₁)]	=	0
[false]	=	23505
[id^#(x₁)]	=	0
[p^#(x₁, x₂)]	=	x₁ + 0
[true]	=	2805
[f(x₁)]	=	0
[not^#(x₁)]	=	0
[p(x₁, x₂)]	=	0
[if(x₁, x₂, x₃)]	=	x₂ + x₃ + 0
[0]	=	11821
[h^#(x₁)]	=	0
[k^#(x₁, x₂)]	=	0
[gt^#(x₁, x₂)]	=	0
[f^#(x₁)]	=	0
[g^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[id(x₁)]	=	x₁ + 28872
[t^#(x₁)]	=	0
[n^#(x₁, x₂)]	=	0
[m^#(x₁, x₂)]	=	x₁ + 0
[g(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[not(x₁)]	=	26309
[m(x₁, x₂)]	=	4187

together with the usable rules

if(true,x,y)	→	x	(18)
k(0,s(y))	→	0	(8)
if(false,x,y)	→	y	(19)
id(x)	→	x	(17)
gt(s(x),0)	→	true	(27)
gt(0,y)	→	false	(28)
gt(s(x),s(y))	→	gt(x,y)	(29)

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

m^#(s(x),s(y))

→

m^#(x,y)

(53)

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

f^#(s(x))	→	h^#(x)	(42)
h^#(s(x))	→	f^#(x)	(40)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[h(x₁)]	=	0
[s(x₁)]	=	x₁ + 1
[n(x₁, x₂)]	=	32968
[gt(x₁, x₂)]	=	1
[minus(x₁, x₂)]	=	1
[and(x₁, x₂)]	=	0
[k(x₁, x₂)]	=	32969
[t(x₁)]	=	0
[false]	=	1
[id^#(x₁)]	=	0
[p^#(x₁, x₂)]	=	x₁ + 0
[true]	=	1
[f(x₁)]	=	0
[not^#(x₁)]	=	0
[p(x₁, x₂)]	=	0
[if(x₁, x₂, x₃)]	=	x₂ + x₃ + 0
[0]	=	32969
[h^#(x₁)]	=	x₁ + 0
[k^#(x₁, x₂)]	=	0
[gt^#(x₁, x₂)]	=	0
[f^#(x₁)]	=	x₁ + 0
[g^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[id(x₁)]	=	x₁ + 28872
[t^#(x₁)]	=	0
[n^#(x₁, x₂)]	=	0
[m^#(x₁, x₂)]	=	0
[g(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[not(x₁)]	=	1
[m(x₁, x₂)]	=	42004

together with the usable rules

if(true,x,y)	→	x	(18)
k(0,s(y))	→	0	(8)
if(false,x,y)	→	y	(19)
id(x)	→	x	(17)
gt(s(x),0)	→	true	(27)
gt(0,y)	→	false	(28)
gt(s(x),s(y))	→	gt(x,y)	(29)

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

f^#(s(x))	→	h^#(x)	(42)
h^#(s(x))	→	f^#(x)	(40)

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

n^#(s(x),s(y))

→

n^#(x,y)

(31)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[h(x₁)]	=	0
[s(x₁)]	=	x₁ + 1
[n(x₁, x₂)]	=	7690
[gt(x₁, x₂)]	=	1
[minus(x₁, x₂)]	=	1
[and(x₁, x₂)]	=	0
[k(x₁, x₂)]	=	7691
[t(x₁)]	=	0
[false]	=	1
[id^#(x₁)]	=	0
[p^#(x₁, x₂)]	=	x₁ + 0
[true]	=	1
[f(x₁)]	=	0
[not^#(x₁)]	=	0
[p(x₁, x₂)]	=	0
[if(x₁, x₂, x₃)]	=	x₂ + x₃ + 0
[0]	=	7691
[h^#(x₁)]	=	0
[k^#(x₁, x₂)]	=	0
[gt^#(x₁, x₂)]	=	0
[f^#(x₁)]	=	0
[g^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[id(x₁)]	=	x₁ + 28872
[t^#(x₁)]	=	0
[n^#(x₁, x₂)]	=	x₁ + 0
[m^#(x₁, x₂)]	=	0
[g(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[not(x₁)]	=	1
[m(x₁, x₂)]	=	42004

together with the usable rules

if(true,x,y)	→	x	(18)
k(0,s(y))	→	0	(8)
if(false,x,y)	→	y	(19)
id(x)	→	x	(17)
gt(s(x),0)	→	true	(27)
gt(0,y)	→	false	(28)
gt(s(x),s(y))	→	gt(x,y)	(29)

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

n^#(s(x),s(y))

→

n^#(x,y)

(31)

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

k^#(s(x),s(y))

→

k^#(minus(x,y),s(y))

(30)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[h(x₁)]	=	0
[s(x₁)]	=	x₁ + 24169
[n(x₁, x₂)]	=	1
[gt(x₁, x₂)]	=	1
[minus(x₁, x₂)]	=	x₁ + 24168
[and(x₁, x₂)]	=	0
[k(x₁, x₂)]	=	23638
[t(x₁)]	=	0
[false]	=	1
[id^#(x₁)]	=	0
[p^#(x₁, x₂)]	=	x₁ + 0
[true]	=	1
[f(x₁)]	=	0
[not^#(x₁)]	=	0
[p(x₁, x₂)]	=	0
[if(x₁, x₂, x₃)]	=	x₂ + x₃ + 0
[0]	=	23638
[h^#(x₁)]	=	0
[k^#(x₁, x₂)]	=	x₁ + 0
[gt^#(x₁, x₂)]	=	0
[f^#(x₁)]	=	0
[g^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[id(x₁)]	=	x₁ + 28872
[t^#(x₁)]	=	0
[n^#(x₁, x₂)]	=	0
[m^#(x₁, x₂)]	=	0
[g(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[not(x₁)]	=	0
[m(x₁, x₂)]	=	43486

together with the usable rules

if(true,x,y)	→	x	(18)
minus(x,0)	→	x	(15)
k(0,s(y))	→	0	(8)
minus(s(x),s(y))	→	minus(x,y)	(16)
if(false,x,y)	→	y	(19)
id(x)	→	x	(17)
gt(s(x),0)	→	true	(27)
gt(0,y)	→	false	(28)
gt(s(x),s(y))	→	gt(x,y)	(29)

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

k^#(s(x),s(y))

→

k^#(minus(x,y),s(y))

(30)

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

minus^#(s(x),s(y))

→

minus^#(x,y)

(46)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[h(x₁)]	=	0
[s(x₁)]	=	x₁ + 1
[n(x₁, x₂)]	=	35475
[gt(x₁, x₂)]	=	31135
[minus(x₁, x₂)]	=	x₁ + 24168
[and(x₁, x₂)]	=	0
[k(x₁, x₂)]	=	35476
[t(x₁)]	=	0
[false]	=	31135
[id^#(x₁)]	=	0
[p^#(x₁, x₂)]	=	x₁ + 0
[true]	=	14923
[f(x₁)]	=	0
[not^#(x₁)]	=	0
[p(x₁, x₂)]	=	0
[if(x₁, x₂, x₃)]	=	x₂ + x₃ + 0
[0]	=	35476
[h^#(x₁)]	=	0
[k^#(x₁, x₂)]	=	x₁ + 0
[gt^#(x₁, x₂)]	=	0
[f^#(x₁)]	=	0
[g^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	x₂ + 0
[if^#(x₁, x₂, x₃)]	=	0
[id(x₁)]	=	x₁ + 28872
[t^#(x₁)]	=	0
[n^#(x₁, x₂)]	=	0
[m^#(x₁, x₂)]	=	0
[g(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[not(x₁)]	=	46057
[m(x₁, x₂)]	=	43486

together with the usable rules

if(true,x,y)	→	x	(18)
minus(x,0)	→	x	(15)
k(0,s(y))	→	0	(8)
minus(s(x),s(y))	→	minus(x,y)	(16)
if(false,x,y)	→	y	(19)
id(x)	→	x	(17)
gt(s(x),0)	→	true	(27)
gt(0,y)	→	false	(28)
gt(s(x),s(y))	→	gt(x,y)	(29)

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

minus^#(s(x),s(y))

→

minus^#(x,y)

(46)

could be deleted.

1.1.7.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 8^th component contains the pair

gt^#(s(x),s(y))

→

gt^#(x,y)

(62)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[h(x₁)]	=	0
[s(x₁)]	=	x₁ + 1
[n(x₁, x₂)]	=	35475
[gt(x₁, x₂)]	=	14923
[minus(x₁, x₂)]	=	x₁ + 24168
[and(x₁, x₂)]	=	0
[k(x₁, x₂)]	=	35476
[t(x₁)]	=	0
[false]	=	120
[id^#(x₁)]	=	0
[p^#(x₁, x₂)]	=	x₁ + 0
[true]	=	14923
[f(x₁)]	=	0
[not^#(x₁)]	=	0
[p(x₁, x₂)]	=	0
[if(x₁, x₂, x₃)]	=	x₂ + x₃ + 0
[0]	=	35476
[h^#(x₁)]	=	0
[k^#(x₁, x₂)]	=	x₁ + 0
[gt^#(x₁, x₂)]	=	x₂ + 0
[f^#(x₁)]	=	0
[g^#(x₁, x₂)]	=	0
[minus^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[id(x₁)]	=	x₁ + 28872
[t^#(x₁)]	=	0
[n^#(x₁, x₂)]	=	0
[m^#(x₁, x₂)]	=	0
[g(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[not(x₁)]	=	15042
[m(x₁, x₂)]	=	43486

together with the usable rules

if(true,x,y)	→	x	(18)
minus(x,0)	→	x	(15)
k(0,s(y))	→	0	(8)
minus(s(x),s(y))	→	minus(x,y)	(16)
if(false,x,y)	→	y	(19)
id(x)	→	x	(17)
gt(s(x),0)	→	true	(27)
gt(0,y)	→	false	(28)
gt(s(x),s(y))	→	gt(x,y)	(29)

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

gt^#(s(x),s(y))

→

gt^#(x,y)

(62)

could be deleted.

1.1.8.1 Dependency Graph Processor

The dependency pairs are split into 0 components.