Index: /reasoner/reasoner.tex
===================================================================
--- /reasoner/reasoner.tex	(revision 37)
+++ /reasoner/reasoner.tex	(revision 38)
@@ -142,13 +142,11 @@
 \subsubsection{Derived types}
 
-\begin{itemize}
-    \item derived
-      \begin{itemize}
-         \item $base(t)$ the type $t$ is derived from if $isDerived(t)$
-         \item $isDerived(t)$ whether $t$ is a derived type. In this case, $basis(t)$ is the basis type $t$ is derived from, else $basis(t) =\undef$. $decl(d)$ is the specific variable of a derived type used to define restricting constraints.
-         \item $allBase(t) = \begin{cases}\set{t}, & \text{if } isDerived(t) \wedge  base(t) = \undef \\  \set{t} \cup allBase(base(t)), & \text{if } isDerived(t) \wedge base(t) \neq \undef \\ \emptySet, & \text{else}\\ \end{cases}$
-      \end{itemize}
-\end{itemize}
-
+In IVML, a derived type creates a new type based on an existing type. A derived type can restrict the base type by specifiying constraints, as well as a type alias if no further constraints are given.
+
+For a derived type $t$, $isDerived(t)$ returns true and $base(t)$ \TBD{only base or most basic base type?} returns the type $t$ is derived from. For specifying constraints, a base type implicitly declares a variable $decl(d)$ of type $t$. Of course, derived types can be defined based on already existing derived types. In this case, a chain of base types is created, whereby for reasoning typically the most basic type is relevant. For constraint translation in reasoning, it is relevant to iterate over all base types of such a chain, e.g., and to instantiate their declared constraints. Therefore, we define
+
+$$allBase(t) = \begin{cases}\set{t}, & \text{if } isDerived(t) \wedge  base(t) = \undef \\  \set{t} \cup allBase(base(t)), & \text{if } isDerived(t) \wedge base(t) \neq \undef \\ \emptySet, & \text{else}\\ \end{cases}$$
+
+\subsubsection{Reasoning structures \TBD{?Misc?}}
 
 \begin{itemize}