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)))))))))))))))))))))))))))))))

Proof

1 Bounds

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

final states:

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

transitions:

78 → 83

33 → 5

25 → 273

32 → 277

81 → 98

214 → 206

286 → 73

274 → 73

294 → 73

84 → 76

136 → 128

211 → 228

133 → 150

260 → 265

18 → 269

39 → 281

108 → 15

134 → 22

110 → 102

185 → 202

130 → 135

107 → 124

1 → 5

40 → 5

60 → 293

26 → 5

208 → 213

186 → 36

54 → 5

237 → 254

270 → 73

264 → 57

82 → 8

53 → 289

11 → 72

212 → 43

188 → 180

12 → 5

104 → 109

282 → 73

234 → 239

290 → 73

182 → 187

46 → 285

162 → 154

278 → 73

240 → 232

47 → 5

160 → 29

159 → 176

19 → 5

266 → 258

156 → 161

238 → 50

0₁(74) → 75

0₁(129) → 130

0₁(207) → 208

0₁(77) → 78

0₁(256) → 257

0₁(155) → 156

0₁(204) → 205

0₁(230) → 231

0₁(126) → 127

0₁(233) → 234

0₁(181) → 182

0₁(259) → 260

0₁(178) → 179

0₁(100) → 101

0₁(152) → 153

0₁(103) → 104

2₁(98) → 99

2₁(106) → 107

2₁(124) → 125

2₁(150) → 151

2₁(239) → 240

2₁(289) → 290

2₁(293) → 294

2₁(281) → 282

2₁(205) → 206

2₁(179) → 180

2₁(132) → 133

2₁(210) → 211

2₁(262) → 263

2₁(265) → 266

2₁(277) → 278

2₁(231) → 232

2₁(257) → 258

2₁(213) → 214

2₁(187) → 188

2₁(158) → 159

2₁(176) → 177

2₁(202) → 203

2₁(228) → 229

2₁(109) → 110

2₁(75) → 76

2₁(285) → 286

2₁(184) → 185

2₁(236) → 237

2₁(101) → 102

2₁(161) → 162

2₁(80) → 81

2₁(72) → 73

2₁(83) → 84

2₁(127) → 128

2₁(273) → 274

2₁(135) → 136

2₁(269) → 270

2₁(153) → 154

2₁(254) → 255

f3₀ → 2

1₀(20) → 21

1₀(51) → 52

1₀(37) → 38

1₀(29) → 30

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₀(55) → 56

1₀(60) → 54

1₀(39) → 33

1₀(36) → 37

1₀(30) → 31

1₀(11) → 1

1₀(44) → 45

1₀(46) → 40

1₀(50) → 51

1₀(3) → 4

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₀(49) → 50

0₀(4) → 5

0₀(42) → 43

0₀(56) → 57

0₀(35) → 36

0₀(21) → 22

1₁(157) → 158

1₁(237) → 238

1₁(177) → 178

1₁(156) → 157

1₁(263) → 264

1₁(128) → 129

1₁(133) → 134

1₁(258) → 259

1₁(105) → 106

1₁(260) → 261

1₁(99) → 100

1₁(79) → 80

1₁(232) → 233

1₁(255) → 256

1₁(235) → 236

1₁(131) → 132

1₁(107) → 108

1₁(159) → 160

1₁(234) → 235

1₁(104) → 105

1₁(151) → 152

1₁(76) → 77

1₁(206) → 207

1₁(211) → 212

1₁(203) → 204

1₁(125) → 126

1₁(81) → 82

1₁(208) → 209

1₁(130) → 131

1₁(180) → 181

1₁(183) → 184

1₁(73) → 74

1₁(154) → 155

1₁(229) → 230

1₁(209) → 210

1₁(78) → 79

1₁(261) → 262

1₁(185) → 186

1₁(182) → 183

1₁(102) → 103

2₀(22) → 27

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₀(52) → 53

2₀(36) → 41

2₀(43) → 48

2₀(50) → 55

