Ver el código de «GLC T2R2b» - DAO (Demostración asistida por ordenador)

<source lang="isabelle">
header {* T2R2b: Argumentación en lógica de primer orden *}

theory T2R2b
imports Main 
begin

text {* --------------------------------------------------------------- 
  Ejercicio 16. Formalizar, y decidir la corrección, del siguiente
  argumento 
     Supongamos conocidos los siguientes hechos acerca del número de
     aprobados de dos asignaturas A y B: 
     * Si todos los alumnos aprueban la asignatura A, entonces todos
       aprueban la asignatura B.
     * Si algún delegado de la clase aprueba A y B, entonces todos los 
       alumnos aprueban A.
     * Si nadie aprueba B, entonces ningún delegado aprueba A.
     * Si Manuel no aprueba B, entonces nadie aprueba B.
     Por tanto, si Manuel es un delegado y aprueba la asignatura A,
     entonces todos los alumnos aprueban las asignaturas A y B.
  Usar A(x,y) para x aprueba la asignatura y
       D(x)   para x es delegado
       m      para Manuel
       a      para la asignatura A
       b      para la asignatura B
   ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_16a:
  assumes "(∀x. A(x,a)) ⟶ (∀x. A(x,b))"
          "(∃x. D(x) ∧ A(x,a) ∧ A(x,b)) ⟶ (∀x. A(x,a))"
          "(∀x. ¬A(x,b)) ⟶ (∀x. D(x) ⟶ ¬A(x,a))"
          "¬A(m,b) ⟶ (∀x. ¬A(x,b))"
   shows  "D(m) ∧ A(m,a) ⟶ (∀x. A(x,a) ∧ A(x,b))"
using assms
by blast

-- "La demostración estructurada es"
lemma ejercicio_16b:
  assumes "(∀x. A(x,a)) ⟶ (∀x. A(x,b))"
          "(∃x. D(x) ∧ A(x,a) ∧ A(x,b)) ⟶ (∀x. A(x,a))"
          "(∀x. ¬A(x,b)) ⟶ (∀x. D(x) ⟶ ¬A(x,a))"
          "¬A(m,b) ⟶ (∀x. ¬A(x,b))"
   shows  "D(m) ∧ A(m,a) ⟶ (∀x. A(x,a) ∧ A(x,b))"
proof
  assume "D(m) ∧ A(m,a)"
  hence "D(m)" ..
  have "A(m,a)" using `D(m) ∧ A(m,a)` ..
  have "A(m,b)"
  proof (rule ccontr)
    assume "¬A(m,b)"
    with assms(4) have "∀x. ¬A(x,b)" ..
    with assms(3) have "∀x. D(x) ⟶ ¬A(x,a)" ..
    hence "D(m) ⟶ ¬A(m,a)" ..
    hence "¬A(m,a)" using `D(m)` ..
    thus False using `A(m,a)` ..
  qed
  with `A(m,a)` have "A(m,a) ∧ A(m,b)" ..
  with `D(m)` have "D(m) ∧ A(m,a) ∧ A(m,b)" ..
  hence "∃x. D(x) ∧ A(x,a) ∧ A(x,b)" ..
  with assms(2) have "∀x. A(x,a)" ..
  with assms(1) have "∀x. A(x,b)" ..
  show "∀x. A(x,a) ∧ A(x,b)"
  proof
    fix c
    show "A(c,a) ∧ A(c,b)"
    proof
      show "A(c,a)" using `∀x. A(x,a)` ..
    next
      show "A(c,b)" using `∀x. A(x,b)` ..
    qed
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_16c:
  assumes "(∀x. A(x,a)) ⟶ (∀x. A(x,b))"
          "(∃x. D(x) ∧ A(x,a) ∧ A(x,b)) ⟶ (∀x. A(x,a))"
          "(∀x. ¬A(x,b)) ⟶ (∀x. D(x) ⟶ ¬A(x,a))"
          "¬A(m,b) ⟶ (∀x. ¬A(x,b))"
   shows  "D(m) ∧ A(m,a) ⟶ (∀x. A(x,a) ∧ A(x,b))"
proof (rule impI)
  assume "D(m) ∧ A(m,a)"
  hence "D(m)" by (rule conjunct1)
  have "A(m,a)" using `D(m) ∧ A(m,a)` by (rule conjunct2)
  have "A(m,b)"
  proof (rule ccontr)
    assume "¬A(m,b)"
    with assms(4) have "∀x. ¬A(x,b)" by (rule mp)
    with assms(3) have "∀x. D(x) ⟶ ¬A(x,a)" by (rule mp)
    hence "D(m) ⟶ ¬A(m,a)" by (rule allE)
    hence "¬A(m,a)" using `D(m)` by (rule mp)
    thus False using `A(m,a)` by (rule notE)
  qed
  with `A(m,a)` have "A(m,a) ∧ A(m,b)" by (rule conjI)
  with `D(m)` have "D(m) ∧ A(m,a) ∧ A(m,b)" by (rule conjI)
  hence "∃x. D(x) ∧ A(x,a) ∧ A(x,b)" by (rule exI)
  with assms(2) have "∀x. A(x,a)" by (rule mp)
  with assms(1) have "∀x. A(x,b)" by (rule mp)
  show "∀x. A(x,a) ∧ A(x,b)"
  proof (rule allI)
    fix c
    show "A(c,a) ∧ A(c,b)"
    proof (rule conjI)
      show "A(c,a)" using `∀x. A(x,a)` by (rule allE)
    next
      show "A(c,b)" using `∀x. A(x,b)` by (rule allE)
    qed
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 17. Formalizar, y decidir la corrección, del siguiente
  argumento 
     En cierto país oriental se ha celebrado la fase final del
     campeonato mundial de fútbol. Cierto diario deportivo ha publicado
     las siguientes estadísticas de tan magno acontecimiento: 
     * A todos los porteros que no vistieron camiseta negra les marcó un
       gol algún delantero europeo.  
     * Algún portero jugó con botas blancas y sólo le marcaron goles
       jugadores con botas blancas.  
     * Ningún portero se marcó un gol a sí mismo. 
     * Ningún jugador con botas blancas vistió camiseta negra. 
     Por tanto, algún delantero europeo jugó con botas blancas.
  Usar P(x)   para x es portero
       D(x)   para x es delantero europeo 
       N(x)   para x viste camiseta negra
       B(x)   para x juega con botas blancas 
       M(x,y) para x marcó un gol a y
   ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_17a:
  assumes "∀x. P(x) ∧ ¬N(x) ⟶ (∃y. D(y) ∧ M(y,x))"
          "∃x. P(x) ∧ B(x) ∧ (∀y. M(y,x) ⟶ B(y))"
          "¬(∃x. P(x) ∧ M(x,x))"
          "¬(∃x. B(x) ∧ N(x))"
  shows   "∃x. D(x) ∧ B(x)"
using assms
by blast

-- "La demostración estructurada es"
lemma ejercicio_17b:
  assumes "∀x. P(x) ∧ ¬N(x) ⟶ (∃y. D(y) ∧ M(y,x))"
          "∃x. P(x) ∧ B(x) ∧ (∀y. M(y,x) ⟶ B(y))"
          "¬(∃x. P(x) ∧ M(x,x))"
          "¬(∃x. B(x) ∧ N(x))"
  shows   "∃x. D(x) ∧ B(x)"
proof -
  obtain a where a: "P(a) ∧ B(a) ∧ (∀y. M(y,a) ⟶ B(y))"
    using assms(2) ..
  have "P(a) ∧ ¬N(a)" 
  proof 
    show "P(a)" using a ..
  next
    have "B(a) ∧ (∀y. M(y,a) ⟶ B(y))" using a ..
    hence "B(a)" ..
    have "∀x. ¬(B(x) ∧ N(x))" using assms(4) by (rule no_ex)
    hence "¬(B(a) ∧ N(a))" ..
    show "¬N(a)"
    proof
      assume "N(a)"
      with `B(a)` have "B(a) ∧ N(a)" .. 
      with `¬(B(a) ∧ N(a))` show False ..
    qed
  qed
  hence "∃y. D(y) ∧ M(y,a)" 
  proof -
    have "P(a) ∧ ¬N(a) ⟶ (∃y. D(y) ∧ M(y,a))" using assms(1) ..
    thus "∃y. D(y) ∧ M(y,a)" using `P(a) ∧ ¬N(a)` ..
  qed
  then obtain b where "D(b) ∧ M(b,a)" ..
  have "D(b) ∧ B(b)" 
  proof
    show "D(b)" using `D(b) ∧ M(b,a)` ..
  next
    have "M(b,a)" using `D(b) ∧ M(b,a)` ..
    have "B(a) ∧ (∀y. M(y,a) ⟶ B(y))" using a ..
    hence "∀y. M(y,a) ⟶ B(y)" ..
    hence "M(b,a) ⟶ B(b)" ..
    thus "B(b)" using `M(b,a)` ..
  qed
  thus "∃x. D(x) ∧ B(x)" ..
qed

-- "La demostración estructurada es"
lemma ejercicio_17c:
  assumes "∀x. P(x) ∧ ¬N(x) ⟶ (∃y. D(y) ∧ M(y,x))"
          "∃x. P(x) ∧ B(x) ∧ (∀y. M(y,x) ⟶ B(y))"
          "¬(∃x. P(x) ∧ M(x,x))"
          "¬(∃x. B(x) ∧ N(x))"
  shows   "∃x. D(x) ∧ B(x)"
proof -
  obtain a where a: "P(a) ∧ B(a) ∧ (∀y. M(y,a) ⟶ B(y))"
    using assms(2) by (rule exE)
  have "P(a) ∧ ¬N(a)" 
  proof (rule conjI)
    show "P(a)" using a by (rule conjunct1)
  next
    have "B(a) ∧ (∀y. M(y,a) ⟶ B(y))" using a by (rule conjunct2)
    hence "B(a)" by (rule conjunct1)
    have "∀x. ¬(B(x) ∧ N(x))" using assms(4) by (rule no_ex)
    hence "¬(B(a) ∧ N(a))" by (rule allE)
    show "¬N(a)"
    proof (rule notI)
      assume "N(a)"
      with `B(a)` have "B(a) ∧ N(a)" by (rule conjI) 
      with `¬(B(a) ∧ N(a))` show False by (rule notE)
    qed
  qed
  hence "∃y. D(y) ∧ M(y,a)" 
  proof -
    have "P(a) ∧ ¬N(a) ⟶ (∃y. D(y) ∧ M(y,a))" 
      using assms(1) by (rule allE)
    thus "∃y. D(y) ∧ M(y,a)" using `P(a) ∧ ¬N(a)` by (rule mp)
  qed
  then obtain b where "D(b) ∧ M(b,a)" by (rule exE)
  have "D(b) ∧ B(b)" 
  proof (rule conjI)
    show "D(b)" using `D(b) ∧ M(b,a)` by (rule conjunct1)
  next
    have "M(b,a)" using `D(b) ∧ M(b,a)` by (rule conjunct2)
    have "B(a) ∧ (∀y. M(y,a) ⟶ B(y))" using a by (rule conjunct2)
    hence "∀y. M(y,a) ⟶ B(y)" by (rule conjunct2)
    hence "M(b,a) ⟶ B(b)" by (rule allE)
    thus "B(b)" using `M(b,a)` by (rule mp)
  qed
  thus "∃x. D(x) ∧ B(x)" by (rule exI) 
qed

text {* --------------------------------------------------------------- 
  Ejercicio 18. Formalizar, y decidir la corrección, del siguiente
  argumento 
     Las relaciones de parentesco verifican la siguientes propiedades
     generales:  
     * Si x es hermano de y, entonces y es hermano de x. 
     * Todo el mundo es hijo de alguien. 
     * Nadie es hijo del hermano de su padre. 
     * Cualquier padre de una persona es también padre de todos los
       hermanos de esa persona. 
     * Nadie es hijo ni hermano de sí mismo. 
     Tenemos los siguientes miembros de la familia Peláez: Don Antonio,
     Don Luis, Antoñito y Manolito y sabemos que Don Antonio y Don Luis
     son hermanos, Antoñito y Manolito son hermanos, y Antoñito es hijo
     de Don Antonio. Por tanto, Don Luis no es el padre de Manolito.
  Usar A       para Don Antonio
       He(x,y) para x es hermano de y 
       Hi(x,y) para x es hijo de y  
       L       para Don Luis
       a       para Antoñito
       m       para Manolito
   ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_18a:
  assumes "∀x y. He(x,y) ⟶ He(y,x)"
          "∀x. ∃y. Hi(x,y)"
          "∀x y z. Hi(x,y) ∧ He(z,y) ⟶ ¬Hi(x,z)"
          "∀x y. Hi(x,y) ⟶ (∀z. He(z,x) ⟶ Hi(z,y))"
          "∀x. ¬Hi(x,x) ∧ ¬He(x,x)"
          "He(A,L)"
          "He(a,m)"
          "Hi(a,A)"
  shows   "¬Hi(m,L)"
using assms
by blast

-- "La demostración estructurada es"
lemma ejercicio_18b:
  assumes "∀x y. He(x,y) ⟶ He(y,x)"                  
          "∀x. ∃y. Hi(x,y)"                          
          "∀x y z. Hi(x,y) ∧ He(z,y) ⟶ ¬Hi(x,z)"
          "∀x y. Hi(x,y) ⟶ (∀z. He(z,x) ⟶ Hi(z,y))"
          "∀x. ¬Hi(x,x) ∧ ¬He(x,x)"
          "He(A,L)"
          "He(a,m)"
          "Hi(a,A)"
  shows   "¬Hi(m,L)"
proof
  assume "Hi(m,L)"
  have "He(L,A)"
  proof -
    have "∀y. He(A,y) ⟶ He(y,A)" using assms(1) ..
    hence "He(A,L) ⟶ He(L,A)" ..
    thus "He(L,A)" using assms(6) ..
  qed
  have "Hi(a,L)"
  proof -
    have "∀y. Hi(m,y) ⟶ (∀z. He(z,m) ⟶ Hi(z,y))" using assms(4) ..
    hence "Hi(m,L) ⟶ (∀z. He(z,m) ⟶ Hi(z,L))" ..
    hence "∀z. He(z,m) ⟶ Hi(z,L)" using `Hi(m,L)` ..
    hence "He(a,m) ⟶ Hi(a,L)" ..
    thus "Hi(a,L)" using assms(7) ..
  qed 
  have "¬Hi(a,L)"
  proof -
    have "Hi(a,A) ∧ He(L,A)" using assms(8) `He(L,A)` .. 
    have "∀y z. Hi(a,y) ∧ He(z,y) ⟶ ¬Hi(a,z)" using assms(3) ..
    hence "∀z. Hi(a,A) ∧ He(z,A) ⟶ ¬Hi(a,z)" ..
    hence "Hi(a,A) ∧ He(L,A) ⟶ ¬Hi(a,L)" ..
    thus "¬Hi(a,L)" using `Hi(a,A) ∧ He(L,A)` ..
  qed
  thus False using `Hi(a,L)` ..
qed

-- "La demostración detallada es"
lemma ejercicio_18c:
  assumes "∀x y. He(x,y) ⟶ He(y,x)"                  
          "∀x. ∃y. Hi(x,y)"                          
          "∀x y z. Hi(x,y) ∧ He(z,y) ⟶ ¬Hi(x,z)"
          "∀x y. Hi(x,y) ⟶ (∀z. He(z,x) ⟶ Hi(z,y))"
          "∀x. ¬Hi(x,x) ∧ ¬He(x,x)"
          "He(A,L)"
          "He(a,m)"
          "Hi(a,A)"
  shows   "¬Hi(m,L)"
proof (rule notI)
  assume "Hi(m,L)"
  have "He(L,A)"
  proof -
    have "∀y. He(A,y) ⟶ He(y,A)" using assms(1) by (rule allE)
    hence "He(A,L) ⟶ He(L,A)" by (rule allE)
    thus "He(L,A)" using assms(6) by (rule mp)
  qed
  have "Hi(a,L)"
  proof -
    have "∀y. Hi(m,y) ⟶ (∀z. He(z,m) ⟶ Hi(z,y))" 
      using assms(4) by (rule allE)
    hence "Hi(m,L) ⟶ (∀z. He(z,m) ⟶ Hi(z,L))" by (rule allE)
    hence "∀z. He(z,m) ⟶ Hi(z,L)" using `Hi(m,L)` by (rule mp)
    hence "He(a,m) ⟶ Hi(a,L)" by (rule allE)
    thus "Hi(a,L)" using assms(7) by (rule mp)
  qed 
  have "¬Hi(a,L)"
  proof -
    have "Hi(a,A) ∧ He(L,A)" using assms(8) `He(L,A)` by (rule conjI) 
    have "∀y z. Hi(a,y) ∧ He(z,y) ⟶ ¬Hi(a,z)" 
      using assms(3) by (rule allE)
    hence "∀z. Hi(a,A) ∧ He(z,A) ⟶ ¬Hi(a,z)" by (rule allE)
    hence "Hi(a,A) ∧ He(L,A) ⟶ ¬Hi(a,L)" by (rule allE)
    thus "¬Hi(a,L)" using `Hi(a,A) ∧ He(L,A)` by (rule mp)
  qed
  thus False using `Hi(a,L)` by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 19. [Problema del apisonador de Schubert (en inglés, 
  "Schubert’s steamroller")] Formalizar, y decidir la corrección, del
  siguiente argumento 
     Si uno de los miembros del club afeita a algún otro (incluido a
     sí mismo), entonces todos los miembros del club lo han afeitado
     a él (aunque no necesariamente al mismo tiempo). Guido, Lorenzo,
     Petruccio y Cesare pertenecen al club de barberos. Guido ha
     afeitado a Cesare. Por tanto, Petruccio ha afeitado a Lorenzo.
  Usar g      para Guido
       l      para Lorenzo
       p      para Petruccio
       c      para Cesare
       B(x)   para x es un miembro del club de barberos
       A(x,y) para x ha afeitado a y
   ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_19a:
  assumes "∀x. B(x) ∧ (∃y. B(y) ∧ A(x,y)) ⟶ (∀z. B(z) ⟶ A(z,x))"
          "B(g)" 
          "B(l)" 
          "B(p)" 
          "B(c)"
          "A(g,c)"
  shows   "A(p,l)"
using assms
by meson

-- "La demostración estructurada es"
lemma ejercicio_19b:
  assumes "∀x. B(x) ∧ (∃y. B(y) ∧ A(x,y)) ⟶ (∀z. B(z) ⟶ A(z,x))"
          "B(g)" 
          "B(l)" 
          "B(p)" 
          "B(c)"
          "A(g,c)"
  shows   "A(p,l)"
proof -
  have "A(l,g)"
  proof -
    have "B(g) ∧ (∃y. B(y) ∧ A(g,y)) ⟶ (∀z. B(z) ⟶ A(z,g))" 
      using assms(1) ..
    have "B(c) ∧ A(g,c)" using assms(5,6) ..
    hence "(∃y. B(y) ∧ A(g,y))" ..
    with assms(2) have "B(g) ∧ (∃y. B(y) ∧ A(g,y))" .. 
    with `B(g) ∧ (∃y. B(y) ∧ A(g,y)) ⟶ (∀z. B(z) ⟶ A(z,g))` 
    have "(∀z. B(z) ⟶ A(z,g))" ..
    hence "B(l) ⟶ A(l,g)" ..
    thus "A(l,g)" using assms(3) ..
  qed
  have "B(l) ∧ (∃y. B(y) ∧ A(l,y)) ⟶ (∀z. B(z) ⟶ A(z,l))" 
    using assms(1) ..
  have "B(g) ∧ A(l,g)" using assms(2) `A(l,g)` ..
  hence "(∃y. B(y) ∧ A(l,y))" ..
  with assms(3) have "B(l) ∧ (∃y. B(y) ∧ A(l,y))" .. 
  with `B(l) ∧ (∃y. B(y) ∧ A(l,y)) ⟶ (∀z. B(z) ⟶ A(z,l))` 
  have "(∀z. B(z) ⟶ A(z,l))" ..
  hence "B(p) ⟶ A(p,l)" ..
  thus "A(p,l)" using assms(4) ..
qed

-- "La demostración detallada es"
lemma ejercicio_19c:
  assumes "∀x. B(x) ∧ (∃y. B(y) ∧ A(x,y)) ⟶ (∀z. B(z) ⟶ A(z,x))"
          "B(g)" 
          "B(l)" 
          "B(p)" 
          "B(c)"
          "A(g,c)"
  shows   "A(p,l)"
proof -
  have "A(l,g)"
  proof -
    have "B(g) ∧ (∃y. B(y) ∧ A(g,y)) ⟶ (∀z. B(z) ⟶ A(z,g))" 
      using assms(1) by (rule allE)
    have "B(c) ∧ A(g,c)" using assms(5,6) by (rule conjI)
    hence "(∃y. B(y) ∧ A(g,y))" by (rule exI)
    with assms(2) have "B(g) ∧ (∃y. B(y) ∧ A(g,y))" by (rule conjI) 
    with `B(g) ∧ (∃y. B(y) ∧ A(g,y)) ⟶ (∀z. B(z) ⟶ A(z,g))` 
    have "(∀z. B(z) ⟶ A(z,g))" by (rule mp)
    hence "B(l) ⟶ A(l,g)" by (rule allE)
    thus "A(l,g)" using assms(3) by (rule mp)
  qed
  have "B(l) ∧ (∃y. B(y) ∧ A(l,y)) ⟶ (∀z. B(z) ⟶ A(z,l))" 
    using assms(1) by (rule allE)
  have "B(g) ∧ A(l,g)" using assms(2) `A(l,g)` by (rule conjI)
  hence "(∃y. B(y) ∧ A(l,y))" by (rule exI)
  with assms(3) have "B(l) ∧ (∃y. B(y) ∧ A(l,y))" by (rule conjI) 
  with `B(l) ∧ (∃y. B(y) ∧ A(l,y)) ⟶ (∀z. B(z) ⟶ A(z,l))` 
  have "(∀z. B(z) ⟶ A(z,l))" by (rule mp)
  hence "B(p) ⟶ A(p,l)" by (rule allE)
  thus "A(p,l)" using assms(4) by (rule mp)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 20. Formalizar, y decidir la corrección, del siguiente
  argumento 
     Carlos afeita a todos los habitantes de Las Chinas que no se
     afeitan a sí mismo y sólo a ellos. Carlos es un habitante de las
     Chinas. Por consiguiente, Carlos no afeita a nadie.
  Usar A(x,y) para x afeita a y
       C(x)   para x es un habitante de Las Chinas
       c      para Carlos
   ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_20a:
  assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)"
          "C(c)"
  shows   "¬(∃x. A(c,x))"
using assms
by blast

-- "La demostración estructurada es"
lemma ejercicio_20b:
  assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)"
          "C(c)"
  shows   "¬(∃x. A(c,x))"
