YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

a(a(a(a(x0))))	→	a(a(b(b(b(b(b(b(x0))))))))
b(b(a(a(x0))))	→	b(b(b(b(c(c(x0))))))
a(a(b(b(b(b(c(c(x0))))))))	→	a(a(a(a(a(a(b(b(x0))))))))

Proof

1 Bounds

The given TRS is match-bounded by 3. This is shown by the following automaton.

final states:

{16, 10, 1}

transitions:

157 → 19

322 → 167

376 → 124

102 → 164

102 → 304

102 → 346

128 → 224

128 → 232

128 → 327

128 → 370

103 → 58

103 → 18

103 → 275

103 → 113

103 → 99

98 → 122

98 → 252

10 → 80

10 → 4

10 → 3

10 → 295

10 → 97

10 → 96

274 → 24

274 → 168

387 → 168

387 → 24

97 → 166

97 → 295

129 → 218

129 → 283

129 → 319

211 → 50

119 → 216

119 → 281

119 → 306

119 → 348

276 → 269

299 → 123

18 → 58

227 → 150

120 → 210

120 → 298

120 → 344

57 → 21

333 → 368

333 → 406

333 → 410

225 → 150

347 → 253

219 → 23

209 → 50

130 → 102

99 → 113

99 → 275

305 → 123

165 → 50

101 → 158

101 → 184

101 → 321

334 → 359

334 → 397

416 → 329

297 → 170

343 → 328

79 → 59

201 → 114

251 → 233

407 → 253

172 → 200

172 → 268

172 → 381

173 → 226

173 → 239

173 → 336

121 → 18

121 → 103

337 → 328

345 → 253

174 → 101

82 → 26

2 → 95

4 → 22

4 → 80

28 → 78

258 → 151

258 → 329

284 → 185

369 → 123

66 → 16

100 → 149

100 → 250

100 → 342

335 → 100

282 → 185

217 → 23

30 → 20

240 → 233

17 → 49

190 → 60

190 → 115

360 → 114

398 → 382

159 → 23

320 → 167

203 → 59

354 → 115

155 → 208

156 → 202

238 → 51

238 → 124

307 → 167

c₃(371) → 372

c₃(411) → 412

c₃(410) → 411

c₃(381) → 382

c₃(370) → 371

c₃(349) → 350

c₃(348) → 349

c₃(382) → 383

c₁(80) → 81

c₁(81) → 82

b₂(331) → 332

b₂(255) → 256

b₂(235) → 236

b₂(117) → 118

b₂(188) → 189

b₂(124) → 125

b₂(113) → 114

b₂(167) → 168

b₂(186) → 187

b₂(319) → 320

b₂(234) → 235

b₂(115) → 116

b₂(254) → 255

b₂(336) → 337

b₂(114) → 115

b₂(123) → 124

b₂(332) → 333

b₂(187) → 188

b₂(329) → 330

b₂(270) → 271

b₂(321) → 322

b₂(126) → 127

b₂(298) → 299

b₂(125) → 126

b₂(342) → 343

b₂(359) → 360

b₂(200) → 201

b₂(273) → 274

b₂(169) → 170

b₂(118) → 119

b₂(257) → 258

b₂(236) → 237

b₂(116) → 117

b₂(304) → 305

b₂(170) → 171

b₂(306) → 307

b₂(168) → 169

b₂(330) → 331

b₂(256) → 257

b₂(166) → 167

b₂(328) → 329

b₂(327) → 328

b₂(271) → 272

b₂(189) → 190

b₂(237) → 238

b₂(127) → 128

b₂(368) → 369

b₂(171) → 172

b₂(122) → 123

b₂(272) → 273

b₁(226) → 227

b₁(151) → 152

b₁(23) → 24

b₁(150) → 151

b₁(26) → 27

b₁(218) → 219

b₁(78) → 79

b₁(216) → 217

b₁(63) → 64

b₁(59) → 60

b₁(58) → 59

b₁(51) → 52

b₁(210) → 211

b₁(95) → 96

b₁(60) → 61

b₁(152) → 153

b₁(149) → 150

b₁(158) → 159

b₁(202) → 203

b₁(164) → 165

b₁(154) → 155

b₁(25) → 26

b₁(54) → 55

b₁(96) → 97

b₁(50) → 51

b₁(208) → 209

b₁(61) → 62

