YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

0(1(2(x0)))	→	0(3(1(2(x0))))
0(1(2(x0)))	→	1(0(2(1(x0))))
0(1(2(x0)))	→	2(1(4(0(x0))))
0(1(2(x0)))	→	0(2(1(3(3(x0)))))
0(1(2(x0)))	→	0(2(4(1(3(x0)))))
0(1(2(x0)))	→	1(0(2(5(4(x0)))))
0(1(2(x0)))	→	2(1(1(0(3(x0)))))
0(1(2(x0)))	→	2(1(3(4(0(x0)))))
0(1(2(x0)))	→	2(1(4(3(0(x0)))))
0(1(2(x0)))	→	4(0(3(1(2(x0)))))
0(1(2(x0)))	→	4(1(0(3(2(x0)))))
0(1(2(x0)))	→	4(4(2(1(0(x0)))))
0(1(2(x0)))	→	0(0(4(1(2(5(x0))))))
0(1(2(x0)))	→	0(4(5(1(2(5(x0))))))
0(1(2(x0)))	→	0(5(2(3(1(4(x0))))))
0(1(2(x0)))	→	1(0(2(2(3(4(x0))))))
0(1(2(x0)))	→	1(1(4(0(3(2(x0))))))
0(1(2(x0)))	→	2(0(0(3(3(1(x0))))))
0(1(2(x0)))	→	2(0(3(4(1(5(x0))))))
0(1(2(x0)))	→	2(3(2(0(4(1(x0))))))
0(1(2(x0)))	→	2(5(3(0(3(1(x0))))))
0(1(2(x0)))	→	3(2(5(3(1(0(x0))))))
0(1(2(x0)))	→	3(4(0(5(1(2(x0))))))
0(1(2(x0)))	→	5(5(4(2(1(0(x0))))))
0(0(1(2(x0))))	→	0(0(2(4(1(x0)))))
0(0(1(2(x0))))	→	0(2(1(5(0(4(x0))))))
0(0(1(2(x0))))	→	1(0(2(3(5(0(x0))))))
0(0(1(2(x0))))	→	5(1(2(0(4(0(x0))))))
0(0(5(2(x0))))	→	5(3(0(3(0(2(x0))))))
0(1(2(0(x0))))	→	1(2(4(0(0(x0)))))
0(1(2(0(x0))))	→	0(4(1(0(0(2(x0))))))
0(1(2(2(x0))))	→	3(3(0(2(1(2(x0))))))
0(1(5(2(x0))))	→	2(5(1(0(3(x0)))))
0(1(5(2(x0))))	→	0(5(5(3(1(2(x0))))))
0(1(5(2(x0))))	→	1(3(5(0(2(2(x0))))))
0(5(2(2(x0))))	→	3(0(2(1(5(2(x0))))))
1(0(1(2(x0))))	→	0(4(1(2(1(x0)))))
1(0(1(2(x0))))	→	1(2(1(3(0(x0)))))
1(0(1(2(x0))))	→	0(3(1(4(1(2(x0))))))
1(0(1(2(x0))))	→	4(1(4(1(0(2(x0))))))
5(0(1(2(x0))))	→	0(2(1(3(5(x0)))))
5(0(1(2(x0))))	→	2(0(3(1(5(x0)))))
5(0(1(2(x0))))	→	5(3(1(0(3(2(x0))))))
5(0(1(2(x0))))	→	5(5(1(0(2(4(x0))))))
0(1(0(2(2(x0)))))	→	3(0(2(1(0(2(x0))))))
0(1(2(5(2(x0)))))	→	3(5(1(2(2(0(x0))))))
0(1(3(0(0(x0)))))	→	0(0(4(1(3(0(x0))))))
0(1(4(2(2(x0)))))	→	0(2(4(1(5(2(x0))))))
0(1(4(2(2(x0)))))	→	0(2(4(2(1(1(x0))))))
1(3(0(1(2(x0)))))	→	1(3(4(1(0(2(x0))))))

Proof

1 Bounds

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

final states:

{195, 190, 187, 184, 179, 176, 171, 169, 166, 162, 158, 154, 151, 148, 143, 138, 135, 133, 129, 125, 121, 116, 112, 107, 102, 99, 97, 93, 89, 85, 80, 75, 70, 67, 62, 57, 54, 48, 44, 40, 39, 35, 32, 28, 23, 19, 14, 10, 6, 1}

transitions:

272 → 334

272 → 339

23 → 11

239 → 122

322 → 233

176 → 11

