Relación 11

header {* R11: Deducción natural de primer orden *}

theory R11
imports Main 
begin

text {*
  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
  · mp:         ⟦P ⟶ Q; P⟧ ⟹ Q 
  · 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

  · 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 continuación.
  *}

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

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

lemma no_ex: "¬(∃x. P(x)) ⟹ ∀x. ¬P(x)"
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 1. Demostrar
       P a ⟶ (∃x. Q x) ⊢ ∃x. P a ⟶ Q x 
  ------------------------------------------------------------------ *}

-- "maresccas4 irealetei" (* Una! nos ha salido Una!!! *)
lemma ej_1_auto:
  assumes " P a ⟶ (∃x. Q x)"
  shows "∃x. P a ⟶ Q x"
using assms by auto

lemma ej_1:
  fixes P Q :: "'b ⇒ bool" 
  assumes 0:"P a ⟶ (∃x. Q x)"
  shows   "∃x. P a ⟶ Q x"
proof -
  have "¬(P a) ∨ P a" by (rule excluded_middle)
  then show "∃x. P a ⟶ Q x"
  proof (rule disjE)
      {assume 2:"(P a)"
        have 4: "∃x. Q x" using 0 2 ..
        obtain b where "Q b" using 4 by (rule exE)
        then have "P a ⟶ Q b" ..
        then show "∃x. P a ⟶ Q x" by (rule exI)}
      next 
       {assume 2:"¬(P a)"
        {assume "¬(∃x. P a ⟶ Q x)"
         then have 3: "∀x. ¬(P a ⟶ Q x)" by (rule no_ex)
         fix b
         have "¬(P a ⟶ Q b)" using 3 ..
         then have "P a ∧ ¬Q b" by (rule Meson.not_impD)
         then have 4:"P a" ..
         have "False" using 2 4 ..}
        then show " ∃x. P a ⟶ Q x" by (rule ccontr)}
       qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 2. Demostrar
       {∀x y z. R x y ∧ R y z ⟶ R x z, 
        ∀x. ¬(R x x)}
       ⊢ ∀x y. R x y ⟶ ¬(R y x)
  ------------------------------------------------------------------ *}

-- "irealetei maresccas4 pabflomar" (* Dos *)

lemma ej_2:
  assumes "∀x. ∀y. ∀z. R x y ∧ R y z ⟶ R x z"
          "∀x. ¬(R x x)"
  shows "∀x. ∀y. R x y ⟶ ¬(R y x)"
proof -
  {fix a
  {fix b
  {assume 1:"R a b"
  have  "¬(R b a)"
  proof (rule ccontr)
    assume "¬¬(R b a)"
    then have "R b a" by (rule notnotD)
    with 1 have 3:"R a b ∧ R b a" ..
    have "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1) ..
    then have "∀z. R a b ∧ R b z ⟶ R a z" ..
    then have "R a b ∧ R b a ⟶ R a a" ..
    then have "R a a" using 3 ..
    have "¬(R a a)" using assms(2) ..
    then show False using `R a a`..
  qed}
  then have 4:"R a b ⟶ ¬(R b a)" ..}
  then have "∀y. R a y ⟶ ¬ R y a" ..}
  then show "∀x y. R x y ⟶ ¬ R y x" ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 3. Demostrar o refutar
       (∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)
  ------------------------------------------------------------------ *}
-- "irealetei maresccas4 domlloriv pabflomar"
lemma ej_3_auto:
  assumes "∀x. ∃y. P x y"
  shows "∃y. ∀x. P x y"
quickcheck
oops

(*Contra ejemplo
P = (λx. undefined)(a⇣1 := {a⇣2}, a⇣2 := {a⇣1})
*)

text {* --------------------------------------------------------------- 
  Ejercicio 4. Demostrar o refutar
       (∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)
  ------------------------------------------------------------------ *}

-- "irealetei maresccas4"
lemma ej_4_auto:
  assumes "∃y. ∀x. P x y"
  shows "∀x. ∃y. P x y" 
using assms by auto

lemma ej_4:
  assumes 1:"∃y. ∀x. P x y"
  shows "∀x. ∃y. P x y" 
proof -
  {fix a
  obtain b where 2:"∀x. P x b" using 1 ..
  have "P a b" using 2 ..
  then have "∃y. P a y"  ..}
  then show "∀x. ∃y. P x y" ..
qed

