YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 Bounds

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

final states:

{34, 21, 1}

transitions:

33 → 47

260 → 246

59 → 101

34 → 8

107 → 115

1 → 8

165 → 189

21 → 8

251 → 259

172 → 27

171 → 191

116 → 102

264 → 48

258 → 40

66 → 14

114 → 14

113 → 139

46 → 263

158 → 27

190 → 160

203 → 245

210 → 40

151 → 159

2₁(156) → 157

2₁(56) → 57

2₁(200) → 201

2₁(104) → 105

2₁(208) → 209

2₁(170) → 171

2₁(248) → 249

2₁(64) → 65

2₁(112) → 113

2₁(50) → 51

2₁(194) → 195

2₁(142) → 143

2₁(256) → 257

2₁(162) → 163

2₁(148) → 149

5₁(253) → 254

5₁(259) → 260

5₁(47) → 48

5₁(145) → 146

5₁(245) → 246

5₁(101) → 102

5₁(159) → 160

5₁(189) → 190

5₁(205) → 206

5₁(109) → 110

5₁(167) → 168

5₁(115) → 116

5₁(139) → 140

5₁(53) → 54

5₁(153) → 154

5₁(61) → 62

5₁(263) → 264

5₁(197) → 198

5₁(191) → 192

0₁(52) → 53

0₁(150) → 151

0₁(106) → 107

0₁(157) → 158

0₁(164) → 165

0₁(65) → 66

0₁(58) → 59

0₁(196) → 197

0₁(144) → 145

0₁(209) → 210

0₁(202) → 203

0₁(250) → 251

4₁(192) → 193

4₁(54) → 55

4₁(140) → 141

4₁(48) → 49

4₁(160) → 161

4₁(102) → 103

4₁(154) → 155

4₁(246) → 247

4₁(62) → 63

4₁(168) → 169

4₁(198) → 199

4₁(254) → 255

4₁(146) → 147

4₁(110) → 111

4₁(206) → 207

3₀(31) → 32

3₀(44) → 45

3₀(18) → 19

3₀(10) → 11

3₀(4) → 5

3₀(36) → 37

3₀(23) → 24

4₀(9) → 10

4₀(17) → 18

4₀(3) → 4

4₀(43) → 44

4₀(30) → 31

4₀(22) → 23

4₀(35) → 36

2₀(37) → 38

2₀(19) → 20

2₀(45) → 46

2₀(11) → 12

2₀(32) → 33

2₀(5) → 6

2₀(24) → 25

5₀(29) → 30

5₀(42) → 43

5₀(8) → 9

5₀(27) → 35

5₀(14) → 22

5₀(16) → 17

5₀(2) → 3

1₀(12) → 13

1₀(40) → 41

1₀(46) → 34

1₀(6) → 7

1₀(38) → 39

1₀(14) → 15

1₀(41) → 42

1₀(27) → 28

1₀(28) → 29

1₀(33) → 21

1₀(15) → 16

1₀(25) → 26

f6₀ → 2

0₀(26) → 27

0₀(7) → 8

0₀(20) → 1

0₀(39) → 40

0₀(13) → 14

3₁(199) → 200

3₁(55) → 56

3₁(247) → 248

3₁(161) → 162

3₁(63) → 64

3₁(169) → 170

3₁(207) → 208

3₁(49) → 50

3₁(193) → 194

3₁(147) → 148

3₁(103) → 104

3₁(155) → 156

3₁(255) → 256

3₁(141) → 142

3₁(111) → 112

1₁(165) → 166

1₁(249) → 250

1₁(204) → 205

1₁(105) → 106

1₁(163) → 164

1₁(203) → 204

1₁(252) → 253

1₁(60) → 61

1₁(57) → 58

1₁(107) → 108

1₁(51) → 52

1₁(201) → 202

1₁(152) → 153

1₁(149) → 150

1₁(151) → 152

1₁(171) → 172

1₁(166) → 167

1₁(257) → 258

1₁(143) → 144

1₁(113) → 114

1₁(195) → 196

1₁(59) → 60

1₁(251) → 252

1₁(108) → 109

