YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

a(b(a(a(a(a(b(x0)))))))

→

b(a(a(a(a(b(b(a(a(a(a(b(a(x0)))))))))))))

Proof

1 Bounds

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

final states:

{1}

transitions:

322 → 268

280 → 254

98 → 30

3 → 85

50 → 99

218 → 365

9 → 29

224 → 198

1 → 5

1 → 3

1 → 382

1 → 214

1 → 88

392 → 366

44 → 155

86 → 211

36 → 43

36 → 407

336 → 310

204 → 309

212 → 379

112 → 8

30 → 141

42 → 6

42 → 86

42 → 383

42 → 215

42 → 89

434 → 380

434 → 385

434 → 217

434 → 91

414 → 421

198 → 323

154 → 44

154 → 408

168 → 100

462 → 422

148 → 253

142 → 267

378 → 324

92 → 197

266 → 156

266 → 450

210 → 142

56 → 7

408 → 449

420 → 212

420 → 384

420 → 216

420 → 90

b₃(279) → 280

b₃(427) → 428

b₃(254) → 255

b₃(260) → 261

b₃(456) → 457

b₃(371) → 372

b₃(310) → 311

b₃(372) → 373

b₃(316) → 317

b₃(380) → 381

b₃(461) → 462

b₃(335) → 336

b₃(366) → 367

b₃(321) → 322

b₃(273) → 274

b₃(268) → 269

b₃(377) → 378

b₃(433) → 434

b₃(315) → 316

b₃(324) → 325

b₃(428) → 429

b₃(274) → 275

b₃(450) → 451

b₃(386) → 387

b₃(455) → 456

b₃(391) → 392

b₃(265) → 266

b₃(259) → 260

b₃(330) → 331

b₃(329) → 330

b₃(385) → 386

b₃(422) → 423

a₃(331) → 332

a₃(323) → 324

a₃(255) → 256

a₃(373) → 374

a₃(269) → 270

a₃(388) → 389

a₃(311) → 312

a₃(261) → 262

a₃(275) → 276

a₃(451) → 452

a₃(458) → 459

a₃(326) → 327

a₃(375) → 376

a₃(429) → 430

a₃(318) → 319

a₃(389) → 390

a₃(319) → 320

a₃(423) → 424

a₃(309) → 310

a₃(382) → 383

a₃(263) → 264

a₃(431) → 432

a₃(369) → 370

a₃(379) → 380

a₃(383) → 384

a₃(376) → 377

a₃(267) → 268

a₃(325) → 326

a₃(317) → 318

a₃(426) → 427

a₃(454) → 455

a₃(258) → 259

a₃(453) → 454

a₃(332) → 333

a₃(374) → 375

a₃(333) → 334

a₃(387) → 388

a₃(421) → 422

a₃(270) → 271

a₃(334) → 335

a₃(457) → 458

a₃(390) → 391

a₃(253) → 254

a₃(277) → 278

a₃(276) → 277

a₃(367) → 368

a₃(320) → 321

a₃(257) → 258

a₃(460) → 461

a₃(262) → 263

a₃(424) → 425

a₃(313) → 314

a₃(365) → 366

a₃(384) → 385

a₃(314) → 315

a₃(459) → 460

a₃(449) → 450

a₃(256) → 257

a₃(328) → 329

a₃(327) → 328

a₃(271) → 272

a₃(430) → 431

a₃(370) → 371

a₃(312) → 313

a₃(264) → 265

a₃(381) → 382

a₃(368) → 369

a₃(278) → 279

a₃(452) → 453

a₃(425) → 426

a₃(432) → 433

a₃(272) → 273

a₂(151) → 152

a₂(219) → 220

a₂(206) → 207

a₂(150) → 151

a₂(165) → 166

a₂(200) → 201

a₂(412) → 413

a₂(216) → 217

a₂(159) → 160

a₂(144) → 145

a₂(160) → 161

a₂(199) → 200

a₂(166) → 167

a₂(207) → 208

a₂(418) → 419

a₂(205) → 206

a₂(409) → 410

a₂(143) → 144

a₂(220) → 221

a₂(213) → 214

a₂(152) → 153

a₂(149) → 150

a₂(155) → 156

a₂(158) → 159

a₂(201) → 202

a₂(202) → 203

a₂(197) → 198

a₂(222) → 223

a₂(164) → 165

a₂(416) → 417

a₂(407) → 408

a₂(221) → 222

a₂(415) → 416

a₂(163) → 164

a₂(145) → 146

a₂(146) → 147

a₂(208) → 209

a₂(215) → 216

a₂(410) → 411

a₂(411) → 412

a₂(141) → 142

a₂(214) → 215

a₂(417) → 418

a₂(211) → 212

a₂(157) → 158

b₀(3) → 4

b₀(8) → 9

b₀(14) → 1

b₀(9) → 10

a₀(5) → 6

a₀(7) → 8

a₀(10) → 11

a₀(2) → 3

a₀(12) → 13

a₀(6) → 7

a₀(4) → 5

a₀(11) → 12

a₀(13) → 14

f2₀ → 2

a₁(96) → 97

a₁(104) → 105

a₁(37) → 38

a₁(93) → 94

a₁(51) → 52

a₁(40) → 41

a₁(29) → 30

a₁(101) → 102

a₁(88) → 89

a₁(39) → 40

a₁(54) → 55

a₁(95) → 96

a₁(94) → 95

a₁(38) → 39

a₁(107) → 108

a₁(53) → 54

a₁(85) → 86

a₁(31) → 32

a₁(45) → 46

a₁(52) → 53

a₁(108) → 109

a₁(43) → 44

a₁(99) → 100

a₁(48) → 49

a₁(103) → 104

a₁(34) → 35

a₁(90) → 91

a₁(109) → 110

a₁(33) → 34

a₁(110) → 111

a₁(47) → 48

a₁(46) → 47

a₁(32) → 33

a₁(87) → 88

a₁(102) → 103

a₁(89) → 90

b₂(167) → 168

b₂(156) → 157

b₂(414) → 415

b₂(204) → 205

b₂(217) → 218

b₂(408) → 409

b₂(223) → 224

b₂(147) → 148

b₂(218) → 219

b₂(203) → 204

b₂(198) → 199

b₂(161) → 162

b₂(419) → 420

b₂(413) → 414

b₂(142) → 143

b₂(212) → 213

b₂(209) → 210

b₂(162) → 163

b₂(148) → 149

b₂(153) → 154

b₁(44) → 45

b₁(97) → 98

b₁(100) → 101

b₁(41) → 42

b₁(105) → 106

b₁(86) → 87

b₁(106) → 107

b₁(55) → 56

b₁(92) → 93

b₁(91) → 92

b₁(35) → 36

b₁(111) → 112

b₁(49) → 50

b₁(36) → 37

b₁(30) → 31

b₁(50) → 51

