+\clearpage\r
+ \item $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
+ $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
+ $\bullet$ $\bullet$ $\bullet$ $\bullet$ $\bullet$\r
+ \texttt{ prove di nuove definizioni di ac:}\r
+\r
+ \item \textbf{Set of subterms:} %$\SubtmsOf{\tm} \defeq \{ \tmtwo \mid \SubtmOf\tmtwo\tm \}$\r
+ \[\begin{array}{ll}\r
+ \SubtmsOf{\var} & \defeq \{\var\} \\\r
+ \SubtmsOf{\tm\,\tmtwo} & \defeq \SubtmsOf\tm \cup \SubtmsOf\tmtwo \cup \{\tm\,\tmtwo\} \\\r
+ \SubtmsOf{\lambda \var.\, \vec\tm} & \defeq \{\tmtwo\{\Const/\var\} \mid \tmtwo \in\SubtmsOf{\vec\tm}\} \\\r
+ \end{array}\]\r
+ \AC{Note: $\SubtmsOf\cdot$ replaces bound variables with $\Const$ when going under abstractions.}\r
+ \item \textbf{Subterm at position:}\r
+ \[\begin{array}{ll}\r
+ \text{Paths: } \pi & ::= \PathEmpty \mid \PathHd \mid \PathArg i \var \pi \mid \PathAbs\pi\r
+ \end{array}\]\r
+ \AC{\r
+ Given a path, one can retrieve from a term (if possible) the subterm at that position.\r
+\r
+ Since the path may go through abstraction, bound variables that become free\r
+ are renamed to variables of the form $\NamedBoundVar\pi$\r
+ (where $\pi$ is the path in the original inert leading to the abstraction binding that variable).\r
+ }\r
+ \[\begin{array}{ll}\r
+ \tm_\pi & \defeq \tm_\pi^{\Box} \\\r
+ t_{\PathEmpty}^{-} & \defeq t \\\r
+ (x\,t_1\cdots t_n)_{\PathHd}^{-} & \defeq x \\\r
+ (x\,t_1\cdots t_n)_{\PathArg i \var \pi}^{\rho} & \defeq\r
+ (t_i)_\pi^{\rho[\PathArg i \var \Box]} \mbox{(if } 1 \leq i\leq n \mbox{)} \\\r
+ (\lambda x.\, t)_{\PathAbs \pi}^{\rho} & \defeq t_\pi^{\rho[\PathAbs\Box]} \{\var\mapsto\NamedBoundVar{\rho[\PathEmpty]}\} \\\r
+ (t)_{\PathAbs \pi}^{\rho} & \defeq (\lambda x.\, t\, x)_{\PathAbs \pi}^{\rho} \text{ (with } x \text{ fresh) (eta)}\\\r
+ % \Omega_-^- & \defeq \Omega \\\r
+ \end{array}\]\r
+ \item \textbf{Head restriction:} $\OfHead T \var \defeq \{\tm \in T \mid \HeadOf{\tm} (\defeq \tm_{\PathHd}) = \var \}$\r
+ \item \textbf{Distinction:} \underline{$S,R$ is $\Div$--distinct} iff:\r
+ $S$ is empty, or there exists a path $\pi$ \emph{effective} for $\{\Div\}\cup \OfHead{\GarbageOf\Div}{\HeadOf\Div}$, s.t. EITHER:\r
+ \begin{itemize}\r
+ \item $\forall \tm\in \OfHead{\SubtmsOf{\Div}}{\HeadOf\Div}$, $\tm_\pi$ is defined;\r
+ % \item 1. $\exists s\in S$ s.t. $s \not\sim_\pi \Div$;\r
+ \item $\{s\in S \mid s \sim_\pi \Div\},R$ is $\Div$--distinct.\r
+ \end{itemize}\r
+ OR:\r
+\begin{itemize}\r
+ \item $\Div_\pi = \lambda\var.\, -, g$\r
+ (note that $\Div$ has recursively only one garbage);\r
+ % \item $\Div_\pi \neq \Omega$\r
+ \item there is $\Div'\in\SubtmsOf g$ s.t.\r
+ $S',R'$ is $\Div'$--distinct, where:\r
+ $R'\defeq R\cup \bigcup\{\text{subtms of } s \text{ along } \pi \mid s\in S\}$ and\r
+ $S' \defeq \OfHead{R'}{\HeadOf{\Div'}}$.\r
+ \end{itemize}\r
+\r
+ \item \textbf{Semi-$\sigma$-separability: } $(\Div,\Conv)$ are semi-$\sigma$-separable\r
+ IF $\OfHead{\SubtmsOf{\Conv}}{\HeadOf{\Div'}}, \SubtmsOf{\Conv}$ is $\Div'$--distinct for some $\Div'\in\SubtmsOf\Div$.\r
+\r
+ \clearpage\r