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 49d6ec9ee3..0bf1c666b9 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
@@ -13,7 +13,7 @@ module BITWISE-SIMPLIFICATION [symbolic]
     rule A |Int 0 => A [simplification]
     rule A |Int A => A [simplification]
 
-    rule A |Int B => B |Int A [simplification(40), concrete(B), symbolic(A)]
+    rule A |Int B => B |Int A [simplification(30), symbolic(A), concrete(B)]
 
     rule  X |Int _  ==Int 0          => false requires 0 <Int X [simplification, concrete(X)]
     rule (A |Int B) ==Int (B |Int A) => true  [simplification, smt-lemma]
@@ -22,7 +22,7 @@ module BITWISE-SIMPLIFICATION [symbolic]
   // bit-and
   // ###########################################################################
 
-    rule A &Int B => B &Int A [symbolic(A), concrete(B), simplification]
+    rule A &Int B => B &Int A [simplification(30), symbolic(A), concrete(B)]
 
     rule 0 &Int _ => 0 [simplification]
     rule _ &Int 0 => 0 [simplification]
@@ -34,24 +34,26 @@ module BITWISE-SIMPLIFICATION [symbolic]
     rule [bitwise-or-lt-zero]:  (X |Int Y) <Int Z => false requires 0 <=Int X andBool 0 <=Int Y andBool Z <=Int 0 [concrete(Z), simplification]
     rule [bitwise-and-lt-zero]: (X &Int Y) <Int Z => false requires 0 <=Int X andBool 0 <=Int Y andBool Z <=Int 0 [concrete(Z), simplification]
 
-    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]
+    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]:
+      (X |Int Y) <Int Z => true
+      requires 0 <=Int X andBool 0 <=Int Y andBool X <Int Z andBool Y <Int Z
+       andBool Z ==Int 2 ^Int ( log2Int( Z ) ) [simplification, concrete(Z)]
 
     // 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)
+      requires 0 <=Int X andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
        andBool 0 <=Int Y andBool Y <Int X +Int 1
-       [concrete(X), simplification, comm, preserves-definedness]
+       [simplification(40), concrete(X), preserves-definedness]
 
-    // Generalization of: notMaxUIntXXX &Int Y => 0 requires #rangeUInt(XXX, Y)
+    // Generalization of: notMaxUIntXXX &Int Y => 0 requires #rangeUInt(256 -Int XXX, Y)
     rule [bitwise-and-notMaxUInt-zero]:
       X &Int Y => 0
-      requires #rangeUInt(256, X)
-       andBool pow256 -Int X ==Int 2 ^Int ( log2Int ( pow256 -Int X ) )
+      requires #rangeUInt(256, X) andBool pow256 -Int X ==Int 2 ^Int ( log2Int ( pow256 -Int X ) )
        andBool 0 <=Int Y andBool Y <Int pow256 -Int X
-      [simplification, concrete(X), preserves-definedness]
+      [simplification(40), concrete(X), preserves-definedness]
 
     rule [notMaxUInt5-bit-and-nested]:
       notMaxUInt5 &Int ( ( notMaxUInt5 &Int X ) +Int Y ) => chop ( ( notMaxUInt5 &Int X ) +Int ( notMaxUInt5 &Int Y ) )
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k
index 5d2f2f8cfd..910e265d21 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k
@@ -72,30 +72,6 @@ module BYTES-SIMPLIFICATION [symbolic]
        andBool #asWord(B) <Int 2 ^Int (8 *Int W)
       [simplification, concrete(W), preserves-definedness]
 
