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
index cefcf26f74..221528a759 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k
@@ -47,7 +47,6 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic]
   // ########################
 
     rule N <=Int #sizeWordStack ( _ , N ) => true requires 0 <=Int N [simplification, smt-lemma]
-  //  rule #sizeWordStack ( _ : WS, 0 ) => 1 +Int #sizeWordStack ( WS, 0 ) [simplification, smt-lemma]
 
     // #newAddr range
     rule 0 <=Int #newAddr(_,_)             => true   [simplification]
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/summary-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/summary-simplification.k
deleted file mode 100644
index ee3555d60e..0000000000
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/summary-simplification.k
+++ /dev/null
@@ -1,21 +0,0 @@
-requires "../gas.md"
-
-module SUMMARY-SIMPLIFICATION
-    imports SUMMARY-SIMPLIFICATION-COMMON
-endmodule
-
-module SUMMARY-SIMPLIFICATION-COMMON
-    imports GAS
-
- //   rule { true #Equals ( notBool G0 <Gas G1 ) } #And  { true #Equals ( notBool G1 <=Gas G0 ) } => false [simplification]
-
- // ---------------------------------------------------------------------
- // simpification rules for stack underflow check
- rule { WORDSTACK:WordStack #Equals ( W0:Int : ( W1:Int : WS:WordStack ) ) } => 
- //   rule notBool #sizeWordStack ( WORDSTACK:WordStack , 0 ) <Int 1 => { WORDSTACK #Equals ( ?W0:Int : ?WS:WordStack ) } [simplification, symbolic]
- //   rule notBool #sizeWordStack ( WORDSTACK:WordStack , 0 ) <Int 2 => ( #Exists W0:Int . #Exists W1:Int . #Exists WS:WordStack . { WORDSTACK:WordStack #Equals ( W0:Int : ( W1:Int : WS:WordStack ) ) } ) [simplification, symbolic]
- //   rule { true #Equals ( notBool #sizeWordStack ( WORDSTACK:WordStack , 0 ) <Int 2 ) } #And #Not ( #Exists W0:Int . #Exists W1:Int . #Exists WS:WordStack . { WORDSTACK:WordStack #Equals ( W0:Int : ( W1:Int : WS:WordStack ) ) } ) => #Bottom [simplification]
- //   rule notBool #sizeWordStack ( WORDSTACK:WordStack , 0 ) <Int 3 => { WORDSTACK #Equals ( ?W0:Int : ( ?W1:Int : ( ?W2:Int : ?WS:WordStack ) ) ) } [simplification, symbolic]
- //   rule notBool #sizeWordStack ( WORDSTACK:WordStack , 0 ) <Int 4 => { WORDSTACK #Equals ( ?W0:Int : ( ?W1:Int : ( ?W2:Int : ( ?W3:Int : ?WS:WordStack ) ) ) ) } [simplification, symbolic]
-
-endmodule
\ No newline at end of file