Certification Problem

Input (TPDB TRS_Standard/HirokawaMiddeldorp_04/t001)

The rewrite relation of the following TRS is considered.

-(x,0)	→	x	(1)
-(s(x),s(y))	→	-(x,y)	(2)
*(x,0)	→	0	(3)
*(x,s(y))	→	+(*(x,y),x)	(4)
if(true,x,y)	→	x	(5)
if(false,x,y)	→	y	(6)
odd(0)	→	false	(7)
odd(s(0))	→	true	(8)
odd(s(s(x)))	→	odd(x)	(9)
half(0)	→	0	(10)
half(s(0))	→	0	(11)
half(s(s(x)))	→	s(half(x))	(12)
if(true,x,y)	→	true	(13)
if(false,x,y)	→	false	(14)
pow(x,y)	→	f(x,y,s(0))	(15)
f(x,0,z)	→	z	(16)
f(x,s(y),z)	→	if(odd(s(y)),f(x,y,(x,z)),f((x,x),half(s(y)),z))	(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.

odd^#(s(s(x)))	→	odd^#(x)	(18)
f^#(x,s(y),z)	→	f^#(x,y,*(x,z))	(19)
f^#(x,s(y),z)	→	*^#(x,x)	(20)
pow^#(x,y)	→	f^#(x,y,s(0))	(21)
*^#(x,s(y))	→	*^#(x,y)	(22)
f^#(x,s(y),z)	→	*^#(x,z)	(23)
f^#(x,s(y),z)	→	half^#(s(y))	(24)
f^#(x,s(y),z)	→	odd^#(s(y))	(25)
half^#(s(s(x)))	→	half^#(x)	(26)
-^#(s(x),s(y))	→	-^#(x,y)	(27)
f^#(x,s(y),z)	→	f^#(*(x,x),half(s(y)),z)	(28)
f^#(x,s(y),z)	→	if^#(odd(s(y)),f(x,y,(x,z)),f((x,x),half(s(y)),z))	(29)

1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.

The 1^st component contains the pair

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

→

-^#(x,y)

(27)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 1
[pow(x₁, x₂)]	=	0
[false]	=	0
[*^#(x₁, x₂)]	=	0
[half^#(x₁)]	=	0
[true]	=	0
[pow^#(x₁, x₂)]	=	0
[f(x₁, x₂, x₃)]	=	0
[half(x₁)]	=	0
[0]	=	0
[if(x₁, x₂, x₃)]	=	0
[-(x₁, x₂)]	=	0
[f^#(x₁, x₂, x₃)]	=	0
[odd^#(x₁)]	=	0
[odd(x₁)]	=	0
[-^#(x₁, x₂)]	=	x₁ + x₂ + 0
[if^#(x₁, x₂, x₃)]	=	0
[+(x₁, x₂)]	=	0
[*(x₁, x₂)]	=	0

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

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

→

-^#(x,y)

(27)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

f^#(x,s(y),z)	→	f^#(*(x,x),half(s(y)),z)	(28)
f^#(x,s(y),z)	→	f^#(x,y,*(x,z))	(19)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 1
[pow(x₁, x₂)]	=	0
[false]	=	0
[*^#(x₁, x₂)]	=	0
[half^#(x₁)]	=	0
[true]	=	0
[pow^#(x₁, x₂)]	=	0
[f(x₁, x₂, x₃)]	=	0
[half(x₁)]	=	x₁ + 0
[0]	=	2
[if(x₁, x₂, x₃)]	=	0
[-(x₁, x₂)]	=	0
[f^#(x₁, x₂, x₃)]	=	x₂ + 0
[odd^#(x₁)]	=	0
[odd(x₁)]	=	0
[-^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[+(x₁, x₂)]	=	x₁ + 1
[*(x₁, x₂)]	=	1

together with the usable rules

half(0)	→	0	(10)
half(s(s(x)))	→	s(half(x))	(12)
half(s(0))	→	0	(11)

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

f^#(x,s(y),z)

→

f^#(x,y,*(x,z))

(19)

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

f^#(x,s(y),z)

→

f^#(*(x,x),half(s(y)),z)

(28)

1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(f)	=	2
π(-)	=	2
π(f^#)	=	2

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

prec(s)	=	1	status(s)	=	[]	list-extension(s)	=	Lex
prec(pow)	=	0	status(pow)	=	[1, 2]	list-extension(pow)	=	Lex
prec(false)	=	0	status(false)	=	[]	list-extension(false)	=	Lex
prec(*^#)	=	0	status(*^#)	=	[2, 1]	list-extension(*^#)	=	Lex
prec(half^#)	=	0	status(half^#)	=	[]	list-extension(half^#)	=	Lex
prec(true)	=	0	status(true)	=	[]	list-extension(true)	=	Lex
prec(pow^#)	=	0	status(pow^#)	=	[2]	list-extension(pow^#)	=	Lex
prec(half)	=	0	status(half)	=	[]	list-extension(half)	=	Lex
prec(0)	=	0	status(0)	=	[]	list-extension(0)	=	Lex
prec(if)	=	0	status(if)	=	[3]	list-extension(if)	=	Lex
prec(odd^#)	=	0	status(odd^#)	=	[]	list-extension(odd^#)	=	Lex
prec(odd)	=	0	status(odd)	=	[]	list-extension(odd)	=	Lex
prec(-^#)	=	0	status(-^#)	=	[1, 2]	list-extension(-^#)	=	Lex
prec(if^#)	=	0	status(if^#)	=	[3, 2, 1]	list-extension(if^#)	=	Lex
prec(+)	=	3	status(+)	=	[]	list-extension(+)	=	Lex
prec(*)	=	3	status(*)	=	[]	list-extension(*)	=	Lex

and the following Max-polynomial interpretation

[s(x₁)]	=	x₁ + 28102
[pow(x₁, x₂)]	=	x₁ + x₂ + 1
[false]	=	0
[*^#(x₁, x₂)]	=	max(x₁ + 1, x₂ + 1, 0)
[half^#(x₁)]	=	1
[true]	=	0
[pow^#(x₁, x₂)]	=	x₂ + 1
[half(x₁)]	=	x₁ + 0
[0]	=	1
[if(x₁, x₂, x₃)]	=	x₃ + 1
[odd^#(x₁)]	=	1
[odd(x₁)]	=	1
[-^#(x₁, x₂)]	=	x₁ + x₂ + 1
[if^#(x₁, x₂, x₃)]	=	max(x₁ + 1, x₂ + 1, x₃ + 1, 0)
[+(x₁, x₂)]	=	max(x₂ + 1, 0)
[*(x₁, x₂)]	=	max(0)

together with the usable rules

half(0)	→	0	(10)
half(s(s(x)))	→	s(half(x))	(12)
half(s(0))	→	0	(11)

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

f^#(x,s(y),z)

→

f^#(*(x,x),half(s(y)),z)

(28)

could be deleted.

1.1.2.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

half^#(s(s(x)))

→

half^#(x)

(26)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 1
[pow(x₁, x₂)]	=	0
[false]	=	0
[*^#(x₁, x₂)]	=	0
[half^#(x₁)]	=	x₁ + 0
[true]	=	0
[pow^#(x₁, x₂)]	=	0
[f(x₁, x₂, x₃)]	=	0
[half(x₁)]	=	20819
[0]	=	20820
[if(x₁, x₂, x₃)]	=	0
[-(x₁, x₂)]	=	0
[f^#(x₁, x₂, x₃)]	=	0
[odd^#(x₁)]	=	0
[odd(x₁)]	=	0
[-^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[+(x₁, x₂)]	=	x₁ + 1
[*(x₁, x₂)]	=	1

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

half^#(s(s(x)))

→

half^#(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

*^#(x,s(y))

→

*^#(x,y)

(22)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 1
[pow(x₁, x₂)]	=	0
[false]	=	0
[*^#(x₁, x₂)]	=	x₂ + 0
[half^#(x₁)]	=	0
[true]	=	0
[pow^#(x₁, x₂)]	=	0
[f(x₁, x₂, x₃)]	=	0
[half(x₁)]	=	1
[0]	=	2
[if(x₁, x₂, x₃)]	=	0
[-(x₁, x₂)]	=	0
[f^#(x₁, x₂, x₃)]	=	0
[odd^#(x₁)]	=	0
[odd(x₁)]	=	0
[-^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[+(x₁, x₂)]	=	x₁ + 1
[*(x₁, x₂)]	=	1

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

*^#(x,s(y))

→

*^#(x,y)

(22)

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

odd^#(s(s(x)))

→

odd^#(x)

(18)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[s(x₁)]	=	x₁ + 1
[pow(x₁, x₂)]	=	0
[false]	=	0
[*^#(x₁, x₂)]	=	0
[half^#(x₁)]	=	0
[true]	=	0
[pow^#(x₁, x₂)]	=	0
[f(x₁, x₂, x₃)]	=	0
[half(x₁)]	=	1
[0]	=	2
[if(x₁, x₂, x₃)]	=	0
[-(x₁, x₂)]	=	0
[f^#(x₁, x₂, x₃)]	=	0
[odd^#(x₁)]	=	x₁ + 0
[odd(x₁)]	=	0
[-^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[+(x₁, x₂)]	=	x₁ + 1
[*(x₁, x₂)]	=	1

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

odd^#(s(s(x)))

→

odd^#(x)

(18)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 0 components.