Add more constant notations

2 files changed, 384 insertions, 0 deletions

diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index 67fb1a260..847bac809 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -102,6 +102,7 @@ nums = tuple(sorted(set(systematic_nums + [
     134217703,
     134217710,
     134217713,
+    134217718,
     134217719,
     134217726,
     268431360,
@@ -124,6 +125,8 @@ nums = tuple(sorted(set(systematic_nums + [
     1332920885,
     1749801491,
     2147483631,
+    2147483642,
+    2147483646,
     2147483647,
     2863311531,
     2969567231,
@@ -171,9 +174,13 @@ nums = tuple(sorted(set(systematic_nums + [
     34359738341,
     34359738349,
     34359738355,
+    34359738366,
+    68719476682,
     68719476707,
+    68719476710,
     68719476727,
     68719476733,
+    68719476734,
     137436856320,
     137438952991,
     137438953285,
@@ -183,10 +190,16 @@ nums = tuple(sorted(set(systematic_nums + [
     274877906939,
     274877906941,
     549755813783,
+    549755813854,
     549755813869,
+    549755813886,
+    1099511627738,
     1099511627761,
+    1099511627774,
     1425929142271,
+    2199023255522,
     2199023255543,
+    2199023255550,
     4363955208191,
     4398046511079,
     4398046511099,
@@ -195,9 +208,13 @@ nums = tuple(sorted(set(systematic_nums + [
     8796093022183,
     8796093022189,
     8796093022193,
+    8796093022206,
+    17592186044366,
     17592186044399,
     17592186044411,
     17592186044413,
+    17592186044414,
+    35184372088822,
     35184372088829,
     70368735789055,
     70368744177637,
@@ -213,18 +230,27 @@ nums = tuple(sorted(set(systematic_nums + [
     281474976645119,
     281474976710339,
     281474976710631,
+    281474976710638,
     281474976710639,
     281474976710645,
     281474976710647,
     281474976710653,
+    281474976710654,
+    562949953290238,
+    562949953421262,
     562949953421279,
+    562949953421290,
     562949953421293,
     562949953421297,
+    562949953421310,
     1125899873288191,
+    1125899906842558,
     1125899906842593,
+    1125899906842594,
     1125899906842607,
     1125899906842619,
     1125899906842621,
+    1125899906842622,
     1460151441686527,
     2211942517178367,
     2234929182146559,
@@ -232,9 +258,14 @@ nums = tuple(sorted(set(systematic_nums + [
     2251799813160960,
     2251799813684483,
     2251799813685210,
+    2251799813685214,
     2251799813685217,
     2251799813685229,
+    2251799813685238,
     2251799813685239,
+    2251799813685242,
+    2251799813685246,
+    2920302883373054,
     4503595332402223,
     4503599627369927,
     4503599627370015,
@@ -246,6 +277,9 @@ nums = tuple(sorted(set(systematic_nums + [
     4503599627370494,
     9007199187632127,
     9007199254740963,
+    9007199254740982,
+    9007199254740990,
+    18014398509481926,
     18014398509481975,
     18014398509481981,
     18014398509481982,
@@ -253,24 +287,38 @@ nums = tuple(sorted(set(systematic_nums + [
     36028797018963943,
     36028797018963947,
     36028797018963949,
+    36028797018963962,
+    36028797018963964,
+    36028797018963966,
     72056494526300160,
     72057594037927819,
+    72057594037927886,
     72057594037927919,
     72057594037927931,
     72057594037927933,
     72057594037927934,
+    144115188075855638,
     144115188075855853,
     144115188075855857,
+    144115188075855862,
     144115188075855863,
+    144115188075855866,
     144115188075855867,
     144115188075855869,
     144115188075855870,
+    288230376151711706,
     288230376151711717,
     288230376151711727,
+    288230376151711734,
     288230376151711741,
+    288230376151711742,
+    576460752303423434,
+    576460752303423454,
     576460752303423467,
     576460752303423469,
     576460752303423471,
+    576460752303423482,
+    576460752303423486,
     1117984489315730401,
     1152921504606846974,
     3353953467947191203,
@@ -927,6 +975,8 @@ Notation "'0b111111111111111111111101110'" (* 134217710 (0x7ffffee) *)
   := (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~0~1~1~1~0).
 Notation "'0b111111111111111111111110001'" (* 134217713 (0x7fffff1) *)
   := (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~0~0~0~1).
+Notation "'0b111111111111111111111110110'" (* 134217718 (0x7fffff6) *)
+  := (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~0~1~1~0).
 Notation "'0b111111111111111111111110111'" (* 134217719 (0x7fffff7) *)
   := (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~0~1~1~1).
 Notation "'0b111111111111111111111111110'" (* 134217726 (0x7fffffe) *)
@@ -995,6 +1045,10 @@ Notation "'0b1101000010010111101101000010011'" (* 1749801491 (0x684bda13) *)
   := (Const WO~0~1~1~0~1~0~0~0~0~1~0~0~1~0~1~1~1~1~0~1~1~0~1~0~0~0~0~1~0~0~1~1).
 Notation "'0b1111111111111111111111111101111'" (* 2147483631 (0x7fffffef) *)
   := (Const WO~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~0~1~1~1~1).
+Notation "'0b1111111111111111111111111111010'" (* 2147483642 (0x7ffffffa) *)
+  := (Const WO~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~0).
+Notation "'0b1111111111111111111111111111110'" (* 2147483646 (0x7ffffffe) *)
+  := (Const WO~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).
 Notation "'0b1111111111111111111111111111111'" (* 2147483647 (0x7fffffff) *)
   := (Const WO~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).
 Notation "'0b10000000000000000000000000000000'" (* 2147483648 (0x80000000) *)
@@ -1111,18 +1165,26 @@ Notation "'0b11111111111111111111111111111101101'" (* 34359738349 (0x7ffffffed)
   := (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~1~1~1~1~1~1~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 "'0b11111111111111111111111111111110011'" (* 34359738355 (0x7fffffff3) *)
   := (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~1~1~1~1~1~1~1~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 "'0b11111111111111111111111111111111110'" (* 34359738366 (0x7fffffffe) *)
+  := (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~1~1~1~1~1~1~1~1~1~1~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 "'0b11111111111111111111111111111111111'" (* 34359738367 (0x7ffffffff) *)
   := (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~1~1~1~1~1~1~1~1~1~1~1~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 "'0b100000000000000000000000000000000000'" (* 34359738368 (0x800000000) *)
   := (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~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).
 Notation "'0b100000000000000000000000000000000001'" (* 34359738369 (0x800000001) *)
   := (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~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~1).
+Notation "'0b111111111111111111111111111111001010'" (* 68719476682 (0xfffffffca) *)
+  := (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~1~1~1~1~1~1~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 "'0b111111111111111111111111111111100011'" (* 68719476707 (0xfffffffe3) *)
   := (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~1~1~1~1~1~1~1~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 "'0b111111111111111111111111111111100110'" (* 68719476710 (0xfffffffe6) *)
+  := (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~1~1~1~1~1~1~1~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 "'0b111111111111111111111111111111110111'" (* 68719476727 (0xffffffff7) *)
   := (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~1~1~1~1~1~1~1~1~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 "'0b111111111111111111111111111111111101'" (* 68719476733 (0xffffffffd) *)
   := (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~1~1~1~1~1~1~1~1~1~1~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 "'0b111111111111111111111111111111111110'" (* 68719476734 (0xffffffffe) *)
+  := (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~1~1~1~1~1~1~1~1~1~1~1~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 "'0b111111111111111111111111111111111111'" (* 68719476735 (0xfffffffff) *)
   := (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~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0b1000000000000000000000000000000000000'" (* 68719476736 (0x1000000000) *)
@@ -1159,16 +1221,24 @@ Notation "'0b100000000000000000000000000000000000001'" (* 274877906945 (0x400000
   := (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 "'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 "'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 "'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 "'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) *)
   := (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~1).
 Notation "'0b1000000000000000000000000000000000000000'" (* 549755813888 (0x8000000000) *)
   := (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~0).
 Notation "'0b1000000000000000000000000000000000000001'" (* 549755813889 (0x8000000001) *)
   := (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 "'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 "'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) *)
+  := (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~1~1~1~0).
 Notation "'0b1111111111111111111111111111111111111111'" (* 1099511627775 (0xffffffffff) *)
   := (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~1~1~1~1).
 Notation "'0b10000000000000000000000000000000000000000'" (* 1099511627776 (0x10000000000) *)
@@ -1177,8 +1247,12 @@ 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 "'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) *)
   := (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~1~0~1~1~1).
+Notation "'0b11111111111111111111111111111111111111110'" (* 2199023255550 (0x1fffffffffe) *)
+  := (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~1~1~1~1~0).
 Notation "'0b11111111111111111111111111111111111111111'" (* 2199023255551 (0x1ffffffffff) *)
   := (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~1~1~1~1~1).
 Notation "'0b100000000000000000000000000000000000000000'" (* 2199023255552 (0x20000000000) *)
@@ -1207,24 +1281,32 @@ Notation "'0b1111111111111111111111111111111111111101101'" (* 8796093022189 (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~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 "'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) *)
   := (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~1).
 Notation "'0b10000000000000000000000000000000000000000000'" (* 8796093022208 (0x80000000000) *)
   := (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 "'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 "'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 "'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) *)
   := (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~1~0~1).
+Notation "'0b11111111111111111111111111111111111111111110'" (* 17592186044414 (0xffffffffffe) *)
+  := (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~1~1~0).
 Notation "'0b11111111111111111111111111111111111111111111'" (* 17592186044415 (0xfffffffffff) *)
   := (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~1~1~1).
 Notation "'0b100000000000000000000000000000000000000000000'" (* 17592186044416 (0x100000000000) *)
   := (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 "'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 "'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 "'0b111111111111111111111111111111111111111111111'" (* 35184372088831 (0x1fffffffffff) *)
@@ -1273,6 +1355,8 @@ Notation "'0b111111111111111111111111111111111111111011000011'" (* 2814749767103
   := (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 "'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 "'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) *)
   := (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~1).
 Notation "'0b111111111111111111111111111111111111111111110101'" (* 281474976710645 (0xfffffffffff5) *)
@@ -1281,18 +1365,28 @@ Notation "'0b111111111111111111111111111111111111111111110111'" (* 2814749767106
   := (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~1~0~1~1~1).
 Notation "'0b111111111111111111111111111111111111111111111101'" (* 281474976710653 (0xfffffffffffd) *)
   := (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~1~1~1~0~1).
+Notation "'0b111111111111111111111111111111111111111111111110'" (* 281474976710654 (0xfffffffffffe) *)
+  := (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~1~1~1~1~0).
 Notation "'0b111111111111111111111111111111111111111111111111'" (* 281474976710655 (0xffffffffffff) *)
   := (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~1~1~1~1~1).
 Notation "'0b1000000000000000000000000000000000000000000000000'" (* 281474976710656 (0x1000000000000) *)
   := (Const WO~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~0~0~0).
 Notation "'0b1000000000000000000000000000000000000000000000001'" (* 281474976710657 (0x1000000000001) *)
   := (Const WO~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~0~0~1).
+Notation "'0b1111111111111111111111111111111011111111111111110'" (* 562949953290238 (0x1fffffffdfffe) *)
+  := (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~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~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 "'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) *)
+  := (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~0~1~0).
 Notation "'0b1111111111111111111111111111111111111111111101101'" (* 562949953421293 (0x1ffffffffffed) *)
   := (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 "'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) *)
   := (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~1).
 Notation "'0b10000000000000000000000000000000000000000000000000'" (* 562949953421312 (0x2000000000000) *)
@@ -1301,14 +1395,20 @@ Notation "'0b10000000000000000000000000000000000000000000000001'" (* 56294995342
   := (Const WO~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~0~0~0~1).
 Notation "'0b11111111111111111111111101111111111111111111111111'" (* 1125899873288191 (0x3fffffdffffff) *)
   := (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~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 "'0b11111111111111111111111111111111111111111110111110'" (* 1125899906842558 (0x3ffffffffffbe) *)
+  := (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~0~1~1~1~1~1~0).
 Notation "'0b11111111111111111111111111111111111111111111100001'" (* 1125899906842593 (0x3ffffffffffe1) *)
   := (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 "'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) *)
   := (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~1~1~0~1~1).
 Notation "'0b11111111111111111111111111111111111111111111111101'" (* 1125899906842621 (0x3fffffffffffd) *)
   := (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~1~1~1~0~1).
+Notation "'0b11111111111111111111111111111111111111111111111110'" (* 1125899906842622 (0x3fffffffffffe) *)
+  := (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~1~1~1~1~0).
 Notation "'0b11111111111111111111111111111111111111111111111111'" (* 1125899906842623 (0x3ffffffffffff) *)
   := (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~1~1~1~1~1).
 Notation "'0b100000000000000000000000000000000000000000000000000'" (* 1125899906842624 (0x4000000000000) *)
@@ -1329,18 +1429,28 @@ Notation "'0b111111111111111111111111111111111111111110100000011'" (* 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~0~1~0~0~0~0~0~0~1~1).
 Notation "'0b111111111111111111111111111111111111111111111011010'" (* 2251799813685210 (0x7ffffffffffda) *)
   := (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~0~1~1~0~1~0).
+Notation "'0b111111111111111111111111111111111111111111111011110'" (* 2251799813685214 (0x7ffffffffffde) *)
+  := (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~0~1~1~1~1~0).
 Notation "'0b111111111111111111111111111111111111111111111100001'" (* 2251799813685217 (0x7ffffffffffe1) *)
   := (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 "'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) *)
   := (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~1).
+Notation "'0b111111111111111111111111111111111111111111111111010'" (* 2251799813685242 (0x7fffffffffffa) *)
+  := (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~1~0~1~0).
+Notation "'0b111111111111111111111111111111111111111111111111110'" (* 2251799813685246 (0x7fffffffffffe) *)
+  := (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~1~1~1~0).
 Notation "'0b111111111111111111111111111111111111111111111111111'" (* 2251799813685247 (0x7ffffffffffff) *)
   := (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~1~1~1~1).
 Notation "'0b1000000000000000000000000000000000000000000000000000'" (* 2251799813685248 (0x8000000000000) *)
   := (Const WO~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~0~0~0~0~0~0).
 Notation "'0b1000000000000000000000000000000000000000000000000001'" (* 2251799813685249 (0x8000000000001) *)
   := (Const WO~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~0~0~0~0~0~1).
+Notation "'0b1010010111111111111111111111111111111111111111111110'" (* 2920302883373054 (0xa5ffffffffffe) *)
+  := (Const WO~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~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0b1111111111111111111011111111111111111111110000101111'" (* 4503595332402223 (0xffffefffffc2f) *)
   := (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~0~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~1~1~1~1).
 Notation "'0b1111111111111111111111111111111111111111110111000111'" (* 4503599627369927 (0xffffffffffdc7) *)
@@ -1369,12 +1479,18 @@ Notation "'0b11111111111111111111111111011111111111111111111111111'" (* 90071991
   := (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~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).
 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 "'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 "'0b11111111111111111111111111111111111111111111111111110'" (* 9007199254740990 (0x1ffffffffffffe) *)
+  := (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~1~1~1~0).
 Notation "'0b11111111111111111111111111111111111111111111111111111'" (* 9007199254740991 (0x1fffffffffffff) *)
   := (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~1~1~1~1).
 Notation "'0b100000000000000000000000000000000000000000000000000000'" (* 9007199254740992 (0x20000000000000) *)
   := (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~0).
 Notation "'0b100000000000000000000000000000000000000000000000000001'" (* 9007199254740993 (0x20000000000001) *)
   := (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 "'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) *)
@@ -1395,6 +1511,12 @@ Notation "'0b1111111111111111111111111111111111111111111111111101011'" (* 360287
   := (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~1~1~1~1~1~1~1~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~1).
 Notation "'0b1111111111111111111111111111111111111111111111111101101'" (* 36028797018963949 (0x7fffffffffffed) *)
   := (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~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111111111010'" (* 36028797018963962 (0x7ffffffffffffa) *)
+  := (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~1~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111111111100'" (* 36028797018963964 (0x7ffffffffffffc) *)
+  := (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~1~1~1~1~1~1~1~1~1~1~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).
+Notation "'0b1111111111111111111111111111111111111111111111111111110'" (* 36028797018963966 (0x7ffffffffffffe) *)
+  := (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~1~1~1~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111111111111'" (* 36028797018963967 (0x7fffffffffffff) *)
   := (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~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0b10000000000000000000000000000000000000000000000000000000'" (* 36028797018963968 (0x80000000000000) *)
@@ -1405,6 +1527,8 @@ Notation "'0b11111111111111110000000000000000000000000000000000000000'" (* 72056
   := (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~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~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 "'0b11111111111111111111111111111111111111111111111110001011'" (* 72057594037927819 (0xffffffffffff8b) *)
   := (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~1~1~1~1~1~1~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 "'0b11111111111111111111111111111111111111111111111111001110'" (* 72057594037927886 (0xffffffffffffce) *)
+  := (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~1~1~1~1~1~1~1~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 "'0b11111111111111111111111111111111111111111111111111101111'" (* 72057594037927919 (0xffffffffffffef) *)
   := (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~1~1~1~1~1~1~1~1~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 "'0b11111111111111111111111111111111111111111111111111111011'" (* 72057594037927931 (0xfffffffffffffb) *)
@@ -1419,12 +1543,18 @@ Notation "'0b100000000000000000000000000000000000000000000000000000000'" (* 7205
   := (Const WO~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~0~0~0~0).
 Notation "'0b100000000000000000000000000000000000000000000000000000001'" (* 72057594037927937 (0x100000000000001) *)
   := (Const WO~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~0~0~0~1).
+Notation "'0b111111111111111111111111111111111111111111111111100010110'" (* 144115188075855638 (0x1ffffffffffff16) *)
+  := (Const WO~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~1~1~0).
 Notation "'0b111111111111111111111111111111111111111111111111111101101'" (* 144115188075855853 (0x1ffffffffffffed) *)
   := (Const WO~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~1~1~0~1~1~0~1).
 Notation "'0b111111111111111111111111111111111111111111111111111110001'" (* 144115188075855857 (0x1fffffffffffff1) *)
   := (Const WO~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~1~1~1~0~0~0~1).
+Notation "'0b111111111111111111111111111111111111111111111111111110110'" (* 144115188075855862 (0x1fffffffffffff6) *)
+  := (Const WO~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~1~1~1~0~1~1~0).
 Notation "'0b111111111111111111111111111111111111111111111111111110111'" (* 144115188075855863 (0x1fffffffffffff7) *)
   := (Const WO~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~1~1~1~0~1~1~1).
+Notation "'0b111111111111111111111111111111111111111111111111111111010'" (* 144115188075855866 (0x1fffffffffffffa) *)
+  := (Const WO~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~1~1~1~1~0~1~0).
 Notation "'0b111111111111111111111111111111111111111111111111111111011'" (* 144115188075855867 (0x1fffffffffffffb) *)
   := (Const WO~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~1~1~1~1~0~1~1).
 Notation "'0b111111111111111111111111111111111111111111111111111111101'" (* 144115188075855869 (0x1fffffffffffffd) *)
@@ -1437,24 +1567,38 @@ Notation "'0b1000000000000000000000000000000000000000000000000000000000'" (* 144
   := (Const WO~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~0~0~0~0~0).
 Notation "'0b1000000000000000000000000000000000000000000000000000000001'" (* 144115188075855873 (0x200000000000001) *)
   := (Const WO~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~0~0~0~0~1).
+Notation "'0b1111111111111111111111111111111111111111111111111111011010'" (* 288230376151711706 (0x3ffffffffffffda) *)
+  := (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~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111111111100101'" (* 288230376151711717 (0x3ffffffffffffe5) *)
   := (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~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111111111101111'" (* 288230376151711727 (0x3ffffffffffffef) *)
   := (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~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111111111110110'" (* 288230376151711734 (0x3fffffffffffff6) *)
+  := (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~1~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111111111111101'" (* 288230376151711741 (0x3fffffffffffffd) *)
   := (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~1~1~1~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111111111111110'" (* 288230376151711742 (0x3fffffffffffffe) *)
+  := (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~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0b1111111111111111111111111111111111111111111111111111111111'" (* 288230376151711743 (0x3ffffffffffffff) *)
   := (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~1~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0b10000000000000000000000000000000000000000000000000000000000'" (* 288230376151711744 (0x400000000000000) *)
   := (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~0~0~0~0~0~0~0~0~0~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 "'0b10000000000000000000000000000000000000000000000000000000001'" (* 288230376151711745 (0x400000000000001) *)
   := (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~0~0~0~0~0~0~0~0~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 "'0b11111111111111111111111111111111111111111111111111111001010'" (* 576460752303423434 (0x7ffffffffffffca) *)
+  := (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~0~0~1~0~1~0).
+Notation "'0b11111111111111111111111111111111111111111111111111111011110'" (* 576460752303423454 (0x7ffffffffffffde) *)
+  := (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~0~1~1~1~1~0).
 Notation "'0b11111111111111111111111111111111111111111111111111111101011'" (* 576460752303423467 (0x7ffffffffffffeb) *)
   := (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~0~1~1).
 Notation "'0b11111111111111111111111111111111111111111111111111111101101'" (* 576460752303423469 (0x7ffffffffffffed) *)
   := (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 "'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) *)
+  := (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~1~1~0).
 Notation "'0b11111111111111111111111111111111111111111111111111111111111'" (* 576460752303423487 (0x7ffffffffffffff) *)
   := (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~1~1~1).
 Notation "'0b100000000000000000000000000000000000000000000000000000000000'" (* 576460752303423488 (0x800000000000000) *)
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index 05898aa28..e3c7c5be4 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -102,6 +102,7 @@ nums = tuple(sorted(set(systematic_nums + [
     134217703,
     134217710,
     134217713,
+    134217718,
     134217719,
     134217726,
     268431360,
@@ -124,6 +125,8 @@ nums = tuple(sorted(set(systematic_nums + [
     1332920885,
     1749801491,
     2147483631,
+    2147483642,
+    2147483646,
     2147483647,
     2863311531,
     2969567231,
@@ -171,9 +174,13 @@ nums = tuple(sorted(set(systematic_nums + [
     34359738341,
     34359738349,
     34359738355,
+    34359738366,
+    68719476682,
     68719476707,
+    68719476710,
     68719476727,
     68719476733,
+    68719476734,
     137436856320,
     137438952991,
     137438953285,
@@ -183,10 +190,16 @@ nums = tuple(sorted(set(systematic_nums + [
     274877906939,
     274877906941,
     549755813783,
+    549755813854,
     549755813869,
+    549755813886,
+    1099511627738,
     1099511627761,
+    1099511627774,
     1425929142271,
+    2199023255522,
     2199023255543,
+    2199023255550,
     4363955208191,
     4398046511079,
     4398046511099,
@@ -195,9 +208,13 @@ nums = tuple(sorted(set(systematic_nums + [
     8796093022183,
     8796093022189,
     8796093022193,
+    8796093022206,
+    17592186044366,
     17592186044399,
     17592186044411,
     17592186044413,
+    17592186044414,
+    35184372088822,
     35184372088829,
     70368735789055,
     70368744177637,
@@ -213,18 +230,27 @@ nums = tuple(sorted(set(systematic_nums + [
     281474976645119,
     281474976710339,
     281474976710631,
+    281474976710638,
     281474976710639,
     281474976710645,
     281474976710647,
     281474976710653,
+    281474976710654,
+    562949953290238,
+    562949953421262,
     562949953421279,
+    562949953421290,
     562949953421293,
     562949953421297,
+    562949953421310,
     1125899873288191,
+    1125899906842558,
     1125899906842593,
+    1125899906842594,
     1125899906842607,
     1125899906842619,
     1125899906842621,
+    1125899906842622,
     1460151441686527,
     2211942517178367,
     2234929182146559,
@@ -232,9 +258,14 @@ nums = tuple(sorted(set(systematic_nums + [
     2251799813160960,
     2251799813684483,
     2251799813685210,
+    2251799813685214,
     2251799813685217,
     2251799813685229,
+    2251799813685238,
     2251799813685239,
+    2251799813685242,
+    2251799813685246,
+    2920302883373054,
     4503595332402223,
     4503599627369927,
     4503599627370015,
@@ -246,6 +277,9 @@ nums = tuple(sorted(set(systematic_nums + [
     4503599627370494,
     9007199187632127,
     9007199254740963,
+    9007199254740982,
+    9007199254740990,
+    18014398509481926,
     18014398509481975,
     18014398509481981,
     18014398509481982,
@@ -253,24 +287,38 @@ nums = tuple(sorted(set(systematic_nums + [
     36028797018963943,
     36028797018963947,
     36028797018963949,
+    36028797018963962,
+    36028797018963964,
+    36028797018963966,
     72056494526300160,
     72057594037927819,
+    72057594037927886,
     72057594037927919,
     72057594037927931,
     72057594037927933,
     72057594037927934,
+    144115188075855638,
     144115188075855853,
     144115188075855857,
+    144115188075855862,
     144115188075855863,
+    144115188075855866,
     144115188075855867,
     144115188075855869,
     144115188075855870,
+    288230376151711706,
     288230376151711717,
     288230376151711727,
+    288230376151711734,
     288230376151711741,
+    288230376151711742,
+    576460752303423434,
+    576460752303423454,
     576460752303423467,
     576460752303423469,
     576460752303423471,
+    576460752303423482,
+    576460752303423486,
     1117984489315730401,
     1152921504606846974,
     3353953467947191203,
@@ -1475,6 +1523,10 @@ Notation "'0x7fffff1'" (* 134217713 (0x7fffff1) *)
   := (Const 134217713%Z).
 Notation "'0x7fffff1'" (* 134217713 (0x7fffff1) *)
   := (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~0~0~0~1).
+Notation "'0x7fffff6'" (* 134217718 (0x7fffff6) *)
+  := (Const 134217718%Z).
+Notation "'0x7fffff6'" (* 134217718 (0x7fffff6) *)
+  := (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~0~1~1~0).
 Notation "'0x7fffff7'" (* 134217719 (0x7fffff7) *)
   := (Const 134217719%Z).
 Notation "'0x7fffff7'" (* 134217719 (0x7fffff7) *)
@@ -1611,6 +1663,14 @@ Notation "'0x7fffffef'" (* 2147483631 (0x7fffffef) *)
   := (Const 2147483631%Z).
 Notation "'0x7fffffef'" (* 2147483631 (0x7fffffef) *)
   := (Const WO~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~0~1~1~1~1).
+Notation "'0x7ffffffa'" (* 2147483642 (0x7ffffffa) *)
+  := (Const 2147483642%Z).
+Notation "'0x7ffffffa'" (* 2147483642 (0x7ffffffa) *)
+  := (Const WO~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~0).
+Notation "'0x7ffffffe'" (* 2147483646 (0x7ffffffe) *)
+  := (Const 2147483646%Z).
+Notation "'0x7ffffffe'" (* 2147483646 (0x7ffffffe) *)
+  := (Const WO~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).
 Notation "'0x7fffffff'" (* 2147483647 (0x7fffffff) *)
   := (Const 2147483647%Z).
 Notation "'0x7fffffff'" (* 2147483647 (0x7fffffff) *)
@@ -1843,6 +1903,10 @@ Notation "'0x7fffffff3'" (* 34359738355 (0x7fffffff3) *)
   := (Const 34359738355%Z).
 Notation "'0x7fffffff3'" (* 34359738355 (0x7fffffff3) *)
   := (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~1~1~1~1~1~1~1~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 "'0x7fffffffe'" (* 34359738366 (0x7fffffffe) *)
+  := (Const 34359738366%Z).
+Notation "'0x7fffffffe'" (* 34359738366 (0x7fffffffe) *)
+  := (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~1~1~1~1~1~1~1~1~1~1~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 "'0x7ffffffff'" (* 34359738367 (0x7ffffffff) *)
   := (Const 34359738367%Z).
 Notation "'0x7ffffffff'" (* 34359738367 (0x7ffffffff) *)
@@ -1855,10 +1919,18 @@ Notation "'0x800000001'" (* 34359738369 (0x800000001) *)
   := (Const 34359738369%Z).
 Notation "'0x800000001'" (* 34359738369 (0x800000001) *)
   := (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~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~1).
+Notation "'0xfffffffca'" (* 68719476682 (0xfffffffca) *)
+  := (Const 68719476682%Z).
+Notation "'0xfffffffca'" (* 68719476682 (0xfffffffca) *)
+  := (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~1~1~1~1~1~1~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 "'0xfffffffe3'" (* 68719476707 (0xfffffffe3) *)
   := (Const 68719476707%Z).
 Notation "'0xfffffffe3'" (* 68719476707 (0xfffffffe3) *)
   := (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~1~1~1~1~1~1~1~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 "'0xfffffffe6'" (* 68719476710 (0xfffffffe6) *)
+  := (Const 68719476710%Z).
+Notation "'0xfffffffe6'" (* 68719476710 (0xfffffffe6) *)
+  := (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~1~1~1~1~1~1~1~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 "'0xffffffff7'" (* 68719476727 (0xffffffff7) *)
   := (Const 68719476727%Z).
 Notation "'0xffffffff7'" (* 68719476727 (0xffffffff7) *)
@@ -1867,6 +1939,10 @@ Notation "'0xffffffffd'" (* 68719476733 (0xffffffffd) *)
   := (Const 68719476733%Z).
 Notation "'0xffffffffd'" (* 68719476733 (0xffffffffd) *)
   := (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~1~1~1~1~1~1~1~1~1~1~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 "'0xffffffffe'" (* 68719476734 (0xffffffffe) *)
+  := (Const 68719476734%Z).
+Notation "'0xffffffffe'" (* 68719476734 (0xffffffffe) *)
+  := (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~1~1~1~1~1~1~1~1~1~1~1~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 "'0xfffffffff'" (* 68719476735 (0xfffffffff) *)
   := (Const 68719476735%Z).
 Notation "'0xfffffffff'" (* 68719476735 (0xfffffffff) *)
@@ -1939,10 +2015,18 @@ 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 "'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 "'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 "'0x7ffffffffe'" (* 549755813886 (0x7ffffffffe) *)
+  := (Const 549755813886%Z).
+Notation "'0x7ffffffffe'" (* 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 "'0x7fffffffff'" (* 549755813887 (0x7fffffffff) *)
   := (Const 549755813887%Z).
 Notation "'0x7fffffffff'" (* 549755813887 (0x7fffffffff) *)
@@ -1955,10 +2039,18 @@ Notation "'0x8000000001'" (* 549755813889 (0x8000000001) *)
   := (Const 549755813889%Z).
 Notation "'0x8000000001'" (* 549755813889 (0x8000000001) *)
   := (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 "'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 "'0xfffffffff1'" (* 1099511627761 (0xfffffffff1) *)
   := (Const 1099511627761%Z).
 Notation "'0xfffffffff1'" (* 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 "'0xfffffffffe'" (* 1099511627774 (0xfffffffffe) *)
+  := (Const 1099511627774%Z).
+Notation "'0xfffffffffe'" (* 1099511627774 (0xfffffffffe) *)
+  := (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~1~1~1~0).
 Notation "'0xffffffffff'" (* 1099511627775 (0xffffffffff) *)
   := (Const 1099511627775%Z).
 Notation "'0xffffffffff'" (* 1099511627775 (0xffffffffff) *)
@@ -1975,10 +2067,18 @@ 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 "'0x1ffffffffe2'" (* 2199023255522 (0x1ffffffffe2) *)
+  := (Const 2199023255522%Z).
+Notation "'0x1ffffffffe2'" (* 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 "'0x1fffffffff7'" (* 2199023255543 (0x1fffffffff7) *)
   := (Const 2199023255543%Z).
 Notation "'0x1fffffffff7'" (* 2199023255543 (0x1fffffffff7) *)
   := (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~1~0~1~1~1).
+Notation "'0x1fffffffffe'" (* 2199023255550 (0x1fffffffffe) *)
+  := (Const 2199023255550%Z).
+Notation "'0x1fffffffffe'" (* 2199023255550 (0x1fffffffffe) *)
+  := (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~1~1~1~1~0).
 Notation "'0x1ffffffffff'" (* 2199023255551 (0x1ffffffffff) *)
   := (Const 2199023255551%Z).
 Notation "'0x1ffffffffff'" (* 2199023255551 (0x1ffffffffff) *)
@@ -2035,6 +2135,10 @@ 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 "'0x7fffffffffe'" (* 8796093022206 (0x7fffffffffe) *)
+  := (Const 8796093022206%Z).
+Notation "'0x7fffffffffe'" (* 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 "'0x7ffffffffff'" (* 8796093022207 (0x7ffffffffff) *)
   := (Const 8796093022207%Z).
 Notation "'0x7ffffffffff'" (* 8796093022207 (0x7ffffffffff) *)
@@ -2047,6 +2151,10 @@ 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 "'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 "'0xfffffffffef'" (* 17592186044399 (0xfffffffffef) *)
   := (Const 17592186044399%Z).
 Notation "'0xfffffffffef'" (* 17592186044399 (0xfffffffffef) *)
@@ -2059,6 +2167,10 @@ Notation "'0xffffffffffd'" (* 17592186044413 (0xffffffffffd) *)
   := (Const 17592186044413%Z).
 Notation "'0xffffffffffd'" (* 17592186044413 (0xffffffffffd) *)
   := (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~1~0~1).
+Notation "'0xffffffffffe'" (* 17592186044414 (0xffffffffffe) *)
+  := (Const 17592186044414%Z).
+Notation "'0xffffffffffe'" (* 17592186044414 (0xffffffffffe) *)
+  := (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~1~1~0).
 Notation "'0xfffffffffff'" (* 17592186044415 (0xfffffffffff) *)
   := (Const 17592186044415%Z).
 Notation "'0xfffffffffff'" (* 17592186044415 (0xfffffffffff) *)
@@ -2071,6 +2183,10 @@ 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 "'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 "'0x1ffffffffffd'" (* 35184372088829 (0x1ffffffffffd) *)
   := (Const 35184372088829%Z).
 Notation "'0x1ffffffffffd'" (* 35184372088829 (0x1ffffffffffd) *)
@@ -2167,6 +2283,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 "'0xffffffffffee'" (* 281474976710638 (0xffffffffffee) *)
+  := (Const 281474976710638%Z).
+Notation "'0xffffffffffee'" (* 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 "'0xffffffffffef'" (* 281474976710639 (0xffffffffffef) *)
   := (Const 281474976710639%Z).
 Notation "'0xffffffffffef'" (* 281474976710639 (0xffffffffffef) *)
@@ -2183,6 +2303,10 @@ Notation "'0xfffffffffffd'" (* 281474976710653 (0xfffffffffffd) *)
   := (Const 281474976710653%Z).
 Notation "'0xfffffffffffd'" (* 281474976710653 (0xfffffffffffd) *)
   := (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~1~1~1~0~1).
+Notation "'0xfffffffffffe'" (* 281474976710654 (0xfffffffffffe) *)
+  := (Const 281474976710654%Z).
+Notation "'0xfffffffffffe'" (* 281474976710654 (0xfffffffffffe) *)
+  := (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~1~1~1~1~0).
 Notation "'0xffffffffffff'" (* 281474976710655 (0xffffffffffff) *)
   := (Const 281474976710655%Z).
 Notation "'0xffffffffffff'" (* 281474976710655 (0xffffffffffff) *)
@@ -2195,10 +2319,22 @@ Notation "'0x1000000000001'" (* 281474976710657 (0x1000000000001) *)
   := (Const 281474976710657%Z).
 Notation "'0x1000000000001'" (* 281474976710657 (0x1000000000001) *)
   := (Const WO~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~0~0~1).
+Notation "'0x1fffffffdfffe'" (* 562949953290238 (0x1fffffffdfffe) *)
+  := (Const 562949953290238%Z).
+Notation "'0x1fffffffdfffe'" (* 562949953290238 (0x1fffffffdfffe) *)
+  := (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~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0).
+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 "'0x1ffffffffffdf'" (* 562949953421279 (0x1ffffffffffdf) *)
   := (Const 562949953421279%Z).
 Notation "'0x1ffffffffffdf'" (* 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 "'0x1ffffffffffea'" (* 562949953421290 (0x1ffffffffffea) *)
+  := (Const 562949953421290%Z).
+Notation "'0x1ffffffffffea'" (* 562949953421290 (0x1ffffffffffea) *)
+  := (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~0~1~0).
 Notation "'0x1ffffffffffed'" (* 562949953421293 (0x1ffffffffffed) *)
   := (Const 562949953421293%Z).
 Notation "'0x1ffffffffffed'" (* 562949953421293 (0x1ffffffffffed) *)
@@ -2207,6 +2343,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 "'0x1fffffffffffe'" (* 562949953421310 (0x1fffffffffffe) *)
+  := (Const 562949953421310%Z).
+Notation "'0x1fffffffffffe'" (* 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 "'0x1ffffffffffff'" (* 562949953421311 (0x1ffffffffffff) *)
   := (Const 562949953421311%Z).
 Notation "'0x1ffffffffffff'" (* 562949953421311 (0x1ffffffffffff) *)
@@ -2223,10 +2363,18 @@ Notation "'0x3fffffdffffff'" (* 1125899873288191 (0x3fffffdffffff) *)
   := (Const 1125899873288191%Z).
 Notation "'0x3fffffdffffff'" (* 1125899873288191 (0x3fffffdffffff) *)
   := (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~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 "'0x3ffffffffffbe'" (* 1125899906842558 (0x3ffffffffffbe) *)
+  := (Const 1125899906842558%Z).
+Notation "'0x3ffffffffffbe'" (* 1125899906842558 (0x3ffffffffffbe) *)
+  := (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~0~1~1~1~1~1~0).
 Notation "'0x3ffffffffffe1'" (* 1125899906842593 (0x3ffffffffffe1) *)
   := (Const 1125899906842593%Z).
 Notation "'0x3ffffffffffe1'" (* 1125899906842593 (0x3ffffffffffe1) *)
   := (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 "'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 "'0x3ffffffffffef'" (* 1125899906842607 (0x3ffffffffffef) *)
   := (Const 1125899906842607%Z).
 Notation "'0x3ffffffffffef'" (* 1125899906842607 (0x3ffffffffffef) *)
@@ -2239,6 +2387,10 @@ Notation "'0x3fffffffffffd'" (* 1125899906842621 (0x3fffffffffffd) *)
   := (Const 1125899906842621%Z).
 Notation "'0x3fffffffffffd'" (* 1125899906842621 (0x3fffffffffffd) *)
   := (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~1~1~1~0~1).
+Notation "'0x3fffffffffffe'" (* 1125899906842622 (0x3fffffffffffe) *)
+  := (Const 1125899906842622%Z).
+Notation "'0x3fffffffffffe'" (* 1125899906842622 (0x3fffffffffffe) *)
+  := (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~1~1~1~1~0).
 Notation "'0x3ffffffffffff'" (* 1125899906842623 (0x3ffffffffffff) *)
   := (Const 1125899906842623%Z).
 Notation "'0x3ffffffffffff'" (* 1125899906842623 (0x3ffffffffffff) *)
@@ -2279,6 +2431,10 @@ Notation "'0x7ffffffffffda'" (* 2251799813685210 (0x7ffffffffffda) *)
   := (Const 2251799813685210%Z).
 Notation "'0x7ffffffffffda'" (* 2251799813685210 (0x7ffffffffffda) *)
   := (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~0~1~1~0~1~0).
+Notation "'0x7ffffffffffde'" (* 2251799813685214 (0x7ffffffffffde) *)
+  := (Const 2251799813685214%Z).
+Notation "'0x7ffffffffffde'" (* 2251799813685214 (0x7ffffffffffde) *)
+  := (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~0~1~1~1~1~0).
 Notation "'0x7ffffffffffe1'" (* 2251799813685217 (0x7ffffffffffe1) *)
   := (Const 2251799813685217%Z).
 Notation "'0x7ffffffffffe1'" (* 2251799813685217 (0x7ffffffffffe1) *)
@@ -2287,10 +2443,22 @@ 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 "'0x7fffffffffff6'" (* 2251799813685238 (0x7fffffffffff6) *)
+  := (Const 2251799813685238%Z).
+Notation "'0x7fffffffffff6'" (* 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 "'0x7fffffffffff7'" (* 2251799813685239 (0x7fffffffffff7) *)
   := (Const 2251799813685239%Z).
 Notation "'0x7fffffffffff7'" (* 2251799813685239 (0x7fffffffffff7) *)
   := (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~1).
+Notation "'0x7fffffffffffa'" (* 2251799813685242 (0x7fffffffffffa) *)
+  := (Const 2251799813685242%Z).
+Notation "'0x7fffffffffffa'" (* 2251799813685242 (0x7fffffffffffa) *)
+  := (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~1~0~1~0).
+Notation "'0x7fffffffffffe'" (* 2251799813685246 (0x7fffffffffffe) *)
+  := (Const 2251799813685246%Z).
+Notation "'0x7fffffffffffe'" (* 2251799813685246 (0x7fffffffffffe) *)
+  := (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~1~1~1~0).
 Notation "'0x7ffffffffffff'" (* 2251799813685247 (0x7ffffffffffff) *)
   := (Const 2251799813685247%Z).
 Notation "'0x7ffffffffffff'" (* 2251799813685247 (0x7ffffffffffff) *)
@@ -2303,6 +2471,10 @@ Notation "'0x8000000000001'" (* 2251799813685249 (0x8000000000001) *)
   := (Const 2251799813685249%Z).
 Notation "'0x8000000000001'" (* 2251799813685249 (0x8000000000001) *)
   := (Const WO~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~0~0~0~0~0~1).
+Notation "'0xa5ffffffffffe'" (* 2920302883373054 (0xa5ffffffffffe) *)
+  := (Const 2920302883373054%Z).
+Notation "'0xa5ffffffffffe'" (* 2920302883373054 (0xa5ffffffffffe) *)
+  := (Const WO~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~1~1~1~1~1~1~1~1~1~1~0).
 Notation "'0xffffefffffc2f'" (* 4503595332402223 (0xffffefffffc2f) *)
   := (Const 4503595332402223%Z).
 Notation "'0xffffefffffc2f'" (* 4503595332402223 (0xffffefffffc2f) *)
@@ -2359,6 +2531,14 @@ 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 "'0x1ffffffffffff6'" (* 9007199254740982 (0x1ffffffffffff6) *)
+  := (Const 9007199254740982%Z).
+Notation "'0x1ffffffffffff6'" (* 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 "'0x1ffffffffffffe'" (* 9007199254740990 (0x1ffffffffffffe) *)
+  := (Const 9007199254740990%Z).
+Notation "'0x1ffffffffffffe'" (* 9007199254740990 (0x1ffffffffffffe) *)
+  := (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~1~1~1~0).
 Notation "'0x1fffffffffffff'" (* 9007199254740991 (0x1fffffffffffff) *)
   := (Const 9007199254740991%Z).
 Notation "'0x1fffffffffffff'" (* 9007199254740991 (0x1fffffffffffff) *)
@@ -2371,6 +2551,10 @@ Notation "'0x20000000000001'" (* 9007199254740993 (0x20000000000001) *)
   := (Const 9007199254740993%Z).
 Notation "'0x20000000000001'" (* 9007199254740993 (0x20000000000001) *)
   := (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 "'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 "'0x3ffffffffffff7'" (* 18014398509481975 (0x3ffffffffffff7) *)
   := (Const 18014398509481975%Z).
 Notation "'0x3ffffffffffff7'" (* 18014398509481975 (0x3ffffffffffff7) *)
@@ -2411,6 +2595,18 @@ Notation "'0x7fffffffffffed'" (* 36028797018963949 (0x7fffffffffffed) *)
   := (Const 36028797018963949%Z).
 Notation "'0x7fffffffffffed'" (* 36028797018963949 (0x7fffffffffffed) *)
   := (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~1~1~1~1~1~1~1~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 "'0x7ffffffffffffa'" (* 36028797018963962 (0x7ffffffffffffa) *)
+  := (Const 36028797018963962%Z).
+Notation "'0x7ffffffffffffa'" (* 36028797018963962 (0x7ffffffffffffa) *)
+  := (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~1~1~1~1~1~1~1~1~1~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 "'0x7ffffffffffffc'" (* 36028797018963964 (0x7ffffffffffffc) *)
+  := (Const 36028797018963964%Z).
+Notation "'0x7ffffffffffffc'" (* 36028797018963964 (0x7ffffffffffffc) *)
+  := (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~1~1~1~1~1~1~1~1~1~1~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).
+Notation "'0x7ffffffffffffe'" (* 36028797018963966 (0x7ffffffffffffe) *)
+  := (Const 36028797018963966%Z).
+Notation "'0x7ffffffffffffe'" (* 36028797018963966 (0x7ffffffffffffe) *)
+  := (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~1~1~1~1~1~1~1~1~1~1~1~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 "'0x7fffffffffffff'" (* 36028797018963967 (0x7fffffffffffff) *)
   := (Const 36028797018963967%Z).
 Notation "'0x7fffffffffffff'" (* 36028797018963967 (0x7fffffffffffff) *)
@@ -2431,6 +2627,10 @@ Notation "'0xffffffffffff8b'" (* 72057594037927819 (0xffffffffffff8b) *)
   := (Const 72057594037927819%Z).
 Notation "'0xffffffffffff8b'" (* 72057594037927819 (0xffffffffffff8b) *)
   := (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~1~1~1~1~1~1~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 "'0xffffffffffffce'" (* 72057594037927886 (0xffffffffffffce) *)
+  := (Const 72057594037927886%Z).
+Notation "'0xffffffffffffce'" (* 72057594037927886 (0xffffffffffffce) *)
+  := (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~1~1~1~1~1~1~1~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 "'0xffffffffffffef'" (* 72057594037927919 (0xffffffffffffef) *)
   := (Const 72057594037927919%Z).
 Notation "'0xffffffffffffef'" (* 72057594037927919 (0xffffffffffffef) *)
@@ -2459,6 +2659,10 @@ Notation "'0x100000000000001'" (* 72057594037927937 (0x100000000000001) *)
   := (Const 72057594037927937%Z).
 Notation "'0x100000000000001'" (* 72057594037927937 (0x100000000000001) *)
   := (Const WO~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~0~0~0~1).
+Notation "'0x1ffffffffffff16'" (* 144115188075855638 (0x1ffffffffffff16) *)
+  := (Const 144115188075855638%Z).
+Notation "'0x1ffffffffffff16'" (* 144115188075855638 (0x1ffffffffffff16) *)
+  := (Const WO~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~1~1~0).
 Notation "'0x1ffffffffffffed'" (* 144115188075855853 (0x1ffffffffffffed) *)
   := (Const 144115188075855853%Z).
 Notation "'0x1ffffffffffffed'" (* 144115188075855853 (0x1ffffffffffffed) *)
@@ -2467,10 +2671,18 @@ Notation "'0x1fffffffffffff1'" (* 144115188075855857 (0x1fffffffffffff1) *)
   := (Const 144115188075855857%Z).
 Notation "'0x1fffffffffffff1'" (* 144115188075855857 (0x1fffffffffffff1) *)
   := (Const WO~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~1~1~1~0~0~0~1).
+Notation "'0x1fffffffffffff6'" (* 144115188075855862 (0x1fffffffffffff6) *)
+  := (Const 144115188075855862%Z).
+Notation "'0x1fffffffffffff6'" (* 144115188075855862 (0x1fffffffffffff6) *)
+  := (Const WO~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~1~1~1~0~1~1~0).
 Notation "'0x1fffffffffffff7'" (* 144115188075855863 (0x1fffffffffffff7) *)
   := (Const 144115188075855863%Z).
 Notation "'0x1fffffffffffff7'" (* 144115188075855863 (0x1fffffffffffff7) *)
   := (Const WO~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~1~1~1~0~1~1~1).
+Notation "'0x1fffffffffffffa'" (* 144115188075855866 (0x1fffffffffffffa) *)
+  := (Const 144115188075855866%Z).
+Notation "'0x1fffffffffffffa'" (* 144115188075855866 (0x1fffffffffffffa) *)
+  := (Const WO~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~1~1~1~1~0~1~0).
 Notation "'0x1fffffffffffffb'" (* 144115188075855867 (0x1fffffffffffffb) *)
   := (Const 144115188075855867%Z).
 Notation "'0x1fffffffffffffb'" (* 144115188075855867 (0x1fffffffffffffb) *)
@@ -2495,6 +2707,10 @@ Notation "'0x200000000000001'" (* 144115188075855873 (0x200000000000001) *)
   := (Const 144115188075855873%Z).
 Notation "'0x200000000000001'" (* 144115188075855873 (0x200000000000001) *)
   := (Const WO~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~0~0~0~0~1).
+Notation "'0x3ffffffffffffda'" (* 288230376151711706 (0x3ffffffffffffda) *)
+  := (Const 288230376151711706%Z).
+Notation "'0x3ffffffffffffda'" (* 288230376151711706 (0x3ffffffffffffda) *)
+  := (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~1~1~1~1~1~1~1~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 "'0x3ffffffffffffe5'" (* 288230376151711717 (0x3ffffffffffffe5) *)
   := (Const 288230376151711717%Z).
 Notation "'0x3ffffffffffffe5'" (* 288230376151711717 (0x3ffffffffffffe5) *)
@@ -2503,10 +2719,18 @@ Notation "'0x3ffffffffffffef'" (* 288230376151711727 (0x3ffffffffffffef) *)
   := (Const 288230376151711727%Z).
 Notation "'0x3ffffffffffffef'" (* 288230376151711727 (0x3ffffffffffffef) *)
   := (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~1~1~1~1~1~1~1~1~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 "'0x3fffffffffffff6'" (* 288230376151711734 (0x3fffffffffffff6) *)
+  := (Const 288230376151711734%Z).
+Notation "'0x3fffffffffffff6'" (* 288230376151711734 (0x3fffffffffffff6) *)
+  := (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~1~1~1~1~1~1~1~1~1~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 "'0x3fffffffffffffd'" (* 288230376151711741 (0x3fffffffffffffd) *)
   := (Const 288230376151711741%Z).
 Notation "'0x3fffffffffffffd'" (* 288230376151711741 (0x3fffffffffffffd) *)
   := (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~1~1~1~1~1~1~1~1~1~1~1~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 "'0x3fffffffffffffe'" (* 288230376151711742 (0x3fffffffffffffe) *)
+  := (Const 288230376151711742%Z).
+Notation "'0x3fffffffffffffe'" (* 288230376151711742 (0x3fffffffffffffe) *)
+  := (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~1~1~1~1~1~1~1~1~1~1~1~1~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 "'0x3ffffffffffffff'" (* 288230376151711743 (0x3ffffffffffffff) *)
   := (Const 288230376151711743%Z).
 Notation "'0x3ffffffffffffff'" (* 288230376151711743 (0x3ffffffffffffff) *)
@@ -2519,6 +2743,14 @@ Notation "'0x400000000000001'" (* 288230376151711745 (0x400000000000001) *)
   := (Const 288230376151711745%Z).
 Notation "'0x400000000000001'" (* 288230376151711745 (0x400000000000001) *)
   := (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~0~0~0~0~0~0~0~0~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 "'0x7ffffffffffffca'" (* 576460752303423434 (0x7ffffffffffffca) *)
+  := (Const 576460752303423434%Z).
+Notation "'0x7ffffffffffffca'" (* 576460752303423434 (0x7ffffffffffffca) *)
+  := (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~0~0~1~0~1~0).
+Notation "'0x7ffffffffffffde'" (* 576460752303423454 (0x7ffffffffffffde) *)
+  := (Const 576460752303423454%Z).
+Notation "'0x7ffffffffffffde'" (* 576460752303423454 (0x7ffffffffffffde) *)
+  := (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~0~1~1~1~1~0).
 Notation "'0x7ffffffffffffeb'" (* 576460752303423467 (0x7ffffffffffffeb) *)
   := (Const 576460752303423467%Z).
 Notation "'0x7ffffffffffffeb'" (* 576460752303423467 (0x7ffffffffffffeb) *)
@@ -2531,6 +2763,14 @@ 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 "'0x7fffffffffffffa'" (* 576460752303423482 (0x7fffffffffffffa) *)
+  := (Const 576460752303423482%Z).
+Notation "'0x7fffffffffffffa'" (* 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 "'0x7fffffffffffffe'" (* 576460752303423486 (0x7fffffffffffffe) *)
+  := (Const 576460752303423486%Z).
+Notation "'0x7fffffffffffffe'" (* 576460752303423486 (0x7fffffffffffffe) *)
+  := (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~1~1~0).
 Notation "'0x7ffffffffffffff'" (* 576460752303423487 (0x7ffffffffffffff) *)
   := (Const 576460752303423487%Z).
 Notation "'0x7ffffffffffffff'" (* 576460752303423487 (0x7ffffffffffffff) *)