Certification Problem

Input (TPDB TRS_Standard/CiME_04/list-sum-prod-bin-assoc-distr-app)

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)
*(0(x),y)	→	0(*(x,y))	(10)
*(1(x),y)	→	+(0(*(x,y)),y)	(11)
((x,y),z)	→	(x,(y,z))	(12)
*(x,+(y,z))	→	+((x,y),(x,z))	(13)
app(nil,l)	→	l	(14)
app(cons(x,l1),l2)	→	cons(x,app(l1,l2))	(15)
sum(nil)	→	0(#)	(16)
sum(cons(x,l))	→	+(x,sum(l))	(17)
sum(app(l1,l2))	→	+(sum(l1),sum(l2))	(18)
prod(nil)	→	1(#)	(19)
prod(cons(x,l))	→	*(x,prod(l))	(20)
prod(app(l1,l2))	→	*(prod(l1),prod(l2))	(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.

*^#(x,+(y,z))	→	+^#((x,y),(x,z))	(22)
sum^#(app(l1,l2))	→	+^#(sum(l1),sum(l2))	(23)
*^#(1(x),y)	→	0^#(*(x,y))	(24)
+^#(1(x),1(y))	→	+^#(+(x,y),1(#))	(25)
^#((x,y),z)	→	*^#(y,z)	(26)
prod^#(cons(x,l))	→	prod^#(l)	(27)
+^#(+(x,y),z)	→	+^#(x,+(y,z))	(28)
sum^#(nil)	→	0^#(#)	(29)
+^#(1(x),1(y))	→	0^#(+(+(x,y),1(#)))	(30)
sum^#(app(l1,l2))	→	sum^#(l2)	(31)
+^#(1(x),1(y))	→	+^#(x,y)	(32)
sum^#(app(l1,l2))	→	sum^#(l1)	(33)
+^#(+(x,y),z)	→	+^#(y,z)	(34)
prod^#(app(l1,l2))	→	*^#(prod(l1),prod(l2))	(35)
*^#(1(x),y)	→	*^#(x,y)	(36)
prod^#(cons(x,l))	→	*^#(x,prod(l))	(37)
*^#(1(x),y)	→	+^#(0(*(x,y)),y)	(38)
+^#(0(x),0(y))	→	+^#(x,y)	(39)
prod^#(app(l1,l2))	→	prod^#(l2)	(40)
+^#(0(x),0(y))	→	0^#(+(x,y))	(41)
+^#(0(x),1(y))	→	+^#(x,y)	(42)
sum^#(cons(x,l))	→	sum^#(l)	(43)
app^#(cons(x,l1),l2)	→	app^#(l1,l2)	(44)
prod^#(app(l1,l2))	→	prod^#(l1)	(45)
*^#(0(x),y)	→	*^#(x,y)	(46)
*^#(x,+(y,z))	→	*^#(x,y)	(47)
+^#(1(x),0(y))	→	+^#(x,y)	(48)
^#((x,y),z)	→	^#(x,(y,z))	(49)
*^#(0(x),y)	→	0^#(*(x,y))	(50)
*^#(x,+(y,z))	→	*^#(x,z)	(51)
sum^#(cons(x,l))	→	+^#(x,sum(l))	(52)

1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.

The 1^st component contains the pair

app^#(cons(x,l1),l2)

→

app^#(l1,l2)

(44)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	0
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[*^#(x₁, x₂)]	=	0
[#]	=	0
[sum(x₁)]	=	0
[0(x₁)]	=	0
[nil]	=	0
[app^#(x₁, x₂)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₂ + 1
[+(x₁, x₂)]	=	0
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	0
[*(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	0

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

app^#(cons(x,l1),l2)

→

app^#(l1,l2)

(44)

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

sum^#(app(l1,l2))	→	sum^#(l1)	(33)
sum^#(app(l1,l2))	→	sum^#(l2)	(31)
sum^#(cons(x,l))	→	sum^#(l)	(43)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	0
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[*^#(x₁, x₂)]	=	0
[#]	=	0
[sum(x₁)]	=	0
[0(x₁)]	=	0
[nil]	=	0
[app^#(x₁, x₂)]	=	0
[cons(x₁, x₂)]	=	x₂ + 1
[+(x₁, x₂)]	=	0
[sum^#(x₁)]	=	x₁ + 0
[+^#(x₁, x₂)]	=	0
[*(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	x₁ + x₂ + 1

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

sum^#(app(l1,l2))	→	sum^#(l1)	(33)
sum^#(app(l1,l2))	→	sum^#(l2)	(31)
sum^#(cons(x,l))	→	sum^#(l)	(43)

could be deleted.

1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

prod^#(app(l1,l2))	→	prod^#(l1)	(45)
prod^#(cons(x,l))	→	prod^#(l)	(27)
prod^#(app(l1,l2))	→	prod^#(l2)	(40)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	0
[prod(x₁)]	=	0
[prod^#(x₁)]	=	x₁ + 0
[*^#(x₁, x₂)]	=	0
[#]	=	0
[sum(x₁)]	=	0
[0(x₁)]	=	0
[nil]	=	0
[app^#(x₁, x₂)]	=	0
[cons(x₁, x₂)]	=	x₂ + 1
[+(x₁, x₂)]	=	0
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	0
[*(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	x₁ + x₂ + 1

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

prod^#(app(l1,l2))	→	prod^#(l1)	(45)
prod^#(cons(x,l))	→	prod^#(l)	(27)
prod^#(app(l1,l2))	→	prod^#(l2)	(40)

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,+(y,z))	→	*^#(x,z)	(51)
^#((x,y),z)	→	^#(x,(y,z))	(49)
*^#(x,+(y,z))	→	*^#(x,y)	(47)
*^#(0(x),y)	→	*^#(x,y)	(46)
^#((x,y),z)	→	*^#(y,z)	(26)
*^#(1(x),y)	→	*^#(x,y)	(36)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	x₁ + 2
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[*^#(x₁, x₂)]	=	x₁ + 0
[#]	=	1
[sum(x₁)]	=	0
[0(x₁)]	=	x₁ + 1
[nil]	=	0
[app^#(x₁, x₂)]	=	0
[cons(x₁, x₂)]	=	1
[+(x₁, x₂)]	=	x₂ + 4
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	0
[*(x₁, x₂)]	=	x₁ + x₂ + 1
[app(x₁, x₂)]	=	1

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

^#((x,y),z)	→	^#(x,(y,z))	(49)
*^#(0(x),y)	→	*^#(x,y)	(46)
^#((x,y),z)	→	*^#(y,z)	(26)
*^#(1(x),y)	→	*^#(x,y)	(36)

could be deleted.

1.1.4.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

*^#(x,+(y,z))	→	*^#(x,z)	(51)
*^#(x,+(y,z))	→	*^#(x,y)	(47)

1.1.4.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	0
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[*^#(x₁, x₂)]	=	max(x₂ + 1, 0)
[#]	=	0
[sum(x₁)]	=	0
[0(x₁)]	=	0
[nil]	=	0
[app^#(x₁, x₂)]	=	max(0)
[cons(x₁, x₂)]	=	max(0)
[+(x₁, x₂)]	=	max(x₁ + 1, x₂ + 0, 0)
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	max(0)
[*(x₁, x₂)]	=	max(0)
[app(x₁, x₂)]	=	max(0)

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

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

→

*^#(x,y)

(47)

could be deleted.

1.1.4.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

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

→

*^#(x,z)

(51)

1.1.4.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	0
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[*^#(x₁, x₂)]	=	max(x₂ + 11293, 0)
[#]	=	0
[sum(x₁)]	=	0
[0(x₁)]	=	0
[nil]	=	0
[app^#(x₁, x₂)]	=	max(0)
[cons(x₁, x₂)]	=	max(0)
[+(x₁, x₂)]	=	max(x₂ + 21239, 0)
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	max(0)
[*(x₁, x₂)]	=	max(0)
[app(x₁, x₂)]	=	max(0)

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

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

→

*^#(x,z)

(51)

could be deleted.

1.1.4.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 5^th component contains the pair

+^#(+(x,y),z)	→	+^#(y,z)	(34)
+^#(1(x),1(y))	→	+^#(x,y)	(32)
+^#(1(x),0(y))	→	+^#(x,y)	(48)
+^#(+(x,y),z)	→	+^#(x,+(y,z))	(28)
+^#(1(x),1(y))	→	+^#(+(x,y),1(#))	(25)
+^#(0(x),1(y))	→	+^#(x,y)	(42)
+^#(0(x),0(y))	→	+^#(x,y)	(39)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	x₁ + 1427
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[*^#(x₁, x₂)]	=	0
[#]	=	2
[sum(x₁)]	=	0
[0(x₁)]	=	x₁ + 1
[nil]	=	0
[app^#(x₁, x₂)]	=	0
[cons(x₁, x₂)]	=	1
[+(x₁, x₂)]	=	x₁ + x₂ + 1424
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	x₁ + x₂ + 0
[*(x₁, x₂)]	=	1
[app(x₁, x₂)]	=	1

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)
+(1(x),1(y))	→	0(+(+(x,y),1(#)))	(7)
+(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)	(34)
+^#(1(x),1(y))	→	+^#(x,y)	(32)
+^#(1(x),0(y))	→	+^#(x,y)	(48)
+^#(1(x),1(y))	→	+^#(+(x,y),1(#))	(25)
+^#(0(x),1(y))	→	+^#(x,y)	(42)
+^#(0(x),0(y))	→	+^#(x,y)	(39)

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)

→

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

(28)

1.1.5.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	x₁ + 37083
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[*^#(x₁, x₂)]	=	0
[#]	=	35658
[sum(x₁)]	=	0
[0(x₁)]	=	x₁ + 1
[nil]	=	0
[app^#(x₁, x₂)]	=	0
[cons(x₁, x₂)]	=	1
[+(x₁, x₂)]	=	x₁ + x₂ + 1424
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	x₁ + 0
[*(x₁, x₂)]	=	35657
[app(x₁, x₂)]	=	1

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)
+(1(x),1(y))	→	0(+(+(x,y),1(#)))	(7)
+(1(x),0(y))	→	1(+(x,y))	(6)
+(x,#)	→	x	(2)

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

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

→

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

(28)

could be deleted.

1.1.5.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.