Diferencia entre revisiones de «Relación 7»

Revisión del 15:12 28 feb 2019

chapter {* R6: Deducción natural proposicional *}

theory R6_Deduccion_natural_proposicional_alu
imports Main 
begin
 
text {*
  --------------------------------------------------------------------- 
  El objetivo de esta relación es demostrar cada uno de los ejercicios
  usando sólo las reglas básicas de deducción natural de la lógica
  proposicional (sin usar el método auto).

  Las reglas básicas de la deducción natural son las siguientes:
  · conjI:      ⟦P; Q⟧ ⟹ P ∧ Q
  · conjunct1:  P ∧ Q ⟹ P
  · conjunct2:  P ∧ Q ⟹ Q  
  · notnotD:    ¬¬ P ⟹ P
  · notnotI:    P ⟹ ¬¬ P
  · mp:         ⟦P ⟶ Q; P⟧ ⟹ Q 
  · mt:         ⟦F ⟶ G; ¬G⟧ ⟹ ¬F 
  · impI:       (P ⟹ Q) ⟹ P ⟶ Q
  · disjI1:     P ⟹ P ∨ Q
  · disjI2:     Q ⟹ P ∨ Q
  · disjE:      ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R 
  · FalseE:     False ⟹ P
  · notE:       ⟦¬P; P⟧ ⟹ R
  · notI:       (P ⟹ False) ⟹ ¬P
  · iffI:       ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
  · iffD1:      ⟦Q = P; Q⟧ ⟹ P 
  · iffD2:      ⟦P = Q; Q⟧ ⟹ P
  · ccontr:     (¬P ⟹ False) ⟹ P
  --------------------------------------------------------------------- 
*}

text {*
  Se usarán las reglas notnotI y mt que demostramos a continuación. *}

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

section {* Implicaciones *}

text {* --------------------------------------------------------------- 
  Ejercicio 1. Demostrar
       p ⟶ q, p ⊢ q
  ------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 cammonagu raffergon2 chrgencar
   gleherlop giafus1 marfruman1 enrparalv pabbergue antramhur alikan
   juacanrod hugrubsan *) 
lemma ejercicio_1:
  assumes 1: "p ⟶ q" and
          2: "p"
  shows "q"
proof -
  show "q" using 1 2 by (rule mp)
qed

(* benber alfmarcua *)
lemma ejercicio_1_1:
  assumes "p ⟶ q"
          "p"
  shows "q"
  using assms by (rule mp)


text {* --------------------------------------------------------------- 
  Ejercicio 2. Demostrar
     p ⟶ q, q ⟶ r, p ⊢ r
  ------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 cammonagu gleherlop raffergon2
   chrgencar giafus1 marfruman1 alfmarcua enrparalv pabbergue antramhur
   alikan juacanrod hugrubsan *) 
lemma ejercicio_2:
  assumes 1: "p ⟶ q" and
          2: "q ⟶ r" and
          3: "p"
  shows "r"
proof -
  have 4: "q" using 1 3 by (rule mp)
  show "r" using 2 4 by (rule mp)
qed

(* benber *)
lemma ejercicio_2_1:
  assumes "p ⟶ q"
          "q ⟶ r"
          "p" 
  shows "r"
proof -
  have "q" using `p ⟶ q` `p` by (rule mp)
  with `q ⟶ r` show "r" by (rule mp)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 3. Demostrar
     p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
  ------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 cammonagu gleherlop raffergon2
   chrgencar giafus1 marfruman1 alfmarcua enrparalv pabbergue antramhur
   alikan juacanrod hugrubsan *) 
lemma ejercicio_3:
  assumes 1: "p ⟶ (q ⟶ r)" and
          2: "p ⟶ q" and
          3: "p"
  shows "r"
proof -
  have 4: "q ⟶ r" using 1 3 by (rule mp)
  have 5: "q" using 2 3 by (rule mp)
  show "r" using 4 5 by (rule mp)
qed

(* benber *)
lemma ejercicio_3_1:
  assumes "p ⟶ (q ⟶ r)"
          "p ⟶ q"
          "p"
  shows "r"
proof -
  have "q ⟶ r" using `p ⟶ (q ⟶ r)` `p` by (rule mp)
  moreover have "q" using `p ⟶ q` `p` by (rule mp)
  ultimately show "r" by (rule mp)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 4. Demostrar
     p ⟶ q, q ⟶ r ⊢ p ⟶ r
  ------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 cammonagu chrgencar raffergon2
   gleherlop giafus1 marfruman1 alfmarcua enrparalv pabbergue antramhur
   alikan juacanrod hugrubsan *) 
lemma ejercicio_4:
  assumes 1: "p ⟶ q" and
          2: "q ⟶ r" 
  shows "p ⟶ r"
proof -
  { assume 3: "p"
    have 4: "q" using 1 3 by (rule mp) 
    have 5: "r" using 2 4 by (rule mp)}
  thus "p ⟶ r" by (rule impI)
qed

(* benber *)
lemma ejercicio_4_1:
  assumes "p ⟶ q"
          "q ⟶ r" 
  shows "p ⟶ r"
proof
  assume p
  with `p ⟶ q` have "q" by (rule mp)
  with `q ⟶ r` show "r" by (rule mp)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 5. Demostrar
     p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
  ------------------------------------------------------------------ *}

(* pabalagon manperjim raffergon2 giafus1 gleherlop marfruman1 alfmarcua
   enrparalv chrgencar pabbergue antramhur alikan hugrubsan *) 
lemma ejercicio_5:
  assumes 1: "p ⟶ (q ⟶ r)" 
  shows   "q ⟶ (p ⟶ r)"
proof (rule impI)
  assume 2: "q"
  show "p ⟶ r"
  proof (rule impI)
    assume 3: "p"
    have 4: "q ⟶ r" using 1 3 by (rule mp)
    show "r" using 4 2 by (rule mp)
  qed
qed

(* benber josgomrom4 juacanrod cammonagu  *)
lemma ejercicio_5_1:
  assumes "p ⟶ (q ⟶ r)" 
  shows   "q ⟶ (p ⟶ r)"
proof
  assume "q"
  show "p ⟶ r"
  proof
    assume "p"
    with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
    thus "r" using `q` by (rule mp)
  qed
qed

(* pabalagon *)
lemma ejercicio_5_2:
  assumes 1: "p ⟶ (q ⟶ r)" 
  shows   "q ⟶ (p ⟶ r)"
proof -
  { assume 2: "q"
    { assume 3: "p"
      have 4: "q ⟶ r" using 1 3 by (rule mp)
      have 5: "r" using 4 2 by (rule mp)}
    hence "p ⟶ r" by (rule impI)
  }
  thus "q ⟶ (p ⟶ r)" by (rule impI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 6. Demostrar
     p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
  ------------------------------------------------------------------ *}

(* pabalagon manperjim cammonagu chrgencar raffergon2 gleherlop giafus1 
   marfruman1 alfmarcua enrparalv pabbergue  antramhur alikan juacanrod
   hugrubsan *) 
lemma ejercicio_6:
  assumes 1: "p ⟶ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ (p ⟶ r)"
proof (rule impI)
  assume 2: "p ⟶ q"
  show "p ⟶ r"
  proof (rule impI)
    assume 3: "p"
    have 4: "q ⟶ r" using 1 3 by (rule mp)
    have 5: "q" using 2 3 by (rule mp)
    show "r" using 4 5 by (rule mp)
  qed
qed

(* benber josgomrom4 *)
lemma ejercicio_6_1:
  assumes "p ⟶ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ (p ⟶ r)"
proof
  assume "p ⟶ q"
  show "p ⟶ r"
  proof
    assume "p"
    with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
    moreover from `p ⟶ q` `p` have "q" by (rule mp)
    ultimately show "r" by (rule mp)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 7. Demostrar
     p ⊢ q ⟶ p
  ------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 giafus1 gleherlop
   marfruman1 enrparalv pabbergue antramhur alikan hugrubsan *) 
lemma ejercicio_7:
  assumes 1: "p"  
  shows   "q ⟶ p"
proof (rule impI)
  assume 2: "q"
  show "p" using 1 by this
qed

(* benber cammonagu juacanrod chrgencar *)
lemma ejercicio_7_1:
  assumes "p"  
  shows   "q ⟶ p"
proof
  show "p" using `p` .
qed

(* alfmarcua *)
lemma ejercicio_7_2:
  assumes "p"  
  shows   "q ⟶ p"
  using assms by (rule impI)

text {* --------------------------------------------------------------- 
  Ejercicio 8. Demostrar
     ⊢ p ⟶ (q ⟶ p)
  ------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 giafus1 marfruman1
   enrparalv pabbergue antramhur alikan hugrubsan *) 
lemma ejercicio_8:
  "p ⟶ (q ⟶ p)"
proof (rule impI)
  assume 1: "p"
  show "q ⟶ p"
  proof (rule impI)
    assume 2: "q"
    show "p" using 1 by this
  qed
qed

(* benber cammonagu gleherlop chrgencar juacanrod alfmarcua *)
lemma ejercicio_8_1:
  "p ⟶ (q ⟶ p)"
  using ejercicio_7_1 by (rule impI)

text {* --------------------------------------------------------------- 
  Ejercicio 9. Demostrar
     p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
  ------------------------------------------------------------------ *}

(* pabalagon manperjim raffergon2 giafus1 marfruman1 alfmarcua enrparalv
   gleherlop antramhur alikan hugrubsan *) 
lemma ejercicio_9:
  assumes 1: "p ⟶ q" 
  shows   "(q ⟶ r) ⟶ (p ⟶ r)"
proof (rule impI)
  assume 2: "q ⟶ r"
  show "p ⟶ r"
  proof (rule impI)
    assume 3: "p"
    have 4: "q" using 1 3 by (rule mp)
    show "r" using 2 4 by (rule mp)
  qed
qed

(* benber josgomrom4 cammonagu chrgencar juacanrod pabbergue *)
lemma ejercicio_9_1:
  assumes "p ⟶ q" 
  shows   "(q ⟶ r) ⟶ (p ⟶ r)"
proof
  assume "q ⟶ r"
  show "p ⟶ r"
  proof
    assume "p"
    with `p ⟶ q` have "q" by (rule mp)
    with `q ⟶ r` show "r" by (rule mp)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 10. Demostrar
     p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
  ------------------------------------------------------------------ *}

(* pabalagon manperjim raffergon2 marfruman1 gleherlop alfmarcua
   enrparalv pabbergue antramhur alikan juacanrod hugrubsan *) 
lemma ejercicio_10:
  assumes 1: "p ⟶ (q ⟶ (r ⟶ s))" 
  shows   "r ⟶ (q ⟶ (p ⟶ s))"
proof (rule impI)
  assume 2: "r"
  show "q ⟶ (p ⟶ s)"
  proof (rule impI)
    assume 3: "q"
    show "p ⟶ s"
    proof (rule impI)
      assume 4: "p"
      have 5: "q ⟶ (r ⟶ s)" using 1 4 by (rule mp)
      have 6: "r ⟶ s" using 5 3 by (rule mp)
      show "s" using 6 2 by (rule mp)
    qed
  qed
qed

(* benber josgomrom4 cammonagu chrgencar giafus1 *)
lemma ejercicio_10_1:
  assumes "p ⟶ (q ⟶ (r ⟶ s))" 
  shows   "r ⟶ (q ⟶ (p ⟶ s))"
proof
  assume "r"
  show "q ⟶ (p ⟶ s)"
  proof
    assume "q"
    show "p ⟶ s"
    proof
      assume "p"
      with `p ⟶ (q ⟶ (r ⟶ s))`
        have "q ⟶ (r ⟶ s)" by (rule mp)
      hence "r ⟶ s" using `q` by (rule mp)
      thus "s" using `r` by (rule mp)
    qed
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 11. Demostrar
     ⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
  ------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 gleherlop cammonagu giafus1 alfmarcua
   chrgencar pabbergue alikan juacanrod hugrubsan *) 
lemma ejercicio_11:
  "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof (rule impI)
  assume 1: "p ⟶ (q ⟶ r)"
  show "(p ⟶ q) ⟶ (p ⟶ r)" using 1 ejercicio_6 by simp
qed

(* pabalagon raffergon2 marfruman1 enrparalv antramhur *)
lemma ejercicio_11_2:
  "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof (rule impI)
  assume 1: "p ⟶ (q ⟶ r)"
  show "(p ⟶ q) ⟶ (p ⟶ r)"
  proof (rule impI)
    assume 2: "p ⟶ q"
    show "p ⟶ r"
    proof (rule impI)
      assume 3: "p"
      have 4: "q ⟶ r" using 1 3 by (rule mp)
      have 5: "q" using 2 3 by (rule mp)
      show "r" using 4 5 by (rule mp)
    qed
  qed
qed

(* benber *)
lemma ejercicio_11_1:
  "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof
  assume "p ⟶ (q ⟶ r)"
  show "(p ⟶ q) ⟶ (p ⟶ r)"
  proof
    assume "p ⟶ q"
    show "p ⟶ r"
    proof
      assume p
      with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
      moreover have "q" using `p ⟶ q` `p` by (rule mp)
      ultimately show r by (rule mp)
    qed
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 12. Demostrar
     (p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
  ------------------------------------------------------------------ *}

(* pabalagon manperjim raffergon2 marfruman1 gleherlop enrparalv
   pabbergue antramhur alikan juacanrod hugrubsan *) 
lemma ejercicio_12:
  assumes 1: "(p ⟶ q) ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
proof (rule impI)
  assume 2: "p"
  show "q ⟶ r"
  proof (rule impI)
    assume 3: "q"
    have 4: "p ⟶ q"
    proof (rule impI)
      assume 5: "p"
      show "q" using 3 by this
    qed
    show "r" using 1 4 by (rule mp)
  qed
qed

(* benber  josgomrom4 cammonagu giafus1 alfmarcua chrgencar *)
lemma ejercicio_12_1:
  assumes "(p ⟶ q) ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
proof
  assume "p"
  show "q ⟶ r"
  proof
    assume "q"
    hence "p ⟶ q" by (rule impI)
    with `(p ⟶ q) ⟶ r` show "r" by (rule mp)
  qed
qed

section {* Conjunciones *}

text {* --------------------------------------------------------------- 
  Ejercicio 13. Demostrar
     p, q ⊢  p ∧ q
  ------------------------------------------------------------------ *}

(* pabalagon *)
lemma ejercicio_13:
  assumes "p"
          "q" 
  shows "p ∧ q"
using assms(1, 2) by (rule conjI)

(* benber manperjim josgomrom4 cammonagu raffergon2 marfruman1 alfmarcua
   enrparalv chrgencar gleherlop pabbergue antramhur juacanrod hugrubsan  
   alikan *)
lemma ejercicio_13_1:
  assumes "p"
          "q" 
  shows "p ∧ q"
  using assms by (rule conjI)

text {* --------------------------------------------------------------- 
  Ejercicio 14. Demostrar
     p ∧ q ⊢ p
  ------------------------------------------------------------------ *}

(* pabalagon  josgomrom4 *)
lemma ejercicio_14:
  assumes "p ∧ q"  
  shows   "p"
  using assms(1) by (rule conjunct1)

(* benber manperjim cammonagu raffergon2 marfruman1 alfmarcua enrparalv
   chrgencar pabbergue gleherlop antramhur hugrubsan juacanrod alikan *) 
lemma ejercicio_14_1:
  assumes "p ∧ q"  
  shows   "p"
  using assms by (rule conjunct1)

text {* --------------------------------------------------------------- 
  Ejercicio 15. Demostrar
     p ∧ q ⊢ q
  ------------------------------------------------------------------ *}

(* pabalagon manperjim juacanrod josgomrom4 *)
lemma ejercicio_15:
  assumes "p ∧ q" 
  shows   "q"
  using assms(1) by (rule conjunct2)

(* benber cammonagu raffergon2 marfruman1 alfmarcua enrparalv chrgencar
   pabbergue antramhur gleherlop hugrubsan alikan *) 
lemma ejercicio_15_1:
  assumes "p ∧ q" 
  shows   "q"
  using assms by (rule conjunct2)

text {* --------------------------------------------------------------- 
  Ejercicio 16. Demostrar
     p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
  ------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
   cammmonagu enrparalv chrgencar gleherlop pabbergue antramhur
   hugrubsan alikan juacanrod cammonagu *)  
lemma ejercicio_16:
  assumes "p ∧ (q ∧ r)"
  shows   "(p ∧ q) ∧ r"
proof -
  have 1: "p" using assms(1) by (rule conjunct1)
  have 2: "q ∧ r" using assms(1) by (rule conjunct2)
  have 3: "q" using 2 by (rule conjunct1)
  have 4: "r" using 2 by (rule conjunct2)
  have 5: "p ∧ q" using 1 3 by (rule conjI)
  show "(p ∧ q) ∧ r" using 5 4 by (rule conjI)
qed

(* benber *)
lemma ejercicio_16_1:
  assumes "p ∧ (q ∧ r)"
  shows   "(p ∧ q) ∧ r"
proof - (* TODO? *)
  have "q ∧ r" using assms by (rule conjunct2)
  have "p" using assms by (rule conjunct1)
  moreover have "q" using `q ∧ r` by (rule conjunct1)
  ultimately have "p ∧ q" by (rule conjI)
  moreover have "r" using `q ∧ r` by (rule conjunct2)
  ultimately show "(p ∧ q) ∧ r" by (rule conjI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 17. Demostrar
     (p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
  ------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
   cammonagu chrgencar gleherlop pabbergue antramhur enrparalv hugrubsan
   juacanrod alikan *)  
lemma ejercicio_17:
  assumes 1: "(p ∧ q) ∧ r" 
  shows   "p ∧ (q ∧ r)"
proof -
  have 2: "r" using 1 by (rule conjunct2)
  have 3: "p ∧ q" using 1 by (rule conjunct1)
  have 4: "p" using 3 by (rule conjunct1)
  have 5: "q" using 3 by (rule conjunct2)
  have 6: "q ∧ r" using 5 2 by (rule conjI)
  show ?thesis using 4 6 by (rule conjI)
qed

(* benber *)
lemma ejercicio_17_1:
  assumes "(p ∧ q) ∧ r" 
  shows   "p ∧ (q ∧ r)"
proof -
  have "p ∧ q" using assms by (rule conjunct1)
  have "p" using `p ∧ q` by (rule conjunct1)
  moreover have "q ∧ r"
  proof (rule conjI)
    show "q" using `p ∧ q` by (rule conjunct2)
  next
    show "r" using assms by (rule conjunct2)
  qed
  ultimately show ?thesis by (rule conjI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 18. Demostrar
     p ∧ q ⊢ p ⟶ q
  ------------------------------------------------------------------ *}

(* pabalagon raffergon2 marfruman1 juacanrod alikan*)
lemma ejercicio_18:
  assumes "p ∧ q" 
  shows   "p ⟶ q"
proof (rule impI)
  assume "p"
  show "q" using assms(1) by (rule conjunct2)
qed

(* benber manperjim josgomrom4 cammonagu alfmarcua chrgencar pabbergue
   gleherlop antramhur enrparalv hugrubsan *) 
lemma ejercicio_18_1:
  assumes "p ∧ q" 
  shows   "p ⟶ q"
proof
  show "q" using assms by (rule conjunct2)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 19. Demostrar
     (p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r   
  ------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
   cammonagu chrgencar gleherlop pabbergue antramhur enrparalv juacanrod
   hugrubsan alikan *)  
lemma ejercicio_19:
  assumes 1: "(p ⟶ q) ∧ (p ⟶ r)" 
  shows   "p ⟶ q ∧ r"
proof (rule impI)
  assume 2: "p"
  have 3: "p ⟶ q" using 1 by (rule conjunct1)
  have 4: "p ⟶ r" using 1 by (rule conjunct2)
  have 5: "q" using 3 2 by (rule mp)
  have 6: "r" using 4 2 by (rule mp)
  show "q ∧ r" using 5 6 by (rule conjI)
qed

(* benber cammonagu *)
lemma ejercicio_19_1:
  assumes "(p ⟶ q) ∧ (p ⟶ r)" 
  shows   "p ⟶ q ∧ r"
proof
  assume p
  show "q ∧ r"
  proof
    have "p ⟶ q" using assms by (rule conjunct1)
    thus "q" using `p` by (rule mp)
  next
    have "p ⟶ r" using assms by (rule conjunct2)
    thus "r" using `p` by (rule mp)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 20. Demostrar
     p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
  ------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
   cammonagu chrgencar gleherlop pabbergue antramhur enrparalv juacanrod
   hugrubsan alikan *)  
lemma ejercicio_20:
  assumes 1: "p ⟶ q ∧ r" 
  shows   "(p ⟶ q) ∧ (p ⟶ r)"
proof (rule conjI)
  show "p ⟶ q"
  proof (rule impI)
    assume 2: "p"
    have 3: "q ∧ r" using 1 2 by (rule mp)
    show 4: "q" using 3 by (rule conjunct1)
  qed
  show "p ⟶ r"
  proof (rule impI)
    assume 2: "p"
    have 3: "q ∧ r" using 1 2 by (rule mp)
    show 4: "r" using 3 by (rule conjunct2)
  qed
qed

(* benber *)
lemma ejercicio_20_1:
  assumes "p ⟶ q ∧ r" 
  shows   "(p ⟶ q) ∧ (p ⟶ r)"
