% TeX root = main.tex
\label{sec:apdx}

\begin{apdxlemma}{\ref{lem:entailment}}\label{apdx:lem:entailment}
    $\varphi_1$ entails $\varphi_2$ if and only if $\varphi_1 \Land
    \neg\varphi_2$ is unsatisfiable.
    \begin{proof}
        \enquote{$\Rightarrow$} Let $\varphi_1$ entails $\varphi_2$, and assume
        an assignment $\beta: \V \rightarrow \Z$ exists such that $\beta \models
        \varphi_1 \Land \neg \varphi_2$. 
        \begin{align*}
            \Rightarrow &\beta \models \varphi_1 \\
            \Rightarrow & \beta \in \llbracket \varphi_1 \rrbracket \\
            \Rightarrow & \beta \in \llbracket \varphi_2 \rrbracket \\
            \Rightarrow & \beta \models \varphi_2 \\
            \Rightarrow & \beta \not\models \neg\varphi_2 \\
            \Rightarrow & \beta \not\models \varphi_1 \Land \neg\varphi_2 \lightning
        \end{align*}
        By contradiction $\varphi_1 \Land \neg\varphi_2$ is unsatisfiable.

        \enquote{$\Leftarrow$} Let $\varphi_1 \Land \neg\varphi_2$ is
        unsatisfiable and assume $\llbracket \varphi_1 \rrbracket \not\subseteq
        \llbracket \varphi_1 \rrbracket$. There exists an assignment 
        \begin{align*}
            & \beta \in \llbracket \varphi_1\rrbracket \\
            \Rightarrow&\beta \models \varphi_1 \\
        \end{align*}
        and 
        \begin{align*}
            &\beta \not\in\llbracket\varphi_2\rrbracket \\
            \Rightarrow& \beta \not\models \varphi_2 \\
            \Rightarrow& \beta \models \neg\varphi_2
        \end{align*}
        Combined $\beta \models \varphi_1 \Land\neg \varphi_2 \lightning$.
        By contradiction $\varphi_1$ entails $\varphi_2$.
    \end{proof}
\end{apdxlemma}


\begin{apdxlemma}{\ref{lem:nonprop_update}}\label{apdx:lem:nonprop_update}
    Given an assignment $s\in\Sigma$, a formula $\varphi$ and an update $u: A
    \rightarrow \Z[\V]$. Without loss of generality $A' = \set{x'}{x \in A}$ is
    a set of fresh variables with $A' \cap \V = \emptyset$. We define
    $u(\varphi) := ((\varphi \Land \LAnd_{x\in A} x' = u(x))|_{A'})[x'/x]_{x\in
    A}$. For any partial assignment $s' = u(s)|_A$ and if $s \models \varphi$,
    then $s' \models u(\varphi)$.

    \begin{proof}
        \begin{align}
            s' &\models ((\varphi \Land \LAnd_{x\in A} x' =
            u(x))|_{A'})[x'/x]_{x\in A} \nonumber\\
            \Leftrightarrow & \models ((\varphi \Land \LAnd_{x\in A} x' =
            u(x))|_{A'})[x'/x]_{x\in A}[x/s'(x)]_{x\in A} \nonumber\\
            \Leftrightarrow & \models ((\varphi \Land \LAnd_{x\in A} x' =
            u(x))|_{A'})[x'/s'(x)]_{x\in A}\label{eq:chaining_subst}\\
            \Leftrightarrow & \models ((\varphi \Land \LAnd_{x\in A} x' =
            u(x)))[x'/s'(x)]_{x\in A} \label{eq:dropping_projection}\\
            \Leftrightarrow & \models ((\varphi \Land \LAnd_{x\in A} x' =
            u(x)))[x'/\bigl(\rho_u(s)\bigr)(x)]_{x\in A}\nonumber\\
            \Leftrightarrow & \models ((\varphi \Land \LAnd_{x\in A} x' =
            u(x)))[x'/\bigl(u(x)\bigr)(s)]_{x\in A}\nonumber\\
            \Leftrightarrow & \models
            (\varphi[x'/\bigl(u(x)\bigr)(s)]_{x_\in A}) \Land (\LAnd_{x\in A}
            x'[x'/\bigl(u(x)\bigr)(s)]_{x_\in A} = u(x)[x'/\bigl(u(x)\bigr)(s)]_{x\in
            A}) \nonumber\\
            \Leftrightarrow & \models
            \varphi \Land \LAnd_{x\in A} x'[x'/\bigl(u(x)\bigr)(s)] =
            u(x) \label{eq:dropping_substitutions}\\
            \Leftrightarrow & \models
            \varphi \Land \LAnd_{x\in A} \bigl(u(x)\bigr)(s) = u(x)\nonumber\\
            \Leftrightarrow & \models
            \varphi[x/s(x)]\Land \LAnd_{x\in A}
            u(x)[x/s(x)] =
            u(x)\label{eq:definition_of_update}\\
            \Leftarrow & \models
            \varphi[x/s(x)]\Land \LAnd_{x\in A}
            u(x)[x/s(x)][x/s(x)] =
            u(x)[x/s(x)]\label{eq:adding_model}\\
            \Leftrightarrow & \models
            (\varphi\Land \LAnd_{x\in A} u(x) = u(x))[x/s(x)]
            \label{eq:dedup_substitution}\\
            \Leftrightarrow & \models
            \varphi[x/s(x)]\nonumber\\
            \Leftrightarrow s & \models \varphi\label{eq:assumption}
        \end{align}

        Equation \ref{eq:chaining_subst} holds, because the substitutions can be
        chained. Equation \ref{eq:dropping_projection} holds, because the
        projection removed no variables contained in the substitution. Hence they
        are just implicitly existentially quantified and not affected otherwise.
        In equation \ref{eq:dropping_substitutions} the substitutions can be
        removed, because $\varphi$ and $u(x)$ do not contain any affected
        variables, as they were freshly generated. In Equation
        \ref{eq:definition_of_update} the update is just replaced by it's
        definition. Equation \ref{eq:adding_model} holds because if $s$ is a
        model for the formula, the formula is satisfiable. The inverse is not
        necessary true. Applying the substitution $[x/s(x)]$ a second
        time, does nothing in Equation \ref{eq:dedup_substitution} because
        $s(x) \in \Z$ and specifically do not contain any variables $x\in A$.
        Afterwards, the substitution is moved to the outside. Equation
        \ref{eq:assumption} holds by assumption.
    \end{proof}
\end{apdxlemma}

\begin{apdxlemma}{\ref{lem:pba}}\label{apdx:lem:pba}
    The property based abstraction is a valid abstraction function. For all
    $\varphi \in \Phi$ and finite set of properties $\Psi \subset \C$, the
    following holds.
    \begin{equation*}
        \llbracket \varphi\rrbracket \subseteq \llbracket\alpha_\Psi\rrbracket
    \end{equation*}
    \begin{proof}
        Let $\varphi \in \Phi$ and $\Psi \subset \C$ be a finite set of
        properties. Let $s \in \llbracket \varphi \rrbracket$ be a satisfying
        assignment of $\varphi$.
        \begin{align*}
            s \in \llbracket \varphi \rrbracket 
            &\Rightarrow s \in \llbracket \psi_i \rrbracket \text{ for all }
            \psi_i \in \Psi
            &\Rightarrow s \in \llbracket \Join_{\psi_i \in \Psi} \llbracket
            \psi_i \rrbracket
            &\Rightarrow s \in \llbracket \alpha_\Psi(\varphi) \rrbracket
        \end{align*}
    \end{proof}
\end{apdxlemma}