YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 Bounds

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

final states:

{313, 295, 277, 259, 240, 221, 205, 192, 178, 166, 152, 141, 130, 121, 114, 101, 91, 82, 72, 63, 54, 45, 37, 29, 21, 16, 13, 8, 5, 1}

transitions:

221 → 11

221 → 17

221 → 3

205 → 9

29 → 222

338 → 50

152 → 3

5 → 223

5 → 3

37 → 46

130 → 206

130 → 222

1 → 222

8 → 9

13 → 17

13 → 3

332 → 333

101 → 22

101 → 222

91 → 222

21 → 102

21 → 222

72 → 153

72 → 3

141 → 73

141 → 9

178 → 22

178 → 222

121 → 47

121 → 30

277 → 278

277 → 55

277 → 3

54 → 3

82 → 30

313 → 131

313 → 46

45 → 3

16 → 7

16 → 6

114 → 9

63 → 73

63 → 9

295 → 46

240 → 9

259 → 7

259 → 6

166 → 9

192 → 75

192 → 278

192 → 55

192 → 3

1₁(335) → 336

1₁(336) → 337

2₁(333) → 334

1₀(189) → 190

1₀(51) → 52

1₀(74) → 75

1₀(190) → 191

1₀(180) → 181

1₀(203) → 204

1₀(46) → 153

1₀(11) → 12

1₀(245) → 246

1₀(310) → 311

1₀(127) → 128

1₀(212) → 213

1₀(200) → 201

1₀(162) → 163

1₀(30) → 55

1₀(41) → 42

1₀(252) → 253

1₀(105) → 106

1₀(25) → 26

1₀(33) → 34

1₀(222) → 223

1₀(58) → 59

1₀(273) → 274

1₀(48) → 49

1₀(24) → 25

1₀(50) → 51

1₀(286) → 287

1₀(165) → 152

1₀(159) → 160

1₀(197) → 198

1₀(288) → 289

1₀(293) → 294

1₀(108) → 109

1₀(64) → 65

1₀(248) → 249

1₀(6) → 17

1₀(136) → 137

1₀(236) → 237

1₀(204) → 192

1₀(62) → 54

1₀(15) → 13

1₀(161) → 162

1₀(81) → 72

1₀(107) → 108

1₀(10) → 11

1₀(220) → 205

1₀(4) → 122

1₀(124) → 125

1₀(14) → 15

1₀(43) → 44

1₀(139) → 140

1₀(2) → 3

1₀(298) → 299

1₀(263) → 264

1₀(213) → 214

1₀(257) → 258

1₀(164) → 165

1₀(85) → 86

1₀(17) → 18

1₀(294) → 277

1₀(241) → 278

1₀(308) → 309

1₀(103) → 104

1₀(243) → 244

1₀(264) → 265

1₀(219) → 220

4₀(73) → 74

4₀(111) → 112

4₀(331) → 332

4₀(228) → 229

4₀(2) → 30

4₀(78) → 79

4₀(132) → 133

4₀(188) → 189

4₀(6) → 314

4₀(129) → 121

4₀(211) → 212

4₀(147) → 148

4₀(32) → 33

4₀(234) → 235

4₀(4) → 167

4₀(46) → 47

4₀(112) → 113

4₀(173) → 174

4₀(77) → 78

4₀(283) → 284

4₀(218) → 219

4₀(254) → 255

4₀(242) → 243

4₀(280) → 281

4₀(89) → 90

4₀(214) → 215

4₀(199) → 200

4₀(172) → 173

4₀(324) → 325

4₀(9) → 241

4₀(125) → 126

4₀(251) → 252

4₀(143) → 144

4₀(128) → 129

4₀(195) → 196

4₀(154) → 155

4₀(265) → 266

4₀(116) → 117

4₀(182) → 183

4₀(90) → 82

4₀(131) → 132

4₀(216) → 217

4₀(274) → 275

4₀(282) → 283

4₀(53) → 45

