Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/186973)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by matchbox @ termCOMP 2023)

1 Closure Under Flat Contexts

Using the flat contexts

{5(), 4(), 3(), 2(), 1(), 0()}

We obtain the transformed TRS

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

1.1 Semantic Labeling

The following interpretations form a model of the rules.

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

[5(x1)] = 6x1 + 0
[4(x1)] = 6x1 + 1
[3(x1)] = 6x1 + 2
[2(x1)] = 6x1 + 3
[1(x1)] = 6x1 + 4
[0(x1)] = 6x1 + 5

We obtain the labeled TRS

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

1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[50(x1)] = x1 +
57684/109
[51(x1)] = x1 +
38870/109
[52(x1)] = x1 +
0
[53(x1)] = x1 +
64331/109
[54(x1)] = x1 +
41377/109
[55(x1)] = x1 +
27071/109
[40(x1)] = x1 +
0
[41(x1)] = x1 +
34707/109
[42(x1)] = x1 +
0
[43(x1)] = x1 +
0
[44(x1)] = x1 +
64440/109
[45(x1)] = x1 +
0
[30(x1)] = x1 +
64331/109
[31(x1)] = x1 +
0
[32(x1)] = x1 +
60927/109
[33(x1)] = x1 +
64331/109
[34(x1)] = x1 +
40986/109
[35(x1)] = x1 +
64331/109
[20(x1)] = x1 +
55286/109
[21(x1)] = x1 +
64331/109
[22(x1)] = x1 +
5
[23(x1)] = x1 +
1
[24(x1)] = x1 +
64440/109
[25(x1)] = x1 +
38065/109
[10(x1)] = x1 +
64331/109
[11(x1)] = x1 +
0
[12(x1)] = x1 +
64331/109
[13(x1)] = x1 +
64440/109
[14(x1)] = x1 +
5
[15(x1)] = x1 +
64440/109
[00(x1)] = x1 +
64331/109
[01(x1)] = x1 +
29348/109
[02(x1)] = x1 +
64331/109
[03(x1)] = x1 +
1
[04(x1)] = x1 +
64876/109
[05(x1)] = x1 +
42941/109
all of the following rules can be deleted.

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

1.1.1.1 R is empty

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