%!TeX root = main.tex
               
\knowledge{notion}
    | intersecting
	| intersecting family
	| intersecting families
\knowledge{notion}
	| chain
	| chains
\knowledge{notion}
	| anti-chain
	| anti-chains
\knowledge{notion}
	| \BArgs
	| \BArgs*\varphi
\knowledge{notion}
	| \EArgs
	| \EArgs*\varphi
\knowledge{notion}
	| $\varphi$-profile
	| $\varphi$-profiles
	| profile
	| profiles
\knowledge{notion}
	| \leftDeltaIntervals
	| \leftDeltaIntervals*
	| \leftDeltaIntervals{i}
	| \leftDeltaIntervals*{i}
\knowledge{notion}
	| \rightDeltaIntervals
	| \rightDeltaIntervals*
	| \rightDeltaIntervals{i}
	| \rightDeltaIntervals*{i}
\knowledge{notion}
	| special $\hsB*$-witness of $\alpha$ at $i$
	| special $\hsB*$-witness
	| special $\hsB*$-witnesses
	| special $\hsX*$-witness
	| special $\hsX*$-witnesses
	| special witness
	| special witnesses
	| Special witnesses
\knowledge{notion}
	| special $\hsE*$-witness of $\alpha$ at $i$
	| special $\hsE*$-witness
	| special $\hsE*$-witnesses
	| Special $\hsE*$-witnesses
\knowledge{notion}
    | \dec
    | \dec*{\varphi}
\knowledge{notion}
    | \enc
    | \enc*{\varphi}



\subsection{Encoding of minimal witnessing intervals}
\label{subsec:intersecting-families}


Example \ref{ex:overlapping} brings up a third ingredient 
that is crucial for the "normalization" procedure,
as it suggests that, in order to mark without ambiguities 
the endpoints of "prefix-minimal" 
(resp., "suffix-minimal") intervals for a formula $\varphi$,
one must first bound the number of distinct right (resp., left) 
endpoints of overlapping intervals. 
A bound will be shown precisely in 
Corollary~\ref{cor:core-bound-i} below.

\begin{definition}\label{def:intersecting-family}
A set $\cI$ of intervals is an ""intersecting family"" 
if there is a point $x$ that is contained in every interval of $\cI$.
\end{definition}

An example of an "intersecting family" of intervals
is shown to the left of Figure \ref{fig:chain-antichain}.

Towards proving the desired bound,
%a proof of Corollary \ref{cor:core-bound-i}, 
we shall first establish two auxiliary lemmas.
The first lemma relates the maximum 
cardinality of a partially ordered set
(e.g., an "intersecting family" of intervals,
partially ordered by containment) to the maximum 
cardinality of its "chains" and "anti-chains".
\AP
Formally, a ""chain"" of a partially ordered set 
is a subset of pairwise comparable elements.
\AP
An ""anti-chain"" is a subset of pairwise 
incomparable elements. 
The first lemma is in fact a rephrasing of 
Dilworth's theorem~\cite{dilworth50} 
(we give a proof here for self-containment):


\begin{figure*}[t]
\centering
\begin{tikzpicture}[scale=0.9]
\begin{scope}[xshift=0]
\draw [|-|] (-2.5,0) -- (1,0);
\draw [|-|] (-1,-0.5) -- (2.5,-0.5);
\draw (0,-1) node {$\vdots$};
\draw [|-|] (-2,-1.5) -- (2,-1.5);
\draw [|-|] (-1.5,-2) -- (1.5,-2);
\end{scope}
\begin{scope}[xshift=180]
\draw [|-|] (-0.5,0) -- (0.5,0);
\fill [pattern color=nicered, pattern=north west lines] 
      (-0.5,-0.15) rectangle (-1,-0.35);
\fill [pattern color=nicered, pattern=north west lines] 
      (0.5,-0.15) rectangle (1,-0.35);
