Relación 7 - Historial de revisiones

Pedrosrei en 10:31 12 abr 2013

2013-04-12T10:31:30Z

2013-04-12T10:17:44Z

2013-04-12T10:13:39Z

2013-04-12T10:04:21Z

2013-04-12T10:04:01Z

2013-04-12T09:59:24Z

2013-04-12T09:47:16Z

2013-04-10T15:32:23Z

2013-04-10T15:08:47Z

2013-04-10T15:07:14Z

@@ Línea 744: / Línea 744: @@
       ⊢ ∃z. P (f a) z (f (f a))
    ------------------------------------------------------------------ *}
+-- "Pedro Ros"
 lemma ejercicio_34b:
    assumes "∀x. P a x x"
            "∀x y z. P x y z ⟶ P (f x) y (f z)"
    shows   "∃z. P (f a) z (f (f a))"
-oops
+proof -
+  have 1: "P a (f a) (f a)" using assms(1)..
 text {* ---------------------------------------------------------------
    Ejercicio 35. Demostrar o refutar

@@ Línea 725: / Línea 725: @@
       ⊢ P (f a) a (f a)
    ------------------------------------------------------------------ *}
+-- "Pedro Ros"
 lemma ejercicio_33:
    assumes "∀x. P a x x"
            "∀x y z. P x y z ⟶ P (f x) y (f z)"
    shows   "P (f a) a (f a)"
-oops
+proof -
 text {* ---------------------------------------------------------------

@@ Línea 687: / Línea 687: @@
         ∃x y. R x y ∨ R y x; ¬(∃x. R x x)⟧ ⟹ ∃x y. x ≠ y
    ------------------------------------------------------------------ *}
+-- "Pedro Ros"
 lemma ejercicio_32:
    fixes R :: "'c ⇒ 'c ⇒ bool"
@@ Línea 693: / Línea 693: @@
            "¬(∃x. R x x)"
    shows   "∃(x::'c) y. x ≠ y"
-oops
+proof -
 text {* ---------------------------------------------------------------

@@ Línea 578: / Línea 578: @@
         ((∀x. P x) ∨ (∀x. Q x)) ⟷ (∀x. P x ∨ Q x)
    ------------------------------------------------------------------ *}
+-- "Pedro Ros"
 lemma ejercicio_27:
    "((∀x. P x) ∨ (∀x. Q x)) ⟷ (∀x. P x ∨ Q x)"
@@ Línea 588: / Línea 588: @@
         ((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)
    ------------------------------------------------------------------ *}
+-- "Pedro Ros"
 lemma ejercicio_28:
    "((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"

@@ Línea 591: / Línea 591: @@
 lemma ejercicio_28:
    "((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"
-oops
+proof
 text {* ---------------------------------------------------------------

@@ Línea 599: / Línea 599: @@
 lemma ejercicio_29:
    "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
 oops

@@ Línea 519: / Línea 519: @@
         (∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)
    ------------------------------------------------------------------ *}
+-- "Pedro Ros"
 lemma ejercicio_25:
    "(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)"
-oops
+proof
 text {* ---------------------------------------------------------------

@@ Línea 145: / Línea 145: @@
         ∃x y. P x y ⟹ ∃u v. P u v
    ------------------------------------------------------------------ *}
+-- "Pedro Ros"
 lemma ejercicio_7:
    assumes "∃x y. P x y"
@@ Línea 317: / Línea 317: @@
         ¬(∀x. ¬(P x)) ⊢ ∃x. P x
    ------------------------------------------------------------------ *}
+-- "Pedro Ros"
 lemma ejercicio_16:
    assumes "¬(∀x. ¬(P x))"
@@ Línea 349: / Línea 349: @@
         ∀x. ¬(P x) ⊢ ¬(∃x. P x)
    ------------------------------------------------------------------ *}
+-- "Pedro Ros"
 lemma ejercicio_17:
    assumes "∀x. ¬(P x)"
@@ Línea 364: / Línea 364: @@
         ∃x. P x ⊢ ¬(∀x. ¬(P x))
    ------------------------------------------------------------------ *}
+-- "Pedro Ros"
 lemma ejercicio_18:
    assumes "∃x. P x"
@@ Línea 379: / Línea 379: @@
         P a ⟶ (∀x. Q x) ⊢ ∀x. P a ⟶ Q x
    ------------------------------------------------------------------ *}
+-- "Pedro Ros"
 lemma ejercicio_19:
    assumes "P a ⟶ (∀x. Q x)"
@@ Línea 399: / Línea 399: @@
         ⊢ ∀x y. R x y ⟶ ¬(R y x)
    ------------------------------------------------------------------ *}
+-- "Pedro Ros"
 lemma ejercicio_20:
    assumes "∀x y z. R x y ∧ R y z ⟶ R x z"

@@ Línea 404: / Línea 404: @@
            "∀x. ¬(R x x)"
    shows   "∀x y. R x y ⟶ ¬(R y x)"
-oops
+proof-
 text {* ---------------------------------------------------------------