lemma ej_4_bis:"(∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)" 
proof 
  assume 1:"∃y. ∀x. P x y"
  {fix a
  obtain b where 2:"∀x. P x b" using 1 ..
  have "P a b" using 2 ..
  then have "∃y. P a y"  ..}
  then show "∀x. ∃y. P x y" ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 5. Demostrar o refutar
     {∀x. P a x x, 
      ∀x y z. P x y z ⟶ P (f x) y (f z)⟧
     ⊢ ∃z. P (f a) z (f (f a))
  ------------------------------------------------------------------ *}

-- "maresccas4"
lemma ej_5:
  assumes "∀x. P a x x"
          "∀x y z. P x y z ⟶ P (f x) y (f z)"
  shows "∃z. P (f a) z (f (f a))"
proof -
  have "P a (f a) (f a)" using assms(1) ..
  have "∀y z. P a y z ⟶ P (f a) y (f z)" using assms(2) ..
  then have "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" ..
  then have "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" ..
  then have "P (f a) (f a) (f (f a))" using `P a (f a) (f a)` ..
  then show "∃z. P (f a) z (f (f a))" ..
qed

-- "irealetei"
lemma ej_5_auto:
  assumes "∀x. P a x x"
  assumes "∀x y z. P x y z ⟶ P (f x) y (f z)"
  shows "∃z. P (f a) z (f (f a))"
using assms by meson

lemma ej_5:
  assumes 1:"∀x. P a x x"
  assumes 2:"∀x y z. P x y z ⟶ P (f x) y (f z)"
  shows "∃z. P (f a) z (f (f a))"
proof -
  have 3:"P a (f a) (f a)" using 1 ..
  have  "∀y z. P a y z ⟶ P (f a) y (f z)" using 2 ..
  then have  "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)"  ..
  then have  4:" P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" ..
  have 5:"P (f a) (f a) (f (f a))" using 4 3 by (rule mp)
  then show "∃z. P (f a) z (f (f a))" ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 6. Demostrar o refutar
     {∀y. Q a y, 
      ∀x y. Q x y ⟶ Q (s x) (s y)} 
     ⊢ ∃z. Qa z ∧ Q z (s (s a))
  ------------------------------------------------------------------ *}

-- "maresccas4"
lemma ej_6:
  assumes "∀y. Q a y"
          "∀x y. Q x y ⟶ Q (s x) (s y)"
  shows "∃z. Q a z ∧ Q z (s (s a))"
proof -
  have "Q a (s a)" using assms(1) ..
  have "∀y. Q a y ⟶ Q (s a) (s y)" using assms(2) ..
  then have "Q a (s a) ⟶ Q (s a) (s (s a))" ..
  then have "Q (s a) (s (s a))" using `Q a (s a)` ..
  with  `Q a (s a)` have "Q a (s a) ∧ Q (s a) (s (s a))"  by (rule conjI)
  then show "∃z. Q a z ∧ Q z (s (s a))" ..
qed

-- "irealetei"
lemma ej_6_auto:
  assumes "∀y. Q a y"
  assumes "∀x y. Q x y ⟶ Q (s x) (s y)"
  shows "∃z. Q a z ∧ Q z (s (s a))"
using assms by meson

lemma ej_6:
  assumes 1:"∀y. Q a y"
  assumes 2:"∀x y. Q x y ⟶ Q (s x) (s y)"
  shows "∃z. Q a z ∧ Q z (s (s a))"
proof
  have 3:"Q a (s a)" using 1 ..
  have "∀y. Q a y ⟶ Q (s a) (s y)" using 2 ..
  then have "Q a (s a) ⟶ Q (s a) (s (s a))" ..
  then have 4:"Q (s a) (s (s a))" using 3  by (rule mp)
  show "Q a (s a) ∧ Q (s a) (s (s a))" using 3 4 by (rule conjI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 7. (En APLI2 el ejercicio 13 de LP) Formalizar, y demostrar
  la corrección, del siguiente argumento 
     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.
  ------------------------------------------------------------------ *}

-- "pabflomar maresccas4 domlloriv"

lemma ej7_pfm:
  assumes 1: "A ∨ P ⟶ R ∧ F" and
          2: "(F ∨ N) ⟶ Or"
 shows "A ⟶ Or"
proof -
  { assume 3: "A"
    have 4: "A ∨ P" using 3 by (rule disjI1)
    have 5: "R ∧ F" using 1 4 by (rule mp)
    have 6: "F" using 5 by (rule conjunct2)
    have 7: "F ∨ N" using 6 by (rule disjI1)
    have 8: "Or" using 2 7 by (rule mp)}
  then show "A ⟶ Or" ..
