diff --git a/package/version b/package/version
index c29f5f75..72400828 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.114
+0.1.115
diff --git a/pyproject.toml b/pyproject.toml
index 44a23b14..40193db8 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "kriscv"
-version = "0.1.114"
+version = "0.1.115"
 description = "K tooling for the RISC-V architecture"
 readme = "README.md"
 requires-python = "~=3.10"
diff --git a/src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md b/src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md
index 81e0e84f..69c03a6b 100644
--- a/src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md
+++ b/src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md
@@ -43,6 +43,13 @@ module BYTES-SIMPLIFICATIONS [symbolic]
     rule [bytes-concat-right-assoc-symb-l]: (B1:Bytes +Bytes B2:Bytes) +Bytes B3:Bytes => B1 +Bytes (B2 +Bytes B3) [symbolic(B1), simplification(40)]
     rule [bytes-concat-right-assoc-symb-r]: (B1:Bytes +Bytes B2:Bytes) +Bytes B3:Bytes => B1 +Bytes (B2 +Bytes B3) [symbolic(B2), simplification(40)]
     rule [bytes-concat-left-assoc-conc]:    B1:Bytes +Bytes (B2:Bytes +Bytes B3:Bytes) => (B1 +Bytes B2) +Bytes B3 [concrete(B1, B2), symbolic(B3), simplification(40)]
+
+    rule [bytes-concat-substr]: substrBytes(A, I0, J0) +Bytes substrBytes(A, I1, J1) => substrBytes(A, I0, J1)
+      requires I0 <=Int J0 andBool I1 <=Int J1 andBool J0 ==Int I1 andBool J1 <=Int lengthBytes(A)
+      [simplification, preserves-definedness]
+    rule [bytes-concat-substr-cxt]: substrBytes(A, I0, J0) +Bytes substrBytes(A, I1, J1) +Bytes B => substrBytes(A, I0, J1) +Bytes B
+      requires I0 <=Int J0 andBool I1 <=Int J1 andBool J0 ==Int I1 andBool J1 <=Int lengthBytes(A)
+      [simplification, preserves-definedness]
 ```
 
 ## Bytes Update Lemmas
diff --git a/src/tests/integration/test-data/specs/bytes-concat-consecutive.k b/src/tests/integration/test-data/specs/bytes-concat-consecutive.k
new file mode 100644
index 00000000..d15135f7
--- /dev/null
+++ b/src/tests/integration/test-data/specs/bytes-concat-consecutive.k
@@ -0,0 +1,14 @@
+module BYTES-CONCAT-CONSECUTIVE
+  imports RISCV
+
+  claim [id]:
+    <instrs> #CHECK_HALT => #HALT </instrs>
+    <pc> 0 </pc>
+    <mem>
+      #bytes(b"\x00\x00\x00\x00" +Bytes substrBytes(reverseBytes(VALUE), 0, 4) +Bytes substrBytes(reverseBytes(VALUE), 4, 8) +Bytes substrBytes(reverseBytes(VALUE), 8, 12) +Bytes substrBytes(reverseBytes(VALUE), 12, 16) +Bytes substrBytes(reverseBytes(VALUE), 16, 20) +Bytes substrBytes(reverseBytes(VALUE), 20, 24) +Bytes substrBytes(reverseBytes(VALUE), 24, 28) +Bytes substrBytes(reverseBytes(VALUE), 28, 32) +Bytes b"\x00\x00\x00\x00" ) .SparseBytes 
+    =>
+    #bytes(b"\x00\x00\x00\x00" +Bytes reverseBytes(VALUE) +Bytes b"\x00\x00\x00\x00" ) .SparseBytes
+    </mem>
+    <haltCond> ADDRESS ( 0 ) </haltCond>
+    requires lengthBytes(VALUE) ==Int 32
+endmodule
diff --git a/uv.lock b/uv.lock
index 1d1bd3ce..372a9af4 100644
--- a/uv.lock
+++ b/uv.lock
@@ -643,7 +643,7 @@ wheels = [
 
 [[package]]
 name = "kriscv"
-version = "0.1.114"
+version = "0.1.115"
 source = { editable = "." }
 dependencies = [
     { name = "filelock" },