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)))	→	1(2(1(2(0(x0)))))
0(3(1(x0)))	→	1(3(2(2(0(x0)))))
0(3(1(x0)))	→	3(2(1(2(0(x0)))))
0(3(1(x0)))	→	1(3(3(3(2(0(x0))))))
0(4(1(x0)))	→	2(1(2(0(4(x0)))))
0(0(4(5(x0))))	→	0(0(2(5(4(x0)))))
0(1(4(1(x0))))	→	0(1(2(2(4(1(x0))))))
0(1(4(5(x0))))	→	4(0(1(2(5(4(x0))))))
0(1(5(1(x0))))	→	1(2(2(5(0(1(x0))))))
0(1(5(3(x0))))	→	0(5(3(2(1(x0)))))
0(2(4(1(x0))))	→	1(3(3(2(0(4(x0))))))
0(2(4(1(x0))))	→	4(2(1(2(0(4(x0))))))
0(2(4(5(x0))))	→	0(2(2(5(0(4(x0))))))
0(3(1(5(x0))))	→	0(1(2(5(3(x0)))))
0(3(1(5(x0))))	→	1(2(5(3(0(4(x0))))))
0(3(5(1(x0))))	→	1(2(5(3(0(x0)))))
0(3(5(1(x0))))	→	0(5(2(1(2(3(x0))))))
0(3(5(5(x0))))	→	0(3(2(5(5(x0)))))
0(4(0(1(x0))))	→	2(0(4(4(0(1(x0))))))
0(4(1(5(x0))))	→	1(2(5(0(4(x0)))))
0(4(3(5(x0))))	→	0(4(3(2(5(4(x0))))))
0(4(5(1(x0))))	→	2(5(4(4(0(1(x0))))))
3(0(1(5(x0))))	→	3(1(4(0(5(4(x0))))))
3(0(3(1(x0))))	→	1(3(3(2(0(x0)))))
3(0(3(5(x0))))	→	3(2(5(0(2(3(x0))))))
3(3(0(1(x0))))	→	0(1(3(2(2(3(x0))))))
3(4(5(1(x0))))	→	3(2(5(4(2(1(x0))))))
4(1(3(5(x0))))	→	1(2(5(3(4(4(x0))))))
4(1(5(1(x0))))	→	4(4(5(1(2(1(x0))))))
4(4(1(5(x0))))	→	4(1(2(5(4(x0)))))
0(1(4(5(5(x0)))))	→	0(5(1(4(2(5(x0))))))
0(2(1(4(5(x0)))))	→	0(0(1(2(5(4(x0))))))
0(2(1(5(5(x0)))))	→	0(1(2(2(5(5(x0))))))
0(4(2(4(1(x0)))))	→	1(3(2(0(4(4(x0))))))
0(4(5(4(3(x0)))))	→	2(5(0(4(4(3(x0))))))
0(5(1(5(1(x0)))))	→	0(5(1(1(2(5(x0))))))
0(5(2(1(5(x0)))))	→	1(2(5(5(0(4(x0))))))
0(5(2(4(1(x0)))))	→	4(5(2(1(2(0(x0))))))
3(0(1(4(1(x0)))))	→	0(4(4(1(3(1(x0))))))
3(0(1(4(1(x0)))))	→	4(3(2(0(1(1(x0))))))
3(0(3(5(5(x0)))))	→	3(3(2(5(0(5(x0))))))
3(0(5(3(1(x0)))))	→	1(0(3(3(2(5(x0))))))
4(0(1(4(1(x0)))))	→	4(4(0(1(3(1(x0))))))
4(0(1(5(1(x0)))))	→	0(1(2(5(4(1(x0))))))
4(0(2(4(5(x0)))))	→	4(0(2(5(0(4(x0))))))
4(1(1(5(1(x0)))))	→	1(1(2(5(4(1(x0))))))
4(5(1(4(1(x0)))))	→	4(4(1(2(1(5(x0))))))
4(5(2(3(1(x0)))))	→	4(3(1(2(2(5(x0))))))
4(5(4(3(1(x0)))))	→	4(1(2(5(3(4(x0))))))
4(5(5(3(1(x0)))))	→	1(3(2(5(5(4(x0))))))

Proof

1 String Reversal

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

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

1.1 Bounds

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

final states:

{192, 190, 186, 182, 177, 173, 171, 167, 162, 157, 152, 148, 143, 140, 137, 133, 130, 128, 124, 120, 116, 111, 109, 106, 102, 98, 51, 93, 88, 83, 81, 76, 72, 68, 67, 64, 62, 57, 52, 49, 45, 41, 35, 30, 25, 20, 16, 11, 7, 1}

transitions:

23 → 207

111 → 3

25 → 144

102 → 31

102 → 3

152 → 117

152 → 3

51 → 94

51 → 3

167 → 117

167 → 3

133 → 153

133 → 12

41 → 3

50 → 231

57 → 144

55 → 237

130 → 117

130 → 3

20 → 117

20 → 3

224 → 178

49 → 117

49 → 3

1 → 178

1 → 3

76 → 38

76 → 31

76 → 3

79 → 239

91 → 243

177 → 3

186 → 94

186 → 3

173 → 144

171 → 3

88 → 3

52 → 117

52 → 3

124 → 144

67 → 3

143 → 117

143 → 3

11 → 94

11 → 3

232 → 208

244 → 220

212 → 178

45 → 12

106 → 3

16 → 94

16 → 3

7 → 94

7 → 3

182 → 117

182 → 3

30 → 117

30 → 3

137 → 3

162 → 94

