Commit 758f2cc2 authored by ehilin02's avatar ehilin02
Browse files

coNP upper bound

parent 38655c8d
......@@ -103,7 +103,7 @@ Because $\Pi$ fixes a total ordering, only one of the sub-cases
%% matchSeq
%%
\begin{figure}[tb]
\vspace{-2eX}
%\vspace{-2eX}
\begin{eqnarray}
\label{eq:mas-base}
\lefteqn{\mathtt{matchSeq}(\Pi, \bsepc_{i=1}^{m} a_i, b)
......@@ -196,7 +196,7 @@ In this situation, we will unfold $\hls{}(t'_1, t'_2; t'_3)$ and consider differ
%% splitAtom
%%
\begin{figure}[htb]
\vspace{-2eX}
%\vspace{-2eX}
\begin{eqnarray}
\label{eq:sa-blk}
\lefteqn{\mathtt{splitAtom}(k, \Pi, \bsepc_{i=1}^{k-1} a_i \sepc \blk(t_1',t_2') \sepc \bsepc_{i=k+1}^{m}a_{i}, b_1 \sepc \bsepc_{j=2}^{n} b_j)}
......
......@@ -195,6 +195,6 @@ From the proof of Proposition~\ref{prop-sat-correct}, we know that there are $h$
\input{entail-hls-one-atom.tex}
\vspace{-2mm}
%\vspace{-2mm}
\input{entail-hls-mult-atoms.tex}
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