102 → 122

102 → 11

32 → 11

89 → 11

338 → 233

80 → 11

10 → 11

273 → 236

97 → 11

129 → 11

352 → 383

133 → 11

184 → 11

57 → 11

187 → 11

341 → 236

59 → 204

325 → 233

99 → 122

99 → 11

304 → 387

224 → 122

107 → 122

107 → 11

62 → 11

1 → 11

40 → 11

123 → 230

123 → 235

123 → 250

123 → 255

123 → 271

123 → 317

390 → 223

44 → 11

135 → 11

402 → 223

179 → 11

125 → 11

251 → 289

251 → 303

138 → 11

121 → 11

171 → 108

171 → 49

6 → 11

302 → 291

404 → 209

116 → 122

116 → 11

54 → 11

75 → 11

386 → 253

292 → 122

270 → 258

368 → 354

67 → 11

350 → 238

143 → 11

301 → 348

28 → 11

232 → 399

284 → 252

252 → 283

318 → 365

14 → 11

373 → 253

93 → 11

63 → 218

306 → 291

306 → 403

12 → 11

85 → 11

112 → 122

112 → 11

169 → 108

169 → 49

236 → 351

236 → 369

282 → 252

234 → 122

234 → 291

290 → 251

162 → 108

162 → 49

35 → 11

158 → 45

158 → 7

231 → 299

256 → 268

256 → 280

48 → 11

190 → 11

154 → 45

154 → 7

254 → 122

148 → 45

148 → 7

320 → 323

259 → 233

195 → 152

195 → 20

195 → 7

19 → 11

210 → 122

70 → 11

166 → 108

166 → 49

151 → 45

151 → 7

355 → 253

3₁(351) → 352

3₁(384) → 385

3₁(339) → 340

3₁(208) → 209

3₁(255) → 256

3₁(335) → 336

3₁(223) → 224

3₁(289) → 290

3₁(206) → 207

3₁(232) → 233

3₁(299) → 300

3₁(387) → 388

3₁(367) → 368

3₁(283) → 284

3₁(256) → 257

3₁(372) → 373

3₁(352) → 353

1₁(220) → 221

1₁(349) → 350

1₁(281) → 282

1₁(231) → 232

1₁(238) → 239

1₁(235) → 236

1₁(365) → 366

1₁(252) → 253

1₁(303) → 304

1₁(257) → 258

1₁(334) → 335

1₁(319) → 320

1₁(268) → 269

1₁(301) → 302

4₁(291) → 292

4₁(251) → 252

4₁(305) → 306

4₁(366) → 367

4₁(348) → 349

4₁(269) → 270

4₁(369) → 370

4₁(401) → 402

4₁(324) → 325

4₁(271) → 272

4₁(320) → 321

2₁(253) → 254

2₁(371) → 372

2₁(221) → 222

2₁(204) → 205

2₁(318) → 319

2₁(236) → 237

2₁(230) → 231

2₁(389) → 390

2₁(340) → 341

2₁(304) → 305

2₁(258) → 259

2₁(218) → 219

2₁(336) → 337

1₀(16) → 17

1₀(11) → 45

1₀(173) → 174

1₀(30) → 31

1₀(49) → 76

1₀(37) → 38

1₀(144) → 145

1₀(3) → 4

1₀(7) → 191

1₀(33) → 34

1₀(66) → 62

1₀(24) → 58

1₀(50) → 51

1₀(8) → 149

1₀(29) → 30

1₀(111) → 107

1₀(114) → 115

1₀(142) → 138

1₀(155) → 156

1₀(68) → 69

1₀(9) → 6

1₀(27) → 23

1₀(15) → 20

1₀(42) → 43

1₀(126) → 127

1₀(196) → 195

1₀(117) → 159

1₀(181) → 182

1₀(124) → 121

1₀(36) → 152

1₀(160) → 161

1₀(163) → 164

1₀(2) → 7

1₀(69) → 67

1₀(104) → 105

1₀(12) → 13

1₀(153) → 151

2₀(109) → 110

2₀(2) → 3

2₀(25) → 26

2₀(31) → 28

2₀(82) → 83

2₀(45) → 46

2₀(21) → 22

2₀(159) → 177

2₀(74) → 70

2₀(188) → 189

2₀(152) → 153

2₀(113) → 114

2₀(193) → 194

2₀(88) → 85

2₀(4) → 130

2₀(59) → 60

2₀(24) → 172

2₀(34) → 32

2₀(164) → 165

2₀(91) → 92