proof -
  have 1: "A(c,c) ⟷ C(c) ∧ ¬A(c,c)" using assms(1) ..
  have "A(c,c)"
  proof (rule ccontr)
    assume "¬A(c,c)"
    with assms(2) have "C(c) ∧ ¬A(c,c)" ..
    with 1 have "A(c,c)" .. 
    with `¬A(c,c)` show False ..
  qed
  have "¬A(c,c)"
  proof -
    have "C(c) ∧ ¬A(c,c)" using 1 `A(c,c)` ..
    thus "¬A(c,c)" ..
  qed
  thus "¬(∃x. A(c,x))" using `A(c,c)` ..
qed

-- "La demostración detallada es"
lemma ejercicio_20c:
  assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)"
          "C(c)"
  shows   "¬(∃x. A(c,x))"
proof -
  have 1: "A(c,c) ⟷ C(c) ∧ ¬A(c,c)" using assms(1) by (rule allE)
  have "A(c,c)"
  proof (rule ccontr)
    assume "¬A(c,c)"
    with assms(2) have "C(c) ∧ ¬A(c,c)" by (rule conjI)
    with 1 have "A(c,c)" by (rule iffD2)
    with `¬A(c,c)` show False by (rule notE)
  qed
  have "¬A(c,c)"
  proof -
    have "C(c) ∧ ¬A(c,c)" using 1 `A(c,c)` by (rule iffD1)
    thus "¬A(c,c)" by (rule conjunct2)
  qed
  thus "¬(∃x. A(c,x))" using `A(c,c)` by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 21. Formalizar, y decidir la corrección, del siguiente
  argumento
     Quien desprecia a todos los fanáticos desprecia también a todos los
     políticos. Alguien no desprecia a un determinado político. Por
     consiguiente, hay un fanático al que no todo el mundo desprecia.
   Usar D(x,y) para x desprecia a y
        F(x)   para x es fanático
        P(x)   para x es político
   ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_21a:
  assumes "∀x. (∀y. F(y) ⟶ D(x,y)) ⟶  (∀y. P(y) ⟶ D(x,y))"
          "∃x y. P(y) ∧ ¬D(x,y)"
  shows   "∃x. F(x) ∧ ¬(∀y. D(y,x))"
