YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 Bounds

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

final states:

{222, 206, 188, 171, 155, 141, 125, 113, 103, 92, 81, 70, 63, 55, 50, 43, 37, 31, 24, 21, 17, 12, 8, 5, 1}

transitions:

81 → 72

81 → 13

103 → 44

50 → 6

5 → 13

37 → 82

37 → 3

55 → 6

31 → 45

31 → 25

1 → 104

1 → 25

8 → 82

8 → 3

222 → 208

222 → 3

125 → 3

21 → 9

141 → 9

171 → 9

188 → 104

188 → 25

63 → 28

63 → 13

12 → 82

12 → 3

113 → 14

113 → 6

182 → 242

245 → 186

17 → 13

206 → 44

92 → 189

92 → 44

24 → 114

24 → 25

43 → 189

43 → 44

70 → 22

70 → 7

70 → 3

155 → 6

1₁(243) → 244

1₀(16) → 12

1₀(53) → 54

1₀(229) → 230

1₀(162) → 163

1₀(157) → 158

1₀(227) → 228

1₀(44) → 82

1₀(207) → 208

1₀(58) → 59

1₀(93) → 94

1₀(80) → 70

1₀(165) → 166

1₀(159) → 160

1₀(138) → 139

1₀(64) → 65

1₀(99) → 100

1₀(6) → 7

1₀(96) → 97

1₀(136) → 137

1₀(109) → 110

1₀(236) → 237

1₀(204) → 205

1₀(230) → 231

1₀(102) → 92

1₀(161) → 162

1₀(220) → 221

1₀(191) → 192

1₀(14) → 22

1₀(139) → 140

1₀(122) → 123

1₀(2) → 3

1₀(178) → 179

1₀(213) → 214

1₀(168) → 169

1₀(156) → 157

1₀(226) → 227

1₀(219) → 220

4₀(72) → 73

4₀(2) → 6

4₀(78) → 79

4₀(231) → 232

4₀(117) → 118

4₀(160) → 161

4₀(74) → 75

4₀(124) → 113

4₀(51) → 52

4₀(201) → 202

4₀(44) → 223

4₀(48) → 49

4₀(88) → 89

4₀(28) → 29

4₀(209) → 210

4₀(234) → 235

4₀(198) → 199

4₀(223) → 224

4₀(210) → 211

4₀(143) → 144

4₀(18) → 19

4₀(217) → 218

4₀(134) → 135

4₀(13) → 14

4₀(169) → 170

4₀(170) → 155

4₀(84) → 85

4₀(67) → 68

4₀(184) → 185

4₀(142) → 143

4₀(166) → 167

4₀(130) → 131

4₀(86) → 87

4₀(3) → 32

4₀(10) → 11

4₀(52) → 53

4₀(94) → 95

4₀(101) → 102

4₀(149) → 150

4₀(196) → 197

4₀(30) → 24

4₀(208) → 209

4₀(151) → 152

3₀(98) → 99

3₀(65) → 66

3₀(33) → 34

3₀(239) → 240

3₀(41) → 42

3₀(216) → 217

3₀(144) → 145

3₀(19) → 20

3₀(7) → 5

3₀(205) → 188

3₀(132) → 133

3₀(34) → 35

3₀(105) → 106

3₀(11) → 8

3₀(167) → 168

3₀(110) → 111

3₀(152) → 153

3₀(202) → 203

3₀(131) → 132

3₀(185) → 186

3₀(56) → 57

3₀(46) → 47

3₀(90) → 91

3₀(29) → 30

3₀(3) → 4

3₀(69) → 63

3₀(104) → 172

3₀(221) → 206

3₀(232) → 233

3₀(146) → 147

3₀(192) → 193

3₀(27) → 28

3₀(71) → 72

3₀(2) → 13

3₀(44) → 71

3₀(186) → 187

5₀(106) → 107

5₀(112) → 103

5₀(218) → 219

5₀(47) → 48

5₀(82) → 83

5₀(164) → 165

5₀(61) → 62

5₀(66) → 67

5₀(128) → 129

5₀(6) → 93

5₀(13) → 18

5₀(147) → 148

5₀(107) → 108

5₀(15) → 16

5₀(235) → 236

5₀(9) → 10

5₀(49) → 43

5₀(154) → 141

5₀(145) → 146

5₀(240) → 241

5₀(62) → 55

5₀(158) → 159

5₀(195) → 196

5₀(57) → 58

5₀(150) → 151

5₀(32) → 33

5₀(176) → 177

5₀(95) → 96

5₀(114) → 207

5₀(45) → 142

5₀(38) → 39

5₀(33) → 64

5₀(228) → 229

5₀(23) → 21

5₀(91) → 81

5₀(104) → 105

5₀(127) → 128

5₀(187) → 171

5₀(2) → 9

5₀(225) → 226

5₀(200) → 201

2₀(59) → 60

2₀(123) → 124

2₀(180) → 181

2₀(135) → 136

2₀(87) → 88

2₀(77) → 78

2₀(189) → 190

2₀(137) → 138

2₀(233) → 234

2₀(193) → 194

2₀(175) → 176

2₀(40) → 41

2₀(19) → 51

2₀(7) → 156

2₀(73) → 74

2₀(211) → 212

2₀(181) → 182

2₀(114) → 115

2₀(183) → 184

2₀(194) → 195

2₀(140) → 125

2₀(133) → 134

2₀(237) → 238

2₀(199) → 200

2₀(42) → 37

2₀(6) → 38

2₀(241) → 222

2₀(83) → 84

2₀(174) → 175

2₀(2) → 44

2₀(163) → 164

2₀(129) → 130

2₀(35) → 36

2₀(116) → 117

2₀(115) → 116

2₀(13) → 189

2₀(100) → 101

2₀(25) → 26

2₀(153) → 154

2₀(203) → 204

f6₀ → 2

0₀(2) → 25

0₀(114) → 126

0₀(177) → 178

0₀(224) → 225

0₀(197) → 198

0₀(54) → 50

0₀(79) → 80

0₀(36) → 31

0₀(215) → 216

0₀(25) → 114

0₀(4) → 1

0₀(26) → 27

0₀(76) → 77

0₀(38) → 56

0₀(89) → 90

0₀(3) → 104

0₀(214) → 215

0₀(14) → 15

0₀(118) → 119

0₀(238) → 239

0₀(121) → 122

0₀(111) → 112

0₀(173) → 174

0₀(45) → 46

0₀(22) → 23

0₀(172) → 173

0₀(75) → 76

0₀(85) → 86

0₀(20) → 17

0₀(120) → 121

0₀(39) → 40

0₀(126) → 127

0₀(97) → 98

0₀(60) → 61

0₀(212) → 213

0₀(108) → 109

0₀(44) → 45

0₀(190) → 191

0₀(179) → 180

0₀(148) → 149

0₀(68) → 69

0₀(119) → 120

0₀(182) → 183

4₁(242) → 243

3₁(244) → 245

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