b₁(224) → 225

b₁(27) → 28

b₁(49) → 50

b₁(53) → 54

b₁(62) → 63

b₁(153) → 154

b₁(24) → 25

b₁(22) → 23

b₁(52) → 53

f3₀ → 2

a₀(20) → 21

a₀(17) → 18

a₀(9) → 1

a₀(8) → 9

a₀(19) → 20

a₀(21) → 16

a₀(18) → 19

a₀(4) → 17

c₂(283) → 284

c₂(296) → 297

c₂(406) → 407

c₂(397) → 398

c₂(344) → 345

c₂(281) → 282

c₂(269) → 270

c₂(184) → 185

c₂(295) → 296

c₂(275) → 276

c₂(239) → 240

c₂(232) → 233

c₂(346) → 347

c₂(185) → 186

c₂(250) → 251

c₂(233) → 234

c₂(268) → 269

c₂(253) → 254

c₂(252) → 253

a₂(333) → 334

a₂(128) → 129

a₂(172) → 173

a₂(120) → 121

a₂(173) → 174

a₂(119) → 120

a₂(334) → 335

a₂(129) → 130

c₀(11) → 12

c₀(2) → 11

a₁(28) → 29

a₁(56) → 57

a₁(156) → 157

a₁(65) → 66

a₁(98) → 99

a₁(64) → 65

a₁(99) → 100

a₁(55) → 56

a₁(155) → 156

a₁(100) → 101

a₁(29) → 30

a₁(101) → 102

a₁(97) → 98

a₁(102) → 103

b₃(383) → 384

b₃(372) → 373

b₃(374) → 375

b₃(415) → 416

b₃(386) → 387

b₃(413) → 414

b₃(353) → 354

b₃(385) → 386

b₃(412) → 413

b₃(384) → 385

b₃(414) → 415

b₃(351) → 352

b₃(375) → 376

b₃(350) → 351

b₃(373) → 374

b₃(352) → 353

b₀(15) → 10

b₀(6) → 7

b₀(13) → 14

b₀(5) → 6

b₀(14) → 15

b₀(12) → 13

b₀(2) → 3

b₀(3) → 4

b₀(4) → 5

b₀(7) → 8

