% \newpage

    For any assignment $s,s' \in\Sigma$, $\varphi\in\C$ and probabilistic update
    $\eta : \PV \rightarrow \Z[\V\union\D]$, if $s\models\varphi$, and $s'
    \in \support_s(\eta(s))$ then $s' \models \unfold(\varphi, \eta)$
    \begin{proof}
        Follows from Lemma \ref{lem:prob_update}.

    For any $\varphi\in2^\C$, assignments $s, s' \in \Sigma$ and probabilistic
    update $\eta : \PV \rightarrow \Z[\V\union\D]$, if $\models\varphi$ then
    \begin{enumerate}
        \item \label{itm:unfold1} $\models\unfold(\varphi, \eta)$. 
        \item \label{itm:unfold2} If additionally $s \models \varphi$ and $s' \in
            \support_s(\eta)$,
            then $s' \models \unfold(\varphi, \eta)$.
    \end{enumerate}
    \begin{proof} 
        Let $\varphi\in2^\C$, $s, s' \in \Sigma$, $s \models \varphi$ and $s'
        \in \support_s(\eta)$. $s' \models \unfold(\varphi, \eta)$ follows from
        Lemma \ref{lem:prob_update}.
         $\models\unfold(\varphi, \eta)$ follows directly from the existence of
         $s \models \varphi$ due to satisfiability and $s' \in \support_s(\eta)$
         since the support cannot be empty. 

        \} & \text{if } t = (l, p, \tau, \eta, \kappa, l') \\ &
        \text { and } \varphi' = \unfold(\varphi, t) \text{ is SAT} \\

        \} & \text{if } \begin{aligned}[t]
            &t = (l, p, \tau, \eta, l'), p \in [0,1], \tau \in 2^\C,\\
            &\eta: \PV \rightarrow \Z[\V\union\D]\text {, and} \\
            &\varphi' = \unfold(\varphi \land \tau, \eta) \text{ is SAT}
        \end{aligned} \\

The following lemma proves that the new transition is similar enough to the
original transition.

The following lemma proves that transitions are unfolded when the guard is
satisfiable from the given version and that the unfolded transition is
\enquote{similar} to the original transition.
\begin{lemma} [Existance, Similarity, Reachability of unfolded transitions]
    \label{lem:existance_and_similarity}
    Let $l \in \Loc_\Prog$, $t' \in \T_\Prog$, $s \in \Sigma$, and $\varphi$ be
    an \gls{fo}-formula over variables $\PV$. Moreover let $t = (l, p, \tau,
    \eta, l')$ with locations $l' \in \Loc_\Prog$, a probability $p \in
    [0,1]$ and an update $\eta: \PV \rightarrow \Z[\V\union\D]$.

\begin{lemma}[Similarity of unfolded transitions]\label{lem:unfold_t_similar}
    For some $\tilde{l, l_1, l_2} \in \Loc_\Prog$, probability $p \in [0,1]$,
    update $\eta: \PV \rightarrow \Z[V\union\D]$, and cost $\kappa \in \R$, let $t
    = (l_1, p, \tau \eta, \kappa, l_2)\in \T_\Prog$. Moreover let $\varphi$ be an
    arbitrary \gls{fo}-formula.
    If $\unfold^*(\langle l, \varphi\rangle, t) \neq \emptyset$ then 

    If $s|\PV \models \varphi \Land \tau$ and $l = l_1$ then:

        \item\label{itm:lequal} $l = l_1$, 
        \item\label{itm:t_exists} $\unfold^*(\langle l, \varphi\rangle, t') =
            \{t^*\}$ for some $t^* \in \T_\text{PE}$,
        \item\label{itm:t_similar} $t^* = (\langle l, \varphi\rangle, p, \tau,
            \eta, \kappa, \langle l_2, \varphi'\rangle)$ for some $\varphi' \in \C$, and 

        \item\label{itm:t_exists} an unfolded transition $t^* \in
            \T_\mathrm{PE}$ exists with 
            \begin{equation*}
                \unfold^*(\langle l, \varphi\rangle, t) = \{t^*\},
            \end{equation*}
        \item\label{itm:t_similar} the unfolded transition $t^*$ is similar to
            the original transition:
            \begin{equation*}
                t^* = (\langle l, \varphi\rangle, p, \tau, \eta, \langle l',
                \varphi'\rangle) \text{ for some }\varphi' \in \C,
            \end{equation*}
        \item\label{itm:new_version_contains_reachable_states} for any
            \textit{reachable} state $s'$, that is there exists a scheduler
            $\scheduler \in \MDS$ and starting state $s_0$ and transitions $t'
            \in \T_\Prog$, for which $\prSs((l, t, s) \rightarrow (l', t', s'))
            > 0$, 
            \begin{equation*}
                s' \models \varphi'.
            \end{equation*}

        The unfolding returns a non empty set if and only if the location $l$ of
        the given version is equal to the start location $l_1$ of the location.
        The unfolding returns only an empty set or a set containing a single
        transition. That new transition contains $p$, $\tau$, $\eta$, and $\kappa$
        which were copied from the original transition. The source and target
        version of the new transition have by construction the same locations as
        the original transition.
    \end{proof}
\end{lemma}

        Let $l \in \Loc_\Prog$, $t' \in \T_\Prog$, and $\varphi \in 2^\C$ If
        $s\models \varphi \Land \tau$ then by lemma \ref{lem:unfold}
        $\models\unfold(\varphi \Land \tau, \eta)$ and by construction the
        transition is unfolded to a single transition $t^* \T_\text{PE}$ with
        $\unfold^*(\langle l, \varphi\rangle, t) = \{t^*\}$.

\begin{lemma}[Existance of unfolded transitions]\label{lem:unfold_t_exists}
    L $l,l' \in \Loc_\Prog$ be locations, $t, t' \in \T$ transitions, $s, s' \in
    \Sigma$ assignments, and let $\varphi$ be an \gls{fo}-formula over variables
    $\PV$. If $s \in \llbracket\varphi\rrbracket$ and $\prSs((l,t,s) \rightarrow
    (l',t',s')) > 0$ for any scheduler $\scheduler$ and starting state  $s_0 \in
    \Sigma$ then
    \begin{enumerate}
        \item Items \ref{itm:lequal} to \ref{itm:t_similar} from Lemma
            \ref{lem:unfold_t_similar} hold, and
        \item\label{itm:smodelsphi}$s' \in \llbracket\varphi'\rrbracket$
    \end{enumerate}

        The similarity follows by construction, as the properties of the
        transition are only copied from the original transition. 

    \begin{proof}
        Let $s_0\in\Sigma$ and $\scheduler$ be any scheduler for which
        $\prSs((l,t,s) \rightarrow (l',t',s')) > 0$. In
        \Sref{ssec:probability_space} the probability measure $\prSs$ was

        Finally let $s_0\in\Sigma$ be any starting state, $\scheduler \MDS$ any
        scheduler, and $t \in \T_\Prog$ be any transition for which
        $\prSs((l,t,s) \rightarrow (l',t',s')) > 0$.
        In \Sref{ssec:probability_space} the probability measure $\prSs$ was

        (l, p, \tau, \eta, \kappa, l')$ for some $p \in [0,1]$, $\tau \in C$, $\eta
        : \PV \rightarrow \Z[\V \union \D]$, and $\kappa \in \R$. It remains to be
        shown that $s' \models \varphi' = \unfold(\varphi \land \tau, t)$. The
        rest follows by construction and Lemma \ref{lem:unfold_t_similar}.

        (l, p, \tau, \eta, l')$ for some $p \in [0,1]$, $\tau \in C$, and $\eta
        : \PV \rightarrow \Z[\V \union \D]$. 

        Using Lemma \ref{lem:unfold} we get $s' \models \unfold(\varphi \Land
        \tau,\eta)$, completing the proof.

        Using lemma \ref{lem:unfold} one gets $s' \models \unfold(\varphi \Land
        \tau, \eta) = \varphi'$ completing the proof.

\begin{align}

\begin{align*}

\end{align}
% \begin{lemma}[Similarity of unfolded general
%     transitions]\label{lem:unfold_g_similar}
%     $\unfold^*(\langle l, \varphi\rangle, g) \neq \emptyset$ if and only if
%     $\unfold^*(\langle l, \varphi\rangle, t_i \neq\emptyset$ for all $t_i \in
%     g$, and 
% \end{lemma}

\end{align*}

\begin{lemma}[Existance, Similarity of unfolded general transitions\label{lem:existance_and_similarity_g}]
   
    Let $l \in \Loc_\Prog$,  $s \in \Sigma$, and $\varphi$ be an
    \gls{fo}-formula over variables $\PV$. Moreover let $g = {t_1, \dots,t_n}
    \in \GTP$. If $s \models \varphi \Land \tau_g$ and $l = l_g$ then:

\begin{lemma}\label{lem:unfold_g}
    Let $l,l' \in \Loc_\Prog$ be locations, $t, t' \in \T$ transitions, $s, s'
    \in \Sigma$ assignments, and let $\varphi \in \C$ be a constraint.
    Furthermore let $g' \in \GT$ be the general transition containing $t'$. If
    $s \in \llbracket\varphi\rrbracket$ and $\prSs((l,t,s) \rightarrow
    (l',t',s')) > 0$ for any scheduler $\scheduler$ and starting state $s_0 \in
    \Sigma$ then 
    \begin{equation*}
        \unfold(\varphi, t') \subseteq \unfold^*(\varphi, g') \neq \emptyset
    \end{equation*}

    \begin{enumerate}
        \item\label{itm:g_exists} the unfolded general transition $g' \in \GTPE$
            is not empty with some $t'_1, \dots, t'_n \in \T_\text{PE}$
            \begin{equation*}
                g' = \unfold^*(\langle l, \varphi\rangle, g) = \{t'_1, \dots,
                t'_n\} \neq \emptyset,
            \end{equation*}
        \item \label{itm:t_in_g_similar} $t_i \in g$ are similar to $t'_i \in
            g'$  for all $i=1, \dots, n$, that is for some $p_i \in [0,1]$, $\eta_i : \PV \rightarrow
                \Z[\V\union\D]$, and $l_i \in \Loc_P$:
            \begin{equation*}
                 t_i' = (\langle l_g, \varphi\rangle, p_i, \tau_g, \eta_i,
                 \langle l_i,\varphi\rangle) \text{ when } t_i = (l_g, p_i, \tau_g, \eta_i, l_i)
            \end{equation*}
    \end{enumerate}

        Follows immediately from Lemma \ref{lem:unfold_t_exists}.

        Let $l \in \Loc_\Prog$,  $s \in \Sigma$, and $\varphi$ be an
        \gls{fo}-formula over variables $\PV$. Moreover let $g = {t_1,
        \dots,t_n} \in \GTP$. If $s \models \varphi \Land \tau_g$ and $l = l_g$
        then: Since all transitions $t_1, \dots t_n$ have the same guard
        $\tau_g$, the non-emptiness follows immediately from Lemma
        \ref{lem:existance_and_similarity}. 
        Let $g' = \{t'_1, \dots,t'_m\} = \unfold^*(\langle l_g, \varphi\rangle,
        g)$ for some $t'_1, \dots, t'_m \in \T_\mathrm{PE}$. Every $t'_i \in g'$
        was created by some unfolding $\unfold^*(\langle l_g, \varphi\rangle,
        t_i)$ where $t_i \in g$. This implies that $n =m$ and by Lemma
        \ref{lem:existance_and_similarity} $t_i$ and $t'_i$ are similar. 

The next lemma shows, that unfolding a general transition creates a valid new
general transition in the partial evaluation graph.
\begin{lemma}[Soundness\label{lem:unfold_sound}]
    For some \gls{pip} $\Prog$, let $\varphi\in\C$, $l\in\Loc$ and $g = \{t_1,
    \dots{},t_n\} \in \GTP$ with guard $\tau_g$. Either $unfold(\langle l,
    \varphi\rangle, g) = \emptyset$ or $unfold(\langle l, \varphi\rangle, g) =
    \{t_1', \dots{},t_n'\}$ where for all $i=1,\dots{},n$:
    \begin{enumerate}
        \item $\{t_i'\} = \unfold^*(\langle l, \varphi\rangle,t_i)$,
        \item $t_i' = (\langle l, \varphi\rangle, p_i, \tau_g, \eta_i,
            \kappa_i,\langle l',\varphi\rangle)$ when $t_i = (l, p_i, \tau_g, \eta_i,
            \kappa_i, l')$ for some $p_i \in [0,1]$, $\eta_i : \PV \rightarrow
            \Z[\V\union\D]$, $\kappa_i\in\R$, and $l' \in \Loc_P$.
    \end{enumerate}
    This implies especially that the probabilities of transitions $t_1' \dots
    t'_n$ add up to 1.

\begin{lemma}[Soundness\label{lem:unfold_g_sound}]
    Let $l \in \Loc_\Prog$,  $s \in \Sigma$, and $\varphi$ be an
    \gls{fo}-formula over variables $\PV$. Let $g \in \GTP$ and $g' =
    \unfold(\langle l, \varphi\rangle, g)$. If $g' \neq \emptyset$ then $g'$ is
    a sound general transition with $\tau_{g'} = \tau_g$, and starting location
    $l_{g'} = \langle l_g, \varphi\rangle$.

        Let $g = \{t_1, \dots, t_n\} \in \GTP$ with $t_i =
        (l_g,p_i,\tau_i,\eta_i,\kappa_i,l'_i)$. 

        By construction $g'$ is only an non-empty set if one transition is
        unfolded and then all transitions are unfolded. Due to the similarity
        shown by lemma \ref{lem:existance_and_similarity_g} all unfolded
        transitions have probabilities adding up to 1, share the same guard
        $\tau_{g'} = \tau_{g}$, and the same starting location $l_{g'} = \langle
        l_g, \varphi\rangle$
    \end{proof}
\end{lemma}
% Lemma \ref{lem:existance_and_similarity_g} implies that if the transition is
% unfolded to a non-empty set, the unfolded set is a sound general transition,
% with a single guard $\tau_{g'}$ used by all transitions of all 
% \begin{lemma}\label{lem:unfold_g}
%     Let $l,l' \in \Loc_\Prog$ be locations, $t, t' \in \T$ transitions, $s, s'
%     \in \Sigma$ assignments, and let $\varphi \in \C$ be a constraint.
%     Furthermore let $g' \in \GT$ be the general transition containing $t'$. If
%     $s \in \llbracket\varphi\rrbracket$ and $\prSs((l,t,s) \rightarrow
%     (l',t',s')) > 0$ for any scheduler $\scheduler$ and starting state $s_0 \in
%     \Sigma$ then 
%     \begin{equation*}
%         \unfold(\varphi, t') \subseteq \unfold^*(\varphi, g') \neq \emptyset
%     \end{equation*}
%     \begin{proof}
%         Follows immediately from the existance asserted in Lemma
%         \ref{lem:existance_and_similarity}.
%     \end{proof}
% \end{lemma}

        By Definition \ref{def:pip} all transitions $t_1,\dots t_n$share the
        same guard $t_i = t_g$ for all $i=1,\dots,n$. All transitions are
        unfolded exactly once by construction. If $\models \varphi \Land
        \tau_g$, then by Lemma \ref{lem:supp_update_not_empty} and Lemma
        \ref{lem:prob_update} so is $ \models \tilde{\eta}(\varphi \Land \tau_g
        \lfloor\eta\rceil)$. Hence by Lemma \ref{lem:unfold} all $\models
        \unfold(\varphi \Land \tau_g, \eta_i)$ and $\unfold^*(\langle l,
        \varphi\rangle, t_i) = \{t_i'\}$ for some $t_i \in 2^{\T_\text{PE}}$ and
        $i=1,\dots,n$. And by Lemma \ref{lem:unfold_t_similar} they have the
        same probability, guard, update and cost.

% \begin{lemma}[Soundness\label{lem:unfold_sound}]
%     For some \gls{pip} $\Prog$, let $\varphi\in\C$, $l\in\Loc$ and $g = \{t_1,
%     \dots{},t_n\} \in \GTP$ with guard $\tau_g$. Either $unfold(\langle l,
%     \varphi\rangle, g) = \emptyset$ or $unfold(\langle l, \varphi\rangle, g) =
%     \{t_1', \dots{},t_n'\}$ where for all $i=1,\dots{},n$:
    % \begin{enumerate}
    %     \item $\{t_i'\} = \unfold^*(\langle l, \varphi\rangle,t_i)$,
    %     \item $t_i' = (\langle l, \varphi\rangle, p_i, \tau_g, \eta_i,
    %         \kappa_i,\langle l',\varphi\rangle)$ when $t_i = (l, p_i, \tau_g, \eta_i,
    %         \kappa_i, l')$ for some $p_i \in [0,1]$, $\eta_i : \PV \rightarrow
    %         \Z[\V\union\D]$, $\kappa_i\in\R$, and $l' \in \Loc_P$.
    % \end{enumerate}
    % This implies especially that the probabilities of transitions $t_1' \dots
    % t'_n$ add up to 1.

        If $\not\models\varphi \Land\tau_g$, all
        $\not\models\unfold(\varphi\Land\tau_g, \eta_i)$ and $unfold(\langle
        l,\varphi\rangle,t_i) = \emptyset$ for all $i=1,\dots,n$.

    % \begin{proof}
    %     Let $g = \{t_1, \dots, t_n\} \in \GTP$ with $t_i =
    %     (l_g,p_i,\tau_i,\eta_i,\kappa_i,l'_i)$. 

        The probabilities of all transition $t_1,\dots, t_n$ in the general
        transition $g$ add up to 1 and so do the probabilities of all
        transitions $t'_1,\dots,t'_n$, because the probabilities are just
        copied.
    \end{proof}
\end{lemma}

    %     By Definition \ref{def:pip} all transitions $t_1,\dots t_n$share the
    %     same guard $t_i = t_g$ for all $i=1,\dots,n$. All transitions are
    %     unfolded exactly once by construction. If $\models \varphi \Land
    %     \tau_g$, then by Lemma \ref{lem:supp_update_not_empty} and Lemma
    %     \ref{lem:prob_update} so is $ \models \tilde{\eta}(\varphi \Land \tau_g
    %     \lfloor\eta\rceil)$. Hence by Lemma \ref{lem:unfold} all $\models
    %     \unfold(\varphi \Land \tau_g, \eta_i)$ and $\unfold^*(\langle l,
    %     \varphi\rangle, t_i) = \{t_i'\}$ for some $t_i \in 2^{\T_\text{PE}}$ and
    %     $i=1,\dots,n$. And by Lemma \ref{lem:unfold_t_similar} they have the
    %     same probability, guard, update and cost.
    %     If $\not\models\varphi \Land\tau_g$, all
    %     $\not\models\unfold(\varphi\Land\tau_g, \eta_i)$ and $unfold(\langle
    %     l,\varphi\rangle,t_i) = \emptyset$ for all $i=1,\dots,n$.
    %     The probabilities of all transition $t_1,\dots, t_n$ in the general
    %     transition $g$ add up to 1 and so do the probabilities of all
    %     transitions $t'_1,\dots,t'_n$, because the probabilities are just
    %     copied.
    % \end{proof}
% \end{lemma}

Lets recap what we just constructed. A source constraint $\varphi\in\C$
describes a set of states. The unfolding computes a new (target) constraint
which describes a polyhedron that containins (at least) all states reachable
from the source constraint via a given transition. A version describes a set of
states at a given location. The overloaded unfolding create new transitions
between (possibly new versions), where every state reachable via an original
transition from a state in the source version, is contained in the target
version. The properties, such as probability, guard, update, and cost are just
copied, without alteration. 

Lets recap what was just constructed. A source constraint $\varphi\in\C$
describes a set of states. The unfolding computes a new (target) set of
constraint which describes a polyhedron that contains (at least) all states
reachable from the source constraint via a given transition. A version describes
a set of states at a given location. The overloaded unfolding create new
transitions between (possibly new versions), where every state reachable via an
original transition from a state in the source version, is contained in the
target version. The properties, such as probability, guard, update, and cost are
just copied, without alteration. 

            \For{$t = (v, \tau, \eta, p, \kappa, v') \in g'$}{
                \uIf {$v' \not\in V(G$}{

            \For{$t = (v, \tau, \eta, p, v') \in g'$}{
                \uIf {$v' \not\in V(G$\label{alg:naive_line_inclusion}}{

graph, as done on line \ref{alg:naive_evaluation_inclusion} of

graph, as done on line \ref{alg:naive_line_inclusion} of Algorithm

    $\Prog'$ is called the \textit{partial evaluation} of $P$.

    $\Prog'$ is called the \textit{partial evaluation} of $\Prog$.

        \ref{lem:unfold_sound}. We set $\bar{g} = g$.

        \ref{lem:existance_and_similarity_g}. We set $\bar{g} = g$.

    GT_G, \langle l_0, \textit{true}\rangle)$ be a new program where $G$ and

    \GTG, \langle l_0, \textit{true}\rangle)$ be a new program where $G$ and

    program $\Prog$.

    program $\Prog$. $\Prog'$ is a sound program.

    $\Prog'$ is a sound program.

        Lemma \ref{lem:unfold_sound} asserts all general transitions found on

        Lemma \ref{lem:unfold_g_sound} asserts all general transitions found on

\todo{section introduction}

    For a pip $\Prog$, a markovian scheduler $\scheduler: \confs \rightarrow \GT
    \union \{g_\bot\}$ of $\Prog$, and the evaluation $\Prog'$ as described in
    Theorem \ref{thm:soundness}, there exists a markovian scheduler
    $\scheduler': \confs' \rightarrow \GT' \union \{g'_\bot\}$, such that for
    all finite prefixes $f\in\fpath$ there exists a finite prefix $f'\in\fpath'$
    with 

    For a \gls{pip} $\Prog$, a markovian scheduler $\scheduler \in \MDS$ of $\Prog$,
    and the evaluation $\Prog'$ as described in Theorem \ref{thm:soundness},
    there exists a markovian scheduler $\scheduler' \in \MDS$, such that for all
    finite prefixes $f\in\fpath_\Prog$ there exists a finite prefix
    $f'\in\fpath_{\Prog'}$ with 

    The proof will be done in two steps, first a scheduler $\scheduler'$ is

    The proof is done in two steps. First a scheduler $\scheduler'$ is

    Then we will do an inductive construction over an arbitrary finite path
    using the previously constructed scheduler. 

    Then using this scheduler, for a finite path $f$ an equivalent finite path
    is constructed by induction. 

    For a pip $\Prog$, a markovian scheduler $\scheduler: \confs \rightarrow \GT
    \union \{g_\bot\}$ of $\Prog$, and the evaluation $\Prog'$ we construct a
    markovian scheduler $\scheduler': \confs_\Prog \rightarrow \GTP \union
    \{g_\bot\}$. 

    For a \gls{pip} $\Prog$, a markovian scheduler $\scheduler \in \MDS$ of
    $\Prog$, and the evaluation $\Prog'$ we construct a markovian scheduler
    $\scheduler' \in \MDS$ for $\Prog'$.

    Let $\langle l, \varphi\rangle \in \vers$ be a version on location
    $l\Loc_\Prog$ and formula $\varphi$. Moreover let $(g, \tilde{s}) =
    \scheduler((l, t, s))$ be the decision taken by the original scheduler. 

    Let $\langle l, \varphi\rangle \in \vers$, be a version on location $l \in
    \Loc_\Prog$ and formula $\varphi$. Let $t'\in\TPn$, $s' \in \Sigma$.
    Moreover let $(g, \tilde{s}) = \scheduler((l, \bar{t'}, s))$ be the decision
    taken by the original scheduler. 

    \varphi\rangle$, not every general transition $g\in\GT$ is unfolded to a new
    transition $g'\in\GT'$. Transitions that can not be taken from a state
    $s\models\varphi$ are filtered by a satisfiability check. This consideration
    is especially important because the (memoryless) scheduler selects the
    general transition independently of the fact that a configuration is
    reachable in first place. If this is the case, the new scheduler will select
    any arbitrary other transition. We will see that this doesn't matter, since
    a decision at an unreachable configuration has no impact on the equivalence
    of admissible runs. 

    \varphi\rangle$, not every general transition is unfolded to a new general
    transition. But in Lemma \ref{lem:existance_and_similarity_g} it was shown
    that an unfolded general transition $g'$ is non-empty if $s \models \varphi
    \land \tau_g$ and $l_g = l$. This consideration is especially important
    because the new (memoryless) scheduler must select a general transition
    independently of the fact that a configuration is reachable in first place. 
    The new scheduler is defined to map to the unfolded general transition of
    $g$. If it doesn't exist, any other general transition is selected, which
    satisfies the properties of a markovian scheduler. 

    We define $g' \in \GT'$ to be the general transition created by unfolding
    the general transition $g \in \GT$ or any other general transition 
    \begin{align} 
        \label{eq:schedulerconstruction1}
        \scheduler((l', t', s')) = 

    In total the new scheduler is defined as follows:
    \begin{equation*}
        \scheduler'((l', t', s')) = 

            (g'_\bot, s') & \text{if } l' = l'_\bot \text{ or } t' = t'_\bot\\
            (\unfold^*(\varphi, g), \tilde{s}) & \text{if } s\models\varphi
            \text{ and } g \neq g_\bot\\
            (g'^*, \tilde{s}^*) & \text{if } g'^* \in \unfold^*(\langle

            (\unfold^*(\langle l', \varphi\rangle, g), \tilde{s}) & 
            \begin{aligned}
                &\text{if }l' = \langle l, \varphi \rangle \neq l_\bot, \varphi
                \in 2^\C, l \in \Loc_\Prog \\
                &\scheduler((l, \bar{t'}, s')) = (g, \tilde{s}), \text{ and }\\
                & s' \models \varphi
            \end{aligned} \\
            (g'^*, \tilde{s}^*) & \text{if } g'^* \in \GTout(\langle

            exists\\
            (g'_\bot, s') & \text{otherwise}

            \text{ exists} \\
            (g_\bot, s') & \text{otherwise}

    \end{align}

    \end{equation*}

    $\Prog'$. We will show items \ref{itm:md1} to \ref{itm:md4} of Definition
    \ref{def:mscheduler}. Let $c' = (l', t', s)$. If $l' = l_\bot$ or $t' =
    t_\bot$, $\scheduler'(c') = (g'_\bot, s)$  follows immediately from the
    construction \ref{eq:schedulerconstruction1}. Next, let $l' \neq l'_\bot$
    and $t' \neq t'_\bot$. Assume $s\not\models\varphi$ the new scheduler
    selects a general transition fulfilling properties (1)-(3) automatically by
    construction. Note that all transitions starting in $l'$ must have been
    created by the unfolding $unfold(l')$ and hence considered by the scheduler
    for selection. 
    Finally assume $s\models\varphi$. If the original scheduler returned $(g,
    \tilde{s}) = \scheduler(c))$ and $g \neq g_\bot$, then $g' =
    \unfold^*(\varphi, g) = \Union_{t\in g} \neq \emptyset$ by lemma () and
    properties (1)-(3) are satisfied
    \begin{enumerate}
        \item $\tilde{s}'(x) = \tilde{s}(x) = s(x)$ for all $x\in\PV$ by
            Definition \ref{def:mscheduler} for $\scheduler$.
        \item $l = l_g$ by Definition \ref{def:mscheduler} for $\scheduler$ and 
            $l' = \langle l, \varphi \rangle = l'_g$ by construction of the
            unfolding (\todo{ref}).
        \item $s \models \tau_g$ by Defeinition \ref{def:mscheduler} and
            $\tau_{g'} = \tau_g$ by construction of the unfolding.
            $s\models\tau_{g'}$ holds.
    \end{enumerate}

    $\Prog'$. 

    If the original scheduler returned the terminal transition $\scheduler(c)=
    (g_\bot, s)$, then so does the new scheduler $\scheduler(c') = (g'_\bot, s)$
    by construction. This is correct because by lemma (\ref{}). 

    Case 1, $s' \models \varphi$. In case the original scheduler $\scheduler(l',
    \bar{t'},s') $ selects $(g_\bot, s')$, so does $\scheduler'$. This is
    correct, because $\scheduler(l, \bar{t'},s) = (g_\bot, s')$ implies by
    Definition \ref{def:mscheduler} that no transition $g\in\GTout(l)$ exists
    where $\tau_g$ can be satisfied and by Lemma
    \ref{lem:existance_and_similarity_g} no such transition can exist in
    $\GTout(l')$. If the original scheduler selects $\scheduler(l, \bar{t'},s) =
    (g, \tilde{s})$ with $g \neq g_\bot$ then by Definition \ref{def:mscheduler}
    $\tilde{s}\models \tau_g$. By $s\models \varphi$ and since $\varphi$
    contains only variables from $\PV$ so does $\tilde{s} \models \varphi$. By
    Lemma \ref{lem:existance_and_similarity_g} $\unfold(\langle l,
    \varphi\rangle) = g' \neq \emptyset$ and $\tilde{s} \models \tau_{g'} =
    \tau_{g}$.

    We interject a small observation following from the above, that will be
    useful for the later induction. 
    \begin{lemma}[Corollary] 
        If $s \models \varphi$ then:
        \begin{enumerate}
            \item $(g_\bot, _) = \scheduler(c)$ if and only if $g'_\bot =
            \scheduler'(c')$.
            \item $(g, _) = \scheduler(c)$ and $(g',_) = \scheduler(c')$ with $g
                \neq g_\bot$ and $g' \neq g'_\bot$ then $g$ and $g'$ have the
                same probability $p$.
        \end{enumerate}
    \end{lemma}

    Case 2, $s' \not\models \varphi$. The properties of a scheduler (see
    Definition \ref{def:mscheduler}) are satisfied by construction.

    Given an admissible run $f^*= c_0\dots{}c_N\in \fpath$ of the original
    program $\Prog$ with $c_i = (l_i,s_i,t_i)$ for all $i = 0,1,\dots$ and a
    scheduler $\scheduler$ for the very same program. Let $\scheduler'$ be
    constructed as above.

    Note, by construction the $\scheduler'$ selects a similar transition and and
    the same variable assignment $\scheduler$ whenever $s \models \varphi$. The
    proof is concluded with an induction using the constructed scheduler
    $\scheduler'$.

    \textbf{Induction hypothesis.} We can find a prefix
    $f'_n=c'_0c'_1\cdots{}c_n \in \fpath'$ of length $n \leq N$ with 

    \textbf{Induction hypothesis.} For any arbitrary run $f= c_0\dots{}c_n\in
    \fpath_\Prog$ of length $n \leq \N$ with with $c_i = (l_i,s_i,t_i)$ and all
    $i = 0,1,\dots$ one can find a prefix $f'_n=c'_0c'_1\cdots{}c_n \in
    \fpath_{\Prog'}$ with:

        \item  $c'_i = (\langle l_i, \varphi_i\rangle,s_i,t'_i)$ for some
            $\varphi_i \in \C$, $t'_i \in \T'$, and $i = 1, \dots, n$

        \item  $c'_i = (\langle l_i, \varphi_i\rangle,t'_i,s_i)$ for some
            $\varphi_i \in 2^\C$, $t'_i \in \TPn$, and $i = 1, \dots, n$

    Items \ref{itm:location_in_version} and \ref{itm:si_models_phi} are useful
    for using the properties of the scheduler but not important for the final
    result.  

    Items \ref{itm:location_in_version} and \ref{itm:si_models_phi} are required
    for the scheduler to select a similar general transition not important for
    the final result.  

    Since $f^*$ is an admissible prefix, $c_0 = (l_0, t_\text{in},s_0)$. Set

    Since $f = c_0$ is an admissible prefix, $c_0 = (l_0, t_\text{in},s_0)$. Set

    \textit{true}\rangle$ is a location in $\Prog'$ since it is added at first by the
    evaluation algorithm. $s_0 \models \textit{true}$ trivially. $\prSs(c_0) =
    \prSs'(c'_0) = 1$ since both $c_0$ and $c'_0$ are valid starting configurations
    in $\Prog$ and $\Prog'$ respectively.

    \textit{true}\rangle$ is a location in $\Prog'$ since it is the first
    location added to $\Prog'$ in line \ref{alg:abstr_line_addl0} of Algorithm
    \ref{alg:evaluate_abstr} and it is set as the start location of $\Prog'$ in
    Definition \ref{def:partial_evaluation}. $s_0 \models \textit{true}$
    trivially. $\prSs(c_0) = \prSs'(c'_0) = 1$ since both $c_0$ and $c'_0$ are
    valid starting configurations in $\Prog$ and $\Prog'$ respectively.

    Assume the induction hypothesis holds for $n < N$ we will construct a prefix
    of length $n+1$ for which the induction hypothesis equally holds. 

    Assume the induction hypothesis holds for $n \in \N$. Let $f = c_0\dots{}
    c_{n+1} \in \fpath_\Prog$ of length $n+1 \in \N$ be an admissible prefix,
    then so is $f^* = c_0\dots{}c_{n}$ of length $n$. By induction hypothesis a
    prefix $f'^* = c'_0\dots{}c'_{n}$ of equal length exists with 

    Since the prefix $f$ is admissible, so is its prefix $f_i =
    c_0c_1\dots{}c_nc_{n+1}$ and by definition \todo{ref}
    \begin{equation*}
        \prSs(f) = \prSs(c_0) \cdot \prod_{i=1,\dots,n+1} \prSs(c_{i-1} \rightarrow
        c_i) > 0
    \end{equation*}
    Let $\scheduler(c_n) = (g_{n+1},\tilde{s}_n)$ by definition \todo{ref}
    \begin{equation*}
        \prSs(c_n \rightarrow c_{n+1}) = p \cdot
        \prod_{x\in\PV}[\eta(x)](\tilde{s}_n)(s_{n+1}(x)) \cdot \prod_{u\in\V\backslash\PV}
        \delta_{\tilde{s}_n(u),s_n(u)} > 0
    \end{equation*}
    Set the state $s'_{n+1} = s_{n+1}$, and the transition $t'_{n+1} =
    \unfold(\varphi_i, t_i)$. $t_{n+1} \in g$ and by construction of the
    unfolding 
    Since $f'_n$ is an admissible path, $\langle l_n, \varphi_n \rangle$ is a valid
    location (version) in $\Prog'$, every version is unfolded by the evaluation
    algorithm immediately after being added to the new program in (\todo{ref}). As
    $g_i$ is selected by the scheduler, $g_{n+1}$ is a general transition with
    $l_{g_{n+1}} = l_n$. As such $g_{n+1}$ is unfolded by the algorithm in
    (\todo{ref}) and so is the transition $t_{n+1}$ as part of unfolding of the
    general transition $g_{n+1}$.
    With $g'_{n+1}=\text{unfold*}(\varphi_n, g_{i+1})$, define the next
    $\scheduler'_{n+1}$ as 
    \begin{equation*}
        \scheduler'_{n+1}(c) = \begin{cases}
            (g'_{n+1}, \tilde{s}_n) & \text{if } c = c'_n \\
            \scheduler'_n & \text{otherwise}
        \end{cases}
    \end{equation*}
    Select $t'_{n+1} = \text{unfold*}(\varphi_n, t_{n+1}) \in g'_{n+1}$
    Recall definition (\todo{ref}), by construction $t'_{n+1}=(\langle l_n,
    \varphi\rangle,p,\tau_i,\eta,\langle l_{n+1}, \varphi_{n+1}\rangle)$
    for some formula $\varphi_{n+1}$.
    \begin{equation*}
        \prSnns(c'_n \rightarrow c'_{n+1}) = p \cdot
        \prod_{x\in\PV}[\eta(x)](\tilde{s'}_n)(s'_{n+1}(x)) \cdot \prod_{u\in\V\backslash\PV}
        \delta_{\tilde{s}(u),s(u)} > 0
    \end{equation*}

    \begin{enumerate}
        \item $\prSs(c_0\dots{}c_n) = \prSns'(c'_0\dots{}c'_n)$
        \item $c'_i = (\langle l_i, \varphi_i\rangle,s_i,t'_i)$ for some
            $\varphi_i \in 2^\C$, $t'_i \in \TPn$, and $i = 1, \dots, n$
        \item $s_i \models \varphi_i$ 
    \end{enumerate}
    
    Let $c_i = (l_i,s_i,t_i)$ for all $i = 0, \dots,n+1$ and since $f$ is
    admissible, let $t_{n+1} = (l_n, p_{n+1},\tau_{n+1}, \eta_{n+1}, l_{n+1})$ with
    a probability $p \in [0,1]$, a guard $\tau_i \in 2^\C$, an update $\eta: \PV
    \rightarrow \Z[\V\union\D]$. Let $\{t'_{n+1}\} = \unfold^*(\langle l_n,
    \varphi_n\rangle)$, due similarity established in Lemma,
    \ref{lem:existance_and_similarity} $t=(\langle l_n, \varphi_n\rangle, p,
    \tau_{n+1}, \eta_{n+1}, \langle \varphi_{n+1}, l_{n+1}\rangle)$ for some
    $\varphi_{n+1} \in 2^\C$. Due to reachability by Lemma
    \ref{lem:existance_and_similarity} $s_{n+1} \models \varphi_{n+1}$. 
    Let $c'_{n+1} = (\langle l_{n+1}, \varphi_{n+1}, t_{n+1}, s_{n+1}$ be the
    last configuration of $f' = c'_0\dots{}c_nc_{n+1}$

    By lemma (\todo{ref}) $s_{n+1} \models \varphi_{n+1}$, fulfilling (3) of the
    induction hypothesis. We fulfill (2) of the induction hypothesis, by
    constructing $c'_{n+1} = (\langle l_{n+1}, \varphi_n\rangle, s_{n+1},
    t'_{n+1})$. By setting $s'_{n+1} = s_{n+1}$ we get $\prSnns(c'_n\rightarrow
    c'_{n+1})= \prSs(c_n \rightarrow c_{n+1})$ and with the induction hypothesis
    \begin{equation*}
        \prSs(f_n) = \prSnns(f'_nc'_{n+1})
    \end{equation*}
    and fulfill (1) of the induction hypothesis.

    Finally, let $\scheduler(c_n) = (g_{n+1},\tilde{s})$ where $g_{n+1} \neq
    g_\bot$ due to $f$ being admissible. By construction of the scheduler
    $\scheduler'$ a similar general transition is selected $\scheduler(c'_n) =
    (g'_{n+1},\tilde{s})@$ where $g'_{n+1} \neq g_\bot$ and with the same guard
    $\tau_g = \tau_{g'}$.

    \begin{align*}
        \prSs(c_n \rightarrow c_{n+1}) &= p \cdot
        \prod_{x\in\PV}[\eta(x)](\tilde{s})(s_{n+1}(x)) \cdot \prod_{u\in\V\backslash\PV}
        \delta_{\tilde{s}_n(u),s_n(u)} \\
        &= \prSns(c'_n \rightarrow c'_{n+1}) \\
        \Leftrightarrow \prSs(f) &= \prSs(f^*) \cdot \prSs(c_n \rightarrow
        c_{n+1}) \\
        &=  \prSs(f'^*) \cdot \prSs(c'_n \rightarrow c'_{n+1}) = \prSns(f')
    \end{align*}
    The induction hypothesis holds for $n+1$.

% \begin{definition}[Reachability]\def{def:reachability}
%     % Das ist falsch. Hier muss \tilde{s} betrachtet werden...
%     Let $l, l' \in \Loc_\Prog$, $t,t' \in \T_\Prog$, and $s,s' \in \Sigma$. A
%     configuration $c' = (l', t', s')$ is \textit{reachable} from $c = (l, t, s)$
%     if and only if there exists a scheduler $\scheduler \in \MDS$ and starting
%     state $s_0 \in \Sigma$ for which $\prSs(c \rightarrow c') > 0$.
% \end{definition}
%     Let $l, l' \in \Loc_\Prog$, $t,t' \in \T_\Prog$, $s,s' \in \Sigma$, and $c'
%     = (l', t', s')$ as well as $c = (l, t, s)$. Let $t = (\_, \_, \tau, \eta,
%     \_)$. When $c'$ is reachable from $c$ this implies: 
%     \begin{enumerate}
%         \item $s \models \tau$
%     \end{enumerate}
%     \begin{proof}
%     \end{proof}

% \begin{lemma}
%     If a 
% \end{lemma}

\subsection{Costs and Runtime-complexity}
The cost of a run (or total reward for the Markov decision process) is
the sum of costs for every transition taken during a run. 

\subsection{Runtime-complexity}
% The cost of a run (or total reward for the Markov decision process) is
% the sum of costs for every transition taken during a run. 

\begin{definition}[Costs]
    For a run $c_0c_1\dots{}\in \runs^\Prog$ the \textit{costs} of $\Cost :
    \runs \rightarrow \overline{\N}$ is a random variable with 
    \begin{equation*}
        \Cost(\Prog)(c_0c_1\dots) = |\set{\kappa_{t_i}}{c_i = (l_i, t_i, s_i) \text{
            and } t_i \neq t_\bot}|
    \end{equation*}
\end{definition}

% \begin{definition}[Costs]
%     For a run $c_0c_1\dots{}\in \runs^\Prog$ the \textit{costs} of $\Cost :
%     \runs \rightarrow \overline{\N}$ is a random variable with 
%     \begin{equation*}
%         \Cost(\Prog)(c_0c_1\dots) = |\set{\kappa_{t_i}}{c_i = (l_i, t_i, s_i) \text{
%             and } t_i \neq t_\bot}|
%     \end{equation*}
% \end{definition}

\begin{definition}[Expected Costs]
    For a scheduler $\scheduler$ and a start location $s_0 \in \Sigma$ the
    expected costs $\Cost(\Prog)_{\scheduler,s_0}$ of a program $\Prog$ is
    defined as the expected value of the random variable $\Cost(\Prog)$:
    \begin{equation*}
        \Cost_{\scheduler,s_0}(\Prog) = \ESs(\Cost(\Prog))
    \end{equation*}
\end{definition}

% \begin{definition}[Expected Costs]
%     For a scheduler $\scheduler$ and a start location $s_0 \in \Sigma$ the
%     expected costs $\Cost(\Prog)_{\scheduler,s_0}$ of a program $\Prog$ is
%     defined as the expected value of the random variable $\Cost(\Prog)$:
%     \begin{equation*}
%         \Cost_{\scheduler,s_0}(\Prog) = \ESs(\Cost(\Prog))
%     \end{equation*}
% \end{definition}

\begin{example}
\end{example}

% \begin{example}
% \end{example}

\begin{definition}[Runtime complexity]

\begin{definition}[Runtime complexity]\label{def:runtime_complexity}

\begin{definition}[Expected runtime complexity, \acrshort{past}]

\begin{definition}[Expected runtime complexity, \acrshort{past}]\label{def:past}

    The \gls{koat}, the complexity analysis tool developed at RWTH University,
    was recently extended to the analysis probabilistic integer programs, with
    the goal to find tight expected runtime-complexity bounds. 
    At the time of writing \gls{koat} does control-flow-refinement via partial
    evaluation by calling the tool iRankFinder externally, making it slow in the
    process and hard to maintain. iRankFinder cannot handle probabilistic
    program, making it impossible to be used for their analysis.
    This thesis applies the techniques of partial evaluation to probabilistic
    programs. A partially evaluated probabilistic integer programs is proven to
    have the same expected runtime-complexity as its original, making this
    technique useful when searching tight expected runtime-complexity bounds on
    probabilistic integer program. 
    The evaluation is shown to work on a Sub-SCC level similar to the original
    the old control-flow-refinement. 
    The newly developed algorithms are implemented natively in \gls{koat} and
    integrated into the existing analysis algorithms using Sub-SCC evaluation.
    The native implementation turns out to be faster on classical integer
    programs, making it a good candidate to replace the old implementation in
    the future. Furthermore, the implementation is shown to improve the found
    expected runtime-bounds found for some probabilistic integer programs as
    well.