proof
  show "p ⟶ q"
  proof
    assume "p"
    with assms have "q ∧ r" by (rule mp)
    thus "q" by (rule conjunct1)
  qed
next
  show "p ⟶ r"
  proof
    assume "p"
    with assms have "q ∧ r" by (rule mp)
    thus "r" by (rule conjunct2)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 21. Demostrar
     p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r
  ------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
   cammonagu chrgencar pabbergue gleherlop antramhur enrparalv juacanrod
   hugrubsan alikan *)  
lemma ejercicio_21:
  assumes 1: "p ⟶ (q ⟶ r)" 
  shows   "p ∧ q ⟶ r"
proof (rule impI)
  assume 2: "p ∧ q"
  have 3: "p" using 2 by (rule conjunct1)
  have 4: "q ⟶ r" using 1 3 by (rule mp)
  have 5: "q" using 2 by (rule conjunct2)
  show "r" using 4 5 by (rule mp)
qed

(* benber *)
lemma ejercicio_21_1:
  assumes "p ⟶ (q ⟶ r)" 
  shows   "p ∧ q ⟶ r"
proof
  assume "p ∧ q"
  hence "p" by (rule conjunct1)
  with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
  moreover from `p ∧ q` have "q" by (rule conjunct2)
  ultimately show "r" by (rule mp)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 22. Demostrar
     p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)
  ------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
   chrgencar pabbergue gleherlop antramhur enrparalv juacanrod hugrubsan
   alikan *)  
lemma ejercicio_22:
  assumes 1: "p ∧ q ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
proof (rule impI)
  assume 2: "p"
  show "q ⟶ r"
  proof (rule impI)
    assume 3: "q"
    have 4: "p ∧ q" using 2 3 by (rule conjI)
    show "r" using 1 4 by (rule mp)
  qed
qed

(* benber cammonagu *)
lemma ejercicio_22_1:
  assumes "p ∧ q ⟶ r" 
  shows   "p ⟶ (q ⟶ r)"
proof
  assume "p"
  show "q ⟶ r"
  proof
    assume "q"
    with `p` have "p ∧ q" by (rule conjI)
    with `p ∧ q ⟶ r` show "r" by (rule mp)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 23. Demostrar
     (p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
  ------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
   chrgencar pabbergue gleherlop antramhur enrparalv juacanrod hugrubsan
   alikan *)  
lemma ejercicio_23:
  assumes 1: "(p ⟶ q) ⟶ r" 
  shows   "p ∧ q ⟶ r"
proof (rule impI)
  assume 2: "p ∧ q"
  have 3: "p ⟶ q"
  proof (rule impI)
    assume "p"
    show "q" using 2 by (rule conjunct2)
  qed
  show "r" using 1 3 by (rule mp)
qed

(* benber cammonagu *)
lemma ejercicio_23_1:
  assumes "(p ⟶ q) ⟶ r" 
  shows   "p ∧ q ⟶ r"
proof
  assume "p ∧ q"
  hence "q" by (rule conjunct2)
  hence "p ⟶ q" by (rule impI)
  with `(p ⟶ q) ⟶ r` show "r" by (rule mp)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 24. Demostrar
     p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
  ------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
   chrgencar pabbergue gleherlop antramhur enrparalv hugrubsan juacanrod
   cammonagu alikan *)  
lemma ejercicio_24:
  assumes 1: "p ∧ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ r"
proof (rule impI)
  assume 2: "p ⟶ q"
  have 3: "p" using 1 by (rule conjunct1)
  have 4: "q ⟶ r" using 1 by (rule conjunct2)
  have 5: "q" using 2 3 by (rule mp)
  show 6: "r" using 4 5 by (rule mp)
qed

(* benber *)
lemma ejercicio_24_1:
  assumes "p ∧ (q ⟶ r)" 
  shows   "(p ⟶ q) ⟶ r"
proof
  have "q ⟶ r" using assms by (rule conjunct2)
  assume "p ⟶ q"
  moreover have "p" using assms by (rule conjunct1)
  ultimately have "q" by (rule mp)
  with `q ⟶ r` show r by (rule mp)
qed

section {* Disyunciones *}

text {* --------------------------------------------------------------- 
  Ejercicio 25. Demostrar
     p ⊢ p ∨ q
  ------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 benber cammonagu raffergon2 marfruman1
   alfmarcua chrgencar gleherlop pabbergue antramhur enrparalv juacanrod
   hugrubsan alikan *)  
lemma ejercicio_25:
  assumes "p"
  shows   "p ∨ q"
  using assms(1) by (rule disjI1)

text {* --------------------------------------------------------------- 
  Ejercicio 26. Demostrar
     q ⊢ p ∨ q
  ------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 benber cammonagu marfruman1 alfmarcua
   chrgencar pabbergue gleherlop antramhur enrparalv juacanrod hugrubsan
   alikan *)  
lemma ejercicio_26:
  assumes "q"
  shows   "p ∨ q"
  using assms(1) by (rule disjI2)

text {* --------------------------------------------------------------- 
  Ejercicio 27. Demostrar
     p ∨ q ⊢ q ∨ p
  ------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 chrgencar
   pabbergue antramhur enrparalv juacanrod hugrubsan cammonagu alikan *) 
lemma ejercicio_27:
  assumes 1: "p ∨ q"
  shows   "q ∨ p"
using 1 proof (rule disjE)
  assume 2: "p" thus "q ∨ p" by (rule disjI2)
next
  assume 3: "q" thus "q ∨ p" by (rule disjI1)
qed

(* benber alfmarcua gleherlop *)
lemma ejercicio_27_1:
  assumes "p ∨ q"
  shows   "q ∨ p"
proof -
  have "p ∨ q" using assms .
  moreover have "p ⟹ q ∨ p" by (rule disjI2)
  moreover have "q ⟹ q ∨ p" by (rule disjI1)
  ultimately show "q ∨ p" by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 28. Demostrar
     q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
  ------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 chrgencar
   gleherlop alfmarcua pabbergue antramhur enrparalv juacanrod hugrubsan
   cammonagu alikan *) 
lemma ejercicio_28:
  assumes 1: "q ⟶ r" 
  shows   "p ∨ q ⟶ p ∨ r"
proof (rule impI)
  assume 2: "p ∨ q" show "p ∨ r" using 2
  proof (rule disjE)
    assume 3: p thus "p ∨ r" by (rule disjI1)
  next
    assume 4: q have r using 1 4 by (rule mp)
    thus "p ∨ r" by (rule disjI2)
  qed
qed

(* benber *)
lemma ejercicio_28_1:
  assumes "q ⟶ r" 
  shows   "p ∨ q ⟶ p ∨ r"
proof
  assume "p ∨ q"
  moreover have "p ⟹ p ∨ r" by (rule disjI1)
  moreover have "q ⟹ p ∨ r"
  proof (rule disjI2)
    assume "q"
    with `q ⟶ r` show "r" by (rule mp)
  qed
  ultimately show "p ∨ r" by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 29. Demostrar
     p ∨ p ⊢ p
  ------------------------------------------------------------------ *}

(* pabalagon juacanrod marfruman1 *)
lemma ejercicio_29:
  assumes 1: "p ∨ p"
  shows   "p"
using 1 proof (rule disjE)
  assume "p" thus "p" .
next
  assume "p" thus "p" .
qed

(* benber manperjim cammonagu josgomrom4 raffergon2 chrgencar alfmarcua
   gleherlop pabbergue antramhur enrparalv hugrubsan alikan *) 
lemma ejercicio_29_1:
  assumes "p ∨ p"
  shows   "p"
  using assms by (rule disjE)

text {* --------------------------------------------------------------- 
  Ejercicio 30. Demostrar
     p ⊢ p ∨ p
  ------------------------------------------------------------------ *}

(* pabalagon manperjim  benber josgomrom4 raffergon2 marfruman1
   chrgencar alfmarcua pabbergue gleherlop antramhur enrparalv hugrubsan
   juacanrod cammonagu alikan *)  
lemma ejercicio_30:
  assumes "p"
  shows   "p ∨ p"
  using assms(1) by (rule disjI1)

text {* --------------------------------------------------------------- 
  Ejercicio 31. Demostrar
     p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
  ------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua pabbergue
   gleherlop antramhur enrparalv juacanrod hugrubsan alikan *) 
lemma ejercicio_31:
  assumes 1: "p ∨ (q ∨ r)"
  shows   "(p ∨ q) ∨ r" (is "?R")
using 1 proof (rule disjE)
  assume "p" hence "p ∨ q" by (rule disjI1)
  thus ?R by (rule disjI1)
next
  assume "q ∨ r" thus ?R
  proof (rule disjE)
    assume "q" hence "p ∨ q" by (rule disjI2)
    thus "(p ∨ q) ∨ r" by (rule disjI1)
  next
    assume "r" thus ?thesis by (rule disjI2)
  qed
qed

(* benber cammonagu *)
lemma ejercicio_31_1:
  assumes "p ∨ (q ∨ r)"
  shows   "(p ∨ q) ∨ r"
proof -
  have "p ∨ (q ∨ r)" using assms .
  moreover {
    assume "p"
    hence "p ∨ q" by (rule disjI1)
    hence "(p ∨ q) ∨ r" by (rule disjI1)
  }
  moreover {
    assume "q ∨ r"
    moreover {
      assume "q"
      hence "p ∨ q" by (rule disjI2)
      hence "(p ∨ q) ∨ r" by (rule disjI1)
    }
    moreover {
      assume "r"
      hence "(p ∨ q) ∨ r" by (rule disjI2)
    }
    ultimately have "(p ∨ q) ∨ r" by (rule disjE)
  }
  ultimately show "(p ∨ q) ∨ r" by (rule disjE)
qed


text {* --------------------------------------------------------------- 
  Ejercicio 32. Demostrar
     (p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
  ------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop
   pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) 
lemma ejercicio_32:
  assumes 1: "(p ∨ q) ∨ r" 
  shows   "p ∨ (q ∨ r)"
using 1 proof (rule disjE)
  assume "p ∨ q" thus ?thesis
  proof (rule disjE)
    assume p thus ?thesis by (rule disjI1)
  next
    assume q hence "q ∨ r" by (rule disjI1)
    thus ?thesis by (rule disjI2)
  qed
next
  assume r hence "q ∨ r" by (rule disjI2)
  thus ?thesis by (rule disjI2)
qed

(* benber cammonagu *)
lemma ejercicio_32_1:
  assumes "(p ∨ q) ∨ r" 
  shows   "p ∨ (q ∨ r)"
proof -
  have "(p ∨ q) ∨ r" using assms .
  moreover {
    assume "p ∨ q"
    moreover {
      assume "p"
      hence ?thesis by (rule disjI1)
    }
    moreover {
      assume "q"
      hence "q ∨ r" by (rule disjI1)
      hence ?thesis by (rule disjI2)
    }
    ultimately have ?thesis by (rule disjE)
  }
  moreover {
    assume "r"
    hence "q ∨ r" by (rule disjI2)
    hence ?thesis by (rule disjI2)
  }
  ultimately show ?thesis by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 33. Demostrar
     p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
  ------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 chrgencar gleherlop
   alfmarcua pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) 
lemma ejercicio_33:
  assumes 1: "p ∧ (q ∨ r)" 
  shows   "(p ∧ q) ∨ (p ∧ r)"
proof -
  have 2: p using 1 by (rule conjunct1)
  show ?thesis
  proof (rule disjE)
    assume 3: q have "p ∧ q" using 2 3 by (rule conjI)
    thus ?thesis by (rule disjI1)
  next
    assume 4: r have "p ∧ r" using 2 4 by (rule conjI)
    thus ?thesis by (rule disjI2)
  next
    show "q ∨ r" using 1 by (rule conjunct2)
  qed
qed

(* benber cammonagu *)
lemma ejercicio_33_1:
  assumes "p ∧ (q ∨ r)" 
  shows   "(p ∧ q) ∨ (p ∧ r)"
proof -
  have "p" using assms by (rule conjunct1)
  have "q ∨ r" using assms by (rule conjunct2)
  moreover {
    assume "q"
    with `p` have "p ∧ q" by (rule conjI)
    hence ?thesis by (rule disjI1)
  }
  moreover {
    assume "r"
    with `p` have "p ∧ r" by (rule conjI)
    hence ?thesis by (rule disjI2)
  }
  ultimately show ?thesis by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 34. Demostrar
     (p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
  ------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 chrgencar alfmarcua
   gleherlop pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) 
lemma ejercicio_34:
  assumes "(p ∧ q) ∨ (p ∧ r)" 
  shows   "p ∧ (q ∨ r)"
using assms(1) proof (rule disjE)
  assume 2: "p ∧ q" hence q by (rule conjunct2)
  hence 3: "q ∨ r" by (rule disjI1)
  have p using 2 by (rule conjunct1)
  thus ?thesis using 3 by (rule conjI)
next
  assume 4: "p ∧ r" hence r by (rule conjunct2)
  hence 5: "q ∨ r" by (rule disjI2)
  have p using 4 by (rule conjunct1)
  thus ?thesis using 5 by (rule conjI)
qed

(* benber cammonagu *)
lemma ejercicio_34_1:
  assumes "(p ∧ q) ∨ (p ∧ r)" 
  shows   "p ∧ (q ∨ r)"
proof -
  have "(p ∧ q) ∨ (p ∧ r)" using assms .
  moreover {
    assume "p ∧ q"
    hence "p" by (rule conjunct1)
    moreover {
      have "q" using `p ∧ q` by (rule conjunct2)
      hence "q ∨ r" by (rule disjI1)
    }
    ultimately have ?thesis by (rule conjI)
  }
  moreover {
    assume "p ∧ r"
    hence "p" by (rule conjunct1)
    moreover {
      have "r" using `p ∧ r` by (rule conjunct2)
      hence "q ∨ r" by (rule disjI2)
    }
    ultimately have ?thesis by (rule conjI)
  }
  ultimately show ?thesis by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 35. Demostrar
     p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
  ------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 chrgencar alfmarcua
   gleherlop pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) 
lemma ejercicio_35:
  assumes "p ∨ (q ∧ r)" 
  shows   "(p ∨ q) ∧ (p ∨ r)"
using assms(1) proof (rule disjE)
  assume 1: p hence 2: "p ∨ r" by (rule disjI1)
  have "p ∨ q" using 1 by (rule disjI1)
  thus ?thesis using 2 by (rule conjI)
next
  assume 3: "q ∧ r" hence r by (rule conjunct2)
  hence 4: "p ∨ r" by (rule disjI2)
  have q using 3 by (rule conjunct1)
  hence "p ∨ q" by (rule disjI2)
  thus ?thesis using 4 by (rule conjI)
qed

(* benber cammonagu *)
lemma ejercicio_35_1:
  assumes "p ∨ (q ∧ r)" 
  shows   "(p ∨ q) ∧ (p ∨ r)"
proof -
  have "p ∨ (q ∧ r)" using assms .
  moreover {
    assume "p"
    hence "p ∨ q" by (rule disjI1)
    moreover have "p ∨ r" using `p` by (rule disjI1)
    ultimately have ?thesis by (rule conjI)
  }
  moreover {
    assume "q ∧ r"
    {
      have "q" using `q ∧ r` by (rule conjunct1)
      hence "p ∨ q" by (rule disjI2)
    }
    moreover {
      have "r" using `q ∧ r` by (rule conjunct2)
      hence "p ∨ r" by (rule disjI2)
    }
    ultimately have ?thesis by (rule conjI)
  }
  ultimately show ?thesis by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 36. Demostrar
     (p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)
  ------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 chrgencar alfmarcua
   gleherlop pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) 
lemma ejercicio_36:
  assumes 1: "(p ∨ q) ∧ (p ∨ r)"
  shows   "p ∨ (q ∧ r)"
proof -
  have 2: "p ∨ q" using 1 by (rule conjunct1)
  have 3: "p ∨ r" using 1 by (rule conjunct2)
  show ?thesis using 2
  proof (rule disjE)
    assume p thus ?thesis by (rule disjI1)
  next
    assume 4: q show ?thesis using 3
    proof (rule disjE)
      assume p thus ?thesis by (rule disjI1)
    next
      assume 5: r have "q ∧ r" using 4 5 by (rule conjI)
      thus ?thesis by (rule disjI2)
    qed
  qed
qed

(* benber cammonagu *)
lemma ejercicio_36_1:
  assumes "(p ∨ q) ∧ (p ∨ r)"
  shows   "p ∨ (q ∧ r)"
proof -
  have "p ∨ q" using assms by (rule conjunct1)
  moreover {
    assume "p"
    hence ?thesis by (rule disjI1)
  }
  moreover {
    assume "q"
    have "p ∨ r" using assms by (rule conjunct2)
    moreover {
      assume "p"
      hence ?thesis by (rule disjI1)
    }
    moreover {
      assume "r"
      with `q` have "q ∧ r" by (rule conjI)
      hence ?thesis by (rule disjI2)
    }
    ultimately have ?thesis by (rule disjE)
  }
  ultimately show ?thesis by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 37. Demostrar
     (p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
  ------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop
   pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) 
lemma ejercicio_37:
  assumes 1: "(p ⟶ r) ∧ (q ⟶ r)" 
  shows   "p ∨ q ⟶ r"
proof (rule impI)
  have 2: "p ⟶ r" using 1 by (rule conjunct1)
  have 3: "q ⟶ r" using 1 by (rule conjunct2)
  assume 4: "p ∨ q" show "r" using 4
  proof (rule disjE)
    assume 5: "p" show "r" using 2 5 by (rule mp)
  next
    assume 6: "q" show "r" using 3 6 by (rule mp)
  qed
qed

(* benber cammonagu *)
lemma ejercicio_37_1:
  assumes "(p ⟶ r) ∧ (q ⟶ r)" 
  shows   "p ∨ q ⟶ r"
proof
  assume "p ∨ q"
  moreover {
    have "p ⟶ r" using assms by (rule conjunct1)
    moreover assume "p"
    ultimately have "r" by (rule mp)
  }
  moreover {
    have "q ⟶ r" using assms by (rule conjunct2)
    moreover assume "q"
    ultimately have "r" by (rule mp)
  }
  ultimately show "r" by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 38. Demostrar
     p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
  ------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop
   pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) 
lemma ejercicio_38:
  assumes "p ∨ q ⟶ r" 
  shows   "(p ⟶ r) ∧ (q ⟶ r)"
proof (rule conjI)
  show "p ⟶ r"
  proof (rule impI)
    assume "p" hence 1: "p ∨ q" by (rule disjI1)
    show "r" using assms(1) 1 by (rule mp)
  qed
next
  show "q ⟶ r"
  proof (rule impI)
    assume q hence 2: "p ∨ q" by (rule disjI2)
    show r using assms(1) 2 by (rule mp)
  qed
qed

(* benber cammonagu*)
lemma ejercicio_38_1:
  assumes "p ∨ q ⟶ r" 
  shows   "(p ⟶ r) ∧ (q ⟶ r)"
proof
  show "p ⟶ r"
  proof
    assume "p"
    hence "p ∨ q" by (rule disjI1)
    with assms show "r" by (rule mp)
  qed
next
  show "q ⟶ r"
  proof
    assume "q"
    hence "p ∨ q" by (rule disjI2)
    with assms show "r" by (rule mp)
  qed
qed

section {* Negaciones *}

text {* --------------------------------------------------------------- 
  Ejercicio 39. Demostrar
     p ⊢ ¬¬p
  ------------------------------------------------------------------ *}

(* pabalagon manperjim  benber josgomrom4 raffergon2 gleherlop
   marfruman1 chrgencar alfmarcua pabbergue enrparalv juacanrod
   hugrubsan cammonagu alikan *)  
lemma ejercicio_39:
  assumes "p"
  shows   "¬¬p"
  using assms(1) by (rule notnotI)

text {* --------------------------------------------------------------- 
  Ejercicio 40. Demostrar
     ¬p ⊢ p ⟶ q
  ------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua pabbergue
   gleherlop juacanrod enrparalv hugrubsan alikan *) 
lemma ejercicio_40:
  assumes 1: "¬p"
  shows   "p ⟶ q"
proof (rule impI)
  assume 2: p show q using 1 2 by (rule notE)
qed

(* benber cammonagu *)
lemma ejercicio_40_1:
  assumes "¬p" 
  shows   "p ⟶ q"
proof
  assume "p"
  with `¬p` show "q" by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 41. Demostrar
     p ⟶ q ⊢ ¬q ⟶ ¬p
  ------------------------------------------------------------------ *}

(* pabalagon manperjim raffergon2 josgomrom4 marfruman1 alfmarcua
   pabbergue gleherlop enrparalv juacanrod hugrubsan alikan *) 
lemma ejercicio_41:
  assumes 1: "p ⟶ q"
  shows   "¬q ⟶ ¬p"
proof (rule impI)
  assume 2: "¬q" show "¬p" using 1 2 by (rule mt)
qed

(* benber cammonagu *)
lemma ejercicio_41_1:
  assumes "p ⟶ q"
  shows   "¬q ⟶ ¬p"
proof
  assume "¬q"
  with `p ⟶ q` show "¬p" by (rule mt)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 42. Demostrar
     p∨q, ¬q ⊢ p
  ------------------------------------------------------------------ *}

