Certification Problem

Input (TPDB TRS_Standard/AProVE_07/wiehe01)

The rewrite relation of the following TRS is considered.

times(x,0)	→	0	(1)
times(x,s(y))	→	plus(times(x,y),x)	(2)
plus(s(x),s(y))	→	s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))))	(3)
plus(s(x),x)	→	plus(if(gt(x,x),id(x),id(x)),s(x))	(4)
plus(zero,y)	→	y	(5)
plus(id(x),s(y))	→	s(plus(x,if(gt(s(y),y),y,s(y))))	(6)
id(x)	→	x	(7)
if(true,x,y)	→	x	(8)
if(false,x,y)	→	y	(9)
not(x)	→	if(x,false,true)	(10)
gt(s(x),zero)	→	true	(11)
gt(zero,y)	→	false	(12)
gt(s(x),s(y))	→	gt(x,y)	(13)

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.

times^#(x,s(y))	→	times^#(x,y)	(14)
gt^#(s(x),s(y))	→	gt^#(x,y)	(15)
plus^#(s(x),s(y))	→	gt^#(x,y)	(16)
plus^#(s(x),s(y))	→	if^#(gt(x,y),x,y)	(17)
plus^#(s(x),s(y))	→	if^#(not(gt(x,y)),id(x),id(y))	(18)
plus^#(s(x),s(y))	→	not^#(gt(x,y))	(19)
plus^#(s(x),s(y))	→	id^#(x)	(20)
plus^#(s(x),x)	→	id^#(x)	(21)
not^#(x)	→	if^#(x,false,true)	(22)
plus^#(s(x),s(y))	→	gt^#(x,y)	(16)
plus^#(id(x),s(y))	→	gt^#(s(y),y)	(23)
plus^#(s(x),x)	→	if^#(gt(x,x),id(x),id(x))	(24)
plus^#(s(x),x)	→	id^#(x)	(21)
plus^#(s(x),x)	→	plus^#(if(gt(x,x),id(x),id(x)),s(x))	(25)
plus^#(id(x),s(y))	→	plus^#(x,if(gt(s(y),y),y,s(y)))	(26)
times^#(x,s(y))	→	plus^#(times(x,y),x)	(27)
plus^#(s(x),s(y))	→	plus^#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))	(28)
plus^#(s(x),s(y))	→	id^#(y)	(29)
plus^#(id(x),s(y))	→	if^#(gt(s(y),y),y,s(y))	(30)
plus^#(s(x),x)	→	gt^#(x,x)	(31)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

The 1^st component contains the pair

times^#(x,s(y))

→

times^#(x,y)

(14)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zero]	=	0
[s(x₁)]	=	x₁ + 1
[gt(x₁, x₂)]	=	0
[plus^#(x₁, x₂)]	=	0
[false]	=	0
[id^#(x₁)]	=	0
[true]	=	0
[not^#(x₁)]	=	0
[times^#(x₁, x₂)]	=	x₂ + 0
[0]	=	0
[if(x₁, x₂, x₃)]	=	0
[times(x₁, x₂)]	=	0
[gt^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[id(x₁)]	=	0
[not(x₁)]	=	0

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

times^#(x,s(y))

→

times^#(x,y)

(14)

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

plus^#(s(x),s(y))	→	plus^#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))	(28)
plus^#(id(x),s(y))	→	plus^#(x,if(gt(s(y),y),y,s(y)))	(26)
plus^#(s(x),x)	→	plus^#(if(gt(x,x),id(x),id(x)),s(x))	(25)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zero]	=	0
[s(x₁)]	=	x₁ + 85474
[gt(x₁, x₂)]	=	max(x₂ + 1, 0)
[plus^#(x₁, x₂)]	=	max(x₁ + 81715, x₂ + 38978, 0)
[false]	=	2
[id^#(x₁)]	=	0
[true]	=	2
[not^#(x₁)]	=	0
[times^#(x₁, x₂)]	=	max(0)
[0]	=	0
[if(x₁, x₂, x₃)]	=	max(x₂ + 42736, x₃ + 0, 0)
[times(x₁, x₂)]	=	max(0)
[gt^#(x₁, x₂)]	=	max(0)
[plus(x₁, x₂)]	=	max(0)
[if^#(x₁, x₂, x₃)]	=	max(0)
[id(x₁)]	=	x₁ + 0
[not(x₁)]	=	x₁ + 0

together with the usable rules

if(true,x,y)	→	x	(8)
id(x)	→	x	(7)
if(false,x,y)	→	y	(9)

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

plus^#(s(x),s(y))	→	plus^#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y)))	(28)
plus^#(s(x),x)	→	plus^#(if(gt(x,x),id(x),id(x)),s(x))	(25)

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

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

→

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

(26)

1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zero]	=	1
[s(x₁)]	=	1
[gt(x₁, x₂)]	=	1
[plus^#(x₁, x₂)]	=	x₁ + 0
[false]	=	1
[id^#(x₁)]	=	0
[true]	=	1
[not^#(x₁)]	=	0
[times^#(x₁, x₂)]	=	0
[0]	=	0
[if(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[times(x₁, x₂)]	=	0
[gt^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[id(x₁)]	=	x₁ + 1
[not(x₁)]	=	1

together with the usable rules

if(true,x,y)	→	x	(8)
id(x)	→	x	(7)
gt(zero,y)	→	false	(12)
gt(s(x),zero)	→	true	(11)
if(false,x,y)	→	y	(9)
gt(s(x),s(y))	→	gt(x,y)	(13)

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

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

→

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

(26)

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

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

→

gt^#(x,y)

(15)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[zero]	=	1
[s(x₁)]	=	x₁ + 1
[gt(x₁, x₂)]	=	1
[plus^#(x₁, x₂)]	=	x₁ + 0
[false]	=	1
[id^#(x₁)]	=	0
[true]	=	1
[not^#(x₁)]	=	0
[times^#(x₁, x₂)]	=	0
[0]	=	0
[if(x₁, x₂, x₃)]	=	x₁ + x₂ + x₃ + 0
[times(x₁, x₂)]	=	0
[gt^#(x₁, x₂)]	=	x₂ + 0
[plus(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[id(x₁)]	=	x₁ + 1
[not(x₁)]	=	1

together with the usable rules

if(true,x,y)	→	x	(8)
id(x)	→	x	(7)
gt(zero,y)	→	false	(12)
gt(s(x),zero)	→	true	(11)
if(false,x,y)	→	y	(9)
gt(s(x),s(y))	→	gt(x,y)	(13)

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

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

→

gt^#(x,y)

(15)

could be deleted.

1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 0 components.