\draw [|-|] (-1,-0.5) -- (1,-0.5);
\draw (0,-1) node {$\vdots$};
\draw [|-|] (-2,-1.5) -- (2,-1.5);
\fill [pattern color=nicered, pattern=north west lines] 
      (-2,-1.65) rectangle (-2.5,-1.85);
\fill [pattern color=nicered, pattern=north west lines] 
      (2,-1.65) rectangle (2.5,-1.85);
\draw [|-|] (-2.5,-2) -- (2.5,-2);
\end{scope}
\begin{scope}[xshift=360]
\draw [|-|] (-2.5,0) -- (0.5,0);
\fill [pattern color=nicered, pattern=north west lines] 
      (-2.5,-0.15) rectangle (-2,-0.35);
\fill [pattern color=nicered, pattern=north west lines] 
      (0.5,-0.15) rectangle (1,-0.35);
\draw [|-|] (-2,-0.5) -- (1,-0.5);
\draw (0,-1) node {$\vdots$};
\draw [|-|] (-1,-1.5) -- (2,-1.5);
\draw [|-|] (-0.5,-2) -- (2.5,-2);
\fill [pattern color=nicered, pattern=north west lines] 
      (-1,-1.65) rectangle (-0.5,-1.85);
\fill [pattern color=nicered, pattern=north west lines] 
      (2,-1.65) rectangle (2.5,-1.85);
\end{scope}
\end{tikzpicture}
\\[5ex]
%\includegraphics[scale=0.63]{figures/intersecting-family.pdf}\hfill
%\includegraphics[scale=0.63]{figures/chain.pdf}\hfill
%\includegraphics[scale=0.63]{figures/antichain.pdf}
\caption{From left to right: an "intersecting family" of intervals, a "chain", and an "anti-chain".}
\label{fig:chain-antichain}
\end{figure*}


\begin{lemma}\label{lem:chain-antichain}
Let $X$ be a partially ordered set and suppose that
all its "chains" and "anti-chains" have cardinality
at most $n$. Then the cardinality of $X$ is at most $n^2$.
\end{lemma}

\begin{proof}
To begin with, notice that $X$ is well-founded, due to the 
hypothesis that "chains" have cardinality at most $n$.
Define the partition $Y_1,Y_2, \ldots$ of $X$, where each
$Y_i$ contains all and only the \emph{minimal} elements of
$X \setminus \bigcup_{j<i} Y_j$ --- in particular, each $Y_i$ 
is defined inductively on the basis of the previous sets 
$Y_1,\dots,Y_{i-1}$.
By construction, every subset $Y_i$ is an "anti-chain",
and hence, by the hypotheses of the claim, it has cardinality
at most $n$. 

Let us now bound by $n$ the number of subsets of the partition.
Towards a contradiction, assume that $Y_1,Y_2,\dots,Y_{n+1}$ 
belong to the partition of $X$.
By construction, for every $1<i\le n+1$ and every $y\in Y_i$, 
there is $y'\in Y_{i-1}$ such that $y'<y$ 
(otherwise $y$ should have been added to $Y_{i-1}$).
Using this property and a simple induction, we can construct 
a "chain" of length $n+1$: we start by taking an arbitrary $y_{n+1}\in Y_{n+1}$
and then we repeatedly use the property to prepend to a "chain"
$y_i < y_{i+1} < \dots < y_{n+1}$, with $i>1$, 
$y_i\in Y_i$, $y_{i+1}\in Y_{i+1}$, \dots, $y_{n+1}\in Y_{n+1}$,
a new element $y_{i-1} < y_i$, with $y_{i-1}\in Y_{i-1}$.
Clearly, such a "chain" of length $n+1$ leads to a 
contradiction, and hence the partition $Y_1, Y_2, \ldots$ 
of $X$ contains at most $n$ elements.
We conclude that $|X| = \sum_{i}|Y_i|\le  n^2$.
\end{proof}


