Certification Problem

Input (TPDB TRS_Standard/CiME_04/big)

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)
eq(#,#)	→	true	(19)
eq(#,1(y))	→	false	(20)
eq(1(x),#)	→	false	(21)
eq(#,0(y))	→	eq(#,y)	(22)
eq(0(x),#)	→	eq(x,#)	(23)
eq(1(x),1(y))	→	eq(x,y)	(24)
eq(0(x),1(y))	→	false	(25)
eq(1(x),0(y))	→	false	(26)
eq(0(x),0(y))	→	eq(x,y)	(27)
ge(0(x),0(y))	→	ge(x,y)	(28)
ge(0(x),1(y))	→	not(ge(y,x))	(29)
ge(1(x),0(y))	→	ge(x,y)	(30)
ge(1(x),1(y))	→	ge(x,y)	(31)
ge(x,#)	→	true	(32)
ge(#,0(x))	→	ge(#,x)	(33)
ge(#,1(x))	→	false	(34)
log(x)	→	-(log'(x),1(#))	(35)
log'(#)	→	#	(36)
log'(1(x))	→	+(log'(x),1(#))	(37)
log'(0(x))	→	if(ge(x,1(#)),+(log'(x),1(#)),#)	(38)
*(#,x)	→	#	(39)
*(0(x),y)	→	0(*(x,y))	(40)
*(1(x),y)	→	+(0(*(x,y)),y)	(41)
((x,y),z)	→	(x,(y,z))	(42)
*(x,+(y,z))	→	+((x,y),(x,z))	(43)
app(nil,l)	→	l	(44)
app(cons(x,l1),l2)	→	cons(x,app(l1,l2))	(45)
sum(nil)	→	0(#)	(46)
sum(cons(x,l))	→	+(x,sum(l))	(47)
sum(app(l1,l2))	→	+(sum(l1),sum(l2))	(48)
prod(nil)	→	1(#)	(49)
prod(cons(x,l))	→	*(x,prod(l))	(50)
prod(app(l1,l2))	→	*(prod(l1),prod(l2))	(51)
mem(x,nil)	→	false	(52)
mem(x,cons(y,l))	→	if(eq(x,y),true,mem(x,l))	(53)
inter(x,nil)	→	nil	(54)
inter(nil,x)	→	nil	(55)
inter(app(l1,l2),l3)	→	app(inter(l1,l3),inter(l2,l3))	(56)
inter(l1,app(l2,l3))	→	app(inter(l1,l2),inter(l1,l3))	(57)
inter(cons(x,l1),l2)	→	ifinter(mem(x,l2),x,l1,l2)	(58)
inter(l1,cons(x,l2))	→	ifinter(mem(x,l1),x,l2,l1)	(59)
ifinter(true,x,l1,l2)	→	cons(x,inter(l1,l2))	(60)
ifinter(false,x,l1,l2)	→	inter(l1,l2)	(61)

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)	(62)
inter^#(l1,app(l2,l3))	→	inter^#(l1,l2)	(63)
log'^#(0(x))	→	+^#(log'(x),1(#))	(64)
*^#(0(x),y)	→	*^#(x,y)	(65)
+^#(+(x,y),z)	→	+^#(x,+(y,z))	(66)
eq^#(0(x),#)	→	eq^#(x,#)	(67)
inter^#(l1,app(l2,l3))	→	app^#(inter(l1,l2),inter(l1,l3))	(68)
-^#(0(x),0(y))	→	-^#(x,y)	(69)
prod^#(app(l1,l2))	→	prod^#(l1)	(70)
app^#(cons(x,l1),l2)	→	app^#(l1,l2)	(71)
inter^#(app(l1,l2),l3)	→	inter^#(l2,l3)	(72)
prod^#(cons(x,l))	→	prod^#(l)	(73)
-^#(0(x),1(y))	→	-^#(-(x,y),1(#))	(74)
+^#(1(x),1(y))	→	+^#(+(x,y),1(#))	(75)
+^#(0(x),1(y))	→	+^#(x,y)	(76)
prod^#(app(l1,l2))	→	prod^#(l2)	(77)
log^#(x)	→	-^#(log'(x),1(#))	(78)
+^#(1(x),1(y))	→	+^#(x,y)	(79)
-^#(1(x),1(y))	→	-^#(x,y)	(80)
+^#(+(x,y),z)	→	+^#(y,z)	(81)
-^#(0(x),0(y))	→	0^#(-(x,y))	(82)
inter^#(app(l1,l2),l3)	→	app^#(inter(l1,l3),inter(l2,l3))	(83)
*^#(1(x),y)	→	*^#(x,y)	(84)
^#((x,y),z)	→	^#(x,(y,z))	(85)
*^#(1(x),y)	→	+^#(0(*(x,y)),y)	(86)
+^#(1(x),1(y))	→	0^#(+(+(x,y),1(#)))	(87)
inter^#(cons(x,l1),l2)	→	ifinter^#(mem(x,l2),x,l1,l2)	(88)
prod^#(cons(x,l))	→	*^#(x,prod(l))	(89)
sum^#(app(l1,l2))	→	sum^#(l2)	(90)
eq^#(1(x),1(y))	→	eq^#(x,y)	(91)
+^#(0(x),0(y))	→	+^#(x,y)	(92)
*^#(1(x),y)	→	0^#(*(x,y))	(93)
+^#(1(x),0(y))	→	+^#(x,y)	(94)
ge^#(1(x),0(y))	→	ge^#(x,y)	(95)
log'^#(1(x))	→	+^#(log'(x),1(#))	(96)
ge^#(0(x),0(y))	→	ge^#(x,y)	(97)
log'^#(0(x))	→	log'^#(x)	(98)
inter^#(app(l1,l2),l3)	→	inter^#(l1,l3)	(99)
-^#(0(x),1(y))	→	-^#(x,y)	(100)
inter^#(cons(x,l1),l2)	→	mem^#(x,l2)	(101)
mem^#(x,cons(y,l))	→	mem^#(x,l)	(102)
log^#(x)	→	log'^#(x)	(103)
-^#(1(x),0(y))	→	-^#(x,y)	(104)
^#((x,y),z)	→	*^#(y,z)	(105)
eq^#(0(x),0(y))	→	eq^#(x,y)	(106)
inter^#(l1,cons(x,l2))	→	mem^#(x,l1)	(107)
ge^#(0(x),1(y))	→	ge^#(y,x)	(108)
inter^#(l1,app(l2,l3))	→	inter^#(l1,l3)	(109)
ifinter^#(true,x,l1,l2)	→	inter^#(l1,l2)	(110)
log'^#(0(x))	→	ge^#(x,1(#))	(111)
sum^#(app(l1,l2))	→	sum^#(l1)	(112)
*^#(0(x),y)	→	0^#(*(x,y))	(113)
log'^#(0(x))	→	if^#(ge(x,1(#)),+(log'(x),1(#)),#)	(114)
ge^#(#,0(x))	→	ge^#(#,x)	(115)
sum^#(cons(x,l))	→	sum^#(l)	(116)
inter^#(l1,cons(x,l2))	→	ifinter^#(mem(x,l1),x,l2,l1)	(117)
mem^#(x,cons(y,l))	→	eq^#(x,y)	(118)
eq^#(#,0(y))	→	eq^#(#,y)	(119)
ifinter^#(false,x,l1,l2)	→	inter^#(l1,l2)	(120)
+^#(0(x),0(y))	→	0^#(+(x,y))	(121)
prod^#(app(l1,l2))	→	*^#(prod(l1),prod(l2))	(122)
sum^#(app(l1,l2))	→	+^#(sum(l1),sum(l2))	(123)
sum^#(cons(x,l))	→	+^#(x,sum(l))	(124)
*^#(x,+(y,z))	→	*^#(x,z)	(125)
*^#(x,+(y,z))	→	+^#((x,y),(x,z))	(126)
-^#(1(x),1(y))	→	0^#(-(x,y))	(127)
sum^#(nil)	→	0^#(#)	(128)
log'^#(1(x))	→	log'^#(x)	(129)
ge^#(0(x),1(y))	→	not^#(ge(y,x))	(130)
ge^#(1(x),1(y))	→	ge^#(x,y)	(131)
mem^#(x,cons(y,l))	→	if^#(eq(x,y),true,mem(x,l))	(132)

1.1 Dependency Graph Processor

The dependency pairs are split into 14 components.

The 1^st component contains the pair

sum^#(app(l1,l2))	→	sum^#(l2)	(90)
sum^#(cons(x,l))	→	sum^#(l)	(116)
sum^#(app(l1,l2))	→	sum^#(l1)	(112)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	0
[mem(x₁, x₂)]	=	0
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[ifinter(x₁,...,x₄)]	=	0
[eq(x₁, x₂)]	=	0
[false]	=	0
[ge^#(x₁, x₂)]	=	0
[mem^#(x₁, x₂)]	=	0
[*^#(x₁, x₂)]	=	0
[log^#(x₁)]	=	0
[#]	=	0
[ifinter^#(x₁,...,x₄)]	=	0
[true]	=	0
[eq^#(x₁, x₂)]	=	0
[sum(x₁)]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	0
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[nil]	=	0
[log'^#(x₁)]	=	0
[-(x₁, x₂)]	=	0
[app^#(x₁, x₂)]	=	0
[-^#(x₁, x₂)]	=	0
[cons(x₁, x₂)]	=	x₂ + 1
[if^#(x₁, x₂, x₃)]	=	0
[inter(x₁, x₂)]	=	0
[inter^#(x₁, x₂)]	=	0
[+(x₁, x₂)]	=	0
[log'(x₁)]	=	0
[sum^#(x₁)]	=	x₁ + 0
[+^#(x₁, x₂)]	=	0
[not(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^#(l2)	(90)
sum^#(cons(x,l))	→	sum^#(l)	(116)
sum^#(app(l1,l2))	→	sum^#(l1)	(112)

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

prod^#(app(l1,l2))	→	prod^#(l2)	(77)
prod^#(cons(x,l))	→	prod^#(l)	(73)
prod^#(app(l1,l2))	→	prod^#(l1)	(70)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	0
[mem(x₁, x₂)]	=	0
[prod(x₁)]	=	0
[prod^#(x₁)]	=	x₁ + 0
[ifinter(x₁,...,x₄)]	=	0
[eq(x₁, x₂)]	=	0
[false]	=	0
[ge^#(x₁, x₂)]	=	0
[mem^#(x₁, x₂)]	=	0
[*^#(x₁, x₂)]	=	0
[log^#(x₁)]	=	0
[#]	=	0
[ifinter^#(x₁,...,x₄)]	=	0
[true]	=	0
[eq^#(x₁, x₂)]	=	0
[sum(x₁)]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	0
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[nil]	=	0
[log'^#(x₁)]	=	0
[-(x₁, x₂)]	=	0
[app^#(x₁, x₂)]	=	0
[-^#(x₁, x₂)]	=	0
[cons(x₁, x₂)]	=	x₂ + 1
[if^#(x₁, x₂, x₃)]	=	0
[inter(x₁, x₂)]	=	0
[inter^#(x₁, x₂)]	=	0
[+(x₁, x₂)]	=	0
[log'(x₁)]	=	0
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	0
[not(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^#(l2)	(77)
prod^#(cons(x,l))	→	prod^#(l)	(73)
prod^#(app(l1,l2))	→	prod^#(l1)	(70)

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

-^#(0(x),1(y))	→	-^#(x,y)	(100)
-^#(1(x),1(y))	→	-^#(x,y)	(80)
-^#(0(x),1(y))	→	-^#(-(x,y),1(#))	(74)
-^#(0(x),0(y))	→	-^#(x,y)	(69)
-^#(1(x),0(y))	→	-^#(x,y)	(104)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	x₁ + 20163
[mem(x₁, x₂)]	=	0
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[ifinter(x₁,...,x₄)]	=	0
[eq(x₁, x₂)]	=	0
[false]	=	0
[ge^#(x₁, x₂)]	=	0
[mem^#(x₁, x₂)]	=	0
[*^#(x₁, x₂)]	=	0
[log^#(x₁)]	=	0
[#]	=	0
[ifinter^#(x₁,...,x₄)]	=	0
[true]	=	0
[eq^#(x₁, x₂)]	=	0
[sum(x₁)]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	x₁ + 20164
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[nil]	=	0
[log'^#(x₁)]	=	0
[-(x₁, x₂)]	=	x₂ + 11293
[app^#(x₁, x₂)]	=	0
[-^#(x₁, x₂)]	=	x₂ + 0
[cons(x₁, x₂)]	=	1
[if^#(x₁, x₂, x₃)]	=	0
[inter(x₁, x₂)]	=	0
[inter^#(x₁, x₂)]	=	0
[+(x₁, x₂)]	=	0
[log'(x₁)]	=	0
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	0
[not(x₁)]	=	0
[*(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	1

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

-^#(0(x),1(y))	→	-^#(x,y)	(100)
-^#(1(x),1(y))	→	-^#(x,y)	(80)
-^#(0(x),0(y))	→	-^#(x,y)	(69)
-^#(1(x),0(y))	→	-^#(x,y)	(104)

could be deleted.

1.1.3.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(#))

(74)

1.1.3.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	x₁ + 8946
[mem(x₁, x₂)]	=	0
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[ifinter(x₁,...,x₄)]	=	0
[eq(x₁, x₂)]	=	0
[false]	=	0
[ge^#(x₁, x₂)]	=	0
[mem^#(x₁, x₂)]	=	0
[*^#(x₁, x₂)]	=	0
[log^#(x₁)]	=	0
[#]	=	42207
[ifinter^#(x₁,...,x₄)]	=	0
[true]	=	0
[eq^#(x₁, x₂)]	=	0
[sum(x₁)]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	x₁ + 8946
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[nil]	=	0
[log'^#(x₁)]	=	0
[-(x₁, x₂)]	=	x₁ + 0
[app^#(x₁, x₂)]	=	0
[-^#(x₁, x₂)]	=	x₁ + 0
[cons(x₁, x₂)]	=	1
[if^#(x₁, x₂, x₃)]	=	0
[inter(x₁, x₂)]	=	0
[inter^#(x₁, x₂)]	=	0
[+(x₁, x₂)]	=	0
[log'(x₁)]	=	0
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	0
[not(x₁)]	=	0
[*(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	1

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(#))

(74)

could be deleted.

1.1.3.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 4^th component contains the pair

log'^#(0(x))	→	log'^#(x)	(98)
log'^#(1(x))	→	log'^#(x)	(129)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	x₁ + 1
[mem(x₁, x₂)]	=	0
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[ifinter(x₁,...,x₄)]	=	0
[eq(x₁, x₂)]	=	0
[false]	=	0
[ge^#(x₁, x₂)]	=	0
[mem^#(x₁, x₂)]	=	0
[*^#(x₁, x₂)]	=	0
[log^#(x₁)]	=	0
[#]	=	30205
[ifinter^#(x₁,...,x₄)]	=	0
[true]	=	0
[eq^#(x₁, x₂)]	=	0
[sum(x₁)]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	x₁ + 1
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[nil]	=	0
[log'^#(x₁)]	=	x₁ + 0
[-(x₁, x₂)]	=	x₁ + 0
[app^#(x₁, x₂)]	=	0
[-^#(x₁, x₂)]	=	x₁ + 0
[cons(x₁, x₂)]	=	1
[if^#(x₁, x₂, x₃)]	=	0
[inter(x₁, x₂)]	=	0
[inter^#(x₁, x₂)]	=	0
[+(x₁, x₂)]	=	0
[log'(x₁)]	=	0
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	0
[not(x₁)]	=	0
[*(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	1

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

log'^#(0(x))	→	log'^#(x)	(98)
log'^#(1(x))	→	log'^#(x)	(129)

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

ge^#(1(x),1(y))	→	ge^#(x,y)	(131)
ge^#(0(x),0(y))	→	ge^#(x,y)	(97)
ge^#(1(x),0(y))	→	ge^#(x,y)	(95)
ge^#(0(x),1(y))	→	ge^#(y,x)	(108)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	x₁ + 2241
[mem(x₁, x₂)]	=	0
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[ifinter(x₁,...,x₄)]	=	0
[eq(x₁, x₂)]	=	0
[false]	=	0
[ge^#(x₁, x₂)]	=	x₁ + x₂ + 0
[mem^#(x₁, x₂)]	=	0
[*^#(x₁, x₂)]	=	0
[log^#(x₁)]	=	0
[#]	=	1
[ifinter^#(x₁,...,x₄)]	=	0
[true]	=	0
[eq^#(x₁, x₂)]	=	0
[sum(x₁)]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	x₁ + 2241
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[nil]	=	0
[log'^#(x₁)]	=	0
[-(x₁, x₂)]	=	x₁ + 0
[app^#(x₁, x₂)]	=	0
[-^#(x₁, x₂)]	=	x₁ + 0
[cons(x₁, x₂)]	=	1
[if^#(x₁, x₂, x₃)]	=	0
[inter(x₁, x₂)]	=	0
[inter^#(x₁, x₂)]	=	0
[+(x₁, x₂)]	=	0
[log'(x₁)]	=	0
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	0
[not(x₁)]	=	0
[*(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	1

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^#(1(x),1(y))	→	ge^#(x,y)	(131)
ge^#(0(x),0(y))	→	ge^#(x,y)	(97)
ge^#(1(x),0(y))	→	ge^#(x,y)	(95)
ge^#(0(x),1(y))	→	ge^#(y,x)	(108)

could be deleted.

1.1.5.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 6^th component contains the pair

ge^#(#,0(x))

→

ge^#(#,x)

(115)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	x₁ + 591
[mem(x₁, x₂)]	=	0
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[ifinter(x₁,...,x₄)]	=	0
[eq(x₁, x₂)]	=	0
[false]	=	0
[ge^#(x₁, x₂)]	=	x₂ + 0
[mem^#(x₁, x₂)]	=	0
[*^#(x₁, x₂)]	=	0
[log^#(x₁)]	=	0
[#]	=	3287
[ifinter^#(x₁,...,x₄)]	=	0
[true]	=	0
[eq^#(x₁, x₂)]	=	0
[sum(x₁)]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	x₁ + 591
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[nil]	=	0
[log'^#(x₁)]	=	0
[-(x₁, x₂)]	=	x₁ + 0
[app^#(x₁, x₂)]	=	0
[-^#(x₁, x₂)]	=	x₁ + 0
[cons(x₁, x₂)]	=	1
[if^#(x₁, x₂, x₃)]	=	0
[inter(x₁, x₂)]	=	0
[inter^#(x₁, x₂)]	=	0
[+(x₁, x₂)]	=	0
[log'(x₁)]	=	0
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	0
[not(x₁)]	=	0
[*(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	1

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)

(115)

could be deleted.

1.1.6.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 7^th component contains the pair

inter^#(app(l1,l2),l3)	→	inter^#(l1,l3)	(99)
inter^#(cons(x,l1),l2)	→	ifinter^#(mem(x,l2),x,l1,l2)	(88)
ifinter^#(false,x,l1,l2)	→	inter^#(l1,l2)	(120)
inter^#(l1,cons(x,l2))	→	ifinter^#(mem(x,l1),x,l2,l1)	(117)
inter^#(app(l1,l2),l3)	→	inter^#(l2,l3)	(72)
ifinter^#(true,x,l1,l2)	→	inter^#(l1,l2)	(110)
inter^#(l1,app(l2,l3))	→	inter^#(l1,l3)	(109)
inter^#(l1,app(l2,l3))	→	inter^#(l1,l2)	(63)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	x₁ + 23612
[mem(x₁, x₂)]	=	x₁ + x₂ + 0
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[ifinter(x₁,...,x₄)]	=	0
[eq(x₁, x₂)]	=	x₁ + 1
[false]	=	23614
[ge^#(x₁, x₂)]	=	0
[mem^#(x₁, x₂)]	=	0
[*^#(x₁, x₂)]	=	0
[log^#(x₁)]	=	0
[#]	=	12618
[ifinter^#(x₁,...,x₄)]	=	x₃ + x₄ + 1
[true]	=	0
[eq^#(x₁, x₂)]	=	0
[sum(x₁)]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	x₁ + 23612
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[nil]	=	23614
[log'^#(x₁)]	=	0
[-(x₁, x₂)]	=	x₁ + 0
[app^#(x₁, x₂)]	=	0
[-^#(x₁, x₂)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₂ + 2
[if^#(x₁, x₂, x₃)]	=	0
[inter(x₁, x₂)]	=	0
[inter^#(x₁, x₂)]	=	x₁ + x₂ + 0
[+(x₁, x₂)]	=	0
[log'(x₁)]	=	0
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	0
[not(x₁)]	=	0
[*(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	x₁ + x₂ + 1

together with the usable rules

0(#)	→	#	(1)
-(x,#)	→	x	(10)
mem(x,nil)	→	false	(52)
-(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

inter^#(app(l1,l2),l3)	→	inter^#(l1,l3)	(99)
inter^#(cons(x,l1),l2)	→	ifinter^#(mem(x,l2),x,l1,l2)	(88)
ifinter^#(false,x,l1,l2)	→	inter^#(l1,l2)	(120)
inter^#(l1,cons(x,l2))	→	ifinter^#(mem(x,l1),x,l2,l1)	(117)
inter^#(app(l1,l2),l3)	→	inter^#(l2,l3)	(72)
ifinter^#(true,x,l1,l2)	→	inter^#(l1,l2)	(110)
inter^#(l1,app(l2,l3))	→	inter^#(l1,l3)	(109)
inter^#(l1,app(l2,l3))	→	inter^#(l1,l2)	(63)

could be deleted.

1.1.7.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 8^th component contains the pair

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

→

app^#(l1,l2)

(71)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	x₁ + 23612
[mem(x₁, x₂)]	=	x₁ + x₂ + 0
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[ifinter(x₁,...,x₄)]	=	0
[eq(x₁, x₂)]	=	x₁ + 1
[false]	=	23614
[ge^#(x₁, x₂)]	=	0
[mem^#(x₁, x₂)]	=	0
[*^#(x₁, x₂)]	=	0
[log^#(x₁)]	=	0
[#]	=	12618
[ifinter^#(x₁,...,x₄)]	=	1
[true]	=	0
[eq^#(x₁, x₂)]	=	0
[sum(x₁)]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	x₁ + 23612
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[nil]	=	23614
[log'^#(x₁)]	=	0
[-(x₁, x₂)]	=	x₁ + 0
[app^#(x₁, x₂)]	=	x₁ + 0
[-^#(x₁, x₂)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₂ + 2
[if^#(x₁, x₂, x₃)]	=	0
[inter(x₁, x₂)]	=	0
[inter^#(x₁, x₂)]	=	0
[+(x₁, x₂)]	=	0
[log'(x₁)]	=	0
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	0
[not(x₁)]	=	0
[*(x₁, x₂)]	=	0
[app(x₁, x₂)]	=	1

together with the usable rules

0(#)	→	#	(1)
-(x,#)	→	x	(10)
mem(x,nil)	→	false	(52)
-(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

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

→

app^#(l1,l2)

(71)

could be deleted.

1.1.8.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 9^th component contains the pair

*^#(x,+(y,z))	→	*^#(x,z)	(125)
^#((x,y),z)	→	^#(x,(y,z))	(85)
*^#(1(x),y)	→	*^#(x,y)	(84)
^#((x,y),z)	→	*^#(y,z)	(105)
*^#(0(x),y)	→	*^#(x,y)	(65)
*^#(x,+(y,z))	→	*^#(x,y)	(62)

1.1.9 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	x₁ + 1
[mem(x₁, x₂)]	=	x₁ + x₂ + 0
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[ifinter(x₁,...,x₄)]	=	0
[eq(x₁, x₂)]	=	x₁ + 1
[false]	=	3
[ge^#(x₁, x₂)]	=	0
[mem^#(x₁, x₂)]	=	0
[*^#(x₁, x₂)]	=	x₁ + 0
[log^#(x₁)]	=	0
[#]	=	1
[ifinter^#(x₁,...,x₄)]	=	1
[true]	=	0
[eq^#(x₁, x₂)]	=	0
[sum(x₁)]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	x₁ + 1
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[nil]	=	3
[log'^#(x₁)]	=	0
[-(x₁, x₂)]	=	x₁ + 0
[app^#(x₁, x₂)]	=	0
[-^#(x₁, x₂)]	=	x₁ + 0
[cons(x₁, x₂)]	=	x₂ + 2
[if^#(x₁, x₂, x₃)]	=	0
[inter(x₁, x₂)]	=	0
[inter^#(x₁, x₂)]	=	0
[+(x₁, x₂)]	=	x₁ + x₂ + 1
[log'(x₁)]	=	0
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	0
[not(x₁)]	=	0
[*(x₁, x₂)]	=	x₁ + x₂ + 1
[app(x₁, x₂)]	=	1

together with the usable rules

0(#)	→	#	(1)
-(x,#)	→	x	(10)
mem(x,nil)	→	false	(52)
-(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

^#((x,y),z)	→	^#(x,(y,z))	(85)
*^#(1(x),y)	→	*^#(x,y)	(84)
^#((x,y),z)	→	*^#(y,z)	(105)
*^#(0(x),y)	→	*^#(x,y)	(65)

could be deleted.

1.1.9.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

*^#(x,+(y,z))	→	*^#(x,z)	(125)
*^#(x,+(y,z))	→	*^#(x,y)	(62)

1.1.9.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	0
[mem(x₁, x₂)]	=	max(0)
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[ifinter(x₁,...,x₄)]	=	max(0)
[eq(x₁, x₂)]	=	max(0)
[false]	=	0
[ge^#(x₁, x₂)]	=	max(0)
[mem^#(x₁, x₂)]	=	max(0)
[*^#(x₁, x₂)]	=	max(x₂ + 7720, 0)
[log^#(x₁)]	=	0
[#]	=	0
[ifinter^#(x₁,...,x₄)]	=	max(0)
[true]	=	0
[eq^#(x₁, x₂)]	=	max(0)
[sum(x₁)]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	0
[if(x₁, x₂, x₃)]	=	max(0)
[ge(x₁, x₂)]	=	max(0)
[nil]	=	0
[log'^#(x₁)]	=	0
[-(x₁, x₂)]	=	max(0)
[app^#(x₁, x₂)]	=	max(0)
[-^#(x₁, x₂)]	=	max(0)
[cons(x₁, x₂)]	=	max(0)
[if^#(x₁, x₂, x₃)]	=	max(0)
[inter(x₁, x₂)]	=	max(0)
[inter^#(x₁, x₂)]	=	max(0)
[+(x₁, x₂)]	=	max(x₁ + 39, x₂ + 0, 0)
[log'(x₁)]	=	0
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	max(0)
[not(x₁)]	=	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)

(62)

could be deleted.

1.1.9.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)

(125)

1.1.9.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	0
[mem(x₁, x₂)]	=	max(0)
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[ifinter(x₁,...,x₄)]	=	max(0)
[eq(x₁, x₂)]	=	max(0)
[false]	=	0
[ge^#(x₁, x₂)]	=	max(0)
[mem^#(x₁, x₂)]	=	max(0)
[*^#(x₁, x₂)]	=	max(x₂ + 16575, 0)
[log^#(x₁)]	=	0
[#]	=	0
[ifinter^#(x₁,...,x₄)]	=	max(0)
[true]	=	0
[eq^#(x₁, x₂)]	=	max(0)
[sum(x₁)]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	0
[if(x₁, x₂, x₃)]	=	max(0)
[ge(x₁, x₂)]	=	max(0)
[nil]	=	0
[log'^#(x₁)]	=	0
[-(x₁, x₂)]	=	max(0)
[app^#(x₁, x₂)]	=	max(0)
[-^#(x₁, x₂)]	=	max(0)
[cons(x₁, x₂)]	=	max(0)
[if^#(x₁, x₂, x₃)]	=	max(0)
[inter(x₁, x₂)]	=	max(0)
[inter^#(x₁, x₂)]	=	max(0)
[+(x₁, x₂)]	=	max(x₂ + 1, 0)
[log'(x₁)]	=	0
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	max(0)
[not(x₁)]	=	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)

(125)

could be deleted.

1.1.9.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 10^th component contains the pair

+^#(1(x),0(y))	→	+^#(x,y)	(94)
+^#(0(x),0(y))	→	+^#(x,y)	(92)
+^#(+(x,y),z)	→	+^#(y,z)	(81)
+^#(1(x),1(y))	→	+^#(x,y)	(79)
+^#(0(x),1(y))	→	+^#(x,y)	(76)
+^#(1(x),1(y))	→	+^#(+(x,y),1(#))	(75)
+^#(+(x,y),z)	→	+^#(x,+(y,z))	(66)

1.1.10 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	x₁ + 3
[mem(x₁, x₂)]	=	x₁ + x₂ + 0
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[ifinter(x₁,...,x₄)]	=	0
[eq(x₁, x₂)]	=	x₁ + 1
[false]	=	5
[ge^#(x₁, x₂)]	=	0
[mem^#(x₁, x₂)]	=	0
[*^#(x₁, x₂)]	=	0
[log^#(x₁)]	=	0
[#]	=	1
[ifinter^#(x₁,...,x₄)]	=	1
[true]	=	0
[eq^#(x₁, x₂)]	=	0
[sum(x₁)]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	x₁ + 1
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[nil]	=	5
[log'^#(x₁)]	=	0
[-(x₁, x₂)]	=	x₁ + 37986
[app^#(x₁, x₂)]	=	0
[-^#(x₁, x₂)]	=	0
[cons(x₁, x₂)]	=	x₂ + 18781
[if^#(x₁, x₂, x₃)]	=	0
[inter(x₁, x₂)]	=	0
[inter^#(x₁, x₂)]	=	0
[+(x₁, x₂)]	=	x₁ + x₂ + 1
[log'(x₁)]	=	0
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	x₁ + x₂ + 0
[not(x₁)]	=	0
[*(x₁, x₂)]	=	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)
mem(x,nil)	→	false	(52)
+(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),0(y))	→	+^#(x,y)	(94)
+^#(0(x),0(y))	→	+^#(x,y)	(92)
+^#(+(x,y),z)	→	+^#(y,z)	(81)
+^#(1(x),1(y))	→	+^#(x,y)	(79)
+^#(0(x),1(y))	→	+^#(x,y)	(76)
+^#(1(x),1(y))	→	+^#(+(x,y),1(#))	(75)

could be deleted.

1.1.10.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))

(66)

1.1.10.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	x₁ + 3
[mem(x₁, x₂)]	=	x₁ + x₂ + 0
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[ifinter(x₁,...,x₄)]	=	0
[eq(x₁, x₂)]	=	x₁ + 1
[false]	=	5
[ge^#(x₁, x₂)]	=	0
[mem^#(x₁, x₂)]	=	0
[*^#(x₁, x₂)]	=	0
[log^#(x₁)]	=	0
[#]	=	1
[ifinter^#(x₁,...,x₄)]	=	1
[true]	=	0
[eq^#(x₁, x₂)]	=	0
[sum(x₁)]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	x₁ + 1
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[nil]	=	5
[log'^#(x₁)]	=	0
[-(x₁, x₂)]	=	x₁ + 1
[app^#(x₁, x₂)]	=	0
[-^#(x₁, x₂)]	=	0
[cons(x₁, x₂)]	=	x₂ + 18781
[if^#(x₁, x₂, x₃)]	=	0
[inter(x₁, x₂)]	=	0
[inter^#(x₁, x₂)]	=	0
[+(x₁, x₂)]	=	x₁ + x₂ + 1
[log'(x₁)]	=	0
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	x₁ + 0
[not(x₁)]	=	0
[*(x₁, x₂)]	=	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)
mem(x,nil)	→	false	(52)
+(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))

(66)

could be deleted.

1.1.10.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 11^th component contains the pair

mem^#(x,cons(y,l))

→

mem^#(x,l)

(102)

1.1.11 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	x₁ + 3
[mem(x₁, x₂)]	=	x₁ + x₂ + 0
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[ifinter(x₁,...,x₄)]	=	0
[eq(x₁, x₂)]	=	x₁ + 1
[false]	=	5
[ge^#(x₁, x₂)]	=	0
[mem^#(x₁, x₂)]	=	x₂ + 0
[*^#(x₁, x₂)]	=	0
[log^#(x₁)]	=	0
[#]	=	1
[ifinter^#(x₁,...,x₄)]	=	1
[true]	=	0
[eq^#(x₁, x₂)]	=	0
[sum(x₁)]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	x₁ + 1
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[nil]	=	5
[log'^#(x₁)]	=	0
[-(x₁, x₂)]	=	x₁ + 1
[app^#(x₁, x₂)]	=	0
[-^#(x₁, x₂)]	=	0
[cons(x₁, x₂)]	=	x₂ + 18781
[if^#(x₁, x₂, x₃)]	=	0
[inter(x₁, x₂)]	=	0
[inter^#(x₁, x₂)]	=	0
[+(x₁, x₂)]	=	x₁ + x₂ + 1
[log'(x₁)]	=	0
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	x₁ + 0
[not(x₁)]	=	0
[*(x₁, x₂)]	=	x₁ + x₂ + 14972
[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)
mem(x,nil)	→	false	(52)
+(1(x),0(y))	→	1(+(x,y))	(6)
+(x,#)	→	x	(2)

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

mem^#(x,cons(y,l))

→

mem^#(x,l)

(102)

could be deleted.

1.1.11.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 12^th component contains the pair

eq^#(1(x),1(y))	→	eq^#(x,y)	(91)
eq^#(0(x),0(y))	→	eq^#(x,y)	(106)

1.1.12 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	x₁ + 3
[mem(x₁, x₂)]	=	x₁ + x₂ + 0
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[ifinter(x₁,...,x₄)]	=	0
[eq(x₁, x₂)]	=	x₁ + 1
[false]	=	5
[ge^#(x₁, x₂)]	=	0
[mem^#(x₁, x₂)]	=	0
[*^#(x₁, x₂)]	=	0
[log^#(x₁)]	=	0
[#]	=	1
[ifinter^#(x₁,...,x₄)]	=	1
[true]	=	0
[eq^#(x₁, x₂)]	=	x₁ + 0
[sum(x₁)]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	x₁ + 1
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[nil]	=	5
[log'^#(x₁)]	=	0
[-(x₁, x₂)]	=	x₁ + 1
[app^#(x₁, x₂)]	=	0
[-^#(x₁, x₂)]	=	0
[cons(x₁, x₂)]	=	x₂ + 18781
[if^#(x₁, x₂, x₃)]	=	0
[inter(x₁, x₂)]	=	0
[inter^#(x₁, x₂)]	=	0
[+(x₁, x₂)]	=	x₁ + x₂ + 1
[log'(x₁)]	=	0
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	x₁ + 0
[not(x₁)]	=	0
[*(x₁, x₂)]	=	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)
mem(x,nil)	→	false	(52)
+(1(x),0(y))	→	1(+(x,y))	(6)
+(x,#)	→	x	(2)

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

eq^#(1(x),1(y))	→	eq^#(x,y)	(91)
eq^#(0(x),0(y))	→	eq^#(x,y)	(106)

could be deleted.

1.1.12.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 13^th component contains the pair

eq^#(0(x),#)

→

eq^#(x,#)

(67)

1.1.13 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	x₁ + 3
[mem(x₁, x₂)]	=	x₁ + x₂ + 0
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[ifinter(x₁,...,x₄)]	=	0
[eq(x₁, x₂)]	=	x₁ + 1
[false]	=	5
[ge^#(x₁, x₂)]	=	0
[mem^#(x₁, x₂)]	=	0
[*^#(x₁, x₂)]	=	0
[log^#(x₁)]	=	0
[#]	=	1
[ifinter^#(x₁,...,x₄)]	=	1
[true]	=	0
[eq^#(x₁, x₂)]	=	x₁ + 0
[sum(x₁)]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	x₁ + 1
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[nil]	=	5
[log'^#(x₁)]	=	0
[-(x₁, x₂)]	=	x₁ + 1
[app^#(x₁, x₂)]	=	0
[-^#(x₁, x₂)]	=	0
[cons(x₁, x₂)]	=	x₂ + 18781
[if^#(x₁, x₂, x₃)]	=	0
[inter(x₁, x₂)]	=	0
[inter^#(x₁, x₂)]	=	0
[+(x₁, x₂)]	=	x₁ + x₂ + 1
[log'(x₁)]	=	0
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	x₁ + 0
[not(x₁)]	=	0
[*(x₁, x₂)]	=	x₁ + x₂ + 36998
[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)
mem(x,nil)	→	false	(52)
+(1(x),0(y))	→	1(+(x,y))	(6)
+(x,#)	→	x	(2)

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

eq^#(0(x),#)

→

eq^#(x,#)

(67)

could be deleted.

1.1.13.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 14^th component contains the pair

eq^#(#,0(y))

→

eq^#(#,y)

(119)

1.1.14 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	0
[1(x₁)]	=	x₁ + 3
[mem(x₁, x₂)]	=	x₁ + x₂ + 0
[prod(x₁)]	=	0
[prod^#(x₁)]	=	0
[ifinter(x₁,...,x₄)]	=	0
[eq(x₁, x₂)]	=	x₁ + 1
[false]	=	5
[ge^#(x₁, x₂)]	=	0
[mem^#(x₁, x₂)]	=	0
[*^#(x₁, x₂)]	=	0
[log^#(x₁)]	=	0
[#]	=	1
[ifinter^#(x₁,...,x₄)]	=	1
[true]	=	0
[eq^#(x₁, x₂)]	=	x₂ + 0
[sum(x₁)]	=	0
[not^#(x₁)]	=	0
[log(x₁)]	=	0
[0(x₁)]	=	x₁ + 1
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[nil]	=	5
[log'^#(x₁)]	=	0
[-(x₁, x₂)]	=	x₁ + 1
[app^#(x₁, x₂)]	=	0
[-^#(x₁, x₂)]	=	0
[cons(x₁, x₂)]	=	x₂ + 18781
[if^#(x₁, x₂, x₃)]	=	0
[inter(x₁, x₂)]	=	0
[inter^#(x₁, x₂)]	=	0
[+(x₁, x₂)]	=	x₁ + x₂ + 1
[log'(x₁)]	=	0
[sum^#(x₁)]	=	0
[+^#(x₁, x₂)]	=	x₁ + 0
[not(x₁)]	=	0
[*(x₁, x₂)]	=	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)
mem(x,nil)	→	false	(52)
+(1(x),0(y))	→	1(+(x,y))	(6)
+(x,#)	→	x	(2)

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

eq^#(#,0(y))

→

eq^#(#,y)

(119)

could be deleted.

1.1.14.1 Dependency Graph Processor

The dependency pairs are split into 0 components.