Relación 5 - Historial de revisiones

Pedrosrei en 15:28 31 mar 2013

2013-03-31T15:28:14Z

2013-03-31T15:27:05Z

2013-03-20T14:08:53Z

2013-03-20T14:06:40Z

2013-03-20T13:59:45Z

2013-03-20T11:47:32Z

2013-03-19T23:02:12Z

2013-03-19T15:23:55Z

2013-03-19T08:28:55Z

2013-03-19T07:25:17Z

← Revisión anterior		Revisión del 15:28 31 mar 2013
Línea 159:		Línea 159:


−	text {* Por si alguien tiene curiosidad, defino todas las conectivas con las dos que son maximales, las puertas lógicas NAND y NOR: *}	+	text {* Pedro Ros.
		+	Por si alguien tiene curiosidad, defino todas las conectivas con las dos que son maximales, las puertas lógicas NAND y NOR: *}

	definition nand :: "bool ⇒ bool ⇒ bool" where		definition nand :: "bool ⇒ bool ⇒ bool" where

@@ Línea 157: / Línea 157: @@
     thus "A ∨ B ∧ C" by (rule ejercicio_3a)}
 qed
 end
 </source>

@@ Línea 134: / Línea 134: @@
    proof
      assume "(A ⟶ False) ⟶ B ∧ C"
-     hence 4: "A ∨ B ∧ C" by (rule ejercicio_3a)
+     hence "A ∨ B ∧ C" by (rule ejercicio_3a)
      with 2 show "A"..
    qed

@@ Línea 135: / Línea 135: @@
      assume "(A ⟶ False) ⟶ B ∧ C"
      hence 4: "A ∨ B ∧ C" by (rule ejercicio_3a)
-     show "A" using 4
+     with 2 show "A"..
    qed
    show "A⟶((A ⟶ False)⟶ B ∧ C)"

@@ Línea 127: / Línea 127: @@
 assumes "(A ∨ B ∧ C) ⟷ A"
 shows "(((A ⟶ False) ⟶ B ∧ C) ⟶ A) ∧ (A⟶((A ⟶ False)⟶ B ∧ C))"
-proof -
+proof
    have 1: "((A ∨ B ∧ C) ⟶ A) ∧ (A ⟶ (A ∨ B ∧ C))" using assms by (rule ejercicio_1a)
    hence 2: "(A ∨ B ∧ C) ⟶ A"..
    have 3: "A ⟶ (A ∨ B ∧ C)" using 1..
-   have 4: "((A ⟶ False) ⟶ B ∧ C) ⟶ A"
+   show "((A ⟶ False) ⟶ B ∧ C) ⟶ A"
    proof
      assume "(A ⟶ False) ⟶ B ∧ C"
-     hence 5: "A ∨ B ∧ C" by (rule ejercicio_3a)
+     hence 4: "A ∨ B ∧ C" by (rule ejercicio_3a)
-     show "A"
+     show "A" using 4
      proof
        assume "A"
@@ Línea 146: / Línea 145: @@
      qed
    qed
-   have 6: "A⟶((A ⟶ False)⟶ B ∧ C)"
+   show "A⟶((A ⟶ False)⟶ B ∧ C)"
    proof
      assume "A"
      with 3 have "A ∨ B ∧ C"..
      thus "(A ⟶ False)⟶ B ∧ C" by (rule ejercicio_3b)
    qed
 qed

← Revisión anterior		Revisión del 11:47 20 mar 2013
Línea 65:		Línea 65:
	qed		qed

		+	lemma ejercicio_2b:
		+	assumes "¬A"
		+	shows "A⟶ False"
		+	proof
		+	assume "A"
		+	show "False" using assms `A` by (rule notE)
		+	qed

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

@@ Línea 114: / Línea 114: @@
    equivalencia.
    ------------------------------------------------------------------ *}
 end
 </source>

@@ Línea 72: / Línea 72: @@
    y demostrar la equivalencia.
    ------------------------------------------------------------------ *}
 text {* ---------------------------------------------------------------