Index: /reasoner/consTranslation.tex
===================================================================
--- /reasoner/consTranslation.tex	(revision 211)
+++ /reasoner/consTranslation.tex	(revision 212)
@@ -274,24 +274,37 @@
 As a generic type, an IVML container variable can declare the contained element type. Moreover, a container differs from other IVML types, as a container can hold an arbitrary number of elements. The element values can be defined through a default value expression, an assignment constraint or respective container operations. However, there is no direct opportunity to define constraints for a container type. Of course, constraints can defined for container variables, but also through a derived type, the contained element type, or the actual type of the individual elements. The actual element type is important, in particular for elements of a container type, as due to type refinement an individual container element may have a more specific type than the element type defined for the container. For the element type, a reference type appears to be transparent, i.e., constraints are imposed by the target type of the reference and basic types do not impose further constraints as no constraints can be defined on them (cf. Section \ref{sectNotationOthers}). 
 
-As containers can hold an arbitrary number of elements, specifying a constraint over a container (not an individual element) often involves all-quantification. However, a change of a single element leads to a re-evaluation of quantfied container constraints. As a performance optimization strategy, the constraint translation might internally unroll a container for reasoning over quantified constraints, i.e., create constraints for the individual elements and take care of the changes of the individual element variables. Although potentially more efficient in some cases, unrolling is not possible for all IVML container types, e.g., \IVML{Set}-types do not offer index-based access to the individual elements. Thus, as a generic uniform translation pattern, we apply quantification.
+As containers can hold an arbitrary number of elements, specifying a constraint over a container (not an individual element) often involves all-quantification. However, a change of a single element leads to a re-evaluation of quantfied container constraints. As a performance optimization strategy, the constraint translation might internally unroll a container for reasoning over quantified constraints, i.e., create constraints for the individual elements and take care of the changes of the individual element variables. Although potentially more efficient in some cases, unrolling is not possible for all IVML container types, e.g., \IVML{Set}-types do not offer index-based access to the individual elements, i.e., may require transformations into corresponding \IVML{Sequence}-types. So far, to achieve a uniform translation patterns, we apply quantification rather than unrolling.
 
 \grayPara{
     \patternDerivationLabel{\IVMLcontainer{T}\ v\IVML{;}}{\nonumber\\\bigcup_{t~\in~usedTypes(v),~ c~\in~constraints(t)}\IVMLforall{f(v, t)}{\IVML{i}}{\varSubstitution{\constraintWith{c}{x}}{x=\IVML{i}, \IVMLself{}=\IVML{i}, \variableMapping}}}{forContainerQuant}
-    \patternDerivationLabel{\IVMLcontainer{T}\  v\IVML{;}~\constraintWith{c}{v}\IVML{;}}{\nonumber\\\varSubstitution{\constraintWith{c}{v}}{\variableMapping}}{forContainerTop}
+    \patternDerivationLabel{\IVMLcontainer{T}\  v\IVML{;}~\constraintWith{c}{v}\IVML{;}}{\varSubstitution{\constraintWith{c}{v}}{\variableMapping}}{forContainerTop}
 }
 