(* pabalagon manperjim raffergon2 josgomrom4 marfruman1 alfmarcua
   pabbergue gleherlop enrparalv juacanrod hugrubsan alikan *) 
lemma ejercicio_42:
  assumes "p∨q"
          "¬q" 
  shows   "p"
using assms(1) proof (rule disjE)
  assume "p" thus "p" .
next
  assume 2: "q" show "p" using assms(2) 2 by (rule notE)
qed

(* benber cammonagu *)
lemma ejercicio_42_1:
  assumes "p∨q"
          "¬q" 
  shows   "p"
proof -
  note `p ∨ q`
  moreover have "p ⟹ p" .
  moreover {
    assume "q"
    with `¬q` have "p" by (rule notE)
  }
  ultimately show "p" by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 43. Demostrar
     p ∨ q, ¬p ⊢ q
  ------------------------------------------------------------------ *}

(* pabalagon manperjim raffergon2 josgomrom4 marfruman1 alfmarcua
   pabbergue gleherlop enrparalv juacanrod hugrubsan alikan *) 
lemma ejercicio_43:
  assumes "p ∨ q"
          "¬p" 
  shows   "q"
using assms(1) proof (rule disjE)
  assume 1: "p" show "q" using assms(2) 1 by (rule notE)
next
  assume "q" thus "q" .
qed

(* benber cammonagu*)
lemma ejercicio_43_1:
  assumes "p ∨ q"
          "¬p" 
  shows   "q"
proof -
  note `p ∨ q`
  moreover {
    assume "p"
    with `¬p` have "q" by (rule notE)
  }
  moreover have "q ⟹ q" .
  ultimately show "q" by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 44. Demostrar
     p ∨ q ⊢ ¬(¬p ∧ ¬q)
  ------------------------------------------------------------------ *}

(* pabalagon manperjim gleherlop josgomrom4 marfruman1 pabbergue
   juacanrod hugrubsan alikan *) 
lemma ejercicio_44:
  assumes "p ∨ q" 
  shows   "¬(¬p ∧ ¬q)"
proof (rule notI)
  assume 1: "¬p ∧ ¬q" hence 2: "¬p" by (rule conjunct1)
  have 3: "¬q" using 1 by (rule conjunct2)
  show "False"
  using assms(1) proof (rule disjE)
    assume 4: "p" show ?thesis using 2 4 by (rule notE)
  next
    assume 5: "q" show ?thesis using 3 5 by (rule notE)
  qed
qed

(* benber alfmarcua cammonagu *)
lemma ejercicio_44_1:
  assumes "p ∨ q" 
  shows   "¬(¬p ∧ ¬q)"
proof
  assume "¬p ∧ ¬q"
  note `p ∨ q`
  moreover {
    from `¬p ∧ ¬q` have "¬p" by (rule conjunct1)
    moreover assume "p"
    ultimately have "False" by (rule notE)
  }
  moreover {
    from `¬p ∧ ¬q` have "¬q" by (rule conjunct2)
    moreover assume "q"
    ultimately have "False" by (rule notE)
  }
  ultimately show "False" by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 45. Demostrar
     p ∧ q ⊢ ¬(¬p ∨ ¬q)
  ------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 gleherlop pabbergue
   juacanrod hugrubsan alikan *) 
lemma ejercicio_45:
  assumes 1: "p ∧ q" 
  shows   "¬(¬p ∨ ¬q)"
proof (rule notI)
  assume 2: "¬p ∨ ¬q" have 3: "p" using 1 by (rule conjunct1)
  have 4: "q" using 1 by (rule conjunct2)
  show "False" using 2
  proof (rule disjE)
    assume "¬p" thus ?thesis using 3 by (rule notE)
  next
    assume "¬q" thus ?thesis using 4 by (rule notE)
  qed
qed

(* benber alfmarcua cammonagu *)
lemma ejercicio_45_1:
  assumes "p ∧ q" 
  shows   "¬(¬p ∨ ¬q)"
proof
  assume "¬p ∨ ¬q"
  moreover {
    assume "¬p"
    moreover have "p" using `p ∧ q` by (rule conjunct1)
    ultimately have "False" by (rule notE)
  }
  moreover {
    assume "¬q"
    moreover have "q" using `p ∧ q` by (rule conjunct2)
    ultimately have "False" by (rule notE)
  }
  ultimately show False by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 46. Demostrar
     ¬(p ∨ q) ⊢ ¬p ∧ ¬q
  ------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 gleherlop pabbergue
   juacanrod hugrubsan alikan *) 
lemma ejercicio_46:
  assumes 1: "¬(p ∨ q)" 
  shows   "¬p ∧ ¬q"
proof (rule conjI)
  show "¬p"
  proof (rule notI)
    assume p hence 2: "p ∨ q" by (rule disjI1)
    show False using 1 2 by (rule notE)
  qed
  show "¬q"
  proof (rule notI)
    assume q hence 3: "p ∨ q" by (rule disjI2)
    show False using 1 3 by (rule notE)
  qed
qed

(* benber cammmonagu *)
lemma ejercicio_46_1:
  assumes "¬(p ∨ q)" 
  shows   "¬p ∧ ¬q"
proof
  show "¬p"
  proof (rule ccontr)
    assume "¬¬p"
    hence "p" by (rule notnotD)
    hence "p ∨ q" by (rule disjI1)
    with assms show "False" by (rule notE)
  qed
next
  show "¬q"
  proof (rule ccontr)
    assume "¬¬q"
    hence "q" by (rule notnotD)
    hence "p ∨ q" by (rule disjI2)
    with assms show "False" by (rule notE)
  qed
qed

(* alfmarcua *)
lemma ejercicio_46_2:
  assumes "¬(p ∨ q)" 
  shows   "¬p ∧ ¬q"
proof (rule conjI)
  have "p ⟹ p ∨ q" by (rule disjI1)
  then have "p ⟶ p ∨ q" by (rule impI)
  then show "¬ p" using assms by (rule mt)
next
  have "q ⟹ p ∨ q" by (rule disjI2)
  then have "q ⟶ p ∨ q" by (rule impI)
  then show "¬ q" using assms by (rule mt)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 47. Demostrar
     ¬p ∧ ¬q ⊢ ¬(p ∨ q)
  ------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 pabbregue juacanrod
   hugrubsan alikan *) 
lemma ejercicio_47:
  assumes 1: "¬p ∧ ¬q" 
  shows   "¬(p ∨ q)"
proof (rule notI)
  have 2: "¬p" using 1 by (rule conjunct1)
  have 3: "¬q" using 1 by (rule conjunct2)
  assume 4: "p ∨ q"
  show False
  using 4 proof (rule disjE)
    assume 5: p show ?thesis using 2 5 by (rule notE)
  next
    assume 6: q show ?thesis using 3 6 by (rule notE)
  qed
qed

(* benber gleherlop cammonagu*)
lemma ejercicio_47_1:
  assumes "¬p ∧ ¬q" 
  shows   "¬(p ∨ q)"
proof
  assume "p ∨ q"
  hence "¬(¬p ∧ ¬q)" by (rule ejercicio_44_1)
  thus "False" using assms by (rule notE)
qed

(* alfmarcua *)
lemma ejercicio_47_2:
  assumes "¬p ∧ ¬q" 
  shows   "¬(p ∨ q)"
proof (rule notI)
  have "¬ p" using assms by (rule conjunct1)
  have "¬ q" using assms by (rule conjunct2)
  assume "p ∨ q"
  then have "q" using `¬ p` by (rule ejercicio_43)
  show False using `¬ q` `q` by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 48. Demostrar
     ¬p ∨ ¬q ⊢ ¬(p ∧ q)
  ------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 pabbergue juacanrod
   hugrubsan alikan *) 
lemma ejercicio_48:
  assumes 1: "¬p ∨ ¬q"
  shows   "¬(p ∧ q)"
proof (rule notI)
  assume 2: "p ∧ q" hence 3: p by (rule conjunct1)
  have 4: q using 2 by (rule conjunct2)
  show False
  using 1 proof (rule disjE)
    assume "¬p" thus ?thesis using 3 by (rule notE)
  next
    assume "¬q" thus ?thesis using 4 by (rule notE)
  qed
qed

(* benber alfmarcua gleherlop cammonagu *)
lemma ejercicio_48_1:
  assumes "¬p ∨ ¬q"
  shows   "¬(p ∧ q)"
proof
  assume "p ∧ q"
  hence "¬(¬p ∨ ¬q)" by (rule ejercicio_45_1)
  thus "False" using assms by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 49. Demostrar
     ⊢ ¬(p ∧ ¬p)
  ------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 alfmarcu gleherlop
   hugrubsan juacanrod cammonagu alikan *) 
lemma ejercicio_49:
  "¬(p ∧ ¬p)"
proof (rule notI)
  assume 1: "p ∧ ¬p" hence 2: p by (rule conjunct1)
  have "¬p" using 1 by (rule conjunct2)
  thus "False" using 2 by (rule notE)
qed

(* benber *)
lemma ejercicio_49_1:
  "¬(p ∧ ¬p)"
proof
  assume "p ∧ ¬p"
  hence "¬p" by (rule conjunct2)
  moreover have "p" using `p ∧ ¬p` by (rule conjunct1)
  ultimately show "False" by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 50. Demostrar
     p ∧ ¬p ⊢ q
  ------------------------------------------------------------------ *}

(* pabalagon manperjim raffergon2 josgomrom4 marfruman1 gleherlop
   alfmarcua enrparalv pabbergue juacanrod hugrubsan alikan *) 
lemma ejercicio_50:
  assumes 1: "p ∧ ¬p"
  shows   "q"
proof (rule notE)
  show p using 1 by (rule conjunct1)
  show "¬p" using 1 by (rule conjunct2)
qed

(* benber cammonagu*)
lemma ejercicio_50_1:
  assumes "p ∧ ¬p" 
  shows   "q"
proof -
  have "¬p" using `p ∧ ¬p` by (rule conjunct2)
  moreover have "p" using `p ∧ ¬p` by (rule conjunct1)
  ultimately show "q" by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 51. Demostrar
     ¬¬p ⊢ p
  ------------------------------------------------------------------ *}

(* pabalagon manperjim benber raffergon2 josgomrom4 marfruman1 gleherlop
   alfmarcua enrparalv pabbergue juacanrod hugrubsan cammmonagu alikan *) 
lemma ejercicio_51:
  assumes "¬¬p"
  shows   "p"
  using assms(1) by (rule notnotD)

text {* --------------------------------------------------------------- 
  Ejercicio 52. Demostrar
     ⊢ p ∨ ¬p
  ------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 juacanrod pabbergue alikan *)
lemma ejercicio_52:
  "p ∨ ¬p"
proof (rule ccontr)
  assume 1: "¬(p ∨ ¬p)"
  have 2: "¬p" proof (rule notI)
    assume p hence 3: "p ∨ ¬p" by (rule disjI1)
    show "False" using 1 3 by (rule notE)
  qed
  have 4: "p ∨ ¬p" using 2 by (rule disjI2)
  show "False" using 1 4 by (rule notE)
qed

(* benber cammonagu *)
lemma ejercicio_52_1:
  "p ∨ ¬p"
proof (rule ccontr)
  assume "¬ (p ∨ ¬ p)"
  hence "¬p ∧ ¬¬p" by (rule ejercicio_46_1)
  hence "¬p" by (rule conjunct1)
  moreover {
    have "¬¬p" using `¬p ∧ ¬¬p` by (rule conjunct2)
    hence "p" by (rule notnotD)
  }
  ultimately show "False" by (rule notE)
qed

(* alfmarcua *)
lemma ejercicio_52_2:
  "p ∨ ¬p"
proof (rule ccontr)
  assume "¬ (p ∨ ¬ p)"
  then have "¬ p ∧ ¬¬ p" by (rule ejercicio_46)
  then show False by (rule ejercicio_50)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 53. Demostrar
     ⊢ ((p ⟶ q) ⟶ p) ⟶ p
  ------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop
   juacanrod pabbergue *) 
lemma ejercicio_53:
  "((p ⟶ q) ⟶ p) ⟶ p"
proof (rule impI)
  assume 1: "(p ⟶ q) ⟶ p"
  show p proof (rule ccontr)
    assume 2: "¬p"
    have 3: "¬(p ⟶ q)" using 1 2 by (rule mt)
    have 4: "p ⟶ q" proof (rule impI)
      assume 5: p show q using 2 5 by (rule notE)
    qed
    show False using 3 4 by (rule notE)
  qed
qed

(* benber cammonagu *)
lemma ejercicio_53_1:
  "((p ⟶ q) ⟶ p) ⟶ p"
proof
  assume "(p ⟶ q) ⟶ p"
  have "p ∨ ¬p" by (rule ejercicio_52_1)
  moreover have "p ⟹ p" .
  moreover {
    assume "¬ p"
    hence "p ⟶ q" by (rule ejercicio_40_1)
    with `(p ⟶ q) ⟶ p` have "p" by (rule mp)
  }
  ultimately show "p" by (rule disjE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 54. Demostrar
     ¬q ⟶ ¬p ⊢ p ⟶ q
  ------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 gleherlop juacanrod
   pabbergue *) 
lemma ejercicio_54:
  assumes 1: "¬q ⟶ ¬p"
  shows   "p ⟶ q"
proof (rule impI)
  assume 2: "p" hence 3: "¬¬p" by (rule notnotI)
  have "¬¬q" using 1 3 by (rule mt)
  thus "q" by (rule notnotD)
qed

(* benber alfmarcua  cammonagu *)
lemma ejercicio_54_1:
  assumes "¬q ⟶ ¬p"
  shows   "p ⟶ q"
proof
  assume "p"
  hence "¬¬p" by (rule notnotI)
  with assms have "¬¬q" by (rule mt)
  thus "q" by (rule notnotD)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 55. Demostrar
     ¬(¬p ∧ ¬q) ⊢ p ∨ q
  ------------------------------------------------------------------ *}

(* pabalagon marfruman1*)
lemma ejercicio_55:
  assumes 1: "¬(¬p ∧ ¬q)"
  shows   "p ∨ q"
proof (rule ccontr)
  assume 2: "¬(p ∨ q)"
  have 3: "p"
  proof (rule ccontr)
    assume 4: "¬p"
    have 5: "q"
    proof (rule ccontr)
      assume 6: "¬q" have 7: "¬p ∧ ¬q" using 4 6 by (rule conjI)
      show False using 1 7 by (rule notE)
    qed
    have 8: "p ∨ q" using 5 by (rule disjI2)
    show False using 2 8 by (rule notE)
  qed
  have 9: "p ∨ q" using 3 by (rule disjI1)
  show False using 2 9 by (rule notE)
qed

(* benber alfmarcua josgomrom4 manperjim pabbergue juacanrod cammonagu *)
lemma ejercicio_55_1:
  assumes "¬(¬p ∧ ¬q)"
  shows   "p ∨ q"
proof (rule ccontr)
  assume "¬(p ∨ q)"
  hence "¬p ∧ ¬q" by (rule ejercicio_46_1)
  with assms show False by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 56. Demostrar
     ¬(¬p ∨ ¬q) ⊢ p ∧ q
  ------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 gleherlop juacanrod
   pabbergue *) 
lemma ejercicio_56:
  assumes 1: "¬(¬p ∨ ¬q)" 
  shows   "p ∧ q"
proof (rule conjI)
  show 3: p
  proof (rule ccontr)
    assume "¬p" hence 4: "¬p ∨ ¬q" by (rule disjI1)
    show False using 1 4 by (rule notE)
  qed
  show 5: q
  proof (rule ccontr)
    assume "¬q" hence 6: "¬p ∨ ¬q" by (rule disjI2)
    show False using 1 6 by (rule notE)
  qed
qed

(* benber alfmarcua cammonagu *)
lemma ejercicio_56_1:
  assumes "¬(¬p ∨ ¬q)" 
  shows   "p ∧ q"
proof -
  have "¬¬p ∧ ¬¬q" using assms by (rule ejercicio_46_1)
  hence "¬¬p" by (rule conjunct1)
  hence "p" by (rule notnotD)
  moreover {
    have "¬¬q" using `¬¬p ∧ ¬¬q` by (rule conjunct2)
    hence "q" by (rule notnotD)
  }
  ultimately show "p ∧ q" by (rule conjI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 57. Demostrar
     ¬(p ∧ q) ⊢ ¬p ∨ ¬q
  ------------------------------------------------------------------ *}

(* pabalagon manperjim marfruman1 josgomrom4 gleherlop juacanrod
   pabbergue *) 
lemma ejercicio_57:
  assumes 1: "¬(p ∧ q)"
  shows   "¬p ∨ ¬q"
proof (rule ccontr)
  assume 2: "¬(¬p ∨ ¬q)"
  show False using 1
  proof (rule notE)
    show 3: "p ∧ q"
    proof (rule conjI)
      show p
      proof (rule ccontr)
        assume "¬p" hence 4: "¬p ∨ ¬q" by (rule disjI1)
        show False using 2 4 by (rule notE)
      qed
    next
      show q
      proof (rule ccontr)
        assume "¬q" hence 5: "¬p ∨ ¬q" by (rule disjI2)
        show False using 2 5 by (rule notE)
      qed
    qed
  qed
qed

(* benber alfmarcua cammonagu *)
lemma ejercicio_57_1:
  assumes "¬(p ∧ q)"
  shows   "¬p ∨ ¬q"
proof (rule ccontr)
  assume "¬(¬p ∨ ¬q)"
  hence "p ∧ q" by (rule ejercicio_56_1)
  with assms show "False" by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 58. Demostrar
     ⊢ (p ⟶ q) ∨ (q ⟶ p)
  ------------------------------------------------------------------ *}

(* pabalagon manperjim josgomrom4 marfruman1 juacanrod pabbergue *)
lemma ejercicio_58:
  "(p ⟶ q) ∨ (q ⟶ p)"
proof -
  have "(p ⟶ q) ∨ ¬(p ⟶ q)" proof (rule ccontr)
    assume 1: "¬((p ⟶ q) ∨ ¬(p ⟶ q))"
    have 2: "¬(p ⟶ q)" proof (rule notI)
      assume "p ⟶ q" 
      hence 3: "(p ⟶ q) ∨ ¬(p ⟶ q)" by (rule disjI1)
      show False using 1 3 by (rule notE)
    qed
    hence 4: "(p ⟶ q) ∨ ¬(p ⟶ q)" by (rule disjI2)
    show "False" using 1 4 by (rule notE)
  qed
  thus ?thesis proof (rule disjE)
    assume "p ⟶ q" thus ?thesis by (rule disjI1)
  next
    assume 1: "¬(p ⟶ q)"
    have "q ⟶ p" proof (rule impI)
      assume 2: q
      have 3: "p ⟶ q" proof (rule impI)
        assume p show q using 2 .
      qed
      show p using 1 3 by (rule notE)
    qed
    thus ?thesis by (rule disjI2)
  qed
qed

(* pabalagon gleherlop *)
lemma ejercicio_58_2:
  "(p ⟶ q) ∨ (q ⟶ p)"
proof (rule ccontr)
  assume 1: "¬((p ⟶ q) ∨ (q ⟶ p))"
  hence 1: "(p ∧ ¬q) ∧ (q ∧ ¬p)" by simp
  hence "p ∧ ¬q" ..
  hence 2: p ..
  have "q ∧ ¬p" using 1 ..
  hence 3: "¬p" ..
  show False using 3 2 by (rule notE)
qed

(* benber cammonagu *)
lemma ejercicio_58_1:
  "(p ⟶ q) ∨ (q ⟶ p)"
proof (rule ccontr)
  assume "¬ ((p ⟶ q) ∨ (q ⟶ p))"
  hence 1: "¬(p ⟶ q) ∧ ¬(q ⟶ p)" by (rule ejercicio_46_1)

  have "p ∨ ¬p" by (rule ejercicio_52_1)
  moreover {
    assume "p"
    hence "q ⟶ p" by (rule ejercicio_7_1)

    have "¬(q ⟶ p)" using 1 by (rule conjunct2)
    hence "False" using `q ⟶ p` by (rule notE)
  }
  moreover {
    assume "¬p"
    hence "p ⟶ q" by (rule ejercicio_40_1)

    have "¬(p ⟶ q)" using 1 by (rule conjunct1)
    hence "False" using `p ⟶ q` by (rule notE)
  }
  ultimately show "False" by (rule disjE)
  moreover {
    assume "p"
    hence "q ⟶ p" by (rule ejercicio_7_1)

    have "¬(q ⟶ p)" using 1 by (rule conjunct2)
    hence "False" using `q ⟶ p` by (rule notE)
  }
qed

(* alfmarcua *)
lemma ejercicio_58_3:
  "(p ⟶ q) ∨ (q ⟶ p)"
proof (rule disjE)
  show "p ∨ ¬ p" by (rule ejercicio_52)
next
  assume "¬p"
  then have "p ⟶ q" by (rule ejercicio_40)
  then show ?thesis by (rule disjI1)
next
  assume "p"
  then have "q ⟶ p" by (rule ejercicio_7)
  then show ?thesis by (rule disjI2)
qed

end

@@ Línea 1: / Línea 1: @@
 <source lang="isabelle">
-chapter {* R7: Deducción natural de primer orden *}
+chapter {* R6: Deducción natural proposicional *}
-theory R7_Deduccion_natural_de_primer_orden
+theory R6_Deduccion_natural_proposicional_alu
 imports Main
 begin
