%!TeX root = main.tex
      
\knowledge{notion}
	| expansion
	| expanded
\knowledge{notion}
	| expander
	| expanders
         

\subsection{Expanders}\label{subsec:expanders}

A first ingredient of the "normalization" procedure 
of $\BEpi$ formulas is 
that of an "expander". Intuitively, this is a formula that constrains 
new propositional letters on the basis of the old ones in an arbitrary 
("homogeneous") "interval structure". 
%and that preserves "satisfiability" 
%when conjoined with any other formula over the original "signature".

\begin{definition}\label{def:expander}
Let $\signature\subseteq\signaturebis$ be two "signatures", and 
let $\cS=\intervalstructure$ and $\cS'=\intervalstructurebis$ be 
"interval structures" over $\signature$ and $\signaturebis$, respectively.
We say that $\cS'$ is an ""expansion"" of $\cS$ if $\timedomainbis=\timedomain$ and 
$\sigma'(I)\cap\signature=\sigma(I)$ for all intervals $I\in\intervaldomain$.

\AP
An ""expander"" from $\signature$ to $\signaturebis$
is a $\BEpi$ formula $\xi$ over $\signaturebis$ such that,
for every "interval structure" $\cS$ over $\signature$, 
there is an "expansion" $\cS'$ of $\cS$ over $\signaturebis$ 
that makes $\xi$ "valid@valid over".
\end{definition}

We report below a simple lemma about expanders.

\begin{restatable}{lemma}{ExpanderEquivalence}
\label{lem:expander-equivalence}
If $\xi$ is an "expander" from $\signature$ to $\signaturebis$,
$\psi$ and $\psi'$ are formulas over the "signatures" 
$\signature$ and $\signaturebis$, respectively, and
$\psi,\psi'$ are "equivalent" over all "interval structures" 
where $\xi$ is "valid@valid over",
then $\psi$ and $\psi' \wedge \hsGu\xi$ are "equi-satisfiable".
\end{restatable}

\begin{proof}
Suppose that $\psi' \wedge \hsGu\xi$ is "satisfied by" 
an "interval structure" $\cS'$ over $\signaturebis$.
Because, $\xi$ is "valid over" $\cS'$, $\psi$ is
"equivalent" to $\psi'$ over $\cS'$, and hence 
$\cS'$ "satisfies" $\psi$.
Conversely, if $\psi$ is "satisfied by" an "interval structure" 
$\cS$ over $\signature$, then there is an "expansion"
$\cS'$ of $\cS$ that makes 
$\xi$ "valid@valid over". 
This implies that $\psi$ and $\psi'$ are "equivalent"
over $\cS'$. Hence $\cS'$ "satisfies" $\psi'$, and
$\psi' \wedge \hsGu\xi$ as well.
\end{proof}


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