YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 String Reversal

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

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

1.1 Bounds

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

final states:

{193, 187, 184, 180, 179, 174, 170, 166, 164, 161, 156, 151, 149, 145, 143, 140, 135, 131, 128, 125, 123, 120, 116, 111, 107, 102, 98, 97, 92, 87, 83, 79, 75, 71, 65, 61, 57, 56, 51, 48, 44, 39, 34, 29, 25, 22, 20, 14, 8, 1}

transitions:

239 → 257

111 → 188

25 → 188

61 → 188

102 → 188

29 → 188

315 → 288

128 → 15

87 → 188

98 → 188

51 → 188

97 → 188

289 → 35

129 → 205

129 → 212

129 → 232

167 → 262

149 → 66

211 → 16

145 → 188

39 → 188

120 → 36

120 → 26

120 → 15

184 → 117

184 → 188

57 → 188

218 → 16

187 → 188

34 → 188

65 → 188

20 → 188

193 → 66

107 → 188

1 → 35

1 → 9

123 → 188

8 → 35

8 → 9

71 → 194

71 → 9

44 → 188

135 → 188

179 → 194

179 → 9

261 → 243

125 → 15

296 → 35

79 → 188

170 → 188

161 → 188

268 → 35

116 → 188

22 → 188

75 → 194

75 → 9

237 → 210

174 → 188

143 → 188

180 → 4

180 → 9

244 → 35

14 → 35

14 → 9

140 → 188

182 → 283

182 → 290

182 → 310

83 → 188

48 → 188

164 → 188

168 → 238

320 → 36

285 → 316

131 → 194

131 → 9

92 → 188

166 → 16

166 → 9

56 → 188

151 → 194

151 → 9

156 → 188

3₁(260) → 261

3₁(215) → 216

3₁(293) → 294

3₁(234) → 235

3₁(291) → 292

3₁(208) → 209

3₁(286) → 287

3₁(316) → 317

3₁(236) → 237

3₁(312) → 313

3₁(213) → 214

3₁(241) → 242

3₁(257) → 258

3₁(314) → 315

3₁(264) → 265

2₁(258) → 259

2₁(239) → 240

2₁(240) → 241

2₁(319) → 320

2₁(207) → 208

2₁(285) → 286

2₁(267) → 268

4₁(287) → 288

4₁(209) → 210

4₁(216) → 217

4₁(243) → 244

4₁(294) → 295

5₁(232) → 233

5₁(259) → 260

5₁(242) → 243

5₁(310) → 311

5₁(265) → 266

5₁(317) → 318

3₀(31) → 32

3₀(16) → 17

3₀(115) → 111

3₀(67) → 68

3₀(53) → 129

3₀(11) → 12

3₀(127) → 165

3₀(146) → 147

3₀(157) → 158

3₀(112) → 113

3₀(3) → 88

3₀(195) → 196

3₀(66) → 67

3₀(77) → 78

3₀(150) → 149

3₀(26) → 27

3₀(133) → 134

3₀(18) → 19

3₀(64) → 61

3₀(113) → 162

3₀(9) → 10

3₀(99) → 100

3₀(6) → 124

3₀(94) → 95

3₀(84) → 85

3₀(136) → 137

3₀(109) → 110

3₀(62) → 63

3₀(72) → 73

3₀(15) → 58

3₀(101) → 98

3₀(42) → 43

3₀(81) → 82

3₀(10) → 45

3₀(5) → 6

3₀(4) → 21

3₀(117) → 118

3₀(36) → 37

3₀(40) → 41

3₀(2) → 30

3₀(152) → 153

3₀(103) → 104

2₀(2) → 66

2₀(132) → 133

2₀(31) → 108

2₀(155) → 151

2₀(26) → 62

2₀(42) → 150

2₀(192) → 187

2₀(4) → 5

2₀(144) → 143

2₀(80) → 81

2₀(119) → 116

2₀(91) → 87

2₀(60) → 57

2₀(141) → 142

2₀(9) → 40

2₀(93) → 146

2₀(23) → 24

2₀(169) → 166