2₀(123) → 124

2₀(191) → 192

2₀(105) → 106

2₀(11) → 180

2₀(134) → 133

2₀(64) → 65

2₀(13) → 10

2₀(17) → 18

2₀(63) → 64

2₀(79) → 75

2₀(84) → 80

2₀(168) → 166

2₀(180) → 181

2₀(38) → 35

2₀(49) → 50

2₀(145) → 146

2₀(3) → 139

2₀(81) → 100

2₀(7) → 8

3₀(76) → 167

3₀(183) → 179

3₀(147) → 143

3₀(160) → 196

3₀(86) → 87

3₀(108) → 109

3₀(156) → 157

3₀(7) → 71

3₀(58) → 59

3₀(178) → 176

3₀(45) → 90

3₀(132) → 129

3₀(11) → 36

3₀(43) → 170

3₀(77) → 78

3₀(92) → 89

3₀(131) → 132

3₀(3) → 41

3₀(96) → 93

3₀(12) → 33

3₀(83) → 84

3₀(15) → 16

3₀(49) → 163

3₀(117) → 118

3₀(71) → 72

3₀(119) → 120

3₀(2) → 15

3₀(141) → 142

3₀(4) → 5

3₀(24) → 63

4₀(42) → 68

4₀(47) → 44

4₀(192) → 193

4₀(46) → 47

4₀(122) → 123

4₀(152) → 185

4₀(11) → 12

4₀(36) → 37

4₀(1) → 39

4₀(4) → 155

4₀(7) → 81

4₀(43) → 40

4₀(20) → 21

4₀(161) → 158

4₀(149) → 150

4₀(159) → 160

4₀(145) → 188

4₀(95) → 96

4₀(51) → 52

4₀(76) → 77

4₀(127) → 128

4₀(55) → 56

4₀(2) → 24

5₀(90) → 91

5₀(87) → 88

5₀(60) → 61

5₀(24) → 25

5₀(175) → 171

5₀(98) → 97

5₀(120) → 116

5₀(140) → 141

5₀(5) → 136

5₀(11) → 108

5₀(182) → 183

5₀(4) → 94

5₀(174) → 175

5₀(2) → 49

5₀(3) → 144

5₀(30) → 134

5₀(170) → 169

5₀(103) → 104

5₀(115) → 112

5₀(47) → 98

5₀(136) → 137

5₀(51) → 55

f6₀ → 2

0₀(2) → 11

0₀(157) → 154

0₀(167) → 168

0₀(18) → 14

0₀(177) → 178

0₀(56) → 54

0₀(117) → 126

0₀(65) → 66

0₀(128) → 125

0₀(146) → 147

0₀(110) → 111

0₀(24) → 103

0₀(189) → 187

0₀(71) → 86

0₀(8) → 9

0₀(61) → 57

0₀(26) → 27

0₀(150) → 148

0₀(3) → 117

0₀(11) → 122

0₀(100) → 101

0₀(118) → 119

0₀(53) → 48

0₀(94) → 95

0₀(81) → 82

0₀(139) → 140

0₀(130) → 131

0₀(137) → 135

0₀(15) → 29

0₀(165) → 162

0₀(52) → 53

0₀(101) → 99

0₀(22) → 19

0₀(172) → 173

0₀(12) → 113

0₀(73) → 74

0₀(186) → 184

0₀(41) → 42

0₀(78) → 79

0₀(5) → 1

0₀(185) → 186

0₀(106) → 102

0₀(72) → 73

0₀(194) → 190

0₁(250) → 251

0₁(237) → 238

0₁(300) → 301

0₁(400) → 401

0₁(321) → 322

0₁(207) → 208

0₁(205) → 206

0₁(219) → 220

0₁(280) → 281

0₁(354) → 355

0₁(383) → 384

0₁(222) → 223

0₁(370) → 371

0₁(233) → 234

0₁(353) → 354

5₁(403) → 404

5₁(337) → 338

5₁(399) → 400

5₁(388) → 389

5₁(385) → 386

5₁(209) → 210

5₁(272) → 273

5₁(317) → 318

5₁(323) → 324