162 → 3

35 → 144

240 → 220

190 → 187

190 → 94

190 → 3

154 → 201

68 → 3

206 → 152

148 → 117

148 → 3

43 → 219

192 → 94

192 → 3

238 → 208

f6₀ → 2

5₀(179) → 180

5₀(59) → 60

5₀(123) → 120

5₀(96) → 97

5₀(65) → 141

5₀(189) → 186

5₀(185) → 182

5₀(193) → 194

5₀(166) → 162

5₀(21) → 89

5₀(118) → 119

5₀(139) → 137

5₀(32) → 63

5₀(9) → 193

5₀(42) → 43

5₀(126) → 127

5₀(74) → 75

5₀(4) → 65

5₀(174) → 175

5₀(26) → 46

5₀(36) → 144

5₀(75) → 72

5₀(129) → 128

5₀(28) → 29

5₀(161) → 157

5₀(33) → 129

5₀(13) → 99

5₀(39) → 40

5₀(86) → 87

5₀(159) → 160

5₀(112) → 113

4₁(211) → 212

2₀(114) → 115

2₀(73) → 74

2₀(100) → 101

2₀(70) → 71

2₀(165) → 166

2₀(26) → 58

2₀(14) → 15

2₀(183) → 184

2₀(144) → 145

2₀(37) → 174

2₀(85) → 86

2₀(58) → 59

2₀(178) → 179

2₀(8) → 9

2₀(125) → 126

2₀(32) → 33

2₀(38) → 39

2₀(107) → 108

2₀(187) → 188

2₀(158) → 159

2₀(46) → 69

2₀(36) → 53

2₀(18) → 19

2₀(3) → 4

2₀(47) → 48

2₀(104) → 105

2₀(9) → 10

2₀(54) → 55

2₀(12) → 13

2₀(146) → 147

2₀(27) → 28

2₀(117) → 118

2₀(31) → 32

2₀(5) → 6

2₀(103) → 104

2₀(17) → 50

2₀(122) → 123

2₀(2) → 21

2₀(4) → 42

2₀(153) → 154

2₀(188) → 189

2₀(138) → 139

2₀(22) → 23

1₀(115) → 111

1₀(53) → 54

1₀(46) → 121

1₀(92) → 88

1₀(37) → 38

1₀(112) → 183

1₀(3) → 178

1₀(44) → 41

1₀(48) → 45

1₀(121) → 138

1₀(184) → 185

1₀(21) → 22

1₀(26) → 31

1₀(80) → 76

1₀(170) → 167

1₀(108) → 106

1₀(155) → 156

1₀(113) → 114

1₀(151) → 148

1₀(27) → 125

1₀(145) → 146

1₀(149) → 150

1₀(13) → 14

1₀(4) → 5

1₀(181) → 177

1₀(36) → 117

1₀(2) → 3

1₀(172) → 171

1₀(34) → 30

1₀(168) → 169

1₀(69) → 70

1₀(156) → 152

1₀(12) → 94

1₀(153) → 187

0₁(223) → 224

0₁(205) → 206

0₁(210) → 211

3₀(2) → 12

3₀(31) → 103

3₀(71) → 68

3₀(26) → 73

3₀(136) → 133

3₀(46) → 47

3₀(119) → 191

3₀(164) → 165

3₀(150) → 151

3₀(12) → 158

3₀(8) → 17

3₀(105) → 102

3₀(36) → 153

3₀(163) → 164

3₀(17) → 18

3₀(169) → 170

3₀(63) → 62

3₀(84) → 85

3₀(3) → 8

3₀(101) → 98

3₀(65) → 66

0₀(2) → 26

0₀(91) → 92

0₀(9) → 131

0₀(65) → 82

0₀(10) → 7

0₀(175) → 176

0₀(50) → 51

0₀(95) → 96

0₀(99) → 100

0₀(79) → 80

0₀(19) → 16

0₀(36) → 37

0₀(55) → 56

0₀(43) → 44

0₀(21) → 77

0₀(26) → 27

0₀(89) → 134

0₀(3) → 163

0₀(147) → 143

0₀(6) → 1

0₀(141) → 142

0₀(66) → 67

0₀(23) → 24

0₀(112) → 168

0₀(15) → 11

0₀(154) → 155

0₀(60) → 61

0₀(160) → 161

2₁(231) → 232

2₁(207) → 208

2₁(204) → 205

2₁(209) → 210

2₁(202) → 203

2₁(220) → 221

2₁(222) → 223

2₁(237) → 238

1₁(221) → 222

1₁(219) → 220

1₁(239) → 240

1₁(203) → 204

1₁(243) → 244

1₁(208) → 209

1₁(201) → 202

4₀(87) → 83

4₀(29) → 25

4₀(191) → 190

4₀(132) → 130

4₀(142) → 140

4₀(97) → 93

4₀(135) → 136

4₀(78) → 79

4₀(99) → 107

4₀(82) → 81

4₀(61) → 57

4₀(63) → 172

4₀(94) → 95

4₀(26) → 84

4₀(66) → 110

4₀(36) → 112

4₀(84) → 149

4₀(56) → 52

4₀(90) → 91

4₀(67) → 64

4₀(89) → 90

4₀(194) → 192

4₀(119) → 116

4₀(40) → 35

4₀(176) → 173

4₀(110) → 109

4₀(121) → 122

4₀(131) → 132

4₀(24) → 20

4₀(180) → 181

4₀(134) → 135

4₀(51) → 49

4₀(77) → 78

4₀(33) → 34

4₀(127) → 124

4₀(2) → 36

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