Buenos días
Estuvimos intentando hacer el ejercicio 7.8 pero no logramos encarar la prueba por ningún lado. En primer lugar queríamos saber si el enunciado que planteamos para el lema es correcto:
Lemma ej7_8: forall (d d2: Memoria), v1 <> v2 /\ Execute PP_ej7 d d2 -> lookup d2 v2 = false /\ lookup d2 v1 = true.
Si es correcto, no supimos mucho cómo realizar la prueba. Intentamos usando inversión y nos empezó a quedar una prueba re larga que no pudimos terminar en ningún momento. Tienen alguna sugerencia sobre cómo realizar la prueba?
Gracias y saludos