Relación 6 - Historial de revisiones

Pedrosrei en 14:26 7 abr 2013

2013-04-07T14:26:09Z

Pedrosrei en 10:01 7 abr 2013

2013-04-07T10:01:00Z

Mostrar los cambios

Pedrosrei en 08:49 7 abr 2013

2013-04-07T08:49:42Z

Pedrosrei en 10:30 6 abr 2013

2013-04-06T10:30:54Z

Pedrosrei en 10:20 6 abr 2013

2013-04-06T10:20:26Z

Pedrosrei en 10:03 6 abr 2013

2013-04-06T10:03:18Z

Pedrosrei en 09:42 6 abr 2013

2013-04-06T09:42:19Z

Pedrosrei en 08:35 6 abr 2013

2013-04-06T08:35:53Z

Pedrosrei en 09:53 5 abr 2013

2013-04-05T09:53:22Z

Pedrosrei en 15:40 4 abr 2013

2013-04-04T15:40:58Z

@@ Línea 753: / Línea 753: @@
         A(x,y) para x ha afeitado a y
     ------------------------------------------------------------------ *}
+lemma ejercicio_19a:
 text {* ---------------------------------------------------------------
    Ejercicio 20. Formalizar el siguiente argumento

@@ Línea 948: / Línea 948: @@
    ------------------------------------------------------------------ *}
 -- "Pedro Ros"
-lemma ejercicio_24:
-assumes 1:"∀x. ((L(x)∨Ca(x)∨Or(x)∨Pa(x)∨Z(x))⟶A(x))" and  "(∃x. L(x))∧(∃x. Ca(x))∧(∃x. Or(x))∧(∃x. Pa(x))∧(∃x. Z(x))"and
+lemma ejercicio_24f:
-:"(∃x. S(x))∧(∀y. S(y)⟶Pa(y))"and
+  assumes a1: "∀x. ((L(x)∨Z(x)∨Pa(x)∨Or(x)∨Ca(x)) ⟶ A(x))" and
-:"∀x. (A(x) ⟶ ((∀y.∀z.(Pa(z)⟶(A(y)∧M(y,x)∧Co(y,z))⟶Co(x,y))∧(Pa(y)⟶Co(x,y)) )))" and
+          a2: "(∃x. L(x))∧(∃x. Z(x))∧(∃x. Pa(x))∧(∃x. Or(x))∧(∃x. Ca(x))" and
-:"∀x. ((Or(x)∨Ca(x))⟶(∀y. (Pa(y)⟶M(x,y))))" and "∀x. (∀y. ((Z(y)∧Pa(x))⟶M(x,y)))" and "∀x. (∀y. ((L(y)∧Z(x))⟶M(x,y)))"and
+          c: "(∃x. S(s))∧(∃x. Pl(x))"and
-:"∀x. ∀y. ∀z. ((L(x)∧S(y)∧Z(z))⟶ (¬Co(x,y)∧ ¬Co(x,z)))" and "∀x. ∀y. ∀z.((Pa(x)∧Or(y)∧Ca(z))⟶ (Co(x,y)∧¬Co(x,z)))" and
+          d: "∀x. (A(x)⟶((∀y. Pl(y)⟶Co(x,y))∨(∀y. A(y)∧M(y,x)∧(∃z. Pl(z)∧Co(y,z))⟶Co(x,y))))"and
-:"∀x. ∀y. (∃z. ((Pa(z)∧Ca(x)∧Or(y))⟶(Co(x,z)∨Co(y,z))))"
+          e: "∀x. ∀y.(Pa(y)∧(Or(x)∨Ca(x))⟶M(x,y))∧((Pa(y)∧Z(x))⟶M(y,x))∧((Z(y)∧L(x))⟶M(y,x))" and
-shows "∃x. (∃y. (∃z. (S(z)∧A(y)∧Co(y,z)∧A(x)∧Co(x,y))))"
+          f: "∀x. ∀y.(L(y)∧(S(x)∨Z(x))⟶ ¬Co(y,x))∧((Pa(x)∧Or(y))⟶Co(x,y))∧((Pa(x)∧Ca(y))⟶¬Co(x,y))" and
-quickcheck
+          g: "∀x. (Ca(x)∨Or(x))⟶ (∃y. Pl(y)∧Co(x,y))"
-using assms by auto
+  shows "∃x. ∃y. ∃z. (A(x)∧A(y)∧Pl(z)∧Co(x,y)∧Co(y,z))"

@@ Línea 977: / Línea 977: @@
    assumes 1:"A(r,c)" and
 :"¬S(p,a)" and
-:"∀x. ((¬S(x,a))⟶(A(x,r)))" and
+:"∀x. (¬S(x,a)⟶ A(x,r))" and
 :"∀x. ∀y. (A(x,y)⟷A(y,x))" and
-:"(∃x. A(x,r))⟶(∀y. (A(y,r)⟶(y=x)))"  and
+:"∀x. (A(x,r) ⟶ (∀y. A(y,r)⟶(x=y)))"
    shows   "p=c"
