Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/4970)

The rewrite relation of the following TRS is considered.

5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)
2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

There are 166 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

5^#(5(x1))	→	5^#(4(0(2(5(4(5(2(1(x1)))))))))	(114)
5^#(5(3(x1)))	→	0^#(x1)	(187)
5^#(2(5(5(0(4(x1))))))	→	4^#(4(x1))	(112)
4^#(4(5(2(4(2(2(x1)))))))	→	2^#(2(1(x1)))	(113)
5^#(5(x1))	→	4^#(0(2(5(4(5(2(1(x1))))))))	(111)
4^#(4(5(2(4(2(2(x1)))))))	→	5^#(4(5(1(2(2(1(x1)))))))	(184)
5^#(5(5(1(4(x1)))))	→	0^#(x1)	(110)
4^#(4(5(2(4(2(2(x1)))))))	→	5^#(5(4(5(1(2(2(1(x1))))))))	(182)
4^#(4(5(2(4(2(2(x1)))))))	→	5^#(1(2(2(1(x1)))))	(105)
4^#(4(5(2(4(2(2(x1)))))))	→	0^#(5(5(4(5(1(2(2(1(x1)))))))))	(181)
2^#(5(0(4(x1))))	→	0^#(0(x1))	(180)
5^#(5(3(x1)))	→	0^#(1(5(0(x1))))	(179)
5^#(5(x1))	→	5^#(4(5(2(1(x1)))))	(101)
0^#(1(5(5(5(3(5(x1)))))))	→	5^#(1(0(1(2(0(5(x1)))))))	(99)
5^#(2(5(5(0(4(x1))))))	→	2^#(1(4(4(x1))))	(97)
2^#(5(5(x1)))	→	4^#(4(0(0(1(1(2(x1)))))))	(178)
5^#(5(3(x1)))	→	4^#(4(1(0(1(5(0(x1)))))))	(95)
2^#(5(0(4(x1))))	→	4^#(4(5(1(0(0(x1))))))	(177)
4^#(4(5(2(4(2(2(x1)))))))	→	4^#(0(5(5(4(5(1(2(2(1(x1))))))))))	(94)
5^#(5(5(x1)))	→	0^#(0(x1))	(93)
5^#(5(x1))	→	0^#(4(x1))	(175)
5^#(5(2(4(5(0(x1))))))	→	2^#(4(0(4(2(0(x1))))))	(92)
2^#(5(5(3(4(x1)))))	→	2^#(4(4(x1)))	(91)
4^#(5(5(5(x1))))	→	0^#(5(x1))	(90)
2^#(5(5(x1)))	→	0^#(1(1(2(x1))))	(172)
2^#(5(5(x1)))	→	4^#(2(5(4(4(0(0(1(1(2(x1))))))))))	(89)
2^#(5(0(4(x1))))	→	2^#(4(4(5(1(0(0(x1)))))))	(171)
5^#(5(x1))	→	0^#(5(4(0(2(5(4(5(2(1(x1))))))))))	(87)
5^#(5(x1))	→	4^#(1(1(1(1(4(4(0(4(x1)))))))))	(170)
5^#(5(5(1(4(x1)))))	→	4^#(4(0(x1)))	(86)
5^#(5(5(x1)))	→	0^#(x1)	(85)
5^#(2(4(x1)))	→	2^#(x1)	(168)
5^#(5(x1))	→	4^#(5(2(1(x1))))	(84)
5^#(5(5(1(4(x1)))))	→	4^#(0(x1))	(83)
4^#(4(5(2(4(2(2(x1)))))))	→	2^#(1(x1))	(81)
4^#(5(5(5(x1))))	→	2^#(1(0(5(x1))))	(80)
5^#(5(x1))	→	0^#(2(5(4(5(2(1(x1)))))))	(163)
5^#(2(4(x1)))	→	4^#(2(4(2(x1))))	(78)
5^#(5(5(x1)))	→	5^#(0(0(x1)))	(162)
2^#(5(5(x1)))	→	4^#(0(0(1(1(2(x1))))))	(161)
5^#(5(2(4(5(0(x1))))))	→	2^#(0(x1))	(159)
5^#(5(2(4(5(0(x1))))))	→	0^#(4(2(0(x1))))	(77)
4^#(4(5(2(4(2(2(x1)))))))	→	4^#(5(1(2(2(1(x1))))))	(157)
4^#(5(2(4(x1))))	→	4^#(1(5(5(2(0(3(1(3(3(x1))))))))))	(158)
5^#(5(3(x1)))	→	5^#(4(4(1(0(1(5(0(x1))))))))	(76)
5^#(5(x1))	→	4^#(x1)	(75)
5^#(5(x1))	→	5^#(2(1(x1)))	(156)
5^#(5(3(x1)))	→	4^#(1(0(1(5(0(x1))))))	(74)
5^#(5(5(x1)))	→	4^#(1(0(1(4(5(0(0(x1))))))))	(155)
2^#(5(0(4(x1))))	→	0^#(x1)	(71)
2^#(5(0(4(x1))))	→	5^#(1(0(0(x1))))	(153)
4^#(2(5(5(1(5(x1))))))	→	4^#(2(5(x1)))	(70)
5^#(5(3(x1)))	→	5^#(0(x1))	(150)
5^#(5(5(x1)))	→	4^#(5(0(0(x1))))	(68)
5^#(5(x1))	→	2^#(5(4(5(2(1(x1))))))	(66)
0^#(1(5(5(5(3(5(x1)))))))	→	2^#(5(1(0(1(2(0(5(x1))))))))	(67)
0^#(1(5(5(5(3(5(x1)))))))	→	2^#(0(5(x1)))	(148)
5^#(5(x1))	→	4^#(4(0(4(x1))))	(62)
2^#(5(0(4(x1))))	→	4^#(5(1(0(0(x1)))))	(145)
5^#(2(4(x1)))	→	2^#(4(2(x1)))	(141)
5^#(2(4(x1)))	→	4^#(2(x1))	(55)
0^#(1(5(5(5(3(5(x1)))))))	→	0^#(5(x1))	(56)
0^#(1(5(5(5(3(5(x1)))))))	→	0^#(1(2(0(5(x1)))))	(52)
2^#(5(5(x1)))	→	0^#(0(1(1(2(x1)))))	(48)
2^#(5(5(x1)))	→	2^#(x1)	(137)
4^#(5(2(4(x1))))	→	5^#(5(2(0(3(1(3(3(x1))))))))	(135)
5^#(5(5(x1)))	→	0^#(1(4(5(0(0(x1))))))	(133)
2^#(5(5(3(4(x1)))))	→	0^#(2(4(4(x1))))	(132)
4^#(2(5(5(1(5(x1))))))	→	2^#(5(x1))	(40)
2^#(5(5(x1)))	→	5^#(4(4(0(0(1(1(2(x1))))))))	(130)
5^#(5(2(4(5(0(x1))))))	→	4^#(0(4(2(0(x1)))))	(39)
5^#(2(5(5(0(4(x1))))))	→	5^#(2(1(4(4(x1)))))	(38)
5^#(5(2(4(5(0(x1))))))	→	4^#(2(0(x1)))	(37)
2^#(5(5(x1)))	→	2^#(5(4(4(0(0(1(1(2(x1)))))))))	(124)
5^#(5(2(4(5(0(x1))))))	→	4^#(2(4(0(4(2(0(x1)))))))	(33)
5^#(5(2(4(5(0(x1))))))	→	2^#(1(1(4(2(4(0(4(2(0(x1))))))))))	(123)
5^#(5(x1))	→	2^#(1(x1))	(121)
2^#(5(5(3(4(x1)))))	→	4^#(4(x1))	(29)
5^#(5(x1))	→	4^#(0(4(x1)))	(118)
2^#(5(5(3(4(x1)))))	→	4^#(0(2(4(4(x1)))))	(24)

