Buenas noches,
Estamos intentando realizar la prueba del ejercicio 7.7 pero tenemos dudas sobre como encararla. Intentamos hacer inversión sobre las hipótesis de Execute, y también intentamos hacer inducción sobre los naturales n1 y n2 pero no estamos logrando demostrar lo que se pide. Tienen alguna sugerencia sobre como encarar la prueba?
Gracias y saludos!
Hola.
Sugiero, como paso más general de la prueba, hacer inducción de n1 (el primer natural de la suma).
Luego vean cuando conviene aplicar inversion, el constructor del repeat y la hipótesis inductiva. Pueden usar tácticas automáticas para probar pasos simples.
Saludos, Carlos
Gracias Carlos por tu respuesta, con lo que sugerís nos salió. Además, queríamos preguntar si es válido usar la tactica omega de la librería Omega para completar una parte de la prueba que nos quedó el siguiente goal:
n + n2 + 1 = n + 1 + n2
Saludos!
Hola.
Me alegro!
Si, pueden usar omega para resolver ciertas propiedades sobre números.
Saludos Carlos