Index: /reasoner/consTranslation.tex
===================================================================
--- /reasoner/consTranslation.tex	(revision 199)
+++ /reasoner/consTranslation.tex	(revision 200)
@@ -18,11 +18,9 @@
 
 \grayPara{
-\begin{gather*}
-   \patternDerivation{T \text{ } v = deflt\IVML{;}}{access(v) = deflt} \\
-   \patternDerivation{\IVML{annotate } a = deflt \IVML{ to} *\IVML{;} T \text{ } v\IVML{;}}{access(v.a) = deflt} \\
-\end{gather*}
-}
-
-In Algorithm \ref{algTranslateDeclaration}, we apply the translation patterns above: Let $v$ be a variable with default value expression $deflt$. The first transformation pattern above turns $deflt$ into an assignment constraint. If $v$ is nested in a compound or a sequence, a qualified access expression for $v$ is required in the resulting constraint. We indicate this in terms of the $access(e)$ function on the right side. $access(e)$ returns $e$ if $e$ is already (an accessor expression based on) a top-level variable. $access(e)$ turns $e$ into an accessor (path) expression based on a respective top-level variable. The second pattern refers to annotations. As introduced in Section \ref{sectNotationVarDecls}, annotations are variables denoting an orthogonal configuration dimension of 'ordinary' variables. Thus, an annotation $a$ is translated in the context of the underlying 'ordinary' variable named $v$ in the pattern, i.e., requires  a qualification based on $v$. In Algorithm \ref{algTranslateDeclaration}, we will focus on the first transformation pattern. As stated above, we will defer more complex translations to later sections, e.g., annotations to Section \ref{sectAnnotationDefaults}, as these algorithms can then re-use the more generic translation of variables discussed here.
+   \patternDerivationLabel{T \text{ } v = deflt\IVML{;}}{access(v) = deflt}{forVarDecl}
+   \patternDerivationLabel{\IVML{annotate } a = deflt \IVML{ to} *\IVML{;} T \text{ } v\IVML{;}}{access(v.a) = deflt}{forVarDeclAnnotation}
+}
+
+In Algorithm \ref{algTranslateDeclaration}, we apply the translation patterns above: Let $v$ be a variable with default value expression $deflt$. Pattern \ref{forVarDecl} turns $deflt$ into an assignment constraint. If $v$ is nested in a compound or a sequence, a qualified access expression for $v$ is required in the resulting constraint. We indicate this in terms of the $access(e)$ function on the right side. $access(e)$ returns $e$ if $e$ is already (an accessor expression based on) a top-level variable. $access(e)$ turns $e$ into an accessor (path) expression based on a respective top-level variable. Pattern \ref{forVarDeclAnnotation} targets annotations. As introduced in Section \ref{sectNotationVarDecls}, annotations are variables denoting an orthogonal configuration dimension of 'ordinary' variables. Thus, an annotation $a$ is translated in the context of the underlying 'ordinary' variable named $v$ in the pattern, i.e., requires  a qualification based on $v$. In Algorithm \ref{algTranslateDeclaration}, we will focus on the first transformation pattern. As stated above, we will defer more complex translations to later sections, e.g., annotations to Section \ref{sectAnnotationDefaults}, as these algorithms can then re-use the more generic translation of variables discussed here.
 
 Algorithm \ref{algTranslateDeclaration} translates all constraints related to a given variable declaration $d$ and its configuration variable $v$, which may be $\undef$ for type-only translations\footnote{\label{fnVariableNull}When initializing a configuration or creating constraints from a  complex constant value expression, variables may not already be in place in all cases.}. Default value assignment constraints created in Algorithm \ref{algTranslateDeclaration} are stored either in the global set for default constraints $\defaultConstraints$ or the set for deferred default constraints $\deferredDefaultConstraints$. As the type of $v$ may be a complex type such as a compound, Algorithm \ref{algTranslateDeclaration} delegates these translations to more specialized algorithms, which use Algorithm \ref{algTranslateDeclaration} recursively. As thereby the translation context changes, the involved algorithms incrementally adjust the access expression $ca$ and the variable mapping $\variableMapping$. 