1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)
5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)

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

4^#(4(5(2(4(2(2(x1)))))))	→	5^#(1(2(2(1(x1)))))	(105)
0^#(1(5(5(5(3(5(x1)))))))	→	5^#(1(0(1(2(0(5(x1)))))))	(99)
5^#(5(3(x1)))	→	5^#(4(4(1(0(1(5(0(x1))))))))	(76)
2^#(5(0(4(x1))))	→	5^#(1(0(0(x1))))	(153)

could be deleted.

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

5^#(2(5(5(0(4(x1))))))	→	4^#(4(x1))	(112)
5^#(2(5(5(0(4(x1))))))	→	2^#(1(4(4(x1))))	(97)
5^#(2(5(5(0(4(x1))))))	→	5^#(2(1(4(4(x1)))))	(38)
5^#(2(4(x1)))	→	2^#(x1)	(168)
5^#(2(4(x1)))	→	4^#(2(x1))	(55)
5^#(2(4(x1)))	→	2^#(4(2(x1)))	(141)
5^#(2(4(x1)))	→	4^#(2(4(2(x1))))	(78)
2^#(5(0(4(x1))))	→	0^#(x1)	(71)
2^#(5(0(4(x1))))	→	0^#(0(x1))	(180)
2^#(5(0(4(x1))))	→	4^#(5(1(0(0(x1)))))	(145)
2^#(5(0(4(x1))))	→	4^#(4(5(1(0(0(x1))))))	(177)
2^#(5(0(4(x1))))	→	2^#(4(4(5(1(0(0(x1)))))))	(171)
5^#(5(x1))	→	2^#(1(x1))	(121)
5^#(5(x1))	→	5^#(2(1(x1)))	(156)
5^#(5(x1))	→	4^#(5(2(1(x1))))	(84)
5^#(5(x1))	→	5^#(4(5(2(1(x1)))))	(101)
5^#(5(x1))	→	2^#(5(4(5(2(1(x1))))))	(66)
5^#(5(x1))	→	0^#(2(5(4(5(2(1(x1)))))))	(163)
5^#(5(x1))	→	4^#(0(2(5(4(5(2(1(x1))))))))	(111)
5^#(5(x1))	→	5^#(4(0(2(5(4(5(2(1(x1)))))))))	(114)
5^#(5(x1))	→	0^#(5(4(0(2(5(4(5(2(1(x1))))))))))	(87)
2^#(5(5(x1)))	→	2^#(x1)	(137)
2^#(5(5(x1)))	→	0^#(1(1(2(x1))))	(172)
2^#(5(5(x1)))	→	0^#(0(1(1(2(x1)))))	(48)
2^#(5(5(x1)))	→	4^#(0(0(1(1(2(x1))))))	(161)
2^#(5(5(x1)))	→	4^#(4(0(0(1(1(2(x1)))))))	(178)
2^#(5(5(x1)))	→	5^#(4(4(0(0(1(1(2(x1))))))))	(130)
2^#(5(5(x1)))	→	2^#(5(4(4(0(0(1(1(2(x1)))))))))	(124)
2^#(5(5(x1)))	→	4^#(2(5(4(4(0(0(1(1(2(x1))))))))))	(89)
4^#(4(5(2(4(2(2(x1)))))))	→	2^#(1(x1))	(81)
4^#(4(5(2(4(2(2(x1)))))))	→	2^#(2(1(x1)))	(113)
4^#(4(5(2(4(2(2(x1)))))))	→	4^#(5(1(2(2(1(x1))))))	(157)
4^#(4(5(2(4(2(2(x1)))))))	→	5^#(4(5(1(2(2(1(x1)))))))	(184)
4^#(4(5(2(4(2(2(x1)))))))	→	5^#(5(4(5(1(2(2(1(x1))))))))	(182)
4^#(4(5(2(4(2(2(x1)))))))	→	0^#(5(5(4(5(1(2(2(1(x1)))))))))	(181)
4^#(4(5(2(4(2(2(x1)))))))	→	4^#(0(5(5(4(5(1(2(2(1(x1))))))))))	(94)
5^#(5(2(4(5(0(x1))))))	→	2^#(0(x1))	(159)
5^#(5(2(4(5(0(x1))))))	→	4^#(2(0(x1)))	(37)
5^#(5(2(4(5(0(x1))))))	→	0^#(4(2(0(x1))))	(77)
5^#(5(2(4(5(0(x1))))))	→	4^#(0(4(2(0(x1)))))	(39)
5^#(5(2(4(5(0(x1))))))	→	2^#(4(0(4(2(0(x1))))))	(92)
5^#(5(2(4(5(0(x1))))))	→	4^#(2(4(0(4(2(0(x1)))))))	(33)
5^#(5(2(4(5(0(x1))))))	→	2^#(1(1(4(2(4(0(4(2(0(x1))))))))))	(123)
4^#(2(5(5(1(5(x1))))))	→	2^#(5(x1))	(40)
4^#(2(5(5(1(5(x1))))))	→	4^#(2(5(x1)))	(70)
4^#(5(5(5(x1))))	→	0^#(5(x1))	(90)
4^#(5(5(5(x1))))	→	2^#(1(0(5(x1))))	(80)
5^#(5(5(x1)))	→	0^#(x1)	(85)
5^#(5(5(x1)))	→	0^#(0(x1))	(93)
5^#(5(5(x1)))	→	5^#(0(0(x1)))	(162)
5^#(5(5(x1)))	→	4^#(5(0(0(x1))))	(68)
5^#(5(5(x1)))	→	0^#(1(4(5(0(0(x1))))))	(133)
5^#(5(5(x1)))	→	4^#(1(0(1(4(5(0(0(x1))))))))	(155)
0^#(1(5(5(5(3(5(x1)))))))	→	0^#(5(x1))	(56)
0^#(1(5(5(5(3(5(x1)))))))	→	2^#(0(5(x1)))	(148)
0^#(1(5(5(5(3(5(x1)))))))	→	0^#(1(2(0(5(x1)))))	(52)
0^#(1(5(5(5(3(5(x1)))))))	→	2^#(5(1(0(1(2(0(5(x1))))))))	(67)
2^#(5(5(3(4(x1)))))	→	4^#(4(x1))	(29)
2^#(5(5(3(4(x1)))))	→	2^#(4(4(x1)))	(91)
2^#(5(5(3(4(x1)))))	→	0^#(2(4(4(x1))))	(132)
2^#(5(5(3(4(x1)))))	→	4^#(0(2(4(4(x1)))))	(24)
4^#(5(2(4(x1))))	→	5^#(5(2(0(3(1(3(3(x1))))))))	(135)
4^#(5(2(4(x1))))	→	4^#(1(5(5(2(0(3(1(3(3(x1))))))))))	(158)
5^#(5(5(1(4(x1)))))	→	0^#(x1)	(110)
5^#(5(5(1(4(x1)))))	→	4^#(0(x1))	(83)
5^#(5(5(1(4(x1)))))	→	4^#(4(0(x1)))	(86)
5^#(5(3(x1)))	→	0^#(x1)	(187)
5^#(5(3(x1)))	→	5^#(0(x1))	(150)
5^#(5(3(x1)))	→	0^#(1(5(0(x1))))	(179)
5^#(5(3(x1)))	→	4^#(1(0(1(5(0(x1))))))	(74)
5^#(5(3(x1)))	→	4^#(4(1(0(1(5(0(x1)))))))	(95)
5^#(5(x1))	→	4^#(x1)	(75)
5^#(5(x1))	→	0^#(4(x1))	(175)
5^#(5(x1))	→	4^#(0(4(x1)))	(118)
5^#(5(x1))	→	4^#(4(0(4(x1))))	(62)
5^#(5(x1))	→	4^#(1(1(1(1(4(4(0(4(x1)))))))))	(170)