+text {*
+  ---------------------------------------------------------------------
+  El objetivo de esta relación es demostrar cada uno de los ejercicios
+  usando sólo las reglas básicas de deducción natural de la lógica
+  proposicional (sin usar el método auto).
-text {*
+   Las reglas básicas de la deducción natural son las siguientes:
-   Demostrar o refutar los siguientes lemas usando sólo las reglas
-  básicas de deducción natural de la lógica proposicional, de los
-  cuantificadores y de la igualdad:
    · conjI:      ⟦P; Q⟧ ⟹ P ∧ Q
    · conjunct1:  P ∧ Q ⟹ P
    · conjunct2:  P ∧ Q ⟹ Q
    · notnotD:    ¬¬ P ⟹ P
+  · notnotI:    P ⟹ ¬¬ P
    · mp:         ⟦P ⟶ Q; P⟧ ⟹ Q
+  · mt:         ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
    · impI:       (P ⟹ Q) ⟹ P ⟶ Q
    · disjI1:     P ⟹ P ∨ Q
@@ Línea 26: / Línea 31: @@
    · iffD2:      ⟦P = Q; Q⟧ ⟹ P
    · ccontr:     (¬P ⟹ False) ⟹ P
+   ---------------------------------------------------------------------
-   · allI:       ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
-  · allE:       (⋀x. P x) ⟹ ∀x. P x
-  · exI:        P x ⟹ ∃x. P x
-  · exE:        ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q
-  · refl:       t = t
-  · subst:      ⟦s = t; P s⟧ ⟹ P t
-  · trans:      ⟦r = s; s = t⟧ ⟹ r = t
-  · sym:        s = t ⟹ t = s
-  · not_sym:    t ≠ s ⟹ s ≠ t
-  · ssubst:     ⟦t = s; P s⟧ ⟹ P t
-  · box_equals: ⟦a = b; a = c; b = d⟧ ⟹ a: = d
-  · arg_cong:   x = y ⟹ f x = f y
-  · fun_cong:   f = g ⟹ f x = g x
-  · cong:       ⟦f = g; x = y⟧ ⟹ f x = g y
 *}
 text {*
-   Se usarán las reglas notnotI, mt y not_ex que demostramos a
+   Se usarán las reglas notnotI y mt que demostramos a continuación. *}
-  continuación. *}
 lemma notnotI: "P ⟹ ¬¬ P"
@@ Línea 54: / Línea 43: @@
 by auto
-lemma no_ex: "¬(∃x. P(x)) ⟹ ∀x. ¬P(x)"
+section {* Implicaciones *}
-by auto
 text {* ---------------------------------------------------------------
    Ejercicio 1. Demostrar
-        P a ⟶ (∃x. Q x) ⊢ ∃x. P a ⟶ Q x
+        p ⟶ q, p ⊢ q
    ------------------------------------------------------------------ *}
+(* pabalagon manperjim josgomrom4 cammonagu raffergon2 chrgencar
+   gleherlop giafus1 marfruman1 enrparalv pabbergue antramhur alikan
+   juacanrod hugrubsan *)
+lemma ejercicio_1:
+  assumes 1: "p ⟶ q" and
+: "p"
+  shows "q"
+proof -
+  show "q" using 1 2 by (rule mp)
+qed
+(* benber alfmarcua *)
+lemma ejercicio_1_1:
+  assumes "p ⟶ q"
+          "p"
+  shows "q"
+  using assms by (rule mp)
+text {* ---------------------------------------------------------------
+  Ejercicio 2. Demostrar
+     p ⟶ q, q ⟶ r, p ⊢ r
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim josgomrom4 cammonagu gleherlop raffergon2
+   chrgencar giafus1 marfruman1 alfmarcua enrparalv pabbergue antramhur
+   alikan juacanrod hugrubsan *)
+lemma ejercicio_2:
+  assumes 1: "p ⟶ q" and
+: "q ⟶ r" and
+: "p"
+  shows "r"
+proof -
+  have 4: "q" using 1 3 by (rule mp)
+  show "r" using 2 4 by (rule mp)
+qed
 (* benber *)
-lemma
+lemma ejercicio_2_1:
-   assumes "P a ⟶ (∃x. Q x)"
+   assumes "p ⟶ q"
-   shows "∃x. P a ⟶ Q x"
+          "q ⟶ r"
-proof (rule ccontr)
+          "p"
-   assume "∄x. P a ⟶ Q x"
+  shows "r"
+proof -
+  have "q" using `p ⟶ q` `p` by (rule mp)
+  with `q ⟶ r` show "r" by (rule mp)
+qed
+text {* ---------------------------------------------------------------
+  Ejercicio 3. Demostrar
+     p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim josgomrom4 cammonagu gleherlop raffergon2
+   chrgencar giafus1 marfruman1 alfmarcua enrparalv pabbergue antramhur
+   alikan juacanrod hugrubsan *)
+lemma ejercicio_3:
+  assumes 1: "p ⟶ (q ⟶ r)" and
+: "p ⟶ q" and
+: "p"
+   shows "r"
+proof -
+  have 4: "q ⟶ r" using 1 3 by (rule mp)
+  have 5: "q" using 2 3 by (rule mp)
+  show "r" using 4 5 by (rule mp)
+qed
+(* benber *)
+lemma ejercicio_3_1:
+  assumes "p ⟶ (q ⟶ r)"
+          "p ⟶ q"
+          "p"
+  shows "r"
+proof -
+  have "q ⟶ r" using `p ⟶ (q ⟶ r)` `p` by (rule mp)
+  moreover have "q" using `p ⟶ q` `p` by (rule mp)
+  ultimately show "r" by (rule mp)
+qed
+text {* ---------------------------------------------------------------
+  Ejercicio 4. Demostrar
+     p ⟶ q, q ⟶ r ⊢ p ⟶ r
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim josgomrom4 cammonagu chrgencar raffergon2
+   gleherlop giafus1 marfruman1 alfmarcua enrparalv pabbergue antramhur
+   alikan juacanrod hugrubsan *)
+lemma ejercicio_4:
+  assumes 1: "p ⟶ q" and
+: "q ⟶ r"
+  shows "p ⟶ r"
+proof -
+  { assume 3: "p"
+    have 4: "q" using 1 3 by (rule mp)
+    have 5: "r" using 2 4 by (rule mp)}
+  thus "p ⟶ r" by (rule impI)
+qed
+(* benber *)
+lemma ejercicio_4_1:
+  assumes "p ⟶ q"
+          "q ⟶ r"
+  shows "p ⟶ r"
+proof
+   assume p
+  with `p ⟶ q` have "q" by (rule mp)
+  with `q ⟶ r` show "r" by (rule mp)
+qed
+text {* ---------------------------------------------------------------
+  Ejercicio 5. Demostrar
+     p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim raffergon2 giafus1 gleherlop marfruman1 alfmarcua
+   enrparalv chrgencar pabbergue antramhur alikan hugrubsan *)
+lemma ejercicio_5:
+  assumes 1: "p ⟶ (q ⟶ r)"
+  shows   "q ⟶ (p ⟶ r)"
+proof (rule impI)
+  assume 2: "q"
+  show "p ⟶ r"
+  proof (rule impI)
+    assume 3: "p"
+    have 4: "q ⟶ r" using 1 3 by (rule mp)
+    show "r" using 4 2 by (rule mp)
+  qed
+qed
-   have "P a ⟶ (∃x. P a ⟶ Q x)"
+(* benber josgomrom4 juacanrod cammonagu  *)
+lemma ejercicio_5_1:
+   assumes "p ⟶ (q ⟶ r)"
+  shows   "q ⟶ (p ⟶ r)"
+proof
+  assume "q"
+  show "p ⟶ r"
    proof
-     assume "P a"
+     assume "p"
-     with assms have "∃x. Q x" by (rule mp)
+     with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
-     moreover have "⋀x. Q x ⟹ ∃x'. P a ⟶ Q x'"
+     thus "r" using `q` by (rule mp)
-    proof -
+  qed
-       fix x
+qed
-       assume "Q x"
-      hence "P a ⟶ Q x" by (rule impI)
+(* pabalagon *)
-      thus "∃x'. P a ⟶ Q x'" by (rule exI)
+lemma ejercicio_5_2:
-     qed
+  assumes 1: "p ⟶ (q ⟶ r)"
-     ultimately show "∃x. P a ⟶ Q x" by (rule exE)
+  shows   "q ⟶ (p ⟶ r)"
+proof -
+  { assume 2: "q"
+    { assume 3: "p"
+       have 4: "q ⟶ r" using 1 3 by (rule mp)
+       have 5: "r" using 4 2 by (rule mp)}
+    hence "p ⟶ r" by (rule impI)
+  }
+  thus "q ⟶ (p ⟶ r)" by (rule impI)
+qed
+text {* ---------------------------------------------------------------
+  Ejercicio 6. Demostrar
+     p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim cammonagu chrgencar raffergon2 gleherlop giafus1
+   marfruman1 alfmarcua enrparalv pabbergue  antramhur alikan juacanrod
+   hugrubsan *)
+lemma ejercicio_6:
+  assumes 1: "p ⟶ (q ⟶ r)"
+  shows   "(p ⟶ q) ⟶ (p ⟶ r)"
+proof (rule impI)
+  assume 2: "p ⟶ q"
+  show "p ⟶ r"
+  proof (rule impI)
+    assume 3: "p"
+    have 4: "q ⟶ r" using 1 3 by (rule mp)
+     have 5: "q" using 2 3 by (rule mp)
+     show "r" using 4 5 by (rule mp)
    qed
-  moreover note `∄x. P a ⟶ Q x`
+qed
-  ultimately have "¬(P a)" by (rule mt)
-   have "¬(P a) ⟶ (∃x. P a ⟶ Q x)"
+(* benber josgomrom4 *)
-  proof
+lemma ejercicio_6_1:
-    fix x
+  assumes "p ⟶ (q ⟶ r)"
-    assume "¬(P a)"
+  shows   "(p ⟶ q) ⟶ (p ⟶ r)"
-    have "P a ⟶ Q x"
+proof
-    proof
+  assume "p ⟶ q"
-      assume "P a"
+  show "p ⟶ r"
-      with `¬(P a)` have "False" by (rule notE)
+  proof
-      thus "Q x" by (rule FalseE)
+    assume "p"
-     qed
+    with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
-    thus "∃x. P a ⟶ Q x" by (rule exI)
+    moreover from `p ⟶ q` `p` have "q" by (rule mp)
+     ultimately show "r" by (rule mp)
    qed
-   moreover note `∄x. P a ⟶ Q x`
+qed
-   ultimately have "¬¬(P a)" by (rule mt)
-   moreover note `¬(P a)`
+text {* ---------------------------------------------------------------
-   ultimately show "False" by (rule notE)
+   Ejercicio 7. Demostrar
+     p ⊢ q ⟶ p
+   ------------------------------------------------------------------ *}
+(* pabalagon manperjim josgomrom4 raffergon2 giafus1 gleherlop
+   marfruman1 enrparalv pabbergue antramhur alikan hugrubsan *)
+lemma ejercicio_7:
+  assumes 1: "p"
+  shows   "q ⟶ p"
+proof (rule impI)
+   assume 2: "q"
+   show "p" using 1 by this
+qed
+(* benber cammonagu juacanrod chrgencar *)
+lemma ejercicio_7_1:
+  assumes "p"
+  shows   "q ⟶ p"
+proof
+  show "p" using `p` .
 qed
 (* alfmarcua *)
-lemma ejercicio_52:
+lemma ejercicio_7_2:
-   "p ∨ ¬p"
+   assumes "p"
-proof (rule ccontr)
+  shows   "q ⟶ p"
-   assume 1: "¬(p ∨ ¬p)"
+  using assms by (rule impI)
-   have 2: "¬p" proof (rule notI)
-     assume p hence 3: "p ∨ ¬p" by (rule disjI1)
+text {* ---------------------------------------------------------------
-     show "False" using 1 3 by (rule notE)
+  Ejercicio 8. Demostrar
+     ⊢ p ⟶ (q ⟶ p)
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim josgomrom4 raffergon2 giafus1 marfruman1
+   enrparalv pabbergue antramhur alikan hugrubsan *)
+lemma ejercicio_8:
+  "p ⟶ (q ⟶ p)"
+proof (rule impI)
+   assume 1: "p"
+   show "q ⟶ p"
+  proof (rule impI)
+     assume 2: "q"
+     show "p" using 1 by this
    qed
-  have 4: "p ∨ ¬p" using 2 by (rule disjI2)
-  show "False" using 1 4 by (rule notE)
 qed
-lemma ejercicio_1:
+(* benber cammonagu gleherlop chrgencar juacanrod alfmarcua *)
-   assumes "P a ⟶ (∃x. Q x)"
+lemma ejercicio_8_1:
-   shows "∃x. P a ⟶ Q x"
+   "p ⟶ (q ⟶ p)"
-proof (rule disjE)
+   using ejercicio_7_1 by (rule impI)
-  show "P a ∨ ¬ P a" by (rule ejercicio_52)
-next
+text {* ---------------------------------------------------------------
-  assume "P a"
+   Ejercicio 9. Demostrar
-   have "∃x. Q x" using assms `P a` by (rule mp)
+     p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
-   then obtain b where "Q b" by (rule exE)
+   ------------------------------------------------------------------ *}
-   have "P a ⟹ Q b" using `P a` `Q b` by simp
-   have "P a ⟶ Q b" using `P a ⟹ Q b` by (rule impI)
+(* pabalagon manperjim raffergon2 giafus1 marfruman1 alfmarcua enrparalv
-  then show "∃x. P a ⟶ Q x" by (rule exI)
+   gleherlop antramhur alikan hugrubsan *)
-next
+lemma ejercicio_9:
-   assume "¬ P a"
+   assumes 1: "p ⟶ q"
-   fix b
+   shows   "(q ⟶ r) ⟶ (p ⟶ r)"
-  have "P a ⟶ Q b"
+proof (rule impI)
+   assume 2: "q ⟶ r"
+   show "p ⟶ r"
    proof (rule impI)
-     assume "P a"
+     assume 3: "p"
-     with `¬(P a)` have "False" by (rule notE)
+    have 4: "q" using 1 3 by (rule mp)
-     then show "Q b" by (rule FalseE)
+    show "r" using 2 4 by (rule mp)
+  qed
+qed
+(* benber josgomrom4 cammonagu chrgencar juacanrod pabbergue *)
+lemma ejercicio_9_1:
+  assumes "p ⟶ q"
+  shows   "(q ⟶ r) ⟶ (p ⟶ r)"
+proof
+  assume "q ⟶ r"
+  show "p ⟶ r"
+  proof
+    assume "p"
+     with `p ⟶ q` have "q" by (rule mp)
+     with `q ⟶ r` show "r" by (rule mp)
    qed
-  thus "∃x. P a ⟶ Q x" by (rule exI)
 qed
-(* pabalagon manperjim josgomrom4 gleherlop marfruman1 raffergon2 hugrubsan pabbergue enrparalv giafus1 antramhur *)
+text {* ---------------------------------------------------------------
-lemma ejercicio_1:
+  Ejercicio 10. Demostrar
-   assumes "P a ⟶ (∃x. Q x)"
+     p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
-   shows "∃x. P a ⟶ Q x"
+  ------------------------------------------------------------------ *}
-proof (rule disjE)
-   show "¬P a ∨ P a" by (rule excluded_middle)
+(* pabalagon manperjim raffergon2 marfruman1 gleherlop alfmarcua
-next
+   enrparalv pabbergue antramhur alikan juacanrod hugrubsan *)
-  fix b
+lemma ejercicio_10:
-  assume 3: "¬P a"
+   assumes 1: "p ⟶ (q ⟶ (r ⟶ s))"
-  have "P a ⟶ Q b" proof (rule impI)
+   shows   "r ⟶ (q ⟶ (p ⟶ s))"
-    assume 4: "P a" show "Q b" using 3 4 by (rule notE)
+proof (rule impI)
+  assume 2: "r"
+   show "q ⟶ (p ⟶ s)"
+  proof (rule impI)
+    assume 3: "q"
+    show "p ⟶ s"
+    proof (rule impI)
+      assume 4: "p"
+      have 5: "q ⟶ (r ⟶ s)" using 1 4 by (rule mp)
+      have 6: "r ⟶ s" using 5 3 by (rule mp)
+      show "s" using 6 2 by (rule mp)
+    qed
    qed
-   thus ?thesis by (rule exI)
+qed
-next
-   assume 1: "P a"
+(* benber josgomrom4 cammonagu chrgencar giafus1 *)
-   have "∃x. Q x" using assms(1) 1 by (rule mp)
+lemma ejercicio_10_1:
-  then obtain b where 2: "Q b" by (rule exE)
+  assumes "p ⟶ (q ⟶ (r ⟶ s))"
-  have "P a ⟶ Q b" proof (rule impI)
+  shows   "r ⟶ (q ⟶ (p ⟶ s))"
-     assume "P a" show "Q b" using 2 .
+proof
+   assume "r"
+   show "q ⟶ (p ⟶ s)"
+  proof
+    assume "q"
+    show "p ⟶ s"
+    proof
+      assume "p"
+      with `p ⟶ (q ⟶ (r ⟶ s))`
+        have "q ⟶ (r ⟶ s)" by (rule mp)
+      hence "r ⟶ s" using `q` by (rule mp)
+      thus "s" using `r` by (rule mp)
+     qed
    qed
-  thus ?thesis by (rule exI)
 qed
 text {* ---------------------------------------------------------------
-   Ejercicio 2. Demostrar
+   Ejercicio 11. Demostrar
-       {∀x y z. R x y ∧ R y z ⟶ R x z,
+     ⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
-        ∀x. ¬(R x x)}
-       ⊢ ∀x y. R x y ⟶ ¬(R y x)
    ------------------------------------------------------------------ *}
-(* benber *)
+(* pabalagon manperjim josgomrom4 gleherlop cammonagu giafus1 alfmarcua
-lemma
+   chrgencar pabbergue alikan juacanrod hugrubsan *)
-   assumes A1: "∀x y z. R x y ∧ R y z ⟶ R x z"
+lemma ejercicio_11:
-    and A2: "∀x. ¬(R x x)"
+   "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
-  shows "∀x y. R x y ⟶ ¬(R y x)"
+proof (rule impI)
-proof -
+  assume 1: "p ⟶ (q ⟶ r)"
-  {
+  show "(p ⟶ q) ⟶ (p ⟶ r)" using 1 ejercicio_6 by simp
-    fix x y
+qed
-    {
-      assume "R x y"
-      have "¬ (R y x)"
-      proof (rule ccontr)
-        assume "¬ ¬ (R y x)"
-        hence "R y x" by (rule notnotD)
-        note `∀x y z. R x y ∧ R y z ⟶ R x z`
+(* pabalagon raffergon2 marfruman1 enrparalv antramhur *)
-        moreover have "∀ y z. R x y ∧ R y z ⟶ R x z ⟹ False"
+lemma ejercicio_11_2:
-        proof -
+  "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
-          assume "∀ y z. R x y ∧ R y z ⟶ R x z"
+proof (rule impI)
-          moreover have "∀ z. R x y ∧ R y z ⟶ R x z ⟹ False"
+  assume 1: "p ⟶ (q ⟶ r)"
-          proof -
+  show "(p ⟶ q) ⟶ (p ⟶ r)"
-            assume "∀ z. R x y ∧ R y z ⟶ R x z"
+  proof (rule impI)
-            moreover have "R x y ∧ R y x ⟶ R x x ⟹ False"
+    assume 2: "p ⟶ q"
-            proof -
+    show "p ⟶ r"
-              assume "R x y ∧ R y x ⟶ R x x"
+    proof (rule impI)
-              moreover {
+      assume 3: "p"
-                note `R x y`
+      have 4: "q ⟶ r" using 1 3 by (rule mp)
-                moreover note `R y x`
+       have 5: "q" using 2 3 by (rule mp)
-                ultimately have "R x y ∧ R y x" by (rule conjI)
+      show "r" using 4 5 by (rule mp)
-              }
+    qed
-              ultimately have "R x x" by (rule mp)
+   qed
-              note `∀x. ¬(R x x)`
-              moreover {
-                assume "¬(R x x)"
-                moreover note `R x x`
-                ultimately have "False" by (rule notE)
-              }
-              ultimately show "False" by (rule allE)
-            qed
-            ultimately show "False" by (rule allE)
-          qed
-          ultimately show "False" by (rule allE)
-        qed
-        ultimately show "False" by (rule allE)
-       qed
-    }
-    hence "R x y ⟶ ¬ (R y x)" by (rule impI)
-  }
-  hence "⋀x. ∀y. R x y ⟶ ¬ (R y x)" by (rule allI)
-   thus ?thesis by (rule allI)
 qed
