Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/132611)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over the naturals

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

all of the following rules can be deleted.

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

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

1^#(0(2(2(5(1(3(1(3(3(2(5(x1))))))))))))	→	3^#(5(3(5(0(5(2(3(0(2(4(0(2(3(4(x1)))))))))))))))	(97)
1^#(0(2(2(5(1(3(1(3(3(2(5(x1))))))))))))	→	3^#(5(0(5(2(3(0(2(4(0(2(3(4(x1)))))))))))))	(98)
1^#(0(2(2(5(1(3(1(3(3(2(5(x1))))))))))))	→	2^#(3(0(2(4(0(2(3(4(x1)))))))))	(99)
1^#(0(2(2(5(1(3(1(3(3(2(5(x1))))))))))))	→	3^#(0(2(4(0(2(3(4(x1))))))))	(100)
1^#(0(2(2(5(1(3(1(3(3(2(5(x1))))))))))))	→	2^#(4(0(2(3(4(x1))))))	(101)
1^#(0(2(2(5(1(3(1(3(3(2(5(x1))))))))))))	→	2^#(3(4(x1)))	(102)
1^#(0(2(2(5(1(3(1(3(3(2(5(x1))))))))))))	→	3^#(4(x1))	(103)
1^#(5(1(1(1(5(1(3(2(3(1(5(x1))))))))))))	→	1^#(3(4(4(4(5(3(3(3(5(2(1(5(4(1(5(2(5(x1))))))))))))))))))	(104)
1^#(5(1(1(1(5(1(3(2(3(1(5(x1))))))))))))	→	3^#(4(4(4(5(3(3(3(5(2(1(5(4(1(5(2(5(x1)))))))))))))))))	(105)
1^#(5(1(1(1(5(1(3(2(3(1(5(x1))))))))))))	→	3^#(3(3(5(2(1(5(4(1(5(2(5(x1))))))))))))	(106)
1^#(5(1(1(1(5(1(3(2(3(1(5(x1))))))))))))	→	3^#(3(5(2(1(5(4(1(5(2(5(x1)))))))))))	(107)
1^#(5(1(1(1(5(1(3(2(3(1(5(x1))))))))))))	→	3^#(5(2(1(5(4(1(5(2(5(x1))))))))))	(108)
1^#(5(1(1(1(5(1(3(2(3(1(5(x1))))))))))))	→	2^#(1(5(4(1(5(2(5(x1))))))))	(109)
1^#(5(1(1(1(5(1(3(2(3(1(5(x1))))))))))))	→	1^#(5(4(1(5(2(5(x1)))))))	(110)
1^#(5(1(1(1(5(1(3(2(3(1(5(x1))))))))))))	→	1^#(5(2(5(x1))))	(111)
1^#(5(1(1(1(5(1(3(2(3(1(5(x1))))))))))))	→	2^#(5(x1))	(112)
2^#(0(2(4(5(1(2(2(5(3(5(0(x1))))))))))))	→	1^#(5(4(1(4(3(4(5(3(4(5(2(x1))))))))))))	(113)
2^#(0(2(4(5(1(2(2(5(3(5(0(x1))))))))))))	→	1^#(4(3(4(5(3(4(5(2(x1)))))))))	(114)
2^#(0(2(4(5(1(2(2(5(3(5(0(x1))))))))))))	→	3^#(4(5(3(4(5(2(x1)))))))	(115)
2^#(0(2(4(5(1(2(2(5(3(5(0(x1))))))))))))	→	3^#(4(5(2(x1))))	(116)
2^#(0(2(4(5(1(2(2(5(3(5(0(x1))))))))))))	→	2^#(x1)	(117)
2^#(2(1(0(2(5(1(2(1(5(4(5(x1))))))))))))	→	3^#(5(4(5(4(0(2(2(0(1(3(4(4(3(5(x1)))))))))))))))	(118)
2^#(2(1(0(2(5(1(2(1(5(4(5(x1))))))))))))	→	2^#(2(0(1(3(4(4(3(5(x1)))))))))	(119)
2^#(2(1(0(2(5(1(2(1(5(4(5(x1))))))))))))	→	2^#(0(1(3(4(4(3(5(x1))))))))	(120)
2^#(2(1(0(2(5(1(2(1(5(4(5(x1))))))))))))	→	1^#(3(4(4(3(5(x1))))))	(121)
2^#(2(1(0(2(5(1(2(1(5(4(5(x1))))))))))))	→	3^#(4(4(3(5(x1)))))	(122)
2^#(2(1(0(2(5(1(2(1(5(4(5(x1))))))))))))	→	3^#(5(x1))	(123)
2^#(3(1(1(3(0(3(0(4(0(5(3(x1))))))))))))	→	2^#(0(1(2(4(3(4(1(4(4(3(4(1(4(4(0(3(x1)))))))))))))))))	(124)
2^#(3(1(1(3(0(3(0(4(0(5(3(x1))))))))))))	→	1^#(2(4(3(4(1(4(4(3(4(1(4(4(0(3(x1)))))))))))))))	(125)
2^#(3(1(1(3(0(3(0(4(0(5(3(x1))))))))))))	→	2^#(4(3(4(1(4(4(3(4(1(4(4(0(3(x1))))))))))))))	(126)
2^#(3(1(1(3(0(3(0(4(0(5(3(x1))))))))))))	→	3^#(4(1(4(4(3(4(1(4(4(0(3(x1))))))))))))	(127)
2^#(3(1(1(3(0(3(0(4(0(5(3(x1))))))))))))	→	1^#(4(4(3(4(1(4(4(0(3(x1))))))))))	(128)
2^#(3(1(1(3(0(3(0(4(0(5(3(x1))))))))))))	→	3^#(4(1(4(4(0(3(x1)))))))	(129)
2^#(3(1(1(3(0(3(0(4(0(5(3(x1))))))))))))	→	1^#(4(4(0(3(x1)))))	(130)
2^#(5(1(3(0(0(4(5(3(1(3(4(x1))))))))))))	→	1^#(5(4(0(5(4(0(2(4(0(1(2(x1))))))))))))	(131)
2^#(5(1(3(0(0(4(5(3(1(3(4(x1))))))))))))	→	2^#(4(0(1(2(x1)))))	(132)
2^#(5(1(3(0(0(4(5(3(1(3(4(x1))))))))))))	→	1^#(2(x1))	(133)
2^#(5(1(3(0(0(4(5(3(1(3(4(x1))))))))))))	→	2^#(x1)	(134)
3^#(3(1(2(5(1(2(0(5(5(0(0(x1))))))))))))	→	3^#(4(4(5(4(1(3(1(4(4(0(5(4(3(2(0(2(x1)))))))))))))))))	(135)
3^#(3(1(2(5(1(2(0(5(5(0(0(x1))))))))))))	→	1^#(3(1(4(4(0(5(4(3(2(0(2(x1))))))))))))	(136)
3^#(3(1(2(5(1(2(0(5(5(0(0(x1))))))))))))	→	3^#(1(4(4(0(5(4(3(2(0(2(x1)))))))))))	(137)
3^#(3(1(2(5(1(2(0(5(5(0(0(x1))))))))))))	→	1^#(4(4(0(5(4(3(2(0(2(x1))))))))))	(138)
3^#(3(1(2(5(1(2(0(5(5(0(0(x1))))))))))))	→	3^#(2(0(2(x1))))	(139)
3^#(3(1(2(5(1(2(0(5(5(0(0(x1))))))))))))	→	2^#(0(2(x1)))	(140)
3^#(3(1(2(5(1(2(0(5(5(0(0(x1))))))))))))	→	2^#(x1)	(141)
3^#(5(5(0(2(3(5(0(5(0(4(0(x1))))))))))))	→	2^#(1(3(0(5(4(4(2(x1))))))))	(142)
3^#(5(5(0(2(3(5(0(5(0(4(0(x1))))))))))))	→	1^#(3(0(5(4(4(2(x1)))))))	(143)
3^#(5(5(0(2(3(5(0(5(0(4(0(x1))))))))))))	→	3^#(0(5(4(4(2(x1))))))	(144)
3^#(5(5(0(2(3(5(0(5(0(4(0(x1))))))))))))	→	2^#(x1)	(145)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

2^#(2(1(0(2(5(1(2(1(5(4(5(x1))))))))))))	→	3^#(5(x1))	(123)
3^#(5(5(0(2(3(5(0(5(0(4(0(x1))))))))))))	→	2^#(x1)	(145)
2^#(0(2(4(5(1(2(2(5(3(5(0(x1))))))))))))	→	2^#(x1)	(117)
2^#(5(1(3(0(0(4(5(3(1(3(4(x1))))))))))))	→	2^#(x1)	(134)

1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

Using the linear polynomial interpretation over the naturals

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

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

1.1.1.1.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

3^#(5(5(0(2(3(5(0(5(0(4(0(x1))))))))))))	→	2^#(x1)	(145)

1	>	1
2^#(2(1(0(2(5(1(2(1(5(4(5(x1))))))))))))	→	3^#(5(x1))	(123)

1	>	1
2^#(0(2(4(5(1(2(2(5(3(5(0(x1))))))))))))	→	2^#(x1)	(117)

1	>	1
2^#(5(1(3(0(0(4(5(3(1(3(4(x1))))))))))))	→	2^#(x1)	(134)

1	>	1

As there is no critical graph in the transitive closure, there are no infinite chains.