Relación 7 - Historial de revisiones

Jalonso: Protegió «Relación 7» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

2019-03-06T18:50:45Z

Protegió «Relación 7» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Jalonso en 17:22 4 mar 2019

2019-03-04T17:22:29Z

Mostrar los cambios

Aribatval en 15:46 4 mar 2019

2019-03-04T15:46:08Z

Mostrar los cambios

Aribatval en 15:20 4 mar 2019

2019-03-04T15:20:11Z

Chrgencar en 13:35 4 mar 2019

2019-03-04T13:35:36Z

Alikan en 11:24 4 mar 2019

2019-03-04T11:24:53Z

Enrparalv en 11:07 4 mar 2019

2019-03-04T11:07:46Z

Jalonso en 13:13 28 feb 2019

2019-02-28T13:13:59Z

Jalonso en 13:12 28 feb 2019

2019-02-28T13:12:45Z

Mostrar los cambios

Antramhur en 20:19 26 feb 2019

2019-02-26T20:19:12Z

@@ Línea 52: / Línea 52: @@
 (* pabalagon manperjim josgomrom4 cammonagu raffergon2 chrgencar
     gleherlop giafus1 marfruman1 enrparalv pabbergue antramhur alikan
-    juacanrod hugrubsan *)
+    juacanrod hugrubsan aribatval*)
 lemma ejercicio_1:
    assumes 1: "p ⟶ q" and
@@ Línea 76: / Línea 76: @@
 (* pabalagon manperjim josgomrom4 cammonagu gleherlop raffergon2
     chrgencar giafus1 marfruman1 alfmarcua enrparalv pabbergue antramhur
-    alikan juacanrod hugrubsan *)
+    alikan juacanrod hugrubsan aribatval*)
 lemma ejercicio_2:
    assumes 1: "p ⟶ q" and
@@ Línea 105: / Línea 105: @@
 (* pabalagon manperjim josgomrom4 cammonagu gleherlop raffergon2
     chrgencar giafus1 marfruman1 alfmarcua enrparalv pabbergue antramhur
-    alikan juacanrod hugrubsan *)
+    alikan juacanrod hugrubsan aribatval*)
 lemma ejercicio_3:
    assumes 1: "p ⟶ (q ⟶ r)" and
@@ Línea 136: / Línea 136: @@
 (* pabalagon manperjim josgomrom4 cammonagu chrgencar raffergon2
     gleherlop giafus1 marfruman1 alfmarcua enrparalv pabbergue antramhur
-    alikan juacanrod hugrubsan *)
+    alikan juacanrod hugrubsan aribatval*)
 lemma ejercicio_4:
    assumes 1: "p ⟶ q" and
@@ Línea 165: / Línea 165: @@
 (* pabalagon manperjim raffergon2 giafus1 gleherlop marfruman1 alfmarcua
-    enrparalv chrgencar pabbergue antramhur alikan hugrubsan *)
+    enrparalv chrgencar pabbergue antramhur alikan hugrubsan aribatval*)
 lemma ejercicio_5:
    assumes 1: "p ⟶ (q ⟶ r)"
@@ Línea 214: / Línea 214: @@
 (* pabalagon manperjim cammonagu chrgencar raffergon2 gleherlop giafus1
     marfruman1 alfmarcua enrparalv pabbergue  antramhur alikan juacanrod
-    hugrubsan *)
+    hugrubsan aribatval*)
 lemma ejercicio_6:
    assumes 1: "p ⟶ (q ⟶ r)"
@@ Línea 250: / Línea 250: @@
 (* pabalagon manperjim josgomrom4 raffergon2 giafus1 gleherlop
-    marfruman1 enrparalv pabbergue antramhur alikan hugrubsan *)
+    marfruman1 enrparalv pabbergue antramhur alikan hugrubsan aribatval*)
 lemma ejercicio_7:
    assumes 1: "p"
@@ Línea 279: / Línea 279: @@
 (* pabalagon manperjim josgomrom4 raffergon2 giafus1 marfruman1
-    enrparalv pabbergue antramhur alikan hugrubsan *)
+    enrparalv pabbergue antramhur alikan hugrubsan aribatval*)
 lemma ejercicio_8:
    "p ⟶ (q ⟶ p)"
