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

Proof

1 String Reversal

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

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

1.1 Bounds

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

final states:

{380, 364, 346, 328, 311, 293, 280, 262, 247, 230, 213, 197, 182, 167, 151, 137, 123, 108, 95, 84, 72, 60, 47, 35, 26, 19, 14, 9, 5, 1}

transitions:

364 → 15

364 → 3

429 → 279

280 → 61

401 → 216

84 → 61

167 → 6

276 → 426

213 → 62

213 → 36

108 → 16

108 → 73

108 → 61

9 → 62

9 → 36

5 → 61

95 → 61

20 → 398

293 → 153

293 → 400

293 → 4

293 → 36

380 → 61

1 → 62

1 → 36

123 → 6

60 → 10

197 → 294

197 → 3

26 → 36

72 → 7

72 → 20

346 → 11

346 → 61

311 → 6

173 → 414

230 → 21

230 → 36

14 → 36

417 → 176

182 → 125

182 → 73

182 → 61

137 → 124

137 → 3

35 → 125

35 → 73

35 → 61

47 → 6

154 → 410

413 → 157

19 → 233

19 → 3

328 → 61

151 → 61

262 → 61

247 → 36

3₁(410) → 411

3₁(398) → 399

3₁(426) → 427

3₁(414) → 415

4₀(383) → 384

4₀(355) → 356

4₀(130) → 131

4₀(180) → 181

4₀(53) → 54

4₀(11) → 12

4₀(310) → 293

4₀(127) → 128

4₀(73) → 74

4₀(92) → 93

4₀(162) → 163

4₀(300) → 301

4₀(317) → 318

4₀(270) → 271

4₀(37) → 38

4₀(41) → 42

4₀(252) → 253

4₀(193) → 194

4₀(359) → 360

4₀(3) → 109

4₀(333) → 334

4₀(271) → 272

4₀(44) → 45

4₀(240) → 241

4₀(354) → 355

4₀(129) → 130

4₀(319) → 320

4₀(207) → 208

4₀(373) → 374

4₀(307) → 308

4₀(58) → 59

4₀(273) → 274

4₀(61) → 231

4₀(93) → 94

4₀(8) → 5

4₀(256) → 257

4₀(52) → 53

4₀(362) → 363

4₀(228) → 229

4₀(347) → 348

4₀(388) → 389

4₀(133) → 134

4₀(296) → 297

4₀(381) → 382

4₀(199) → 200

4₀(332) → 333

4₀(59) → 47

4₀(70) → 71

4₀(179) → 180

4₀(302) → 303

4₀(336) → 337

4₀(287) → 288

4₀(94) → 84

4₀(145) → 146

4₀(110) → 111

4₀(62) → 63

4₀(71) → 60

4₀(322) → 323

4₀(148) → 149

4₀(101) → 102

4₀(42) → 43

4₀(126) → 127

4₀(97) → 98

4₀(107) → 95

4₀(10) → 347

4₀(63) → 64

4₀(202) → 203

4₀(28) → 29

4₀(340) → 341

4₀(259) → 260

4₀(116) → 117

4₀(2) → 10

4₀(360) → 361

4₀(263) → 264

4₀(363) → 346

4₀(242) → 243

4₀(375) → 376

4₀(147) → 148

4₀(351) → 352

4₀(85) → 86

4₀(385) → 386

4₀(54) → 55

4₀(393) → 394

4₀(38) → 39

4₀(389) → 390

4₀(243) → 244

4₀(153) → 154

4₀(370) → 371

5₀(284) → 285

5₀(20) → 138

5₀(109) → 110

5₀(357) → 358

5₀(2) → 20

5₀(339) → 340

5₀(31) → 32

5₀(45) → 46

5₀(21) → 22

5₀(160) → 161

5₀(6) → 7

5₀(16) → 17

5₀(32) → 33

5₀(348) → 349

5₀(50) → 51

5₀(291) → 292

5₀(192) → 193

5₀(371) → 372

5₀(112) → 113

5₀(77) → 78

5₀(369) → 370

5₀(222) → 223

5₀(379) → 364

5₀(233) → 234

5₀(267) → 268

5₀(378) → 379

5₀(12) → 13

5₀(114) → 115

5₀(303) → 304

5₀(374) → 375

5₀(187) → 188

5₀(106) → 107

5₀(210) → 211

5₀(11) → 27

5₀(135) → 136

5₀(172) → 173

5₀(298) → 299

5₀(324) → 325

5₀(99) → 100

5₀(356) → 357

5₀(143) → 144

5₀(347) → 381

5₀(183) → 184

5₀(305) → 306

5₀(217) → 218

5₀(367) → 368

5₀(170) → 171

5₀(285) → 286

5₀(67) → 68

5₀(184) → 185

5₀(313) → 314

5₀(306) → 307

5₀(330) → 331

5₀(121) → 122

5₀(372) → 373

5₀(189) → 190

5₀(349) → 350

5₀(43) → 44

5₀(104) → 105

5₀(40) → 41

5₀(272) → 273

5₀(22) → 23

5₀(343) → 344

3₀(226) → 227

3₀(227) → 228

3₀(150) → 137

3₀(216) → 217

3₀(212) → 197

3₀(142) → 143

3₀(7) → 8

3₀(136) → 123

3₀(6) → 294

3₀(220) → 221

3₀(203) → 204

3₀(120) → 121

3₀(323) → 324

3₀(312) → 313

3₀(46) → 35

3₀(90) → 91

3₀(268) → 269

3₀(75) → 76

3₀(195) → 196

3₀(87) → 88

3₀(3) → 124

3₀(139) → 140

3₀(140) → 141

3₀(345) → 328

3₀(111) → 112

3₀(57) → 58

