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

Proof

1 String Reversal

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

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

1.1 Bounds

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

final states:

{327, 308, 291, 274, 260, 244, 227, 211, 195, 180, 166, 152, 140, 126, 114, 102, 91, 79, 69, 59, 48, 41, 32, 24, 18, 15, 12, 8, 5, 1}

transitions:

102 → 19

102 → 9

32 → 33

152 → 6

152 → 9

274 → 11

274 → 9

15 → 25

211 → 9

260 → 181

260 → 33

18 → 10

18 → 33

227 → 51

227 → 103

227 → 33

41 → 16

41 → 3

5 → 153

5 → 25

59 → 128

59 → 9

1 → 33

8 → 10

8 → 33

79 → 3

91 → 9

308 → 70

308 → 49

180 → 181

180 → 33

244 → 3

114 → 10

114 → 33

12 → 92

12 → 25

140 → 127

69 → 153

69 → 25

126 → 181

126 → 33

48 → 92

48 → 25

48 → 34

195 → 19

195 → 9

24 → 3

166 → 212

166 → 25

163 → 351

327 → 328

327 → 49

291 → 3

355 → 212

4₁(353) → 354

4₁(352) → 353

4₀(51) → 52

4₀(130) → 131

4₀(65) → 66

4₀(53) → 54

4₀(169) → 170

4₀(292) → 293

4₀(310) → 311

4₀(127) → 128

4₀(252) → 253

4₀(112) → 113

4₀(3) → 6

4₀(251) → 252

4₀(44) → 45

4₀(125) → 114

4₀(267) → 268

4₀(58) → 48

4₀(268) → 269

4₀(87) → 88

4₀(286) → 287

4₀(285) → 286

4₀(159) → 160

4₀(288) → 289

4₀(238) → 239

4₀(170) → 171

4₀(272) → 273

4₀(311) → 312

4₀(324) → 325

4₀(68) → 59

4₀(332) → 333

4₀(9) → 19

4₀(289) → 290

4₀(83) → 84

4₀(201) → 202

4₀(27) → 28

4₀(6) → 7

4₀(287) → 288

4₀(145) → 146

4₀(84) → 85

4₀(204) → 205

4₀(230) → 231

4₀(320) → 321

4₀(101) → 91

4₀(39) → 40

4₀(149) → 150

4₀(76) → 77

4₀(281) → 282

4₀(13) → 14

4₀(81) → 82

4₀(107) → 108

4₀(10) → 11

4₀(318) → 319

4₀(117) → 118

4₀(265) → 266

4₀(122) → 123

4₀(2) → 9

4₀(298) → 299

4₀(178) → 179

4₀(242) → 243

4₀(176) → 177

4₀(192) → 193

4₀(282) → 283

4₀(156) → 157

4₀(226) → 211

4₀(103) → 141

4₀(38) → 39

4₀(255) → 256

4₀(218) → 219

1₀(228) → 229

1₀(2) → 33

1₀(31) → 24

1₀(175) → 176

1₀(338) → 339

1₀(74) → 75

1₀(205) → 206

1₀(129) → 130

1₀(193) → 194

1₀(297) → 298

1₀(266) → 267

1₀(50) → 51

1₀(309) → 310

1₀(173) → 174

1₀(77) → 78

1₀(80) → 81

1₀(283) → 284

1₀(224) → 225

1₀(100) → 101

1₀(232) → 233

1₀(150) → 151

1₀(317) → 318

1₀(185) → 186

1₀(190) → 191

1₀(123) → 124

1₀(60) → 61

1₀(61) → 62

1₀(191) → 192

1₀(333) → 334

1₀(270) → 271

1₀(334) → 335

1₀(321) → 322

1₀(296) → 297

1₀(9) → 10

1₀(277) → 278

1₀(183) → 184

1₀(163) → 164

1₀(139) → 126

1₀(148) → 149

1₀(90) → 79

1₀(216) → 217

1₀(49) → 103

1₀(271) → 272

1₀(10) → 13

1₀(127) → 181

1₀(341) → 342

1₀(196) → 197

1₀(30) → 31

