Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/264033)

The rewrite relation of the following TRS is considered.

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

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

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

1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS

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

1.1.1 Rule Removal

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

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

1.1.1.1 Rule Removal

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

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

1.1.1.1.1 Rule Removal

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

1.1.1.1.1.1 R is empty

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