Commit 1a5a10f0 authored by ehilin02's avatar ehilin02
Browse files

section 5.2

parent ed1f4619
......@@ -6,7 +6,7 @@
Using the arguments similar to the one given for the case $n=1$,
we simplify $\varphi\models_\preceq \psi$ with
$\varphi \equiv \Pi: a_1 \sepc \cdots \sepc a_m$ and
$\psi \equiv \Pi': b_1 \sepc \cdots \sepc b_n$ to:
$\psi \equiv \Pi': b_1 \sepc \cdots \sepc b_n$ to
%
\begin{align*}
C_\preceq \land \Pi: a_1 \sepc \cdots \sepc a_m \models_\preceq b_1\sepc \cdots \sepc b_n.
......
......@@ -191,7 +191,7 @@ a case analysis on the form of the first atom of the antecedent, $a_1$, follows.
\begin{align*}
{\sf Ufld}_{x', x''}(\hls{}(t''_1, t''_2; t''_3)) \triangleq\
& \hls{}(t''_1, x'; t''_3) \sepc x' \pto x''- x' \sepc \\
& \blk(x'+1, x'') \sepc \hls{}(x'', t''_2; t''_3),
& \blk(x'+1, x'') \sepc \hls{}(x'', t''_2; t''_3).
\end{align*}
%then $\varphi \models_\preceq \psi$ does not hold, since
% Indeed,
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment