-\subsection{Deriving refresh rates}\label{sec:deriving_refresh_rates}
-Based on these refresh rates, the system can automatically derive refresh rates for composed \gls{MTASK} expressions using $\mathcal{R}$.
-We use the operator $\cap_{\textit{safe}}$ to compose refresh ranges.
-When the ranges overlap the result is the overlapping range.
-Otherwise, the result is the range with the lowest numbers.
-The rationale is that subtasks should not be delayed longer than their refresh range.
-Evaluating a task earlier should not change its result but can consume more energy.
-
-\begin{align}
- \cap_{\textit{safe}} :: \refreshrate{\mathit{Int}}{\mathit{Int}} \; \refreshrate{\mathit{Int}}{\mathit{Int}} & \shortrightarrow \refreshrate{\mathit{Int}}{\mathit{Int}} & \notag \\
- R_1 \cap_{\textit{safe}} R_2 & = R_1 \cap R_2 & \text{if } R_1 \cap R_2 \neq \emptyset \\
- \refreshrate{l_1}{h_1} \cap_{\textit{safe}} \refreshrate{l_2}{h_2} & = \refreshrate{l_2}{h_2} & \text{if } h_2 < l_1 \\
- R_1 \cap_{\textit{safe}} R_2 & = R_1 & \text{otherwise}
-\end{align}
-
-\begin{align}
- \mathcal{R} :: (\mathit{MTask}~v~a) & \shortrightarrow \refreshrate{\mathit{Int}}{\mathit{Int}} \notag \\
- \mathcal{R} (t_1~{.||.}~t_2) & = \mathcal{R}(t_1) \cap_{\textit{safe}} \mathcal{R}(t_2) \label{R:or} \\
- \mathcal{R}(t_1~{.\&\&.}~t_2) & = \mathcal{R}(t_1) \cap_{\textit{safe}} \mathcal{R}(t_2) \label{R:and}\\
- \mathcal{R}(t_1~{>\!\!>\!|.}~t_2) & = \mathcal{R}(t_1) \label{R:seq} \\
- \mathcal{R}(t~{>\!\!>\!=.}~f) & = \mathcal{R}(t) \label{R:bind} \\
- \mathcal{R}(t~{>\!\!>\!\!*.}~[a_1 \ldots a_n]) & = \mathcal{R}(t) \label{R:step} \\
- \mathcal{R}(\mathit{rpeat}~t) & = \refreshrate{0}{0} \label{R:rpeat} \\
- \mathcal{R}(\mathit{rpeatEvery}~d~t) & = \refreshrate{0}{0} \label{R:rpeatevery} \\
- \mathcal{R}(delay~d) & = \refreshrate{d}{d} \label{R:delay} \\
- \mathcal{R}(t) & =
- \left\{%
+\subsection{Deriving rewrite rates}\label{sec:deriving_rewrite_rates}
+Based on these default rewrite rates, the system automatically derives rewrite rates for composed \gls{MTASK} expressions using the function $\mathcal{R}$ as shown in \cref{equ:r}.
+
+\begin{equ}
+ \begin{align}
+ \mathcal{R} :: (\mathit{MTask}~v~a) & \shortrightarrow \rewriterate{\mathit{Int}}{\mathit{Int}} \notag \\
+ \mathcal{R} (t_1~{.||.}~t_2) & = \mathcal{R}(t_1) \cap_{\textit{safe}} \mathcal{R}(t_2) \label{R:or} \\
+ \mathcal{R}(t_1~{.\&\&.}~t_2) & = \mathcal{R}(t_1) \cap_{\textit{safe}} \mathcal{R}(t_2) \label{R:and}\\
+ \mathcal{R}(t~{>\!\!>\!\!*.}~[a_1 \ldots a_n]) & = \mathcal{R}(t) \label{R:step} \\
+ \mathcal{R}(\mathit{rpeat}~t~\mathit{start}) & =
+ \left\{\begin{array}{ll}
+ \mathcal{R}(t) & \text{if $t$ is unstable}\\
+ \rewriterate{r_1-\mathit{start}}{r_2-\mathit{start}} & \text{otherwise}\\
+ \end{array}\right.\\
+ \mathcal{R} (\mathit{waitUntil}~d) & = \rewriterate{e-\mathit{time}}{e-\mathit{time}}\label{R:delay}\\
+ \mathcal{R} (t) & =
+ \left\{%
+ \begin{array}{ll}
+ \rewriterate{\infty}{\infty}~& \text{if}~t~\text{is Stable} \\
+ \rewriterate{r_l}{r_u} & \text{otherwise}
+ \end{array}
+ \right.\label{R:other}
+ \end{align}
+ \caption{Function $\mathcal{R}$ for deriving refresh rates.}%
+ \label{equ:r}
+\end{equ}
+
+\subsubsection{Parallel combinators}
+For parallel combinators, the \emph{or}-combinator (\cleaninline{.\|\|.}) in \cref{R:or} and the \emph{and}-combinator (\cleaninline{.&&.}) in \cref{R:and}, the safe intersection (see \cref{equ:safe_intersect}) of the rewrite rates is taken to determine the rewrite rate of the complete task.
+The conventional intersection does not suffice here because it yields an empty intersection when the intervals do not overlap.
+In that case, the safe intersection behaves will return the range with the lowest numbers.
+The rationale is that subtasks should not be delayed longer than their rewrite range.
+Evaluating a task earlier should not change its result but just consumes more energy.
+
+\begin{equ}
+ \[
+ X \cap_{\textit{safe}} Y = \left\{%