YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 Bounds

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

final states:

{164, 160, 157, 155, 151, 149, 147, 144, 139, 134, 129, 125, 121, 116, 111, 108, 105, 104, 102, 98, 97, 93, 89, 85, 79, 78, 74, 68, 66, 64, 59, 54, 53, 38, 50, 48, 46, 43, 42, 40, 37, 32, 28, 23, 18, 15, 10, 6, 1}

transitions:

78 → 7

157 → 69

23 → 7

111 → 55

111 → 7

102 → 69

32 → 7

89 → 7

98 → 90

98 → 19

10 → 7

97 → 19

15 → 7

129 → 7

149 → 19

260 → 227

18 → 7

184 → 177

50 → 7

213 → 226

213 → 247

108 → 69

134 → 126

134 → 7

147 → 19

37 → 7

59 → 7

65 → 176

31 → 189

246 → 193

1 → 7

40 → 7

60 → 69

139 → 7

125 → 7

38 → 90

38 → 19

79 → 7

233 → 209

248 → 213

257 → 259

121 → 7

6 → 7

116 → 55

116 → 7

54 → 55

54 → 7

105 → 166

105 → 69

53 → 90

53 → 19

28 → 7

212 → 243

258 → 227

66 → 7

14 → 183

93 → 7

85 → 7

182 → 126

42 → 7

137 → 191

137 → 206

137 → 211

137 → 229

64 → 7

216 → 55

46 → 7

48 → 7

160 → 69

190 → 177

164 → 166

164 → 69

68 → 7

74 → 7

195 → 55

144 → 7

43 → 7

210 → 55

151 → 165

151 → 19

155 → 90

155 → 19

192 → 255

228 → 209

f6₀ → 2

5₀(16) → 106

5₀(99) → 109

5₀(96) → 93

5₀(34) → 38

5₀(5) → 47

5₀(69) → 86

5₀(6) → 67

5₀(165) → 166

5₀(84) → 79

5₀(76) → 103

5₀(4) → 41

5₀(162) → 163

5₀(83) → 84

5₀(2) → 69

5₀(3) → 99

5₀(142) → 143

5₀(58) → 54

5₀(52) → 50

5₀(33) → 44

5₀(47) → 49

5₀(153) → 154

5₀(159) → 157

5₀(141) → 158

1₁(208) → 209

1₁(255) → 256

1₁(178) → 179

1₁(229) → 230

1₁(194) → 195

1₁(257) → 258

1₁(212) → 213

4₁(213) → 214

3₀(114) → 115

3₀(106) → 107

3₀(33) → 34

3₀(73) → 68

3₀(26) → 27

3₀(41) → 42

3₀(86) → 87

3₀(7) → 60

3₀(130) → 152

3₀(136) → 137

3₀(45) → 43

3₀(112) → 122

3₀(168) → 164

3₀(99) → 100

3₀(95) → 96

3₀(38) → 156

3₀(77) → 74

3₀(92) → 89

3₀(109) → 110

3₀(36) → 32

3₀(82) → 83

3₀(47) → 46

3₀(40) → 104

3₀(69) → 70

3₀(57) → 58

3₀(9) → 6

3₀(25) → 26

3₀(12) → 29

3₀(101) → 98

3₀(128) → 125

3₀(61) → 62

3₀(21) → 22

3₀(117) → 118

3₀(67) → 66

3₀(119) → 120

3₀(17) → 15

3₀(2) → 11

3₀(141) → 142

3₀(4) → 5

3₀(39) → 37

3₀(22) → 18

5₁(183) → 184

5₁(259) → 260

5₁(189) → 190

5₁(176) → 177

0₀(51) → 52

0₀(16) → 17

0₀(115) → 111

0₀(35) → 36

0₀(11) → 112

0₀(127) → 128

0₀(146) → 144

0₀(30) → 31

0₀(120) → 116

0₀(3) → 4

0₀(7) → 55

0₀(44) → 45

0₀(91) → 92

0₀(24) → 25

0₀(123) → 124

0₀(135) → 136

0₀(140) → 141

0₀(133) → 129

0₀(56) → 57

0₀(118) → 119

0₀(60) → 61

0₀(75) → 76

0₀(72) → 73

0₀(161) → 162

0₀(76) → 77

0₀(13) → 14

0₀(81) → 82

0₀(88) → 85

0₀(90) → 126

0₀(2) → 7

0₀(20) → 21

0₀(38) → 39

3₁(232) → 233

3₁(211) → 212

3₁(177) → 178

3₁(247) → 248

3₁(193) → 194

3₁(181) → 182

3₁(209) → 210

3₁(256) → 257

3₁(245) → 246

2₀(2) → 3

2₀(31) → 28

2₀(71) → 72

2₀(19) → 20

2₀(87) → 88

2₀(112) → 113

2₀(80) → 81

2₀(150) → 149

2₀(70) → 161

2₀(12) → 16

2₀(11) → 24

2₀(14) → 10

2₀(154) → 151

2₀(137) → 138

2₀(156) → 155

2₀(90) → 91

2₀(69) → 117

2₀(166) → 167

2₀(130) → 131

2₀(7) → 8

2₀(65) → 64

1₀(2) → 19

1₀(167) → 168

1₀(163) → 160

1₀(123) → 148

1₀(49) → 48

1₀(110) → 108

1₀(19) → 165

1₀(80) → 130

1₀(113) → 114

1₀(152) → 153

1₀(131) → 132

1₀(107) → 105

1₀(8) → 9

1₀(63) → 59

1₀(138) → 134

1₀(38) → 53

1₀(3) → 33

1₀(11) → 12

1₀(14) → 97

1₀(100) → 101

1₀(62) → 63

1₀(70) → 71

1₀(94) → 95

1₀(1) → 65

1₀(137) → 150

1₀(27) → 23

1₀(103) → 102

1₀(34) → 35

1₀(41) → 40

1₀(5) → 1

1₀(158) → 159

1₀(122) → 123

1₀(69) → 90

0₁(231) → 232

0₁(192) → 193

0₁(214) → 215

0₁(206) → 207

0₁(180) → 181

0₁(244) → 245

0₁(227) → 228

2₁(179) → 180

2₁(207) → 208

2₁(226) → 227

2₁(230) → 231

2₁(215) → 216

2₁(191) → 192

2₁(243) → 244

4₀(29) → 30

4₀(143) → 139

4₀(100) → 145

4₀(132) → 133

4₀(69) → 135

4₀(124) → 121

4₀(36) → 78

4₀(4) → 94

4₀(148) → 147

4₀(145) → 146

4₀(3) → 140

4₀(34) → 51

4₀(126) → 127

4₀(33) → 75

4₀(12) → 13

4₀(55) → 56

4₀(2) → 80

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