@@ -78,17 +76,21 @@
 \subsection{Derived types}\label{sectDerivedTypes}
 
-As introduced in Section \ref{sectNotationDerivedTypes}, a derived datatype $t$ is defined as a restriction or an alias of its base type $base(t)$. A derived type $t$ is a type restriction of $base(t)$, if $t$ defines restricting constraints over $base(t)$ using the local variable $decl(t)$ representing $t$. Type $t$ is a type alias, i.e., a type with the same constraints as the base type but different type name, if $constraints(t) = \emptySet$. The base type of a derived type can in particular be another derived type, but, of course, also any other IVML type. If a variable $v$ is declared to be of a derived type $t$, all constraints defined for $t$ over $base(t)$ must hold for $v$. In particular, if $base(t)$ is a derived type, all constraints over all base types $allBase(t)$ of $t$ must hold transitively. Whether these constraints are fullfilled depends on the actual value of $v$. 
-
-The constraint translation follows this chained type structure and instantiates all constraints defined along the nesting as shown in the following translation pattern. 
-
-\grayPara{
-\begin{gather*}
-    \patternDerivation{\IVML{typedef } t_i \IVML{ with }(c_i); T\ v\IVML{;}}{\bigcup_{t_i \in allBase(T)} \varSubstitution{c_i}{decl(t_i)=deref(t_i, v), \variableMapping}}
-\end{gather*}
-}
-
-Given a variable $v$ of derived type $T$, all constraints induced by the derived type and all its base types are turned into instantiated constraints. During instantiation, we appy a substitution, which replaces the respective local variable by $v$ or an accessor expression to $v$ and, if applicable, any cross-referenced variables in $\variableMapping$. It is important to mention that just substituting the respective local variable by $v$ is not sufficient, as also reference types can be used as base type. A reference type requires then de-referencing of $v$, e.g., to permit access to the slots of a compound variable. This is indicated in the translation pattern by the function $deref(t, v)$, which either dereferences $v$ with respect to $t$ or returns $v$ if no de-referencing is needed.
-
-For a given variable $v$ (in terms of declaration $d$ and for technical reasons its type $t$), Algorithm \ref{algTranslateDerivedDatatypeConstraints} instantiates all constraints defined for all dereferenced transitive base types. However, we must consider whether we perform this instantiation for a container variable\footnote{The actual implementation receives the iterator variable causing the creation of the quantifier constraint and the parent model element for creating the constraints.}. If $v$ is a container variable, we create an all-quantifying constraint over all container elements, whereby the iterator variable $i$ of the quantifier substitutes $decl(t)$. If the derived type $t$ is defined based on some reference type, we must dereference the iterator variable $i$ appropriately. If $v$ is not a container variable, we substitute $decl(t)$ by the actual variable $d$. It is important to note that this substitution is transitive if $d$ is a compound slot, i.e., if $d$ is also mentioned in $\variableMapping$, the previously collected compound accessor for $d$ (in Algorithm \ref{algTranslateCompoundDeclaration}) is used to substitute $decl(t)$. The respective composite expression for $i$ is created through the function $deref(t, ex)$ shown below. The resulting constraints are stored in the set of top-level constraints $\topLevelConstraints$ as the variables in the resulting constraints are then fully qualified and in IVML derived types can only be defined on top level. % shall not make a difference for nested variables as they are already initialized
+As introduced in Section \ref{sectNotationDerivedTypes}, a derived datatype $t$ is defined as a restriction or an alias of its base type $base(t)$. A derived type $t$ is a type restriction of $base(t)$, if $t$ defines constraints over $base(t)$ using the local variable $decl(t)$ of type $t$. Type $t$ is a type alias, i.e., a type with the same constraints as the base type but different type name, if $constraints(t) = \emptySet$. In particular, $base(t)$ can be another derived type. If variable $v$ is of derived type $t$, all constraints defined for $t$ must hold for $v$. Moreover, if $base(t)$ is a derived type, all constraints defined for all base types $allBase(t)$ of $t$ must hold transitively. %Whether these constraints are fullfilled depends on the actual value of $v$. 
+
+The constraint translation follows this chained structure of base types and instantiates all constraints as shown in the following translation patterns:
+
+\grayPara{
+    \patternDerivationLabel{\IVML{typedef } T \IVML{ with }(c); T\ v\IVML{;}}{\nonumber\\\bigcup_{\begin{matrix}\scriptstyle u\ \in\ \set{t\ \cup\ allBase(T)},\\\scriptstyle c\ \in\ constraints(u)\end{matrix}} \varSubstitution{c}{decl(u)=deref(u, v), \variableMapping}}{formDerivedDatatypeConstraints}
+    \patternDerivationLabel{\IVML{typedef } containerOf(T) \IVML{ with }(c); T\ v\IVML{;}}{\nonumber\\\bigcup_{\begin{matrix}\scriptstyle u\ \in\ \set{t\ \cup\ allBase(T)},\\\scriptstyle c\ \in\ constraints(u)\end{matrix}} \varSubstitution{v\rightarrow\IVML{forall(i:}c}{decl(u)=deref(u, i), \variableMapping}\IVML{)}}{formDerivedDatatypeConstraintsContainer}
+}
+
+As shown in Pattern \ref{formDerivedDatatypeConstraints}, given a variable $v$ of derived type $T$, all constraints induced by the derived type and all its base types are turned into instantiated constraints. During instantiation, we appy a substitution, which replaces the local variable of the respective derived type by $v$ or an accessor expression to $v$ as well as any cross-referenced variables in $\variableMapping$. However, substituting the respective local variable by $v$ is not sufficient, as also reference types can be used as base type. A reference type requires de-referencing, e.g., to permit access to the slots of a compound variable. This is indicated in the translation pattern by the function $deref(t, v)$, which either dereferences $v$ with respect to $t$ or returns $v$ if no de-referencing is needed. For container variables, we must all-quantfy the constraint, whereby the iterator variable $i$ of the quantifier substitutes $decl(t)$ as displayed in Pattern \ref{formDerivedDatatypeConstraintsContainer}.
+
+The dereferencing operation\footnote{The implementation dereferences in an iterative manner when explicitly adding a variable mapping in addition to $\variableMapping$ to the substitution visitor.} takes a type $t$ and a basis expression $ex$. For each reference base type in the chain of base types, it adds a call of the IVML dereferencing operation \IVML{refBy} around $ex$. For other types, $deref$ just returns $ex$.
+%
+$$deref(t, ex)=\begin{cases} deref(base(t), ex), & \text{if } isDerived(t) \wedge\\&\ \neg isReference(base(t)) \\ \IVML{refBy}(deref(base(base(t)), ex)), & \text{if } isDerived(t) \wedge \\&\ isReference(base(t))\\ ex, & \text{else}\\\end{cases}$$
+%
+
+Algorithm \ref{algTranslateDerivedDatatypeConstraints} instantiates all constraints defined for all dereferenced transitive base types of declaration $d$ and its (actual) type $t$. First, we collect in line \ref{algTranslateDerivedDatatypeConstraintsCollectConstraints} all constraints for $d$ considering chained derived types. Lines \ref{algTranslateDerivedDatatypeConstraintsTranslateCollectionStart}-\ref{algTranslateDerivedDatatypeConstraintsTranslateCollectionEnd} realize Pattern \ref{formDerivedDatatypeConstraintsContainer}, i.e., if $v$ is a container variable, we create an all-quantifying constraint over all container elements and substitute $decl(t)$ with the iterator variable\footnote{The actual implementation receives the iterator variable causing the creation of the quantifier constraint and the parent model element for creating the constraints.} $i$. Lines \ref{algTranslateDerivedDatatypeConstraintsTranslateOtherStart}-\ref{algTranslateDerivedDatatypeConstraintsTranslateOtherEnd} realize Pattern \ref{formDerivedDatatypeConstraints}, i.e., if $v$ is not a container variable, we substitute $decl(t)$ by $d$. It is worth mentioning that the substitutions are transitive if $d$ is a compound slot, i.e., if $d$ is a key in $\variableMapping$, its compound accessor substitutes $decl(t)$. The resulting constraints are stored as top-level constraints $\topLevelConstraints$ as IVML derived types can only be defined on top-level. % shall not make a difference for nested variables as they are already initialized
 
 \begin{algorithm}[H]