272	→	334
272	→	339
23	→	11
239	→	122
322	→	233
176	→	11
102	→	122
102	→	11
32	→	11
89	→	11
338	→	233
80	→	11
10	→	11
273	→	236
97	→	11
129	→	11
352	→	383
133	→	11
184	→	11
57	→	11
187	→	11
341	→	236
59	→	204
325	→	233
99	→	122
99	→	11
304	→	387
224	→	122
107	→	122
107	→	11
62	→	11
1	→	11
40	→	11
123	→	230
123	→	235
123	→	250
123	→	255
123	→	271
123	→	317
390	→	223
44	→	11
135	→	11
402	→	223
179	→	11
125	→	11
251	→	289
251	→	303
138	→	11
121	→	11
171	→	108
171	→	49
6	→	11
302	→	291
404	→	209
116	→	122
116	→	11
54	→	11
75	→	11
386	→	253
292	→	122
270	→	258
368	→	354
67	→	11
350	→	238
143	→	11
301	→	348
28	→	11
232	→	399
284	→	252
252	→	283
318	→	365
14	→	11
373	→	253
93	→	11
63	→	218
306	→	291
306	→	403
12	→	11
85	→	11
112	→	122
112	→	11
169	→	108
169	→	49
236	→	351
236	→	369
282	→	252
234	→	122
234	→	291
290	→	251
162	→	108
162	→	49
35	→	11
158	→	45
158	→	7
231	→	299
256	→	268
256	→	280
48	→	11
190	→	11
154	→	45
154	→	7
254	→	122
148	→	45
148	→	7
320	→	323
259	→	233
195	→	152
195	→	20
195	→	7
19	→	11
210	→	122
70	→	11
166	→	108
166	→	49
151	→	45
151	→	7
355	→	253
3₁(351)	→	352
3₁(384)	→	385
3₁(339)	→	340
3₁(208)	→	209
3₁(255)	→	256
3₁(335)	→	336
3₁(223)	→	224
3₁(289)	→	290
3₁(206)	→	207
3₁(232)	→	233
3₁(299)	→	300
3₁(387)	→	388
3₁(367)	→	368
3₁(283)	→	284
3₁(256)	→	257
3₁(372)	→	373
3₁(352)	→	353
1₁(220)	→	221
1₁(349)	→	350
1₁(281)	→	282
1₁(231)	→	232
1₁(238)	→	239
1₁(235)	→	236
1₁(365)	→	366
1₁(252)	→	253
1₁(303)	→	304
1₁(257)	→	258
1₁(334)	→	335
1₁(319)	→	320
1₁(268)	→	269
1₁(301)	→	302
4₁(291)	→	292
4₁(251)	→	252
4₁(305)	→	306
4₁(366)	→	367
4₁(348)	→	349
4₁(269)	→	270
4₁(369)	→	370
4₁(401)	→	402
4₁(324)	→	325
4₁(271)	→	272
4₁(320)	→	321
2₁(253)	→	254
2₁(371)	→	372
2₁(221)	→	222
2₁(204)	→	205
2₁(318)	→	319
2₁(236)	→	237
2₁(230)	→	231
2₁(389)	→	390
2₁(340)	→	341
2₁(304)	→	305
2₁(258)	→	259
2₁(218)	→	219
2₁(336)	→	337
1₀(16)	→	17
1₀(11)	→	45
1₀(173)	→	174
1₀(30)	→	31
1₀(49)	→	76
1₀(37)	→	38
1₀(144)	→	145
1₀(3)	→	4
1₀(7)	→	191
1₀(33)	→	34
1₀(66)	→	62
1₀(24)	→	58
1₀(50)	→	51
1₀(8)	→	149
1₀(29)	→	30
1₀(111)	→	107
1₀(114)	→	115
1₀(142)	→	138
1₀(155)	→	156
1₀(68)	→	69
1₀(9)	→	6
1₀(27)	→	23
1₀(15)	→	20
1₀(42)	→	43
1₀(126)	→	127
1₀(196)	→	195
1₀(117)	→	159
1₀(181)	→	182
1₀(124)	→	121
1₀(36)	→	152
1₀(160)	→	161
1₀(163)	→	164
1₀(2)	→	7
1₀(69)	→	67
1₀(104)	→	105
1₀(12)	→	13
1₀(153)	→	151
2₀(109)	→	110
2₀(2)	→	3
2₀(25)	→	26
2₀(31)	→	28
2₀(82)	→	83
2₀(45)	→	46
2₀(21)	→	22
2₀(159)	→	177
2₀(74)	→	70
2₀(188)	→	189
2₀(152)	→	153
2₀(113)	→	114
2₀(193)	→	194
2₀(88)	→	85
2₀(4)	→	130
2₀(59)	→	60
2₀(24)	→	172
2₀(34)	→	32
2₀(164)	→	165
2₀(91)	→	92
2₀(123)	→	124
2₀(191)	→	192
2₀(105)	→	106
2₀(11)	→	180
2₀(134)	→	133
2₀(64)	→	65
2₀(13)	→	10
2₀(17)	→	18
2₀(63)	→	64
2₀(79)	→	75
2₀(84)	→	80
2₀(168)	→	166
2₀(180)	→	181
2₀(38)	→	35
2₀(49)	→	50
2₀(145)	→	146
2₀(3)	→	139
2₀(81)	→	100
2₀(7)	→	8
3₀(76)	→	167
3₀(183)	→	179
3₀(147)	→	143
3₀(160)	→	196
3₀(86)	→	87
3₀(108)	→	109
3₀(156)	→	157
3₀(7)	→	71
3₀(58)	→	59
3₀(178)	→	176
3₀(45)	→	90
3₀(132)	→	129
3₀(11)	→	36
3₀(43)	→	170
3₀(77)	→	78
3₀(92)	→	89
3₀(131)	→	132
3₀(3)	→	41
3₀(96)	→	93
3₀(12)	→	33
3₀(83)	→	84
3₀(15)	→	16
3₀(49)	→	163
3₀(117)	→	118
3₀(71)	→	72
3₀(119)	→	120
3₀(2)	→	15
3₀(141)	→	142
3₀(4)	→	5
3₀(24)	→	63
4₀(42)	→	68
4₀(47)	→	44
4₀(192)	→	193
4₀(46)	→	47
4₀(122)	→	123
4₀(152)	→	185
4₀(11)	→	12
4₀(36)	→	37
4₀(1)	→	39
4₀(4)	→	155
4₀(7)	→	81
4₀(43)	→	40
4₀(20)	→	21
4₀(161)	→	158
4₀(149)	→	150
4₀(159)	→	160
4₀(145)	→	188
4₀(95)	→	96
4₀(51)	→	52
4₀(76)	→	77
4₀(127)	→	128
4₀(55)	→	56
4₀(2)	→	24
5₀(90)	→	91
5₀(87)	→	88
5₀(60)	→	61
5₀(24)	→	25
5₀(175)	→	171
5₀(98)	→	97
5₀(120)	→	116
5₀(140)	→	141
5₀(5)	→	136
5₀(11)	→	108
5₀(182)	→	183
5₀(4)	→	94
5₀(174)	→	175
5₀(2)	→	49
5₀(3)	→	144
5₀(30)	→	134
5₀(170)	→	169
5₀(103)	→	104
5₀(115)	→	112
5₀(47)	→	98
5₀(136)	→	137
5₀(51)	→	55
f6₀	→	2
0₀(2)	→	11
0₀(157)	→	154
0₀(167)	→	168
0₀(18)	→	14
0₀(177)	→	178
0₀(56)	→	54
0₀(117)	→	126
0₀(65)	→	66
0₀(128)	→	125
0₀(146)	→	147
0₀(110)	→	111
0₀(24)	→	103
0₀(189)	→	187
0₀(71)	→	86
0₀(8)	→	9
0₀(61)	→	57
0₀(26)	→	27
0₀(150)	→	148
0₀(3)	→	117
0₀(11)	→	122
0₀(100)	→	101
0₀(118)	→	119
0₀(53)	→	48
0₀(94)	→	95
0₀(81)	→	82
0₀(139)	→	140
0₀(130)	→	131
0₀(137)	→	135
0₀(15)	→	29
0₀(165)	→	162
0₀(52)	→	53
0₀(101)	→	99
0₀(22)	→	19
0₀(172)	→	173
0₀(12)	→	113
0₀(73)	→	74
0₀(186)	→	184
0₀(41)	→	42
0₀(78)	→	79
0₀(5)	→	1
0₀(185)	→	186
0₀(106)	→	102
0₀(72)	→	73
0₀(194)	→	190
0₁(250)	→	251
0₁(237)	→	238
0₁(300)	→	301
0₁(400)	→	401
0₁(321)	→	322
0₁(207)	→	208
0₁(205)	→	206
0₁(219)	→	220
0₁(280)	→	281
0₁(354)	→	355
0₁(383)	→	384
0₁(222)	→	223
0₁(370)	→	371
0₁(233)	→	234
0₁(353)	→	354
5₁(403)	→	404
5₁(337)	→	338
5₁(399)	→	400
5₁(388)	→	389
5₁(385)	→	386
5₁(209)	→	210
5₁(272)	→	273
5₁(317)	→	318
5₁(323)	→	324