Certification Problem

Input (TPDB SRS_Standard/Mixed_SRS/turing_add)

The rewrite relation of the following TRS is considered.

1(q0(1(x1))) 0(1(q1(x1))) (1)
1(q0(0(x1))) 0(0(q1(x1))) (2)
1(q1(1(x1))) 1(1(q1(x1))) (3)
1(q1(0(x1))) 1(0(q1(x1))) (4)
0(q1(x1)) q2(1(x1)) (5)
1(q2(x1)) q2(1(x1)) (6)
0(q2(x1)) 0(q0(x1)) (7)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by matchbox @ termCOMP 2023)

1 Closure Under Flat Contexts

Using the flat contexts

{q1(), q0(), q2(), 1(), 0()}

We obtain the transformed TRS
q1(1(q0(1(x1)))) q1(0(1(q1(x1)))) (8)
q1(1(q0(0(x1)))) q1(0(0(q1(x1)))) (9)
q1(1(q1(1(x1)))) q1(1(1(q1(x1)))) (10)
q1(1(q1(0(x1)))) q1(1(0(q1(x1)))) (11)
q1(0(q1(x1))) q1(q2(1(x1))) (12)
q1(1(q2(x1))) q1(q2(1(x1))) (13)
q1(0(q2(x1))) q1(0(q0(x1))) (14)
q0(1(q0(1(x1)))) q0(0(1(q1(x1)))) (15)
q0(1(q0(0(x1)))) q0(0(0(q1(x1)))) (16)
q0(1(q1(1(x1)))) q0(1(1(q1(x1)))) (17)
q0(1(q1(0(x1)))) q0(1(0(q1(x1)))) (18)
q0(0(q1(x1))) q0(q2(1(x1))) (19)
q0(1(q2(x1))) q0(q2(1(x1))) (20)
q0(0(q2(x1))) q0(0(q0(x1))) (21)
q2(1(q0(1(x1)))) q2(0(1(q1(x1)))) (22)
q2(1(q0(0(x1)))) q2(0(0(q1(x1)))) (23)
q2(1(q1(1(x1)))) q2(1(1(q1(x1)))) (24)
q2(1(q1(0(x1)))) q2(1(0(q1(x1)))) (25)
q2(0(q1(x1))) q2(q2(1(x1))) (26)
q2(1(q2(x1))) q2(q2(1(x1))) (27)
q2(0(q2(x1))) q2(0(q0(x1))) (28)
1(1(q0(1(x1)))) 1(0(1(q1(x1)))) (29)
1(1(q0(0(x1)))) 1(0(0(q1(x1)))) (30)
1(1(q1(1(x1)))) 1(1(1(q1(x1)))) (31)
1(1(q1(0(x1)))) 1(1(0(q1(x1)))) (32)
1(0(q1(x1))) 1(q2(1(x1))) (33)
1(1(q2(x1))) 1(q2(1(x1))) (34)
1(0(q2(x1))) 1(0(q0(x1))) (35)
0(1(q0(1(x1)))) 0(0(1(q1(x1)))) (36)
0(1(q0(0(x1)))) 0(0(0(q1(x1)))) (37)
0(1(q1(1(x1)))) 0(1(1(q1(x1)))) (38)
0(1(q1(0(x1)))) 0(1(0(q1(x1)))) (39)
0(0(q1(x1))) 0(q2(1(x1))) (40)
0(1(q2(x1))) 0(q2(1(x1))) (41)
0(0(q2(x1))) 0(0(q0(x1))) (42)

1.1 Semantic Labeling

The following interpretations form a model of the rules.

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

[q1(x1)] = 5x1 + 0
[q0(x1)] = 5x1 + 1
[q2(x1)] = 5x1 + 2
[1(x1)] = 5x1 + 3
[0(x1)] = 5x1 + 4

We obtain the labeled TRS

