Certification Problem

Input (TPDB TRS_Standard/Various_04/21)

The rewrite relation of the following TRS is considered.

+(p1,p1)	→	p2	(1)
+(p1,+(p2,p2))	→	p5	(2)
+(p5,p5)	→	p10	(3)
+(+(x,y),z)	→	+(x,+(y,z))	(4)
+(p1,+(p1,x))	→	+(p2,x)	(5)
+(p1,+(p2,+(p2,x)))	→	+(p5,x)	(6)
+(p2,p1)	→	+(p1,p2)	(7)
+(p2,+(p1,x))	→	+(p1,+(p2,x))	(8)
+(p2,+(p2,p2))	→	+(p1,p5)	(9)
+(p2,+(p2,+(p2,x)))	→	+(p1,+(p5,x))	(10)
+(p5,p1)	→	+(p1,p5)	(11)
+(p5,+(p1,x))	→	+(p1,+(p5,x))	(12)
+(p5,p2)	→	+(p2,p5)	(13)
+(p5,+(p2,x))	→	+(p2,+(p5,x))	(14)
+(p5,+(p5,x))	→	+(p10,x)	(15)
+(p10,p1)	→	+(p1,p10)	(16)
+(p10,+(p1,x))	→	+(p1,+(p10,x))	(17)
+(p10,p2)	→	+(p2,p10)	(18)
+(p10,+(p2,x))	→	+(p2,+(p10,x))	(19)
+(p10,p5)	→	+(p5,p10)	(20)
+(p10,+(p5,x))	→	+(p5,+(p10,x))	(21)

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.

+^#(p5,p2)	→	+^#(p2,p5)	(22)
+^#(p5,+(p1,x))	→	+^#(p5,x)	(23)
+^#(p1,+(p1,x))	→	+^#(p2,x)	(24)
+^#(p10,p5)	→	+^#(p5,p10)	(25)
+^#(p2,+(p2,+(p2,x)))	→	+^#(p1,+(p5,x))	(26)
+^#(+(x,y),z)	→	+^#(x,+(y,z))	(27)
+^#(p5,+(p5,x))	→	+^#(p10,x)	(28)
+^#(p2,+(p2,+(p2,x)))	→	+^#(p5,x)	(29)
+^#(p10,+(p1,x))	→	+^#(p1,+(p10,x))	(30)
+^#(+(x,y),z)	→	+^#(y,z)	(31)
+^#(p10,p1)	→	+^#(p1,p10)	(32)
+^#(p5,+(p2,x))	→	+^#(p2,+(p5,x))	(33)
+^#(p2,p1)	→	+^#(p1,p2)	(34)
+^#(p5,+(p1,x))	→	+^#(p1,+(p5,x))	(35)
+^#(p2,+(p1,x))	→	+^#(p2,x)	(36)
+^#(p10,+(p2,x))	→	+^#(p10,x)	(37)
+^#(p10,+(p5,x))	→	+^#(p10,x)	(38)
+^#(p10,p2)	→	+^#(p2,p10)	(39)
+^#(p2,+(p1,x))	→	+^#(p1,+(p2,x))	(40)
+^#(p10,+(p2,x))	→	+^#(p2,+(p10,x))	(41)
+^#(p2,+(p2,p2))	→	+^#(p1,p5)	(42)
+^#(p1,+(p2,+(p2,x)))	→	+^#(p5,x)	(43)
+^#(p5,+(p2,x))	→	+^#(p5,x)	(44)
+^#(p10,+(p1,x))	→	+^#(p10,x)	(45)
+^#(p5,p1)	→	+^#(p1,p5)	(46)
+^#(p10,+(p5,x))	→	+^#(p5,+(p10,x))	(47)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

+^#(+(x,y),z) → +^#(y,z) (31)

+^#(+(x,y),z) → +^#(x,+(y,z)) (27)

1.1.1 Reduction Pair Processor with Usable Rules
Using the Max-polynomial interpretation

[p5] = 56473

[p10] = 112948

[p2] = 22588

[+(x₁, x₂)] = x₁ + x₂ + 1

