From ca582e04335d1a627f5f9bcf958a48fbc3025473 Mon Sep 17 00:00:00 2001 From: Martin Lundfall Date: Fri, 23 Aug 2019 11:37:02 +0200 Subject: [PATCH] lemmas.k.md: remove fake news math --- src/lemmas.k.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lemmas.k.md b/src/lemmas.k.md index 0f05df119..18857c642 100644 --- a/src/lemmas.k.md +++ b/src/lemmas.k.md @@ -441,7 +441,7 @@ rule (A +Int pow256) -Int #unsigned(B) => A -Int B // mului // lemmas for sufficiency -rule A *Word #unsigned(B) => #unsigned(A *Int B) +rule A *Int #unsigned(B) => #unsigned(A *Int B) requires #rangeUInt(256, A) andBool #rangeSInt(256, B) andBool #rangeSInt(256, A *Int B)