aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-11-12 20:37:12 -0500
committerGravatar Jason Gross <jgross@mit.edu>2017-11-12 20:37:12 -0500
commite5efbf51add38c90d7bbdde6d1887762fa1ecc8f (patch)
tree9730652ed6225058c09c78d895bcc6d83a7a683c
parentb818fa6c80bd1ec686b0cba05dfdde89f7911b66 (diff)
Add more constant notations
Diffstat
-rw-r--r--src/Compilers/Z/BinaryNotationConstants.v171
-rw-r--r--src/Compilers/Z/HexNotationConstants.v285
2 files changed, 456 insertions, 0 deletions
diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index a990f2bda..f18efd962 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -90,6 +90,7 @@ nums = tuple(sorted(set(systematic_nums + [
4194286,
4194287,
4194293,
+ 4194299,
4194302,
8323583,
8386654,
@@ -104,6 +105,8 @@ nums = tuple(sorted(set(systematic_nums + [
8388577,
8388581,
8388591,
+ 8388595,
+ 8388598,
8388599,
8388605,
8388606,
@@ -116,6 +119,7 @@ nums = tuple(sorted(set(systematic_nums + [
16777162,
16777182,
16777189,
+ 16777190,
16777191,
16777199,
16777201,
@@ -140,6 +144,7 @@ nums = tuple(sorted(set(systematic_nums + [
67108798,
67108826,
67108833,
+ 67108839,
67108845,
67108847,
67108849,
@@ -149,6 +154,7 @@ nums = tuple(sorted(set(systematic_nums + [
67108861,
67108862,
134217666,
+ 134217678,
134217690,
134217694,
134217697,
@@ -168,11 +174,13 @@ nums = tuple(sorted(set(systematic_nums + [
268435426,
268435438,
268435441,
+ 268435443,
268435445,
268435452,
268435453,
268435454,
536870882,
+ 536870886,
536870890,
536870893,
536870906,
@@ -242,6 +250,10 @@ nums = tuple(sorted(set(systematic_nums + [
8589934567,
8589934575,
8589934587,
+ 8589934590,
+ 17179869134,
+ 17179869174,
+ 17179869182,
34359738341,
34359738349,
34359738355,
@@ -256,19 +268,32 @@ nums = tuple(sorted(set(systematic_nums + [
137438952991,
137438953285,
137438953355,
+ 137438953454,
+ 274844352511,
+ 274877906919,
274877906927,
274877906933,
274877906939,
274877906941,
+ 274877906942,
+ 549688705022,
549755813783,
+ 549755813838,
549755813854,
+ 549755813855,
+ 549755813866,
549755813869,
+ 549755813878,
+ 549755813882,
549755813886,
1099511627566,
+ 1099511627710,
1099511627738,
+ 1099511627759,
1099511627761,
1099511627774,
1425929142271,
+ 2199023255518,
2199023255522,
2199023255543,
2199023255550,
@@ -280,26 +305,47 @@ nums = tuple(sorted(set(systematic_nums + [
8727910416382,
8796090925055,
8796093021443,
+ 8796093022158,
+ 8796093022179,
8796093022183,
8796093022189,
8796093022193,
+ 8796093022198,
+ 8796093022205,
8796093022206,
+ 17592181850110,
+ 17592186044358,
17592186044366,
+ 17592186044378,
17592186044399,
+ 17592186044410,
17592186044411,
17592186044413,
17592186044414,
+ 35184372088715,
+ 35184372088768,
+ 35184372088798,
35184372088822,
+ 35184372088826,
35184372088829,
+ 35184372088830,
70368735789055,
+ 70368744177430,
70368744177637,
70368744177647,
+ 70368744177651,
+ 70368744177658,
70368744177659,
70368744177661,
+ 70368744177662,
140737471578110,
+ 140737488355274,
140737488355294,
+ 140737488355301,
+ 140737488355302,
140737488355303,
140737488355313,
+ 140737488355318,
140737488355319,
140737488355326,
194613558116351,
@@ -307,9 +353,11 @@ nums = tuple(sorted(set(systematic_nums + [
281470681743359,
281474976645119,
281474976710339,
+ 281474976710602,
281474976710606,
281474976710626,
281474976710631,
+ 281474976710637,
281474976710638,
281474976710639,
281474976710645,
@@ -321,15 +369,18 @@ nums = tuple(sorted(set(systematic_nums + [
562949953290238,
562949953420678,
562949953421262,
+ 562949953421274,
562949953421279,
562949953421290,
562949953421293,
562949953421297,
+ 562949953421303,
562949953421310,
1125899873288191,
1125899906842558,
1125899906842593,
1125899906842594,
+ 1125899906842606,
1125899906842607,
1125899906842619,
1125899906842621,
@@ -344,6 +395,7 @@ nums = tuple(sorted(set(systematic_nums + [
2251799813685214,
2251799813685217,
2251799813685229,
+ 2251799813685231,
2251799813685238,
2251799813685239,
2251799813685242,
@@ -360,6 +412,7 @@ nums = tuple(sorted(set(systematic_nums + [
4503599627370309,
4503599627370434,
4503599627370458,
+ 4503599627370462,
4503599627370478,
4503599627370479,
4503599627370491,
@@ -371,10 +424,12 @@ nums = tuple(sorted(set(systematic_nums + [
9007199254740614,
9007199254740618,
9007199254740963,
+ 9007199254740977,
9007199254740982,
9007199254740988,
9007199254740990,
18014398509481926,
+ 18014398509481954,
18014398509481975,
18014398509481981,
18014398509481982,
@@ -422,12 +477,14 @@ nums = tuple(sorted(set(systematic_nums + [
576460752303423467,
576460752303423469,
576460752303423471,
+ 576460752303423473,
576460752303423482,
576460752303423486,
1117984489315730401,
1152921504606846934,
1152921504606846938,
1152921504606846942,
+ 1152921504606846946,
1152921504606846974,
2305843009213693948,
2305843009213693950,
@@ -1031,6 +1088,8 @@ Notation "'0b1111111111111111101111'" (* 4194287 (0x3fffef) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1).
Notation "'0b1111111111111111110101'" (* 4194293 (0x3ffff5) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~1).
+Notation "'0b1111111111111111111011'" (* 4194299 (0x3ffffb) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1).
Notation "'0b1111111111111111111110'" (* 4194302 (0x3ffffe) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
Notation "'0b1111111111111111111111'" (* 4194303 (0x3fffff) *)
@@ -1065,6 +1124,10 @@ Notation "'0b11111111111111111100101'" (* 8388581 (0x7fffe5) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1).
Notation "'0b11111111111111111101111'" (* 8388591 (0x7fffef) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1).
+Notation "'0b11111111111111111110011'" (* 8388595 (0x7ffff3) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1).
+Notation "'0b11111111111111111110110'" (* 8388598 (0x7ffff6) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0).
Notation "'0b11111111111111111110111'" (* 8388599 (0x7ffff7) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1).
Notation "'0b11111111111111111111101'" (* 8388605 (0x7ffffd) *)
@@ -1095,6 +1158,8 @@ Notation "'0b111111111111111111011110'" (* 16777182 (0xffffde) *)
:= (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
Notation "'0b111111111111111111100101'" (* 16777189 (0xffffe5) *)
:= (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1).
+Notation "'0b111111111111111111100110'" (* 16777190 (0xffffe6) *)
+ := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~0).
Notation "'0b111111111111111111100111'" (* 16777191 (0xffffe7) *)
:= (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1).
Notation "'0b111111111111111111101111'" (* 16777199 (0xffffef) *)
@@ -1155,6 +1220,8 @@ Notation "'0b11111111111111111111011010'" (* 67108826 (0x3ffffda) *)
:= (Const WO~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0).
Notation "'0b11111111111111111111100001'" (* 67108833 (0x3ffffe1) *)
:= (Const WO~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1).
+Notation "'0b11111111111111111111100111'" (* 67108839 (0x3ffffe7) *)
+ := (Const WO~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1).
Notation "'0b11111111111111111111101101'" (* 67108845 (0x3ffffed) *)
:= (Const WO~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1).
Notation "'0b11111111111111111111101111'" (* 67108847 (0x3ffffef) *)
@@ -1179,6 +1246,8 @@ Notation "'0b100000000000000000000000001'" (* 67108865 (0x4000001) *)
:= (Const WO~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
Notation "'0b111111111111111111111000010'" (* 134217666 (0x7ffffc2) *)
:= (Const WO~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0).
+Notation "'0b111111111111111111111001110'" (* 134217678 (0x7ffffce) *)
+ := (Const WO~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1~0).
Notation "'0b111111111111111111111011010'" (* 134217690 (0x7ffffda) *)
:= (Const WO~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0).
Notation "'0b111111111111111111111011110'" (* 134217694 (0x7ffffde) *)
@@ -1223,6 +1292,8 @@ Notation "'0b1111111111111111111111101110'" (* 268435438 (0xfffffee) *)
:= (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0).
Notation "'0b1111111111111111111111110001'" (* 268435441 (0xffffff1) *)
:= (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1).
+Notation "'0b1111111111111111111111110011'" (* 268435443 (0xffffff3) *)
+ := (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1).
Notation "'0b1111111111111111111111110101'" (* 268435445 (0xffffff5) *)
:= (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~1).
Notation "'0b1111111111111111111111111100'" (* 268435452 (0xffffffc) *)
@@ -1239,6 +1310,8 @@ Notation "'0b10000000000000000000000000001'" (* 268435457 (0x10000001) *)
:= (Const WO~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
Notation "'0b11111111111111111111111100010'" (* 536870882 (0x1fffffe2) *)
:= (Const WO~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0).
+Notation "'0b11111111111111111111111100110'" (* 536870886 (0x1fffffe6) *)
+ := (Const WO~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~0).
Notation "'0b11111111111111111111111101010'" (* 536870890 (0x1fffffea) *)
:= (Const WO~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~1~0).
Notation "'0b11111111111111111111111101101'" (* 536870893 (0x1fffffed) *)
@@ -1399,12 +1472,20 @@ Notation "'0b111111111111111111111111111101111'" (* 8589934575 (0x1ffffffef) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1).
Notation "'0b111111111111111111111111111111011'" (* 8589934587 (0x1fffffffb) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1).
+Notation "'0b111111111111111111111111111111110'" (* 8589934590 (0x1fffffffe) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
Notation "'0b111111111111111111111111111111111'" (* 8589934591 (0x1ffffffff) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
Notation "'0b1000000000000000000000000000000000'" (* 8589934592 (0x200000000) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
Notation "'0b1000000000000000000000000000000001'" (* 8589934593 (0x200000001) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0b1111111111111111111111111111001110'" (* 17179869134 (0x3ffffffce) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1~0).
+Notation "'0b1111111111111111111111111111110110'" (* 17179869174 (0x3fffffff6) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0).
+Notation "'0b1111111111111111111111111111111110'" (* 17179869182 (0x3fffffffe) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
Notation "'0b1111111111111111111111111111111111'" (* 17179869183 (0x3ffffffff) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
Notation "'0b10000000000000000000000000000000000'" (* 17179869184 (0x400000000) *)
@@ -1451,12 +1532,18 @@ Notation "'0b1111111111111111111111111111101000101'" (* 137438953285 (0x1fffffff
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~1~0~1).
Notation "'0b1111111111111111111111111111110001011'" (* 137438953355 (0x1fffffff8b) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0~1~1).
+Notation "'0b1111111111111111111111111111111101110'" (* 137438953454 (0x1fffffffee) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0).
Notation "'0b1111111111111111111111111111111111111'" (* 137438953471 (0x1fffffffff) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
Notation "'0b10000000000000000000000000000000000000'" (* 137438953472 (0x2000000000) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
Notation "'0b10000000000000000000000000000000000001'" (* 137438953473 (0x2000000001) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0b11111111111101111111111111111111111111'" (* 274844352511 (0x3ffdffffff) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0b11111111111111111111111111111111100111'" (* 274877906919 (0x3fffffffe7) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1).
Notation "'0b11111111111111111111111111111111101111'" (* 274877906927 (0x3fffffffef) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1).
Notation "'0b11111111111111111111111111111111110101'" (* 274877906933 (0x3ffffffff5) *)
@@ -1465,18 +1552,32 @@ Notation "'0b11111111111111111111111111111111111011'" (* 274877906939 (0x3ffffff
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1).
Notation "'0b11111111111111111111111111111111111101'" (* 274877906941 (0x3ffffffffd) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1).
+Notation "'0b11111111111111111111111111111111111110'" (* 274877906942 (0x3ffffffffe) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
Notation "'0b11111111111111111111111111111111111111'" (* 274877906943 (0x3fffffffff) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
Notation "'0b100000000000000000000000000000000000000'" (* 274877906944 (0x4000000000) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
Notation "'0b100000000000000000000000000000000000001'" (* 274877906945 (0x4000000001) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0b111111111111011111111111111111111111110'" (* 549688705022 (0x7ffbfffffe) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
Notation "'0b111111111111111111111111111111110010111'" (* 549755813783 (0x7fffffff97) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~1~1).
+Notation "'0b111111111111111111111111111111111001110'" (* 549755813838 (0x7fffffffce) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1~0).
Notation "'0b111111111111111111111111111111111011110'" (* 549755813854 (0x7fffffffde) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
+Notation "'0b111111111111111111111111111111111011111'" (* 549755813855 (0x7fffffffdf) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1).
+Notation "'0b111111111111111111111111111111111101010'" (* 549755813866 (0x7fffffffea) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~1~0).
Notation "'0b111111111111111111111111111111111101101'" (* 549755813869 (0x7fffffffed) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1).
+Notation "'0b111111111111111111111111111111111110110'" (* 549755813878 (0x7ffffffff6) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0).
+Notation "'0b111111111111111111111111111111111111010'" (* 549755813882 (0x7ffffffffa) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0).
Notation "'0b111111111111111111111111111111111111110'" (* 549755813886 (0x7ffffffffe) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
Notation "'0b111111111111111111111111111111111111111'" (* 549755813887 (0x7fffffffff) *)
@@ -1487,8 +1588,12 @@ Notation "'0b1000000000000000000000000000000000000001'" (* 549755813889 (0x80000
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
Notation "'0b1111111111111111111111111111111100101110'" (* 1099511627566 (0xffffffff2e) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~1~1~0).
+Notation "'0b1111111111111111111111111111111110111110'" (* 1099511627710 (0xffffffffbe) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~0).
Notation "'0b1111111111111111111111111111111111011010'" (* 1099511627738 (0xffffffffda) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0).
+Notation "'0b1111111111111111111111111111111111101111'" (* 1099511627759 (0xffffffffef) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1).
Notation "'0b1111111111111111111111111111111111110001'" (* 1099511627761 (0xfffffffff1) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1).
Notation "'0b1111111111111111111111111111111111111110'" (* 1099511627774 (0xfffffffffe) *)
@@ -1501,6 +1606,8 @@ Notation "'0b10000000000000000000000000000000000000001'" (* 1099511627777 (0x100
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
Notation "'0b10100101111111111111111111111111111111111'" (* 1425929142271 (0x14bffffffff) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~1~0~0~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0b11111111111111111111111111111111111011110'" (* 2199023255518 (0x1ffffffffde) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
Notation "'0b11111111111111111111111111111111111100010'" (* 2199023255522 (0x1ffffffffe2) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0).
Notation "'0b11111111111111111111111111111111111110111'" (* 2199023255543 (0x1fffffffff7) *)
@@ -1535,12 +1642,20 @@ Notation "'0b1111111111111111111110111111111111111111111'" (* 8796090925055 (0x7
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
Notation "'0b1111111111111111111111111111111110100000011'" (* 8796093021443 (0x7fffffffd03) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~0~0~1~1).
+Notation "'0b1111111111111111111111111111111111111001110'" (* 8796093022158 (0x7ffffffffce) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1~0).
+Notation "'0b1111111111111111111111111111111111111100011'" (* 8796093022179 (0x7ffffffffe3) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~1).
Notation "'0b1111111111111111111111111111111111111100111'" (* 8796093022183 (0x7ffffffffe7) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1).
Notation "'0b1111111111111111111111111111111111111101101'" (* 8796093022189 (0x7ffffffffed) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1).
Notation "'0b1111111111111111111111111111111111111110001'" (* 8796093022193 (0x7fffffffff1) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1).
+Notation "'0b1111111111111111111111111111111111111110110'" (* 8796093022198 (0x7fffffffff6) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0).
+Notation "'0b1111111111111111111111111111111111111111101'" (* 8796093022205 (0x7fffffffffd) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1).
Notation "'0b1111111111111111111111111111111111111111110'" (* 8796093022206 (0x7fffffffffe) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
Notation "'0b1111111111111111111111111111111111111111111'" (* 8796093022207 (0x7ffffffffff) *)
@@ -1549,10 +1664,18 @@ Notation "'0b10000000000000000000000000000000000000000000'" (* 8796093022208 (0x
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
Notation "'0b10000000000000000000000000000000000000000001'" (* 8796093022209 (0x80000000001) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0b11111111111111111111101111111111111111111110'" (* 17592181850110 (0xfffffbffffe) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
+Notation "'0b11111111111111111111111111111111111111000110'" (* 17592186044358 (0xfffffffffc6) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~1~0).
Notation "'0b11111111111111111111111111111111111111001110'" (* 17592186044366 (0xfffffffffce) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1~0).
+Notation "'0b11111111111111111111111111111111111111011010'" (* 17592186044378 (0xfffffffffda) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0).
Notation "'0b11111111111111111111111111111111111111101111'" (* 17592186044399 (0xfffffffffef) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1).
+Notation "'0b11111111111111111111111111111111111111111010'" (* 17592186044410 (0xffffffffffa) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0).
Notation "'0b11111111111111111111111111111111111111111011'" (* 17592186044411 (0xffffffffffb) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1).
Notation "'0b11111111111111111111111111111111111111111101'" (* 17592186044413 (0xffffffffffd) *)
@@ -1565,10 +1688,20 @@ Notation "'0b100000000000000000000000000000000000000000000'" (* 17592186044416 (
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0).
Notation "'0b100000000000000000000000000000000000000000001'" (* 17592186044417 (0x100000000001) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0b111111111111111111111111111111111111110001011'" (* 35184372088715 (0x1fffffffff8b) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0~1~1).
+Notation "'0b111111111111111111111111111111111111111000000'" (* 35184372088768 (0x1fffffffffc0) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~0~0).
+Notation "'0b111111111111111111111111111111111111111011110'" (* 35184372088798 (0x1fffffffffde) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
Notation "'0b111111111111111111111111111111111111111110110'" (* 35184372088822 (0x1ffffffffff6) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0).
+Notation "'0b111111111111111111111111111111111111111111010'" (* 35184372088826 (0x1ffffffffffa) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0).
Notation "'0b111111111111111111111111111111111111111111101'" (* 35184372088829 (0x1ffffffffffd) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1).
+Notation "'0b111111111111111111111111111111111111111111110'" (* 35184372088830 (0x1ffffffffffe) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
Notation "'0b111111111111111111111111111111111111111111111'" (* 35184372088831 (0x1fffffffffff) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
Notation "'0b1000000000000000000000000000000000000000000000'" (* 35184372088832 (0x200000000000) *)
@@ -1577,14 +1710,22 @@ Notation "'0b1000000000000000000000000000000000000000000001'" (* 35184372088833
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
Notation "'0b1111111111111111111111011111111111111111111111'" (* 70368735789055 (0x3fffff7fffff) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0b1111111111111111111111111111111111111100010110'" (* 70368744177430 (0x3fffffffff16) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0~1~1~0).
Notation "'0b1111111111111111111111111111111111111111100101'" (* 70368744177637 (0x3fffffffffe5) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1).
Notation "'0b1111111111111111111111111111111111111111101111'" (* 70368744177647 (0x3fffffffffef) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1).
+Notation "'0b1111111111111111111111111111111111111111110011'" (* 70368744177651 (0x3ffffffffff3) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1).
+Notation "'0b1111111111111111111111111111111111111111111010'" (* 70368744177658 (0x3ffffffffffa) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0).
Notation "'0b1111111111111111111111111111111111111111111011'" (* 70368744177659 (0x3ffffffffffb) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1).
Notation "'0b1111111111111111111111111111111111111111111101'" (* 70368744177661 (0x3ffffffffffd) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1).
+Notation "'0b1111111111111111111111111111111111111111111110'" (* 70368744177662 (0x3ffffffffffe) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
Notation "'0b1111111111111111111111111111111111111111111111'" (* 70368744177663 (0x3fffffffffff) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
Notation "'0b10000000000000000000000000000000000000000000000'" (* 70368744177664 (0x400000000000) *)
@@ -1593,12 +1734,20 @@ Notation "'0b10000000000000000000000000000000000000000000001'" (* 70368744177665
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
Notation "'0b11111111111111111111110111111111111111111111110'" (* 140737471578110 (0x7ffffefffffe) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
+Notation "'0b11111111111111111111111111111111111111111001010'" (* 140737488355274 (0x7fffffffffca) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~0).
Notation "'0b11111111111111111111111111111111111111111011110'" (* 140737488355294 (0x7fffffffffde) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
+Notation "'0b11111111111111111111111111111111111111111100101'" (* 140737488355301 (0x7fffffffffe5) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1).
+Notation "'0b11111111111111111111111111111111111111111100110'" (* 140737488355302 (0x7fffffffffe6) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~0).
Notation "'0b11111111111111111111111111111111111111111100111'" (* 140737488355303 (0x7fffffffffe7) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1).
Notation "'0b11111111111111111111111111111111111111111110001'" (* 140737488355313 (0x7ffffffffff1) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1).
+Notation "'0b11111111111111111111111111111111111111111110110'" (* 140737488355318 (0x7ffffffffff6) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0).
Notation "'0b11111111111111111111111111111111111111111110111'" (* 140737488355319 (0x7ffffffffff7) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1).
Notation "'0b11111111111111111111111111111111111111111111110'" (* 140737488355326 (0x7ffffffffffe) *)
@@ -1619,12 +1768,16 @@ Notation "'0b111111111111111111111111111111101111111111111111'" (* 2814749766451
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
Notation "'0b111111111111111111111111111111111111111011000011'" (* 281474976710339 (0xfffffffffec3) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~0~0~0~1~1).
+Notation "'0b111111111111111111111111111111111111111111001010'" (* 281474976710602 (0xffffffffffca) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~0).
Notation "'0b111111111111111111111111111111111111111111001110'" (* 281474976710606 (0xffffffffffce) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1~0).
Notation "'0b111111111111111111111111111111111111111111100010'" (* 281474976710626 (0xffffffffffe2) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0).
Notation "'0b111111111111111111111111111111111111111111100111'" (* 281474976710631 (0xffffffffffe7) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1).
+Notation "'0b111111111111111111111111111111111111111111101101'" (* 281474976710637 (0xffffffffffed) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1).
Notation "'0b111111111111111111111111111111111111111111101110'" (* 281474976710638 (0xffffffffffee) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0).
Notation "'0b111111111111111111111111111111111111111111101111'" (* 281474976710639 (0xffffffffffef) *)
@@ -1653,6 +1806,8 @@ Notation "'0b1111111111111111111111111111111111111110110000110'" (* 562949953420
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~0~0~0~1~1~0).
Notation "'0b1111111111111111111111111111111111111111111001110'" (* 562949953421262 (0x1ffffffffffce) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1~0).
+Notation "'0b1111111111111111111111111111111111111111111011010'" (* 562949953421274 (0x1ffffffffffda) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0).
Notation "'0b1111111111111111111111111111111111111111111011111'" (* 562949953421279 (0x1ffffffffffdf) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1).
Notation "'0b1111111111111111111111111111111111111111111101010'" (* 562949953421290 (0x1ffffffffffea) *)
@@ -1661,6 +1816,8 @@ Notation "'0b1111111111111111111111111111111111111111111101101'" (* 562949953421
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1).
Notation "'0b1111111111111111111111111111111111111111111110001'" (* 562949953421297 (0x1fffffffffff1) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1).
+Notation "'0b1111111111111111111111111111111111111111111110111'" (* 562949953421303 (0x1fffffffffff7) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1).
Notation "'0b1111111111111111111111111111111111111111111111110'" (* 562949953421310 (0x1fffffffffffe) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
Notation "'0b1111111111111111111111111111111111111111111111111'" (* 562949953421311 (0x1ffffffffffff) *)
@@ -1677,6 +1834,8 @@ Notation "'0b11111111111111111111111111111111111111111111100001'" (* 11258999068
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1).
Notation "'0b11111111111111111111111111111111111111111111100010'" (* 1125899906842594 (0x3ffffffffffe2) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0).
+Notation "'0b11111111111111111111111111111111111111111111101110'" (* 1125899906842606 (0x3ffffffffffee) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0).
Notation "'0b11111111111111111111111111111111111111111111101111'" (* 1125899906842607 (0x3ffffffffffef) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1).
Notation "'0b11111111111111111111111111111111111111111111111011'" (* 1125899906842619 (0x3fffffffffffb) *)
@@ -1711,6 +1870,8 @@ Notation "'0b111111111111111111111111111111111111111111111100001'" (* 2251799813
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1).
Notation "'0b111111111111111111111111111111111111111111111101101'" (* 2251799813685229 (0x7ffffffffffed) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1).
+Notation "'0b111111111111111111111111111111111111111111111101111'" (* 2251799813685231 (0x7ffffffffffef) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1).
Notation "'0b111111111111111111111111111111111111111111111110110'" (* 2251799813685238 (0x7fffffffffff6) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0).
Notation "'0b111111111111111111111111111111111111111111111110111'" (* 2251799813685239 (0x7fffffffffff7) *)
@@ -1749,6 +1910,8 @@ Notation "'0b1111111111111111111111111111111111111111111111000010'" (* 450359962
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0).
Notation "'0b1111111111111111111111111111111111111111111111011010'" (* 4503599627370458 (0xfffffffffffda) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0).
+Notation "'0b1111111111111111111111111111111111111111111111011110'" (* 4503599627370462 (0xfffffffffffde) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
Notation "'0b1111111111111111111111111111111111111111111111101110'" (* 4503599627370478 (0xfffffffffffee) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0).
Notation "'0b1111111111111111111111111111111111111111111111101111'" (* 4503599627370479 (0xfffffffffffef) *)
@@ -1777,6 +1940,8 @@ Notation "'0b11111111111111111111111111111111111111111111010001010'" (* 90071992
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~1~0~1~0).
Notation "'0b11111111111111111111111111111111111111111111111100011'" (* 9007199254740963 (0x1fffffffffffe3) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~1).
+Notation "'0b11111111111111111111111111111111111111111111111110001'" (* 9007199254740977 (0x1ffffffffffff1) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1).
Notation "'0b11111111111111111111111111111111111111111111111110110'" (* 9007199254740982 (0x1ffffffffffff6) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0).
Notation "'0b11111111111111111111111111111111111111111111111111100'" (* 9007199254740988 (0x1ffffffffffffc) *)
@@ -1791,6 +1956,8 @@ Notation "'0b100000000000000000000000000000000000000000000000000001'" (* 9007199
:= (Const WO~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
Notation "'0b111111111111111111111111111111111111111111111111000110'" (* 18014398509481926 (0x3fffffffffffc6) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~1~0).
+Notation "'0b111111111111111111111111111111111111111111111111100010'" (* 18014398509481954 (0x3fffffffffffe2) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0).
Notation "'0b111111111111111111111111111111111111111111111111110111'" (* 18014398509481975 (0x3ffffffffffff7) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1).
Notation "'0b111111111111111111111111111111111111111111111111111101'" (* 18014398509481981 (0x3ffffffffffffd) *)
@@ -1915,6 +2082,8 @@ Notation "'0b11111111111111111111111111111111111111111111111111111101101'" (* 57
:= (Const WO~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1).
Notation "'0b11111111111111111111111111111111111111111111111111111101111'" (* 576460752303423471 (0x7ffffffffffffef) *)
:= (Const WO~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1).
+Notation "'0b11111111111111111111111111111111111111111111111111111110001'" (* 576460752303423473 (0x7fffffffffffff1) *)
+ := (Const WO~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1).
Notation "'0b11111111111111111111111111111111111111111111111111111111010'" (* 576460752303423482 (0x7fffffffffffffa) *)
:= (Const WO~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0).
Notation "'0b11111111111111111111111111111111111111111111111111111111110'" (* 576460752303423486 (0x7fffffffffffffe) *)
@@ -1933,6 +2102,8 @@ Notation "'0b111111111111111111111111111111111111111111111111111111011010'" (* 1
:= (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0).
Notation "'0b111111111111111111111111111111111111111111111111111111011110'" (* 1152921504606846942 (0xfffffffffffffde) *)
:= (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
+Notation "'0b111111111111111111111111111111111111111111111111111111100010'" (* 1152921504606846946 (0xfffffffffffffe2) *)
+ := (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0).
Notation "'0b111111111111111111111111111111111111111111111111111111111110'" (* 1152921504606846974 (0xffffffffffffffe) *)
:= (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
Notation "'0b111111111111111111111111111111111111111111111111111111111111'" (* 1152921504606846975 (0xfffffffffffffff) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index 98dcc2bd6..a5ab779cd 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -90,6 +90,7 @@ nums = tuple(sorted(set(systematic_nums + [
4194286,
4194287,
4194293,
+ 4194299,
4194302,
8323583,
8386654,
@@ -104,6 +105,8 @@ nums = tuple(sorted(set(systematic_nums + [
8388577,
8388581,
8388591,
+ 8388595,
+ 8388598,
8388599,
8388605,
8388606,
@@ -116,6 +119,7 @@ nums = tuple(sorted(set(systematic_nums + [
16777162,
16777182,
16777189,
+ 16777190,
16777191,
16777199,
16777201,
@@ -140,6 +144,7 @@ nums = tuple(sorted(set(systematic_nums + [
67108798,
67108826,
67108833,
+ 67108839,
67108845,
67108847,
67108849,
@@ -149,6 +154,7 @@ nums = tuple(sorted(set(systematic_nums + [
67108861,
67108862,
134217666,
+ 134217678,
134217690,
134217694,
134217697,
@@ -168,11 +174,13 @@ nums = tuple(sorted(set(systematic_nums + [
268435426,
268435438,
268435441,
+ 268435443,
268435445,
268435452,
268435453,
268435454,
536870882,
+ 536870886,
536870890,
536870893,
536870906,
@@ -242,6 +250,10 @@ nums = tuple(sorted(set(systematic_nums + [
8589934567,
8589934575,
8589934587,
+ 8589934590,
+ 17179869134,
+ 17179869174,
+ 17179869182,
34359738341,
34359738349,
34359738355,
@@ -256,19 +268,32 @@ nums = tuple(sorted(set(systematic_nums + [
137438952991,
137438953285,
137438953355,
+ 137438953454,
+ 274844352511,
+ 274877906919,
274877906927,
274877906933,
274877906939,
274877906941,
+ 274877906942,
+ 549688705022,
549755813783,
+ 549755813838,
549755813854,
+ 549755813855,
+ 549755813866,
549755813869,
+ 549755813878,
+ 549755813882,
549755813886,
1099511627566,
+ 1099511627710,
1099511627738,
+ 1099511627759,
1099511627761,
1099511627774,
1425929142271,
+ 2199023255518,
2199023255522,
2199023255543,
2199023255550,
@@ -280,26 +305,47 @@ nums = tuple(sorted(set(systematic_nums + [
8727910416382,
8796090925055,
8796093021443,
+ 8796093022158,
+ 8796093022179,
8796093022183,
8796093022189,
8796093022193,
+ 8796093022198,
+ 8796093022205,
8796093022206,
+ 17592181850110,
+ 17592186044358,
17592186044366,
+ 17592186044378,
17592186044399,
+ 17592186044410,
17592186044411,
17592186044413,
17592186044414,
+ 35184372088715,
+ 35184372088768,
+ 35184372088798,
35184372088822,
+ 35184372088826,
35184372088829,
+ 35184372088830,
70368735789055,
+ 70368744177430,
70368744177637,
70368744177647,
+ 70368744177651,
+ 70368744177658,
70368744177659,
70368744177661,
+ 70368744177662,
140737471578110,
+ 140737488355274,
140737488355294,
+ 140737488355301,
+ 140737488355302,
140737488355303,
140737488355313,
+ 140737488355318,
140737488355319,
140737488355326,
194613558116351,
@@ -307,9 +353,11 @@ nums = tuple(sorted(set(systematic_nums + [
281470681743359,
281474976645119,
281474976710339,
+ 281474976710602,
281474976710606,
281474976710626,
281474976710631,
+ 281474976710637,
281474976710638,
281474976710639,
281474976710645,
@@ -321,15 +369,18 @@ nums = tuple(sorted(set(systematic_nums + [
562949953290238,
562949953420678,
562949953421262,
+ 562949953421274,
562949953421279,
562949953421290,
562949953421293,
562949953421297,
+ 562949953421303,
562949953421310,
1125899873288191,
1125899906842558,
1125899906842593,
1125899906842594,
+ 1125899906842606,
1125899906842607,
1125899906842619,
1125899906842621,
@@ -344,6 +395,7 @@ nums = tuple(sorted(set(systematic_nums + [
2251799813685214,
2251799813685217,
2251799813685229,
+ 2251799813685231,
2251799813685238,
2251799813685239,
2251799813685242,
@@ -360,6 +412,7 @@ nums = tuple(sorted(set(systematic_nums + [
4503599627370309,
4503599627370434,
4503599627370458,
+ 4503599627370462,
4503599627370478,
4503599627370479,
4503599627370491,
@@ -371,10 +424,12 @@ nums = tuple(sorted(set(systematic_nums + [
9007199254740614,
9007199254740618,
9007199254740963,
+ 9007199254740977,
9007199254740982,
9007199254740988,
9007199254740990,
18014398509481926,
+ 18014398509481954,
18014398509481975,
18014398509481981,
18014398509481982,
@@ -422,12 +477,14 @@ nums = tuple(sorted(set(systematic_nums + [
576460752303423467,
576460752303423469,
576460752303423471,
+ 576460752303423473,
576460752303423482,
576460752303423486,
1117984489315730401,
1152921504606846934,
1152921504606846938,
1152921504606846942,
+ 1152921504606846946,
1152921504606846974,
2305843009213693948,
2305843009213693950,
@@ -1525,6 +1582,10 @@ Notation "'0x3ffff5'" (* 4194293 (0x3ffff5) *)
:= (Const 4194293%Z).
Notation "'0x3ffff5'" (* 4194293 (0x3ffff5) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~1).
+Notation "'0x3ffffb'" (* 4194299 (0x3ffffb) *)
+ := (Const 4194299%Z).
+Notation "'0x3ffffb'" (* 4194299 (0x3ffffb) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1).
Notation "'0x3ffffe'" (* 4194302 (0x3ffffe) *)
:= (Const 4194302%Z).
Notation "'0x3ffffe'" (* 4194302 (0x3ffffe) *)
@@ -1593,6 +1654,14 @@ Notation "'0x7fffef'" (* 8388591 (0x7fffef) *)
:= (Const 8388591%Z).
Notation "'0x7fffef'" (* 8388591 (0x7fffef) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1).
+Notation "'0x7ffff3'" (* 8388595 (0x7ffff3) *)
+ := (Const 8388595%Z).
+Notation "'0x7ffff3'" (* 8388595 (0x7ffff3) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1).
+Notation "'0x7ffff6'" (* 8388598 (0x7ffff6) *)
+ := (Const 8388598%Z).
+Notation "'0x7ffff6'" (* 8388598 (0x7ffff6) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0).
Notation "'0x7ffff7'" (* 8388599 (0x7ffff7) *)
:= (Const 8388599%Z).
Notation "'0x7ffff7'" (* 8388599 (0x7ffff7) *)
@@ -1653,6 +1722,10 @@ Notation "'0xffffe5'" (* 16777189 (0xffffe5) *)
:= (Const 16777189%Z).
Notation "'0xffffe5'" (* 16777189 (0xffffe5) *)
:= (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1).
+Notation "'0xffffe6'" (* 16777190 (0xffffe6) *)
+ := (Const 16777190%Z).
+Notation "'0xffffe6'" (* 16777190 (0xffffe6) *)
+ := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~0).
Notation "'0xffffe7'" (* 16777191 (0xffffe7) *)
:= (Const 16777191%Z).
Notation "'0xffffe7'" (* 16777191 (0xffffe7) *)
@@ -1773,6 +1846,10 @@ Notation "'0x3ffffe1'" (* 67108833 (0x3ffffe1) *)
:= (Const 67108833%Z).
Notation "'0x3ffffe1'" (* 67108833 (0x3ffffe1) *)
:= (Const WO~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1).
+Notation "'0x3ffffe7'" (* 67108839 (0x3ffffe7) *)
+ := (Const 67108839%Z).
+Notation "'0x3ffffe7'" (* 67108839 (0x3ffffe7) *)
+ := (Const WO~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1).
Notation "'0x3ffffed'" (* 67108845 (0x3ffffed) *)
:= (Const 67108845%Z).
Notation "'0x3ffffed'" (* 67108845 (0x3ffffed) *)
@@ -1821,6 +1898,10 @@ Notation "'0x7ffffc2'" (* 134217666 (0x7ffffc2) *)
:= (Const 134217666%Z).
Notation "'0x7ffffc2'" (* 134217666 (0x7ffffc2) *)
:= (Const WO~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0).
+Notation "'0x7ffffce'" (* 134217678 (0x7ffffce) *)
+ := (Const 134217678%Z).
+Notation "'0x7ffffce'" (* 134217678 (0x7ffffce) *)
+ := (Const WO~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1~0).
Notation "'0x7ffffda'" (* 134217690 (0x7ffffda) *)
:= (Const 134217690%Z).
Notation "'0x7ffffda'" (* 134217690 (0x7ffffda) *)
@@ -1909,6 +1990,10 @@ Notation "'0xffffff1'" (* 268435441 (0xffffff1) *)
:= (Const 268435441%Z).
Notation "'0xffffff1'" (* 268435441 (0xffffff1) *)
:= (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1).
+Notation "'0xffffff3'" (* 268435443 (0xffffff3) *)
+ := (Const 268435443%Z).
+Notation "'0xffffff3'" (* 268435443 (0xffffff3) *)
+ := (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1).
Notation "'0xffffff5'" (* 268435445 (0xffffff5) *)
:= (Const 268435445%Z).
Notation "'0xffffff5'" (* 268435445 (0xffffff5) *)
@@ -1941,6 +2026,10 @@ Notation "'0x1fffffe2'" (* 536870882 (0x1fffffe2) *)
:= (Const 536870882%Z).
Notation "'0x1fffffe2'" (* 536870882 (0x1fffffe2) *)
:= (Const WO~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0).
+Notation "'0x1fffffe6'" (* 536870886 (0x1fffffe6) *)
+ := (Const 536870886%Z).
+Notation "'0x1fffffe6'" (* 536870886 (0x1fffffe6) *)
+ := (Const WO~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~0).
Notation "'0x1fffffea'" (* 536870890 (0x1fffffea) *)
:= (Const 536870890%Z).
Notation "'0x1fffffea'" (* 536870890 (0x1fffffea) *)
@@ -2261,6 +2350,10 @@ Notation "'0x1fffffffb'" (* 8589934587 (0x1fffffffb) *)
:= (Const 8589934587%Z).
Notation "'0x1fffffffb'" (* 8589934587 (0x1fffffffb) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1).
+Notation "'0x1fffffffe'" (* 8589934590 (0x1fffffffe) *)
+ := (Const 8589934590%Z).
+Notation "'0x1fffffffe'" (* 8589934590 (0x1fffffffe) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
Notation "'0x1ffffffff'" (* 8589934591 (0x1ffffffff) *)
:= (Const 8589934591%Z).
Notation "'0x1ffffffff'" (* 8589934591 (0x1ffffffff) *)
@@ -2273,6 +2366,18 @@ Notation "'0x200000001'" (* 8589934593 (0x200000001) *)
:= (Const 8589934593%Z).
Notation "'0x200000001'" (* 8589934593 (0x200000001) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0x3ffffffce'" (* 17179869134 (0x3ffffffce) *)
+ := (Const 17179869134%Z).
+Notation "'0x3ffffffce'" (* 17179869134 (0x3ffffffce) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1~0).
+Notation "'0x3fffffff6'" (* 17179869174 (0x3fffffff6) *)
+ := (Const 17179869174%Z).
+Notation "'0x3fffffff6'" (* 17179869174 (0x3fffffff6) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0).
+Notation "'0x3fffffffe'" (* 17179869182 (0x3fffffffe) *)
+ := (Const 17179869182%Z).
+Notation "'0x3fffffffe'" (* 17179869182 (0x3fffffffe) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
Notation "'0x3ffffffff'" (* 17179869183 (0x3ffffffff) *)
:= (Const 17179869183%Z).
Notation "'0x3ffffffff'" (* 17179869183 (0x3ffffffff) *)
@@ -2365,6 +2470,10 @@ Notation "'0x1fffffff8b'" (* 137438953355 (0x1fffffff8b) *)
:= (Const 137438953355%Z).
Notation "'0x1fffffff8b'" (* 137438953355 (0x1fffffff8b) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0~1~1).
+Notation "'0x1fffffffee'" (* 137438953454 (0x1fffffffee) *)
+ := (Const 137438953454%Z).
+Notation "'0x1fffffffee'" (* 137438953454 (0x1fffffffee) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0).
Notation "'0x1fffffffff'" (* 137438953471 (0x1fffffffff) *)
:= (Const 137438953471%Z).
Notation "'0x1fffffffff'" (* 137438953471 (0x1fffffffff) *)
@@ -2377,6 +2486,14 @@ Notation "'0x2000000001'" (* 137438953473 (0x2000000001) *)
:= (Const 137438953473%Z).
Notation "'0x2000000001'" (* 137438953473 (0x2000000001) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0x3ffdffffff'" (* 274844352511 (0x3ffdffffff) *)
+ := (Const 274844352511%Z).
+Notation "'0x3ffdffffff'" (* 274844352511 (0x3ffdffffff) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0x3fffffffe7'" (* 274877906919 (0x3fffffffe7) *)
+ := (Const 274877906919%Z).
+Notation "'0x3fffffffe7'" (* 274877906919 (0x3fffffffe7) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1).
Notation "'0x3fffffffef'" (* 274877906927 (0x3fffffffef) *)
:= (Const 274877906927%Z).
Notation "'0x3fffffffef'" (* 274877906927 (0x3fffffffef) *)
@@ -2393,6 +2510,10 @@ Notation "'0x3ffffffffd'" (* 274877906941 (0x3ffffffffd) *)
:= (Const 274877906941%Z).
Notation "'0x3ffffffffd'" (* 274877906941 (0x3ffffffffd) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1).
+Notation "'0x3ffffffffe'" (* 274877906942 (0x3ffffffffe) *)
+ := (Const 274877906942%Z).
+Notation "'0x3ffffffffe'" (* 274877906942 (0x3ffffffffe) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
Notation "'0x3fffffffff'" (* 274877906943 (0x3fffffffff) *)
:= (Const 274877906943%Z).
Notation "'0x3fffffffff'" (* 274877906943 (0x3fffffffff) *)
@@ -2405,18 +2526,42 @@ Notation "'0x4000000001'" (* 274877906945 (0x4000000001) *)
:= (Const 274877906945%Z).
Notation "'0x4000000001'" (* 274877906945 (0x4000000001) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0x7ffbfffffe'" (* 549688705022 (0x7ffbfffffe) *)
+ := (Const 549688705022%Z).
+Notation "'0x7ffbfffffe'" (* 549688705022 (0x7ffbfffffe) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
Notation "'0x7fffffff97'" (* 549755813783 (0x7fffffff97) *)
:= (Const 549755813783%Z).
Notation "'0x7fffffff97'" (* 549755813783 (0x7fffffff97) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~1~1).
+Notation "'0x7fffffffce'" (* 549755813838 (0x7fffffffce) *)
+ := (Const 549755813838%Z).
+Notation "'0x7fffffffce'" (* 549755813838 (0x7fffffffce) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1~0).
Notation "'0x7fffffffde'" (* 549755813854 (0x7fffffffde) *)
:= (Const 549755813854%Z).
Notation "'0x7fffffffde'" (* 549755813854 (0x7fffffffde) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
+Notation "'0x7fffffffdf'" (* 549755813855 (0x7fffffffdf) *)
+ := (Const 549755813855%Z).
+Notation "'0x7fffffffdf'" (* 549755813855 (0x7fffffffdf) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1).
+Notation "'0x7fffffffea'" (* 549755813866 (0x7fffffffea) *)
+ := (Const 549755813866%Z).
+Notation "'0x7fffffffea'" (* 549755813866 (0x7fffffffea) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~1~0).
Notation "'0x7fffffffed'" (* 549755813869 (0x7fffffffed) *)
:= (Const 549755813869%Z).
Notation "'0x7fffffffed'" (* 549755813869 (0x7fffffffed) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1).
+Notation "'0x7ffffffff6'" (* 549755813878 (0x7ffffffff6) *)
+ := (Const 549755813878%Z).
+Notation "'0x7ffffffff6'" (* 549755813878 (0x7ffffffff6) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0).
+Notation "'0x7ffffffffa'" (* 549755813882 (0x7ffffffffa) *)
+ := (Const 549755813882%Z).
+Notation "'0x7ffffffffa'" (* 549755813882 (0x7ffffffffa) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0).
Notation "'0x7ffffffffe'" (* 549755813886 (0x7ffffffffe) *)
:= (Const 549755813886%Z).
Notation "'0x7ffffffffe'" (* 549755813886 (0x7ffffffffe) *)
@@ -2437,10 +2582,18 @@ Notation "'0xffffffff2e'" (* 1099511627566 (0xffffffff2e) *)
:= (Const 1099511627566%Z).
Notation "'0xffffffff2e'" (* 1099511627566 (0xffffffff2e) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~1~1~0).
+Notation "'0xffffffffbe'" (* 1099511627710 (0xffffffffbe) *)
+ := (Const 1099511627710%Z).
+Notation "'0xffffffffbe'" (* 1099511627710 (0xffffffffbe) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~0).
Notation "'0xffffffffda'" (* 1099511627738 (0xffffffffda) *)
:= (Const 1099511627738%Z).
Notation "'0xffffffffda'" (* 1099511627738 (0xffffffffda) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0).
+Notation "'0xffffffffef'" (* 1099511627759 (0xffffffffef) *)
+ := (Const 1099511627759%Z).
+Notation "'0xffffffffef'" (* 1099511627759 (0xffffffffef) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1).
Notation "'0xfffffffff1'" (* 1099511627761 (0xfffffffff1) *)
:= (Const 1099511627761%Z).
Notation "'0xfffffffff1'" (* 1099511627761 (0xfffffffff1) *)
@@ -2465,6 +2618,10 @@ Notation "'0x14bffffffff'" (* 1425929142271 (0x14bffffffff) *)
:= (Const 1425929142271%Z).
Notation "'0x14bffffffff'" (* 1425929142271 (0x14bffffffff) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~1~0~0~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0x1ffffffffde'" (* 2199023255518 (0x1ffffffffde) *)
+ := (Const 2199023255518%Z).
+Notation "'0x1ffffffffde'" (* 2199023255518 (0x1ffffffffde) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
Notation "'0x1ffffffffe2'" (* 2199023255522 (0x1ffffffffe2) *)
:= (Const 2199023255522%Z).
Notation "'0x1ffffffffe2'" (* 2199023255522 (0x1ffffffffe2) *)
@@ -2533,6 +2690,14 @@ Notation "'0x7fffffffd03'" (* 8796093021443 (0x7fffffffd03) *)
:= (Const 8796093021443%Z).
Notation "'0x7fffffffd03'" (* 8796093021443 (0x7fffffffd03) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~0~0~1~1).
+Notation "'0x7ffffffffce'" (* 8796093022158 (0x7ffffffffce) *)
+ := (Const 8796093022158%Z).
+Notation "'0x7ffffffffce'" (* 8796093022158 (0x7ffffffffce) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1~0).
+Notation "'0x7ffffffffe3'" (* 8796093022179 (0x7ffffffffe3) *)
+ := (Const 8796093022179%Z).
+Notation "'0x7ffffffffe3'" (* 8796093022179 (0x7ffffffffe3) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~1).
Notation "'0x7ffffffffe7'" (* 8796093022183 (0x7ffffffffe7) *)
:= (Const 8796093022183%Z).
Notation "'0x7ffffffffe7'" (* 8796093022183 (0x7ffffffffe7) *)
@@ -2545,6 +2710,14 @@ Notation "'0x7fffffffff1'" (* 8796093022193 (0x7fffffffff1) *)
:= (Const 8796093022193%Z).
Notation "'0x7fffffffff1'" (* 8796093022193 (0x7fffffffff1) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1).
+Notation "'0x7fffffffff6'" (* 8796093022198 (0x7fffffffff6) *)
+ := (Const 8796093022198%Z).
+Notation "'0x7fffffffff6'" (* 8796093022198 (0x7fffffffff6) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0).
+Notation "'0x7fffffffffd'" (* 8796093022205 (0x7fffffffffd) *)
+ := (Const 8796093022205%Z).
+Notation "'0x7fffffffffd'" (* 8796093022205 (0x7fffffffffd) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1).
Notation "'0x7fffffffffe'" (* 8796093022206 (0x7fffffffffe) *)
:= (Const 8796093022206%Z).
Notation "'0x7fffffffffe'" (* 8796093022206 (0x7fffffffffe) *)
@@ -2561,14 +2734,30 @@ Notation "'0x80000000001'" (* 8796093022209 (0x80000000001) *)
:= (Const 8796093022209%Z).
Notation "'0x80000000001'" (* 8796093022209 (0x80000000001) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0xfffffbffffe'" (* 17592181850110 (0xfffffbffffe) *)
+ := (Const 17592181850110%Z).
+Notation "'0xfffffbffffe'" (* 17592181850110 (0xfffffbffffe) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
+Notation "'0xfffffffffc6'" (* 17592186044358 (0xfffffffffc6) *)
+ := (Const 17592186044358%Z).
+Notation "'0xfffffffffc6'" (* 17592186044358 (0xfffffffffc6) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~1~0).
Notation "'0xfffffffffce'" (* 17592186044366 (0xfffffffffce) *)
:= (Const 17592186044366%Z).
Notation "'0xfffffffffce'" (* 17592186044366 (0xfffffffffce) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1~0).
+Notation "'0xfffffffffda'" (* 17592186044378 (0xfffffffffda) *)
+ := (Const 17592186044378%Z).
+Notation "'0xfffffffffda'" (* 17592186044378 (0xfffffffffda) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0).
Notation "'0xfffffffffef'" (* 17592186044399 (0xfffffffffef) *)
:= (Const 17592186044399%Z).
Notation "'0xfffffffffef'" (* 17592186044399 (0xfffffffffef) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1).
+Notation "'0xffffffffffa'" (* 17592186044410 (0xffffffffffa) *)
+ := (Const 17592186044410%Z).
+Notation "'0xffffffffffa'" (* 17592186044410 (0xffffffffffa) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0).
Notation "'0xffffffffffb'" (* 17592186044411 (0xffffffffffb) *)
:= (Const 17592186044411%Z).
Notation "'0xffffffffffb'" (* 17592186044411 (0xffffffffffb) *)
@@ -2593,14 +2782,34 @@ Notation "'0x100000000001'" (* 17592186044417 (0x100000000001) *)
:= (Const 17592186044417%Z).
Notation "'0x100000000001'" (* 17592186044417 (0x100000000001) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1).
+Notation "'0x1fffffffff8b'" (* 35184372088715 (0x1fffffffff8b) *)
+ := (Const 35184372088715%Z).
+Notation "'0x1fffffffff8b'" (* 35184372088715 (0x1fffffffff8b) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0~1~1).
+Notation "'0x1fffffffffc0'" (* 35184372088768 (0x1fffffffffc0) *)
+ := (Const 35184372088768%Z).
+Notation "'0x1fffffffffc0'" (* 35184372088768 (0x1fffffffffc0) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~0~0).
+Notation "'0x1fffffffffde'" (* 35184372088798 (0x1fffffffffde) *)
+ := (Const 35184372088798%Z).
+Notation "'0x1fffffffffde'" (* 35184372088798 (0x1fffffffffde) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
Notation "'0x1ffffffffff6'" (* 35184372088822 (0x1ffffffffff6) *)
:= (Const 35184372088822%Z).
Notation "'0x1ffffffffff6'" (* 35184372088822 (0x1ffffffffff6) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0).
+Notation "'0x1ffffffffffa'" (* 35184372088826 (0x1ffffffffffa) *)
+ := (Const 35184372088826%Z).
+Notation "'0x1ffffffffffa'" (* 35184372088826 (0x1ffffffffffa) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0).
Notation "'0x1ffffffffffd'" (* 35184372088829 (0x1ffffffffffd) *)
:= (Const 35184372088829%Z).
Notation "'0x1ffffffffffd'" (* 35184372088829 (0x1ffffffffffd) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1).
+Notation "'0x1ffffffffffe'" (* 35184372088830 (0x1ffffffffffe) *)
+ := (Const 35184372088830%Z).
+Notation "'0x1ffffffffffe'" (* 35184372088830 (0x1ffffffffffe) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
Notation "'0x1fffffffffff'" (* 35184372088831 (0x1fffffffffff) *)
:= (Const 35184372088831%Z).
Notation "'0x1fffffffffff'" (* 35184372088831 (0x1fffffffffff) *)
@@ -2617,6 +2826,10 @@ Notation "'0x3fffff7fffff'" (* 70368735789055 (0x3fffff7fffff) *)
:= (Const 70368735789055%Z).
Notation "'0x3fffff7fffff'" (* 70368735789055 (0x3fffff7fffff) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
+Notation "'0x3fffffffff16'" (* 70368744177430 (0x3fffffffff16) *)
+ := (Const 70368744177430%Z).
+Notation "'0x3fffffffff16'" (* 70368744177430 (0x3fffffffff16) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0~1~1~0).
Notation "'0x3fffffffffe5'" (* 70368744177637 (0x3fffffffffe5) *)
:= (Const 70368744177637%Z).
Notation "'0x3fffffffffe5'" (* 70368744177637 (0x3fffffffffe5) *)
@@ -2625,6 +2838,14 @@ Notation "'0x3fffffffffef'" (* 70368744177647 (0x3fffffffffef) *)
:= (Const 70368744177647%Z).
Notation "'0x3fffffffffef'" (* 70368744177647 (0x3fffffffffef) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1).
+Notation "'0x3ffffffffff3'" (* 70368744177651 (0x3ffffffffff3) *)
+ := (Const 70368744177651%Z).
+Notation "'0x3ffffffffff3'" (* 70368744177651 (0x3ffffffffff3) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1).
+Notation "'0x3ffffffffffa'" (* 70368744177658 (0x3ffffffffffa) *)
+ := (Const 70368744177658%Z).
+Notation "'0x3ffffffffffa'" (* 70368744177658 (0x3ffffffffffa) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0).
Notation "'0x3ffffffffffb'" (* 70368744177659 (0x3ffffffffffb) *)
:= (Const 70368744177659%Z).
Notation "'0x3ffffffffffb'" (* 70368744177659 (0x3ffffffffffb) *)
@@ -2633,6 +2854,10 @@ Notation "'0x3ffffffffffd'" (* 70368744177661 (0x3ffffffffffd) *)
:= (Const 70368744177661%Z).
Notation "'0x3ffffffffffd'" (* 70368744177661 (0x3ffffffffffd) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1).
+Notation "'0x3ffffffffffe'" (* 70368744177662 (0x3ffffffffffe) *)
+ := (Const 70368744177662%Z).
+Notation "'0x3ffffffffffe'" (* 70368744177662 (0x3ffffffffffe) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
Notation "'0x3fffffffffff'" (* 70368744177663 (0x3fffffffffff) *)
:= (Const 70368744177663%Z).
Notation "'0x3fffffffffff'" (* 70368744177663 (0x3fffffffffff) *)
@@ -2649,10 +2874,22 @@ Notation "'0x7ffffefffffe'" (* 140737471578110 (0x7ffffefffffe) *)
:= (Const 140737471578110%Z).
Notation "'0x7ffffefffffe'" (* 140737471578110 (0x7ffffefffffe) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
+Notation "'0x7fffffffffca'" (* 140737488355274 (0x7fffffffffca) *)
+ := (Const 140737488355274%Z).
+Notation "'0x7fffffffffca'" (* 140737488355274 (0x7fffffffffca) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~0).
Notation "'0x7fffffffffde'" (* 140737488355294 (0x7fffffffffde) *)
:= (Const 140737488355294%Z).
Notation "'0x7fffffffffde'" (* 140737488355294 (0x7fffffffffde) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
+Notation "'0x7fffffffffe5'" (* 140737488355301 (0x7fffffffffe5) *)
+ := (Const 140737488355301%Z).
+Notation "'0x7fffffffffe5'" (* 140737488355301 (0x7fffffffffe5) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1).
+Notation "'0x7fffffffffe6'" (* 140737488355302 (0x7fffffffffe6) *)
+ := (Const 140737488355302%Z).
+Notation "'0x7fffffffffe6'" (* 140737488355302 (0x7fffffffffe6) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~0).
Notation "'0x7fffffffffe7'" (* 140737488355303 (0x7fffffffffe7) *)
:= (Const 140737488355303%Z).
Notation "'0x7fffffffffe7'" (* 140737488355303 (0x7fffffffffe7) *)
@@ -2661,6 +2898,10 @@ Notation "'0x7ffffffffff1'" (* 140737488355313 (0x7ffffffffff1) *)
:= (Const 140737488355313%Z).
Notation "'0x7ffffffffff1'" (* 140737488355313 (0x7ffffffffff1) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1).
+Notation "'0x7ffffffffff6'" (* 140737488355318 (0x7ffffffffff6) *)
+ := (Const 140737488355318%Z).
+Notation "'0x7ffffffffff6'" (* 140737488355318 (0x7ffffffffff6) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0).
Notation "'0x7ffffffffff7'" (* 140737488355319 (0x7ffffffffff7) *)
:= (Const 140737488355319%Z).
Notation "'0x7ffffffffff7'" (* 140737488355319 (0x7ffffffffff7) *)
@@ -2701,6 +2942,10 @@ Notation "'0xfffffffffec3'" (* 281474976710339 (0xfffffffffec3) *)
:= (Const 281474976710339%Z).
Notation "'0xfffffffffec3'" (* 281474976710339 (0xfffffffffec3) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~0~0~0~1~1).
+Notation "'0xffffffffffca'" (* 281474976710602 (0xffffffffffca) *)
+ := (Const 281474976710602%Z).
+Notation "'0xffffffffffca'" (* 281474976710602 (0xffffffffffca) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~0).
Notation "'0xffffffffffce'" (* 281474976710606 (0xffffffffffce) *)
:= (Const 281474976710606%Z).
Notation "'0xffffffffffce'" (* 281474976710606 (0xffffffffffce) *)
@@ -2713,6 +2958,10 @@ Notation "'0xffffffffffe7'" (* 281474976710631 (0xffffffffffe7) *)
:= (Const 281474976710631%Z).
Notation "'0xffffffffffe7'" (* 281474976710631 (0xffffffffffe7) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1).
+Notation "'0xffffffffffed'" (* 281474976710637 (0xffffffffffed) *)
+ := (Const 281474976710637%Z).
+Notation "'0xffffffffffed'" (* 281474976710637 (0xffffffffffed) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1).
Notation "'0xffffffffffee'" (* 281474976710638 (0xffffffffffee) *)
:= (Const 281474976710638%Z).
Notation "'0xffffffffffee'" (* 281474976710638 (0xffffffffffee) *)
@@ -2769,6 +3018,10 @@ Notation "'0x1ffffffffffce'" (* 562949953421262 (0x1ffffffffffce) *)
:= (Const 562949953421262%Z).
Notation "'0x1ffffffffffce'" (* 562949953421262 (0x1ffffffffffce) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~1~1~0).
+Notation "'0x1ffffffffffda'" (* 562949953421274 (0x1ffffffffffda) *)
+ := (Const 562949953421274%Z).
+Notation "'0x1ffffffffffda'" (* 562949953421274 (0x1ffffffffffda) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0).
Notation "'0x1ffffffffffdf'" (* 562949953421279 (0x1ffffffffffdf) *)
:= (Const 562949953421279%Z).
Notation "'0x1ffffffffffdf'" (* 562949953421279 (0x1ffffffffffdf) *)
@@ -2785,6 +3038,10 @@ Notation "'0x1fffffffffff1'" (* 562949953421297 (0x1fffffffffff1) *)
:= (Const 562949953421297%Z).
Notation "'0x1fffffffffff1'" (* 562949953421297 (0x1fffffffffff1) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1).
+Notation "'0x1fffffffffff7'" (* 562949953421303 (0x1fffffffffff7) *)
+ := (Const 562949953421303%Z).
+Notation "'0x1fffffffffff7'" (* 562949953421303 (0x1fffffffffff7) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1).
Notation "'0x1fffffffffffe'" (* 562949953421310 (0x1fffffffffffe) *)
:= (Const 562949953421310%Z).
Notation "'0x1fffffffffffe'" (* 562949953421310 (0x1fffffffffffe) *)
@@ -2817,6 +3074,10 @@ Notation "'0x3ffffffffffe2'" (* 1125899906842594 (0x3ffffffffffe2) *)
:= (Const 1125899906842594%Z).
Notation "'0x3ffffffffffe2'" (* 1125899906842594 (0x3ffffffffffe2) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0).
+Notation "'0x3ffffffffffee'" (* 1125899906842606 (0x3ffffffffffee) *)
+ := (Const 1125899906842606%Z).
+Notation "'0x3ffffffffffee'" (* 1125899906842606 (0x3ffffffffffee) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0).
Notation "'0x3ffffffffffef'" (* 1125899906842607 (0x3ffffffffffef) *)
:= (Const 1125899906842607%Z).
Notation "'0x3ffffffffffef'" (* 1125899906842607 (0x3ffffffffffef) *)
@@ -2885,6 +3146,10 @@ Notation "'0x7ffffffffffed'" (* 2251799813685229 (0x7ffffffffffed) *)
:= (Const 2251799813685229%Z).
Notation "'0x7ffffffffffed'" (* 2251799813685229 (0x7ffffffffffed) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1).
+Notation "'0x7ffffffffffef'" (* 2251799813685231 (0x7ffffffffffef) *)
+ := (Const 2251799813685231%Z).
+Notation "'0x7ffffffffffef'" (* 2251799813685231 (0x7ffffffffffef) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1).
Notation "'0x7fffffffffff6'" (* 2251799813685238 (0x7fffffffffff6) *)
:= (Const 2251799813685238%Z).
Notation "'0x7fffffffffff6'" (* 2251799813685238 (0x7fffffffffff6) *)
@@ -2961,6 +3226,10 @@ Notation "'0xfffffffffffda'" (* 4503599627370458 (0xfffffffffffda) *)
:= (Const 4503599627370458%Z).
Notation "'0xfffffffffffda'" (* 4503599627370458 (0xfffffffffffda) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~1~0).
+Notation "'0xfffffffffffde'" (* 4503599627370462 (0xfffffffffffde) *)
+ := (Const 4503599627370462%Z).
+Notation "'0xfffffffffffde'" (* 4503599627370462 (0xfffffffffffde) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
Notation "'0xfffffffffffee'" (* 4503599627370478 (0xfffffffffffee) *)
:= (Const 4503599627370478%Z).
Notation "'0xfffffffffffee'" (* 4503599627370478 (0xfffffffffffee) *)
@@ -3017,6 +3286,10 @@ Notation "'0x1fffffffffffe3'" (* 9007199254740963 (0x1fffffffffffe3) *)
:= (Const 9007199254740963%Z).
Notation "'0x1fffffffffffe3'" (* 9007199254740963 (0x1fffffffffffe3) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~1).
+Notation "'0x1ffffffffffff1'" (* 9007199254740977 (0x1ffffffffffff1) *)
+ := (Const 9007199254740977%Z).
+Notation "'0x1ffffffffffff1'" (* 9007199254740977 (0x1ffffffffffff1) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1).
Notation "'0x1ffffffffffff6'" (* 9007199254740982 (0x1ffffffffffff6) *)
:= (Const 9007199254740982%Z).
Notation "'0x1ffffffffffff6'" (* 9007199254740982 (0x1ffffffffffff6) *)
@@ -3045,6 +3318,10 @@ Notation "'0x3fffffffffffc6'" (* 18014398509481926 (0x3fffffffffffc6) *)
:= (Const 18014398509481926%Z).
Notation "'0x3fffffffffffc6'" (* 18014398509481926 (0x3fffffffffffc6) *)
:= (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~1~0).
+Notation "'0x3fffffffffffe2'" (* 18014398509481954 (0x3fffffffffffe2) *)
+ := (Const 18014398509481954%Z).
+Notation "'0x3fffffffffffe2'" (* 18014398509481954 (0x3fffffffffffe2) *)
+ := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0).
Notation "'0x3ffffffffffff7'" (* 18014398509481975 (0x3ffffffffffff7) *)
:= (Const 18014398509481975%Z).
Notation "'0x3ffffffffffff7'" (* 18014398509481975 (0x3ffffffffffff7) *)
@@ -3293,6 +3570,10 @@ Notation "'0x7ffffffffffffef'" (* 576460752303423471 (0x7ffffffffffffef) *)
:= (Const 576460752303423471%Z).
Notation "'0x7ffffffffffffef'" (* 576460752303423471 (0x7ffffffffffffef) *)
:= (Const WO~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1).
+Notation "'0x7fffffffffffff1'" (* 576460752303423473 (0x7fffffffffffff1) *)
+ := (Const 576460752303423473%Z).
+Notation "'0x7fffffffffffff1'" (* 576460752303423473 (0x7fffffffffffff1) *)
+ := (Const WO~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1).
Notation "'0x7fffffffffffffa'" (* 576460752303423482 (0x7fffffffffffffa) *)
:= (Const 576460752303423482%Z).
Notation "'0x7fffffffffffffa'" (* 576460752303423482 (0x7fffffffffffffa) *)
@@ -3329,6 +3610,10 @@ Notation "'0xfffffffffffffde'" (* 1152921504606846942 (0xfffffffffffffde) *)
:= (Const 1152921504606846942%Z).
Notation "'0xfffffffffffffde'" (* 1152921504606846942 (0xfffffffffffffde) *)
:= (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~0).
+Notation "'0xfffffffffffffe2'" (* 1152921504606846946 (0xfffffffffffffe2) *)
+ := (Const 1152921504606846946%Z).
+Notation "'0xfffffffffffffe2'" (* 1152921504606846946 (0xfffffffffffffe2) *)
+ := (Const WO~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0).
Notation "'0xffffffffffffffe'" (* 1152921504606846974 (0xffffffffffffffe) *)
:= (Const 1152921504606846974%Z).
Notation "'0xffffffffffffffe'" (* 1152921504606846974 (0xffffffffffffffe) *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 03:22:59 +0000