Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/149277)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by matchbox @ termCOMP 2023)

1 Closure Under Flat Contexts

Using the flat contexts

{2(), 1(), 0()}

We obtain the transformed TRS

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

1.1 Closure Under Flat Contexts

Using the flat contexts

{2(), 1(), 0()}

We obtain the transformed TRS

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

1.1.1 Semantic Labeling

The following interpretations form a model of the rules.

As carrier we take the set {0,...,8}. Symbols are labeled by the interpretation of their arguments using the interpretations (modulo 9):

[2(x1)] = 3x1 + 0
[1(x1)] = 3x1 + 1
[0(x1)] = 3x1 + 2

We obtain the labeled TRS

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

1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[20(x1)] = x1 +
628361015/164799
[23(x1)] = x1 +
904417963/329598
[26(x1)] = x1 +
560718811/329598
[21(x1)] = x1 +
500438207/164799
[24(x1)] = x1 +
1263845009/329598
[27(x1)] = x1 +
804104225/329598
[22(x1)] = x1 +
341494441/329598
[25(x1)] = x1 +
417624331/329598
[28(x1)] = x1 +
102260225/109866
[10(x1)] = x1 +
19236238/164799
[13(x1)] = x1 +
191085814/164799
[16(x1)] = x1 +
19236238/164799
[11(x1)] = x1 +
371/18
[14(x1)] = x1 +
1
[17(x1)] = x1 +
389/18
[12(x1)] = x1 +
72809149/164799
[15(x1)] = x1 +
0
[18(x1)] = x1 +
1098690379/659196
[00(x1)] = x1 +
628525814/164799
[03(x1)] = x1 +
1263515411/329598
[06(x1)] = x1 +
628361015/164799
[01(x1)] = x1 +
840079147/219732
[04(x1)] = x1 +
0
[07(x1)] = x1 +
226/9
[02(x1)] = x1 +
628361015/164799
[05(x1)] = x1 +
0
[08(x1)] = x1 +
149382878/54933
all of the following rules can be deleted.

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

1.1.1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.