qed

-- "irealetei"
lemma ej_7_auto:
  assumes "A ∨ P ⟶ R ∧ F"
  assumes "F ∨ N ⟶ Or"
  shows "A ⟶ Or"
using assms by auto

lemma ej_7:
  assumes 1:"A ∨ P ⟶ R ∧ F"
  assumes 2:"F ∨ N ⟶ Or"
  shows "A ⟶ Or"
proof 
    assume "A"
    then have 3:"A ∨ P" ..
    have "R ∧ F" using 1 3 by (rule mp)
    then have "F" ..
    then have 4:"F ∨ N" ..
    show "Or" using 2 4 by (rule mp)
qed 

text {* --------------------------------------------------------------- 
  Ejercicio 8. (En APLI2 el ejercicio 5 de LP) Formalizar, y demostrar
  la corrección, del siguiente argumento 
     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.
  ------------------------------------------------------------------ *}
-- "pabflomar" 

lemma ej8_pfm:
  assumes  "A ⟶ (M ⟷ ¬B)" 
          "A ∨ B"
 shows "¬B ⟶ M"

proof (rule disjE)
  show "A ∨ B" using assms(2) by simp
  next
  { assume "A"
    with assms(1) have "M ⟷ ¬B"  by (rule mp)
    then show "¬B ⟶ M" using assms by simp}
  next
  { assume 1:"B"
    {assume 2:"¬B"
      then have "M" using 1 by (rule notE)}
      then show "¬B ⟶ M" by (rule impI)
 }
qed

-- "maresccas4 irealetei"
lemma ej_8:
  assumes "(A ⟶ M) ⟷ ¬B"
          "A ∨ B"
  shows "¬B ⟶ M"
using assms(2)
proof
  { assume "A"
    { assume "¬B"
      have "¬B ⟶ (A ⟶ M)" using assms(1) ..
      then have "A ⟶ M" using `¬B` ..
      then have "M" using `A` .. }
    then show "¬B ⟶ M" ..
  }
next
  { assume "B"
    { assume "¬B"
      then have False using `B` ..
      then have "M" .. }
    then show "¬B ⟶ M" ..
  }
qed


text {* --------------------------------------------------------------- 
  Ejercicio 9. (En APLI2 el ejercicio 13 de LPO) Formalizar, y decidir
  la corrección, del siguiente argumento 
     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
  ------------------------------------------------------------------ *}
-- "julrobrel "
lemma apli2_ej13_lpo:
    assumes "∀ x. ¬R(x) ⟶ R(p(x))"
      shows "∃ x. R(x) ∧ R(p(p(x)))"
using assms
by auto

lemma apli2_ej13_lpo_d:
    assumes 0:"∀ x. ¬R(x) ⟶ R(p(x))"
      shows "∃ x. R(x) ∧ R(p(p(x)))"
oops

-- "irealetei"
lemma ej_9_auto:
  assumes "∀x. ¬R(x)⟶R(p(x))"
  shows "∃y. R(y) ⟶ R(p(p(y)))"
using assms by auto

-- "maresccas4"
lemma ej_9:
  assumes "∀x. ¬R x ⟶ R (p x)"
  shows "∃x. R x ∧ R(p (p x))"
proof -
  have "¬(∃x. ¬R(p x)) ∨ (∃x. ¬R(p x))" by (rule excluded_middle)
  then show "∃x. R x ∧ R(p (p x))"
  proof (rule disjE)
    assume "¬(∃x. ¬R(p x))"
    then have 1:"∀x. ¬¬R(p x)" by (rule no_ex)
    {fix a
      have "¬¬R(p a)" using 1 ..
      then have "R(p a)" by (rule notnotD)}
    then have 2:"∀x. R(p x)" ..
    {fix a
      have 3:"R(p a)" using 2 ..
      have 4:"R(p (p (p a)))" using 2 ..
      have "R(p a) ∧ R(p (p (p a)))" using 3 4 ..}
    then show "∃x. R x ∧ R(p (p x))" ..
  next
    assume "∃x. ¬R(p x)"
    obtain a where 1:"¬R(p a)" using `∃x. ¬R(p x)` ..
    have "¬R(p a) ⟶ R(p (p a))" using assms ..
    then have 2:"R(p (p a))" using 1 ..
    have "¬R a ⟶ R(p a)" using assms ..
    then have "¬¬R a" using 1 by (rule mt)
    then have 3:"R a" by (rule notnotD)
    then have  "R a ∧ R(p (p a))" using 2 by (rule conjI)
    then show "∃x. R x ∧ R(p (p x))" ..
  qed