4₀(327) → 328

4₀(96) → 97

4₀(194) → 195

4₀(30) → 31

4₀(246) → 247

4₀(7) → 5

4₀(35) → 36

3₀(226) → 227

3₀(227) → 228

3₀(126) → 127

3₀(23) → 24

3₀(70) → 71

3₀(150) → 151

3₀(315) → 316

3₀(289) → 290

3₀(19) → 20

3₀(86) → 87

3₀(217) → 218

3₀(309) → 310

3₀(99) → 100

3₀(6) → 7

3₀(60) → 61

3₀(231) → 232

3₀(134) → 135

3₀(247) → 248

3₀(79) → 80

3₀(155) → 156

3₀(158) → 159

3₀(314) → 315

3₀(56) → 57

3₀(88) → 89

3₀(46) → 64

3₀(268) → 269

3₀(3) → 4

3₀(47) → 48

3₀(271) → 272

3₀(40) → 41

3₀(284) → 285

3₀(276) → 259

3₀(64) → 142

3₀(113) → 101

3₀(9) → 10

3₀(196) → 197

3₀(146) → 147

3₀(61) → 62

3₀(305) → 306

3₀(83) → 84

3₀(275) → 276

3₀(193) → 194

3₀(27) → 28

3₀(223) → 224

3₀(287) → 288

3₀(325) → 326

3₀(20) → 16

3₀(135) → 136

3₀(31) → 32

3₀(67) → 68

3₀(318) → 319

3₀(296) → 297

3₀(17) → 92

3₀(10) → 14

3₀(93) → 94

3₀(2) → 6

3₀(302) → 303

3₀(198) → 199

3₀(66) → 67

3₀(186) → 187

5₀(170) → 171

5₀(140) → 130

5₀(42) → 43

5₀(238) → 239

5₀(191) → 178

5₀(160) → 161

5₀(142) → 143

5₀(244) → 245

5₀(255) → 256

5₀(46) → 131

5₀(281) → 282

5₀(151) → 141

5₀(177) → 166

5₀(122) → 123

5₀(153) → 154

5₀(98) → 99

5₀(208) → 209

5₀(44) → 37

5₀(169) → 170

5₀(157) → 158

5₀(28) → 21

5₀(7) → 193

5₀(323) → 324

5₀(239) → 221

5₀(118) → 119

5₀(148) → 149

5₀(285) → 286

5₀(167) → 168

5₀(209) → 210

5₀(232) → 233

5₀(9) → 38

5₀(290) → 291

5₀(307) → 308

5₀(321) → 322

5₀(80) → 81

5₀(30) → 179

5₀(102) → 103

5₀(306) → 307

5₀(137) → 138

5₀(34) → 35

5₀(292) → 293

5₀(175) → 176

5₀(185) → 186

5₀(210) → 211

5₀(262) → 263

5₀(109) → 110

5₀(68) → 69

5₀(312) → 295

5₀(233) → 234

5₀(115) → 116

5₀(12) → 8

5₀(75) → 76

5₀(253) → 254

5₀(2) → 46

0₀(267) → 268

0₀(303) → 304

0₀(235) → 236

0₀(179) → 180

0₀(261) → 262

0₀(330) → 331

0₀(87) → 88

0₀(229) → 230

0₀(230) → 231

0₀(55) → 56

0₀(18) → 19

0₀(95) → 96

0₀(94) → 95

0₀(270) → 271

0₀(322) → 323

0₀(120) → 114

0₀(7) → 83

0₀(92) → 93

0₀(258) → 240

0₀(250) → 251

0₀(225) → 226

0₀(46) → 206

0₀(22) → 23

0₀(260) → 261

0₀(181) → 182

0₀(9) → 102

0₀(183) → 184

0₀(133) → 134

0₀(215) → 216

0₀(6) → 22

0₀(84) → 85

0₀(76) → 77

0₀(241) → 242

0₀(144) → 145

0₀(201) → 202

