Relación 10 - Historial de revisiones

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

2018-07-16T15:46:12Z

Texto reemplazado: «isar» por «isabelle»

Zoiruicha en 01:06 10 mar 2014

2014-03-10T01:06:06Z

Jaisalmen en 00:39 10 mar 2014

2014-03-10T00:39:26Z

Domlloriv en 17:56 8 mar 2014

2014-03-08T17:56:20Z

Juaruipav en 09:53 2 mar 2014

2014-03-02T09:53:50Z

Julrobrel: En esta ocasión no he conseguido aportar nada, los ejercicios de los compañeros me han parecido muy buenos.

2014-02-09T18:00:23Z

En esta ocasión no he conseguido aportar nada, los ejercicios de los compañeros me han parecido muy buenos.

Domlloriv en 08:17 3 feb 2014

2014-02-03T08:17:24Z

Irealetei en 13:08 29 ene 2014

2014-01-29T13:08:43Z

Irealetei en 12:14 29 ene 2014

2014-01-29T12:14:46Z

Irealetei en 12:11 29 ene 2014

2014-01-29T12:11:58Z

Mostrar los cambios

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

@@ Línea 122: / Línea 122: @@
    ------------------------------------------------------------------ *}
---"marescpla, pabflomar"
+--"marescpla, pabflomar,jaisalmen, zoiruicha"
   lemma 02:
@@ Línea 243: / Línea 243: @@
---"marescpla"
+--"marescpla,jaisalmen, zoiruicha"
    lemma 03:
        assumes 1:"¬(p ∨ q)"
@@ Línea 326: / Línea 326: @@
 qed
--- "diecabmen1 domlloriv"
+-- "diecabmen1 domlloriv,jaisalmen, zoiruicha"
 lemma Ejercicio_4:
    assumes "¬p ∧ ¬q"
@@ Línea 431: / Línea 431: @@
    ------------------------------------------------------------------ *}
--- "maresccas4 diecabmen1 domlloriv, julrobrel"
+-- "maresccas4 diecabmen1 domlloriv, julrobrel,jaisalmen, zoiruicha"
 lemma
    assumes "¬p ∨ ¬q"
@@ Línea 543: / Línea 543: @@
       ⊢ ((p ⟶ q) ⟶ p) ⟶ p
    ------------------------------------------------------------------ *}
--- "diecabmen1 maresccas4 pabflomar juaruipav domlloriv"
+-- "diecabmen1 maresccas4 pabflomar juaruipav domlloriv,jaisalmen, zoiruicha"
 lemma Ejercicio_6:
    shows "((p ⟶ q) ⟶ p) ⟶ p"
@@ Línea 617: / Línea 617: @@
---"marescpla"
+--"marescpla,jaisalmen, zoiruicha"
    lemma 07:
      assumes "¬q ⟶ ¬p"

@@ Línea 52: / Línea 52: @@
    ------------------------------------------------------------------ *}
---"marescpla, pabflomar"
+--"marescpla, pabflomar, jaisalmen, zoiruicha"
    lemma 01:

@@ Línea 642: / Línea 642: @@
---"juaruipav, julrobrel"
+--"juaruipav, julrobrel, domlloriv"
 lemma ej7_juaruipav:
@@ Línea 799: / Línea 799: @@
       ¬(p ∧ q) ⊢ ¬p ∨ ¬q
    ------------------------------------------------------------------ *}
--- "pabflomar, julrobrel, juaruipav"
+-- "pabflomar, julrobrel, juaruipav, domlloriv"
 lemma ej10_pfm:
    assumes "¬(p ∧ q)"

@@ Línea 799: / Línea 799: @@
       ¬(p ∧ q) ⊢ ¬p ∨ ¬q
    ------------------------------------------------------------------ *}
--- "pabflomar, julrobrel"
+-- "pabflomar, julrobrel, juaruipav"
 lemma ej10_pfm:
    assumes "¬(p ∧ q)"
@@ Línea 974: / Línea 974: @@
 qed
--- "irealetei domlloriv"
+-- "irealetei domlloriv juaruipav"
 lemma ej11_auto:"(p ⟶ q) ∨ (q ⟶ p)"

@@ Línea 81: / Línea 81: @@
 qed
---"juaruipav"
+--"juaruipav, julrobrel"
   lemma ej1_juaruipav:
   assumes 1:"p ∨ q"
@@ Línea 95: / Línea 95: @@
 qed
---"irealetei"
+--"irealetei, julrobrel"
 lemma ej1_auto:
    assumes 1:"p ∨ q"
@@ Línea 182: / Línea 182: @@
   qed
