YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 Bounds

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

final states:

{243, 226, 209, 192, 175, 163, 149, 137, 125, 112, 99, 87, 78, 70, 62, 51, 42, 35, 28, 21, 16, 13, 9, 5, 1}

transitions:

78 → 88

87 → 115

87 → 88

51 → 52

149 → 88

226 → 6

9 → 113

9 → 88

5 → 150

5 → 88

209 → 88

175 → 193

175 → 52

243 → 113

243 → 88

99 → 113

99 → 88

62 → 100

62 → 17

1 → 53

1 → 6

13 → 6

125 → 88

21 → 6

28 → 193

28 → 52

16 → 7

16 → 3

112 → 52

42 → 88

137 → 10

35 → 176

35 → 3

70 → 88

163 → 150

163 → 88

192 → 244

192 → 3

f6₀ → 2

4₀(121) → 122

4₀(77) → 70

4₀(96) → 97

4₀(230) → 231

4₀(189) → 190

4₀(247) → 248

4₀(227) → 228

4₀(118) → 119

4₀(98) → 87

4₀(120) → 121

4₀(188) → 189

4₀(250) → 251

4₀(211) → 212

4₀(225) → 209

4₀(46) → 47

4₀(114) → 115

4₀(222) → 223

4₀(133) → 134

4₀(186) → 187

4₀(167) → 168

4₀(182) → 183

4₀(85) → 86

4₀(63) → 64

4₀(151) → 152

4₀(240) → 241

4₀(162) → 149

4₀(82) → 83

4₀(43) → 44

4₀(83) → 84

4₀(2) → 88

4₀(228) → 229

4₀(26) → 27

4₀(170) → 171

4₀(231) → 232

4₀(129) → 130

4₀(103) → 104

4₀(58) → 59

4₀(52) → 150

4₀(161) → 162

4₀(259) → 260

4₀(10) → 113

4₀(33) → 34

4₀(17) → 29

4₀(153) → 154

4₀(204) → 205

4₀(150) → 151

4₀(248) → 249

2₀(106) → 107

2₀(219) → 220

2₀(126) → 127

2₀(100) → 101

2₀(200) → 201

2₀(216) → 217

2₀(252) → 253

2₀(30) → 31

2₀(37) → 38

2₀(169) → 170

2₀(130) → 131

2₀(174) → 163

2₀(143) → 144

2₀(32) → 33

2₀(6) → 7

2₀(220) → 221

2₀(202) → 203

2₀(56) → 57

2₀(88) → 210

2₀(197) → 198

2₀(29) → 30

2₀(238) → 239

2₀(18) → 36

2₀(3) → 43

2₀(139) → 140

2₀(234) → 235

2₀(113) → 114

2₀(140) → 141

2₀(111) → 99

2₀(57) → 58

2₀(25) → 26

2₀(12) → 9

2₀(261) → 243

2₀(146) → 147

2₀(193) → 194

2₀(27) → 21

2₀(223) → 224

2₀(20) → 16

2₀(246) → 247

2₀(17) → 18

2₀(122) → 123

2₀(10) → 176

2₀(2) → 3

2₀(22) → 23

2₀(52) → 244

0₀(244) → 245

0₀(239) → 240

0₀(115) → 116

0₀(180) → 181

0₀(49) → 50

0₀(105) → 106

0₀(224) → 225

0₀(207) → 208

0₀(91) → 92

0₀(184) → 185

0₀(93) → 94

0₀(8) → 5

0₀(135) → 136

0₀(52) → 53

0₀(206) → 207

0₀(165) → 166

0₀(108) → 109

0₀(128) → 129

0₀(199) → 200

0₀(237) → 238

0₀(59) → 60

0₀(208) → 192

0₀(201) → 202

0₀(179) → 180

0₀(145) → 146

0₀(119) → 120

0₀(109) → 110

0₀(75) → 76

0₀(102) → 103

0₀(55) → 56

0₀(76) → 77

0₀(214) → 215

0₀(205) → 206

0₀(97) → 98

0₀(63) → 164

0₀(4) → 14

0₀(117) → 118

0₀(160) → 161

0₀(40) → 41

0₀(2) → 6

0₀(164) → 165

0₀(17) → 79

0₀(241) → 242

0₀(104) → 105

0₀(54) → 55

0₀(217) → 218

0₀(132) → 133

1₀(72) → 73

1₀(2) → 52

1₀(255) → 256

1₀(45) → 46

1₀(159) → 160

1₀(155) → 156

1₀(152) → 153

1₀(71) → 72

1₀(110) → 111

1₀(88) → 193

1₀(24) → 25

1₀(144) → 145

1₀(173) → 174

1₀(218) → 219

1₀(254) → 255

1₀(185) → 186

1₀(198) → 199

1₀(260) → 261

1₀(61) → 51

1₀(191) → 175

1₀(176) → 177

1₀(141) → 142

1₀(253) → 254

1₀(36) → 37

1₀(18) → 63

1₀(195) → 196

1₀(23) → 24

1₀(212) → 213

1₀(17) → 138

1₀(107) → 108

1₀(257) → 258

1₀(131) → 132

1₀(168) → 169

1₀(86) → 78

1₀(10) → 11

1₀(101) → 102

3₀(2) → 17

3₀(18) → 19

3₀(156) → 157

3₀(134) → 135

3₀(258) → 259

3₀(48) → 49

3₀(50) → 42

3₀(67) → 68

3₀(79) → 80

3₀(166) → 167

3₀(232) → 233

3₀(215) → 216

3₀(235) → 236

3₀(92) → 93

3₀(4) → 1

3₀(74) → 75

3₀(3) → 4

3₀(17) → 100

3₀(249) → 250

3₀(11) → 12

3₀(84) → 85

3₀(147) → 148

3₀(245) → 246

3₀(53) → 54

3₀(136) → 125

3₀(256) → 257

3₀(81) → 82

3₀(251) → 252

3₀(7) → 8

3₀(15) → 13

3₀(172) → 173

3₀(183) → 184

3₀(39) → 40

3₀(73) → 74

3₀(154) → 155

3₀(229) → 230

3₀(41) → 35

3₀(44) → 45

3₀(187) → 188

3₀(242) → 226

3₀(88) → 227

3₀(68) → 69

3₀(47) → 48

3₀(171) → 172

3₀(69) → 62

5₀(19) → 20

5₀(17) → 126

5₀(142) → 143

5₀(123) → 124

5₀(177) → 178

5₀(203) → 204

5₀(88) → 89

5₀(53) → 71

5₀(94) → 95

5₀(124) → 112

5₀(66) → 67

5₀(60) → 61

5₀(157) → 158

5₀(196) → 197

5₀(236) → 237

5₀(90) → 91

5₀(10) → 22

5₀(148) → 137

5₀(181) → 182

5₀(89) → 90

5₀(116) → 117

5₀(194) → 195

5₀(14) → 15

5₀(80) → 81

5₀(31) → 32

5₀(65) → 66

5₀(190) → 191

5₀(158) → 159

5₀(34) → 28

5₀(95) → 96

5₀(138) → 139

5₀(210) → 211

5₀(64) → 65

5₀(38) → 39

5₀(233) → 234

5₀(127) → 128

5₀(178) → 179

5₀(2) → 10

5₀(221) → 222

5₀(213) → 214

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