Ultimately, we aim at applying Lemma~\ref{lem:chain-antichain} 
to bound the cardinality of every "intersecting family" of 
"prefix-minimal" (resp., "suffix-minimal") intervals with 
pairwise distinct right (resp., left) endpoints, 
using the containment relation as partial order.
To this end, it is crucial to bound the cardinalities of 
the "chains" and "anti-chains" of such an "intersecting family".
It will be also convenient to avoid singleton intervals 
when reasoning about "intersecting families" 
(note that there is at most one singleton interval 
in every "intersecting family").

\begin{lemma}\label{lem:chain-bound}
Let $\cS$ be an "interval structure", 
$\varphi$ a $\BEpi$ formula, 
$\cI$ an "intersecting family" of non-singleton "prefix-minimal" 
(resp., "suffix-minimal") intervals for $\varphi$, 
with pairwise distinct right (resp., left) endpoints, 
and $\cI'$ a "chain" or an "anti-chain" of $\cI$, 
where the partial order is given by containment. 
We have that
%
\begin{equation}\label{eq:bound}
  |\cI'| ~\le~ 2^{2|\varphi|}.
\end{equation}
\end{lemma}


\begin{proof}
We present the proof for an "intersecting family" 
of non-singleton \emph{"prefix-minimal"} intervals for $\varphi$ 
(the case of "suffix-minimal" intervals uses symmetric arguments).
Towards a contradiction, assume that there exist 
a $\BEpi$ formula $\varphi$, 
an "intersecting family" 
$\cI$ of non-singleton "prefix-minimal" intervals for
$\varphi$ with pairwise distinct right endpoints, 
and a subset $\cI'$ of $\cI$ that is a "chain" or an 
"anti-chain" and that violates the bound \eqref{eq:bound}, 
i.e., $\cI'$ contains more than $2^{2|\varphi|}$ intervals.
We also assume, without loss of generality, that 
$\varphi$ is a smallest formula witnessing this 
violation of the bound
(later we will exploit this 
assumption when considering families of "prefix-minimal" 
intervals for subformulas of $\varphi$).

\AP
Let $""\BArgs*\varphi""$ (resp., $""\EArgs*\varphi""$) be
the set of formulas $\alpha$ such that $\hsB\alpha$ (resp., $\hsE\alpha$) is
a subformula of $\varphi$ with no other modal operator above it.
For example, if $\varphi = \hsB\alpha_1 \:\wedge\: \hsB\hsB\alpha_2 \:\wedge\: \hsE\hsB\alpha_3$,
then $\BArgs\varphi = \{\alpha_1,\hsB\alpha_2\}$ and $\EArgs = \{\hsB\alpha_3\}$.
Note that $|\varphi| \geq |\BArgs\varphi| + |\EArgs\varphi|$.

\AP
Define the ""$\varphi$-profile"" of a non-singleton interval 
$I$ as the pair $(B,E)$, where $B$ (resp., $E$) is the set 
of formulas $\alpha\in\BArgs{\varphi}$
(resp., $\alpha\in\EArgs{\varphi}$) that "hold at" 
"prefixes" (resp., "suffixes") of $I$. 
Note that any two non-singleton intervals 
with the same "$\varphi$-profile" 
either both "satisfy@holds at" $\varphi$ 
or both "satisfy@holds at" $\neg\varphi$;
in particular, this holds thanks to the 
fact that $\varphi$ is in "homogeneous normal form".

We also observe that 
there are at most $2^{|\BArgs{\varphi}| + |\EArgs{\varphi}|}$ 
distinct "$\varphi$-profiles". 
Therefore, by our assumption on $\cI'$, there are
\[
  n ~>~ 2^{2|\varphi| - |\BArgs{\varphi}| - |\EArgs{\varphi}|}
\]
intervals $I_1,\dots,I_n \in \cI'$ with the same $\varphi$-profile.
Without loss of generality, assume that the intervals $I_1,\dots,I_n$ 
are listed based on the natural ordering of their right endpoints, 
that is, $\max(I_1) < \dots < \max(I_n)$.
Depending on $\cI'$ being a "chain" or an "anti-chain", 
the left endpoints of these intervals are also ordered, 
in descending, resp., ascending order
(see Figure \ref{fig:chain-antichain}).

