YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 String Reversal

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

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

1.1 Bounds

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

final states:

{163, 158, 154, 150, 144, 140, 137, 133, 130, 126, 121, 116, 113, 109, 107, 104, 100, 97, 92, 88, 83, 78, 73, 71, 69, 66, 63, 60, 57, 53, 50, 45, 39, 34, 30, 27, 25, 23, 18, 16, 15, 13, 10, 6, 1}

transitions:

78 → 3

223 → 167

23 → 3

221 → 187

25 → 3

205 → 184

229 → 181

10 → 3

97 → 3

15 → 3

133 → 3

18 → 3

39 → 3

184 → 204

184 → 256

50 → 3

57 → 3

213 → 169

187 → 196

187 → 220

34 → 3

199 → 54

185 → 54

185 → 198

130 → 3

107 → 79

107 → 3

1 → 3

40 → 166

40 → 181

40 → 206

40 → 230

71 → 3

13 → 3

183 → 186

183 → 222

60 → 3

197 → 184

73 → 3

233 → 187

170 → 54

170 → 212

251 → 182

150 → 3

207 → 181

257 → 168

121 → 3

6 → 3

116 → 3

109 → 3

88 → 3

249 → 54

53 → 3

2 → 250

188 → 214

45 → 3

66 → 3

16 → 3

63 → 3

104 → 3

140 → 3

100 → 3

69 → 3

113 → 3

182 → 228

126 → 3

30 → 3

137 → 3

189 → 54

158 → 3

231 → 244

83 → 3

154 → 3

215 → 169

92 → 3

144 → 3

27 → 3

163 → 54

163 → 3

0₁(247) → 248

0₁(187) → 188

0₁(231) → 232

0₁(166) → 167

0₁(168) → 169

0₁(184) → 185

0₁(245) → 246

0₁(182) → 183

1₁(228) → 229

1₁(246) → 247

1₁(188) → 189

1₁(212) → 213

1₁(181) → 182

1₁(186) → 187

1₁(167) → 168

1₁(244) → 245

3₁(220) → 221

3₁(230) → 231

3₁(250) → 251

3₁(198) → 199

1₀(31) → 32

1₀(74) → 75

1₀(35) → 36

1₀(19) → 20

1₀(3) → 4

1₀(7) → 35

1₀(93) → 101

1₀(8) → 11

1₀(29) → 27

1₀(114) → 115

1₀(64) → 110

1₀(79) → 80

1₀(102) → 103

1₀(47) → 48

1₀(40) → 46

1₀(2) → 7

1₀(85) → 86

1₀(1) → 24

1₀(156) → 157

1₀(54) → 55

1₀(12) → 10

3₀(2) → 40

3₀(159) → 160

3₀(160) → 161

3₀(74) → 84

3₀(6) → 15

3₀(98) → 99

3₀(59) → 57

3₀(76) → 108

3₀(164) → 165

3₀(141) → 142

3₀(11) → 28

3₀(9) → 72

3₀(93) → 94

3₀(64) → 65

3₀(118) → 119

3₀(138) → 139

3₀(145) → 146

3₀(146) → 147

3₀(3) → 93

3₀(127) → 128

3₀(40) → 117

3₀(65) → 70

0₀(124) → 125

0₀(148) → 149

0₀(42) → 43

0₀(41) → 54

0₀(14) → 13

0₀(86) → 87

0₀(142) → 143

0₀(7) → 8

0₀(58) → 59

0₀(51) → 52

0₀(84) → 114

0₀(11) → 12

0₀(32) → 33

0₀(99) → 97

0₀(38) → 34

0₀(152) → 153

0₀(155) → 156

0₀(55) → 56

0₀(129) → 126

0₀(46) → 47

0₀(75) → 76

0₀(36) → 37

0₀(28) → 29

0₀(40) → 41

0₀(139) → 137

0₀(9) → 6

0₀(101) → 102

0₀(161) → 162

0₀(94) → 95

0₀(61) → 62

0₀(20) → 21

0₀(135) → 136

0₀(74) → 79

0₀(31) → 164

0₀(48) → 49

0₀(67) → 68

0₀(119) → 120

0₀(17) → 16

0₀(2) → 3

0₀(4) → 5

0₀(22) → 18

0₀(89) → 90

4₀(19) → 127

4₀(106) → 104

4₀(132) → 130

4₀(8) → 31

4₀(58) → 61

4₀(5) → 51

4₀(157) → 154

4₀(41) → 42

4₀(49) → 45

4₀(52) → 50

4₀(3) → 122

4₀(74) → 134

4₀(95) → 96

4₀(77) → 73

4₀(111) → 112

4₀(2) → 145

5₀(64) → 155

5₀(70) → 69

5₀(123) → 124

5₀(147) → 148

5₀(93) → 151

5₀(96) → 92

5₀(65) → 63

5₀(72) → 71

5₀(128) → 129

5₀(40) → 67

5₀(42) → 98

5₀(165) → 163

5₀(84) → 85

5₀(117) → 118

5₀(4) → 105

5₀(151) → 152

5₀(2) → 74

5₀(3) → 89

5₀(122) → 123

5₀(103) → 100

5₀(58) → 138

5₀(108) → 107

5₀(134) → 135

5₀(112) → 109

f6₀ → 2

2₀(2) → 19

2₀(149) → 144

2₀(56) → 53

2₀(91) → 88

2₀(9) → 17

2₀(90) → 91

2₀(105) → 106

2₀(110) → 111

2₀(67) → 141

2₀(79) → 131

2₀(80) → 81

2₀(24) → 23

2₀(131) → 132

2₀(43) → 44

2₀(8) → 9

2₀(21) → 22

2₀(26) → 25

2₀(37) → 38

2₀(76) → 77

2₀(74) → 159

2₀(3) → 64

2₀(11) → 14

2₀(87) → 83

2₀(136) → 133

2₀(62) → 60

2₀(125) → 121

2₀(81) → 82

2₀(33) → 30

2₀(82) → 78

2₀(120) → 116

2₀(12) → 26

2₀(143) → 140

2₀(162) → 158

2₀(41) → 58

2₀(44) → 39

2₀(5) → 1

2₀(68) → 66

2₀(115) → 113

2₀(153) → 150

4₁(256) → 257

4₁(232) → 233

4₁(248) → 249

4₁(222) → 223

2₁(204) → 205

2₁(183) → 184

2₁(169) → 170

2₁(196) → 197

2₁(214) → 215

2₁(206) → 207

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