2₀(197) → 193

2₀(66) → 93

2₀(15) → 112

2₀(86) → 83

2₀(3) → 175

2₀(10) → 76

2₀(30) → 157

2₀(122) → 120

2₀(40) → 72

4₀(124) → 123

4₀(177) → 178

4₀(41) → 42

4₀(78) → 75

4₀(63) → 64

4₀(30) → 52

4₀(147) → 148

4₀(160) → 156

4₀(37) → 38

4₀(85) → 86

4₀(58) → 59

4₀(45) → 46

4₀(32) → 33

4₀(95) → 96

4₀(6) → 7

4₀(134) → 131

4₀(110) → 107

4₀(176) → 177

4₀(88) → 89

4₀(46) → 47

4₀(82) → 79

4₀(3) → 117

4₀(104) → 105

4₀(113) → 114

4₀(163) → 161

4₀(196) → 197

4₀(96) → 92

4₀(12) → 13

4₀(27) → 28

4₀(21) → 20

4₀(74) → 71

4₀(67) → 99

4₀(17) → 185

4₀(10) → 23

4₀(2) → 188

4₀(68) → 69

4₀(138) → 139

4₀(171) → 172

4₀(89) → 90

4₀(186) → 184

0₀(17) → 18

0₀(47) → 44

0₀(129) → 130

0₀(54) → 55

0₀(28) → 25

0₀(56) → 179

0₀(43) → 39

0₀(13) → 8

0₀(118) → 119

0₀(9) → 152

0₀(49) → 50

0₀(182) → 183

0₀(52) → 126

0₀(189) → 190

0₀(3) → 136

0₀(175) → 176

0₀(185) → 186

0₀(114) → 115

0₀(24) → 22

0₀(38) → 34

0₀(33) → 29

0₀(188) → 189

0₀(105) → 106

0₀(2) → 3

5₀(90) → 91

5₀(70) → 97

5₀(93) → 94

5₀(137) → 138

5₀(53) → 54

5₀(21) → 121

5₀(73) → 74

5₀(190) → 191

5₀(9) → 26

5₀(23) → 49

5₀(191) → 192

5₀(194) → 195

5₀(50) → 48

5₀(69) → 70

5₀(126) → 127

5₀(66) → 103

5₀(76) → 77

5₀(2) → 15

5₀(3) → 80

5₀(30) → 167

5₀(168) → 169

5₀(35) → 36

5₀(52) → 53

5₀(108) → 109

5₀(136) → 171

5₀(106) → 102

5₀(15) → 84

5₀(158) → 159

5₀(67) → 181

5₀(100) → 101

5₀(153) → 154

f6₀ → 2

1₀(2) → 9

1₀(167) → 168

1₀(117) → 132

1₀(9) → 35

1₀(10) → 11

1₀(19) → 14

1₀(30) → 31

1₀(55) → 51

1₀(159) → 160

1₀(178) → 174

1₀(181) → 182

1₀(3) → 4

1₀(66) → 194

1₀(70) → 65

1₀(23) → 144

1₀(121) → 122

1₀(173) → 170

1₀(139) → 135

1₀(130) → 128

1₀(7) → 1

1₀(15) → 16

1₀(165) → 164

1₀(172) → 173

1₀(127) → 125

1₀(42) → 56

1₀(183) → 180

1₀(126) → 141

1₀(154) → 155

1₀(142) → 140

1₀(162) → 163

1₀(59) → 60

1₀(148) → 145

0₁(217) → 218

0₁(263) → 264

0₁(283) → 284

0₁(313) → 314

0₁(235) → 236

0₁(205) → 206

0₁(295) → 296

1₁(212) → 213

1₁(266) → 267

1₁(318) → 319

1₁(290) → 291

1₁(292) → 293

1₁(311) → 312

1₁(210) → 211

1₁(262) → 263

1₁(233) → 234

1₁(284) → 285

1₁(288) → 289

1₁(238) → 239

1₁(214) → 215

1₁(206) → 207

