YES Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

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

Proof

1 String Reversal

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

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

1.1 Bounds

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

final states:

{257, 256, 253, 249, 247, 245, 242, 240, 238, 235, 232, 227, 224, 223, 220, 217, 215, 211, 208, 205, 202, 197, 192, 190, 185, 182, 179, 175, 171, 168, 164, 163, 162, 160, 157, 151, 149, 147, 142, 140, 138, 136, 132, 129, 125, 121, 117, 113, 108, 104, 102, 98, 94, 90, 85, 82, 77, 73, 72, 71, 70, 65, 62, 57, 51, 46, 44, 39, 36, 31, 30, 26, 23, 18, 12, 7, 1}

transitions:

223 → 32

33 → 32

157 → 86

157 → 152

23 → 152

102 → 32

205 → 32

202 → 32

98 → 32

51 → 32

289 → 194

129 → 186

129 → 13

136 → 66

136 → 32

149 → 32

211 → 152

145 → 284

18 → 152

18 → 143

227 → 32

39 → 32

57 → 32

108 → 32

9 → 260

147 → 32

65 → 32

185 → 32

175 → 32

90 → 66

90 → 32

224 → 32

62 → 32

31 → 32

1 → 152

197 → 32

44 → 32

73 → 32

179 → 32

26 → 152

261 → 278

125 → 40

125 → 32

235 → 32

253 → 32

36 → 32

208 → 32

72 → 32

138 → 66

138 → 32

257 → 32

121 → 228

121 → 13

171 → 228

171 → 13

220 → 32

249 → 32

283 → 186

82 → 32

117 → 32

265 → 136

232 → 86

232 → 152

12 → 152

85 → 186

85 → 13

77 → 32

104 → 32

140 → 143

140 → 152

7 → 152

217 → 32

113 → 32

182 → 32

30 → 32

46 → 32

162 → 228

162 → 13

240 → 32

256 → 32

245 → 32

160 → 32

190 → 32

164 → 32

168 → 32

242 → 32

215 → 32

132 → 186

132 → 13

142 → 143

142 → 152

70 → 32

163 → 32

151 → 32

94 → 32

192 → 32

238 → 32

247 → 32

4₁(263) → 264

4₁(279) → 280

4₁(287) → 288

0₁(281) → 282

0₁(260) → 261

0₁(284) → 285

2₁(278) → 279

3₁(282) → 283

3₁(285) → 286

3₁(261) → 262

1₀(74) → 75

1₀(130) → 131

1₀(35) → 31

1₀(67) → 68

1₀(53) → 54

1₀(19) → 20

1₀(169) → 170

1₀(183) → 216

1₀(78) → 79

1₀(127) → 128

1₀(200) → 201

1₀(146) → 142

1₀(49) → 50

1₀(37) → 38

1₀(144) → 145

1₀(41) → 42

1₀(252) → 249

1₀(112) → 108

1₀(95) → 96

1₀(33) → 34

1₀(231) → 227

1₀(58) → 59

1₀(24) → 25

1₀(184) → 182

1₀(21) → 22

1₀(150) → 149

1₀(93) → 90

1₀(8) → 9

1₀(87) → 88

1₀(133) → 134

1₀(155) → 156

1₀(56) → 51

1₀(64) → 62

1₀(237) → 235

1₀(118) → 158

1₀(83) → 84

1₀(27) → 28

1₀(6) → 45

1₀(60) → 61

1₀(119) → 120

1₀(109) → 176

1₀(187) → 188

1₀(148) → 147

1₀(15) → 16

1₀(196) → 192

1₀(13) → 14

1₀(81) → 77

1₀(10) → 11

1₀(4) → 5

1₀(181) → 179

1₀(43) → 39

1₀(139) → 138

1₀(2) → 3

1₀(213) → 214

1₀(69) → 65

1₀(153) → 154

0₀(20) → 37

0₀(2) → 13

0₀(78) → 95

0₀(255) → 253

0₀(155) → 241

0₀(124) → 121

0₀(152) → 186

0₀(201) → 197

0₀(19) → 118

0₀(48) → 49

0₀(88) → 89

0₀(32) → 228

0₀(42) → 43

0₀(28) → 29

0₀(209) → 210

0₀(4) → 165

0₀(59) → 60

0₀(34) → 35

0₀(174) → 171

0₀(80) → 81

0₀(243) → 244

0₀(8) → 99

0₀(258) → 259

0₀(123) → 124

0₀(141) → 140

0₀(126) → 127

0₀(135) → 132

0₀(172) → 173