using assms
by blast

-- "La demostración semiautomática es"
lemma ejercicio_21b:
  assumes "∀x. (∀y. F(y) ⟶ D(x,y)) ⟶  (∀y. P(y) ⟶ D(x,y))"
          "∃x y. P(y) ∧ ¬D(x,y)"
  shows   "∃x. F(x) ∧ ¬(∀y. D(y,x))"
proof -
  obtain a where "∃y. P(y) ∧ ¬D(a,y)" using assms(2) ..
  then obtain b where "P(b) ∧ ¬D(a,b)" ..
  hence "¬(∀y. P(y) ⟶ D(a,y))" by auto
  have "(∀y. F(y) ⟶ D(a,y)) ⟶  (∀y. P(y) ⟶ D(a,y))" using assms(1) ..
  hence "¬(∀y. F(y) ⟶ D(a,y))" using `¬(∀y. P(y) ⟶ D(a,y))` by (rule mt)
  hence "∃y. ¬(F(y) ⟶ D(a,y))" by (rule no_para_todo)  
  then obtain c where "¬(F(c) ⟶ D(a,c))" ..
  hence "F(c) ∧ ¬(∀y. D(y,c))" by auto
  thus "∃x. F(x) ∧ ¬(∀y. D(y,x))" ..
qed