qed

text {* --------------------------------------------------------------- 
  Ejercicio 10. (En APLI2 el ejercicio 10 de LPO) Formalizar, y decidir
  la corrección, del siguiente argumento 
     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
  ------------------------------------------------------------------ *}
-- "julrobrel"
lemma apli2_ej10_lpo:
    assumes "∀ x. Af(x) ⟶ (∀ y. E(y) ⟶ Ap(x,y))"
            "∀ y. E(y) ⟶ ¬ Ap(j,y)"
      shows "∃ y. E(y) ∧ N(y) ⟶ ¬Af(j)"
using assms
by auto

lemma apli2_ej10_lpo_d:
    assumes 0:"∀ x. Af(x) ⟶ (∀ y. E(y) ⟶ Ap(x,y))"
        and 1:"∀ y. E(y) ⟶ ¬ Ap(j,y)"
      shows "∃ y. E(y) ∧ N(y) ⟶ ¬Af(j)"
oops

-- "irealetei"
lemma ej_10_auto:
  assumes "∀x y. Af(x) ∧ E(y) ⟶ Ap(x, y)"
  assumes "∀y. E(y) ⟶ ¬Ap(j,y)"
  shows "∃y. N(y) ∧ E(y) ⟶ ¬Af(j)"
using assms by auto

-- "maresccas4"
lemma ej_10:
  assumes "∀x y. (Af(x) ∧ E(y)) ⟶ Ap(x, y)"
          " ∀x. E(x) ⟶ ¬Ap(j, x)"
  shows "∃x. E(x) ∧ N(x) ⟶ ¬Af(j)"
proof -
  { fix a
    { assume 1:"E(a) ∧ N(a)"
      have "¬Af(j)"
      proof
        assume "Af(j)"
        have "E(a)" using 1 ..
        have 2:"Af(j) ∧ E(a)" using `Af(j)` `E(a)` ..
        have "∀x. Af(j) ∧ E(x) ⟶ Ap(j, x)" using assms(1) ..
        then have "Af(j) ∧ E(a) ⟶ Ap(j, a)" ..
        then have a:"Ap(j, a)" using 2 ..
        have "E(a) ⟶ ¬Ap(j, a)" using assms(2) ..
        then have "¬Ap(j, a)" using `E(a)` ..
        then show "False" using a ..
      qed}
    then have "E(a) ∧ N(a) ⟶ ¬Af(j)" ..}
  then show "∃x. E(x) ∧ N(x) ⟶ ¬Af(j)" ..
qed
-- pabflomar --

lemma ej10_pfm:
  assumes "∀x y. Af(x) ∧ E(y) ⟶ Ap(x,y)"
          "∀x. E(x) ⟶ ¬Ap(j,x)"
  shows "∀x. E(x) ∧ N(x)  ⟶ ¬Af(j)"
using assms by auto

text {* --------------------------------------------------------------- 
  Ejercicio 11. 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
   ------------------------------------------------------------------ *}

-- "julrobrel"
lemma apli2_ej24_lpo:
  assumes "¬ (∃ x. P(x) ∧ R(x))"
          "∀ x. P(x) ∧ ¬ Q(x) ⟶ R(x)"
  shows   "P(a) ⟶ Q(a)"
using assms
by auto

-- "julrobrel"
lemma apli2_ej24_lpo_d:
  assumes 0:"¬ (∃ x. P(x) ∧ R(x))"
      and 1:"∀ x. P(x) ∧ ¬ Q(x) ⟶ R(x)"
  shows   "P(a) ⟶ Q(a)"
oops

-- "julrobrel: cuatro sencillos lemas, aunque no faciles de demostrar, y al final el principal"

--"julrobrel: es el modus tollens(mt)"
lemma apli2_ej24_lpo_d_aux1:
  assumes 0:"p ∧ ¬q ⟶ r"
  shows   "¬r⟶¬p ∨ q"
using assms
by auto

lemma modus_tollens:
  assumes 1:"p ⟶ q"
      and 2:"¬q"
    shows   "¬p"
proof -
  {assume 3:"p"
   have   4:"q" using 1 3 by (rule mp)
   have   5:"False" using 2 4 by (rule notE)}
  thus "¬p" ..
qed

lemma modus_tollens2:
  assumes 1:"p ⟶ q"
    shows   "¬q ⟶ ¬p"
