Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z030)

The rewrite relation of the following TRS is considered.

b(a(b(a(a(a(x1))))))

→

a(a(a(b(a(b(a(b(a(x1)))))))))

(1)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Bounds

The given TRS is match-(raise)-bounded by 6. This is shown by the following automaton.

final states:

{2, 1}

transitions:

61	→	107
205	→	177
89	→	59
89	→	61
89	→	139
89	→	84
87	→	127
98	→	59
98	→	8
214	→	229
10	→	78
97	→	105
96	→	159
136	→	111
136	→	177
149	→	109
184	→	84
219	→	209
134	→	218
147	→	165
62	→	80
1	→	34
13	→	1
13	→	6
13	→	45
13	→	8
183	→	197
86	→	175
79	→	56
116	→	93
88	→	141
54	→	6
174	→	113
2	→	4
11	→	53
11	→	55
66	→	57
106	→	57
63	→	65
12	→	47
140	→	82
217	→	181
217	→	220
64	→	8
64	→	10
64	→	6
64	→	54
64	→	90
64	→	57
46	→	6
35	→	5
48	→	6
160	→	141
203	→	208
228	→	200
238	→	223
b₆(234)	→	235
b₆(232)	→	233
b₆(230)	→	231
a₄(175)	→	176
a₄(203)	→	204
a₄(173)	→	174
a₄(169)	→	170
a₄(183)	→	184
a₄(127)	→	128
a₄(200)	→	201
a₄(129)	→	130
a₄(135)	→	136
a₄(167)	→	168
a₄(134)	→	135
a₄(165)	→	166
a₄(133)	→	134
a₄(198)	→	199
a₄(179)	→	180
a₄(131)	→	132
a₄(204)	→	205
a₄(177)	→	178
a₄(171)	→	172
a₄(181)	→	182
a₄(202)	→	203
a₄(182)	→	183
a₄(172)	→	173
b₄(132)	→	133
b₄(201)	→	202
b₄(176)	→	177
b₄(199)	→	200
b₄(128)	→	129
b₄(170)	→	171
b₄(197)	→	198
b₄(168)	→	169
b₄(180)	→	181
b₄(178)	→	179
b₄(166)	→	167
b₄(130)	→	131
b₃(81)	→	82
b₃(108)	→	109
b₃(85)	→	86
b₃(112)	→	113
b₃(143)	→	144
b₃(110)	→	111
b₃(139)	→	140
b₃(145)	→	146
b₃(83)	→	84
b₃(141)	→	142
a₁(11)	→	12
a₁(8)	→	9
a₁(12)	→	13
a₁(34)	→	35
a₁(4)	→	5
a₁(6)	→	7
a₁(10)	→	11
b₁(5)	→	6
b₁(45)	→	46
b₁(7)	→	8
b₁(9)	→	10
b₁(47)	→	48
b₁(53)	→	54
a₅(218)	→	219
a₅(223)	→	224
a₅(227)	→	228
a₅(208)	→	209
a₅(226)	→	227
a₅(216)	→	217
a₅(210)	→	211
a₅(214)	→	215
a₅(212)	→	213
a₅(215)	→	216
a₅(221)	→	222
a₅(225)	→	226
b₅(224)	→	225
b₅(211)	→	212
b₅(222)	→	223
b₅(213)	→	214
b₅(209)	→	210
b₅(220)	→	221
a₀(1)	→	2
a₀(2)	→	2
b₂(105)	→	106
b₂(58)	→	59
b₂(94)	→	95
b₂(92)	→	93
b₂(90)	→	91
b₂(56)	→	57
b₂(60)	→	61
b₂(65)	→	66
a₃(114)	→	115
a₃(146)	→	147
a₃(80)	→	81
a₃(113)	→	114
a₃(107)	→	108
a₃(159)	→	160
a₃(84)	→	85
a₃(86)	→	87
a₃(147)	→	148
a₃(87)	→	88
a₃(111)	→	112
a₃(82)	→	83
a₃(142)	→	143
a₃(109)	→	110
a₃(144)	→	145
a₃(88)	→	89
a₃(148)	→	149
a₃(115)	→	116
a₆(235)	→	236
a₆(237)	→	238
a₆(236)	→	237
a₆(229)	→	230
a₆(233)	→	234
a₆(231)	→	232
b₀(1)	→	1
b₀(2)	→	1
a₂(97)	→	98
a₂(95)	→	96
a₂(93)	→	94
a₂(63)	→	64
a₂(96)	→	97
a₂(55)	→	56
a₂(91)	→	92
a₂(59)	→	60
a₂(61)	→	62
a₂(57)	→	58
a₂(62)	→	63
a₂(78)	→	79

The automaton is closed under rewriting as it is compatible.