Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/247906)

The rewrite relation of the following TRS is considered.

0(x1) → 1(x1) (1)
0(0(x1)) → 0(x1) (2)
3(4(5(x1))) → 4(3(5(x1))) (3)
2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) → 0(0(1(0(1(1(0(1(1(1(1(1(1(1(1(0(0(0(0(0(0(1(1(1(1(1(0(0(1(1(1(1(0(0(1(1(1(1(0(1(1(0(0(0(0(0(1(1(0(0(0(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) (4)
1(1(1(1(1(1(0(1(1(1(1(1(1(0(0(0(1(0(1(1(1(0(1(1(1(0(1(0(1(0(1(1(0(1(0(0(1(1(0(1(0(1(0(1(0(0(0(0(0(0(0(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) → 2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) (5)

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(☐), 3(☐), 4(☐), 5(☐), 2(☐)}

We obtain the transformed TRS
0(0(x1)) → 0(x1) (2)
0(0(x1)) → 0(1(x1)) (6)
1(0(x1)) → 1(1(x1)) (7)
3(0(x1)) → 3(1(x1)) (8)
4(0(x1)) → 4(1(x1)) (9)
5(0(x1)) → 5(1(x1)) (10)
2(0(x1)) → 2(1(x1)) (11)
0(3(4(5(x1)))) → 0(4(3(5(x1)))) (12)
1(3(4(5(x1)))) → 1(4(3(5(x1)))) (13)
3(3(4(5(x1)))) → 3(4(3(5(x1)))) (14)
4(3(4(5(x1)))) → 4(4(3(5(x1)))) (15)
5(3(4(5(x1)))) → 5(4(3(5(x1)))) (16)
2(3(4(5(x1)))) → 2(4(3(5(x1)))) (17)
0(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) → 0(0(0(1(0(1(1(0(1(1(1(1(1(1(1(1(0(0(0(0(0(0(1(1(1(1(1(0(0(1(1(1(1(0(0(1(1(1(1(0(1(1(0(0(0(0(0(1(1(0(0(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) (18)
1(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) → 1(0(0(1(0(1(1(0(1(1(1(1(1(1(1(1(0(0(0(0(0(0(1(1(1(1(1(0(0(1(1(1(1(0(0(1(1(1(1(0(1(1(0(0(0(0(0(1(1(0(0(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) (19)
3(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) → 3(0(0(1(0(1(1(0(1(1(1(1(1(1(1(1(0(0(0(0(0(0(1(1(1(1(1(0(0(1(1(1(1(0(0(1(1(1(1(0(1(1(0(0(0(0(0(1(1(0(0(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) (20)
4(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) → 4(0(0(1(0(1(1(0(1(1(1(1(1(1(1(1(0(0(0(0(0(0(1(1(1(1(1(0(0(1(1(1(1(0(0(1(1(1(1(0(1(1(0(0(0(0(0(1(1(0(0(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) (21)
5(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) → 5(0(0(1(0(1(1(0(1(1(1(1(1(1(1(1(0(0(0(0(0(0(1(1(1(1(1(0(0(1(1(1(1(0(0(1(1(1(1(0(1(1(0(0(0(0(0(1(1(0(0(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) (22)
2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) → 2(0(0(1(0(1(1(0(1(1(1(1(1(1(1(1(0(0(0(0(0(0(1(1(1(1(1(0(0(1(1(1(1(0(0(1(1(1(1(0(1(1(0(0(0(0(0(1(1(0(0(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) (23)
0(1(1(1(1(1(1(0(1(1(1(1(1(1(0(0(0(1(0(1(1(1(0(1(1(1(0(1(0(1(0(1(1(0(1(0(0(1(1(0(1(0(1(0(1(0(0(0(0(0(0(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) → 0(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) (24)
1(1(1(1(1(1(1(0(1(1(1(1(1(1(0(0(0(1(0(1(1(1(0(1(1(1(0(1(0(1(0(1(1(0(1(0(0(1(1(0(1(0(1(0(1(0(0(0(0(0(0(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) → 1(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) (25)
3(1(1(1(1(1(1(0(1(1(1(1(1(1(0(0(0(1(0(1(1(1(0(1(1(1(0(1(0(1(0(1(1(0(1(0(0(1(1(0(1(0(1(0(1(0(0(0(0(0(0(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) → 3(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) (26)
4(1(1(1(1(1(1(0(1(1(1(1(1(1(0(0(0(1(0(1(1(1(0(1(1(1(0(1(0(1(0(1(1(0(1(0(0(1(1(0(1(0(1(0(1(0(0(0(0(0(0(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) → 4(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) (27)
5(1(1(1(1(1(1(0(1(1(1(1(1(1(0(0(0(1(0(1(1(1(0(1(1(1(0(1(0(1(0(1(1(0(1(0(0(1(1(0(1(0(1(0(1(0(0(0(0(0(0(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) → 5(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) (28)
2(1(1(1(1(1(1(0(1(1(1(1(1(1(0(0(0(1(0(1(1(1(0(1(1(1(0(1(0(1(0(1(1(0(1(0(0(1(1(0(1(0(1(0(1(0(0(0(0(0(0(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) → 2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) (29)

1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS

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

1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[00(x1)] = 1 · x1 + 6
[01(x1)] = 1 · x1 + 1
[03(x1)] = 1 · x1 + 1
[04(x1)] = 1 · x1
[05(x1)] = 1 · x1 + 4
[02(x1)] = 1 · x1 + 6
[10(x1)] = 1 · x1 + 2
[11(x1)] = 1 · x1 + 1
[13(x1)] = 1 · x1
[14(x1)] = 1 · x1
[15(x1)] = 1 · x1 + 3
[12(x1)] = 1 · x1 + 5
[30(x1)] = 1 · x1 + 1
[31(x1)] = 1 · x1
[40(x1)] = 1 · x1 + 2
[41(x1)] = 1 · x1
[50(x1)] = 1 · x1
[51(x1)] = 1 · x1
[20(x1)] = 1 · x1 + 1
[21(x1)] = 1 · x1
[34(x1)] = 1 · x1 + 1
[45(x1)] = 1 · x1
[43(x1)] = 1 · x1
[35(x1)] = 1 · x1
[53(x1)] = 1 · x1
[54(x1)] = 1 · x1 + 1
[55(x1)] = 1 · x1
[52(x1)] = 1 · x1 + 4
[33(x1)] = 1 · x1 + 1
[44(x1)] = 1 · x1 + 1
[23(x1)] = 1 · x1
[24(x1)] = 1 · x1
[22(x1)] = 1 · x1 + 4
[25(x1)] = 1 · x1
[32(x1)] = 1 · x1 + 5
[42(x1)] = 1 · x1 + 3
all of the following rules can be deleted.

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

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[50(x1)] = 1 · x1 + 1
[01(x1)] = 1 · x1
[51(x1)] = 1 · x1
[11(x1)] = 1 · x1
[04(x1)] = 1 · x1 + 1
[14(x1)] = 1 · x1 + 1
[43(x1)] = 1 · x1
[34(x1)] = 1 · x1
[45(x1)] = 1 · x1
[44(x1)] = 1 · x1
[35(x1)] = 1 · x1
[53(x1)] = 1 · x1
[54(x1)] = 1 · x1
[55(x1)] = 1 · x1
[52(x1)] = 1 · x1
[10(x1)] = 1 · x1
[00(x1)] = 1 · x1
[13(x1)] = 1 · x1 + 1
[02(x1)] = 1 · x1
[22(x1)] = 1 · x1
[23(x1)] = 1 · x1
[24(x1)] = 1 · x1
[31(x1)] = 1 · x1
[32(x1)] = 1 · x1
all of the following rules can be deleted.
50(01(x1)) → 51(11(x1)) (61)
50(04(x1)) → 51(14(x1)) (63)
01(11(11(11(11(11(10(01(11(11(11(11(11(10(00(00(01(10(01(11(11(10(01(11(11(10(01(10(01(10(01(11(10(01(10(00(01(11(10(01(10(01(10(01(10(00(00(00(00(00(00(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) → 02(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) (146)
01(11(11(11(11(11(10(01(11(11(11(11(11(10(00(00(01(10(01(11(11(10(01(11(11(10(01(10(01(10(01(11(10(01(10(00(01(11(10(01(10(01(10(01(10(00(00(00(00(00(00(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) → 02(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) (147)
31(11(11(11(11(11(10(01(11(11(11(11(11(10(00(00(01(10(01(11(11(10(01(11(11(10(01(10(01(10(01(11(10(01(10(00(01(11(10(01(10(01(10(01(10(00(00(00(00(00(00(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) → 32(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) (158)
31(11(11(11(11(11(10(01(11(11(11(11(11(10(00(00(01(10(01(11(11(10(01(11(11(10(01(10(01(10(01(11(10(01(10(00(01(11(10(01(10(01(10(01(10(00(00(00(00(00(00(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) → 32(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(22(...display limit reached...))))))))))))))))))))))))))))))))))))))))))))))))))) (159)

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[43(x1)] = 1 · x1 + 1
[34(x1)] = 1 · x1
[45(x1)] = 1 · x1 + 1
[50(x1)] = 1 · x1
[44(x1)] = 1 · x1
[35(x1)] = 1 · x1
[51(x1)] = 1 · x1
[53(x1)] = 1 · x1
[54(x1)] = 1 · x1
[55(x1)] = 1 · x1
[52(x1)] = 1 · x1
all of the following rules can be deleted.
43(34(45(50(x1)))) → 44(43(35(50(x1)))) (90)
43(34(45(51(x1)))) → 44(43(35(51(x1)))) (91)
43(34(45(53(x1)))) → 44(43(35(53(x1)))) (92)
43(34(45(54(x1)))) → 44(43(35(54(x1)))) (93)
43(34(45(55(x1)))) → 44(43(35(55(x1)))) (94)
43(34(45(52(x1)))) → 44(43(35(52(x1)))) (95)

1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[53(x1)] = 1 · x1
[34(x1)] = 1 · x1 + 1
[45(x1)] = 1 · x1
[50(x1)] = 1 · x1
[54(x1)] = 1 · x1
[43(x1)] = 1 · x1
[35(x1)] = 1 · x1
[51(x1)] = 1 · x1
[55(x1)] = 1 · x1
[52(x1)] = 1 · x1
all of the following rules can be deleted.
53(34(45(50(x1)))) → 54(43(35(50(x1)))) (96)
53(34(45(51(x1)))) → 54(43(35(51(x1)))) (97)
53(34(45(53(x1)))) → 54(43(35(53(x1)))) (98)
53(34(45(54(x1)))) → 54(43(35(54(x1)))) (99)
53(34(45(55(x1)))) → 54(43(35(55(x1)))) (100)
53(34(45(52(x1)))) → 54(43(35(52(x1)))) (101)

1.1.1.1.1.1.1 R is empty

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