239	→	257
111	→	188
25	→	188
61	→	188
102	→	188
29	→	188
315	→	288
128	→	15
87	→	188
98	→	188
51	→	188
97	→	188
289	→	35
129	→	205
129	→	212
129	→	232
167	→	262
149	→	66
211	→	16
145	→	188
39	→	188
120	→	36
120	→	26
120	→	15
184	→	117
184	→	188
57	→	188
218	→	16
187	→	188
34	→	188
65	→	188
20	→	188
193	→	66
107	→	188
1	→	35
1	→	9
123	→	188
8	→	35
8	→	9
71	→	194
71	→	9
44	→	188
135	→	188
179	→	194
179	→	9
261	→	243
125	→	15
296	→	35
79	→	188
170	→	188
161	→	188
268	→	35
116	→	188
22	→	188
75	→	194
75	→	9
237	→	210
174	→	188
143	→	188
180	→	4
180	→	9
244	→	35
14	→	35
14	→	9
140	→	188
182	→	283
182	→	290
182	→	310
83	→	188
48	→	188
164	→	188
168	→	238
320	→	36
285	→	316
131	→	194
131	→	9
92	→	188
166	→	16
166	→	9
56	→	188
151	→	194
151	→	9
156	→	188
3₁(260)	→	261
3₁(215)	→	216
3₁(293)	→	294
3₁(234)	→	235
3₁(291)	→	292
3₁(208)	→	209
3₁(286)	→	287
3₁(316)	→	317
3₁(236)	→	237
3₁(312)	→	313
3₁(213)	→	214
3₁(241)	→	242
3₁(257)	→	258
3₁(314)	→	315
3₁(264)	→	265
2₁(258)	→	259
2₁(239)	→	240
2₁(240)	→	241
2₁(319)	→	320
2₁(207)	→	208
2₁(285)	→	286
2₁(267)	→	268
4₁(287)	→	288
4₁(209)	→	210
4₁(216)	→	217
4₁(243)	→	244
4₁(294)	→	295
5₁(232)	→	233
5₁(259)	→	260
5₁(242)	→	243
5₁(310)	→	311
5₁(265)	→	266
5₁(317)	→	318
3₀(31)	→	32
3₀(16)	→	17
3₀(115)	→	111
3₀(67)	→	68
3₀(53)	→	129
3₀(11)	→	12
3₀(127)	→	165
3₀(146)	→	147
3₀(157)	→	158
3₀(112)	→	113
3₀(3)	→	88
3₀(195)	→	196
3₀(66)	→	67
3₀(77)	→	78
3₀(150)	→	149
3₀(26)	→	27
3₀(133)	→	134
3₀(18)	→	19
3₀(64)	→	61
3₀(113)	→	162
3₀(9)	→	10
3₀(99)	→	100
3₀(6)	→	124
3₀(94)	→	95
3₀(84)	→	85
3₀(136)	→	137
3₀(109)	→	110
3₀(62)	→	63
3₀(72)	→	73
3₀(15)	→	58
3₀(101)	→	98
3₀(42)	→	43
3₀(81)	→	82
3₀(10)	→	45
3₀(5)	→	6
3₀(4)	→	21
3₀(117)	→	118
3₀(36)	→	37
3₀(40)	→	41
3₀(2)	→	30
3₀(152)	→	153
3₀(103)	→	104
2₀(2)	→	66
2₀(132)	→	133
2₀(31)	→	108
2₀(155)	→	151
2₀(26)	→	62
2₀(42)	→	150
2₀(192)	→	187
2₀(4)	→	5
2₀(144)	→	143
2₀(80)	→	81
2₀(119)	→	116
2₀(91)	→	87
2₀(60)	→	57
2₀(141)	→	142
2₀(9)	→	40
2₀(93)	→	146
2₀(23)	→	24
2₀(169)	→	166
2₀(197)	→	193
2₀(66)	→	93
2₀(15)	→	112
2₀(86)	→	83
2₀(3)	→	175
2₀(10)	→	76
2₀(30)	→	157
2₀(122)	→	120
2₀(40)	→	72
4₀(124)	→	123
4₀(177)	→	178
4₀(41)	→	42
4₀(78)	→	75
4₀(63)	→	64
4₀(30)	→	52
4₀(147)	→	148
4₀(160)	→	156
4₀(37)	→	38
4₀(85)	→	86
4₀(58)	→	59
4₀(45)	→	46
4₀(32)	→	33
4₀(95)	→	96
4₀(6)	→	7
4₀(134)	→	131
4₀(110)	→	107
4₀(176)	→	177
4₀(88)	→	89
4₀(46)	→	47
4₀(82)	→	79
4₀(3)	→	117
4₀(104)	→	105
4₀(113)	→	114
4₀(163)	→	161
4₀(196)	→	197
4₀(96)	→	92
4₀(12)	→	13
4₀(27)	→	28
4₀(21)	→	20
4₀(74)	→	71
4₀(67)	→	99
4₀(17)	→	185
4₀(10)	→	23
4₀(2)	→	188
4₀(68)	→	69
4₀(138)	→	139
4₀(171)	→	172
4₀(89)	→	90
4₀(186)	→	184
0₀(17)	→	18
0₀(47)	→	44
0₀(129)	→	130
0₀(54)	→	55
0₀(28)	→	25
0₀(56)	→	179
0₀(43)	→	39
0₀(13)	→	8
0₀(118)	→	119
0₀(9)	→	152
0₀(49)	→	50
0₀(182)	→	183
0₀(52)	→	126
0₀(189)	→	190
0₀(3)	→	136
0₀(175)	→	176
0₀(185)	→	186
0₀(114)	→	115
0₀(24)	→	22
0₀(38)	→	34
0₀(33)	→	29
0₀(188)	→	189
0₀(105)	→	106
0₀(2)	→	3
5₀(90)	→	91
5₀(70)	→	97
5₀(93)	→	94
5₀(137)	→	138
5₀(53)	→	54
5₀(21)	→	121
5₀(73)	→	74
5₀(190)	→	191
5₀(9)	→	26
5₀(23)	→	49
5₀(191)	→	192
5₀(194)	→	195
5₀(50)	→	48
5₀(69)	→	70
5₀(126)	→	127
5₀(66)	→	103
5₀(76)	→	77
5₀(2)	→	15
5₀(3)	→	80
5₀(30)	→	167
5₀(168)	→	169
5₀(35)	→	36
5₀(52)	→	53
5₀(108)	→	109
5₀(136)	→	171
5₀(106)	→	102
5₀(15)	→	84
5₀(158)	→	159
5₀(67)	→	181
5₀(100)	→	101
5₀(153)	→	154
f6₀	→	2
1₀(2)	→	9
1₀(167)	→	168
1₀(117)	→	132
1₀(9)	→	35
1₀(10)	→	11
1₀(19)	→	14
1₀(30)	→	31
1₀(55)	→	51
1₀(159)	→	160
1₀(178)	→	174
1₀(181)	→	182
1₀(3)	→	4
1₀(66)	→	194
1₀(70)	→	65
1₀(23)	→	144
1₀(121)	→	122
1₀(173)	→	170
1₀(139)	→	135
1₀(130)	→	128
1₀(7)	→	1
1₀(15)	→	16
1₀(165)	→	164
1₀(172)	→	173
1₀(127)	→	125
1₀(42)	→	56
1₀(183)	→	180
1₀(126)	→	141
1₀(154)	→	155
1₀(142)	→	140
1₀(162)	→	163
1₀(59)	→	60
1₀(148)	→	145
0₁(217)	→	218
0₁(263)	→	264
0₁(283)	→	284
0₁(313)	→	314
0₁(235)	→	236
0₁(205)	→	206
0₁(295)	→	296
1₁(212)	→	213
1₁(266)	→	267
1₁(318)	→	319
1₁(290)	→	291
1₁(292)	→	293
1₁(311)	→	312
1₁(210)	→	211
1₁(262)	→	263
1₁(233)	→	234
1₁(284)	→	285
1₁(288)	→	289
1₁(238)	→	239
1₁(214)	→	215
1₁(206)	→	207