There are 175 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
[q10(x1)] = x1 +
2
[q11(x1)] = x1 +
2
[q12(x1)] = x1 +
2
[q13(x1)] = x1 +
2
[q14(x1)] = x1 +
2
[q00(x1)] = x1 +
0
[q01(x1)] = x1 +
0
[q02(x1)] = x1 +
0
[q03(x1)] = x1 +
3
[q04(x1)] = x1 +
3
[q20(x1)] = x1 +
4
[q21(x1)] = x1 +
4
[q22(x1)] = x1 +
1
[q23(x1)] = x1 +
0
[q24(x1)] = x1 +
0
[10(x1)] = x1 +
2
[11(x1)] = x1 +
3
[12(x1)] = x1 +
1
[13(x1)] = x1 +
0
[14(x1)] = x1 +
0
[00(x1)] = x1 +
2
[01(x1)] = x1 +
0
[02(x1)] = x1 +
3
[03(x1)] = x1 +
2
[04(x1)] = x1 +
2
all of the following rules can be deleted.

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

1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
13(q03(11(13(x1)))) q13(10(03(14(x1)))) (218)
14(q03(11(13(x1)))) q14(10(03(14(x1)))) (219)
13(q03(11(q03(x1)))) q13(10(03(q04(x1)))) (220)
14(q03(11(q03(x1)))) q14(10(03(q04(x1)))) (221)
13(q03(11(03(x1)))) q13(10(03(04(x1)))) (222)
14(q03(11(03(x1)))) q14(10(03(04(x1)))) (223)
13(q03(11(q13(x1)))) q13(10(03(q14(x1)))) (224)
14(q03(11(q13(x1)))) q14(10(03(q14(x1)))) (225)
13(q03(11(q23(x1)))) q13(10(03(q24(x1)))) (226)
14(q03(11(q23(x1)))) q14(10(03(q24(x1)))) (227)
01(q04(11(13(x1)))) q11(00(04(14(x1)))) (228)
01(q04(11(q03(x1)))) q11(00(04(q04(x1)))) (229)
01(q04(11(03(x1)))) q11(00(04(04(x1)))) (230)
01(q04(11(q13(x1)))) q11(00(04(q14(x1)))) (231)
01(q04(11(q23(x1)))) q11(00(04(q24(x1)))) (232)
13(q13(10(13(x1)))) q13(10(13(13(x1)))) (233)
14(q13(10(13(x1)))) q14(10(13(13(x1)))) (234)
13(q13(10(q03(x1)))) q13(10(13(q03(x1)))) (235)
14(q13(10(q03(x1)))) q14(10(13(q03(x1)))) (236)
13(q13(10(03(x1)))) q13(10(13(03(x1)))) (237)
14(q13(10(03(x1)))) q14(10(13(03(x1)))) (238)
13(q13(10(q13(x1)))) q13(10(13(q13(x1)))) (239)
14(q13(10(q13(x1)))) q14(10(13(q13(x1)))) (240)
13(q13(10(q23(x1)))) q13(10(13(q23(x1)))) (241)
14(q13(10(q23(x1)))) q14(10(13(q23(x1)))) (242)
01(q14(10(13(x1)))) q11(00(14(13(x1)))) (243)
01(q14(10(q03(x1)))) q11(00(14(q03(x1)))) (244)
01(q14(10(03(x1)))) q11(00(14(03(x1)))) (245)
01(q14(10(q13(x1)))) q11(00(14(q13(x1)))) (246)
01(q14(10(q23(x1)))) q11(00(14(q23(x1)))) (247)
q11(00(14(x1))) 11(q23(12(x1))) (248)
q11(00(04(x1))) 11(q23(02(x1))) (249)
q11(00(q24(x1))) 11(q23(q22(x1))) (250)
q23(12(13(x1))) 13(q23(12(x1))) (251)
q24(12(13(x1))) 14(q23(12(x1))) (252)
q22(12(13(x1))) 12(q23(12(x1))) (253)
q23(12(03(x1))) 13(q23(02(x1))) (254)
q24(12(03(x1))) 14(q23(02(x1))) (255)
q22(12(03(x1))) 12(q23(02(x1))) (256)
q23(12(q23(x1))) 13(q23(q22(x1))) (257)
q24(12(q23(x1))) 14(q23(q22(x1))) (258)
q22(12(q23(x1))) 12(q23(q22(x1))) (259)
q23(02(14(x1))) q03(01(14(x1))) (260)
q24(02(14(x1))) q04(01(14(x1))) (261)
q23(02(q04(x1))) q03(01(q04(x1))) (262)
q24(02(q04(x1))) q04(01(q04(x1))) (263)
q23(02(04(x1))) q03(01(04(x1))) (264)
q24(02(04(x1))) q04(01(04(x1))) (265)
q23(02(q14(x1))) q03(01(q14(x1))) (266)
q24(02(q14(x1))) q04(01(q14(x1))) (267)
q23(02(q24(x1))) q03(01(q24(x1))) (268)
q24(02(q24(x1))) q04(01(q24(x1))) (269)

