Certification Problem

Input (TPDB TRS_Standard/CiME_04/log2)

The rewrite relation of the following TRS is considered.

0(#)	→	#	(1)
+(#,x)	→	x	(2)
+(x,#)	→	x	(3)
+(0(x),0(y))	→	0(+(x,y))	(4)
+(0(x),1(y))	→	1(+(x,y))	(5)
+(1(x),0(y))	→	1(+(x,y))	(6)
+(1(x),1(y))	→	0(+(+(x,y),1(#)))	(7)
+(+(x,y),z)	→	+(x,+(y,z))	(8)
-(#,x)	→	#	(9)
-(x,#)	→	x	(10)
-(0(x),0(y))	→	0(-(x,y))	(11)
-(0(x),1(y))	→	1(-(-(x,y),1(#)))	(12)
-(1(x),0(y))	→	1(-(x,y))	(13)
-(1(x),1(y))	→	0(-(x,y))	(14)
not(true)	→	false	(15)
not(false)	→	true	(16)
if(true,x,y)	→	x	(17)
if(false,x,y)	→	y	(18)
ge(0(x),0(y))	→	ge(x,y)	(19)
ge(0(x),1(y))	→	not(ge(y,x))	(20)
ge(1(x),0(y))	→	ge(x,y)	(21)
ge(1(x),1(y))	→	ge(x,y)	(22)
ge(x,#)	→	true	(23)
ge(#,0(x))	→	ge(#,x)	(24)
ge(#,1(x))	→	false	(25)
log(x)	→	-(log'(x),1(#))	(26)
log'(#)	→	#	(27)
log'(1(x))	→	+(log'(x),1(#))	(28)
log'(0(x))	→	if(ge(x,1(#)),+(log'(x),1(#)),#)	(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.

log'^#(0(x))	→	ge^#(x,1(#))	(30)
+^#(0(x),0(y))	→	0^#(+(x,y))	(31)
-^#(1(x),0(y))	→	-^#(x,y)	(32)
-^#(1(x),1(y))	→	-^#(x,y)	(33)
ge^#(#,0(x))	→	ge^#(#,x)	(34)
-^#(0(x),1(y))	→	-^#(x,y)	(35)
log^#(x)	→	-^#(log'(x),1(#))	(36)
ge^#(0(x),0(y))	→	ge^#(x,y)	(37)
-^#(1(x),1(y))	→	0^#(-(x,y))	(38)
ge^#(0(x),1(y))	→	not^#(ge(y,x))	(39)
+^#(0(x),0(y))	→	+^#(x,y)	(40)
log^#(x)	→	log'^#(x)	(41)
log'^#(1(x))	→	+^#(log'(x),1(#))	(42)
-^#(0(x),0(y))	→	0^#(-(x,y))	(43)
-^#(0(x),1(y))	→	-^#(-(x,y),1(#))	(44)
+^#(1(x),0(y))	→	+^#(x,y)	(45)
+^#(+(x,y),z)	→	+^#(y,z)	(46)
ge^#(1(x),1(y))	→	ge^#(x,y)	(47)
+^#(+(x,y),z)	→	+^#(x,+(y,z))	(48)
+^#(1(x),1(y))	→	+^#(+(x,y),1(#))	(49)
+^#(0(x),1(y))	→	+^#(x,y)	(50)
ge^#(1(x),0(y))	→	ge^#(x,y)	(51)
log'^#(1(x))	→	log'^#(x)	(52)
+^#(1(x),1(y))	→	0^#(+(+(x,y),1(#)))	(53)
log'^#(0(x))	→	+^#(log'(x),1(#))	(54)
log'^#(0(x))	→	if^#(ge(x,1(#)),+(log'(x),1(#)),#)	(55)
-^#(0(x),0(y))	→	-^#(x,y)	(56)
ge^#(0(x),1(y))	→	ge^#(y,x)	(57)
log'^#(0(x))	→	log'^#(x)	(58)
+^#(1(x),1(y))	→	+^#(x,y)	(59)

1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.

The 1^st component contains the pair

log'^#(0(x))	→	log'^#(x)	(58)
log'^#(1(x))	→	log'^#(x)	(52)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	x₁ + 1
[false]	=	0
[ge^#(x₁, x₂)]	=	0
[log^#(x₁)]	=	0
[#]	=	0
[true]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	x₁ + 1
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[log'^#(x₁)]	=	x₁ + 0
[-(x₁, x₂)]	=	0
[-^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[+(x₁, x₂)]	=	0
[log'(x₁)]	=	0
[+^#(x₁, x₂)]	=	0
[not(x₁)]	=	0

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

log'^#(0(x))	→	log'^#(x)	(58)
log'^#(1(x))	→	log'^#(x)	(52)

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

-^#(0(x),0(y))	→	-^#(x,y)	(56)
-^#(0(x),1(y))	→	-^#(x,y)	(35)
-^#(1(x),1(y))	→	-^#(x,y)	(33)
-^#(1(x),0(y))	→	-^#(x,y)	(32)
-^#(0(x),1(y))	→	-^#(-(x,y),1(#))	(44)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	x₁ + 2
[false]	=	0
[ge^#(x₁, x₂)]	=	0
[log^#(x₁)]	=	0
[#]	=	0
[true]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	x₁ + 1
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[log'^#(x₁)]	=	0
[-(x₁, x₂)]	=	x₂ + 1
[-^#(x₁, x₂)]	=	x₂ + 0
[if^#(x₁, x₂, x₃)]	=	0
[+(x₁, x₂)]	=	0
[log'(x₁)]	=	0
[+^#(x₁, x₂)]	=	0
[not(x₁)]	=	0

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

-^#(0(x),0(y))	→	-^#(x,y)	(56)
-^#(0(x),1(y))	→	-^#(x,y)	(35)
-^#(1(x),1(y))	→	-^#(x,y)	(33)
-^#(1(x),0(y))	→	-^#(x,y)	(32)

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

-^#(0(x),1(y))

→

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

(44)

1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	x₁ + 5854
[false]	=	0
[ge^#(x₁, x₂)]	=	0
[log^#(x₁)]	=	0
[#]	=	0
[true]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	x₁ + 5854
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[log'^#(x₁)]	=	0
[-(x₁, x₂)]	=	x₁ + 0
[-^#(x₁, x₂)]	=	x₁ + 0
[if^#(x₁, x₂, x₃)]	=	0
[+(x₁, x₂)]	=	0
[log'(x₁)]	=	0
[+^#(x₁, x₂)]	=	0
[not(x₁)]	=	0

together with the usable rules

0(#)	→	#	(1)
-(x,#)	→	x	(10)
-(1(x),1(y))	→	0(-(x,y))	(14)
-(0(x),1(y))	→	1(-(-(x,y),1(#)))	(12)
-(0(x),0(y))	→	0(-(x,y))	(11)
-(#,x)	→	#	(9)
-(1(x),0(y))	→	1(-(x,y))	(13)

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

-^#(0(x),1(y))

→

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

(44)

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

ge^#(0(x),1(y))	→	ge^#(y,x)	(57)
ge^#(0(x),0(y))	→	ge^#(x,y)	(37)
ge^#(1(x),0(y))	→	ge^#(x,y)	(51)
ge^#(1(x),1(y))	→	ge^#(x,y)	(47)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	x₁ + 1
[false]	=	0
[ge^#(x₁, x₂)]	=	x₁ + x₂ + 0
[log^#(x₁)]	=	0
[#]	=	0
[true]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	x₁ + 1
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[log'^#(x₁)]	=	0
[-(x₁, x₂)]	=	x₁ + 0
[-^#(x₁, x₂)]	=	x₁ + 0
[if^#(x₁, x₂, x₃)]	=	0
[+(x₁, x₂)]	=	0
[log'(x₁)]	=	0
[+^#(x₁, x₂)]	=	0
[not(x₁)]	=	0

together with the usable rules

0(#)	→	#	(1)
-(x,#)	→	x	(10)
-(1(x),1(y))	→	0(-(x,y))	(14)
-(0(x),1(y))	→	1(-(-(x,y),1(#)))	(12)
-(0(x),0(y))	→	0(-(x,y))	(11)
-(#,x)	→	#	(9)
-(1(x),0(y))	→	1(-(x,y))	(13)

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

ge^#(0(x),1(y))	→	ge^#(y,x)	(57)
ge^#(0(x),0(y))	→	ge^#(x,y)	(37)
ge^#(1(x),0(y))	→	ge^#(x,y)	(51)
ge^#(1(x),1(y))	→	ge^#(x,y)	(47)

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

ge^#(#,0(x))

→

ge^#(#,x)

(34)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	x₁ + 1
[false]	=	0
[ge^#(x₁, x₂)]	=	x₂ + 0
[log^#(x₁)]	=	0
[#]	=	0
[true]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	x₁ + 1
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[log'^#(x₁)]	=	0
[-(x₁, x₂)]	=	x₁ + 0
[-^#(x₁, x₂)]	=	x₁ + 0
[if^#(x₁, x₂, x₃)]	=	0
[+(x₁, x₂)]	=	0
[log'(x₁)]	=	0
[+^#(x₁, x₂)]	=	0
[not(x₁)]	=	0

together with the usable rules

0(#)	→	#	(1)
-(x,#)	→	x	(10)
-(1(x),1(y))	→	0(-(x,y))	(14)
-(0(x),1(y))	→	1(-(-(x,y),1(#)))	(12)
-(0(x),0(y))	→	0(-(x,y))	(11)
-(#,x)	→	#	(9)
-(1(x),0(y))	→	1(-(x,y))	(13)

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

ge^#(#,0(x))

→

ge^#(#,x)

(34)

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

+^#(1(x),1(y))	→	+^#(x,y)	(59)
+^#(0(x),0(y))	→	+^#(x,y)	(40)
+^#(0(x),1(y))	→	+^#(x,y)	(50)
+^#(1(x),1(y))	→	+^#(+(x,y),1(#))	(49)
+^#(+(x,y),z)	→	+^#(x,+(y,z))	(48)
+^#(+(x,y),z)	→	+^#(y,z)	(46)
+^#(1(x),0(y))	→	+^#(x,y)	(45)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	x₁ + 24867
[false]	=	0
[ge^#(x₁, x₂)]	=	0
[log^#(x₁)]	=	0
[#]	=	0
[true]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	x₁ + 24867
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[log'^#(x₁)]	=	0
[-(x₁, x₂)]	=	x₁ + 0
[-^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[+(x₁, x₂)]	=	x₁ + x₂ + 0
[log'(x₁)]	=	0
[+^#(x₁, x₂)]	=	x₁ + x₂ + 0
[not(x₁)]	=	0

together with the usable rules

+(0(x),0(y))	→	0(+(x,y))	(4)
+(+(x,y),z)	→	+(x,+(y,z))	(8)
0(#)	→	#	(1)
+(x,#)	→	x	(3)
+(0(x),1(y))	→	1(+(x,y))	(5)
-(x,#)	→	x	(10)
+(1(x),1(y))	→	0(+(+(x,y),1(#)))	(7)
-(1(x),1(y))	→	0(-(x,y))	(14)
-(0(x),1(y))	→	1(-(-(x,y),1(#)))	(12)
-(0(x),0(y))	→	0(-(x,y))	(11)
-(#,x)	→	#	(9)
-(1(x),0(y))	→	1(-(x,y))	(13)
+(1(x),0(y))	→	1(+(x,y))	(6)
+(#,x)	→	x	(2)

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

+^#(1(x),1(y))	→	+^#(x,y)	(59)
+^#(0(x),0(y))	→	+^#(x,y)	(40)
+^#(0(x),1(y))	→	+^#(x,y)	(50)
+^#(1(x),1(y))	→	+^#(+(x,y),1(#))	(49)
+^#(1(x),0(y))	→	+^#(x,y)	(45)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

+^#(+(x,y),z)	→	+^#(y,z)	(46)
+^#(+(x,y),z)	→	+^#(x,+(y,z))	(48)

1.1.5.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	1036
[false]	=	0
[ge^#(x₁, x₂)]	=	0
[log^#(x₁)]	=	0
[#]	=	1
[true]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	2
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[log'^#(x₁)]	=	0
[-(x₁, x₂)]	=	x₁ + 3564
[-^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[+(x₁, x₂)]	=	x₁ + x₂ + 1
[log'(x₁)]	=	0
[+^#(x₁, x₂)]	=	x₁ + 0
[not(x₁)]	=	0

together with the usable rules

+(0(x),0(y))	→	0(+(x,y))	(4)
+(+(x,y),z)	→	+(x,+(y,z))	(8)
0(#)	→	#	(1)
+(x,#)	→	x	(3)
+(0(x),1(y))	→	1(+(x,y))	(5)
-(x,#)	→	x	(10)
+(1(x),1(y))	→	0(+(+(x,y),1(#)))	(7)
-(1(x),1(y))	→	0(-(x,y))	(14)
-(0(x),1(y))	→	1(-(-(x,y),1(#)))	(12)
-(#,x)	→	#	(9)
-(1(x),0(y))	→	1(-(x,y))	(13)
+(1(x),0(y))	→	1(+(x,y))	(6)
+(#,x)	→	x	(2)

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

+^#(+(x,y),z)	→	+^#(y,z)	(46)
+^#(+(x,y),z)	→	+^#(x,+(y,z))	(48)

could be deleted.

1.1.5.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.