diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
index 94b8e1a206..72b28ed8bd 100644
--- a/kevm-pyk/pyproject.toml
+++ b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.413"
+version = "1.0.414"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py
index 4be637f809..723ba5a060 100644
--- a/kevm-pyk/src/kevm_pyk/__init__.py
+++ b/kevm-pyk/src/kevm_pyk/__init__.py
@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.413'
+VERSION: Final = '1.0.414'
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k
index c857bb8da8..6484391392 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k
@@ -34,11 +34,12 @@ module BITWISE-SIMPLIFICATION [symbolic]
     rule maxUInt48  &Int X <Int pow48  => true requires 0 <=Int X [simplification, smt-lemma]
     rule maxUInt160 &Int X <Int pow160 => true requires 0 <=Int X [simplification, smt-lemma]
 
-    rule [bitwise-and-identity]:
+    // Generalization of: maxUIntXXX &Int Y => Y requires #rangeUInt(XXX, Y)
+    rule [bitwise-and-maxUInt-identity]:
       X &Int Y => Y
       requires 0 <=Int X
        andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
-       andBool 0 <=Int Y andBool Y <Int 2 ^Int log2Int(X +Int 1)
+       andBool 0 <=Int Y andBool Y <Int X +Int 1
        [concrete(X), simplification, comm]
 
     rule [bitwise-or-geq-zero]:  0 <=Int (X |Int Y) => true requires 0 <=Int X andBool 0 <=Int Y [simplification]
@@ -47,36 +48,28 @@ module BITWISE-SIMPLIFICATION [symbolic]
     rule [bitwise-and-lt]:       (X &Int Y) <Int Z      => true requires 0 <=Int X andBool 0 <=Int Y andBool (X <Int Z orBool Y <Int Z)          [simplification]
     rule [bitwise-or-lt-pow256]: (X |Int Y) <Int pow256 => true requires 0 <=Int X andBool 0 <=Int Y andBool X <Int pow256 andBool Y <Int pow256 [simplification]
 
