El reemplazo entra por un solo argumento

El enunciado, textual: «Pruebe que si $r,s,t\in T^{\tau }$ y $t^{\prime }$ es el resultado de reemplazar una ocurrencia de $s$ en $t$ por $r$, entonces $t^{\prime }\in T^{\tau }$.» Es el inciso (f) del Lema 4 de la Guía 9 (p. 7), el de ocurrencias de términos en términos, cuya prueba la guía deja al lector.

La lista deja usar sin enunciar el menú y la lectura única, y nada más. La prueba de la guía para ocurrencias se apoya en el inciso (c) del mismo lema, y el (c) en el Lema 2, el mordisqueo de términos. El mordisqueo la guía lo da sin prueba (Ejercicio 9), y se puede citar enunciado; acá se lo evita, y se prueba todo lo que se usa con el menú y la lectura única como únicas herramientas.

01 · Qué pide, en criollo

Un término es una palabra. Adentro de esa palabra hay otro término, $s$, en algún lugar: se lo recorta y en el hueco se pega $r$. El ejercicio dice que lo que queda vuelve a ser término.

Con el tipo de la guía, $\tau =(\{\mathrm{uno},\mathrm{doli}\},\{\mathrm{MAS},\mathrm{P}\},\{\mathrm{Her}\},a)$ con $a(\mathrm{MAS})=4$, $a(\mathrm{P})=1$ y $a(\mathrm{Her})=3$, el término de nivel 3 de la página 2 es

$$t=\mathrm{P}(\mathrm{MAS}(\mathrm{P}(\mathrm{X}4),\mathrm{MAS}(\mathrm{X}1,\mathrm{X}2,\mathrm{X}3,\mathrm{X}4),\mathrm{X}19,\mathrm{X}5))$$

Tiene 37 símbolos y once ocurrencias de subtérminos: él mismo, los dos $\mathrm{MAS}$, $\mathrm{P}(\mathrm{X}4)$ y siete variables, con $\mathrm{X}4$ dos veces, a partir de 9 y de 26. Reemplazando la $\mathrm{X}4$ que empieza en 26 por $\mathrm{P}(\mathrm{P}(\mathrm{uno}))$ queda

$$\mathrm{P}(\mathrm{MAS}(\mathrm{P}(\mathrm{X}4),\mathrm{MAS}(\mathrm{X}1,\mathrm{X}2,\mathrm{X}3,\mathrm{P}(\mathrm{P}(\mathrm{uno}))),\mathrm{X}19,\mathrm{X}5))$$

que es un término de nivel 5. Y reemplazando $\mathrm{MAS}(\mathrm{X}1,\mathrm{X}2,\mathrm{X}3,\mathrm{X}4)$, que empieza en 13, por $\mathrm{uno}$ queda $\mathrm{P}(\mathrm{MAS}(\mathrm{P}(\mathrm{X}4),\mathrm{uno},\mathrm{X}19,\mathrm{X}5))$, de nivel 3. El nivel cambia; lo que se conserva es ser término.

Que $s$ sea término no es decorativo. La palabra $\mathrm{X}1,\mathrm{X}2$ también ocurre en $t$, a partir de 17, y no es un término. Reemplazándola por $\mathrm{uno}$ queda $\mathrm{P}(\mathrm{MAS}(\mathrm{P}(\mathrm{X}4),\mathrm{MAS}(\mathrm{uno},\mathrm{X}3,\mathrm{X}4),\mathrm{X}19,\mathrm{X}5))$, que no es término: el $\mathrm{MAS}$ de adentro quedó con tres argumentos. Lo que pasó es que $\mathrm{X}1,\mathrm{X}2$ se monta sobre una coma que separa dos argumentos, y el reemplazo se comió la coma.

Eso es exactamente lo que no le puede pasar a un término. La $\mathrm{X}4$ desde 26 no es $t$, y cae adentro del único argumento de $\mathrm{P}$; adentro de ese argumento, que es un $\mathrm{MAS}$, cae en su segundo argumento, $\mathrm{MAS}(\mathrm{X}1,\mathrm{X}2,\mathrm{X}3,\mathrm{X}4)$; y ahí es el cuarto argumento entero. En cada piso el reemplazo entra por un solo argumento, y el resto de la palabra queda igual. Esa es toda la prueba: una inducción en el nivel de $t$, con un hecho de ocurrencias para saber por dónde entra.

02 · Las herramientas

