Certification Problem

Input (TPDB SRS_Standard/ICFP_2010/140664)

The rewrite relation of the following TRS is considered.

0(0(0(0(1(0(1(0(1(0(0(2(1(x1))))))))))))) 0(0(0(2(0(0(2(0(0(0(0(0(2(0(0(2(2(x1))))))))))))))))) (1)
0(0(0(0(2(2(2(2(1(1(2(0(1(x1))))))))))))) 0(0(0(0(0(1(0(0(0(0(1(2(2(0(2(0(1(x1))))))))))))))))) (2)
0(0(0(1(0(2(1(2(1(1(0(1(1(x1))))))))))))) 0(0(2(1(1(0(0(1(0(0(2(2(0(0(2(0(1(x1))))))))))))))))) (3)
0(0(0(2(1(1(0(2(2(0(0(1(0(x1))))))))))))) 0(0(0(0(0(0(0(0(0(0(2(2(1(0(0(2(2(x1))))))))))))))))) (4)
0(0(0(2(2(0(1(0(1(2(0(2(0(x1))))))))))))) 0(0(2(0(0(0(1(0(0(0(0(0(0(0(2(2(2(x1))))))))))))))))) (5)
0(0(1(0(0(2(0(1(1(2(2(1(2(x1))))))))))))) 0(0(0(0(0(1(2(0(2(0(2(2(2(1(1(0(0(x1))))))))))))))))) (6)
0(0(1(0(1(2(2(1(2(2(2(2(0(x1))))))))))))) 0(0(2(0(2(0(2(0(2(2(2(1(0(0(0(0(1(x1))))))))))))))))) (7)
0(0(1(0(2(1(2(1(2(2(0(0(0(x1))))))))))))) 0(0(0(2(0(1(0(2(0(0(2(0(0(2(0(0(0(x1))))))))))))))))) (8)
0(0(1(1(0(2(1(0(0(1(0(1(1(x1))))))))))))) 0(0(2(1(0(2(0(0(2(2(0(0(0(2(2(0(1(x1))))))))))))))))) (9)
0(0(1(1(2(1(0(1(2(0(1(0(1(x1))))))))))))) 0(0(0(0(1(1(0(1(2(0(2(2(2(0(0(2(1(x1))))))))))))))))) (10)
0(0(1(2(0(0(0(2(2(0(1(2(0(x1))))))))))))) 0(0(0(2(2(0(0(1(0(0(2(0(0(0(2(0(0(x1))))))))))))))))) (11)
0(0(1(2(2(1(2(1(0(0(0(2(1(x1))))))))))))) 0(0(2(1(0(0(2(2(0(1(0(0(2(2(0(0(0(x1))))))))))))))))) (12)
0(0(2(0(0(1(0(0(2(0(2(1(2(x1))))))))))))) 0(0(2(0(0(0(0(1(0(0(0(2(2(1(0(0(2(x1))))))))))))))))) (13)
0(0(2(0(0(1(1(0(0(1(1(0(1(x1))))))))))))) 0(0(1(2(0(2(1(0(0(0(2(2(0(0(0(2(0(x1))))))))))))))))) (14)
0(0(2(0(0(2(1(2(2(0(1(0(1(x1))))))))))))) 0(0(0(2(0(0(1(2(0(0(2(0(0(0(0(1(2(x1))))))))))))))))) (15)
0(0(2(0(2(1(2(0(2(2(0(1(0(x1))))))))))))) 0(0(0(0(0(2(1(0(1(1(2(0(2(0(0(0(0(x1))))))))))))))))) (16)
0(0(2(1(0(2(0(1(2(1(0(0(0(x1))))))))))))) 0(0(2(0(0(0(0(0(2(0(1(0(0(0(0(1(2(x1))))))))))))))))) (17)
0(0(2(2(0(2(0(2(1(0(0(1(2(x1))))))))))))) 0(0(0(0(2(0(0(0(2(1(0(0(0(2(0(1(2(x1))))))))))))))))) (18)
0(0(2(2(1(0(0(1(1(1(0(1(1(x1))))))))))))) 0(0(0(0(0(0(2(2(0(2(0(1(1(2(2(1(1(x1))))))))))))))))) (19)
0(0(2(2(1(0(2(0(1(1(1(2(0(x1))))))))))))) 0(0(0(1(2(2(2(2(0(1(0(0(2(2(0(2(0(x1))))))))))))))))) (20)
0(0(2(2(2(2(1(2(1(2(0(1(0(x1))))))))))))) 0(0(0(0(0(2(0(1(0(1(2(0(0(2(2(1(0(x1))))))))))))))))) (21)
0(1(0(0(0(1(2(2(2(0(2(1(1(x1))))))))))))) 0(2(2(2(0(2(2(0(0(2(1(0(0(0(0(0(1(x1))))))))))))))))) (22)
0(1(1(0(2(0(2(2(0(2(2(1(0(x1))))))))))))) 0(2(2(0(0(1(1(0(2(1(0(1(0(0(0(0(0(x1))))))))))))))))) (23)
0(1(1(2(0(0(2(0(0(0(2(2(1(x1))))))))))))) 0(2(1(0(0(0(1(0(0(0(0(1(1(0(0(2(0(x1))))))))))))))))) (24)
0(1(2(0(1(0(0(0(1(0(1(0(2(x1))))))))))))) 0(2(0(2(1(0(0(2(0(0(0(0(0(0(2(0(2(x1))))))))))))))))) (25)
0(1(2(0(1(2(0(1(0(0(0(2(1(x1))))))))))))) 0(2(2(2(2(0(2(0(0(0(0(0(2(2(1(0(0(x1))))))))))))))))) (26)
0(2(0(0(2(2(2(0(1(0(2(1(2(x1))))))))))))) 0(1(0(0(0(0(0(0(2(0(1(0(2(2(2(2(0(x1))))))))))))))))) (27)
0(2(0(1(0(2(0(2(0(2(0(1(2(x1))))))))))))) 0(1(0(0(0(1(0(1(0(2(2(2(0(0(0(0(0(x1))))))))))))))))) (28)
0(2(0(1(2(2(0(2(0(0(2(2(0(x1))))))))))))) 0(0(0(0(1(0(0(0(2(1(0(0(0(0(1(1(2(x1))))))))))))))))) (29)
0(2(0(2(1(1(1(1(2(0(0(1(2(x1))))))))))))) 0(1(1(0(0(1(0(2(2(0(2(1(0(0(0(1(2(x1))))))))))))))))) (30)
0(2(1(0(2(1(1(2(2(2(1(2(0(x1))))))))))))) 0(2(2(0(2(0(2(2(1(0(0(2(2(2(0(2(0(x1))))))))))))))))) (31)
0(2(1(2(0(0(0(0(1(2(0(1(0(x1))))))))))))) 0(0(0(0(0(0(0(0(0(0(1(1(1(2(0(1(0(x1))))))))))))))))) (32)
0(2(1(2(0(2(1(0(1(1(2(0(0(x1))))))))))))) 0(2(2(0(1(0(2(0(0(0(2(0(1(0(2(0(0(x1))))))))))))))))) (33)
0(2(2(0(2(2(1(1(2(0(0(0(0(x1))))))))))))) 0(0(0(0(0(0(0(2(0(0(2(0(0(2(1(0(2(x1))))))))))))))))) (34)
0(2(2(1(2(1(2(2(2(0(0(0(0(x1))))))))))))) 0(2(2(2(2(0(0(0(2(0(0(0(0(0(2(1(0(x1))))))))))))))))) (35)
0(2(2(2(1(0(0(2(2(2(1(0(2(x1))))))))))))) 0(0(0(2(2(0(2(0(1(1(2(0(0(0(0(0(2(x1))))))))))))))))) (36)
1(0(0(1(0(2(1(0(0(1(1(0(2(x1))))))))))))) 2(0(0(1(2(1(0(0(0(0(0(0(0(1(1(0(0(x1))))))))))))))))) (37)
1(0(0(1(2(0(0(2(1(2(0(2(1(x1))))))))))))) 2(0(0(0(0(1(1(0(0(1(2(2(0(0(0(2(0(x1))))))))))))))))) (38)
1(0(0(1(2(1(2(0(0(0(2(2(0(x1))))))))))))) 1(0(0(0(0(0(2(2(2(2(0(0(0(0(1(2(0(x1))))))))))))))))) (39)
1(0(0(2(2(0(1(1(1(1(2(0(0(x1))))))))))))) 1(0(0(2(0(2(1(0(0(1(2(0(0(2(2(0(0(x1))))))))))))))))) (40)
1(0(1(0(0(0(1(2(2(1(2(1(0(x1))))))))))))) 2(0(0(0(0(0(0(2(2(2(2(2(1(1(0(1(0(x1))))))))))))))))) (41)
1(0(1(2(0(0(2(0(2(1(1(0(0(x1))))))))))))) 2(0(2(1(0(0(0(0(1(0(0(0(2(2(0(1(0(x1))))))))))))))))) (42)
1(0(2(0(2(2(0(0(2(1(2(0(2(x1))))))))))))) 1(0(2(2(0(1(0(2(0(0(1(0(0(0(0(0(2(x1))))))))))))))))) (43)
1(1(0(2(0(0(1(0(2(0(1(0(1(x1))))))))))))) 2(0(1(0(0(1(0(1(0(1(0(0(0(0(2(0(1(x1))))))))))))))))) (44)
1(1(2(1(0(0(2(2(2(0(0(0(0(x1))))))))))))) 1(1(0(1(1(0(0(0(2(2(0(0(0(0(0(0(0(x1))))))))))))))))) (45)
1(1(2(2(0(0(1(2(2(2(0(2(1(x1))))))))))))) 1(2(2(1(1(0(0(0(0(0(0(0(1(2(1(2(1(x1))))))))))))))))) (46)
1(2(0(0(0(0(2(1(2(2(0(2(1(x1))))))))))))) 2(0(1(0(0(0(1(0(0(1(0(0(0(2(0(2(0(x1))))))))))))))))) (47)
1(2(0(2(0(2(1(0(0(0(1(1(2(x1))))))))))))) 1(1(0(0(1(0(0(1(0(0(0(0(0(0(1(0(1(x1))))))))))))))))) (48)
1(2(1(0(2(0(2(1(0(0(0(2(2(x1))))))))))))) 2(0(0(0(0(0(1(0(2(0(1(1(0(0(0(0(0(x1))))))))))))))))) (49)
1(2(2(0(0(2(2(2(0(1(0(2(1(x1))))))))))))) 1(1(0(0(1(0(0(0(2(1(0(0(2(2(0(2(0(x1))))))))))))))))) (50)
1(2(2(0(1(1(2(2(2(0(0(1(0(x1))))))))))))) 2(0(1(0(2(1(1(2(0(0(0(1(0(2(0(0(0(x1))))))))))))))))) (51)
1(2(2(1(2(0(1(2(0(0(1(0(0(x1))))))))))))) 1(0(1(0(0(1(0(0(1(0(0(0(1(0(1(0(0(x1))))))))))))))))) (52)
1(2(2(2(2(2(1(0(2(2(1(1(0(x1))))))))))))) 2(0(2(0(2(0(1(0(0(2(0(1(0(0(1(1(0(x1))))))))))))))))) (53)
2(0(0(0(0(1(1(0(1(1(0(1(2(x1))))))))))))) 2(0(0(0(0(1(2(0(0(2(0(0(1(0(2(0(0(x1))))))))))))))))) (54)
2(0(1(0(0(2(1(2(2(0(1(2(1(x1))))))))))))) 1(1(2(2(1(0(0(0(0(0(2(0(2(0(0(2(0(x1))))))))))))))))) (55)
2(0(1(0(2(0(0(0(2(1(0(1(0(x1))))))))))))) 2(0(1(2(0(0(0(0(1(0(0(0(0(2(0(1(0(x1))))))))))))))))) (56)
2(0(1(1(1(0(1(1(0(0(0(0(0(x1))))))))))))) 1(0(1(0(0(0(2(0(0(0(0(1(0(0(0(0(0(x1))))))))))))))))) (57)
2(0(1(2(1(1(1(0(2(1(0(0(0(x1))))))))))))) 2(0(1(1(2(0(2(2(1(0(0(0(0(2(0(0(0(x1))))))))))))))))) (58)
2(0(2(0(0(2(1(2(0(1(0(2(1(x1))))))))))))) 1(2(0(0(0(0(0(0(0(0(1(0(2(1(1(0(1(x1))))))))))))))))) (59)
2(0(2(0(1(1(0(0(0(2(1(2(1(x1))))))))))))) 2(0(1(0(2(1(0(0(1(2(2(0(0(0(0(0(0(x1))))))))))))))))) (60)
2(1(0(0(1(2(0(0(2(1(2(1(0(x1))))))))))))) 2(1(0(0(0(2(2(0(0(2(2(2(0(0(1(0(0(x1))))))))))))))))) (61)
2(1(0(0(2(0(0(2(2(0(1(2(1(x1))))))))))))) 2(1(0(2(0(2(2(0(2(1(0(0(0(0(0(0(0(x1))))))))))))))))) (62)
2(1(0(0(2(1(2(0(1(0(0(1(0(x1))))))))))))) 0(0(2(2(0(1(0(0(1(0(0(0(0(0(0(1(0(x1))))))))))))))))) (63)
2(1(0(2(1(1(0(0(0(2(0(1(0(x1))))))))))))) 0(2(0(0(2(2(0(2(0(0(0(0(0(2(1(0(0(x1))))))))))))))))) (64)
2(1(1(0(0(0(2(1(2(0(0(2(1(x1))))))))))))) 2(2(1(0(0(2(1(0(0(0(0(0(0(2(2(2(0(x1))))))))))))))))) (65)
2(1(2(0(0(1(2(2(2(0(2(1(0(x1))))))))))))) 2(1(0(1(0(0(0(2(0(2(0(0(1(2(0(0(0(x1))))))))))))))))) (66)
2(1(2(1(0(0(0(2(2(0(0(0(1(x1))))))))))))) 0(0(1(0(0(0(0(0(2(1(0(0(0(0(2(0(1(x1))))))))))))))))) (67)
2(2(0(0(2(1(2(0(0(2(1(0(0(x1))))))))))))) 0(0(2(1(0(0(0(1(0(0(0(0(1(0(0(0(0(x1))))))))))))))))) (68)
2(2(0(1(0(0(1(1(1(0(2(0(1(x1))))))))))))) 2(1(0(2(2(1(0(1(0(0(0(0(0(1(0(0(1(x1))))))))))))))))) (69)
2(2(2(1(1(0(2(0(0(0(0(0(1(x1))))))))))))) 2(2(1(0(0(0(0(0(1(0(0(0(0(0(2(0(1(x1))))))))))))))))) (70)
2(2(2(1(2(0(2(1(2(0(0(0(0(x1))))))))))))) 0(0(2(0(0(0(0(0(1(0(0(2(2(2(0(0(0(x1))))))))))))))))) (71)

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 213 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 639 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 5751 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 +
132016/25
[23(x1)] = x1 +
13947/5
[26(x1)] = x1 +
82436/15
[21(x1)] = x1 +
397757/75
[24(x1)] = x1 +
346549/75
[27(x1)] = x1 +
190772/25
[22(x1)] = x1 +
5772
[25(x1)] = x1 +
180856/25
[28(x1)] = x1 +
67784/25
[10(x1)] = x1 +
209186/25
[13(x1)] = x1 +
208411/25
[16(x1)] = x1 +
200244/25
[11(x1)] = x1 +
29452/5
[14(x1)] = x1 +
210211/25
[17(x1)] = x1 +
208261/25
[12(x1)] = x1 +
550708/75
[15(x1)] = x1 +
208261/25
[18(x1)] = x1 +
193067/75
[00(x1)] = x1 +
22496/75
[03(x1)] = x1 +
147112/75
[06(x1)] = x1 +
38
[01(x1)] = x1 +
0
[04(x1)] = x1 +
53601/25
[07(x1)] = x1 +
2591/75
[02(x1)] = x1 +
0
[05(x1)] = x1 +
1
[08(x1)] = x1 +
0
all of the following rules can be deleted.

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