YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

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

1.1 Bounds

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

final states:

{271, 256, 240, 226, 211, 196, 183, 168, 153, 137, 124, 112, 97, 80, 67, 52, 36, 19, 1}

transitions:

271 → 259

271 → 3

80 → 171

80 → 81

97 → 5

97 → 37

97 → 20

211 → 23

211 → 169

211 → 81

226 → 6

226 → 38

226 → 21

226 → 3

1 → 241

1 → 81

183 → 4

183 → 3

36 → 3

153 → 39

153 → 197

153 → 81

52 → 23

52 → 169

52 → 81

124 → 85

124 → 53

124 → 4

124 → 3

67 → 198

67 → 241

67 → 81

112 → 4

112 → 3

137 → 154

137 → 81

240 → 128

240 → 38

240 → 21

240 → 3

256 → 83

256 → 21

256 → 3

168 → 39

168 → 197

168 → 81

19 → 53

19 → 4

19 → 3

196 → 241

196 → 81

f3₀ → 2

0₀(59) → 60

0₀(82) → 83

0₀(115) → 116

0₀(230) → 231

0₀(208) → 209

0₀(20) → 21

0₀(56) → 57

0₀(51) → 36

0₀(236) → 237

0₀(37) → 38

0₀(175) → 176

0₀(245) → 246

0₀(29) → 30

0₀(5) → 6

0₀(127) → 128

0₀(63) → 64

0₀(45) → 46

0₀(145) → 146

0₀(148) → 149

0₀(166) → 167

0₀(64) → 65

0₀(98) → 99

0₀(229) → 230

0₀(43) → 44

0₀(250) → 251

0₀(138) → 139

0₀(147) → 148

0₀(280) → 281

0₀(154) → 227

0₀(107) → 108

0₀(8) → 9

0₀(194) → 195

0₀(191) → 192

0₀(258) → 259

0₀(232) → 233

0₀(195) → 183

0₀(69) → 70

0₀(71) → 72

0₀(235) → 236

0₀(123) → 112

0₀(133) → 134

0₀(2) → 3

0₀(32) → 33

0₀(12) → 13

0₀(269) → 270

0₀(15) → 16

0₀(164) → 165

0₀(21) → 22

0₀(47) → 48

0₀(90) → 91

0₀(261) → 262

0₀(253) → 254

0₀(18) → 1

0₀(84) → 85

0₀(223) → 224

0₀(282) → 283

0₀(54) → 55

0₀(259) → 260

0₀(83) → 84

0₀(110) → 111

0₀(132) → 133

0₀(31) → 32

0₀(172) → 173

0₀(173) → 174

0₀(162) → 163

0₀(65) → 66

0₀(249) → 250

0₀(99) → 100

0₀(244) → 245

0₀(218) → 219

0₀(205) → 206

0₀(262) → 263

0₀(120) → 121

0₀(203) → 204

0₀(155) → 156

0₀(39) → 40

0₀(206) → 207

0₀(4) → 53

0₀(270) → 256

0₀(49) → 50

0₀(72) → 73

0₀(247) → 248

0₀(277) → 278

0₀(66) → 52

0₀(73) → 74

0₀(100) → 101

0₀(95) → 96

0₀(11) → 12

0₀(171) → 172

0₀(40) → 41

0₀(220) → 221

0₀(214) → 215

0₀(108) → 109

0₀(237) → 238

0₀(44) → 45

0₀(239) → 226

0₀(141) → 142

0₀(46) → 47

0₀(50) → 51

0₀(3) → 4

0₀(88) → 89

0₀(121) → 122

0₀(68) → 69

0₀(157) → 158

0₀(255) → 240

0₀(210) → 196

0₀(13) → 14

0₀(113) → 114

0₀(125) → 126

0₀(92) → 93

0₀(140) → 184

0₀(178) → 179

0₀(268) → 269

0₀(185) → 186

0₀(274) → 275

0₀(199) → 200

0₀(169) → 170

0₀(179) → 180

0₀(265) → 266

0₀(35) → 19

0₀(105) → 106

