diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md
index 25bad17..5dc5e5c 100644
--- a/src/uniswap-summaries.md
+++ b/src/uniswap-summaries.md
@@ -3020,6 +3020,106 @@ module SOLIDITY-UNISWAP-FIDUPDATE-3-SUMMARY
Storage => Storage [ vidBalances <- write({write({Storage [ vidBalances ] orDefault .Map}:>Value, ListItem(V1), ({read({Storage [ vidBalances ] orDefault .Map}:>Value, ListItem(V1), (mapping ( address account => uint256 )))}:>MInt{256} -MInt V3:MInt{256}), (mapping ( address account => uint256)))}:>Value, ListItem(V2), ({read({Storage [ vidBalances ] orDefault .Map}:>Value, ListItem(V2), (mapping ( address account => uint256 )))}:>MInt{256} +MInt V3:MInt{256}), (mapping ( address account => uint256))) ]
requires V1 =/=MInt 0p160 andBool V2 =/=MInt 0p160
andBool {read({Storage [ vidBalances ] orDefault .Map}:>Value, ListItem(V1), (mapping ( address account => uint256 )))}:>MInt{256} >=uMInt V3:MInt{256} [priority(40)]
+endmodule
+```
+
+```k
+module SOLIDITY-UNISWAP-SETUP-SUMMARY
+ imports SOLIDITY-CONFIGURATION
+ imports SOLIDITY-UNISWAP-TOKENS
+ imports SOLIDITY-EXPRESSION
+ imports SOLIDITY-STATEMENT
+
+ rule bind ( .List , .List , .List , .TypedVals , .List , .List ) ~> vidWeth = new wETHMock ( .TypedVals ) ; vidDai = new dAIMock ( .TypedVals ) ; vidUsdc = new uSDCMock ( .TypedVals ) ; vidUni = new uniswapV2Swap ( address ( vidWeth , .TypedVals ) , address ( vidDai , .TypedVals ) , address ( vidUsdc , .TypedVals ) , .TypedVals ) ; .Statements => .K ...
+ true
+ THIS
+ TYPE
+ TYPE
+
+ ...
+
+ THIS
+ TYPE
+
+ S => S [ vidWeth <- ADDR ] [ vidDai <- ADDR +MInt 1p160 ] [ vidUsdc <- ADDR +MInt 2p160 ] [ vidUni <- ADDR +MInt 3p160 ]
+
+ ...
+
+ (.Bag =>
+ ADDR
+ wETHMock
+
+ constUINT256MAX |-> 115792089237316195423570985008687907853269984665640564039457584007913129639935p256
+
+ ...
+
+
+ ADDR +MInt 1p160
+ dAIMock
+
+ constUINTMAX |-> 115792089237316195423570985008687907853269984665640564039457584007913129639935p256
+
+
+
+ ADDR +MInt 2p160
+ uSDCMock
+
+ constUINT256MAX |-> 115792089237316195423570985008687907853269984665640564039457584007913129639935p256
+
+
+
+ ADDR +MInt 3p160
+ uniswapV2Swap
+
+ dai |-> ADDR +MInt 1p160
+ router |-> ADDR +MInt 4p160
+ usdc |-> ADDR +MInt 2p160
+ weth |-> ADDR
+
+
+
+ ADDR +MInt 4p160
+ uniswapV2Router02
+
+ localPairs |-> ( ADDR |-> ( (ADDR +MInt 1p160 |-> ADDR +MInt 5p160)
+ (ADDR +MInt 2p160 |-> ADDR +MInt 6p160) )
+ (ADDR +MInt 1p160 |-> ( ADDR +MInt 2p160 |-> ADDR +MInt 7p160 )) )
+
+
+
+ ADDR +MInt 5p160
+ uniswapV2Pair
+
+ constMINIMUMLIQUIDITY |-> 1000p256
+ constUINT112MAX |-> 5192296858534827628530496329220095p256
+ token0 |-> ADDR
+ token1 |-> ADDR +MInt 1p160
+
+
+
+ ADDR +MInt 6p160
+ uniswapV2Pair
+
+ constMINIMUMLIQUIDITY |-> 1000p256
+ constUINT112MAX |-> 5192296858534827628530496329220095p256
+ token0 |-> ADDR
+ token1 |-> ADDR +MInt 2p160
+
+
+
+ ADDR +MInt 7p160
+ uniswapV2Pair
+
+ constMINIMUMLIQUIDITY |-> 1000p256
+ constUINT112MAX |-> 5192296858534827628530496329220095p256
+ token0 |-> ADDR +MInt 1p160
+ token1 |-> ADDR +MInt 2p160
+
+ )
+ ...
+
+ ADDR => ADDR +MInt 8p160
+ setUp [priority(40)]
endmodule
```
@@ -3034,6 +3134,7 @@ module SOLIDITY-UNISWAP-SUMMARIES
imports SOLIDITY-UNISWAP-FIDSWAP-SUMMARY
imports SOLIDITY-UNISWAP-FIDUPDATE-4-SUMMARY
imports SOLIDITY-UNISWAP-FIDUPDATE-3-SUMMARY
+ imports SOLIDITY-UNISWAP-SETUP-SUMMARY
endmodule
```