Hola Rodrigo:
Hay que tener en cuenta que la regla RI4 involucra dos sustituciones:
t1 =' t2 φ[t1/z]
——————————————————————— RI4*
φ[t2/z]
Las dos sustituciones son [t1/z] y [t2/z].
En este caso tenemos:
- φ = P(z,y)
- t1 = y
- t2 = f(y)
Entonces nos queda:
y =' f(y) P(z,y)[y/z]
———————————————————————–————— RI4*
P(z,y)[f(y)/z]
La variable z "desaparece" cuando hacemos la sustitución pero aún aparece en la justificación.
Si tomáramos φ = P(z,z) ahí nos quedaría P(y,y) arriba y P(f(y),f(y)) abajo. Pero esto no es lo que queremos hacer.
La idea es poner la variable "fantasma" z en el lugar donde quiero que se haga el reemplazo de término por término.
saludos