322	→	268
280	→	254
98	→	30
3	→	85
50	→	99
218	→	365
9	→	29
224	→	198
1	→	5
1	→	3
1	→	382
1	→	214
1	→	88
392	→	366
44	→	155
86	→	211
36	→	43
36	→	407
336	→	310
204	→	309
212	→	379
112	→	8
30	→	141
42	→	6
42	→	86
42	→	383
42	→	215
42	→	89
434	→	380
434	→	385
434	→	217
434	→	91
414	→	421
198	→	323
154	→	44
154	→	408
168	→	100
462	→	422
148	→	253
142	→	267
378	→	324
92	→	197
266	→	156
266	→	450
210	→	142
56	→	7
408	→	449
420	→	212
420	→	384
420	→	216
420	→	90
b₃(279)	→	280
b₃(427)	→	428
b₃(254)	→	255
b₃(260)	→	261
b₃(456)	→	457
b₃(371)	→	372
b₃(310)	→	311
b₃(372)	→	373
b₃(316)	→	317
b₃(380)	→	381
b₃(461)	→	462
b₃(335)	→	336
b₃(366)	→	367
b₃(321)	→	322
b₃(273)	→	274
b₃(268)	→	269
b₃(377)	→	378
b₃(433)	→	434
b₃(315)	→	316
b₃(324)	→	325
b₃(428)	→	429
b₃(274)	→	275
b₃(450)	→	451
b₃(386)	→	387
b₃(455)	→	456
b₃(391)	→	392
b₃(265)	→	266
b₃(259)	→	260
b₃(330)	→	331
b₃(329)	→	330
b₃(385)	→	386
b₃(422)	→	423
a₃(331)	→	332
a₃(323)	→	324
a₃(255)	→	256
a₃(373)	→	374
a₃(269)	→	270
a₃(388)	→	389
a₃(311)	→	312
a₃(261)	→	262
a₃(275)	→	276
a₃(451)	→	452
a₃(458)	→	459
a₃(326)	→	327
a₃(375)	→	376
a₃(429)	→	430
a₃(318)	→	319
a₃(389)	→	390
a₃(319)	→	320
a₃(423)	→	424
a₃(309)	→	310
a₃(382)	→	383
a₃(263)	→	264
a₃(431)	→	432
a₃(369)	→	370
a₃(379)	→	380
a₃(383)	→	384
a₃(376)	→	377
a₃(267)	→	268
a₃(325)	→	326
a₃(317)	→	318
a₃(426)	→	427
a₃(454)	→	455
a₃(258)	→	259
a₃(453)	→	454
a₃(332)	→	333
a₃(374)	→	375
a₃(333)	→	334
a₃(387)	→	388
a₃(421)	→	422
a₃(270)	→	271
a₃(334)	→	335
a₃(457)	→	458
a₃(390)	→	391
a₃(253)	→	254
a₃(277)	→	278
a₃(276)	→	277
a₃(367)	→	368
a₃(320)	→	321
a₃(257)	→	258
a₃(460)	→	461
a₃(262)	→	263
a₃(424)	→	425
a₃(313)	→	314
a₃(365)	→	366
a₃(384)	→	385
a₃(314)	→	315
a₃(459)	→	460
a₃(449)	→	450
a₃(256)	→	257
a₃(328)	→	329
a₃(327)	→	328
a₃(271)	→	272
a₃(430)	→	431
a₃(370)	→	371
a₃(312)	→	313
a₃(264)	→	265
a₃(381)	→	382
a₃(368)	→	369
a₃(278)	→	279
a₃(452)	→	453
a₃(425)	→	426
a₃(432)	→	433
a₃(272)	→	273
a₂(151)	→	152
a₂(219)	→	220
a₂(206)	→	207
a₂(150)	→	151
a₂(165)	→	166
a₂(200)	→	201
a₂(412)	→	413
a₂(216)	→	217
a₂(159)	→	160
a₂(144)	→	145
a₂(160)	→	161
a₂(199)	→	200
a₂(166)	→	167
a₂(207)	→	208
a₂(418)	→	419
a₂(205)	→	206
a₂(409)	→	410
a₂(143)	→	144
a₂(220)	→	221
a₂(213)	→	214
a₂(152)	→	153
a₂(149)	→	150
a₂(155)	→	156
a₂(158)	→	159
a₂(201)	→	202
a₂(202)	→	203
a₂(197)	→	198
a₂(222)	→	223
a₂(164)	→	165
a₂(416)	→	417
a₂(407)	→	408
a₂(221)	→	222
a₂(415)	→	416
a₂(163)	→	164
a₂(145)	→	146
a₂(146)	→	147
a₂(208)	→	209
a₂(215)	→	216
a₂(410)	→	411
a₂(411)	→	412
a₂(141)	→	142
a₂(214)	→	215
a₂(417)	→	418
a₂(211)	→	212
a₂(157)	→	158
b₀(3)	→	4
b₀(8)	→	9
b₀(14)	→	1
b₀(9)	→	10
a₀(5)	→	6
a₀(7)	→	8
a₀(10)	→	11
a₀(2)	→	3
a₀(12)	→	13
a₀(6)	→	7
a₀(4)	→	5
a₀(11)	→	12
a₀(13)	→	14
f2₀	→	2
a₁(96)	→	97
a₁(104)	→	105
a₁(37)	→	38
a₁(93)	→	94
a₁(51)	→	52
a₁(40)	→	41
a₁(29)	→	30
a₁(101)	→	102
a₁(88)	→	89
a₁(39)	→	40
a₁(54)	→	55
a₁(95)	→	96
a₁(94)	→	95
a₁(38)	→	39
a₁(107)	→	108
a₁(53)	→	54
a₁(85)	→	86
a₁(31)	→	32
a₁(45)	→	46
a₁(52)	→	53
a₁(108)	→	109
a₁(43)	→	44
a₁(99)	→	100
a₁(48)	→	49
a₁(103)	→	104
a₁(34)	→	35
a₁(90)	→	91
a₁(109)	→	110
a₁(33)	→	34
a₁(110)	→	111
a₁(47)	→	48
a₁(46)	→	47
a₁(32)	→	33
a₁(87)	→	88
a₁(102)	→	103
a₁(89)	→	90
b₂(167)	→	168
b₂(156)	→	157
b₂(414)	→	415
b₂(204)	→	205
b₂(217)	→	218
b₂(408)	→	409
b₂(223)	→	224
b₂(147)	→	148
b₂(218)	→	219
b₂(203)	→	204
b₂(198)	→	199
b₂(161)	→	162
b₂(419)	→	420
b₂(413)	→	414
b₂(142)	→	143
b₂(212)	→	213
b₂(209)	→	210
b₂(162)	→	163
b₂(148)	→	149
b₂(153)	→	154
b₁(44)	→	45
b₁(97)	→	98
b₁(100)	→	101
b₁(41)	→	42
b₁(105)	→	106
b₁(86)	→	87
b₁(106)	→	107
b₁(55)	→	56
b₁(92)	→	93
b₁(91)	→	92
b₁(35)	→	36
b₁(111)	→	112
b₁(49)	→	50
b₁(36)	→	37
b₁(30)	→	31
b₁(50)	→	51