Buenas tardes!
No hemos podido avanzar con este ejercicio. No se nos ha ocurrido como encarar el axioma dado.
Podrían guiarnos?
Gracias
Hola.
Para poder probar este lema tienen que usar la información que proporciona el axioma leinv. Luego de introducir la variable n, pueden hacer:
elim (leinv (S n) O).
Notar que leinv la instanció para los parámetros relevantes del ejercicio (ya que el goal es inicialmente: ~(le (S n) O)). Observar que al ser "leinv(S n) O" es una disyunción, el elim aplica la regla de eliminación de este conectivo, generando de obligaciones/caminos de prueba. Pueden usar los axiomas del ejercicios 10, ya que el ejercicio 11 es continuación de éste. Por ejemplo, disc será útil.
Espero que esto ayude; sino volvé a escribir.
Saludos, Carlos
Una corrección: "leinv (S n) O" no es una disyunción, sino un implica "->". La disyunción es "elim (leinv (S n) O HleS)", donde HleS corresponde a: Le (S n) O.
Saludos, Carlos
Buenas! gracias por la respuesta.
Me queda la duda cómo utilizar el ejercicio 10 si están en diferentes secciones. Podemos modificar el template para que estén en la misma?