Relación 9 - Historial de revisiones

WikiSysop: Texto reemplazado: «isar» por «isabelle»

2018-07-16T15:46:16Z

Texto reemplazado: «isar» por «isabelle»

2014-03-09T13:44:07Z

2014-03-09T13:41:56Z

2014-03-09T13:39:25Z

2014-03-09T00:11:43Z

2014-03-08T15:15:11Z

2014-01-23T14:17:14Z

2014-01-23T12:40:15Z

2014-01-23T11:44:45Z

2014-01-23T11:22:51Z

← Revisión anterior		Revisión del 15:46 16 jul 2018
Línea 1:		Línea 1:
−	<source lang="~~isar~~">	+	<source lang="isabelle">
	header {* R9: Deducción natural proposicional (1) *}		header {* R9: Deducción natural proposicional (1) *}

@@ Línea 547: / Línea 547: @@
    ------------------------------------------------------------------ *}
--- "irealetei diecabmen1, julrobrel"
+-- "irealetei diecabmen1, julrobrel, jaisalmen, zoiruicha"
 lemma ej8_auto:
    assumes "q ⟶ r"
@@ Línea 641: / Línea 641: @@
    ------------------------------------------------------------------ *}
--- "irealetei diecabmen1, julrobrel, domlloriv"
+-- "irealetei diecabmen1, julrobrel, domlloriv, jaisamlem, zoiruicha"
 lemma ej9_auto:
    assumes  "(p ⟶ r) ∧ (q ⟶ r)"
@@ Línea 743: / Línea 743: @@
    ------------------------------------------------------------------ *}
--- "irealetei diecabmen1, julrobrel, domlloriv"
+-- "irealetei diecabmen1, julrobrel, domlloriv, jaisalmen zoiruicha"
 lemma ej10_auto:
    assumes  "p ∨ q ⟶ r"

@@ Línea 402: / Línea 402: @@
    ------------------------------------------------------------------ *}
--- "irealetei,julrobrel"
+-- "irealetei,julrobrel jaisalmen zoiruicha"
 lemma ej6_auto:
    assumes  "p ⟶ q ∧ r"
@@ Línea 478: / Línea 478: @@
    ------------------------------------------------------------------ *}
--- "irealetei,julrobrel, pabflomar, domlloriv"
+-- "irealetei,julrobrel, pabflomar, domlloriv jaisalmen, zoiruicha"
 lemma ej7_auto:
    assumes " p ∧ (q ⟶ r)"

@@ Línea 337: / Línea 337: @@
    ------------------------------------------------------------------ *}
--- "irealetei,julrobrel, domlloriv"
+-- "irealetei,julrobrel, domlloriv jaisalmen zoiruicha"
 lemma ej5_auto:
    assumes "(p ⟶ q) ∧ (p ⟶ r)"

@@ Línea 11: / Línea 11: @@
    de deducción natural de la lógica proposicional.
-   Las reglas básicas de la deducción natural necesarias son las
+   Las reglas básicas de la deducción natural necesarias son las1
    siguientes:
    · conjI:      ⟦P; Q⟧ ⟹ P ∧ Q
@@ Línea 44: / Línea 44: @@
    ------------------------------------------------------------------ *}
--- "irealetei,julrobrel, pabflomar juaruipav domlloriv"
+-- "irealetei,julrobrel, pabflomar juaruipav domlloriv jaisalmen zoiruicha"
 lemma ej1_auto:
    assumes "p ⟶ (q ⟶ r)"
@@ Línea 112: / Línea 112: @@
    ------------------------------------------------------------------ *}
--- "irealetei,julrobrel, pabflomar, domlloriv"
+-- "irealetei,julrobrel, pabflomar, domlloriv jaisalmen zoiruicha"
 lemma ej2_auto:
    assumes " p ⟶ (q ⟶ r)"
@@ Línea 197: / Línea 197: @@
    ------------------------------------------------------------------ *}
--- "irealetei, domlloriv, pabflomar"
+-- "irealetei, domlloriv, pabflomar jaisalmen zoiruicha"
 lemma ej3_auto:"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
   by auto
@@ Línea 284: / Línea 284: @@
    ------------------------------------------------------------------ *}
--- "irealetei,julrobrel, domlloriv"
+-- "irealetei,julrobrel, domlloriv jaisalmen zoiruicha"
 lemma ej4_auto:
    assumes "(p ⟶ q) ⟶ r"

@@ Línea 304: / Línea 304: @@
 qed
--- "juaruipav"
+-- "juaruipav irealetei"
 lemma ej4-jua:
 assumes 1: "(p ⟶ q) ⟶ r"

@@ Línea 780: / Línea 780: @@
 qed
---"juaruipav"
+--"juaruipav, pabflomar"
 lemma ej10:
 assumes 1:" p ∨ q ⟶ r"

@@ Línea 407: / Línea 407: @@
    shows  "(p ⟶ q) ∧ (p ⟶ r)"
 using assms by auto
+-- "pabflomar"
 lemma ej6:
    assumes  1:"p ⟶ q ∧ r"