@@ -96,18 +98,14 @@
   \KwIn{declaration $d$, type $t$}
   \KwData{derived type constraints $\topLevelConstraints$}
-  $cs \assng \bigcup_{t \in deref(allBase(t))} constraints(t)$\;
-  \uIf{$isContainer(t)$}{
+  $cs \assng \bigcup_{t \in deref(allBase(t))} constraints(t)$\;\label{algTranslateDerivedDatatypeConstraintsCollectConstraints}
+  \uIf{$isContainer(t)$}{\label{algTranslateDerivedDatatypeConstraintsTranslateCollectionStart}
       $cs \assng \setWith{\createConstraint{\varSubstitutionOtherVarMapping{\IVML{forAll(i:}c\IVML{)}}{decl(t)=deref(t, i)}}}{c\in cs}$\;
-  }\Else{
-      $cs \assng \setWith{\createConstraint{\varSubstitutionOtherVarMapping{c}{decl(t)=deref(t, v)}}}{c\in cs}$\;
-  }
+  }\Else{\label{algTranslateDerivedDatatypeConstraintsTranslateCollectionEnd}\label{algTranslateDerivedDatatypeConstraintsTranslateOtherStart}
+      $cs \assng \setWith{\createConstraint{\varSubstitutionOtherVarMapping{c}{decl(t)=deref(t, d)}}}{c\in cs}$\;
+  }\label{algTranslateDerivedDatatypeConstraintsTranslateOtherEnd}
   $add(\topLevelConstraints, cs, true, \undef)$\;
  \caption{Translating constraints for derived types (\IVML{translateDerivedDatatypeConstraints}).}\label{algTranslateDerivedDatatypeConstraints}
 \end{algorithm}
 %
