Skip to content

Commit

Permalink
and a few more typos
Browse files Browse the repository at this point in the history
thanks Matt
  • Loading branch information
rzach committed Apr 25, 2018
1 parent ef71e65 commit 7553196
Show file tree
Hide file tree
Showing 2 changed files with 10 additions and 6 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -81,9 +81,13 @@
$\mSat{M}{!B \cif !C}[w]$ iff either
\begin{enumerate}
\item\ollabel{sphere-vac} For all $u \in \bigcup O_w$, $\mSat/{M}{!C}[u]$, or
\item\ollabel{sphere-nonvac} For some $S \in O_w$ and some $u \in
S$, $\mSat{M}{!B}[u]$ and for all $v \in S$, either
$\mSat/{M}{!B}[u]$ or $\mSat{M}{!C}[u]$.
\item\ollabel{sphere-nonvac} For some $S \in O_w$,
\begin{enumerate}
\item $\mSat{M}{!B}[u]$ for some $u \in
S$, and
\item for all $v \in S$, either
$\mSat/{M}{!B}[v]$ or $\mSat{M}{!C}[v]$.
\end{enumerate}
\end{enumerate}
\end{defn}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@
variables are $p_1$, \dots, $p_n$, and let $!D_1$, \dots,
$!D_n$ be modal !!{formula}s. Then for any assignment $\pAssign{v}$,
any model $\mModel{M} = \tuple{W, R, V}$, and any $w \in W$ such
that $v(p_i) = \True$ if and only if $\mSat{M}{!D_i}[w]$ we have
that $\pAssign{v}(p_i) = \True$ if and only if $\mSat{M}{!D_i}[w]$ we have
that $\pSat{v}{!A}$ if and only if
$\mSat{M}{\SSubst{!A}{\subst{!D_1}{p_1}, \dots,
\subst{!D_n}{p_n}}}[w]$.
Expand All @@ -51,7 +51,7 @@
and $\mSat{M}{\ltrue}[w]$}.}{}
\item \indcase{!A}{p_i}{%
\begin{align*}
\pSat{v}{p_i} \Leftrightarrow {} & v(p_i) = \True &&
\pSat{v}{p_i} \Leftrightarrow {} & \pAssign{v}(p_i) = \True &&
\text{by definition of $\pSat{v}{p_i}$};\\
\Leftrightarrow {} & \mSat{M}{!D_i}[w] && \text{by assumption}\\
\Leftrightarrow {} & \mSat{M}{\SSubst{p_i}{\subst{!D_1}{p_1}, \dots,
Expand All @@ -61,7 +61,7 @@
\end{align*}}
\tagitem{prvFalse}{\indcase{!A}{\lnot !B}{%
\begin{align*}
\pSat{v}{\lnot !B} \Leftrightarrow & \pSat/{v}{!B}
\pSat{v}{\lnot !B} \Leftrightarrow {} & \pSat/{v}{!B}
&& \text{by definition of $\pSat{v}{}$};\\
\Leftrightarrow {} & \mSat/{M}{\SSubst{!B}{\subst{!D_1}{p_1}, \dots,
\subst{!D_n}{p_n}}}[w] && \text{by induction hypothesis};\\
Expand Down

0 comments on commit 7553196

Please sign in to comment.