Index: /reasoner/consTranslation.tex
===================================================================
--- /reasoner/consTranslation.tex	(revision 200)
+++ /reasoner/consTranslation.tex	(revision 201)
@@ -110,8 +110,13 @@
 \subsection{Compound types}\label{sectCompoundDefaults}
 
-For a compound variable, in IVML one can define constraints in two different ways: 1) Constraints nested within compound type definitions or sub-structures with the same scope such as annotation assignments or eval blocks. Both, unqualified slots (implicitly qualified through the containing scope) or qualified variable access expressions can be used. Nested constraints imply all-quantification over all instances of the respective compound type~\cite{IVML-LS}. 2) Top-level constraints using qualified slot access expressions only.  We translate tese two ways using the following schema:
+For a compound variable, constraints can be defined in two different ways: 
+\begin{enumerate}
+  \item Constraints nested within the compound type definition or sub-structures having the same scope, e.g., annotation assignment blocks or eval blocks. In these constraints, both, unqualified slots (implicitly qualified through the containing scope) or qualified variable access expressions can be used. Nested constraints imply all-quantification over all instances of the compound type~\cite{IVML-LS}. 
+  \item Top-level constraints using qualified slot access expressions only. 
+\end{enumerate}
+We translate these two ways using the following schema:
 
 \grayPara{
-    \patternDerivation{\IVML{compound } C \IVML{\{} T s = deflt\IVML{;\}; } C\ v \IVML{;}}{\varSubstitution{s = deflt}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}
+    \patternDerivationLabel{\IVML{compound } C \IVML{\{} T s = deflt\IVML{;\}; } C\ v \IVML{;}}{\varSubstitution{s = deflt}{\IVMLself{}=access(v), s=access(v.s),\variableMapping}}{forCompoundDefault}
     \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}}
@@ -122,7 +127,7 @@
 The compound type translation must consider the following situations (discussed along the pattern sequence given above):
 
-\begin{enumerate}
-
-  \item \emph{Instantiation of a compound slot with default value expression to an assignment constraint:} As mentioned in Section \ref{sectTranslationDeclarationTypesDefaults}, slot initialization as well as slot annotations are handled by recursive execution of Algorithm \ref{algTranslateDeclaration} with an incrementally created access expression, here starting with $v$. Thus, the translation of compound types must create a respective variable mapping (in an own context frame) and apply the already discussed translation.
+\begin{itemize}
+
+  \item \emph{Compound slot with default value expression:} The default value is instantiated into a default value assignment constraint as shown in Pattern \ref{forCompoundDefault}. For a top-level compound variable $v$, the actual value for \IVMLself{} is determined by $access(v)$ and the accessor for slot $s$ by $access(v.s)$. For nested slots of compound types, Algorithm \ref{algTranslateDeclaration} is called recursively with the respective access expression.
 
   \item \emph{IVML compound type $C$ with declared slot $s$ and contained constraint $c(s)$ over slot $s$:} The translation is applied if a variable $v$ of type $C$, i.e., a concrete instance of a compound type is declared. A contained constraint is instantiated by qualifying all compound-scoped variable occurrences, i.e., by replacing \IVMLself{} with the actual variable $v$, the slot $s$ with the respective qualified access $v.s$ as well as all other known variable mappings including remaining slots. Thus, the variable mapping for a compound must be created before any slot is translated. Nested compounds are implicitly considered through the $access$ function, i.e., by respective access prefix expressions. Moreover, compound instances and, thus, constraints induced by compound types, may occur in containers. In Section \ref{sectContainerDefaults}, we will discuss the translations of containers, which recursively utilizes the translation of variables, i.e., Algorithm \ref{algTranslateDeclaration} and, thus, of compound types.
@@ -134,5 +139,5 @@
   \item \emph{Top-level constraint defined over a compound variable $v$:} Due to the mandatory use of only qualified slot access expressions in IVML, no translation is needed and such constraints are handled through line \ref{algTranslateConstraintsTopLevelConstraints} in Algorithm \ref{algTranslateConstraints}. 
 
-\end{enumerate}
+\end{itemize}
 
 We will now focus on the second pattern and discuss the respective translation Algorithm \ref{algTranslateCompoundDeclaration}. The idea is to visit all slots and constraints in the compound type and its refined compound types, first for creating the variable mapping (Algorithm \ref{algRegisterCompoundMapping}), then for translating all constraints (Algorithm \ref{algTranslateCompoundContent}). In some situations, both steps must be carried out individually instead of a fixed sequence, e.g., to perform the translation of potentially inter-dependent compound slot default values between both steps as discussed for Algorithm \ref{algTranslateDeclaration}. As compound slots are nested variable declarations, Algorithm \ref{algTranslateDeclaration} is responsible for translating slots and their annotations. Akin to Algorithm \ref{algTranslateDeclaration}, default values of annotations (here given in terms of annotation assignments) are only turned into assignment constraints if the reasoner is not in incremental mode. Finally, eval blocks (due to evaluation priority) and then directly nested constraints and constraints in assignment blocks of a compound and all refined compound types are translated.