@@ Línea 302: / Línea 302: @@
 (* pabalagon manperjim raffergon2 giafus1 marfruman1 alfmarcua enrparalv
-    gleherlop antramhur alikan hugrubsan *)
+    gleherlop antramhur alikan hugrubsan aribatval*)
 lemma ejercicio_9:
    assumes 1: "p ⟶ q"
@@ Línea 336: / Línea 336: @@
 (* pabalagon manperjim raffergon2 marfruman1 gleherlop alfmarcua
-    enrparalv pabbergue antramhur alikan juacanrod hugrubsan *)
+    enrparalv pabbergue antramhur alikan juacanrod hugrubsan aribatval*)
 lemma ejercicio_10:
    assumes 1: "p ⟶ (q ⟶ (r ⟶ s))"

@@ Línea 957: / Línea 957: @@
 (* pabalagon manperjim marfruman1 josgomrom4 alfmarcua pabbergue
-    gleherlop antramhur enrparalv juacanrod hugrubsan alikan *)
+    gleherlop antramhur enrparalv juacanrod hugrubsan alikan chrgencar *)
 lemma ejercicio_31:
    assumes 1: "p ∨ (q ∨ r)"
@@ Línea 1008: / Línea 1008: @@
 (* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop
-    pabbergue antramhur enrparalv juacanrod hugrubsan alikan *)
+    pabbergue antramhur enrparalv juacanrod hugrubsan alikan chrgencar *)
 lemma ejercicio_32:
    assumes 1: "(p ∨ q) ∨ r"
@@ Línea 1058: / Línea 1058: @@
 (* pabalagon manperjim marfruman1 josgomrom4 chrgencar gleherlop
-    alfmarcua pabbergue antramhur enrparalv juacanrod hugrubsan alikan *)
+    alfmarcua pabbergue antramhur enrparalv juacanrod hugrubsan alikan
 lemma ejercicio_33:
    assumes 1: "p ∧ (q ∨ r)"
@@ Línea 1254: / Línea 1255: @@
 (* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop
-    pabbergue antramhur enrparalv juacanrod hugrubsan alikan *)
+    pabbergue antramhur enrparalv juacanrod hugrubsan alikan chrgencar *)
 lemma ejercicio_37:
    assumes 1: "(p ⟶ r) ∧ (q ⟶ r)"
@@ Línea 1294: / Línea 1295: @@
 (* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop
-    pabbergue antramhur enrparalv juacanrod hugrubsan alikan *)
+    pabbergue antramhur enrparalv juacanrod hugrubsan alikan chrgencar *)
 lemma ejercicio_38:
    assumes "p ∨ q ⟶ r"
@@ Línea 1353: / Línea 1354: @@
 (* pabalagon manperjim marfruman1 josgomrom4 alfmarcua pabbergue
-    gleherlop juacanrod enrparalv hugrubsan alikan *)
+    gleherlop juacanrod enrparalv hugrubsan alikan chrgencar *)
 lemma ejercicio_40:
    assumes 1: "¬p"
@@ Línea 1376: / Línea 1377: @@
 (* pabalagon manperjim raffergon2 josgomrom4 marfruman1 alfmarcua
-    pabbergue gleherlop enrparalv juacanrod hugrubsan alikan *)
+    pabbergue gleherlop chrgencar enrparalv juacanrod hugrubsan alikan *)
 lemma ejercicio_41:
    assumes 1: "p ⟶ q"
@@ Línea 1399: / Línea 1400: @@
 (* pabalagon manperjim raffergon2 josgomrom4 marfruman1 alfmarcua
-    pabbergue gleherlop enrparalv juacanrod hugrubsan alikan *)
+    pabbergue gleherlop chrgencar enrparalv juacanrod hugrubsan alikan *)
 lemma ejercicio_42:
    assumes "p∨q"
@@ Línea 1431: / Línea 1432: @@
 (* pabalagon manperjim raffergon2 josgomrom4 marfruman1 alfmarcua
-    pabbergue gleherlop enrparalv juacanrod hugrubsan alikan *)
+    pabbergue gleherlop chrgencar enrparalv juacanrod hugrubsan alikan *)
 lemma ejercicio_43:
    assumes "p ∨ q"