-- "En la demostración estructurada usaremos el siguiente lema"
lemma no_implica: 
  assumes "¬(p ⟶ q)"
  shows   "p ∧ ¬q"
using assms
by auto

-- "La demostración estructurada del lema es"
lemma no_implica_1: 
  assumes "¬(p ⟶ q)"
  shows   "p ∧ ¬q"
proof
  show "p"
  proof (rule ccontr)
    assume "¬p"
    have "p ⟶ q"
    proof
      assume "p"
      with `¬p` show "q" .. 
    qed
    with assms show False ..
  qed
next
  show "¬q"
  proof
    assume "q"
    have "p ⟶ q"
    proof
      assume "p"
      show "q" using `q` .
    qed
    with assms show False ..
  qed
qed

-- "La demostración detallada del lema es"
lemma no_implica_2: 
  assumes "¬(p ⟶ q)"
  shows   "p ∧ ¬q"
proof (rule conjI)
  show "p"
  proof (rule ccontr)
    assume "¬p"
    have "p ⟶ q"
    proof (rule impI)
      assume "p"
      with `¬p` show "q" by (rule notE) 
    qed
    with assms show False by (rule notE) 
  qed
next
  show "¬q"
  proof (rule notI)
    assume "q"
    have "p ⟶ q"
    proof (rule impI)
      assume "p"
      show "q" using `q` by this
    qed
    with assms show False by (rule notE)
  qed
qed

-- "La demostración estructurada es"
lemma ejercicio_21c:
  assumes "∀x. (∀y. F(y) ⟶ D(x,y)) ⟶  (∀y. P(y) ⟶ D(x,y))"
          "∃x y. P(y) ∧ ¬D(x,y)"
  shows   "∃x. F(x) ∧ ¬(∀y. D(y,x))"