Los términos (Guía 9, p. 1). $T_0^{\tau }=\mathrm{Var}\cup 𝒞$ y $$T_{k+1}^{\tau }=T_k^{\tau }\cup \{f(t_1,\dots ,t_n):f\in {ℱ}_n,n\ge 1,t_1,\dots ,t_n\in T_k^{\tau }\}$$, con $T^{\tau }={\bigcup }_{k\ge 0}{T}_k^{\tau }$. La palabra $f(t_1,\dots ,t_n)$ es la concatenación del nombre $f$, el «(», los $n$ argumentos separados por $n-1$ comas, y el «)». Cada nivel contiene al anterior.

Las variables (p. 1). La variable $x_n$ es la palabra $\mathrm{X}$ seguida de la escritura decimal de $n$, con los numerales en itálica salvo el último, que va en negrita. Una variable tiene un solo numeral negrita, y es su último símbolo.

El tipo (Guía 8, p. 4). En $\tau =(𝒞,ℱ,ℛ,a)$ los nombres de constante son palabras no vacías de un alfabeto ${\Sigma }_1$, los de función de ${\Sigma }_2$ y los de relación de ${\Sigma }_3$, con estas condiciones: los tres alfabetos son disjuntos de a pares; ninguno contiene ∀, ∃, ¬, ∨, ∧, →, ↔, los paréntesis, la coma, ≡, la $\mathrm{X}$ ni los numerales; y (3) ninguna palabra de $𝒞$ es subpalabra propia de otra palabra de $𝒞$, y lo mismo en $ℱ$ y en $ℛ$.

Ocurrencias (p. 6). $\alpha$ ocurre a partir de $i$ en $\beta$ si $\beta =\delta \alpha \gamma$ con $|\delta |=i-1$. Esa ocurrencia ocupa las posiciones $i$ a $i+|\alpha |-1$, y sucede dentro de otra si todas sus posiciones están entre las de la otra. Reemplazarla por ${\gamma }^{\prime }$ da $\delta {\gamma }^{\prime }\gamma$.

Lema 1 (Menú para términos, p. 3) y Teorema 3 (Lectura única de términos, p. 5). Se usan sin enunciar; quedan acá para tenerlos a mano. El menú: si $t\in T_{k+1}^{\tau }$, entonces $t\in \mathrm{Var}\cup 𝒞$ o $t=f(t_1,\dots ,t_n)$ con $f\in {ℱ}_n$, $n\ge 1$ y $t_1,\dots ,t_n\in T_k^{\tau }$. La lectura única: dado $t\in T^{\tau }$ se da una y sólo una de (1) $t\in \mathrm{Var}\cup 𝒞$, (2) hay únicos $n\ge 1$, $f\in {ℱ}_n$, $t_1,\dots ,t_n\in T^{\tau }$ con $t=f(t_1,\dots ,t_n)$.

Hecho 0 (el primer símbolo). Sea $s\in T^{\tau }$. Si $s$ empieza con $\mathrm{X}$, es una variable; si empieza con un símbolo de ${\Sigma }_1$, es un nombre de constante; si empieza con un símbolo de ${\Sigma }_2$, es de la forma $g(s_1,\dots ,s_m)$, y entonces $g$ es el tramo de $s$ que va hasta antes de su primer «(». Ningún término empieza con «(», «)», una coma ni un numeral.

Prueba. Por la lectura única, $s$ es una variable, que empieza con $\mathrm{X}$; un nombre de constante, que empieza con un símbolo de ${\Sigma }_1$; o $g(s_1,\dots ,s_m)$, que empieza con el primer símbolo de $g$, que está en ${\Sigma }_2$. Como ${\Sigma }_1$ y ${\Sigma }_2$ son disjuntos y ninguno tiene la $\mathrm{X}$, el primer símbolo dice cuál de los tres casos es. Ninguno empieza con paréntesis, coma ni numeral. Y como $g$ no tiene paréntesis, el primer «(» de $g(s_1,\dots ,s_m)$ es el que sigue a $g$. ∎

03 · El hecho de ocurrencias: por dónde entra el reemplazo

Lo que la inducción necesita es el inciso (c) del Lema 4 de la Guía 9:

Lema 4(c). Si $s\in T^{\tau }$, $s\ne f(t_1,\dots ,t_n)$ y $s$ ocurre en $f(t_1,\dots ,t_n)$, entonces dicha ocurrencia sucede dentro de algún $t_j$.

Para probarlo conviene uno un poco más fuerte, que se deja probar por inducción. La palabra $z$ que va después es lo que el término tiene a su derecha cuando es un argumento de otro: una coma y el resto, o el «)» del final.

Lema A. Sean $u,s\in T^{\tau }$ y $z$ una palabra que es $\epsilon$ o empieza con una coma o con «)». Si $s$ ocurre en $uz$ a partir de $p$, con $p\le |u|$, entonces la ocurrencia está dentro de $u$, o sea $p+|s|-1\le |u|$; y si además $p=1$, entonces $s=u$.

