lemma correction

runtimeverification · Oct 9, 2024 · 32f95b3 · 32f95b3
1 parent ad5bce8
commit 32f95b3
Showing 1 changed file with 1 addition and 1 deletion.
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
@@ -228,7 +228,7 @@ module BYTES-SIMPLIFICATION [symbolic]
       [simplification]
 
     rule [memUpdate-concat-in-left]: (B1 +Bytes B2) [ S := B ] => (B1 [ S := B ]) +Bytes B2
-      requires 0 <=Int S andBool S +Int lengthBytes(B) <=Int lengthBytes(B1)
+      requires 0 <=Int S andBool S +Int lengthBytes(B) <Int lengthBytes(B1)
       [simplification(40)]
 
     rule [memUpdate-concat-in-right]: (B1 +Bytes B2) [ S := B ] => B1 +Bytes (B2 [ S -Int lengthBytes(B1) := B ])