1₀(246) → 247

1₀(153) → 154

1₀(294) → 295

3₀(106) → 107

3₀(280) → 281

3₀(225) → 226

3₀(239) → 240

3₀(165) → 152

3₀(42) → 261

3₀(63) → 64

3₀(250) → 251

3₀(144) → 145

3₀(147) → 148

3₀(19) → 309

3₀(86) → 87

3₀(278) → 279

3₀(293) → 294

3₀(136) → 137

3₀(174) → 175

3₀(45) → 46

3₀(11) → 8

3₀(6) → 292

3₀(220) → 221

3₀(307) → 291

3₀(134) → 135

3₀(247) → 248

3₀(213) → 214

3₀(342) → 343

3₀(155) → 156

3₀(314) → 315

3₀(92) → 93

3₀(131) → 132

3₀(56) → 57

3₀(222) → 223

3₀(82) → 83

3₀(3) → 4

3₀(47) → 41

3₀(243) → 227

3₀(40) → 32

3₀(104) → 105

3₀(264) → 265

3₀(154) → 155

3₀(345) → 327

3₀(9) → 16

3₀(25) → 26

3₀(96) → 97

3₀(304) → 305

3₀(161) → 162

3₀(146) → 147

3₀(94) → 95

3₀(189) → 190

3₀(215) → 216

3₀(328) → 329

3₀(135) → 136

3₀(181) → 182

3₀(71) → 72

3₀(119) → 120

3₀(336) → 337

3₀(93) → 275

3₀(2) → 3

3₀(302) → 303

3₀(256) → 257

3₀(141) → 142

3₀(214) → 215

3₀(153) → 196

3₀(237) → 238

5₀(29) → 30

5₀(299) → 300

5₀(143) → 144

5₀(97) → 98

5₀(120) → 121

5₀(99) → 100

5₀(223) → 224

5₀(279) → 280

5₀(151) → 140

5₀(203) → 204

5₀(335) → 336

5₀(263) → 264

5₀(124) → 125

5₀(269) → 270

5₀(202) → 203

5₀(241) → 242

5₀(157) → 158

5₀(54) → 55

5₀(28) → 29

5₀(6) → 115

5₀(339) → 340

5₀(20) → 21

5₀(167) → 168

5₀(248) → 249

5₀(209) → 210

5₀(235) → 236

5₀(249) → 250

5₀(14) → 12

5₀(16) → 17

5₀(3) → 228

5₀(240) → 241

5₀(70) → 71

5₀(62) → 63

5₀(137) → 138

5₀(158) → 159

5₀(219) → 220

5₀(110) → 111

5₀(138) → 139

5₀(109) → 110

5₀(64) → 65

5₀(300) → 301

5₀(212) → 213

5₀(313) → 314

5₀(315) → 316

5₀(188) → 189

5₀(325) → 326

5₀(187) → 188

5₀(245) → 246

5₀(2) → 127

5₀(221) → 222

0₀(340) → 341

0₀(184) → 185

0₀(337) → 338

0₀(121) → 122

0₀(236) → 237

0₀(275) → 276

0₀(261) → 262

0₀(331) → 332

0₀(290) → 274

0₀(229) → 230

0₀(305) → 306

0₀(197) → 198

0₀(312) → 313

0₀(128) → 129

0₀(273) → 260

0₀(21) → 22

0₀(118) → 119

0₀(253) → 254

0₀(19) → 245

0₀(322) → 323

0₀(258) → 259

0₀(73) → 74

0₀(295) → 296

0₀(9) → 60

0₀(194) → 180

0₀(199) → 200

0₀(42) → 43

0₀(206) → 207

0₀(6) → 167

0₀(186) → 187

0₀(127) → 328

0₀(49) → 50

0₀(171) → 172

0₀(177) → 178

0₀(113) → 102

0₀(2) → 49

0₀(3) → 70

0₀(26) → 27

0₀(36) → 37

0₀(75) → 76

0₀(142) → 143

0₀(231) → 232

0₀(168) → 169

0₀(116) → 117

0₀(103) → 104

0₀(210) → 195