For the rest of the proof, unless otherwise stated, 
$i$ will denote a natural number from $1$ to $n-1$, and will 
be used in particular to index pairs of consecutive 
intervals, say $I_i$ and $I_{i+1}$.
\AP
For every $i$, let
$w_i < x_i \leq y_i < z_i$ be the four endpoints of $I_i$ and $I_{i+1}$.
Further, let $""\leftDeltaIntervals*{i}"" = [w_i+1,x_i]$ and
$""\rightDeltaIntervals*{i}"" = [y_i,z_i-1]$ (these intervals are represented 
by the red dashed rectangles in Figure \ref{fig:chain-antichain}).
Thanks to the fact that $\cI'$ is a "chain" or an "anti-chain", 
the $\leftDeltaIntervals{i}$'s and the $\rightDeltaIntervals{i}$'s 
are pairwise disjoint across all $i$ 
(this property will be used later and is the main reason 
for restricting our attention to "chains" and "anti-chains").

\AP
Given $\alpha\in\BArgs{\varphi}$ and $1\le i<n$, 
a ""special $\hsB*$-witness of $\alpha$ at $i$"" (if it exists)
is the "prefix-minimal" interval for $\alpha$ that has the 
same left endpoint as $I_{i+1}$ and whose right endpoint belongs to $\rightDeltaIntervals{i}$.
Figure \ref{fig:special-witnesses} gives two examples
of "special $\hsB*$-witnesses", represented by green brackets:
one example is for the "chain" arrangement and the other
is for the "anti-chain" arrangement.
\AP
Symmetrically, given $\alpha\in\EArgs{\varphi}$ and $1\le i<n$,
a ""special $\hsE*$-witness of $\alpha$ at $i$"" (if it exists) is the "suffix-minimal"
interval for $\alpha$ that has the same right endpoint as $I_i$ and whose 
 left endpoint belongs to $\leftDeltaIntervals{i}$.
"Special $\hsE*$-witnesses" are represented in Figure
\ref{fig:special-witnesses} by blue brackets.

Now, we tag an index $1\le i<n$ with a pair $(B,\alpha)$
(resp., $(E,\alpha)$) whenever
$\alpha\in\BArgs{\varphi}$ (resp., $\alpha\in\EArgs{\varphi}$) and
there is a "special $\hsB*$-witness" (resp., "$\hsE*$-witness@special $\hsE*$-witness") 
of $\alpha$ at $i$.
If there is no "special witness" for any $\alpha$, 
then we tag $i$ with the symbol $\bot$.
Let $K_i = [\min(I_{i+1}),\max(I_i)]$ and observe
that $K_i$ is a \emph{proper "prefix"} of $I_{i+1}$.
We will prove that, for some index $i$, the interval 
$K_i$ "satisfies@holds at" $\varphi$, thus contradicting 
"prefix-minimality" of $I_{i+1}$.
Towards this, it will be sufficient to find an 
index $i$ tagged with $\bot$. 
Indeed, if this happens, then we claim that 


\begin{figure*}[t!]
\centering
\begin{tikzpicture}[scale=0.95]
\begin{scope}
\coordinate (A) at (1,0);
\coordinate (B) at (2,0);
\coordinate (C) at (4,0);
\coordinate (D) at (0,-0.75);
\coordinate (E) at (5,-0.75);
\coordinate (F) at (6,-0.75);
%
\draw [|-|] (B) -- (C);
\draw [|-|] (D) -- (F);
%
\draw [nicecyan, above round brace] ([yshift=7] A) -- ([yshift=7] C)
      node [above=-0.1, midway, yshift=8] {$\alpha$};
\draw [nicegreen, below round brace] ([yshift=-7] D) -- ([yshift=-7] E)
      node [below=-0.1, midway, yshift=-8] {$\alpha$};
%
\fill [pattern color=nicered, pattern=north west lines] 
      ([yshift=-7] B) rectangle ([yshift=7] D);
\fill [pattern color=nicered, pattern=north west lines] 
      ([yshift=-7] C) rectangle ([yshift=7] F);
