YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(x0))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(x0)))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0)))))))))))))))))))))))))))))))
0(1(2(1(x0))))	→	1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x0))))))))))))))))))))))))))))))))))

Proof

1 Bounds

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

final states:

{61, 54, 47, 40, 33, 26, 19, 12, 1}

transitions:

33 → 5

111 → 116

221 → 213

25 → 306

61 → 5

32 → 310

315 → 80

89 → 8

271 → 57

273 → 265

303 → 80

167 → 29

299 → 291

18 → 302

39 → 314

218 → 235

219 → 43

331 → 80

319 → 80

241 → 246

193 → 36

293 → 298

1 → 5

40 → 5

60 → 326

323 → 80

26 → 5

297 → 64

91 → 83

141 → 22

311 → 80

88 → 105

54 → 5

270 → 287

67 → 330

143 → 135

53 → 322

117 → 109

11 → 79

244 → 261

114 → 131

12 → 5

85 → 90

169 → 161

140 → 157

137 → 142

46 → 318

189 → 194

115 → 15

245 → 50

47 → 5

267 → 272

215 → 220

195 → 187

19 → 5

166 → 183

163 → 168

192 → 209

327 → 80

247 → 239

307 → 80

0₁(211) → 212

0₁(292) → 293

0₁(162) → 163

0₁(240) → 241

0₁(159) → 160

0₁(133) → 134

0₁(237) → 238

0₁(289) → 290

0₁(84) → 85

0₁(136) → 137

0₁(110) → 111

0₁(214) → 215

0₁(81) → 82

0₁(107) → 108

0₁(263) → 264

0₁(185) → 186

0₁(266) → 267

0₁(188) → 189

2₁(295) → 296

2₁(326) → 327

2₁(165) → 166

2₁(298) → 299

2₁(306) → 307

2₁(272) → 273

2₁(183) → 184

2₁(160) → 161

2₁(108) → 109

2₁(212) → 213

2₁(142) → 143

2₁(322) → 323

2₁(310) → 311

2₁(217) → 218

2₁(105) → 106

2₁(168) → 169

2₁(220) → 221

2₁(134) → 135

2₁(79) → 80

2₁(314) → 315

2₁(194) → 195

2₁(209) → 210

2₁(131) → 132

2₁(90) → 91

2₁(87) → 88

2₁(238) → 239

2₁(82) → 83

2₁(243) → 244

2₁(139) → 140

2₁(264) → 265

2₁(113) → 114

2₁(116) → 117

2₁(235) → 236

2₁(191) → 192

2₁(261) → 262

2₁(287) → 288

2₁(318) → 319

2₁(246) → 247

2₁(302) → 303

2₁(269) → 270

2₁(330) → 331

2₁(290) → 291

2₁(157) → 158

2₁(186) → 187

f3₀ → 2

1₀(20) → 21

1₀(51) → 52

1₀(37) → 38

1₀(29) → 30

1₀(64) → 65

1₀(43) → 44

1₀(9) → 10

1₀(58) → 59

1₀(8) → 9

1₀(32) → 26

1₀(41) → 42

1₀(15) → 16

1₀(18) → 12

1₀(16) → 17

1₀(27) → 28

1₀(25) → 19

1₀(57) → 58

1₀(23) → 24

1₀(6) → 7

1₀(65) → 66

1₀(55) → 56

1₀(60) → 54

1₀(39) → 33

1₀(36) → 37

1₀(30) → 31

1₀(11) → 1

1₀(44) → 45

1₀(46) → 40

1₀(62) → 63

1₀(50) → 51

1₀(3) → 4

1₀(67) → 61

1₀(13) → 14

1₀(48) → 49

1₀(22) → 23

1₀(34) → 35

1₀(53) → 47

0₀(28) → 29

0₀(14) → 15

0₀(7) → 8

0₀(63) → 64

0₀(49) → 50

0₀(4) → 5

0₀(42) → 43

0₀(56) → 57

0₀(35) → 36

0₀(21) → 22

1₁(163) → 164

1₁(114) → 115

1₁(288) → 289

1₁(184) → 185

1₁(213) → 214

1₁(166) → 167

1₁(80) → 81

1₁(215) → 216

1₁(294) → 295

1₁(189) → 190

1₁(291) → 292

1₁(239) → 240

1₁(236) → 237

1₁(138) → 139

1₁(244) → 245

1₁(164) → 165

1₁(86) → 87

1₁(192) → 193

1₁(135) → 136

1₁(218) → 219

1₁(83) → 84

1₁(140) → 141

1₁(132) → 133

1₁(216) → 217

1₁(262) → 263

1₁(241) → 242

1₁(111) → 112

1₁(161) → 162

1₁(112) → 113

1₁(137) → 138

1₁(267) → 268

1₁(293) → 294

1₁(85) → 86

1₁(268) → 269

1₁(270) → 271

1₁(187) → 188

1₁(242) → 243

1₁(109) → 110

1₁(190) → 191

1₁(210) → 211

1₁(106) → 107

1₁(296) → 297

1₁(88) → 89

1₁(158) → 159

1₁(265) → 266

2₀(22) → 27

2₀(66) → 67

2₀(38) → 39

2₀(24) → 25

2₀(8) → 13

2₀(10) → 11

2₀(15) → 20

2₀(29) → 34

2₀(17) → 18

2₀(45) → 46

2₀(5) → 6

2₀(59) → 60

2₀(31) → 32

2₀(2) → 3

2₀(57) → 62

2₀(52) → 53

2₀(36) → 41

2₀(43) → 48

2₀(50) → 55

