this is for holding javascript data
Matthew Milano added subsubsection_i_First_direction_by__.tex
about 9 years ago
Commit id: fa3f9dae4eb65f2748d101bc5716ba35ce971ad6
deletions | additions
diff --git a/subsubsection_i_First_direction_by__.tex b/subsubsection_i_First_direction_by__.tex
new file mode 100644
index 0000000..7ae471c
--- /dev/null
+++ b/subsubsection_i_First_direction_by__.tex
...
\subsubsection*{i}
First direction: by contradiction. We assume that $(\I,r',m') \vDash \varphi$ for all points $(r',m')$ that are S-reachable from $(r,m)$ while $(\I,r,m) \vDash \neg C_S \varphi$.
As $(\I,r,m) \vDash \neg C_S \varphi$, by definition there exists some $k$ such that $(\I,r,m) \vDash \neg E^k_S \varphi$. Thus there also $\exists i \in S(r,m)$ s.t. $(\I,r,m) \vDash \neg B^S_i$, remember this $i$, we'll use it later. As $(\I,r,m) \vDash \neg B^S_i$, $\exists (r',m')$ s.t. $r_i(m) = r'_i(m')$ and $i \in S(r',m')$ where $(\I, r', m') \vDash \neg \varphi$. But $(r',m')$ is only one $i$-hop away from $(r,m)$, and is thus clearly $S$-reachable