0₀(9) → 10

0₀(68) → 69

0₀(195) → 196

0₀(27) → 206

0₀(154) → 155

0₀(134) → 135

0₀(13) → 109

0₀(118) → 119

0₀(63) → 64

0₀(131) → 129

0₀(84) → 82

0₀(221) → 222

0₀(145) → 146

0₀(226) → 224

0₀(3) → 4

0₀(52) → 53

0₀(75) → 76

0₀(246) → 245

0₀(122) → 123

3₀(114) → 233

3₀(106) → 107

3₀(177) → 178

3₀(100) → 101

3₀(218) → 239

3₀(42) → 148

3₀(30) → 70

3₀(86) → 212

3₀(166) → 167

3₀(173) → 174

3₀(35) → 139

3₀(210) → 208

3₀(34) → 83

3₀(11) → 137

3₀(99) → 105

3₀(43) → 162

3₀(152) → 193

3₀(194) → 195

3₀(228) → 229

3₀(172) → 180

3₀(97) → 94

3₀(154) → 243

3₀(9) → 27

3₀(191) → 190

3₀(204) → 202

3₀(13) → 91

3₀(5) → 6

3₀(10) → 24

3₀(2) → 52

3₀(188) → 189

3₀(198) → 199

3₀(16) → 17

3₀(89) → 85

4₀(143) → 144

4₀(42) → 150

4₀(186) → 187

4₀(8) → 78

4₀(47) → 48

4₀(172) → 236

4₀(86) → 87

4₀(230) → 231

4₀(152) → 153

4₀(66) → 67

4₀(236) → 237

4₀(4) → 126

4₀(13) → 19

4₀(92) → 93

4₀(20) → 21

4₀(248) → 247

4₀(9) → 74

4₀(52) → 58

4₀(251) → 252

4₀(14) → 15

4₀(40) → 41

4₀(3) → 47

4₀(30) → 71

4₀(32) → 33

4₀(110) → 169

4₀(183) → 184

4₀(114) → 115

4₀(180) → 181

4₀(109) → 114

4₀(199) → 200

4₀(259) → 257

4₀(111) → 112

4₀(55) → 56

4₀(2) → 8

4₀(221) → 246

5₀(31) → 163

5₀(59) → 63

5₀(156) → 151

5₀(229) → 230

5₀(96) → 97

5₀(20) → 218

5₀(189) → 185

5₀(137) → 136

5₀(53) → 250

5₀(79) → 80

5₀(128) → 125

5₀(193) → 194

5₀(152) → 198

5₀(34) → 258

5₀(120) → 117

5₀(188) → 191

5₀(54) → 55

5₀(61) → 57

5₀(91) → 92

5₀(9) → 122

5₀(222) → 220

5₀(50) → 46

5₀(214) → 211

5₀(11) → 30

5₀(167) → 164

5₀(76) → 73

5₀(38) → 36

5₀(241) → 240

5₀(216) → 215

5₀(2) → 32

5₀(45) → 44

5₀(107) → 104

5₀(170) → 168

5₀(122) → 225

5₀(116) → 113

5₀(103) → 102

5₀(29) → 72

5₀(52) → 66

5₀(101) → 98

5₀(161) → 160

5₀(244) → 242

5₀(110) → 111

5₀(10) → 203

5₀(13) → 40

5₀(207) → 205

5₀(178) → 175

5₀(254) → 255

5₀(219) → 217

5₀(86) → 172

5₀(154) → 221

5₀(204) → 223

f6₀ → 2

2₀(2) → 152

2₀(250) → 251

2₀(28) → 141

2₀(9) → 133

2₀(105) → 106

2₀(95) → 103

2₀(99) → 100

2₀(225) → 226

2₀(55) → 248

2₀(239) → 238

2₀(25) → 23

2₀(92) → 183

2₀(159) → 157

2₀(8) → 143

2₀(233) → 234

2₀(234) → 232

2₀(206) → 207

2₀(17) → 12

2₀(11) → 7

2₀(6) → 1

2₀(218) → 219

2₀(176) → 177

2₀(203) → 204

2₀(29) → 26

2₀(27) → 254

2₀(165) → 166

2₀(22) → 18

2₀(20) → 130

2₀(97) → 256

2₀(212) → 213

2₀(16) → 161

2₀(109) → 110

2₀(13) → 86

2₀(158) → 159

2₀(115) → 116

2₀(122) → 209

5₁(286) → 287

5₁(262) → 263

1₁(264) → 265

1₁(288) → 289

1₁(280) → 281