%      
\draw (-1,0) node {$I_i$};
\draw (-1,-1) node {$I_{i+1}$};
\end{scope}
%
\begin{scope}[xshift=260]
\coordinate (A) at (0,0);
\coordinate (B) at (1,0);
\coordinate (C) at (4,0);
\coordinate (D) at (2,-0.75);
\coordinate (E) at (5,-0.75);
\coordinate (F) at (6,-0.75);
%
\draw [|-|] (A) -- (C);
\draw [|-|] (D) -- (F);
%
\draw [nicecyan, above round brace] ([yshift=7] B) -- ([yshift=7] C)
      node [above, midway, yshift=8] {$\alpha$};
\draw [nicegreen, below round brace] ([yshift=-7] D) -- ([yshift=-7] E)
      node [below, midway, yshift=-8] {$\alpha$};
%
\fill [pattern color=nicered, pattern=north west lines] 
      ([yshift=-7] A) rectangle ([yshift=7] D);
\fill [pattern color=nicered, pattern=north west lines] 
      ([yshift=-7] C) rectangle ([yshift=7] F);
%      
\draw (-1,0) node {$I_i$};
\draw (-1,-1) node {$I_{i+1}$};
\end{scope}
\end{tikzpicture}
%\includegraphics[scale=0.8]{figures/chain-witness.pdf}\hfill
%\includegraphics[scale=0.8]{figures/antichain-witness.pdf}
\caption{"Special witnesses" in a "chain" (left) 
and in an "anti-chain" (right).}
\label{fig:special-witnesses}
\end{figure*}


\begin{claim}
Every formula 
$\alpha\in\BArgs{\varphi}$ (resp., $\alpha\in\EArgs{\varphi}$) 
that "holds at" a "prefix" (resp., "suffix") of $I_i$ also 
"holds at" a "prefix" (resp., "suffix") of $K_{i}$, and 
vice versa. 
\end{claim}

The above claim would then imply that the 
"$\varphi$-profile" of $K_i$ coincides with 
that of $I_i$, and hence $K_i\models\varphi$.

\begin{proof}[Proof of the claim]
%To prove the claim, 
Assume that index $i$ is tagged with $\bot$.
Consider some $\alpha\in\BArgs{\varphi}$.
If $\alpha$ "holds at" a "prefix" of $I_i$, 
then $\alpha$ "holds at" some "prefix"
of $I_{i+1}$ as well, because $I_i$ and $I_{i+1}$ 
have the same "$\varphi$-profile".
Let $J$ be the smallest "prefix" of $I_{i+1}$ 
that "satisfies@holds at" $\alpha$.
Due to $i$ being tagged with $\bot$, we have that 
$\max(J) < \max(I_i) = \max(K_i)$, meaning that 
$J$ is also a "prefix" of $K_i$.
Conversely, if $\alpha$ "holds at" a "prefix" of $K_i$, 
then it trivially "holds at" a "prefix" of $I_{i+1}$ as well, 
and thus it "holds at" a "prefix" of $I_{i}$, too,
because $I_i$ and $I_{i+1}$ have the same "$\varphi$-profile".
Next, consider some $\alpha\in\EArgs{\varphi}$.
If $\alpha$ "holds at" some "suffix" of $I_i$, then let $J$ be the smallest "suffix" of $I_{i}$ that "satisfies@holds at" $\alpha$.
Due to $i$ being tagged with $\bot$, 
we have that $\min(J) > \min(I_{i+1}) = \min(K_i)$, 
meaning that $J$ is also a "suffix" of $K_i$.
Conversely, assume that $\alpha$ "holds at" some 
"suffix" of $K_i$ and let $J$ be the smallest "suffix" 
of $K_{i}$ that "satisfies@holds at" $\alpha$.
Once again, since $i$ is tagged with $\bot$, 
we have that $\min(J) > \min(I_{i})$, meaning 
that $J$ is a "suffix" of $I_i$, too.
\end{proof}
%
%This completes the proof of the claim.

