Q2.1 - We want to specify the Tokyo subway system, where (see figure) there are several lines ($L$), represented by different colours, whose stops ($P$) are numbered sequentially, and where stations ($E$) may include stops from different lines $-\!-$ e.g. the $\mathsf{Otemachi}$ station, which has stops $\fbox{$\frac C {11}$}$, $\fbox{$\frac M {18}$}$, etc. $-\!-$ allowing passengers to change lines.
Knowing that each stop is always associated with exactly one station, the simplified model
was defined, associating each stop with its line, number, and station. For example, if $p$ is the stop $\fbox{$\frac M {18}$}$ in the figure, then we have
$\begin{array}{l}st\ p = Otemachi\\\mathit{ln}\ p = M\\nr\ p = 18\end{array}$.
Clearly, the numbering system for stops on the lines requires the following invariant:
If $n+1$ is the number of a stop on a given line, then there is another stop on the same line numbered $n$.
Which of the following formulations of this invariant would you choose?
\begin{eqnarray} && \frac{nr}{succ \cdot nr} \subseteq \frac{ln}{ln} \label{eq:181128a} \\&& \nonumber\\&& \frac{nr}{succ} \subseteq nr \cdot \frac{ln}{ln} \end{eqnarray}where $succ\ n = n+1$ is the successor function on $\Nat$?
Convert each "magic square" into the equivalent logical expression and decide, providing justification.
$\Box$