0₀(2) → 222

0₀(163) → 164

0₀(299) → 300

0₀(26) → 27

0₀(36) → 29

0₀(316) → 317

0₀(168) → 169

0₀(149) → 150

0₀(326) → 327

0₀(110) → 111

0₀(272) → 273

0₀(329) → 330

0₀(67) → 115

0₀(104) → 105

f6₀ → 2

2₀(2) → 9

2₀(317) → 318

2₀(237) → 238

2₀(123) → 124

2₀(156) → 157

2₀(117) → 118

2₀(332) → 313

2₀(9) → 73

2₀(224) → 225

2₀(65) → 66

2₀(10) → 260

2₀(300) → 301

2₀(184) → 185

2₀(49) → 50

2₀(202) → 203

2₀(291) → 292

2₀(71) → 63

2₀(4) → 1

2₀(138) → 139

2₀(38) → 39

2₀(206) → 207

2₀(249) → 250

2₀(176) → 177

2₀(100) → 91

2₀(320) → 321

2₀(311) → 312

2₀(256) → 257

2₀(304) → 305

2₀(241) → 296

2₀(269) → 270

2₀(52) → 53

2₀(39) → 40

2₀(319) → 320

2₀(57) → 58

2₀(174) → 175

2₀(97) → 98

2₀(278) → 279

2₀(266) → 267

2₀(187) → 188

2₀(59) → 60

2₀(328) → 329

2₀(145) → 146

2₀(106) → 107

2₀(279) → 280

2₀(207) → 208

2₀(301) → 302

2₀(119) → 120

2₀(171) → 172

2₀(297) → 298

2₀(69) → 70

3₁(334) → 335

5₁(337) → 338