proof -
  obtain a where "∃y. P(y) ∧ ¬D(a,y)" using assms(2) ..
  then obtain b where b: "P(b) ∧ ¬D(a,b)" ..
  have "¬(∀y. P(y) ⟶ D(a,y))"
  proof
    assume "∀y. P(y) ⟶ D(a,y)"
    hence "P(b) ⟶ D(a,b)" ..
    have "P(b)" using b ..
    with `P(b) ⟶ D(a,b)` have "D(a,b)" ..
    have "¬D(a,b)" using b ..
    thus False using `D(a,b)` ..
  qed
  have "(∀y. F(y) ⟶ D(a,y)) ⟶  (∀y. P(y) ⟶ D(a,y))" using assms(1) ..
  hence "¬(∀y. F(y) ⟶ D(a,y))" using `¬(∀y. P(y) ⟶ D(a,y))` by (rule mt)
  hence "∃y. ¬(F(y) ⟶ D(a,y))" by (rule no_para_todo)  
  then obtain c where c: "¬(F(c) ⟶ D(a,c))" ..
  have "F(c) ∧ ¬(∀y. D(y,c))" 
  proof
    have "F(c) ∧ ¬D(a,c)" using c by (rule no_implica)
    thus "F(c)" ..
  next
    show "¬(∀y. D(y,c))"
    proof
      assume "∀y. D(y,c)"
      hence "D(a,c)" ..
      have "F(c) ∧ ¬D(a,c)" using c by (rule no_implica)
      hence "¬D(a,c)" ..
      thus False using `D(a,c)` ..
    qed
  qed
  thus "∃x. F(x) ∧ ¬(∀y. D(y,x))" ..
qed

-- "La demostración detallada es"
lemma ejercicio_21d:
  assumes "∀x. (∀y. F(y) ⟶ D(x,y)) ⟶  (∀y. P(y) ⟶ D(x,y))"
          "∃x y. P(y) ∧ ¬D(x,y)"
  shows   "∃x. F(x) ∧ ¬(∀y. D(y,x))"
