Certification Problem

Input (TPDB TRS_Standard/Kaliszyk_19/arith)

The rewrite relation of the following TRS is considered.

There are 108 ruless (increase limit for explicit display).

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.

mult^#(BIT1(m),BIT0(n))	→	plus^#(BIT0(n),BIT0(BIT0(mult(m,n))))	(109)
minus^#(BIT0(m),BIT0(n))	→	BIT0^#(minus(m,n))	(110)
ODD^#(NUMERAL(n))	→	ODD^#(n)	(111)
exp^#(BIT1(m),BIT1(n))	→	mult^#(BIT1(m),exp(BIT1(m),n))	(112)
PRE^#(BIT0(n))	→	eq^#(n,0)	(113)
plus^#(BIT0(m),BIT0(n))	→	BIT0^#(plus(m,n))	(114)
PRE^#(NUMERAL(n))	→	NUMERAL^#(PRE(n))	(115)
exp^#(NUMERAL(m),NUMERAL(n))	→	NUMERAL^#(exp(m,n))	(116)
lt^#(BIT1(m),BIT1(n))	→	lt^#(m,n)	(117)
SUC^#(NUMERAL(n))	→	NUMERAL^#(SUC(n))	(118)
ge^#(0,BIT0(n))	→	ge^#(0,n)	(119)
plus^#(NUMERAL(m),NUMERAL(n))	→	NUMERAL^#(plus(m,n))	(120)
lt^#(BIT1(m),BIT0(n))	→	lt^#(m,n)	(121)
exp^#(BIT0(m),BIT0(n))	→	exp^#(BIT0(m),n)	(122)
gt^#(BIT0(n),0)	→	gt^#(n,0)	(123)
exp^#(NUMERAL(m),NUMERAL(n))	→	exp^#(m,n)	(124)
mult^#(BIT1(m),BIT1(n))	→	plus^#(plus(BIT1(m),BIT0(n)),BIT0(BIT0(mult(m,n))))	(125)
exp^#(BIT0(m),BIT1(n))	→	exp^#(BIT0(m),n)	(126)
ge^#(NUMERAL(n),NUMERAL(m))	→	ge^#(n,m)	(127)
mult^#(BIT0(m),BIT1(n))	→	plus^#(BIT0(m),BIT0(BIT0(mult(m,n))))	(128)
le^#(BIT0(m),BIT0(n))	→	le^#(m,n)	(129)
mult^#(BIT1(m),BIT1(n))	→	mult^#(m,n)	(130)
minus^#(BIT1(m),BIT1(n))	→	minus^#(m,n)	(131)
plus^#(NUMERAL(m),NUMERAL(n))	→	plus^#(m,n)	(132)
exp^#(0,BIT0(n))	→	mult^#(exp(0,n),exp(0,n))	(133)
eq^#(NUMERAL(m),NUMERAL(n))	→	eq^#(m,n)	(134)
mult^#(BIT1(m),BIT1(n))	→	BIT0^#(n)	(135)
PRE^#(NUMERAL(n))	→	PRE^#(n)	(136)
lt^#(BIT0(m),BIT1(n))	→	le^#(m,n)	(137)
exp^#(BIT0(m),BIT0(n))	→	mult^#(exp(BIT0(m),n),exp(BIT0(m),n))	(138)
minus^#(BIT0(m),BIT1(n))	→	BIT0^#(minus(m,n))	(139)
exp^#(BIT1(m),BIT0(n))	→	exp^#(BIT1(m),n)	(140)
le^#(BIT0(m),BIT1(n))	→	le^#(m,n)	(141)
EVEN^#(NUMERAL(n))	→	EVEN^#(n)	(142)
plus^#(BIT0(m),BIT1(n))	→	plus^#(m,n)	(143)
mult^#(BIT1(m),BIT1(n))	→	BIT0^#(mult(m,n))	(144)
mult^#(BIT0(m),BIT1(n))	→	BIT0^#(BIT0(mult(m,n)))	(145)
mult^#(NUMERAL(m),NUMERAL(n))	→	mult^#(m,n)	(146)
SUC^#(BIT1(n))	→	SUC^#(n)	(147)
exp^#(BIT0(m),BIT1(n))	→	exp^#(BIT0(m),n)	(126)
SUC^#(BIT1(n))	→	BIT0^#(SUC(n))	(148)
mult^#(BIT0(m),BIT0(n))	→	BIT0^#(mult(m,n))	(149)
mult^#(BIT0(m),BIT1(n))	→	mult^#(m,n)	(150)
lt^#(NUMERAL(m),NUMERAL(n))	→	lt^#(m,n)	(151)
SUC^#(NUMERAL(n))	→	SUC^#(n)	(152)
exp^#(BIT0(m),BIT1(n))	→	mult^#(BIT0(m),exp(BIT0(m),n))	(153)
exp^#(BIT1(m),BIT0(n))	→	mult^#(exp(BIT1(m),n),exp(BIT1(m),n))	(154)
exp^#(BIT1(m),BIT1(n))	→	exp^#(BIT1(m),n)	(155)
ge^#(BIT0(n),BIT1(m))	→	gt^#(n,m)	(156)
mult^#(BIT1(m),BIT1(n))	→	BIT0^#(BIT0(mult(m,n)))	(157)
le^#(BIT1(m),BIT1(n))	→	le^#(m,n)	(158)
mult^#(BIT0(m),BIT0(n))	→	mult^#(m,n)	(159)
exp^#(BIT1(m),BIT0(n))	→	exp^#(BIT1(m),n)	(140)
plus^#(BIT1(m),BIT1(n))	→	BIT0^#(SUC(plus(m,n)))	(160)
exp^#(BIT1(m),BIT1(n))	→	exp^#(BIT1(m),n)	(155)
minus^#(BIT0(m),BIT1(n))	→	minus^#(m,n)	(161)
gt^#(NUMERAL(n),NUMERAL(m))	→	gt^#(n,m)	(162)
le^#(NUMERAL(m),NUMERAL(n))	→	le^#(m,n)	(163)
lt^#(BIT0(m),BIT0(n))	→	lt^#(m,n)	(164)
ge^#(BIT0(n),BIT0(m))	→	ge^#(n,m)	(165)
exp^#(0,BIT0(n))	→	exp^#(0,n)	(166)
gt^#(BIT1(n),BIT1(m))	→	gt^#(n,m)	(167)
gt^#(BIT0(n),BIT0(m))	→	gt^#(n,m)	(168)
exp^#(BIT0(m),BIT0(n))	→	exp^#(BIT0(m),n)	(122)
mult^#(NUMERAL(m),NUMERAL(n))	→	NUMERAL^#(mult(m,n))	(169)
plus^#(BIT1(m),BIT1(n))	→	plus^#(m,n)	(170)
minus^#(BIT1(m),BIT0(n))	→	minus^#(m,n)	(171)
PRE^#(BIT1(n))	→	BIT0^#(n)	(172)
mult^#(BIT1(m),BIT0(n))	→	mult^#(m,n)	(173)
gt^#(BIT1(n),BIT0(m))	→	ge^#(n,m)	(174)
ge^#(BIT1(n),BIT1(m))	→	ge^#(n,m)	(175)
exp^#(BIT1(m),BIT1(n))	→	mult^#(mult(BIT1(m),exp(BIT1(m),n)),exp(BIT1(m),n))	(176)
le^#(BIT0(n),0)	→	le^#(n,0)	(177)
eq^#(BIT0(n),0)	→	eq^#(n,0)	(178)
plus^#(BIT0(m),BIT0(n))	→	plus^#(m,n)	(179)
minus^#(BIT0(m),BIT0(n))	→	minus^#(m,n)	(180)
le^#(BIT1(m),BIT0(n))	→	lt^#(m,n)	(181)
minus^#(BIT1(m),BIT1(n))	→	BIT0^#(minus(m,n))	(182)
gt^#(BIT0(n),BIT1(m))	→	gt^#(n,m)	(183)
minus^#(BIT1(m),BIT0(n))	→	le^#(n,m)	(184)
eq^#(0,BIT0(n))	→	eq^#(0,n)	(185)
plus^#(BIT1(m),BIT1(n))	→	SUC^#(plus(m,n))	(186)
eq^#(BIT0(m),BIT0(n))	→	eq^#(m,n)	(187)
plus^#(BIT1(m),BIT0(n))	→	plus^#(m,n)	(188)
exp^#(BIT0(m),BIT1(n))	→	mult^#(mult(BIT0(m),exp(BIT0(m),n)),exp(BIT0(m),n))	(189)
PRE^#(BIT0(n))	→	PRE^#(n)	(190)
eq^#(BIT1(m),BIT1(n))	→	eq^#(m,n)	(191)
minus^#(NUMERAL(m),NUMERAL(n))	→	minus^#(m,n)	(192)
mult^#(BIT1(m),BIT0(n))	→	BIT0^#(BIT0(mult(m,n)))	(193)
mult^#(BIT0(m),BIT1(n))	→	BIT0^#(mult(m,n))	(194)
ge^#(BIT1(n),BIT0(m))	→	ge^#(n,m)	(195)
mult^#(BIT1(m),BIT1(n))	→	plus^#(BIT1(m),BIT0(n))	(196)
exp^#(0,BIT0(n))	→	exp^#(0,n)	(166)
minus^#(NUMERAL(m),NUMERAL(n))	→	NUMERAL^#(minus(m,n))	(197)
mult^#(BIT1(m),BIT0(n))	→	BIT0^#(mult(m,n))	(198)
mult^#(BIT0(m),BIT0(n))	→	BIT0^#(BIT0(mult(m,n)))	(199)
minus^#(BIT0(m),BIT1(n))	→	PRE^#(BIT0(minus(m,n)))	(200)
lt^#(0,BIT0(n))	→	lt^#(0,n)	(201)

