No me quedó claro del teórico que pasa si al hacer la sustitución aparecen ligaduras nuevas. Por ejemplo en el siguiente caso
En la parte derecha del AND, al sustituir queda ((Existe x2) f1(x1,x2) =' x1 ), por lo que aparece una ocurrencia ligada de x2 y antes no había ninguna.
¿Qué sucede en estos casos?
Tenía entendido que la sustitución no se podía realizar, pero compañeros me dijeron que en las clases de consulta de práctico dijeron que eso cambió y que si se puede realizar.
Si es posible también indíquenme como debería quedar la sustitución en caso de que no se pueda realizar y en caso de que si se pueda realizar, ¿Qué deberíamos escribir como solución?
¿Existe algún lugar donde estén todas las reglas de la sustitución actualizadas a este curso para poder leerlas? Ya que si el teórico que aparece en OpenFing es diferente al actual, no quiero hacer otras cosas diferentes a como se dan ahora.
Yo estaba leyendo de la PPT que aparece en esta sección pero ahí indica que
Y yo entiendo si no se cumple lo que "Tenemos que exigir [...]" que entonces no podíamos hacer la sustitución.
¡Muchas gracias!
Saludos,
Diego Furrer.