-    rule [buf-asWord-invert-rl]:
-      #asWord ( #buf ( WB:Int, X:Int ) ) => X
-      requires 0 <=Int WB andBool 0 <=Int X andBool
-               ( ( WB <=Int 32 andBool X <Int 2 ^Int (8 *Int WB) ) orBool
-                 ( WB  >Int 32 andBool X <Int pow256 ) )
-      [simplification, concrete(WB), preserves-definedness]
-
-    rule [buf-asWord-invert-rl-range]:
-      #asWord ( #range ( #buf ( WB:Int, X:Int ), S:Int, WR:Int ) ) => X
-      requires 0 <=Int WB andBool 0 <=Int X andBool 0 <=Int S andBool 0 <=Int WR
-       andBool S +Int WR ==Int WB
-       andBool X <Int 2 ^Int (8 *Int WR)
-      [simplification, concrete(WB, S, WR), preserves-definedness]
-
-    rule [asWord-trim-leading-zeros-concat]:
-      #asWord ( BZ +Bytes B ) => #asWord ( B )
-      requires #asInteger ( BZ ) ==Int 0
-      [simplification, concrete(BZ)]
-
-    rule [asWord-trim-overflowing-zeros]:
-      #asWord ( B ) => #asWord ( #range(B, lengthBytes(B) -Int 32, 32) )
-      requires 32 <Int lengthBytes(B)
-      [simplification]
-
     rule [buf-zero-concat-base]:
       #buf(W1:Int, 0) +Bytes #buf(W2:Int, 0) => #buf(W1 +Int W2, 0)
       requires 0 <=Int W1 andBool 0 <=Int W2
@@ -244,24 +220,6 @@ module BYTES-SIMPLIFICATION [symbolic]
       #range(#padRightToWidth(_, BUF), 0, WIDTH) => BUF
       requires lengthBytes(BUF) ==Int WIDTH [simplification]
 