---"irealetei"
+--"irealetei, julrobrel"
 lemma ej2_auto:
    assumes 1:"p ∧ q"
@@ Línea 281: / Línea 281: @@
    qed
---"irealetei"
+--"irealetei, julrobrel"
 lemma ej3_auto:
    assumes "¬(p ∨ q)"
@@ Línea 385: / Línea 385: @@
 qed
---"juaruipav"
+--"juaruipav, julrobrel"
 lemma ej4_juaruipav:
 assumes 1:" ¬p ∧ ¬q"
@@ Línea 431: / Línea 431: @@
    ------------------------------------------------------------------ *}
--- "maresccas4 diecabmen1 domlloriv"
+-- "maresccas4 diecabmen1 domlloriv, julrobrel"
 lemma
    assumes "¬p ∨ ¬q"
@@ Línea 580: / Línea 580: @@
    qed
---"irealetei"
+--"irealetei, julrobrel"
 lemma ej6_auto:"((p ⟶ q) ⟶ p) ⟶ p"
 using assms by auto
@@ Línea 642: / Línea 642: @@
---"juaruipav"
+--"juaruipav, julrobrel"
 lemma ej7_juaruipav:
@@ Línea 709: / Línea 709: @@
    qed
---"irealetei"
+--"irealetei, julrobrel"
 lemma ej8_auto:
     assumes "¬(¬p ∧ ¬q)"
@@ Línea 773: / Línea 773: @@
    qed
---"irealetei"
+--"irealetei, julrobrel"
 lemma ej9_auto:
     assumes "¬(¬p ∨ ¬q)"
@@ Línea 799: / Línea 799: @@
       ¬(p ∧ q) ⊢ ¬p ∨ ¬q
    ------------------------------------------------------------------ *}
--- "pabflomar"
+-- "pabflomar, julrobrel"
 lemma ej10_pfm:
    assumes "¬(p ∧ q)"
@@ Línea 948: / Línea 948: @@
 qed
--- "pabflomar"
+-- "pabflomar, julrobrel"
 {* Sólo cambia respecto de marco en el cambio del . por by this *}
 lemma

@@ Línea 67: / Línea 67: @@
    qed
---"diecabmen1 maresccas4"
+--"diecabmen1 maresccas4 domlloriv"
 lemma Ejercicio_1:
    assumes "p ∨ q"
@@ Línea 142: / Línea 142: @@
     qed
---"diecabmen1 maresccas4"
+--"diecabmen1 maresccas4 domlloriv"
 lemma Ejercicio_2:
    assumes "p ∧ q"
@@ Línea 226: / Línea 226: @@
 qed
--- "diecabmen1 pabflomar"
+-- "diecabmen1 pabflomar domlloriv"
 lemma Ejercicio_3:
    assumes "¬(p ∨ q)"
@@ Línea 326: / Línea 326: @@
 qed
--- "diecabmen1"
+-- "diecabmen1 domlloriv"
 lemma Ejercicio_4:
    assumes "¬p ∧ ¬q"
@@ Línea 431: / Línea 431: @@
    ------------------------------------------------------------------ *}
--- "maresccas4 diecabmen1"
+-- "maresccas4 diecabmen1 domlloriv"
 lemma
    assumes "¬p ∨ ¬q"
@@ Línea 543: / Línea 543: @@
       ⊢ ((p ⟶ q) ⟶ p) ⟶ p
    ------------------------------------------------------------------ *}
--- "diecabmen1 maresccas4 pabflomar juaruipav"
+-- "diecabmen1 maresccas4 pabflomar juaruipav domlloriv"
 lemma Ejercicio_6:
    shows "((p ⟶ q) ⟶ p) ⟶ p"
@@ Línea 730: / Línea 730: @@
       ¬(¬p ∨ ¬q) ⊢ p ∧ q
    ------------------------------------------------------------------ *}
--- "diecabmen1, maresccas4"
+-- "diecabmen1, maresccas4 domlloriv"
 lemma Ejercicio_9:
    assumes "¬(¬p ∨ ¬q)"
@@ Línea 974: / Línea 974: @@
 qed
--- "irealetei"
+-- "irealetei domlloriv"
 lemma ej11_auto:"(p ⟶ q) ∨ (q ⟶ p)"

@@ Línea 580: / Línea 580: @@
    qed
 text {* ---------------------------------------------------------------
@@ Línea 955: / Línea 974: @@
 qed
 end
 </source>

← Revisión anterior		Revisión del 12:14 29 ene 2014
Línea 840:		Línea 840:
	with assms(1) show False ..		with assms(1) show False ..
	qed		qed
−
−	~~--"irealetei"~~