-   // We should probably generalize the simplifications below for relevant powers of two.
-    rule notMaxUInt5   &Int X => 0 requires #rangeUInt(  5, X) [simplification]
-    rule notMaxUInt8   &Int X => 0 requires #rangeUInt(  8, X) [simplification]
-    rule notMaxUInt16  &Int X => 0 requires #rangeUInt( 16, X) [simplification]
-    rule notMaxUInt32  &Int X => 0 requires #rangeUInt( 32, X) [simplification]
-    rule notMaxUInt64  &Int X => 0 requires #rangeUInt( 64, X) [simplification]
-    rule notMaxUInt96  &Int X => 0 requires #rangeUInt( 96, X) [simplification]
-    rule notMaxUInt128 &Int X => 0 requires #rangeUInt(128, X) [simplification]
-    rule notMaxUInt160 &Int X => 0 requires #rangeUInt(160, X) [simplification]
-    rule notMaxUInt192 &Int X => 0 requires #rangeUInt(192, X) [simplification]
-    rule notMaxUInt208 &Int X => 0 requires #rangeUInt(208, X) [simplification]
-    rule notMaxUInt224 &Int X => 0 requires #rangeUInt(224, X) [simplification]
-    rule notMaxUInt240 &Int X => 0 requires #rangeUInt(240, X) [simplification]
-    rule notMaxUInt248 &Int X => 0 requires #rangeUInt(248, X) [simplification]
-
-    rule notMaxUInt240 &Int (X <<Int 240) => X <<Int 240 requires #rangeUInt(16, X) [simplification]
-    rule notMaxUInt248 &Int (X <<Int 248) => X <<Int 248 requires #rangeUInt( 8, X) [simplification]
-
-    rule maxUInt8   &Int (X |Int (notMaxUInt8   &Int _)) => maxUInt8   &Int X [simplification]
-    rule maxUInt16  &Int (X |Int (notMaxUInt16  &Int _)) => maxUInt16  &Int X [simplification]
-    rule maxUInt32  &Int (X |Int (notMaxUInt32  &Int _)) => maxUInt32  &Int X [simplification]
-    rule maxUInt64  &Int (X |Int (notMaxUInt64  &Int _)) => maxUInt64  &Int X [simplification]
-    rule maxUInt96  &Int (X |Int (notMaxUInt96  &Int _)) => maxUInt96  &Int X [simplification]
-    rule maxUInt128 &Int (X |Int (notMaxUInt128 &Int _)) => maxUInt128 &Int X [simplification]
-    rule maxUInt160 &Int (X |Int (notMaxUInt160 &Int _)) => maxUInt160 &Int X [simplification]
-    rule maxUInt192 &Int (X |Int (notMaxUInt192 &Int _)) => maxUInt192 &Int X [simplification]
-    rule maxUInt208 &Int (X |Int (notMaxUInt208 &Int _)) => maxUInt208 &Int X [simplification]
-    rule maxUInt224 &Int (X |Int (notMaxUInt224 &Int _)) => maxUInt224 &Int X [simplification]
-    rule maxUInt240 &Int (X |Int (notMaxUInt240 &Int _)) => maxUInt240 &Int X [simplification]
-    rule maxUInt248 &Int (X |Int (notMaxUInt248 &Int _)) => maxUInt248 &Int X [simplification]
+    // Generalization of: notMaxUIntXXX &Int Y => 0 requires #rangeUInt(XXX, Y)
+    rule [bitwise-and-notMaxUInt-zero]:
+      X &Int Y => 0
+      requires #rangeUInt(256, X)
+       andBool 2 ^Int ( log2Int ( pow256 -Int X ) ) ==Int pow256 -Int X
+       andBool 0 <=Int Y andBool Y <Int pow256 -Int X
+      [simplification, concrete(X)]
+
+    // Generalization of: notMaxUIntXXX &Int (Y <<Int XXX) => Y <<Int XXX requires #rangeUInt(256 -Int XXX, Y)
+    rule X &Int (Y <<Int Z) => Y <<Int Z
+      requires #rangeUInt(256, X)
+       andBool 2 ^Int ( log2Int ( pow256 -Int X ) ) ==Int pow256 -Int X
+       andBool Z ==Int log2Int ( pow256 -Int X )
+       andBool 0 <=Int Y andBool Y <Int 2 ^Int ( 256 -Int Z )
+      [simplification, concrete(X, Z), comm]
+
+    // Generalization of: maxUIntXXX &Int (Y |Int (notMaxUIntXXX &Int T)) => maxUIntXXX &Int Y
+    rule X &Int (Y |Int (Z &Int T)) => X &Int Y
+      requires 0 <=Int X andBool 0 <=Int Y andBool 0 <=Int Z andBool 0 <=Int T
+       andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
+       andBool X +Int Z ==Int maxUInt256
+      [simplification, concrete(X, Z), comm]
 
     rule [lengthBytes-upInt-32-lower-bound]:
       lengthBytes(X) <=Int notMaxUInt5 &Int ( lengthBytes(X) +Int 31 ) => true
diff --git a/package/version b/package/version
index a72006d007..7ce89ff651 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-1.0.413
+1.0.414
diff --git a/tests/specs/functional/lemmas-spec.k b/tests/specs/functional/lemmas-spec.k
index 9fd2b506de..dee3b618a4 100644
--- a/tests/specs/functional/lemmas-spec.k
+++ b/tests/specs/functional/lemmas-spec.k
@@ -465,35 +465,47 @@ module LEMMAS-SPEC
  // bitwise
  // -------
 