-The dereferencing operation\footnote{The actual implementation performs the dereferencing in an iterative manner when explicitly adding a variable mapping in addition to $\variableMapping$ to the substitution visitor.} for Algorithm \ref{algTranslateDerivedDatatypeConstraints} takes a type $t$ and a basis expression $ex$. For each reference base type in the chain of base types, it adds a call of the (internal) IVML dereferencing operation \IVML{refBy} around $ex$ or the recursively built up expression to $ex$. Other types than derived types immediately lead to $ex$ as result.
-%
-$$deref(t, ex)=\begin{cases} deref(base(t), ex), & \text{if } isDerived(t) \wedge \neg isReference(base(t)) \\ \IVML{refBy}(deref(base(base(t)), ex)), & \text{if } isDerived(t) \wedge isReference(base(t))\\ ex, & \text{else}\\\end{cases}$$
-%
 \subsection{Compound types}\label{sectCompoundDefaults}
 
@@ -115,11 +113,9 @@
 
 \grayPara{
-\begin{gather*}
-    \patternDerivation{\IVML{compound } C \IVML{\{} T s = deflt\IVML{;\}; } C\ v \IVML{;}}{\varSubstitution{s = deflt}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}\\
-    \patternDerivation{\IVML{compound } C \IVML{\{} T s\IVML{; } c(s)\IVML{\}; } C\ v \IVML{;}}{\varSubstitution{c(s)}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}\\
-    \patternDerivation{\IVML{compound } C \IVML{\{} T s\IVML{; eval \{} c(s)\IVML{\}\}; } C\ v \IVML{;}}{\varSubstitution{c(s)}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}\\
-    \patternDerivation{\IVML{compound } C \IVML{\{} T s\IVML{; assign (\ldots) to \{} c(s)\IVML{\}\}; } C\ v \IVML{;}}{\\\varSubstitution{c(s)}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}\\
-    \patternDerivation{\IVML{compound } C \IVML{\{} T s \IVML{\}; }  C\  v \IVML{; } c(v.s)\IVML{;}}{\varSubstitution{c(v.s)}{\variableMapping}}\\
-\end{gather*}
+    \patternDerivation{\IVML{compound } C \IVML{\{} T s = deflt\IVML{;\}; } C\ v \IVML{;}}{\varSubstitution{s = deflt}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}
+    \patternDerivation{\IVML{compound } C \IVML{\{} T s\IVML{; } c(s)\IVML{\}; } C\ v \IVML{;}}{\varSubstitution{c(s)}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}
+    \patternDerivation{\IVML{compound } C \IVML{\{} T s\IVML{; eval \{} c(s)\IVML{\}\}; } C\ v \IVML{;}}{\varSubstitution{c(s)}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}
+    \patternDerivation{\IVML{compound } C \IVML{\{} T s\IVML{; assign (\ldots) to \{} c(s)\IVML{\}\}; } C\ v \IVML{;}}{\nonumber\\\varSubstitution{c(s)}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}
+    \patternDerivation{\IVML{compound } C \IVML{\{} T s \IVML{\}; }  C\  v \IVML{; } c(v.s)\IVML{;}}{\varSubstitution{c(v.s)}{\variableMapping}}
 }
 
