Index: /reasoner/consTranslation.tex
===================================================================
--- /reasoner/consTranslation.tex	(revision 202)
+++ /reasoner/consTranslation.tex	(revision 203)
@@ -131,5 +131,5 @@
   \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}. When translating 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{Constraint $c(s)$ defined on compound slot $s$:} For a compound variable $v$ of type $C$, contained constraints are 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.
+  \item \emph{Constraint $\constraintWith{c}{s}$ defined on compound slot $s$:} For a compound variable $v$ of type $C$, contained constraints are 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.
 
   \item \emph{Eval blocks:} Here nesting becomes transparent and constraints are translated as if they were defined directly in the containing compound type, i.e., according to the second pattern. However, eval blocks require a higher constraint evaluation priority in the compound scope as we will detail below. 
@@ -256,6 +256,6 @@
 
 \grayPara{
-    \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}}
+    \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{\constraintWith{c}{x}}{x=\IVML{w}, \IVMLself{}=\IVML{w}, \variableMapping}\IVML{)}}
+    \patternDerivation{\IVML{containerOf(}T\IVML{) } v\IVML{;}~\constraintWith{c}{v}\IVML{;}}{\varSubstitution{\constraintWith{c}{v}}{\variableMapping}}
 }
 
@@ -267,5 +267,5 @@
 %
 \begin{equation}
-ca\rightarrow \underbrace{\IVML{flatten()}\rightarrow}_{\text{if isNested(e)}}\underbrace{\IVML{selectByKind(}t\IVML{)}\rightarrow}_{\text{if } \subTypeOf{t}{nested^*(e)}}\IVML{forAll}(x:c(x))
+ca\rightarrow \underbrace{\IVML{flatten()}\rightarrow}_{\text{if isNested(e)}}\underbrace{\IVML{selectByKind(}t\IVML{)}\rightarrow}_{\text{if } \subTypeOf{t}{nested^*(e)}}\IVML{forAll}(x:\constraintWith{c}{x})
 \label{fSimpleContainerQuantorPrefix}
 \end{equation}
@@ -351,5 +351,5 @@
 %
 \begin{equation}
-\underbrace{\underbrace{ca}_{1: ca}\rightarrow \IVML{flatten}}_{1:e}\rightarrow\IVML{forAll}(\underbrace{l}_{1:l}:\underbrace{\underbrace{l.s}_{2: ca}\rightarrow\IVML{flatten}}_{2:e}\rightarrow\IVML{forAll}(\underbrace{l_2}_{2:l}:c(l_2)))
+\underbrace{\underbrace{ca}_{1: ca}\rightarrow \IVML{flatten}}_{1:e}\rightarrow\IVML{forAll}(\underbrace{l}_{1:l}:\underbrace{\underbrace{l.s}_{2: ca}\rightarrow\IVML{flatten}}_{2:e}\rightarrow\IVML{forAll}(\underbrace{l_2}_{2:l}:\constraintWith{c}{l_2}))
 \label{fNestedContainerQuantorPrefix}
 \end{equation}
@@ -399,10 +399,10 @@
         \ForEach{$a\in annotations(v)$}{
 %           $ac\assng \closedCases{\createExpression{\IVMLMeta{acc}(ca,a)}, & \text{if } ca  \neq \undef \wedge~qualifyAnnotation(v, a)\\ ca, &\text{else}}$\;
-           $translateDeclaration(decl(a), a, annAc(a, v, ca, \variableMapping))$\;\label{algTranslateAnnotationDeclarationsTranslateDeclV}
+           $translateDeclaration(decl(a), a, annAcc(a, v, ca, \variableMapping))$\;\label{algTranslateAnnotationDeclarationsTranslateDeclV}
          }
        }\Else{\label{algTranslateAnnotationDeclarationsTranslateVEnd}\label{algTranslateAnnotationDeclarationsTranslateDStart}
         \ForEach{$a\in annotations(d)$}{
 %           $ac\assng \closedCases{\createExpression{\IVMLMeta{acc}(ca,a)}, & \text{if } \neq \undef \wedge~qualifyAnnotation(v, a)\\ ca, &\text{else}}$\;
-           $translateDeclaration(a, \undef, annAc(a, v, ca, \variableMapping))$\;\label{algTranslateAnnotationDeclarationsTranslateDeclD}
+           $translateDeclaration(a, \undef, annAcc(a, v, ca, \variableMapping))$\;\label{algTranslateAnnotationDeclarationsTranslateDeclD}
          }
        }\label{algTranslateAnnotationDeclarationsTranslateDEnd}