proof -
  obtain a where "∃y. P(y) ∧ ¬D(a,y)" using assms(2) by (rule exE)
  then obtain b where b: "P(b) ∧ ¬D(a,b)" by (rule exE)
  have "¬(∀y. P(y) ⟶ D(a,y))"
  proof (rule notI)
    assume "∀y. P(y) ⟶ D(a,y)"
    hence "P(b) ⟶ D(a,b)" by (rule allE)
    have "P(b)" using b by (rule conjunct1)
    with `P(b) ⟶ D(a,b)` have "D(a,b)" by (rule mp)
    have "¬D(a,b)" using b by (rule conjunct2)
    thus False using `D(a,b)` by (rule notE)
  qed
  have "(∀y. F(y) ⟶ D(a,y)) ⟶  (∀y. P(y) ⟶ D(a,y))" 
    using assms(1) by (rule allE)
  hence "¬(∀y. F(y) ⟶ D(a,y))" using `¬(∀y. P(y) ⟶ D(a,y))` by (rule mt)
  hence "∃y. ¬(F(y) ⟶ D(a,y))" by (rule no_para_todo)  
  then obtain c where c: "¬(F(c) ⟶ D(a,c))" by (rule exE)
  have "F(c) ∧ ¬(∀y. D(y,c))" 
  proof (rule conjI)
    have "F(c) ∧ ¬D(a,c)" using c by (rule no_implica)
    thus "F(c)" by (rule conjunct1)
  next
    show "¬(∀y. D(y,c))"
    proof (rule notI)
      assume "∀y. D(y,c)"
      hence "D(a,c)" by (rule allE)
      have "F(c) ∧ ¬D(a,c)" using c by (rule no_implica)
      hence "¬D(a,c)" by (rule conjunct2)
      thus False using `D(a,c)` by (rule notE)
    qed
  qed
  thus "∃x. F(x) ∧ ¬(∀y. D(y,x))" by (rule exI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 22. Formalizar, y decidir la corrección, del siguiente
  argumento
     El hombre puro ama todo lo que es puro. Por tanto, el hombre puro
     se ama a sí mismo.
  Usar A(x,y) para x ama a y
       H(x)   para x es un hombre
       P(x)   para x es puro
   ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_22a:
  assumes "∀x. H(x) ∧ P(x) ⟶ (∀y. P(y) ⟶ A(x,y))"
  shows   "∀x. H(x) ∧ P(x) ⟶ A(x,x)"
using assms
by auto

-- "La demostración estructurada es"
lemma ejercicio_22b:
  assumes "∀x. H(x) ∧ P(x) ⟶ (∀y. P(y) ⟶ A(x,y))"
  shows   "∀x. H(x) ∧ P(x) ⟶ A(x,x)"
proof
  fix b
  show "H(b) ∧ P(b) ⟶ A(b,b)"
  proof
    assume "H(b) ∧ P(b)"
    hence "P(b)" ..
    have "H(b) ∧ P(b) ⟶ (∀y. P(y) ⟶ A(b,y))" using assms ..
    hence "∀y. P(y) ⟶ A(b,y)" using `H(b) ∧ P(b)` ..
    hence "P(b) ⟶ A(b,b)" ..
    thus "A(b,b)" using `P(b)` ..
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_22c:
  assumes "∀x. H(x) ∧ P(x) ⟶ (∀y. P(y) ⟶ A(x,y))"
  shows   "∀x. H(x) ∧ P(x) ⟶ A(x,x)"
proof (rule allI)
  fix b
  show "H(b) ∧ P(b) ⟶ A(b,b)"
  proof (rule impI)
    assume "H(b) ∧ P(b)"
    hence "P(b)" by (rule conjunct2)
    have "H(b) ∧ P(b) ⟶ (∀y. P(y) ⟶ A(b,y))" 
      using assms by (rule allE)
    hence "∀y. P(y) ⟶ A(b,y)" using `H(b) ∧ P(b)` by (rule mp)
    hence "P(b) ⟶ A(b,b)" by (rule allE)
    thus "A(b,b)" using `P(b)` by (rule mp)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 23. Formalizar, y decidir la corrección, del siguiente
  argumento
     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
   ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_23a:
  assumes "¬(∃x. P(x) ∧ R(x))"
          "∀x. P(x) ∧ ¬Q(x) ⟶ R(x)"
  shows   "P(a) ⟶ Q(a)"
using assms
by auto

-- "La demostración estructurada es"
lemma ejercicio_23b:
  assumes "¬(∃x. P(x) ∧ R(x))"
          "∀x. P(x) ∧ ¬Q(x) ⟶ R(x)"
  shows   "P(a) ⟶ Q(a)"
proof
  assume "P(a)"
  show "Q(a)"
  proof (rule ccontr)
    assume "¬Q(a)"
    with `P(a)` have "P(a) ∧ ¬Q(a)" ..
    have "P(a) ∧ ¬Q(a) ⟶ R(a)" using assms(2) ..
    hence "R(a)" using `P(a) ∧ ¬Q(a)` ..
    with `P(a)` have "P(a) ∧ R(a)" ..
    hence "∃x. P(x) ∧ R(x)" ..
    with assms(1) show False ..
  qed
qed

-- "La demostración detallada es"
lemma ejercicio_23c:
  assumes "¬(∃x. P(x) ∧ R(x))"
          "∀x. P(x) ∧ ¬Q(x) ⟶ R(x)"
  shows   "P(a) ⟶ Q(a)"
proof (rule impI)
  assume "P(a)"
  show "Q(a)"
  proof (rule ccontr)
    assume "¬Q(a)"
    with `P(a)` have "P(a) ∧ ¬Q(a)" by (rule conjI)
    have "P(a) ∧ ¬Q(a) ⟶ R(a)" using assms(2) by (rule allE)
    hence "R(a)" using `P(a) ∧ ¬Q(a)` by (rule mp)
    with `P(a)` have "P(a) ∧ R(a)" by (rule conjI)
    hence "∃x. P(x) ∧ R(x)" by (rule exI)
    with assms(1) show False by (rule notE)
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 24. Formalizar, y decidir la corrección, del siguiente
  argumento
     1. Los lobos, zorros, pájaros, orugas y caracoles son animales y
        existen algunos ejemplares de estos animales. 
     2. También hay algunas semillas y las semillas son plantas. 
     3. A todo animal le gusta o bien comer todo tipo de plantas o bien
        le gusta comerse a todos los animales más pequeños que él mismo
        que gustan de comer algunas plantas. 
     4. Las orugas y los caracoles son mucho más pequeños que los
        pájaros, que son mucho más pequeños que los zorros que a su vez
        son mucho más pequeños que los lobos. 
     5. A los lobos no les gusta comer ni zorros ni semillas, mientras
        que a los pájaros les gusta comer orugas pero no caracoles. 
     6. Las orugas y los caracoles gustan de comer algunas plantas. 
     7. Luego, existe un animal al que le gusta comerse un animal al que
        le gusta comer semillas.  
  Usar A(x)    para x es un animal
       Ca(x)   para x es un caracol
       Co(x,y) para x le gusta comerse a y
       L(x)    para x es un lobo
       M(x,y)  para x es más pequeño que y
       Or(x)   para x es una oruga
       Pa(x)   para x es un pájaro
       Pl(x)   para x es una planta
       S(x)    para x es una semilla
       Z(x)    para x es un zorro
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_24a:
  assumes
   (*  1 *) "∀x. L(x) ⟶ A(x)"
   (*  2 *) "∀x. Z(x) ⟶ A(x)"
   (*  3 *) "∀x. Pa(x) ⟶ A(x)"
   (*  4 *) "∀x. Or(x) ⟶ A(x)"
   (*  5 *) "∀x. Ca(x) ⟶ A(x)"
   (*  6 *) "∃x. L(x)"
   (*  7 *) "∃x. Z(x)"
   (*  8 *) "∃x. Pa(x)"
   (*  9 *) "∃x. Or(x)"
   (* 10 *) "∃x. Ca(x)"
   (* 11 *) "∃x. S(x)"
   (* 12 *) "∀x. S(x) ⟶ Pl(x)"
   (* 13 *) "∀x. A(x) ⟶ 
                 (∀y. Pl(y) ⟶ Co(x,y)) ∨ 
                 (∀y. A(y) ∧ M(y,x) ∧ (∃z. Pl(z) ∧ Co(y,z)) ⟶ Co(x,y))"
   (* 14 *) "∀x y. Pa(y) ∧ (Ca(x) ∨ Or(x)) ⟶ M(x,y)"
   (* 15 *) "∀x y. Pa(x) ∧ Z(y) ⟶ M(x,y)"
   (* 16 *) "∀x y. Z(x) ∧ L(y) ⟶ M(x,y)"
   (* 17 *) "∀x y. L(x) ∧ (Z(y)∨ S(y)) ⟶ ¬Co(x,y)"
   (* 18 *) "∀x y. Pa(x) ∧ Or(y) ⟶ Co(x,y)"
   (* 19 *) "∀x y. Pa(x) ∧ Ca(y) ⟶ ¬Co(x,y)"
   (* 20 *) "∀x. Or(x) ∨ Ca(x) ⟶ (∃y. Pl(y) ∧ Co(x,y))"
  shows
   "∃x y. A(x) ∧ A(y) ∧ (∃z. S(z) ∧ Co(y,z) ∧ Co(x,y))"
using assms
by meson

-- "La demostración semiautomática es"
lemma ejercicio_24b:
  assumes
   (*  1 *) "∀x. L(x) ⟶ A(x)"
   (*  2 *) "∀x. Z(x) ⟶ A(x)"
   (*  3 *) "∀x. Pa(x) ⟶ A(x)"
   (*  4 *) "∀x. Or(x) ⟶ A(x)"
   (*  5 *) "∀x. Ca(x) ⟶ A(x)"
   (*  6 *) "∃x. L(x)"
   (*  7 *) "∃x. Z(x)"
   (*  8 *) "∃x. Pa(x)"
   (*  9 *) "∃x. Or(x)"
   (* 10 *) "∃x. Ca(x)"
   (* 11 *) "∃x. S(x)"
   (* 12 *) "∀x. S(x) ⟶ Pl(x)"
   (* 13 *) "∀x. A(x) ⟶ 
                 (∀y. Pl(y) ⟶ Co(x,y)) ∨ 
                 (∀y. A(y) ∧ M(y,x) ∧ (∃z. Pl(z) ∧ Co(y,z)) ⟶ Co(x,y))"
   (* 14 *) "∀x y. Pa(y) ∧ (Ca(x) ∨ Or(x)) ⟶ M(x,y)"
   (* 15 *) "∀x y. Pa(x) ∧ Z(y) ⟶ M(x,y)"
   (* 16 *) "∀x y. Z(x) ∧ L(y) ⟶ M(x,y)"
   (* 17 *) "∀x y. L(x) ∧ (Z(y)∨ S(y)) ⟶ ¬Co(x,y)"
   (* 18 *) "∀x y. Pa(x) ∧ Or(y) ⟶ Co(x,y)"
   (* 19 *) "∀x y. Pa(x) ∧ Ca(y) ⟶ ¬Co(x,y)"
   (* 20 *) "∀x. Or(x) ∨ Ca(x) ⟶ (∃y. Pl(y) ∧ Co(x,y))"
  shows
   "∃x y. A(x) ∧ A(y) ∧ (∃z. S(z) ∧ Co(y,z) ∧ Co(x,y))"
proof -
  obtain l where l: "L(l)" using assms(6) ..
  obtain z where z: "Z(z)" using assms(7) ..
  obtain p where p: "Pa(p)" using assms(8) ..
  obtain c where c: "Ca(c)" using assms(10) ..
  obtain s where s: "S(s)" using assms(11) ..
  have 1: "Co(p,s)" using p c s assms(3,5,12,13,14,19,20) by meson
  have 2: "¬Co(z,s)" using z l s assms(1,2,12,16,17,13) by meson 
  have 3: "M(p,z)" using p z assms(15) by auto
  have 4: "Co(z,p)" using z p s 1 2 3 assms(2,3,12,13) by meson
  hence "Co(z,p) ∧ Co(p,s)" using 1 .. 
  thus "∃x y. A(x) ∧ A(y) ∧ (∃z. S(z) ∧ Co(y,z) ∧ Co(x,y))" 
    using z p s assms(2,3) by meson
qed

lemma instancia:
  assumes "∀x. P(x) ⟶ Q(x)"
          "P(a)"
  shows   "Q(a)"
proof -
  have "P(a) ⟶ Q(a)" using assms(1) ..
  thus "Q(a)" using assms(2) ..
qed

lemma mt2:
  assumes "p ∧ q ∧ r ⟶ s"
          "p"
          "q"
          "¬s"
  shows   "¬r"
proof
  assume "r"
  with `q` have "q ∧ r" ..
  with `p` have "p ∧ q ∧ r" ..
  with assms(1) have "s" ..
  with `¬s` show False ..
qed

lemma mp3: 
  assumes "p ∧ q ∧ r ⟶ s"
          "p"
          "q"
          "r"
  shows   "s"
proof -
  have "q ∧ r" using assms(3,4) ..
  with `p` have "p ∧ q ∧ r" ..
  with assms(1) show "s" ..
qed

lemma conjI3:
  assumes "p"
          "q"
          "r"
  shows   "p ∧ q ∧ r"
proof -
  have "q ∧ r" using assms(2,3) ..
  with `p` show "p ∧ q ∧ r" ..
qed

-- "La demostración estructurada es"
lemma ejercicio_24c:
  assumes
   (*  1 *) "∀x. L(x) ⟶ A(x)"
   (*  2 *) "∀x. Z(x) ⟶ A(x)"
   (*  3 *) "∀x. Pa(x) ⟶ A(x)"
   (*  4 *) "∀x. Or(x) ⟶ A(x)"
   (*  5 *) "∀x. Ca(x) ⟶ A(x)"
   (*  6 *) "∃x. L(x)"
   (*  7 *) "∃x. Z(x)"
   (*  8 *) "∃x. Pa(x)"
   (*  9 *) "∃x. Or(x)"
   (* 10 *) "∃x. Ca(x)"
   (* 11 *) "∃x. S(x)"
   (* 12 *) "∀x. S(x) ⟶ Pl(x)"
   (* 13 *) "∀x. A(x) ⟶ 
                 (∀y. Pl(y) ⟶ Co(x,y)) ∨ 
                 (∀y. A(y) ∧ M(y,x) ∧ (∃z. Pl(z) ∧ Co(y,z)) ⟶ Co(x,y))"
   (* 14 *) "∀x y. Pa(y) ∧ (Ca(x) ∨ Or(x)) ⟶ M(x,y)"
   (* 15 *) "∀x y. Pa(x) ∧ Z(y) ⟶ M(x,y)"
   (* 16 *) "∀x y. Z(x) ∧ L(y) ⟶ M(x,y)"
   (* 17 *) "∀x y. L(x) ∧ (Z(y)∨ S(y)) ⟶ ¬Co(x,y)"
   (* 18 *) "∀x y. Pa(x) ∧ Or(y) ⟶ Co(x,y)"
   (* 19 *) "∀x y. Pa(x) ∧ Ca(y) ⟶ ¬Co(x,y)"
   (* 20 *) "∀x. Or(x) ∨ Ca(x) ⟶ (∃y. Pl(y) ∧ Co(x,y))"
  shows
   "∃x y. A(x) ∧ A(y) ∧ (∃z. S(z) ∧ Co(y,z) ∧ Co(x,y))"
proof -
  obtain l where l: "L(l)" using assms(6) ..
  obtain z where z: "Z(z)" using assms(7) ..
  obtain p where p: "Pa(p)" using assms(8) ..
  obtain c where c: "Ca(c)" using assms(10) ..
  obtain s where s: "S(s)" using assms(11) ..
  have 1: "Co(p,s)" 
  proof -
    have "¬Co(p,c)"
    proof -
      have "Pa(p) ∧ Ca(c)" using p c ..
      have "∀y. Pa(p) ∧ Ca(y) ⟶ ¬Co(p,y)" using assms(19) ..
      hence "Pa(p) ∧ Ca(c) ⟶ ¬Co(p,c)" ..
      thus "¬Co(p,c)" using `Pa(p) ∧ Ca(c)` .. 
    qed
    have "∃y. Pl(y) ∧ Co(c,y)" 
    proof -
      have "Or(c) ∨ Ca(c)" using c ..
      have "Or(c) ∨ Ca(c) ⟶ (∃y. Pl(y) ∧ Co(c,y))" using assms(20) ..
      thus "∃y. Pl(y) ∧ Co(c,y)" using `Or(c) ∨ Ca(c)` ..
    qed 
    have "M(c,p)"
    proof -
      have "∀y. Pa(y) ∧ (Ca(c) ∨ Or(c)) ⟶ M(c,y)" using assms(14) ..
      hence "Pa(p) ∧ (Ca(c) ∨ Or(c)) ⟶ M(c,p)" ..
      have "Ca(c) ∨ Or(c)" using c ..
      with p have "Pa(p) ∧ (Ca(c) ∨ Or(c))" ..
      with `Pa(p) ∧ (Ca(c) ∨ Or(c)) ⟶ M(c,p)` show "M(c,p)" ..
    qed
    show "Co(p,s)"
    proof -
      have "A(p)" using assms(3) p by (rule instancia)
      have "A(p) ⟶ (∀y. Pl(y) ⟶ Co(p,y)) ∨ 
                     (∀y. A(y) ∧ M(y,p) ∧ (∃z. Pl(z) ∧ Co(y,z)) ⟶ Co(p,y))"
        using assms(13) ..
      hence "(∀y. Pl(y) ⟶ Co(p,y)) ∨ 
             (∀y. A(y) ∧ M(y,p) ∧ (∃z. Pl(z) ∧ Co(y,z)) ⟶ Co(p,y))"
        using `A(p)` ..
      thus "Co(p,s)"
      proof
        assume "∀y. Pl(y) ⟶ Co(p,y)"
        hence "Pl(s) ⟶ Co(p,s)" ..
        have "Pl(s)" using assms(12) s by (rule instancia)
        with `Pl(s) ⟶ Co(p,s)` show "Co(p,s)" ..
      next
        assume "∀y. A(y) ∧ M(y,p) ∧ (∃z. Pl(z) ∧ Co(y,z)) ⟶ Co(p,y)"
        hence "A(c) ∧ M(c,p) ∧ (∃z. Pl(z) ∧ Co(c,z)) ⟶ Co(p,c)" ..
        have "Co(p,c)"
        proof -
          have "A(c)" using assms(5) c by (rule instancia)
          have "M(c,p) ∧ (∃z. Pl(z) ∧ Co(c,z))" 
            using `M(c,p)` `∃z. Pl(z) ∧ Co(c,z)` ..
          with `A(c)` have "A(c) ∧ M(c,p) ∧ (∃z. Pl(z) ∧ Co(c,z))" ..
          with `A(c) ∧ M(c,p) ∧ (∃z. Pl(z) ∧ Co(c,z)) ⟶ Co(p,c)`
          show "Co(p,c)" ..
        qed
        with `¬Co(p,c)` show "Co(p,s)" ..
      qed
    qed
  qed
  have 2: "¬Co(z,s)"
  proof -
    have "M(z,l)"
    proof -
      have "Z(z) ∧ L(l)" using z l ..
      have "∀y. Z(z) ∧ L(y) ⟶ M(z,y)" using assms(16) ..
      hence "Z(z) ∧ L(l) ⟶ M(z,l)" ..
      thus "M(z,l)" using `Z(z) ∧ L(l)` ..
    qed
    have "¬Co(l,z)" 
    proof -
      have "∀y. L(l) ∧ (Z(y)∨ S(y)) ⟶ ¬Co(l,y)" using assms(17) ..
      hence "L(l) ∧ (Z(z)∨ S(z)) ⟶ ¬Co(l,z)" ..
      have "Z(z)∨ S(z)" using z ..
      with l have "L(l) ∧ (Z(z)∨ S(z))" ..
      with `L(l) ∧ (Z(z)∨ S(z)) ⟶ ¬Co(l,z)` show "¬Co(l,z)" .. 
    qed
    have "¬Co(l,s)"
    proof -
      have "∀y. L(l) ∧ (Z(y)∨ S(y)) ⟶ ¬Co(l,y)" using assms(17) ..
      hence "L(l) ∧ (Z(s)∨ S(s)) ⟶ ¬Co(l,s)" ..
      have "Z(s)∨ S(s)" using s ..
      with l have "L(l) ∧ (Z(s)∨ S(s))" ..
      with `L(l) ∧ (Z(s)∨ S(s)) ⟶ ¬Co(l,s)` show "¬Co(l,s)" .. 
    qed
    show "¬Co(z,s)"
    proof -
      have "A(l)" using assms(1) l by (rule instancia)
      have "A(l) ⟶ (∀y. Pl(y) ⟶ Co(l,y)) ∨ 
                     (∀y. A(y) ∧ M(y,l) ∧ (∃z. Pl(z) ∧ Co(y,z)) ⟶ Co(l,y))"
        using assms(13) ..
      hence  "(∀y. Pl(y) ⟶ Co(l,y)) ∨ 
              (∀y. A(y) ∧ M(y,l) ∧ (∃z. Pl(z) ∧ Co(y,z)) ⟶ Co(l,y))"
        using `A(l)` ..
      thus "¬Co(z,s)"
      proof
        assume "∀y. Pl(y) ⟶ Co(l,y)"
        hence "Pl(s) ⟶ Co(l,s)" ..
        have "Pl(s)" using assms(12) s by (rule instancia)
        with `Pl(s) ⟶ Co(l,s)` have "Co(l,s)" ..
        with `¬Co(l,s)` show "¬Co(z,s)" ..
      next
        assume "∀y. A(y) ∧ M(y,l) ∧ (∃u. Pl(u) ∧ Co(y,u)) ⟶ Co(l,y)"
        hence zl: "A(z) ∧ M(z,l) ∧ (∃u. Pl(u) ∧ Co(z,u)) ⟶ Co(l,z)" ..
        have "A(z)" using assms(2) z by (rule instancia)
        have "¬(∃u. Pl(u) ∧ Co(z,u))" 
          using zl `A(z)` `M(z,l)` `¬Co(l,z)` by (rule mt2)
        show "¬Co(z,s)"
        proof
          assume "Co(z,s)"
          have "Pl(s)" using assms(12) s by (rule instancia)
          hence "Pl(s) ∧ Co(z,s)" using `Co(z,s)` ..
          hence "∃u. Pl(u) ∧ Co(z,u)" ..
          with `¬(∃u. Pl(u) ∧ Co(z,u))` show False ..
        qed 
      qed
    qed
  qed
  have 3: "M(p,z)"
  proof -
    have "Pa(p) ∧ Z(z)" using p z ..
    have "∀y. Pa(p) ∧ Z(y) ⟶ M(p,y)" using assms(15) ..
    hence "Pa(p) ∧ Z(z) ⟶ M(p,z)" ..
    thus "M(p,z)" using `Pa(p) ∧ Z(z)` ..
  qed
  have 4: "Co(z,p)"
  proof -
    have "A(z)" using assms(2) z by (rule instancia)
    have "A(z) ⟶ (∀y. Pl(y) ⟶ Co(z,y)) ∨ 
                   (∀y. A(y) ∧ M(y,z) ∧ (∃u. Pl(u) ∧ Co(y,u)) ⟶ Co(z,y))"
      using assms(13) ..
    hence "(∀y. Pl(y) ⟶ Co(z,y)) ∨ 
           (∀y. A(y) ∧ M(y,z) ∧ (∃u. Pl(u) ∧ Co(y,u)) ⟶ Co(z,y))"
      using `A(z)` ..
    thus "Co(z,p)"
    proof 
      assume "∀y. Pl(y) ⟶ Co(z,y)"
      hence "Pl(s) ⟶ Co(z,s)" ..
      have "Pl(s)" using assms(12) s by (rule instancia)
      with `Pl(s) ⟶ Co(z,s)` have "Co(z,s)" ..
      with `¬Co(z,s)` show "Co(z,p)" ..
    next
      assume "∀y. A(y) ∧ M(y,z) ∧ (∃u. Pl(u) ∧ Co(y,u)) ⟶ Co(z,y)"
      hence pz: "A(p) ∧ M(p,z) ∧ (∃u. Pl(u) ∧ Co(p,u)) ⟶ Co(z,p)" ..
      have "A(p)" using assms(3) p by (rule instancia)
      have "∃u. Pl(u) ∧ Co(p,u)"
      proof -
        have "Pl(s)" using assms(12) s by (rule instancia)
        hence "Pl(s) ∧ Co(p,s)" using `Co(p,s)` ..  
        thus "∃u. Pl(u) ∧ Co(p,u)" ..
      qed
      show "Co(z,p)" using pz `A(p)` `M(p,z)` `∃u. Pl(u) ∧ Co(p,u)`
        by (rule mp3)
    qed
  qed
  hence "Co(z,p) ∧ Co(p,s)" using 1 .. 
  show "∃x y. A(x) ∧ A(y) ∧ (∃u. S(u) ∧ Co(y,u) ∧ Co(x,y))" 
  proof -
    have "A(z)" using assms(2) z by (rule instancia)
    have "A(p)" using assms(3) p by (rule instancia)
    have "S(s) ∧ Co(p,s) ∧ Co(z,p)" using s `Co(p,s)` `Co(z,p)` 
      by (rule conjI3)
    hence "∃u. S(u) ∧ Co(p,u) ∧ Co(z,p)" ..
    have "A(z) ∧ A(p) ∧ (∃u. S(u) ∧ Co(p,u) ∧ Co(z,p))"
      using `A(z)` `A(p)` `∃u. S(u) ∧ Co(p,u) ∧ Co(z,p)`
      by (rule conjI3)
    hence "∃y. A(z) ∧ A(y) ∧ (∃u. S(u) ∧ Co(y,u) ∧ Co(z,y))" ..
    thus "∃x y. A(x) ∧ A(y) ∧ (∃u. S(u) ∧ Co(y,u) ∧ Co(x,y))" ..
  qed
qed

end
</source>