diff options
Diffstat (limited to 'papers/3.tex')
| -rw-r--r-- | papers/3.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/papers/3.tex b/papers/3.tex index 6066649..84a52f1 100644 --- a/papers/3.tex +++ b/papers/3.tex @@ -205,7 +205,7 @@ $\forall x (Xx \ba x=y), Haec(X)(z) \wedge z \neq y \vdash Xy \ba y=y \\ \end{quote} Then, from $\vdash Haec(X)(y) \ra Tra(X)(y)$, we can observe that: \\ \begin{quote} -\begin{tabulary}{\textwidth}{Lr} +\begin{tabulary}{\textwidth}{LR} $\vdash \Box Haec(X)(y) \ra \Box Tra(X)(y)$ & (K) \\ $\vdash \Box \forall x (Xx \ba x=y) \ra \Box \Box \forall x (Xx \ba x=y)$ & (\textbf{4})\\ $\vdash Haec(X)(y) \ra \Box Haec(X)(y)$ & (Chaining conditionals) \\ @@ -214,7 +214,7 @@ $\vdash Haec(X)(y) \ra \Box Tra(X)(y)$ & \end{quote} \subsection{The proof for (o-Tracking)} \begin{quote} -\begin{tabulary}{\textwidth}{Lr} +\begin{tabulary}{\textwidth}{LR} $\vdash Haec(X)(o) \ra Tra(X)(o)$ & (Proved above) \\ $\vdash \exists X Haec(X)(o) \ra \exists X Tra(X)(o)$ & (Derivable from $\forall$ rule) \\ $\vdash \Box \exists X Haec(X)(o) \ra \Box \exists X Tra(X)(o)$ & (K)\\ |