1.1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
q11#(00(q24(x1))) q22#(x1) (270)
q11#(00(q24(x1))) q23#(q22(x1)) (271)
q11#(00(14(x1))) q23#(12(x1)) (272)
q11#(00(04(x1))) q23#(02(x1)) (273)
q22#(12(q23(x1))) q22#(x1) (274)
q22#(12(q23(x1))) q23#(q22(x1)) (275)
q22#(12(13(x1))) q23#(12(x1)) (276)
q22#(12(03(x1))) q23#(02(x1)) (277)
q23#(12(q23(x1))) q22#(x1) (278)
q23#(12(q23(x1))) q23#(q22(x1)) (279)
q23#(12(q23(x1))) 13#(q23(q22(x1))) (280)
q23#(12(13(x1))) q23#(12(x1)) (281)
q23#(12(13(x1))) 13#(q23(12(x1))) (282)
q23#(12(03(x1))) q23#(02(x1)) (283)
q23#(12(03(x1))) 13#(q23(02(x1))) (284)
q23#(02(q14(x1))) 01#(q14(x1)) (285)
q23#(02(q04(x1))) 01#(q04(x1)) (286)
q23#(02(q24(x1))) 01#(q24(x1)) (287)
q23#(02(14(x1))) 01#(14(x1)) (288)
q23#(02(04(x1))) 01#(04(x1)) (289)
q24#(12(q23(x1))) q22#(x1) (290)
q24#(12(q23(x1))) q23#(q22(x1)) (291)
q24#(12(q23(x1))) 14#(q23(q22(x1))) (292)
q24#(12(13(x1))) q23#(12(x1)) (293)
q24#(12(13(x1))) 14#(q23(12(x1))) (294)
q24#(12(03(x1))) q23#(02(x1)) (295)
q24#(12(03(x1))) 14#(q23(02(x1))) (296)
q24#(02(q14(x1))) 01#(q14(x1)) (297)
q24#(02(q04(x1))) 01#(q04(x1)) (298)
q24#(02(q24(x1))) 01#(q24(x1)) (299)
q24#(02(14(x1))) 01#(14(x1)) (300)
q24#(02(04(x1))) 01#(04(x1)) (301)
13#(q13(10(q13(x1)))) 13#(q13(x1)) (302)
13#(q13(10(q03(x1)))) 13#(q03(x1)) (303)
13#(q13(10(q23(x1)))) 13#(q23(x1)) (304)
13#(q13(10(13(x1)))) 13#(13(x1)) (305)
13#(q13(10(03(x1)))) 13#(03(x1)) (306)
13#(q03(11(q23(x1)))) q24#(x1) (307)
13#(q03(11(13(x1)))) 14#(x1) (308)
14#(q13(10(q13(x1)))) 13#(q13(x1)) (309)
14#(q13(10(q03(x1)))) 13#(q03(x1)) (310)
14#(q13(10(q23(x1)))) 13#(q23(x1)) (311)
14#(q13(10(13(x1)))) 13#(13(x1)) (312)
14#(q13(10(03(x1)))) 13#(03(x1)) (313)
14#(q03(11(q23(x1)))) q24#(x1) (314)
14#(q03(11(13(x1)))) 14#(x1) (315)
01#(q14(10(q13(x1)))) q11#(00(14(q13(x1)))) (316)
01#(q14(10(q13(x1)))) 14#(q13(x1)) (317)
01#(q14(10(q03(x1)))) q11#(00(14(q03(x1)))) (318)
01#(q14(10(q03(x1)))) 14#(q03(x1)) (319)
01#(q14(10(q23(x1)))) q11#(00(14(q23(x1)))) (320)
01#(q14(10(q23(x1)))) 14#(q23(x1)) (321)
01#(q14(10(13(x1)))) q11#(00(14(13(x1)))) (322)
01#(q14(10(13(x1)))) 14#(13(x1)) (323)
01#(q14(10(03(x1)))) q11#(00(14(03(x1)))) (324)
01#(q14(10(03(x1)))) 14#(03(x1)) (325)
01#(q04(11(q13(x1)))) q11#(00(04(q14(x1)))) (326)
01#(q04(11(q03(x1)))) q11#(00(04(q04(x1)))) (327)
01#(q04(11(q23(x1)))) q11#(00(04(q24(x1)))) (328)
01#(q04(11(q23(x1)))) q24#(x1) (329)
01#(q04(11(13(x1)))) q11#(00(04(14(x1)))) (330)
01#(q04(11(13(x1)))) 14#(x1) (331)
01#(q04(11(03(x1)))) q11#(00(04(04(x1)))) (332)

