Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/140654)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Closure Under Flat Contexts

Using the flat contexts

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

We obtain the transformed TRS
0(0(0(1(2(1(1(1(0(0(1(0(1(x1))))))))))))) → 0(0(1(0(1(1(0(2(0(0(2(0(1(0(1(0(1(x1))))))))))))))))) (1)
0(0(1(0(0(1(1(1(0(1(2(0(1(x1))))))))))))) → 0(1(1(0(0(1(0(1(1(1(1(0(2(0(1(1(1(x1))))))))))))))))) (2)
0(0(1(0(1(0(1(0(0(1(0(2(0(x1))))))))))))) → 0(1(1(1(0(1(1(2(1(2(0(1(1(1(0(1(1(x1))))))))))))))))) (3)
0(0(1(1(1(1(1(2(1(1(2(1(1(x1))))))))))))) → 0(1(2(0(1(0(0(1(2(1(0(0(1(0(1(1(1(x1))))))))))))))))) (4)
0(1(0(2(0(2(1(0(0(1(0(1(1(x1))))))))))))) → 0(0(0(1(1(1(1(1(0(2(2(0(1(1(1(0(1(x1))))))))))))))))) (5)
0(1(0(2(2(1(1(2(1(2(2(0(1(x1))))))))))))) → 0(1(2(2(0(0(1(0(1(0(2(1(0(2(2(0(1(x1))))))))))))))))) (6)
0(1(1(0(1(1(0(1(0(2(1(0(0(x1))))))))))))) → 0(1(2(0(1(1(0(1(1(1(1(1(0(0(1(0(0(x1))))))))))))))))) (7)
0(1(1(1(2(1(2(0(1(2(1(0(1(x1))))))))))))) → 0(1(0(1(0(1(1(0(0(1(0(2(0(1(0(0(1(x1))))))))))))))))) (8)
0(2(0(0(1(1(2(0(1(0(1(0(2(x1))))))))))))) → 0(0(1(2(0(0(1(0(1(0(1(1(0(0(1(1(1(x1))))))))))))))))) (9)
1(0(2(0(0(2(0(1(2(0(1(0(1(x1))))))))))))) → 1(1(0(0(1(0(2(1(2(0(1(1(1(0(1(1(1(x1))))))))))))))))) (10)
1(0(2(0(2(1(0(2(0(1(1(2(0(x1))))))))))))) → 1(2(0(2(0(0(1(0(1(0(0(0(1(2(0(1(0(x1))))))))))))))))) (11)
1(1(0(0(2(2(2(0(1(2(0(1(1(x1))))))))))))) → 1(0(1(1(1(0(0(1(2(0(1(2(0(0(0(0(1(x1))))))))))))))))) (12)
1(2(0(1(0(2(0(1(0(1(2(1(0(x1))))))))))))) → 1(0(1(1(2(0(1(0(0(1(0(0(1(0(1(2(0(x1))))))))))))))))) (13)
1(2(1(2(0(0(0(1(1(1(0(0(1(x1))))))))))))) → 1(1(1(1(0(2(0(1(1(0(1(1(2(2(0(0(1(x1))))))))))))))))) (14)
2(0(0(0(2(2(0(2(2(0(1(0(1(x1))))))))))))) → 2(0(0(1(1(2(1(1(2(0(0(1(2(1(2(0(1(x1))))))))))))))))) (15)
2(0(2(1(1(1(1(0(2(0(1(0(1(x1))))))))))))) → 2(1(2(0(2(0(1(0(1(2(0(1(0(1(1(1(1(x1))))))))))))))))) (17)
2(1(2(2(1(1(2(2(0(1(1(0(1(x1))))))))))))) → 2(1(1(1(2(0(1(2(2(0(0(0(1(1(1(0(1(x1))))))))))))))))) (18)
0(2(0(2(1(0(0(1(0(0(0(1(1(1(x1)))))))))))))) → 0(0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x1)))))))))))))))))) (20)
1(2(0(2(1(0(0(1(0(0(0(1(1(1(x1)))))))))))))) → 1(0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x1)))))))))))))))))) (21)
2(2(0(2(1(0(0(1(0(0(0(1(1(1(x1)))))))))))))) → 2(0(2(1(2(1(0(1(1(1(0(1(0(1(0(0(1(1(x1)))))))))))))))))) (22)
0(2(2(1(1(1(1(0(1(1(2(0(1(0(x1)))))))))))))) → 0(0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x1)))))))))))))))))) (23)
1(2(2(1(1(1(1(0(1(1(2(0(1(0(x1)))))))))))))) → 1(0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x1)))))))))))))))))) (24)
2(2(2(1(1(1(1(0(1(1(2(0(1(0(x1)))))))))))))) → 2(0(1(0(1(1(1(1(1(2(2(0(1(2(1(1(1(0(x1)))))))))))))))))) (25)

