Certification Problem

Input (TPDB TRS_Standard/Various_04/14)

The rewrite relation of the following TRS is considered.

O(0)	→	0	(1)
+(0,x)	→	x	(2)
+(x,0)	→	x	(3)
+(O(x),O(y))	→	O(+(x,y))	(4)
+(O(x),I(y))	→	I(+(x,y))	(5)
+(I(x),O(y))	→	I(+(x,y))	(6)
+(I(x),I(y))	→	O(+(+(x,y),I(0)))	(7)
+(x,+(y,z))	→	+(+(x,y),z)	(8)
-(x,0)	→	x	(9)
-(0,x)	→	0	(10)
-(O(x),O(y))	→	O(-(x,y))	(11)
-(O(x),I(y))	→	I(-(-(x,y),I(1)))	(12)
-(I(x),O(y))	→	I(-(x,y))	(13)
-(I(x),I(y))	→	O(-(x,y))	(14)
not(true)	→	false	(15)
not(false)	→	true	(16)
and(x,true)	→	x	(17)
and(x,false)	→	false	(18)
if(true,x,y)	→	x	(19)
if(false,x,y)	→	y	(20)
ge(O(x),O(y))	→	ge(x,y)	(21)
ge(O(x),I(y))	→	not(ge(y,x))	(22)
ge(I(x),O(y))	→	ge(x,y)	(23)
ge(I(x),I(y))	→	ge(x,y)	(24)
ge(x,0)	→	true	(25)
ge(0,O(x))	→	ge(0,x)	(26)
ge(0,I(x))	→	false	(27)
Log'(0)	→	0	(28)
Log'(I(x))	→	+(Log'(x),I(0))	(29)
Log'(O(x))	→	if(ge(x,I(0)),+(Log'(x),I(0)),0)	(30)
Log(x)	→	-(Log'(x),I(0))	(31)
Val(L(x))	→	x	(32)
Val(N(x,l,r))	→	x	(33)
Min(L(x))	→	x	(34)
Min(N(x,l,r))	→	Min(l)	(35)
Max(L(x))	→	x	(36)
Max(N(x,l,r))	→	Max(r)	(37)
BS(L(x))	→	true	(38)
BS(N(x,l,r))	→	and(and(ge(x,Max(l)),ge(Min(r),x)),and(BS(l),BS(r)))	(39)
Size(L(x))	→	I(0)	(40)
Size(N(x,l,r))	→	+(+(Size(l),Size(r)),I(1))	(41)
WB(L(x))	→	true	(42)
WB(N(x,l,r))	→	and(if(ge(Size(l),Size(r)),ge(I(0),-(Size(l),Size(r))),ge(I(0),-(Size(r),Size(l)))),and(WB(l),WB(r)))	(43)

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.

WB^#(N(x,l,r))	→	if^#(ge(Size(l),Size(r)),ge(I(0),-(Size(l),Size(r))),ge(I(0),-(Size(r),Size(l))))	(44)
+^#(I(x),I(y))	→	+^#(x,y)	(45)
ge^#(I(x),I(y))	→	ge^#(x,y)	(46)
-^#(I(x),I(y))	→	O^#(-(x,y))	(47)
BS^#(N(x,l,r))	→	ge^#(x,Max(l))	(48)
+^#(I(x),I(y))	→	+^#(+(x,y),I(0))	(49)
+^#(I(x),I(y))	→	O^#(+(+(x,y),I(0)))	(50)
Log'^#(O(x))	→	if^#(ge(x,I(0)),+(Log'(x),I(0)),0)	(51)
BS^#(N(x,l,r))	→	Max^#(l)	(52)
+^#(O(x),I(y))	→	+^#(x,y)	(53)
BS^#(N(x,l,r))	→	ge^#(Min(r),x)	(54)
+^#(x,+(y,z))	→	+^#(+(x,y),z)	(55)
+^#(O(x),O(y))	→	+^#(x,y)	(56)
Log'^#(O(x))	→	ge^#(x,I(0))	(57)
WB^#(N(x,l,r))	→	ge^#(I(0),-(Size(l),Size(r)))	(58)
+^#(x,+(y,z))	→	+^#(x,y)	(59)
ge^#(O(x),I(y))	→	ge^#(y,x)	(60)
Log'^#(O(x))	→	Log'^#(x)	(61)
BS^#(N(x,l,r))	→	BS^#(l)	(62)
WB^#(N(x,l,r))	→	Size^#(l)	(63)
WB^#(N(x,l,r))	→	Size^#(r)	(64)
WB^#(N(x,l,r))	→	-^#(Size(r),Size(l))	(65)
ge^#(O(x),O(y))	→	ge^#(x,y)	(66)
Max^#(N(x,l,r))	→	Max^#(r)	(67)
Size^#(N(x,l,r))	→	Size^#(r)	(68)
BS^#(N(x,l,r))	→	and^#(ge(x,Max(l)),ge(Min(r),x))	(69)
WB^#(N(x,l,r))	→	Size^#(r)	(64)
-^#(O(x),I(y))	→	-^#(-(x,y),I(1))	(70)
ge^#(0,O(x))	→	ge^#(0,x)	(71)
WB^#(N(x,l,r))	→	and^#(WB(l),WB(r))	(72)
ge^#(I(x),O(y))	→	ge^#(x,y)	(73)
BS^#(N(x,l,r))	→	BS^#(r)	(74)
BS^#(N(x,l,r))	→	Min^#(r)	(75)
+^#(I(x),O(y))	→	+^#(x,y)	(76)
Size^#(N(x,l,r))	→	+^#(+(Size(l),Size(r)),I(1))	(77)
WB^#(N(x,l,r))	→	-^#(Size(l),Size(r))	(78)
Log'^#(O(x))	→	+^#(Log'(x),I(0))	(79)
WB^#(N(x,l,r))	→	ge^#(I(0),-(Size(r),Size(l)))	(80)
Log^#(x)	→	-^#(Log'(x),I(0))	(81)
WB^#(N(x,l,r))	→	Size^#(r)	(64)
BS^#(N(x,l,r))	→	and^#(and(ge(x,Max(l)),ge(Min(r),x)),and(BS(l),BS(r)))	(82)
-^#(O(x),O(y))	→	-^#(x,y)	(83)
Size^#(N(x,l,r))	→	Size^#(l)	(84)
Log^#(x)	→	Log'^#(x)	(85)
-^#(O(x),O(y))	→	O^#(-(x,y))	(86)
+^#(O(x),O(y))	→	O^#(+(x,y))	(87)
Log'^#(I(x))	→	+^#(Log'(x),I(0))	(88)
-^#(O(x),I(y))	→	-^#(x,y)	(89)
Min^#(N(x,l,r))	→	Min^#(l)	(90)
-^#(I(x),O(y))	→	-^#(x,y)	(91)
-^#(I(x),I(y))	→	-^#(x,y)	(92)
Size^#(N(x,l,r))	→	+^#(Size(l),Size(r))	(93)
WB^#(N(x,l,r))	→	WB^#(r)	(94)
WB^#(N(x,l,r))	→	ge^#(Size(l),Size(r))	(95)
WB^#(N(x,l,r))	→	and^#(if(ge(Size(l),Size(r)),ge(I(0),-(Size(l),Size(r))),ge(I(0),-(Size(r),Size(l)))),and(WB(l),WB(r)))	(96)
ge^#(O(x),I(y))	→	not^#(ge(y,x))	(97)
WB^#(N(x,l,r))	→	Size^#(l)	(63)
WB^#(N(x,l,r))	→	WB^#(l)	(98)
WB^#(N(x,l,r))	→	Size^#(l)	(63)
BS^#(N(x,l,r))	→	and^#(BS(l),BS(r))	(99)
Log'^#(I(x))	→	Log'^#(x)	(100)

