Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/160427)

The rewrite relation of the following TRS is considered.

There are 110 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

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

We obtain the transformed TRS

There are 330 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 990 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 8910 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 +
0
[23(x1)] = x1 +
9031/25
[26(x1)] = x1 +
9146/25
[21(x1)] = x1 +
2422683/25
[24(x1)] = x1 +
709573/50
[27(x1)] = x1 +
4852289/50
[22(x1)] = x1 +
9146/25
[25(x1)] = x1 +
3467113/50
[28(x1)] = x1 +
1631001/50
[10(x1)] = x1 +
2881781/25
[13(x1)] = x1 +
3225978/25
[16(x1)] = x1 +
3225978/25
[11(x1)] = x1 +
11219/50
[14(x1)] = x1 +
0
[17(x1)] = x1 +
9146/25
[12(x1)] = x1 +
645982/5
[15(x1)] = x1 +
4838967/50
[18(x1)] = x1 +
3235004/25
[00(x1)] = x1 +
248439/50
[03(x1)] = x1 +
935023/50
[06(x1)] = x1 +
2995551/50
[01(x1)] = x1 +
3226143/25
[04(x1)] = x1 +
1159522/25
[07(x1)] = x1 +
646191/5
[02(x1)] = x1 +
1391568/25
[05(x1)] = x1 +
3226143/25
[08(x1)] = x1 +
2308087/25
all of the following rules can be deleted.

There are 8910 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.