@@ -255,8 +251,6 @@
 
 \grayPara{
-\begin{gather*}
-    \patternDerivation{\IVML{containerOf(}T\IVML{) } v\IVML{;}}{\\\bigcup_{t~\in~usedTypes(v),~ c~\in~constraints(t)}f(v, t)\rightarrow \IVML{forall(w:}\varSubstitution{c(x)}{x=\IVML{w}, \IVMLself{}=\IVML{w}, \variableMapping}\IVML{)}}\\
+    \patternDerivation{\IVML{containerOf(}T\IVML{) } v\IVML{;}}{\nonumber\\\bigcup_{t~\in~usedTypes(v),~ c~\in~constraints(t)}f(v, t)\rightarrow \IVML{forall(w:}\varSubstitution{c(x)}{x=\IVML{w}, \IVMLself{}=\IVML{w}, \variableMapping}\IVML{)}}
     \patternDerivation{\IVML{containerOf(}T\IVML{) } v\IVML{;}~c(v)\IVML{;}}{\varSubstitution{c(v)}{\variableMapping}}
-\end{gather*}
 }
 
@@ -385,8 +379,6 @@
 
 \grayPara{
-\begin{gather*}
-   \patternDerivation{\IVML{annotate } a = deflt \IVML{ to } *\IVML{;} T \text{ } v\IVML{;}}{access(v.a) = deflt}\\
-   \patternDerivation{\IVML{assign (} a = deflt \IVML{) to \{} T~v\IVML{;} \IVML{ assign} \ldots \IVML{\}}}{access(v.a) = deflt \ldots}\\
-\end{gather*}
+   \patternDerivation{\IVML{annotate } a = deflt \IVML{ to } *\IVML{;} T \text{ } v\IVML{;}}{access(v.a) = deflt}
+   \patternDerivation{\IVML{assign (} a = deflt \IVML{) to \{} T~v\IVML{;} \IVML{ assign} \ldots \IVML{\}}}{access(v.a) = deflt \ldots}
 }
 