1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

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

together with the usable rules

5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)
5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)

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

5^#(2(5(5(0(4(x1))))))	→	4^#(4(x1))	(112)
5^#(2(5(5(0(4(x1))))))	→	2^#(1(4(4(x1))))	(97)
5^#(2(5(5(0(4(x1))))))	→	5^#(2(1(4(4(x1)))))	(38)

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

5^#(2(4(x1)))	→	2^#(x1)	(168)
5^#(2(4(x1)))	→	4^#(2(x1))	(55)
5^#(2(4(x1)))	→	2^#(4(2(x1)))	(141)
5^#(2(4(x1)))	→	4^#(2(4(2(x1))))	(78)
2^#(5(0(4(x1))))	→	0^#(x1)	(71)
2^#(5(0(4(x1))))	→	0^#(0(x1))	(180)
2^#(5(0(4(x1))))	→	4^#(5(1(0(0(x1)))))	(145)
2^#(5(0(4(x1))))	→	4^#(4(5(1(0(0(x1))))))	(177)
2^#(5(0(4(x1))))	→	2^#(4(4(5(1(0(0(x1)))))))	(171)
5^#(5(x1))	→	2^#(1(x1))	(121)
5^#(5(x1))	→	5^#(2(1(x1)))	(156)
5^#(5(x1))	→	4^#(5(2(1(x1))))	(84)
5^#(5(x1))	→	5^#(4(5(2(1(x1)))))	(101)
5^#(5(x1))	→	2^#(5(4(5(2(1(x1))))))	(66)
5^#(5(x1))	→	0^#(2(5(4(5(2(1(x1)))))))	(163)
5^#(5(x1))	→	4^#(0(2(5(4(5(2(1(x1))))))))	(111)
5^#(5(x1))	→	5^#(4(0(2(5(4(5(2(1(x1)))))))))	(114)
5^#(5(x1))	→	0^#(5(4(0(2(5(4(5(2(1(x1))))))))))	(87)
2^#(5(5(x1)))	→	2^#(x1)	(137)
2^#(5(5(x1)))	→	0^#(1(1(2(x1))))	(172)
2^#(5(5(x1)))	→	0^#(0(1(1(2(x1)))))	(48)
2^#(5(5(x1)))	→	4^#(0(0(1(1(2(x1))))))	(161)
2^#(5(5(x1)))	→	4^#(4(0(0(1(1(2(x1)))))))	(178)
2^#(5(5(x1)))	→	5^#(4(4(0(0(1(1(2(x1))))))))	(130)
2^#(5(5(x1)))	→	2^#(5(4(4(0(0(1(1(2(x1)))))))))	(124)
2^#(5(5(x1)))	→	4^#(2(5(4(4(0(0(1(1(2(x1))))))))))	(89)
4^#(4(5(2(4(2(2(x1)))))))	→	2^#(1(x1))	(81)
4^#(4(5(2(4(2(2(x1)))))))	→	2^#(2(1(x1)))	(113)
4^#(4(5(2(4(2(2(x1)))))))	→	4^#(5(1(2(2(1(x1))))))	(157)
4^#(4(5(2(4(2(2(x1)))))))	→	5^#(4(5(1(2(2(1(x1)))))))	(184)
4^#(4(5(2(4(2(2(x1)))))))	→	5^#(5(4(5(1(2(2(1(x1))))))))	(182)
4^#(4(5(2(4(2(2(x1)))))))	→	0^#(5(5(4(5(1(2(2(1(x1)))))))))	(181)
4^#(4(5(2(4(2(2(x1)))))))	→	4^#(0(5(5(4(5(1(2(2(1(x1))))))))))	(94)
5^#(5(2(4(5(0(x1))))))	→	2^#(0(x1))	(159)
5^#(5(2(4(5(0(x1))))))	→	4^#(2(0(x1)))	(37)
5^#(5(2(4(5(0(x1))))))	→	0^#(4(2(0(x1))))	(77)
5^#(5(2(4(5(0(x1))))))	→	4^#(0(4(2(0(x1)))))	(39)
5^#(5(2(4(5(0(x1))))))	→	2^#(4(0(4(2(0(x1))))))	(92)
5^#(5(2(4(5(0(x1))))))	→	4^#(2(4(0(4(2(0(x1)))))))	(33)
5^#(5(2(4(5(0(x1))))))	→	2^#(1(1(4(2(4(0(4(2(0(x1))))))))))	(123)
4^#(2(5(5(1(5(x1))))))	→	2^#(5(x1))	(40)
4^#(2(5(5(1(5(x1))))))	→	4^#(2(5(x1)))	(70)
4^#(5(5(5(x1))))	→	0^#(5(x1))	(90)
4^#(5(5(5(x1))))	→	2^#(1(0(5(x1))))	(80)
5^#(5(5(x1)))	→	0^#(x1)	(85)
5^#(5(5(x1)))	→	0^#(0(x1))	(93)
5^#(5(5(x1)))	→	5^#(0(0(x1)))	(162)
5^#(5(5(x1)))	→	4^#(5(0(0(x1))))	(68)
5^#(5(5(x1)))	→	0^#(1(4(5(0(0(x1))))))	(133)
5^#(5(5(x1)))	→	4^#(1(0(1(4(5(0(0(x1))))))))	(155)
0^#(1(5(5(5(3(5(x1)))))))	→	0^#(5(x1))	(56)
0^#(1(5(5(5(3(5(x1)))))))	→	2^#(0(5(x1)))	(148)
0^#(1(5(5(5(3(5(x1)))))))	→	0^#(1(2(0(5(x1)))))	(52)
0^#(1(5(5(5(3(5(x1)))))))	→	2^#(5(1(0(1(2(0(5(x1))))))))	(67)
2^#(5(5(3(4(x1)))))	→	4^#(4(x1))	(29)
2^#(5(5(3(4(x1)))))	→	2^#(4(4(x1)))	(91)
2^#(5(5(3(4(x1)))))	→	0^#(2(4(4(x1))))	(132)
2^#(5(5(3(4(x1)))))	→	4^#(0(2(4(4(x1)))))	(24)
4^#(5(2(4(x1))))	→	5^#(5(2(0(3(1(3(3(x1))))))))	(135)
4^#(5(2(4(x1))))	→	4^#(1(5(5(2(0(3(1(3(3(x1))))))))))	(158)
5^#(5(5(1(4(x1)))))	→	0^#(x1)	(110)
5^#(5(5(1(4(x1)))))	→	4^#(0(x1))	(83)
5^#(5(5(1(4(x1)))))	→	4^#(4(0(x1)))	(86)
5^#(5(3(x1)))	→	0^#(x1)	(187)
5^#(5(3(x1)))	→	5^#(0(x1))	(150)
5^#(5(3(x1)))	→	0^#(1(5(0(x1))))	(179)
5^#(5(3(x1)))	→	4^#(1(0(1(5(0(x1))))))	(74)
5^#(5(3(x1)))	→	4^#(4(1(0(1(5(0(x1)))))))	(95)
5^#(5(x1))	→	4^#(x1)	(75)
5^#(5(x1))	→	0^#(4(x1))	(175)
5^#(5(x1))	→	4^#(0(4(x1)))	(118)
5^#(5(x1))	→	4^#(4(0(4(x1))))	(62)
5^#(5(x1))	→	4^#(1(1(1(1(4(4(0(4(x1)))))))))	(170)