It remains to prove that at least one index $i$ is tagged with $\bot$.
For this, we bound the number of indices tagged with pairs of the form 
$(X,\alpha)$, with $X=B$ (resp., $X=E$) and $\alpha\in\XArgs{\varphi}$.
By construction, for each tag $(X,\alpha)$, the 
"special $\hsX*$-witnesses" of $\alpha$ form an 
"intersecting" ("anti@anti-chain"-)"chain" $\cI_{X,\alpha}$ of
"prefix-minimal" (resp., "suffix-minimal") 
intervals for $\alpha$. 
Moreover, we know that:
\begin{itemize}
\item All intervals in $\cI_{X,\alpha}$ are non-singleton.

      This is because the only scenario where a 
      \emph{singleton} "special $\hsX*$-witness" arises is when 
      $\cI'$ is "anti-chain", $n=2$, and $\max(I_1) = \min(I_2)$.
      This scenario is however excluded by the fact that
      $n > 2^{2|\varphi| - |\BArgs{\varphi}| - |\EArgs{\varphi}|} \ge 2$.
%
\item The intervals in $\cI_{X,\alpha}$ have pairwise distinct
      right (resp., left) endpoints.
      
	  This is because those endpoints belong to
	  the intervals $\rightDeltaIntervals{i}$
	  (resp., $\leftDeltaIntervals{i}$), which
	  are pairwise disjoint across all $i$'s.
%
\item The cardinality of each ("anti@anti-chain"-)"chain" 
      $\cI_{X,\alpha}$ is at most $2^{2|\alpha|}$.

      This is thanks to the previous properties and because 
      $\alpha$ is a proper subformula of $\varphi$, which 
      was assumed to be a smallest formula violating 
      the bound \eqref{eq:bound}.
\end{itemize}
In view of the last property, we derive that the number
of indices that are \emph{not} tagged with $\bot$ is 
\begin{align*}
  n' &~\le~ \sum\nolimits_{\alpha\in\BArgs{\varphi}} 2^{2|\alpha|} 
            ~+~ 
            \sum\nolimits_{\alpha\in\EArgs{\varphi}} 2^{2|\alpha|}
  \\
     &~\le~ 2^{\sum_{\alpha\in\BArgs{\varphi}} 2|\alpha| \:+\: 
               \sum_{\alpha\in\EArgs{\varphi}} 2|\alpha| } \ ,
\end{align*}
where the last inequality follows from  majorating sums with products.
Next, recall that
$n > 2^{2|\varphi| - |\BArgs{\varphi}| - |\EArgs{\varphi}|}$,
and hence the number of indices $1\le i<n$ that are tagged 
with $\bot$ is
\[
  n - 1 - n' 
  ~\ge~ 2^{2|\varphi| - |\BArgs{\varphi}| - |\EArgs{\varphi}|}
        ~-~
        2^{\sum_{\alpha\in\BArgs{\varphi}} 2|\alpha| \:+\: 
           \sum_{\alpha\in\EArgs{\varphi}} 2|\alpha|} \ .
\]
We prove that the right hand-side number is always positive 
by showing that 
$2|\varphi| - |\BArgs{\varphi}| - |\EArgs{\varphi}| 
 > 
 \sum_{\alpha\in\BArgs{\varphi}} 2|\alpha| \:+\: 
 \sum_{\alpha\in\EArgs{\varphi}} 2|\alpha|$.
We distinguish two cases, depending on whether
or not $\varphi$ contains modal operators.
If $\varphi$ contains no modal operators, then
$2|\varphi| - |\BArgs{\varphi}| - |\EArgs{\varphi}| 
 = 2|\varphi| 
 > 0
 = \sum_{\alpha\in\BArgs{\varphi}} 2|\alpha| \:+\: 
   \sum_{\alpha\in\EArgs{\varphi}} 2|\alpha|$.