1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.

The 1^st component contains the pair

Log'^#(I(x))	→	Log'^#(x)	(100)
Log'^#(O(x))	→	Log'^#(x)	(61)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[1]	=	0
[Size^#(x₁)]	=	0
[WB^#(x₁)]	=	0
[O^#(x₁)]	=	0
[Log(x₁)]	=	0
[Log^#(x₁)]	=	0
[BS^#(x₁)]	=	0
[and(x₁, x₂)]	=	0
[r]	=	0
[Size(x₁)]	=	0
[false]	=	0
[l]	=	0
[ge^#(x₁, x₂)]	=	0
[Log'^#(x₁)]	=	x₁ + 0
[Min(x₁)]	=	0
[Min^#(x₁)]	=	0
[O(x₁)]	=	x₁ + 1
[true]	=	0
[Val(x₁)]	=	0
[not^#(x₁)]	=	0
[I(x₁)]	=	x₁ + 1
[0]	=	0
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[Max^#(x₁)]	=	0
[BS(x₁)]	=	0
[-(x₁, x₂)]	=	0
[WB(x₁)]	=	0
[L(x₁)]	=	0
[N(x₁, x₂, x₃)]	=	0
[-^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[Log'(x₁)]	=	0
[Val^#(x₁)]	=	0
[+(x₁, x₂)]	=	0
[+^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[not(x₁)]	=	0
[Max(x₁)]	=	0

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

Log'^#(I(x))	→	Log'^#(x)	(100)
Log'^#(O(x))	→	Log'^#(x)	(61)

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

-^#(O(x),I(y))	→	-^#(-(x,y),I(1))	(70)
-^#(I(x),I(y))	→	-^#(x,y)	(92)
-^#(I(x),O(y))	→	-^#(x,y)	(91)
-^#(O(x),I(y))	→	-^#(x,y)	(89)
-^#(O(x),O(y))	→	-^#(x,y)	(83)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[1]	=	0
[Size^#(x₁)]	=	0
[WB^#(x₁)]	=	0
[O^#(x₁)]	=	0
[Log(x₁)]	=	0
[Log^#(x₁)]	=	0
[BS^#(x₁)]	=	0
[and(x₁, x₂)]	=	0
[r]	=	0
[Size(x₁)]	=	0
[false]	=	0
[l]	=	0
[ge^#(x₁, x₂)]	=	0
[Log'^#(x₁)]	=	0
[Min(x₁)]	=	0
[Min^#(x₁)]	=	0
[O(x₁)]	=	x₁ + 1
[true]	=	0
[Val(x₁)]	=	0
[not^#(x₁)]	=	0
[I(x₁)]	=	x₁ + 2
[0]	=	2
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[Max^#(x₁)]	=	0
[BS(x₁)]	=	0
[-(x₁, x₂)]	=	x₂ + 1
[WB(x₁)]	=	0
[L(x₁)]	=	0
[N(x₁, x₂, x₃)]	=	0
[-^#(x₁, x₂)]	=	x₂ + 0
[if^#(x₁, x₂, x₃)]	=	0
[Log'(x₁)]	=	0
[Val^#(x₁)]	=	0
[+(x₁, x₂)]	=	0
[+^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[not(x₁)]	=	0
[Max(x₁)]	=	0

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

-^#(I(x),I(y))	→	-^#(x,y)	(92)
-^#(I(x),O(y))	→	-^#(x,y)	(91)
-^#(O(x),I(y))	→	-^#(x,y)	(89)
-^#(O(x),O(y))	→	-^#(x,y)	(83)

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

-^#(O(x),I(y))

→

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

(70)

1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[1]	=	1
[Size^#(x₁)]	=	0
[WB^#(x₁)]	=	0
[O^#(x₁)]	=	0
[Log(x₁)]	=	0
[Log^#(x₁)]	=	0
[BS^#(x₁)]	=	0
[and(x₁, x₂)]	=	0
[r]	=	0
[Size(x₁)]	=	0
[false]	=	0
[l]	=	0
[ge^#(x₁, x₂)]	=	0
[Log'^#(x₁)]	=	0
[Min(x₁)]	=	0
[Min^#(x₁)]	=	0
[O(x₁)]	=	x₁ + 24867
[true]	=	0
[Val(x₁)]	=	0
[not^#(x₁)]	=	0
[I(x₁)]	=	x₁ + 24867
[0]	=	0
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[Max^#(x₁)]	=	0
[BS(x₁)]	=	0
[-(x₁, x₂)]	=	x₁ + 0
[WB(x₁)]	=	0
[L(x₁)]	=	0
[N(x₁, x₂, x₃)]	=	0
[-^#(x₁, x₂)]	=	x₁ + 0
[if^#(x₁, x₂, x₃)]	=	0
[Log'(x₁)]	=	0
[Val^#(x₁)]	=	0
[+(x₁, x₂)]	=	0
[+^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[not(x₁)]	=	0
[Max(x₁)]	=	0

together with the usable rules

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

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

-^#(O(x),I(y))

→

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

(70)

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^#(I(x),O(y))	→	ge^#(x,y)	(73)
ge^#(O(x),O(y))	→	ge^#(x,y)	(66)
ge^#(O(x),I(y))	→	ge^#(y,x)	(60)
ge^#(I(x),I(y))	→	ge^#(x,y)	(46)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[1]	=	1
[Size^#(x₁)]	=	0
[WB^#(x₁)]	=	0
[O^#(x₁)]	=	0
[Log(x₁)]	=	0
[Log^#(x₁)]	=	0
[BS^#(x₁)]	=	0
[and(x₁, x₂)]	=	0
[r]	=	0
[Size(x₁)]	=	0
[false]	=	0
[l]	=	0
[ge^#(x₁, x₂)]	=	x₁ + x₂ + 0
[Log'^#(x₁)]	=	0
[Min(x₁)]	=	0
[Min^#(x₁)]	=	0
[O(x₁)]	=	x₁ + 17678
[true]	=	0
[Val(x₁)]	=	0
[not^#(x₁)]	=	0
[I(x₁)]	=	x₁ + 17678
[0]	=	0
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[Max^#(x₁)]	=	0
[BS(x₁)]	=	0
[-(x₁, x₂)]	=	x₁ + 0
[WB(x₁)]	=	0
[L(x₁)]	=	0
[N(x₁, x₂, x₃)]	=	0
[-^#(x₁, x₂)]	=	x₁ + 0
[if^#(x₁, x₂, x₃)]	=	0
[Log'(x₁)]	=	0
[Val^#(x₁)]	=	0
[+(x₁, x₂)]	=	0
[+^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[not(x₁)]	=	0
[Max(x₁)]	=	0

together with the usable rules

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

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

ge^#(I(x),O(y))	→	ge^#(x,y)	(73)
ge^#(O(x),O(y))	→	ge^#(x,y)	(66)
ge^#(O(x),I(y))	→	ge^#(y,x)	(60)
ge^#(I(x),I(y))	→	ge^#(x,y)	(46)

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,O(x))

→

ge^#(0,x)

(71)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[1]	=	1
[Size^#(x₁)]	=	0
[WB^#(x₁)]	=	0
[O^#(x₁)]	=	0
[Log(x₁)]	=	0
[Log^#(x₁)]	=	0
[BS^#(x₁)]	=	0
[and(x₁, x₂)]	=	0
[r]	=	0
[Size(x₁)]	=	0
[false]	=	0
[l]	=	0
[ge^#(x₁, x₂)]	=	x₂ + 0
[Log'^#(x₁)]	=	0
[Min(x₁)]	=	0
[Min^#(x₁)]	=	0
[O(x₁)]	=	x₁ + 17678
[true]	=	0
[Val(x₁)]	=	0
[not^#(x₁)]	=	0
[I(x₁)]	=	x₁ + 17678
[0]	=	0
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[Max^#(x₁)]	=	0
[BS(x₁)]	=	0
[-(x₁, x₂)]	=	x₁ + 0
[WB(x₁)]	=	0
[L(x₁)]	=	0
[N(x₁, x₂, x₃)]	=	0
[-^#(x₁, x₂)]	=	x₁ + 0
[if^#(x₁, x₂, x₃)]	=	0
[Log'(x₁)]	=	0
[Val^#(x₁)]	=	0
[+(x₁, x₂)]	=	0
[+^#(x₁, x₂)]	=	0
[and^#(x₁, x₂)]	=	0
[not(x₁)]	=	0
[Max(x₁)]	=	0

together with the usable rules

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

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

ge^#(0,O(x))

→

ge^#(0,x)

(71)

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

+^#(I(x),O(y))	→	+^#(x,y)	(76)
+^#(x,+(y,z))	→	+^#(x,y)	(59)
+^#(O(x),O(y))	→	+^#(x,y)	(56)
+^#(x,+(y,z))	→	+^#(+(x,y),z)	(55)
+^#(O(x),I(y))	→	+^#(x,y)	(53)
+^#(I(x),I(y))	→	+^#(+(x,y),I(0))	(49)
+^#(I(x),I(y))	→	+^#(x,y)	(45)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[1]	=	0
[Size^#(x₁)]	=	0
[WB^#(x₁)]	=	0
[O^#(x₁)]	=	0
[Log(x₁)]	=	0
[Log^#(x₁)]	=	0
[BS^#(x₁)]	=	0
[and(x₁, x₂)]	=	0
[r]	=	0
[Size(x₁)]	=	0
[false]	=	0
[l]	=	0
[ge^#(x₁, x₂)]	=	0
[Log'^#(x₁)]	=	0
[Min(x₁)]	=	0
[Min^#(x₁)]	=	0
[O(x₁)]	=	x₁ + 25074
[true]	=	0
[Val(x₁)]	=	0
[not^#(x₁)]	=	0
[I(x₁)]	=	x₁ + 25074
[0]	=	0
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[Max^#(x₁)]	=	0
[BS(x₁)]	=	0
[-(x₁, x₂)]	=	x₁ + x₂ + 0
[WB(x₁)]	=	0
[L(x₁)]	=	0
[N(x₁, x₂, x₃)]	=	0
[-^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[Log'(x₁)]	=	0
[Val^#(x₁)]	=	0
[+(x₁, x₂)]	=	x₁ + x₂ + 0
[+^#(x₁, x₂)]	=	x₂ + 0
[and^#(x₁, x₂)]	=	0
[not(x₁)]	=	0
[Max(x₁)]	=	0

together with the usable rules

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

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

+^#(I(x),O(y))	→	+^#(x,y)	(76)
+^#(O(x),O(y))	→	+^#(x,y)	(56)
+^#(O(x),I(y))	→	+^#(x,y)	(53)
+^#(I(x),I(y))	→	+^#(x,y)	(45)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

+^#(x,+(y,z))	→	+^#(x,y)	(59)
+^#(x,+(y,z))	→	+^#(+(x,y),z)	(55)

1.1.5.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[1]	=	0
[Size^#(x₁)]	=	0
[WB^#(x₁)]	=	0
[O^#(x₁)]	=	0
[Log(x₁)]	=	0
[Log^#(x₁)]	=	0
[BS^#(x₁)]	=	0
[and(x₁, x₂)]	=	0
[r]	=	0
[Size(x₁)]	=	0
[false]	=	0
[l]	=	0
[ge^#(x₁, x₂)]	=	0
[Log'^#(x₁)]	=	0
[Min(x₁)]	=	0
[Min^#(x₁)]	=	0
[O(x₁)]	=	41171
[true]	=	0
[Val(x₁)]	=	0
[not^#(x₁)]	=	0
[I(x₁)]	=	x₁ + 20585
[0]	=	0
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[Max^#(x₁)]	=	0
[BS(x₁)]	=	0
[-(x₁, x₂)]	=	x₁ + x₂ + 0
[WB(x₁)]	=	0
[L(x₁)]	=	0
[N(x₁, x₂, x₃)]	=	0
[-^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[Log'(x₁)]	=	0
[Val^#(x₁)]	=	0
[+(x₁, x₂)]	=	x₁ + x₂ + 31598
[+^#(x₁, x₂)]	=	x₂ + 0
[and^#(x₁, x₂)]	=	0
[not(x₁)]	=	0
[Max(x₁)]	=	0

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

+^#(x,+(y,z))	→	+^#(x,y)	(59)
+^#(x,+(y,z))	→	+^#(+(x,y),z)	(55)

could be deleted.

1.1.5.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

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

→

+^#(+(x,y),I(0))

(49)

1.1.5.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[1]	=	1
[Size^#(x₁)]	=	0
[WB^#(x₁)]	=	0
[O^#(x₁)]	=	0
[Log(x₁)]	=	0
[Log^#(x₁)]	=	0
[BS^#(x₁)]	=	0
[and(x₁, x₂)]	=	0
[r]	=	0
[Size(x₁)]	=	0
[false]	=	0
[l]	=	0
[ge^#(x₁, x₂)]	=	0
[Log'^#(x₁)]	=	0
[Min(x₁)]	=	0
[Min^#(x₁)]	=	0
[O(x₁)]	=	x₁ + 2332
[true]	=	0
[Val(x₁)]	=	0
[not^#(x₁)]	=	0
[I(x₁)]	=	x₁ + 2332
[0]	=	0
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[Max^#(x₁)]	=	0
[BS(x₁)]	=	0
[-(x₁, x₂)]	=	x₁ + 0
[WB(x₁)]	=	0
[L(x₁)]	=	0
[N(x₁, x₂, x₃)]	=	0
[-^#(x₁, x₂)]	=	0
[if^#(x₁, x₂, x₃)]	=	0
[Log'(x₁)]	=	0
[Val^#(x₁)]	=	0
[+(x₁, x₂)]	=	x₁ + x₂ + 0
[+^#(x₁, x₂)]	=	x₁ + x₂ + 0
[and^#(x₁, x₂)]	=	0
[not(x₁)]	=	0
[Max(x₁)]	=	0

together with the usable rules

+(O(x),O(y))	→	O(+(x,y))	(4)
+(x,+(y,z))	→	+(+(x,y),z)	(8)
O(0)	→	0	(1)
+(x,0)	→	x	(3)
+(O(x),I(y))	→	I(+(x,y))	(5)
+(I(x),I(y))	→	O(+(+(x,y),I(0)))	(7)
+(I(x),O(y))	→	I(+(x,y))	(6)
+(0,x)	→	x	(2)

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

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

→

+^#(+(x,y),I(0))

(49)

could be deleted.

1.1.5.1.2.1 Dependency Graph Processor

The dependency pairs are split into 0 components.