From 570c9e207e22c7333c5328901f5b6d72f53eefba Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Wed, 21 Aug 2024 22:35:46 +0200
Subject: [PATCH] two more lemmas

---
 src/kontrol/kdist/kontrol_lemmas.md | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/kontrol/kdist/kontrol_lemmas.md b/src/kontrol/kdist/kontrol_lemmas.md
index cb894ebf7..4a907a0c4 100644
--- 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
 ```
\ No newline at end of file