No se si es valido pero hice esto:
Me definí: Variable t s: U.
Luego hice:
Proof.
intro H0.
exists (t).
exists (s).
exact (H0 s t).
Qed.
Porque no funciona esta demostracion?
En respuesta a Alejandro Sebastian Flocken Rodriguez
Re: [Practico 2] Ejercicio 4.1
de Carlos Luna -
Hola Alejandro.
No deberías definir variables de tipo U. La información que precisás debería salir de las eliminaciones de los existe que surgen al hacer la introducción de la "->" al inicio. No solo van a aparecer los elementos de tipo U sino las condiciones que éstos cumplen, que son necesarias para probar: exists y:U, exists x:U, (R x y).
Saludos, Carlos
En respuesta a Carlos Luna
Re: [Practico 2] Ejercicio 4.1
Llegue hasta:
Theorem e41: (exists x:U, exists y:U, (R x y)) -> exists y:U, exists x:U, (R x y).
Proof.
intro H0.
elim H0.
intro x.
intro H1.
elim H1.
intro y.
intro H2.
luego me tranque, intente hacer apply (H0) de diferentes formas pero algo estoy haciendo mal.
Que es lo que me falta?
Theorem e41: (exists x:U, exists y:U, (R x y)) -> exists y:U, exists x:U, (R x y).
Proof.
intro H0.
elim H0.
intro x.
intro H1.
elim H1.
intro y.
intro H2.
luego me tranque, intente hacer apply (H0) de diferentes formas pero algo estoy haciendo mal.
Que es lo que me falta?
En respuesta a Alejandro Sebastian Flocken Rodriguez
Re: [Practico 2] Ejercicio 4.1
de Carlos Luna -
Hola.
Con los testigos a la vista, la prueba la terminás con:
exists y.
exists x.
assumption.
Saludos, Carlos