adding further in_keys lemmas

runtimeverification · Dec 26, 2024 · 1aa76f6 · 1aa76f6
1 parent f306263
commit 1aa76f6
Showing 1 changed file with 4 additions and 0 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
@@ -127,6 +127,10 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic]
     rule ( _:Map [ K1 <- V ] ):Map [ K2 ] => V            requires         K1 ==K K2 [simplification(45), preserves-definedness]
     rule ( M:Map [ K1 <- _ ] ):Map [ K2 ] => M:Map [ K2 ] requires notBool K1 ==K K2 [simplification(45), preserves-definedness]
 
+    // Symbolic membership of map concat
+    rule K1 in_keys( ( K2 -> _ ) _:Map ) => true          requires         K1 ==K K2 [simplification(45), preserves-definedness]
+    rule K1 in_keys( ( K2 -> _ ) M:Map ) => K1 in_keys(M) requires notBool K1 ==K K2 [simplification(45), preserves-definedness]
+
     // Symbolic membership of map update
     rule K1 in_keys( _:Map [ K2 <- _ ] ) => true          requires         K1 ==K K2 [simplification(45), preserves-definedness]
     rule K1 in_keys( M:Map [ K2 <- _ ] ) => K1 in_keys(M) requires notBool K1 ==K K2 [simplification(45), preserves-definedness]