From 32f95b30b1eb43f682442d6103c48a7e9dde83bc Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Wed, 9 Oct 2024 22:18:06 +0100
Subject: [PATCH] lemma correction

---
 .../kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k  | 2 +-
 1 file changed, 1 insertion(+), 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
index 1a3e6b37a3..00ad215864 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
@@ -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 ])