@@ Línea 1463: / Línea 1464: @@
 (* pabalagon manperjim gleherlop josgomrom4 marfruman1 pabbergue
-    juacanrod hugrubsan alikan *)
+    juacanrod hugrubsan alikan chrgencar *)
 lemma ejercicio_44:
    assumes "p ∨ q"
@@ Línea 1504: / Línea 1505: @@
 (* pabalagon manperjim marfruman1 josgomrom4 gleherlop pabbergue
-    juacanrod hugrubsan alikan *)
+    juacanrod hugrubsan alikan chrgencar *)
 lemma ejercicio_45:
    assumes 1: "p ∧ q"
@@ Línea 1544: / Línea 1545: @@
 (* pabalagon manperjim marfruman1 josgomrom4 gleherlop pabbergue
-    juacanrod hugrubsan alikan *)
+    juacanrod hugrubsan alikan chrgencar *)
 lemma ejercicio_46:
    assumes 1: "¬(p ∨ q)"
@@ Línea 1619: / Línea 1620: @@
 qed
-(* benber gleherlop cammonagu*)
+(* benber gleherlop cammonagu chrgencar *)
 lemma ejercicio_47_1:
    assumes "¬p ∧ ¬q"
@@ Línea 1662: / Línea 1663: @@
 qed
-(* benber alfmarcua gleherlop cammonagu *)
+(* benber alfmarcua gleherlop cammonagu chrgencar *)
 lemma ejercicio_48_1:
    assumes "¬p ∨ ¬q"
@@ Línea 1678: / Línea 1679: @@
 (* pabalagon manperjim marfruman1 josgomrom4 alfmarcu gleherlop
-    hugrubsan juacanrod cammonagu alikan *)
+    hugrubsan juacanrod cammonagu alikan chrgencar *)
 lemma ejercicio_49:
    "¬(p ∧ ¬p)"
@@ Línea 1703: / Línea 1704: @@
 (* pabalagon manperjim raffergon2 josgomrom4 marfruman1 gleherlop
-    alfmarcua enrparalv pabbergue juacanrod hugrubsan alikan *)
+    alfmarcua enrparalv pabbergue juacanrod hugrubsan alikan chrgencar *)
 lemma ejercicio_50:
    assumes 1: "p ∧ ¬p"
@@ Línea 1728: / Línea 1729: @@
 (* pabalagon manperjim benber raffergon2 josgomrom4 marfruman1 gleherlop
-    alfmarcua enrparalv pabbergue juacanrod hugrubsan cammmonagu alikan *)
+    alfmarcua enrparalv pabbergue juacanrod hugrubsan cammmonagu alikan
 lemma ejercicio_51:
    assumes "¬¬p"
@@ Línea 1739: / Línea 1741: @@
    ------------------------------------------------------------------ *}
-(* pabalagon manperjim marfruman1 josgomrom4 juacanrod pabbergue alikan enrparalv *)
+(* pabalagon manperjim marfruman1 josgomrom4 juacanrod pabbergue alikan enrparalv
 lemma ejercicio_52:
    "p ∨ ¬p"
@@ Línea 1781: / Línea 1784: @@
 (* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop
-    juacanrod pabbergue enrparalv *)
+    juacanrod pabbergue enrparalv chrgencar *)
 lemma ejercicio_53:
    "((p ⟶ q) ⟶ p) ⟶ p"
@@ Línea 1817: / Línea 1820: @@
 (* pabalagon manperjim marfruman1 josgomrom4 gleherlop juacanrod
-    pabbergue enrparalv *)
+    pabbergue enrparalv chrgencar *)
 lemma ejercicio_54:
    assumes 1: "¬q ⟶ ¬p"
@@ Línea 1880: / Línea 1883: @@
 (* pabalagon manperjim marfruman1 josgomrom4 gleherlop juacanrod
-    pabbergue enrparalv *)
+    pabbergue enrparalv chrgencar *)
 lemma ejercicio_56:
    assumes 1: "¬(¬p ∨ ¬q)"