-    claim <k> runLemma ( notMaxUInt5   &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt (   5 , X )
-    claim <k> runLemma ( notMaxUInt8   &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt (   8 , X )
-    claim <k> runLemma ( notMaxUInt16  &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt (  16 , X )
-    claim <k> runLemma ( notMaxUInt32  &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt (  32 , X )
-    claim <k> runLemma ( notMaxUInt64  &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt (  64 , X )
-    claim <k> runLemma ( notMaxUInt96  &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt (  96 , X )
-    claim <k> runLemma ( notMaxUInt128 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 128 , X )
-    claim <k> runLemma ( notMaxUInt160 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 160 , X )
-    claim <k> runLemma ( notMaxUInt192 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 192 , X )
-    claim <k> runLemma ( notMaxUInt208 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 208 , X )
-    claim <k> runLemma ( notMaxUInt224 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 224 , X )
-    claim <k> runLemma ( notMaxUInt240 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 240 , X )
-    claim <k> runLemma ( notMaxUInt248 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 248 , X )
-
-    claim <k> runLemma ( notMaxUInt240 &Int ( X <<Int 240 ) ) => doneLemma( X <<Int 240 ) ... </k> requires #rangeUInt ( 16 , X )
-    claim <k> runLemma ( notMaxUInt248 &Int ( X <<Int 248 ) ) => doneLemma( X <<Int 248 ) ... </k> requires #rangeUInt (  8 , X )
-
-    claim <k> runLemma ( maxUInt8   &Int ( X |Int ( notMaxUInt8   &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (   8 , X )
-    claim <k> runLemma ( maxUInt16  &Int ( X |Int ( notMaxUInt16  &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (  16 , X )
-    claim <k> runLemma ( maxUInt32  &Int ( X |Int ( notMaxUInt32  &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (  32 , X )
-    claim <k> runLemma ( maxUInt64  &Int ( X |Int ( notMaxUInt64  &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (  64 , X )
-    claim <k> runLemma ( maxUInt96  &Int ( X |Int ( notMaxUInt96  &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (  96 , X )
-    claim <k> runLemma ( maxUInt128 &Int ( X |Int ( notMaxUInt128 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 128 , X )
-    claim <k> runLemma ( maxUInt160 &Int ( X |Int ( notMaxUInt160 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 160 , X )
-    claim <k> runLemma ( maxUInt192 &Int ( X |Int ( notMaxUInt192 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 192 , X )
-    claim <k> runLemma ( maxUInt208 &Int ( X |Int ( notMaxUInt208 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 208 , X )
-    claim <k> runLemma ( maxUInt224 &Int ( X |Int ( notMaxUInt224 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 224 , X )
-    claim <k> runLemma ( maxUInt240 &Int ( X |Int ( notMaxUInt240 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 240 , X )
-    claim <k> runLemma ( maxUInt248 &Int ( X |Int ( notMaxUInt248 &Int _ ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 248 , X )
+    claim [bit-n005-0]: <k> runLemma ( notMaxUInt5   &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt (   5 , X )
+    claim [bit-n008-0]: <k> runLemma ( notMaxUInt8   &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt (   8 , X )
+    claim [bit-n016-0]: <k> runLemma ( notMaxUInt16  &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt (  16 , X )
+    claim [bit-n032-0]: <k> runLemma ( notMaxUInt32  &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt (  32 , X )
+    claim [bit-n064-0]: <k> runLemma ( notMaxUInt64  &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt (  64 , X )
+    claim [bit-n096-0]: <k> runLemma ( notMaxUInt96  &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt (  96 , X )
+    claim [bit-n128-0]: <k> runLemma ( notMaxUInt128 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 128 , X )
+    claim [bit-n160-0]: <k> runLemma ( notMaxUInt160 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 160 , X )
+    claim [bit-n192-0]: <k> runLemma ( notMaxUInt192 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 192 , X )
+    claim [bit-n208-0]: <k> runLemma ( notMaxUInt208 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 208 , X )
+    claim [bit-n224-0]: <k> runLemma ( notMaxUInt224 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 224 , X )
+    claim [bit-n240-0]: <k> runLemma ( notMaxUInt240 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 240 , X )
+    claim [bit-n248-0]: <k> runLemma ( notMaxUInt248 &Int X ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 248 , X )
+
+    claim [bit-n005-shl]: <k> runLemma ( notMaxUInt5   &Int ( X <<Int   5 ) ) => doneLemma( X <<Int   5 ) ... </k> requires 0 <=Int X andBool X <Int 2 ^Int 249
+    claim [bit-n008-shl]: <k> runLemma ( notMaxUInt8   &Int ( X <<Int   8 ) ) => doneLemma( X <<Int   8 ) ... </k> requires #rangeUInt ( 248 , X )
+    claim [bit-n016-shl]: <k> runLemma ( notMaxUInt16  &Int ( X <<Int  16 ) ) => doneLemma( X <<Int  16 ) ... </k> requires #rangeUInt ( 240 , X )
+    claim [bit-n032-shl]: <k> runLemma ( notMaxUInt32  &Int ( X <<Int  32 ) ) => doneLemma( X <<Int  32 ) ... </k> requires #rangeUInt ( 224 , X )
+    claim [bit-n064-shl]: <k> runLemma ( notMaxUInt64  &Int ( X <<Int  64 ) ) => doneLemma( X <<Int  64 ) ... </k> requires #rangeUInt ( 192 , X )
+    claim [bit-n096-shl]: <k> runLemma ( notMaxUInt96  &Int ( X <<Int  96 ) ) => doneLemma( X <<Int  96 ) ... </k> requires #rangeUInt ( 160 , X )
+    claim [bit-n128-shl]: <k> runLemma ( notMaxUInt128 &Int ( X <<Int 128 ) ) => doneLemma( X <<Int 128 ) ... </k> requires #rangeUInt ( 128 , X )
+    claim [bit-n160-shl]: <k> runLemma ( notMaxUInt160 &Int ( X <<Int 160 ) ) => doneLemma( X <<Int 160 ) ... </k> requires #rangeUInt (  96 , X )
+    claim [bit-n192-shl]: <k> runLemma ( notMaxUInt192 &Int ( X <<Int 192 ) ) => doneLemma( X <<Int 192 ) ... </k> requires #rangeUInt (  64 , X )
+    claim [bit-n208-shl]: <k> runLemma ( notMaxUInt208 &Int ( X <<Int 208 ) ) => doneLemma( X <<Int 208 ) ... </k> requires #rangeUInt (  48 , X )
+    claim [bit-n224-shl]: <k> runLemma ( notMaxUInt224 &Int ( X <<Int 224 ) ) => doneLemma( X <<Int 224 ) ... </k> requires #rangeUInt (  32 , X )
+    claim [bit-n240-shl]: <k> runLemma ( notMaxUInt240 &Int ( X <<Int 240 ) ) => doneLemma( X <<Int 240 ) ... </k> requires #rangeUInt (  16 , X )
+    claim [bit-n248-shl]: <k> runLemma ( notMaxUInt248 &Int ( X <<Int 248 ) ) => doneLemma( X <<Int 248 ) ... </k> requires #rangeUInt (   8 , X )
+
+    claim [bit-005-m-or-nm]: <k> runLemma ( maxUInt5   &Int ( X |Int ( notMaxUInt5   &Int T ) ) ) => doneLemma( X ) ... </k> requires 0 <=Int X andBool X <Int 2 ^Int 5 andBool 0 <=Int T
+    claim [bit-008-m-or-nm]: <k> runLemma ( maxUInt8   &Int ( X |Int ( notMaxUInt8   &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (   8 , X ) andBool 0 <=Int T
+    claim [bit-016-m-or-nm]: <k> runLemma ( maxUInt16  &Int ( X |Int ( notMaxUInt16  &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (  16 , X ) andBool 0 <=Int T
+    claim [bit-032-m-or-nm]: <k> runLemma ( maxUInt32  &Int ( X |Int ( notMaxUInt32  &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (  32 , X ) andBool 0 <=Int T
+    claim [bit-064-m-or-nm]: <k> runLemma ( maxUInt64  &Int ( X |Int ( notMaxUInt64  &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (  64 , X ) andBool 0 <=Int T
+    claim [bit-096-m-or-nm]: <k> runLemma ( maxUInt96  &Int ( X |Int ( notMaxUInt96  &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt (  96 , X ) andBool 0 <=Int T
+    claim [bit-128-m-or-nm]: <k> runLemma ( maxUInt128 &Int ( X |Int ( notMaxUInt128 &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 128 , X ) andBool 0 <=Int T
+    claim [bit-160-m-or-nm]: <k> runLemma ( maxUInt160 &Int ( X |Int ( notMaxUInt160 &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 160 , X ) andBool 0 <=Int T
+    claim [bit-192-m-or-nm]: <k> runLemma ( maxUInt192 &Int ( X |Int ( notMaxUInt192 &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 192 , X ) andBool 0 <=Int T
+    claim [bit-208-m-or-nm]: <k> runLemma ( maxUInt208 &Int ( X |Int ( notMaxUInt208 &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 208 , X ) andBool 0 <=Int T
+    claim [bit-224-m-or-nm]: <k> runLemma ( maxUInt224 &Int ( X |Int ( notMaxUInt224 &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 224 , X ) andBool 0 <=Int T
+    claim [bit-240-m-or-nm]: <k> runLemma ( maxUInt240 &Int ( X |Int ( notMaxUInt240 &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 240 , X ) andBool 0 <=Int T
+    claim [bit-248-m-or-nm]: <k> runLemma ( maxUInt248 &Int ( X |Int ( notMaxUInt248 &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 248 , X ) andBool 0 <=Int T
 
     claim <k> runLemma ( #buf ( 32 , #asWord ( X ) ) ) => doneLemma( X ) </k> requires lengthBytes(X) ==Int 32
     claim <k> runLemma ( #buf ( 32 , X <<Int 248 ) ) => doneLemma( #buf ( 1 , X ) +Bytes #buf ( 31 , 0 ) ) ... </k> requires #rangeUInt (  8 , X )