From d554f57d063593c31900b94cc08f0916bd43eb7d Mon Sep 17 00:00:00 2001
From: csoroz <csoroz@gmail.com>
Date: Tue, 12 Nov 2019 20:49:46 +0100
Subject: [PATCH 1/2] Update utxo.tex

---
 shelley/chain-and-ledger/formal-spec/utxo.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/shelley/chain-and-ledger/formal-spec/utxo.tex b/shelley/chain-and-ledger/formal-spec/utxo.tex
index 29f9d6b4572..f5110e65ac0 100644
--- a/shelley/chain-and-ledger/formal-spec/utxo.tex
+++ b/shelley/chain-and-ledger/formal-spec/utxo.tex
@@ -321,7 +321,7 @@ \subsection{UTxO Transitions}
       \var{decayed} \leteq \decayedTx{pp}{stkCreds}~{tx}
       \\
       \var{depositChange} \leteq
-        (\deposits{pp}~{stpools}~{\txcerts{tx}}) - (\var{refunded} + \var{decayed})
+        \deposits{pp}~{stpools}~{(\txcerts{tx})} - (\var{refunded} + \var{decayed})
     }
     {
       \begin{array}{r}

From 582b8e1b29156c575ed209994ea30f04decb645d Mon Sep 17 00:00:00 2001
From: csoroz <csoroz@gmail.com>
Date: Tue, 12 Nov 2019 20:52:33 +0100
Subject: [PATCH 2/2] Update properties.tex

---
 shelley/chain-and-ledger/formal-spec/properties.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/shelley/chain-and-ledger/formal-spec/properties.tex b/shelley/chain-and-ledger/formal-spec/properties.tex
index 9f8a6239939..43f741e935d 100644
--- a/shelley/chain-and-ledger/formal-spec/properties.tex
+++ b/shelley/chain-and-ledger/formal-spec/properties.tex
@@ -624,7 +624,7 @@ \subsection{Non-negative Deposit Pot}
   \end{equation*}
   Looking at the $\mathsf{UTXO}$ transition in Figure~\ref{fig:rules:utxo-shelley},
   \begin{equation*}
-    \var{deposits}' = \var{deposits} + (\deposits{pp}~{stpools}~{\txcerts{tx}})
+    \var{deposits}' = \var{deposits} + \deposits{pp}~{stpools}~{(\txcerts{tx})}
     - (\var{refunded} + \var{decayed})
   \end{equation*}
   The function $\fun{deposits}$ is defined in Figure~\ref{fig:functions:deposits-refunds}