1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS
00(00(01(12(21(11(11(10(00(01(10(01(10(x1))))))))))))) → 00(01(10(01(11(10(02(20(00(02(20(01(10(01(10(01(10(x1))))))))))))))))) (26)
00(00(01(12(21(11(11(10(00(01(10(01(11(x1))))))))))))) → 00(01(10(01(11(10(02(20(00(02(20(01(10(01(10(01(11(x1))))))))))))))))) (27)
00(00(01(12(21(11(11(10(00(01(10(01(12(x1))))))))))))) → 00(01(10(01(11(10(02(20(00(02(20(01(10(01(10(01(12(x1))))))))))))))))) (28)
00(01(10(00(01(11(11(10(01(12(20(01(10(x1))))))))))))) → 01(11(10(00(01(10(01(11(11(11(10(02(20(01(11(11(10(x1))))))))))))))))) (29)
00(01(10(00(01(11(11(10(01(12(20(01(11(x1))))))))))))) → 01(11(10(00(01(10(01(11(11(11(10(02(20(01(11(11(11(x1))))))))))))))))) (30)
00(01(10(00(01(11(11(10(01(12(20(01(12(x1))))))))))))) → 01(11(10(00(01(10(01(11(11(11(10(02(20(01(11(11(12(x1))))))))))))))))) (31)
00(01(10(01(10(01(10(00(01(10(02(20(00(x1))))))))))))) → 01(11(11(10(01(11(12(21(12(20(01(11(11(10(01(11(10(x1))))))))))))))))) (32)
00(01(10(01(10(01(10(00(01(10(02(20(01(x1))))))))))))) → 01(11(11(10(01(11(12(21(12(20(01(11(11(10(01(11(11(x1))))))))))))))))) (33)
00(01(10(01(10(01(10(00(01(10(02(20(02(x1))))))))))))) → 01(11(11(10(01(11(12(21(12(20(01(11(11(10(01(11(12(x1))))))))))))))))) (34)
00(01(11(11(11(11(12(21(11(12(21(11(10(x1))))))))))))) → 01(12(20(01(10(00(01(12(21(10(00(01(10(01(11(11(10(x1))))))))))))))))) (35)
00(01(11(11(11(11(12(21(11(12(21(11(11(x1))))))))))))) → 01(12(20(01(10(00(01(12(21(10(00(01(10(01(11(11(11(x1))))))))))))))))) (36)
00(01(11(11(11(11(12(21(11(12(21(11(12(x1))))))))))))) → 01(12(20(01(10(00(01(12(21(10(00(01(10(01(11(11(12(x1))))))))))))))))) (37)
01(10(02(20(02(21(10(00(01(10(01(11(10(x1))))))))))))) → 00(00(01(11(11(11(11(10(02(22(20(01(11(11(10(01(10(x1))))))))))))))))) (38)
01(10(02(20(02(21(10(00(01(10(01(11(11(x1))))))))))))) → 00(00(01(11(11(11(11(10(02(22(20(01(11(11(10(01(11(x1))))))))))))))))) (39)
01(10(02(20(02(21(10(00(01(10(01(11(12(x1))))))))))))) → 00(00(01(11(11(11(11(10(02(22(20(01(11(11(10(01(12(x1))))))))))))))))) (40)
01(10(02(22(21(11(12(21(12(22(20(01(10(x1))))))))))))) → 01(12(22(20(00(01(10(01(10(02(21(10(02(22(20(01(10(x1))))))))))))))))) (41)
01(10(02(22(21(11(12(21(12(22(20(01(11(x1))))))))))))) → 01(12(22(20(00(01(10(01(10(02(21(10(02(22(20(01(11(x1))))))))))))))))) (42)
01(10(02(22(21(11(12(21(12(22(20(01(12(x1))))))))))))) → 01(12(22(20(00(01(10(01(10(02(21(10(02(22(20(01(12(x1))))))))))))))))) (43)
01(11(10(01(11(10(01(10(02(21(10(00(00(x1))))))))))))) → 01(12(20(01(11(10(01(11(11(11(11(10(00(01(10(00(00(x1))))))))))))))))) (44)
01(11(10(01(11(10(01(10(02(21(10(00(01(x1))))))))))))) → 01(12(20(01(11(10(01(11(11(11(11(10(00(01(10(00(01(x1))))))))))))))))) (45)
01(11(10(01(11(10(01(10(02(21(10(00(02(x1))))))))))))) → 01(12(20(01(11(10(01(11(11(11(11(10(00(01(10(00(02(x1))))))))))))))))) (46)
01(11(11(12(21(12(20(01(12(21(10(01(10(x1))))))))))))) → 01(10(01(10(01(11(10(00(01(10(02(20(01(10(00(01(10(x1))))))))))))))))) (47)
01(11(11(12(21(12(20(01(12(21(10(01(11(x1))))))))))))) → 01(10(01(10(01(11(10(00(01(10(02(20(01(10(00(01(11(x1))))))))))))))))) (48)
01(11(11(12(21(12(20(01(12(21(10(01(12(x1))))))))))))) → 01(10(01(10(01(11(10(00(01(10(02(20(01(10(00(01(12(x1))))))))))))))))) (49)
02(20(00(01(11(12(20(01(10(01(10(02(20(x1))))))))))))) → 00(01(12(20(00(01(10(01(10(01(11(10(00(01(11(11(10(x1))))))))))))))))) (50)
02(20(00(01(11(12(20(01(10(01(10(02(21(x1))))))))))))) → 00(01(12(20(00(01(10(01(10(01(11(10(00(01(11(11(11(x1))))))))))))))))) (51)
02(20(00(01(11(12(20(01(10(01(10(02(22(x1))))))))))))) → 00(01(12(20(00(01(10(01(10(01(11(10(00(01(11(11(12(x1))))))))))))))))) (52)
10(02(20(00(02(20(01(12(20(01(10(01(10(x1))))))))))))) → 11(10(00(01(10(02(21(12(20(01(11(11(10(01(11(11(10(x1))))))))))))))))) (53)
10(02(20(00(02(20(01(12(20(01(10(01(11(x1))))))))))))) → 11(10(00(01(10(02(21(12(20(01(11(11(10(01(11(11(11(x1))))))))))))))))) (54)
10(02(20(00(02(20(01(12(20(01(10(01(12(x1))))))))))))) → 11(10(00(01(10(02(21(12(20(01(11(11(10(01(11(11(12(x1))))))))))))))))) (55)
10(02(20(02(21(10(02(20(01(11(12(20(00(x1))))))))))))) → 12(20(02(20(00(01(10(01(10(00(00(01(12(20(01(10(00(x1))))))))))))))))) (56)
10(02(20(02(21(10(02(20(01(11(12(20(01(x1))))))))))))) → 12(20(02(20(00(01(10(01(10(00(00(01(12(20(01(10(01(x1))))))))))))))))) (57)
10(02(20(02(21(10(02(20(01(11(12(20(02(x1))))))))))))) → 12(20(02(20(00(01(10(01(10(00(00(01(12(20(01(10(02(x1))))))))))))))))) (58)
11(10(00(02(22(22(20(01(12(20(01(11(10(x1))))))))))))) → 10(01(11(11(10(00(01(12(20(01(12(20(00(00(00(01(10(x1))))))))))))))))) (59)
11(10(00(02(22(22(20(01(12(20(01(11(11(x1))))))))))))) → 10(01(11(11(10(00(01(12(20(01(12(20(00(00(00(01(11(x1))))))))))))))))) (60)
11(10(00(02(22(22(20(01(12(20(01(11(12(x1))))))))))))) → 10(01(11(11(10(00(01(12(20(01(12(20(00(00(00(01(12(x1))))))))))))))))) (61)
12(20(01(10(02(20(01(10(01(12(21(10(00(x1))))))))))))) → 10(01(11(12(20(01(10(00(01(10(00(01(10(01(12(20(00(x1))))))))))))))))) (62)
12(20(01(10(02(20(01(10(01(12(21(10(01(x1))))))))))))) → 10(01(11(12(20(01(10(00(01(10(00(01(10(01(12(20(01(x1))))))))))))))))) (63)
12(20(01(10(02(20(01(10(01(12(21(10(02(x1))))))))))))) → 10(01(11(12(20(01(10(00(01(10(00(01(10(01(12(20(02(x1))))))))))))))))) (64)
12(21(12(20(00(00(01(11(11(10(00(01(10(x1))))))))))))) → 11(11(11(10(02(20(01(11(10(01(11(12(22(20(00(01(10(x1))))))))))))))))) (65)
12(21(12(20(00(00(01(11(11(10(00(01(11(x1))))))))))))) → 11(11(11(10(02(20(01(11(10(01(11(12(22(20(00(01(11(x1))))))))))))))))) (66)
12(21(12(20(00(00(01(11(11(10(00(01(12(x1))))))))))))) → 11(11(11(10(02(20(01(11(10(01(11(12(22(20(00(01(12(x1))))))))))))))))) (67)
20(00(00(02(22(20(02(22(20(01(10(01(10(x1))))))))))))) → 20(00(01(11(12(21(11(12(20(00(01(12(21(12(20(01(10(x1))))))))))))))))) (68)
20(00(00(02(22(20(02(22(20(01(10(01(11(x1))))))))))))) → 20(00(01(11(12(21(11(12(20(00(01(12(21(12(20(01(11(x1))))))))))))))))) (69)
20(00(00(02(22(20(02(22(20(01(10(01(12(x1))))))))))))) → 20(00(01(11(12(21(11(12(20(00(01(12(21(12(20(01(12(x1))))))))))))))))) (70)
20(02(21(11(11(11(10(02(20(01(10(01(10(x1))))))))))))) → 21(12(20(02(20(01(10(01(12(20(01(10(01(11(11(11(10(x1))))))))))))))))) (71)
20(02(21(11(11(11(10(02(20(01(10(01(11(x1))))))))))))) → 21(12(20(02(20(01(10(01(12(20(01(10(01(11(11(11(11(x1))))))))))))))))) (72)
20(02(21(11(11(11(10(02(20(01(10(01(12(x1))))))))))))) → 21(12(20(02(20(01(10(01(12(20(01(10(01(11(11(11(12(x1))))))))))))))))) (73)
21(12(22(21(11(12(22(20(01(11(10(01(10(x1))))))))))))) → 21(11(11(12(20(01(12(22(20(00(00(01(11(11(10(01(10(x1))))))))))))))))) (74)
21(12(22(21(11(12(22(20(01(11(10(01(11(x1))))))))))))) → 21(11(11(12(20(01(12(22(20(00(00(01(11(11(10(01(11(x1))))))))))))))))) (75)
21(12(22(21(11(12(22(20(01(11(10(01(12(x1))))))))))))) → 21(11(11(12(20(01(12(22(20(00(00(01(11(11(10(01(12(x1))))))))))))))))) (76)
02(20(02(21(10(00(01(10(00(00(01(11(11(10(x1)))))))))))))) → 00(02(21(12(21(10(01(11(11(10(01(10(01(10(00(01(11(10(x1)))))))))))))))))) (77)
02(20(02(21(10(00(01(10(00(00(01(11(11(11(x1)))))))))))))) → 00(02(21(12(21(10(01(11(11(10(01(10(01(10(00(01(11(11(x1)))))))))))))))))) (78)
02(20(02(21(10(00(01(10(00(00(01(11(11(12(x1)))))))))))))) → 00(02(21(12(21(10(01(11(11(10(01(10(01(10(00(01(11(12(x1)))))))))))))))))) (79)
12(20(02(21(10(00(01(10(00(00(01(11(11(10(x1)))))))))))))) → 10(02(21(12(21(10(01(11(11(10(01(10(01(10(00(01(11(10(x1)))))))))))))))))) (80)
12(20(02(21(10(00(01(10(00(00(01(11(11(11(x1)))))))))))))) → 10(02(21(12(21(10(01(11(11(10(01(10(01(10(00(01(11(11(x1)))))))))))))))))) (81)
12(20(02(21(10(00(01(10(00(00(01(11(11(12(x1)))))))))))))) → 10(02(21(12(21(10(01(11(11(10(01(10(01(10(00(01(11(12(x1)))))))))))))))))) (82)
22(20(02(21(10(00(01(10(00(00(01(11(11(10(x1)))))))))))))) → 20(02(21(12(21(10(01(11(11(10(01(10(01(10(00(01(11(10(x1)))))))))))))))))) (83)
22(20(02(21(10(00(01(10(00(00(01(11(11(11(x1)))))))))))))) → 20(02(21(12(21(10(01(11(11(10(01(10(01(10(00(01(11(11(x1)))))))))))))))))) (84)
22(20(02(21(10(00(01(10(00(00(01(11(11(12(x1)))))))))))))) → 20(02(21(12(21(10(01(11(11(10(01(10(01(10(00(01(11(12(x1)))))))))))))))))) (85)
02(22(21(11(11(11(10(01(11(12(20(01(10(00(x1)))))))))))))) → 00(01(10(01(11(11(11(11(12(22(20(01(12(21(11(11(10(00(x1)))))))))))))))))) (86)
02(22(21(11(11(11(10(01(11(12(20(01(10(01(x1)))))))))))))) → 00(01(10(01(11(11(11(11(12(22(20(01(12(21(11(11(10(01(x1)))))))))))))))))) (87)
02(22(21(11(11(11(10(01(11(12(20(01(10(02(x1)))))))))))))) → 00(01(10(01(11(11(11(11(12(22(20(01(12(21(11(11(10(02(x1)))))))))))))))))) (88)
12(22(21(11(11(11(10(01(11(12(20(01(10(00(x1)))))))))))))) → 10(01(10(01(11(11(11(11(12(22(20(01(12(21(11(11(10(00(x1)))))))))))))))))) (89)
12(22(21(11(11(11(10(01(11(12(20(01(10(01(x1)))))))))))))) → 10(01(10(01(11(11(11(11(12(22(20(01(12(21(11(11(10(01(x1)))))))))))))))))) (90)
12(22(21(11(11(11(10(01(11(12(20(01(10(02(x1)))))))))))))) → 10(01(10(01(11(11(11(11(12(22(20(01(12(21(11(11(10(02(x1)))))))))))))))))) (91)
22(22(21(11(11(11(10(01(11(12(20(01(10(00(x1)))))))))))))) → 20(01(10(01(11(11(11(11(12(22(20(01(12(21(11(11(10(00(x1)))))))))))))))))) (92)
22(22(21(11(11(11(10(01(11(12(20(01(10(01(x1)))))))))))))) → 20(01(10(01(11(11(11(11(12(22(20(01(12(21(11(11(10(01(x1)))))))))))))))))) (93)
22(22(21(11(11(11(10(01(11(12(20(01(10(02(x1)))))))))))))) → 20(01(10(01(11(11(11(11(12(22(20(01(12(21(11(11(10(02(x1)))))))))))))))))) (94)

