diff --git a/kwasm-polkadot-host.md b/kwasm-polkadot-host.md
index ba3a023..9fad85f 100644
--- a/kwasm-polkadot-host.md
+++ b/kwasm-polkadot-host.md
@@ -16,6 +16,7 @@ module KWASM-POLKADOT-HOST
     imports K-IO
     imports WASM-TEST
     imports KWASM-LEMMAS
+    imports MERGED-RULES
 
     configuration
       <polkadot-host>
@@ -56,6 +57,185 @@ module KWASM-POLKADOT-HOST
            <funcIds> ... ID |-> IDX:Int ... </funcIds>
            ...
         </moduleInst>
+endmodule
+```
+
+Merged Rules
+============
+
+This is a set of rules created by identifying common sub-sequences of semantic steps during execution of the `set_free_balance` function.
+
+Most rules could not be used as they were printed, but had to be massaged in the following ways.
+-   Remove <generatedTop> cell
+-   Remove ellipsis inserted under that cell
+-   Remove ensures
+-   ~> DotVar\W* => ...
+-   #init\([^l]\)locals => #init_locals \1
+-   S SS => S SS:Stmts
+-   `BOP` => `BOP:IBinOp`,
+-   remove `<polkadot-host>`
+
+```k
+module MERGED-RULES
+    imports WASM-TEST
+    
+    rule <wasm>
+           <k>
+                 (     ITYPE0 .const VAL
+             ~> ITYPE0 . BOP:IBinOp:IBinOp SS =>     ITYPE0 . BOP C1 VAL modInt #pow( ITYPE0 )
+             ~> SS )
+             ...
+           </k>
+           <valstack>
+             ( < ITYPE0 > C1 : VALSTACK0 => VALSTACK0 )
+           </valstack>
+           ...
+         </wasm>
+         requires notBool SS ==K .EmptyStmts andBool false ==K #pow( ITYPE0 ) ==Int 0 andBool true
+  [priority(25)]
+
+    rule <wasm>
+           <k>
+                 (     #init_locals  N  VALUE0 : VALUE2 : VALSTACK0 =>     #init_locals  N +Int 2  VALSTACK0 )
+             ...
+           </k>
+           <curFrame>
+             <locals>
+               ( LOCALS => LOCALS [ N <- VALUE0 ] [ N +Int 1 <- VALUE2 ] )
+             </locals>
+             ...
+           </curFrame>
+           ...
+         </wasm>
+         requires true andBool true
+  [priority(25)]
+
+    rule <wasm>
+           <k>
+                 (     ITYPE .const VAL
+             ~> S SS:Stmts =>     S
+             ~> SS )
+             ...
+           </k>
+           <valstack>
+             ( VALSTACK => < ITYPE > VAL modInt #pow( ITYPE ) : VALSTACK )
+           </valstack>
+           ...
+         </wasm>
+         requires notBool SS ==K .EmptyStmts andBool false ==K #pow( ITYPE ) ==Int 0 andBool true
+  [priority(25)]
+
+    rule <wasm>
+           <k>
+                 (     #init_locals  N  VALUE0 : VALSTACK =>     #init_locals  N +Int 1  VALSTACK )
+             ...
+           </k>
+           <curFrame>
+             <locals>
+               ( LOCALS => LOCALS [ N <- VALUE0 ] )
+             </locals>
+             ...
+           </curFrame>
+           ...
+         </wasm>
+         requires true andBool true
+  [priority(25)]
 
+    rule <wasm>
+           <k>
+                 (     ITYPE0 .const VAL ITYPE0 . BOP:IBinOp SS0 =>     ITYPE0 . BOP C1 VAL modInt #pow( ITYPE0 )
+             ~> SS0 )
+             ...
+           </k>
+           <valstack>
+             ( < ITYPE0 > C1 : VALSTACK0 => VALSTACK0 )
+           </valstack>
+           ...
+         </wasm>
+         requires notBool SS0 ==K .EmptyStmts andBool false ==K #pow( ITYPE0 ) ==Int 0 andBool true
+  [priority(25)]
+
+    rule <wasm>
+           <k>
+                 (     V
+             ~> S SS:Stmts =>     S
+             ~> SS )
+             ...
+           </k>
+           <valstack>
+             ( VALSTACK => V : VALSTACK )
+           </valstack>
+           ...
+         </wasm>
+         requires notBool V ==K undefined andBool notBool SS ==K .EmptyStmts
+```
+
+The following rule required extra massaging:
+
+-   Remove `#Forall` side condition.
+-   Change #SemanticCastToInt to regular typing.
+-   Dotvar5 in the `<locals>` cell => ... on both sides.
+
+```k
+    rule <wasm>
+           <k>
+                 (     local.get I:Int
+             ~> S SS:Stmts =>     S
+             ~> SS )
+             ...
+           </k>
+           <valstack>
+             ( VALSTACK => VALUE : VALSTACK )
+           </valstack>
+           <curFrame>
+             <locals>
+               ... I |-> VALUE ...
+             </locals>
+             ...
+           </curFrame>
+           ...
+         </wasm>
+         requires notBool SS ==K .EmptyStmts andBool true
+  [priority(25)]
+
+    rule <wasm>
+           <k>
+                 (     local.get I:Int S0 SS0 =>     S0
+             ~> SS0 )
+             ...
+           </k>
+           <valstack>
+             ( VALSTACK => VALUE : VALSTACK )
+           </valstack>
+           <curFrame>
+             <locals>
+               ... I |-> VALUE ...
+             </locals>
+             ...
+           </curFrame>
+           ...
+         </wasm>
+         requires notBool SS0 ==K .EmptyStmts
+  andBool true
+  [priority(25)]
+
+    rule <wasm>
+           <k>
+                 (     local.get I:Int ITYPE0 .const VAL ITYPE0 . BOP:IBinOp SS1 =>     ITYPE0 . BOP C1 VAL modInt #pow( ITYPE0 )
+             ~> SS1 )
+             ...
+           </k>
+           <curFrame>
+             <locals>
+               ... I |-> < ITYPE0 > C1 ...
+             </locals>
+             ...
+           </curFrame>
+           ...
+         </wasm>
+         requires notBool SS1 ==K .EmptyStmts andBool false ==K #pow( ITYPE0 ) ==Int 0 andBool true
+```
+
+```k
 endmodule
 ```
diff --git a/search.py b/search.py
index e2b2838..08dbdbe 100755
--- a/search.py
+++ b/search.py
@@ -99,7 +99,7 @@ def wasm_stmts_flattened(stmts, stmtType = 'Stmt'):
 sys.stdout.flush()
 
 if args['command'] == 'summary':
-    ruleMerges = merge_rules_max_productivity(ruleSeqs, min_merged_success_rate = 0.25, min_occurance_rate = 0.05)
+    ruleMerges = merge_rules_max_productivity(ruleSeqs, min_merged_success_rate = 0.15, min_occurance_rate = 0.00)
     mergedRules = tryMergeRules(WASM_definition_haskell_no_coverage_dir, WASM_definition_main_file, WASM_definition_main_module, ruleMerges)
     for mr in mergedRules:
         print('Merged Rule:')