78	→	83
33	→	5
25	→	273
32	→	277
81	→	98
214	→	206
286	→	73
274	→	73
294	→	73
84	→	76
136	→	128
211	→	228
133	→	150
260	→	265
18	→	269
39	→	281
108	→	15
134	→	22
110	→	102
185	→	202
130	→	135
107	→	124
1	→	5
40	→	5
60	→	293
26	→	5
208	→	213
186	→	36
54	→	5
237	→	254
270	→	73
264	→	57
82	→	8
53	→	289
11	→	72
212	→	43
188	→	180
12	→	5
104	→	109
282	→	73
234	→	239
290	→	73
182	→	187
46	→	285
162	→	154
278	→	73
240	→	232
47	→	5
160	→	29
159	→	176
19	→	5
266	→	258
156	→	161
238	→	50
0₁(74)	→	75
0₁(129)	→	130
0₁(207)	→	208
0₁(77)	→	78
0₁(256)	→	257
0₁(155)	→	156
0₁(204)	→	205
0₁(230)	→	231
0₁(126)	→	127
0₁(233)	→	234
0₁(181)	→	182
0₁(259)	→	260
0₁(178)	→	179
0₁(100)	→	101
0₁(152)	→	153
0₁(103)	→	104
2₁(98)	→	99
2₁(106)	→	107
2₁(124)	→	125
2₁(150)	→	151
2₁(239)	→	240
2₁(289)	→	290
2₁(293)	→	294
2₁(281)	→	282
2₁(205)	→	206
2₁(179)	→	180
2₁(132)	→	133
2₁(210)	→	211
2₁(262)	→	263
2₁(265)	→	266
2₁(277)	→	278
2₁(231)	→	232
2₁(257)	→	258
2₁(213)	→	214
2₁(187)	→	188
2₁(158)	→	159
2₁(176)	→	177
2₁(202)	→	203
2₁(228)	→	229
2₁(109)	→	110
2₁(75)	→	76
2₁(285)	→	286
2₁(184)	→	185
2₁(236)	→	237
2₁(101)	→	102
2₁(161)	→	162
2₁(80)	→	81
2₁(72)	→	73
2₁(83)	→	84
2₁(127)	→	128
2₁(273)	→	274
2₁(135)	→	136
2₁(269)	→	270
2₁(153)	→	154
2₁(254)	→	255
f3₀	→	2
1₀(20)	→	21
1₀(51)	→	52
1₀(37)	→	38
1₀(29)	→	30
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₀(55)	→	56
1₀(60)	→	54
1₀(39)	→	33
1₀(36)	→	37
1₀(30)	→	31
1₀(11)	→	1
1₀(44)	→	45
1₀(46)	→	40
1₀(50)	→	51
1₀(3)	→	4
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₀(49)	→	50
0₀(4)	→	5
0₀(42)	→	43
0₀(56)	→	57
0₀(35)	→	36
0₀(21)	→	22
1₁(157)	→	158
1₁(237)	→	238
1₁(177)	→	178
1₁(156)	→	157
1₁(263)	→	264
1₁(128)	→	129
1₁(133)	→	134
1₁(258)	→	259
1₁(105)	→	106
1₁(260)	→	261
1₁(99)	→	100
1₁(79)	→	80
1₁(232)	→	233
1₁(255)	→	256
1₁(235)	→	236
1₁(131)	→	132
1₁(107)	→	108
1₁(159)	→	160
1₁(234)	→	235
1₁(104)	→	105
1₁(151)	→	152
1₁(76)	→	77
1₁(206)	→	207
1₁(211)	→	212
1₁(203)	→	204
1₁(125)	→	126
1₁(81)	→	82
1₁(208)	→	209
1₁(130)	→	131
1₁(180)	→	181
1₁(183)	→	184
1₁(73)	→	74
1₁(154)	→	155
1₁(229)	→	230
1₁(209)	→	210
1₁(78)	→	79
1₁(261)	→	262
1₁(185)	→	186
1₁(182)	→	183
1₁(102)	→	103
2₀(22)	→	27
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₀(52)	→	53
2₀(36)	→	41
2₀(43)	→	48
2₀(50)	→	55