Certification Problem

Input (TPDB SRS_Standard/Trafo_06/dup09)

The rewrite relation of the following TRS is considered.

0(0(((x1))))	→	((1(1(x1))))	(1)
1(1(((x1))))	→	0(0(#(#(x1))))	(2)
#(#(0(0(x1))))	→	0(0(#(#(x1))))	(3)
#(#(1(1(x1))))	→	1(1(#(#(x1))))	(4)
#(#($($(x1))))	→	(($($(x1))))	(5)
#(#(#(#(x1))))	→	#(#(x1))	(6)
#(#(((x1))))	→	((x1))	(7)

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.

1^#(1(((x1))))	→	0^#(#(#(x1)))	(8)
#^#(#(0(0(x1))))	→	0^#(#(#(x1)))	(9)
#^#(#(1(1(x1))))	→	#^#(#(x1))	(10)
0^#(0(((x1))))	→	1^#(1(x1))	(11)
#^#(#(1(1(x1))))	→	1^#(1(#(#(x1))))	(12)
#^#(#(1(1(x1))))	→	1^#(#(#(x1)))	(13)
#^#(#(1(1(x1))))	→	#^#(x1)	(14)
#^#(#(0(0(x1))))	→	#^#(#(x1))	(15)
0^#(0(((x1))))	→	1^#(x1)	(16)
#^#(#(0(0(x1))))	→	0^#(0(#(#(x1))))	(17)
1^#(1(((x1))))	→	#^#(#(x1))	(18)
1^#(1(((x1))))	→	0^#(0(#(#(x1))))	(19)
#^#(#(0(0(x1))))	→	#^#(x1)	(20)
1^#(1(((x1))))	→	#^#(x1)	(21)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

1^#(1(((x1))))	→	#^#(x1)	(21)
#^#(#(1(1(x1))))	→	#^#(x1)	(14)
#^#(#(1(1(x1))))	→	1^#(#(#(x1)))	(13)
#^#(#(0(0(x1))))	→	#^#(x1)	(20)
1^#(1(((x1))))	→	0^#(0(#(#(x1))))	(19)
1^#(1(((x1))))	→	#^#(#(x1))	(18)
#^#(#(1(1(x1))))	→	1^#(1(#(#(x1))))	(12)
0^#(0(((x1))))	→	1^#(1(x1))	(11)
#^#(#(1(1(x1))))	→	#^#(#(x1))	(10)
#^#(#(0(0(x1))))	→	0^#(#(#(x1)))	(9)
#^#(#(0(0(x1))))	→	0^#(0(#(#(x1))))	(17)
0^#(0(((x1))))	→	1^#(x1)	(16)
#^#(#(0(0(x1))))	→	#^#(#(x1))	(15)
1^#(1(((x1))))	→	0^#(#(#(x1)))	(8)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	x₁ + 0
[1(x₁)]	=	x₁ + 10451
[#^#(x₁)]	=	x₁ + 107307
[#(x₁)]	=	x₁ + 32286
[0(x₁)]	=	x₁ + 10451
[$(x₁)]	=	36466
[1^#(x₁)]	=	x₁ + 64571
[*(x₁)]	=	x₁ + 32286

together with the usable rules

#(#(1(1(x1))))	→	1(1(#(#(x1))))	(4)
0(0(((x1))))	→	((1(1(x1))))	(1)
#(#(0(0(x1))))	→	0(0(#(#(x1))))	(3)
#(#($($(x1))))	→	(($($(x1))))	(5)
#(#(((x1))))	→	((x1))	(7)
#(#(#(#(x1))))	→	#(#(x1))	(6)
1(1(((x1))))	→	0(0(#(#(x1))))	(2)

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

1^#(1(((x1))))	→	#^#(x1)	(21)
#^#(#(1(1(x1))))	→	#^#(x1)	(14)
#^#(#(1(1(x1))))	→	1^#(#(#(x1)))	(13)
#^#(#(0(0(x1))))	→	#^#(x1)	(20)
1^#(1(((x1))))	→	0^#(0(#(#(x1))))	(19)
1^#(1(((x1))))	→	#^#(#(x1))	(18)
#^#(#(1(1(x1))))	→	1^#(1(#(#(x1))))	(12)
0^#(0(((x1))))	→	1^#(1(x1))	(11)
#^#(#(1(1(x1))))	→	#^#(#(x1))	(10)
#^#(#(0(0(x1))))	→	0^#(#(#(x1)))	(9)
#^#(#(0(0(x1))))	→	0^#(0(#(#(x1))))	(17)
0^#(0(((x1))))	→	1^#(x1)	(16)
#^#(#(0(0(x1))))	→	#^#(#(x1))	(15)
1^#(1(((x1))))	→	0^#(#(#(x1)))	(8)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.