Fix: misplaced parens in deposits function (formal spec) (#1027)

* Update utxo.tex * Update properties.tex
IntersectMBO · Nov 15, 2019 · ec170e3 · ec170e3
2 parents 57766e2 + 582b8e1
commit ec170e3
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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}

diff --git 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}