lemma corrections

runtimeverification · Aug 21, 2024 · 63727d8 · 63727d8
1 parent 272c711
commit 63727d8
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/test/kontrol/lido-lemmas.k b/test/kontrol/lido-lemmas.k
@@ -46,8 +46,8 @@ module LIDO-LEMMAS
     rule A *Int B => B *Int A [simplification(30), symbolic(A), concrete(B)]
 
     // /Int
-    rule 0 /Int B         => 0         requires B =/=Int 0 [simplification, preserves-definedness]
-    rule A /Int B ==Int 0 => A ==Int 0 requires B =/=Int 0 [simplification, preserves-definedness]
+    rule 0 /Int B         => 0        requires B =/=Int 0                 [simplification, preserves-definedness]
+    rule A /Int B ==Int 0 => A <Int B requires 0 <=Int A andBool 0 <Int B [simplification, preserves-definedness]
 
     rule ( A *Int B ) /Int C => ( A /Int C ) *Int B requires A modInt C ==Int 0 [simplification, concrete(A, C), preserves-definedness]