@@ Línea 1918: / Línea 1921: @@
 (* pabalagon manperjim marfruman1 josgomrom4 gleherlop juacanrod
-    pabbergue enrparalv *)
+    pabbergue enrparalv chrgencar *)
 lemma ejercicio_57:
    assumes 1: "¬(p ∧ q)"
@@ Línea 1987: / Línea 1990: @@
 qed
-(* pabalagon gleherlop *)
+(* pabalagon gleherlop chrgencar *)
 lemma ejercicio_58_2:
    "(p ⟶ q) ∨ (q ⟶ p)"

@@ Línea 596: / Línea 596: @@
    ------------------------------------------------------------------ *}
-(* pabalagon raffergon2 marfruman1 juacanrod alikan*)
+(* pabalagon raffergon2 marfruman1 juacanrod alikan *)
 lemma ejercicio_18:
    assumes "p ∧ q"

@@ Línea 1739: / Línea 1739: @@
    ------------------------------------------------------------------ *}
-(* pabalagon manperjim marfruman1 josgomrom4 juacanrod pabbergue alikan *)
+(* pabalagon manperjim marfruman1 josgomrom4 juacanrod pabbergue alikan enrparalv *)
 lemma ejercicio_52:
    "p ∨ ¬p"
@@ Línea 1781: / Línea 1781: @@
 (* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop
-    juacanrod pabbergue *)
+    juacanrod pabbergue enrparalv *)
 lemma ejercicio_53:
    "((p ⟶ q) ⟶ p) ⟶ p"
@@ Línea 1817: / Línea 1817: @@
 (* pabalagon manperjim marfruman1 josgomrom4 gleherlop juacanrod
-    pabbergue *)
+    pabbergue enrparalv *)
 lemma ejercicio_54:
    assumes 1: "¬q ⟶ ¬p"
@@ Línea 1864: / Línea 1864: @@
 qed
-(* benber alfmarcua josgomrom4 manperjim pabbergue juacanrod cammonagu *)
+(* benber alfmarcua josgomrom4 manperjim pabbergue juacanrod cammonagu enrparalv *)
 lemma ejercicio_55_1:
    assumes "¬(¬p ∧ ¬q)"
@@ Línea 1880: / Línea 1880: @@
 (* pabalagon manperjim marfruman1 josgomrom4 gleherlop juacanrod
-    pabbergue *)
+    pabbergue enrparalv *)
 lemma ejercicio_56:
    assumes 1: "¬(¬p ∨ ¬q)"
@@ Línea 1918: / Línea 1918: @@
 (* pabalagon manperjim marfruman1 josgomrom4 gleherlop juacanrod
-    pabbergue *)
+    pabbergue enrparalv *)
 lemma ejercicio_57:
    assumes 1: "¬(p ∧ q)"
@@ Línea 1958: / Línea 1958: @@
    ------------------------------------------------------------------ *}
-(* pabalagon manperjim josgomrom4 marfruman1 juacanrod pabbergue *)
+(* pabalagon manperjim josgomrom4 marfruman1 juacanrod pabbergue enrparalv *)
 lemma ejercicio_58:
    "(p ⟶ q) ∨ (q ⟶ p)"

@@ Línea 2: / Línea 2: @@
 chapter {* R6: Deducción natural proposicional *}
-theory R6_Deduccion_natural_proposicional_alu
+theory R6_Deduccion_natural_proposicional
 imports Main
 begin

← Revisión anterior	Revisión del 18:50 6 mar 2019
(Sin diferencias)

@@ Línea 140: / Línea 140: @@
 qed
-(* pabalagon manperjim josgomrom4 gleherlop marfruman1 raffergon2 hugrubsan pabbergue enrparalv giafus1 *)
+(* pabalagon manperjim josgomrom4 gleherlop marfruman1 raffergon2 hugrubsan pabbergue enrparalv giafus1 antramhur *)
 lemma ejercicio_1:
    assumes "P a ⟶ (∃x. Q x)"
