Index: /reasoner/consTranslation.tex
===================================================================
--- /reasoner/consTranslation.tex	(revision 209)
+++ /reasoner/consTranslation.tex	(revision 210)
@@ -272,16 +272,18 @@
 \subsection{Container types}\label{sectContainerDefaults}
 
-As a generic type, an IVML container variable can only 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 or an assignment constraint. Thus, there is no direct opportunity to define constraints for a container. However, constraints can be imposed indirectly if a container acts as base type for a derived type, through the contained type or the actual type of the individual element. If the element type is a compound, a derived type, a constraint type or, transitively, a nested container, the specific type indirectly imposes constraints further characterizing (the contents of) a container variable. The actual element type is important, in particular for elements of a container type, as due to type refinements an individual container element may have a more specific type than the element type defined by the container type. 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 own constraints can be defined on them. 
-
-As containers can hold an arbitrary number of elements, specifying a constraint over a container typically involves quantification, usually all-quantification. As an alternative, we might internally unroll a container for reasoning, 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., set-based types do not offer an index-based access to the elements. Thus, as a generic uniform translation pattern, we apply quantification.
+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.
 
 \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{\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}}
+    \patternDerivationLabel{\IVML{containerOf(}T\IVML{) } v\IVML{;}}{\nonumber\\\bigcup_{t~\in~usedTypes(v),~ c~\in~constraints(t)}f(v, t)\rightarrow \IVML{forall(i:}\varSubstitution{\constraintWith{c}{x}}{x=\IVML{i}, \IVMLself{}=\IVML{i}, \variableMapping}\IVML{)}}{forContainerQuant}
+    \patternDerivationLabel{\IVML{containerOf(}T\IVML{) } v\IVML{;}~\constraintWith{c}{v}\IVML{;}}{\nonumber\\\varSubstitution{\constraintWith{c}{v}}{\variableMapping}}{forContainerTop}
 }
 
-There are two basic translation patterns for containers, the first one for constraints induced by the types used in the container and the second one for top-level constraints over collection variables. We will focus here on the first pattern, as the second pattern comes for free as part of the translation of the top-level constraints in Algorithm \ref{algTranslateConstraints}, line \ref{algTranslateConstraintsTopLevelEvals}.
-
-For the first pattern, we consider all declared and used element types in the actual container value of the container variable $v$ and create for each constraint implied by these types an all-quantified constraint over $v$. In more details, let $t$ be a declared or used element type in $v$, then we can quantify all container elements (or at least a subset of type $t$) 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)$. 
+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$.
Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 209)
+++ /reasoner/reasoner.tex	(revision 210)
@@ -25,4 +25,5 @@
 \newcommand\IVMLacc[2]{\IVMLMeta{acc}\IVML{(}#1,#2\IVML{)}}
 \newcommand\IVMLassign[2]{\IVMLMeta{assign}\IVML{(}#1,#2\IVML{)}}
+\newcommand\IVMLcontainer[1]{\IVML{containerOf(}#1\IVML{)}}
 \newcommand\addSet[0]{\cup}
 \newcommand\addSeq[0]{\oplus}