Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/264033)

The rewrite relation of the following TRS is considered.

0(0(1(0(2(x1)))))	→	0(0(1(2(2(x1)))))	(1)
0(0(1(0(2(x1)))))	→	0(0(2(1(2(x1)))))	(2)
0(0(1(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(3)
0(0(1(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(4)
0(0(1(0(2(x1)))))	→	0(1(2(0(2(x1)))))	(5)
0(0(1(0(2(x1)))))	→	0(1(2(2(0(x1)))))	(6)
0(0(1(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(7)
0(0(1(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(8)
0(0(1(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(9)
0(0(1(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(10)
0(0(1(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(11)
0(0(1(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(12)
0(0(1(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(13)
0(0(1(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(14)
0(0(1(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(15)
0(0(1(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(16)
0(0(1(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(17)
0(0(1(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(18)
0(0(1(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(19)
0(0(1(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(20)
0(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(21)
0(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(22)
0(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(23)
0(1(2(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(24)
0(1(2(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(25)
0(1(2(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(26)
0(1(2(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(27)
0(1(2(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(28)
0(1(2(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(29)
0(1(2(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(30)
0(1(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(31)
0(1(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(32)
0(1(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(33)
0(1(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(34)
1(0(1(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(35)
1(0(1(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(36)
1(0(1(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(37)
1(0(1(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(38)
1(0(1(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(39)
1(0(1(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(40)
1(0(1(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(41)
1(0(1(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(42)
1(0(1(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(43)
1(0(1(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(44)
1(0(1(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(45)
1(0(1(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(46)
1(0(1(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(47)
1(0(1(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(48)
1(0(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(49)
1(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(50)
1(0(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(51)
1(0(1(0(2(x1)))))	→	2(1(2(2(0(x1)))))	(52)
1(0(1(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(53)
1(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(54)
1(0(1(0(2(x1)))))	→	2(2(1(2(0(x1)))))	(55)
1(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(56)
1(0(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(57)
1(0(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(58)
1(0(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(59)
1(0(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(60)
1(0(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(61)
1(0(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(62)
1(1(2(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(63)
1(1(2(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(64)
1(1(2(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(65)
1(1(2(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(66)
1(1(2(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(67)
1(1(2(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(68)
1(1(2(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(69)
1(1(2(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(70)
1(1(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(71)
1(1(2(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(72)
1(1(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(73)
1(1(2(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(74)
1(1(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(75)
1(1(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(76)
1(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(77)
1(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(78)
1(1(2(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(79)
1(1(2(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(80)
1(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(81)
1(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(82)
1(2(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(83)
2(0(1(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(84)
2(0(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(85)
2(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(86)
2(0(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(87)
2(0(1(0(2(x1)))))	→	2(1(2(2(0(x1)))))	(88)
2(0(1(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(89)
2(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(90)
2(0(1(0(2(x1)))))	→	2(2(1(2(0(x1)))))	(91)
2(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(92)
2(1(1(0(2(x1)))))	→	2(0(1(0(2(x1)))))	(93)
2(1(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(94)
2(1(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(95)
2(1(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(96)
2(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(97)
2(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(98)
2(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(99)
2(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(100)

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.

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

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

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

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	x₁ + 11798
[1(x₁)]	=	x₁ + 11799
[2^#(x₁)]	=	x₁ + 0
[0(x₁)]	=	x₁ + 11799
[2(x₁)]	=	x₁ + 1
[1^#(x₁)]	=	x₁ + 1

together with the usable rules

0(0(1(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(18)
1(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(50)
1(1(2(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(80)
0(0(1(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(4)
0(0(1(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(15)
0(0(1(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(8)
1(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(54)
0(0(1(0(2(x1)))))	→	0(0(1(2(2(x1)))))	(1)
1(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(77)
0(0(1(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(3)
0(0(1(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(16)
0(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(21)
1(0(1(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(36)
1(1(2(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(68)
2(0(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(85)
2(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(100)
0(1(2(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(26)
1(1(2(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(63)
0(0(1(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(19)
0(1(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(32)
0(0(1(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(17)
1(0(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(60)
0(1(2(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(27)
2(0(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(87)
2(0(1(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(84)
0(1(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(34)
0(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(22)
0(1(2(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(28)
1(1(2(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(65)
1(0(1(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(44)
0(0(1(0(2(x1)))))	→	0(1(2(0(2(x1)))))	(5)
1(1(2(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(72)
0(1(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(33)
1(1(2(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(64)
2(1(1(0(2(x1)))))	→	2(0(1(0(2(x1)))))	(93)
2(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(92)
0(0(1(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(10)
1(0(1(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(39)
0(0(1(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(7)
2(0(1(0(2(x1)))))	→	2(1(2(2(0(x1)))))	(88)
0(0(1(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(20)
0(1(2(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(25)
1(0(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(49)
1(0(1(0(2(x1)))))	→	2(1(2(2(0(x1)))))	(52)
0(1(2(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(30)
1(0(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(62)
0(0(1(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(14)
1(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(82)
2(0(1(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(89)
1(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(56)
1(1(2(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(79)
0(1(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(31)
0(0(1(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(12)
1(1(2(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(69)
2(1(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(96)
1(0(1(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(45)
1(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(78)
1(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(81)
0(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(23)
1(1(2(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(70)
0(1(2(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(24)
2(1(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(94)
1(1(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(76)
1(0(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(57)
2(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(98)
0(0(1(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(11)
0(0(1(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(9)
0(0(1(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(13)
1(0(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(51)
2(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(90)
1(0(1(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(40)
1(1(2(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(67)
1(0(1(0(2(x1)))))	→	2(2(1(2(0(x1)))))	(55)
1(0(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(59)
0(0(1(0(2(x1)))))	→	0(1(2(2(0(x1)))))	(6)
1(0(1(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(38)
1(0(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(61)
1(0(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(58)
1(1(2(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(74)
1(1(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(75)
1(0(1(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(48)
1(1(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(71)
1(0(1(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(53)
1(0(1(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(47)
1(1(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(73)
2(0(1(0(2(x1)))))	→	2(2(1(2(0(x1)))))	(91)
2(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(97)
2(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(99)
1(0(1(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(37)
1(0(1(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(41)
2(1(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(95)
1(0(1(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(42)
1(0(1(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(46)
1(1(2(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(66)
1(2(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(83)
1(0(1(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(35)
0(1(2(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(29)
1(0(1(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(43)
2(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(86)
0(0(1(0(2(x1)))))	→	0(0(2(1(2(x1)))))	(2)

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

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

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.

The 1^st component contains the pair

2^#(1(2(0(2(x1)))))	→	2^#(2(2(1(0(x1)))))	(116)
2^#(1(1(0(2(x1)))))	→	2^#(0(1(0(2(x1)))))	(163)
2^#(1(2(0(2(x1)))))	→	2^#(1(0(2(2(x1)))))	(330)
2^#(1(2(0(2(x1)))))	→	2^#(0(1(2(2(x1)))))	(247)
2^#(1(2(0(2(x1)))))	→	2^#(2(1(0(2(x1)))))	(248)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	x₁ + 11798
[1(x₁)]	=	1144
[2^#(x₁)]	=	x₁ + 0
[0(x₁)]	=	x₁ + 0
[2(x₁)]	=	1143
[1^#(x₁)]	=	x₁ + 1

together with the usable rules

0(0(1(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(18)
1(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(50)
1(1(2(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(80)
0(0(1(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(4)
0(0(1(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(15)
0(0(1(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(8)
1(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(54)
0(0(1(0(2(x1)))))	→	0(0(1(2(2(x1)))))	(1)
1(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(77)
0(0(1(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(3)
0(0(1(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(16)
0(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(21)
1(0(1(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(36)
1(1(2(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(68)
2(0(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(85)
2(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(100)
0(1(2(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(26)
1(1(2(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(63)
0(0(1(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(19)
0(1(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(32)
0(0(1(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(17)
1(0(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(60)
0(1(2(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(27)
2(0(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(87)
2(0(1(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(84)
0(1(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(34)
0(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(22)
0(1(2(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(28)
1(1(2(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(65)
1(0(1(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(44)
0(0(1(0(2(x1)))))	→	0(1(2(0(2(x1)))))	(5)
1(1(2(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(72)
0(1(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(33)
1(1(2(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(64)
2(1(1(0(2(x1)))))	→	2(0(1(0(2(x1)))))	(93)
2(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(92)
0(0(1(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(10)
1(0(1(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(39)
0(0(1(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(7)
2(0(1(0(2(x1)))))	→	2(1(2(2(0(x1)))))	(88)
0(0(1(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(20)
0(1(2(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(25)
1(0(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(49)
1(0(1(0(2(x1)))))	→	2(1(2(2(0(x1)))))	(52)
0(1(2(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(30)
1(0(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(62)
0(0(1(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(14)
1(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(82)
2(0(1(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(89)
1(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(56)
1(1(2(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(79)
0(1(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(31)
0(0(1(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(12)
1(1(2(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(69)
2(1(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(96)
1(0(1(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(45)
1(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(78)
1(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(81)
0(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(23)
1(1(2(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(70)
0(1(2(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(24)
2(1(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(94)
1(1(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(76)
1(0(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(57)
2(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(98)
0(0(1(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(11)
0(0(1(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(9)
0(0(1(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(13)
1(0(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(51)
2(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(90)
1(0(1(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(40)
1(1(2(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(67)
1(0(1(0(2(x1)))))	→	2(2(1(2(0(x1)))))	(55)
1(0(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(59)
0(0(1(0(2(x1)))))	→	0(1(2(2(0(x1)))))	(6)
1(0(1(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(38)
1(0(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(61)
1(0(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(58)
1(1(2(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(74)
1(1(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(75)
1(0(1(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(48)
1(1(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(71)
1(0(1(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(53)
1(0(1(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(47)
1(1(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(73)
2(0(1(0(2(x1)))))	→	2(2(1(2(0(x1)))))	(91)
2(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(97)
2(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(99)
1(0(1(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(37)
1(0(1(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(41)
2(1(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(95)
1(0(1(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(42)
1(0(1(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(46)
1(1(2(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(66)
1(2(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(83)
1(0(1(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(35)
0(1(2(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(29)
1(0(1(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(43)
2(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(86)
0(0(1(0(2(x1)))))	→	0(0(2(1(2(x1)))))	(2)

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

2^#(1(2(0(2(x1)))))	→	2^#(2(2(1(0(x1)))))	(116)
2^#(1(2(0(2(x1)))))	→	2^#(2(1(0(2(x1)))))	(248)

could be deleted.

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

2^#(1(1(0(2(x1)))))	→	2^#(0(1(0(2(x1)))))	(163)
2^#(1(2(0(2(x1)))))	→	2^#(1(0(2(2(x1)))))	(330)
2^#(1(2(0(2(x1)))))	→	2^#(0(1(2(2(x1)))))	(247)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(2^#)

in combination with the following Weighted Path Order with the following precedence and status

prec(0^#)	=	0	status(0^#)	=	[]	list-extension(0^#)	=	Lex
prec(1)	=	1	status(1)	=	[]	list-extension(1)	=	Lex
prec(0)	=	0	status(0)	=	[]	list-extension(0)	=	Lex
prec(2)	=	2	status(2)	=	[]	list-extension(2)	=	Lex
prec(1^#)	=	0	status(1^#)	=	[]	list-extension(1^#)	=	Lex

and the following Max-polynomial interpretation

[0^#(x₁)]	=	1
[1(x₁)]	=	x₁ + 59069
[0(x₁)]	=	x₁ + 59069
[2(x₁)]	=	x₁ + 29534
[1^#(x₁)]	=	1

together with the usable rules

0(0(1(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(18)
1(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(50)
1(1(2(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(80)
0(0(1(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(4)
0(0(1(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(15)
0(0(1(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(8)
1(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(54)
0(0(1(0(2(x1)))))	→	0(0(1(2(2(x1)))))	(1)
1(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(77)
0(0(1(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(3)
0(0(1(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(16)
0(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(21)
1(0(1(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(36)
1(1(2(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(68)
2(0(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(85)
2(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(100)
0(1(2(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(26)
1(1(2(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(63)
0(0(1(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(19)
0(1(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(32)
0(0(1(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(17)
1(0(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(60)
0(1(2(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(27)
2(0(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(87)
2(0(1(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(84)
0(1(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(34)
0(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(22)
0(1(2(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(28)
1(1(2(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(65)
1(0(1(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(44)
0(0(1(0(2(x1)))))	→	0(1(2(0(2(x1)))))	(5)
1(1(2(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(72)
0(1(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(33)
1(1(2(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(64)
2(1(1(0(2(x1)))))	→	2(0(1(0(2(x1)))))	(93)
2(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(92)
0(0(1(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(10)
1(0(1(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(39)
0(0(1(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(7)
2(0(1(0(2(x1)))))	→	2(1(2(2(0(x1)))))	(88)
0(0(1(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(20)
0(1(2(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(25)
1(0(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(49)
1(0(1(0(2(x1)))))	→	2(1(2(2(0(x1)))))	(52)
0(1(2(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(30)
1(0(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(62)
0(0(1(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(14)
1(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(82)
2(0(1(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(89)
1(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(56)
1(1(2(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(79)
0(1(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(31)
0(0(1(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(12)
1(1(2(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(69)
2(1(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(96)
1(0(1(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(45)
1(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(78)
1(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(81)
0(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(23)
1(1(2(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(70)
0(1(2(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(24)
2(1(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(94)
1(1(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(76)
1(0(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(57)
2(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(98)
0(0(1(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(11)
0(0(1(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(9)
0(0(1(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(13)
1(0(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(51)
2(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(90)
1(0(1(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(40)
1(1(2(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(67)
1(0(1(0(2(x1)))))	→	2(2(1(2(0(x1)))))	(55)
1(0(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(59)
0(0(1(0(2(x1)))))	→	0(1(2(2(0(x1)))))	(6)
1(0(1(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(38)
1(0(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(61)
1(0(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(58)
1(1(2(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(74)
1(1(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(75)
1(0(1(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(48)
1(1(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(71)
1(0(1(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(53)
1(0(1(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(47)
1(1(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(73)
2(0(1(0(2(x1)))))	→	2(2(1(2(0(x1)))))	(91)
2(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(97)
2(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(99)
1(0(1(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(37)
1(0(1(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(41)
2(1(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(95)
1(0(1(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(42)
1(0(1(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(46)
1(1(2(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(66)
1(2(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(83)
1(0(1(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(35)
0(1(2(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(29)
1(0(1(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(43)
2(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(86)
0(0(1(0(2(x1)))))	→	0(0(2(1(2(x1)))))	(2)

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

2^#(1(1(0(2(x1)))))	→	2^#(0(1(0(2(x1)))))	(163)
2^#(1(2(0(2(x1)))))	→	2^#(0(1(2(2(x1)))))	(247)

could be deleted.

1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

2^#(1(2(0(2(x1)))))

→

2^#(1(0(2(2(x1)))))

(330)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(2^#)

in combination with the following Weighted Path Order with the following precedence and status

prec(0^#)	=	0	status(0^#)	=	[]	list-extension(0^#)	=	Lex
prec(1)	=	2	status(1)	=	[1]	list-extension(1)	=	Lex
prec(0)	=	0	status(0)	=	[]	list-extension(0)	=	Lex
prec(2)	=	1	status(2)	=	[1]	list-extension(2)	=	Lex
prec(1^#)	=	0	status(1^#)	=	[]	list-extension(1^#)	=	Lex

and the following Max-polynomial interpretation

[0^#(x₁)]	=	1
[1(x₁)]	=	x₁ + 27376
[0(x₁)]	=	x₁ + 27376
[2(x₁)]	=	x₁ + 0
[1^#(x₁)]	=	1

together with the usable rules

0(0(1(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(18)
1(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(50)
1(1(2(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(80)
0(0(1(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(4)
0(0(1(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(15)
0(0(1(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(8)
1(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(54)
0(0(1(0(2(x1)))))	→	0(0(1(2(2(x1)))))	(1)
1(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(77)
0(0(1(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(3)
0(0(1(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(16)
0(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(21)
1(0(1(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(36)
1(1(2(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(68)
2(0(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(85)
2(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(100)
0(1(2(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(26)
1(1(2(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(63)
0(0(1(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(19)
0(1(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(32)
0(0(1(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(17)
1(0(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(60)
0(1(2(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(27)
2(0(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(87)
2(0(1(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(84)
0(1(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(34)
0(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(22)
0(1(2(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(28)
1(1(2(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(65)
1(0(1(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(44)
0(0(1(0(2(x1)))))	→	0(1(2(0(2(x1)))))	(5)
1(1(2(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(72)
0(1(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(33)
1(1(2(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(64)
2(1(1(0(2(x1)))))	→	2(0(1(0(2(x1)))))	(93)
2(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(92)
0(0(1(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(10)
1(0(1(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(39)
0(0(1(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(7)
2(0(1(0(2(x1)))))	→	2(1(2(2(0(x1)))))	(88)
0(0(1(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(20)
0(1(2(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(25)
1(0(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(49)
1(0(1(0(2(x1)))))	→	2(1(2(2(0(x1)))))	(52)
0(1(2(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(30)
1(0(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(62)
0(0(1(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(14)
1(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(82)
2(0(1(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(89)
1(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(56)
1(1(2(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(79)
0(1(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(31)
0(0(1(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(12)
1(1(2(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(69)
2(1(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(96)
1(0(1(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(45)
1(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(78)
1(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(81)
0(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(23)
1(1(2(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(70)
0(1(2(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(24)
2(1(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(94)
1(1(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(76)
1(0(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(57)
2(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(98)
0(0(1(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(11)
0(0(1(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(9)
0(0(1(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(13)
1(0(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(51)
2(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(90)
1(0(1(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(40)
1(1(2(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(67)
1(0(1(0(2(x1)))))	→	2(2(1(2(0(x1)))))	(55)
1(0(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(59)
0(0(1(0(2(x1)))))	→	0(1(2(2(0(x1)))))	(6)
1(0(1(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(38)
1(0(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(61)
1(0(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(58)
1(1(2(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(74)
1(1(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(75)
1(0(1(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(48)
1(1(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(71)
1(0(1(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(53)
1(0(1(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(47)
1(1(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(73)
2(0(1(0(2(x1)))))	→	2(2(1(2(0(x1)))))	(91)
2(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(97)
2(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(99)
1(0(1(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(37)
1(0(1(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(41)
2(1(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(95)
1(0(1(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(42)
1(0(1(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(46)
1(1(2(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(66)
1(2(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(83)
1(0(1(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(35)
0(1(2(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(29)
1(0(1(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(43)
2(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(86)
0(0(1(0(2(x1)))))	→	0(0(2(1(2(x1)))))	(2)

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

2^#(1(2(0(2(x1)))))

→

2^#(1(0(2(2(x1)))))

(330)

could be deleted.

1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 2^nd component contains the pair

1^#(1(2(0(2(x1)))))	→	1^#(0(2(0(2(x1)))))	(244)
1^#(1(2(0(2(x1)))))	→	1^#(1(0(2(2(x1)))))	(313)
1^#(1(2(0(2(x1)))))	→	1^#(0(2(1(2(x1)))))	(113)
1^#(1(2(0(2(x1)))))	→	1^#(0(2(2(0(x1)))))	(205)
1^#(1(2(0(2(x1)))))	→	1^#(0(1(2(2(x1)))))	(238)
1^#(1(2(0(2(x1)))))	→	1^#(2(1(0(2(x1)))))	(296)
1^#(1(2(0(2(x1)))))	→	1^#(0(0(2(2(x1)))))	(334)
1^#(2(2(0(2(x1)))))	→	1^#(0(2(2(2(x1)))))	(286)

1.1.1.1.2 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	11798
[1(x₁)]	=	43325
[2^#(x₁)]	=	0
[0(x₁)]	=	x₁ + 0
[2(x₁)]	=	43324
[1^#(x₁)]	=	x₁ + 1

together with the usable rules

0(0(1(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(18)
1(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(50)
1(1(2(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(80)
0(0(1(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(4)
0(0(1(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(15)
0(0(1(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(8)
1(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(54)
0(0(1(0(2(x1)))))	→	0(0(1(2(2(x1)))))	(1)
1(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(77)
0(0(1(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(3)
0(0(1(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(16)
0(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(21)
1(0(1(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(36)
1(1(2(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(68)
2(0(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(85)
2(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(100)
0(1(2(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(26)
1(1(2(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(63)
0(0(1(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(19)
0(1(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(32)
0(0(1(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(17)
1(0(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(60)
0(1(2(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(27)
2(0(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(87)
2(0(1(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(84)
0(1(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(34)
0(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(22)
0(1(2(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(28)
1(1(2(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(65)
1(0(1(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(44)
0(0(1(0(2(x1)))))	→	0(1(2(0(2(x1)))))	(5)
1(1(2(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(72)
0(1(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(33)
1(1(2(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(64)
2(1(1(0(2(x1)))))	→	2(0(1(0(2(x1)))))	(93)
2(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(92)
0(0(1(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(10)
1(0(1(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(39)
0(0(1(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(7)
2(0(1(0(2(x1)))))	→	2(1(2(2(0(x1)))))	(88)
0(0(1(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(20)
0(1(2(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(25)
1(0(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(49)
1(0(1(0(2(x1)))))	→	2(1(2(2(0(x1)))))	(52)
0(1(2(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(30)
1(0(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(62)
0(0(1(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(14)
1(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(82)
2(0(1(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(89)
1(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(56)
1(1(2(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(79)
0(1(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(31)
0(0(1(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(12)
1(1(2(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(69)
2(1(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(96)
1(0(1(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(45)
1(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(78)
1(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(81)
0(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(23)
1(1(2(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(70)
0(1(2(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(24)
2(1(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(94)
1(1(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(76)
1(0(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(57)
2(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(98)
0(0(1(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(11)
0(0(1(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(9)
0(0(1(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(13)
1(0(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(51)
2(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(90)
1(0(1(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(40)
1(1(2(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(67)
1(0(1(0(2(x1)))))	→	2(2(1(2(0(x1)))))	(55)
1(0(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(59)
0(0(1(0(2(x1)))))	→	0(1(2(2(0(x1)))))	(6)
1(0(1(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(38)
1(0(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(61)
1(0(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(58)
1(1(2(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(74)
1(1(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(75)
1(0(1(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(48)
1(1(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(71)
1(0(1(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(53)
1(0(1(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(47)
1(1(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(73)
2(0(1(0(2(x1)))))	→	2(2(1(2(0(x1)))))	(91)
2(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(97)
2(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(99)
1(0(1(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(37)
1(0(1(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(41)
2(1(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(95)
1(0(1(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(42)
1(0(1(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(46)
1(1(2(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(66)
1(2(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(83)
1(0(1(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(35)
0(1(2(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(29)
1(0(1(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(43)
2(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(86)
0(0(1(0(2(x1)))))	→	0(0(2(1(2(x1)))))	(2)

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

1^#(1(2(0(2(x1)))))	→	1^#(0(2(0(2(x1)))))	(244)
1^#(1(2(0(2(x1)))))	→	1^#(0(2(1(2(x1)))))	(113)
1^#(1(2(0(2(x1)))))	→	1^#(0(2(2(0(x1)))))	(205)
1^#(1(2(0(2(x1)))))	→	1^#(2(1(0(2(x1)))))	(296)
1^#(1(2(0(2(x1)))))	→	1^#(0(0(2(2(x1)))))	(334)

could be deleted.

1.1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

1^#(1(2(0(2(x1)))))	→	1^#(1(0(2(2(x1)))))	(313)
1^#(1(2(0(2(x1)))))	→	1^#(0(1(2(2(x1)))))	(238)
1^#(2(2(0(2(x1)))))	→	1^#(0(2(2(2(x1)))))	(286)

1.1.1.1.2.1.1 Reduction Pair Processor with Usable Rules

Using the argument filter

π(2^#)

in combination with the following Weighted Path Order with the following precedence and status

prec(0^#)	=	0	status(0^#)	=	[]	list-extension(0^#)	=	Lex
prec(1)	=	2	status(1)	=	[1]	list-extension(1)	=	Lex
prec(0)	=	0	status(0)	=	[]	list-extension(0)	=	Lex
prec(2)	=	1	status(2)	=	[1]	list-extension(2)	=	Lex
prec(1^#)	=	0	status(1^#)	=	[1]	list-extension(1^#)	=	Lex

and the following Max-polynomial interpretation

[0^#(x₁)]	=	1
[1(x₁)]	=	x₁ + 1
[0(x₁)]	=	x₁ + 1
[2(x₁)]	=	x₁ + 0
[1^#(x₁)]	=	x₁ + 1

together with the usable rules

0(0(1(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(18)
1(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(50)
1(1(2(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(80)
0(0(1(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(4)
0(0(1(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(15)
0(0(1(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(8)
1(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(54)
0(0(1(0(2(x1)))))	→	0(0(1(2(2(x1)))))	(1)
1(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(77)
0(0(1(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(3)
0(0(1(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(16)
0(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(21)
1(0(1(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(36)
1(1(2(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(68)
2(0(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(85)
2(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(100)
0(1(2(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(26)
1(1(2(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(63)
0(0(1(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(19)
0(1(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(32)
0(0(1(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(17)
1(0(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(60)
0(1(2(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(27)
2(0(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(87)
2(0(1(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(84)
0(1(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(34)
0(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(22)
0(1(2(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(28)
1(1(2(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(65)
1(0(1(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(44)
0(0(1(0(2(x1)))))	→	0(1(2(0(2(x1)))))	(5)
1(1(2(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(72)
0(1(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(33)
1(1(2(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(64)
2(1(1(0(2(x1)))))	→	2(0(1(0(2(x1)))))	(93)
2(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(92)
0(0(1(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(10)
1(0(1(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(39)
0(0(1(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(7)
2(0(1(0(2(x1)))))	→	2(1(2(2(0(x1)))))	(88)
0(0(1(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(20)
0(1(2(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(25)
1(0(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(49)
1(0(1(0(2(x1)))))	→	2(1(2(2(0(x1)))))	(52)
0(1(2(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(30)
1(0(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(62)
0(0(1(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(14)
1(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(82)
2(0(1(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(89)
1(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(56)
1(1(2(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(79)
0(1(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(31)
0(0(1(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(12)
1(1(2(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(69)
2(1(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(96)
1(0(1(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(45)
1(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(78)
1(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(81)
0(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(23)
1(1(2(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(70)
0(1(2(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(24)
2(1(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(94)
1(1(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(76)
1(0(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(57)
2(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(98)
0(0(1(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(11)
0(0(1(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(9)
0(0(1(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(13)
1(0(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(51)
2(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(90)
1(0(1(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(40)
1(1(2(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(67)
1(0(1(0(2(x1)))))	→	2(2(1(2(0(x1)))))	(55)
1(0(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(59)
0(0(1(0(2(x1)))))	→	0(1(2(2(0(x1)))))	(6)
1(0(1(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(38)
1(0(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(61)
1(0(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(58)
1(1(2(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(74)
1(1(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(75)
1(0(1(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(48)
1(1(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(71)
1(0(1(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(53)
1(0(1(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(47)
1(1(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(73)
2(0(1(0(2(x1)))))	→	2(2(1(2(0(x1)))))	(91)
2(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(97)
2(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(99)
1(0(1(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(37)
1(0(1(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(41)
2(1(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(95)
1(0(1(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(42)
1(0(1(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(46)
1(1(2(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(66)
1(2(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(83)
1(0(1(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(35)
0(1(2(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(29)
1(0(1(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(43)
2(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(86)
0(0(1(0(2(x1)))))	→	0(0(2(1(2(x1)))))	(2)

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

1^#(1(2(0(2(x1)))))	→	1^#(1(0(2(2(x1)))))	(313)
1^#(1(2(0(2(x1)))))	→	1^#(0(1(2(2(x1)))))	(238)
1^#(2(2(0(2(x1)))))	→	1^#(0(2(2(2(x1)))))	(286)

could be deleted.

1.1.1.1.2.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.

The 3^rd component contains the pair

0^#(1(2(0(2(x1)))))	→	0^#(2(1(0(2(x1)))))	(326)
0^#(1(2(0(2(x1)))))	→	0^#(1(1(2(2(x1)))))	(331)
0^#(1(2(0(2(x1)))))	→	0^#(1(0(2(2(x1)))))	(354)
0^#(1(2(0(2(x1)))))	→	0^#(2(2(1(0(x1)))))	(198)

1.1.1.1.3 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	x₁ + 11798
[1(x₁)]	=	13507
[2^#(x₁)]	=	0
[0(x₁)]	=	13507
[2(x₁)]	=	13506
[1^#(x₁)]	=	1

together with the usable rules

0(0(1(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(18)
1(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(50)
1(1(2(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(80)
0(0(1(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(4)
0(0(1(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(15)
0(0(1(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(8)
1(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(54)
0(0(1(0(2(x1)))))	→	0(0(1(2(2(x1)))))	(1)
1(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(77)
0(0(1(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(3)
0(0(1(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(16)
0(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(21)
1(0(1(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(36)
1(1(2(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(68)
2(0(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(85)
2(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(100)
0(1(2(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(26)
1(1(2(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(63)
0(0(1(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(19)
0(1(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(32)
0(0(1(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(17)
1(0(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(60)
0(1(2(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(27)
2(0(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(87)
2(0(1(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(84)
0(1(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(34)
0(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(22)
0(1(2(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(28)
1(1(2(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(65)
1(0(1(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(44)
0(0(1(0(2(x1)))))	→	0(1(2(0(2(x1)))))	(5)
1(1(2(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(72)
0(1(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(33)
1(1(2(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(64)
2(1(1(0(2(x1)))))	→	2(0(1(0(2(x1)))))	(93)
2(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(92)
0(0(1(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(10)
1(0(1(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(39)
0(0(1(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(7)
2(0(1(0(2(x1)))))	→	2(1(2(2(0(x1)))))	(88)
0(0(1(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(20)
0(1(2(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(25)
1(0(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(49)
1(0(1(0(2(x1)))))	→	2(1(2(2(0(x1)))))	(52)
0(1(2(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(30)
1(0(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(62)
0(0(1(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(14)
1(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(82)
2(0(1(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(89)
1(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(56)
1(1(2(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(79)
0(1(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(31)
0(0(1(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(12)
1(1(2(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(69)
2(1(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(96)
1(0(1(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(45)
1(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(78)
1(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(81)
0(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(23)
1(1(2(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(70)
0(1(2(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(24)
2(1(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(94)
1(1(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(76)
1(0(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(57)
2(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(98)
0(0(1(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(11)
0(0(1(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(9)
0(0(1(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(13)
1(0(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(51)
2(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(90)
1(0(1(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(40)
1(1(2(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(67)
1(0(1(0(2(x1)))))	→	2(2(1(2(0(x1)))))	(55)
1(0(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(59)
0(0(1(0(2(x1)))))	→	0(1(2(2(0(x1)))))	(6)
1(0(1(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(38)
1(0(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(61)
1(0(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(58)
1(1(2(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(74)
1(1(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(75)
1(0(1(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(48)
1(1(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(71)
1(0(1(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(53)
1(0(1(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(47)
1(1(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(73)
2(0(1(0(2(x1)))))	→	2(2(1(2(0(x1)))))	(91)
2(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(97)
2(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(99)
1(0(1(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(37)
1(0(1(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(41)
2(1(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(95)
1(0(1(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(42)
1(0(1(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(46)
1(1(2(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(66)
1(2(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(83)
1(0(1(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(35)
0(1(2(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(29)
1(0(1(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(43)
2(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(86)
0(0(1(0(2(x1)))))	→	0(0(2(1(2(x1)))))	(2)

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

0^#(1(2(0(2(x1)))))	→	0^#(2(1(0(2(x1)))))	(326)
0^#(1(2(0(2(x1)))))	→	0^#(2(2(1(0(x1)))))	(198)

could be deleted.

1.1.1.1.3.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

0^#(1(2(0(2(x1)))))	→	0^#(1(1(2(2(x1)))))	(331)
0^#(1(2(0(2(x1)))))	→	0^#(1(0(2(2(x1)))))	(354)

1.1.1.1.3.1.1 Reduction Pair Processor with Usable Rules

Using the matrix interpretations of dimension 2 with strict dimension 1 over the naturals

[0^#(x₁)]

1	0
0	0

· x₁ +

[1(x₁)]

1	0
0	0

· x₁ +

[2^#(x₁)]

[0(x₁)]

1	1
0	0

· x₁ +

[2(x₁)]

1	1
0	0

· x₁ +

[1^#(x₁)]

together with the usable rules

0(0(1(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(18)
1(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(50)
1(1(2(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(80)
0(0(1(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(4)
0(0(1(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(15)
0(0(1(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(8)
1(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(54)
0(0(1(0(2(x1)))))	→	0(0(1(2(2(x1)))))	(1)
1(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(77)
0(0(1(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(3)
0(0(1(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(16)
0(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(21)
1(0(1(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(36)
1(1(2(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(68)
2(0(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(85)
2(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(100)
0(1(2(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(26)
1(1(2(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(63)
0(0(1(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(19)
0(1(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(32)
0(0(1(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(17)
1(0(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(60)
0(1(2(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(27)
2(0(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(87)
2(0(1(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(84)
0(1(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(34)
0(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(22)
0(1(2(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(28)
1(1(2(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(65)
1(0(1(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(44)
0(0(1(0(2(x1)))))	→	0(1(2(0(2(x1)))))	(5)
1(1(2(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(72)
0(1(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(33)
1(1(2(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(64)
2(1(1(0(2(x1)))))	→	2(0(1(0(2(x1)))))	(93)
2(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(92)
0(0(1(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(10)
1(0(1(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(39)
0(0(1(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(7)
2(0(1(0(2(x1)))))	→	2(1(2(2(0(x1)))))	(88)
0(0(1(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(20)
0(1(2(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(25)
1(0(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(49)
1(0(1(0(2(x1)))))	→	2(1(2(2(0(x1)))))	(52)
0(1(2(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(30)
1(0(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(62)
0(0(1(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(14)
1(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(82)
2(0(1(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(89)
1(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(56)
1(1(2(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(79)
0(1(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(31)
0(0(1(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(12)
1(1(2(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(69)
2(1(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(96)
1(0(1(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(45)
1(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(78)
1(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(81)
0(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(23)
1(1(2(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(70)
0(1(2(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(24)
2(1(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(94)
1(1(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(76)
1(0(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(57)
2(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(98)
0(0(1(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(11)
0(0(1(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(9)
0(0(1(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(13)
1(0(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(51)
2(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(90)
1(0(1(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(40)
1(1(2(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(67)
1(0(1(0(2(x1)))))	→	2(2(1(2(0(x1)))))	(55)
1(0(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(59)
0(0(1(0(2(x1)))))	→	0(1(2(2(0(x1)))))	(6)
1(0(1(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(38)
1(0(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(61)
1(0(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(58)
1(1(2(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(74)
1(1(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(75)
1(0(1(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(48)
1(1(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(71)
1(0(1(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(53)
1(0(1(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(47)
1(1(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(73)
2(0(1(0(2(x1)))))	→	2(2(1(2(0(x1)))))	(91)
2(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(97)
2(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(99)
1(0(1(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(37)
1(0(1(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(41)
2(1(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(95)
1(0(1(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(42)
1(0(1(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(46)
1(1(2(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(66)
1(2(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(83)
1(0(1(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(35)
0(1(2(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(29)
1(0(1(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(43)
2(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(86)
0(0(1(0(2(x1)))))	→	0(0(2(1(2(x1)))))	(2)

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

0^#(1(2(0(2(x1)))))

→

0^#(1(0(2(2(x1)))))

(354)

could be deleted.

1.1.1.1.3.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

0^#(1(2(0(2(x1)))))

→

0^#(1(1(2(2(x1)))))

(331)

1.1.1.1.3.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the matrix interpretations of dimension 2 with strict dimension 1 over the naturals

[0^#(x₁)]

0	1
0	0

· x₁ +

[1(x₁)]

0	0
0	1

· x₁ +

28146

[2^#(x₁)]

[0(x₁)]

0	0
0	1

· x₁ +

28146

[2(x₁)]

0	0
1	1

· x₁ +

28145

[1^#(x₁)]

together with the usable rules

0(0(1(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(18)
1(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(50)
1(1(2(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(80)
0(0(1(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(4)
0(0(1(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(15)
0(0(1(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(8)
1(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(54)
0(0(1(0(2(x1)))))	→	0(0(1(2(2(x1)))))	(1)
1(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(77)
0(0(1(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(3)
0(0(1(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(16)
0(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(21)
1(0(1(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(36)
1(1(2(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(68)
2(0(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(85)
2(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(100)
0(1(2(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(26)
1(1(2(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(63)
0(0(1(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(19)
0(1(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(32)
0(0(1(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(17)
1(0(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(60)
0(1(2(0(2(x1)))))	→	0(2(1(0(2(x1)))))	(27)
2(0(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(87)
2(0(1(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(84)
0(1(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(34)
0(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(22)
0(1(2(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(28)
1(1(2(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(65)
1(0(1(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(44)
0(0(1(0(2(x1)))))	→	0(1(2(0(2(x1)))))	(5)
1(1(2(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(72)
0(1(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(33)
1(1(2(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(64)
2(1(1(0(2(x1)))))	→	2(0(1(0(2(x1)))))	(93)
2(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(92)
0(0(1(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(10)
1(0(1(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(39)
0(0(1(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(7)
2(0(1(0(2(x1)))))	→	2(1(2(2(0(x1)))))	(88)
0(0(1(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(20)
0(1(2(0(2(x1)))))	→	0(1(1(2(2(x1)))))	(25)
1(0(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(49)
1(0(1(0(2(x1)))))	→	2(1(2(2(0(x1)))))	(52)
0(1(2(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(30)
1(0(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(62)
0(0(1(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(14)
1(1(2(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(82)
2(0(1(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(89)
1(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(56)
1(1(2(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(79)
0(1(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(31)
0(0(1(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(12)
1(1(2(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(69)
2(1(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(96)
1(0(1(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(45)
1(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(78)
1(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(81)
0(0(1(0(2(x1)))))	→	2(2(2(1(0(x1)))))	(23)
1(1(2(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(70)
0(1(2(0(2(x1)))))	→	0(1(0(2(2(x1)))))	(24)
2(1(1(0(2(x1)))))	→	2(0(2(1(2(x1)))))	(94)
1(1(2(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(76)
1(0(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(57)
2(1(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(98)
0(0(1(0(2(x1)))))	→	0(2(2(1(2(x1)))))	(11)
0(0(1(0(2(x1)))))	→	0(2(1(2(2(x1)))))	(9)
0(0(1(0(2(x1)))))	→	1(0(2(0(2(x1)))))	(13)
1(0(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(51)
2(0(1(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(90)
1(0(1(0(2(x1)))))	→	1(0(2(1(2(x1)))))	(40)
1(1(2(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(67)
1(0(1(0(2(x1)))))	→	2(2(1(2(0(x1)))))	(55)
1(0(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(59)
0(0(1(0(2(x1)))))	→	0(1(2(2(0(x1)))))	(6)
1(0(1(0(2(x1)))))	→	1(0(1(2(2(x1)))))	(38)
1(0(2(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(61)
1(0(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(58)
1(1(2(0(2(x1)))))	→	1(2(1(0(2(x1)))))	(74)
1(1(2(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(75)
1(0(1(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(48)
1(1(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(71)
1(0(1(0(2(x1)))))	→	2(2(0(1(2(x1)))))	(53)
1(0(1(0(2(x1)))))	→	1(2(2(2(0(x1)))))	(47)
1(1(2(0(2(x1)))))	→	1(2(0(2(2(x1)))))	(73)
2(0(1(0(2(x1)))))	→	2(2(1(2(0(x1)))))	(91)
2(1(2(0(2(x1)))))	→	2(0(1(2(2(x1)))))	(97)
2(1(2(0(2(x1)))))	→	2(2(1(0(2(x1)))))	(99)
1(0(1(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(37)
1(0(1(0(2(x1)))))	→	1(0(2(2(0(x1)))))	(41)
2(1(1(0(2(x1)))))	→	2(1(2(0(2(x1)))))	(95)
1(0(1(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(42)
1(0(1(0(2(x1)))))	→	1(2(2(0(2(x1)))))	(46)
1(1(2(0(2(x1)))))	→	1(0(0(2(2(x1)))))	(66)
1(2(2(0(2(x1)))))	→	1(0(2(2(2(x1)))))	(83)
1(0(1(0(2(x1)))))	→	0(1(2(2(2(x1)))))	(35)
0(1(2(0(2(x1)))))	→	0(2(2(1(0(x1)))))	(29)
1(0(1(0(2(x1)))))	→	1(1(0(2(2(x1)))))	(43)
2(0(1(0(2(x1)))))	→	2(1(0(2(2(x1)))))	(86)
0(0(1(0(2(x1)))))	→	0(0(2(1(2(x1)))))	(2)

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

0^#(1(2(0(2(x1)))))

→

0^#(1(1(2(2(x1)))))

(331)

could be deleted.

1.1.1.1.3.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.