YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 String Reversal

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

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

1.1 Bounds

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

final states:

{276, 268, 260, 252, 244, 235, 226, 220, 212, 203, 194, 186, 177, 170, 161, 153, 144, 135, 127, 119, 111, 102, 92, 83, 73, 64, 54, 45, 37, 32, 22, 12, 1}

transitions:

111 → 93

102 → 55

32 → 3

119 → 93

276 → 13

260 → 93

226 → 46

226 → 3

37 → 145

37 → 93

1 → 93

127 → 23

135 → 145

135 → 93

73 → 227

73 → 23

235 → 13

170 → 24

170 → 55

161 → 46

161 → 3

268 → 55

177 → 55

186 → 93

153 → 178

153 → 13

220 → 93

54 → 13

22 → 55

244 → 93

212 → 23

252 → 3

45 → 93

12 → 3

64 → 227

64 → 23

83 → 23

203 → 24

203 → 55

92 → 94

92 → 74

144 → 112

144 → 3

194 → 23

f6₀ → 2

4₀(274) → 275

4₀(59) → 60

4₀(123) → 124

4₀(180) → 221

4₀(65) → 66

4₀(233) → 234

4₀(197) → 198

4₀(155) → 156

4₀(198) → 199

4₀(227) → 245

4₀(24) → 25

4₀(205) → 206

4₀(139) → 140

4₀(270) → 271

4₀(7) → 33

4₀(61) → 62

4₀(243) → 235

4₀(277) → 278

4₀(237) → 238

4₀(215) → 216

4₀(71) → 72

4₀(38) → 39

4₀(182) → 183

4₀(80) → 81

4₀(74) → 236

4₀(201) → 202

4₀(151) → 152

4₀(89) → 90

4₀(174) → 175

4₀(2) → 13

4₀(107) → 108

4₀(231) → 232

4₀(116) → 117

4₀(210) → 211

4₀(149) → 150

4₀(164) → 165

4₀(56) → 57

4₀(13) → 178

4₀(204) → 205

4₀(195) → 196

4₀(57) → 58

4₀(104) → 105

4₀(160) → 153

4₀(112) → 113

5₀(98) → 99

5₀(65) → 213

5₀(126) → 119

5₀(23) → 145

5₀(225) → 220

5₀(26) → 27

5₀(76) → 77

5₀(251) → 244

5₀(230) → 231

5₀(19) → 20

5₀(7) → 8

5₀(51) → 52

5₀(267) → 260

5₀(143) → 135

5₀(79) → 80

5₀(187) → 188

5₀(55) → 103

5₀(222) → 223

5₀(87) → 88

5₀(238) → 239

5₀(266) → 267

5₀(249) → 250

5₀(69) → 70

5₀(264) → 265

5₀(255) → 256

5₀(9) → 10

5₀(163) → 164

5₀(128) → 129

5₀(224) → 225

5₀(189) → 190

5₀(193) → 186

5₀(273) → 274

5₀(21) → 12

5₀(53) → 45

5₀(117) → 118

5₀(246) → 247

5₀(2) → 93

5₀(24) → 253

5₀(44) → 37

5₀(138) → 139

5₀(66) → 67

3₀(279) → 280

3₀(254) → 255

3₀(239) → 240

3₀(16) → 17

3₀(130) → 131

3₀(35) → 36

3₀(67) → 68

3₀(169) → 161

3₀(209) → 210

3₀(146) → 147

3₀(157) → 158

3₀(3) → 46

3₀(271) → 272

3₀(129) → 130

3₀(121) → 277

3₀(50) → 51

3₀(8) → 9

3₀(52) → 53

3₀(228) → 229

3₀(140) → 141

3₀(56) → 112

3₀(113) → 114

3₀(208) → 209

3₀(60) → 61

3₀(84) → 85

3₀(247) → 248

3₀(39) → 40

3₀(13) → 84

3₀(90) → 91

3₀(261) → 262

3₀(4) → 5

3₀(124) → 125

3₀(14) → 15

3₀(265) → 266

3₀(40) → 41