@@ Línea 249: / Línea 249: @@
-(* pabalagon manperjim josgomrom4 gleherlop raffergon2 hugrubsan pabbergue giafus1 *)
+(* pabalagon manperjim josgomrom4 gleherlop raffergon2 hugrubsan pabbergue giafus1 antramhur *)
 lemma ejercicio_2:
    assumes "∀x y z. R x y ∧ R y z ⟶ R x z"
@@ Línea 319: / Línea 319: @@
    oops
-(* pabalagon manperjim pabbergue josgomrom4 gleherlop hugrubsan giafus1 *)
+(* pabalagon manperjim pabbergue josgomrom4 gleherlop hugrubsan giafus1 antramhur *)
 text{*
 Contraejemplo en los naturales, para todo x existe y tal que x < y, pero no
@@ Línea 358: / Línea 358: @@
 qed
-(* pabalagon manperjim josgomrom4 gleherlop hugrubsan pabbergue *)
+(* pabalagon manperjim josgomrom4 gleherlop hugrubsan pabbergue antramhur *)
 lemma ejercicio_4: "(∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)"
 proof (rule impI)
@@ Línea 406: / Línea 406: @@
 qed
-(* pabalagon manperjim josgomrom4 gleherlop marfruman1 raffergon2 hugrubsan pabbergue giafus1 *)
+(* pabalagon manperjim josgomrom4 gleherlop marfruman1 raffergon2 hugrubsan pabbergue giafus1 antramhur *)
 lemma ejercicio_5:
    assumes "∀x. P a x x"
@@ Línea 437: / Línea 437: @@
 qed
-(* pabalagon manperjim josgomrom4 gleherlop marfruman1 raffergon2 hugrubsan pabbergue enrparalv *)
+(* pabalagon manperjim josgomrom4 gleherlop marfruman1 raffergon2 hugrubsan pabbergue enrparalv antramhur *)
 lemma ejercicio_6:
    assumes "∀y. Q a y"
@@ Línea 468: / Línea 468: @@
    ------------------------------------------------------------------ *}
-(* benber manperjim alfmarcua pabalagon marfruman1 josgomrom4 gleherlop raffergon2 hugrubsan pabbergue enrparalv giafus1 *)
+(* benber manperjim alfmarcua pabalagon marfruman1 josgomrom4 gleherlop raffergon2 hugrubsan pabbergue enrparalv giafus1
 lemma
    assumes "A ∨ P ⟶ R ∧ F"
@@ Línea 536: / Línea 537: @@
 qed
-(* pabalagon manperjim josgomrom4 gleherlop raffergon2 hugrubsan pabbergue enrparalv giafus1 *)
+(* pabalagon manperjim josgomrom4 gleherlop raffergon2 hugrubsan pabbergue enrparalv giafus1 antramhur *)
 lemma ejercicio_8:
    assumes "A ⟶ (M ⟷ ¬B)"
@@ Línea 677: / Línea 678: @@
 qed
-(* pabalagon manperjim marfruman1 josgomrom4 gleherlop raffergon2 hugrubsan pabbergue enrparalv giafus1 *)
+(* pabalagon manperjim marfruman1 josgomrom4 gleherlop raffergon2 hugrubsan pabbergue enrparalv giafus1 antramhur *)
 lemma ejercicio_9:
    assumes "∀x. ¬R x ⟶ R (p x)"
@@ Línea 793: / Línea 794: @@
 qed
-(* pabalagon manperjim josgomrom4 gleherlop raffergon2 hugrubsan pabbergue enrparalv giafus1 *)
+(* pabalagon manperjim josgomrom4 gleherlop raffergon2 hugrubsan pabbergue enrparalv giafus1 antramhur *)
 lemma ejercicio_10:
    assumes "∀x y. Af x ∧ E y ⟶ Ap x y"
@@ Línea 866: / Línea 867: @@
 qed
-(* pabalagon manperjim marfruman1 josgomrom4 gleherlop hugrubsan pabbergue enrparalv giafus1 *)
+(* pabalagon manperjim marfruman1 josgomrom4 gleherlop hugrubsan pabbergue enrparalv giafus1 antramhur *)
 lemma ejercicio_11:
    assumes "¬(∃x. P x ∧ R x)"