221	→	11
221	→	17
221	→	3
205	→	9
29	→	222
338	→	50
152	→	3
5	→	223
5	→	3
37	→	46
130	→	206
130	→	222
1	→	222
8	→	9
13	→	17
13	→	3
332	→	333
101	→	22
101	→	222
91	→	222
21	→	102
21	→	222
72	→	153
72	→	3
141	→	73
141	→	9
178	→	22
178	→	222
121	→	47
121	→	30
277	→	278
277	→	55
277	→	3
54	→	3
82	→	30
313	→	131
313	→	46
45	→	3
16	→	7
16	→	6
114	→	9
63	→	73
63	→	9
295	→	46
240	→	9
259	→	7
259	→	6
166	→	9
192	→	75
192	→	278
192	→	55
192	→	3
1₁(335)	→	336
1₁(336)	→	337
2₁(333)	→	334
1₀(189)	→	190
1₀(51)	→	52
1₀(74)	→	75
1₀(190)	→	191
1₀(180)	→	181
1₀(203)	→	204
1₀(46)	→	153
1₀(11)	→	12
1₀(245)	→	246
1₀(310)	→	311
1₀(127)	→	128
1₀(212)	→	213
1₀(200)	→	201
1₀(162)	→	163
1₀(30)	→	55
1₀(41)	→	42
1₀(252)	→	253
1₀(105)	→	106
1₀(25)	→	26
1₀(33)	→	34
1₀(222)	→	223
1₀(58)	→	59
1₀(273)	→	274
1₀(48)	→	49
1₀(24)	→	25
1₀(50)	→	51
1₀(286)	→	287
1₀(165)	→	152
1₀(159)	→	160
1₀(197)	→	198
1₀(288)	→	289
1₀(293)	→	294
1₀(108)	→	109
1₀(64)	→	65
1₀(248)	→	249
1₀(6)	→	17
1₀(136)	→	137
1₀(236)	→	237
1₀(204)	→	192
1₀(62)	→	54
1₀(15)	→	13
1₀(161)	→	162
1₀(81)	→	72
1₀(107)	→	108
1₀(10)	→	11
1₀(220)	→	205
1₀(4)	→	122
1₀(124)	→	125
1₀(14)	→	15
1₀(43)	→	44
1₀(139)	→	140
1₀(2)	→	3
1₀(298)	→	299
1₀(263)	→	264
1₀(213)	→	214
1₀(257)	→	258
1₀(164)	→	165
1₀(85)	→	86
1₀(17)	→	18
1₀(294)	→	277
1₀(241)	→	278
1₀(308)	→	309
1₀(103)	→	104
1₀(243)	→	244
1₀(264)	→	265
1₀(219)	→	220
4₀(73)	→	74
4₀(111)	→	112
4₀(331)	→	332
4₀(228)	→	229
4₀(2)	→	30
4₀(78)	→	79
4₀(132)	→	133
4₀(188)	→	189
4₀(6)	→	314
4₀(129)	→	121
4₀(211)	→	212
4₀(147)	→	148
4₀(32)	→	33
4₀(234)	→	235
4₀(4)	→	167
4₀(46)	→	47
4₀(112)	→	113
4₀(173)	→	174
4₀(77)	→	78
4₀(283)	→	284
4₀(218)	→	219
4₀(254)	→	255
4₀(242)	→	243
4₀(280)	→	281
4₀(89)	→	90
4₀(214)	→	215
4₀(199)	→	200
4₀(172)	→	173
4₀(324)	→	325
4₀(9)	→	241
4₀(125)	→	126
4₀(251)	→	252
4₀(143)	→	144
4₀(128)	→	129
4₀(195)	→	196
4₀(154)	→	155
4₀(265)	→	266
4₀(116)	→	117
4₀(182)	→	183
4₀(90)	→	82
4₀(131)	→	132
4₀(216)	→	217
4₀(274)	→	275
4₀(282)	→	283
4₀(53)	→	45
4₀(327)	→	328
4₀(96)	→	97
4₀(194)	→	195
4₀(30)	→	31
4₀(246)	→	247
4₀(7)	→	5
4₀(35)	→	36
3₀(226)	→	227
3₀(227)	→	228
3₀(126)	→	127
3₀(23)	→	24
3₀(70)	→	71
3₀(150)	→	151
3₀(315)	→	316
3₀(289)	→	290
3₀(19)	→	20
3₀(86)	→	87
3₀(217)	→	218
3₀(309)	→	310
3₀(99)	→	100
3₀(6)	→	7
3₀(60)	→	61
3₀(231)	→	232
3₀(134)	→	135
3₀(247)	→	248
3₀(79)	→	80
3₀(155)	→	156
3₀(158)	→	159
3₀(314)	→	315
3₀(56)	→	57
3₀(88)	→	89
3₀(46)	→	64
3₀(268)	→	269
3₀(3)	→	4
3₀(47)	→	48
3₀(271)	→	272
3₀(40)	→	41
3₀(284)	→	285
3₀(276)	→	259
3₀(64)	→	142
3₀(113)	→	101
3₀(9)	→	10
3₀(196)	→	197
3₀(146)	→	147
3₀(61)	→	62
3₀(305)	→	306
3₀(83)	→	84
3₀(275)	→	276
3₀(193)	→	194
3₀(27)	→	28
3₀(223)	→	224
3₀(287)	→	288
3₀(325)	→	326
3₀(20)	→	16
3₀(135)	→	136
3₀(31)	→	32
3₀(67)	→	68
3₀(318)	→	319
3₀(296)	→	297
3₀(17)	→	92
3₀(10)	→	14
3₀(93)	→	94
3₀(2)	→	6
3₀(302)	→	303
3₀(198)	→	199
3₀(66)	→	67
3₀(186)	→	187
5₀(170)	→	171
5₀(140)	→	130
5₀(42)	→	43
5₀(238)	→	239
5₀(191)	→	178
5₀(160)	→	161
5₀(142)	→	143
5₀(244)	→	245
5₀(255)	→	256
5₀(46)	→	131
5₀(281)	→	282
5₀(151)	→	141
5₀(177)	→	166
5₀(122)	→	123
5₀(153)	→	154
5₀(98)	→	99
5₀(208)	→	209
5₀(44)	→	37
5₀(169)	→	170
5₀(157)	→	158
5₀(28)	→	21
5₀(7)	→	193
5₀(323)	→	324
5₀(239)	→	221
5₀(118)	→	119
5₀(148)	→	149
5₀(285)	→	286
5₀(167)	→	168
5₀(209)	→	210
5₀(232)	→	233
5₀(9)	→	38
5₀(290)	→	291
5₀(307)	→	308
5₀(321)	→	322
5₀(80)	→	81
5₀(30)	→	179
5₀(102)	→	103
5₀(306)	→	307
5₀(137)	→	138
5₀(34)	→	35
5₀(292)	→	293
5₀(175)	→	176
5₀(185)	→	186
5₀(210)	→	211
5₀(262)	→	263
5₀(109)	→	110
5₀(68)	→	69
5₀(312)	→	295
5₀(233)	→	234
5₀(115)	→	116
5₀(12)	→	8
5₀(75)	→	76
5₀(253)	→	254
5₀(2)	→	46
0₀(267)	→	268
0₀(303)	→	304
0₀(235)	→	236
0₀(179)	→	180
0₀(261)	→	262
0₀(330)	→	331
0₀(87)	→	88
0₀(229)	→	230
0₀(230)	→	231
0₀(55)	→	56
0₀(18)	→	19
0₀(95)	→	96
0₀(94)	→	95
0₀(270)	→	271
0₀(322)	→	323
0₀(120)	→	114
0₀(7)	→	83
0₀(92)	→	93
0₀(258)	→	240
0₀(250)	→	251
0₀(225)	→	226
0₀(46)	→	206
0₀(22)	→	23
0₀(260)	→	261
0₀(181)	→	182
0₀(9)	→	102
0₀(183)	→	184
0₀(133)	→	134
0₀(215)	→	216
0₀(6)	→	22
0₀(84)	→	85
0₀(76)	→	77
0₀(241)	→	242
0₀(144)	→	145
0₀(201)	→	202
0₀(2)	→	222
0₀(163)	→	164
0₀(299)	→	300
0₀(26)	→	27
0₀(36)	→	29
0₀(316)	→	317
0₀(168)	→	169
0₀(149)	→	150
0₀(326)	→	327
0₀(110)	→	111
0₀(272)	→	273
0₀(329)	→	330
0₀(67)	→	115
0₀(104)	→	105
f6₀	→	2
2₀(2)	→	9
2₀(317)	→	318
2₀(237)	→	238
2₀(123)	→	124
2₀(156)	→	157
2₀(117)	→	118
2₀(332)	→	313
2₀(9)	→	73
2₀(224)	→	225
2₀(65)	→	66
2₀(10)	→	260
2₀(300)	→	301
2₀(184)	→	185
2₀(49)	→	50
2₀(202)	→	203
2₀(291)	→	292
2₀(71)	→	63
2₀(4)	→	1
2₀(138)	→	139
2₀(38)	→	39
2₀(206)	→	207
2₀(249)	→	250
2₀(176)	→	177
2₀(100)	→	91
2₀(320)	→	321
2₀(311)	→	312
2₀(256)	→	257
2₀(304)	→	305
2₀(241)	→	296
2₀(269)	→	270
2₀(52)	→	53
2₀(39)	→	40
2₀(319)	→	320
2₀(57)	→	58
2₀(174)	→	175
2₀(97)	→	98
2₀(278)	→	279
2₀(266)	→	267
2₀(187)	→	188
2₀(59)	→	60
2₀(328)	→	329
2₀(145)	→	146
2₀(106)	→	107
2₀(279)	→	280
2₀(207)	→	208
2₀(301)	→	302
2₀(119)	→	120
2₀(171)	→	172
2₀(297)	→	298
2₀(69)	→	70
3₁(334)	→	335
5₁(337)	→	338