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