223	→	32
33	→	32
157	→	86
157	→	152
23	→	152
102	→	32
205	→	32
202	→	32
98	→	32
51	→	32
289	→	194
129	→	186
129	→	13
136	→	66
136	→	32
149	→	32
211	→	152
145	→	284
18	→	152
18	→	143
227	→	32
39	→	32
57	→	32
108	→	32
9	→	260
147	→	32
65	→	32
185	→	32
175	→	32
90	→	66
90	→	32
224	→	32
62	→	32
31	→	32
1	→	152
197	→	32
44	→	32
73	→	32
179	→	32
26	→	152
261	→	278
125	→	40
125	→	32
235	→	32
253	→	32
36	→	32
208	→	32
72	→	32
138	→	66
138	→	32
257	→	32
121	→	228
121	→	13
171	→	228
171	→	13
220	→	32
249	→	32
283	→	186
82	→	32
117	→	32
265	→	136
232	→	86
232	→	152
12	→	152
85	→	186
85	→	13
77	→	32
104	→	32
140	→	143
140	→	152
7	→	152
217	→	32
113	→	32
182	→	32
30	→	32
46	→	32
162	→	228
162	→	13
240	→	32
256	→	32
245	→	32
160	→	32
190	→	32
164	→	32
168	→	32
242	→	32
215	→	32
132	→	186
132	→	13
142	→	143
142	→	152
70	→	32
163	→	32
151	→	32
94	→	32
192	→	32
238	→	32
247	→	32
4₁(263)	→	264
4₁(279)	→	280
4₁(287)	→	288
0₁(281)	→	282
0₁(260)	→	261
0₁(284)	→	285
2₁(278)	→	279
3₁(282)	→	283
3₁(285)	→	286
3₁(261)	→	262
1₀(74)	→	75
1₀(130)	→	131
1₀(35)	→	31
1₀(67)	→	68
1₀(53)	→	54
1₀(19)	→	20
1₀(169)	→	170
1₀(183)	→	216
1₀(78)	→	79
1₀(127)	→	128
1₀(200)	→	201
1₀(146)	→	142
1₀(49)	→	50
1₀(37)	→	38
1₀(144)	→	145
1₀(41)	→	42
1₀(252)	→	249
1₀(112)	→	108
1₀(95)	→	96
1₀(33)	→	34
1₀(231)	→	227
1₀(58)	→	59
1₀(24)	→	25
1₀(184)	→	182
1₀(21)	→	22
1₀(150)	→	149
1₀(93)	→	90
1₀(8)	→	9
1₀(87)	→	88
1₀(133)	→	134
1₀(155)	→	156
1₀(56)	→	51
1₀(64)	→	62
1₀(237)	→	235
1₀(118)	→	158
1₀(83)	→	84
1₀(27)	→	28
1₀(6)	→	45
1₀(60)	→	61
1₀(119)	→	120
1₀(109)	→	176
1₀(187)	→	188
1₀(148)	→	147
1₀(15)	→	16
1₀(196)	→	192
1₀(13)	→	14
1₀(81)	→	77
1₀(10)	→	11
1₀(4)	→	5
1₀(181)	→	179
1₀(43)	→	39
1₀(139)	→	138
1₀(2)	→	3
1₀(213)	→	214
1₀(69)	→	65
1₀(153)	→	154
0₀(20)	→	37
0₀(2)	→	13
0₀(78)	→	95
0₀(255)	→	253
0₀(155)	→	241
0₀(124)	→	121
0₀(152)	→	186
0₀(201)	→	197
0₀(19)	→	118
0₀(48)	→	49
0₀(88)	→	89
0₀(32)	→	228
0₀(42)	→	43
0₀(28)	→	29
0₀(209)	→	210
0₀(4)	→	165
0₀(59)	→	60
0₀(34)	→	35
0₀(174)	→	171
0₀(80)	→	81
0₀(243)	→	244
0₀(8)	→	99
0₀(258)	→	259
0₀(123)	→	124
0₀(141)	→	140
0₀(126)	→	127
0₀(135)	→	132
0₀(172)	→	173
0₀(9)	→	10
0₀(68)	→	69
0₀(195)	→	196
0₀(27)	→	206
0₀(154)	→	155
0₀(134)	→	135
0₀(13)	→	109
0₀(118)	→	119
0₀(63)	→	64
0₀(131)	→	129
0₀(84)	→	82
0₀(221)	→	222
0₀(145)	→	146
0₀(226)	→	224
0₀(3)	→	4
0₀(52)	→	53
0₀(75)	→	76
0₀(246)	→	245
0₀(122)	→	123
3₀(114)	→	233
3₀(106)	→	107
3₀(177)	→	178
3₀(100)	→	101
3₀(218)	→	239
3₀(42)	→	148
3₀(30)	→	70
3₀(86)	→	212
3₀(166)	→	167
3₀(173)	→	174
3₀(35)	→	139
3₀(210)	→	208
3₀(34)	→	83
3₀(11)	→	137
3₀(99)	→	105
3₀(43)	→	162
3₀(152)	→	193
3₀(194)	→	195
3₀(228)	→	229
3₀(172)	→	180
3₀(97)	→	94
3₀(154)	→	243
3₀(9)	→	27
3₀(191)	→	190
3₀(204)	→	202
3₀(13)	→	91
3₀(5)	→	6
3₀(10)	→	24
3₀(2)	→	52
3₀(188)	→	189
3₀(198)	→	199
3₀(16)	→	17
3₀(89)	→	85
4₀(143)	→	144
4₀(42)	→	150
4₀(186)	→	187
4₀(8)	→	78
4₀(47)	→	48
4₀(172)	→	236
4₀(86)	→	87
4₀(230)	→	231
4₀(152)	→	153
4₀(66)	→	67
4₀(236)	→	237
4₀(4)	→	126
4₀(13)	→	19
4₀(92)	→	93
4₀(20)	→	21
4₀(248)	→	247
4₀(9)	→	74
4₀(52)	→	58
4₀(251)	→	252
4₀(14)	→	15
4₀(40)	→	41
4₀(3)	→	47
4₀(30)	→	71
4₀(32)	→	33
4₀(110)	→	169
4₀(183)	→	184
4₀(114)	→	115
4₀(180)	→	181
4₀(109)	→	114
4₀(199)	→	200
4₀(259)	→	257
4₀(111)	→	112
4₀(55)	→	56
4₀(2)	→	8
4₀(221)	→	246
5₀(31)	→	163
5₀(59)	→	63
5₀(156)	→	151
5₀(229)	→	230
5₀(96)	→	97
5₀(20)	→	218
5₀(189)	→	185
5₀(137)	→	136
5₀(53)	→	250
5₀(79)	→	80
5₀(128)	→	125
5₀(193)	→	194
5₀(152)	→	198
5₀(34)	→	258
5₀(120)	→	117
5₀(188)	→	191
5₀(54)	→	55
5₀(61)	→	57
5₀(91)	→	92
5₀(9)	→	122
5₀(222)	→	220
5₀(50)	→	46
5₀(214)	→	211
5₀(11)	→	30
5₀(167)	→	164
5₀(76)	→	73
5₀(38)	→	36
5₀(241)	→	240
5₀(216)	→	215
5₀(2)	→	32
5₀(45)	→	44
5₀(107)	→	104
5₀(170)	→	168
5₀(122)	→	225
5₀(116)	→	113
5₀(103)	→	102
5₀(29)	→	72
5₀(52)	→	66
5₀(101)	→	98
5₀(161)	→	160
5₀(244)	→	242
5₀(110)	→	111
5₀(10)	→	203
5₀(13)	→	40
5₀(207)	→	205
5₀(178)	→	175
5₀(254)	→	255
5₀(219)	→	217
5₀(86)	→	172
5₀(154)	→	221
5₀(204)	→	223
f6₀	→	2
2₀(2)	→	152
2₀(250)	→	251
2₀(28)	→	141
2₀(9)	→	133
2₀(105)	→	106
2₀(95)	→	103
2₀(99)	→	100
2₀(225)	→	226
2₀(55)	→	248
2₀(239)	→	238
2₀(25)	→	23
2₀(92)	→	183
2₀(159)	→	157
2₀(8)	→	143
2₀(233)	→	234
2₀(234)	→	232
2₀(206)	→	207
2₀(17)	→	12
2₀(11)	→	7
2₀(6)	→	1
2₀(218)	→	219
2₀(176)	→	177
2₀(203)	→	204
2₀(29)	→	26
2₀(27)	→	254
2₀(165)	→	166
2₀(22)	→	18
2₀(20)	→	130
2₀(97)	→	256
2₀(212)	→	213
2₀(16)	→	161
2₀(109)	→	110
2₀(13)	→	86
2₀(158)	→	159
2₀(115)	→	116
2₀(122)	→	209
5₁(286)	→	287
5₁(262)	→	263
1₁(264)	→	265
1₁(288)	→	289
1₁(280)	→	281