@@ -486,10 +478,8 @@
 
 \grayPara{
-\begin{gather*}
-   \patternDerivation{\IVML{Constraint}~v = ex\IVML{;}}{\varSubstitution{ex}{\variableMapping}}\\
-   \patternDerivation{\IVML{Compound}~C =~\IVML{\{Constraint } s = ex\IVML{;} \IVML{\}}\IVML{; } C v\IVML{;}}{\varSubstitution{ex}{\IVMLself{}=v, \variableMapping}}\\
-   \patternDerivation{\IVML{containerOf(Constraint)}~v = \IVML{\{}ex_1 , \ldots, ex_n\IVML{\}}\IVML{;}}{\varSubstitution{ex_1}{\variableMapping}, \ldots, \varSubstitution{ex_n}{\variableMapping}}\\
-   \patternDerivation{\IVML{Compound}~C =~\IVML{\{containerOf(Constraint) } s = \IVML{\{}ex_1 , \ldots, ex_n\IVML{\}}\IVML{;} \IVML{\}}\IVML{; } C v\IVML{;}\\}{\varSubstitution{ex_1}{\IVMLself{}=v, \variableMapping}, \ldots, \varSubstitution{ex_n}{\IVMLself{}=v, \variableMapping}}\\
-\end{gather*}
+   \patternDerivation{\IVML{Constraint}~v = ex\IVML{;}}{\varSubstitution{ex}{\variableMapping}}
+   \patternDerivation{\IVML{Compound}~C =~\IVML{\{Constraint } s = ex\IVML{;} \IVML{\}}\IVML{; } C v\IVML{;}}{\varSubstitution{ex}{\IVMLself{}=v, \variableMapping}}
+   \patternDerivation{\IVML{containerOf(Constraint)}~v = \IVML{\{}ex_1 , \ldots, ex_n\IVML{\}}\IVML{;}}{\varSubstitution{ex_1}{\variableMapping}, \ldots, \varSubstitution{ex_n}{\variableMapping}}
+   \patternDerivation{\IVML{Compound}~C =~\IVML{\{containerOf(Constraint) } s = \IVML{\{}ex_1 , \ldots, ex_n\IVML{\}}\IVML{;} \IVML{\}}\IVML{; } C v\IVML{;}\nonumber\\}{\varSubstitution{ex_1}{\IVMLself{}=v, \variableMapping}, \ldots, \varSubstitution{ex_n}{\IVMLself{}=v, \variableMapping}}
 }
 
@@ -527,8 +517,6 @@
 
 \grayPara{
-\begin{gather*}
-   \patternDerivation{v = \IVML{\{}\ldots, ex,\ldots\IVML{\}}}{\ldots, \varSubstitution{ex}{\variableMapping}, \ldots}\\
-   \patternDerivation{v = \IVML{\{} s = ex \IVML{\}}}{\varSubstitution{ex}{\variableMapping}}\\
-\end{gather*}
+   \patternDerivation{v = \IVML{\{}\ldots, ex,\ldots\IVML{\}}}{\ldots, \varSubstitution{ex}{\variableMapping}, \ldots}
+   \patternDerivation{v = \IVML{\{} s = ex \IVML{\}}}{\varSubstitution{ex}{\variableMapping}}
 }
 
