Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/57852)

The rewrite relation of the following TRS is considered.

0(1(2(1(x1))))	→	0(2(2(2(1(x1)))))	(1)
0(2(1(1(2(0(2(x1)))))))	→	2(2(2(0(2(1(2(2(x1))))))))	(2)
2(0(0(0(0(1(0(x1)))))))	→	1(2(2(2(1(2(1(0(1(x1)))))))))	(3)
0(0(0(1(1(0(0(1(0(1(1(0(0(x1)))))))))))))	→	2(2(1(2(0(2(2(1(1(1(2(2(1(0(x1))))))))))))))	(4)
0(1(1(0(0(1(1(2(1(2(0(0(2(x1)))))))))))))	→	1(2(2(2(1(2(1(0(2(2(0(0(1(2(2(2(2(x1)))))))))))))))))	(5)
1(0(0(0(1(0(1(1(0(1(1(0(1(2(0(1(x1))))))))))))))))	→	2(2(1(1(2(1(2(0(0(1(2(0(0(1(1(0(0(0(x1))))))))))))))))))	(6)
1(0(0(2(0(2(1(0(0(2(0(2(2(0(2(2(x1))))))))))))))))	→	0(0(2(1(2(0(2(0(0(2(0(1(2(0(2(2(x1))))))))))))))))	(7)
1(1(0(1(1(2(0(0(0(0(0(0(1(2(0(0(x1))))))))))))))))	→	2(0(1(1(0(0(2(0(0(2(2(2(0(2(1(2(2(x1)))))))))))))))))	(8)
2(0(0(2(2(2(0(1(2(1(2(0(1(1(0(0(x1))))))))))))))))	→	2(2(2(2(2(2(2(1(2(0(0(2(1(0(1(0(1(2(1(2(x1))))))))))))))))))))	(9)
1(1(1(1(1(1(2(1(0(1(2(1(0(2(2(0(1(x1)))))))))))))))))	→	1(1(2(2(0(2(2(2(2(1(0(1(2(0(2(1(0(0(0(x1)))))))))))))))))))	(10)
0(2(0(0(2(1(0(0(0(0(1(0(2(1(1(1(0(1(x1))))))))))))))))))	→	0(1(2(2(1(0(0(2(2(1(1(1(1(2(1(1(2(1(0(x1)))))))))))))))))))	(11)
1(1(2(1(2(1(1(1(1(1(1(2(2(1(0(1(2(1(x1))))))))))))))))))	→	2(0(2(2(2(2(2(1(1(1(2(0(1(0(2(1(2(2(1(2(2(2(1(2(2(2(x1))))))))))))))))))))))))))	(12)
0(0(1(0(2(0(1(0(1(1(2(0(0(1(0(0(0(1(1(x1)))))))))))))))))))	→	0(2(2(2(0(2(0(1(2(1(1(0(1(2(2(0(1(0(0(2(2(2(2(x1)))))))))))))))))))))))	(13)
0(2(0(2(1(0(2(2(1(0(0(2(0(0(0(2(0(0(1(x1)))))))))))))))))))	→	2(2(0(0(1(2(1(2(1(2(2(2(2(1(0(2(1(1(2(0(x1))))))))))))))))))))	(14)
1(0(0(2(2(0(2(0(2(0(0(2(1(1(0(0(0(1(2(x1)))))))))))))))))))	→	2(2(1(0(2(1(0(2(1(2(1(2(1(0(2(2(2(1(2(2(1(2(x1))))))))))))))))))))))	(15)
0(1(0(0(1(2(2(0(1(0(1(1(1(2(1(1(1(1(0(2(0(x1)))))))))))))))))))))	→	1(0(1(1(1(1(2(2(1(1(2(1(0(0(0(2(2(0(2(0(0(2(x1))))))))))))))))))))))	(16)
1(1(0(1(0(1(1(2(1(0(0(0(1(0(2(0(1(0(0(1(0(1(x1))))))))))))))))))))))	→	0(1(1(1(1(1(0(0(2(1(0(0(2(1(2(0(2(2(1(2(2(1(1(x1)))))))))))))))))))))))	(17)
0(2(0(2(2(1(0(1(2(1(0(0(1(0(2(0(0(0(0(0(2(2(0(x1)))))))))))))))))))))))	→	2(1(1(2(2(1(2(2(2(1(0(0(2(2(0(1(0(1(2(0(0(2(1(1(x1))))))))))))))))))))))))	(18)
1(0(0(1(2(1(2(0(0(0(2(1(0(2(0(2(0(0(0(0(0(1(1(2(2(x1)))))))))))))))))))))))))	→	1(1(1(1(2(0(1(2(2(2(1(2(1(0(1(2(2(0(2(2(2(0(0(1(0(2(x1))))))))))))))))))))))))))	(19)
2(1(2(2(1(2(2(2(0(0(2(1(1(1(0(1(1(2(0(1(1(2(0(2(2(x1)))))))))))))))))))))))))	→	2(2(2(2(0(0(1(2(1(2(0(0(2(1(2(0(2(2(1(2(0(0(2(2(0(1(x1))))))))))))))))))))))))))	(20)
1(0(0(2(1(1(1(1(1(2(2(1(1(1(0(2(1(0(1(2(1(2(0(0(1(2(x1))))))))))))))))))))))))))	→	2(1(2(2(1(2(1(0(2(2(2(1(0(2(2(1(0(1(0(2(2(2(2(1(2(1(2(1(1(0(2(x1)))))))))))))))))))))))))))))))	(21)
0(1(2(1(2(2(0(0(0(1(2(1(0(2(0(0(0(1(2(2(2(0(0(0(1(2(1(x1)))))))))))))))))))))))))))	→	2(2(1(2(2(2(1(2(2(2(2(1(2(2(0(2(1(1(1(0(1(0(2(2(1(1(0(1(x1))))))))))))))))))))))))))))	(22)
1(2(2(0(2(0(1(2(1(2(2(0(2(1(1(1(1(2(0(1(0(0(1(2(0(1(2(x1)))))))))))))))))))))))))))	→	1(2(0(0(2(2(0(2(2(0(0(2(0(0(1(2(0(0(2(2(2(0(1(2(1(0(1(2(x1))))))))))))))))))))))))))))	(23)
0(2(0(2(0(1(0(0(1(0(2(0(0(0(0(1(0(0(2(2(2(1(1(2(0(2(1(2(2(2(x1))))))))))))))))))))))))))))))	→	2(2(1(2(0(1(1(1(2(2(1(2(2(2(0(1(2(2(2(1(2(1(1(1(0(0(1(2(2(0(0(x1)))))))))))))))))))))))))))))))	(24)
1(0(2(0(2(0(2(0(0(1(1(1(2(0(1(0(0(0(1(2(0(1(1(2(0(0(2(1(0(0(x1))))))))))))))))))))))))))))))	→	1(0(1(2(2(1(2(1(2(0(1(1(0(0(2(2(2(2(1(2(0(1(1(1(1(1(2(2(2(2(1(1(x1))))))))))))))))))))))))))))))))	(25)
1(0(2(2(0(2(1(1(0(2(0(1(2(0(2(1(0(1(0(2(1(0(0(1(0(0(2(0(2(2(x1))))))))))))))))))))))))))))))	→	1(1(0(1(2(2(1(1(1(2(1(2(2(0(0(2(2(1(1(2(0(1(2(1(2(0(2(0(2(0(0(2(x1))))))))))))))))))))))))))))))))	(26)
1(2(0(2(0(0(1(2(2(1(1(0(1(2(0(1(0(1(0(0(2(0(1(0(1(0(1(0(2(0(x1))))))))))))))))))))))))))))))	→	2(1(0(2(2(2(0(2(1(2(0(0(2(1(2(2(2(0(1(2(2(2(1(1(0(1(1(0(1(1(0(2(x1))))))))))))))))))))))))))))))))	(27)
2(2(2(1(2(0(0(1(1(1(2(0(0(2(0(1(1(0(2(1(0(2(0(2(1(1(0(0(0(2(x1))))))))))))))))))))))))))))))	→	2(2(2(1(2(1(2(2(2(1(0(0(2(2(1(0(2(2(0(0(2(0(0(0(2(1(1(2(1(1(1(2(2(2(x1))))))))))))))))))))))))))))))))))	(28)
0(1(1(0(0(2(2(1(0(1(1(1(2(2(1(2(0(0(1(1(0(0(2(0(2(2(0(1(1(1(1(x1)))))))))))))))))))))))))))))))	→	0(2(2(0(1(0(1(1(2(1(2(0(0(0(0(0(1(0(1(0(1(2(2(2(2(0(0(0(1(2(1(2(x1))))))))))))))))))))))))))))))))	(29)
0(1(1(1(2(1(1(0(1(2(2(2(0(1(2(1(0(0(1(2(2(1(1(2(0(1(1(1(2(1(1(x1)))))))))))))))))))))))))))))))	→	2(2(1(1(2(1(2(1(2(2(1(0(0(2(1(2(2(2(0(0(0(2(2(0(2(1(1(1(0(2(2(2(x1))))))))))))))))))))))))))))))))	(30)
1(2(1(1(1(1(2(1(0(1(0(2(2(0(0(1(0(1(0(1(2(1(1(1(1(0(2(2(2(2(1(x1)))))))))))))))))))))))))))))))	→	2(0(1(2(2(2(1(2(0(0(2(2(1(1(2(2(2(0(1(2(1(2(1(2(2(1(2(1(1(2(0(1(0(x1)))))))))))))))))))))))))))))))))	(31)
2(0(1(0(1(2(1(2(2(2(0(1(0(0(0(1(2(0(1(1(1(1(2(2(0(0(0(1(0(0(0(x1)))))))))))))))))))))))))))))))	→	2(2(0(2(2(0(2(1(1(2(1(2(2(1(0(0(1(0(2(0(2(2(2(1(0(2(2(0(1(0(2(2(1(2(x1))))))))))))))))))))))))))))))))))	(32)
0(2(2(2(0(1(2(1(0(2(0(1(2(2(0(1(2(1(1(1(1(1(2(0(1(1(2(2(0(1(0(1(x1))))))))))))))))))))))))))))))))	→	2(2(0(1(0(1(2(0(0(2(0(2(2(2(1(2(2(2(1(0(1(1(1(0(1(1(2(0(1(1(1(1(x1))))))))))))))))))))))))))))))))	(33)
1(0(0(2(2(1(0(2(1(2(0(2(0(2(0(2(0(1(1(2(2(1(0(0(0(1(0(1(2(1(2(0(x1))))))))))))))))))))))))))))))))	→	2(2(0(1(0(1(1(1(2(2(1(2(1(0(2(2(2(2(1(2(1(1(2(0(2(2(2(0(0(0(1(1(1(x1)))))))))))))))))))))))))))))))))	(34)
1(2(1(1(1(0(1(2(1(0(1(2(1(1(2(2(0(2(2(1(1(1(1(0(1(2(0(1(1(1(1(1(x1))))))))))))))))))))))))))))))))	→	2(0(1(2(0(2(0(2(1(0(0(0(0(2(2(2(2(2(1(1(0(2(2(2(0(2(2(2(0(1(0(2(2(1(1(x1)))))))))))))))))))))))))))))))))))	(35)
0(1(0(0(1(2(1(2(0(1(1(1(0(1(0(0(2(1(2(0(2(1(1(0(1(0(0(1(1(0(1(0(1(x1)))))))))))))))))))))))))))))))))	→	2(0(0(0(1(0(1(2(2(2(0(1(0(2(0(2(2(2(1(0(1(0(0(2(2(2(0(1(1(1(1(1(1(1(x1))))))))))))))))))))))))))))))))))	(36)
0(2(0(0(2(1(1(0(0(0(2(2(1(0(2(1(0(1(0(0(1(1(2(0(1(1(2(2(0(1(1(1(0(x1)))))))))))))))))))))))))))))))))	→	0(1(2(1(2(2(1(0(2(1(1(2(2(1(2(1(1(0(2(1(0(0(0(2(2(1(2(2(2(2(1(0(0(2(x1))))))))))))))))))))))))))))))))))	(37)
1(2(2(2(0(1(0(0(1(2(1(0(1(1(0(1(1(1(2(1(1(1(2(1(0(0(0(1(0(0(0(1(2(x1)))))))))))))))))))))))))))))))))	→	2(2(2(2(2(2(2(1(0(1(0(2(2(0(0(2(2(2(0(0(0(2(0(0(1(1(2(2(1(2(2(2(1(0(1(0(1(0(2(0(x1))))))))))))))))))))))))))))))))))))))))	(38)
1(1(0(2(0(2(0(0(0(1(1(0(1(0(1(0(1(1(2(1(0(2(0(0(2(2(1(0(0(2(0(2(0(2(x1))))))))))))))))))))))))))))))))))	→	0(2(1(0(0(0(2(2(2(1(2(2(2(2(2(1(0(0(2(2(2(0(0(0(0(1(1(0(1(1(2(1(2(2(2(x1)))))))))))))))))))))))))))))))))))	(39)
1(1(2(1(0(2(0(0(0(2(0(0(2(0(1(0(0(0(0(2(1(0(0(0(0(1(2(2(0(1(1(2(0(1(x1))))))))))))))))))))))))))))))))))	→	2(2(1(2(2(2(2(1(0(2(1(2(2(2(1(1(2(2(1(2(0(1(0(1(1(2(2(1(1(1(0(2(1(2(2(0(0(2(x1))))))))))))))))))))))))))))))))))))))	(40)
1(0(1(1(1(1(1(2(2(1(0(2(0(0(1(0(0(0(0(2(1(1(1(1(0(0(0(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))	→	0(2(0(1(1(2(1(1(1(2(2(0(2(0(2(2(1(2(1(1(2(0(1(2(1(1(2(1(2(1(1(0(1(0(2(1(x1))))))))))))))))))))))))))))))))))))	(41)
1(1(2(0(0(0(1(1(0(1(0(2(2(1(2(1(0(2(2(2(0(2(1(1(2(0(0(0(2(0(1(2(0(0(1(x1)))))))))))))))))))))))))))))))))))	→	2(2(2(1(1(2(2(0(0(2(0(1(1(2(2(1(1(2(0(1(2(1(0(2(1(2(0(2(2(1(0(0(2(0(0(0(x1))))))))))))))))))))))))))))))))))))	(42)
0(0(0(0(0(0(2(1(0(1(0(1(0(1(0(1(2(0(0(1(1(0(2(1(0(2(0(0(0(0(2(2(1(2(2(0(x1))))))))))))))))))))))))))))))))))))	→	1(2(0(0(0(0(1(1(1(2(0(1(2(1(2(2(2(2(1(2(0(1(1(2(1(1(0(1(2(0(1(0(0(0(2(0(0(1(x1))))))))))))))))))))))))))))))))))))))	(43)
0(0(1(2(2(1(1(2(0(0(1(0(2(2(0(0(2(0(1(0(1(0(1(2(2(1(0(2(1(1(0(1(0(0(0(1(x1))))))))))))))))))))))))))))))))))))	→	1(1(2(2(1(2(0(2(2(2(1(2(1(2(0(0(1(2(2(0(0(1(0(1(2(0(0(1(0(1(1(0(1(1(1(1(1(0(x1))))))))))))))))))))))))))))))))))))))	(44)
0(1(1(0(2(0(0(2(1(1(2(0(2(0(1(0(2(0(2(2(2(1(0(0(0(1(1(0(0(2(2(0(0(0(0(2(x1))))))))))))))))))))))))))))))))))))	→	2(2(2(2(1(0(2(0(0(0(0(0(2(2(1(0(1(0(1(2(0(0(0(0(1(2(2(1(2(2(2(2(2(0(1(2(1(1(0(2(x1))))))))))))))))))))))))))))))))))))))))	(45)
0(2(0(0(2(1(1(1(0(2(2(1(1(1(0(0(0(1(0(0(0(2(0(1(1(0(1(0(0(2(0(0(0(2(0(0(x1))))))))))))))))))))))))))))))))))))	→	2(1(2(0(2(1(0(2(1(0(1(1(0(2(2(2(2(1(1(0(2(2(1(2(1(2(0(1(0(1(2(1(2(2(2(0(0(0(x1))))))))))))))))))))))))))))))))))))))	(46)
1(1(2(2(0(1(2(1(2(1(2(2(0(2(0(0(2(2(1(1(0(1(0(0(0(2(1(1(1(1(2(1(2(0(2(2(x1))))))))))))))))))))))))))))))))))))	→	1(1(1(2(0(0(2(1(2(0(1(2(2(2(2(0(2(2(2(1(0(1(0(0(1(2(1(1(1(1(2(0(2(1(0(2(x1))))))))))))))))))))))))))))))))))))	(47)
0(2(0(0(2(0(0(1(0(2(0(0(0(0(2(1(0(0(0(2(2(0(1(0(2(2(0(0(2(0(2(0(0(1(0(1(2(x1)))))))))))))))))))))))))))))))))))))	→	2(2(1(2(1(0(1(1(2(2(2(2(1(0(2(0(0(1(1(2(2(1(0(1(1(1(0(1(1(0(2(1(0(2(2(0(1(2(2(2(x1))))))))))))))))))))))))))))))))))))))))	(48)
0(2(0(2(0(2(1(0(0(0(1(1(1(2(1(0(1(2(1(2(0(1(1(2(0(2(0(0(1(0(2(2(2(2(0(0(2(x1)))))))))))))))))))))))))))))))))))))	→	2(2(1(0(1(2(0(1(2(1(2(2(2(2(2(1(0(2(1(2(0(2(1(1(2(1(1(1(0(0(0(2(0(2(0(2(2(1(x1))))))))))))))))))))))))))))))))))))))	(49)
1(1(0(2(0(2(1(1(1(2(2(2(1(1(2(1(0(2(0(2(0(2(1(2(1(1(1(2(0(2(1(1(2(2(0(1(0(x1)))))))))))))))))))))))))))))))))))))	→	1(2(2(2(1(2(2(0(1(2(2(1(1(2(1(0(0(2(2(0(2(0(1(2(1(2(2(0(1(2(2(2(1(1(0(0(2(0(x1))))))))))))))))))))))))))))))))))))))	(50)
2(1(0(1(0(0(1(0(0(0(1(1(2(2(1(0(0(1(1(1(0(1(0(1(2(1(2(1(0(1(2(1(0(2(0(0(1(x1)))))))))))))))))))))))))))))))))))))	→	1(1(2(2(0(0(2(0(2(1(2(0(2(0(1(2(2(2(1(1(1(0(0(1(0(0(1(1(1(1(1(1(2(1(0(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))	(51)
2(1(0(0(1(1(1(1(0(1(1(0(1(2(0(0(2(2(0(2(1(2(1(2(2(2(0(0(1(0(2(1(2(1(0(2(1(2(x1))))))))))))))))))))))))))))))))))))))	→	2(0(1(0(0(1(2(0(2(1(2(1(2(1(0(2(0(2(2(2(2(2(2(1(0(0(0(2(2(2(0(2(0(0(2(2(1(0(1(1(0(x1)))))))))))))))))))))))))))))))))))))))))	(52)
1(1(0(0(0(2(1(2(1(1(0(0(1(1(1(2(2(0(0(0(1(0(1(0(1(0(2(1(0(0(1(0(1(1(1(2(2(1(0(x1)))))))))))))))))))))))))))))))))))))))	→	2(0(0(0(2(2(1(1(2(1(1(2(2(1(2(1(0(1(1(0(0(1(2(0(0(0(0(0(0(0(0(1(0(1(0(1(1(2(2(1(2(x1)))))))))))))))))))))))))))))))))))))))))	(53)
2(0(2(0(2(1(2(1(1(0(1(1(2(1(2(2(0(1(0(0(2(2(0(1(1(0(1(1(1(2(2(0(1(0(0(1(2(0(2(x1)))))))))))))))))))))))))))))))))))))))	→	2(0(1(0(0(2(2(0(0(2(2(2(2(0(2(0(0(2(1(1(1(0(1(2(0(2(2(1(2(0(0(2(1(1(1(2(0(1(2(1(2(2(x1))))))))))))))))))))))))))))))))))))))))))	(54)
0(1(1(0(2(1(0(2(1(2(0(0(1(0(2(0(0(2(0(2(1(0(1(0(1(2(2(0(1(0(0(1(2(2(0(1(0(0(0(0(x1))))))))))))))))))))))))))))))))))))))))	→	0(2(2(2(2(2(2(1(1(2(2(1(1(2(0(1(1(2(1(2(2(1(2(0(1(1(2(0(1(1(2(1(1(0(1(2(0(1(1(2(2(x1)))))))))))))))))))))))))))))))))))))))))	(55)
0(1(0(1(0(0(2(0(2(0(1(0(2(1(0(1(0(1(2(0(0(0(1(0(2(2(0(2(0(0(0(1(1(1(1(1(0(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))	→	1(1(0(0(1(2(2(0(0(2(1(1(2(2(0(0(1(1(1(0(2(2(2(0(1(0(2(2(0(2(0(2(1(2(1(1(2(1(0(1(2(2(1(x1)))))))))))))))))))))))))))))))))))))))))))	(56)
1(1(0(2(0(1(2(0(0(1(1(0(0(2(1(0(1(0(1(2(1(2(2(0(1(1(2(0(1(2(1(0(1(1(0(1(0(1(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))	→	1(0(0(0(2(1(0(2(0(0(0(0(0(1(0(2(2(0(0(2(2(2(2(2(0(2(0(0(0(1(0(0(1(0(1(0(2(2(2(2(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	(57)
1(1(0(2(2(1(0(2(2(2(1(0(0(0(2(0(0(2(2(0(1(2(1(2(2(1(1(0(0(1(2(0(0(2(2(2(0(0(0(1(1(x1)))))))))))))))))))))))))))))))))))))))))	→	1(1(1(2(2(2(2(2(2(1(1(2(0(2(0(1(0(2(1(0(0(0(1(2(2(2(1(2(2(2(0(2(2(0(1(1(2(2(2(2(2(1(2(2(x1))))))))))))))))))))))))))))))))))))))))))))	(58)
2(2(1(2(0(0(0(0(0(1(2(2(0(1(0(0(2(1(1(0(1(2(1(0(0(1(0(1(0(2(0(0(1(0(2(2(2(1(1(0(2(x1)))))))))))))))))))))))))))))))))))))))))	→	2(1(1(2(1(1(2(1(1(0(2(0(0(0(1(2(2(2(0(2(0(0(2(0(1(0(0(2(1(1(1(1(2(2(2(0(0(2(0(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))	(59)
2(0(1(2(1(1(1(2(1(2(1(2(0(0(0(0(1(2(2(1(1(1(0(2(1(1(0(0(0(0(1(0(0(0(1(1(0(2(0(1(1(1(x1))))))))))))))))))))))))))))))))))))))))))	→	2(1(2(1(2(1(1(2(2(1(0(1(2(0(2(1(0(0(2(1(0(2(2(2(2(1(0(2(2(0(1(2(1(0(2(2(2(1(1(0(2(2(1(0(x1))))))))))))))))))))))))))))))))))))))))))))	(60)
2(1(2(1(1(0(0(0(0(1(0(1(2(2(0(1(0(2(1(1(2(1(1(2(2(1(0(1(1(1(1(1(1(0(2(2(2(1(0(0(0(0(x1))))))))))))))))))))))))))))))))))))))))))	→	2(1(2(1(2(2(2(2(2(0(0(1(0(0(1(1(2(1(2(2(0(0(2(0(1(1(2(2(1(0(0(1(1(2(2(1(0(2(2(2(1(1(1(2(x1))))))))))))))))))))))))))))))))))))))))))))	(61)
0(1(2(1(0(0(2(0(0(2(1(1(1(2(2(1(0(2(0(2(1(2(2(0(2(0(1(0(1(2(1(1(0(0(0(1(0(0(1(2(1(0(1(x1)))))))))))))))))))))))))))))))))))))))))))	→	0(1(2(0(2(1(0(2(2(1(2(1(1(0(1(1(0(1(2(2(2(0(1(0(1(2(2(2(2(0(1(1(2(2(0(1(1(2(1(2(0(2(1(2(2(2(x1))))))))))))))))))))))))))))))))))))))))))))))	(62)
0(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	0(2(2(2(0(0(2(1(2(0(2(1(0(1(2(0(2(1(1(2(0(1(2(1(1(2(2(2(1(0(0(2(2(0(0(0(0(1(0(1(1(1(0(x1)))))))))))))))))))))))))))))))))))))))))))	(63)
0(0(2(1(0(0(2(1(2(2(0(1(2(0(0(0(2(0(0(0(0(0(0(0(1(0(0(2(0(2(0(0(2(2(0(2(1(1(1(1(2(1(0(2(0(x1)))))))))))))))))))))))))))))))))))))))))))))	→	2(2(1(2(1(1(2(0(2(2(2(1(1(2(2(0(1(2(0(0(0(0(0(1(0(1(1(0(2(0(0(0(0(2(2(1(2(2(2(0(2(0(2(0(1(2(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))))	(64)
0(2(1(2(2(1(1(1(1(0(1(1(0(2(0(1(0(2(2(0(2(0(0(1(1(2(0(0(0(0(2(1(2(2(1(1(2(2(0(1(1(2(0(1(0(x1)))))))))))))))))))))))))))))))))))))))))))))	→	2(2(0(2(2(1(1(0(2(2(0(0(2(1(0(0(1(1(0(0(2(1(2(1(1(1(2(1(0(1(2(2(2(2(2(1(1(1(2(2(0(2(2(0(1(2(x1))))))))))))))))))))))))))))))))))))))))))))))	(65)
1(0(1(2(1(1(0(2(2(0(1(2(2(0(0(2(1(0(1(0(0(1(2(1(0(2(1(1(0(0(0(1(0(0(0(2(1(1(0(1(2(2(0(1(0(x1)))))))))))))))))))))))))))))))))))))))))))))	→	1(0(2(1(0(0(0(2(2(0(1(1(0(1(2(2(1(0(2(1(2(2(2(1(1(1(1(2(2(2(1(1(1(1(1(0(0(0(0(0(1(0(2(2(0(0(0(2(x1))))))))))))))))))))))))))))))))))))))))))))))))	(66)
1(0(2(0(0(1(0(1(1(1(1(1(2(1(0(1(0(0(1(2(0(2(0(0(0(1(0(0(2(1(2(0(1(1(0(0(0(1(0(2(1(2(1(1(1(x1)))))))))))))))))))))))))))))))))))))))))))))	→	2(0(1(0(1(0(1(1(2(0(2(2(2(0(2(0(2(0(1(1(2(0(1(1(2(2(0(1(1(0(1(0(0(2(2(2(1(0(2(0(1(0(0(2(1(0(x1))))))))))))))))))))))))))))))))))))))))))))))	(67)
1(1(1(0(0(2(1(0(2(2(0(2(0(0(1(1(0(1(2(2(1(0(1(1(2(0(0(2(2(1(1(2(0(0(0(1(1(0(0(0(0(0(1(2(0(x1)))))))))))))))))))))))))))))))))))))))))))))	→	1(0(0(2(1(0(2(0(1(1(1(1(2(0(1(2(0(2(0(0(2(2(2(1(2(1(2(2(1(2(0(0(2(0(1(1(1(2(0(1(1(1(1(0(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))	(68)
0(0(2(0(2(0(2(0(2(0(2(0(0(2(2(2(1(1(1(0(0(1(1(1(1(1(1(2(1(2(1(2(0(1(0(1(1(1(1(2(0(1(2(1(1(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	1(1(2(2(0(2(0(2(1(2(2(1(2(0(2(1(2(1(1(2(2(2(2(1(0(1(1(1(0(1(0(0(1(0(2(0(2(1(2(2(0(2(1(2(1(2(1(2(x1))))))))))))))))))))))))))))))))))))))))))))))))	(69)
0(2(0(2(2(0(2(0(1(2(1(2(0(0(0(1(0(1(1(2(1(1(2(0(0(0(0(1(1(1(1(2(1(0(2(0(1(1(0(1(0(1(0(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	2(1(1(2(0(1(2(0(2(0(1(2(0(1(2(2(2(2(1(1(1(2(2(2(0(2(1(2(2(0(0(1(0(0(0(0(2(0(1(2(1(1(2(1(2(0(1(0(x1))))))))))))))))))))))))))))))))))))))))))))))))	(70)
0(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	2(2(2(0(1(2(0(0(1(0(1(0(2(1(0(2(0(1(0(0(1(2(0(2(0(0(1(0(0(0(0(1(0(0(0(0(2(2(0(0(2(0(0(2(0(0(x1))))))))))))))))))))))))))))))))))))))))))))))	(71)
1(1(0(2(2(2(1(1(0(1(0(0(0(2(1(1(1(1(1(1(0(2(0(0(0(0(2(2(0(1(1(0(1(1(1(0(1(2(1(1(0(0(1(2(0(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	1(2(2(2(2(2(1(0(2(0(0(0(1(1(2(2(2(1(2(1(0(0(0(0(0(2(2(0(0(0(0(0(0(1(2(2(2(0(2(1(0(1(1(0(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	(72)
2(0(2(2(2(1(2(2(2(2(2(2(2(0(0(1(0(0(2(2(2(1(1(0(0(2(2(0(0(1(0(2(2(0(2(1(2(2(0(1(0(1(2(0(0(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	2(2(2(2(2(1(0(2(0(0(1(2(2(2(1(2(0(1(2(2(1(1(2(0(0(1(0(2(2(1(1(2(0(1(0(1(0(2(2(2(1(1(2(0(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))	(73)
0(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	0(0(1(1(1(1(1(0(2(2(2(1(2(1(0(2(2(1(2(2(1(2(0(1(2(0(0(0(1(1(2(1(0(0(1(0(2(2(2(1(0(1(1(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	(74)
2(1(0(2(0(0(0(2(0(2(2(1(1(2(2(1(1(2(1(0(1(1(0(0(2(0(0(1(0(2(1(1(0(0(2(2(1(1(1(1(0(2(2(0(1(0(2(0(x1))))))))))))))))))))))))))))))))))))))))))))))))	→	2(1(2(2(0(1(0(1(0(0(0(0(0(1(2(1(1(1(2(1(2(0(2(1(0(1(0(2(1(1(2(0(1(1(0(1(0(2(1(2(0(0(2(2(2(2(1(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))	(75)

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₁ + 6
[1(x₁)]	=	1 · x₁ + 5
[2(x₁)]	=	1 · x₁

all of the following rules can be deleted.

0(1(2(1(x1))))	→	0(2(2(2(1(x1)))))	(1)
0(2(1(1(2(0(2(x1)))))))	→	2(2(2(0(2(1(2(2(x1))))))))	(2)
2(0(0(0(0(1(0(x1)))))))	→	1(2(2(2(1(2(1(0(1(x1)))))))))	(3)
0(0(0(1(1(0(0(1(0(1(1(0(0(x1)))))))))))))	→	2(2(1(2(0(2(2(1(1(1(2(2(1(0(x1))))))))))))))	(4)
0(1(1(0(0(1(1(2(1(2(0(0(2(x1)))))))))))))	→	1(2(2(2(1(2(1(0(2(2(0(0(1(2(2(2(2(x1)))))))))))))))))	(5)
1(0(0(0(1(0(1(1(0(1(1(0(1(2(0(1(x1))))))))))))))))	→	2(2(1(1(2(1(2(0(0(1(2(0(0(1(1(0(0(0(x1))))))))))))))))))	(6)
1(1(0(1(1(2(0(0(0(0(0(0(1(2(0(0(x1))))))))))))))))	→	2(0(1(1(0(0(2(0(0(2(2(2(0(2(1(2(2(x1)))))))))))))))))	(8)
2(0(0(2(2(2(0(1(2(1(2(0(1(1(0(0(x1))))))))))))))))	→	2(2(2(2(2(2(2(1(2(0(0(2(1(0(1(0(1(2(1(2(x1))))))))))))))))))))	(9)
1(1(1(1(1(1(2(1(0(1(2(1(0(2(2(0(1(x1)))))))))))))))))	→	1(1(2(2(0(2(2(2(2(1(0(1(2(0(2(1(0(0(0(x1)))))))))))))))))))	(10)
0(2(0(0(2(1(0(0(0(0(1(0(2(1(1(1(0(1(x1))))))))))))))))))	→	0(1(2(2(1(0(0(2(2(1(1(1(1(2(1(1(2(1(0(x1)))))))))))))))))))	(11)
1(1(2(1(2(1(1(1(1(1(1(2(2(1(0(1(2(1(x1))))))))))))))))))	→	2(0(2(2(2(2(2(1(1(1(2(0(1(0(2(1(2(2(1(2(2(2(1(2(2(2(x1))))))))))))))))))))))))))	(12)
0(0(1(0(2(0(1(0(1(1(2(0(0(1(0(0(0(1(1(x1)))))))))))))))))))	→	0(2(2(2(0(2(0(1(2(1(1(0(1(2(2(0(1(0(0(2(2(2(2(x1)))))))))))))))))))))))	(13)
0(2(0(2(1(0(2(2(1(0(0(2(0(0(0(2(0(0(1(x1)))))))))))))))))))	→	2(2(0(0(1(2(1(2(1(2(2(2(2(1(0(2(1(1(2(0(x1))))))))))))))))))))	(14)
1(0(0(2(2(0(2(0(2(0(0(2(1(1(0(0(0(1(2(x1)))))))))))))))))))	→	2(2(1(0(2(1(0(2(1(2(1(2(1(0(2(2(2(1(2(2(1(2(x1))))))))))))))))))))))	(15)
0(1(0(0(1(2(2(0(1(0(1(1(1(2(1(1(1(1(0(2(0(x1)))))))))))))))))))))	→	1(0(1(1(1(1(2(2(1(1(2(1(0(0(0(2(2(0(2(0(0(2(x1))))))))))))))))))))))	(16)
1(1(0(1(0(1(1(2(1(0(0(0(1(0(2(0(1(0(0(1(0(1(x1))))))))))))))))))))))	→	0(1(1(1(1(1(0(0(2(1(0(0(2(1(2(0(2(2(1(2(2(1(1(x1)))))))))))))))))))))))	(17)
0(2(0(2(2(1(0(1(2(1(0(0(1(0(2(0(0(0(0(0(2(2(0(x1)))))))))))))))))))))))	→	2(1(1(2(2(1(2(2(2(1(0(0(2(2(0(1(0(1(2(0(0(2(1(1(x1))))))))))))))))))))))))	(18)
1(0(0(1(2(1(2(0(0(0(2(1(0(2(0(2(0(0(0(0(0(1(1(2(2(x1)))))))))))))))))))))))))	→	1(1(1(1(2(0(1(2(2(2(1(2(1(0(1(2(2(0(2(2(2(0(0(1(0(2(x1))))))))))))))))))))))))))	(19)
2(1(2(2(1(2(2(2(0(0(2(1(1(1(0(1(1(2(0(1(1(2(0(2(2(x1)))))))))))))))))))))))))	→	2(2(2(2(0(0(1(2(1(2(0(0(2(1(2(0(2(2(1(2(0(0(2(2(0(1(x1))))))))))))))))))))))))))	(20)
1(0(0(2(1(1(1(1(1(2(2(1(1(1(0(2(1(0(1(2(1(2(0(0(1(2(x1))))))))))))))))))))))))))	→	2(1(2(2(1(2(1(0(2(2(2(1(0(2(2(1(0(1(0(2(2(2(2(1(2(1(2(1(1(0(2(x1)))))))))))))))))))))))))))))))	(21)
0(1(2(1(2(2(0(0(0(1(2(1(0(2(0(0(0(1(2(2(2(0(0(0(1(2(1(x1)))))))))))))))))))))))))))	→	2(2(1(2(2(2(1(2(2(2(2(1(2(2(0(2(1(1(1(0(1(0(2(2(1(1(0(1(x1))))))))))))))))))))))))))))	(22)
1(2(2(0(2(0(1(2(1(2(2(0(2(1(1(1(1(2(0(1(0(0(1(2(0(1(2(x1)))))))))))))))))))))))))))	→	1(2(0(0(2(2(0(2(2(0(0(2(0(0(1(2(0(0(2(2(2(0(1(2(1(0(1(2(x1))))))))))))))))))))))))))))	(23)
0(2(0(2(0(1(0(0(1(0(2(0(0(0(0(1(0(0(2(2(2(1(1(2(0(2(1(2(2(2(x1))))))))))))))))))))))))))))))	→	2(2(1(2(0(1(1(1(2(2(1(2(2(2(0(1(2(2(2(1(2(1(1(1(0(0(1(2(2(0(0(x1)))))))))))))))))))))))))))))))	(24)
1(0(2(0(2(0(2(0(0(1(1(1(2(0(1(0(0(0(1(2(0(1(1(2(0(0(2(1(0(0(x1))))))))))))))))))))))))))))))	→	1(0(1(2(2(1(2(1(2(0(1(1(0(0(2(2(2(2(1(2(0(1(1(1(1(1(2(2(2(2(1(1(x1))))))))))))))))))))))))))))))))	(25)
1(0(2(2(0(2(1(1(0(2(0(1(2(0(2(1(0(1(0(2(1(0(0(1(0(0(2(0(2(2(x1))))))))))))))))))))))))))))))	→	1(1(0(1(2(2(1(1(1(2(1(2(2(0(0(2(2(1(1(2(0(1(2(1(2(0(2(0(2(0(0(2(x1))))))))))))))))))))))))))))))))	(26)
1(2(0(2(0(0(1(2(2(1(1(0(1(2(0(1(0(1(0(0(2(0(1(0(1(0(1(0(2(0(x1))))))))))))))))))))))))))))))	→	2(1(0(2(2(2(0(2(1(2(0(0(2(1(2(2(2(0(1(2(2(2(1(1(0(1(1(0(1(1(0(2(x1))))))))))))))))))))))))))))))))	(27)
2(2(2(1(2(0(0(1(1(1(2(0(0(2(0(1(1(0(2(1(0(2(0(2(1(1(0(0(0(2(x1))))))))))))))))))))))))))))))	→	2(2(2(1(2(1(2(2(2(1(0(0(2(2(1(0(2(2(0(0(2(0(0(0(2(1(1(2(1(1(1(2(2(2(x1))))))))))))))))))))))))))))))))))	(28)
0(1(1(0(0(2(2(1(0(1(1(1(2(2(1(2(0(0(1(1(0(0(2(0(2(2(0(1(1(1(1(x1)))))))))))))))))))))))))))))))	→	0(2(2(0(1(0(1(1(2(1(2(0(0(0(0(0(1(0(1(0(1(2(2(2(2(0(0(0(1(2(1(2(x1))))))))))))))))))))))))))))))))	(29)
0(1(1(1(2(1(1(0(1(2(2(2(0(1(2(1(0(0(1(2(2(1(1(2(0(1(1(1(2(1(1(x1)))))))))))))))))))))))))))))))	→	2(2(1(1(2(1(2(1(2(2(1(0(0(2(1(2(2(2(0(0(0(2(2(0(2(1(1(1(0(2(2(2(x1))))))))))))))))))))))))))))))))	(30)
1(2(1(1(1(1(2(1(0(1(0(2(2(0(0(1(0(1(0(1(2(1(1(1(1(0(2(2(2(2(1(x1)))))))))))))))))))))))))))))))	→	2(0(1(2(2(2(1(2(0(0(2(2(1(1(2(2(2(0(1(2(1(2(1(2(2(1(2(1(1(2(0(1(0(x1)))))))))))))))))))))))))))))))))	(31)
2(0(1(0(1(2(1(2(2(2(0(1(0(0(0(1(2(0(1(1(1(1(2(2(0(0(0(1(0(0(0(x1)))))))))))))))))))))))))))))))	→	2(2(0(2(2(0(2(1(1(2(1(2(2(1(0(0(1(0(2(0(2(2(2(1(0(2(2(0(1(0(2(2(1(2(x1))))))))))))))))))))))))))))))))))	(32)
1(0(0(2(2(1(0(2(1(2(0(2(0(2(0(2(0(1(1(2(2(1(0(0(0(1(0(1(2(1(2(0(x1))))))))))))))))))))))))))))))))	→	2(2(0(1(0(1(1(1(2(2(1(2(1(0(2(2(2(2(1(2(1(1(2(0(2(2(2(0(0(0(1(1(1(x1)))))))))))))))))))))))))))))))))	(34)
1(2(1(1(1(0(1(2(1(0(1(2(1(1(2(2(0(2(2(1(1(1(1(0(1(2(0(1(1(1(1(1(x1))))))))))))))))))))))))))))))))	→	2(0(1(2(0(2(0(2(1(0(0(0(0(2(2(2(2(2(1(1(0(2(2(2(0(2(2(2(0(1(0(2(2(1(1(x1)))))))))))))))))))))))))))))))))))	(35)
0(1(0(0(1(2(1(2(0(1(1(1(0(1(0(0(2(1(2(0(2(1(1(0(1(0(0(1(1(0(1(0(1(x1)))))))))))))))))))))))))))))))))	→	2(0(0(0(1(0(1(2(2(2(0(1(0(2(0(2(2(2(1(0(1(0(0(2(2(2(0(1(1(1(1(1(1(1(x1))))))))))))))))))))))))))))))))))	(36)
0(2(0(0(2(1(1(0(0(0(2(2(1(0(2(1(0(1(0(0(1(1(2(0(1(1(2(2(0(1(1(1(0(x1)))))))))))))))))))))))))))))))))	→	0(1(2(1(2(2(1(0(2(1(1(2(2(1(2(1(1(0(2(1(0(0(0(2(2(1(2(2(2(2(1(0(0(2(x1))))))))))))))))))))))))))))))))))	(37)
1(2(2(2(0(1(0(0(1(2(1(0(1(1(0(1(1(1(2(1(1(1(2(1(0(0(0(1(0(0(0(1(2(x1)))))))))))))))))))))))))))))))))	→	2(2(2(2(2(2(2(1(0(1(0(2(2(0(0(2(2(2(0(0(0(2(0(0(1(1(2(2(1(2(2(2(1(0(1(0(1(0(2(0(x1))))))))))))))))))))))))))))))))))))))))	(38)
1(1(0(2(0(2(0(0(0(1(1(0(1(0(1(0(1(1(2(1(0(2(0(0(2(2(1(0(0(2(0(2(0(2(x1))))))))))))))))))))))))))))))))))	→	0(2(1(0(0(0(2(2(2(1(2(2(2(2(2(1(0(0(2(2(2(0(0(0(0(1(1(0(1(1(2(1(2(2(2(x1)))))))))))))))))))))))))))))))))))	(39)
1(1(2(1(0(2(0(0(0(2(0(0(2(0(1(0(0(0(0(2(1(0(0(0(0(1(2(2(0(1(1(2(0(1(x1))))))))))))))))))))))))))))))))))	→	2(2(1(2(2(2(2(1(0(2(1(2(2(2(1(1(2(2(1(2(0(1(0(1(1(2(2(1(1(1(0(2(1(2(2(0(0(2(x1))))))))))))))))))))))))))))))))))))))	(40)
1(0(1(1(1(1(1(2(2(1(0(2(0(0(1(0(0(0(0(2(1(1(1(1(0(0(0(0(2(1(0(1(1(2(1(x1)))))))))))))))))))))))))))))))))))	→	0(2(0(1(1(2(1(1(1(2(2(0(2(0(2(2(1(2(1(1(2(0(1(2(1(1(2(1(2(1(1(0(1(0(2(1(x1))))))))))))))))))))))))))))))))))))	(41)
1(1(2(0(0(0(1(1(0(1(0(2(2(1(2(1(0(2(2(2(0(2(1(1(2(0(0(0(2(0(1(2(0(0(1(x1)))))))))))))))))))))))))))))))))))	→	2(2(2(1(1(2(2(0(0(2(0(1(1(2(2(1(1(2(0(1(2(1(0(2(1(2(0(2(2(1(0(0(2(0(0(0(x1))))))))))))))))))))))))))))))))))))	(42)
0(0(0(0(0(0(2(1(0(1(0(1(0(1(0(1(2(0(0(1(1(0(2(1(0(2(0(0(0(0(2(2(1(2(2(0(x1))))))))))))))))))))))))))))))))))))	→	1(2(0(0(0(0(1(1(1(2(0(1(2(1(2(2(2(2(1(2(0(1(1(2(1(1(0(1(2(0(1(0(0(0(2(0(0(1(x1))))))))))))))))))))))))))))))))))))))	(43)
0(0(1(2(2(1(1(2(0(0(1(0(2(2(0(0(2(0(1(0(1(0(1(2(2(1(0(2(1(1(0(1(0(0(0(1(x1))))))))))))))))))))))))))))))))))))	→	1(1(2(2(1(2(0(2(2(2(1(2(1(2(0(0(1(2(2(0(0(1(0(1(2(0(0(1(0(1(1(0(1(1(1(1(1(0(x1))))))))))))))))))))))))))))))))))))))	(44)
0(1(1(0(2(0(0(2(1(1(2(0(2(0(1(0(2(0(2(2(2(1(0(0(0(1(1(0(0(2(2(0(0(0(0(2(x1))))))))))))))))))))))))))))))))))))	→	2(2(2(2(1(0(2(0(0(0(0(0(2(2(1(0(1(0(1(2(0(0(0(0(1(2(2(1(2(2(2(2(2(0(1(2(1(1(0(2(x1))))))))))))))))))))))))))))))))))))))))	(45)
0(2(0(0(2(1(1(1(0(2(2(1(1(1(0(0(0(1(0(0(0(2(0(1(1(0(1(0(0(2(0(0(0(2(0(0(x1))))))))))))))))))))))))))))))))))))	→	2(1(2(0(2(1(0(2(1(0(1(1(0(2(2(2(2(1(1(0(2(2(1(2(1(2(0(1(0(1(2(1(2(2(2(0(0(0(x1))))))))))))))))))))))))))))))))))))))	(46)
0(2(0(0(2(0(0(1(0(2(0(0(0(0(2(1(0(0(0(2(2(0(1(0(2(2(0(0(2(0(2(0(0(1(0(1(2(x1)))))))))))))))))))))))))))))))))))))	→	2(2(1(2(1(0(1(1(2(2(2(2(1(0(2(0(0(1(1(2(2(1(0(1(1(1(0(1(1(0(2(1(0(2(2(0(1(2(2(2(x1))))))))))))))))))))))))))))))))))))))))	(48)
0(2(0(2(0(2(1(0(0(0(1(1(1(2(1(0(1(2(1(2(0(1(1(2(0(2(0(0(1(0(2(2(2(2(0(0(2(x1)))))))))))))))))))))))))))))))))))))	→	2(2(1(0(1(2(0(1(2(1(2(2(2(2(2(1(0(2(1(2(0(2(1(1(2(1(1(1(0(0(0(2(0(2(0(2(2(1(x1))))))))))))))))))))))))))))))))))))))	(49)
1(1(0(2(0(2(1(1(1(2(2(2(1(1(2(1(0(2(0(2(0(2(1(2(1(1(1(2(0(2(1(1(2(2(0(1(0(x1)))))))))))))))))))))))))))))))))))))	→	1(2(2(2(1(2(2(0(1(2(2(1(1(2(1(0(0(2(2(0(2(0(1(2(1(2(2(0(1(2(2(2(1(1(0(0(2(0(x1))))))))))))))))))))))))))))))))))))))	(50)
2(1(0(1(0(0(1(0(0(0(1(1(2(2(1(0(0(1(1(1(0(1(0(1(2(1(2(1(0(1(2(1(0(2(0(0(1(x1)))))))))))))))))))))))))))))))))))))	→	1(1(2(2(0(0(2(0(2(1(2(0(2(0(1(2(2(2(1(1(1(0(0(1(0(0(1(1(1(1(1(1(2(1(0(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))	(51)
2(1(0(0(1(1(1(1(0(1(1(0(1(2(0(0(2(2(0(2(1(2(1(2(2(2(0(0(1(0(2(1(2(1(0(2(1(2(x1))))))))))))))))))))))))))))))))))))))	→	2(0(1(0(0(1(2(0(2(1(2(1(2(1(0(2(0(2(2(2(2(2(2(1(0(0(0(2(2(2(0(2(0(0(2(2(1(0(1(1(0(x1)))))))))))))))))))))))))))))))))))))))))	(52)
1(1(0(0(0(2(1(2(1(1(0(0(1(1(1(2(2(0(0(0(1(0(1(0(1(0(2(1(0(0(1(0(1(1(1(2(2(1(0(x1)))))))))))))))))))))))))))))))))))))))	→	2(0(0(0(2(2(1(1(2(1(1(2(2(1(2(1(0(1(1(0(0(1(2(0(0(0(0(0(0(0(0(1(0(1(0(1(1(2(2(1(2(x1)))))))))))))))))))))))))))))))))))))))))	(53)
2(0(2(0(2(1(2(1(1(0(1(1(2(1(2(2(0(1(0(0(2(2(0(1(1(0(1(1(1(2(2(0(1(0(0(1(2(0(2(x1)))))))))))))))))))))))))))))))))))))))	→	2(0(1(0(0(2(2(0(0(2(2(2(2(0(2(0(0(2(1(1(1(0(1(2(0(2(2(1(2(0(0(2(1(1(1(2(0(1(2(1(2(2(x1))))))))))))))))))))))))))))))))))))))))))	(54)
0(1(1(0(2(1(0(2(1(2(0(0(1(0(2(0(0(2(0(2(1(0(1(0(1(2(2(0(1(0(0(1(2(2(0(1(0(0(0(0(x1))))))))))))))))))))))))))))))))))))))))	→	0(2(2(2(2(2(2(1(1(2(2(1(1(2(0(1(1(2(1(2(2(1(2(0(1(1(2(0(1(1(2(1(1(0(1(2(0(1(1(2(2(x1)))))))))))))))))))))))))))))))))))))))))	(55)
0(1(0(1(0(0(2(0(2(0(1(0(2(1(0(1(0(1(2(0(0(0(1(0(2(2(0(2(0(0(0(1(1(1(1(1(0(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))	→	1(1(0(0(1(2(2(0(0(2(1(1(2(2(0(0(1(1(1(0(2(2(2(0(1(0(2(2(0(2(0(2(1(2(1(1(2(1(0(1(2(2(1(x1)))))))))))))))))))))))))))))))))))))))))))	(56)
1(1(0(2(0(1(2(0(0(1(1(0(0(2(1(0(1(0(1(2(1(2(2(0(1(1(2(0(1(2(1(0(1(1(0(1(0(1(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))	→	1(0(0(0(2(1(0(2(0(0(0(0(0(1(0(2(2(0(0(2(2(2(2(2(0(2(0(0(0(1(0(0(1(0(1(0(2(2(2(2(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	(57)
1(1(0(2(2(1(0(2(2(2(1(0(0(0(2(0(0(2(2(0(1(2(1(2(2(1(1(0(0(1(2(0(0(2(2(2(0(0(0(1(1(x1)))))))))))))))))))))))))))))))))))))))))	→	1(1(1(2(2(2(2(2(2(1(1(2(0(2(0(1(0(2(1(0(0(0(1(2(2(2(1(2(2(2(0(2(2(0(1(1(2(2(2(2(2(1(2(2(x1))))))))))))))))))))))))))))))))))))))))))))	(58)
2(2(1(2(0(0(0(0(0(1(2(2(0(1(0(0(2(1(1(0(1(2(1(0(0(1(0(1(0(2(0(0(1(0(2(2(2(1(1(0(2(x1)))))))))))))))))))))))))))))))))))))))))	→	2(1(1(2(1(1(2(1(1(0(2(0(0(0(1(2(2(2(0(2(0(0(2(0(1(0(0(2(1(1(1(1(2(2(2(0(0(2(0(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))	(59)
2(0(1(2(1(1(1(2(1(2(1(2(0(0(0(0(1(2(2(1(1(1(0(2(1(1(0(0(0(0(1(0(0(0(1(1(0(2(0(1(1(1(x1))))))))))))))))))))))))))))))))))))))))))	→	2(1(2(1(2(1(1(2(2(1(0(1(2(0(2(1(0(0(2(1(0(2(2(2(2(1(0(2(2(0(1(2(1(0(2(2(2(1(1(0(2(2(1(0(x1))))))))))))))))))))))))))))))))))))))))))))	(60)
2(1(2(1(1(0(0(0(0(1(0(1(2(2(0(1(0(2(1(1(2(1(1(2(2(1(0(1(1(1(1(1(1(0(2(2(2(1(0(0(0(0(x1))))))))))))))))))))))))))))))))))))))))))	→	2(1(2(1(2(2(2(2(2(0(0(1(0(0(1(1(2(1(2(2(0(0(2(0(1(1(2(2(1(0(0(1(1(2(2(1(0(2(2(2(1(1(1(2(x1))))))))))))))))))))))))))))))))))))))))))))	(61)
0(1(2(1(0(0(2(0(0(2(1(1(1(2(2(1(0(2(0(2(1(2(2(0(2(0(1(0(1(2(1(1(0(0(0(1(0(0(1(2(1(0(1(x1)))))))))))))))))))))))))))))))))))))))))))	→	0(1(2(0(2(1(0(2(2(1(2(1(1(0(1(1(0(1(2(2(2(0(1(0(1(2(2(2(2(0(1(1(2(2(0(1(1(2(1(2(0(2(1(2(2(2(x1))))))))))))))))))))))))))))))))))))))))))))))	(62)
0(0(2(1(0(0(2(1(2(2(0(1(2(0(0(0(2(0(0(0(0(0(0(0(1(0(0(2(0(2(0(0(2(2(0(2(1(1(1(1(2(1(0(2(0(x1)))))))))))))))))))))))))))))))))))))))))))))	→	2(2(1(2(1(1(2(0(2(2(2(1(1(2(2(0(1(2(0(0(0(0(0(1(0(1(1(0(2(0(0(0(0(2(2(1(2(2(2(0(2(0(2(0(1(2(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))))	(64)
0(2(1(2(2(1(1(1(1(0(1(1(0(2(0(1(0(2(2(0(2(0(0(1(1(2(0(0(0(0(2(1(2(2(1(1(2(2(0(1(1(2(0(1(0(x1)))))))))))))))))))))))))))))))))))))))))))))	→	2(2(0(2(2(1(1(0(2(2(0(0(2(1(0(0(1(1(0(0(2(1(2(1(1(1(2(1(0(1(2(2(2(2(2(1(1(1(2(2(0(2(2(0(1(2(x1))))))))))))))))))))))))))))))))))))))))))))))	(65)
1(0(1(2(1(1(0(2(2(0(1(2(2(0(0(2(1(0(1(0(0(1(2(1(0(2(1(1(0(0(0(1(0(0(0(2(1(1(0(1(2(2(0(1(0(x1)))))))))))))))))))))))))))))))))))))))))))))	→	1(0(2(1(0(0(0(2(2(0(1(1(0(1(2(2(1(0(2(1(2(2(2(1(1(1(1(2(2(2(1(1(1(1(1(0(0(0(0(0(1(0(2(2(0(0(0(2(x1))))))))))))))))))))))))))))))))))))))))))))))))	(66)
1(0(2(0(0(1(0(1(1(1(1(1(2(1(0(1(0(0(1(2(0(2(0(0(0(1(0(0(2(1(2(0(1(1(0(0(0(1(0(2(1(2(1(1(1(x1)))))))))))))))))))))))))))))))))))))))))))))	→	2(0(1(0(1(0(1(1(2(0(2(2(2(0(2(0(2(0(1(1(2(0(1(1(2(2(0(1(1(0(1(0(0(2(2(2(1(0(2(0(1(0(0(2(1(0(x1))))))))))))))))))))))))))))))))))))))))))))))	(67)
1(1(1(0(0(2(1(0(2(2(0(2(0(0(1(1(0(1(2(2(1(0(1(1(2(0(0(2(2(1(1(2(0(0(0(1(1(0(0(0(0(0(1(2(0(x1)))))))))))))))))))))))))))))))))))))))))))))	→	1(0(0(2(1(0(2(0(1(1(1(1(2(0(1(2(0(2(0(0(2(2(2(1(2(1(2(2(1(2(0(0(2(0(1(1(1(2(0(1(1(1(1(0(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))	(68)
0(0(2(0(2(0(2(0(2(0(2(0(0(2(2(2(1(1(1(0(0(1(1(1(1(1(1(2(1(2(1(2(0(1(0(1(1(1(1(2(0(1(2(1(1(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	1(1(2(2(0(2(0(2(1(2(2(1(2(0(2(1(2(1(1(2(2(2(2(1(0(1(1(1(0(1(0(0(1(0(2(0(2(1(2(2(0(2(1(2(1(2(1(2(x1))))))))))))))))))))))))))))))))))))))))))))))))	(69)
0(2(0(2(2(0(2(0(1(2(1(2(0(0(0(1(0(1(1(2(1(1(2(0(0(0(0(1(1(1(1(2(1(0(2(0(1(1(0(1(0(1(0(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	2(1(1(2(0(1(2(0(2(0(1(2(0(1(2(2(2(2(1(1(1(2(2(2(0(2(1(2(2(0(0(1(0(0(0(0(2(0(1(2(1(1(2(1(2(0(1(0(x1))))))))))))))))))))))))))))))))))))))))))))))))	(70)
1(1(0(2(2(2(1(1(0(1(0(0(0(2(1(1(1(1(1(1(0(2(0(0(0(0(2(2(0(1(1(0(1(1(1(0(1(2(1(1(0(0(1(2(0(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	1(2(2(2(2(2(1(0(2(0(0(0(1(1(2(2(2(1(2(1(0(0(0(0(0(2(2(0(0(0(0(0(0(1(2(2(2(0(2(1(0(1(1(0(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	(72)
2(0(2(2(2(1(2(2(2(2(2(2(2(0(0(1(0(0(2(2(2(1(1(0(0(2(2(0(0(1(0(2(2(0(2(1(2(2(0(1(0(1(2(0(0(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	2(2(2(2(2(1(0(2(0(0(1(2(2(2(1(2(0(1(2(2(1(1(2(0(0(1(0(2(2(1(1(2(0(1(0(1(0(2(2(2(1(1(2(0(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))	(73)
2(1(0(2(0(0(0(2(0(2(2(1(1(2(2(1(1(2(1(0(1(1(0(0(2(0(0(1(0(2(1(1(0(0(2(2(1(1(1(1(0(2(2(0(1(0(2(0(x1))))))))))))))))))))))))))))))))))))))))))))))))	→	2(1(2(2(0(1(0(1(0(0(0(0(0(1(2(1(1(1(2(1(2(0(2(1(0(1(0(2(1(1(2(0(1(1(0(1(0(2(1(2(0(0(2(2(2(2(1(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))	(75)

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

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

1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

The 1^st component contains the pair

1^#(1(2(2(0(1(2(1(2(1(2(2(0(2(0(0(2(2(1(1(0(1(0(0(0(2(1(1(1(1(2(1(2(0(2(2(x1))))))))))))))))))))))))))))))))))))	→	1^#(1(1(1(2(0(2(1(0(2(x1))))))))))	(119)
1^#(1(2(2(0(1(2(1(2(1(2(2(0(2(0(0(2(2(1(1(0(1(0(0(0(2(1(1(1(1(2(1(2(0(2(2(x1))))))))))))))))))))))))))))))))))))	→	1^#(1(1(2(0(2(1(0(2(x1)))))))))	(120)
1^#(1(2(2(0(1(2(1(2(1(2(2(0(2(0(0(2(2(1(1(0(1(0(0(0(2(1(1(1(1(2(1(2(0(2(2(x1))))))))))))))))))))))))))))))))))))	→	1^#(1(2(0(2(1(0(2(x1))))))))	(121)
1^#(1(2(2(0(1(2(1(2(1(2(2(0(2(0(0(2(2(1(1(0(1(0(0(0(2(1(1(1(1(2(1(2(0(2(2(x1))))))))))))))))))))))))))))))))))))	→	0^#(2(1(0(2(x1)))))	(123)
0^#(2(2(2(0(1(2(1(0(2(0(1(2(2(0(1(2(1(1(1(1(1(2(0(1(1(2(2(0(1(0(1(x1))))))))))))))))))))))))))))))))	→	1^#(0(1(1(1(0(1(1(2(0(1(1(1(1(x1))))))))))))))	(92)
1^#(1(2(2(0(1(2(1(2(1(2(2(0(2(0(0(2(2(1(1(0(1(0(0(0(2(1(1(1(1(2(1(2(0(2(2(x1))))))))))))))))))))))))))))))))))))	→	1^#(0(2(x1)))	(124)
1^#(1(2(2(0(1(2(1(2(1(2(2(0(2(0(0(2(2(1(1(0(1(0(0(0(2(1(1(1(1(2(1(2(0(2(2(x1))))))))))))))))))))))))))))))))))))	→	0^#(2(x1))	(125)
0^#(2(2(2(0(1(2(1(0(2(0(1(2(2(0(1(2(1(1(1(1(1(2(0(1(1(2(2(0(1(0(1(x1))))))))))))))))))))))))))))))))	→	0^#(1(1(1(0(1(1(2(0(1(1(1(1(x1)))))))))))))	(93)
0^#(2(2(2(0(1(2(1(0(2(0(1(2(2(0(1(2(1(1(1(1(1(2(0(1(1(2(2(0(1(0(1(x1))))))))))))))))))))))))))))))))	→	1^#(1(1(0(1(1(2(0(1(1(1(1(x1))))))))))))	(94)
0^#(2(2(2(0(1(2(1(0(2(0(1(2(2(0(1(2(1(1(1(1(1(2(0(1(1(2(2(0(1(0(1(x1))))))))))))))))))))))))))))))))	→	1^#(1(0(1(1(2(0(1(1(1(1(x1)))))))))))	(95)
0^#(2(2(2(0(1(2(1(0(2(0(1(2(2(0(1(2(1(1(1(1(1(2(0(1(1(2(2(0(1(0(1(x1))))))))))))))))))))))))))))))))	→	1^#(0(1(1(2(0(1(1(1(1(x1))))))))))	(96)
0^#(2(2(2(0(1(2(1(0(2(0(1(2(2(0(1(2(1(1(1(1(1(2(0(1(1(2(2(0(1(0(1(x1))))))))))))))))))))))))))))))))	→	0^#(1(1(2(0(1(1(1(1(x1)))))))))	(97)
0^#(2(2(2(0(1(2(1(0(2(0(1(2(2(0(1(2(1(1(1(1(1(2(0(1(1(2(2(0(1(0(1(x1))))))))))))))))))))))))))))))))	→	1^#(1(2(0(1(1(1(1(x1))))))))	(98)
0^#(2(2(2(0(1(2(1(0(2(0(1(2(2(0(1(2(1(1(1(1(1(2(0(1(1(2(2(0(1(0(1(x1))))))))))))))))))))))))))))))))	→	0^#(1(1(1(1(x1)))))	(100)
0^#(2(2(2(0(1(2(1(0(2(0(1(2(2(0(1(2(1(1(1(1(1(2(0(1(1(2(2(0(1(0(1(x1))))))))))))))))))))))))))))))))	→	1^#(1(1(1(x1))))	(101)
0^#(2(2(2(0(1(2(1(0(2(0(1(2(2(0(1(2(1(1(1(1(1(2(0(1(1(2(2(0(1(0(1(x1))))))))))))))))))))))))))))))))	→	1^#(1(1(x1)))	(102)
0^#(2(2(2(0(1(2(1(0(2(0(1(2(2(0(1(2(1(1(1(1(1(2(0(1(1(2(2(0(1(0(1(x1))))))))))))))))))))))))))))))))	→	1^#(1(x1))	(103)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	1^#(0(0(2(2(0(0(0(0(1(0(1(1(1(0(x1)))))))))))))))	(141)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(2(2(0(0(0(0(1(0(1(1(1(0(x1))))))))))))))	(142)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	0^#(2(2(0(0(0(0(1(0(1(1(1(0(x1)))))))))))))	(143)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(0(0(1(0(1(1(1(0(x1))))))))))	(144)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(0(1(0(1(1(1(0(x1)))))))))	(145)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(1(0(1(1(1(0(x1))))))))	(146)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	0^#(1(0(1(1(1(0(x1)))))))	(147)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	1^#(0(1(1(1(0(x1))))))	(148)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	0^#(1(1(1(0(x1)))))	(149)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	1^#(1(1(0(x1))))	(150)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	1^#(1(0(x1)))	(151)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	1^#(0(x1))	(152)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(2(0(0(1(0(0(0(0(1(0(0(0(0(2(2(0(0(2(0(0(2(0(0(x1))))))))))))))))))))))))	(168)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(1(0(0(0(0(1(0(0(0(0(2(2(0(0(2(0(0(2(0(0(x1))))))))))))))))))))))	(169)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(1(0(0(0(0(1(0(0(0(0(2(2(0(0(2(0(0(2(0(0(x1)))))))))))))))))))))	(170)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	1^#(0(0(0(0(1(0(0(0(0(2(2(0(0(2(0(0(2(0(0(x1))))))))))))))))))))	(171)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(0(0(1(0(0(0(0(2(2(0(0(2(0(0(2(0(0(x1)))))))))))))))))))	(172)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(0(1(0(0(0(0(2(2(0(0(2(0(0(2(0(0(x1))))))))))))))))))	(173)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(1(0(0(0(0(2(2(0(0(2(0(0(2(0(0(x1)))))))))))))))))	(174)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(1(0(0(0(0(2(2(0(0(2(0(0(2(0(0(x1))))))))))))))))	(175)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	1^#(0(0(0(0(2(2(0(0(2(0(0(2(0(0(x1)))))))))))))))	(176)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(0(0(2(2(0(0(2(0(0(2(0(0(x1))))))))))))))	(177)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(0(2(2(0(0(2(0(0(2(0(0(x1)))))))))))))	(178)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(2(2(0(0(2(0(0(2(0(0(x1))))))))))))	(179)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(2(2(0(0(2(0(0(2(0(0(x1)))))))))))	(180)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(2(0(0(2(0(0(x1))))))))	(181)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(2(0(0(2(0(0(x1)))))))	(182)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(2(0(0(x1)))))	(183)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(2(0(0(x1))))	(184)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(x1))	(185)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(x1)	(186)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(0(1(1(2(1(0(0(1(0(2(2(2(1(0(1(1(1(0(0(0(x1))))))))))))))))))))))	(202)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(1(1(2(1(0(0(1(0(2(2(2(1(0(1(1(1(0(0(0(x1)))))))))))))))))))))	(203)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(1(1(2(1(0(0(1(0(2(2(2(1(0(1(1(1(0(0(0(x1))))))))))))))))))))	(204)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	1^#(1(2(1(0(0(1(0(2(2(2(1(0(1(1(1(0(0(0(x1)))))))))))))))))))	(205)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	1^#(0(0(1(0(2(2(2(1(0(1(1(1(0(0(0(x1))))))))))))))))	(207)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(1(0(2(2(2(1(0(1(1(1(0(0(0(x1)))))))))))))))	(208)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(1(0(2(2(2(1(0(1(1(1(0(0(0(x1))))))))))))))	(209)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	1^#(0(2(2(2(1(0(1(1(1(0(0(0(x1)))))))))))))	(210)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(2(2(2(1(0(1(1(1(0(0(0(x1))))))))))))	(211)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	1^#(0(1(1(1(0(0(0(x1))))))))	(212)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(1(1(1(0(0(0(x1)))))))	(213)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	1^#(1(1(0(0(0(x1))))))	(214)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	1^#(1(0(0(0(x1)))))	(215)

1.1.1.1 Reduction Pair Processor

Using the linear polynomial interpretation over the naturals

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

the pairs

1^#(1(2(2(0(1(2(1(2(1(2(2(0(2(0(0(2(2(1(1(0(1(0(0(0(2(1(1(1(1(2(1(2(0(2(2(x1))))))))))))))))))))))))))))))))))))	→	1^#(1(1(1(2(0(2(1(0(2(x1))))))))))	(119)
1^#(1(2(2(0(1(2(1(2(1(2(2(0(2(0(0(2(2(1(1(0(1(0(0(0(2(1(1(1(1(2(1(2(0(2(2(x1))))))))))))))))))))))))))))))))))))	→	1^#(1(1(2(0(2(1(0(2(x1)))))))))	(120)
1^#(1(2(2(0(1(2(1(2(1(2(2(0(2(0(0(2(2(1(1(0(1(0(0(0(2(1(1(1(1(2(1(2(0(2(2(x1))))))))))))))))))))))))))))))))))))	→	1^#(1(2(0(2(1(0(2(x1))))))))	(121)
1^#(1(2(2(0(1(2(1(2(1(2(2(0(2(0(0(2(2(1(1(0(1(0(0(0(2(1(1(1(1(2(1(2(0(2(2(x1))))))))))))))))))))))))))))))))))))	→	0^#(2(1(0(2(x1)))))	(123)
0^#(2(2(2(0(1(2(1(0(2(0(1(2(2(0(1(2(1(1(1(1(1(2(0(1(1(2(2(0(1(0(1(x1))))))))))))))))))))))))))))))))	→	1^#(0(1(1(1(0(1(1(2(0(1(1(1(1(x1))))))))))))))	(92)
1^#(1(2(2(0(1(2(1(2(1(2(2(0(2(0(0(2(2(1(1(0(1(0(0(0(2(1(1(1(1(2(1(2(0(2(2(x1))))))))))))))))))))))))))))))))))))	→	1^#(0(2(x1)))	(124)
1^#(1(2(2(0(1(2(1(2(1(2(2(0(2(0(0(2(2(1(1(0(1(0(0(0(2(1(1(1(1(2(1(2(0(2(2(x1))))))))))))))))))))))))))))))))))))	→	0^#(2(x1))	(125)
0^#(2(2(2(0(1(2(1(0(2(0(1(2(2(0(1(2(1(1(1(1(1(2(0(1(1(2(2(0(1(0(1(x1))))))))))))))))))))))))))))))))	→	0^#(1(1(1(0(1(1(2(0(1(1(1(1(x1)))))))))))))	(93)
0^#(2(2(2(0(1(2(1(0(2(0(1(2(2(0(1(2(1(1(1(1(1(2(0(1(1(2(2(0(1(0(1(x1))))))))))))))))))))))))))))))))	→	1^#(1(1(0(1(1(2(0(1(1(1(1(x1))))))))))))	(94)
0^#(2(2(2(0(1(2(1(0(2(0(1(2(2(0(1(2(1(1(1(1(1(2(0(1(1(2(2(0(1(0(1(x1))))))))))))))))))))))))))))))))	→	1^#(1(0(1(1(2(0(1(1(1(1(x1)))))))))))	(95)
0^#(2(2(2(0(1(2(1(0(2(0(1(2(2(0(1(2(1(1(1(1(1(2(0(1(1(2(2(0(1(0(1(x1))))))))))))))))))))))))))))))))	→	1^#(0(1(1(2(0(1(1(1(1(x1))))))))))	(96)
0^#(2(2(2(0(1(2(1(0(2(0(1(2(2(0(1(2(1(1(1(1(1(2(0(1(1(2(2(0(1(0(1(x1))))))))))))))))))))))))))))))))	→	0^#(1(1(2(0(1(1(1(1(x1)))))))))	(97)
0^#(2(2(2(0(1(2(1(0(2(0(1(2(2(0(1(2(1(1(1(1(1(2(0(1(1(2(2(0(1(0(1(x1))))))))))))))))))))))))))))))))	→	1^#(1(2(0(1(1(1(1(x1))))))))	(98)
0^#(2(2(2(0(1(2(1(0(2(0(1(2(2(0(1(2(1(1(1(1(1(2(0(1(1(2(2(0(1(0(1(x1))))))))))))))))))))))))))))))))	→	0^#(1(1(1(1(x1)))))	(100)
0^#(2(2(2(0(1(2(1(0(2(0(1(2(2(0(1(2(1(1(1(1(1(2(0(1(1(2(2(0(1(0(1(x1))))))))))))))))))))))))))))))))	→	1^#(1(1(1(x1))))	(101)
0^#(2(2(2(0(1(2(1(0(2(0(1(2(2(0(1(2(1(1(1(1(1(2(0(1(1(2(2(0(1(0(1(x1))))))))))))))))))))))))))))))))	→	1^#(1(1(x1)))	(102)
0^#(2(2(2(0(1(2(1(0(2(0(1(2(2(0(1(2(1(1(1(1(1(2(0(1(1(2(2(0(1(0(1(x1))))))))))))))))))))))))))))))))	→	1^#(1(x1))	(103)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	1^#(0(0(2(2(0(0(0(0(1(0(1(1(1(0(x1)))))))))))))))	(141)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(2(2(0(0(0(0(1(0(1(1(1(0(x1))))))))))))))	(142)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	0^#(2(2(0(0(0(0(1(0(1(1(1(0(x1)))))))))))))	(143)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(0(0(1(0(1(1(1(0(x1))))))))))	(144)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(0(1(0(1(1(1(0(x1)))))))))	(145)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(1(0(1(1(1(0(x1))))))))	(146)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	0^#(1(0(1(1(1(0(x1)))))))	(147)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	1^#(0(1(1(1(0(x1))))))	(148)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	0^#(1(1(1(0(x1)))))	(149)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	1^#(1(1(0(x1))))	(150)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	1^#(1(0(x1)))	(151)
0^#(2(2(2(1(2(2(0(2(0(2(0(0(0(2(0(0(1(1(2(1(1(1(0(1(2(2(2(1(0(1(2(2(0(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))))	→	1^#(0(x1))	(152)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(2(0(0(1(0(0(0(0(1(0(0(0(0(2(2(0(0(2(0(0(2(0(0(x1))))))))))))))))))))))))	(168)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(1(0(0(0(0(1(0(0(0(0(2(2(0(0(2(0(0(2(0(0(x1))))))))))))))))))))))	(169)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(1(0(0(0(0(1(0(0(0(0(2(2(0(0(2(0(0(2(0(0(x1)))))))))))))))))))))	(170)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	1^#(0(0(0(0(1(0(0(0(0(2(2(0(0(2(0(0(2(0(0(x1))))))))))))))))))))	(171)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(0(0(1(0(0(0(0(2(2(0(0(2(0(0(2(0(0(x1)))))))))))))))))))	(172)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(0(1(0(0(0(0(2(2(0(0(2(0(0(2(0(0(x1))))))))))))))))))	(173)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(1(0(0(0(0(2(2(0(0(2(0(0(2(0(0(x1)))))))))))))))))	(174)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(1(0(0(0(0(2(2(0(0(2(0(0(2(0(0(x1))))))))))))))))	(175)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	1^#(0(0(0(0(2(2(0(0(2(0(0(2(0(0(x1)))))))))))))))	(176)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(0(0(2(2(0(0(2(0(0(2(0(0(x1))))))))))))))	(177)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(0(2(2(0(0(2(0(0(2(0(0(x1)))))))))))))	(178)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(2(2(0(0(2(0(0(2(0(0(x1))))))))))))	(179)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(2(2(0(0(2(0(0(2(0(0(x1)))))))))))	(180)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(2(0(0(2(0(0(x1))))))))	(181)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(2(0(0(2(0(0(x1)))))))	(182)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(2(0(0(x1)))))	(183)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(2(0(0(x1))))	(184)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(x1))	(185)
0^#(2(2(0(0(2(0(0(1(0(1(0(1(0(1(2(0(2(0(0(0(0(2(2(0(0(1(0(0(0(0(1(2(0(1(0(2(0(0(0(2(0(2(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(x1)	(186)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(0(1(1(2(1(0(0(1(0(2(2(2(1(0(1(1(1(0(0(0(x1))))))))))))))))))))))	(202)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(1(1(2(1(0(0(1(0(2(2(2(1(0(1(1(1(0(0(0(x1)))))))))))))))))))))	(203)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(1(1(2(1(0(0(1(0(2(2(2(1(0(1(1(1(0(0(0(x1))))))))))))))))))))	(204)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	1^#(1(2(1(0(0(1(0(2(2(2(1(0(1(1(1(0(0(0(x1)))))))))))))))))))	(205)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	1^#(0(0(1(0(2(2(2(1(0(1(1(1(0(0(0(x1))))))))))))))))	(207)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(0(1(0(2(2(2(1(0(1(1(1(0(0(0(x1)))))))))))))))	(208)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(1(0(2(2(2(1(0(1(1(1(0(0(0(x1))))))))))))))	(209)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	1^#(0(2(2(2(1(0(1(1(1(0(0(0(x1)))))))))))))	(210)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(2(2(2(1(0(1(1(1(0(0(0(x1))))))))))))	(211)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	1^#(0(1(1(1(0(0(0(x1))))))))	(212)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	0^#(1(1(1(0(0(0(x1)))))))	(213)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	1^#(1(1(0(0(0(x1))))))	(214)
0^#(0(0(2(1(1(2(0(1(1(0(2(0(1(1(2(2(1(2(2(1(2(2(1(0(1(0(0(2(1(1(1(0(1(1(0(2(2(2(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))	→	1^#(1(0(0(0(x1)))))	(215)

could be deleted.

1.1.1.1.1 P is empty

There are no pairs anymore.