157	→	19
322	→	167
376	→	124
102	→	164
102	→	304
102	→	346
128	→	224
128	→	232
128	→	327
128	→	370
103	→	58
103	→	18
103	→	275
103	→	113
103	→	99
98	→	122
98	→	252
10	→	80
10	→	4
10	→	3
10	→	295
10	→	97
10	→	96
274	→	24
274	→	168
387	→	168
387	→	24
97	→	166
97	→	295
129	→	218
129	→	283
129	→	319
211	→	50
119	→	216
119	→	281
119	→	306
119	→	348
276	→	269
299	→	123
18	→	58
227	→	150
120	→	210
120	→	298
120	→	344
57	→	21
333	→	368
333	→	406
333	→	410
225	→	150
347	→	253
219	→	23
209	→	50
130	→	102
99	→	113
99	→	275
305	→	123
165	→	50
101	→	158
101	→	184
101	→	321
334	→	359
334	→	397
416	→	329
297	→	170
343	→	328
79	→	59
201	→	114
251	→	233
407	→	253
172	→	200
172	→	268
172	→	381
173	→	226
173	→	239
173	→	336
121	→	18
121	→	103
337	→	328
345	→	253
174	→	101
82	→	26
2	→	95
4	→	22
4	→	80
28	→	78
258	→	151
258	→	329
284	→	185
369	→	123
66	→	16
100	→	149
100	→	250
100	→	342
335	→	100
282	→	185
217	→	23
30	→	20
240	→	233
17	→	49
190	→	60
190	→	115
360	→	114
398	→	382
159	→	23
320	→	167
203	→	59
354	→	115
155	→	208
156	→	202
238	→	51
238	→	124
307	→	167
c₃(371)	→	372
c₃(411)	→	412
c₃(410)	→	411
c₃(381)	→	382
c₃(370)	→	371
c₃(349)	→	350
c₃(348)	→	349
c₃(382)	→	383
c₁(80)	→	81
c₁(81)	→	82
b₂(331)	→	332
b₂(255)	→	256
b₂(235)	→	236
b₂(117)	→	118
b₂(188)	→	189
b₂(124)	→	125
b₂(113)	→	114
b₂(167)	→	168
b₂(186)	→	187
b₂(319)	→	320
b₂(234)	→	235
b₂(115)	→	116
b₂(254)	→	255
b₂(336)	→	337
b₂(114)	→	115
b₂(123)	→	124
b₂(332)	→	333
b₂(187)	→	188
b₂(329)	→	330
b₂(270)	→	271
b₂(321)	→	322
b₂(126)	→	127
b₂(298)	→	299
b₂(125)	→	126
b₂(342)	→	343
b₂(359)	→	360
b₂(200)	→	201
b₂(273)	→	274
b₂(169)	→	170
b₂(118)	→	119
b₂(257)	→	258
b₂(236)	→	237
b₂(116)	→	117
b₂(304)	→	305
b₂(170)	→	171
b₂(306)	→	307
b₂(168)	→	169
b₂(330)	→	331
b₂(256)	→	257
b₂(166)	→	167
b₂(328)	→	329
b₂(327)	→	328
b₂(271)	→	272
b₂(189)	→	190
b₂(237)	→	238
b₂(127)	→	128
b₂(368)	→	369
b₂(171)	→	172
b₂(122)	→	123
b₂(272)	→	273
b₁(226)	→	227
b₁(151)	→	152
b₁(23)	→	24
b₁(150)	→	151
b₁(26)	→	27
b₁(218)	→	219
b₁(78)	→	79
b₁(216)	→	217
b₁(63)	→	64
b₁(59)	→	60
b₁(58)	→	59
b₁(51)	→	52
b₁(210)	→	211
b₁(95)	→	96
b₁(60)	→	61
b₁(152)	→	153
b₁(149)	→	150
b₁(158)	→	159
b₁(202)	→	203
b₁(164)	→	165
b₁(154)	→	155
b₁(25)	→	26
b₁(54)	→	55
b₁(96)	→	97
b₁(50)	→	51
b₁(208)	→	209
b₁(61)	→	62
b₁(224)	→	225
b₁(27)	→	28
b₁(49)	→	50
b₁(53)	→	54
b₁(62)	→	63
b₁(153)	→	154
b₁(24)	→	25
b₁(22)	→	23
b₁(52)	→	53
f3₀	→	2
a₀(20)	→	21
a₀(17)	→	18
a₀(9)	→	1
a₀(8)	→	9
a₀(19)	→	20
a₀(21)	→	16
a₀(18)	→	19
a₀(4)	→	17
c₂(283)	→	284
c₂(296)	→	297
c₂(406)	→	407
c₂(397)	→	398
c₂(344)	→	345
c₂(281)	→	282
c₂(269)	→	270
c₂(184)	→	185
c₂(295)	→	296
c₂(275)	→	276
c₂(239)	→	240
c₂(232)	→	233
c₂(346)	→	347
c₂(185)	→	186
c₂(250)	→	251
c₂(233)	→	234
c₂(268)	→	269
c₂(253)	→	254
c₂(252)	→	253
a₂(333)	→	334
a₂(128)	→	129
a₂(172)	→	173
a₂(120)	→	121
a₂(173)	→	174
a₂(119)	→	120
a₂(334)	→	335
a₂(129)	→	130
c₀(11)	→	12
c₀(2)	→	11
a₁(28)	→	29
a₁(56)	→	57
a₁(156)	→	157
a₁(65)	→	66
a₁(98)	→	99
a₁(64)	→	65
a₁(99)	→	100
a₁(55)	→	56
a₁(155)	→	156
a₁(100)	→	101
a₁(29)	→	30
a₁(101)	→	102
a₁(97)	→	98
a₁(102)	→	103
b₃(383)	→	384
b₃(372)	→	373
b₃(374)	→	375
b₃(415)	→	416
b₃(386)	→	387
b₃(413)	→	414
b₃(353)	→	354
b₃(385)	→	386
b₃(412)	→	413
b₃(384)	→	385
b₃(414)	→	415
b₃(351)	→	352
b₃(375)	→	376
b₃(350)	→	351
b₃(373)	→	374
b₃(352)	→	353
b₀(15)	→	10
b₀(6)	→	7
b₀(13)	→	14
b₀(5)	→	6
b₀(14)	→	15
b₀(12)	→	13
b₀(2)	→	3
b₀(3)	→	4
b₀(4)	→	5
b₀(7)	→	8