# A Formal Analysis of the Mimblewimble Cryptocurrency Protocol +
## Appendix B Background on the Z Notation
\(r\)0}  
As can be seen, operations are defined by means of schemas. The expression _DBank_ in the declaration part is a shorthand for including the schemas _Bank_ and _Bank_\({}^{\prime}\). We already know what it means including _Bank_. _Bank_\({}^{\prime}\) is equal to _Bank_ but all of its variables are decorated with a prime. Therefore, _Bank_\({}^{\prime}\) declares _balances_\({}^{\prime}\) of the same types than that in _Bank_. When a state variable is decorated with the prime it is assumed to be an after-state variable. The net effect of including _DBank_ is, then, the declaration of one before-state variable and one after-state variable. A \(D\) expression is included in every operation schema that produces a state change. Variables decorated with a question mark, like _n_?, are assumed to be input variables. Then, _n_? represents the account number to be assigned to the new savings account. To simplify the specification a little bit we assume that a bank's clerk provides the account number when the operation is called--instead of the system generating it. Note that the predicate part consists of two atomic predicates. When two or more predicates are in different rows they are assumed to be a conjunction. In other words:  
_n_? _dom_ _balances_  
_balances_ \({}^{\prime}=\) _balances_ \(\cup\) {_n_? \(r\)0}  
is equivalent to:  
_n_? _dom_ _balances_ \(\wedge\) _balances_\({}^{\prime}=\) _balances_ \(\cup\) {_n_? \(r\)0}  
_balances_ \({}^{\prime}=\) _balances_ \(\cup\) {_n_?\(Z\) uses the standard symbols of discrete mathematics and set theory so we think it will not be difficult for the reader to understand each predicate. Remember that functions and relations are sets of ordered pairs so they can participate in set expressions. For instance, _balances_\(\cup\)\(\{n?\)\(\mapsto\)\(0\}\) adds an ordered pair to _clients_. Again, the expression _balances_\({}^{\prime}=\)\(\bigcup\)\(\{n?\)\(\mapsto\)\(0\}\) is actually a predicate saying that _balances_\({}^{\prime}\) is equal to _balances_\(\cup\)\(\{n?\)\(\mapsto\)\(0\}\), and not that the latter is assigned to the former. In other words, this predicate says that the value of _balances_ in the after-state is equal to the value of _balances_ in the before-state plus the ordered pair \(n?\)\(\mapsto\)\(0\). Note that operations are defined by giving their preconditions and postconditions. In _NewClientOk_ the precondition is:  
\(n?\
otin\text{dom}\;\textit{balances}\)  
while its postcondition is:  
\(\textit{balances}^{\prime}=\textit{balances}\cup\{n?\)\(\mapsto\)\(0\}\)  
Therefore, _NewClientOk_ does not say what the system shall do when \(n?\
otin\text{dom}\;\textit{balances}\) does not hold. The bank says that nothing has to be done when the account number chosen by the clerk is already in use. Then, we define a new schema for this case:  
\(\textit{AccountAlreadyExists}==\)  
\([\Xi\textit{Bank};\;n? :\textit{ACCNUM}\;|\;n?\in\text{dom}\;\textit{balances}]\)  
This is another way of writing schemas, called horizontal form. It has the same meaning than:  
\(\textit{AccountAlreadyExists}\)  
\(\Xi\textit{Bank}\)  
\(n? :\textit{ACCNUM}\)  
\(n?\in\text{dom}\;\textit{balances}\)  
\(\Xi\textit{Bank}\)  
\(\Delta\textit{Bank}\)  
\(\textit{balances}^{\prime}=\textit{balances}\)  
If a \(\Xi\) expression is included in an operation schema, it means that the operation will not produce a state change because all the primed state variables are equal to their unprimed counterparts. When a schema whose predicate part is not empty is included in another schema, the net effect is twofold: (a) the declaration part of the former is included in the declaration part of the latter; and (b) the predicate of the former is conjoined to the predicate of the latter. Hence, _AccountAlreadyExists_ could have been written as follows:  
\(\textit{AccountAlreadyExists}\)  
\(\textit{balances},\textit{balances}^{\prime}:\textit{ACCNUM}\)  
\(n?