1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[00(x1)] = 1 · x1 + 1
[01(x1)] = 1 · x1
[12(x1)] = 1 · x1 + 1
[21(x1)] = 1 · x1 + 2
[11(x1)] = 1 · x1
[10(x1)] = 1 · x1
[02(x1)] = 1 · x1 + 2
[20(x1)] = 1 · x1
[22(x1)] = 1 · x1 + 2
all of the following rules can be deleted.
00(01(10(01(10(01(10(00(01(10(02(20(00(x1))))))))))))) → 01(11(11(10(01(11(12(21(12(20(01(11(11(10(01(11(10(x1))))))))))))))))) (32)
00(01(10(01(10(01(10(00(01(10(02(20(02(x1))))))))))))) → 01(11(11(10(01(11(12(21(12(20(01(11(11(10(01(11(12(x1))))))))))))))))) (34)
00(01(11(11(11(11(12(21(11(12(21(11(10(x1))))))))))))) → 01(12(20(01(10(00(01(12(21(10(00(01(10(01(11(11(10(x1))))))))))))))))) (35)
00(01(11(11(11(11(12(21(11(12(21(11(11(x1))))))))))))) → 01(12(20(01(10(00(01(12(21(10(00(01(10(01(11(11(11(x1))))))))))))))))) (36)
00(01(11(11(11(11(12(21(11(12(21(11(12(x1))))))))))))) → 01(12(20(01(10(00(01(12(21(10(00(01(10(01(11(11(12(x1))))))))))))))))) (37)
01(10(02(20(02(21(10(00(01(10(01(11(10(x1))))))))))))) → 00(00(01(11(11(11(11(10(02(22(20(01(11(11(10(01(10(x1))))))))))))))))) (38)
01(10(02(20(02(21(10(00(01(10(01(11(11(x1))))))))))))) → 00(00(01(11(11(11(11(10(02(22(20(01(11(11(10(01(11(x1))))))))))))))))) (39)
01(10(02(20(02(21(10(00(01(10(01(11(12(x1))))))))))))) → 00(00(01(11(11(11(11(10(02(22(20(01(11(11(10(01(12(x1))))))))))))))))) (40)
01(11(10(01(11(10(01(10(02(21(10(00(00(x1))))))))))))) → 01(12(20(01(11(10(01(11(11(11(11(10(00(01(10(00(00(x1))))))))))))))))) (44)
01(11(10(01(11(10(01(10(02(21(10(00(01(x1))))))))))))) → 01(12(20(01(11(10(01(11(11(11(11(10(00(01(10(00(01(x1))))))))))))))))) (45)
01(11(10(01(11(10(01(10(02(21(10(00(02(x1))))))))))))) → 01(12(20(01(11(10(01(11(11(11(11(10(00(01(10(00(02(x1))))))))))))))))) (46)
01(11(11(12(21(12(20(01(12(21(10(01(10(x1))))))))))))) → 01(10(01(10(01(11(10(00(01(10(02(20(01(10(00(01(10(x1))))))))))))))))) (47)
01(11(11(12(21(12(20(01(12(21(10(01(11(x1))))))))))))) → 01(10(01(10(01(11(10(00(01(10(02(20(01(10(00(01(11(x1))))))))))))))))) (48)
01(11(11(12(21(12(20(01(12(21(10(01(12(x1))))))))))))) → 01(10(01(10(01(11(10(00(01(10(02(20(01(10(00(01(12(x1))))))))))))))))) (49)
02(20(00(01(11(12(20(01(10(01(10(02(20(x1))))))))))))) → 00(01(12(20(00(01(10(01(10(01(11(10(00(01(11(11(10(x1))))))))))))))))) (50)
02(20(00(01(11(12(20(01(10(01(10(02(21(x1))))))))))))) → 00(01(12(20(00(01(10(01(10(01(11(10(00(01(11(11(11(x1))))))))))))))))) (51)
02(20(00(01(11(12(20(01(10(01(10(02(22(x1))))))))))))) → 00(01(12(20(00(01(10(01(10(01(11(10(00(01(11(11(12(x1))))))))))))))))) (52)
10(02(20(02(21(10(02(20(01(11(12(20(00(x1))))))))))))) → 12(20(02(20(00(01(10(01(10(00(00(01(12(20(01(10(00(x1))))))))))))))))) (56)
10(02(20(02(21(10(02(20(01(11(12(20(01(x1))))))))))))) → 12(20(02(20(00(01(10(01(10(00(00(01(12(20(01(10(01(x1))))))))))))))))) (57)
10(02(20(02(21(10(02(20(01(11(12(20(02(x1))))))))))))) → 12(20(02(20(00(01(10(01(10(00(00(01(12(20(01(10(02(x1))))))))))))))))) (58)
11(10(00(02(22(22(20(01(12(20(01(11(10(x1))))))))))))) → 10(01(11(11(10(00(01(12(20(01(12(20(00(00(00(01(10(x1))))))))))))))))) (59)
11(10(00(02(22(22(20(01(12(20(01(11(11(x1))))))))))))) → 10(01(11(11(10(00(01(12(20(01(12(20(00(00(00(01(11(x1))))))))))))))))) (60)
11(10(00(02(22(22(20(01(12(20(01(11(12(x1))))))))))))) → 10(01(11(11(10(00(01(12(20(01(12(20(00(00(00(01(12(x1))))))))))))))))) (61)
12(20(01(10(02(20(01(10(01(12(21(10(00(x1))))))))))))) → 10(01(11(12(20(01(10(00(01(10(00(01(10(01(12(20(00(x1))))))))))))))))) (62)
12(20(01(10(02(20(01(10(01(12(21(10(01(x1))))))))))))) → 10(01(11(12(20(01(10(00(01(10(00(01(10(01(12(20(01(x1))))))))))))))))) (63)
12(20(01(10(02(20(01(10(01(12(21(10(02(x1))))))))))))) → 10(01(11(12(20(01(10(00(01(10(00(01(10(01(12(20(02(x1))))))))))))))))) (64)
12(21(12(20(00(00(01(11(11(10(00(01(10(x1))))))))))))) → 11(11(11(10(02(20(01(11(10(01(11(12(22(20(00(01(10(x1))))))))))))))))) (65)
12(21(12(20(00(00(01(11(11(10(00(01(11(x1))))))))))))) → 11(11(11(10(02(20(01(11(10(01(11(12(22(20(00(01(11(x1))))))))))))))))) (66)
12(21(12(20(00(00(01(11(11(10(00(01(12(x1))))))))))))) → 11(11(11(10(02(20(01(11(10(01(11(12(22(20(00(01(12(x1))))))))))))))))) (67)
21(12(22(21(11(12(22(20(01(11(10(01(10(x1))))))))))))) → 21(11(11(12(20(01(12(22(20(00(00(01(11(11(10(01(10(x1))))))))))))))))) (74)
21(12(22(21(11(12(22(20(01(11(10(01(11(x1))))))))))))) → 21(11(11(12(20(01(12(22(20(00(00(01(11(11(10(01(11(x1))))))))))))))))) (75)
21(12(22(21(11(12(22(20(01(11(10(01(12(x1))))))))))))) → 21(11(11(12(20(01(12(22(20(00(00(01(11(11(10(01(12(x1))))))))))))))))) (76)
22(20(02(21(10(00(01(10(00(00(01(11(11(10(x1)))))))))))))) → 20(02(21(12(21(10(01(11(11(10(01(10(01(10(00(01(11(10(x1)))))))))))))))))) (83)
22(20(02(21(10(00(01(10(00(00(01(11(11(11(x1)))))))))))))) → 20(02(21(12(21(10(01(11(11(10(01(10(01(10(00(01(11(11(x1)))))))))))))))))) (84)
22(20(02(21(10(00(01(10(00(00(01(11(11(12(x1)))))))))))))) → 20(02(21(12(21(10(01(11(11(10(01(10(01(10(00(01(11(12(x1)))))))))))))))))) (85)
22(22(21(11(11(11(10(01(11(12(20(01(10(00(x1)))))))))))))) → 20(01(10(01(11(11(11(11(12(22(20(01(12(21(11(11(10(00(x1)))))))))))))))))) (92)
22(22(21(11(11(11(10(01(11(12(20(01(10(01(x1)))))))))))))) → 20(01(10(01(11(11(11(11(12(22(20(01(12(21(11(11(10(01(x1)))))))))))))))))) (93)
22(22(21(11(11(11(10(01(11(12(20(01(10(02(x1)))))))))))))) → 20(01(10(01(11(11(11(11(12(22(20(01(12(21(11(11(10(02(x1)))))))))))))))))) (94)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[00(x1)] = 1 · x1
[01(x1)] = 1 · x1
[12(x1)] = 1 · x1
[21(x1)] = 1 · x1
[11(x1)] = 1 · x1
[10(x1)] = 1 · x1
[02(x1)] = 1 · x1
[20(x1)] = 1 · x1
[22(x1)] = 1 · x1 + 1
all of the following rules can be deleted.
20(00(00(02(22(20(02(22(20(01(10(01(10(x1))))))))))))) → 20(00(01(11(12(21(11(12(20(00(01(12(21(12(20(01(10(x1))))))))))))))))) (68)
20(00(00(02(22(20(02(22(20(01(10(01(11(x1))))))))))))) → 20(00(01(11(12(21(11(12(20(00(01(12(21(12(20(01(11(x1))))))))))))))))) (69)
20(00(00(02(22(20(02(22(20(01(10(01(12(x1))))))))))))) → 20(00(01(11(12(21(11(12(20(00(01(12(21(12(20(01(12(x1))))))))))))))))) (70)

1.1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

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

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.