-\[
-\begin{array}{rcl}
- \SEM{\TACTICAL{T}}{\xi}{[g_1;\dots;g_n]::\Gamma}{\tau}{\kappa}
- \quad (n\geq 1)
- & =
- & \langle\xi_n,
- \MAPFUN{\mathtt{Open}}{G^O_n}::\DEEPCLOSEFUN{G^C_n}{\Gamma},
- \tau\setminus G^C_n,\kappa\setminus G^O_n\rangle
- \\[1ex]
-
- \multicolumn{3}{l}{\hspace{2em}\mathit{where} ~
- \left\{
- \begin{array}{rcll}
- \langle\xi_0, G^O_0, G^C_0\rangle & = & \langle\xi, [], []\rangle \\
- \langle\xi_{i+1}, G^O_{i+1}, G^C_{i+1}\rangle
- & =
- & \langle\xi_i, G^O_i, G^C_i\rangle
- & g_{i+1}\in G^C_i \\
- \langle\xi_{i+1}, G^O_{i+1}, G^C_{i+1}\rangle
- & =
- & \langle\xi, (G^O_i\setminus G^C)\cup G^O, G^C_i\cup G^C\rangle
- & g_{i+1}\not\in G^C_i \\
- & & \mathit{where} ~ \langle\xi,G^O,G^C\rangle=\TSEM{T}{\xi_i}{g_{i+1}}
- \\
- \end{array}
- \right.
- }
- \\[2ex]
-
- \SEM{C_1 ~ \SEMICOLON ~ C_2}{\xi}{\Gamma}{\tau}{\kappa}
- & =
- & \SEM{C_2}{\xi'}{\Gamma'}{\tau'}{\kappa'}
- \\[1ex]
-
- & & \mathit{where} ~
- \langle\xi',\Gamma',\tau',\kappa',\rangle =
- \SEM{C_1}{\xi}{\Gamma}{\tau}{\kappa}
- \\[2ex]
-
- \SEM{C~\DOT~}{\xi}{\Gamma}{\tau}{\kappa}
- & =
- & \langle \xi'', \Gamma'', \tau'', \kappa'' \rangle
- \\[1ex]
-
- \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.}
- \\[2ex]
-
- \SEM{~\BRANCH~}{\xi}{[g_1;\dots;g_n]::\Gamma}{\tau}{\kappa}
- \quad (n\geq 2)
- & =
- & \langle\xi, [g_1]::[g_2;\dots;g_n]::\Gamma, []::\tau, []::\kappa\rangle
- \\[2ex]
-
- \SEM{~\SHIFT~}{\xi}{G::[g_i;\dots;g_n]::\Gamma}{T::\tau}{K::\kappa}
- & =
- & \langle\xi,
- [g_i]::[g_{i+1};\dots;g_n]::\Gamma,
- \tau'::\tau,
- []::\kappa\rangle
- \\[1ex]
-
- & & \mathit{where} ~
- \tau' = T\cup\MAPFUN{\GOALOFFUN}{\FILTERFUN{\ISOPENFUN}{G}}\cup K
- \\[2ex]
-
- \SEM{~\MERGE~}{\xi}{G::[g_i;\dots;g_n]::\Gamma}{T::\tau}{K::\kappa}
- & =
- & \langle \xi, \Gamma'::\Gamma, \tau, \kappa \rangle
- \\[1ex]
-
- & & \mathit{where} ~
- \Gamma' =
- T \cup\FILTERFUN{\ISOPENFUN}{G}
- \cup[g_i;\dots;g_n]
- \cup\MAPFUN{\mathtt{Open}}{K}
- \\[2ex]
-
- \SEM{\SELECT{n_1,\dots,n_k}{C}}{\xi}{\Gamma}{\tau}{\kappa}
- & =
- & \langle \xi',\Gamma',\tau',\kappa' \rangle
- \\[1ex]
-
- & & \mathit{where} ~
- \forall ~ i=1,\dots,k,~\exists ~ \alpha_i,~\langle n_i,\alpha_i\rangle \in \xi
- \\[1ex]
-
- & & \mathit{and} ~
- \langle \xi', []::\Gamma', []::\tau', []::\kappa' \rangle
- = \SEM{C}{\xi}{\MAPFUN{\mathtt{Open}}{[n_1;\dots;n_k]}::\Gamma}{[]::\tau}{[]::\kappa}
- \\[2ex]