33	→	5
111	→	116
221	→	213
25	→	306
61	→	5
32	→	310
315	→	80
89	→	8
271	→	57
273	→	265
303	→	80
167	→	29
299	→	291
18	→	302
39	→	314
218	→	235
219	→	43
331	→	80
319	→	80
241	→	246
193	→	36
293	→	298
1	→	5
40	→	5
60	→	326
323	→	80
26	→	5
297	→	64
91	→	83
141	→	22
311	→	80
88	→	105
54	→	5
270	→	287
67	→	330
143	→	135
53	→	322
117	→	109
11	→	79
244	→	261
114	→	131
12	→	5
85	→	90
169	→	161
140	→	157
137	→	142
46	→	318
189	→	194
115	→	15
245	→	50
47	→	5
267	→	272
215	→	220
195	→	187
19	→	5
166	→	183
163	→	168
192	→	209
327	→	80
247	→	239
307	→	80
0₁(211)	→	212
0₁(292)	→	293
0₁(162)	→	163
0₁(240)	→	241
0₁(159)	→	160
0₁(133)	→	134
0₁(237)	→	238
0₁(289)	→	290
0₁(84)	→	85
0₁(136)	→	137
0₁(110)	→	111
0₁(214)	→	215
0₁(81)	→	82
0₁(107)	→	108
0₁(263)	→	264
0₁(185)	→	186
0₁(266)	→	267
0₁(188)	→	189
2₁(295)	→	296
2₁(326)	→	327
2₁(165)	→	166
2₁(298)	→	299
2₁(306)	→	307
2₁(272)	→	273
2₁(183)	→	184
2₁(160)	→	161
2₁(108)	→	109
2₁(212)	→	213
2₁(142)	→	143
2₁(322)	→	323
2₁(310)	→	311
2₁(217)	→	218
2₁(105)	→	106
2₁(168)	→	169
2₁(220)	→	221
2₁(134)	→	135
2₁(79)	→	80
2₁(314)	→	315
2₁(194)	→	195
2₁(209)	→	210
2₁(131)	→	132
2₁(90)	→	91
2₁(87)	→	88
2₁(238)	→	239
2₁(82)	→	83
2₁(243)	→	244
2₁(139)	→	140
2₁(264)	→	265
2₁(113)	→	114
2₁(116)	→	117
2₁(235)	→	236
2₁(191)	→	192
2₁(261)	→	262
2₁(287)	→	288
2₁(318)	→	319
2₁(246)	→	247
2₁(302)	→	303
2₁(269)	→	270
2₁(330)	→	331
2₁(290)	→	291
2₁(157)	→	158
2₁(186)	→	187
f3₀	→	2
1₀(20)	→	21
1₀(51)	→	52
1₀(37)	→	38
1₀(29)	→	30
1₀(64)	→	65
1₀(43)	→	44
1₀(9)	→	10
1₀(58)	→	59
1₀(8)	→	9
1₀(32)	→	26
1₀(41)	→	42
1₀(15)	→	16
1₀(18)	→	12
1₀(16)	→	17
1₀(27)	→	28
1₀(25)	→	19
1₀(57)	→	58
1₀(23)	→	24
1₀(6)	→	7
1₀(65)	→	66
1₀(55)	→	56
1₀(60)	→	54
1₀(39)	→	33
1₀(36)	→	37
1₀(30)	→	31
1₀(11)	→	1
1₀(44)	→	45
1₀(46)	→	40
1₀(62)	→	63
1₀(50)	→	51
1₀(3)	→	4
1₀(67)	→	61
1₀(13)	→	14
1₀(48)	→	49
1₀(22)	→	23
1₀(34)	→	35
1₀(53)	→	47
0₀(28)	→	29
0₀(14)	→	15
0₀(7)	→	8
0₀(63)	→	64
0₀(49)	→	50
0₀(4)	→	5
0₀(42)	→	43
0₀(56)	→	57
0₀(35)	→	36
0₀(21)	→	22
1₁(163)	→	164
1₁(114)	→	115
1₁(288)	→	289
1₁(184)	→	185
1₁(213)	→	214
1₁(166)	→	167
1₁(80)	→	81
1₁(215)	→	216
1₁(294)	→	295
1₁(189)	→	190
1₁(291)	→	292
1₁(239)	→	240
1₁(236)	→	237
1₁(138)	→	139
1₁(244)	→	245
1₁(164)	→	165
1₁(86)	→	87
1₁(192)	→	193
1₁(135)	→	136
1₁(218)	→	219
1₁(83)	→	84
1₁(140)	→	141
1₁(132)	→	133
1₁(216)	→	217
1₁(262)	→	263
1₁(241)	→	242
1₁(111)	→	112
1₁(161)	→	162
1₁(112)	→	113
1₁(137)	→	138
1₁(267)	→	268
1₁(293)	→	294
1₁(85)	→	86
1₁(268)	→	269
1₁(270)	→	271
1₁(187)	→	188
1₁(242)	→	243
1₁(109)	→	110
1₁(190)	→	191
1₁(210)	→	211
1₁(106)	→	107
1₁(296)	→	297
1₁(88)	→	89
1₁(158)	→	159
1₁(265)	→	266
2₀(22)	→	27
2₀(66)	→	67
2₀(38)	→	39
2₀(24)	→	25
2₀(8)	→	13
2₀(10)	→	11
2₀(15)	→	20
2₀(29)	→	34
2₀(17)	→	18
2₀(45)	→	46
2₀(5)	→	6
2₀(59)	→	60
2₀(31)	→	32
2₀(2)	→	3
2₀(57)	→	62
2₀(52)	→	53
2₀(36)	→	41
2₀(43)	→	48
2₀(50)	→	55