two more lemmas

runtimeverification · Aug 21, 2024 · 570c9e2 · 570c9e2
1 parent f709606
commit 570c9e2
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/src/kontrol/kdist/kontrol_lemmas.md b/src/kontrol/kdist/kontrol_lemmas.md
@@ -456,5 +456,12 @@ module KONTROL-AUX-LEMMAS
       requires 0 <=Int A
       [simplification]
 
+    rule bool2Word(X) *Int Y ==Int Z => (X andBool (Y ==Int Z)) orBool ((notBool X) andBool Z ==Int 0)
+      [simplification]
+
+    rule X *Int Y <=Int Z => Y <Int ( Z +Int 1 ) /Int X
+      requires 0 <Int X andBool 0 <=Int Z andBool ( Z +Int 1) modInt X ==Int 0
+      [simplification, concrete(X, Z), preserves-definedness]
+
 endmodule
 ```