-There are two basic translation patterns for containers: Pattern \ref{forContainerQuant} considers all used element types in the actual value of container variable $v$ and creates for each defined constraint of these types an all-quantified constraint over $v$. Let $t$ be a used element type in $v$. Then we can apply respective constraints by quantifying over all container elements (of type $t$). This happens  through a quantor iterator variable $x$ of type $t$ and apply all constraints for $t$ by instantiating the constraints for $x$, i.e., qualifying all used slots with respect to $x$ and replacing \IVMLself{}. Although indivdual constraints may appear superfluous, they are needed to provide detailed error messages and also to keep the re-evaluation effort low. However, if the container is nested, i.e., $T$ is again a container over a certain type, in IVML we must flatten the container, i.e., remove all nested containers, to apply the constraints to all individual elements. As mentioned above, if $\subTypeOf{t}{T}$, accessing specific properties such as compound slots requires some form of type casting / selection on the elements of the container. These additional container transformations depend on the actual container type and are represented in the schema by the function $f(v, t)$. 
-
-
-Pattern \ref{forContainerTop} defines the translation for top-level constraints over collection variables. We will focus here on Pattern \ref{forContainerQuant}, as Pattern \ref{forContainerTop} is implicitly handled by the translation of top-level constraints in Algorithm \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelEvals}.
-
-
-Basically, $f(v, t)$ turns a sequence into a set to avoid duplicated constraints, flattens a nested container and applies type selects if needed to enable access to slots defined in refined compounds. Therefore, $f(v, t)$ uses the IMVL container operations \IVML{flatten} and \IVML{selectByKind}. Let $ca$ be a container access expression, e.g., $ca=\createExpression{decl(v)}$. If $ca$ is of a nested container type, we apply the \IVML{flatten} operation to extract all element values from all nested containers into one top-level container, i.e., enable access even to deeply nested container elements. We apply the \IVML{selectByKind} operation if $t$ is a subtype of the element type of the container, as otherwise slots defined on the  specific type $t$ are not accessible. Finally, as shown in the transformation pattern, we apply an all-quantor over the elements of the (projected) collection using the temporary iterator variable $x$ to the respective constraint $c$ after appropriate variable substitution, in particular to \IVMLself{} by $x$.
+There are two basic translation patterns for containers: Pattern \ref{forContainerQuant} considers all used element types in $v$ and Pattern \ref{forContainerTop} illustrates the transformation for top-level container variables.
+\begin{itemize}
+\item For each constraint defined for the element types used in the actual value of container $v$, Pattern \ref{forContainerQuant} creates an all-quantified constraint over $v$. Let $t$ be a used element type in $v$. Then we can apply the constraints defined for $t$ by a quantification over all container elements (of type $t$). Let $c(x)$ be a constraint defined for type $t$, i.e., the constraint is expressed over variable $x$ of type $t$. If we want to apply $c(x)$ to all container elements of type $t$, we all-quantify the container and express $c(x)$ over the iterator variable $i$ of type $t$, i.e., substitute in particular $x$ and \IVMLself{} by $i$. However, if $v$ is a nested container, we may have to flatten $v$, i.e., remove all nested containers, to apply the constraint to the individual elements. Further, if $\subTypeOf{t}{T}$, accessing specific compound slots requires type casting / selection on the element values. Whether we need these additional container operations depends on the actual types of $v$ and $t$. We generivally represent these operations in Pattern \ref{forContainerQuant}  by $f(v, t)$. Although indivdual quantified constraints may appear superfluous, i.e., we might aim at creating joined quantified expressions for individual types, the individual constraints are needed to provide detailed reasoning error messages. 
+
+\item Pattern \ref{forContainerTop} defines the usual translation for top-level constraints over collection variables, i.e., the potential need to substitute top-level variables by the actual access expressions collected in $\variableMapping$.
+\end{itemize}
+
+We will focus here on Pattern \ref{forContainerQuant}, as Pattern \ref{forContainerTop} is implicitly handled by the translation of top-level constraints in Algorithm \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelEvals}. First, we detail $f(v,t)$ in Section \ref{sectAdjContainer}. Then, we discuss Algorithm \ref{algTranslateContainerDeclaration} in Section \ref{sectTranslContainer} as well as subsequent algorithms.
+
+\subsubsection{Adjusting Containers}\label{sectAdjContainer}
+
+In summary, $f(v, t)$ turns a sequence into a set to avoid duplicated constraints, flattens a nested container and applies type selects if needed to enable access to slots defined in refined compounds. Therefore, $f(v, t)$ uses the IMVL container operations \IVML{flatten} and \IVML{selectByKind}.
+
+If $ca$ is a nested container (and $t$ is not a container type), we apply the IVML \IVML{flatten} operation to extract all element values from all nested containers into a single joint container. As a side effect, we enable access even to deeply nested container elements. 
+
+If $t$ is a subtype of the element type of the container, we apply the \IVML{selectByKind} operation, as otherwise slots defined on the  specific type $t$ are not accessible. 
+
+$f(v, t)$ composes both optional operations as shown in Schema \ref{fSimpleContainerQuantorPrefix}. Pattern \ref{forContainerQuant} uses $f(v, t)$ to create quantified constraints, i.e., appends the all-quantor with a respective iterator variable and constraint.
 %
 \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:\constraintWith{c}{x})
+\IVMLforall{v\IVMLcarrow \underbrace{\IVML{flatten()}\IVMLcarrow}_{\text{if isNested(e)}}\underbrace{\IVML{selectByKind(}t\IVML{)}}_{\text{if } \subTypeOf{t}{nested^*(e)}}}{i}{\constraintWith{c}{i}}
 \label{fSimpleContainerQuantorPrefix}
 \end{equation}
 %
+\subsubsection{Translating Containers}\label{sectTranslContainer}
+
 Algorithm \ref{algTranslateContainerDeclaration} translates a container variable declaration. The core idea of this algorithm is to determine the used types for all container elements and for each type to instantiate the constraints as explained above. However, used types are only availabe if a container value has been assigned. If no container value is available, we resort to the static type of the declaration of the container variable. During constraint translation, we distinguish between constraint containers, for which we directly turn the values into constraints, and container types that may imply further constraints such as containers over compounds or containers over derived types.
 
Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 211)
+++ /reasoner/reasoner.tex	(revision 212)
@@ -21,5 +21,6 @@
 \newcommand\IVMLnull[0]{\texttt{null}}
 \newcommand\IVMLMeta[1]{\texttt{#1}} %\underline{}
-\newcommand\IVMLforallSep[4]{#1\IVML{->forall(}#2#3#4\IVML{)}}
+\newcommand\IVMLcarrow[0]{\IVML{->}}
+\newcommand\IVMLforallSep[4]{#1\IVMLcarrow{}\IVML{forall(}#2#3#4\IVML{)}}
 \newcommand\IVMLforall[3]{\IVMLforallSep{#1}{#2}{:}{#3}}
 \newcommand\IVMLacc[2]{\IVMLMeta{acc}\IVML{(}#1,#2\IVML{)}}