1.1 Dependency Graph Processor

The dependency pairs are split into 19 components.

The 1^st component contains the pair

EVEN^#(NUMERAL(n))

→

EVEN^#(n)

(142)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	0
[ODD(x₁)]	=	0
[BIT1(x₁)]	=	0
[le^#(x₁, x₂)]	=	0
[lt^#(x₁, x₂)]	=	0
[EVEN(x₁)]	=	0
[gt(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	0
[T]	=	0
[F]	=	0
[plus^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[ge^#(x₁, x₂)]	=	0
[exp^#(x₁, x₂)]	=	0
[NUMERAL(x₁)]	=	x₁ + 1
[eq^#(x₁, x₂)]	=	0
[mult(x₁, x₂)]	=	0
[ODD^#(x₁)]	=	0
[0]	=	0
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[NUMERAL^#(x₁)]	=	0
[SUC^#(x₁)]	=	0
[BIT0^#(x₁)]	=	0
[gt^#(x₁, x₂)]	=	0
[PRE(x₁)]	=	0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[EVEN^#(x₁)]	=	x₁ + 0
[BIT0(x₁)]	=	0
[exp(x₁, x₂)]	=	0
[PRE^#(x₁)]	=	0
[SUC(x₁)]	=	0
[lt(x₁, x₂)]	=	0
[mult^#(x₁, x₂)]	=	0

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

EVEN^#(NUMERAL(n))

→

EVEN^#(n)

(142)

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

eq^#(BIT1(m),BIT1(n))	→	eq^#(m,n)	(191)
eq^#(BIT0(m),BIT0(n))	→	eq^#(m,n)	(187)
eq^#(NUMERAL(m),NUMERAL(n))	→	eq^#(m,n)	(134)

1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	0
[ODD(x₁)]	=	0
[BIT1(x₁)]	=	x₁ + 1
[le^#(x₁, x₂)]	=	0
[lt^#(x₁, x₂)]	=	0
[EVEN(x₁)]	=	0
[gt(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	0
[T]	=	0
[F]	=	0
[plus^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[ge^#(x₁, x₂)]	=	0
[exp^#(x₁, x₂)]	=	0
[NUMERAL(x₁)]	=	x₁ + 30094
[eq^#(x₁, x₂)]	=	x₁ + x₂ + 0
[mult(x₁, x₂)]	=	0
[ODD^#(x₁)]	=	0
[0]	=	0
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[NUMERAL^#(x₁)]	=	0
[SUC^#(x₁)]	=	0
[BIT0^#(x₁)]	=	0
[gt^#(x₁, x₂)]	=	0
[PRE(x₁)]	=	0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[EVEN^#(x₁)]	=	0
[BIT0(x₁)]	=	x₁ + 14235
[exp(x₁, x₂)]	=	0
[PRE^#(x₁)]	=	0
[SUC(x₁)]	=	0
[lt(x₁, x₂)]	=	0
[mult^#(x₁, x₂)]	=	0

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

eq^#(BIT1(m),BIT1(n))	→	eq^#(m,n)	(191)
eq^#(BIT0(m),BIT0(n))	→	eq^#(m,n)	(187)
eq^#(NUMERAL(m),NUMERAL(n))	→	eq^#(m,n)	(134)

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

eq^#(0,BIT0(n))

→

eq^#(0,n)

(185)

1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	0
[ODD(x₁)]	=	0
[BIT1(x₁)]	=	1
[le^#(x₁, x₂)]	=	0
[lt^#(x₁, x₂)]	=	0
[EVEN(x₁)]	=	0
[gt(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	0
[T]	=	0
[F]	=	0
[plus^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[ge^#(x₁, x₂)]	=	0
[exp^#(x₁, x₂)]	=	0
[NUMERAL(x₁)]	=	30094
[eq^#(x₁, x₂)]	=	x₂ + 0
[mult(x₁, x₂)]	=	0
[ODD^#(x₁)]	=	0
[0]	=	0
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[NUMERAL^#(x₁)]	=	0
[SUC^#(x₁)]	=	0
[BIT0^#(x₁)]	=	0
[gt^#(x₁, x₂)]	=	0
[PRE(x₁)]	=	0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[EVEN^#(x₁)]	=	0
[BIT0(x₁)]	=	x₁ + 14235
[exp(x₁, x₂)]	=	0
[PRE^#(x₁)]	=	0
[SUC(x₁)]	=	0
[lt(x₁, x₂)]	=	0
[mult^#(x₁, x₂)]	=	0

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

eq^#(0,BIT0(n))

→

eq^#(0,n)

(185)

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

minus^#(BIT0(m),BIT1(n))	→	minus^#(m,n)	(161)
minus^#(NUMERAL(m),NUMERAL(n))	→	minus^#(m,n)	(192)
minus^#(BIT1(m),BIT1(n))	→	minus^#(m,n)	(131)
minus^#(BIT0(m),BIT0(n))	→	minus^#(m,n)	(180)
minus^#(BIT1(m),BIT0(n))	→	minus^#(m,n)	(171)

1.1.4 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	0
[ODD(x₁)]	=	0
[BIT1(x₁)]	=	x₁ + 1
[le^#(x₁, x₂)]	=	0
[lt^#(x₁, x₂)]	=	0
[EVEN(x₁)]	=	0
[gt(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	0
[T]	=	0
[F]	=	0
[plus^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[ge^#(x₁, x₂)]	=	0
[exp^#(x₁, x₂)]	=	0
[NUMERAL(x₁)]	=	x₁ + 1
[eq^#(x₁, x₂)]	=	0
[mult(x₁, x₂)]	=	0
[ODD^#(x₁)]	=	0
[0]	=	0
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[NUMERAL^#(x₁)]	=	0
[SUC^#(x₁)]	=	0
[BIT0^#(x₁)]	=	0
[gt^#(x₁, x₂)]	=	0
[PRE(x₁)]	=	0
[minus^#(x₁, x₂)]	=	x₁ + 0
[plus(x₁, x₂)]	=	0
[EVEN^#(x₁)]	=	0
[BIT0(x₁)]	=	x₁ + 1
[exp(x₁, x₂)]	=	0
[PRE^#(x₁)]	=	0
[SUC(x₁)]	=	0
[lt(x₁, x₂)]	=	0
[mult^#(x₁, x₂)]	=	0

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

minus^#(BIT0(m),BIT1(n))	→	minus^#(m,n)	(161)
minus^#(NUMERAL(m),NUMERAL(n))	→	minus^#(m,n)	(192)
minus^#(BIT1(m),BIT1(n))	→	minus^#(m,n)	(131)
minus^#(BIT0(m),BIT0(n))	→	minus^#(m,n)	(180)
minus^#(BIT1(m),BIT0(n))	→	minus^#(m,n)	(171)

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

PRE^#(BIT0(n))	→	PRE^#(n)	(190)
PRE^#(NUMERAL(n))	→	PRE^#(n)	(136)

1.1.5 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	0
[ODD(x₁)]	=	0
[BIT1(x₁)]	=	1
[le^#(x₁, x₂)]	=	0
[lt^#(x₁, x₂)]	=	0
[EVEN(x₁)]	=	0
[gt(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	0
[T]	=	0
[F]	=	0
[plus^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[ge^#(x₁, x₂)]	=	0
[exp^#(x₁, x₂)]	=	0
[NUMERAL(x₁)]	=	x₁ + 1
[eq^#(x₁, x₂)]	=	0
[mult(x₁, x₂)]	=	0
[ODD^#(x₁)]	=	0
[0]	=	0
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[NUMERAL^#(x₁)]	=	0
[SUC^#(x₁)]	=	0
[BIT0^#(x₁)]	=	0
[gt^#(x₁, x₂)]	=	0
[PRE(x₁)]	=	0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[EVEN^#(x₁)]	=	0
[BIT0(x₁)]	=	x₁ + 1
[exp(x₁, x₂)]	=	0
[PRE^#(x₁)]	=	x₁ + 0
[SUC(x₁)]	=	0
[lt(x₁, x₂)]	=	0
[mult^#(x₁, x₂)]	=	0

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

PRE^#(BIT0(n))	→	PRE^#(n)	(190)
PRE^#(NUMERAL(n))	→	PRE^#(n)	(136)

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

exp^#(BIT0(m),BIT1(n))	→	exp^#(BIT0(m),n)	(126)
exp^#(BIT0(m),BIT1(n))	→	exp^#(BIT0(m),n)	(126)
exp^#(NUMERAL(m),NUMERAL(n))	→	exp^#(m,n)	(124)
exp^#(BIT0(m),BIT0(n))	→	exp^#(BIT0(m),n)	(122)
exp^#(BIT0(m),BIT0(n))	→	exp^#(BIT0(m),n)	(122)

1.1.6 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	0
[ODD(x₁)]	=	0
[BIT1(x₁)]	=	x₁ + 1
[le^#(x₁, x₂)]	=	0
[lt^#(x₁, x₂)]	=	0
[EVEN(x₁)]	=	0
[gt(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	0
[T]	=	0
[F]	=	0
[plus^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[ge^#(x₁, x₂)]	=	0
[exp^#(x₁, x₂)]	=	x₂ + 0
[NUMERAL(x₁)]	=	x₁ + 1
[eq^#(x₁, x₂)]	=	0
[mult(x₁, x₂)]	=	0
[ODD^#(x₁)]	=	0
[0]	=	36466
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[NUMERAL^#(x₁)]	=	0
[SUC^#(x₁)]	=	0
[BIT0^#(x₁)]	=	0
[gt^#(x₁, x₂)]	=	0
[PRE(x₁)]	=	0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[EVEN^#(x₁)]	=	0
[BIT0(x₁)]	=	x₁ + 1
[exp(x₁, x₂)]	=	0
[PRE^#(x₁)]	=	0
[SUC(x₁)]	=	0
[lt(x₁, x₂)]	=	0
[mult^#(x₁, x₂)]	=	0

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

exp^#(BIT0(m),BIT1(n))	→	exp^#(BIT0(m),n)	(126)
exp^#(BIT0(m),BIT1(n))	→	exp^#(BIT0(m),n)	(126)
exp^#(NUMERAL(m),NUMERAL(n))	→	exp^#(m,n)	(124)
exp^#(BIT0(m),BIT0(n))	→	exp^#(BIT0(m),n)	(122)
exp^#(BIT0(m),BIT0(n))	→	exp^#(BIT0(m),n)	(122)

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

exp^#(BIT1(m),BIT1(n))	→	exp^#(BIT1(m),n)	(155)
exp^#(BIT1(m),BIT0(n))	→	exp^#(BIT1(m),n)	(140)
exp^#(BIT1(m),BIT1(n))	→	exp^#(BIT1(m),n)	(155)
exp^#(BIT1(m),BIT0(n))	→	exp^#(BIT1(m),n)	(140)

1.1.7 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	0
[ODD(x₁)]	=	0
[BIT1(x₁)]	=	x₁ + 1
[le^#(x₁, x₂)]	=	0
[lt^#(x₁, x₂)]	=	0
[EVEN(x₁)]	=	0
[gt(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	0
[T]	=	0
[F]	=	0
[plus^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[ge^#(x₁, x₂)]	=	0
[exp^#(x₁, x₂)]	=	x₂ + 0
[NUMERAL(x₁)]	=	1
[eq^#(x₁, x₂)]	=	0
[mult(x₁, x₂)]	=	0
[ODD^#(x₁)]	=	0
[0]	=	1
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[NUMERAL^#(x₁)]	=	0
[SUC^#(x₁)]	=	0
[BIT0^#(x₁)]	=	0
[gt^#(x₁, x₂)]	=	0
[PRE(x₁)]	=	0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[EVEN^#(x₁)]	=	0
[BIT0(x₁)]	=	x₁ + 1
[exp(x₁, x₂)]	=	0
[PRE^#(x₁)]	=	0
[SUC(x₁)]	=	0
[lt(x₁, x₂)]	=	0
[mult^#(x₁, x₂)]	=	0

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

exp^#(BIT1(m),BIT1(n))	→	exp^#(BIT1(m),n)	(155)
exp^#(BIT1(m),BIT0(n))	→	exp^#(BIT1(m),n)	(140)
exp^#(BIT1(m),BIT1(n))	→	exp^#(BIT1(m),n)	(155)
exp^#(BIT1(m),BIT0(n))	→	exp^#(BIT1(m),n)	(140)

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

gt^#(NUMERAL(n),NUMERAL(m))	→	gt^#(n,m)	(162)
ge^#(BIT0(n),BIT1(m))	→	gt^#(n,m)	(156)
ge^#(BIT1(n),BIT0(m))	→	ge^#(n,m)	(195)
gt^#(BIT0(n),BIT1(m))	→	gt^#(n,m)	(183)
ge^#(NUMERAL(n),NUMERAL(m))	→	ge^#(n,m)	(127)
ge^#(BIT1(n),BIT1(m))	→	ge^#(n,m)	(175)
gt^#(BIT1(n),BIT0(m))	→	ge^#(n,m)	(174)
gt^#(BIT0(n),BIT0(m))	→	gt^#(n,m)	(168)
gt^#(BIT1(n),BIT1(m))	→	gt^#(n,m)	(167)
ge^#(BIT0(n),BIT0(m))	→	ge^#(n,m)	(165)

1.1.8 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	0
[ODD(x₁)]	=	0
[BIT1(x₁)]	=	x₁ + 1
[le^#(x₁, x₂)]	=	0
[lt^#(x₁, x₂)]	=	0
[EVEN(x₁)]	=	0
[gt(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	0
[T]	=	0
[F]	=	0
[plus^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[ge^#(x₁, x₂)]	=	x₁ + x₂ + 0
[exp^#(x₁, x₂)]	=	0
[NUMERAL(x₁)]	=	x₁ + 1
[eq^#(x₁, x₂)]	=	0
[mult(x₁, x₂)]	=	0
[ODD^#(x₁)]	=	0
[0]	=	35657
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[NUMERAL^#(x₁)]	=	0
[SUC^#(x₁)]	=	0
[BIT0^#(x₁)]	=	0
[gt^#(x₁, x₂)]	=	x₁ + x₂ + 0
[PRE(x₁)]	=	0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[EVEN^#(x₁)]	=	0
[BIT0(x₁)]	=	x₁ + 1
[exp(x₁, x₂)]	=	0
[PRE^#(x₁)]	=	0
[SUC(x₁)]	=	0
[lt(x₁, x₂)]	=	0
[mult^#(x₁, x₂)]	=	0

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

gt^#(NUMERAL(n),NUMERAL(m))	→	gt^#(n,m)	(162)
ge^#(BIT0(n),BIT1(m))	→	gt^#(n,m)	(156)
ge^#(BIT1(n),BIT0(m))	→	ge^#(n,m)	(195)
gt^#(BIT0(n),BIT1(m))	→	gt^#(n,m)	(183)
ge^#(NUMERAL(n),NUMERAL(m))	→	ge^#(n,m)	(127)
ge^#(BIT1(n),BIT1(m))	→	ge^#(n,m)	(175)
gt^#(BIT1(n),BIT0(m))	→	ge^#(n,m)	(174)
gt^#(BIT0(n),BIT0(m))	→	gt^#(n,m)	(168)
gt^#(BIT1(n),BIT1(m))	→	gt^#(n,m)	(167)
ge^#(BIT0(n),BIT0(m))	→	ge^#(n,m)	(165)

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

ge^#(0,BIT0(n))

→

ge^#(0,n)

(119)

1.1.9 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	0
[ODD(x₁)]	=	0
[BIT1(x₁)]	=	1
[le^#(x₁, x₂)]	=	0
[lt^#(x₁, x₂)]	=	0
[EVEN(x₁)]	=	0
[gt(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	0
[T]	=	0
[F]	=	0
[plus^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[ge^#(x₁, x₂)]	=	x₂ + 0
[exp^#(x₁, x₂)]	=	0
[NUMERAL(x₁)]	=	1
[eq^#(x₁, x₂)]	=	0
[mult(x₁, x₂)]	=	0
[ODD^#(x₁)]	=	0
[0]	=	35657
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[NUMERAL^#(x₁)]	=	0
[SUC^#(x₁)]	=	0
[BIT0^#(x₁)]	=	0
[gt^#(x₁, x₂)]	=	0
[PRE(x₁)]	=	0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[EVEN^#(x₁)]	=	0
[BIT0(x₁)]	=	x₁ + 1
[exp(x₁, x₂)]	=	0
[PRE^#(x₁)]	=	0
[SUC(x₁)]	=	0
[lt(x₁, x₂)]	=	0
[mult^#(x₁, x₂)]	=	0

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

ge^#(0,BIT0(n))

→

ge^#(0,n)

(119)

could be deleted.

1.1.9.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 10^th component contains the pair

gt^#(BIT0(n),0)

→

gt^#(n,0)

(123)

1.1.10 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	0
[ODD(x₁)]	=	0
[BIT1(x₁)]	=	1
[le^#(x₁, x₂)]	=	0
[lt^#(x₁, x₂)]	=	0
[EVEN(x₁)]	=	0
[gt(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	0
[T]	=	0
[F]	=	0
[plus^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[ge^#(x₁, x₂)]	=	0
[exp^#(x₁, x₂)]	=	0
[NUMERAL(x₁)]	=	1
[eq^#(x₁, x₂)]	=	0
[mult(x₁, x₂)]	=	0
[ODD^#(x₁)]	=	0
[0]	=	1
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[NUMERAL^#(x₁)]	=	0
[SUC^#(x₁)]	=	0
[BIT0^#(x₁)]	=	0
[gt^#(x₁, x₂)]	=	x₁ + 0
[PRE(x₁)]	=	0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[EVEN^#(x₁)]	=	0
[BIT0(x₁)]	=	x₁ + 1
[exp(x₁, x₂)]	=	0
[PRE^#(x₁)]	=	0
[SUC(x₁)]	=	0
[lt(x₁, x₂)]	=	0
[mult^#(x₁, x₂)]	=	0

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

gt^#(BIT0(n),0)

→

gt^#(n,0)

(123)

could be deleted.

1.1.10.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 11^th component contains the pair

exp^#(0,BIT0(n))	→	exp^#(0,n)	(166)
exp^#(0,BIT0(n))	→	exp^#(0,n)	(166)

1.1.11 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	0
[ODD(x₁)]	=	0
[BIT1(x₁)]	=	1
[le^#(x₁, x₂)]	=	0
[lt^#(x₁, x₂)]	=	0
[EVEN(x₁)]	=	0
[gt(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	0
[T]	=	0
[F]	=	0
[plus^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[ge^#(x₁, x₂)]	=	0
[exp^#(x₁, x₂)]	=	x₂ + 0
[NUMERAL(x₁)]	=	1
[eq^#(x₁, x₂)]	=	0
[mult(x₁, x₂)]	=	0
[ODD^#(x₁)]	=	0
[0]	=	1
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[NUMERAL^#(x₁)]	=	0
[SUC^#(x₁)]	=	0
[BIT0^#(x₁)]	=	0
[gt^#(x₁, x₂)]	=	0
[PRE(x₁)]	=	0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[EVEN^#(x₁)]	=	0
[BIT0(x₁)]	=	x₁ + 1
[exp(x₁, x₂)]	=	0
[PRE^#(x₁)]	=	0
[SUC(x₁)]	=	0
[lt(x₁, x₂)]	=	0
[mult^#(x₁, x₂)]	=	0

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

exp^#(0,BIT0(n))	→	exp^#(0,n)	(166)
exp^#(0,BIT0(n))	→	exp^#(0,n)	(166)

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^#(BIT0(n),0)

→

eq^#(n,0)

(178)

1.1.12 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	0
[ODD(x₁)]	=	0
[BIT1(x₁)]	=	1
[le^#(x₁, x₂)]	=	0
[lt^#(x₁, x₂)]	=	0
[EVEN(x₁)]	=	0
[gt(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	0
[T]	=	0
[F]	=	0
[plus^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[ge^#(x₁, x₂)]	=	0
[exp^#(x₁, x₂)]	=	0
[NUMERAL(x₁)]	=	1
[eq^#(x₁, x₂)]	=	x₁ + 0
[mult(x₁, x₂)]	=	0
[ODD^#(x₁)]	=	0
[0]	=	1
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[NUMERAL^#(x₁)]	=	0
[SUC^#(x₁)]	=	0
[BIT0^#(x₁)]	=	0
[gt^#(x₁, x₂)]	=	0
[PRE(x₁)]	=	0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[EVEN^#(x₁)]	=	0
[BIT0(x₁)]	=	x₁ + 1
[exp(x₁, x₂)]	=	0
[PRE^#(x₁)]	=	0
[SUC(x₁)]	=	0
[lt(x₁, x₂)]	=	0
[mult^#(x₁, x₂)]	=	0

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

eq^#(BIT0(n),0)

→

eq^#(n,0)

(178)

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

mult^#(BIT0(m),BIT0(n))	→	mult^#(m,n)	(159)
mult^#(BIT0(m),BIT1(n))	→	mult^#(m,n)	(150)
mult^#(NUMERAL(m),NUMERAL(n))	→	mult^#(m,n)	(146)
mult^#(BIT1(m),BIT1(n))	→	mult^#(m,n)	(130)
mult^#(BIT1(m),BIT0(n))	→	mult^#(m,n)	(173)

1.1.13 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	0
[ODD(x₁)]	=	0
[BIT1(x₁)]	=	x₁ + 1
[le^#(x₁, x₂)]	=	0
[lt^#(x₁, x₂)]	=	0
[EVEN(x₁)]	=	0
[gt(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	0
[T]	=	0
[F]	=	0
[plus^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[ge^#(x₁, x₂)]	=	0
[exp^#(x₁, x₂)]	=	0
[NUMERAL(x₁)]	=	x₁ + 61160
[eq^#(x₁, x₂)]	=	0
[mult(x₁, x₂)]	=	0
[ODD^#(x₁)]	=	0
[0]	=	1
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[NUMERAL^#(x₁)]	=	0
[SUC^#(x₁)]	=	0
[BIT0^#(x₁)]	=	0
[gt^#(x₁, x₂)]	=	0
[PRE(x₁)]	=	0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[EVEN^#(x₁)]	=	0
[BIT0(x₁)]	=	x₁ + 11966
[exp(x₁, x₂)]	=	0
[PRE^#(x₁)]	=	0
[SUC(x₁)]	=	0
[lt(x₁, x₂)]	=	0
[mult^#(x₁, x₂)]	=	x₁ + x₂ + 0

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

mult^#(BIT0(m),BIT0(n))	→	mult^#(m,n)	(159)
mult^#(BIT0(m),BIT1(n))	→	mult^#(m,n)	(150)
mult^#(NUMERAL(m),NUMERAL(n))	→	mult^#(m,n)	(146)
mult^#(BIT1(m),BIT1(n))	→	mult^#(m,n)	(130)
mult^#(BIT1(m),BIT0(n))	→	mult^#(m,n)	(173)

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

ODD^#(NUMERAL(n))

→

ODD^#(n)

(111)

1.1.14 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	0
[ODD(x₁)]	=	0
[BIT1(x₁)]	=	1
[le^#(x₁, x₂)]	=	0
[lt^#(x₁, x₂)]	=	0
[EVEN(x₁)]	=	0
[gt(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	0
[T]	=	0
[F]	=	0
[plus^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[ge^#(x₁, x₂)]	=	0
[exp^#(x₁, x₂)]	=	0
[NUMERAL(x₁)]	=	x₁ + 61160
[eq^#(x₁, x₂)]	=	0
[mult(x₁, x₂)]	=	0
[ODD^#(x₁)]	=	x₁ + 0
[0]	=	1
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[NUMERAL^#(x₁)]	=	0
[SUC^#(x₁)]	=	0
[BIT0^#(x₁)]	=	0
[gt^#(x₁, x₂)]	=	0
[PRE(x₁)]	=	0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[EVEN^#(x₁)]	=	0
[BIT0(x₁)]	=	x₁ + 11966
[exp(x₁, x₂)]	=	0
[PRE^#(x₁)]	=	0
[SUC(x₁)]	=	0
[lt(x₁, x₂)]	=	0
[mult^#(x₁, x₂)]	=	0

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

ODD^#(NUMERAL(n))

→

ODD^#(n)

(111)

could be deleted.

1.1.14.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 15^th component contains the pair

plus^#(BIT1(m),BIT0(n))	→	plus^#(m,n)	(188)
plus^#(BIT0(m),BIT1(n))	→	plus^#(m,n)	(143)
plus^#(NUMERAL(m),NUMERAL(n))	→	plus^#(m,n)	(132)
plus^#(BIT0(m),BIT0(n))	→	plus^#(m,n)	(179)
plus^#(BIT1(m),BIT1(n))	→	plus^#(m,n)	(170)

1.1.15 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	0
[ODD(x₁)]	=	0
[BIT1(x₁)]	=	x₁ + 1
[le^#(x₁, x₂)]	=	0
[lt^#(x₁, x₂)]	=	0
[EVEN(x₁)]	=	0
[gt(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	0
[T]	=	0
[F]	=	0
[plus^#(x₁, x₂)]	=	x₁ + x₂ + 0
[eq(x₁, x₂)]	=	0
[ge^#(x₁, x₂)]	=	0
[exp^#(x₁, x₂)]	=	0
[NUMERAL(x₁)]	=	x₁ + 29525
[eq^#(x₁, x₂)]	=	0
[mult(x₁, x₂)]	=	0
[ODD^#(x₁)]	=	0
[0]	=	1
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[NUMERAL^#(x₁)]	=	0
[SUC^#(x₁)]	=	0
[BIT0^#(x₁)]	=	0
[gt^#(x₁, x₂)]	=	0
[PRE(x₁)]	=	0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[EVEN^#(x₁)]	=	0
[BIT0(x₁)]	=	x₁ + 44849
[exp(x₁, x₂)]	=	0
[PRE^#(x₁)]	=	0
[SUC(x₁)]	=	0
[lt(x₁, x₂)]	=	0
[mult^#(x₁, x₂)]	=	0

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

plus^#(BIT1(m),BIT0(n))	→	plus^#(m,n)	(188)
plus^#(BIT0(m),BIT1(n))	→	plus^#(m,n)	(143)
plus^#(NUMERAL(m),NUMERAL(n))	→	plus^#(m,n)	(132)
plus^#(BIT0(m),BIT0(n))	→	plus^#(m,n)	(179)
plus^#(BIT1(m),BIT1(n))	→	plus^#(m,n)	(170)

could be deleted.

1.1.15.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 16^th component contains the pair

SUC^#(NUMERAL(n))	→	SUC^#(n)	(152)
SUC^#(BIT1(n))	→	SUC^#(n)	(147)

1.1.16 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	0
[ODD(x₁)]	=	0
[BIT1(x₁)]	=	x₁ + 1
[le^#(x₁, x₂)]	=	0
[lt^#(x₁, x₂)]	=	0
[EVEN(x₁)]	=	0
[gt(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	0
[T]	=	0
[F]	=	0
[plus^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[ge^#(x₁, x₂)]	=	0
[exp^#(x₁, x₂)]	=	0
[NUMERAL(x₁)]	=	x₁ + 29525
[eq^#(x₁, x₂)]	=	0
[mult(x₁, x₂)]	=	0
[ODD^#(x₁)]	=	0
[0]	=	1
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[NUMERAL^#(x₁)]	=	0
[SUC^#(x₁)]	=	x₁ + 0
[BIT0^#(x₁)]	=	0
[gt^#(x₁, x₂)]	=	0
[PRE(x₁)]	=	0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[EVEN^#(x₁)]	=	0
[BIT0(x₁)]	=	x₁ + 44849
[exp(x₁, x₂)]	=	0
[PRE^#(x₁)]	=	0
[SUC(x₁)]	=	0
[lt(x₁, x₂)]	=	0
[mult^#(x₁, x₂)]	=	0

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

SUC^#(NUMERAL(n))	→	SUC^#(n)	(152)
SUC^#(BIT1(n))	→	SUC^#(n)	(147)

could be deleted.

1.1.16.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 17^th component contains the pair

le^#(NUMERAL(m),NUMERAL(n))	→	le^#(m,n)	(163)
le^#(BIT1(m),BIT1(n))	→	le^#(m,n)	(158)
lt^#(NUMERAL(m),NUMERAL(n))	→	lt^#(m,n)	(151)
le^#(BIT0(m),BIT1(n))	→	le^#(m,n)	(141)
lt^#(BIT0(m),BIT1(n))	→	le^#(m,n)	(137)
le^#(BIT1(m),BIT0(n))	→	lt^#(m,n)	(181)
le^#(BIT0(m),BIT0(n))	→	le^#(m,n)	(129)
lt^#(BIT1(m),BIT0(n))	→	lt^#(m,n)	(121)
lt^#(BIT1(m),BIT1(n))	→	lt^#(m,n)	(117)
lt^#(BIT0(m),BIT0(n))	→	lt^#(m,n)	(164)

1.1.17 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	0
[ODD(x₁)]	=	0
[BIT1(x₁)]	=	x₁ + 1
[le^#(x₁, x₂)]	=	x₁ + x₂ + 0
[lt^#(x₁, x₂)]	=	x₁ + x₂ + 1
[EVEN(x₁)]	=	0
[gt(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	0
[T]	=	0
[F]	=	0
[plus^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[ge^#(x₁, x₂)]	=	0
[exp^#(x₁, x₂)]	=	0
[NUMERAL(x₁)]	=	x₁ + 29525
[eq^#(x₁, x₂)]	=	0
[mult(x₁, x₂)]	=	0
[ODD^#(x₁)]	=	0
[0]	=	1
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[NUMERAL^#(x₁)]	=	0
[SUC^#(x₁)]	=	0
[BIT0^#(x₁)]	=	0
[gt^#(x₁, x₂)]	=	0
[PRE(x₁)]	=	0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[EVEN^#(x₁)]	=	0
[BIT0(x₁)]	=	x₁ + 1
[exp(x₁, x₂)]	=	0
[PRE^#(x₁)]	=	0
[SUC(x₁)]	=	0
[lt(x₁, x₂)]	=	0
[mult^#(x₁, x₂)]	=	0

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

le^#(NUMERAL(m),NUMERAL(n))	→	le^#(m,n)	(163)
le^#(BIT1(m),BIT1(n))	→	le^#(m,n)	(158)
lt^#(NUMERAL(m),NUMERAL(n))	→	lt^#(m,n)	(151)
le^#(BIT0(m),BIT1(n))	→	le^#(m,n)	(141)
lt^#(BIT0(m),BIT1(n))	→	le^#(m,n)	(137)
le^#(BIT1(m),BIT0(n))	→	lt^#(m,n)	(181)
le^#(BIT0(m),BIT0(n))	→	le^#(m,n)	(129)
lt^#(BIT1(m),BIT0(n))	→	lt^#(m,n)	(121)
lt^#(BIT1(m),BIT1(n))	→	lt^#(m,n)	(117)
lt^#(BIT0(m),BIT0(n))	→	lt^#(m,n)	(164)

could be deleted.

1.1.17.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 18^th component contains the pair

le^#(BIT0(n),0)

→

le^#(n,0)

(177)

1.1.18 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	0
[ODD(x₁)]	=	0
[BIT1(x₁)]	=	1
[le^#(x₁, x₂)]	=	x₁ + 0
[lt^#(x₁, x₂)]	=	1
[EVEN(x₁)]	=	0
[gt(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	0
[T]	=	0
[F]	=	0
[plus^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[ge^#(x₁, x₂)]	=	0
[exp^#(x₁, x₂)]	=	0
[NUMERAL(x₁)]	=	29525
[eq^#(x₁, x₂)]	=	0
[mult(x₁, x₂)]	=	0
[ODD^#(x₁)]	=	0
[0]	=	1
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[NUMERAL^#(x₁)]	=	0
[SUC^#(x₁)]	=	0
[BIT0^#(x₁)]	=	0
[gt^#(x₁, x₂)]	=	0
[PRE(x₁)]	=	0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[EVEN^#(x₁)]	=	0
[BIT0(x₁)]	=	x₁ + 1
[exp(x₁, x₂)]	=	0
[PRE^#(x₁)]	=	0
[SUC(x₁)]	=	0
[lt(x₁, x₂)]	=	0
[mult^#(x₁, x₂)]	=	0

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

le^#(BIT0(n),0)

→

le^#(n,0)

(177)

could be deleted.

1.1.18.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 19^th component contains the pair

lt^#(0,BIT0(n))

→

lt^#(0,n)

(201)

1.1.19 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[le(x₁, x₂)]	=	0
[ODD(x₁)]	=	0
[BIT1(x₁)]	=	1
[le^#(x₁, x₂)]	=	0
[lt^#(x₁, x₂)]	=	x₂ + 1
[EVEN(x₁)]	=	0
[gt(x₁, x₂)]	=	0
[minus(x₁, x₂)]	=	0
[T]	=	0
[F]	=	0
[plus^#(x₁, x₂)]	=	0
[eq(x₁, x₂)]	=	0
[ge^#(x₁, x₂)]	=	0
[exp^#(x₁, x₂)]	=	0
[NUMERAL(x₁)]	=	29525
[eq^#(x₁, x₂)]	=	0
[mult(x₁, x₂)]	=	0
[ODD^#(x₁)]	=	0
[0]	=	1
[if(x₁, x₂, x₃)]	=	0
[ge(x₁, x₂)]	=	0
[NUMERAL^#(x₁)]	=	0
[SUC^#(x₁)]	=	0
[BIT0^#(x₁)]	=	0
[gt^#(x₁, x₂)]	=	0
[PRE(x₁)]	=	0
[minus^#(x₁, x₂)]	=	0
[plus(x₁, x₂)]	=	0
[EVEN^#(x₁)]	=	0
[BIT0(x₁)]	=	x₁ + 1
[exp(x₁, x₂)]	=	0
[PRE^#(x₁)]	=	0
[SUC(x₁)]	=	0
[lt(x₁, x₂)]	=	0
[mult^#(x₁, x₂)]	=	0

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

lt^#(0,BIT0(n))

→

lt^#(0,n)

(201)

could be deleted.

1.1.19.1 Dependency Graph Processor

The dependency pairs are split into 0 components.