Otherwise, if $\varphi$ contains at least one modal 
operator, then we observe that \emph{(i)} the size of $\varphi$
is at least the sum of the sizes of the subformulas 
$\hsX\alpha$, for $X \in \{ B, E \}$ and $\alpha\in\XArgs{\varphi}$,
which are $|\hsX\alpha| = |\alpha| + 1$,
and \emph{(ii)}
$\sum_{\alpha\in\XArgs{\varphi}}(|\alpha| + 1) = 
 \big(\sum_{\alpha\in\XArgs{\varphi}}|\alpha|\big) + |\XArgs{\varphi}|$, for $X \in \{ B, E \}$.
From this we derive:
\begin{align*}
  & 2|\varphi| - |\BArgs{\varphi}| - |\EArgs{\varphi}|
  \\[1ex]
  \ge~ &\sum\nolimits_{\alpha\in\BArgs{\varphi}} 2|\alpha| 
        ~+~
        \sum\nolimits_{\alpha\in\EArgs{\varphi}} 2|\alpha|
        ~+~
        |\BArgs{\varphi}| ~+~ |\EArgs{\varphi}| 
  \\[1ex]
  >~  &\sum\nolimits_{\alpha\in\BArgs{\varphi}} 2|\alpha| 
        ~+~
        \sum\nolimits_{\alpha\in\EArgs{\varphi}} 2|\alpha| \ .
\end{align*}
We have just shown that at least one index $i$ 
must be tagged with $\bot$, which completes the proof
of the lemma.
\end{proof}



Putting together Lemmas \ref{lem:chain-antichain}
and \ref{lem:chain-bound}, we obtain the desired bound
for an arbitrary "intersecting family" of non-singleton
"prefix@prefix-minimal"/"suffix-minimal" intervals for 
$\varphi$:

%\AP
%For the sake of brevity, we denote by
%$""\LeftEndpoints*(\cI)""$ (resp., $""\RightEndpoints*(\cI)""$) 
%the set of all left (resp., right) endpoints of intervals from an "intersecting family" $\cI$.

\begin{restatable}{corollary}{CoreBoundCorollaryI}
\label{cor:core-bound-i}
Let $\cS$ be an "interval structure", 
$\varphi$ a $\BEpi$ formula, 
and $\cI$ an "intersecting family" of non-singleton 
"prefix-minimal" (resp., "suffix-minimal") intervals 
for $\varphi$. 
Then the number of distinct right (resp., left) endpoints
of intervals of $\cI$ is at most $2^{4|\varphi|}$.
%$\RightEndpoints(\cI)$ (resp., $\LeftEndpoints(\cI)$)
%has cardinality at most $2^{4|\varphi|}$.
\end{restatable}

We conclude this part by showing how "prefix-minimal" intervals
for $\varphi$ can be characterized using fresh 
propositional letters
and suitable formulas $\dec{\varphi}$ and $\enc{\varphi}$ 
(a similar corollary can be stated for "suffix-minimal" intervals).

\begin{restatable}{corollary}{CoreBoundCorollaryII}
\label{cor:core-bound-ii}
Consider a $\BEpi$ formula $\varphi$ 
over a "signature" $\signature$
and let $\signature' = \signature \uplus\{p_1,\dots,p_m,\ell,r,s\}$,
where $p_1,\dots,p_m$, $\ell,r,s$ are fresh propositional letters
and $m=4|\varphi|$ (this $m$ is precisely the exponent appearing 
in the bound of Corollary \ref{cor:core-bound-i}).
\AP
Define the $\BEpi$ formulas%
\footnote{Note that, despite the notation, 
          the formula $\dec{\varphi}$ only depends 
          on the signature and the size of $\varphi$,
          whereas $\enc{\varphi}$ depends entirely on $\varphi$.}