-(* alfmarcua marfruman1 enrparalv*)
+(* benber *)
-lemma ejercicio_2:
+lemma ejercicio_11_1:
-   assumes "∀x y z. R x y ∧ R y z ⟶ R x z"
+   "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
-          "∀x. ¬(R x x)"
+proof
-        shows "∀x y. R x y ⟶ ¬(R y x)"
+  assume "p ⟶ (q ⟶ r)"
-proof (rule allI)
+   show "(p ⟶ q) ⟶ (p ⟶ r)"
-  fix a
+   proof
-   show "∀y. R a y ⟶ ¬ R y a"
+     assume "p ⟶ q"
-   proof (rule allI, rule impI)
+     show "p ⟶ r"
-    fix b
+     proof
-     assume "R a b"
+       assume p
-     show "¬ R b a"
+       with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
-     proof (rule notI)
+       moreover have "q" using `p ⟶ q` `p` by (rule mp)
-       assume "R b a"
+       ultimately show r by (rule mp)
-       have "R a b ∧ R b a" using `R a b` `R b a` by (rule conjI)
-      have "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1) by (rule allE)
-      then have "∀z. R a b ∧ R b z ⟶ R a z" by (rule allE)
-      then have "R a b ∧ R b a ⟶ R a a" by (rule allE)
-       then have "R a a" using `R a b ∧ R b a` by (rule mp)
-       have "¬ (R a a)" using assms(2) by (rule allE)
-      then show False using `R a a` by (rule notE)
      qed
    qed
 qed
