- \item \ZEROPOS: map $g -> 0, \OPEN~g$
- \item \INITPOS: map $g -> i, \OPEN~g$
- \item \ISFRESH: $\OPEN~g, 0 -> true | \_ -> false$
- \item \FILTEROPEN: $G -> \FILTER(\ISOPEN,G)$
- \item \DEEPCLOSE: prende uno stack ed un insieme di goal da chiudere, traversa
- lo stack rimuovendo le occorrenze dei goal da $\tau$ e $\kappa$ e marcandole
- chiuse in $\Gamma$
+ \item $\ZEROPOS([g_1;\cdots;g_n]) =
+ [\langle 0,\OPEN~g_1\rangle;\cdots;\langle 0,\OPEN~g_n\rangle]$
+ \item $\INITPOS([\langle i_1,s_1\rangle;\cdots;\langle i_n,s_n\rangle]) =
+ [\langle 1,\OPEN~s_1\rangle;\cdots;\langle n,\OPEN~s_n\rangle]$
+ \item $\ISFRESH(s) =
+ \left\{
+ \begin{array}{ll}
+ \mathit{true} & \mathrm{if} ~ s = \langle n, \OPEN~g\rangle\land n > 0 \\
+ \mathit{false} & \mathrm{otherwise} \\
+ \end{array}
+ \right.$
+ \item $\FILTEROPEN(\mathit{locs})=
+ \left\{
+ \begin{array}{ll}
+ [] & \mathrm{if}~\mathit{locs} = [] \\
+ \langle i,\OPEN~g\rangle :: \FILTEROPEN(\mathit{tl})
+ & \mathrm{if}~\mathit{locs} = \langle i,\OPEN~g\rangle :: \mathit{tl} \\
+ \FILTEROPEN(\mathit{tl})
+ & \mathrm{if}~\mathit{locs} = \mathit{hd} :: \mathit{tl} \\
+ \end{array}
+ \right.$
+ \item $\REMOVEGOALS(G,\mathit{locs}) =
+ \left\{
+ \begin{array}{ll}
+ [] & \mathrm{if}~\mathit{locs} = [] \\
+ \REMOVEGOALS(G,\mathit{tl})
+ & \mathrm{if}~\mathit{locs} = \langle i,\OPEN~g\rangle :: \mathit{tl}
+ \land g\in G\\
+ hd :: \REMOVEGOALS(G,\mathit{tl})
+ & \mathrm{if}~\mathit{locs} = \mathit{hd} :: \mathit{tl} \\
+ \end{array}
+ \right.$
+ \item $\DEEPCLOSE(G,S)$: (intuition) given a set of goals $G$ and a stack $S$
+ it returns a new stack $S'$ identical to the given one with the exceptions
+ that each locator whose goal is in $G$ is marked as closed in $\Gamma$ stack
+ components and removed from $\tau$ and $\kappa$ components.
+ \item $\GOALS(S)$: (inutition) return all goals appearing in whatever position
+ on a given stack $S$.