Lines Matching refs:item
38 \item
42 \item
49 \item
64 \item
70 \item
76 \item
107 \item
113 \item
161 \item
167 \item
173 \item
179 \item
227 \item $S^\#$ unites the sorts of $\Phi(\Sigma)$ and the set
230 \item $\leq^\#$ extends the subsort relation $\leq$ with pairs
233 \item $F^\#$ adds the function symbols $\{f:[w] \rightarrow [s]\}$ for all
236 \item $P^\#$ adds the predicate symbol $rew$ on all new sorts.
320 \item
323 \item axiomatization of the sorts in $\iota(\Sigma_M)$ as free types
327 \item homomorphism conditions for $h$:
334 \item surjectivity of homomorphisms:
338 \item a second-order formula saying that the kernel of $h$ ($\mathit{ker}(h)$)
415 \item on $\Sigma_M$, $k$ coincides with $n$;
417 \item on $\iota(\Sigma_M)$, the interpretation of sorts and function symbols
422 \item $make$ assigns to each $x$ the term $make(x)$;
424 \item the homomorphism $h$ is defined inductively as follows:
428 \item $h(\mathit{make}(x)) = x$, if $x \in n_s$ and $s\in \mathit{Sorts}(\Sigma)$;
430 \item $h(\mathit{make}(t)) = h(t)$, otherwise;
432 \item $h(\iota(f)(t_1, \dots, t_n))$ is defined iff $f(h(t_1), \ldots, h(t_n))$
437 \item for predicates in $\iota(\Sigma_M)$ we define