3₀(387) → 388

3₀(25) → 19

3₀(232) → 233

3₀(304) → 305

3₀(161) → 162

3₀(146) → 147

3₀(80) → 81

3₀(224) → 225

3₀(15) → 183

3₀(337) → 338

3₀(49) → 50

3₀(20) → 152

3₀(13) → 9

3₀(117) → 118

3₀(297) → 298

3₀(48) → 49

3₀(103) → 104

3₀(10) → 15

3₀(2) → 3

3₀(141) → 142

3₀(188) → 189

3₀(138) → 139

3₀(211) → 212

3₀(171) → 172

3₀(66) → 67

3₀(89) → 90

3₀(186) → 187

0₀(286) → 287

0₀(301) → 302

0₀(29) → 30

0₀(238) → 239

0₀(341) → 342

0₀(283) → 284

0₀(191) → 192

0₀(201) → 202

0₀(318) → 319

0₀(327) → 311

0₀(223) → 224

0₀(279) → 262

0₀(342) → 343

0₀(344) → 345

0₀(164) → 165

0₀(391) → 392

0₀(122) → 108

0₀(98) → 99

0₀(208) → 209

0₀(169) → 170

0₀(27) → 28

0₀(96) → 97

0₀(241) → 242

0₀(157) → 158

0₀(196) → 182

0₀(236) → 237

0₀(365) → 366

0₀(56) → 57

0₀(239) → 240

0₀(234) → 235

0₀(118) → 119

0₀(39) → 40

0₀(10) → 48

0₀(20) → 214

0₀(181) → 167

0₀(276) → 277

0₀(15) → 198

0₀(149) → 150

0₀(154) → 155

0₀(30) → 31

0₀(338) → 339

0₀(329) → 330

0₀(308) → 309

0₀(190) → 191

0₀(292) → 280

0₀(176) → 177

0₀(173) → 174

0₀(254) → 255

0₀(185) → 186

0₀(250) → 251

0₀(85) → 365

0₀(79) → 80

0₀(33) → 34

0₀(23) → 24

0₀(55) → 56

0₀(105) → 106

0₀(2) → 6

0₀(258) → 259

0₀(221) → 222

0₀(225) → 226

1₀(64) → 65

1₀(376) → 377

1₀(48) → 85

1₀(275) → 276

1₀(261) → 247

1₀(331) → 332

1₀(290) → 291

1₀(366) → 367

1₀(353) → 354

1₀(65) → 66

1₀(321) → 322

1₀(266) → 267

1₀(335) → 336

1₀(88) → 89

1₀(155) → 156

1₀(200) → 201

1₀(352) → 353

1₀(128) → 129

1₀(152) → 329

1₀(68) → 69

1₀(394) → 395

1₀(361) → 362

1₀(205) → 206

1₀(253) → 254

1₀(139) → 281

1₀(125) → 126

1₀(277) → 278

1₀(214) → 215

1₀(206) → 207

1₀(325) → 326

1₀(119) → 120

1₀(76) → 77

1₀(74) → 75

1₀(386) → 387

1₀(218) → 219

1₀(113) → 114

1₀(281) → 282

1₀(174) → 175

1₀(2) → 61

1₀(163) → 164

1₀(3) → 73

1₀(316) → 317

1₀(392) → 393

1₀(37) → 263

1₀(124) → 125

1₀(168) → 169

1₀(255) → 256

1₀(326) → 327

1₀(78) → 79

1₀(282) → 283

1₀(288) → 289

1₀(244) → 245

1₀(10) → 11

1₀(115) → 116

1₀(134) → 135

1₀(102) → 103

1₀(17) → 18

1₀(178) → 179

1₀(289) → 290

1₀(15) → 16

1₀(315) → 316

1₀(100) → 101

1₀(204) → 205

1₀(377) → 378

1₀(81) → 82

1₀(159) → 160

1₀(246) → 230

1₀(257) → 258

1₀(397) → 380

f6₀ → 2

2₀(2) → 36

2₀(51) → 52

2₀(18) → 14

2₀(384) → 385

2₀(237) → 238

2₀(274) → 275

2₀(177) → 178

2₀(156) → 157

2₀(358) → 359

2₀(395) → 396

2₀(91) → 92

2₀(299) → 300

2₀(175) → 176

2₀(260) → 261

2₀(314) → 315

2₀(166) → 151

2₀(309) → 310

2₀(232) → 248

2₀(350) → 351

2₀(36) → 37

2₀(215) → 216

2₀(152) → 153

2₀(235) → 236

2₀(24) → 25

2₀(294) → 295

2₀(131) → 132

2₀(4) → 1

2₀(61) → 62

2₀(390) → 391

2₀(334) → 335

2₀(138) → 312

2₀(248) → 249

2₀(3) → 4

2₀(264) → 265

2₀(249) → 250

2₀(86) → 87

2₀(83) → 72

2₀(245) → 246

2₀(320) → 321

2₀(198) → 199

2₀(132) → 133

2₀(269) → 270

2₀(1) → 168

2₀(295) → 296

2₀(251) → 252

2₀(165) → 166

2₀(382) → 383

2₀(20) → 21

2₀(82) → 83

2₀(73) → 96

2₀(368) → 369

2₀(396) → 397

2₀(229) → 213

2₀(209) → 210

2₀(278) → 279

2₀(34) → 26

2₀(219) → 220

2₀(144) → 145

2₀(231) → 232

2₀(158) → 159

2₀(194) → 195

2₀(265) → 266

2₀(69) → 70

2₁(399) → 400

2₁(428) → 429

2₁(411) → 412

2₁(415) → 416

2₁(427) → 428

2₁(400) → 401

2₁(412) → 413

2₁(416) → 417

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