-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathmodel.tla
1514 lines (1352 loc) · 97.9 KB
/
model.tla
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
------------------------------- MODULE model -------------------------------
EXTENDS Integers, Naturals, Sequences, TLC, TLAPS
CONSTANT N
ASSUME NNAT == N \in Nat
CONSTANTS MEM_LENGTH, MEM_WIDTH
VARIABLE MEM
MEMORY == [0 .. (MEM_LENGTH) -> [0 .. (MEM_WIDTH) -> {TRUE,FALSE}]]
\* Init == MEM = [0 .. (MEM_LENGTH) |-> [0 .. (MEM_WIDTH) |-> FALSE]]
\* TypeInvariant == MEM \in MEMORY
BVN == [0..N -> {TRUE,FALSE}]
BV32 == [0..31 -> {TRUE,FALSE}]
BV64 == [0..63 -> {TRUE,FALSE}]
ANDN == [f \in BVN |-> [g \in BVN |-> [i \in 0..N |-> f[i] /\ g[i]]]]
AND32 == [f \in BV32 |-> [g \in BV32 |-> [i \in 0..31 |-> f[i] /\ g[i]]]]
AND64 == [f \in BV64 |-> [g \in BV64 |-> [i \in 0..63 |-> f[i] /\ g[i]]]]
ORN == [f \in BVN |-> [g \in BVN |-> [i \in 0..N |-> f[i] \/ g[i]]]]
OR32 == [f \in BV32 |-> [g \in BV32 |-> [i \in 0..31 |-> f[i] \/ g[i]]]]
OR64 == [f \in BV64 |-> [g \in BV64 |-> [i \in 0..63 |-> f[i] \/ g[i]]]]
EXPANDN == [b \in {TRUE,FALSE} |-> [i \in 0..N |-> b]]
EXPAND64 == [b \in {TRUE,FALSE} |-> [i \in 0..63 |-> b]]
XORN == [f \in BVN |-> [g \in BVN |-> [i \in 0..N |-> ((f[i] /\ ~g[i]) \/ (~f[i] /\ g[i]))]]]
XOR64 == [f \in BV64 |-> [g \in BV64 |-> [i \in 0..63 |-> ((f[i] /\ ~g[i]) \/ (~f[i] /\ g[i]))]]]
CMP32 == [f \in BVN |-> [g \in BVN |->
~XORN[f][g][0] /\ ~XORN[f][g][1] /\ ~XORN[f][g][2] /\
~XORN[f][g][3] /\ ~XORN[f][g][4] /\ ~XORN[f][g][5] /\
~XORN[f][g][6] /\ ~XORN[f][g][7] /\ ~XORN[f][g][8] /\
~XORN[f][g][9] /\ ~XORN[f][g][10] /\ ~XORN[f][g][11] /\
~XORN[f][g][12] /\ ~XORN[f][g][13] /\ ~XORN[f][g][14] /\
~XORN[f][g][15] /\ ~XORN[f][g][16] /\ ~XORN[f][g][17] /\
~XORN[f][g][18] /\ ~XORN[f][g][19] /\ ~XORN[f][g][20] /\
~XORN[f][g][21] /\ ~XORN[f][g][22] /\ ~XORN[f][g][23] /\
~XORN[f][g][24] /\ ~XORN[f][g][25] /\ ~XORN[f][g][26] /\
~XORN[f][g][27] /\ ~XORN[f][g][28] /\ ~XORN[f][g][29] /\
~XORN[f][g][30] /\ ~XORN[f][g][31] ]]
CMP64 == [f \in BVN |-> [g \in BVN |->
~XORN[f][g][0] /\ ~XORN[f][g][1] /\ ~XORN[f][g][2] /\
~XORN[f][g][3] /\ ~XORN[f][g][4] /\ ~XORN[f][g][5] /\
~XORN[f][g][6] /\ ~XORN[f][g][7] /\ ~XORN[f][g][8] /\
~XORN[f][g][9] /\ ~XORN[f][g][10] /\ ~XORN[f][g][11] /\
~XORN[f][g][12] /\ ~XORN[f][g][13] /\ ~XORN[f][g][14] /\
~XORN[f][g][15] /\ ~XORN[f][g][16] /\ ~XORN[f][g][17] /\
~XORN[f][g][18] /\ ~XORN[f][g][19] /\ ~XORN[f][g][20] /\
~XORN[f][g][21] /\ ~XORN[f][g][22] /\ ~XORN[f][g][23] /\
~XORN[f][g][24] /\ ~XORN[f][g][25] /\ ~XORN[f][g][26] /\
~XORN[f][g][27] /\ ~XORN[f][g][28] /\ ~XORN[f][g][29] /\
~XORN[f][g][30] /\ ~XORN[f][g][31] /\
~XORN[f][g][32] /\ ~XORN[f][g][33] /\ ~XORN[f][g][34] /\
~XORN[f][g][35] /\ ~XORN[f][g][36] /\ ~XORN[f][g][37] /\
~XORN[f][g][38] /\ ~XORN[f][g][39] /\ ~XORN[f][g][40] /\
~XORN[f][g][41] /\ ~XORN[f][g][42] /\ ~XORN[f][g][43] /\
~XORN[f][g][44] /\ ~XORN[f][g][45] /\ ~XORN[f][g][46] /\
~XORN[f][g][47] /\ ~XORN[f][g][48] /\ ~XORN[f][g][49] /\
~XORN[f][g][50] /\ ~XORN[f][g][51] /\ ~XORN[f][g][52] /\
~XORN[f][g][53] /\ ~XORN[f][g][54] /\ ~XORN[f][g][55] /\
~XORN[f][g][56] /\ ~XORN[f][g][57] /\ ~XORN[f][g][58] /\
~XORN[f][g][59] /\ ~XORN[f][g][60] /\ ~XORN[f][g][61] /\
~XORN[f][g][62] /\ ~XORN[f][g][63] ]]
CMP_EQ_LT_GT == [b0 \in {TRUE,FALSE} |-> [b1 \in {TRUE,FALSE} |->
[eq \in {TRUE,FALSE} |-> [lt \in {TRUE,FALSE} |-> [gt \in {TRUE,FALSE} |->
[i \in 0..2 |->
((i=0) /\ ((b0 /\ b1) \/ (~b0 /\ ~b1)) /\ eq) \/
((i=1) /\ ((~b0 /\ b1 /\ eq) \/ lt)) \/
((i=2) /\ ((b0 /\ ~b1 /\ eq) \/ gt)) ]]]]]]
CMP_EQ_LT_GT_1 == [f \in BVN |-> [g \in BVN |-> [i \in 0..63 |->
[eq \in {TRUE,FALSE} |-> [lt \in {TRUE,FALSE} |-> [gt \in {TRUE,FALSE} |->
CMP_EQ_LT_GT[f[i]][g[i]][eq][lt][gt]
]]]]]]
CMP_EQ_LT_GT_2 == [f \in BVN |-> [g \in BVN |-> [i \in {x \in 0..62 : x%2=0} |->
[eq \in {TRUE,FALSE} |-> [lt \in {TRUE,FALSE} |-> [gt \in {TRUE,FALSE} |->
CMP_EQ_LT_GT_1[f][g][i]
[CMP_EQ_LT_GT_1[f][g][i+1][eq][lt][gt][0]]
[CMP_EQ_LT_GT_1[f][g][i+1][eq][lt][gt][1]]
[CMP_EQ_LT_GT_1[f][g][i+1][eq][lt][gt][2]] ]]]]]]
CMP_EQ_LT_GT_3 == [f \in BVN |-> [g \in BVN |-> [i \in 0..61 |->
[eq \in {TRUE,FALSE} |-> [lt \in {TRUE,FALSE} |-> [gt \in {TRUE,FALSE} |->
CMP_EQ_LT_GT_1[f][g][i]
[CMP_EQ_LT_GT_2[f][g][i+1][eq][lt][gt][0]]
[CMP_EQ_LT_GT_2[f][g][i+1][eq][lt][gt][1]]
[CMP_EQ_LT_GT_2[f][g][i+1][eq][lt][gt][2]]
]]]]]]
CMP_EQ_LT_GT_4 == [f \in BVN |-> [g \in BVN |-> [i \in {x \in 0..60 : x%4=0} |->
[eq \in {TRUE,FALSE} |-> [lt \in {TRUE,FALSE} |-> [gt \in {TRUE,FALSE} |->
CMP_EQ_LT_GT_2[f][g][i]
[CMP_EQ_LT_GT_2[f][g][i+2][eq][lt][gt][0]]
[CMP_EQ_LT_GT_2[f][g][i+2][eq][lt][gt][1]]
[CMP_EQ_LT_GT_2[f][g][i+2][eq][lt][gt][2]] ]]]]]]
CMP_EQ_LT_GT_8 == [f \in BVN |-> [g \in BVN |-> [i \in {0,8,16,24,32,40,48,56} |->
[eq \in {TRUE,FALSE} |-> [lt \in {TRUE,FALSE} |-> [gt \in {TRUE,FALSE} |->
CMP_EQ_LT_GT_4[f][g][i]
[CMP_EQ_LT_GT_4[f][g][i+4][eq][lt][gt][0]]
[CMP_EQ_LT_GT_4[f][g][i+4][eq][lt][gt][1]]
[CMP_EQ_LT_GT_4[f][g][i+4][eq][lt][gt][2]] ]]]]]]
CMP_EQ_LT_GT_16 == [f \in BVN |-> [g \in BVN |-> [i \in {0,16,32,48} |->
[eq \in {TRUE,FALSE} |-> [lt \in {TRUE,FALSE} |-> [gt \in {TRUE,FALSE} |->
CMP_EQ_LT_GT_8[f][g][i]
[CMP_EQ_LT_GT_8[f][g][i+8][eq][lt][gt][0]]
[CMP_EQ_LT_GT_8[f][g][i+8][eq][lt][gt][1]]
[CMP_EQ_LT_GT_8[f][g][i+8][eq][lt][gt][2]] ]]]]]]
CMP_EQ_LT_GT_32 == [f \in BVN |-> [g \in BVN |-> [i \in {0,32} |->
[eq \in {TRUE,FALSE} |-> [lt \in {TRUE,FALSE} |-> [gt \in {TRUE,FALSE} |->
CMP_EQ_LT_GT_16[f][g][i]
[CMP_EQ_LT_GT_16[f][g][i+16][eq][lt][gt][0]]
[CMP_EQ_LT_GT_16[f][g][i+16][eq][lt][gt][1]]
[CMP_EQ_LT_GT_16[f][g][i+16][eq][lt][gt][2]] ]]]]]]
b0 == [i \in 0..63 |-> FALSE]
b1 == [i \in 0..63 |-> (i=0)]
b2 == [i \in 0..63 |-> (i=1)]
b3 == [i \in 0..63 |-> (i=0) \/ (i=1)]
b4 == [i \in 0..63 |-> (i=2)]
b5 == [i \in 0..63 |-> (i=0) \/ (i=2)]
b6 == [i \in 0..63 |-> (i=1) \/ (i=2)]
b7 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2)]
b8 == [i \in 0..63 |-> (i=3)]
b9 == [i \in 0..63 |-> (i=0) \/ (i=3)]
b10 == [i \in 0..63 |-> (i=1) \/ (i=3)]
b11 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3)]
b12 == [i \in 0..63 |-> (i=2) \/ (i=3)]
b13 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3)]
b14 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3)]
b15 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3)]
b16 == [i \in 0..63 |-> (i=4)]
b17 == [i \in 0..63 |-> (i=0) \/ (i=4)]
b18 == [i \in 0..63 |-> (i=1) \/ (i=4)]
b19 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=4)]
b20 == [i \in 0..63 |-> (i=2) \/ (i=4)]
b21 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=4)]
b22 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=4)]
b23 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=4)]
b24 == [i \in 0..63 |-> (i=3) \/ (i=4)]
b25 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=4)]
b26 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=4)]
b27 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=4)]
b28 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=4)]
b29 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=4)]
b30 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=4)]
b31 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=4)]
b32 == [i \in 0..63 |-> (i=5)]
b33 == [i \in 0..63 |-> (i=0) \/ (i=5)]
b34 == [i \in 0..63 |-> (i=1) \/ (i=5)]
b35 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=5)]
b36 == [i \in 0..63 |-> (i=2) \/ (i=5)]
b37 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=5)]
b38 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=5)]
b39 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=5)]
b40 == [i \in 0..63 |-> (i=3) \/ (i=5)]
b41 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=5)]
b42 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=5)]
b43 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=5)]
b44 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=5)]
b45 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=5)]
b46 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=5)]
b47 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=5)]
b48 == [i \in 0..63 |-> (i=4) \/ (i=5)]
b49 == [i \in 0..63 |-> (i=0) \/ (i=4) \/ (i=5)]
b50 == [i \in 0..63 |-> (i=1) \/ (i=4) \/ (i=5)]
b51 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=4) \/ (i=5)]
b52 == [i \in 0..63 |-> (i=2) \/ (i=4) \/ (i=5)]
b53 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=4) \/ (i=5)]
b54 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=4) \/ (i=5)]
b55 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=4) \/ (i=5)]
b56 == [i \in 0..63 |-> (i=3) \/ (i=4) \/ (i=5)]
b57 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=4) \/ (i=5)]
b58 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=4) \/ (i=5)]
b59 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=4) \/ (i=5)]
b60 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=4) \/ (i=5)]
b61 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5)]
b62 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5)]
b63 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5)]
b64 == [i \in 0..63 |-> (i=6)]
b65 == [i \in 0..63 |-> (i=0) \/ (i=6)]
b66 == [i \in 0..63 |-> (i=1) \/ (i=6)]
b67 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=6)]
b68 == [i \in 0..63 |-> (i=2) \/ (i=6)]
b69 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=6)]
b70 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=6)]
b71 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=6)]
b72 == [i \in 0..63 |-> (i=3) \/ (i=6)]
b73 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=6)]
b74 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=6)]
b75 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=6)]
b76 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=6)]
b77 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=6)]
b78 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=6)]
b79 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=6)]
b80 == [i \in 0..63 |-> (i=4) \/ (i=6)]
b81 == [i \in 0..63 |-> (i=0) \/ (i=4) \/ (i=6)]
b82 == [i \in 0..63 |-> (i=1) \/ (i=4) \/ (i=6)]
b83 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=4) \/ (i=6)]
b84 == [i \in 0..63 |-> (i=2) \/ (i=4) \/ (i=6)]
b85 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=4) \/ (i=6)]
b86 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=4) \/ (i=6)]
b87 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=4) \/ (i=6)]
b88 == [i \in 0..63 |-> (i=3) \/ (i=4) \/ (i=6)]
b89 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=4) \/ (i=6)]
b90 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=4) \/ (i=6)]
b91 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=4) \/ (i=6)]
b92 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=4) \/ (i=6)]
b93 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=6)]
b94 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=6)]
b95 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=6)]
b96 == [i \in 0..63 |-> (i=5) \/ (i=6)]
b97 == [i \in 0..63 |-> (i=0) \/ (i=5) \/ (i=6)]
b98 == [i \in 0..63 |-> (i=1) \/ (i=5) \/ (i=6)]
b99 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=5) \/ (i=6)]
b100 == [i \in 0..63 |-> (i=2) \/ (i=5) \/ (i=6)]
b101 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=5) \/ (i=6)]
b102 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=5) \/ (i=6)]
b103 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=5) \/ (i=6)]
b104 == [i \in 0..63 |-> (i=3) \/ (i=5) \/ (i=6)]
b105 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=5) \/ (i=6)]
b106 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=5) \/ (i=6)]
b107 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=5) \/ (i=6)]
b108 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=5) \/ (i=6)]
b109 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=5) \/ (i=6)]
b110 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=5) \/ (i=6)]
b111 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=5) \/ (i=6)]
b112 == [i \in 0..63 |-> (i=4) \/ (i=5) \/ (i=6)]
b113 == [i \in 0..63 |-> (i=0) \/ (i=4) \/ (i=5) \/ (i=6)]
b114 == [i \in 0..63 |-> (i=1) \/ (i=4) \/ (i=5) \/ (i=6)]
b115 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=4) \/ (i=5) \/ (i=6)]
b116 == [i \in 0..63 |-> (i=2) \/ (i=4) \/ (i=5) \/ (i=6)]
b117 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=4) \/ (i=5) \/ (i=6)]
b118 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=4) \/ (i=5) \/ (i=6)]
b119 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=4) \/ (i=5) \/ (i=6)]
b120 == [i \in 0..63 |-> (i=3) \/ (i=4) \/ (i=5) \/ (i=6)]
b121 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6)]
b122 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6)]
b123 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6)]
b124 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6)]
b125 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6)]
b126 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6)]
b127 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6)]
b128 == [i \in 0..63 |-> (i=7)]
b129 == [i \in 0..63 |-> (i=0) \/ (i=7)]
b130 == [i \in 0..63 |-> (i=1) \/ (i=7)]
b131 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=7)]
b132 == [i \in 0..63 |-> (i=2) \/ (i=7)]
b133 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=7)]
b134 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=7)]
b135 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=7)]
b136 == [i \in 0..63 |-> (i=3) \/ (i=7)]
b137 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=7)]
b138 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=7)]
b139 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=7)]
b140 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=7)]
b141 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=7)]
b142 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=7)]
b143 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=7)]
b144 == [i \in 0..63 |-> (i=4) \/ (i=7)]
b145 == [i \in 0..63 |-> (i=0) \/ (i=4) \/ (i=7)]
b146 == [i \in 0..63 |-> (i=1) \/ (i=4) \/ (i=7)]
b147 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=4) \/ (i=7)]
b148 == [i \in 0..63 |-> (i=2) \/ (i=4) \/ (i=7)]
b149 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=4) \/ (i=7)]
b150 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=4) \/ (i=7)]
b151 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=4) \/ (i=7)]
b152 == [i \in 0..63 |-> (i=3) \/ (i=4) \/ (i=7)]
b153 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=4) \/ (i=7)]
b154 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=4) \/ (i=7)]
b155 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=4) \/ (i=7)]
b156 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=4) \/ (i=7)]
b157 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=7)]
b158 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=7)]
b159 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=7)]
b160 == [i \in 0..63 |-> (i=5) \/ (i=7)]
b161 == [i \in 0..63 |-> (i=0) \/ (i=5) \/ (i=7)]
b162 == [i \in 0..63 |-> (i=1) \/ (i=5) \/ (i=7)]
b163 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=5) \/ (i=7)]
b164 == [i \in 0..63 |-> (i=2) \/ (i=5) \/ (i=7)]
b165 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=5) \/ (i=7)]
b166 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=5) \/ (i=7)]
b167 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=5) \/ (i=7)]
b168 == [i \in 0..63 |-> (i=3) \/ (i=5) \/ (i=7)]
b169 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=5) \/ (i=7)]
b170 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=5) \/ (i=7)]
b171 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=5) \/ (i=7)]
b172 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=5) \/ (i=7)]
b173 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=5) \/ (i=7)]
b174 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=5) \/ (i=7)]
b175 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=5) \/ (i=7)]
b176 == [i \in 0..63 |-> (i=4) \/ (i=5) \/ (i=7)]
b177 == [i \in 0..63 |-> (i=0) \/ (i=4) \/ (i=5) \/ (i=7)]
b178 == [i \in 0..63 |-> (i=1) \/ (i=4) \/ (i=5) \/ (i=7)]
b179 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=4) \/ (i=5) \/ (i=7)]
b180 == [i \in 0..63 |-> (i=2) \/ (i=4) \/ (i=5) \/ (i=7)]
b181 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=4) \/ (i=5) \/ (i=7)]
b182 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=4) \/ (i=5) \/ (i=7)]
b183 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=4) \/ (i=5) \/ (i=7)]
b184 == [i \in 0..63 |-> (i=3) \/ (i=4) \/ (i=5) \/ (i=7)]
b185 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=7)]
b186 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=7)]
b187 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=7)]
b188 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=7)]
b189 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=7)]
b190 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=7)]
b191 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=7)]
b192 == [i \in 0..63 |-> (i=6) \/ (i=7)]
b193 == [i \in 0..63 |-> (i=0) \/ (i=6) \/ (i=7)]
b194 == [i \in 0..63 |-> (i=1) \/ (i=6) \/ (i=7)]
b195 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=6) \/ (i=7)]
b196 == [i \in 0..63 |-> (i=2) \/ (i=6) \/ (i=7)]
b197 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=6) \/ (i=7)]
b198 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=6) \/ (i=7)]
b199 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=6) \/ (i=7)]
b200 == [i \in 0..63 |-> (i=3) \/ (i=6) \/ (i=7)]
b201 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=6) \/ (i=7)]
b202 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=6) \/ (i=7)]
b203 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=6) \/ (i=7)]
b204 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=6) \/ (i=7)]
b205 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=6) \/ (i=7)]
b206 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=6) \/ (i=7)]
b207 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=6) \/ (i=7)]
b208 == [i \in 0..63 |-> (i=4) \/ (i=6) \/ (i=7)]
b209 == [i \in 0..63 |-> (i=0) \/ (i=4) \/ (i=6) \/ (i=7)]
b210 == [i \in 0..63 |-> (i=1) \/ (i=4) \/ (i=6) \/ (i=7)]
b211 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=4) \/ (i=6) \/ (i=7)]
b212 == [i \in 0..63 |-> (i=2) \/ (i=4) \/ (i=6) \/ (i=7)]
b213 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=4) \/ (i=6) \/ (i=7)]
b214 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=4) \/ (i=6) \/ (i=7)]
b215 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=4) \/ (i=6) \/ (i=7)]
b216 == [i \in 0..63 |-> (i=3) \/ (i=4) \/ (i=6) \/ (i=7)]
b217 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=4) \/ (i=6) \/ (i=7)]
b218 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=4) \/ (i=6) \/ (i=7)]
b219 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=4) \/ (i=6) \/ (i=7)]
b220 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=4) \/ (i=6) \/ (i=7)]
b221 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=6) \/ (i=7)]
b222 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=6) \/ (i=7)]
b223 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=6) \/ (i=7)]
b224 == [i \in 0..63 |-> (i=5) \/ (i=6) \/ (i=7)]
b225 == [i \in 0..63 |-> (i=0) \/ (i=5) \/ (i=6) \/ (i=7)]
b226 == [i \in 0..63 |-> (i=1) \/ (i=5) \/ (i=6) \/ (i=7)]
b227 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=5) \/ (i=6) \/ (i=7)]
b228 == [i \in 0..63 |-> (i=2) \/ (i=5) \/ (i=6) \/ (i=7)]
b229 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=5) \/ (i=6) \/ (i=7)]
b230 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=5) \/ (i=6) \/ (i=7)]
b231 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=5) \/ (i=6) \/ (i=7)]
b232 == [i \in 0..63 |-> (i=3) \/ (i=5) \/ (i=6) \/ (i=7)]
b233 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=5) \/ (i=6) \/ (i=7)]
b234 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=5) \/ (i=6) \/ (i=7)]
b235 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=5) \/ (i=6) \/ (i=7)]
b236 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=5) \/ (i=6) \/ (i=7)]
b237 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=5) \/ (i=6) \/ (i=7)]
b238 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=5) \/ (i=6) \/ (i=7)]
b239 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=5) \/ (i=6) \/ (i=7)]
b240 == [i \in 0..63 |-> (i=4) \/ (i=5) \/ (i=6) \/ (i=7)]
b241 == [i \in 0..63 |-> (i=0) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7)]
b242 == [i \in 0..63 |-> (i=1) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7)]
b243 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7)]
b244 == [i \in 0..63 |-> (i=2) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7)]
b245 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7)]
b246 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7)]
b247 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7)]
b248 == [i \in 0..63 |-> (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7)]
b249 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7)]
b250 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7)]
b251 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7)]
b252 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7)]
b253 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7)]
b254 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7)]
b255 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7)]
b256 == [i \in 0..63 |-> (i=8)]
b257 == [i \in 0..63 |-> (i=0) \/ (i=8)]
b258 == [i \in 0..63 |-> (i=1) \/ (i=8)]
b259 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=8)]
b260 == [i \in 0..63 |-> (i=2) \/ (i=8)]
b261 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=8)]
b262 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=8)]
b263 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=8)]
b264 == [i \in 0..63 |-> (i=3) \/ (i=8)]
b265 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=8)]
b266 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=8)]
b267 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=8)]
b268 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=8)]
b269 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=8)]
b270 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=8)]
b271 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=8)]
b272 == [i \in 0..63 |-> (i=4) \/ (i=8)]
b273 == [i \in 0..63 |-> (i=0) \/ (i=4) \/ (i=8)]
b274 == [i \in 0..63 |-> (i=1) \/ (i=4) \/ (i=8)]
b275 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=4) \/ (i=8)]
b276 == [i \in 0..63 |-> (i=2) \/ (i=4) \/ (i=8)]
b277 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=4) \/ (i=8)]
b278 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=4) \/ (i=8)]
b279 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=4) \/ (i=8)]
b280 == [i \in 0..63 |-> (i=3) \/ (i=4) \/ (i=8)]
b281 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=4) \/ (i=8)]
b282 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=4) \/ (i=8)]
b283 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=4) \/ (i=8)]
b284 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=4) \/ (i=8)]
b285 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=8)]
b286 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=8)]
b287 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=8)]
b288 == [i \in 0..63 |-> (i=5) \/ (i=8)]
b289 == [i \in 0..63 |-> (i=0) \/ (i=5) \/ (i=8)]
b290 == [i \in 0..63 |-> (i=1) \/ (i=5) \/ (i=8)]
b291 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=5) \/ (i=8)]
b292 == [i \in 0..63 |-> (i=2) \/ (i=5) \/ (i=8)]
b293 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=5) \/ (i=8)]
b294 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=5) \/ (i=8)]
b295 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=5) \/ (i=8)]
b296 == [i \in 0..63 |-> (i=3) \/ (i=5) \/ (i=8)]
b297 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=5) \/ (i=8)]
b298 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=5) \/ (i=8)]
b299 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=5) \/ (i=8)]
b300 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=5) \/ (i=8)]
b301 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=5) \/ (i=8)]
b302 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=5) \/ (i=8)]
b303 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=5) \/ (i=8)]
b304 == [i \in 0..63 |-> (i=4) \/ (i=5) \/ (i=8)]
b305 == [i \in 0..63 |-> (i=0) \/ (i=4) \/ (i=5) \/ (i=8)]
b306 == [i \in 0..63 |-> (i=1) \/ (i=4) \/ (i=5) \/ (i=8)]
b307 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=4) \/ (i=5) \/ (i=8)]
b308 == [i \in 0..63 |-> (i=2) \/ (i=4) \/ (i=5) \/ (i=8)]
b309 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=4) \/ (i=5) \/ (i=8)]
b310 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=4) \/ (i=5) \/ (i=8)]
b311 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=4) \/ (i=5) \/ (i=8)]
b312 == [i \in 0..63 |-> (i=3) \/ (i=4) \/ (i=5) \/ (i=8)]
b313 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=8)]
b314 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=8)]
b315 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=8)]
b316 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=8)]
b317 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=8)]
b318 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=8)]
b319 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=8)]
b320 == [i \in 0..63 |-> (i=6) \/ (i=8)]
b321 == [i \in 0..63 |-> (i=0) \/ (i=6) \/ (i=8)]
b322 == [i \in 0..63 |-> (i=1) \/ (i=6) \/ (i=8)]
b323 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=6) \/ (i=8)]
b324 == [i \in 0..63 |-> (i=2) \/ (i=6) \/ (i=8)]
b325 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=6) \/ (i=8)]
b326 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=6) \/ (i=8)]
b327 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=6) \/ (i=8)]
b328 == [i \in 0..63 |-> (i=3) \/ (i=6) \/ (i=8)]
b329 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=6) \/ (i=8)]
b330 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=6) \/ (i=8)]
b331 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=6) \/ (i=8)]
b332 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=6) \/ (i=8)]
b333 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=6) \/ (i=8)]
b334 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=6) \/ (i=8)]
b335 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=6) \/ (i=8)]
b336 == [i \in 0..63 |-> (i=4) \/ (i=6) \/ (i=8)]
b337 == [i \in 0..63 |-> (i=0) \/ (i=4) \/ (i=6) \/ (i=8)]
b338 == [i \in 0..63 |-> (i=1) \/ (i=4) \/ (i=6) \/ (i=8)]
b339 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=4) \/ (i=6) \/ (i=8)]
b340 == [i \in 0..63 |-> (i=2) \/ (i=4) \/ (i=6) \/ (i=8)]
b341 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=4) \/ (i=6) \/ (i=8)]
b342 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=4) \/ (i=6) \/ (i=8)]
b343 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=4) \/ (i=6) \/ (i=8)]
b344 == [i \in 0..63 |-> (i=3) \/ (i=4) \/ (i=6) \/ (i=8)]
b345 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=4) \/ (i=6) \/ (i=8)]
b346 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=4) \/ (i=6) \/ (i=8)]
b347 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=4) \/ (i=6) \/ (i=8)]
b348 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=4) \/ (i=6) \/ (i=8)]
b349 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=6) \/ (i=8)]
b350 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=6) \/ (i=8)]
b351 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=6) \/ (i=8)]
b352 == [i \in 0..63 |-> (i=5) \/ (i=6) \/ (i=8)]
b353 == [i \in 0..63 |-> (i=0) \/ (i=5) \/ (i=6) \/ (i=8)]
b354 == [i \in 0..63 |-> (i=1) \/ (i=5) \/ (i=6) \/ (i=8)]
b355 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=5) \/ (i=6) \/ (i=8)]
b356 == [i \in 0..63 |-> (i=2) \/ (i=5) \/ (i=6) \/ (i=8)]
b357 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=5) \/ (i=6) \/ (i=8)]
b358 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=5) \/ (i=6) \/ (i=8)]
b359 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=5) \/ (i=6) \/ (i=8)]
b360 == [i \in 0..63 |-> (i=3) \/ (i=5) \/ (i=6) \/ (i=8)]
b361 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=5) \/ (i=6) \/ (i=8)]
b362 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=5) \/ (i=6) \/ (i=8)]
b363 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=5) \/ (i=6) \/ (i=8)]
b364 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=5) \/ (i=6) \/ (i=8)]
b365 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=5) \/ (i=6) \/ (i=8)]
b366 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=5) \/ (i=6) \/ (i=8)]
b367 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=5) \/ (i=6) \/ (i=8)]
b368 == [i \in 0..63 |-> (i=4) \/ (i=5) \/ (i=6) \/ (i=8)]
b369 == [i \in 0..63 |-> (i=0) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=8)]
b370 == [i \in 0..63 |-> (i=1) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=8)]
b371 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=8)]
b372 == [i \in 0..63 |-> (i=2) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=8)]
b373 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=8)]
b374 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=8)]
b375 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=8)]
b376 == [i \in 0..63 |-> (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=8)]
b377 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=8)]
b378 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=8)]
b379 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=8)]
b380 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=8)]
b381 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=8)]
b382 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=8)]
b383 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=8)]
b384 == [i \in 0..63 |-> (i=7) \/ (i=8)]
b385 == [i \in 0..63 |-> (i=0) \/ (i=7) \/ (i=8)]
b386 == [i \in 0..63 |-> (i=1) \/ (i=7) \/ (i=8)]
b387 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=7) \/ (i=8)]
b388 == [i \in 0..63 |-> (i=2) \/ (i=7) \/ (i=8)]
b389 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=7) \/ (i=8)]
b390 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=7) \/ (i=8)]
b391 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=7) \/ (i=8)]
b392 == [i \in 0..63 |-> (i=3) \/ (i=7) \/ (i=8)]
b393 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=7) \/ (i=8)]
b394 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=7) \/ (i=8)]
b395 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=7) \/ (i=8)]
b396 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=7) \/ (i=8)]
b397 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=7) \/ (i=8)]
b398 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=7) \/ (i=8)]
b399 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=7) \/ (i=8)]
b400 == [i \in 0..63 |-> (i=4) \/ (i=7) \/ (i=8)]
b401 == [i \in 0..63 |-> (i=0) \/ (i=4) \/ (i=7) \/ (i=8)]
b402 == [i \in 0..63 |-> (i=1) \/ (i=4) \/ (i=7) \/ (i=8)]
b403 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=4) \/ (i=7) \/ (i=8)]
b404 == [i \in 0..63 |-> (i=2) \/ (i=4) \/ (i=7) \/ (i=8)]
b405 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=4) \/ (i=7) \/ (i=8)]
b406 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=4) \/ (i=7) \/ (i=8)]
b407 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=4) \/ (i=7) \/ (i=8)]
b408 == [i \in 0..63 |-> (i=3) \/ (i=4) \/ (i=7) \/ (i=8)]
b409 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=4) \/ (i=7) \/ (i=8)]
b410 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=4) \/ (i=7) \/ (i=8)]
b411 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=4) \/ (i=7) \/ (i=8)]
b412 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=4) \/ (i=7) \/ (i=8)]
b413 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=7) \/ (i=8)]
b414 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=7) \/ (i=8)]
b415 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=7) \/ (i=8)]
b416 == [i \in 0..63 |-> (i=5) \/ (i=7) \/ (i=8)]
b417 == [i \in 0..63 |-> (i=0) \/ (i=5) \/ (i=7) \/ (i=8)]
b418 == [i \in 0..63 |-> (i=1) \/ (i=5) \/ (i=7) \/ (i=8)]
b419 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=5) \/ (i=7) \/ (i=8)]
b420 == [i \in 0..63 |-> (i=2) \/ (i=5) \/ (i=7) \/ (i=8)]
b421 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=5) \/ (i=7) \/ (i=8)]
b422 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=5) \/ (i=7) \/ (i=8)]
b423 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=5) \/ (i=7) \/ (i=8)]
b424 == [i \in 0..63 |-> (i=3) \/ (i=5) \/ (i=7) \/ (i=8)]
b425 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=5) \/ (i=7) \/ (i=8)]
b426 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=5) \/ (i=7) \/ (i=8)]
b427 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=5) \/ (i=7) \/ (i=8)]
b428 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=5) \/ (i=7) \/ (i=8)]
b429 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=5) \/ (i=7) \/ (i=8)]
b430 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=5) \/ (i=7) \/ (i=8)]
b431 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=5) \/ (i=7) \/ (i=8)]
b432 == [i \in 0..63 |-> (i=4) \/ (i=5) \/ (i=7) \/ (i=8)]
b433 == [i \in 0..63 |-> (i=0) \/ (i=4) \/ (i=5) \/ (i=7) \/ (i=8)]
b434 == [i \in 0..63 |-> (i=1) \/ (i=4) \/ (i=5) \/ (i=7) \/ (i=8)]
b435 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=4) \/ (i=5) \/ (i=7) \/ (i=8)]
b436 == [i \in 0..63 |-> (i=2) \/ (i=4) \/ (i=5) \/ (i=7) \/ (i=8)]
b437 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=4) \/ (i=5) \/ (i=7) \/ (i=8)]
b438 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=4) \/ (i=5) \/ (i=7) \/ (i=8)]
b439 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=4) \/ (i=5) \/ (i=7) \/ (i=8)]
b440 == [i \in 0..63 |-> (i=3) \/ (i=4) \/ (i=5) \/ (i=7) \/ (i=8)]
b441 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=7) \/ (i=8)]
b442 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=7) \/ (i=8)]
b443 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=7) \/ (i=8)]
b444 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=7) \/ (i=8)]
b445 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=7) \/ (i=8)]
b446 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=7) \/ (i=8)]
b447 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=7) \/ (i=8)]
b448 == [i \in 0..63 |-> (i=6) \/ (i=7) \/ (i=8)]
b449 == [i \in 0..63 |-> (i=0) \/ (i=6) \/ (i=7) \/ (i=8)]
b450 == [i \in 0..63 |-> (i=1) \/ (i=6) \/ (i=7) \/ (i=8)]
b451 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=6) \/ (i=7) \/ (i=8)]
b452 == [i \in 0..63 |-> (i=2) \/ (i=6) \/ (i=7) \/ (i=8)]
b453 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=6) \/ (i=7) \/ (i=8)]
b454 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=6) \/ (i=7) \/ (i=8)]
b455 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=6) \/ (i=7) \/ (i=8)]
b456 == [i \in 0..63 |-> (i=3) \/ (i=6) \/ (i=7) \/ (i=8)]
b457 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=6) \/ (i=7) \/ (i=8)]
b458 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=6) \/ (i=7) \/ (i=8)]
b459 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=6) \/ (i=7) \/ (i=8)]
b460 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=6) \/ (i=7) \/ (i=8)]
b461 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=6) \/ (i=7) \/ (i=8)]
b462 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=6) \/ (i=7) \/ (i=8)]
b463 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=6) \/ (i=7) \/ (i=8)]
b464 == [i \in 0..63 |-> (i=4) \/ (i=6) \/ (i=7) \/ (i=8)]
b465 == [i \in 0..63 |-> (i=0) \/ (i=4) \/ (i=6) \/ (i=7) \/ (i=8)]
b466 == [i \in 0..63 |-> (i=1) \/ (i=4) \/ (i=6) \/ (i=7) \/ (i=8)]
b467 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=4) \/ (i=6) \/ (i=7) \/ (i=8)]
b468 == [i \in 0..63 |-> (i=2) \/ (i=4) \/ (i=6) \/ (i=7) \/ (i=8)]
b469 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=4) \/ (i=6) \/ (i=7) \/ (i=8)]
b470 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=4) \/ (i=6) \/ (i=7) \/ (i=8)]
b471 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=4) \/ (i=6) \/ (i=7) \/ (i=8)]
b472 == [i \in 0..63 |-> (i=3) \/ (i=4) \/ (i=6) \/ (i=7) \/ (i=8)]
b473 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=4) \/ (i=6) \/ (i=7) \/ (i=8)]
b474 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=4) \/ (i=6) \/ (i=7) \/ (i=8)]
b475 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=4) \/ (i=6) \/ (i=7) \/ (i=8)]
b476 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=4) \/ (i=6) \/ (i=7) \/ (i=8)]
b477 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=6) \/ (i=7) \/ (i=8)]
b478 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=6) \/ (i=7) \/ (i=8)]
b479 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=6) \/ (i=7) \/ (i=8)]
b480 == [i \in 0..63 |-> (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b481 == [i \in 0..63 |-> (i=0) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b482 == [i \in 0..63 |-> (i=1) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b483 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b484 == [i \in 0..63 |-> (i=2) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b485 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b486 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b487 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b488 == [i \in 0..63 |-> (i=3) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b489 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b490 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b491 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b492 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b493 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b494 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b495 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b496 == [i \in 0..63 |-> (i=4) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b497 == [i \in 0..63 |-> (i=0) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b498 == [i \in 0..63 |-> (i=1) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b499 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b500 == [i \in 0..63 |-> (i=2) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b501 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b502 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b503 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b504 == [i \in 0..63 |-> (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b505 == [i \in 0..63 |-> (i=0) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b506 == [i \in 0..63 |-> (i=1) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b507 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b508 == [i \in 0..63 |-> (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b509 == [i \in 0..63 |-> (i=0) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b510 == [i \in 0..63 |-> (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b511 == [i \in 0..63 |-> (i=0) \/ (i=1) \/ (i=2) \/ (i=3) \/ (i=4) \/ (i=5) \/ (i=6) \/ (i=7) \/ (i=8)]
b512 == [i \in 0..63 |-> (i=9)]
BIN == [b \in {TRUE,FALSE} |-> IF b THEN 1 ELSE 0]
BIN32 == [f \in BV32 |-> BIN[f[0]]*2^0 + BIN[f[1]]*2^1 + BIN[f[2]]*2^2 + BIN[f[3]]*2^3 + BIN[f[4]]*2^4 + BIN[f[5]]*2^5 + BIN[f[6]]*2^6 + BIN[f[7]]*2^7 + BIN[f[8]]*2^8 + BIN[f[9]]*2^9 + BIN[f[10]]*2^10 + BIN[f[11]]*2^11 + BIN[f[12]]*2^12 + BIN[f[13]]*2^13 + BIN[f[14]]*2^14 + BIN[f[15]]*2^15 + BIN[f[16]]*2^16 + BIN[f[17]]*2^17 + BIN[f[18]]*2^18 + BIN[f[19]]*2^19 + BIN[f[20]]*2^20 + BIN[f[21]]*2^21 + BIN[f[22]]*2^22 + BIN[f[23]]*2^23 + BIN[f[24]]*2^24 + BIN[f[25]]*2^25 + BIN[f[26]]*2^26 + BIN[f[27]]*2^27 + BIN[f[28]]*2^28 + BIN[f[29]]*2^29 + BIN[f[30]]*2^30]
SLR32 == [f \in BV32 |-> [g \in BV32 |-> [i \in 0..31 |->
(CMP32[AND32[f][b31]][b31] /\
(i=0) /\ g[31]
) \/
(CMP32[AND32[f][b31]][b30] /\
( ((i=0) /\ g[30]) \/ ((i=1) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b29] /\
( ((i=0) /\ g[29]) \/ ((i=1) /\ g[30]) \/ ((i=2) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b28] /\
( ((i=0) /\ g[28]) \/ ((i=1) /\ g[29]) \/ ((i=2) /\ g[30]) \/ ((i=3) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b27] /\
( ((i=0) /\ g[27]) \/ ((i=1) /\ g[28]) \/ ((i=2) /\ g[29]) \/ ((i=3) /\ g[30]) \/ ((i=4) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b26] /\
( ((i=0) /\ g[26]) \/ ((i=1) /\ g[27]) \/ ((i=2) /\ g[28]) \/ ((i=3) /\ g[29]) \/ ((i=4) /\ g[30]) \/ ((i=5) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b25] /\
( ((i=0) /\ g[25]) \/ ((i=1) /\ g[26]) \/ ((i=2) /\ g[27]) \/ ((i=3) /\ g[28]) \/ ((i=4) /\ g[29]) \/ ((i=5) /\ g[30]) \/ ((i=6) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b24] /\
( ((i=0) /\ g[24]) \/ ((i=1) /\ g[25]) \/ ((i=2) /\ g[26]) \/ ((i=3) /\ g[27]) \/ ((i=4) /\ g[28]) \/ ((i=5) /\ g[29]) \/ ((i=6) /\ g[30]) \/ ((i=7) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b23] /\
( ((i=0) /\ g[23]) \/ ((i=1) /\ g[24]) \/ ((i=2) /\ g[25]) \/ ((i=3) /\ g[26]) \/ ((i=4) /\ g[27]) \/ ((i=5) /\ g[28]) \/ ((i=6) /\ g[29]) \/ ((i=7) /\ g[30]) \/ ((i=8) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b22] /\
( ((i=0) /\ g[22]) \/ ((i=1) /\ g[23]) \/ ((i=2) /\ g[24]) \/ ((i=3) /\ g[25]) \/ ((i=4) /\ g[26]) \/ ((i=5) /\ g[27]) \/ ((i=6) /\ g[28]) \/ ((i=7) /\ g[29]) \/ ((i=8) /\ g[30]) \/ ((i=9) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b21] /\
( ((i=0) /\ g[21]) \/ ((i=1) /\ g[22]) \/ ((i=2) /\ g[23]) \/ ((i=3) /\ g[24]) \/ ((i=4) /\ g[25]) \/ ((i=5) /\ g[26]) \/ ((i=6) /\ g[27]) \/ ((i=7) /\ g[28]) \/ ((i=8) /\ g[29]) \/ ((i=9) /\ g[30]) \/ ((i=10) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b20] /\
( ((i=0) /\ g[20]) \/ ((i=1) /\ g[21]) \/ ((i=2) /\ g[22]) \/ ((i=3) /\ g[23]) \/ ((i=4) /\ g[24]) \/ ((i=5) /\ g[25]) \/ ((i=6) /\ g[26]) \/ ((i=7) /\ g[27]) \/ ((i=8) /\ g[28]) \/ ((i=9) /\ g[29]) \/ ((i=10) /\ g[30]) \/ ((i=11) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b19] /\
( ((i=0) /\ g[19]) \/ ((i=1) /\ g[20]) \/ ((i=2) /\ g[21]) \/ ((i=3) /\ g[22]) \/ ((i=4) /\ g[23]) \/ ((i=5) /\ g[24]) \/ ((i=6) /\ g[25]) \/ ((i=7) /\ g[26]) \/ ((i=8) /\ g[27]) \/ ((i=9) /\ g[28]) \/ ((i=10) /\ g[29]) \/ ((i=11) /\ g[30]) \/ ((i=12) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b18] /\
( ((i=0) /\ g[18]) \/ ((i=1) /\ g[19]) \/ ((i=2) /\ g[20]) \/ ((i=3) /\ g[21]) \/ ((i=4) /\ g[22]) \/ ((i=5) /\ g[23]) \/ ((i=6) /\ g[24]) \/ ((i=7) /\ g[25]) \/ ((i=8) /\ g[26]) \/ ((i=9) /\ g[27]) \/ ((i=10) /\ g[28]) \/ ((i=11) /\ g[29]) \/ ((i=12) /\ g[30]) \/ ((i=13) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b17] /\
( ((i=0) /\ g[17]) \/ ((i=1) /\ g[18]) \/ ((i=2) /\ g[19]) \/ ((i=3) /\ g[20]) \/ ((i=4) /\ g[21]) \/ ((i=5) /\ g[22]) \/ ((i=6) /\ g[23]) \/ ((i=7) /\ g[24]) \/ ((i=8) /\ g[25]) \/ ((i=9) /\ g[26]) \/ ((i=10) /\ g[27]) \/ ((i=11) /\ g[28]) \/ ((i=12) /\ g[29]) \/ ((i=13) /\ g[30]) \/ ((i=14) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b16] /\
( ((i=0) /\ g[16]) \/ ((i=1) /\ g[17]) \/ ((i=2) /\ g[18]) \/ ((i=3) /\ g[19]) \/ ((i=4) /\ g[20]) \/ ((i=5) /\ g[21]) \/ ((i=6) /\ g[22]) \/ ((i=7) /\ g[23]) \/ ((i=8) /\ g[24]) \/ ((i=9) /\ g[25]) \/ ((i=10) /\ g[26]) \/ ((i=11) /\ g[27]) \/ ((i=12) /\ g[28]) \/ ((i=13) /\ g[29]) \/ ((i=14) /\ g[30]) \/ ((i=15) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b15] /\
( ((i=0) /\ g[15]) \/ ((i=1) /\ g[16]) \/ ((i=2) /\ g[17]) \/ ((i=3) /\ g[18]) \/ ((i=4) /\ g[19]) \/ ((i=5) /\ g[20]) \/ ((i=6) /\ g[21]) \/ ((i=7) /\ g[22]) \/ ((i=8) /\ g[23]) \/ ((i=9) /\ g[24]) \/ ((i=10) /\ g[25]) \/ ((i=11) /\ g[26]) \/ ((i=12) /\ g[27]) \/ ((i=13) /\ g[28]) \/ ((i=14) /\ g[29]) \/ ((i=15) /\ g[30]) \/ ((i=16) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b14] /\
( ((i=0) /\ g[14]) \/ ((i=1) /\ g[15]) \/ ((i=2) /\ g[16]) \/ ((i=3) /\ g[17]) \/ ((i=4) /\ g[18]) \/ ((i=5) /\ g[19]) \/ ((i=6) /\ g[20]) \/ ((i=7) /\ g[21]) \/ ((i=8) /\ g[22]) \/ ((i=9) /\ g[23]) \/ ((i=10) /\ g[24]) \/ ((i=11) /\ g[25]) \/ ((i=12) /\ g[26]) \/ ((i=13) /\ g[27]) \/ ((i=14) /\ g[28]) \/ ((i=15) /\ g[29]) \/ ((i=16) /\ g[30]) \/ ((i=17) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b13] /\
( ((i=0) /\ g[13]) \/ ((i=1) /\ g[14]) \/ ((i=2) /\ g[15]) \/ ((i=3) /\ g[16]) \/ ((i=4) /\ g[17]) \/ ((i=5) /\ g[18]) \/ ((i=6) /\ g[19]) \/ ((i=7) /\ g[20]) \/ ((i=8) /\ g[21]) \/ ((i=9) /\ g[22]) \/ ((i=10) /\ g[23]) \/ ((i=11) /\ g[24]) \/ ((i=12) /\ g[25]) \/ ((i=13) /\ g[26]) \/ ((i=14) /\ g[27]) \/ ((i=15) /\ g[28]) \/ ((i=16) /\ g[29]) \/ ((i=17) /\ g[30]) \/ ((i=18) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b12] /\
( ((i=0) /\ g[12]) \/ ((i=1) /\ g[13]) \/ ((i=2) /\ g[14]) \/ ((i=3) /\ g[15]) \/ ((i=4) /\ g[16]) \/ ((i=5) /\ g[17]) \/ ((i=6) /\ g[18]) \/ ((i=7) /\ g[19]) \/ ((i=8) /\ g[20]) \/ ((i=9) /\ g[21]) \/ ((i=10) /\ g[22]) \/ ((i=11) /\ g[23]) \/ ((i=12) /\ g[24]) \/ ((i=13) /\ g[25]) \/ ((i=14) /\ g[26]) \/ ((i=15) /\ g[27]) \/ ((i=16) /\ g[28]) \/ ((i=17) /\ g[29]) \/ ((i=18) /\ g[30]) \/ ((i=19) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b11] /\
( ((i=0) /\ g[11]) \/ ((i=1) /\ g[12]) \/ ((i=2) /\ g[13]) \/ ((i=3) /\ g[14]) \/ ((i=4) /\ g[15]) \/ ((i=5) /\ g[16]) \/ ((i=6) /\ g[17]) \/ ((i=7) /\ g[18]) \/ ((i=8) /\ g[19]) \/ ((i=9) /\ g[20]) \/ ((i=10) /\ g[21]) \/ ((i=11) /\ g[22]) \/ ((i=12) /\ g[23]) \/ ((i=13) /\ g[24]) \/ ((i=14) /\ g[25]) \/ ((i=15) /\ g[26]) \/ ((i=16) /\ g[27]) \/ ((i=17) /\ g[28]) \/ ((i=18) /\ g[29]) \/ ((i=19) /\ g[30]) \/ ((i=20) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b10] /\
( ((i=0) /\ g[10]) \/ ((i=1) /\ g[11]) \/ ((i=2) /\ g[12]) \/ ((i=3) /\ g[13]) \/ ((i=4) /\ g[14]) \/ ((i=5) /\ g[15]) \/ ((i=6) /\ g[16]) \/ ((i=7) /\ g[17]) \/ ((i=8) /\ g[18]) \/ ((i=9) /\ g[19]) \/ ((i=10) /\ g[20]) \/ ((i=11) /\ g[21]) \/ ((i=12) /\ g[22]) \/ ((i=13) /\ g[23]) \/ ((i=14) /\ g[24]) \/ ((i=15) /\ g[25]) \/ ((i=16) /\ g[26]) \/ ((i=17) /\ g[27]) \/ ((i=18) /\ g[28]) \/ ((i=19) /\ g[29]) \/ ((i=20) /\ g[30]) \/ ((i=21) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b9] /\
( ((i=0) /\ g[9]) \/ ((i=1) /\ g[10]) \/ ((i=2) /\ g[11]) \/ ((i=3) /\ g[12]) \/ ((i=4) /\ g[13]) \/ ((i=5) /\ g[14]) \/ ((i=6) /\ g[15]) \/ ((i=7) /\ g[16]) \/ ((i=8) /\ g[17]) \/ ((i=9) /\ g[18]) \/ ((i=10) /\ g[19]) \/ ((i=11) /\ g[20]) \/ ((i=12) /\ g[21]) \/ ((i=13) /\ g[22]) \/ ((i=14) /\ g[23]) \/ ((i=15) /\ g[24]) \/ ((i=16) /\ g[25]) \/ ((i=17) /\ g[26]) \/ ((i=18) /\ g[27]) \/ ((i=19) /\ g[28]) \/ ((i=20) /\ g[29]) \/ ((i=21) /\ g[30]) \/ ((i=22) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b8] /\
( ((i=0) /\ g[8]) \/ ((i=1) /\ g[9]) \/ ((i=2) /\ g[10]) \/ ((i=3) /\ g[11]) \/ ((i=4) /\ g[12]) \/ ((i=5) /\ g[13]) \/ ((i=6) /\ g[14]) \/ ((i=7) /\ g[15]) \/ ((i=8) /\ g[16]) \/ ((i=9) /\ g[17]) \/ ((i=10) /\ g[18]) \/ ((i=11) /\ g[19]) \/ ((i=12) /\ g[20]) \/ ((i=13) /\ g[21]) \/ ((i=14) /\ g[22]) \/ ((i=15) /\ g[23]) \/ ((i=16) /\ g[24]) \/ ((i=17) /\ g[25]) \/ ((i=18) /\ g[26]) \/ ((i=19) /\ g[27]) \/ ((i=20) /\ g[28]) \/ ((i=21) /\ g[29]) \/ ((i=22) /\ g[30]) \/ ((i=23) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b7] /\
( ((i=0) /\ g[7]) \/ ((i=1) /\ g[8]) \/ ((i=2) /\ g[9]) \/ ((i=3) /\ g[10]) \/ ((i=4) /\ g[11]) \/ ((i=5) /\ g[12]) \/ ((i=6) /\ g[13]) \/ ((i=7) /\ g[14]) \/ ((i=8) /\ g[15]) \/ ((i=9) /\ g[16]) \/ ((i=10) /\ g[17]) \/ ((i=11) /\ g[18]) \/ ((i=12) /\ g[19]) \/ ((i=13) /\ g[20]) \/ ((i=14) /\ g[21]) \/ ((i=15) /\ g[22]) \/ ((i=16) /\ g[23]) \/ ((i=17) /\ g[24]) \/ ((i=18) /\ g[25]) \/ ((i=19) /\ g[26]) \/ ((i=20) /\ g[27]) \/ ((i=21) /\ g[28]) \/ ((i=22) /\ g[29]) \/ ((i=23) /\ g[30]) \/ ((i=24) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b6] /\
( ((i=0) /\ g[6]) \/ ((i=1) /\ g[7]) \/ ((i=2) /\ g[8]) \/ ((i=3) /\ g[9]) \/ ((i=4) /\ g[10]) \/ ((i=5) /\ g[11]) \/ ((i=6) /\ g[12]) \/ ((i=7) /\ g[13]) \/ ((i=8) /\ g[14]) \/ ((i=9) /\ g[15]) \/ ((i=10) /\ g[16]) \/ ((i=11) /\ g[17]) \/ ((i=12) /\ g[18]) \/ ((i=13) /\ g[19]) \/ ((i=14) /\ g[20]) \/ ((i=15) /\ g[21]) \/ ((i=16) /\ g[22]) \/ ((i=17) /\ g[23]) \/ ((i=18) /\ g[24]) \/ ((i=19) /\ g[25]) \/ ((i=20) /\ g[26]) \/ ((i=21) /\ g[27]) \/ ((i=22) /\ g[28]) \/ ((i=23) /\ g[29]) \/ ((i=24) /\ g[30]) \/ ((i=25) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b5] /\
( ((i=0) /\ g[5]) \/ ((i=1) /\ g[6]) \/ ((i=2) /\ g[7]) \/ ((i=3) /\ g[8]) \/ ((i=4) /\ g[9]) \/ ((i=5) /\ g[10]) \/ ((i=6) /\ g[11]) \/ ((i=7) /\ g[12]) \/ ((i=8) /\ g[13]) \/ ((i=9) /\ g[14]) \/ ((i=10) /\ g[15]) \/ ((i=11) /\ g[16]) \/ ((i=12) /\ g[17]) \/ ((i=13) /\ g[18]) \/ ((i=14) /\ g[19]) \/ ((i=15) /\ g[20]) \/ ((i=16) /\ g[21]) \/ ((i=17) /\ g[22]) \/ ((i=18) /\ g[23]) \/ ((i=19) /\ g[24]) \/ ((i=20) /\ g[25]) \/ ((i=21) /\ g[26]) \/ ((i=22) /\ g[27]) \/ ((i=23) /\ g[28]) \/ ((i=24) /\ g[29]) \/ ((i=25) /\ g[30]) \/ ((i=26) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b4] /\
( ((i=0) /\ g[4]) \/ ((i=1) /\ g[5]) \/ ((i=2) /\ g[6]) \/ ((i=3) /\ g[7]) \/ ((i=4) /\ g[8]) \/ ((i=5) /\ g[9]) \/ ((i=6) /\ g[10]) \/ ((i=7) /\ g[11]) \/ ((i=8) /\ g[12]) \/ ((i=9) /\ g[13]) \/ ((i=10) /\ g[14]) \/ ((i=11) /\ g[15]) \/ ((i=12) /\ g[16]) \/ ((i=13) /\ g[17]) \/ ((i=14) /\ g[18]) \/ ((i=15) /\ g[19]) \/ ((i=16) /\ g[20]) \/ ((i=17) /\ g[21]) \/ ((i=18) /\ g[22]) \/ ((i=19) /\ g[23]) \/ ((i=20) /\ g[24]) \/ ((i=21) /\ g[25]) \/ ((i=22) /\ g[26]) \/ ((i=23) /\ g[27]) \/ ((i=24) /\ g[28]) \/ ((i=25) /\ g[29]) \/ ((i=26) /\ g[30]) \/ ((i=27) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b3] /\
( ((i=0) /\ g[3]) \/ ((i=1) /\ g[4]) \/ ((i=2) /\ g[5]) \/ ((i=3) /\ g[6]) \/ ((i=4) /\ g[7]) \/ ((i=5) /\ g[8]) \/ ((i=6) /\ g[9]) \/ ((i=7) /\ g[10]) \/ ((i=8) /\ g[11]) \/ ((i=9) /\ g[12]) \/ ((i=10) /\ g[13]) \/ ((i=11) /\ g[14]) \/ ((i=12) /\ g[15]) \/ ((i=13) /\ g[16]) \/ ((i=14) /\ g[17]) \/ ((i=15) /\ g[18]) \/ ((i=16) /\ g[19]) \/ ((i=17) /\ g[20]) \/ ((i=18) /\ g[21]) \/ ((i=19) /\ g[22]) \/ ((i=20) /\ g[23]) \/ ((i=21) /\ g[24]) \/ ((i=22) /\ g[25]) \/ ((i=23) /\ g[26]) \/ ((i=24) /\ g[27]) \/ ((i=25) /\ g[28]) \/ ((i=26) /\ g[29]) \/ ((i=27) /\ g[30]) \/ ((i=28) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b2] /\
( ((i=0) /\ g[2]) \/ ((i=1) /\ g[3]) \/ ((i=2) /\ g[4]) \/ ((i=3) /\ g[5]) \/ ((i=4) /\ g[6]) \/ ((i=5) /\ g[7]) \/ ((i=6) /\ g[8]) \/ ((i=7) /\ g[9]) \/ ((i=8) /\ g[10]) \/ ((i=9) /\ g[11]) \/ ((i=10) /\ g[12]) \/ ((i=11) /\ g[13]) \/ ((i=12) /\ g[14]) \/ ((i=13) /\ g[15]) \/ ((i=14) /\ g[16]) \/ ((i=15) /\ g[17]) \/ ((i=16) /\ g[18]) \/ ((i=17) /\ g[19]) \/ ((i=18) /\ g[20]) \/ ((i=19) /\ g[21]) \/ ((i=20) /\ g[22]) \/ ((i=21) /\ g[23]) \/ ((i=22) /\ g[24]) \/ ((i=23) /\ g[25]) \/ ((i=24) /\ g[26]) \/ ((i=25) /\ g[27]) \/ ((i=26) /\ g[28]) \/ ((i=27) /\ g[29]) \/ ((i=28) /\ g[30]) \/ ((i=29) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b1] /\
( ((i=0) /\ g[1]) \/ ((i=1) /\ g[2]) \/ ((i=2) /\ g[3]) \/ ((i=3) /\ g[4]) \/ ((i=4) /\ g[5]) \/ ((i=5) /\ g[6]) \/ ((i=6) /\ g[7]) \/ ((i=7) /\ g[8]) \/ ((i=8) /\ g[9]) \/ ((i=9) /\ g[10]) \/ ((i=10) /\ g[11]) \/ ((i=11) /\ g[12]) \/ ((i=12) /\ g[13]) \/ ((i=13) /\ g[14]) \/ ((i=14) /\ g[15]) \/ ((i=15) /\ g[16]) \/ ((i=16) /\ g[17]) \/ ((i=17) /\ g[18]) \/ ((i=18) /\ g[19]) \/ ((i=19) /\ g[20]) \/ ((i=20) /\ g[21]) \/ ((i=21) /\ g[22]) \/ ((i=22) /\ g[23]) \/ ((i=23) /\ g[24]) \/ ((i=24) /\ g[25]) \/ ((i=25) /\ g[26]) \/ ((i=26) /\ g[27]) \/ ((i=27) /\ g[28]) \/ ((i=28) /\ g[29]) \/ ((i=29) /\ g[30]) \/ ((i=30) /\ g[31]) )
) \/
(CMP32[AND32[f][b31]][b0] /\ g[i])
]]]
(*
xR11[0,32] := { (xR8==69) (xR13[0,32]) } +
{ [xR8==194] [(0 ≤ xR12[15,23] ≤ 2) (xR12[28,32]) + (xR12[15,23]==59) (xR12[32,40])] } +
{ (xR8==192) (xR12[15,23]==32) (xR13[32,64]) } +
{ ~(xR8==69) ~(xR8==192) ~(xR8==194) (xR11[0,32]) }
xR11 := { (xR8==128) (RCF[3,5]==0) (RIP)mem } +
{ ~(xR8==128) (xR11) }
*)
\* xR12[15,22]
xR12_15_22 == [i \in 0..63 |-> ((i=0) /\ xR12[15]) \/ ((i=1) /\ xR12[16]) \/ ((i=2) /\ xR12[17]) \/ ((i=3) /\ xR12[18]) \/ ((i=4) /\ xR12[19]) \/ ((i=5) /\ xR12[20]) \/ ((i=6) /\ xR12[21]) \/ ((i=7) /\ xR12[22])]
\* xR12[28,31]
xR12_28_31 == [i \in 0..63 |-> ((i=0) /\ xR12[28]) \/ ((i=1) /\ xR12[29]) \/ ((i=2) /\ xR12[30]) \/ ((i=3) /\ xR12[31])]
\* xR12[32,39]
xR12_32_39 == [i \in 0..63 |-> ((i=0) /\ xR12[32]) \/ ((i=1) /\ xR12[33]) \/ ((i=2) /\ xR12[34]) \/ ((i=3) /\ xR12[35]) \/ ((i=4) /\ xR12[36]) \/ ((i=5) /\ xR12[37]) \/ ((i=6) /\ xR12[38]) \/ ((i=7) /\ xR12[39])]
\* xR13[32,63]
xR13_32_63 ==[i \in 0..63 |-> ((i=0) /\ xR13[32]) \/ ((i=1) /\ xR13[33]) \/ ((i=2) /\ xR13[34]) \/ ((i=3) /\ xR13[35]) \/ ((i=4) /\ xR13[36]) \/ ((i=5) /\ xR13[37]) \/ ((i=6) /\ xR13[38]) \/ ((i=7) /\ xR13[39]) \/ ((i=8) /\ xR13[40]) \/ ((i=9) /\ xR13[41]) \/ ((i=10) /\ xR13[42]) \/ ((i=11) /\ xR13[43]) \/ ((i=12) /\ xR13[44]) \/ ((i=13) /\ xR13[45]) \/ ((i=14) /\ xR13[46]) \/ ((i=15) /\ xR13[47]) \/ ((i=16) /\ xR13[48]) \/ ((i=17) /\ xR13[49]) \/ ((i=18) /\ xR13[50]) \/ ((i=19) /\ xR13[51]) \/ ((i=20) /\ xR13[52]) \/ ((i=21) /\ xR13[53]) \/ ((i=22) /\ xR13[54]) \/ ((i=23) /\ xR13[55]) \/ ((i=24) /\ xR13[56]) \/ ((i=25) /\ xR13[57]) \/ ((i=26) /\ xR13[58]) \/ ((i=27) /\ xR13[59]) \/ ((i=28) /\ xR13[60]) \/ ((i=29) /\ xR13[61]) \/ ((i=30) /\ xR13[62]) \/ ((i=31) /\ xR13[63]) ]
\* RCF[3,4]
RCF_3_4 == [i \in 0..63 |-> ((i=0) /\ RCF[3]) \/ ((i=1) /\ RCF[4])]
\* (0 ≤ xR12[15,22] ≤ 2)
zero_gte_xR12_15_22_lte_two == CMP64[xR12_15_22][b0] \/ CMP64[xR12_15_22][b1] \/ CMP64[xR12_15_22][b2]
xR11 == [ i \in 0..63 |->
(
\* xR11[0,31]
((i >= 0) /\ (i <= 31)) /\
(
\* (xR8=69) /\ (xR13[0,31])
(CMP64[xR8][b69] /\ xR13[i]) \/
\* (xR8=194) /\ [(0 ≤ xR12[15,22] ≤ 2) /\ (xR12[28,31]) \/ (xR12[15,22]=59) /\ (xR12[32,39])]
(CMP64[xR8][b194] /\ ( (zero_gte_xR12_15_22_lte_two /\ xR12_28_31[i]) \/ (CMP64[xR12_15_22][b59] /\ xR12_32_39[i]))) \/
\* (xR8=192) /\ (xR12[15,22]=32) /\ xR13[32,63]
(CMP64[xR8][b192] /\ CMP64[xR12_15_22][b32] /\ xR13_32_63[i]) \/
\* (xR8=128) /\ (RCF[3,4]=0) /\ MEM[RIP]
(CMP64[xR8][b128] /\ CMP64[RCF_3_4][b0] /\ MEM[BIN32[RIP]][i]) \/
\* ~(xR8=69) /\ ~(xR8=192) /\ ~(xR8=194) /\ ~(xR8=128) /\ xR11[0,31]
(~CMP64[xR8][b69] /\ ~CMP64[xR8][b194] /\ ~CMP64[xR8][b192] /\ ~CMP64[xR8][b128] /\ xR11[i])
)
) \/
(
\* xR11[32,63]
((i >= 32) /\ (i <= 63)) /\
(
\* (xR8=128) /\ (RCF[3,4]=0) /\ MEM[RIP]
(CMP64[xR8][b128] /\ CMP64[RCF_3_4][b0] /\ MEM[BIN32[RIP]][i]) \/
\* ~(xR8=128) /\ (xR11)
(~CMP64[xR8][b128] /\ xR11[i])
)
)]
(*
INSTRUCTION_FORMAT_CORRECT :=
[
[0 ≤ xR11[0,8] ≤ 2] [(xR11[23,27]==1) + (xR11[23,27]==2) + (xR11[23,27]==4) + (xR11[23,27]==8)] [xR11[59,64]==0] +
[9 ≤ xR11[0,8] ≤ 10] [xR11[50,64]==0] + [17 ≤ xR11[0,8] ≤ 33] [xR11[18,64]==0] + [xR11[0,8]==44] [xR11[45,64]==0] +
[51 ≤ xR11[0,8] ≤ 53] [xR11[13,64]==0] + [xR11[0,8]==59] [xR11[16,64]==0] + [60 ≤ xR11[0,8] ≤ 67] [xR11[40,64]==0] +
[76 ≤ xR11[0,8] ≤ 78] [xR11[8,64]==0]
]
*)
\* xR11[0,7]
xR11_0_7 == [i \in 0..63 |-> (i>=0) /\ (i<=7) /\ xR11[i]]
\* xR11[8,63]
xR11_8_63 == [i \in 0..63 |-> ((i=0) /\ xR11[8]) \/ ((i=1) /\ xR11[9]) \/ ((i=2) /\ xR11[10]) \/ ((i=3) /\ xR11[11]) \/ ((i=4) /\ xR11[12]) \/ ((i=5) /\ xR11[13]) \/ ((i=6) /\ xR11[14]) \/ ((i=7) /\ xR11[15]) \/ ((i=8) /\ xR11[16]) \/ ((i=9) /\ xR11[17]) \/ ((i=10) /\ xR11[18]) \/ ((i=11) /\ xR11[19]) \/ ((i=12) /\ xR11[20]) \/ ((i=13) /\ xR11[21]) \/ ((i=14) /\ xR11[22]) \/ ((i=15) /\ xR11[23]) \/ ((i=16) /\ xR11[24]) \/ ((i=17) /\ xR11[25]) \/ ((i=18) /\ xR11[26]) \/ ((i=19) /\ xR11[27]) \/ ((i=20) /\ xR11[28]) \/ ((i=21) /\ xR11[29]) \/ ((i=22) /\ xR11[30]) \/ ((i=23) /\ xR11[31]) \/ ((i=24) /\ xR11[32]) \/ ((i=25) /\ xR11[33]) \/ ((i=26) /\ xR11[34]) \/ ((i=27) /\ xR11[35]) \/ ((i=28) /\ xR11[36]) \/ ((i=29) /\ xR11[37]) \/ ((i=30) /\ xR11[38]) \/ ((i=31) /\ xR11[39]) \/ ((i=32) /\ xR11[40]) \/ ((i=33) /\ xR11[41]) \/ ((i=34) /\ xR11[42]) \/ ((i=35) /\ xR11[43]) \/ ((i=36) /\ xR11[44]) \/ ((i=37) /\ xR11[45]) \/ ((i=38) /\ xR11[46]) \/ ((i=39) /\ xR11[47]) \/ ((i=40) /\ xR11[48]) \/ ((i=41) /\ xR11[49]) \/ ((i=42) /\ xR11[50]) \/ ((i=43) /\ xR11[51]) \/ ((i=44) /\ xR11[52]) \/ ((i=45) /\ xR11[53]) \/ ((i=46) /\ xR11[54]) \/ ((i=47) /\ xR11[55]) \/ ((i=48) /\ xR11[56]) \/ ((i=49) /\ xR11[57]) \/ ((i=50) /\ xR11[58]) \/ ((i=51) /\ xR11[59]) \/ ((i=52) /\ xR11[60]) \/ ((i=53) /\ xR11[61]) \/ ((i=54) /\ xR11[62]) \/ ((i=55) /\ xR11[63])]
\* xR11[13,63]
xR11_13_63 == [i \in 0..63 |-> ((i=0) /\ xR11[13]) \/ ((i=1) /\ xR11[14]) \/ ((i=2) /\ xR11[15]) \/ ((i=3) /\ xR11[16]) \/ ((i=4) /\ xR11[17]) \/ ((i=5) /\ xR11[18]) \/ ((i=6) /\ xR11[19]) \/ ((i=7) /\ xR11[20]) \/ ((i=8) /\ xR11[21]) \/ ((i=9) /\ xR11[22]) \/ ((i=10) /\ xR11[23]) \/ ((i=11) /\ xR11[24]) \/ ((i=12) /\ xR11[25]) \/ ((i=13) /\ xR11[26]) \/ ((i=14) /\ xR11[27]) \/ ((i=15) /\ xR11[28]) \/ ((i=16) /\ xR11[29]) \/ ((i=17) /\ xR11[30]) \/ ((i=18) /\ xR11[31]) \/ ((i=19) /\ xR11[32]) \/ ((i=20) /\ xR11[33]) \/ ((i=21) /\ xR11[34]) \/ ((i=22) /\ xR11[35]) \/ ((i=23) /\ xR11[36]) \/ ((i=24) /\ xR11[37]) \/ ((i=25) /\ xR11[38]) \/ ((i=26) /\ xR11[39]) \/ ((i=27) /\ xR11[40]) \/ ((i=28) /\ xR11[41]) \/ ((i=29) /\ xR11[42]) \/ ((i=30) /\ xR11[43]) \/ ((i=31) /\ xR11[44]) \/ ((i=32) /\ xR11[45]) \/ ((i=33) /\ xR11[46]) \/ ((i=34) /\ xR11[47]) \/ ((i=35) /\ xR11[48]) \/ ((i=36) /\ xR11[49]) \/ ((i=37) /\ xR11[50]) \/ ((i=38) /\ xR11[51]) \/ ((i=39) /\ xR11[52]) \/ ((i=40) /\ xR11[53]) \/ ((i=41) /\ xR11[54]) \/ ((i=42) /\ xR11[55]) \/ ((i=43) /\ xR11[56]) \/ ((i=44) /\ xR11[57]) \/ ((i=45) /\ xR11[58]) \/ ((i=46) /\ xR11[59]) \/ ((i=47) /\ xR11[60]) \/ ((i=48) /\ xR11[61]) \/ ((i=49) /\ xR11[62]) \/ ((i=50) /\ xR11[63])]
\* xR11[16,63]
xR11_16_63 == [i \in 0..63 |-> ((i=0) /\ xR11[16]) \/ ((i=1) /\ xR11[17]) \/ ((i=2) /\ xR11[18]) \/ ((i=3) /\ xR11[19]) \/ ((i=4) /\ xR11[20]) \/ ((i=5) /\ xR11[21]) \/ ((i=6) /\ xR11[22]) \/ ((i=7) /\ xR11[23]) \/ ((i=8) /\ xR11[24]) \/ ((i=9) /\ xR11[25]) \/ ((i=10) /\ xR11[26]) \/ ((i=11) /\ xR11[27]) \/ ((i=12) /\ xR11[28]) \/ ((i=13) /\ xR11[29]) \/ ((i=14) /\ xR11[30]) \/ ((i=15) /\ xR11[31]) \/ ((i=16) /\ xR11[32]) \/ ((i=17) /\ xR11[33]) \/ ((i=18) /\ xR11[34]) \/ ((i=19) /\ xR11[35]) \/ ((i=20) /\ xR11[36]) \/ ((i=21) /\ xR11[37]) \/ ((i=22) /\ xR11[38]) \/ ((i=23) /\ xR11[39]) \/ ((i=24) /\ xR11[40]) \/ ((i=25) /\ xR11[41]) \/ ((i=26) /\ xR11[42]) \/ ((i=27) /\ xR11[43]) \/ ((i=28) /\ xR11[44]) \/ ((i=29) /\ xR11[45]) \/ ((i=30) /\ xR11[46]) \/ ((i=31) /\ xR11[47]) \/ ((i=32) /\ xR11[48]) \/ ((i=33) /\ xR11[49]) \/ ((i=34) /\ xR11[50]) \/ ((i=35) /\ xR11[51]) \/ ((i=36) /\ xR11[52]) \/ ((i=37) /\ xR11[53]) \/ ((i=38) /\ xR11[54]) \/ ((i=39) /\ xR11[55]) \/ ((i=40) /\ xR11[56]) \/ ((i=41) /\ xR11[57]) \/ ((i=42) /\ xR11[58]) \/ ((i=43) /\ xR11[59]) \/ ((i=44) /\ xR11[60]) \/ ((i=45) /\ xR11[61]) \/ ((i=46) /\ xR11[62]) \/ ((i=47) /\ xR11[63])]
\* xR11[18,63]
xR11_18_63 == [i \in 0..63 |-> ((i=0) /\ xR11[18]) \/ ((i=1) /\ xR11[19]) \/ ((i=2) /\ xR11[20]) \/ ((i=3) /\ xR11[21]) \/ ((i=4) /\ xR11[22]) \/ ((i=5) /\ xR11[23]) \/ ((i=6) /\ xR11[24]) \/ ((i=7) /\ xR11[25]) \/ ((i=8) /\ xR11[26]) \/ ((i=9) /\ xR11[27]) \/ ((i=10) /\ xR11[28]) \/ ((i=11) /\ xR11[29]) \/ ((i=12) /\ xR11[30]) \/ ((i=13) /\ xR11[31]) \/ ((i=14) /\ xR11[32]) \/ ((i=15) /\ xR11[33]) \/ ((i=16) /\ xR11[34]) \/ ((i=17) /\ xR11[35]) \/ ((i=18) /\ xR11[36]) \/ ((i=19) /\ xR11[37]) \/ ((i=20) /\ xR11[38]) \/ ((i=21) /\ xR11[39]) \/ ((i=22) /\ xR11[40]) \/ ((i=23) /\ xR11[41]) \/ ((i=24) /\ xR11[42]) \/ ((i=25) /\ xR11[43]) \/ ((i=26) /\ xR11[44]) \/ ((i=27) /\ xR11[45]) \/ ((i=28) /\ xR11[46]) \/ ((i=29) /\ xR11[47]) \/ ((i=30) /\ xR11[48]) \/ ((i=31) /\ xR11[49]) \/ ((i=32) /\ xR11[50]) \/ ((i=33) /\ xR11[51]) \/ ((i=34) /\ xR11[52]) \/ ((i=35) /\ xR11[53]) \/ ((i=36) /\ xR11[54]) \/ ((i=37) /\ xR11[55]) \/ ((i=38) /\ xR11[56]) \/ ((i=39) /\ xR11[57]) \/ ((i=40) /\ xR11[58]) \/ ((i=41) /\ xR11[59]) \/ ((i=42) /\ xR11[60]) \/ ((i=43) /\ xR11[61]) \/ ((i=44) /\ xR11[62]) \/ ((i=45) /\ xR11[63])]
\* xR11[23,26]
xR11_23_26 == [i \in 0..63 |-> ((i=0) /\ xR11[23]) \/ ((i=1) /\ xR11[24]) \/ ((i=2) /\ xR11[25]) \/ ((i=3) /\ xR11[26])]
\* xR11[40,63]
xR11_40_63 == [i \in 0..63 |-> ((i=0) /\ xR11[40]) \/ ((i=1) /\ xR11[41]) \/ ((i=2) /\ xR11[42]) \/ ((i=3) /\ xR11[43]) \/ ((i=4) /\ xR11[44]) \/ ((i=5) /\ xR11[45]) \/ ((i=6) /\ xR11[46]) \/ ((i=7) /\ xR11[47]) \/ ((i=8) /\ xR11[48]) \/ ((i=9) /\ xR11[49]) \/ ((i=10) /\ xR11[50]) \/ ((i=11) /\ xR11[51]) \/ ((i=12) /\ xR11[52]) \/ ((i=13) /\ xR11[53]) \/ ((i=14) /\ xR11[54]) \/ ((i=15) /\ xR11[55]) \/ ((i=16) /\ xR11[56]) \/ ((i=17) /\ xR11[57]) \/ ((i=18) /\ xR11[58]) \/ ((i=19) /\ xR11[59]) \/ ((i=20) /\ xR11[60]) \/ ((i=21) /\ xR11[61]) \/ ((i=22) /\ xR11[62]) \/ ((i=23) /\ xR11[63])]
\* xR11[45,63]
xR11_45_63 == [i \in 0..63 |-> ((i=0) /\ xR11[45]) \/ ((i=1) /\ xR11[46]) \/ ((i=2) /\ xR11[47]) \/ ((i=3) /\ xR11[48]) \/ ((i=4) /\ xR11[49]) \/ ((i=5) /\ xR11[50]) \/ ((i=6) /\ xR11[51]) \/ ((i=7) /\ xR11[52]) \/ ((i=8) /\ xR11[53]) \/ ((i=9) /\ xR11[54]) \/ ((i=10) /\ xR11[55]) \/ ((i=11) /\ xR11[56]) \/ ((i=12) /\ xR11[57]) \/ ((i=13) /\ xR11[58]) \/ ((i=14) /\ xR11[59]) \/ ((i=15) /\ xR11[60]) \/ ((i=16) /\ xR11[61]) \/ ((i=17) /\ xR11[62]) \/ ((i=18) /\ xR11[63])]
\* xR11[50,63]
xR11_50_63 == [i \in 0..63 |-> ((i=0) /\ xR11[50]) \/ ((i=1) /\ xR11[51]) \/ ((i=2) /\ xR11[52]) \/ ((i=3) /\ xR11[53]) \/ ((i=4) /\ xR11[54]) \/ ((i=5) /\ xR11[55]) \/ ((i=6) /\ xR11[56]) \/ ((i=7) /\ xR11[57]) \/ ((i=8) /\ xR11[58]) \/ ((i=9) /\ xR11[59]) \/ ((i=10) /\ xR11[60]) \/ ((i=11) /\ xR11[61]) \/ ((i=12) /\ xR11[62]) \/ ((i=13) /\ xR11[63])]
\* xR11[59,63]
xR11_59_63 == [i \in 0..63 |-> ((i=0) /\ xR11[59]) \/ ((i=1) /\ xR11[60]) \/ ((i=2) /\ xR11[61]) \/ ((i=3) /\ xR11[62]) \/ ((i=4) /\ xR11[63])]
\* (0 ≤ xR11[0,7] ≤ 2)
zero_gte_xR11_0_7_lte_two == CMP64[xR11_0_7][b0] \/ CMP64[xR11_0_7][b1] \/ CMP64[xR11_0_7][b2]
\* (9 ≤ xR11[0,7] ≤ 10)
nine_gte_xR11_0_7_lte_ten == CMP64[xR11_0_7][b9] \/ CMP64[xR11_0_7][b10]
\* (17 ≤ xR11[0,7] ≤ 33)
seventeen_gte_xR11_0_7_lte_thirtytthree == CMP64[xR11_0_7][b17] \/ CMP64[xR11_0_7][b18] \/ CMP64[xR11_0_7][b19] \/ CMP64[xR11_0_7][b20] \/ CMP64[xR11_0_7][b21] \/ CMP64[xR11_0_7][b22] \/ CMP64[xR11_0_7][b23] \/ CMP64[xR11_0_7][b24] \/ CMP64[xR11_0_7][b25] \/ CMP64[xR11_0_7][b26] \/ CMP64[xR11_0_7][b27] \/ CMP64[xR11_0_7][b28] \/ CMP64[xR11_0_7][b29] \/ CMP64[xR11_0_7][b30] \/ CMP64[xR11_0_7][b31] \/ CMP64[xR11_0_7][b32] \/ CMP64[xR11_0_7][b33]
\* (51 ≤ xR11[0,7] ≤ 53)
fiftyone_gte_xR11_0_7_lte_fiftythree == CMP64[xR11_0_7][b51] \/ CMP64[xR11_0_7][b52] \/ CMP64[xR11_0_7][b53]
\* (60 ≤ xR11[0,7] ≤ 67)
sixty_gte_xR11_0_7_lte_sixtyseven == CMP64[xR11_0_7][b60] \/ CMP64[xR11_0_7][b61] \/ CMP64[xR11_0_7][b62] \/ CMP64[xR11_0_7][b63] \/ CMP64[xR11_0_7][b64] \/ CMP64[xR11_0_7][b65] \/ CMP64[xR11_0_7][b66] \/ CMP64[xR11_0_7][b67]
\* (76 ≤ xR11[0,7] ≤ 78)
seventysix_gte_xR11_0_7_lte_seventyeight == CMP64[xR11_0_7][b76] \/ CMP64[xR11_0_7][b77] \/ CMP64[xR11_0_7][b78]
INSTRUCTION_FORMAT_CORRECT ==
\* (0 ≤ xR11[0,7] ≤ 2) /\ [(xR11[23,26]=1) \/ (xR11[23,26]=2) \/ (xR11[23,26]=4) \/ (xR11[23,26]=8)] /\ [xR11[59,63]=0]
(zero_gte_xR11_0_7_lte_two /\ (CMP64[xR11_23_26][b1] \/ CMP64[xR11_23_26][b2] \/ CMP64[xR11_23_26][b4] \/ CMP64[xR11_23_26][b8]) /\ CMP64[xR11_59_63][b0]) \/
\* [9 ≤ xR11[0,7] ≤ 10] /\ [xR11[50,63]=0] \/ [17 ≤ xR11[0,7] ≤ 33] /\ [xR11[18,63]=0] \/ [xR11[0,7]=44] /\ [xR11[45,63]=0]
(nine_gte_xR11_0_7_lte_ten /\ CMP64[xR11_50_63][b0]) \/ (seventeen_gte_xR11_0_7_lte_thirtytthree /\ CMP64[xR11_18_63][b0]) \/ (CMP64[xR11_0_7][b44] /\ CMP64[xR11_45_63][b0]) \/
\* [51 ≤ xR11[0,7] ≤ 53] /\ [xR11[13,63]=0] \/ [xR11[0,7]=59] /\ [xR11[16,63]=0] \/ [60 ≤ xR11[0,7] ≤ 67] /\ [xR11[40,63]=0]
(fiftyone_gte_xR11_0_7_lte_fiftythree /\ CMP64[xR11_13_63][b0]) \/ (CMP64[xR11_0_7][b59] /\ CMP64[xR11_16_63][b0]) \/ (sixty_gte_xR11_0_7_lte_sixtyseven /\ CMP64[xR11_40_63][b0]) \/
\* [76 ≤ xR11[0,7] ≤ 78] /\ [xR11[8,63]=0]
(seventysix_gte_xR11_0_7_lte_seventyeight /\ CMP64[xR11_8_63][b0])
(*
xR12[0,1] = { [xR8==192] [(xR12[15,23]==31) + (xR12[15,23]==33) + (xR12[15,23]==52) + (59 ≤ xR12[15,23] ≤ 60)] } +
{ (xR8==68) } + { (xR8==69) } + { (xR8==72) } +
{ (xR8==65) (xR12[0,1]) }
xR12[1,2] = { [2 ≤ xR8 ≤ 31] [~(xR13[0,32]==0) + (xR12[2,3])] [xR12[2,3]] } +
{ (xR8==65) (xR12[0,1] + xR12[1,2]) } +
{ (33 ≤ xR8 ≤ 63) (xR12[2,3]) } +
{ [(xR8==66) | (xR8==32)] [xR12[1,2]] }
xR12[2,3] = { [xR8==32] [(xR13[(xR8)(31)]) (xR14[(xR8)(31)]) + (xR12[1,2]) ((xR13[(xR8) (31)]) + (xR14[(xR8) (31)]))] } +
{ [33 ≤ xR8 ≤ 63] [(xR13[(xR8)(31)]) (xR14[(xR8)(31)]) + (xR12[2,3]) ((xR13[(xR8) (31)]) + (xR14[(xR8) (31)]))] } +
{ [(xR8==64) | (2 ≤ xR8 ≤ 31) | (xR8==71)] [xR12[2,3]] }
xR12[3,4] = { (xR8==66) (xR13[31,32]) } +
{ (32 ≤ xR8 ≤ 64) (xR12[3,4]) }
xR12[4,5] = { (xR8==66) (xR14[31,32]) } +
(32 ≤ xR8 ≤ 64) (xR12[4,5])
xR12[5,6] = { (xR8==67) ~(xR11[0,32]==0) ~(xR15[0,32]==0) ~(xR11[0,32]==1) ~(xR15[0,32]==1) (xR11[31,32]) } +
{ ~(xR8==67) (xR12[5,6]) }
xR12[6,7] = { (xR8==67) ~(xR11[0,32]==0) ~(xR15[0,32]==0) ~(xR11[0,32]==1) ~(xR15[0,32]==1) (xR15[31,32]) } +
{ ~(xR8==67) (xR12[6,7]) }
xR12[7,8] = { (xR8==193) (xR12[63,64]) } +
{ [xR8==67] [~(xR11[0,32]==0) ~(xR11[0,32]==1) (xR15[0,32]==1) (xR11[31,32]) + ~(xR15[0,32]==0) ~(xR15[0,32]==1) (xR11[0,32]==1) (xR15[31,32])] } +
{ (xR8==73) (xR13[31,32]) } +
{ [xR8==66] ~[xR12[1,2]] [~(xR13[0,32]==0) (xR14[0,32]==0) (xR13[31,32]) + (xR13[0,32]==0) ~(xR14[0,32]==0) (xR14[31,32])] } +
{ [xR8==64] ~[(xR13[31,32]) ~(xR12[3,4]) ~(xR12[4,5]) + ~(xR13[31,32]) (xR12[3,4]) (xR12[4,5])] [xR13[31,32]] } +
{ ~(xR8==64) ~(xR8==66) ~(xR8==67) ~(xR8==73) ~(xR8==193) (xR12[7,8]) }
xR12[9,10] = { (xR8==193) (xR12[32,64]==0) } +
{ [xR8==67] [(xR11[0,32]==0) + (xR15[0,32]==0)] } +
{ (xR8==73) (xR13[0,32]==0) } +
{ (xR8==66) (xR13[0,32]==0) (xR14[0,32]==0) } +
{ [xR8==64] ~[(xR13[31,32]) ~(xR12[3,4]) ~(xR12[4,5]) + ~(xR13[31,32]) (xR12[3,4]) (xR12[4,5])] [xR13[31,32]] [xR13[0,32]==0] } +
{ ~(xR8==64) ~(xR8==66) ~(xR8==67) ~(xR8==73) ~(xR8==193) (xR12[9,10]) }
xR12[15,23] = { (xR8==160) (INSTRUCTION_FORMAT_CORRECT) (xR11[0,8]) } +
{ ~(xR8==160) (xR12[15,23]) }
xR12[23,28] = { (xR8==160) (INSTRUCTION_FORMAT_CORRECT) (xR11[8,13]) } +
{ ~(xR8==160) (xR12[23,28]) }
xR12[28,32] = { (xR8==160) (INSTRUCTION_FORMAT_CORRECT) (xR11[23,27]) } +
{ ~(xR8==160) (xR12[28,32]) }
xR12[32,64] = { [xR8==224] [(xR12[15,23]==0) + (xR12[15,23]==9)] [0 ≤ xR12[32,64] ≤ 0x2000000] [(0 ≤ xR12[32,64] ≤ 0x2000000) (xR12[32,64])]mem } +
{ (xR8==225) (xR12[15,23]==59) [xR12[32,64] (xR8==225) (xR12[15,23]==59)]mem } +
{ (xR8==160) (INSTRUCTION_FORMAT_CORRECT) (xR11[8,40]) } +
{ [xR8==167] [(xR11[0,8]==44) (xR11[13,45]) + (9 ≤ xR11[0,8] < 10) (xR11[18,50]) + (0 ≤ xR11[0,8] < 2) (xR11[27,59]) ] } +
{ (xR8==194) ~(xR12[15,23]==33) ~(xR12[15,23]==59) ~(xR12[15,23]==60) (xR13[0,32]) } +
{ [xR8==192] [(xR12[15,23]==24) (xR13[32,64]) (xR14[32,64]) + (xR12[15,23]==25) ((xR13[32,64]) + (xR14[32,64])) + (xR12[15,23]==26) ((xR13[32,64]) ~(xR14[32,64]) + ~(xR13[32,64]) (xR14[32,64])) + (xR12[15,23]==27) ((xR13[32,64]) << ((xR14[32,64]) (31))) + (xR12[15,23]==28) ((xR13[32,64]) >> ((xR14[32,64]) (31))) + (xR12[15,23]==29) ((xR13[32,64]) >>> ((xR14[32,64]) (31))) + (xR12[15,23]==51) ~(xR13[32,64])] }
{ [(xR8==196) + (xR8==197)] [xR13[0,32]] } +
{ ~(xR8==160) ~(xR8==167) ~(xR8==192) ~(xR8==194) ~(xR8==196) ~(xR8==197) ~(xR8==224) ~(xR8==225) (xR12[32,64]) }
*)
xR12 == [ i \in 0..63 |->
(
\* xR12[0]
(i=0) /\
(
\* [xR8=192] /\ [(xR12[15,22]=31) \/ (xR12[15,22]=33) \/ (xR12[15,22]=52) \/ (59 ≤ xR12[15,22] ≤ 60)]
(CMP64[xR8][b192] /\ (CMP64[xR12_15_22][b31] \/ CMP64[xR12_15_22][b33] \/ CMP64[xR12_15_22][b52] \/ CMP64[xR12_15_22][b59] \/ CMP64[xR12_15_22][b60])) \/
\* (xR8=68) \/ (xR8=69) \/ (xR8=72)
(CMP64[xR8][b68] \/ CMP64[xR8][b69] \/ CMP64[xR8][b72]) \/
\* (xR8=65) /\ (xR12[0])
(CMP64[xR8][b65] /\ xR12[0])
)
) \/
(
\* xR12[1]
(i=1) /\
(
)
)
(*
xR12[0,1] = { [xR8==192] [(xR12[15,23]==31) + (xR12[15,23]==33) + (xR12[15,23]==52) + (59 ≤ xR12[15,23] ≤ 60)] } +
{ (xR8==68) } + { (xR8==69) } + { (xR8==72) } +
{ (xR8==65) (xR12[0,1]) }
xR12[1,2] = { [2 ≤ xR8 ≤ 31] [~(xR13[0,32]==0) + (xR12[2,3])] [xR12[2,3]] } +
{ (xR8==65) (xR12[0,1] + xR12[1,2]) } +
{ (33 ≤ xR8 ≤ 63) (xR12[2,3]) } +
{ [(xR8==66) | (xR8==32)] [xR12[1,2]] }
xR12[2,3] = { [xR8==32] [(xR13[(xR8)(31)]) (xR14[(xR8)(31)]) + (xR12[1,2]) ((xR13[(xR8) (31)]) + (xR14[(xR8) (31)]))] } +
{ [33 ≤ xR8 ≤ 63] [(xR13[(xR8)(31)]) (xR14[(xR8)(31)]) + (xR12[2,3]) ((xR13[(xR8) (31)]) + (xR14[(xR8) (31)]))] } +
{ [(xR8==64) | (2 ≤ xR8 ≤ 31) | (xR8==71)] [xR12[2,3]] }
xR12[3,4] = { (xR8==66) (xR13[31,32]) } +
{ (32 ≤ xR8 ≤ 64) (xR12[3,4]) }
xR12[4,5] = { (xR8==66) (xR14[31,32]) } +
(32 ≤ xR8 ≤ 64) (xR12[4,5])
xR12[5,6] = { (xR8==67) ~(xR11[0,32]==0) ~(xR15[0,32]==0) ~(xR11[0,32]==1) ~(xR15[0,32]==1) (xR11[31,32]) } +
{ ~(xR8==67) (xR12[5,6]) }
xR12[6,7] = { (xR8==67) ~(xR11[0,32]==0) ~(xR15[0,32]==0) ~(xR11[0,32]==1) ~(xR15[0,32]==1) (xR15[31,32]) } +
{ ~(xR8==67) (xR12[6,7]) }
xR12[7,8] = { (xR8==193) (xR12[63,64]) } +
{ [xR8==67] [~(xR11[0,32]==0) ~(xR11[0,32]==1) (xR15[0,32]==1) (xR11[31,32]) + ~(xR15[0,32]==0) ~(xR15[0,32]==1) (xR11[0,32]==1) (xR15[31,32])] } +
{ (xR8==73) (xR13[31,32]) } +
{ [xR8==66] ~[xR12[1,2]] [~(xR13[0,32]==0) (xR14[0,32]==0) (xR13[31,32]) + (xR13[0,32]==0) ~(xR14[0,32]==0) (xR14[31,32])] } +
{ [xR8==64] ~[(xR13[31,32]) ~(xR12[3,4]) ~(xR12[4,5]) + ~(xR13[31,32]) (xR12[3,4]) (xR12[4,5])] [xR13[31,32]] } +
{ ~(xR8==64) ~(xR8==66) ~(xR8==67) ~(xR8==73) ~(xR8==193) (xR12[7,8]) }
xR12[9,10] = { (xR8==193) (xR12[32,64]==0) } +
{ [xR8==67] [(xR11[0,32]==0) + (xR15[0,32]==0)] } +
{ (xR8==73) (xR13[0,32]==0) } +
{ (xR8==66) (xR13[0,32]==0) (xR14[0,32]==0) } +
{ [xR8==64] ~[(xR13[31,32]) ~(xR12[3,4]) ~(xR12[4,5]) + ~(xR13[31,32]) (xR12[3,4]) (xR12[4,5])] [xR13[31,32]] [xR13[0,32]==0] } +
{ ~(xR8==64) ~(xR8==66) ~(xR8==67) ~(xR8==73) ~(xR8==193) (xR12[9,10]) }
xR12[15,23] = { (xR8==160) (INSTRUCTION_FORMAT_CORRECT) (xR11[0,8]) } +
{ ~(xR8==160) (xR12[15,23]) }
xR12[23,28] = { (xR8==160) (INSTRUCTION_FORMAT_CORRECT) (xR11[8,13]) } +