\begin{align*}
  ""\dec*{\varphi}"" 
  &~=~~ \Big( \hsB(\pi\wedge\ell) ~\wedge~ \hsE(\pi\wedge r) 
        ~\wedge~ \\[-1ex]
  &~~~~ \phantom{\Big(} ~~ \bigwedge\nolimits_{i=1,\dots,m} \big(\hsB(\pi\wedge p_i) \iff 
                                                \hsE(\pi\wedge p_i)\big) \Big) \\
  &~\vee~~ (\pi \wedge s) 
%  \numberthis
%  \label{eq:decoding}
  \\[2ex]
  ""\enc*{\varphi}""
%  &~=~~ \underbrace{\neg(\pi \wedge \ell \wedge r) 
%                    \,\wedge\, 
%                    \neg(\pi \wedge \ell \wedge s) 
%                    \,\wedge\, 
%                    \neg(\pi \wedge r \wedge s)}%
%        _{\midward{\text{\scriptsize$\ell,r,s$ are in mutual exclusion}}} \\[1ex]
  &~=~~ 
%  &~\wedge~~ 
  \underbrace{\big(\dec{\varphi} \wedge \neg\hsB\dec{\varphi} ~\rightarrow~ \varphi \big)}%
             _{\midward{\text{\scriptsize\qquad\qquad\quad
                                         prefix-minimial intervals for $\dec{\varphi}$ satisfy $\varphi$}}}  \\[1ex]
  &~\wedge~~ 
  \underbrace{\big(\varphi \wedge \neg\hsB\dec{\varphi} ~\rightarrow~ \dec{\varphi} \big)}%
             _{\midward{\text{\scriptsize\qquad\qquad\quad 
                                         prefix-minimal intervals for $\varphi$ satisfy $\dec{\varphi}$}}}
%  \numberthis
%  \label{eq:encoding}
\end{align*}
We have that $\enc{\varphi}$ is an "expander" from 
$\signature$ to $\signature'$
and that $\hsB\varphi$ and $\hsB\dec{\varphi}$ are 
"equivalent" over all "interval structures" that make 
$\enc{\varphi}$ "valid@valid over".
\end{restatable}

\begin{proof}
Let us first explain the intended use of the fresh propositional
letters $p_1,\dots,p_m$, $\ell,r,s$.
The letters $p_1,\dots,p_m$ will annotate points of an 
"interval structure" with $m$-tuples of bits, thus enumerating
an exponentially-large set (e.g.,~$\{1,\dots,2^m\}$). 
More precisely, the left and right endpoints of every non-singleton 
"prefix-minimal" interval for $\varphi$ will be identified by having 
labels $\ell$ and $r$, respectively, and the same $m$-tuple of bits 
--- this correlation between endpoints is checked by the first disjunct 
of $\dec{\varphi}$.
Singleton "prefix-minimal" intervals for $\varphi$ will instead be 
identified by the special label $s$ --- this is checked in the second
disjunct of $\dec{\varphi}$.
%
% The remaining points will have none of the labels $\ell,r,s$.
%
Another important constraint is that every two intersecting intervals 
that are non-singleton, "prefix-minimal" for $\gamma$, and not a 
"suffix" one of another will have their endpoints marked by different 
$m$-tuples of bits.

Corollary \ref{cor:core-bound-i} guarantees the existence 
of an annotation satisfying all the above constraints.
Such an annotation is enforced precisely by the formula $\enc{\varphi}$,
which turns out to be an "expander" from $\signature$ to $\signature'$
(namely, every "interval structure" over $\signature$ admits an 
"expansion" over $\signature'$ that makes $\enc{\varphi}$ "valid@valid over").
%
Moreover, if the annotation is correct, namely, if 
$\enc{\varphi}$ is "valid over" an expanded "interval structure",
then every "prefix-minimal" interval for $\varphi$ is also 
a "prefix-minimal" interval for $\dec{\varphi}$, and vice versa.
Note that there may still exist intervals that "satisfy" 
$\varphi$ but not $\dec{\varphi}$, or vice versa; however,
those intervals will always contain proper "prefixes" that
"satisfy" both $\varphi$ and $\dec{\varphi}$.
Overall, this proves that the two formulas $\hsB\varphi$ 
and $\hsB\dec{\varphi}$ are "equivalent" over
expanded "interval structures" that make $\enc{\varphi}$
"valid@valid over".
\end{proof}


%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End: