Speedup to first 10 steps of mcd proofs

diff --git a/tests/specs/mcd/concrete-rules.txt b/tests/specs/mcd/concrete-rules.txt
index c15aca708..8e7906129 100644
--- a/tests/specs/mcd/concrete-rules.txt
+++ b/tests/specs/mcd/concrete-rules.txt
@@ -27,3 +27,5 @@ EVM-TYPES.upDivInt
 SERIALIZATION.keccak
 SERIALIZATION.#newAddr
 SERIALIZATION.#newAddrCreate2
+EVM.isPrecompiledAccount.true
+EVM.isPrecompiledAccount.false
diff --git a/tests/specs/mcd/dsvalue-read-pass-spec.k b/tests/specs/mcd/dsvalue-read-pass-spec.k
index d179cb2dc..06a0c7d14 100644
--- a/tests/specs/mcd/dsvalue-read-pass-spec.k
+++ b/tests/specs/mcd/dsvalue-read-pass-spec.k
@@ -62,16 +62,7 @@ module DSVALUE-READ-PASS-SPEC
         </evm>
         <network>
           <chainID> VChainId </chainID>
-          <activeAccounts> SetItem(ACCT_ID)
-          SetItem(1)
-          SetItem(2)
-          SetItem(3)
-          SetItem(4)
-          SetItem(5)
-          SetItem(6)
-          SetItem(7)
-          SetItem(8)
-          SetItem(9) _ </activeAccounts>
+          <activeAccounts> SetItem(ACCT_ID) |Set #precompiledAccounts(ISTANBUL) |Set _ </activeAccounts>
           <accounts>
             <account>
               <acctID> ACCT_ID </acctID>
diff --git a/tests/specs/mcd/verification.k b/tests/specs/mcd/verification.k
index b512b096d..64a938191 100644
--- a/tests/specs/mcd/verification.k
+++ b/tests/specs/mcd/verification.k
@@ -20,7 +20,7 @@ module LEMMAS-MCD-SYNTAX

     syntax Bool ::= #notPrecompileAddress ( Int ) [function]
  // --------------------------------------------------------
-    rule #notPrecompileAddress ( X ) => 0 ==Int X orBool (10 <=Int X andBool #rangeAddress(X))
+    rule #notPrecompileAddress ( X ) => notBool #isPrecompiledAccount(X, ISTANBUL)

     syntax Int ::= #string2Word ( String ) [function]
  // -------------------------------------------------
@@ -58,6 +58,11 @@ module LEMMAS-MCD-HASKELL [symbolic, kore]

     rule chop(Y) => Y +Int pow256 requires #rangeSInt(256, Y) andBool Y <Int 0 [simplification]

+    rule .Set -Set _:Set => .Set [simplification]
+    rule (SetItem(X) REST) -Set SetItem(Y) => SetItem(X) (REST -Set SetItem(Y)) requires (notBool #notPrecompileAddress(X)) andBool #notPrecompileAddress(Y) [simplification]
+
+    rule { ACCT #Equals I } => #Bottom requires #notPrecompileAddress(ACCT) andBool notBool #notPrecompileAddress(I) [simplification, anywhere]
+
     // ### flapper-yank-pass-rough

     rule #range(M:Memory [ K <- V ], START, WIDTH) => #range(M [ K := (V : .ByteArray) ], START, WIDTH)

Start by reviewing the proposed changes in tests/specs/mcd/concrete-rules.txt, tests/specs/mcd/dsvalue-read-pass-spec.k, and tests/specs/mcd/verification.k. Run the relevant MCD proof specifications and compare their first ten steps with the current behavior. Done means the proofs complete faster while the affected specifications continue to pass.