Index: /reasoner/mainAlgorithms.tex
===================================================================
--- /reasoner/mainAlgorithms.tex	(revision 199)
+++ /reasoner/mainAlgorithms.tex	(revision 200)
@@ -142,12 +142,10 @@
 
 \grayPara{
-\begin{gather*}
-   \patternDerivation{T \text{ } v\IVML{;} c(v)\IVML{;}}{c(v)} \\
-   \patternDerivation{T \text{ } v\IVML{; assign (\ldots) to \{} c(v)\IVML{\};}}{c(v)} \\
-   \patternDerivation{T \text{ } v\IVML{; eval \{} c(v)\IVML{\};}}{c(v)} \\
-\end{gather*}
+   \patternDerivationLabel{T \text{ } v\IVML{;} c(v)\IVML{;}}{c(v)}{formTopLevelConstraint}
+   \patternDerivationLabel{T \text{ } v\IVML{; assign (\ldots) to \{} c(v)\IVML{\};}}{c(v)}{formTopLevelAssign}
+   \patternDerivationLabel{T \text{ } v\IVML{; eval \{} c(v)\IVML{\};}}{c(v)}{formTopLevelEval}
 }
 
-Top-level constraints are defined using top-level variables, which are already fully qualified so no translation is needed, because these variables already represent complete access expressions. This is indicated by the first translation pattern. Similarly, constraints defined in top-level (nested) annotation assignments are already qualified and can be directly used for reasoning as indicated by the second translation pattern. Moreover, annotation assignments represent constraints that assign values to annotations of contained declared (top-level) variables. Similarly, these constraints can be used in reasoning without translation. This is implied in the second translation pattern. Also the variables used in constraints listed in (nested) top-level eval-blocks are fully qualified. In contrast, the evaluation of constraints in eval blocks must be prioritized over the other (top-level) constraints~\cite{IVML-LS}.
+Top-level constraints are defined using top-level variables, which are already fully qualified so no translation is needed, because these variables already represent complete access expressions. This is indicated by Pattern \ref{formTopLevelConstraint}. Similarly, constraints defined in top-level (nested) annotation assignments are already qualified and can be directly used for reasoning as indicated by Pattern \ref{formTopLevelAssign}. Moreover, annotation assignments represent constraints that assign values to annotations of contained declared (top-level) variables. Similarly, these constraints can be used in reasoning without translation. This is implied in Pattern \ref{formTopLevelAssign}. Also the variables used in constraints listed in (nested) top-level eval-blocks are fully qualified. In contrast, as shown in Pattern \ref{formTopLevelEval} the evaluation of constraints in eval blocks must be prioritized over the other (top-level) constraints~\cite{IVML-LS}.
 
 To prioritize the constraints, the constraint translation uses four global sequences, which are populated during the constraint translation and, finally, added to the constraint $base$ (also a sequence). In more details, we maintain:
Index: /reasoner/notation.tex
===================================================================
--- /reasoner/notation.tex	(revision 199)
+++ /reasoner/notation.tex	(revision 200)
@@ -157,7 +157,5 @@
 
 \grayPara{
-\begin{gather*}
-   \patternDerivation{T \text{ } v = deflt\IVML{;}}{v = deflt} \\
-\end{gather*}
+   \nonumber\patternDerivation{T \text{ } v = deflt\IVML{;}}{v = deflt}
 }
 
Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 199)
+++ /reasoner/reasoner.tex	(revision 200)
@@ -58,7 +58,8 @@
 \newcommand\tabAlgLines[3]{Alg.\ref{#1} (\ref{#2}-\ref{#3})}
 \newcommand\tabAlgFollow[0]{ $\rightarrow$ }
-\newcommand\grayPara[1]{\noindent\adjustbox{bgcolor=gray!20,minipage=[t]{\linewidth}}{#1}\linebreak}
+\newcommand\grayPara[1]{\noindent\adjustbox{bgcolor=gray!20,minipage=[t]{\linewidth}}{\begin{gather}#1\nonumber\end{gather}}\linebreak}
 \newcommand\patternDerivationSymbol[0]{\leadsto}
-\newcommand\patternDerivation[2]{#1 \patternDerivationSymbol #2}
+\newcommand\patternDerivation[2]{#1 \patternDerivationSymbol #2\\}
+\newcommand\patternDerivationLabel[3]{#1 \patternDerivationSymbol #2\label{#3}\\}
 
 \let\emph\relax % there's no \RedeclareTextFontCommand