- \SEM{~\DOT~}{\xi}{[]::\Gamma}{\tau}{(n::N)::\kappa}
- & =
- & \langle\xi, [\OPEN{n}]::\Gamma, \tau, N::\kappa\rangle
+ \multicolumn{3}{l}{\hspace{2em}\mathit{where} ~
+ \langle \xi',G::\Gamma',\tau',K::\kappa' \rangle
+ = \SEM{C}{\xi}{\Gamma}{\tau}{\kappa}}
+ \\[1ex]
+
+ \multicolumn{3}{l}{\hspace{2em}\mathit{and} ~
+ \langle \xi'', \Gamma'', \tau'', \kappa'' \rangle =
+ \left\{
+ \begin{array}{ll}
+ \langle \xi', [g]::\Gamma', \tau', (\MAPFUN{\GOALOFFUN}{G'}\cup K)::\kappa'
+ \rangle
+ & \FILTERFUN{\ISOPENFUN}{G} = g::G'
+ \\
+ \langle \xi', [\mathtt{Open}~n]::\Gamma', \tau', K'::\kappa' \rangle
+ & \FILTERFUN{\ISOPENFUN}{G} = []~\land~K=n::K'
+ \end{array}
+ \right.}