Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 17)
+++ /reasoner/reasoner.tex	(revision 18)
@@ -198,8 +198,8 @@
           \uIf{$ isContainer(type(d)) $}{
               \ForAll{$u \iterAssng usedTypes(dflt)$}{
-                   \TBD{$collectCompoundsCollection(d, u)$}\;
+                   \TBD{$collectDefaultsCompoundsCollection(d, u)$}\;
               }
            }\ElseIf{$ca \neq \undef$}{
-               \lIf{$self \in deflt \vee \TBD{isOverridenSlot(d)}$}{$dfltS \assng c_{dd}$}
+               \lIf{$self \in deflt \vee isOverridenSlot(d)$}{$dfltS \assng c_{dd}$}
                $dflt \assng dflt|_{self=ca}$\;
            }
@@ -255,17 +255,20 @@
 \subsubsection{Collection default constraints}\label{deflt_collections}
 
-Constraints defined on types that are implicitly instantiated within a collection must be turned into individual constraints and stored in the constraint base. This holds only for compound instances, but not for compound references as the reference targets are already instantiated variables.
+Constraints defined on types that are implicitly instantiated within a collection must be turned into individual constraints with proper access (all-quantification) and stored in the constraint base. This holds only for compound instances, but not for compound references as the reference targets are already instantiated variables. Algorithm \ref{algCollectDefaultsCompoundCollection} performs this transformation for a variable declaration $d$ and a specific type $t$ used within the default value expression of $d$. For all slots $s$ of $t$ and its refined compounds, the algorithm creates a new default constraint. If $d$ is nested, $d$ must first be flattened (can be omitted $d$ is not a nested collection). Then, all elements not complying with $d$ must be filtered out so that the remaining expression can be applied to the specific slots of type $t$ (the type selection can be omitted if $t=type(d)$). Then, an all-quantification over all elements of type $t$ of the collection using the iterator variable $i$ applies an assignment expression to the respective slot $s$, assigning to $i.s$ the default value expression of $s$ with \IVML{self} substituted by the iterator variable $i$.
 
 \TBD{What about typedefs/derived?}
 
-\begin{itemize}
-\item \textbf{Parameter:} collection $c$ 
-
-\item \textbf{Elements:} $elts = \bigcup_{v\in\setWith{allRefines^+(c)}{c \in elements(c)}} : dfltSlots(v)$
-
-\item \textbf{Transformation ($s\in elts$):} $\langle flatten(c)\rightarrow forAll(i|assng(i.\bf{name(s)}, \bf{default(s)}|_{self=i}\rangle$
-
-\item \textbf{Optimization:} Replace $flatten(c)$ by $\left.\begin{cases}flatten(c), & \text{if } isNested(c) \\ c, &\text{else}\end{cases}\right\}$ to save an unneeded operation in case of non-nested collections.
-\end{itemize}
+\begin{algorithm}[H]
+  \SetAlgoLined
+  \KwIn{declaration $d$, (specific) type $t$}
+  \KwData{deferred default constraints $c_{dd}$}
+  \ForAll{$s \iterAssng \setWith{dfltSlots(u)}{u \in allRefines^+(t)}$}{
+      $c_{dd} \assng c_{dd} \cup \createDefaultConstraint{\IVML{typeSelect}(\IVML{flatten}(d), t)\rightarrow \IVML{forAll}(i|\IVML{assign}(i.name(s), default(s)|_{self=i})}$\;
+   }
+
+ \caption{Translates and collects defaults in compound collections (\IVML{collectDefaultsCompoundCollection}).}\label{algCollectDefaultsCompoundCollection}
+\end{algorithm}
+
+
 
 \section{Constraint translation}\label{sectConstraintTranslation}