1.1.1.1.1.1 Monotonic Reduction Pair Processor with Usable Rules

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[q11(x1)] = x1 +
3
[q13(x1)] = x1 +
3
[q14(x1)] = x1 +
3
[q03(x1)] = x1 +
3
[q04(x1)] = x1 +
3
[q22(x1)] = x1 +
0
[q23(x1)] = x1 +
0
[q24(x1)] = x1 +
0
[10(x1)] = x1 +
3
[11(x1)] = x1 +
3
[12(x1)] = x1 +
3
[13(x1)] = x1 +
3
[14(x1)] = x1 +
3
[00(x1)] = x1 +
0
[01(x1)] = x1 +
0
[02(x1)] = x1 +
3
[03(x1)] = x1 +
3
[04(x1)] = x1 +
3
[q11#(x1)] = x1 +
2
[q22#(x1)] = x1 +
0
[q23#(x1)] = x1 +
1
[q24#(x1)] = x1 +
3
[13#(x1)] = x1 +
0
[14#(x1)] = x1 +
0
[01#(x1)] = x1 +
3
together with the usable rules
13(q03(11(13(x1)))) q13(10(03(14(x1)))) (218)
14(q03(11(13(x1)))) q14(10(03(14(x1)))) (219)
13(q03(11(q03(x1)))) q13(10(03(q04(x1)))) (220)
14(q03(11(q03(x1)))) q14(10(03(q04(x1)))) (221)
13(q03(11(03(x1)))) q13(10(03(04(x1)))) (222)
14(q03(11(03(x1)))) q14(10(03(04(x1)))) (223)
13(q03(11(q13(x1)))) q13(10(03(q14(x1)))) (224)
14(q03(11(q13(x1)))) q14(10(03(q14(x1)))) (225)
13(q03(11(q23(x1)))) q13(10(03(q24(x1)))) (226)
14(q03(11(q23(x1)))) q14(10(03(q24(x1)))) (227)
01(q04(11(13(x1)))) q11(00(04(14(x1)))) (228)
01(q04(11(q03(x1)))) q11(00(04(q04(x1)))) (229)
01(q04(11(03(x1)))) q11(00(04(04(x1)))) (230)
01(q04(11(q13(x1)))) q11(00(04(q14(x1)))) (231)
01(q04(11(q23(x1)))) q11(00(04(q24(x1)))) (232)
13(q13(10(13(x1)))) q13(10(13(13(x1)))) (233)
14(q13(10(13(x1)))) q14(10(13(13(x1)))) (234)
13(q13(10(q03(x1)))) q13(10(13(q03(x1)))) (235)
14(q13(10(q03(x1)))) q14(10(13(q03(x1)))) (236)
13(q13(10(03(x1)))) q13(10(13(03(x1)))) (237)
14(q13(10(03(x1)))) q14(10(13(03(x1)))) (238)
13(q13(10(q13(x1)))) q13(10(13(q13(x1)))) (239)
14(q13(10(q13(x1)))) q14(10(13(q13(x1)))) (240)
13(q13(10(q23(x1)))) q13(10(13(q23(x1)))) (241)
14(q13(10(q23(x1)))) q14(10(13(q23(x1)))) (242)
01(q14(10(13(x1)))) q11(00(14(13(x1)))) (243)
01(q14(10(q03(x1)))) q11(00(14(q03(x1)))) (244)
01(q14(10(03(x1)))) q11(00(14(03(x1)))) (245)
01(q14(10(q13(x1)))) q11(00(14(q13(x1)))) (246)
01(q14(10(q23(x1)))) q11(00(14(q23(x1)))) (247)
q11(00(14(x1))) 11(q23(12(x1))) (248)
q11(00(04(x1))) 11(q23(02(x1))) (249)
q11(00(q24(x1))) 11(q23(q22(x1))) (250)
q23(12(13(x1))) 13(q23(12(x1))) (251)
q24(12(13(x1))) 14(q23(12(x1))) (252)
q22(12(13(x1))) 12(q23(12(x1))) (253)
q23(12(03(x1))) 13(q23(02(x1))) (254)
q24(12(03(x1))) 14(q23(02(x1))) (255)
q22(12(03(x1))) 12(q23(02(x1))) (256)
q23(12(q23(x1))) 13(q23(q22(x1))) (257)
q24(12(q23(x1))) 14(q23(q22(x1))) (258)
q22(12(q23(x1))) 12(q23(q22(x1))) (259)
q23(02(14(x1))) q03(01(14(x1))) (260)
q24(02(14(x1))) q04(01(14(x1))) (261)
q23(02(q04(x1))) q03(01(q04(x1))) (262)
q24(02(q04(x1))) q04(01(q04(x1))) (263)
q23(02(04(x1))) q03(01(04(x1))) (264)
q24(02(04(x1))) q04(01(04(x1))) (265)
q23(02(q14(x1))) q03(01(q14(x1))) (266)
q24(02(q14(x1))) q04(01(q14(x1))) (267)
q23(02(q24(x1))) q03(01(q24(x1))) (268)
q24(02(q24(x1))) q04(01(q24(x1))) (269)
(w.r.t. the implicit argument filter of the reduction pair), the pairs
q11#(00(q24(x1))) q22#(x1) (270)
q11#(00(q24(x1))) q23#(q22(x1)) (271)
q11#(00(14(x1))) q23#(12(x1)) (272)
q11#(00(04(x1))) q23#(02(x1)) (273)
q22#(12(q23(x1))) q22#(x1) (274)
q22#(12(q23(x1))) q23#(q22(x1)) (275)
q22#(12(13(x1))) q23#(12(x1)) (276)
q22#(12(03(x1))) q23#(02(x1)) (277)
q23#(12(q23(x1))) q22#(x1) (278)
q23#(12(q23(x1))) q23#(q22(x1)) (279)
q23#(12(q23(x1))) 13#(q23(q22(x1))) (280)
q23#(12(13(x1))) q23#(12(x1)) (281)
q23#(12(13(x1))) 13#(q23(12(x1))) (282)
q23#(12(03(x1))) q23#(02(x1)) (283)
q23#(12(03(x1))) 13#(q23(02(x1))) (284)
q23#(02(q14(x1))) 01#(q14(x1)) (285)
q23#(02(q04(x1))) 01#(q04(x1)) (286)
q23#(02(q24(x1))) 01#(q24(x1)) (287)
q23#(02(14(x1))) 01#(14(x1)) (288)
q23#(02(04(x1))) 01#(04(x1)) (289)
q24#(12(q23(x1))) q22#(x1) (290)
q24#(12(q23(x1))) q23#(q22(x1)) (291)
q24#(12(q23(x1))) 14#(q23(q22(x1))) (292)
q24#(12(13(x1))) q23#(12(x1)) (293)
q24#(12(13(x1))) 14#(q23(12(x1))) (294)
q24#(12(03(x1))) q23#(02(x1)) (295)
q24#(12(03(x1))) 14#(q23(02(x1))) (296)
q24#(02(q14(x1))) 01#(q14(x1)) (297)
q24#(02(q04(x1))) 01#(q04(x1)) (298)
q24#(02(q24(x1))) 01#(q24(x1)) (299)
q24#(02(14(x1))) 01#(14(x1)) (300)
q24#(02(04(x1))) 01#(04(x1)) (301)
13#(q13(10(q13(x1)))) 13#(q13(x1)) (302)
13#(q13(10(q03(x1)))) 13#(q03(x1)) (303)
13#(q13(10(q23(x1)))) 13#(q23(x1)) (304)
13#(q13(10(13(x1)))) 13#(13(x1)) (305)
13#(q13(10(03(x1)))) 13#(03(x1)) (306)
13#(q03(11(q23(x1)))) q24#(x1) (307)
13#(q03(11(13(x1)))) 14#(x1) (308)
14#(q13(10(q13(x1)))) 13#(q13(x1)) (309)
14#(q13(10(q03(x1)))) 13#(q03(x1)) (310)
14#(q13(10(q23(x1)))) 13#(q23(x1)) (311)
14#(q13(10(13(x1)))) 13#(13(x1)) (312)
14#(q13(10(03(x1)))) 13#(03(x1)) (313)
14#(q03(11(q23(x1)))) q24#(x1) (314)
14#(q03(11(13(x1)))) 14#(x1) (315)
01#(q14(10(q13(x1)))) q11#(00(14(q13(x1)))) (316)
01#(q14(10(q13(x1)))) 14#(q13(x1)) (317)
01#(q14(10(q03(x1)))) q11#(00(14(q03(x1)))) (318)
01#(q14(10(q03(x1)))) 14#(q03(x1)) (319)
01#(q14(10(q23(x1)))) q11#(00(14(q23(x1)))) (320)
01#(q14(10(q23(x1)))) 14#(q23(x1)) (321)
01#(q14(10(13(x1)))) q11#(00(14(13(x1)))) (322)
01#(q14(10(13(x1)))) 14#(13(x1)) (323)
01#(q14(10(03(x1)))) q11#(00(14(03(x1)))) (324)
01#(q14(10(03(x1)))) 14#(03(x1)) (325)
01#(q04(11(q13(x1)))) q11#(00(04(q14(x1)))) (326)
01#(q04(11(q03(x1)))) q11#(00(04(q04(x1)))) (327)
01#(q04(11(q23(x1)))) q11#(00(04(q24(x1)))) (328)
01#(q04(11(q23(x1)))) q24#(x1) (329)
01#(q04(11(13(x1)))) q11#(00(04(14(x1)))) (330)
01#(q04(11(13(x1)))) 14#(x1) (331)
01#(q04(11(03(x1)))) q11#(00(04(04(x1)))) (332)
and no rules could be deleted.

1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.