-quickcheck
+proof -
-using assms by auto
+  have "¬S(p,a) ⟶ A(p,r)" using 3..
 text {* ---------------------------------------------------------------

← Revisión anterior		Revisión del 10:20 6 abr 2013
Línea 843:		Línea 843:
	using assms by auto		using assms by auto

		+	-- "Pedro Ros"
		+	lemma ejercicio_22b:
		+	assumes "∀x. ∀y. ((H(x) ∧ P(x) ∧ P(y))⟶ A(x,y))"
		+	shows "∀x. ((H(x)∧ P(x))⟶A(x,x))"
		+	proof
		+	fix a
		+	have "∀y. (H(a) ∧ P(a) ∧ P(y))⟶ A(a,y)" using assms..
		+	hence 1:"H(a) ∧ P(a) ∧ P(a)⟶ A(a,a)" ..
		+	show "H(a) ∧ P(a) ⟶ A(a,a)"
		+	proof
		+	assume a:"H(a) ∧ P(a)"
		+	hence b:"P(a)"..
		+	have "H(a)" using a..
		+	have "P(a)∧P(a)" using b b..
		+	with `H(a)`have "H(a) ∧ P(a) ∧ P(a)"..
		+	with 1 show "A(a,a)"..
		+	qed
		+	qed

	text {* ---------------------------------------------------------------		text {* ---------------------------------------------------------------

@@ Línea 805: / Línea 805: @@
 lemma ejercicio_21:
 assumes 1:"∀x. ((∀y. ((F(y)∧D(x,y)))⟶(∀z. P(z)⟶D(x,z)))) "and
-:"∃x. (∃y. P(y)∧(¬D(x,y)))" and
+:"∃x. (∃y. P(y)∧(¬D(x,y)))"
 shows "¬(∀x. (∃y. (F(y)∧D(x,y))))"
-quickcheck
+proof
-using assms by auto
+  assume 3:"∀x. (∃y. (F(y)∧D(x,y)))"

@@ Línea 640: / Línea 640: @@
 shows "∃x.(D(x) ∧ B(x))"
 oops
 text {* ---------------------------------------------------------------

← Revisión anterior		Revisión del 09:53 5 abr 2013
Línea 421:		Línea 421:
	shows "∀x. (¬E(x)∨(C(x,m)∧¬R(x)))"		shows "∀x. (¬E(x)∨(C(x,m)∧¬R(x)))"
	using assms by auto		using assms by auto
		+
		+	-- "Pedro Ros"
		+	lemma ejercicio_11b:
		+	assumes 1:"∀x. (∀y. (C(x,y)⟶(A(x,y)∨I(x))))"and
		+	2:"∀x. (I(x)⟶ ¬R(x))" and
		+	3:"∀x. ((E(x)⟶(C(x,m)∧¬A(x,m))))"
		+	shows "¬(∃x. ¬(¬E(x)∨(C(x,m)∧¬R(x))))"
		+	proof
		+	assume "(∃x. ¬(¬E(x)∨(C(x,m)∧¬R(x))))"
		+	then obtain a where "¬(¬E(a)∨(C(a,m)∧¬R(a)))"..
		+	hence 4:"¬¬E(a) ∧ ¬(C(a,m)∧ ¬R(a))" by (rule ejercicio_46)
		+	hence "¬¬E(a)"..
		+	hence 5:"E(a)" by (rule notnotD)
		+	have 6: "¬(C(a,m)∧ ¬R(a))" using 4..
		+	hence 7: "¬C(a,m) ∨ ¬¬R(a)" by (rule ejercicio_57)
		+	have "E(a)⟶C(a,m)∧ ¬A(a,m)" using 3..
		+	hence 10:"C(a,m)∧ ¬A(a,m)" using 5..
		+	hence 8:"C(a,m)"..
		+	show False
		+	proof-
		+	have "¬C(a,m) ∨ ¬¬R(a)" using 7.
		+	moreover
		+	{assume "¬C(a,m)"
		+	hence False using 8..}
		+	moreover
		+	{assume 9:"¬¬R(a)"
		+	have "I(a)⟶ ¬R(a)" using 2..
		+	hence 11:"¬I(a)" using 9 by (rule mt)
		+	have "(∀y. (C(a,y)⟶(A(a,y)∨I(a))))" using 1..
		+	hence "(C(a,m)⟶(A(a,m)∨I(a)))"..
		+	hence 12:"(A(a,m)∨I(a))" using 8..
		+	have "¬A(a,m)" using 10..
		+	with 12 have "I(a)" by (rule ejercicio_43)
		+	with 11 have False ..}
		+	ultimately
		+	show False..
		+	qed
		+	qed

@@ Línea 416: / Línea 416: @@
 -- "Pedro Ros"
 lemma ejercicio_11:
-assumes 1:"∀x. (∀y. ((y≠x)∧C(x,y)⟶(A(x,y)∨I(x))))"and
+assumes 1:"∀x. (∀y. (C(x,y)⟶(A(x,y)∨I(x))))"and
 :"∀x. (I(x)⟶ ¬R(x))" and
-:"∀x. ((E(x)⟶C(x,m)))" and
+:"∀x. ((E(x)⟶C(x,m)∧¬A(x,m)))"
-          "∀x. (x≠m)"
+shows   "∀x. (¬E(x)∨(C(x,m)∧¬R(x)))"
 using assms by auto