1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	42513
[1(x₁)]	=	0
[4(x₁)]	=	21257
[5(x₁)]	=	42513
[3(x₁)]	=	0
[2^#(x₁)]	=	42513
[4^#(x₁)]	=	42513
[0(x₁)]	=	42513
[5^#(x₁)]	=	x₁ + 0
[2(x₁)]	=	x₁ + 21257
[1^#(x₁)]	=	0

together with the usable rules

5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)
5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)

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

5^#(2(4(x1)))	→	2^#(x1)	(168)
5^#(2(4(x1)))	→	4^#(2(x1))	(55)
5^#(2(4(x1)))	→	2^#(4(2(x1)))	(141)
5^#(2(4(x1)))	→	4^#(2(4(2(x1))))	(78)
5^#(5(x1))	→	5^#(2(1(x1)))	(156)
5^#(5(x1))	→	5^#(4(5(2(1(x1)))))	(101)
5^#(5(x1))	→	5^#(4(0(2(5(4(5(2(1(x1)))))))))	(114)
2^#(5(5(x1)))	→	5^#(4(4(0(0(1(1(2(x1))))))))	(130)
4^#(4(5(2(4(2(2(x1)))))))	→	5^#(4(5(1(2(2(1(x1)))))))	(184)

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^#(5(0(4(x1))))	→	0^#(x1)	(71)
2^#(5(0(4(x1))))	→	0^#(0(x1))	(180)
2^#(5(0(4(x1))))	→	4^#(5(1(0(0(x1)))))	(145)
2^#(5(0(4(x1))))	→	4^#(4(5(1(0(0(x1))))))	(177)
2^#(5(0(4(x1))))	→	2^#(4(4(5(1(0(0(x1)))))))	(171)
5^#(5(x1))	→	2^#(1(x1))	(121)
5^#(5(x1))	→	4^#(5(2(1(x1))))	(84)
5^#(5(x1))	→	2^#(5(4(5(2(1(x1))))))	(66)
5^#(5(x1))	→	0^#(2(5(4(5(2(1(x1)))))))	(163)
5^#(5(x1))	→	4^#(0(2(5(4(5(2(1(x1))))))))	(111)
5^#(5(x1))	→	0^#(5(4(0(2(5(4(5(2(1(x1))))))))))	(87)
2^#(5(5(x1)))	→	2^#(x1)	(137)
2^#(5(5(x1)))	→	0^#(1(1(2(x1))))	(172)
2^#(5(5(x1)))	→	0^#(0(1(1(2(x1)))))	(48)
2^#(5(5(x1)))	→	4^#(0(0(1(1(2(x1))))))	(161)
2^#(5(5(x1)))	→	4^#(4(0(0(1(1(2(x1)))))))	(178)
2^#(5(5(x1)))	→	2^#(5(4(4(0(0(1(1(2(x1)))))))))	(124)
2^#(5(5(x1)))	→	4^#(2(5(4(4(0(0(1(1(2(x1))))))))))	(89)
4^#(4(5(2(4(2(2(x1)))))))	→	2^#(1(x1))	(81)
4^#(4(5(2(4(2(2(x1)))))))	→	2^#(2(1(x1)))	(113)
4^#(4(5(2(4(2(2(x1)))))))	→	4^#(5(1(2(2(1(x1))))))	(157)
4^#(4(5(2(4(2(2(x1)))))))	→	5^#(5(4(5(1(2(2(1(x1))))))))	(182)
4^#(4(5(2(4(2(2(x1)))))))	→	0^#(5(5(4(5(1(2(2(1(x1)))))))))	(181)
4^#(4(5(2(4(2(2(x1)))))))	→	4^#(0(5(5(4(5(1(2(2(1(x1))))))))))	(94)
5^#(5(2(4(5(0(x1))))))	→	2^#(0(x1))	(159)
5^#(5(2(4(5(0(x1))))))	→	4^#(2(0(x1)))	(37)
5^#(5(2(4(5(0(x1))))))	→	0^#(4(2(0(x1))))	(77)
5^#(5(2(4(5(0(x1))))))	→	4^#(0(4(2(0(x1)))))	(39)
5^#(5(2(4(5(0(x1))))))	→	2^#(4(0(4(2(0(x1))))))	(92)
5^#(5(2(4(5(0(x1))))))	→	4^#(2(4(0(4(2(0(x1)))))))	(33)
5^#(5(2(4(5(0(x1))))))	→	2^#(1(1(4(2(4(0(4(2(0(x1))))))))))	(123)
4^#(2(5(5(1(5(x1))))))	→	2^#(5(x1))	(40)
4^#(2(5(5(1(5(x1))))))	→	4^#(2(5(x1)))	(70)
4^#(5(5(5(x1))))	→	0^#(5(x1))	(90)
4^#(5(5(5(x1))))	→	2^#(1(0(5(x1))))	(80)
5^#(5(5(x1)))	→	0^#(x1)	(85)
5^#(5(5(x1)))	→	0^#(0(x1))	(93)
5^#(5(5(x1)))	→	5^#(0(0(x1)))	(162)
5^#(5(5(x1)))	→	4^#(5(0(0(x1))))	(68)
5^#(5(5(x1)))	→	0^#(1(4(5(0(0(x1))))))	(133)
5^#(5(5(x1)))	→	4^#(1(0(1(4(5(0(0(x1))))))))	(155)
0^#(1(5(5(5(3(5(x1)))))))	→	0^#(5(x1))	(56)
0^#(1(5(5(5(3(5(x1)))))))	→	2^#(0(5(x1)))	(148)
0^#(1(5(5(5(3(5(x1)))))))	→	0^#(1(2(0(5(x1)))))	(52)
0^#(1(5(5(5(3(5(x1)))))))	→	2^#(5(1(0(1(2(0(5(x1))))))))	(67)
2^#(5(5(3(4(x1)))))	→	4^#(4(x1))	(29)
2^#(5(5(3(4(x1)))))	→	2^#(4(4(x1)))	(91)
2^#(5(5(3(4(x1)))))	→	0^#(2(4(4(x1))))	(132)
2^#(5(5(3(4(x1)))))	→	4^#(0(2(4(4(x1)))))	(24)
4^#(5(2(4(x1))))	→	5^#(5(2(0(3(1(3(3(x1))))))))	(135)
4^#(5(2(4(x1))))	→	4^#(1(5(5(2(0(3(1(3(3(x1))))))))))	(158)
5^#(5(5(1(4(x1)))))	→	0^#(x1)	(110)
5^#(5(5(1(4(x1)))))	→	4^#(0(x1))	(83)
5^#(5(5(1(4(x1)))))	→	4^#(4(0(x1)))	(86)
5^#(5(3(x1)))	→	0^#(x1)	(187)
5^#(5(3(x1)))	→	5^#(0(x1))	(150)
5^#(5(3(x1)))	→	0^#(1(5(0(x1))))	(179)
5^#(5(3(x1)))	→	4^#(1(0(1(5(0(x1))))))	(74)
5^#(5(3(x1)))	→	4^#(4(1(0(1(5(0(x1)))))))	(95)
5^#(5(x1))	→	4^#(x1)	(75)
5^#(5(x1))	→	0^#(4(x1))	(175)
5^#(5(x1))	→	4^#(0(4(x1)))	(118)
5^#(5(x1))	→	4^#(4(0(4(x1))))	(62)
5^#(5(x1))	→	4^#(1(1(1(1(4(4(0(4(x1)))))))))	(170)

1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	26551
[1(x₁)]	=	0
[4(x₁)]	=	0
[5(x₁)]	=	x₁ + 26551
[3(x₁)]	=	0
[2^#(x₁)]	=	26551
[4^#(x₁)]	=	26551
[0(x₁)]	=	26551
[5^#(x₁)]	=	x₁ + 0
[2(x₁)]	=	0
[1^#(x₁)]	=	0

together with the usable rules

5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)
5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)

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

5^#(5(5(x1)))	→	0^#(x1)	(85)
5^#(5(5(x1)))	→	0^#(0(x1))	(93)
5^#(5(5(x1)))	→	5^#(0(0(x1)))	(162)
5^#(5(5(x1)))	→	4^#(5(0(0(x1))))	(68)
5^#(5(5(x1)))	→	0^#(1(4(5(0(0(x1))))))	(133)
5^#(5(5(x1)))	→	4^#(1(0(1(4(5(0(0(x1))))))))	(155)
5^#(5(5(1(4(x1)))))	→	0^#(x1)	(110)
5^#(5(5(1(4(x1)))))	→	4^#(0(x1))	(83)
5^#(5(5(1(4(x1)))))	→	4^#(4(0(x1)))	(86)

could be deleted.

1.1.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^#(5(0(4(x1))))	→	0^#(x1)	(71)
2^#(5(0(4(x1))))	→	0^#(0(x1))	(180)
2^#(5(0(4(x1))))	→	4^#(5(1(0(0(x1)))))	(145)
2^#(5(0(4(x1))))	→	4^#(4(5(1(0(0(x1))))))	(177)
2^#(5(0(4(x1))))	→	2^#(4(4(5(1(0(0(x1)))))))	(171)
5^#(5(x1))	→	2^#(1(x1))	(121)
5^#(5(x1))	→	4^#(5(2(1(x1))))	(84)
5^#(5(x1))	→	2^#(5(4(5(2(1(x1))))))	(66)
5^#(5(x1))	→	0^#(2(5(4(5(2(1(x1)))))))	(163)
5^#(5(x1))	→	4^#(0(2(5(4(5(2(1(x1))))))))	(111)
5^#(5(x1))	→	0^#(5(4(0(2(5(4(5(2(1(x1))))))))))	(87)
2^#(5(5(x1)))	→	2^#(x1)	(137)
2^#(5(5(x1)))	→	0^#(1(1(2(x1))))	(172)
2^#(5(5(x1)))	→	0^#(0(1(1(2(x1)))))	(48)
2^#(5(5(x1)))	→	4^#(0(0(1(1(2(x1))))))	(161)
2^#(5(5(x1)))	→	4^#(4(0(0(1(1(2(x1)))))))	(178)
2^#(5(5(x1)))	→	2^#(5(4(4(0(0(1(1(2(x1)))))))))	(124)
2^#(5(5(x1)))	→	4^#(2(5(4(4(0(0(1(1(2(x1))))))))))	(89)
4^#(4(5(2(4(2(2(x1)))))))	→	2^#(1(x1))	(81)
4^#(4(5(2(4(2(2(x1)))))))	→	2^#(2(1(x1)))	(113)
4^#(4(5(2(4(2(2(x1)))))))	→	4^#(5(1(2(2(1(x1))))))	(157)
4^#(4(5(2(4(2(2(x1)))))))	→	5^#(5(4(5(1(2(2(1(x1))))))))	(182)
4^#(4(5(2(4(2(2(x1)))))))	→	0^#(5(5(4(5(1(2(2(1(x1)))))))))	(181)
4^#(4(5(2(4(2(2(x1)))))))	→	4^#(0(5(5(4(5(1(2(2(1(x1))))))))))	(94)
5^#(5(2(4(5(0(x1))))))	→	2^#(0(x1))	(159)
5^#(5(2(4(5(0(x1))))))	→	4^#(2(0(x1)))	(37)
5^#(5(2(4(5(0(x1))))))	→	0^#(4(2(0(x1))))	(77)
5^#(5(2(4(5(0(x1))))))	→	4^#(0(4(2(0(x1)))))	(39)
5^#(5(2(4(5(0(x1))))))	→	2^#(4(0(4(2(0(x1))))))	(92)
5^#(5(2(4(5(0(x1))))))	→	4^#(2(4(0(4(2(0(x1)))))))	(33)
5^#(5(2(4(5(0(x1))))))	→	2^#(1(1(4(2(4(0(4(2(0(x1))))))))))	(123)
4^#(2(5(5(1(5(x1))))))	→	2^#(5(x1))	(40)
4^#(2(5(5(1(5(x1))))))	→	4^#(2(5(x1)))	(70)
4^#(5(5(5(x1))))	→	0^#(5(x1))	(90)
4^#(5(5(5(x1))))	→	2^#(1(0(5(x1))))	(80)
0^#(1(5(5(5(3(5(x1)))))))	→	0^#(5(x1))	(56)
0^#(1(5(5(5(3(5(x1)))))))	→	2^#(0(5(x1)))	(148)
0^#(1(5(5(5(3(5(x1)))))))	→	0^#(1(2(0(5(x1)))))	(52)
0^#(1(5(5(5(3(5(x1)))))))	→	2^#(5(1(0(1(2(0(5(x1))))))))	(67)
2^#(5(5(3(4(x1)))))	→	4^#(4(x1))	(29)
2^#(5(5(3(4(x1)))))	→	2^#(4(4(x1)))	(91)
2^#(5(5(3(4(x1)))))	→	0^#(2(4(4(x1))))	(132)
2^#(5(5(3(4(x1)))))	→	4^#(0(2(4(4(x1)))))	(24)
4^#(5(2(4(x1))))	→	5^#(5(2(0(3(1(3(3(x1))))))))	(135)
4^#(5(2(4(x1))))	→	4^#(1(5(5(2(0(3(1(3(3(x1))))))))))	(158)
5^#(5(3(x1)))	→	0^#(x1)	(187)
5^#(5(3(x1)))	→	5^#(0(x1))	(150)
5^#(5(3(x1)))	→	0^#(1(5(0(x1))))	(179)
5^#(5(3(x1)))	→	4^#(1(0(1(5(0(x1))))))	(74)
5^#(5(3(x1)))	→	4^#(4(1(0(1(5(0(x1)))))))	(95)
5^#(5(x1))	→	4^#(x1)	(75)
5^#(5(x1))	→	0^#(4(x1))	(175)
5^#(5(x1))	→	4^#(0(4(x1)))	(118)
5^#(5(x1))	→	4^#(4(0(4(x1))))	(62)
5^#(5(x1))	→	4^#(1(1(1(1(4(4(0(4(x1)))))))))	(170)

1.1.1.1.1.1.1.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₁)]

[1(x₁)]

0	0
1	0

· x₁ +

[4(x₁)]

[5(x₁)]

1	1
0	1

· x₁ +

[3(x₁)]

[2^#(x₁)]

[4^#(x₁)]

1	0
0	0

· x₁ +

[0(x₁)]

[5^#(x₁)]

x₁ +

[2(x₁)]

1	0
0	0

· x₁ +

[1^#(x₁)]

together with the usable rules

5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)
5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)

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

4^#(2(5(5(1(5(x1))))))	→	2^#(5(x1))	(40)
4^#(2(5(5(1(5(x1))))))	→	4^#(2(5(x1)))	(70)
4^#(5(5(5(x1))))	→	0^#(5(x1))	(90)
4^#(5(5(5(x1))))	→	2^#(1(0(5(x1))))	(80)

could be deleted.

1.1.1.1.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^#(5(0(4(x1))))	→	0^#(x1)	(71)
2^#(5(0(4(x1))))	→	0^#(0(x1))	(180)
2^#(5(0(4(x1))))	→	4^#(5(1(0(0(x1)))))	(145)
2^#(5(0(4(x1))))	→	4^#(4(5(1(0(0(x1))))))	(177)
2^#(5(0(4(x1))))	→	2^#(4(4(5(1(0(0(x1)))))))	(171)
5^#(5(x1))	→	2^#(1(x1))	(121)
5^#(5(x1))	→	4^#(5(2(1(x1))))	(84)
5^#(5(x1))	→	2^#(5(4(5(2(1(x1))))))	(66)
5^#(5(x1))	→	0^#(2(5(4(5(2(1(x1)))))))	(163)
5^#(5(x1))	→	4^#(0(2(5(4(5(2(1(x1))))))))	(111)
5^#(5(x1))	→	0^#(5(4(0(2(5(4(5(2(1(x1))))))))))	(87)
2^#(5(5(x1)))	→	2^#(x1)	(137)
2^#(5(5(x1)))	→	0^#(1(1(2(x1))))	(172)
2^#(5(5(x1)))	→	0^#(0(1(1(2(x1)))))	(48)
2^#(5(5(x1)))	→	4^#(0(0(1(1(2(x1))))))	(161)
2^#(5(5(x1)))	→	4^#(4(0(0(1(1(2(x1)))))))	(178)
2^#(5(5(x1)))	→	2^#(5(4(4(0(0(1(1(2(x1)))))))))	(124)
2^#(5(5(x1)))	→	4^#(2(5(4(4(0(0(1(1(2(x1))))))))))	(89)
4^#(4(5(2(4(2(2(x1)))))))	→	2^#(1(x1))	(81)
4^#(4(5(2(4(2(2(x1)))))))	→	2^#(2(1(x1)))	(113)
4^#(4(5(2(4(2(2(x1)))))))	→	4^#(5(1(2(2(1(x1))))))	(157)
4^#(4(5(2(4(2(2(x1)))))))	→	5^#(5(4(5(1(2(2(1(x1))))))))	(182)
4^#(4(5(2(4(2(2(x1)))))))	→	0^#(5(5(4(5(1(2(2(1(x1)))))))))	(181)
4^#(4(5(2(4(2(2(x1)))))))	→	4^#(0(5(5(4(5(1(2(2(1(x1))))))))))	(94)
5^#(5(2(4(5(0(x1))))))	→	2^#(0(x1))	(159)
5^#(5(2(4(5(0(x1))))))	→	4^#(2(0(x1)))	(37)
5^#(5(2(4(5(0(x1))))))	→	0^#(4(2(0(x1))))	(77)
5^#(5(2(4(5(0(x1))))))	→	4^#(0(4(2(0(x1)))))	(39)
5^#(5(2(4(5(0(x1))))))	→	2^#(4(0(4(2(0(x1))))))	(92)
5^#(5(2(4(5(0(x1))))))	→	4^#(2(4(0(4(2(0(x1)))))))	(33)
5^#(5(2(4(5(0(x1))))))	→	2^#(1(1(4(2(4(0(4(2(0(x1))))))))))	(123)
0^#(1(5(5(5(3(5(x1)))))))	→	0^#(5(x1))	(56)
0^#(1(5(5(5(3(5(x1)))))))	→	2^#(0(5(x1)))	(148)
0^#(1(5(5(5(3(5(x1)))))))	→	0^#(1(2(0(5(x1)))))	(52)
0^#(1(5(5(5(3(5(x1)))))))	→	2^#(5(1(0(1(2(0(5(x1))))))))	(67)
2^#(5(5(3(4(x1)))))	→	4^#(4(x1))	(29)
2^#(5(5(3(4(x1)))))	→	2^#(4(4(x1)))	(91)
2^#(5(5(3(4(x1)))))	→	0^#(2(4(4(x1))))	(132)
2^#(5(5(3(4(x1)))))	→	4^#(0(2(4(4(x1)))))	(24)
4^#(5(2(4(x1))))	→	5^#(5(2(0(3(1(3(3(x1))))))))	(135)
4^#(5(2(4(x1))))	→	4^#(1(5(5(2(0(3(1(3(3(x1))))))))))	(158)
5^#(5(3(x1)))	→	0^#(x1)	(187)
5^#(5(3(x1)))	→	5^#(0(x1))	(150)
5^#(5(3(x1)))	→	0^#(1(5(0(x1))))	(179)
5^#(5(3(x1)))	→	4^#(1(0(1(5(0(x1))))))	(74)
5^#(5(3(x1)))	→	4^#(4(1(0(1(5(0(x1)))))))	(95)
5^#(5(x1))	→	4^#(x1)	(75)
5^#(5(x1))	→	0^#(4(x1))	(175)
5^#(5(x1))	→	4^#(0(4(x1)))	(118)
5^#(5(x1))	→	4^#(4(0(4(x1))))	(62)
5^#(5(x1))	→	4^#(1(1(1(1(4(4(0(4(x1)))))))))	(170)

1.1.1.1.1.1.1.1.1.1.1.1.1 Reduction Pair Processor with Usable Rules

Using the Max-polynomial interpretation

[0^#(x₁)]	=	26550
[1(x₁)]	=	5332
[4(x₁)]	=	5332
[5(x₁)]	=	x₁ + 5335
[3(x₁)]	=	4900
[2^#(x₁)]	=	x₁ + 15882
[4^#(x₁)]	=	26551
[0(x₁)]	=	10235
[5^#(x₁)]	=	26551
[2(x₁)]	=	5332
[1^#(x₁)]	=	0

together with the usable rules

5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)
5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)

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

2^#(5(0(4(x1))))	→	0^#(x1)	(71)
2^#(5(0(4(x1))))	→	0^#(0(x1))	(180)
2^#(5(0(4(x1))))	→	4^#(5(1(0(0(x1)))))	(145)
2^#(5(0(4(x1))))	→	4^#(4(5(1(0(0(x1))))))	(177)
2^#(5(0(4(x1))))	→	2^#(4(4(5(1(0(0(x1)))))))	(171)
5^#(5(x1))	→	2^#(1(x1))	(121)
5^#(5(x1))	→	2^#(5(4(5(2(1(x1))))))	(66)
5^#(5(x1))	→	0^#(2(5(4(5(2(1(x1)))))))	(163)
5^#(5(x1))	→	0^#(5(4(0(2(5(4(5(2(1(x1))))))))))	(87)
2^#(5(5(x1)))	→	2^#(x1)	(137)
2^#(5(5(x1)))	→	0^#(1(1(2(x1))))	(172)
2^#(5(5(x1)))	→	0^#(0(1(1(2(x1)))))	(48)
2^#(5(5(x1)))	→	4^#(0(0(1(1(2(x1))))))	(161)
2^#(5(5(x1)))	→	4^#(4(0(0(1(1(2(x1)))))))	(178)
2^#(5(5(x1)))	→	2^#(5(4(4(0(0(1(1(2(x1)))))))))	(124)
2^#(5(5(x1)))	→	4^#(2(5(4(4(0(0(1(1(2(x1))))))))))	(89)
4^#(4(5(2(4(2(2(x1)))))))	→	2^#(1(x1))	(81)
4^#(4(5(2(4(2(2(x1)))))))	→	2^#(2(1(x1)))	(113)
4^#(4(5(2(4(2(2(x1)))))))	→	0^#(5(5(4(5(1(2(2(1(x1)))))))))	(181)
5^#(5(2(4(5(0(x1))))))	→	2^#(0(x1))	(159)
5^#(5(2(4(5(0(x1))))))	→	0^#(4(2(0(x1))))	(77)
5^#(5(2(4(5(0(x1))))))	→	2^#(4(0(4(2(0(x1))))))	(92)
5^#(5(2(4(5(0(x1))))))	→	2^#(1(1(4(2(4(0(4(2(0(x1))))))))))	(123)
0^#(1(5(5(5(3(5(x1)))))))	→	2^#(0(5(x1)))	(148)
0^#(1(5(5(5(3(5(x1)))))))	→	2^#(5(1(0(1(2(0(5(x1))))))))	(67)
2^#(5(5(3(4(x1)))))	→	4^#(4(x1))	(29)
2^#(5(5(3(4(x1)))))	→	2^#(4(4(x1)))	(91)
2^#(5(5(3(4(x1)))))	→	0^#(2(4(4(x1))))	(132)
2^#(5(5(3(4(x1)))))	→	4^#(0(2(4(4(x1)))))	(24)
5^#(5(3(x1)))	→	0^#(x1)	(187)
5^#(5(3(x1)))	→	0^#(1(5(0(x1))))	(179)
5^#(5(x1))	→	0^#(4(x1))	(175)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.

The 1^st component contains the pair

0^#(1(5(5(5(3(5(x1)))))))	→	0^#(5(x1))	(56)
0^#(1(5(5(5(3(5(x1)))))))	→	0^#(1(2(0(5(x1)))))	(52)

1.1.1.1.1.1.1.1.1.1.1.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
1	0

· x₁ +

[4(x₁)]

[5(x₁)]

0	1
0	0

· x₁ +

[3(x₁)]

0	0
1	0

· x₁ +

[2^#(x₁)]

[4^#(x₁)]

[0(x₁)]

0	0
1	0

· x₁ +

[5^#(x₁)]

[2(x₁)]

1	0
1	0

· x₁ +

[1^#(x₁)]

together with the usable rules

5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)
5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)

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

0^#(1(5(5(5(3(5(x1)))))))

→

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

(52)

could be deleted.

1.1.1.1.1.1.1.1.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

0^#(1(5(5(5(3(5(x1)))))))

→

0^#(5(x1))

(56)

1.1.1.1.1.1.1.1.1.1.1.1.1.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₁)]

13573

19029

[4(x₁)]

28350

19029

[5(x₁)]

1	1
0	0

· x₁ +

42056

19026

[3(x₁)]

[2^#(x₁)]

[4^#(x₁)]

[0(x₁)]

42076

19026

[5^#(x₁)]

[2(x₁)]

0	1
1	0

· x₁ +

28349

[1^#(x₁)]

together with the usable rules

5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)
5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)

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

0^#(1(5(5(5(3(5(x1)))))))

→

0^#(5(x1))

(56)

could be deleted.

1.1.1.1.1.1.1.1.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

5^#(5(x1))	→	4^#(5(2(1(x1))))	(84)
5^#(5(x1))	→	4^#(0(2(5(4(5(2(1(x1))))))))	(111)
4^#(4(5(2(4(2(2(x1)))))))	→	4^#(5(1(2(2(1(x1))))))	(157)
4^#(4(5(2(4(2(2(x1)))))))	→	5^#(5(4(5(1(2(2(1(x1))))))))	(182)
4^#(4(5(2(4(2(2(x1)))))))	→	4^#(0(5(5(4(5(1(2(2(1(x1))))))))))	(94)
5^#(5(2(4(5(0(x1))))))	→	4^#(2(0(x1)))	(37)
5^#(5(2(4(5(0(x1))))))	→	4^#(0(4(2(0(x1)))))	(39)
5^#(5(2(4(5(0(x1))))))	→	4^#(2(4(0(4(2(0(x1)))))))	(33)
4^#(5(2(4(x1))))	→	5^#(5(2(0(3(1(3(3(x1))))))))	(135)
4^#(5(2(4(x1))))	→	4^#(1(5(5(2(0(3(1(3(3(x1))))))))))	(158)
5^#(5(3(x1)))	→	5^#(0(x1))	(150)
5^#(5(3(x1)))	→	4^#(1(0(1(5(0(x1))))))	(74)
5^#(5(3(x1)))	→	4^#(4(1(0(1(5(0(x1)))))))	(95)
5^#(5(x1))	→	4^#(x1)	(75)
5^#(5(x1))	→	4^#(0(4(x1)))	(118)
5^#(5(x1))	→	4^#(4(0(4(x1))))	(62)
5^#(5(x1))	→	4^#(1(1(1(1(4(4(0(4(x1)))))))))	(170)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.2 Reduction Pair Processor with Usable Rules

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

[0^#(x₁)]

[1(x₁)]

[4(x₁)]

0	1
0	0

· x₁ +

495

14607

[5(x₁)]

1	0
1	0

· x₁ +

[3(x₁)]

[2^#(x₁)]

[4^#(x₁)]

1	0
1	0

· x₁ +

[0(x₁)]

[5^#(x₁)]

0	1
0	1

· x₁ +

15093

15092

[2(x₁)]

1	1
0	0

· x₁ +

15086

14607

[1^#(x₁)]

together with the usable rules

5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)
5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)

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

5^#(5(x1))	→	4^#(5(2(1(x1))))	(84)
5^#(5(x1))	→	4^#(0(2(5(4(5(2(1(x1))))))))	(111)
4^#(4(5(2(4(2(2(x1)))))))	→	4^#(5(1(2(2(1(x1))))))	(157)
4^#(4(5(2(4(2(2(x1)))))))	→	5^#(5(4(5(1(2(2(1(x1))))))))	(182)
4^#(4(5(2(4(2(2(x1)))))))	→	4^#(0(5(5(4(5(1(2(2(1(x1))))))))))	(94)
5^#(5(2(4(5(0(x1))))))	→	4^#(2(0(x1)))	(37)
5^#(5(2(4(5(0(x1))))))	→	4^#(0(4(2(0(x1)))))	(39)
5^#(5(2(4(5(0(x1))))))	→	4^#(2(4(0(4(2(0(x1)))))))	(33)
4^#(5(2(4(x1))))	→	5^#(5(2(0(3(1(3(3(x1))))))))	(135)
4^#(5(2(4(x1))))	→	4^#(1(5(5(2(0(3(1(3(3(x1))))))))))	(158)
5^#(5(3(x1)))	→	4^#(1(0(1(5(0(x1))))))	(74)
5^#(5(3(x1)))	→	4^#(4(1(0(1(5(0(x1)))))))	(95)
5^#(5(x1))	→	4^#(x1)	(75)
5^#(5(x1))	→	4^#(0(4(x1)))	(118)
5^#(5(x1))	→	4^#(4(0(4(x1))))	(62)
5^#(5(x1))	→	4^#(1(1(1(1(4(4(0(4(x1)))))))))	(170)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

5^#(5(3(x1)))

→

5^#(0(x1))

(150)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.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(x₁)]

0	0
1	0

· x₁ +

[4(x₁)]

7167

[5(x₁)]

1	1
0	1

· x₁ +

7169

[3(x₁)]

0	1
0	0

· x₁ +

[2^#(x₁)]

[4^#(x₁)]

0	0
1	0

· x₁ +

[0(x₁)]

0	0
0	1

· x₁ +

7167

[5^#(x₁)]

1	1
0	0

· x₁ +

15093

15092

[2(x₁)]

0	0
1	0

· x₁ +

7167

[1^#(x₁)]

together with the usable rules

5(2(5(5(0(4(x1))))))	→	0(4(2(3(3(5(2(1(4(4(x1))))))))))	(18)
5(2(4(x1)))	→	0(5(0(2(3(3(4(2(4(2(x1))))))))))	(4)
1(2(4(5(2(4(x1))))))	→	3(3(5(3(0(4(0(3(1(3(x1))))))))))	(15)
2(5(0(4(x1))))	→	4(4(3(2(4(4(5(1(0(0(x1))))))))))	(8)
5(5(x1))	→	0(5(4(0(2(5(4(5(2(1(x1))))))))))	(1)
2(5(5(x1)))	→	4(2(5(4(4(0(0(1(1(2(x1))))))))))	(3)
4(1(5(5(0(4(x1))))))	→	1(0(3(0(4(2(4(4(3(4(x1))))))))))	(16)
4(4(5(2(4(2(2(x1)))))))	→	4(0(5(5(4(5(1(2(2(1(x1))))))))))	(21)
5(5(2(4(5(0(x1))))))	→	2(1(1(4(2(4(0(4(2(0(x1))))))))))	(19)
4(2(5(5(1(5(x1))))))	→	2(3(4(2(1(1(3(4(2(5(x1))))))))))	(17)
5(5(2(x1)))	→	0(1(3(2(3(0(3(2(5(3(x1))))))))))	(5)
4(5(5(5(x1))))	→	1(5(1(2(0(3(2(1(0(5(x1))))))))))	(10)
5(5(5(x1)))	→	5(3(4(1(0(1(4(5(0(0(x1))))))))))	(7)
0(1(5(5(5(3(5(x1)))))))	→	5(3(2(5(1(0(1(2(0(5(x1))))))))))	(20)
0(4(4(5(5(5(x1))))))	→	0(4(4(4(3(3(4(1(3(1(x1))))))))))	(14)
2(5(5(3(4(x1)))))	→	4(5(4(3(1(4(0(2(4(4(x1))))))))))	(12)
0(2(5(3(4(x1)))))	→	3(2(4(3(1(5(1(1(3(4(x1))))))))))	(11)
4(5(2(4(x1))))	→	4(1(5(5(2(0(3(1(3(3(x1))))))))))	(9)
5(5(5(1(4(x1)))))	→	3(3(0(5(0(4(3(4(4(0(x1))))))))))	(13)
5(5(3(x1)))	→	0(3(5(4(4(1(0(1(5(0(x1))))))))))	(6)
5(5(x1))	→	3(4(1(1(1(1(4(4(0(4(x1))))))))))	(2)

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

5^#(5(3(x1)))

→

5^#(0(x1))

(150)

could be deleted.

1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.