[+^#(x₁, x₂)] = x₁ + 0

[p1] = 11293

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

+^#(+(x,y),z) → +^#(y,z) (31)

+^#(+(x,y),z) → +^#(x,+(y,z)) (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

+^#(p10,+(p5,x))	→	+^#(p5,+(p10,x))	(47)
+^#(p10,+(p1,x))	→	+^#(p1,+(p10,x))	(30)
+^#(p10,+(p1,x))	→	+^#(p10,x)	(45)
+^#(p2,+(p2,+(p2,x)))	→	+^#(p5,x)	(29)
+^#(p5,+(p2,x))	→	+^#(p5,x)	(44)
+^#(p1,+(p2,+(p2,x)))	→	+^#(p5,x)	(43)
+^#(p5,+(p5,x))	→	+^#(p10,x)	(28)
+^#(p10,+(p2,x))	→	+^#(p2,+(p10,x))	(41)
+^#(p2,+(p1,x))	→	+^#(p1,+(p2,x))	(40)
+^#(p2,+(p2,+(p2,x)))	→	+^#(p1,+(p5,x))	(26)
+^#(p1,+(p1,x))	→	+^#(p2,x)	(24)
+^#(p10,+(p5,x))	→	+^#(p10,x)	(38)
+^#(p10,+(p2,x))	→	+^#(p10,x)	(37)
+^#(p5,+(p1,x))	→	+^#(p5,x)	(23)
+^#(p2,+(p1,x))	→	+^#(p2,x)	(36)
+^#(p5,+(p1,x))	→	+^#(p1,+(p5,x))	(35)
+^#(p5,+(p2,x))	→	+^#(p2,+(p5,x))	(33)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[p5]	=	2
[p10]	=	1
[p2]	=	3
[+(x₁, x₂)]	=	x₁ + x₂ + 41063
[+^#(x₁, x₂)]	=	x₂ + 0
[p1]	=	4

together with the usable rules

+(p10,p2)	→	+(p2,p10)	(18)
+(+(x,y),z)	→	+(x,+(y,z))	(4)
+(p5,+(p5,x))	→	+(p10,x)	(15)
+(p2,+(p1,x))	→	+(p1,+(p2,x))	(8)
+(p1,p1)	→	p2	(1)
+(p5,p5)	→	p10	(3)
+(p10,p1)	→	+(p1,p10)	(16)
+(p10,+(p5,x))	→	+(p5,+(p10,x))	(21)
+(p10,+(p2,x))	→	+(p2,+(p10,x))	(19)
+(p10,+(p1,x))	→	+(p1,+(p10,x))	(17)
+(p1,+(p1,x))	→	+(p2,x)	(5)
+(p2,+(p2,+(p2,x)))	→	+(p1,+(p5,x))	(10)
+(p2,p1)	→	+(p1,p2)	(7)
+(p10,p5)	→	+(p5,p10)	(20)
+(p5,+(p2,x))	→	+(p2,+(p5,x))	(14)
+(p5,+(p1,x))	→	+(p1,+(p5,x))	(12)
+(p5,p1)	→	+(p1,p5)	(11)
+(p2,+(p2,p2))	→	+(p1,p5)	(9)
+(p5,p2)	→	+(p2,p5)	(13)
+(p1,+(p2,+(p2,x)))	→	+(p5,x)	(6)
+(p1,+(p2,p2))	→	p5	(2)

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

+^#(p10,+(p5,x))	→	+^#(p5,+(p10,x))	(47)
+^#(p10,+(p1,x))	→	+^#(p1,+(p10,x))	(30)
+^#(p10,+(p1,x))	→	+^#(p10,x)	(45)
+^#(p2,+(p2,+(p2,x)))	→	+^#(p5,x)	(29)
+^#(p5,+(p2,x))	→	+^#(p5,x)	(44)
+^#(p1,+(p2,+(p2,x)))	→	+^#(p5,x)	(43)
+^#(p5,+(p5,x))	→	+^#(p10,x)	(28)
+^#(p10,+(p2,x))	→	+^#(p2,+(p10,x))	(41)
+^#(p2,+(p1,x))	→	+^#(p1,+(p2,x))	(40)
+^#(p2,+(p2,+(p2,x)))	→	+^#(p1,+(p5,x))	(26)
+^#(p1,+(p1,x))	→	+^#(p2,x)	(24)
+^#(p10,+(p5,x))	→	+^#(p10,x)	(38)
+^#(p10,+(p2,x))	→	+^#(p10,x)	(37)
+^#(p5,+(p1,x))	→	+^#(p5,x)	(23)
+^#(p2,+(p1,x))	→	+^#(p2,x)	(36)
+^#(p5,+(p1,x))	→	+^#(p1,+(p5,x))	(35)
+^#(p5,+(p2,x))	→	+^#(p2,+(p5,x))	(33)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.