src/lemmas.k.md: fix TIME rule

rangeUInt(224, pow224) is false, which means our rule wouldn't have applied.
dapp-org · Apr 14, 2020 · 6ef4644 · 6ef4644
1 parent 417de9f
commit 6ef4644
Showing 1 changed file with 1 addition and 3 deletions.
diff --git a/src/lemmas.k.md b/src/lemmas.k.md
@@ -73,9 +73,7 @@ rule (X &Int Y) <=Int X => true
 ```
 
 ```k
-rule chop((X &Int Y) *Int Z) => (X &Int Y) *Int Z
-  requires (#rangeUInt(32,  X) orBool #rangeUInt(32, Y))
-  andBool #rangeUInt(224, Z)
+rule ((maxUInt32 &Int X) *Int pow224) <= maxUInt256 => true
 ```
 
 Repeated application of `modInt` can be simplified as follows. This lets us clean the storage