We may then construct an IOA \(\gamma \in \Theta (s)\)  from each of the
remaining types by setting, for \(1 \le i \le k\) ,
\(\gamma ^{{in}}(i)=\lbrace  C \mid \forall r . C \in t \rbrace \)  and
\(\gamma ^{{out}}(i)=\lbrace  \forall r C \mid \forall r . C \in t \rbrace \) .
All
this is clearly possible in time \(O(k) \cdot 2^{O(||)}\) . In
particular, the set of all types can be constructed by enumerating
all subsets \(t \subseteq {sub}()\)  and then checking for
satisfiability w.r.t. , which is possible in time
\(2^{O(||)}\)  using a type elimination procedure
[1]}. The overall running time achieved
is thus \(2^{O(|| \cdot k)} \cdot ||\) , which is \(2^{O(|Q| \cdot k)} \cdot ||\) .