0₀(52) → 53

0₀(326) → 308

0₀(108) → 109

0₀(259) → 244

0₀(115) → 116

0₀(33) → 80

0₀(207) → 208

0₀(254) → 255

0₀(57) → 58

0₀(160) → 161

0₀(257) → 258

f6₀ → 2

2₀(2) → 25

2₀(344) → 345

2₀(330) → 331

2₀(46) → 47

2₀(329) → 330

2₀(9) → 212

2₀(306) → 307

2₀(133) → 134

2₀(105) → 106

2₀(98) → 99

2₀(95) → 96

2₀(67) → 68

2₀(19) → 20

2₀(303) → 304

2₀(323) → 324

2₀(55) → 56

2₀(25) → 92

2₀(217) → 218

2₀(43) → 44

2₀(4) → 1

2₀(233) → 234

2₀(37) → 38

2₀(234) → 235

2₀(89) → 90

2₀(3) → 153

2₀(164) → 165

2₀(17) → 15

2₀(284) → 285

2₀(66) → 67

2₀(198) → 199

2₀(23) → 18

2₀(132) → 133

2₀(316) → 317

2₀(262) → 263

2₀(111) → 112

2₀(208) → 209

2₀(7) → 5

2₀(33) → 34

2₀(35) → 36

2₀(93) → 94

2₀(22) → 23

2₀(172) → 173

2₀(85) → 86

2₀(319) → 320

2₀(276) → 277

2₀(162) → 163

2₀(343) → 344

2₀(34) → 35

2₀(78) → 69

2₀(16) → 42

2₀(179) → 166

2₀(200) → 201

2₀(88) → 89

2₀(72) → 73

2₀(301) → 302

2₀(182) → 183

3₁(351) → 352

2₁(354) → 355

