fix: move the simlification rules to the same place

Author: Stevengre

kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md

@@ -52,9 +52,16 @@ If nothing is removed, the list remains the same. If all elements are removed, n
 ```
 
 The `#mapOffset` function maps `#adjustRef` over a lists of `Value`s, leaving the list length unchanged.
-Definedness of the list and list elements is also guaranteed.
+Definedness of the list and list elements is also guaranteed.  
+The helper `#adjustRef` reduces to the original value when the offset is zero and merges nested offset adjustments.
 
 ```k
+  rule #adjustRef(VAL:Value, 0) => VAL [simplification]
+
+  rule #adjustRef(#adjustRef(VAL, OFFSET1), OFFSET2)
+    => #adjustRef(VAL, OFFSET1 +Int OFFSET2)
+    [simplification]
+
   rule size(#mapOffset(L, _)) => size(L) [simplification, preserves-definedness]
 
   rule #Ceil(#mapOffset(L, _)[I]) => #Ceil(L) #And {true #Equals 0 <=Int I} #And {true #Equals I <Int size(L)} [simplification]

kmir/src/kmir/kdist/mir-semantics/rt/data.md

@@ -428,12 +428,6 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
     => Range(#mapOffset(ELEMS, OFFSET))
   rule #adjustRef(TL, _) => TL [owise]
 
-  rule #adjustRef(#adjustRef(VAL, OFFSET1), OFFSET2)
-    => #adjustRef(VAL, OFFSET1 +Int OFFSET2)
-    [simplification]
-
-  rule #adjustRef(VAL:Value, 0) => VAL [simplification]
-
   syntax List ::= #mapOffset ( List, Int ) [function, total]
   // -------------------------------------------------------
   rule #mapOffset(.List, _)