33	→	47
260	→	246
59	→	101
34	→	8
107	→	115
1	→	8
165	→	189
21	→	8
251	→	259
172	→	27
171	→	191
116	→	102
264	→	48
258	→	40
66	→	14
114	→	14
113	→	139
46	→	263
158	→	27
190	→	160
203	→	245
210	→	40
151	→	159
2₁(156)	→	157
2₁(56)	→	57
2₁(200)	→	201
2₁(104)	→	105
2₁(208)	→	209
2₁(170)	→	171
2₁(248)	→	249
2₁(64)	→	65
2₁(112)	→	113
2₁(50)	→	51
2₁(194)	→	195
2₁(142)	→	143
2₁(256)	→	257
2₁(162)	→	163
2₁(148)	→	149
5₁(253)	→	254
5₁(259)	→	260
5₁(47)	→	48
5₁(145)	→	146
5₁(245)	→	246
5₁(101)	→	102
5₁(159)	→	160
5₁(189)	→	190
5₁(205)	→	206
5₁(109)	→	110
5₁(167)	→	168
5₁(115)	→	116
5₁(139)	→	140
5₁(53)	→	54
5₁(153)	→	154
5₁(61)	→	62
5₁(263)	→	264
5₁(197)	→	198
5₁(191)	→	192
0₁(52)	→	53
0₁(150)	→	151
0₁(106)	→	107
0₁(157)	→	158
0₁(164)	→	165
0₁(65)	→	66
0₁(58)	→	59
0₁(196)	→	197
0₁(144)	→	145
0₁(209)	→	210
0₁(202)	→	203
0₁(250)	→	251
4₁(192)	→	193
4₁(54)	→	55
4₁(140)	→	141
4₁(48)	→	49
4₁(160)	→	161
4₁(102)	→	103
4₁(154)	→	155
4₁(246)	→	247
4₁(62)	→	63
4₁(168)	→	169
4₁(198)	→	199
4₁(254)	→	255
4₁(146)	→	147
4₁(110)	→	111
4₁(206)	→	207
3₀(31)	→	32
3₀(44)	→	45
3₀(18)	→	19
3₀(10)	→	11
3₀(4)	→	5
3₀(36)	→	37
3₀(23)	→	24
4₀(9)	→	10
4₀(17)	→	18
4₀(3)	→	4
4₀(43)	→	44
4₀(30)	→	31
4₀(22)	→	23
4₀(35)	→	36
2₀(37)	→	38
2₀(19)	→	20
2₀(45)	→	46
2₀(11)	→	12
2₀(32)	→	33
2₀(5)	→	6
2₀(24)	→	25
5₀(29)	→	30
5₀(42)	→	43
5₀(8)	→	9
5₀(27)	→	35
5₀(14)	→	22
5₀(16)	→	17
5₀(2)	→	3
1₀(12)	→	13
1₀(40)	→	41
1₀(46)	→	34
1₀(6)	→	7
1₀(38)	→	39
1₀(14)	→	15
1₀(41)	→	42
1₀(27)	→	28
1₀(28)	→	29
1₀(33)	→	21
1₀(15)	→	16
1₀(25)	→	26
f6₀	→	2
0₀(26)	→	27
0₀(7)	→	8
0₀(20)	→	1
0₀(39)	→	40
0₀(13)	→	14
3₁(199)	→	200
3₁(55)	→	56
3₁(247)	→	248
3₁(161)	→	162
3₁(63)	→	64
3₁(169)	→	170
3₁(207)	→	208
3₁(49)	→	50
3₁(193)	→	194
3₁(147)	→	148
3₁(103)	→	104
3₁(155)	→	156
3₁(255)	→	256
3₁(141)	→	142
3₁(111)	→	112
1₁(165)	→	166
1₁(249)	→	250
1₁(204)	→	205
1₁(105)	→	106
1₁(163)	→	164
1₁(203)	→	204
1₁(252)	→	253
1₁(60)	→	61
1₁(57)	→	58
1₁(107)	→	108
1₁(51)	→	52
1₁(201)	→	202
1₁(152)	→	153
1₁(149)	→	150
1₁(151)	→	152
1₁(171)	→	172
1₁(166)	→	167
1₁(257)	→	258
1₁(143)	→	144
1₁(113)	→	114
1₁(195)	→	196
1₁(59)	→	60
1₁(251)	→	252
1₁(108)	→	109