Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 139)
+++ /reasoner/reasoner.tex	(revision 140)
@@ -255,5 +255,5 @@
 In some cases, constraints cannot be created in terms of a single step, i.e., sub-expressions are created iteratively. To indicate this, we denote the creation of an expression by $\createExpression{expr}$, e.g., $\createExpression{\IVML{add}(x, 25)}$ for the IVML expression \IVML{x + 25}. When creating expressions, in particular in an incremental fashion, sometimes a temporary (local) IVML variable is needed, e.g., for an IVML let-expression or a container iterator. We state the creation of such a variable by $\IVMLMeta{var}(t)$, i.e., request the creation of a temporary variable\footnote{We don't care for the variable name in this document.} of type $t$. For a variable $v=\IVMLMeta{var}(t)$ holds $isLocal(v) = true$. 
 
-Before reasoning over the constraints given in an IVML project, several kinds of constraints must be transformed, in particular to instantiate constraints defined for types through qualifying access expressions based on top-level variables. To illustrate the transformations performed by an algorithm in this document, we apply constraint transformation patterns. A \emph{constraint transformation pattern} indicates how a certain IVML model fragment is instantiated to a corresponding constraint given in IVML constraint notation rather than the algorithm notation for creating constraints introduced in this section. The model fragment is given on the left side of the derivation symbol $\patternDerivationSymbol$, the corresponding constraint on the right side of $\patternDerivationSymbol$. In such a pattern, variable parts are given in italics to indicate the information flow between both sides. Constant parts are given in normal font, IVML syntax in \IVML{teletype}. One or more transformation patterns are displayed in a gray box. For example, the pattern below indicates that an IVML declaration for variable $v$ (with type $T$ and default value expression $deflt$) is translated into an assignment constraint, which assigns the (value of the) default expression $deflt$ to $v$.
+Before reasoning over the constraints given in an IVML project, several kinds of constraints must be transformed, in particular to instantiate constraints defined for types through qualifying access expressions based on top-level variables. To illustrate the transformations performed by an algorithm in this document, we apply constraint transformation patterns. A \emph{constraint transformation pattern} indicates how a certain IVML model fragment is instantiated to a corresponding constraint given in IVML constraint notation rather than the algorithm notation for creating constraints introduced in this section. The model fragment acting as prerequisite is given on the left side of the derivation symbol $\patternDerivationSymbol$, the corresponding constraint on the right side of $\patternDerivationSymbol$. In such a pattern, variable parts are given in italics to indicate the information flow between both sides. Constant parts are given in normal font, IVML syntax in \IVML{teletype}. One or more transformation patterns are displayed in a gray box. For example, the pattern below indicates that an IVML declaration for variable $v$ (with type $T$ and default value expression $deflt$) is translated into an assignment constraint, which assigns the (value of the) default expression $deflt$ to $v$.
 
 \grayPara{
@@ -647,12 +647,12 @@
 As introduced in Section \ref{sectNotationVarDecls}, an IVML variable declaration consists of a type, a variable name and an optional default value expression. At its core, the translation of a variable declaration creates an assignment constraint for the default value expressions and instantiates all constraints defined by the variable type. If known, the translation considers the actual type of the variable defined by the configured value, which may in particular have a refined (compatible) compound type and, thus, a refined set of constraint. However, due to the complex structure of IVML types, identifying the constraints defined by a type may require a transitive or even recursive traversal over refined or underlying base types, e.g., in case of a typedef or a container.
 
-Let $v$ be a given variable with default value expression $deflt$, then the first transformation pattern below turns $default(v)$ into an assignment constraint. If $v$ is nested in a compound or a sequence, a qualified access expression is required. In the transformation pattern, we indicate this by the access expression $ca.$ on the right side, which is empty for top-level variables. As introduced in Section \ref{sectNotationVarDecls}, annotations are variables allowing an an orthogonal configuration dimension for 'ordinary' variables. Thus, an annotation can be translated similarly to an ordinary variable, but require a qualification through the respective ordinary variable as indicated in the second transformation pattern.
-
 \grayPara{
 \begin{gather*}
    \patternDerivation{T \text{ } v = deflt\IVML{;}}{ca.v = deflt} \\
-   \patternDerivation{\IVML{annotate } a = deflt \IVML{ to } *\IVML{;} T \text{ } v\IVML{;}}{ca.v.a = deflt}
+   \patternDerivation{\IVML{annotate } a = deflt \IVML{ to} *\IVML{;} T \text{ } v\IVML{;}}{ca.v.a = deflt} \\
 \end{gather*}
 }
+
+Let $v$ be a given variable with default value expression $deflt$, then 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 is required. In the transformation pattern, we indicate this by a generic access expression ($ca.$) on the right side, which is empty for top-level variables. The second pattern refers to annotations. As introduced in Section \ref{sectNotationVarDecls}, annotations are variables allowing an an orthogonal configuration dimension for 'ordinary' variables. Thus, an annotation is translated similarly to an ordinary variable, but requires in addition a qualification through the respective ordinary variable.
 
 Algorithm \ref{algTranslateDeclaration} translates all constraints related to a given variable declaration $d$ and respective variable $v$ through their actual type. Basically, the algorithm considers for the given variable, depending on the actual type, derived type constraints, annotation defaults, compound constraints, container constraints, and constraints of overridden slots leading to a deferred default initialization through the global constraints set $\deferredDefaultConstraints$.