Leído en criollo: un término que empieza adentro de otro termina adentro de él, y si empiezan juntos son el mismo. La condición sobre $z$ hace falta. Con las constantes $\mathrm{uno}$ y $\mathrm{noli}$ de la página 5, que se mordisquean, en $\mathrm{uno}$ seguida de $\mathrm{li}$ el término $\mathrm{noli}$ empieza en la posición 2, adentro de $\mathrm{uno}$, y se sale.

Prueba. Usaremos la Regla de Inducción desde 0. Para cada $k\in \omega$ sea ${\mathrm{Enu}}_k$ el enunciado:

${\mathrm{Enu}}_k$: para todo $u\in T_k^{\tau }$, todo $s\in T^{\tau }$, toda palabra $z$ que sea $\epsilon$ o empiece con una coma o con «)», y todo $p\le |u|$: si $s$ ocurre en $uz$ a partir de $p$, entonces $p+|s|-1\le |u|$, y si además $p=1$, entonces $s=u$.

Llamemos $w=uz$.

${\mathrm{Enu}}_0$ es verdadero. Sea $u\in T_0^{\tau }=\mathrm{Var}\cup 𝒞$.

• Caso $u\in \mathrm{Var}$. El primer símbolo de $u$ es $\mathrm{X}$ y los demás son numerales. Si $p>1$, $s$ empezaría con un numeral, y por el Hecho 0 ningún término empieza así. Luego $p=1$ y $s$ empieza con $\mathrm{X}$: por el Hecho 0 es una variable, y su único negrita es su último símbolo. Los símbolos de $s$ son los primeros $|s|$ de $w$, y el primer negrita de $w$ está en la posición $|u|$, porque los de antes son la $\mathrm{X}$ y numerales itálicos. Si fuera $|s|<|u|$, el último símbolo de $s$ sería itálico; si fuera $|s|>|u|$, $s$ tendría un negrita antes del final. Luego $|s|=|u|$ y $s=u$.
• Caso $u\in 𝒞$. El símbolo de $w$ en la posición $p$ es de ${\Sigma }_1$, así que por el Hecho 0 $s$ es un nombre de constante, y todos sus símbolos están en ${\Sigma }_1$. Después de los símbolos de $u$, en $w$ viene $z$, que es vacía o empieza con una coma o un «)», que no están en ${\Sigma }_1$. Luego $s$ termina antes de llegar a $z$: $p+|s|-1\le |u|$. Si además $p=1$, $s$ es tramo inicial de $u$, los dos en $𝒞$, y por la condición (3) del tipo $s$ no es subpalabra propia de $u$: $s=u$.

${\mathrm{Enu}}_k$ implica ${\mathrm{Enu}}_{k+1}$. Supongamos que vale ${\mathrm{Enu}}_k$ y sean $u\in T_{k+1}^{\tau }$, $s$, $z$ y $p$ como en ${\mathrm{Enu}}_{k+1}$.

