My attempts to solve puzzles of Advent of Code
Day 3
+1188
-1
+2
-1
2021/AoC.lean
+2
-1
2021/AoC.lean
+185
2021/AoC/Day3.lean
+185
2021/AoC/Day3.lean
···
1
+
namespace Day3
2
+
3
+
inductive Bit where
4
+
| zero
5
+
| one
6
+
deriving Repr, Inhabited, DecidableEq
7
+
8
+
namespace Bit
9
+
10
+
def bitToString : Bit -> String :=
11
+
fun b => match b with
12
+
| Bit.zero => "zero"
13
+
| Bit.one => "one"
14
+
15
+
instance : ToString Bit where
16
+
toString := bitToString
17
+
18
+
def fromChar (c: Char): OptionM Bit :=
19
+
match c with
20
+
| '0' => some Bit.zero
21
+
| '1' => some Bit.one
22
+
| _ => none
23
+
24
+
def toNat (b: Bit): Nat :=
25
+
match b with
26
+
| Bit.zero => 0
27
+
| Bit.one => 1
28
+
29
+
def parse (xs: String): Array Bit :=
30
+
xs.foldl (fun acc c => flip Option.getD acc <| Option.map acc.push <| fromChar c) #[]
31
+
32
+
def toDecimal : Array Bit -> Nat
33
+
| #[] => 1
34
+
| bs =>
35
+
bs.reverse.foldl
36
+
(fun acc b => (acc.fst + b.toNat * 2 ^ acc.snd, acc.snd + 1))
37
+
(0, 0) |>
38
+
Prod.fst
39
+
end Bit
40
+
41
+
structure BitCount where
42
+
zero : Nat
43
+
one: Nat
44
+
deriving Repr, Inhabited
45
+
46
+
namespace BitCount
47
+
48
+
def bitCountToString : BitCount -> String :=
49
+
fun bs => s!"\{zero:= {bs.zero}, one:= {bs.one}}"
50
+
51
+
instance : ToString BitCount where
52
+
toString := bitCountToString
53
+
54
+
def default : BitCount := { zero := 0, one := 0 }
55
+
56
+
def bitCountAdd (a: BitCount) (b: BitCount): BitCount :=
57
+
{ zero := a.zero + b.zero, one := a.one + b.one }
58
+
59
+
instance : Add BitCount where
60
+
add := bitCountAdd
61
+
62
+
def restArr (len: Nat) (idx: Nat): Array BitCount :=
63
+
if (len > idx) then
64
+
#[]
65
+
else
66
+
Array.mkArray (idx + 1 - len) BitCount.default
67
+
68
+
def update (bs: Array BitCount) (b: Bit) (idx: Nat): Array BitCount :=
69
+
let ys: BitCount × Array BitCount :=
70
+
bs.get? idx |>
71
+
Option.map (fun a => (a, bs)) |>
72
+
flip Option.getD (BitCount.default, bs.append <| restArr bs.size idx)
73
+
74
+
match b with
75
+
| Bit.zero => ys.snd.setD idx { ys.fst with zero := ys.fst.zero + 1 }
76
+
| Bit.one => ys.snd.setD idx { ys.fst with one := ys.fst.one + 1 }
77
+
78
+
79
+
def fromBits (xs: Array Bit): Array BitCount :=
80
+
xs.foldl (fun (acc, idx) b => (update acc b idx, idx + 1)) (#[], 0) |>
81
+
Prod.fst
82
+
83
+
def updateBitCount : BitCount -> Bit -> BitCount
84
+
| bc, Bit.zero => { bc with zero := bc.zero + 1 }
85
+
| bc, Bit.one => { bc with one := bc.one + 1 }
86
+
87
+
def fromBitsToBitCount (xs: Array Bit): BitCount :=
88
+
xs.foldl updateBitCount BitCount.default
89
+
90
+
def filterCommon : Nat -> BitCount -> (BitCount -> Bit) -> Array Bit -> Bool :=
91
+
fun idx b f xs =>
92
+
let x: OptionM Bool := do
93
+
let v <- xs.get? idx
94
+
if v = f b then true else none
95
+
96
+
x.getD false
97
+
98
+
def mostCommon : BitCount -> Bit := fun b => if b.one >= b.zero then Bit.one else Bit.zero
99
+
def leastCommon : BitCount -> Bit := fun b => if b.one >= b.zero then Bit.zero else Bit.one
100
+
101
+
def intermediateAcc : Array (Array Bit) × Array (Array Bit) -> Nat -> BitCount × BitCount :=
102
+
fun out index =>
103
+
(fromBitsToBitCount <| out.fst.map (·.get! index), fromBitsToBitCount <| out.snd.map (·.get! index))
104
+
105
+
def checkEmpty (xs: Array α) (ys: Array α): Array α :=
106
+
if (ys.size = 0) then xs else ys
107
+
108
+
def filterTuple : Array (Array Bit) × Array (Array Bit) -> Nat -> BitCount × BitCount -> Array (Array Bit) × Array (Array Bit) :=
109
+
fun out index acc =>
110
+
(
111
+
checkEmpty out.fst <| out.fst.filter (filterCommon index acc.fst mostCommon),
112
+
checkEmpty out.snd <| out.snd.filter (filterCommon index acc.snd leastCommon)
113
+
)
114
+
115
+
116
+
partial def update': Array (Array Bit) × Array (Array Bit) -> Array (Array Bit) × Array (Array Bit) :=
117
+
fun (xs, ys) => do
118
+
let rec loop (out: Array (Array Bit) × Array (Array Bit)) (acc: BitCount × BitCount) (index: Nat) :=
119
+
if (out.fst.size <= 1 && out.snd.size <= 1) || (index + 1 = (out.fst.get! 0).size) then
120
+
out
121
+
else
122
+
loop
123
+
(filterTuple out index acc)
124
+
(intermediateAcc (filterTuple out index acc) (index + 1))
125
+
(index + 1)
126
+
127
+
loop (xs, ys) (intermediateAcc (xs, ys) 0) 0
128
+
129
+
130
+
def fromBits' (xs: Array (Array Bit)): Array (Array Bit) × Array (Array Bit) :=
131
+
update' (xs, xs)
132
+
133
+
134
+
def merge (x: Array BitCount) (y: Array BitCount): Array BitCount :=
135
+
if x.size > 0
136
+
then
137
+
if y.size > 0 then
138
+
x.zipWith y Add.add
139
+
else
140
+
x
141
+
else
142
+
y
143
+
144
+
def mergeAll (xs: Array (Array BitCount)): Array BitCount :=
145
+
xs.foldl (fun acc ys => merge acc ys) #[]
146
+
147
+
def toGammaEpsilon (bc: BitCount): Bit × Bit :=
148
+
if bc.one > bc.zero then (Bit.one, Bit.zero) else (Bit.zero, Bit.one)
149
+
150
+
def toRates (bs: Array BitCount): (Array Bit × Array Bit) :=
151
+
bs.map toGammaEpsilon |>
152
+
Array.foldl
153
+
(fun (gs, es) (g, e) => (gs.push g, es.push e))
154
+
(#[] , #[])
155
+
156
+
end BitCount
157
+
158
+
159
+
160
+
def part1 (bs: Array (Array Bit)): Nat := do
161
+
bs.map BitCount.fromBits |>
162
+
BitCount.mergeAll |>
163
+
BitCount.toRates |>
164
+
Prod.map Bit.toDecimal Bit.toDecimal |>
165
+
fun (g, e) => g * e
166
+
167
+
168
+
def part2 (bs: Array (Array Bit)) :=
169
+
let (o2, co2) := Prod.map (Bit.toDecimal <| ·.get! 0) (Bit.toDecimal <| ·.get! 0) <| BitCount.fromBits' bs
170
+
o2 * co2
171
+
172
+
open IO.FS
173
+
174
+
def run : IO Unit := do
175
+
let day3 := "./data/day3.txt"
176
+
let readings <- lines day3
177
+
178
+
let bits := readings.map Bit.parse
179
+
180
+
let part1Result <- part1 bits
181
+
let part2Result <- part2 bits
182
+
183
+
IO.println <| ( part1Result, part2Result )
184
+
185
+
end Day3
+1
2021/Main.lean
+1
2021/Main.lean
+1000
2021/data/day3.txt
+1000
2021/data/day3.txt
···
1
+
110001010110
2
+
011101111101
3
+
111011110101
4
+
011110101000
5
+
100100011001
6
+
011001001110
7
+
101011000101
8
+
110000111111
9
+
110110101000
10
+
010101101000
11
+
001101001101
12
+
111000001011
13
+
111000011010
14
+
001111001000
15
+
100110001111
16
+
111100110100
17
+
100000010101
18
+
001110100000
19
+
100111110110
20
+
100110000110
21
+
111100101101
22
+
100101010100
23
+
011100010011
24
+
111010110000
25
+
110100011110
26
+
111010101100
27
+
111001001101
28
+
110001110100
29
+
100110111011
30
+
101111111011
31
+
011100111000
32
+
010011110010
33
+
111001011011
34
+
110100111000
35
+
111000011001
36
+
010100000000
37
+
100000101111
38
+
010100110010
39
+
110001101000
40
+
000101101001
41
+
001111101010
42
+
100100000001
43
+
101000111011
44
+
101110001111
45
+
000100011000
46
+
100110101110
47
+
111011101010
48
+
010110001101
49
+
110100001111
50
+
011110101100
51
+
101000011100
52
+
111101111101
53
+
110101010100
54
+
101100111111
55
+
111110110101
56
+
011011110111
57
+
101101000111
58
+
111101000011
59
+
001011110110
60
+
110011110111
61
+
000011101111
62
+
100001101010
63
+
111011101101
64
+
010110111000
65
+
110101111100
66
+
110010101000
67
+
001011001010
68
+
000110101001
69
+
000001000011
70
+
111100001010
71
+
100110111010
72
+
111011111000
73
+
011111101111
74
+
000010100111
75
+
111011011111
76
+
011101110010
77
+
000000100111
78
+
100111000100
79
+
000010010111
80
+
101111101011
81
+
011111000101
82
+
011100100101
83
+
011000111101
84
+
011110001010
85
+
100110101011
86
+
011011010011
87
+
011100000101
88
+
011110000100
89
+
000110110010
90
+
001101101110
91
+
110011000001
92
+
110100111110
93
+
110011000101
94
+
000101011110
95
+
001010000000
96
+
000011000010
97
+
110010111110
98
+
011111110110
99
+
100000110000
100
+
011101111000
101
+
100011100101
102
+
101000000101
103
+
001111010011
104
+
010110110011
105
+
000100100100
106
+
001010001001
107
+
010011100100
108
+
110101110011
109
+
001001000001
110
+
101110110010
111
+
001001000110
112
+
010010100000
113
+
000111101011
114
+
010010001000
115
+
011111000111
116
+
010011010001
117
+
110101101101
118
+
000110010101
119
+
111011110100
120
+
010000110101
121
+
110110101111
122
+
010110111101
123
+
100000010000
124
+
001010011111
125
+
111001001111
126
+
011110110111
127
+
101011000111
128
+
010100011110
129
+
111100100011
130
+
110100110110
131
+
001000011000
132
+
011011111101
133
+
111111110010
134
+
000011110010
135
+
110101111101
136
+
001011111101
137
+
000010011000
138
+
001111101101
139
+
100010010101
140
+
111101110001
141
+
011010110101
142
+
011000000110
143
+
111110100011
144
+
000010111001
145
+
101001111100
146
+
001011011010
147
+
100110111110
148
+
000111001010
149
+
001011101110
150
+
100010110110
151
+
001100110000
152
+
000110001010
153
+
100010001000
154
+
111110011110
155
+
110011111000
156
+
100011101110
157
+
001110100101
158
+
010110110000
159
+
101110101010
160
+
110111010111
161
+
110011000100
162
+
100110101100
163
+
101110100110
164
+
010101011101
165
+
100111100010
166
+
010110110010
167
+
000111100001
168
+
101001101001
169
+
011101110101
170
+
011111100111
171
+
000101010011
172
+
110111100010
173
+
011110000000
174
+
011101110110
175
+
110100110100
176
+
111110111001
177
+
000100000011
178
+
011110111011
179
+
011010100111
180
+
111100110111
181
+
100010011101
182
+
011001001111
183
+
001010101100
184
+
010110111010
185
+
111000110010
186
+
011011100111
187
+
101111000010
188
+
110011011100
189
+
110110011110
190
+
000101011100
191
+
100100110000
192
+
110000100011
193
+
011001101001
194
+
110000100010
195
+
001000000011
196
+
010110001100
197
+
111111000001
198
+
101111011100
199
+
100100100101
200
+
101010100110
201
+
011110000001
202
+
010100110110
203
+
010111011000
204
+
011110100010
205
+
101000110010
206
+
110001011011
207
+
111110011111
208
+
111100100110
209
+
111110101000
210
+
010001111101
211
+
111000101111
212
+
111001010110
213
+
101000001111
214
+
000100101001
215
+
011101011001
216
+
111101111100
217
+
010001100100
218
+
010111011100
219
+
100101010110
220
+
001010110010
221
+
010010111110
222
+
101110011100
223
+
111100101010
224
+
001001111111
225
+
011101010000
226
+
111011111101
227
+
011000001110
228
+
111100110010
229
+
001001111101
230
+
011100001110
231
+
001001001000
232
+
110011101111
233
+
010001011110
234
+
001100100100
235
+
011100110000
236
+
111100001110
237
+
111110110000
238
+
000011000011
239
+
011000000011
240
+
110010111111
241
+
011110001011
242
+
101110100010
243
+
100100111000
244
+
111101011010
245
+
000111110101
246
+
010100001001
247
+
110010101101
248
+
001101011111
249
+
000101100101
250
+
110011101100
251
+
110111111111
252
+
111000011000
253
+
010000100100
254
+
110101101011
255
+
101010101001
256
+
100111001101
257
+
111011000001
258
+
101101111010
259
+
111001111001
260
+
001001110100
261
+
000111110000
262
+
010111010110
263
+
100011010111
264
+
111011011101
265
+
100010100001
266
+
000111001110
267
+
111100010001
268
+
101001101101
269
+
111101100111
270
+
100110100010
271
+
000010100101
272
+
010010110111
273
+
101100000101
274
+
111011010110
275
+
101101101101
276
+
001110110111
277
+
110011011111
278
+
011111111001
279
+
100100001100
280
+
101010011101
281
+
100000110110
282
+
110101010000
283
+
110110110111
284
+
101001110110
285
+
100001000101
286
+
110100001001
287
+
000111000100
288
+
101000101001
289
+
111111001100
290
+
101011000100
291
+
111000010100
292
+
100111000110
293
+
111011010100
294
+
101101011101
295
+
010000101101
296
+
000110110110
297
+
001110000101
298
+
001010001000
299
+
100111101111
300
+
001011101001
301
+
001100111101
302
+
110111011111
303
+
111010011010
304
+
001110101111
305
+
101000001110
306
+
101001110001
307
+
110111010010
308
+
011111100101
309
+
110001001001
310
+
010010111010
311
+
000001001010
312
+
011000001100
313
+
100000111011
314
+
111000010101
315
+
001110011001
316
+
010001001100
317
+
001100010101
318
+
001011011000
319
+
001101100100
320
+
011001111111
321
+
010010001011
322
+
100010011111
323
+
100011000100
324
+
000110011110
325
+
010010000000
326
+
110110011001
327
+
111000111010
328
+
111010000111
329
+
111011110110
330
+
101101100111
331
+
111100101001
332
+
110001101110
333
+
111101100001
334
+
011111110111
335
+
110110101001
336
+
000111010101
337
+
101011111111
338
+
100110001000
339
+
101000100000
340
+
110101110010
341
+
010100011011
342
+
000000100101
343
+
000000011110
344
+
101011110000
345
+
101001100001
346
+
111010101101
347
+
000011011100
348
+
000000100010
349
+
001011100000
350
+
001110111111
351
+
110100111001
352
+
010110110111
353
+
010111111010
354
+
110100011010
355
+
000101011111
356
+
001000011100
357
+
010011001011
358
+
111011001100
359
+
101111001101
360
+
100010000001
361
+
011000001010
362
+
101010000011
363
+
110110010100
364
+
101001011101
365
+
100001010001
366
+
110011010101
367
+
000001100000
368
+
100101000101
369
+
110110100110
370
+
110001111010
371
+
111011101011
372
+
010010111101
373
+
000110100101
374
+
011110101110
375
+
000101110001
376
+
111111101100
377
+
011100110010
378
+
100011111010
379
+
010011111101
380
+
101000010101
381
+
011000101000
382
+
011111001111
383
+
111001111010
384
+
100000000100
385
+
010000101001
386
+
110000001000
387
+
100100001101
388
+
011001111010
389
+
110111110111
390
+
000011100111
391
+
001100110001
392
+
000111010001
393
+
101110011110
394
+
110010000010
395
+
101100001101
396
+
001000001100
397
+
101110011001
398
+
111000000110
399
+
000111111100
400
+
001110001110
401
+
100011110100
402
+
001011101100
403
+
011010010010
404
+
101000011111
405
+
110001011010
406
+
011001000000
407
+
010011110001
408
+
100001111011
409
+
011011001111
410
+
110100010011
411
+
010111010001
412
+
010101011011
413
+
100000001100
414
+
100111101010
415
+
100010100000
416
+
110000110001
417
+
010000010101
418
+
010101000010
419
+
010100101100
420
+
110101000001
421
+
100010010110
422
+
110011101011
423
+
010101011001
424
+
010001000011
425
+
000011111110
426
+
111110011101
427
+
011010010000
428
+
011011111100
429
+
110010110011
430
+
001101111011
431
+
000011111101
432
+
110000010110
433
+
111011011011
434
+
111110000000
435
+
101100111010
436
+
100110011111
437
+
110111011001
438
+
110110010010
439
+
010010011110
440
+
010110010101
441
+
101110000000
442
+
011001110110
443
+
100110100011
444
+
111101111010
445
+
110101010011
446
+
111110100010
447
+
100110001100
448
+
010010100010
449
+
101010100001
450
+
000000000101
451
+
111001011100
452
+
100100111110
453
+
000000011010
454
+
110011111101
455
+
010100000011
456
+
100001111111
457
+
110001011001
458
+
111111100011
459
+
111101110000
460
+
100011001101
461
+
110001010100
462
+
100110000111
463
+
111110110110
464
+
001011000011
465
+
111111000000
466
+
101011101101
467
+
110001111011
468
+
011111001000
469
+
000001011101
470
+
001101000011
471
+
001000010000
472
+
000011001110
473
+
011001101000
474
+
110101100101
475
+
001111110111
476
+
111110111101
477
+
000011000111
478
+
001010011100
479
+
110010010011
480
+
110001110111
481
+
111010010011
482
+
100010001110
483
+
110000101000
484
+
011001011000
485
+
011100100000
486
+
001000011001
487
+
101011110011
488
+
001010011110
489
+
110100000101
490
+
010011011110
491
+
011001100001
492
+
011110011010
493
+
100110000000
494
+
010110010100
495
+
000100111110
496
+
110101110101
497
+
000110111100
498
+
010000000111
499
+
111101010100
500
+
111011011100
501
+
000010000011
502
+
001100100001
503
+
110010110001
504
+
010010000010
505
+
001000010110
506
+
011001000001
507
+
010100101110
508
+
011100010100
509
+
100000011010
510
+
010111100000
511
+
010111011001
512
+
011100101001
513
+
101110101011
514
+
110010011001
515
+
111110001110
516
+
011100011100
517
+
110000101010
518
+
000010100010
519
+
100101101110
520
+
100010111010
521
+
110101100001
522
+
101111000100
523
+
101000111001
524
+
011111101101
525
+
111100111110
526
+
011001001000
527
+
110100110010
528
+
000011010101
529
+
111010111011
530
+
010010011000
531
+
100101000100
532
+
111010100100
533
+
000111001101
534
+
010001011000
535
+
111101101100
536
+
111110001111
537
+
110100011011
538
+
111100010101
539
+
111001111100
540
+
011100111011
541
+
011011101111
542
+
011001000011
543
+
011100111101
544
+
010100100010
545
+
110101010110
546
+
101100001000
547
+
001100101001
548
+
000001001111
549
+
000110010100
550
+
111101101010
551
+
100111000111
552
+
001011000111
553
+
001011111011
554
+
110101011100
555
+
110000110101
556
+
010001000110
557
+
011100101111
558
+
101110010001
559
+
001011001000
560
+
100100110010
561
+
000011111000
562
+
010010010000
563
+
001011100010
564
+
000000110011
565
+
000101011010
566
+
101111110000
567
+
100001010100
568
+
101110110110
569
+
001100000101
570
+
110111001101
571
+
010001010011
572
+
101011001111
573
+
111111111110
574
+
110011010011
575
+
011101000101
576
+
100001101000
577
+
011001101100
578
+
011100010000
579
+
001111111000
580
+
010110011111
581
+
111101110100
582
+
100011011101
583
+
100010110011
584
+
110111011000
585
+
100110010101
586
+
001001000000
587
+
101000100110
588
+
011010011010
589
+
000000000110
590
+
010011001010
591
+
110000110010
592
+
100001011010
593
+
101111001001
594
+
100010101001
595
+
110111111100
596
+
000010111110
597
+
000110101111
598
+
011101001011
599
+
101110011010
600
+
111101010101
601
+
001101100110
602
+
111100001101
603
+
000011100000
604
+
100111010110
605
+
110100100111
606
+
100011100110
607
+
100001011110
608
+
001110110011
609
+
101011010011
610
+
001100001000
611
+
111011001110
612
+
110011100000
613
+
101000011001
614
+
011100100001
615
+
000110001011
616
+
001001001001
617
+
000011011101
618
+
000010111010
619
+
011001100111
620
+
101001011011
621
+
010001101101
622
+
101110001011
623
+
000001011110
624
+
011100110001
625
+
110011111011
626
+
001101010011
627
+
000101000110
628
+
110101000000
629
+
110000101111
630
+
000110110111
631
+
110100101100
632
+
111011110000
633
+
011110011101
634
+
001101000001
635
+
011010001010
636
+
101000111010
637
+
111101111000
638
+
000010000000
639
+
000010001010
640
+
110000100110
641
+
110010100111
642
+
110000001100
643
+
100010000100
644
+
110010100101
645
+
111011101001
646
+
100011110000
647
+
010110110110
648
+
111100011011
649
+
110001101111
650
+
110010101111
651
+
001001001010
652
+
100100000011
653
+
110100100011
654
+
101010110001
655
+
001001011111
656
+
101101110110
657
+
001111010101
658
+
110000010011
659
+
010110001110
660
+
011011011100
661
+
000000110100
662
+
100101110001
663
+
011011001100
664
+
100101000001
665
+
100101101101
666
+
101010001110
667
+
110101100110
668
+
111010111101
669
+
111001000101
670
+
010101111100
671
+
000110000000
672
+
001010111010
673
+
110110000001
674
+
100000101110
675
+
111011110010
676
+
000111000101
677
+
011001110010
678
+
000100101010
679
+
101001010010
680
+
010001100001
681
+
000101100000
682
+
111000101110
683
+
000100010010
684
+
110110000011
685
+
010101001010
686
+
110101101110
687
+
101111101000
688
+
110011100101
689
+
111110110011
690
+
000100010011
691
+
110110010001
692
+
111100000010
693
+
011011111011
694
+
101101101001
695
+
101011011001
696
+
011011011111
697
+
101100110001
698
+
011011100010
699
+
011101010101
700
+
011101110100
701
+
010000101011
702
+
010110011011
703
+
111001101001
704
+
010010010010
705
+
010111000010
706
+
100001101100
707
+
000000101110
708
+
000000110101
709
+
111001000100
710
+
110111001110
711
+
111100111001
712
+
110101010010
713
+
111100011000
714
+
100110100100
715
+
000100000000
716
+
110111101011
717
+
001011110111
718
+
010101101011
719
+
101110001100
720
+
111111101010
721
+
111100010110
722
+
101000110011
723
+
110100010000
724
+
010010001100
725
+
011101111100
726
+
000011110001
727
+
011010101010
728
+
110001101010
729
+
101001000011
730
+
100010000110
731
+
110100111101
732
+
000011110110
733
+
001010100110
734
+
010111010101
735
+
101011100111
736
+
000101001000
737
+
110010001000
738
+
001100000100
739
+
010000111100
740
+
111011111111
741
+
100101001010
742
+
110011100111
743
+
100011100000
744
+
101010011111
745
+
010111100101
746
+
110110110101
747
+
010111010000
748
+
110011001110
749
+
101100111101
750
+
000001100001
751
+
111010100001
752
+
010000010110
753
+
001001000101
754
+
101011110001
755
+
000101101110
756
+
011110000010
757
+
110011110100
758
+
100001000001
759
+
100000011110
760
+
001101100101
761
+
101111101101
762
+
110010010100
763
+
010111101110
764
+
010101110111
765
+
101010101000
766
+
000100000010
767
+
111000001010
768
+
101100001100
769
+
101010000001
770
+
101001101011
771
+
110110000000
772
+
101100101101
773
+
101010110011
774
+
011000001001
775
+
101010111010
776
+
000001001100
777
+
101001000010
778
+
110000001111
779
+
110101001101
780
+
110011111111
781
+
010110101111
782
+
001101110110
783
+
111010001010
784
+
001010100010
785
+
000101101011
786
+
001100010111
787
+
101111100111
788
+
010100000101
789
+
110111110000
790
+
000110111011
791
+
110000011000
792
+
100101010000
793
+
101010111100
794
+
100101000111
795
+
001110100111
796
+
001000111011
797
+
011010010100
798
+
111110010010
799
+
010101010000
800
+
101100010110
801
+
000011001100
802
+
010010101011
803
+
011011000100
804
+
011100111100
805
+
111010111010
806
+
101111010000
807
+
101011010000
808
+
001010100111
809
+
010100111100
810
+
011001000010
811
+
011110110100
812
+
111000001001
813
+
110010110010
814
+
101011111001
815
+
110001111001
816
+
101001000100
817
+
010100100011
818
+
000110110101
819
+
001000100010
820
+
100110110010
821
+
000100010001
822
+
010100010010
823
+
001011000000
824
+
110101011000
825
+
001001101011
826
+
000111101110
827
+
000100110000
828
+
010000010100
829
+
001011011011
830
+
100000001110
831
+
111010110100
832
+
111001101011
833
+
101110110011
834
+
111010111111
835
+
010101010100
836
+
001110111110
837
+
111010110110
838
+
001101001011
839
+
010111101011
840
+
000110100011
841
+
100001010000
842
+
011111001010
843
+
011001001001
844
+
101100001001
845
+
001100111011
846
+
001001110111
847
+
101110110000
848
+
010011010100
849
+
001100001111
850
+
001111100001
851
+
010100010011
852
+
001001000010
853
+
100101001100
854
+
001010001101
855
+
011011001001
856
+
101110110001
857
+
010001110100
858
+
101101011001
859
+
010001111001
860
+
011101001000
861
+
010011100011
862
+
001000111010
863
+
111110100101
864
+
110000010001
865
+
110100000000
866
+
101011101110
867
+
011101001111
868
+
111110001101
869
+
101100010000
870
+
010100010101
871
+
000010001000
872
+
111111010110
873
+
000100010100
874
+
110100010101
875
+
110010000110
876
+
001111010111
877
+
000100101100
878
+
001111100111
879
+
011110001101
880
+
000111001111
881
+
000001000110
882
+
101100100000
883
+
110100010100
884
+
001011010000
885
+
101011100110
886
+
010000101010
887
+
101001000101
888
+
011000010110
889
+
010111110100
890
+
110010001001
891
+
001111010000
892
+
010010100111
893
+
011001010001
894
+
100010100010
895
+
011111010101
896
+
011100000010
897
+
110101110000
898
+
001010110100
899
+
101110111110
900
+
000010110100
901
+
101100000100
902
+
111010110111
903
+
001001101010
904
+
111010010110
905
+
011011001010
906
+
100001010111
907
+
110010011101
908
+
010110100001
909
+
110000111101
910
+
011001110111
911
+
111110001010
912
+
000101101010
913
+
010011101101
914
+
110111010001
915
+
111011011010
916
+
001111111010
917
+
100111001111
918
+
010111111111
919
+
010000010000
920
+
001111110011
921
+
100110100000
922
+
000100101111
923
+
001000010010
924
+
110001010001
925
+
001011100111
926
+
101111111111
927
+
100101101001
928
+
000010011001
929
+
011011001101
930
+
010110100000
931
+
101001101100
932
+
010010001111
933
+
110111001001
934
+
101011001000
935
+
001001010010
936
+
011011001000
937
+
001110010110
938
+
011011101011
939
+
100111111101
940
+
110001001111
941
+
001110101001
942
+
101101111011
943
+
101011011101
944
+
100100011111
945
+
100001001111
946
+
101000001010
947
+
000010011010
948
+
010110010010
949
+
100101110100
950
+
010100010100
951
+
110111001111
952
+
100000101001
953
+
010110101100
954
+
011101010011
955
+
000111000011
956
+
000000101010
957
+
101001110010
958
+
010101001000
959
+
111100000001
960
+
100101000010
961
+
010011011010
962
+
011111110011
963
+
011111010011
964
+
110001000101
965
+
100010101011
966
+
111010011101
967
+
010110010110
968
+
110011101000
969
+
101001000000
970
+
000000011100
971
+
010011100000
972
+
101010111000
973
+
000101110101
974
+
100111111110
975
+
010100100110
976
+
110110110100
977
+
110001001011
978
+
100010111101
979
+
111111111101
980
+
111111110101
981
+
000110100110
982
+
001100110011
983
+
000011100101
984
+
111000110011
985
+
111010100010
986
+
101010011001
987
+
001110011010
988
+
010100000100
989
+
010010000011
990
+
101000000001
991
+
000011110000
992
+
010011011100
993
+
111000110001
994
+
010111101111
995
+
101100010010
996
+
101110111111
997
+
111101100101
998
+
001100101011
999
+
100110111100
1000
+
011100011010