streamlining set simplifications

runtimeverification · Nov 2, 2023 · 69624a0 · 69624a0
1 parent 61fac3d
commit 69624a0
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k
@@ -42,9 +42,6 @@ module LEMMAS [symbolic]
     rule X in S:Set SetItem ( Y ) => true   requires X ==Int Y  [simplification]
     rule X in S:Set SetItem ( Y ) => X in S requires X =/=Int Y [simplification]
 
-    rule X in ( S:Set |Set SetItem ( Y ) ) => true   requires X ==Int Y  [simplification]
-    rule X in ( S:Set |Set SetItem ( Y ) ) => X in S requires X =/=Int Y [simplification]
-
   // ########################
   // Word Reasoning
   // ########################