• Caso $u\in T_k^{\tau }$. Vale la conclusión por ${\mathrm{Enu}}_k$.
• Caso $u=f(u_1,\dots ,u_n)$ con $f\in {ℱ}_n$ y $u_1,\dots ,u_n\in T_k^{\tau }$. En $u$, las posiciones $1$ a $|f|$ son las de $f$; después vienen el «(», los argumentos con las comas que los separan, y el «)» en la posición $|u|$. Según dónde cae $p$:
  • $p=1$. $s$ empieza con el primer símbolo de $f$, que está en ${\Sigma }_2$; por el Hecho 0, $s=g(s_1,\dots ,s_m)$ con $g\in {ℱ}_m$ y $s_1,\dots ,s_m\in T^{\tau }$, y $g$ es lo que hay en $s$ antes de su primer «(». Como $s$ es tramo inicial de $w$ y tiene un «(», ese es también el primer «(» de $w$, y lo que hay antes en $w$ es $f$: $g=f$, y $m=a(f)=n$. Ahora $s_1$ y $u_1$ empiezan en la misma posición de $w$, la $|f|+2$, y desde ahí $w$ es $u_1{z}_1$, donde $z_1$ es lo que sigue a $u_1$: una coma y el resto, o «)» y el resto. Así que $s_1$ ocurre en $u_1{z}_1$ a partir de 1, y como $u_1\in T_k^{\tau }$, ${\mathrm{Enu}}_k$ da $s_1=u_1$. Si $n>1$, después de $s_1$ viene en $s$ una coma, y después de $u_1$ en $w$ también; $s_2$ y $u_2$ empiezan juntos, y el mismo argumento da $s_2=u_2$. Repitiéndolo, $s_j=u_j$ para $j=1,\dots ,n$, y entonces $s=f(u_1,\dots ,u_n)=u$. En particular la ocurrencia está dentro de $u$.
  • $1<p\le |f|$. $s$ empieza con un símbolo de $f$, que está en ${\Sigma }_2$, así que $s=g(s_1,\dots ,s_m)$ y $g$ es lo que hay en $s$ antes de su primer «(». En $w$, el primer «(» a partir de $p$ es el de la posición $|f|+1$, porque $f$ no tiene paréntesis. Entonces $g$ son los símbolos de $f$ desde la posición $p$ hasta el final: un tramo final propio de $f$, porque $p>1$. Los dos están en $ℱ$, y eso contradice la condición (3) del tipo. Este caso no se da.
  • $p$ es la posición del «(», de una de las comas que separan argumentos o del «)» final. Entonces $s$ empezaría con «(», una coma o «)», y por el Hecho 0 ningún término empieza así. Este caso no se da.
  • $p$ cae en las posiciones de algún $u_j$, que ocupa de la $a$ a la $b$ en $w$. Desde la posición $a$, $w$ es $u_j{z}_j$, donde $z_j$ empieza con la coma que sigue a $u_j$ si $j<n$, o con el «)» de $u$ si $j=n$. $s$ ocurre en $u_j{z}_j$ a partir de $p-a+1\le |u_j|$, y como $u_j\in T_k^{\tau }$, por ${\mathrm{Enu}}_k$ la ocurrencia está dentro de $u_j$: $p+|s|-1\le b\le |u|$. Acá $p\ge a>1$, así que la segunda parte de la conclusión no tiene nada que pedir.

Por la Regla de Inducción desde 0 vale ${\mathrm{Enu}}_k$ para todo $k$, y como todo término está en algún $T_k^{\tau }$, vale el Lema A. ∎

Prueba del Lema 4(c). Sea $t=f(t_1,\dots ,t_n)$ y una ocurrencia de $s$ en $t$ a partir de $p$. Si fuera $p=1$, el Lema A con $u=t$ y $z=\epsilon$ daría $s=t$, contra la hipótesis. Con $p>1$ los casos son los tres últimos del paso de arriba, con $u=t$ y $z=\epsilon$: dentro del nombre $f$ no se da, en un paréntesis o una coma de $t$ no se da, y si cae en las posiciones de un $t_j$, el Lema A aplicado a $t_j$ dice que la ocurrencia está dentro de $t_j$. Es un solo $t_j$, porque los argumentos ocupan posiciones disjuntas. ∎

Al revés también vale: si $s=t$, la única ocurrencia es a partir de 1, porque desde $p>1$ no entran $|t|$ símbolos. Así que hay exactamente dos posibilidades, y son las dos del paso de la inducción del ejercicio: la ocurrencia empieza en 1 y es $t$ entera, o empieza después y vive adentro de un único argumento.

04 · La mariposa: de atrás para adelante

La meta es $t^{\prime }\in T^{\tau }$, y lo único que se sabe de $t^{\prime }$ es cómo se obtuvo de $t$. Las propiedades de todos los términos se prueban por inducción en el nivel, así que la pregunta es qué pasa en el paso: $t=f(t_1,\dots ,t_n)$ con argumentos de nivel más bajo, y se reemplaza una ocurrencia de $s$ en algún lado.

Si la ocurrencia es $t$ entera, $t^{\prime }=r$, que es término por hipótesis. Si no, por el Lema 4(c) está adentro de un único $t_j$, y reemplazarla en $t$ es reemplazarla en $t_j$ y dejar todo lo demás —el nombre, los paréntesis, las comas, los otros argumentos— como estaba:

$$t^{\prime }=f(t_1,\dots ,t_{j-1},t_j^{\prime },t_{j+1},\dots ,t_n)$$

donde $t_j^{\prime }$ es el resultado de reemplazar esa ocurrencia en $t_j$ por $r$. $t_j$ tiene nivel más bajo, y la hipótesis inductiva dice que $t_j^{\prime }$ es término. Falta un detalle: $t_j^{\prime }$ puede tener un nivel más alto que los otros argumentos —en el ejemplo de la sección 01 pasó de 0 a 2—, y la definición pide los $n$ argumentos en un mismo $T_M^{\tau }$. Se toma $M$ el máximo, y como los niveles crecen, todos están ahí.

Por qué ${\mathrm{Enu}}_k$ lleva a $r$, a $s$ y a la ocurrencia adentro. La hipótesis inductiva se aplica a $t_j$, no a $t$, y a una ocurrencia que es la misma pero contada desde otro lugar: en $t_j$ empieza en otra posición. Si ${\mathrm{Enu}}_k$ hablara de una ocurrencia fija de $t$, no diría nada de $t_j$. En este ejercicio $r$ y $s$ son los mismos en el paso y en la hipótesis, así que dejarlos afuera no rompería la prueba; escribirlos adentro no cuesta nada y es lo que pide la lista: todas las cuantificaciones adentro.

Abajo se elige dónde empieza $s$, tocando un símbolo del término. Si ahí empieza un término, se ve por qué argumento entra el reemplazo en cada piso; si no, en qué caso del Lema A cae esa posición.

Las posiciones donde no empieza ningún término son las de los tres casos imposibles del Lema A: adentro de un nombre de función, en un paréntesis o una coma, en un numeral o adentro de un nombre de constante. En las otras, la bajada termina siempre igual: en algún piso, $s$ es el argumento entero.

05 · El escarabajo: la prueba como se entrega

Se escriben, en este orden, el Hecho 0, el Lema A y el Lema 4(c), con sus pruebas, como en las secciones 02 y 03. Después:

Prueba del ejercicio. Usaremos la Regla de Inducción desde 0. Para cada $k\in \omega$ sea ${\mathrm{Enu}}_k$ el enunciado:

${\mathrm{Enu}}_k$: para todo $t\in T_k^{\tau }$ y todos $r,s\in T^{\tau }$, si $t^{\prime }$ es el resultado de reemplazar una ocurrencia de $s$ en $t$ por $r$, entonces $t^{\prime }\in T^{\tau }$.

• ${\mathrm{Enu}}_0$ es verdadero. Sean $t\in T_0^{\tau }=\mathrm{Var}\cup 𝒞$, $r,s\in T^{\tau }$ y una ocurrencia de $s$ en $t$ a partir de $p$. Veamos que $p=1$. Si $t\in \mathrm{Var}$ y $p>1$, $s$ empezaría con un numeral, y ningún término empieza así (Hecho 0). Si $t\in 𝒞$ y $p>1$, $s$ empezaría con un símbolo de ${\Sigma }_1$ y sería un nombre de constante (Hecho 0); por el Lema A con $z=\epsilon$ estaría dentro de $t$, y sería una subpalabra propia del nombre de constante $t$, contra la condición (3) del tipo. Luego $p=1$, y por el Lema A con $u=t$ y $z=\epsilon$, $s=t$. Reemplazar esa ocurrencia por $r$ da $t^{\prime }=r\in T^{\tau }$.
• ${\mathrm{Enu}}_k$ implica ${\mathrm{Enu}}_{k+1}$. Supongamos que vale ${\mathrm{Enu}}_k$. Sean $t\in T_{k+1}^{\tau }$, $r,s\in T^{\tau }$ y $t^{\prime }$ el resultado de reemplazar una ocurrencia de $s$ en $t$, a partir de $p$, por $r$. Por definición de $T_{k+1}^{\tau }$ hay dos casos.
  • Caso $t\in T_k^{\tau }$. Por ${\mathrm{Enu}}_k$, $t^{\prime }\in T^{\tau }$.
  • Caso $t=f(t_1,\dots ,t_n)$, con $f\in {ℱ}_n$, $n\ge 1$ y $t_1,\dots ,t_n\in T_k^{\tau }$.
    • Si $p=1$, por el Lema A con $u=t$ y $z=\epsilon$, $s=t$: la ocurrencia es $t$ entera, y $t^{\prime }=r\in T^{\tau }$.
    • Si $p>1$, entonces $s\ne t$, porque desde $p>1$ no entran $|t|$ símbolos. Por el Lema 4(c), la ocurrencia sucede dentro de un único $t_j$. Sea $t_j^{\prime }$ el resultado de reemplazarla en $t_j$ por $r$. Como el reemplazo no toca ninguna posición fuera de $t_j$, $$t^{\prime }=f(t_1,\dots ,t_{j-1},t_j^{\prime },t_{j+1},\dots ,t_n)$$ Como $t_j\in T_k^{\tau }$, por ${\mathrm{Enu}}_k$ aplicado a $t_j$, $r$ y $s$, $t_j^{\prime }\in T^{\tau }$, o sea $t_j^{\prime }\in T_m^{\tau }$ para algún $m$. Sea $M=\max (k,m)$. Como los niveles crecen, $t_1,\dots ,t_{j-1},t_j^{\prime },t_{j+1},\dots ,t_n\in T_M^{\tau }$, y por definición $t^{\prime }\in T_{M+1}^{\tau }\subseteq T^{\tau }$.

Por la Regla de Inducción desde 0, ${\mathrm{Enu}}_k$ vale para todo $k\in \omega$. Dado $t\in T^{\tau }$, está en algún $T_k^{\tau }$, y ${\mathrm{Enu}}_k$ da $t^{\prime }\in T^{\tau }$. ∎

06 · Lo que hace perder puntos, y lo que se lleva

Lo que hace perder puntos. Decir «la ocurrencia está en algún $t_j$» sin enunciar ni probar el Lema 4(c): es un resultado de la guía, no el menú ni la lectura única. Olvidar el caso en que la ocurrencia es $t$ entera, que es el único en que el (c) no se aplica. Olvidar el caso $t\in T_k^{\tau }$ del paso. Escribir $t^{\prime }\in T_{k+1}^{\tau }$: no es cierto en general, porque $r$ puede tener cualquier nivel; lo que se prueba es $t^{\prime }\in T^{\tau }$, con el máximo de los niveles. Y escribir un ${\mathrm{Enu}}_k$ que no dice para qué términos vale: «${\mathrm{Enu}}_k$: $t^{\prime }\in T^{\tau }$» sin el «para todo $t\in T_k^{\tau }$» no es un enunciado.

Lo que se lleva. El molde —el caso de la ocurrencia entera, y el (c) para mandar la ocurrencia adentro de un argumento— es el de los Ejercicios 6, 7 y 8 de la lista, que también reemplazan ocurrencias en un término: sacar algunas $\mathrm{P}(x_1)$, cambiar $s_1$ por $s_2$ y cambiar $\mathrm{F1}$ por $\mathrm{F2}$. En el Ejercicio 3 lo que se reemplaza, $,\mathrm{X}1$, no es un término, y una ocurrencia sí puede montarse sobre una coma de afuera: ese caso es justamente el que hay que agregar. Las ocurrencias y los reemplazos, con más ejemplos, están en Ocurrencias y reemplazos, y la prueba de la guía, que usa el mordisqueo, en Se compara por el lado de lo que ya se sabe.

Para tener a mano

1. Inducción en el nivel de $t$, con ${\mathrm{Enu}}_k$: para todo $t\in T_k^{\tau }$ y todos $r,s\in T^{\tau }$, el resultado de reemplazar una ocurrencia de $s$ en $t$ por $r$ es término.
2. En el paso, la ocurrencia empieza en 1 y es $t$ entera (entonces $t^{\prime }=r$), o empieza después y vive adentro de un único argumento (entonces se reemplaza ahí y se usa ${\mathrm{Enu}}_k$).
3. Ese hecho es el Lema 4(c) de la Guía 9, y se enuncia y se prueba. Sin el mordisqueo sale del Lema A: un término que empieza adentro de otro termina adentro de él, y si empiezan juntos son el mismo.
4. El primer símbolo decide: $\mathrm{X}$ es variable, ${\Sigma }_1$ es constante, ${\Sigma }_2$ es $g(\dots )$; con «(», «)», coma o numeral no empieza ningún término.
5. $t_j^{\prime }$ puede subir de nivel: se toma $M$ el máximo y $t^{\prime }\in T_{M+1}^{\tau }$.