0₀(176) → 177

0₀(224) → 225

0₀(75) → 76

0₀(246) → 247

0₀(150) → 151

0₀(216) → 217

0₀(283) → 271

0₀(273) → 274

0₀(227) → 228

0₀(118) → 119

0₀(233) → 234

0₀(142) → 143

0₀(53) → 54

2₀(96) → 80

2₀(177) → 178

2₀(128) → 129

2₀(152) → 137

2₀(9) → 10

2₀(61) → 62

2₀(28) → 29

2₀(22) → 23

2₀(78) → 79

2₀(79) → 67

2₀(122) → 123

2₀(93) → 94

2₀(193) → 194

2₀(70) → 71

2₀(23) → 24

2₀(24) → 25

2₀(101) → 102

2₀(252) → 253

2₀(180) → 181

2₀(201) → 202

2₀(234) → 235

2₀(225) → 211

2₀(76) → 77

2₀(266) → 267

2₀(167) → 153

2₀(221) → 222

2₀(276) → 277

2₀(174) → 175

2₀(143) → 144

2₀(275) → 276

2₀(209) → 210

2₀(58) → 59

2₀(181) → 182

2₀(57) → 58

2₀(187) → 188

2₀(38) → 39

2₀(263) → 264

2₀(81) → 241

2₀(165) → 166

2₀(2) → 81

2₀(85) → 86

2₀(257) → 258

2₀(55) → 56

2₀(228) → 229

2₀(158) → 159

2₀(138) → 154

2₀(4) → 169

2₀(149) → 150

2₀(106) → 107

2₀(215) → 216

2₀(25) → 26

2₀(186) → 187

2₀(192) → 193

2₀(139) → 140

2₀(74) → 75

2₀(197) → 198

2₀(207) → 208

2₀(136) → 124

2₀(109) → 110

2₀(33) → 34

2₀(182) → 168

2₀(60) → 61

2₀(62) → 63

2₀(77) → 78

2₀(251) → 252

2₀(260) → 261

2₀(134) → 135

2₀(30) → 31

2₀(170) → 171

2₀(135) → 136

2₀(21) → 197

2₀(41) → 42

2₀(129) → 130

2₀(89) → 90

1₀(144) → 145

1₀(243) → 244

1₀(82) → 212

1₀(219) → 220

1₀(248) → 249

1₀(267) → 268

1₀(103) → 104

1₀(94) → 95

1₀(146) → 147

1₀(104) → 105

1₀(189) → 190

1₀(26) → 27

1₀(160) → 161

1₀(163) → 164

1₀(10) → 11

1₀(99) → 272

1₀(130) → 131

1₀(48) → 49

1₀(6) → 7

1₀(188) → 189

1₀(202) → 203

1₀(198) → 199

1₀(17) → 18

1₀(241) → 242

1₀(154) → 155

1₀(212) → 213

1₀(131) → 132

1₀(254) → 255

1₀(204) → 205

1₀(161) → 162

1₀(117) → 118

1₀(281) → 282

1₀(20) → 138

1₀(126) → 127

1₀(86) → 87

1₀(14) → 15

1₀(81) → 82

1₀(55) → 113

1₀(87) → 88

1₀(217) → 218

1₀(213) → 214

1₀(190) → 191

1₀(91) → 92

1₀(84) → 125

1₀(42) → 43

1₀(272) → 273

1₀(2) → 20

1₀(21) → 257

1₀(184) → 185

1₀(116) → 117

1₀(37) → 98

1₀(111) → 97

1₀(278) → 279

1₀(151) → 152

1₀(200) → 201

1₀(114) → 115

1₀(231) → 232

1₀(27) → 28

1₀(156) → 157

1₀(102) → 103

1₀(159) → 160

1₀(238) → 239

1₀(3) → 37

1₀(242) → 243

1₀(264) → 265

1₀(140) → 141

1₀(16) → 17

1₀(119) → 120

1₀(23) → 68

1₀(222) → 223

1₀(4) → 5

1₀(34) → 35

1₀(7) → 8

1₀(279) → 280

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