+text {* ---------------------------------------------------------------
+  Ejercicio 12. Demostrar
+     (p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
+  ------------------------------------------------------------------ *}
-(* pabalagon manperjim josgomrom4 gleherlop raffergon2 hugrubsan pabbergue giafus1 antramhur *)
+(* pabalagon manperjim raffergon2 marfruman1 gleherlop enrparalv
-lemma ejercicio_2:
+   pabbergue antramhur alikan juacanrod hugrubsan *)
-   assumes "∀x y z. R x y ∧ R y z ⟶ R x z"
+lemma ejercicio_12:
-          "∀x. ¬(R x x)"
+   assumes 1: "(p ⟶ q) ⟶ r"
-   shows "∀x y. R x y ⟶ ¬(R y x)"
+   shows   "p ⟶ (q ⟶ r)"
-proof (rule allI)
+proof (rule impI)
-   fix a
+   assume 2: "p"
-   show "∀y. R a y ⟶ ¬(R y a)"
+   show "q ⟶ r"
-   proof (rule allI)
+   proof (rule impI)
-     fix b
+     assume 3: "q"
-    have "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1) by (rule allE)
+     have 4: "p ⟶ q"
-    hence "∀z. R a b ∧ R b z ⟶ R a z" by (rule allE)
+     proof (rule impI)
-    hence 1: "R a b ∧ R b a ⟶ R a a" by (rule allE)
+       assume 5: "p"
-     have 2: "¬(R a a)" using assms(2) by (rule allE)
+       show "q" using 3 by this
-     show "R a b ⟶ ¬(R b a)" proof (rule impI)
-       assume 3: "R a b"
-       show "¬(R b a)"
-      proof (rule ccontr)
-        assume "¬¬R b a"
-        hence 4: "R b a" by (rule notnotD)
-        have 5: "R a b ∧ R b a" using 3 4 by (rule conjI)
-        have 6: "R a a" using 1 5 by (rule mp)
-        show False using 2 6 by (rule notE)
-      qed
      qed
+    show "r" using 1 4 by (rule mp)
    qed
 qed
+(* benber  josgomrom4 cammonagu giafus1 alfmarcua chrgencar *)
+lemma ejercicio_12_1:
+  assumes "(p ⟶ q) ⟶ r"
+  shows   "p ⟶ (q ⟶ r)"
+proof
+  assume "p"
+  show "q ⟶ r"
+  proof
+    assume "q"
+    hence "p ⟶ q" by (rule impI)
+    with `(p ⟶ q) ⟶ r` show "r" by (rule mp)
+  qed
+qed
+section {* Conjunciones *}
+text {* ---------------------------------------------------------------
+  Ejercicio 13. Demostrar
+     p, q ⊢  p ∧ q
+  ------------------------------------------------------------------ *}
 (* pabalagon *)
-lemma ejercicio_2_2:
+lemma ejercicio_13:
-   assumes "∀x y z. R x y ∧ R y z ⟶ R x z"
+   assumes "p"
-          "∀x. ¬(R x x)"
+          "q"
-   shows "∀x y. R x y ⟶ ¬(R y x)"
+  shows "p ∧ q"
+using assms(1, 2) by (rule conjI)
+(* benber manperjim josgomrom4 cammonagu raffergon2 marfruman1 alfmarcua
+   enrparalv chrgencar gleherlop pabbergue antramhur juacanrod hugrubsan
+   alikan *)
+lemma ejercicio_13_1:
+  assumes "p"
+          "q"
+  shows "p ∧ q"
+  using assms by (rule conjI)
+text {* ---------------------------------------------------------------
+  Ejercicio 14. Demostrar
+     p ∧ q ⊢ p
+  ------------------------------------------------------------------ *}
+(* pabalagon  josgomrom4 *)
+lemma ejercicio_14:
+  assumes "p ∧ q"
+  shows   "p"
+  using assms(1) by (rule conjunct1)
+(* benber manperjim cammonagu raffergon2 marfruman1 alfmarcua enrparalv
+   chrgencar pabbergue gleherlop antramhur hugrubsan juacanrod alikan *)
+lemma ejercicio_14_1:
+  assumes "p ∧ q"
+  shows   "p"
+  using assms by (rule conjunct1)
+text {* ---------------------------------------------------------------
+  Ejercicio 15. Demostrar
+     p ∧ q ⊢ q
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim juacanrod josgomrom4 *)
+lemma ejercicio_15:
+  assumes "p ∧ q"
+   shows   "q"
+  using assms(1) by (rule conjunct2)
+(* benber cammonagu raffergon2 marfruman1 alfmarcua enrparalv chrgencar
+   pabbergue antramhur gleherlop hugrubsan alikan *)
+lemma ejercicio_15_1:
+  assumes "p ∧ q"
+  shows   "q"
+  using assms by (rule conjunct2)
+text {* ---------------------------------------------------------------
+  Ejercicio 16. Demostrar
+     p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
+   cammmonagu enrparalv chrgencar gleherlop pabbergue antramhur
+   hugrubsan alikan juacanrod cammonagu *)
+lemma ejercicio_16:
+  assumes "p ∧ (q ∧ r)"
+  shows   "(p ∧ q) ∧ r"
 proof -
-   { fix a
+   have 1: "p" using assms(1) by (rule conjunct1)
-    { fix b
+  have 2: "q ∧ r" using assms(1) by (rule conjunct2)
-      have "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1) by (rule allE)
+  have 3: "q" using 2 by (rule conjunct1)
-      hence "∀z. R a b ∧ R b z ⟶ R a z" by (rule allE)
+  have 4: "r" using 2 by (rule conjunct2)
-      hence 1: "R a b ∧ R b a ⟶ R a a" by (rule allE)
+  have 5: "p ∧ q" using 1 3 by (rule conjI)
-      have 2: "¬(R a a)" using assms(2) by (rule allE)
+  show "(p ∧ q) ∧ r" using 5 4 by (rule conjI)
-      have "R a b ⟶ ¬(R b a)" proof (rule impI)
+qed
-        assume 3: "R a b"
-        show "¬(R b a)"
+(* benber *)
-        proof (rule ccontr)
+lemma ejercicio_16_1:
-          assume "¬¬R b a"
+  assumes "p ∧ (q ∧ r)"
-          hence 4: "R b a" by (rule notnotD)
+  shows   "(p ∧ q) ∧ r"
-          have 5: "R a b ∧ R b a" using 3 4 by (rule conjI)
+proof - (* TODO? *)
-          have 6: "R a a" using 1 5 by (rule mp)
+  have "q ∧ r" using assms by (rule conjunct2)
-          show False using 2 6 by (rule notE)
+  have "p" using assms by (rule conjunct1)
-        qed
+  moreover have "q" using `q ∧ r` by (rule conjunct1)
-      qed}
+  ultimately have "p ∧ q" by (rule conjI)
-    hence "∀y. R a y ⟶ ¬(R y a)" by (rule allI)}
+  moreover have "r" using `q ∧ r` by (rule conjunct2)
-   thus "∀x y. R x y ⟶ ¬(R y x)" by (rule allI)
+  ultimately show "(p ∧ q) ∧ r" by (rule conjI)
+qed
+text {* ---------------------------------------------------------------
+  Ejercicio 17. Demostrar
+     (p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
+   cammonagu chrgencar gleherlop pabbergue antramhur enrparalv hugrubsan
+   juacanrod alikan *)
+lemma ejercicio_17:
+  assumes 1: "(p ∧ q) ∧ r"
+  shows   "p ∧ (q ∧ r)"
+proof -
+  have 2: "r" using 1 by (rule conjunct2)
+  have 3: "p ∧ q" using 1 by (rule conjunct1)
+  have 4: "p" using 3 by (rule conjunct1)
+  have 5: "q" using 3 by (rule conjunct2)
+  have 6: "q ∧ r" using 5 2 by (rule conjI)
+  show ?thesis using 4 6 by (rule conjI)
+qed
+(* benber *)
+lemma ejercicio_17_1:
+  assumes "(p ∧ q) ∧ r"
+  shows   "p ∧ (q ∧ r)"
+proof -
+  have "p ∧ q" using assms by (rule conjunct1)
+  have "p" using `p ∧ q` by (rule conjunct1)
+   moreover have "q ∧ r"
+  proof (rule conjI)
+    show "q" using `p ∧ q` by (rule conjunct2)
+  next
+    show "r" using assms by (rule conjunct2)
+  qed
+  ultimately show ?thesis by (rule conjI)
 qed
 text {* ---------------------------------------------------------------
-   Ejercicio 3. Demostrar o refutar
+   Ejercicio 18. Demostrar
-       (∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)
+     p ∧ q ⊢ p ⟶ q
    ------------------------------------------------------------------ *}
-(* benber pabbergue*)
+(* pabalagon raffergon2 marfruman1 juacanrod alikan*)
-(* No es cierto si el universo consiste en más que un objeto. En ese caso, asignar la igualdad (=) a P
+lemma ejercicio_18:
-   es un contraejemplo. *)
+  assumes "p ∧ q"
+  shows   "p ⟶ q"
+proof (rule impI)
+  assume "p"
+  show "q" using assms(1) by (rule conjunct2)
+qed
+(* benber manperjim josgomrom4 cammonagu alfmarcua chrgencar pabbergue
+   gleherlop antramhur enrparalv hugrubsan *)
+lemma ejercicio_18_1:
+  assumes "p ∧ q"
+  shows   "p ⟶ q"
+proof
+  show "q" using assms by (rule conjunct2)
+qed
+text {* ---------------------------------------------------------------
+  Ejercicio 19. Demostrar
+     (p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r
+   ------------------------------------------------------------------ *}
-(* alfmarcua marfruman1 raffergon2 enrparalv*)
+(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
-lemma ejercicio_3:
+   cammonagu chrgencar gleherlop pabbergue antramhur enrparalv juacanrod
-   "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
+   hugrubsan alikan *)
-   quickcheck
+lemma ejercicio_19:
-   oops
+   assumes 1: "(p ⟶ q) ∧ (p ⟶ r)"
+  shows   "p ⟶ q ∧ r"
+proof (rule impI)
+  assume 2: "p"
+   have 3: "p ⟶ q" using 1 by (rule conjunct1)
+   have 4: "p ⟶ r" using 1 by (rule conjunct2)
+  have 5: "q" using 3 2 by (rule mp)
+  have 6: "r" using 4 2 by (rule mp)
+  show "q ∧ r" using 5 6 by (rule conjI)
+qed
-(* pabalagon manperjim pabbergue josgomrom4 gleherlop hugrubsan giafus1 antramhur *)
+(* benber cammonagu *)
-text{*
+lemma ejercicio_19_1:
-Contraejemplo en los naturales, para todo x existe y tal que x < y, pero no
+  assumes "(p ⟶ q) ∧ (p ⟶ r)"
-existe y tal que para todo x, x < y
+  shows   "p ⟶ q ∧ r"
-*}
+proof
-lemma ejercicio_3: "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
+  assume p
-   quickcheck
+  show "q ∧ r"
-  oops
+  proof
+    have "p ⟶ q" using assms by (rule conjunct1)
+    thus "q" using `p` by (rule mp)
+  next
+    have "p ⟶ r" using assms by (rule conjunct2)
+    thus "r" using `p` by (rule mp)
+   qed
+qed
 text {* ---------------------------------------------------------------
-   Ejercicio 4. Demostrar o refutar
+   Ejercicio 20. Demostrar
-       (∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)
+     p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
    ------------------------------------------------------------------ *}
+(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
+   cammonagu chrgencar gleherlop pabbergue antramhur enrparalv juacanrod
+   hugrubsan alikan *)
+lemma ejercicio_20:
+  assumes 1: "p ⟶ q ∧ r"
+  shows   "(p ⟶ q) ∧ (p ⟶ r)"
+proof (rule conjI)
+  show "p ⟶ q"
+  proof (rule impI)
+    assume 2: "p"
+    have 3: "q ∧ r" using 1 2 by (rule mp)
+    show 4: "q" using 3 by (rule conjunct1)
+  qed
+  show "p ⟶ r"
+  proof (rule impI)
+    assume 2: "p"
+    have 3: "q ∧ r" using 1 2 by (rule mp)
+    show 4: "r" using 3 by (rule conjunct2)
+  qed
+qed
 (* benber *)
-lemma "(∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)"
+lemma ejercicio_20_1:
+  assumes "p ⟶ q ∧ r"
+  shows   "(p ⟶ q) ∧ (p ⟶ r)"
 proof
-   assume "∃y. ∀x. P x y"
+   show "p ⟶ q"
-  moreover have "⋀y. ∀x. P x y ⟹ ∀x. ∃y'. P x y'"
    proof
-     fix x y
+     assume "p"
-     assume "∀x'. P x' y"
+    with assms have "q ∧ r" by (rule mp)
-     hence "P x y" by (rule allE)
+    thus "q" by (rule conjunct1)
-     thus "∃y'. P x y'" by (rule exI)
+  qed
+next
+  show "p ⟶ r"
+  proof
+     assume "p"
+     with assms have "q ∧ r" by (rule mp)
+     thus "r" by (rule conjunct2)
    qed
-  ultimately show "∀x. ∃y. P x y" by (rule exE)
 qed
-(* alfmarcua marfruman1 raffergon2 enrparalv *)
+text {* ---------------------------------------------------------------
-lemma ejercicio_4:
+  Ejercicio 21. Demostrar
-   "(∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)"
+     p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r
-proof (rule impI, rule allI)
+  ------------------------------------------------------------------ *}
-   fix a
-   assume "∃y. ∀x. P x y"
+(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
-   then obtain b where "∀x. P x b" by (rule exE)
+   cammonagu chrgencar pabbergue gleherlop antramhur enrparalv juacanrod
-   then have "P a b" by (rule allE)
+   hugrubsan alikan *)
-   then show "∃y. P a y" by (rule exI)
+lemma ejercicio_21:
+   assumes 1: "p ⟶ (q ⟶ r)"
+  shows   "p ∧ q ⟶ r"
+proof (rule impI)
+  assume 2: "p ∧ q"
+  have 3: "p" using 2 by (rule conjunct1)
+  have 4: "q ⟶ r" using 1 3 by (rule mp)
+  have 5: "q" using 2 by (rule conjunct2)
+  show "r" using 4 5 by (rule mp)
+qed
+(* benber *)
+lemma ejercicio_21_1:
+   assumes "p ⟶ (q ⟶ r)"
+  shows   "p ∧ q ⟶ r"
+proof
+   assume "p ∧ q"
+  hence "p" by (rule conjunct1)
+   with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
+   moreover from `p ∧ q` have "q" by (rule conjunct2)
+   ultimately show "r" by (rule mp)
 qed
-(* pabalagon manperjim josgomrom4 gleherlop hugrubsan pabbergue antramhur *)
+text {* ---------------------------------------------------------------
-lemma ejercicio_4: "(∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)"
+  Ejercicio 22. Demostrar
+     p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
+   chrgencar pabbergue gleherlop antramhur enrparalv juacanrod hugrubsan
+   alikan *)
+lemma ejercicio_22:
+  assumes 1: "p ∧ q ⟶ r"
+  shows   "p ⟶ (q ⟶ r)"
 proof (rule impI)
-   assume "∃y. ∀x. P x y"
+   assume 2: "p"
-   moreover have "⋀y. ∀x. P x y ⟹ ∀x. ∃y. P x y"
+   show "q ⟶ r"
+  proof (rule impI)
+    assume 3: "q"
+    have 4: "p ∧ q" using 2 3 by (rule conjI)
+    show "r" using 1 4 by (rule mp)
+  qed
+qed
+(* benber cammonagu *)
+lemma ejercicio_22_1:
+  assumes "p ∧ q ⟶ r"
+  shows   "p ⟶ (q ⟶ r)"
+proof
+  assume "p"
+  show "q ⟶ r"
    proof
-    fix x0 y0
+     assume "q"
-     assume "∀x. P x y0"
+     with `p` have "p ∧ q" by (rule conjI)
-     hence "P x0 y0" by (rule allE)
+     with `p ∧ q ⟶ r` show "r" by (rule mp)
-     thus "∃y. P x0 y" by (rule exI)
    qed
-  ultimately show "∀x. ∃y. P x y" by (rule exE)
 qed
 text {* ---------------------------------------------------------------
-   Ejercicio 5. Demostrar o refutar
+   Ejercicio 23. Demostrar
-      {∀x. P a x x,
+      (p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
-      ∀x y z. P x y z ⟶ P (f x) y (f z)⟧
-     ⊢ ∃z. P (f a) z (f (f a))
    ------------------------------------------------------------------ *}
+(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
+   chrgencar pabbergue gleherlop antramhur enrparalv juacanrod hugrubsan
+   alikan *)
+lemma ejercicio_23:
+  assumes 1: "(p ⟶ q) ⟶ r"
+  shows   "p ∧ q ⟶ r"
+proof (rule impI)
+  assume 2: "p ∧ q"
+  have 3: "p ⟶ q"
+  proof (rule impI)
+    assume "p"
+    show "q" using 2 by (rule conjunct2)
+  qed
+  show "r" using 1 3 by (rule mp)
+qed
+(* benber cammonagu *)
+lemma ejercicio_23_1:
+  assumes "(p ⟶ q) ⟶ r"
+  shows   "p ∧ q ⟶ r"
+proof
+  assume "p ∧ q"
+  hence "q" by (rule conjunct2)
+  hence "p ⟶ q" by (rule impI)
+  with `(p ⟶ q) ⟶ r` show "r" by (rule mp)
+qed
+text {* ---------------------------------------------------------------
+  Ejercicio 24. Demostrar
+     p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
+   chrgencar pabbergue gleherlop antramhur enrparalv hugrubsan juacanrod
+   cammonagu alikan *)
+lemma ejercicio_24:
+  assumes 1: "p ∧ (q ⟶ r)"
+  shows   "(p ⟶ q) ⟶ r"
+proof (rule impI)
+  assume 2: "p ⟶ q"
+  have 3: "p" using 1 by (rule conjunct1)
+  have 4: "q ⟶ r" using 1 by (rule conjunct2)
+  have 5: "q" using 2 3 by (rule mp)
+  show 6: "r" using 4 5 by (rule mp)
+qed
 (* benber *)
-lemma
+lemma ejercicio_24_1:
-   assumes A1: "∀ x. P a x x"
+   assumes "p ∧ (q ⟶ r)"
-    and A2: "∀x y z. P x y z ⟶ P (f x) y (f z)"
+   shows   "(p ⟶ q) ⟶ r"
-   shows "∃z. P (f a) z (f (f a))"
 proof
-  from A2
+   have "q ⟶ r" using assms by (rule conjunct2)
-   have "∀y z. P a y z ⟶ P (f a) y (f z)" by (rule allE)
+   assume "p ⟶ q"
-   hence "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" by (rule allE)
+   moreover have "p" using assms by (rule conjunct1)
-   hence "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" by (rule allE)
+   ultimately have "q" by (rule mp)
-   moreover have "P a (f a) (f a)" using A1 by (rule allE)
+   with `q ⟶ r` show r by (rule mp)
-   ultimately show "P (f a) (f a) (f (f a))" by (rule mp)
 qed
-(* alfmarcua enrparalv *)
+section {* Disyunciones *}
-lemma ejercicio_5:
-   assumes "∀x. P a x x"
+text {* ---------------------------------------------------------------
-          "∀x y z. P x y z ⟶ P (f x) y (f z)"
+  Ejercicio 25. Demostrar
-        shows "∃z. P (f a) z (f (f a))"
+     p ⊢ p ∨ q
-proof (rule exI, rule mp)
+  ------------------------------------------------------------------ *}
-   show "P a (f a) (f a)" using assms(1) by (rule allE)
+(* pabalagon manperjim josgomrom4 benber cammonagu raffergon2 marfruman1
+   alfmarcua chrgencar gleherlop pabbergue antramhur enrparalv juacanrod
+   hugrubsan alikan *)
+lemma ejercicio_25:
+   assumes "p"
+  shows   "p ∨ q"
+  using assms(1) by (rule disjI1)
+text {* ---------------------------------------------------------------
+  Ejercicio 26. Demostrar
+     q ⊢ p ∨ q
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim josgomrom4 benber cammonagu marfruman1 alfmarcua
+   chrgencar pabbergue gleherlop antramhur enrparalv juacanrod hugrubsan
+   alikan *)
+lemma ejercicio_26:
+  assumes "q"
+  shows   "p ∨ q"
+  using assms(1) by (rule disjI2)
+text {* ---------------------------------------------------------------
+  Ejercicio 27. Demostrar
+     p ∨ q ⊢ q ∨ p
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 chrgencar
+   pabbergue antramhur enrparalv juacanrod hugrubsan cammonagu alikan *)
+lemma ejercicio_27:
+  assumes 1: "p ∨ q"
+  shows   "q ∨ p"
+using 1 proof (rule disjE)
+   assume 2: "p" thus "q ∨ p" by (rule disjI2)
 next
-   have "∀y z. P a y z ⟶ P (f a) y (f z)" using assms(2) by (rule allE)
+   assume 3: "q" thus "q ∨ p" by (rule disjI1)
-  then have "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" by (rule allE)
-  then show "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" by (rule allE)
 qed
-(* pabalagon manperjim josgomrom4 gleherlop marfruman1 raffergon2 hugrubsan pabbergue giafus1 antramhur *)
+(* benber alfmarcua gleherlop *)
-lemma ejercicio_5:
+lemma ejercicio_27_1:
-   assumes "∀x. P a x x"
+   assumes "p ∨ q"
-          "∀x y z. P x y z ⟶ P (f x) y (f z)"
+   shows   "q ∨ p"
-   shows "∃z. P (f a) z (f (f a))"
+proof -
-proof (rule exI)
+   have "p ∨ q" using assms .
-   have "∀y z. P a y z ⟶ P (f a) y (f z)" using assms(2) ..
+   moreover have "p ⟹ q ∨ p" by (rule disjI2)
-   hence "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" ..
+   moreover have "q ⟹ q ∨ p" by (rule disjI1)
-  hence "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" ..
+   ultimately show "q ∨ p" by (rule disjE)
-   moreover have "P a (f a) (f a)" using assms(1) by (rule allE)
-   ultimately show "P (f a) (f a) (f (f a))" by (rule mp)
 qed
 text {* ---------------------------------------------------------------
-   Ejercicio 6. Demostrar o refutar
+   Ejercicio 28. Demostrar
-      {∀y. Q a y,
+      q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
-      ∀x y. Q x y ⟶ Q (s x) (s y)}
-     ⊢ ∃z. Qa z ∧ Q z (s (s a))
    ------------------------------------------------------------------ *}
-(* benber alfmarcua giafus1 *)
+(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 chrgencar
-lemma
+   gleherlop alfmarcua pabbergue antramhur enrparalv juacanrod hugrubsan
-   assumes "∀y. Q a y"
+   cammonagu alikan *)
-      and "∀x y. Q x y ⟶ Q (s x) (s y)"
+lemma ejercicio_28:
-     shows "∃z. Q a z ∧ Q z (s (s a))"
+   assumes 1: "q ⟶ r"
+  shows   "p ∨ q ⟶ p ∨ r"
+proof (rule impI)
+  assume 2: "p ∨ q" show "p ∨ r" using 2
+  proof (rule disjE)
+    assume 3: p thus "p ∨ r" by (rule disjI1)
+  next
+    assume 4: q have r using 1 4 by (rule mp)
+     thus "p ∨ r" by (rule disjI2)
+  qed
+qed
+(* benber *)
+lemma ejercicio_28_1:
+  assumes "q ⟶ r"
+  shows   "p ∨ q ⟶ p ∨ r"
 proof
-   have "Q a a" using `∀y. Q a y` by (rule allE)
+   assume "p ∨ q"
-   moreover have "Q a (s (s a))" using `∀y. Q a y` by (rule allE)
+  moreover have "p ⟹ p ∨ r" by (rule disjI1)
-   ultimately show "Q a a ∧ Q a (s (s a))" by (rule conjI)
+   moreover have "q ⟹ p ∨ r"
+  proof (rule disjI2)
+    assume "q"
+    with `q ⟶ r` show "r" by (rule mp)
+  qed
+   ultimately show "p ∨ r" by (rule disjE)
 qed
-(* pabalagon manperjim josgomrom4 gleherlop marfruman1 raffergon2 hugrubsan pabbergue enrparalv antramhur *)
+text {* ---------------------------------------------------------------
-lemma ejercicio_6:
+  Ejercicio 29. Demostrar
-   assumes "∀y. Q a y"
+     p ∨ p ⊢ p
-          "∀x y. Q x y ⟶ Q (s x) (s y)"
+  ------------------------------------------------------------------ *}
-   shows "∃z. Q a z ∧ Q z (s (s a))"
-proof (rule exI)
+(* pabalagon juacanrod marfruman1 *)
-   have "∀y. Q a y ⟶ Q (s a) (s y)" using assms(2) by (rule allE)
+lemma ejercicio_29:
-  hence "Q a (s a) ⟶ Q (s a) (s (s a))" by (rule allE)
+   assumes 1: "p ∨ p"
-  moreover have "Q a (s a)" using assms(1) by (rule allE)
+   shows   "p"
-   ultimately have "Q (s a) (s (s a))" by (rule mp)
+using 1 proof (rule disjE)
-  with `Q a (s a)` show "Q a (s a) ∧ Q (s a) (s (s a))" by (rule conjI)
+   assume "p" thus "p" .
+next
+   assume "p" thus "p" .
 qed
+(* benber manperjim cammonagu josgomrom4 raffergon2 chrgencar alfmarcua
+   gleherlop pabbergue antramhur enrparalv hugrubsan alikan *)
+lemma ejercicio_29_1:
+  assumes "p ∨ p"
+  shows   "p"
+  using assms by (rule disjE)
 text {* ---------------------------------------------------------------
-   Ejercicio 7. (En APLI2 el ejercicio 13 de LP) Formalizar, y demostrar
+   Ejercicio 30. Demostrar
-  la corrección, del siguiente argumento
+      p ⊢ p ∨ p
-     Si la válvula está abierta o la monitorización está preparada,
-     entonces se envía una señal de reconocimiento y un mensaje de
-     funcionamiento al controlador del ordenador. Si se envía un mensaje
-     de funcionamiento al controlador del ordenador o el sistema está en
-     estado normal, entonces se aceptan las órdenes del operador. Por lo
-     tanto, si la válvula está abierta, entonces se aceptan las órdenes
-      del operador.
-  Usar A : La válvula está abierta.
-       P : La monitorización está preparada.
-       R : Envía una señal de reconocimiento.
-       F : Envía un mensaje de funcionamiento.
-       N : El sistema está en estado normal.
-       Or : Se aceptan órdenes del operador.
    ------------------------------------------------------------------ *}
-(* benber manperjim alfmarcua pabalagon marfruman1 josgomrom4 gleherlop raffergon2 hugrubsan pabbergue enrparalv giafus1
+(* pabalagon manperjim  benber josgomrom4 raffergon2 marfruman1
- antramhur *)
+   chrgencar alfmarcua pabbergue gleherlop antramhur enrparalv hugrubsan
-lemma
+   juacanrod cammonagu alikan *)
-   assumes "A ∨ P ⟶ R ∧ F"
+lemma ejercicio_30:
-     and "F ∨ N ⟶ Or"
+  assumes "p"
-   shows "A ⟶ Or"
+  shows   "p ∨ p"
-proof
+  using assms(1) by (rule disjI1)
-   assume "A"
-  hence "A ∨ P" by (rule disjI1)
+text {* ---------------------------------------------------------------
-   with `A ∨ P ⟶ R ∧ F` have "R ∧ F" by (rule mp)
+  Ejercicio 31. Demostrar
-  hence "F" by (rule conjunct2)
+     p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
-  hence "F ∨ N" by (rule disjI1)
+  ------------------------------------------------------------------ *}
-   with `F ∨ N ⟶ Or` show "Or" by (rule mp)
+(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua pabbergue
+   gleherlop antramhur enrparalv juacanrod hugrubsan alikan *)
+lemma ejercicio_31:
+   assumes 1: "p ∨ (q ∨ r)"
+  shows   "(p ∨ q) ∨ r" (is "?R")
+using 1 proof (rule disjE)
+  assume "p" hence "p ∨ q" by (rule disjI1)
+  thus ?R by (rule disjI1)
+next
+  assume "q ∨ r" thus ?R
+  proof (rule disjE)
+    assume "q" hence "p ∨ q" by (rule disjI2)
+     thus "(p ∨ q) ∨ r" by (rule disjI1)
+  next
+    assume "r" thus ?thesis by (rule disjI2)
+  qed
+qed
+(* benber cammonagu *)
+lemma ejercicio_31_1:
+  assumes "p ∨ (q ∨ r)"
+   shows   "(p ∨ q) ∨ r"
+proof -
+  have "p ∨ (q ∨ r)" using assms .
+   moreover {
+    assume "p"
+    hence "p ∨ q" by (rule disjI1)
+    hence "(p ∨ q) ∨ r" by (rule disjI1)
+   }
+  moreover {
+    assume "q ∨ r"
+    moreover {
+      assume "q"
+      hence "p ∨ q" by (rule disjI2)
+      hence "(p ∨ q) ∨ r" by (rule disjI1)
+    }
+    moreover {
+      assume "r"
+      hence "(p ∨ q) ∨ r" by (rule disjI2)
+    }
+    ultimately have "(p ∨ q) ∨ r" by (rule disjE)
+   }
+  ultimately show "(p ∨ q) ∨ r" by (rule disjE)
 qed
 text {* ---------------------------------------------------------------
-   Ejercicio 8. (En APLI2 el ejercicio 5 de LP) Formalizar, y demostrar
+   Ejercicio 32. Demostrar
-  la corrección, del siguiente argumento
+     (p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
-     En cierto experimento, cuando hemos empleado un fármaco A, el
-     paciente ha mejorado considerablemente en el caso, y sólo en el
-     caso, en que no se haya empleado también un fármaco B. Además, o se
-     ha empleado el fármaco A o se ha empleado el fármaco B. En
-     consecuencia, podemos afirmar que si no hemos empleado el fármaco
-     B, el paciente ha mejorado considerablemente.
-  Usar A: Hemos empleado el fármaco A.
-       B: Hemos empleado el fármaco B.
-       M: El paciente ha mejorado notablemente.
    ------------------------------------------------------------------ *}
-(* benber *)
+(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop
-lemma
+   pabbergue antramhur enrparalv juacanrod hugrubsan alikan *)
-   assumes "A ⟶ (M ⟷ ¬B)"
+lemma ejercicio_32:
-    and "A ∨ B"
+   assumes 1: "(p ∨ q) ∨ r"
-   shows "¬B ⟶ M"
+  shows   "p ∨ (q ∨ r)"
-proof
+using 1 proof (rule disjE)
-   assume "¬B"
+   assume "p ∨ q" thus ?thesis
-   note `A ∨ B`
+  proof (rule disjE)
+    assume p thus ?thesis by (rule disjI1)
+  next
+    assume q hence "q ∨ r" by (rule disjI1)
+    thus ?thesis by (rule disjI2)
+  qed
+next
+   assume r hence "q ∨ r" by (rule disjI2)
+  thus ?thesis by (rule disjI2)
+qed
+(* benber cammonagu *)
+lemma ejercicio_32_1:
+   assumes "(p ∨ q) ∨ r"
+  shows   "p ∨ (q ∨ r)"
+proof -
+  have "(p ∨ q) ∨ r" using assms .
    moreover {
-     assume "A"
+     assume "p ∨ q"
-     with `A ⟶ (M ⟷ ¬B)` have "M ⟷ ¬B" by (rule mp)
+     moreover {
-     hence "¬B ⟹ M" by (rule iffD2)
+      assume "p"
-     hence "M" using `¬B` .
+      hence ?thesis by (rule disjI1)
+     }
+    moreover {
+      assume "q"
+      hence "q ∨ r" by (rule disjI1)
+      hence ?thesis by (rule disjI2)
+     }
+    ultimately have ?thesis by (rule disjE)
    }
    moreover {
-     note `¬B`
+     assume "r"
-    moreover assume "B"
+     hence "q ∨ r" by (rule disjI2)
-     ultimately have "M" by (rule notE)
+    hence ?thesis by (rule disjI2)
    }
-   ultimately show "M" by (rule disjE)
+   ultimately show ?thesis by (rule disjE)
 qed
-(* alfmarcua marfruman1 *)
+text {* ---------------------------------------------------------------
-lemma ejercicio_8:
+  Ejercicio 33. Demostrar
-   assumes "A ∧ ¬ B ⟶ M"
+     p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
-          "A ∨ B"
+  ------------------------------------------------------------------ *}
-   shows "¬ B ⟶ M"
-proof (rule impI)
+(* pabalagon manperjim marfruman1 josgomrom4 chrgencar gleherlop
-  assume "¬B"
+   alfmarcua pabbergue antramhur enrparalv juacanrod hugrubsan alikan *)
-   show "M" using assms(2)
+lemma ejercicio_33:
+   assumes 1: "p ∧ (q ∨ r)"
+   shows   "(p ∧ q) ∨ (p ∧ r)"
+proof -
+  have 2: p using 1 by (rule conjunct1)
+   show ?thesis
    proof (rule disjE)
-     assume "A"
+     assume 3: q have "p ∧ q" using 2 3 by (rule conjI)
-    then have "A ∧ ¬ B" using `¬ B` by (rule conjI)
+     thus ?thesis by (rule disjI1)
-     show "M" using assms(1) `A ∧ ¬ B` by (rule mp)
    next
-     assume "B"
+     assume 4: r have "p ∧ r" using 2 4 by (rule conjI)
-     show "M" using `¬ B` `B` by (rule notE)
+    thus ?thesis by (rule disjI2)
+  next
+     show "q ∨ r" using 1 by (rule conjunct2)
    qed
 qed
-(* pabalagon manperjim josgomrom4 gleherlop raffergon2 hugrubsan pabbergue enrparalv giafus1 antramhur *)
+(* benber cammonagu *)
-lemma ejercicio_8:
+lemma ejercicio_33_1:
-   assumes "A ⟶ (M ⟷ ¬B)"
+   assumes "p ∧ (q ∨ r)"
-          "A ∨ B"
+  shows   "(p ∧ q) ∨ (p ∧ r)"
-        shows "¬B ⟶ M"
+proof -
-using assms(2) proof (rule disjE)
+  have "p" using assms by (rule conjunct1)
-   assume 1: A
+  have "q ∨ r" using assms by (rule conjunct2)
-   have 2: "M ⟷ ¬B" using assms(1) 1 by (rule mp)
+  moreover {
-   show "¬B ⟶ M" proof (rule impI)
+    assume "q"
-    assume 3: "¬B" show M using 2 3 by (rule iffD2)
+    with `p` have "p ∧ q" by (rule conjI)
-   qed
+    hence ?thesis by (rule disjI1)
+  }
+  moreover {
+    assume "r"
+    with `p` have "p ∧ r" by (rule conjI)
+    hence ?thesis by (rule disjI2)
+  }
+  ultimately show ?thesis by (rule disjE)
+qed
+text {* ---------------------------------------------------------------
+  Ejercicio 34. Demostrar
+     (p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
+   ------------------------------------------------------------------ *}
+(* pabalagon manperjim marfruman1 josgomrom4 chrgencar alfmarcua
+   gleherlop pabbergue antramhur enrparalv juacanrod hugrubsan alikan *)
+lemma ejercicio_34:
+   assumes "(p ∧ q) ∨ (p ∧ r)"
+  shows   "p ∧ (q ∨ r)"
+using assms(1) proof (rule disjE)
+   assume 2: "p ∧ q" hence q by (rule conjunct2)
+  hence 3: "q ∨ r" by (rule disjI1)
+  have p using 2 by (rule conjunct1)
+   thus ?thesis using 3 by (rule conjI)
 next
-   assume 4: B
+   assume 4: "p ∧ r" hence r by (rule conjunct2)
-   show ?thesis proof (rule impI)
+   hence 5: "q ∨ r" by (rule disjI2)
-     assume "¬B" thus M using 4 by (rule notE)
+  have p using 4 by (rule conjunct1)
-   qed
+  thus ?thesis using 5 by (rule conjI)
+qed
+(* benber cammonagu *)
+lemma ejercicio_34_1:
+  assumes "(p ∧ q) ∨ (p ∧ r)"
+  shows   "p ∧ (q ∨ r)"
+proof -
+  have "(p ∧ q) ∨ (p ∧ r)" using assms .
+  moreover {
+    assume "p ∧ q"
+    hence "p" by (rule conjunct1)
+    moreover {
+      have "q" using `p ∧ q` by (rule conjunct2)
+      hence "q ∨ r" by (rule disjI1)
+    }
+    ultimately have ?thesis by (rule conjI)
+  }
+  moreover {
+     assume "p ∧ r"
+    hence "p" by (rule conjunct1)
+    moreover {
+      have "r" using `p ∧ r` by (rule conjunct2)
+      hence "q ∨ r" by (rule disjI2)
+    }
+    ultimately have ?thesis by (rule conjI)
+   }
+  ultimately show ?thesis by (rule disjE)
 qed
 text {* ---------------------------------------------------------------
-   Ejercicio 9. (En APLI2 el ejercicio 13 de LPO) Formalizar, y decidir
+   Ejercicio 35. Demostrar
-  la corrección, del siguiente argumento
+      p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
-      Toda persona pobre tiene un padre rico. Por tanto, existe una
-     persona rica que tiene un abuelo rico.
-  Usar R(x) para x es rico
-       p(x) para el padre de x
    ------------------------------------------------------------------ *}
-(* benber *)
+(* pabalagon manperjim marfruman1 josgomrom4 chrgencar alfmarcua
-lemma
+   gleherlop pabbergue antramhur enrparalv juacanrod hugrubsan alikan *)
-   assumes "∀x. ¬ R x ⟶ R (p x)"
+lemma ejercicio_35:
-   shows "∃x. R x ∧ R (p (p x))"
+   assumes "p ∨ (q ∧ r)"
+  shows   "(p ∨ q) ∧ (p ∨ r)"
+using assms(1) proof (rule disjE)
+  assume 1: p hence 2: "p ∨ r" by (rule disjI1)
+  have "p ∨ q" using 1 by (rule disjI1)
+  thus ?thesis using 2 by (rule conjI)
+next
+   assume 3: "q ∧ r" hence r by (rule conjunct2)
+  hence 4: "p ∨ r" by (rule disjI2)
+  have q using 3 by (rule conjunct1)
+  hence "p ∨ q" by (rule disjI2)
+  thus ?thesis using 4 by (rule conjI)
+qed
+(* benber cammonagu *)
+lemma ejercicio_35_1:
+  assumes "p ∨ (q ∧ r)"
+  shows   "(p ∨ q) ∧ (p ∨ r)"
 proof -
-   have 0: "p ∨ ¬ p" for p
+   have "p ∨ (q ∧ r)" using assms .
-  proof (rule ccontr)
+  moreover {
-     assume "¬ (p ∨ ¬ p)"
+    assume "p"
+    hence "p ∨ q" by (rule disjI1)
+    moreover have "p ∨ r" using `p` by (rule disjI1)
+    ultimately have ?thesis by (rule conjI)
+  }
+  moreover {
+     assume "q ∧ r"
+    {
+      have "q" using `q ∧ r` by (rule conjunct1)
+      hence "p ∨ q" by (rule disjI2)
+    }
      moreover {
-       have "p"
+       have "r" using `q ∧ r` by (rule conjunct2)
-      proof (rule ccontr)
+       hence "p ∨ r" by (rule disjI2)
-        assume "¬ p"
-        hence "p ∨ ¬ p" by (rule disjI2)
-        with `¬ (p ∨ ¬ p)` show "False" by (rule notE)
-      qed
-       hence "p ∨ ¬ p" by (rule disjI1)
      }
-     ultimately show "False" by (rule notE)
+     ultimately have ?thesis by (rule conjI)
-  qed
+  }
+  ultimately show ?thesis by (rule disjE)
+qed
-   have "¬ R x ⟶ R (p x)" for x using assms(1) by (rule allE)
+text {* ---------------------------------------------------------------
-   hence 1: "¬ R x ⟹ R (p x)" for x by (rule mp)
+   Ejercicio 36. Demostrar
+     (p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)
+   ------------------------------------------------------------------ *}
-   have 2: "⟦R y; ¬ R (p y)⟧ ⟹ ?thesis" for y
+(* pabalagon manperjim marfruman1 josgomrom4 chrgencar alfmarcua
-   proof
+   gleherlop pabbergue antramhur enrparalv juacanrod hugrubsan alikan *)
-    assume "R y"
+lemma ejercicio_36:
-    assume "¬ R (p y)"
+   assumes 1: "(p ∨ q) ∧ (p ∨ r)"
-    hence "R (p (p y))" by (rule 1)
+   shows   "p ∨ (q ∧ r)"
-     with `R y` show "R y ∧ R (p (p y))" by (rule conjI)
+proof -
+  have 2: "p ∨ q" using 1 by (rule conjunct1)
+  have 3: "p ∨ r" using 1 by (rule conjunct2)
+  show ?thesis using 2
+  proof (rule disjE)
+    assume p thus ?thesis by (rule disjI1)
+  next
+     assume 4: q show ?thesis using 3
+    proof (rule disjE)
+      assume p thus ?thesis by (rule disjI1)
+    next
+      assume 5: r have "q ∧ r" using 4 5 by (rule conjI)
+      thus ?thesis by (rule disjI2)
+    qed
    qed
+qed
-   have 3: "R y ⟹ ?thesis" for y
+(* benber cammonagu *)
-   proof -
+lemma ejercicio_36_1:
-     assume "R y"
+   assumes "(p ∨ q) ∧ (p ∨ r)"
+   shows   "p ∨ (q ∧ r)"
-     have "R (p y) ∨ ¬ R (p y)" by (rule 0)
+proof -
+  have "p ∨ q" using assms by (rule conjunct1)
+  moreover {
+     assume "p"
+    hence ?thesis by (rule disjI1)
+  }
+  moreover {
+    assume "q"
+     have "p ∨ r" using assms by (rule conjunct2)
      moreover {
-       assume "R (p y)"
+       assume "p"
-      have "R (p (p y)) ∨ ¬ R (p (p y))" by (rule 0)
+       hence ?thesis by (rule disjI1)
-       moreover {
-        assume "R (p (p y))"
-        with `R y` have "R y ∧ R (p (p y))" by (rule conjI)
-        hence ?thesis by (rule exI)
-      }
-      moreover {
-        assume "¬ R (p (p y))"
-        with `R (p y)` have ?thesis by (rule 2)
-      }
-      ultimately have ?thesis by (rule disjE)
      }
      moreover {
-       assume "¬ R (p y)"
+       assume "r"
-       with `R y` have ?thesis by (rule 2)
+       with `q` have "q ∧ r" by (rule conjI)
+      hence ?thesis by (rule disjI2)
      }
-     ultimately show ?thesis by (rule disjE)
+     ultimately have ?thesis by (rule disjE)
+  }
+  ultimately show ?thesis by (rule disjE)
+qed
+text {* ---------------------------------------------------------------
+  Ejercicio 37. Demostrar
+     (p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop
+   pabbergue antramhur enrparalv juacanrod hugrubsan alikan *)
+lemma ejercicio_37:
+  assumes 1: "(p ⟶ r) ∧ (q ⟶ r)"
+  shows   "p ∨ q ⟶ r"
+proof (rule impI)
+  have 2: "p ⟶ r" using 1 by (rule conjunct1)
+  have 3: "q ⟶ r" using 1 by (rule conjunct2)
+  assume 4: "p ∨ q" show "r" using 4
+  proof (rule disjE)
+    assume 5: "p" show "r" using 2 5 by (rule mp)
+  next
+    assume 6: "q" show "r" using 3 6 by (rule mp)
    qed
+qed
-   fix y
+(* benber cammonagu *)
-   have "R y ∨ ¬ R y" by (rule 0)
+lemma ejercicio_37_1:
+   assumes "(p ⟶ r) ∧ (q ⟶ r)"
+   shows   "p ∨ q ⟶ r"
+proof
+  assume "p ∨ q"
    moreover {
-     assume "R y"
+     have "p ⟶ r" using assms by (rule conjunct1)
-     hence ?thesis by (rule 3)
+    moreover assume "p"
+     ultimately have "r" by (rule mp)
    }
    moreover {
-     assume "¬ R y"
+     have "q ⟶ r" using assms by (rule conjunct2)
-     hence "R (p y)" by (rule 1)
+     moreover assume "q"
-     hence ?thesis by (rule 3)
+     ultimately have "r" by (rule mp)
    }
-   ultimately show ?thesis by (rule disjE)
+   ultimately show "r" by (rule disjE)
 qed
-(* alfmarcua *)
+text {* ---------------------------------------------------------------
-lemma ejercicio_9:
+  Ejercicio 38. Demostrar
-   assumes "∀ x. ¬ R x ⟶ R (p x)"
+     p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
-   shows "∃x. R x ∧ R (p (p x))"
+  ------------------------------------------------------------------ *}
-proof (rule disjE, rule ejercicio_52)
-  have prelemma:"(∃y. ¬ R (p y)) ⟶ ?thesis"
+(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop
+   pabbergue antramhur enrparalv juacanrod hugrubsan alikan *)
+lemma ejercicio_38:
+   assumes "p ∨ q ⟶ r"
+   shows   "(p ⟶ r) ∧ (q ⟶ r)"
+proof (rule conjI)
+  show "p ⟶ r"
+  proof (rule impI)
+    assume "p" hence 1: "p ∨ q" by (rule disjI1)
+    show "r" using assms(1) 1 by (rule mp)
+  qed
+next
+  show "q ⟶ r"
    proof (rule impI)
-     assume "∃y. ¬ R (p y)"
+     assume q hence 2: "p ∨ q" by (rule disjI2)
-    then obtain b where  "¬ R (p b)" by (rule exE)
+     show r using assms(1) 2 by (rule mp)
-     have "¬ R (p b) ⟶ R (p (p b))" using assms by (rule allE)
+  qed
-    then have "R (p (p b))" using `¬ R (p b)` by (rule mp)
+qed
-    have "¬ R b ⟶ R (p b)" using assms by (rule allE)
-    then have "¬¬ R b" using `¬ R (p b)` by (rule mt)
+(* benber cammonagu*)
-     then have "R b" by (rule notnotD)
+lemma ejercicio_38_1:
-     then have "R b ∧ R (p (p b))" using `R (p (p b))` by (rule conjI)
+  assumes "p ∨ q ⟶ r"
-     then show "∃x. R x ∧ R (p (p x))" by (rule exI)
+  shows   "(p ⟶ r) ∧ (q ⟶ r)"
+proof
+  show "p ⟶ r"
+  proof
+     assume "p"
+     hence "p ∨ q" by (rule disjI1)
+     with assms show "r" by (rule mp)
    qed
+next
-   fix a
+  show "q ⟶ r"
-   show "R (p a) ⟹ ?thesis"
+  proof
-   proof (rule disjE, rule ejercicio_52)
+    assume "q"
-    assume "R (p a)"
+    hence "p ∨ q" by (rule disjI2)
-    show "R (p (p a)) ⟹ ?thesis"
+    with assms show "r" by (rule mp)
-    proof (rule disjE, rule ejercicio_52)
+   qed
-      assume "R (p (p (p a)))"
+qed
-      have "R (p a) ∧ R (p (p (p a)))" using `R (p a)` `R (p (p (p a)))`  by (rule conjI)
-      then show ?thesis by (rule exI)
+section {* Negaciones *}
-    next
-      assume "¬ R (p (p (p a)))"
+text {* ---------------------------------------------------------------
-      then have "∃y. ¬ R (p y)" by (rule exI)
+   Ejercicio 39. Demostrar
-      show ?thesis using prelemma `∃y. ¬ R (p y)` by (rule mp)
+     p ⊢ ¬¬p
-    qed
+   ------------------------------------------------------------------ *}
+(* pabalagon manperjim  benber josgomrom4 raffergon2 gleherlop
+   marfruman1 chrgencar alfmarcua pabbergue enrparalv juacanrod
+   hugrubsan cammonagu alikan *)
+lemma ejercicio_39:
+  assumes "p"
+  shows   "¬¬p"
+  using assms(1) by (rule notnotI)
+text {* ---------------------------------------------------------------
+  Ejercicio 40. Demostrar
+     ¬p ⊢ p ⟶ q
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua pabbergue
+   gleherlop juacanrod enrparalv hugrubsan alikan *)
+lemma ejercicio_40:
+  assumes 1: "¬p"
+   shows   "p ⟶ q"
+proof (rule impI)
+  assume 2: p show q using 1 2 by (rule notE)
+qed
+(* benber cammonagu *)
+lemma ejercicio_40_1:
+  assumes "¬p"
+  shows   "p ⟶ q"
+proof
+  assume "p"
+  with `¬p` show "q" by (rule notE)
+qed
+text {* ---------------------------------------------------------------
+  Ejercicio 41. Demostrar
+     p ⟶ q ⊢ ¬q ⟶ ¬p
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim raffergon2 josgomrom4 marfruman1 alfmarcua
+   pabbergue gleherlop enrparalv juacanrod hugrubsan alikan *)
+lemma ejercicio_41:
+  assumes 1: "p ⟶ q"
+  shows   "¬q ⟶ ¬p"
+proof (rule impI)
+  assume 2: "¬q" show "¬p" using 1 2 by (rule mt)
+qed
+(* benber cammonagu *)
+lemma ejercicio_41_1:
+  assumes "p ⟶ q"
+  shows   "¬q ⟶ ¬p"
+proof
+  assume "¬q"
+  with `p ⟶ q` show "¬p" by (rule mt)
+qed
+text {* ---------------------------------------------------------------
+  Ejercicio 42. Demostrar
+     p∨q, ¬q ⊢ p
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim raffergon2 josgomrom4 marfruman1 alfmarcua
+   pabbergue gleherlop enrparalv juacanrod hugrubsan alikan *)
+lemma ejercicio_42:
+  assumes "p∨q"
+          "¬q"
+  shows   "p"
+using assms(1) proof (rule disjE)
+  assume "p" thus "p" .
+next
+  assume 2: "q" show "p" using assms(2) 2 by (rule notE)
+qed
+(* benber cammonagu *)
+lemma ejercicio_42_1:
+  assumes "p∨q"
+          "¬q"
+  shows   "p"
+proof -
+  note `p ∨ q`
+  moreover have "p ⟹ p" .
+  moreover {
+    assume "q"
+    with `¬q` have "p" by (rule notE)
+  }
+  ultimately show "p" by (rule disjE)
+qed
+text {* ---------------------------------------------------------------
+  Ejercicio 43. Demostrar
+     p ∨ q, ¬p ⊢ q
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim raffergon2 josgomrom4 marfruman1 alfmarcua
+   pabbergue gleherlop enrparalv juacanrod hugrubsan alikan *)
+lemma ejercicio_43:
+  assumes "p ∨ q"
+          "¬p"
+  shows   "q"
+using assms(1) proof (rule disjE)
+  assume 1: "p" show "q" using assms(2) 1 by (rule notE)
+next
+  assume "q" thus "q" .
+qed
+(* benber cammonagu*)
+lemma ejercicio_43_1:
+  assumes "p ∨ q"
+          "¬p"
+  shows   "q"
+proof -
+  note `p ∨ q`
+  moreover {
+    assume "p"
+    with `¬p` have "q" by (rule notE)
+  }
+  moreover have "q ⟹ q" .
+  ultimately show "q" by (rule disjE)
+qed
+text {* ---------------------------------------------------------------
+  Ejercicio 44. Demostrar
+     p ∨ q ⊢ ¬(¬p ∧ ¬q)
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim gleherlop josgomrom4 marfruman1 pabbergue
+   juacanrod hugrubsan alikan *)
+lemma ejercicio_44:
+  assumes "p ∨ q"
+  shows   "¬(¬p ∧ ¬q)"
+proof (rule notI)
+  assume 1: "¬p ∧ ¬q" hence 2: "¬p" by (rule conjunct1)
+  have 3: "¬q" using 1 by (rule conjunct2)
+  show "False"
+  using assms(1) proof (rule disjE)
+    assume 4: "p" show ?thesis using 2 4 by (rule notE)
+  next
+    assume 5: "q" show ?thesis using 3 5 by (rule notE)
+  qed
+qed
+(* benber alfmarcua cammonagu *)
+lemma ejercicio_44_1:
+  assumes "p ∨ q"
+  shows   "¬(¬p ∧ ¬q)"
+proof
+  assume "¬p ∧ ¬q"
+  note `p ∨ q`
+  moreover {
+    from `¬p ∧ ¬q` have "¬p" by (rule conjunct1)
+    moreover assume "p"
+    ultimately have "False" by (rule notE)
+  }
+  moreover {
+    from `¬p ∧ ¬q` have "¬q" by (rule conjunct2)
+    moreover assume "q"
+    ultimately have "False" by (rule notE)
+  }
+  ultimately show "False" by (rule disjE)
+qed
+text {* ---------------------------------------------------------------
+  Ejercicio 45. Demostrar
+     p ∧ q ⊢ ¬(¬p ∨ ¬q)
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim marfruman1 josgomrom4 gleherlop pabbergue
+   juacanrod hugrubsan alikan *)
+lemma ejercicio_45:
+  assumes 1: "p ∧ q"
+  shows   "¬(¬p ∨ ¬q)"
+proof (rule notI)
+  assume 2: "¬p ∨ ¬q" have 3: "p" using 1 by (rule conjunct1)
+  have 4: "q" using 1 by (rule conjunct2)
+  show "False" using 2
+  proof (rule disjE)
+    assume "¬p" thus ?thesis using 3 by (rule notE)
    next
-     assume "¬ R (p (p a))"
+     assume "¬q" thus ?thesis using 4 by (rule notE)
-    then have "∃y. ¬ R (p y)" by (rule exI)
-    show ?thesis using prelemma `∃y. ¬ R (p y)` by (rule mp)
    qed
+qed
+(* benber alfmarcua cammonagu *)
+lemma ejercicio_45_1:
+  assumes "p ∧ q"
+  shows   "¬(¬p ∨ ¬q)"
+proof
+  assume "¬p ∨ ¬q"
+  moreover {
+    assume "¬p"
+    moreover have "p" using `p ∧ q` by (rule conjunct1)
+    ultimately have "False" by (rule notE)
+  }
+  moreover {
+    assume "¬q"
+    moreover have "q" using `p ∧ q` by (rule conjunct2)
+    ultimately have "False" by (rule notE)
+  }
+  ultimately show False by (rule disjE)
+qed
-   assume "¬ R (p a)"
+text {* ---------------------------------------------------------------
-   then have "∃y. ¬ R (p y)" by (rule exI)
+  Ejercicio 46. Demostrar
-   show ?thesis using prelemma `∃y. ¬ R (p y)` by (rule mp)
+     ¬(p ∨ q) ⊢ ¬p ∧ ¬q
+   ------------------------------------------------------------------ *}
+(* pabalagon manperjim marfruman1 josgomrom4 gleherlop pabbergue
+   juacanrod hugrubsan alikan *)
+lemma ejercicio_46:
+  assumes 1: "¬(p ∨ q)"
+   shows   "¬p ∧ ¬q"
+proof (rule conjI)
+  show "¬p"
+  proof (rule notI)
+    assume p hence 2: "p ∨ q" by (rule disjI1)
+    show False using 1 2 by (rule notE)
+  qed
+   show "¬q"
+  proof (rule notI)
+    assume q hence 3: "p ∨ q" by (rule disjI2)
+    show False using 1 3 by (rule notE)
+  qed
 qed
-(* pabalagon manperjim marfruman1 josgomrom4 gleherlop raffergon2 hugrubsan pabbergue enrparalv giafus1 antramhur *)
+(* benber cammmonagu *)
-lemma ejercicio_9:
+lemma ejercicio_46_1:
-   assumes "∀x. ¬R x ⟶ R (p x)"
+   assumes "¬(p ∨ q)"
-   shows "∃x. R x ∧ R (p (p x))"
+   shows   "¬p ∧ ¬q"
-proof -
+proof
-   fix y
+   show "¬p"
-   have s1: "⟦¬R (p y)⟧ ⟹ ?thesis" for y proof (rule exI)
+   proof (rule ccontr)
-     assume 2: "¬R (p y)"
+     assume "¬¬p"
-     have "¬R (p y) ⟶ R (p (p y))" using assms(1) by (rule allE)
+     hence "p" by (rule notnotD)
-     hence 3: "R (p (p y))" using 2 by (rule mp)
+     hence "p ∨ q" by (rule disjI1)
-     have "¬R y ⟶ R (p y)" using assms(1) by (rule allE)
+     with assms show "False" by (rule notE)
-     hence "¬¬R y" using 2 by (rule mt)
+  qed
-     hence "R y" by (rule notnotD)
+next
-     thus "R y ∧ R (p (p y))" using 3 by (rule conjI)
+  show "¬q"
+  proof (rule ccontr)
+    assume "¬¬q"
+     hence "q" by (rule notnotD)
+     hence "p ∨ q" by (rule disjI2)
+     with assms show "False" by (rule notE)
    qed
-   have s2: "R y ⟹ ?thesis" for y proof -
+qed
-    assume 2: "R y"
-    have "¬R (p y) ∨ R (p y)" by (rule excluded_middle)
+(* alfmarcua *)
-    thus ?thesis proof (rule disjE)
+lemma ejercicio_46_2:
-      assume 3: "¬R (p y)" thus ?thesis by (rule s1)
+   assumes "¬(p ∨ q)"
-    next
+  shows   "¬p ∧ ¬q"
-      assume 4: "R (p y)"
+proof (rule conjI)
-      have "¬R (p (p y)) ∨ R (p (p y))" by (rule excluded_middle)
+  have "p ⟹ p ∨ q" by (rule disjI1)
-      thus ?thesis proof (rule disjE)
+  then have "p ⟶ p ∨ q" by (rule impI)
-        assume "¬R (p (p y))" thus ?thesis by (rule s1)
+  then show "¬ p" using assms by (rule mt)
-      next
+next
-        assume "R (p (p y))"
+  have "q ⟹ p ∨ q" by (rule disjI2)
-        with `R y` have "R y ∧ R (p (p y))" by (rule conjI)
+  then have "q ⟶ p ∨ q" by (rule impI)
-        thus ?thesis by (rule exI)
+  then show "¬ q" using assms by (rule mt)
-      qed
+qed
-    qed
+text {* ---------------------------------------------------------------
+  Ejercicio 47. Demostrar
+     ¬p ∧ ¬q ⊢ ¬(p ∨ q)
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim marfruman1 josgomrom4 pabbregue juacanrod
+   hugrubsan alikan *)
+lemma ejercicio_47:
+  assumes 1: "¬p ∧ ¬q"
+  shows   "¬(p ∨ q)"
+proof (rule notI)
+  have 2: "¬p" using 1 by (rule conjunct1)
+  have 3: "¬q" using 1 by (rule conjunct2)
+  assume 4: "p ∨ q"
+  show False
+  using 4 proof (rule disjE)
+    assume 5: p show ?thesis using 2 5 by (rule notE)
+  next
+    assume 6: q show ?thesis using 3 6 by (rule notE)
    qed
-   have "¬R y ∨ R y" by (rule excluded_middle)
+qed
-   thus ?thesis proof (rule disjE)
-     assume 2: "R y" thus ?thesis by (rule s2)
+(* benber gleherlop cammonagu*)
+lemma ejercicio_47_1:
+  assumes "¬p ∧ ¬q"
+  shows   "¬(p ∨ q)"
+proof
+  assume "p ∨ q"
+  hence "¬(¬p ∧ ¬q)" by (rule ejercicio_44_1)
+  thus "False" using assms by (rule notE)
+qed
+(* alfmarcua *)
+lemma ejercicio_47_2:
+  assumes "¬p ∧ ¬q"
+  shows   "¬(p ∨ q)"
+proof (rule notI)
+  have "¬ p" using assms by (rule conjunct1)
+   have "¬ q" using assms by (rule conjunct2)
+  assume "p ∨ q"
+  then have "q" using `¬ p` by (rule ejercicio_43)
+   show False using `¬ q` `q` by (rule notE)
+qed
+text {* ---------------------------------------------------------------
+  Ejercicio 48. Demostrar
+     ¬p ∨ ¬q ⊢ ¬(p ∧ q)
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim marfruman1 josgomrom4 pabbergue juacanrod
+   hugrubsan alikan *)
+lemma ejercicio_48:
+  assumes 1: "¬p ∨ ¬q"
+  shows   "¬(p ∧ q)"
+proof (rule notI)
+  assume 2: "p ∧ q" hence 3: p by (rule conjunct1)
+  have 4: q using 2 by (rule conjunct2)
+  show False
+  using 1 proof (rule disjE)
+     assume "¬p" thus ?thesis using 3 by (rule notE)
    next
-     assume 4: "¬R y"
+     assume "¬q" thus ?thesis using 4 by (rule notE)
-    have "¬R y ⟶ R (p y)" using assms(1) by (rule allE)
-    hence "R (p y)" using 4 by (rule mp)
-    thus ?thesis by (rule s2)
    qed
+qed
+(* benber alfmarcua gleherlop cammonagu *)
+lemma ejercicio_48_1:
+  assumes "¬p ∨ ¬q"
+  shows   "¬(p ∧ q)"
+proof
+  assume "p ∧ q"
+  hence "¬(¬p ∨ ¬q)" by (rule ejercicio_45_1)
+  thus "False" using assms by (rule notE)
 qed
 text {* ---------------------------------------------------------------
-   Ejercicio 10. (En APLI2 el ejercicio 10 de LPO) Formalizar, y decidir
+   Ejercicio 49. Demostrar
-  la corrección, del siguiente argumento
+      ⊢ ¬(p ∧ ¬p)
-     Los aficionados al fútbol aplauden a cualquier futbolista
-     extranjero. Juanito no aplaude a futbolistas extranjeros. Por
-     tanto, si hay algún futbolista extranjero nacionalizado español,
-      Juanito no es aficionado al fútbol.
-  Usar Af(x)   para x es aficicionado al fútbol
-       Ap(x,y) para x aplaude a y
-       E(x)    para x es un futbolista extranjero
-       N(x)    para x es un futbolista nacionalizado español
-       j       para Juanito
    ------------------------------------------------------------------ *}
+(* pabalagon manperjim marfruman1 josgomrom4 alfmarcu gleherlop
+   hugrubsan juacanrod cammonagu alikan *)
+lemma ejercicio_49:
+  "¬(p ∧ ¬p)"
+proof (rule notI)
+  assume 1: "p ∧ ¬p" hence 2: p by (rule conjunct1)
+  have "¬p" using 1 by (rule conjunct2)
+  thus "False" using 2 by (rule notE)
+qed
 (* benber *)
-lemma
+lemma ejercicio_49_1:
-   assumes "∀x. Af x ⟶ (∀y. E y ⟶ Ap x y)"
+   "¬(p ∧ ¬p)"
-    and "∀x. E x ⟶ ¬ Ap j x"
-  shows "(∃x. E x ∧ N x) ⟶ ¬ Af j"
 proof
-   assume "∃x. E x ∧ N x"
+   assume "p ∧ ¬p"
+  hence "¬p" by (rule conjunct2)
+  moreover have "p" using `p ∧ ¬p` by (rule conjunct1)
+  ultimately show "False" by (rule notE)
+qed
+text {* ---------------------------------------------------------------
+  Ejercicio 50. Demostrar
+     p ∧ ¬p ⊢ q
+  ------------------------------------------------------------------ *}
-   show "¬ Af j"
+(* pabalagon manperjim raffergon2 josgomrom4 marfruman1 gleherlop
-   proof (rule ccontr)
+   alfmarcua enrparalv pabbergue juacanrod hugrubsan alikan *)
-    assume "¬ ¬ Af j"
+lemma ejercicio_50:
-    hence "Af j" by (rule notnotD)
+   assumes 1: "p ∧ ¬p"
+   shows   "q"
+proof (rule notE)
+  show p using 1 by (rule conjunct1)
+  show "¬p" using 1 by (rule conjunct2)
+qed
-    note `∀x. Af x ⟶ (∀y. E y ⟶ Ap x y)`
+(* benber cammonagu*)
-    hence "Af j ⟶ (∀x. E x ⟶ Ap j x)" by (rule allE)
+lemma ejercicio_50_1:
-    moreover note `Af j`
+  assumes "p ∧ ¬p"
-    ultimately have "∀x. E x ⟶ Ap j x" by (rule mp)
+  shows   "q"
+proof -
+  have "¬p" using `p ∧ ¬p` by (rule conjunct2)
+  moreover have "p" using `p ∧ ¬p` by (rule conjunct1)
+  ultimately show "q" by (rule notE)
+qed
-    note `∃x. E x ∧ N x`
+text {* ---------------------------------------------------------------
-    moreover have "E x ∧ N x ⟹ False" for x
+  Ejercicio 51. Demostrar
-    proof -
+     ¬¬p ⊢ p
-      assume "E x ∧ N x"
+  ------------------------------------------------------------------ *}
-      hence "E x" by (rule conjunct1)
-      note `∀x. E x ⟶ Ap j x`
+(* pabalagon manperjim benber raffergon2 josgomrom4 marfruman1 gleherlop
-      hence "E x ⟶ Ap j x" by (rule allE)
+   alfmarcua enrparalv pabbergue juacanrod hugrubsan cammmonagu alikan *)
-      hence "Ap j x" using `E x`  by (rule mp)
+lemma ejercicio_51:
+  assumes "¬¬p"
+  shows   "p"
+  using assms(1) by (rule notnotD)
-      note `∀x. E x ⟶ ¬ Ap j x`
+text {* ---------------------------------------------------------------
-      hence "E x ⟶ ¬ Ap j x" by (rule allE)
+  Ejercicio 52. Demostrar
-      hence "¬ Ap j x" using `E x` by (rule mp)
+     ⊢ p ∨ ¬p
-      thus "False" using `Ap j x` by (rule notE)
+  ------------------------------------------------------------------ *}
-     qed
-    ultimately show "False" by (rule exE)
+(* pabalagon manperjim marfruman1 josgomrom4 juacanrod pabbergue alikan *)
+lemma ejercicio_52:
+  "p ∨ ¬p"
+proof (rule ccontr)
+  assume 1: "¬(p ∨ ¬p)"
+  have 2: "¬p" proof (rule notI)
+    assume p hence 3: "p ∨ ¬p" by (rule disjI1)
+     show "False" using 1 3 by (rule notE)
    qed
+  have 4: "p ∨ ¬p" using 2 by (rule disjI2)
+  show "False" using 1 4 by (rule notE)
 qed
-(* alfmarcua marfruman1 *)
+(* benber cammonagu *)
-lemma ejercicio_10:
+lemma ejercicio_52_1:
-   assumes "∀x y. Af x ∧ E y ⟶ Ap x y"
+  "p ∨ ¬p"
-          "∀y. E y ⟶ ¬ Ap j y"
+proof (rule ccontr)
-   shows "(∃y. E y ∧ N y) ⟶ ¬ Af j"
+  assume "¬ (p ∨ ¬ p)"
+  hence "¬p ∧ ¬¬p" by (rule ejercicio_46_1)
+  hence "¬p" by (rule conjunct1)
+  moreover {
+    have "¬¬p" using `¬p ∧ ¬¬p` by (rule conjunct2)
+    hence "p" by (rule notnotD)
+  }
+  ultimately show "False" by (rule notE)
+qed
+(* alfmarcua *)
+lemma ejercicio_52_2:
+   "p ∨ ¬p"
+proof (rule ccontr)
+  assume "¬ (p ∨ ¬ p)"
+   then have "¬ p ∧ ¬¬ p" by (rule ejercicio_46)
+  then show False by (rule ejercicio_50)
+qed
+text {* ---------------------------------------------------------------
+  Ejercicio 53. Demostrar
+     ⊢ ((p ⟶ q) ⟶ p) ⟶ p
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop
+   juacanrod pabbergue *)
+lemma ejercicio_53:
+  "((p ⟶ q) ⟶ p) ⟶ p"
 proof (rule impI)
-   assume "∃x. E x ∧ N x"
+   assume 1: "(p ⟶ q) ⟶ p"
-  then obtain a where "E a ∧ N a" by (rule exE)
+   show p proof (rule ccontr)
-  then have "E a" by (rule conjunct1)
+     assume 2: "¬p"
-   show "¬ Af j"
+     have 3: "¬(p ⟶ q)" using 1 2 by (rule mt)
-  proof (rule notI, rule notE)
+     have 4: "p ⟶ q" proof (rule impI)
-     assume "Af j"
+      assume 5: p show q using 2 5 by (rule notE)
-     then show "Af j ∧ E a" using `E a` by (rule conjI)
+     qed
-  next
+     show False using 3 4 by (rule notE)
-    have "E a ⟶ ¬ Ap j a" using assms(2) by (rule allE)
-     then have "¬ Ap j a" using `E a` by (rule mp)
-    have "∀y. Af j ∧ E y ⟶ Ap j y" using assms(1) by (rule allE)
-     then have "Af j ∧ E a ⟶ Ap j a" by (rule allE)
-     then show "¬ (Af j ∧ E a)" using `¬ Ap j a` by (rule mt)
    qed
 qed
-(* pabalagon manperjim josgomrom4 gleherlop raffergon2 hugrubsan pabbergue enrparalv giafus1 antramhur *)
+(* benber cammonagu *)
-lemma ejercicio_10:
+lemma ejercicio_53_1:
-   assumes "∀x y. Af x ∧ E y ⟶ Ap x y"
+   "((p ⟶ q) ⟶ p) ⟶ p"
-          "∀x y. x = j ∧ E y ⟶ ¬(Ap x y)"
+proof
-   shows "(∃ x. (E x ∧ N x)) ⟶ ¬(Af j)"
+  assume "(p ⟶ q) ⟶ p"
+  have "p ∨ ¬p" by (rule ejercicio_52_1)
+  moreover have "p ⟹ p" .
+   moreover {
+    assume "¬ p"
+    hence "p ⟶ q" by (rule ejercicio_40_1)
+    with `(p ⟶ q) ⟶ p` have "p" by (rule mp)
+  }
+  ultimately show "p" by (rule disjE)
+qed
+text {* ---------------------------------------------------------------
+  Ejercicio 54. Demostrar
+     ¬q ⟶ ¬p ⊢ p ⟶ q
+  ------------------------------------------------------------------ *}
+(* pabalagon manperjim marfruman1 josgomrom4 gleherlop juacanrod
+   pabbergue *)
+lemma ejercicio_54:
+  assumes 1: "¬q ⟶ ¬p"
+  shows   "p ⟶ q"
 proof (rule impI)
-   assume 1: "∃x. E x ∧ N x"
+   assume 2: "p" hence 3: "¬¬p" by (rule notnotI)
-  show "¬(Af j)" proof (rule ccontr)
+  have "¬¬q" using 1 3 by (rule mt)
-    fix a
+  thus "q" by (rule notnotD)
-    assume "¬¬Af j" hence 2: "Af j" by (rule notnotD)
+qed
-    obtain a where 3: "E a ∧ N a" using 1 by (rule exE)
-    hence 4: "E a" by (rule conjunct1)
+(* benber alfmarcua  cammonagu *)
-    have 5: "N a" using 3 by (rule conjunct2)
+lemma ejercicio_54_1:
-    have "∀y. Af j ∧ E y ⟶ Ap j y" using assms(1) by (rule allE)
+  assumes "¬q ⟶ ¬p"
-    hence 6: "Af j ∧ E a ⟶ Ap j a" by (rule allE)
+  shows   "p ⟶ q"
-    have 7: "Af j ∧ E a" using 2 4 by (rule conjI)
+proof
-    have 8: "Ap j a" using 6 7 by (rule mp)
+  assume "p"
-    have "∀y. j = j ∧ E y ⟶ ¬(Ap j y)" using assms(2) by (rule allE)
+  hence "¬¬p" by (rule notnotI)
-    hence 9: "j = j ∧ E a ⟶ ¬(Ap j a)" by (rule allE)
+  with assms have "¬¬q" by (rule mt)
-     have "j = j" by (rule refl)
+  thus "q" by (rule notnotD)
-    hence 10: "j = j ∧ E a" using 4 by (rule conjI)
+qed
-     have "¬(Ap j a)" using 9 10 by (rule mp)
-     thus False using 8 by (rule notE)
+text {* ---------------------------------------------------------------
+  Ejercicio 55. Demostrar
+     ¬(¬p ∧ ¬q) ⊢ p ∨ q
+  ------------------------------------------------------------------ *}
+(* pabalagon marfruman1*)
+lemma ejercicio_55:
+  assumes 1: "¬(¬p ∧ ¬q)"
+  shows   "p ∨ q"
+proof (rule ccontr)
+  assume 2: "¬(p ∨ q)"
+  have 3: "p"
+  proof (rule ccontr)
+    assume 4: "¬p"
+     have 5: "q"
+    proof (rule ccontr)
+      assume 6: "¬q" have 7: "¬p ∧ ¬q" using 4 6 by (rule conjI)
+      show False using 1 7 by (rule notE)
+    qed
+     have 8: "p ∨ q" using 5 by (rule disjI2)
+     show False using 2 8 by (rule notE)
    qed
+  have 9: "p ∨ q" using 3 by (rule disjI1)
+  show False using 2 9 by (rule notE)
+qed
+(* benber alfmarcua josgomrom4 manperjim pabbergue juacanrod cammonagu *)
+lemma ejercicio_55_1:
+  assumes "¬(¬p ∧ ¬q)"
+  shows   "p ∨ q"
+proof (rule ccontr)
+  assume "¬(p ∨ q)"
+  hence "¬p ∧ ¬q" by (rule ejercicio_46_1)
+  with assms show False by (rule notE)
 qed
 text {* ---------------------------------------------------------------
-   Ejercicio 11. Formalizar, y decidir la corrección, del siguiente
+   Ejercicio 56. Demostrar
-  argumento
+      ¬(¬p ∨ ¬q) ⊢ p ∧ q
-     Ningún socio del club está en deuda con el tesorero del club. Si
+  ------------------------------------------------------------------ *}
-      un socio del club no paga su cuota está en deuda con el tesorero
-     del club. Por tanto, si el tesorero del club es socio del club,
-     entonces paga su cuota.
-  Usar P(x) para x es socio del club
-       Q(x) para x paga su cuota
-       R(x) para x está en deuda con el tesorero
-       a    para el tesorero del club
-   ------------------------------------------------------------------ *}
-(* benber *)
+(* pabalagon manperjim marfruman1 josgomrom4 gleherlop juacanrod
-lemma
+   pabbergue *)
-   assumes A1: "∀x. P x ⟶ R x"
+lemma ejercicio_56:
-     and A2: "∀x. P x ⟶ (¬(Q x) ⟶ R x)"
+   assumes 1: "¬(¬p ∨ ¬q)"
-     and "¬(R a)"
+  shows   "p ∧ q"
-   shows "P a ⟶ Q a"
+proof (rule conjI)
-proof
+  show 3: p
-   have "P a ⟶ (¬(Q a) ⟶ R a)" using A2 by (rule allE)
+  proof (rule ccontr)
-  moreover assume "P a"
+     assume "¬p" hence 4: "¬p ∨ ¬q" by (rule disjI1)
-   ultimately have "¬(Q a) ⟶ R a" by (rule mp)
+    show False using 1 4 by (rule notE)
+  qed
+  show 5: q
+  proof (rule ccontr)
+    assume "¬q" hence 6: "¬p ∨ ¬q" by (rule disjI2)
+     show False using 1 6 by (rule notE)
+  qed
+qed
+(* benber alfmarcua cammonagu *)
+lemma ejercicio_56_1:
+  assumes "¬(¬p ∨ ¬q)"
+   shows   "p ∧ q"
+proof -
+   have "¬¬p ∧ ¬¬q" using assms by (rule ejercicio_46_1)
+  hence "¬¬p" by (rule conjunct1)
+  hence "p" by (rule notnotD)
+  moreover {
+    have "¬¬q" using `¬¬p ∧ ¬¬q` by (rule conjunct2)
+    hence "q" by (rule notnotD)
+  }
+   ultimately show "p ∧ q" by (rule conjI)
+qed
+text {* ---------------------------------------------------------------
+  Ejercicio 57. Demostrar
+     ¬(p ∧ q) ⊢ ¬p ∨ ¬q
+  ------------------------------------------------------------------ *}
-   show "Q a"
+(* pabalagon manperjim marfruman1 josgomrom4 gleherlop juacanrod
-   proof (rule ccontr)
+   pabbergue *)
-    assume "¬(Q a)"
+lemma ejercicio_57:
-     with `¬(Q a) ⟶ R a` have "R a" by (rule mp)
+   assumes 1: "¬(p ∧ q)"
-     with `¬(R a)` show "False" by (rule notE)
+   shows   "¬p ∨ ¬q"
+proof (rule ccontr)
+  assume 2: "¬(¬p ∨ ¬q)"
+  show False using 1
+  proof (rule notE)
+     show 3: "p ∧ q"
+    proof (rule conjI)
+      show p
+      proof (rule ccontr)
+        assume "¬p" hence 4: "¬p ∨ ¬q" by (rule disjI1)
+        show False using 2 4 by (rule notE)
+      qed
+     next
+      show q
+      proof (rule ccontr)
+        assume "¬q" hence 5: "¬p ∨ ¬q" by (rule disjI2)
+        show False using 2 5 by (rule notE)
+      qed
+    qed
    qed
 qed
-(* alfmarcua *)
+(* benber alfmarcua cammonagu *)
-lemma ejercicio_11:
+lemma ejercicio_57_1:
-   assumes "∄x. P x ∧ R x"
+   assumes "¬(p ∧ q)"
-          "∀x. P x ∧ (¬ Q x) ⟶ R x"
+   shows   "¬p ∨ ¬q"
-   shows "P a ⟶ Q a"
+proof (rule ccontr)
-proof (rule impI, rule ccontr)
+   assume "¬(¬p ∨ ¬q)"
-   assume "P a" "¬ Q a"
+   hence "p ∧ q" by (rule ejercicio_56_1)
-  then have "P a ∧ (¬ Q a)" by (rule conjI)
+   with assms show "False" by (rule notE)
-   have "P a ∧ (¬ Q a) ⟶ R a" using assms(2) by (rule allE)
-   then have "R a" using `P a ∧ (¬ Q a)` by (rule mp)
-  have "P a ∧ R a" using `P a` `R a` by (rule conjI)
-  then have "∃x. P x ∧ R x" by (rule exI)
-  show False using assms(1) `∃x. P x ∧ R x` by (rule notE)
 qed
-(* pabalagon manperjim marfruman1 josgomrom4 gleherlop hugrubsan pabbergue enrparalv giafus1 antramhur *)
+text {* ---------------------------------------------------------------
-lemma ejercicio_11:
+  Ejercicio 58. Demostrar
-   assumes "¬(∃x. P x ∧ R x)"
+     ⊢ (p ⟶ q) ∨ (q ⟶ p)
-          "∀x. P x ∧ ¬Q x ⟶ R x"
+  ------------------------------------------------------------------ *}
-   shows "P a ⟶ Q a"
-proof (rule impI)
+(* pabalagon manperjim josgomrom4 marfruman1 juacanrod pabbergue *)
-  assume 1: "P a"
+lemma ejercicio_58:
-  show "Q a" proof (rule ccontr)
+   "(p ⟶ q) ∨ (q ⟶ p)"
-    assume 2: "¬Q a"
+proof -
-    have 3: "P a ∧ ¬Q a" using 1 2 by (rule conjI)
+   have "(p ⟶ q) ∨ ¬(p ⟶ q)" proof (rule ccontr)
-     have 4: "P a ∧ ¬ Q a ⟶R a" using assms(2) by (rule allE)
+    assume 1: "¬((p ⟶ q) ∨ ¬(p ⟶ q))"
-     hence 5: "R a" using 3 by (rule mp)
+    have 2: "¬(p ⟶ q)" proof (rule notI)
-     have 6: "P a ∧ R a" using 1 5 by (rule conjI)
+      assume "p ⟶ q"
-     hence 7: "∃x. P x ∧ R x" by (rule exI)
+      hence 3: "(p ⟶ q) ∨ ¬(p ⟶ q)" by (rule disjI1)
-    show False using assms(1) 7 by (rule notE)
+      show False using 1 3 by (rule notE)
+     qed
+    hence 4: "(p ⟶ q) ∨ ¬(p ⟶ q)" by (rule disjI2)
+     show "False" using 1 4 by (rule notE)
+  qed
+  thus ?thesis proof (rule disjE)
+     assume "p ⟶ q" thus ?thesis by (rule disjI1)
+  next
+     assume 1: "¬(p ⟶ q)"
+    have "q ⟶ p" proof (rule impI)
+      assume 2: q
+      have 3: "p ⟶ q" proof (rule impI)
+        assume p show q using 2 .
+      qed
+      show p using 1 3 by (rule notE)
+    qed
+    thus ?thesis by (rule disjI2)
    qed
+qed
+(* pabalagon gleherlop *)
+lemma ejercicio_58_2:
+  "(p ⟶ q) ∨ (q ⟶ p)"
+proof (rule ccontr)
+  assume 1: "¬((p ⟶ q) ∨ (q ⟶ p))"
+  hence 1: "(p ∧ ¬q) ∧ (q ∧ ¬p)" by simp
+  hence "p ∧ ¬q" ..
+  hence 2: p ..
+  have "q ∧ ¬p" using 1 ..
+  hence 3: "¬p" ..
+  show False using 3 2 by (rule notE)
+qed
+(* benber cammonagu *)
+lemma ejercicio_58_1:
+  "(p ⟶ q) ∨ (q ⟶ p)"
+proof (rule ccontr)
+  assume "¬ ((p ⟶ q) ∨ (q ⟶ p))"
+  hence 1: "¬(p ⟶ q) ∧ ¬(q ⟶ p)" by (rule ejercicio_46_1)
+  have "p ∨ ¬p" by (rule ejercicio_52_1)
+  moreover {
+    assume "p"
+    hence "q ⟶ p" by (rule ejercicio_7_1)
+    have "¬(q ⟶ p)" using 1 by (rule conjunct2)
+    hence "False" using `q ⟶ p` by (rule notE)
+  }
+  moreover {
+    assume "¬p"
+    hence "p ⟶ q" by (rule ejercicio_40_1)
+    have "¬(p ⟶ q)" using 1 by (rule conjunct1)
+    hence "False" using `p ⟶ q` by (rule notE)
+  }
+  ultimately show "False" by (rule disjE)
+  moreover {
+    assume "p"
+    hence "q ⟶ p" by (rule ejercicio_7_1)
+    have "¬(q ⟶ p)" using 1 by (rule conjunct2)
+    hence "False" using `q ⟶ p` by (rule notE)
+  }
+qed
+(* alfmarcua *)
+lemma ejercicio_58_3:
+  "(p ⟶ q) ∨ (q ⟶ p)"
+proof (rule disjE)
+  show "p ∨ ¬ p" by (rule ejercicio_52)
+next
+  assume "¬p"
+  then have "p ⟶ q" by (rule ejercicio_40)
+  then show ?thesis by (rule disjI1)
+next
+  assume "p"
+  then have "q ⟶ p" by (rule ejercicio_7)
+  then show ?thesis by (rule disjI2)
 qed
 end
 </source>

De Razonamiento automático (2018-19)

Revisión del 15:12 28 feb 2019