{"id":4833,"date":"2015-03-16T17:20:16","date_gmt":"2015-03-16T16:20:16","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4833"},"modified":"2015-03-30T17:31:33","modified_gmt":"2015-03-30T15:31:33","slug":"lmf2015-ejercicios-de-deduccion-natural-en-logica-proposicional-con-isabellehol","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/lmf2015-ejercicios-de-deduccion-natural-en-logica-proposicional-con-isabellehol\/","title":{"rendered":"LMF2015: Ejercicios de deducci\u00f3n natural en l\u00f3gica proposicional con Isabelle\/HOL"},"content":{"rendered":"<p>En la clase de hoy del curso <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf-14\">L\u00f3gica matem\u00e1tica y fundamentos<\/a> se han comentado soluciones de los ejercicios de deducci\u00f3n natural en l\u00f3gica proposicional con Isabelle\/HOL.<\/p>\n<p>Para cada uno de los ejercicios se ha presentado distintas demostraciones: desde la detallada (que sea parecida a la mostrada en las transparencias) hasta la autom\u00e1tica.<\/p>\n<p>La teor\u00eda con la relaci\u00f3n de ejercicios y sus soluciones es la siguiente<br \/>\n<!--more--><\/p>\n<pre lang=\"isar\">\nheader {* R3: Deducci\u00f3n natural en l\u00f3gica proposicional con Isabelle\/HOL *}\n\ntheory R3\nimports Main \nbegin\n\ntext {*\n  --------------------------------------------------------------------- \n  El objetivo de esta relaci\u00f3n es lemas usando s\u00f3lo las reglas b\u00e1sicas\n  de deducci\u00f3n natural de la l\u00f3gica proposicional. \n\n  Los ejercicios son los de la asignatura de \"L\u00f3gica inform\u00e1tica\" que se\n  encuentran en http:\/\/goo.gl\/yrPLn\n\n  Las reglas b\u00e1sicas de la deducci\u00f3n natural son las siguientes:\n  \u00b7 conjI:      \u27e6P; Q\u27e7 \u27f9 P \u2227 Q\n  \u00b7 conjunct1:  P \u2227 Q \u27f9 P\n  \u00b7 conjunct2:  P \u2227 Q \u27f9 Q  \n  \u00b7 notnotD:    \u00ac\u00ac P \u27f9 P\n  \u00b7 notnotI:    P \u27f9 \u00ac\u00ac P\n  \u00b7 mp:         \u27e6P \u27f6 Q; P\u27e7 \u27f9 Q \n  \u00b7 mt:         \u27e6F \u27f6 G; \u00acG\u27e7 \u27f9 \u00acF \n  \u00b7 impI:       (P \u27f9 Q) \u27f9 P \u27f6 Q\n  \u00b7 disjI1:     P \u27f9 P \u2228 Q\n  \u00b7 disjI2:     Q \u27f9 P \u2228 Q\n  \u00b7 disjE:      \u27e6P \u2228 Q; P \u27f9 R; Q \u27f9 R\u27e7 \u27f9 R \n  \u00b7 FalseE:     False \u27f9 P\n  \u00b7 notE:       \u27e6\u00acP; P\u27e7 \u27f9 R\n  \u00b7 notI:       (P \u27f9 False) \u27f9 \u00acP\n  \u00b7 iffI:       \u27e6P \u27f9 Q; Q \u27f9 P\u27e7 \u27f9 P = Q\n  \u00b7 iffD1:      \u27e6Q = P; Q\u27e7 \u27f9 P \n  \u00b7 iffD2:      \u27e6P = Q; Q\u27e7 \u27f9 P\n  \u00b7 ccontr:     (\u00acP \u27f9 False) \u27f9 P\n  \u00b7 excluded_middle: \u00acP \u2228 P\n  --------------------------------------------------------------------- \n*}\n\ntext {*\n  Se usar\u00e1n las reglas notnotI y mt que demostramos a continuaci\u00f3n.\n  *}\n\nlemma notnotI: \"P \u27f9 \u00ac\u00ac P\"\nby auto\n\nlemma mt: \"\u27e6F \u27f6 G; \u00acG\u27e7 \u27f9 \u00acF\"\nby auto\n\nsection {* Implicaciones *}\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 1. Demostrar\n       p \u27f6 q, p \u22a2 q\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_1_1:\n  assumes 1: \"p \u27f6 q\" and\n          2: \"p\"\n  shows \"q\"\nproof - \n   show \"q\" using 1 2 by (rule mp)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_1_2:\n  assumes \"p \u27f6 q\"\n          \"p\"\n  shows \"q\"\nproof - \n   show \"q\" using assms ..\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_1_3:\n  assumes \"p \u27f6 q\"\n          \"p\"\n  shows \"q\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 2. Demostrar\n     p \u27f6 q, q \u27f6 r, p \u22a2 r\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_2_1:\n  assumes 1: \"p \u27f6 q\" and \n          2: \"q \u27f6 r\" and \n          3: \"p\" \n  shows \"r\"\nproof -\n  have 4: \"q\" using 1 3 by (rule mp)\n  show \"r\" using 2 4 by (rule mp)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_2_2:\n  assumes \"p \u27f6 q\"\n          \"q \u27f6 r\"\n          \"p\" \n  shows \"r\"\nproof -\n  have \"q\" using assms(1,3) ..\n  show \"r\" using assms(2) `q` ..\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_2_3:\n  assumes \"p \u27f6 q\"\n          \"q \u27f6 r\"\n          \"p\" \n  shows \"r\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 3. Demostrar\n     p \u27f6 (q \u27f6 r), p \u27f6 q, p \u22a2 r\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_3_1:\n  assumes 1: \"p \u27f6 (q \u27f6 r)\" and \n          2: \"p \u27f6 q\" and  \n          3: \"p\"\n  shows \"r\"\nproof -\n  have 4: \"q\" using 2 3 by (rule mp)\n  have 5: \"q \u27f6 r\" using 1 3 by (rule mp)\n  show \"r\" using 5 4 by (rule mp)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_3_2:\n  assumes \"p \u27f6 (q \u27f6 r)\"\n          \"p \u27f6 q\"\n          \"p\"\n  shows   \"r\"\nproof -\n  have \"q\" using assms(2,3) ..\n  have \"q \u27f6 r\" using assms(1,3) ..\n  thus \"r\" using `q` ..\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_3_3:\n  assumes \"p \u27f6 (q \u27f6 r)\"\n          \"p \u27f6 q\"\n          \"p\"\n  shows   \"r\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 4. Demostrar\n     p \u27f6 q, q \u27f6 r \u22a2 p \u27f6 r\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_4_1:\n  assumes 1: \"p \u27f6 q\" and \n          2: \"q \u27f6 r\" \n  shows \"p \u27f6 r\"\nproof (rule impI)\n  assume 3: \"p\"\n  have 4: \"q\" using 1 3 by (rule mp)\n  show \"r\" using 2 4 by (rule mp)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_4_2:\n  assumes \"p \u27f6 q\"\n          \"q \u27f6 r\" \n  shows   \"p \u27f6 r\"\nproof\n  assume \"p\"\n  with assms(1) have \"q\" ..\n  with assms(2) show \"r\" ..\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_4_3:\n  assumes \"p \u27f6 q\"\n          \"q \u27f6 r\" \n  shows   \"p \u27f6 r\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 5. Demostrar\n     p \u27f6 (q \u27f6 r) \u22a2 q \u27f6 (p \u27f6 r)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_5_1:\n  assumes 1: \"p \u27f6 (q \u27f6 r)\" \n  shows   \"q \u27f6 (p \u27f6 r)\"\nproof (rule impI)\n  assume 2: \"q\"\n  show \"p \u27f6 r\"\n  proof (rule impI)\n    assume 3: \"p\"\n    have \"q \u27f6 r\" using 1 3 by (rule mp)\n    thus \"r\" using 2 by (rule mp)\n  qed\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_5_2:\n  assumes \"p \u27f6 (q \u27f6 r)\" \n  shows   \"q \u27f6 (p \u27f6 r)\"\nproof \n  assume \"q\"\n  show \"p \u27f6 r\"\n  proof \n    assume \"p\"\n    with assms(1) have \"q \u27f6 r\" ..\n    thus \"r\" using `q` ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_5_3:\n  assumes \"p \u27f6 (q \u27f6 r)\" \n  shows   \"q \u27f6 (p \u27f6 r)\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 6. Demostrar\n     p \u27f6 (q \u27f6 r) \u22a2 (p \u27f6 q) \u27f6 (p \u27f6 r)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_6_1:\n  assumes 1: \"p \u27f6 (q \u27f6 r)\" \n  shows   \"(p \u27f6 q) \u27f6 (p \u27f6 r)\"\nproof (rule impI)\n  assume 2: \"p \u27f6 q\"\n  show \"p \u27f6 r\"\n  proof (rule impI)\n    assume 3: \"p\"\n    have 4: \"q\" using 2 3 by (rule mp)\n    have 5: \"q \u27f6 r\" using 1 3 by (rule mp)\n    show \"r\" using 5 4 by (rule mp)\n  qed\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_6_2:\n  assumes \"p \u27f6 (q \u27f6 r)\" \n  shows   \"(p \u27f6 q) \u27f6 (p \u27f6 r)\"\nproof \n  assume \"p \u27f6 q\"\n  show \"p \u27f6 r\"\n  proof \n    assume \"p\"\n    with `p \u27f6 q` have \"q\" ..\n    have \"q \u27f6 r\" using assms(1) `p` ..\n    thus \"r\" using `q` ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_6_3:\n  assumes \"p \u27f6 (q \u27f6 r)\" \n  shows   \"(p \u27f6 q) \u27f6 (p \u27f6 r)\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 7. Demostrar\n     p \u22a2 q \u27f6 p\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_7_1:\n  assumes 1: \"p\"  \n  shows      \"q \u27f6 p\"\nproof (rule impI)\n  assume 2: \"q\"\n  show \"p\" using 1 by this\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_7_2:\n  assumes \"p\"  \n  shows   \"q \u27f6 p\"\nproof \n  assume \"q\"\n  show \"p\" using assms(1) .\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_7_3:\n  assumes \"p\"  \n  shows   \"q \u27f6 p\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 8. Demostrar\n     \u22a2 p \u27f6 (q \u27f6 p)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_8_1:\n  \"p \u27f6 (q \u27f6 p)\"\nproof (rule impI)\n  assume 1: \"p\"\n  show \"q \u27f6 p\"\n  proof (rule impI)\n    assume 2: \"q\"\n    show \"p\" using 1 by this\n  qed\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_8_2:\n  \"p \u27f6 (q \u27f6 p)\"\nproof \n  assume \"p\"\n  show \"q \u27f6 p\"\n  proof \n    assume \"q\"\n    show \"p\" using `p` .\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_8_3:\n  \"p \u27f6 (q \u27f6 p)\"\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 9. Demostrar\n     p \u27f6 q \u22a2 (q \u27f6 r) \u27f6 (p \u27f6 r)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_9_1:\n  assumes 1: \"p \u27f6 q\" \n  shows      \"(q \u27f6 r) \u27f6 (p \u27f6 r)\"\nproof (rule impI)\n  assume 2: \"q \u27f6 r\"\n  show \"p \u27f6 r\"\n  proof (rule impI)\n    assume 3: \"p\"\n    have 4: \"q\" using 1 3 by (rule mp)\n    show \"r\" using 2 4 by (rule mp) \n  qed\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_9_2:\n  assumes \"p \u27f6 q\" \n  shows   \"(q \u27f6 r) \u27f6 (p \u27f6 r)\"\nproof \n  assume \"q \u27f6 r\"\n  show \"p \u27f6 r\"\n  proof \n    assume \"p\"\n    with assms(1) have \"q\" ..\n    with `q \u27f6 r` show \"r\" ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_9_3:\n  assumes \"p \u27f6 q\" \n  shows   \"(q \u27f6 r) \u27f6 (p \u27f6 r)\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 10. Demostrar\n     p \u27f6 (q \u27f6 (r \u27f6 s)) \u22a2 r \u27f6 (q \u27f6 (p \u27f6 s))\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_10_1:\n  assumes 1: \"p \u27f6 (q \u27f6 (r \u27f6 s))\" \n  shows      \"r \u27f6 (q \u27f6 (p \u27f6 s))\"\nproof -\n  { assume 2: \"r\"\n    { assume 3: \"q\"\n      { assume 4: \"p\"\n        have 5: \"q \u27f6 (r \u27f6 s)\" using 1 4 by (rule mp)\n        have 6: \"r \u27f6 s\" using 5 3 by (rule mp)\n        have 7: \"s\" using 6 2 by (rule mp) }\n      hence 8: \"p \u27f6 s\" by (rule impI) }\n    hence 9: \"q \u27f6 (p \u27f6 s)\" by (rule impI) }\n  thus 10: \"r \u27f6 (q \u27f6 (p \u27f6 s))\" by (rule impI) \nqed\n\n-- \"Una variante de la demostraci\u00f3n anterior es\"\nlemma ejercicio_10_1b:\n  assumes 1: \"p \u27f6 (q \u27f6 (r \u27f6 s))\" \n  shows      \"r \u27f6 (q \u27f6 (p \u27f6 s))\"\nproof (rule impI)\n  assume 2: \"r\"\n  show \"q \u27f6 (p \u27f6 s)\"\n  proof (rule impI)\n    assume 3: \"q\"\n    show \"p \u27f6 s\"\n    proof (rule impI)\n      assume 4: \"p\"\n      have 5: \"q \u27f6 (r \u27f6 s)\" using 1 4 by (rule mp)\n      have 6: \"r \u27f6 s\" using 5 3 by (rule mp)\n      show \"s\" using 6 2 by (rule mp)\n    qed\n  qed\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_10_2:\n  assumes \"p \u27f6 (q \u27f6 (r \u27f6 s))\" \n  shows   \"r \u27f6 (q \u27f6 (p \u27f6 s))\"\nproof \n  assume \"r\"\n  show \"q \u27f6 (p \u27f6 s)\"\n  proof \n    assume \"q\"\n    show \"p \u27f6 s\"\n    proof \n      assume \"p\"\n      with assms(1) have \"q \u27f6 (r \u27f6 s)\" ..\n      hence \"r \u27f6 s\" using `q` ..\n      thus \"s\" using `r` ..\n    qed\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_10_3:\n  assumes \"p \u27f6 (q \u27f6 (r \u27f6 s))\" \n  shows   \"r \u27f6 (q \u27f6 (p \u27f6 s))\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 11. Demostrar\n     \u22a2 (p \u27f6 (q \u27f6 r)) \u27f6 ((p \u27f6 q) \u27f6 (p \u27f6 r))\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_11_1:\n  \"(p \u27f6 (q \u27f6 r)) \u27f6 ((p \u27f6 q) \u27f6 (p \u27f6 r))\"\nproof -\n  { assume 1: \"p \u27f6 (q \u27f6 r)\"\n    { assume 2: \"p \u27f6 q\"\n      { assume 3: \"p\"\n        have 4: \"q\" using 2 3 by (rule mp)\n        have 5: \"q \u27f6 r\" using 1 3 by (rule mp)\n        have 6: \"r\" using 5 4 by (rule mp) }\n      hence 7: \"p \u27f6 r\" by (rule impI) }\n    hence 8: \"(p \u27f6 q) \u27f6 (p \u27f6 r)\" by (rule impI) }\n  thus \"(p \u27f6 (q \u27f6 r)) \u27f6 ((p \u27f6 q) \u27f6 (p \u27f6 r))\" by (rule impI)\nqed \n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_11_2:\n  \"(p \u27f6 (q \u27f6 r)) \u27f6 ((p \u27f6 q) \u27f6 (p \u27f6 r))\"\nproof \n  assume \"p \u27f6 (q \u27f6 r)\"\n  { assume \"p \u27f6 q\"\n    { assume \"p\"\n      with `p \u27f6 q` have \"q\" ..\n      have \"q \u27f6 r\" using `p \u27f6 (q \u27f6 r)` `p` ..\n      hence \"r\" using `q` .. }\n    hence \"p \u27f6 r\" .. }\n  thus \"(p \u27f6 q) \u27f6 (p \u27f6 r)\" .. \nqed \n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_11_3:\n  \"(p \u27f6 (q \u27f6 r)) \u27f6 ((p \u27f6 q) \u27f6 (p \u27f6 r))\"\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 12. Demostrar\n     (p \u27f6 q) \u27f6 r \u22a2 p \u27f6 (q \u27f6 r)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_12_1:\n  assumes 1: \"(p \u27f6 q) \u27f6 r\" \n  shows      \"p \u27f6 (q \u27f6 r)\"\nproof -\n  { assume 2: \"p\"\n    { assume 3: \"q\"\n      { assume 4: \"p\"\n        have 5: \"q\" using 3 by this } \n      hence 6: \"p \u27f6 q\" by (rule impI)\n      have 7: \"r\" using 1 6 by (rule mp) } \n    hence 8: \"q \u27f6 r\" by (rule impI) } \n  thus 9: \"p \u27f6 (q \u27f6 r)\" by (rule impI) \nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_12_2:\n  assumes \"(p \u27f6 q) \u27f6 r\" \n  shows   \"p \u27f6 (q \u27f6 r)\"\nproof \n  assume \"p\"\n  { assume \"q\"\n    { assume \"p\"\n      have \"q\" using `q` . } \n    hence \"p \u27f6 q\" ..\n    with assms(1) have \"r\" .. } \n  thus \"q \u27f6 r\" ..\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_12_3:\n  assumes \"(p \u27f6 q) \u27f6 r\" \n  shows   \"p \u27f6 (q \u27f6 r)\"\nusing assms\nby auto\n\nsection {* Conjunciones *}\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 13. Demostrar\n     p, q \u22a2  p \u2227 q\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_13_1:\n  assumes 1: \"p\" and \n          2: \"q\" \n  shows \"p \u2227 q\"\nproof -\n  show \"p \u2227 q\" using assms by (rule conjI)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_13_2:\n  assumes \"p\"\n          \"q\" \n  shows \"p \u2227 q\"\nproof \n  show \"p\" using assms(1) .\nnext\n  show \"q\" using assms(2) .\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_13_3:\n  assumes \"p\"\n          \"q\" \n  shows \"p \u2227 q\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 14. Demostrar\n     p \u2227 q \u22a2 p\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_14_1:\n  assumes 1: \"p \u2227 q\"  \n  shows      \"p\"\nproof -\n  show \"p\" using 1 by (rule conjunct1)\nqed \n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_14_2:\n  assumes \"p \u2227 q\"  \n  shows   \"p\"\nproof -\n  show \"p\" using assms ..\nqed \n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_14_3:\n  assumes \"p \u2227 q\"  \n  shows   \"p\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 15. Demostrar\n     p \u2227 q \u22a2 q\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_15_1:\n  assumes 1: \"p \u2227 q\" \n  shows      \"q\"\nproof -\n  show \"q\" using 1 by (rule conjunct2)\nqed \n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_15_2:\n  assumes \"p \u2227 q\" \n  shows   \"q\"\nproof -\n  show \"q\" using assms ..\nqed \n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_15_3:\n  assumes \"p \u2227 q\" \n  shows   \"q\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 16. Demostrar\n     p \u2227 (q \u2227 r) \u22a2 (p \u2227 q) \u2227 r\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_16_1:\n  assumes 1: \"p \u2227 (q \u2227 r)\"\n  shows      \"(p \u2227 q) \u2227 r\"\nproof -\n  have 2: \"p\" using 1 by (rule conjunct1)\n  have 3: \"q \u2227 r\" using 1 by (rule conjunct2)\n  have 4: \"q\" using 3 by (rule conjunct1)\n  have 5: \"p \u2227 q\" using 2 4 by (rule conjI)\n  have 6: \"r\" using 3 by (rule conjunct2)\n  show 7: \"(p \u2227 q) \u2227 r\" using 5 6 by (rule conjI)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_16_2:\n  assumes \"p \u2227 (q \u2227 r)\"\n  shows   \"(p \u2227 q) \u2227 r\"\nproof \n  show \"p \u2227 q\"\n  proof\n    show \"p\" using assms ..\n  next\n    have \"q \u2227 r\" using assms ..\n    thus \"q\" ..\n  qed\nnext\n    have \"q \u2227 r\" using assms ..\n    thus \"r\" ..\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_16_3:\n  assumes \"p \u2227 (q \u2227 r)\"\n  shows   \"(p \u2227 q) \u2227 r\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 17. Demostrar\n     (p \u2227 q) \u2227 r \u22a2 p \u2227 (q \u2227 r)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_17_1:\n  assumes 1: \"(p \u2227 q) \u2227 r\" \n  shows      \"p \u2227 (q \u2227 r)\"\nproof -\n  have 2: \"p \u2227 q\" using 1 by (rule conjunct1)\n  have 3: \"p\" using 2 by (rule conjunct1)\n  have 4: \"q\" using 2 by (rule conjunct2)\n  have 5: \"r\" using 1 by (rule conjunct2)\n  have 6: \"q \u2227 r\" using 4 5 by (rule conjI)\n  show 7: \"p \u2227 (q \u2227 r)\" using 3 6 by (rule conjI)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_17_2:\n  assumes \"(p \u2227 q) \u2227 r\" \n  shows   \"p \u2227 (q \u2227 r)\"\nproof \n  have \"p \u2227 q\" using assms ..\n  thus \"p\" ..\nnext\n  show \"q \u2227 r\"\n  proof\n    have \"p \u2227 q\" using assms ..\n    thus \"q\" ..\n  next\n    show \"r\" using assms ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_17_3:\n  assumes \"(p \u2227 q) \u2227 r\" \n  shows   \"p \u2227 (q \u2227 r)\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 18. Demostrar\n     p \u2227 q \u22a2 p \u27f6 q\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_18_1:\n  assumes 1: \"p \u2227 q\" \n  shows      \"p \u27f6 q\"\nproof (rule impI)\n  assume 2: \"p\"\n  show \"q\" using 1 by (rule conjunct2)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_18_2:\n  assumes \"p \u2227 q\" \n  shows   \"p \u27f6 q\"\nproof \n  assume \"p\"\n  show \"q\" using assms ..\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_18_3:\n  assumes \"p \u2227 q\" \n  shows   \"p \u27f6 q\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 19. Demostrar\n     (p \u27f6 q) \u2227 (p \u27f6 r) \u22a2 p \u27f6 q \u2227 r   \n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_19_1:\n  assumes 1: \"(p \u27f6 q) \u2227 (p \u27f6 r)\" \n  shows      \"p \u27f6 q \u2227 r\"\nproof (rule impI)\n  assume 2: \"p\"\n  have 3: \"p \u27f6 q\" using 1 by (rule conjunct1)\n  have 4: \"q\" using 3 2 by (rule mp)\n  have 5: \"p \u27f6 r\" using 1 by (rule conjunct2)\n  have 6: \"r\" using 5 2 by (rule mp)\n  show 7: \"q \u2227 r\" using 4 6 by (rule conjI)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_19_2:\n  assumes \"(p \u27f6 q) \u2227 (p \u27f6 r)\" \n  shows   \"p \u27f6 q \u2227 r\"\nproof \n  assume \"p\"\n  show \"q \u2227 r\"\n  proof\n    have \"p \u27f6 q\" using assms ..\n    thus \"q\" using `p` ..\n  next\n    have \"p \u27f6 r\" using assms ..\n    thus \"r\" using `p` ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_19_3:\n  assumes \"(p \u27f6 q) \u2227 (p \u27f6 r)\" \n  shows   \"p \u27f6 q \u2227 r\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 20. Demostrar\n     p \u27f6 q \u2227 r \u22a2 (p \u27f6 q) \u2227 (p \u27f6 r)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_20_1:\n  assumes 1: \"p \u27f6 q \u2227 r\" \n  shows      \"(p \u27f6 q) \u2227 (p \u27f6 r)\"\nproof (rule conjI)\n  show \"p \u27f6 q\" \n  proof (rule impI)\n    assume 2: \"p\"\n    have \"q \u2227 r\" using 1 2 by (rule mp)\n    thus \"q\" by (rule conjunct1)\n  qed\nnext \n  show \"p \u27f6 r\"\n  proof (rule impI)\n    assume 3: \"p\"\n    have \"q \u2227 r\" using 1 3 by (rule mp)\n    thus \"r\" by (rule conjunct2)\n  qed\nqed \n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_20_2:\n  assumes \"p \u27f6 q \u2227 r\" \n  shows   \"(p \u27f6 q) \u2227 (p \u27f6 r)\"\nproof \n  show \"p \u27f6 q\" \n  proof \n    assume \"p\"\n    have \"q \u2227 r\" using assms `p` ..\n    thus \"q\" ..\n  qed\nnext \n  show \"p \u27f6 r\"\n  proof \n    assume \"p\"\n    have \"q \u2227 r\" using assms `p` ..\n    thus \"r\" ..\n  qed\nqed \n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_20_3:\n  assumes \"p \u27f6 q \u2227 r\" \n  shows   \"(p \u27f6 q) \u2227 (p \u27f6 r)\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 21. Demostrar\n     p \u27f6 (q \u27f6 r) \u22a2 p \u2227 q \u27f6 r\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_21_1:\n  assumes 1: \"p \u27f6 (q \u27f6 r)\" \n  shows      \"p \u2227 q \u27f6 r\"\nproof (rule impI)\n  assume 2: \"p \u2227 q\"\n  have 3: \"p\" using 2 by (rule conjunct1)\n  have 4: \"q\" using 2 by (rule conjunct2)\n  have 5: \"q \u27f6 r\" using 1 3 by (rule mp)\n  show 6: \"r\" using 5 4 by (rule mp)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_21_2:\n  assumes \"p \u27f6 (q \u27f6 r)\" \n  shows   \"p \u2227 q \u27f6 r\"\nproof \n  assume \"p \u2227 q\"\n  hence \"p\" ..\n  have \"q\" using `p \u2227 q` ..\n  have \"q \u27f6 r\" using assms(1) `p` ..\n  thus \"r\" using `q` ..\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_21_3:\n  assumes \"p \u27f6 (q \u27f6 r)\" \n  shows   \"p \u2227 q \u27f6 r\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 22. Demostrar\n     p \u2227 q \u27f6 r \u22a2 p \u27f6 (q \u27f6 r)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_22_1:\n  assumes 1: \"p \u2227 q \u27f6 r\" \n  shows      \"p \u27f6 (q \u27f6 r)\"\nproof (rule impI)\n  assume 2: \"p\"\n  { assume 3: \"q\"\n    have 4: \"p \u2227 q\" using 2 3 by (rule conjI)\n    have \"r\" using 1 4 by (rule mp) } \n  thus \"q \u27f6 r\" by (rule impI)  \nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_22_2:\n  assumes \"p \u2227 q \u27f6 r\" \n  shows   \"p \u27f6 (q \u27f6 r)\"\nproof \n  assume \"p\"\n  show \"q \u27f6 r\"\n  proof\n    assume \"q\"\n    with `p` have \"p \u2227 q\" ..\n    with  assms(1) show \"r\" .. \n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_22_3:\n  assumes \"p \u2227 q \u27f6 r\" \n  shows   \"p \u27f6 (q \u27f6 r)\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 23. Demostrar\n     (p \u27f6 q) \u27f6 r \u22a2 p \u2227 q \u27f6 r\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_23_1:\n  assumes 1: \"(p \u27f6 q) \u27f6 r\" \n  shows      \"p \u2227 q \u27f6 r\"\nproof (rule impI)\n  assume 2: \"p \u2227 q\"\n  have 3: \"p \u27f6 q\"\n  proof (rule impI)\n    assume 4: \"p\"\n    show \"q\" using 2 by (rule conjunct2)\n  qed\n  show \"r\" using 1 3 by (rule mp)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_23_2:\n  assumes \"(p \u27f6 q) \u27f6 r\" \n  shows   \"p \u2227 q \u27f6 r\"\nproof \n  assume \"p \u2227 q\"\n  have \"p \u27f6 q\"\n  proof\n    assume \"p\"\n    show \"q\" using `p \u2227 q` ..\n  qed\n  with assms show \"r\" ..\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_23_3:\n  assumes \"(p \u27f6 q) \u27f6 r\" \n  shows   \"p \u2227 q \u27f6 r\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 24. Demostrar\n     p \u2227 (q \u27f6 r) \u22a2 (p \u27f6 q) \u27f6 r\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_24_1:\n  assumes 1: \"p \u2227 (q \u27f6 r)\" \n  shows      \"(p \u27f6 q) \u27f6 r\"\nproof (rule impI)\n  assume 2: \"p \u27f6 q\"\n  have 3: \"p\" using 1 by (rule conjunct1)\n  have 4: \"q\" using 2 3 by (rule mp)\n  have 5: \"q \u27f6 r\" using 1 by (rule conjunct2)\n  thus \"r\" using 4 by (rule mp) \nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_24_2:\n  assumes \"p \u2227 (q \u27f6 r)\" \n  shows   \"(p \u27f6 q) \u27f6 r\"\nproof \n  assume \"p \u27f6 q\"\n  have \"p\" using assms ..\n  with `p \u27f6 q` have \"q\" ..\n  have \"q \u27f6 r\" using assms ..\n  thus \"r\" using `q` ..\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_24_3:\n  assumes \"p \u2227 (q \u27f6 r)\" \n  shows   \"(p \u27f6 q) \u27f6 r\"\nusing assms\nby auto\n\nsection {* Disyunciones *}\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 25. Demostrar\n     p \u22a2 p \u2228 q\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_25_1:\n  assumes 1: \"p\"\n  shows      \"p \u2228 q\"\nproof -\n  show \"p \u2228 q\" using 1 by (rule disjI1)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_25_2:\n  assumes \"p\"\n  shows   \"p \u2228 q\"\nproof -\n  show \"p \u2228 q\" using assms ..\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_25_3:\n  assumes \"p\"\n  shows   \"p \u2228 q\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 26. Demostrar\n     q \u22a2 p \u2228 q\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_26_1:\n  assumes 1: \"q\"\n  shows      \"p \u2228 q\"\nproof -\n  show \"p \u2228 q\" using 1 by (rule disjI2)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_26_2:\n  assumes \"q\"\n  shows   \"p \u2228 q\"\nproof -\n  show \"p \u2228 q\" using assms ..\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_26_3:\n  assumes \"q\"\n  shows   \"p \u2228 q\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 27. Demostrar\n     p \u2228 q \u22a2 q \u2228 p\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_27_1:\n  assumes 1: \"p \u2228 q\"\n  shows      \"q \u2228 p\"\nusing 1\nproof (rule disjE)\n  assume \"p\"\n  thus \"q \u2228 p\" by (rule disjI2)\nnext\n  assume \"q\"\n  thus \"q \u2228 p\" by (rule disjI1)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_27_2:\n  assumes \"p \u2228 q\"\n  shows   \"q \u2228 p\"\nusing assms\nproof \n  assume \"p\"\n  thus \"q \u2228 p\" ..\nnext\n  assume \"q\"\n  thus \"q \u2228 p\" ..\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_27_3:\n  assumes \"p \u2228 q\"\n  shows   \"q \u2228 p\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 28. Demostrar\n     q \u27f6 r \u22a2 p \u2228 q \u27f6 p \u2228 r\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_28_1:\n  assumes 1: \"q \u27f6 r\" \n  shows      \"p \u2228 q \u27f6 p \u2228 r\"\nproof (rule impI)\n  assume \"p \u2228 q\"\n  thus \"p \u2228 r\"\n  proof (rule disjE)\n    assume \"p\"\n    thus \"p \u2228 r\" by (rule disjI1)\n  next\n    assume \"q\"\n    have \"r\" using assms `q` by (rule mp)\n    thus \"p \u2228 r\" by (rule disjI2)\n  qed\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_28_2:\n  assumes \"q \u27f6 r\" \n  shows   \"p \u2228 q \u27f6 p \u2228 r\"\nproof \n  assume \"p \u2228 q\"\n  thus \"p \u2228 r\"\n  proof \n    assume \"p\"\n    thus \"p \u2228 r\" ..\n  next\n    assume \"q\"\n    have \"r\" using assms `q` ..\n    thus \"p \u2228 r\" ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_28_3:\n  assumes \"q \u27f6 r\" \n  shows   \"p \u2228 q \u27f6 p \u2228 r\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 29. Demostrar\n     p \u2228 p \u22a2 p\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_29_1:\n  assumes 1: \"p \u2228 p\"\n  shows      \"p\"\nusing 1\nproof (rule disjE)\n  assume \"p\"\n  thus \"p\" by this\nnext\n  assume \"p\"\n  thus \"p\" by this\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_29_2:\n  assumes \"p \u2228 p\"\n  shows   \"p\"\nusing assms\nproof \n  assume \"p\"\n  thus \"p\" .\nnext\n  assume \"p\"\n  thus \"p\" .\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_29_3:\n  assumes \"p \u2228 p\"\n  shows   \"p\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 30. Demostrar\n     p \u22a2 p \u2228 p\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_30_1:\n  assumes 1: \"p\" \n  shows      \"p \u2228 p\"\nproof -\n  show \"p \u2228 p\" using 1 by (rule disjI1)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_30_2:\n  assumes \"p\" \n  shows   \"p \u2228 p\"\nproof -\n  show \"p \u2228 p\" using assms ..\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_30_3:\n  assumes \"p\" \n  shows   \"p \u2228 p\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 31. Demostrar\n     p \u2228 (q \u2228 r) \u22a2 (p \u2228 q) \u2228 r\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_31_1:\n  assumes 1: \"p \u2228 (q \u2228 r)\" \n  shows      \"(p \u2228 q) \u2228 r\"\nusing 1\nproof (rule disjE)\n  assume \"p\"\n  hence \"p \u2228 q\" by (rule disjI1)\n  thus \"(p \u2228 q) \u2228 r\" by (rule disjI1)\nnext\n  assume \"q \u2228 r\"\n  thus \"(p \u2228 q) \u2228 r\"\n  proof (rule disjE)\n    assume \"q\"\n    hence \"p \u2228 q\" by (rule disjI2)\n    thus \"(p \u2228 q) \u2228 r\" by (rule disjI1)\n  next\n    assume \"r\"\n    thus \"(p \u2228 q) \u2228 r\" by (rule disjI2)\n  qed\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_31_2:\n  assumes \"p \u2228 (q \u2228 r)\" \n  shows   \"(p \u2228 q) \u2228 r\"\nusing assms\nproof \n  assume \"p\"\n  hence \"p \u2228 q\" ..\n  thus \"(p \u2228 q) \u2228 r\" ..\nnext\n  assume \"q \u2228 r\"\n  thus \"(p \u2228 q) \u2228 r\"\n  proof \n    assume \"q\"\n    hence \"p \u2228 q\" ..\n    thus \"(p \u2228 q) \u2228 r\" ..\n  next\n    assume \"r\"\n    thus \"(p \u2228 q) \u2228 r\" ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_31_3:\n  assumes \"p \u2228 (q \u2228 r)\" \n  shows   \"(p \u2228 q) \u2228 r\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 32. Demostrar\n     (p \u2228 q) \u2228 r \u22a2 p \u2228 (q \u2228 r)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_32_1:\n  assumes 1: \"(p \u2228 q) \u2228 r\" \n  shows      \"p \u2228 (q \u2228 r)\"\nusing 1\nproof (rule disjE)\n  assume \"p \u2228 q\"\n  thus \"p \u2228 (q \u2228 r)\"\n  proof (rule disjE)\n    assume \"p\"\n    thus \"p \u2228 (q \u2228 r)\" by (rule disjI1)\n  next\n    assume \"q\"\n    hence \"q \u2228 r\" by (rule disjI1)\n    thus \"p \u2228 (q \u2228 r)\" by (rule disjI2)\n  qed\nnext\n  assume \"r\"\n  hence \"q \u2228 r\" by (rule disjI2)\n  thus \"p \u2228 (q \u2228 r)\" by (rule disjI2)\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_32_2:\n  assumes \"(p \u2228 q) \u2228 r\" \n  shows   \"p \u2228 (q \u2228 r)\"\nusing assms\nproof \n  assume \"p \u2228 q\"\n  thus \"p \u2228 (q \u2228 r)\"\n  proof \n    assume \"p\"\n    thus \"p \u2228 (q \u2228 r)\" ..\n  next\n    assume \"q\"\n    hence \"q \u2228 r\" ..\n    thus \"p \u2228 (q \u2228 r)\" ..\n  qed\nnext\n  assume \"r\"\n  hence \"q \u2228 r\" .. \n  thus \"p \u2228 (q \u2228 r)\" ..\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_32_3:\n  assumes \"(p \u2228 q) \u2228 r\" \n  shows   \"p \u2228 (q \u2228 r)\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 33. Demostrar\n     p \u2227 (q \u2228 r) \u22a2 (p \u2227 q) \u2228 (p \u2227 r)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_33_1:\n  assumes 1: \"p \u2227 (q \u2228 r)\" \n  shows      \"(p \u2227 q) \u2228 (p \u2227 r)\"\nproof -\n  have 2: \"p\" using 1 by (rule conjunct1)\n  have 3: \"q \u2228 r\" using 1 by (rule conjunct2)\n  thus \"(p \u2227 q) \u2228 (p \u2227 r)\"\n  proof (rule disjE)\n    assume 4: \"q\"\n    have \"p \u2227 q\" using 2 4 by (rule conjI)\n    thus \"(p \u2227 q) \u2228 (p \u2227 r)\" by (rule disjI1)\n  next\n    assume 5: \"r\"\n    have \"q \u2228 r\" using 1 by (rule conjunct2)\n    thus \"(p \u2227 q) \u2228 (p \u2227 r)\"\n    proof (rule disjE)\n      assume \"q\"\n      have \"p \u2227 q\" using `p` `q` by (rule conjI) \n      thus \"(p \u2227 q) \u2228 (p \u2227 r)\" by (rule disjI1)\n    next\n      assume \"r\"\n      have \"p \u2227 r\" using `p` `r` by (rule conjI) \n      thus \"(p \u2227 q) \u2228 (p \u2227 r)\" by (rule disjI2)\n    qed\n  qed\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_33_2:\n  assumes \"p \u2227 (q \u2228 r)\" \n  shows   \"(p \u2227 q) \u2228 (p \u2227 r)\"\nproof -\n  have \"p\" using assms ..\n  have \"q \u2228 r\" using assms .. \n  thus \"(p \u2227 q) \u2228 (p \u2227 r)\"\n  proof \n    assume \"q\"\n    with `p` have \"p \u2227 q\" ..\n    thus \"(p \u2227 q) \u2228 (p \u2227 r)\" ..\n  next\n    assume \"r\"\n    hence \"q \u2228 r\" ..\n    thus \"(p \u2227 q) \u2228 (p \u2227 r)\"\n    proof \n      assume \"q\"\n      with `p` have \"p \u2227 q\" ..\n      thus \"(p \u2227 q) \u2228 (p \u2227 r)\" ..\n    next\n      assume \"r\"\n      with `p` have \"p \u2227 r\" ..\n      thus \"(p \u2227 q) \u2228 (p \u2227 r)\" ..\n    qed\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_33_3:\n  assumes \"p \u2227 (q \u2228 r)\" \n  shows   \"(p \u2227 q) \u2228 (p \u2227 r)\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 34. Demostrar\n     (p \u2227 q) \u2228 (p \u2227 r) \u22a2 p \u2227 (q \u2228 r)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_34_1:\n  assumes \"(p \u2227 q) \u2228 (p \u2227 r)\" \n  shows   \"p \u2227 (q \u2228 r)\"\nusing assms\nproof (rule disjE)\n  assume 1: \"p \u2227 q\"\n  show \"p \u2227 (q \u2228 r)\"\n  proof (rule conjI)\n    show \"p\" using 1 by (rule conjunct1)\n  next\n    have \"q\" using 1 by (rule conjunct2)\n    thus \"q \u2228 r\" by (rule disjI1)\n  qed\nnext\n  assume 2: \"p \u2227 r\"\n  hence 3: \"p\" by (rule conjunct1)\n  have \"r\" using 2 by (rule conjunct2)\n  hence 4: \"q \u2228 r\" by (rule disjI2)\n  show \"p \u2227 (q \u2228 r)\" using 3 4 by (rule conjI) \nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_34_2:\n  assumes \"(p \u2227 q) \u2228 (p \u2227 r)\" \n  shows   \"p \u2227 (q \u2228 r)\"\nusing assms\nproof \n  assume \"p \u2227 q\"\n  show \"p \u2227 (q \u2228 r)\"\n  proof \n    show \"p\" using `p \u2227 q` ..\n  next\n    have \"q\" using `p \u2227 q` ..\n    thus \"q \u2228 r\" ..\n  qed\nnext\n  assume \"p \u2227 r\"\n  hence \"p\" ..\n  have \"r\" using `p \u2227 r` ..\n  hence \"q \u2228 r\" .. \n  with `p` show \"p \u2227 (q \u2228 r)\" ..\nqed\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_34_3:\n  assumes \"(p \u2227 q) \u2228 (p \u2227 r)\" \n  shows   \"p \u2227 (q \u2228 r)\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 35. Demostrar\n     p \u2228 (q \u2227 r) \u22a2 (p \u2228 q) \u2227 (p \u2228 r)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_35_1:\n  assumes \"p \u2228 (q \u2227 r)\" \n  shows   \"(p \u2228 q) \u2227 (p \u2228 r)\"\nusing assms\nproof\n  assume \"p\"\n  show \"(p \u2228 q) \u2227 (p \u2228 r)\"\n  proof\n    show \"p \u2228 q\" using `p` ..\n  next\n    show \"p \u2228 r\" using `p` ..\n  qed\nnext\n  assume \"q \u2227 r\"\n  show \"(p \u2228 q) \u2227 (p \u2228 r)\"\n  proof\n    have \"q\" using `q \u2227 r` ..\n    thus \"p \u2228 q\" ..\n  next\n    have \"r\" using `q \u2227 r` ..\n    thus \"p \u2228 r\" ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_35_2:\n  assumes \"p \u2228 (q \u2227 r)\" \n  shows   \"(p \u2228 q) \u2227 (p \u2228 r)\"\nusing assms\nproof (rule disjE)\n  assume \"p\"\n  show \"(p \u2228 q) \u2227 (p \u2228 r)\"\n  proof (rule conjI)\n    show \"p \u2228 q\" using `p` by (rule disjI1)\n  next\n    show \"p \u2228 r\" using `p` by (rule disjI1)\n  qed\nnext\n  assume \"q \u2227 r\"\n  show \"(p \u2228 q) \u2227 (p \u2228 r)\"\n  proof (rule conjI)\n    have \"q\" using `q \u2227 r` ..\n    thus \"p \u2228 q\" by (rule disjI2)\n  next\n    have \"r\" using `q \u2227 r` by (rule conjunct2)\n    thus \"p \u2228 r\" by (rule disjI2)\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_35_3:\n  assumes \"p \u2228 (q \u2227 r)\" \n  shows   \"(p \u2228 q) \u2227 (p \u2228 r)\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 36. Demostrar\n     (p \u2228 q) \u2227 (p \u2228 r) \u22a2 p \u2228 (q \u2227 r)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_36_1:\n  assumes \"(p \u2228 q) \u2227 (p \u2228 r)\"\n  shows   \"p \u2228 (q \u2227 r)\"\nproof -\n  have \"p \u2228 q\" using assms ..\n  thus \"p \u2228 (q \u2227 r)\"\n  proof \n    assume \"p\"\n    thus \"p \u2228 (q \u2227 r)\" ..\n  next\n    assume \"q\"\n    have \"p \u2228 r\" using assms ..\n    thus \"p \u2228 (q \u2227 r)\"\n    proof\n      assume \"p\"\n      thus \"p \u2228 (q \u2227 r)\" ..\n    next\n      assume \"r\"\n      with `q` have \"q \u2227 r\" ..\n      thus \"p \u2228 (q \u2227 r)\" ..\n    qed \n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_36_2:\n  assumes \"(p \u2228 q) \u2227 (p \u2228 r)\"\n  shows   \"p \u2228 (q \u2227 r)\"\nproof -\n  have \"p \u2228 q\" using assms by (rule conjunct1)\n  thus \"p \u2228 (q \u2227 r)\"\n  proof (rule disjE)\n    assume \"p\"\n    thus \"p \u2228 (q \u2227 r)\" by (rule disjI1)\n  next\n    assume \"q\"\n    have \"p \u2228 r\" using assms by (rule conjunct2)\n    thus \"p \u2228 (q \u2227 r)\"\n    proof (rule disjE)\n      assume \"p\"\n      thus \"p \u2228 (q \u2227 r)\" by (rule disjI1)\n    next\n      assume \"r\"\n      have \"q \u2227 r\" using `q` `r` by (rule conjI)\n      thus \"p \u2228 (q \u2227 r)\" by (rule disjI2)\n    qed \n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_36_3:\n  assumes \"(p \u2228 q) \u2227 (p \u2228 r)\"\n  shows   \"p \u2228 (q \u2227 r)\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 37. Demostrar\n     (p \u27f6 r) \u2227 (q \u27f6 r) \u22a2 p \u2228 q \u27f6 r\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_37_1:\n  assumes \"(p \u27f6 r) \u2227 (q \u27f6 r)\" \n  shows   \"p \u2228 q \u27f6 r\"\nproof\n  assume \"p \u2228 q\"\n  thus \"r\"\n  proof \n    assume \"p\"\n    have \"p \u27f6 r\" using assms ..\n    thus \"r\" using `p` ..\n  next\n    assume \"q\"\n    have \"q \u27f6 r\" using assms ..\n    thus \"r\" using `q` ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_37_2:\n  assumes \"(p \u27f6 r) \u2227 (q \u27f6 r)\" \n  shows   \"p \u2228 q \u27f6 r\"\nproof (rule impI)\n  assume \"p \u2228 q\"\n  thus \"r\"\n  proof (rule disjE)\n    assume \"p\"\n    have \"p \u27f6 r\" using assms by (rule conjunct1)\n    thus \"r\" using `p` by (rule mp)\n  next\n    assume \"q\"\n    have \"q \u27f6 r\" using assms by (rule conjunct2)\n    thus \"r\" using `q` by (rule mp)\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_37_3:\n  assumes \"(p \u27f6 r) \u2227 (q \u27f6 r)\" \n  shows   \"p \u2228 q \u27f6 r\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 38. Demostrar\n     p \u2228 q \u27f6 r \u22a2 (p \u27f6 r) \u2227 (q \u27f6 r)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_38_1:\n  assumes \"p \u2228 q \u27f6 r\" \n  shows   \"(p \u27f6 r) \u2227 (q \u27f6 r)\"\nproof\n  show \"p \u27f6 r\"\n  proof\n    assume \"p\"\n    hence \"p \u2228 q\" ..\n    with assms show \"r\" ..\n  qed\nnext\n  show \"q \u27f6 r\"\n  proof\n    assume \"q\"\n    hence \"p \u2228 q\" ..\n    with assms show \"r\" ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_38_2:\n  assumes \"p \u2228 q \u27f6 r\" \n  shows   \"(p \u27f6 r) \u2227 (q \u27f6 r)\"\nproof (rule conjI)\n  show \"p \u27f6 r\"\n  proof (rule impI)\n    assume \"p\"\n    hence \"p \u2228 q\" by (rule disjI1)\n    show \"r\" using assms `p \u2228 q` by (rule mp)\n  qed\nnext\n  show \"q \u27f6 r\"\n  proof (rule impI)\n    assume \"q\"\n    hence \"p \u2228 q\" by (rule disjI2)\n    show \"r\" using assms `p \u2228 q` by (rule mp)\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_38_3:\n  assumes \"p \u2228 q \u27f6 r\" \n  shows   \"(p \u27f6 r) \u2227 (q \u27f6 r)\"\nusing assms\nby auto\n\nsection {* Negaci\u00f3n *}\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 39. Demostrar\n     p \u22a2 \u00ac\u00acp\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_39_1:\n  assumes \"p\"\n  shows   \"\u00ac\u00acp\"\nproof -\n  show \"\u00ac\u00acp\" using assms by (rule notnotI)\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_39_2:\n  assumes \"p\"\n  shows   \"\u00ac\u00acp\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 40. Demostrar\n     \u00acp \u22a2 p \u27f6 q\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_40_1:\n  assumes \"\u00acp\" \n  shows   \"p \u27f6 q\"\nproof\n  assume \"p\"\n  with assms(1) show \"q\" ..\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_40_2:\n  assumes \"\u00acp\" \n  shows   \"p \u27f6 q\"\nproof (rule impI)\n  assume \"p\"\n  show \"q\" using assms(1) `p` by (rule notE)\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_40_3:\n  assumes \"\u00acp\" \n  shows   \"p \u27f6 q\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 41. Demostrar\n     p \u27f6 q \u22a2 \u00acq \u27f6 \u00acp\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_41_1:\n  assumes \"p \u27f6 q\"\n  shows   \"\u00acq \u27f6 \u00acp\"\nproof\n  assume \"\u00acq\"\n  with assms(1) show \"\u00acp\" by (rule mt)\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_41_2:\n  assumes \"p \u27f6 q\"\n  shows   \"\u00acq \u27f6 \u00acp\"\nproof (rule impI)\n  assume \"\u00acq\"\n  show \"\u00acp\" using assms(1) `\u00acq` by (rule mt)\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_41_3:\n  assumes \"p \u27f6 q\"\n  shows   \"\u00acq \u27f6 \u00acp\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 42. Demostrar\n     p \u2228 q, \u00acq \u22a2 p\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_42_1:\n  assumes \"p \u2228 q\"\n          \"\u00acq\" \n  shows   \"p\"\nusing assms(1)\nproof\n  assume \"p\"\n  thus \"p\" .\nnext\n  assume \"q\"\n  with assms(2) show \"p\" ..\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_42_2:\n  assumes \"p \u2228 q\"\n          \"\u00acq\" \n  shows   \"p\"\nusing assms(1)\nproof (rule disjE)\n  assume \"p\"\n  thus \"p\" by this\nnext\n  assume \"q\"\n  show \"p\" using assms(2) `q` by (rule notE)\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_42_3:\n  assumes \"p \u2228 q\"\n          \"\u00acq\" \n  shows   \"p\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 42. Demostrar\n     p \u2228 q, \u00acp \u22a2 q\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_43_1:\n  assumes \"p \u2228 q\"\n          \"\u00acp\" \n  shows   \"q\"\nusing assms(1)\nproof\n  assume \"p\"\n  with assms(2) show \"q\" ..\nnext\n  assume \"q\"\n  thus \"q\" .\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_43_2:\n  assumes \"p \u2228 q\"\n          \"\u00acp\" \n  shows   \"q\"\nusing assms(1)\nproof (rule disjE)\n  assume \"p\"\n  show \"q\" using assms(2) `p` by (rule notE)\nnext\n  assume \"q\"\n  thus \"q\" by this\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_43_3:\n  assumes \"p \u2228 q\"\n          \"\u00acp\" \n  shows   \"q\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 44. Demostrar\n     p \u2228 q \u22a2 \u00ac(\u00acp \u2227 \u00acq)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_44_1:\n  assumes \"p \u2228 q\" \n  shows   \"\u00ac(\u00acp \u2227 \u00acq)\"\nproof\n  assume \"\u00acp \u2227 \u00acq\"\n  note `p \u2228 q`\n  thus \"False\" \n  proof\n    assume \"p\"\n    have \"\u00acp\" using `\u00acp \u2227 \u00acq` .. \n    thus \"False\" using `p` ..\n  next \n    assume \"q\"\n    have \"\u00acq\" using `\u00acp \u2227 \u00acq` .. \n    thus \"False\" using `q` ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_44_2:\n  assumes \"p \u2228 q\" \n  shows   \"\u00ac(\u00acp \u2227 \u00acq)\"\nproof (rule notI)\n  assume \"\u00acp \u2227 \u00acq\"\n  note `p \u2228 q`\n  thus \"False\" \n  proof\n    assume \"p\"\n    have \"\u00acp\" using `\u00acp \u2227 \u00acq` by (rule conjunct1) \n    thus \"False\" using `p` by (rule notE)\n  next \n    assume \"q\"\n    have \"\u00acq\" using `\u00acp \u2227 \u00acq` by (rule conjunct2)\n    thus \"False\" using `q` by (rule notE)\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_44_3:\n  assumes \"p \u2228 q\" \n  shows   \"\u00ac(\u00acp \u2227 \u00acq)\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 45. Demostrar\n     p \u2227 q \u22a2 \u00ac(\u00acp \u2228 \u00acq)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_45_1:\n  assumes \"p \u2227 q\" \n  shows   \"\u00ac(\u00acp \u2228 \u00acq)\"\nproof\n  assume \"\u00acp \u2228 \u00acq\"\n  thus \"False\"\n  proof\n    assume \"\u00acp\"\n    have \"p\" using assms ..\n    with `\u00acp` show \"False\" ..\n  next\n    assume \"\u00acq\"\n    have \"q\" using assms ..\n    with `\u00acq` show \"False\" ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_45_2:\n  assumes \"p \u2227 q\" \n  shows   \"\u00ac(\u00acp \u2228 \u00acq)\"\nproof (rule notI)\n  assume \"\u00acp \u2228 \u00acq\"\n  thus \"False\"\n  proof\n    assume \"\u00acp\"\n    have \"p\" using assms by (rule conjunct1)\n    show \"False\" using `\u00acp` `p` by (rule notE)\n  next\n    assume \"\u00acq\"\n    have \"q\" using assms by (rule conjunct2)\n    show \"False\" using `\u00acq` `q` by (rule notE)\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_45_3:\n  assumes \"p \u2227 q\" \n  shows   \"\u00ac(\u00acp \u2228 \u00acq)\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 46. Demostrar\n     \u00ac(p \u2228 q) \u22a2 \u00acp \u2227 \u00acq\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_46_1:\n  assumes \"\u00ac(p \u2228 q)\" \n  shows   \"\u00acp \u2227 \u00acq\"\nproof \n  show \"\u00acp\"\n  proof\n    assume \"p\"\n    hence \"p \u2228 q\" ..\n    with assms show \"False\" ..\n  qed\nnext\n  show \"\u00acq\"\n  proof\n    assume \"q\"\n    hence \"p \u2228 q\" ..\n    with assms show \"False\" ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_46_2:\n  assumes \"\u00ac(p \u2228 q)\" \n  shows   \"\u00acp \u2227 \u00acq\"\nproof (rule conjI)\n  show \"\u00acp\"\n  proof (rule notI)\n    assume \"p\"\n    hence \"p \u2228 q\" by (rule disjI1)\n    show \"False\" using assms `p \u2228 q` by (rule notE)\n  qed\nnext\n  show \"\u00acq\"\n  proof (rule notI)\n    assume \"q\"\n    hence \"p \u2228 q\" by (rule disjI2)\n    show \"False\" using assms `p \u2228 q` by (rule notE)\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_46_3:\n  assumes \"\u00ac(p \u2228 q)\" \n  shows   \"\u00acp \u2227 \u00acq\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 47. Demostrar\n     \u00acp \u2227 \u00acq \u22a2 \u00ac(p \u2228 q)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_47_1:\n  assumes \"\u00acp \u2227 \u00acq\" \n  shows   \"\u00ac(p \u2228 q)\"\nproof\n  assume \"p \u2228 q\"\n  thus False\n  proof\n    assume \"p\"\n    have \"\u00acp\" using assms ..\n    thus False using `p` ..\n  next\n    assume \"q\"\n    have \"\u00acq\" using assms ..\n    thus False using `q` ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_47_2:\n  assumes \"\u00acp \u2227 \u00acq\" \n  shows   \"\u00ac(p \u2228 q)\"\nproof (rule notI)\n  assume \"p \u2228 q\"\n  thus False\n  proof (rule disjE)\n    assume \"p\"\n    have \"\u00acp\" using assms by (rule conjunct1)\n    thus False using `p` by (rule notE)\n  next\n    assume \"q\"\n    have \"\u00acq\" using assms by (rule conjunct2)\n    thus False using `q` by (rule notE)\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_47_3:\n  assumes \"\u00acp \u2227 \u00acq\" \n  shows   \"\u00ac(p \u2228 q)\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 48. Demostrar\n     \u00acp \u2228 \u00acq \u22a2 \u00ac(p \u2227 q)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_48_1:\n  assumes \"\u00acp \u2228 \u00acq\"\n  shows   \"\u00ac(p \u2227 q)\"\nproof\n  assume \"p \u2227 q\"\n  note `\u00acp \u2228 \u00ac q`\n  thus False\n  proof\n    assume \"\u00acp\"\n    have \"p\" using `p \u2227 q` ..\n    with `\u00acp` show False ..\n  next\n    assume \"\u00acq\"\n    have \"q\" using `p \u2227 q` ..\n    with `\u00acq` show False ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_48_2:\n  assumes \"\u00acp \u2228 \u00acq\"\n  shows   \"\u00ac(p \u2227 q)\"\nproof (rule notI)\n  assume \"p \u2227 q\"\n  note `\u00acp \u2228 \u00ac q`\n  thus False\n  proof (rule disjE)\n    assume \"\u00acp\"\n    have \"p\" using `p \u2227 q` by (rule conjunct1)\n    show False using `\u00acp` `p` by (rule notE)\n  next\n    assume \"\u00acq\"\n    have \"q\" using `p \u2227 q` by (rule conjunct2)\n    show False using `\u00acq` `q` by (rule notE)\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_48_3:\n  assumes \"\u00acp \u2228 \u00acq\"\n  shows   \"\u00ac(p \u2227 q)\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 49. Demostrar\n     \u22a2 \u00ac(p \u2227 \u00acp)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_49_1:\n  \"\u00ac(p \u2227 \u00acp)\"\nproof\n  assume \"p \u2227 \u00acp\"\n  hence \"p\" ..\n  have \"\u00acp\" using `p \u2227 \u00acp` ..\n  thus False using `p` .. \nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_49_2:\n  \"\u00ac(p \u2227 \u00acp)\"\nproof (rule notI)\n  assume \"p \u2227 \u00acp\"\n  hence \"p\" by (rule conjunct1)\n  have \"\u00acp\" using `p \u2227 \u00acp` by (rule conjunct2)\n  thus False using `p` by (rule notE)\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_49_3:\n  \"\u00ac(p \u2227 \u00acp)\"\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 50. Demostrar\n     p \u2227 \u00acp \u22a2 q\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_50_1:\n  assumes \"p \u2227 \u00acp\" \n  shows   \"q\"\nproof -\n  have \"p\" using assms ..\n  have \"\u00acp\" using assms ..\n  thus \"q\" using `p` ..\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_50_2:\n  assumes \"p \u2227 \u00acp\" \n  shows   \"q\"\nproof -\n  have \"p\" using assms by (rule conjunct1)\n  have \"\u00acp\" using assms by (rule conjunct2)\n  thus \"q\" using `p` by (rule notE)\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_50_3:\n  assumes \"p \u2227 \u00acp\" \n  shows   \"q\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 51. Demostrar\n     \u00ac\u00acp \u22a2 p\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_51_1:\n  assumes \"\u00ac\u00acp\"\n  shows   \"p\"\nusing assms\nby (rule notnotD)\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_51_2:\n  assumes \"\u00ac\u00acp\"\n  shows   \"p\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 52. Demostrar\n     \u22a2 p \u2228 \u00acp\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_52_1:\n  \"p \u2228 \u00acp\"\nproof -\n  have \"\u00ac\u00acp \u2228 \u00acp\" ..\n  thus \"p \u2228 \u00acp\" by simp\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_52_2:\n  \"p \u2228 \u00acp\"\nproof -\n  have \"\u00ac\u00acp \u2228 \u00acp\" by (rule excluded_middle)\n  thus \"p \u2228 \u00acp\" by simp\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_52_3:\n  \"p \u2228 \u00acp\"\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 53. Demostrar\n     \u22a2 ((p \u27f6 q) \u27f6 p) \u27f6 p\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_53_1:\n  \"((p \u27f6 q) \u27f6 p) \u27f6 p\"\nproof\n  assume \"(p \u27f6 q) \u27f6 p\"\n  show \"p\"\n  proof (rule ccontr)\n    assume \"\u00acp\"\n    have \"\u00ac(p \u27f6 q)\" using `(p \u27f6 q) \u27f6 p` `\u00acp` by (rule mt)\n    have \"p \u27f6 q\"\n    proof\n      assume \"p\"\n      with `\u00acp` show \"q\" ..\n    qed\n    show False using `\u00ac(p \u27f6 q)` `p \u27f6 q` .. \n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_53_2:\n  \"((p \u27f6 q) \u27f6 p) \u27f6 p\"\nproof (rule impI)\n  assume \"(p \u27f6 q) \u27f6 p\"\n  show \"p\"\n  proof (rule ccontr)\n    assume \"\u00acp\"\n    have \"\u00ac(p \u27f6 q)\" using `(p \u27f6 q) \u27f6 p` `\u00acp` by (rule mt)\n    have \"p \u27f6 q\"\n    proof (rule impI)\n      assume \"p\"\n      show \"q\" using `\u00acp` `p` by (rule notE)\n    qed\n    show False using `\u00ac(p \u27f6 q)` `p \u27f6 q` by (rule notE) \n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_53_3:\n  \"((p \u27f6 q) \u27f6 p) \u27f6 p\"\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 54. Demostrar\n     \u00acq \u27f6 \u00acp \u22a2 p \u27f6 q\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_54_1:\n  assumes \"\u00acq \u27f6 \u00acp\"\n  shows   \"p \u27f6 q\"\nproof\n  assume \"p\"\n  show \"q\"\n  proof (rule ccontr)\n    assume \"\u00acq\"\n    with assms have \"\u00acp\" ..\n    thus False using `p` ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_54_2:\n  assumes \"\u00acq \u27f6 \u00acp\"\n  shows   \"p \u27f6 q\"\nproof (rule impI)\n  assume \"p\"\n  show \"q\"\n  proof (rule ccontr)\n    assume \"\u00acq\"\n    have \"\u00acp\" using assms `\u00acq` by (rule mp)\n    thus False using `p` by (rule notE)\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_54_3:\n  assumes \"\u00acq \u27f6 \u00acp\"\n  shows   \"p \u27f6 q\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 55. Demostrar\n     \u00ac(\u00acp \u2227 \u00acq) \u22a2 p \u2228 q\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_55_1:\n  assumes \"\u00ac(\u00acp \u2227 \u00acq)\"\n  shows   \"p \u2228 q\"\nproof -\n  have \"\u00acp \u2228 p\" ..\n  thus \"p \u2228 q\"\n  proof\n    assume \"\u00acp\"\n    have \"\u00acq \u2228 q\" ..\n    thus \"p \u2228 q\"\n    proof\n      assume \"\u00acq\"\n      with `\u00acp` have \"\u00acp \u2227 \u00acq\" ..\n      with assms show \"p \u2228 q\" ..\n    next\n      assume \"q\"\n      thus \"p \u2228 q\" ..\n    qed\n  next\n    assume \"p\"\n    thus \"p \u2228 q\" ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_55_2:\n  assumes \"\u00ac(\u00acp \u2227 \u00acq)\"\n  shows   \"p \u2228 q\"\nproof -\n  have \"\u00acp \u2228 p\" by (rule excluded_middle)\n  thus \"p \u2228 q\"\n  proof\n    assume \"\u00acp\"\n    have \"\u00acq \u2228 q\" by (rule excluded_middle)\n    thus \"p \u2228 q\"\n    proof\n      assume \"\u00acq\"\n      have \"\u00acp \u2227 \u00acq\" using `\u00acp` `\u00acq` by (rule conjI)\n      show \"p \u2228 q\" using assms `\u00acp \u2227 \u00acq` by (rule notE)\n    next\n      assume \"q\"\n      thus \"p \u2228 q\" by (rule disjI2)\n    qed\n  next\n    assume \"p\"\n    thus \"p \u2228 q\" by (rule disjI1)\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_55_3:\n  assumes \"\u00ac(\u00acp \u2227 \u00acq)\"\n  shows   \"p \u2228 q\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 56. Demostrar\n     \u00ac(\u00acp \u2228 \u00acq) \u22a2 p \u2227 q\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_56_1:\n  assumes \"\u00ac(\u00acp \u2228 \u00acq)\" \n  shows   \"p \u2227 q\"\nproof\n  show \"p\"\n  proof (rule ccontr)\n    assume \"\u00acp\"\n    hence \"\u00acp \u2228 \u00acq\" ..\n    with assms show False ..\n  qed\nnext\n  show \"q\"\n  proof (rule ccontr)\n    assume \"\u00acq\"\n    hence \"\u00acp \u2228 \u00acq\" ..\n    with assms show False ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_56_2:\n  assumes \"\u00ac(\u00acp \u2228 \u00acq)\" \n  shows   \"p \u2227 q\"\nproof (rule conjI)\n  show \"p\"\n  proof (rule ccontr)\n    assume \"\u00acp\"\n    hence \"\u00acp \u2228 \u00acq\" by (rule disjI1)\n    show False using assms `\u00acp \u2228 \u00acq` by (rule notE)\n  qed\nnext\n  show \"q\"\n  proof (rule ccontr)\n    assume \"\u00acq\"\n    hence \"\u00acp \u2228 \u00acq\" by (rule disjI2)\n    show False using assms `\u00acp \u2228 \u00acq` by (rule notE)\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_56_3:\n  assumes \"\u00ac(\u00acp \u2228 \u00acq)\" \n  shows   \"p \u2227 q\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 57. Demostrar\n     \u00ac(p \u2227 q) \u22a2 \u00acp \u2228 \u00acq\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_57_1:\n  assumes \"\u00ac(p \u2227 q)\"\n  shows   \"\u00acp \u2228 \u00acq\"\nproof -\n  have \"\u00acp \u2228 p\" ..\n  thus \"\u00acp \u2228 \u00acq\"\n  proof\n    assume \"\u00acp\"\n    thus \"\u00acp \u2228 \u00acq\" ..\n  next\n    assume \"p\"\n    have \"\u00acq \u2228 q\" ..\n    thus \"\u00acp \u2228 \u00acq\" \n    proof\n      assume \"\u00acq\"\n      thus \"\u00acp \u2228 \u00acq\" ..\n    next\n      assume \"q\"\n      with `p` have \"p \u2227 q\" ..\n      with assms show \"\u00acp \u2228 \u00acq\" ..\n    qed\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_57_2:\n  assumes \"\u00ac(p \u2227 q)\"\n  shows   \"\u00acp \u2228 \u00acq\"\nproof -\n  have \"\u00acp \u2228 p\" by (rule excluded_middle)\n  thus \"\u00acp \u2228 \u00acq\"\n  proof (rule disjE)\n    assume \"\u00acp\"\n    thus \"\u00acp \u2228 \u00acq\" by (rule disjI1)\n  next\n    assume \"p\"\n    have \"\u00acq \u2228 q\" by (rule excluded_middle)\n    thus \"\u00acp \u2228 \u00acq\" \n    proof\n      assume \"\u00acq\"\n      thus \"\u00acp \u2228 \u00acq\" by (rule disjI2)\n    next\n      assume \"q\"\n      have \"p \u2227 q\" using `p` `q` by (rule conjI)\n      show \"\u00acp \u2228 \u00acq\" using assms `p \u2227 q` by (rule notE) \n    qed\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_57_3:\n  assumes \"\u00ac(p \u2227 q)\"\n  shows   \"\u00acp \u2228 \u00acq\"\nusing assms\nby auto\n\ntext {* --------------------------------------------------------------- \n  Ejercicio 58. Demostrar\n     \u22a2 (p \u27f6 q) \u2228 (q \u27f6 p)\n  ------------------------------------------------------------------ *}\n\n-- \"La demostraci\u00f3n estructurada es\"\nlemma ejercicio_58_1:\n  \"(p \u27f6 q) \u2228 (q \u27f6 p)\"\nproof -\n  have \"\u00acp \u2228 p\" ..\n  thus \"(p \u27f6 q) \u2228 (q \u27f6 p)\"\n  proof\n    assume \"\u00acp\"\n    have \"p \u27f6 q\"\n    proof\n      assume \"p\"\n      with `\u00acp` show \"q\" ..\n    qed\n    thus \"(p \u27f6 q) \u2228 (q \u27f6 p)\" ..\n  next\n    assume \"p\"\n    have \"q \u27f6 p\"\n    proof\n      assume \"q\"\n      show \"p\" using `p` .\n    qed\n    thus \"(p \u27f6 q) \u2228 (q \u27f6 p)\" ..\n  qed\nqed\n\n-- \"La demostraci\u00f3n detallada es\"\nlemma ejercicio_58_2:\n  \"(p \u27f6 q) \u2228 (q \u27f6 p)\"\nproof -\n  have \"\u00acp \u2228 p\" by (rule excluded_middle)\n  thus \"(p \u27f6 q) \u2228 (q \u27f6 p)\"\n  proof\n    assume \"\u00acp\"\n    have \"p \u27f6 q\"\n    proof (rule impI)\n      assume \"p\"\n      show \"q\" using `\u00acp` `p` by (rule notE)\n    qed\n    thus \"(p \u27f6 q) \u2228 (q \u27f6 p)\" by (rule disjI1)\n  next\n    assume \"p\"\n    have \"q \u27f6 p\"\n    proof\n      assume \"q\"\n      show \"p\" using `p` by this\n    qed\n    thus \"(p \u27f6 q) \u2228 (q \u27f6 p)\" by (rule disjI2)\n  qed\nqed\n\n-- \"La demostraci\u00f3n autom\u00e1tica es\"\nlemma ejercicio_58_3:\n  \"(p \u27f6 q) \u2228 (q \u27f6 p)\"\nby auto\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>En la clase de hoy del curso L\u00f3gica matem\u00e1tica y fundamentos se han comentado soluciones de los ejercicios de deducci\u00f3n natural en l\u00f3gica proposicional con Isabelle\/HOL. Para cada uno de los ejercicios se ha presentado distintas demostraciones: desde la detallada (que sea parecida a la mostrada en las transparencias) hasta la autom\u00e1tica. La teor\u00eda con&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[243],"tags":[144,308,189],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4833"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=4833"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4833\/revisions"}],"predecessor-version":[{"id":4840,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4833\/revisions\/4840"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4833"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4833"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4833"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}