-    rule [range-eq-check]:
-      BZ +Bytes #range ( B, S, W ) ==K B => true
-      requires 0 <=Int S andBool 0 <=Int W
-      andBool lengthBytes( B ) ==Int S +Int W
-      andBool #asInteger( BZ ) ==Int 0
-      andBool lengthBytes( BZ ) ==Int S
-      andBool #asWord ( B ) <Int 2 ^Int ( 8 *Int W )
-      [simplification, concrete(BZ, S, W), comm, preserves-definedness]
-
-    rule [range-eq-check-ml]:
-      { BZ +Bytes #range ( B, S, W ) #Equals B } => #Top
-      requires 0 <=Int S andBool 0 <=Int W
-      andBool lengthBytes( B ) ==Int S +Int W
-      andBool #asInteger( BZ ) ==Int 0
-      andBool lengthBytes( BZ ) ==Int S
-      andBool #asWord ( B ) <Int 2 ^Int ( 8 *Int W )
-      [simplification, concrete(BZ, S, W), comm, preserves-definedness]
-
     // Memory update
 
     rule [memUpdate-is-empty]:
@@ -301,15 +259,7 @@ module BYTES-SIMPLIFICATION [symbolic]
 
     rule [lengthBytes-leq-zero]: lengthBytes(B:Bytes) <=Int 0 => B ==K .Bytes [simplification]
 
-    // #asWord
-
-    rule #asWord(WS) >>Int M => #asWord(#range(WS, 0, lengthBytes(WS) -Int (M /Int 8) ))
-      requires 0 <=Int M andBool M modInt 8 ==Int 0
-      [simplification, preserves-definedness]
-
-    // This simplification needs to be generalised properly
-    rule notMaxUInt224 &Int #asWord(#padRightToWidth(32, BUF)) => #asWord(#padRightToWidth(32, BUF))
-      requires lengthBytes(BUF) <=Int 4 [simplification]
+    // #padToWidth
 
     rule #padToWidth(32, #asByteStack(V)) => #buf(32, V)  requires #rangeUInt(256, V) [simplification]
 
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k
index a4c168fbb2..6c633d290d 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k
@@ -1,17 +1,10 @@
 requires "evm-types.md"
 
 module EVM-INT-SIMPLIFICATION
-    imports EVM-INT-SIMPLIFICATION-HASKELL
-endmodule
-
-module EVM-INT-SIMPLIFICATION-HASKELL [symbolic]
-    imports EVM-INT-SIMPLIFICATION-COMMON
-endmodule
-
-module EVM-INT-SIMPLIFICATION-COMMON
-    imports INT
     imports BOOL
+    imports BUF
     imports EVM-TYPES
+    imports INT
     imports WORD
 
   // ###########################################################################
@@ -57,31 +50,91 @@ module EVM-INT-SIMPLIFICATION-COMMON
   // #asWord
   // ###########################################################################
 
-  rule [asWord-lb]: 0 <=Int #asWord(_WS)     => true [simplification, smt-lemma]
-  rule [asWord-ub]: #asWord(_WS) <Int pow256 => true [simplification, smt-lemma]
-
-  rule [asWord-lt]:
-    #asWord ( BA ) <Int X => true
-    requires 2 ^Int ( 8 *Int lengthBytes(BA) ) <=Int X
-    [concrete(X), simplification]
-
-  rule [asWord-lt-concat]:
-    #asWord ( BA1 +Bytes BA2 ) <Int X => #asWord ( BA1 ) <Int ( X -Int #asWord ( BA2 ) ) /Int ( 2 ^Int ( 8 *Int lengthBytes ( BA2 ) ) )
-    requires ( X -Int #asWord ( BA2 ) ) modInt ( 2 ^Int ( 8 *Int lengthBytes ( BA2 ) ) ) ==Int 0
-    [concrete(BA2, X), simplification, preserves-definedness]
-
-  rule [asWord-lt-range]:
-    #asWord ( #range ( _:Bytes, S, W ) ) <Int X => true
-    requires 0 <=Int S andBool 0 <=Int W
-     andBool 2 ^Int ( 8 *Int W ) <=Int X
-    [simplification, concrete(S, W, X), preserves-definedness]
-
-  rule [lt-asWord-range]:
-    X <Int #asWord ( #range ( B:Bytes, S, W ) ) => X <Int #asWord ( B )
+  // Unification: two `#asWord`s
+  rule [asWord-eq-asWord]:
+    #asWord ( B1 ) ==Int #asWord ( B2 ) => #buf ( 32 -Int lengthBytes(B1), 0 ) +Bytes B1 ==K #buf ( 32 -Int lengthBytes(B2), 0 ) +Bytes B2
+    requires lengthBytes(B1) <=Int 32 andBool lengthBytes(B2) <=Int 32
+    [simplification, preserves-definedness]
+
+  // Unification: two `#asWord`s
+  rule [asWord-eq-asWord-ml]:
+    { #asWord ( B1 ) #Equals #asWord ( B2 ) } => { true #Equals #asWord ( B1 ) ==Int #asWord ( B2 ) }
+    [simplification, preserves-definedness]
+
+  // Unification: `#asWord` and concrete number
+  rule [asWord-eq-num]:
+    #asWord ( B:Bytes ) ==Int X:Int =>
+      0 <=Int X andBool X <Int 2 ^Int (8 *Int lengthBytes(B))
+                andBool B ==K #buf ( lengthBytes(B), X )
+    requires lengthBytes(B) <=Int 32
+    [simplification, concrete(X), comm, preserves-definedness]
+
+  // Unification: `#asWord` and concrete number
+  rule [asWord-eq-num-ml-l]: { #asWord ( B:Bytes ) #Equals X:Int } => { true #Equals #asWord ( B:Bytes ) ==K X:Int } [simplification, concrete(X), preserves-definedness]
+  rule [asWord-eq-num-ml-r]: { X:Int #Equals #asWord ( B:Bytes ) } => { true #Equals #asWord ( B:Bytes ) ==K X:Int } [simplification, concrete(X), preserves-definedness]
+
+  // Reduction: we can always remove leading zeros
+  rule [asWord-trim-leading-zeros]:
+    #asWord ( BZ +Bytes B ) => #asWord ( B )
+    requires #asInteger ( BZ ) ==Int 0
+    [simplification(40), concrete(BZ), preserves-definedness]
+
+  // Reduction: we can always ignore content beyond 32 bytes
+  rule [asWord-trim-overflowing]:
+    #asWord ( B ) => #asWord ( #range(B, lengthBytes(B) -Int 32, 32) )
+    requires 32 <Int lengthBytes(B)
+    [simplification(40), preserves-definedness]
+
+  // Reduction: `#range` can be ignored under certain conditions
+  rule [asWord-range]:
+    #asWord ( #range ( B:Bytes, S, W ) ) => #asWord ( B )
     requires 0 <=Int S andBool 0 <=Int W
+     andBool lengthBytes(B) <=Int 32
      andBool lengthBytes(B) ==Int S +Int W
      andBool #asWord ( B ) <Int 2 ^Int ( 8 *Int W )
-    [simplification, concrete(X, S, W), preserves-definedness]
+    [simplification, concrete(S, W), preserves-definedness]
+
+  // Reduction: `#asWord` inverts `#buf` under certain conditions
+  rule [asWord-buf-inversion]:
+    #asWord ( #buf ( WB:Int, X:Int ) ) => X
+    requires 0 <=Int WB andBool 0 <=Int X andBool X <Int minInt ( 2 ^Int (8 *Int WB), pow256 )
+    [simplification, concrete(WB), preserves-definedness]
+
+  // Reduction: bitwise right shift in terms of `#range`
+  rule [asWord-shr]:
+    #asWord( BA ) >>Int N => #asWord ( #range ( BA, 0, lengthBytes( BA ) -Int ( N /Int 8 ) ) )
+    requires 0 <=Int N andBool N modInt 8 ==Int 0
+    [simplification, concrete(N), preserves-definedness]
+
+  // Reduction: division in terms of `#range`
+  rule [asWord-div]:
+    #asWord( BA ) /Int N => #asWord ( #range ( BA, 0, lengthBytes( BA ) -Int ( log2Int( N ) /Int 8 ) ) )
+    requires 0 <Int N andBool N ==Int 2 ^Int log2Int ( N ) andBool log2Int( N ) modInt 8 ==Int 0
+     andBool lengthBytes ( BA ) <=Int 32
+    [simplification, preserves-definedness]
+
+  // Comparison: `#asWord` is always in the range `[0, pow256)`
+  rule [asWord-lb]: 0 <=Int #asWord( _ )     => true [simplification, smt-lemma]
+  rule [asWord-ub]: #asWord( _ ) <Int pow256 => true [simplification, smt-lemma]
+
+  // Comparison: `#asWord(B)` is certainly less than something that does not fit into `lengthBytes(B)` bytes
+  rule [asWord-lt]:  #asWord ( B )  <Int X:Int => true  requires   2 ^Int (8 *Int minInt(32, lengthBytes(B)))          <=Int X [simplification, preserves-definedness]
+  // Comparison: `#asWord(B)` is certainly less than or equal to something that is not less than the max number fitting into `lengthBytes(B)` bytes
+  rule [asWord-le]:  #asWord ( B ) <=Int X:Int => true  requires ( 2 ^Int (8 *Int minInt(32, lengthBytes(B))) -Int 1 ) <=Int X [simplification, preserves-definedness]
+
+  // Comparison: `#asWord` of `+Bytes` when lower bytes match, with `<Int`
+  rule [asWord-concat-lt]:
+    #asWord ( BA1 +Bytes BA2 ) <Int X:Int => #asWord ( BA1 ) <Int X /Int ( 2 ^Int ( 8 *Int lengthBytes ( BA2 ) ) )
+    requires #asWord ( BA2 ) ==Int X modInt ( 2 ^Int ( 8 *Int lengthBytes ( BA2 ) ) )
+     andBool lengthBytes ( BA1 +Bytes BA2 ) <=Int 32
+    [simplification, concrete(BA2, X), preserves-definedness]
+
+  // Comparison: `#asWord` of `+Bytes` when lower bytes match, with `<=Int`
+  rule [asWord-concat-le]:
+    #asWord ( BA1 +Bytes BA2 ) <=Int X:Int => #asWord ( BA1 ) <=Int X /Int ( 2 ^Int ( 8 *Int lengthBytes ( BA2 ) ) )
+    requires #asWord ( BA2 ) ==Int X modInt ( 2 ^Int ( 8 *Int lengthBytes ( BA2 ) ) )
+     andBool lengthBytes ( BA1 +Bytes BA2 ) <=Int 32
+    [simplification, concrete(BA2, X), preserves-definedness]
 
   // ###########################################################################
   // chop
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k
index 0969d2574a..661fa1c143 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k
@@ -194,14 +194,6 @@ module LEMMAS-HASKELL [symbolic]
     imports EVM
     imports BUF
 
-  // ########################
-  // Word Reasoning
-  // ########################
-
-    rule #asWord(BUF) /Int D => #asWord(#range(BUF, 0, lengthBytes(BUF) -Int log256Int(D)))
-       requires 0 <Int D andBool D <Int pow256 andBool D ==Int 256 ^Int log256Int(D)
-        andBool log256Int(D) <=Int lengthBytes(BUF) [simplification, preserves-definedness]
-
   // ########################
   // Arithmetic
   // ########################
diff --git a/tests/specs/benchmarks/verification.k b/tests/specs/benchmarks/verification.k
index 373f0a195e..dff254eb89 100644
--- a/tests/specs/benchmarks/verification.k
+++ b/tests/specs/benchmarks/verification.k
@@ -17,8 +17,6 @@ module VERIFICATION-COMMON
 
     rule         #asWord(#ecrec(HASH, SIGV, SIGR, SIGS))             => 0    requires         #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification]
     rule 0  <Int #asWord(#ecrec(HASH, SIGV, SIGR, SIGS))             => true requires notBool #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification]
-    rule 0 <=Int #asWord(#ecrec(_   , _   , _   , _   ))             => true                                                      [simplification]
-    rule         #asWord(#ecrec(_   , _   , _   , _   )) <Int pow160 => true                                                      [simplification]
 
     rule #Ceil( #ecrec(HASH, SIGV, SIGR, SIGS) ) => #Top
      requires #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification]
diff --git a/tests/specs/examples/storage-spec.md b/tests/specs/examples/storage-spec.md
index d27e067870..7950c5135e 100644
--- a/tests/specs/examples/storage-spec.md
+++ b/tests/specs/examples/storage-spec.md
@@ -26,7 +26,7 @@ requires "storage-bin-runtime.k"
 
 module VERIFICATION
     imports EDSL
-    imports LEMMAS
+    imports LEMMAS-WITHOUT-SLOT-UPDATES
     imports EVM-OPTIMIZATIONS
     imports STORAGE-VERIFICATION
 
diff --git a/tests/specs/functional/lemmas-spec.k b/tests/specs/functional/lemmas-spec.k
index 0f9cd2517a..3d6bfbf3e0 100644
--- a/tests/specs/functional/lemmas-spec.k
+++ b/tests/specs/functional/lemmas-spec.k
@@ -557,18 +557,18 @@ module LEMMAS-SPEC
     claim [bit-240-m-or-nm]: <k> runLemma ( maxUInt240 &Int ( X |Int ( notMaxUInt240 &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 240 , X ) andBool #rangeUInt(256, T)
     claim [bit-248-m-or-nm]: <k> runLemma ( maxUInt248 &Int ( X |Int ( notMaxUInt248 &Int T ) ) ) => doneLemma( X ) ... </k> requires #rangeUInt ( 248 , X ) andBool #rangeUInt(256, T)
 
-    // claim [bit-008-nm-or-m]: <k> runLemma ( notMaxUInt8   &Int ( X |Int ( maxUInt8   &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 248 , X ) andBool #rangeUInt(256, T)
-    // claim [bit-016-nm-or-m]: <k> runLemma ( notMaxUInt16  &Int ( X |Int ( maxUInt16  &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 240 , X ) andBool #rangeUInt(256, T)
-    // claim [bit-032-nm-or-m]: <k> runLemma ( notMaxUInt32  &Int ( X |Int ( maxUInt32  &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 224 , X ) andBool #rangeUInt(256, T)
-    // claim [bit-064-nm-or-m]: <k> runLemma ( notMaxUInt64  &Int ( X |Int ( maxUInt64  &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 192 , X ) andBool #rangeUInt(256, T)
-    // claim [bit-096-nm-or-m]: <k> runLemma ( notMaxUInt96  &Int ( X |Int ( maxUInt96  &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 160 , X ) andBool #rangeUInt(256, T)
-    // claim [bit-128-nm-or-m]: <k> runLemma ( notMaxUInt128 &Int ( X |Int ( maxUInt128 &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 128 , X ) andBool #rangeUInt(256, T)
-    // claim [bit-160-nm-or-m]: <k> runLemma ( notMaxUInt160 &Int ( X |Int ( maxUInt160 &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt (  96 , X ) andBool #rangeUInt(256, T)
-    // claim [bit-192-nm-or-m]: <k> runLemma ( notMaxUInt192 &Int ( X |Int ( maxUInt192 &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt (  64 , X ) andBool #rangeUInt(256, T)
-    // claim [bit-208-nm-or-m]: <k> runLemma ( notMaxUInt208 &Int ( X |Int ( maxUInt208 &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt (  48 , X ) andBool #rangeUInt(256, T)
-    // claim [bit-224-nm-or-m]: <k> runLemma ( notMaxUInt224 &Int ( X |Int ( maxUInt224 &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt (  32 , X ) andBool #rangeUInt(256, T)
-    // claim [bit-240-nm-or-m]: <k> runLemma ( notMaxUInt240 &Int ( X |Int ( maxUInt240 &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt (  16 , X ) andBool #rangeUInt(256, T)
-    // claim [bit-248-nm-or-m]: <k> runLemma ( notMaxUInt248 &Int ( X |Int ( maxUInt248 &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt (   8 , X ) andBool #rangeUInt(256, T)
+    claim [bit-008-nm-or-m]: <k> runLemma ( notMaxUInt8   &Int ( X |Int ( maxUInt8   &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt (   8 , X ) andBool #rangeUInt(256, T)
+    claim [bit-016-nm-or-m]: <k> runLemma ( notMaxUInt16  &Int ( X |Int ( maxUInt16  &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt (  16 , X ) andBool #rangeUInt(256, T)
+    claim [bit-032-nm-or-m]: <k> runLemma ( notMaxUInt32  &Int ( X |Int ( maxUInt32  &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt (  32 , X ) andBool #rangeUInt(256, T)
+    claim [bit-064-nm-or-m]: <k> runLemma ( notMaxUInt64  &Int ( X |Int ( maxUInt64  &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt (  64 , X ) andBool #rangeUInt(256, T)
+    claim [bit-096-nm-or-m]: <k> runLemma ( notMaxUInt96  &Int ( X |Int ( maxUInt96  &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt (  96 , X ) andBool #rangeUInt(256, T)
+    claim [bit-128-nm-or-m]: <k> runLemma ( notMaxUInt128 &Int ( X |Int ( maxUInt128 &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 128 , X ) andBool #rangeUInt(256, T)
+    claim [bit-160-nm-or-m]: <k> runLemma ( notMaxUInt160 &Int ( X |Int ( maxUInt160 &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 160 , X ) andBool #rangeUInt(256, T)
+    claim [bit-192-nm-or-m]: <k> runLemma ( notMaxUInt192 &Int ( X |Int ( maxUInt192 &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 192 , X ) andBool #rangeUInt(256, T)
+    claim [bit-208-nm-or-m]: <k> runLemma ( notMaxUInt208 &Int ( X |Int ( maxUInt208 &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 208 , X ) andBool #rangeUInt(256, T)
+    claim [bit-224-nm-or-m]: <k> runLemma ( notMaxUInt224 &Int ( X |Int ( maxUInt224 &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 224 , X ) andBool #rangeUInt(256, T)
+    claim [bit-240-nm-or-m]: <k> runLemma ( notMaxUInt240 &Int ( X |Int ( maxUInt240 &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 240 , X ) andBool #rangeUInt(256, T)
+    claim [bit-248-nm-or-m]: <k> runLemma ( notMaxUInt248 &Int ( X |Int ( maxUInt248 &Int T ) ) ) => doneLemma( 0 ) ... </k> requires #rangeUInt ( 248 , X ) andBool #rangeUInt(256, T)
 
     claim [bit-008-m-aW]: <k> runLemma ( maxUInt8   &Int #asWord ( BA ) ) => doneLemma ( #asWord ( #range(BA, 31,  1) ) ) ... </k> requires lengthBytes(BA) ==Int 32
     claim [bit-016-m-aW]: <k> runLemma ( maxUInt16  &Int #asWord ( BA ) ) => doneLemma ( #asWord ( #range(BA, 30,  2) ) ) ... </k> requires lengthBytes(BA) ==Int 32
@@ -668,6 +668,84 @@ module LEMMAS-SPEC
           ) ... </k>
         requires lengthBytes ( VV0_data_114b9705:Bytes ) <=Int 1073741824
 
+    claim [asWord-unif-01]: // two `#asWord`s, both under 32 bytes
+      <k> runLemma(
+            #asWord ( B1 +Bytes B2 ) ==Int #asWord ( B3 )
+          ) => doneLemma(
+            #buf(22, 0) +Bytes B1 +Bytes B2 ==K #buf(16, 0) +Bytes B3
+          ) ... </k>
+        requires lengthBytes(B1) ==Int 4 andBool lengthBytes(B2) ==Int 6
+         andBool lengthBytes(B3) ==Int 16
+
+    claim [asWord-unif-02]: // two `#asWord`s, left over 32 bytes
+      <k> runLemma(
+            #asWord ( B1 +Bytes B2 ) ==Int #asWord ( B3 +Bytes B4 )
+          ) => doneLemma(
+            #range ( B1, 7, 5 ) +Bytes B2 ==K #buf(7, 0) +Bytes B3 +Bytes B4
+          ) ... </k>
+        requires lengthBytes(B1) ==Int 12 andBool lengthBytes(B2) ==Int 27
+         andBool lengthBytes(B3) ==Int 10 andBool lengthBytes(B4) ==Int 15
+
+    claim [asWord-unif-03]: // `#asWord` and constant out of range, buffer length <=Int 32
+      <k> runLemma(
+            #asWord ( B ) ==Int -15 orBool 2 ^Int 160 ==Int #asWord ( B )
+          ) => doneLemma(
+            false
+          ) ... </k>
+          requires lengthBytes(B) ==Int 16
+
+    claim [asWord-unif-04]: // `#asWord` and constant out of range, buffer length >Int 32
+      <k> runLemma(
+            #asWord ( B ) ==Int -15 orBool 2 ^Int 324 ==Int #asWord ( B )
+          ) => doneLemma(
+            false
+          ) ... </k>
+          requires lengthBytes(B) ==Int 36
+
+    claim [asWord-unif-05]: // `#asWord` and constant, buffer length <=Int 32
+      <k> runLemma(
+            #asWord ( B1 +Bytes B2 ) ==Int 9518572911576893851958972884578457483927345
+          ) => doneLemma(
+            B1 +Bytes B2 ==K #buf(27, 9518572911576893851958972884578457483927345)
+          ) ... </k>
+        requires lengthBytes(B1) ==Int 15 andBool lengthBytes(B2) ==Int 12
+
+    claim [asWord-unif-06]: // `#asWord` and constant, buffer length >Int 32
+      <k> runLemma(
+            #asWord ( B1 +Bytes B2 ) ==Int 294572972648782479679175618975648679836
+          ) => doneLemma(
+            #range(B1, 3, 17) +Bytes B2 ==K #buf(32, 294572972648782479679175618975648679836)
+          ) ... </k>
+        requires lengthBytes(B1) ==Int 20 andBool lengthBytes(B2) ==Int 15
+
+    claim [asWord-chop-overflow-div]:
+      <k> runLemma(
+            #asWord( BA1 +Bytes BA2 ) /Int N
+          ) => doneLemma(
+            // #asWord ( BA2 ) /Int N
+            #asWord ( #range ( BA2, 0, lengthBytes( BA2 ) -Int ( log2Int( N ) /Int 8 ) ) )
+          ) ... </k>
+        requires 0 <Int N andBool N ==Int 2 ^Int log2Int ( N ) andBool log2Int( N ) modInt 8 ==Int 0
+         andBool 0 <Int lengthBytes(BA1) andBool lengthBytes(BA2) ==Int 32
+
+    claim [asWord-chop-overflow-lt]:
+      <k> runLemma(
+            #asWord ( BA1 +Bytes BA2 +Bytes BA3 ) <Int X:Int
+          ) => doneLemma(
+            #asWord ( BA2 +Bytes BA3 ) <Int X
+          ) ... </k>
+        requires #asWord ( BA3 ) ==Int X modInt ( 2 ^Int ( 8 *Int lengthBytes ( BA3 ) ) )
+         andBool 0 <Int lengthBytes(BA1) andBool lengthBytes(BA2 +Bytes BA3) ==Int 32
+
+    claim [asWord-chop-overflow-le]:
+      <k> runLemma(
+            #asWord ( BA1 +Bytes BA2 +Bytes BA3 ) <=Int X:Int
+          ) => doneLemma(
+            #asWord ( BA2 +Bytes BA3 ) <=Int X
+          ) ... </k>
+        requires #asWord ( BA3 ) ==Int X modInt ( 2 ^Int ( 8 *Int lengthBytes ( BA3 ) ) )
+         andBool 0 <Int lengthBytes(BA1) andBool lengthBytes(BA2 +Bytes BA3) ==Int 32
+
  // bool2Word
  // ---------