additional lemma for cleaning up specification of getRageQuitSupport

runtimeverification · Jun 22, 2024 · 615778d · 615778d
1 parent 3103f4a
commit 615778d
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/test/kontrol/lido-lemmas.k b/test/kontrol/lido-lemmas.k
@@ -78,6 +78,7 @@ module LIDO-LEMMAS
     // Further arithmetic
     rule ( X *Int Y ) /Int Y => X requires Y =/=Int 0              [simplification, preserves-definedness]
     rule ( X ==Int ( X *Int Y ) /Word Y ) orBool Y ==Int 0 => true [simplification, preserves-definedness]
+    rule ( 0 ==Int          0   /Word Y ) orBool Y ==Int 0 => true [simplification, preserves-definedness]
 
     rule A <=Int B /Int C =>         A  *Int C <=Int B requires 0 <Int C [simplification, preserves-definedness]
     rule A  <Int B /Int C => (A +Int 1) *Int C <=Int B requires 0 <Int C [simplification, preserves-definedness]