proof -
  {assume 2:"¬q"
  have 3:"¬p" using 1 2 by (rule modus_tollens)}
  thus 4:"¬q ⟶ ¬p" by (rule impI)
qed

lemma apli2_ej24_lpo_d_aux1_detalle:
  assumes 0:"p ∧ ¬q ⟶ r"
  shows   "¬r⟶¬p ∨ q"
proof -
  have 1:"(p ∧ ¬q) ⟶ r" using 0 .
  have 2:"¬r ⟶ ¬(p ∧ ¬q)" using 1 by (rule modus_tollens2)
  thus 3:"¬r ⟶ ¬p ∨ q" using 2 by auto (* cada vez estan saliendo mas demostraciones. Aqui hay que demostrar ¬(p ∧ ¬q) = ¬p ∨ q *)
qed

-- "julrobrel"
lemma apli2_ej24_lpo_d_aux2:
  assumes 0:"¬(p ∧ r)"
  shows   "p ⟶ ¬r"
using assms
by auto

--"julrobrel: este lema debe de tener un nombre..."
--"julrobrel: ya he encontrado como se llama: Hypothetical Syllogism (HS)"
lemma apli2_ej24_lpo_d_aux3:
  assumes "(p ⟶ q) ∧ (q ⟶ r)"
  shows   "p ⟶ r"
using assms
by auto

--"julrobrel"
lemma apli2_ej24_lpo_d_aux3_detalle:
  assumes 0:"(p ⟶ q) ∧ (q ⟶ r)"
  shows   "p ⟶ r"
proof -
  have 1:"p⟶q" using 0 by (rule conjunct1)
  have 2:"q⟶r" using 0 by (rule conjunct2)
  {assume 3:"p"
   have 4:"q" using 1 3 by (rule mp)
   have 5:"r" using 2 4 by (rule mp)}
  thus 6:"p⟶r" by (rule impI)
qed

-- "julrobrel"
lemma apli2_ej24_lpo_d_aux4:
  assumes 0:"p⟶(¬p ∨ q)"
  shows   "p ⟶ q"
using assms
by auto

-- "julrobrel"
lemma apli2_ej24_lpo_d:
  assumes 0:"¬ (∃ x. P(x) ∧ R(x))"
      and 1:"∀ x. P(x) ∧ ¬ Q(x) ⟶ R(x)"
    shows   "P(a)⟶Q(a)"
proof -
  have 2:"∀ x. ¬(P(x) ∧ R(x))" using 0 by (rule no_ex)
  fix a
  have 3:"¬(P(a) ∧ R(a))" using 2 ..
  have 4:"P(a) ∧ ¬ Q(a) ⟶ R(a)" using 1 ..
  have 5:"¬R(a) ⟶ ¬ P(a) ∨ Q(a)" using 4 by (rule apli2_ej24_lpo_d_aux1)
  have 6:"P(a)⟶¬R(a)" using 3 by (rule apli2_ej24_lpo_d_aux2)
  have 7:"(P(a)⟶¬R(a)) ∧ (¬R(a) ⟶ ¬P(a) ∨ Q(a))" using 6 5 by (rule conjI)
  have 8:"P(a)⟶(¬P(a) ∨ Q(a))" using 7 by (rule apli2_ej24_lpo_d_aux3)
  have 9:"P(a)⟶Q(a)" using 8 by (rule apli2_ej24_lpo_d_aux4)
  show "P(a)⟶Q(a)" using 9 .
qed


-- "irealetei"
lemma ej_11_auto:
  assumes "∀x. P(x) ⟶ ¬R(x)"
  assumes "∀y. P(y) ∧ ¬Q(y) ⟶ R(y)"
  shows "P(a) ⟶ Q(a)"
using assms by auto

-- "maresccas4"
lemma ej_11:
  assumes "∀x. P(x) ⟶ ¬R(x)"
          "∀x. (P(x) ∧ ¬Q(x)) ⟶ R(x)"
  shows "P(a) ⟶ Q(a)"
proof -
  {assume "P(a)"
  have "Q(a)"
  proof (rule ccontr)
    assume "¬Q(a)"
    have 1:"P(a) ∧ ¬Q(a)" using `P(a)` `¬Q(a)` ..
    have "P(a) ∧ ¬Q(a) ⟶ R(a)" using assms(2) ..
    then have a:"R(a)" using 1 ..
    have "P(a) ⟶ ¬R(a)" using assms(1) ..
    then have "¬R(a)" using `P(a)` ..
    then show "False" using a ..
  qed}
  then show "P(a) ⟶ Q(a)" ..
qed

end