102	→	19
102	→	9
32	→	33
152	→	6
152	→	9
274	→	11
274	→	9
15	→	25
211	→	9
260	→	181
260	→	33
18	→	10
18	→	33
227	→	51
227	→	103
227	→	33
41	→	16
41	→	3
5	→	153
5	→	25
59	→	128
59	→	9
1	→	33
8	→	10
8	→	33
79	→	3
91	→	9
308	→	70
308	→	49
180	→	181
180	→	33
244	→	3
114	→	10
114	→	33
12	→	92
12	→	25
140	→	127
69	→	153
69	→	25
126	→	181
126	→	33
48	→	92
48	→	25
48	→	34
195	→	19
195	→	9
24	→	3
166	→	212
166	→	25
163	→	351
327	→	328
327	→	49
291	→	3
355	→	212
4₁(353)	→	354
4₁(352)	→	353
4₀(51)	→	52
4₀(130)	→	131
4₀(65)	→	66
4₀(53)	→	54
4₀(169)	→	170
4₀(292)	→	293
4₀(310)	→	311
4₀(127)	→	128
4₀(252)	→	253
4₀(112)	→	113
4₀(3)	→	6
4₀(251)	→	252
4₀(44)	→	45
4₀(125)	→	114
4₀(267)	→	268
4₀(58)	→	48
4₀(268)	→	269
4₀(87)	→	88
4₀(286)	→	287
4₀(285)	→	286
4₀(159)	→	160
4₀(288)	→	289
4₀(238)	→	239
4₀(170)	→	171
4₀(272)	→	273
4₀(311)	→	312
4₀(324)	→	325
4₀(68)	→	59
4₀(332)	→	333
4₀(9)	→	19
4₀(289)	→	290
4₀(83)	→	84
4₀(201)	→	202
4₀(27)	→	28
4₀(6)	→	7
4₀(287)	→	288
4₀(145)	→	146
4₀(84)	→	85
4₀(204)	→	205
4₀(230)	→	231
4₀(320)	→	321
4₀(101)	→	91
4₀(39)	→	40
4₀(149)	→	150
4₀(76)	→	77
4₀(281)	→	282
4₀(13)	→	14
4₀(81)	→	82
4₀(107)	→	108
4₀(10)	→	11
4₀(318)	→	319
4₀(117)	→	118
4₀(265)	→	266
4₀(122)	→	123
4₀(2)	→	9
4₀(298)	→	299
4₀(178)	→	179
4₀(242)	→	243
4₀(176)	→	177
4₀(192)	→	193
4₀(282)	→	283
4₀(156)	→	157
4₀(226)	→	211
4₀(103)	→	141
4₀(38)	→	39
4₀(255)	→	256
4₀(218)	→	219
1₀(228)	→	229
1₀(2)	→	33
1₀(31)	→	24
1₀(175)	→	176
1₀(338)	→	339
1₀(74)	→	75
1₀(205)	→	206
1₀(129)	→	130
1₀(193)	→	194
1₀(297)	→	298
1₀(266)	→	267
1₀(50)	→	51
1₀(309)	→	310
1₀(173)	→	174
1₀(77)	→	78
1₀(80)	→	81
1₀(283)	→	284
1₀(224)	→	225
1₀(100)	→	101
1₀(232)	→	233
1₀(150)	→	151
1₀(317)	→	318
1₀(185)	→	186
1₀(190)	→	191
1₀(123)	→	124
1₀(60)	→	61
1₀(61)	→	62
1₀(191)	→	192
1₀(333)	→	334
1₀(270)	→	271
1₀(334)	→	335
1₀(321)	→	322
1₀(296)	→	297
1₀(9)	→	10
1₀(277)	→	278
1₀(183)	→	184
1₀(163)	→	164
1₀(139)	→	126
1₀(148)	→	149
1₀(90)	→	79
1₀(216)	→	217
1₀(49)	→	103
1₀(271)	→	272
1₀(10)	→	13
1₀(127)	→	181
1₀(341)	→	342
1₀(196)	→	197
1₀(30)	→	31
1₀(246)	→	247
1₀(153)	→	154
1₀(294)	→	295
3₀(106)	→	107
3₀(280)	→	281
3₀(225)	→	226
3₀(239)	→	240
3₀(165)	→	152
3₀(42)	→	261
3₀(63)	→	64
3₀(250)	→	251
3₀(144)	→	145
3₀(147)	→	148
3₀(19)	→	309
3₀(86)	→	87
3₀(278)	→	279
3₀(293)	→	294
3₀(136)	→	137
3₀(174)	→	175
3₀(45)	→	46
3₀(11)	→	8
3₀(6)	→	292
3₀(220)	→	221
3₀(307)	→	291
3₀(134)	→	135
3₀(247)	→	248
3₀(213)	→	214
3₀(342)	→	343
3₀(155)	→	156
3₀(314)	→	315
3₀(92)	→	93
3₀(131)	→	132
3₀(56)	→	57
3₀(222)	→	223
3₀(82)	→	83
3₀(3)	→	4
3₀(47)	→	41
3₀(243)	→	227
3₀(40)	→	32
3₀(104)	→	105
3₀(264)	→	265
3₀(154)	→	155
3₀(345)	→	327
3₀(9)	→	16
3₀(25)	→	26
3₀(96)	→	97
3₀(304)	→	305
3₀(161)	→	162
3₀(146)	→	147
3₀(94)	→	95
3₀(189)	→	190
3₀(215)	→	216
3₀(328)	→	329
3₀(135)	→	136
3₀(181)	→	182
3₀(71)	→	72
3₀(119)	→	120
3₀(336)	→	337
3₀(93)	→	275
3₀(2)	→	3
3₀(302)	→	303
3₀(256)	→	257
3₀(141)	→	142
3₀(214)	→	215
3₀(153)	→	196
3₀(237)	→	238
5₀(29)	→	30
5₀(299)	→	300
5₀(143)	→	144
5₀(97)	→	98
5₀(120)	→	121
5₀(99)	→	100
5₀(223)	→	224
5₀(279)	→	280
5₀(151)	→	140
5₀(203)	→	204
5₀(335)	→	336
5₀(263)	→	264
5₀(124)	→	125
5₀(269)	→	270
5₀(202)	→	203
5₀(241)	→	242
5₀(157)	→	158
5₀(54)	→	55
5₀(28)	→	29
5₀(6)	→	115
5₀(339)	→	340
5₀(20)	→	21
5₀(167)	→	168
5₀(248)	→	249
5₀(209)	→	210
5₀(235)	→	236
5₀(249)	→	250
5₀(14)	→	12
5₀(16)	→	17
5₀(3)	→	228
5₀(240)	→	241
5₀(70)	→	71
5₀(62)	→	63
5₀(137)	→	138
5₀(158)	→	159
5₀(219)	→	220
5₀(110)	→	111
5₀(138)	→	139
5₀(109)	→	110
5₀(64)	→	65
5₀(300)	→	301
5₀(212)	→	213
5₀(313)	→	314
5₀(315)	→	316
5₀(188)	→	189
5₀(325)	→	326
5₀(187)	→	188
5₀(245)	→	246
5₀(2)	→	127
5₀(221)	→	222
0₀(340)	→	341
0₀(184)	→	185
0₀(337)	→	338
0₀(121)	→	122
0₀(236)	→	237
0₀(275)	→	276
0₀(261)	→	262
0₀(331)	→	332
0₀(290)	→	274
0₀(229)	→	230
0₀(305)	→	306
0₀(197)	→	198
0₀(312)	→	313
0₀(128)	→	129
0₀(273)	→	260
0₀(21)	→	22
0₀(118)	→	119
0₀(253)	→	254
0₀(19)	→	245
0₀(322)	→	323
0₀(258)	→	259
0₀(73)	→	74
0₀(295)	→	296
0₀(9)	→	60
0₀(194)	→	180
0₀(199)	→	200
0₀(42)	→	43
0₀(206)	→	207
0₀(6)	→	167
0₀(186)	→	187
0₀(127)	→	328
0₀(49)	→	50
0₀(171)	→	172
0₀(177)	→	178
0₀(113)	→	102
0₀(2)	→	49
0₀(3)	→	70
0₀(26)	→	27
0₀(36)	→	37
0₀(75)	→	76
0₀(142)	→	143
0₀(231)	→	232
0₀(168)	→	169
0₀(116)	→	117
0₀(103)	→	104
0₀(210)	→	195
0₀(52)	→	53
0₀(326)	→	308
0₀(108)	→	109
0₀(259)	→	244
0₀(115)	→	116
0₀(33)	→	80
0₀(207)	→	208
0₀(254)	→	255
0₀(57)	→	58
0₀(160)	→	161
0₀(257)	→	258
f6₀	→	2
2₀(2)	→	25
2₀(344)	→	345
2₀(330)	→	331
2₀(46)	→	47
2₀(329)	→	330
2₀(9)	→	212
2₀(306)	→	307
2₀(133)	→	134
2₀(105)	→	106
2₀(98)	→	99
2₀(95)	→	96
2₀(67)	→	68
2₀(19)	→	20
2₀(303)	→	304
2₀(323)	→	324
2₀(55)	→	56
2₀(25)	→	92
2₀(217)	→	218
2₀(43)	→	44
2₀(4)	→	1
2₀(233)	→	234
2₀(37)	→	38
2₀(234)	→	235
2₀(89)	→	90
2₀(3)	→	153
2₀(164)	→	165
2₀(17)	→	15
2₀(284)	→	285
2₀(66)	→	67
2₀(198)	→	199
2₀(23)	→	18
2₀(132)	→	133
2₀(316)	→	317
2₀(262)	→	263
2₀(111)	→	112
2₀(208)	→	209
2₀(7)	→	5
2₀(33)	→	34
2₀(35)	→	36
2₀(93)	→	94
2₀(22)	→	23
2₀(172)	→	173
2₀(85)	→	86
2₀(319)	→	320
2₀(276)	→	277
2₀(162)	→	163
2₀(343)	→	344
2₀(34)	→	35
2₀(78)	→	69
2₀(16)	→	42
2₀(179)	→	166
2₀(200)	→	201
2₀(88)	→	89
2₀(72)	→	73
2₀(301)	→	302
2₀(182)	→	183
3₁(351)	→	352
2₁(354)	→	355