3₀(122) → 123

3₀(2) → 3

3₀(178) → 179

3₀(192) → 193

3₀(216) → 217

3₀(103) → 104

3₀(38) → 171

1₀(2) → 55

1₀(78) → 79

1₀(25) → 26

1₀(31) → 22

1₀(95) → 96

1₀(74) → 75

1₀(6) → 7

1₀(275) → 268

1₀(179) → 180

1₀(58) → 59

1₀(227) → 228

1₀(211) → 203

1₀(110) → 102

1₀(4) → 38

1₀(136) → 261

1₀(77) → 78

1₀(85) → 86

1₀(150) → 151

1₀(70) → 71

1₀(185) → 177

1₀(223) → 224

1₀(191) → 192

1₀(176) → 170

1₀(55) → 56

1₀(141) → 142

1₀(105) → 106

1₀(93) → 204

1₀(181) → 182

1₀(68) → 69

1₀(18) → 19

1₀(27) → 28

1₀(23) → 24

1₀(217) → 218

1₀(148) → 149

1₀(17) → 18

1₀(250) → 251

1₀(257) → 258

1₀(236) → 237

1₀(184) → 185

1₀(241) → 242

1₀(180) → 181

1₀(142) → 143

1₀(166) → 167

1₀(33) → 34

1₀(43) → 44

1₀(248) → 249

1₀(171) → 172

1₀(278) → 279

2₀(2) → 74

2₀(46) → 47

2₀(28) → 29

2₀(196) → 197

2₀(263) → 264

2₀(65) → 128

2₀(133) → 134

2₀(258) → 259

2₀(10) → 11

2₀(48) → 49

2₀(99) → 100

2₀(232) → 233

2₀(36) → 32

2₀(152) → 144

2₀(55) → 136

2₀(24) → 269

2₀(131) → 132

2₀(159) → 160

2₀(63) → 54

2₀(234) → 226

2₀(96) → 97

2₀(272) → 273

2₀(206) → 207

2₀(3) → 4

2₀(214) → 215

2₀(11) → 1

2₀(84) → 187

2₀(86) → 87

2₀(147) → 148

2₀(14) → 154

2₀(245) → 246

2₀(100) → 101

2₀(118) → 111

2₀(62) → 63

2₀(23) → 65

2₀(94) → 95

2₀(132) → 133

2₀(125) → 126

2₀(121) → 122

2₀(262) → 263

2₀(81) → 82

2₀(29) → 30

2₀(137) → 138

2₀(15) → 16

2₀(165) → 166

2₀(259) → 252

2₀(93) → 94

2₀(101) → 92

2₀(240) → 241

2₀(75) → 76

2₀(120) → 121

2₀(108) → 109

2₀(41) → 42

2₀(253) → 254

2₀(188) → 189

2₀(190) → 191

2₀(5) → 6

2₀(199) → 200

2₀(13) → 162

2₀(200) → 201

2₀(158) → 159

2₀(115) → 116

2₀(47) → 48

0₀(42) → 43

0₀(106) → 107

0₀(218) → 219

0₀(97) → 98

0₀(82) → 73

0₀(281) → 276

0₀(172) → 173

0₀(88) → 89

0₀(136) → 137

0₀(269) → 270

0₀(242) → 243

0₀(202) → 194

0₀(13) → 14

0₀(207) → 208

0₀(162) → 163

0₀(93) → 195

0₀(280) → 281

0₀(20) → 21

0₀(167) → 168

0₀(156) → 157

0₀(49) → 50

0₀(72) → 64

0₀(154) → 155

0₀(103) → 120

0₀(145) → 146

0₀(256) → 257

0₀(30) → 31

0₀(34) → 35

0₀(229) → 230

0₀(219) → 212

0₀(173) → 174

0₀(175) → 176

0₀(183) → 184

0₀(114) → 115

0₀(134) → 127

0₀(109) → 110

0₀(91) → 83

0₀(55) → 227

0₀(2) → 23

0₀(221) → 222

0₀(168) → 169

0₀(213) → 214

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