Edición de «Sol 7b» - Lógica matemática y fundamentos (2018-19)

<source lang="isabelle">
theory R7b
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 y los métodos rule, erule, frule, drule y assumption.  
  · 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
  · excluded_middel:(¬P ∨ 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 {* --------------------------------------------------------------- 
  Ejercicio 1. Demostrar
       ∀x. P x ⟶ Q x ⊢ (∀x. P x) ⟶ (∀x. Q x)
  ------------------------------------------------------------------ *}

lemma ej1a: "∀x. P x ⟶ Q x ⟹ (∀x. P x) ⟶ (∀x. Q x)"
  apply (rule impI)  (* ⟦∀x. P x ⟶ Q x; ∀x. P x⟧ ⟹ ∀x. Q x*)
  apply (rule allI)  (* ⋀x. ⟦∀x. P x ⟶ Q x; ∀x. P x⟧ ⟹ Q x *)
  apply (erule allE) (* ⋀x. ⟦∀x. P x; P (?x4 x) ⟶ Q (?x4 x)⟧ ⟹ Q x *)
  apply (erule allE) (* ⋀x. ⟦P (?x4 x) ⟶ Q (?x4 x); P (?x6 x)⟧ ⟹ Q x *)
  apply (erule mp)   (* ⋀x. P (?x6 x) ⟹ P x *)
  apply assumption   (* *)
  done
    
lemma ej1b: "∀x. P x ⟶ Q x ⟹ (∀x. P x) ⟶ (∀x. Q x)"
  apply (rule impI)         (* ⟦∀x. P x ⟶ Q x; ∀x. P x⟧ ⟹ ∀x. Q x *)
  apply (rule allI)         (* ⋀x. ⟦∀x. P x ⟶ Q x; ∀x. P x⟧ ⟹ Q x *)
  apply (erule_tac x=x in allE) (* ⋀x. ⟦∀x. P x; P x ⟶ Q x⟧ ⟹ Q x *)
  apply (erule_tac x=x in allE) (* ⋀x. ⟦P x ⟶ Q x; P x⟧ ⟹ Q x *)
  apply (erule mp)              (* ⋀x. P x ⟹ P x *)
  apply assumption              (* *)
  done
    
lemma ej1c: "∀x. P x ⟶ Q x ⟹ (∀x. P x) ⟶ (∀x. Q x)"
  apply (rule impI)         (* ⟦∀x. P x ⟶ Q x; ∀x. P x⟧ ⟹ ∀x. Q x *)
  apply (rule allI)         (* ⋀x. ⟦∀x. P x ⟶ Q x; ∀x. P x⟧ ⟹ Q x *)
  apply (erule_tac x=x in allE)+ (* ⋀x. ⟦P x ⟶ Q x; P x⟧ ⟹ Q x *)
  apply (erule mp)               (* ⋀x. P x ⟹ P x *)
  apply assumption               (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 2. Demostrar
       ∃x. ¬(P x) ⊢ ¬(∀x. P x)
  ------------------------------------------------------------------ *}

lemma ej2: "∃x. ¬(P x) ⟹ ¬(∀x. P x)"
  apply (rule notI)             (* ⟦∃x. ¬ P x; ∀x. P x⟧ ⟹ False *)
  apply (erule exE)             (* ⋀x. ⟦∀x. P x; ¬ P x⟧ ⟹ False *)
  apply (erule_tac x=x in allE) (* ⋀x. ⟦¬ P x; P x⟧ ⟹ False *)
  apply (erule notE)            (* ⋀x. P x ⟹ P x *) 
  apply assumption              (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 3. Demostrar
       ∀x. P x ⊢ ∀y. P y
  ------------------------------------------------------------------ *}

lemma ej3: "∀x. P x ⟹ ∀y. P y"
  apply (rule allI)             (* ⋀y. ∀x. P x ⟹ P y *)
  apply (erule_tac x=y in allE) (* ⋀y. P y ⟹ P y*)
  apply assumption              (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 4. Demostrar
       ∀x. P x ⟶ Q x ⊢ (∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))
  ------------------------------------------------------------------ *}

lemma ej4: "∀x. P x ⟶ Q x ⟹ (∀x. ¬(Q x)) ⟶ (∀x. ¬(P x))"
  apply (rule impI)    (* ⟦∀x. P x ⟶ Q x; ∀x. ¬ Q x⟧ ⟹ ∀x. ¬ P x *)
  apply (rule allI)    (* ⋀x. ⟦∀x. P x ⟶ Q x; ∀x. ¬ Q x⟧ ⟹ ¬ P x *)
  apply (erule_tac x=x in allE)+ 
                       (* ⋀x. ⟦P x ⟶ Q x; ¬ Q x⟧ ⟹ ¬ P x *)
  apply (rule notI)    (* ⋀x. ⟦P x ⟶ Q x; ¬ Q x; P x⟧ ⟹ False *) 
  apply (erule impE)   (* ⋀x. ⟦¬ Q x; P x⟧ ⟹ P x
                          ⋀x. ⟦¬ Q x; P x; Q x⟧ ⟹ False *) 
   apply assumption    (* ⋀x. ⟦¬ Q x; P x; Q x⟧ ⟹ False *)
  apply (erule notE)   (* ⋀x. ⟦P x; Q x⟧ ⟹ Q x *)
  apply assumption     (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 5. Demostrar
       ∀x. P x  ⟶ ¬(Q x) ⊢ ¬(∃x. P x ∧ Q x)
  ------------------------------------------------------------------ *}

lemma ej5: "∀x. P x  ⟶ ¬(Q x) ⟹ ¬(∃x. P x ∧ Q x)"
  apply (rule notI)   
                 (* ⟦∀x. P x ⟶ ¬ Q x; ∃x. P x ∧ Q x⟧ ⟹ False *)
  apply (erule exE)   
                 (* ⋀x. ⟦∀x. P x ⟶ ¬ Q x; P x ∧ Q x⟧ ⟹ False *)
  apply (frule conjunct1)
                 (* ⋀x. ⟦∀x. P x ⟶ ¬ Q x; P x ∧ Q x; P x⟧ ⟹ False*)
  apply (erule_tac x=x in allE)  
                 (* ⋀x. ⟦P x ∧ Q x; P x; P x ⟶ ¬ Q x⟧ ⟹ False *)
  apply (erule impE)
                 (* ⋀x. ⟦P x ∧ Q x; P x⟧ ⟹ P x
                    ⋀x. ⟦P x ∧ Q x; P x; ¬ Q x⟧ ⟹ False *)
   apply assumption
                 (* ⋀x. ⟦P x ∧ Q x; P x; ¬ Q x⟧ ⟹ False *)
  apply (erule notE)
                 (* ⋀x. ⟦P x ∧ Q x; P x⟧ ⟹ Q x *)
  apply (erule conjunct2)
                 (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 6. Demostrar
       ∀x y. P x y ⊢ ∀u v. P u v
  ------------------------------------------------------------------ *}

lemma ej6a: "∀x y. P x y ⟹ ∀u v. P u v"
  apply (rule allI)              (* ⋀u. ∀x y. P x y ⟹ ∀v. P u v *)
  apply (rule allI)              (* ⋀u v. ∀x y. P x y ⟹ P u v *) 
  apply (erule_tac x=u in allE)  (* ⋀u v. ∀y. P u y ⟹ P u v *)
  apply (erule_tac x=v in allE)  (* ⋀u v. P u v ⟹ P u v *)
  apply assumption               (* *)
  done
    
lemma ej6b: "∀x y. P x y ⟹ ∀u v. P u v"
  apply (rule allI)+    (* ⋀u v. ∀x y. P x y ⟹ P u v *)
  apply (erule allE)+   (* ⋀u v. P (?x4 u v) (?y6 u v) ⟹ P u v *)
  apply assumption      (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 7. Demostrar
       ∃x y. P x y ⟹ ∃u v. P u v
  ------------------------------------------------------------------ *}

lemma ej7a: "∃x y. P x y ⟹ ∃u v. P u v"
  apply (erule exE)            (* ⋀x. ∃y. P x y ⟹ ∃u v. P u v *)
  apply (erule exE)            (* ⋀x y. P x y ⟹ ∃u v. P u v*)
  apply (rule_tac x=x in exI)  (* ⋀x y. P x y ⟹ ∃v. P x v *)
  apply (rule_tac x=y in exI)  (* ⋀x y. P x y ⟹ P x y *)
  apply assumption             (* *)
  done
    
lemma ej7b: "∃x y. P x y ⟹ ∃u v. P u v"
  apply (erule exE)+  (* ⋀x y. P x y ⟹ ∃u v. P u v *)
  apply (rule exI)+   (* ⋀x y. P x y ⟹ P (?u4 x y) (?v6 x y) *)
  apply assumption    (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 8. Demostrar
       ∃x. ∀y. P x y ⊢ ∀y. ∃x. P x y
  ------------------------------------------------------------------ *}

lemma ej8a: "∃x. ∀y. P x y ⟹ ∀y. ∃x. P x y"
  apply (rule allI)              (* ⋀y. ∃x. ∀y. P x y ⟹ ∃x. P x y *)
  apply (erule exE)              (* ⋀y x. ∀y. P x y ⟹ ∃x. P x y *)
  apply (erule_tac x=y in allE)  (* ⋀y x. P x y ⟹ ∃x. P x y *)
  apply (erule_tac x=x in exI)   (* *)
  done
    
lemma ej8b: "∃x. ∀y. P x y ⟹ ∀y. ∃x. P x y"
  apply (rule allI)   (* ⋀y. ∃x. ∀y. P x y ⟹ ∃x. P x y *)
  apply (erule exE)   (* ⋀y x. ∀y. P x y ⟹ ∃x. P x y *)
  apply (erule allE)  (* ⋀y x. P x (?y4 y x) ⟹ ∃x. P x y *)
  apply (erule exI)   (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 9. Demostrar
       ∃x. P a ⟶ Q x ⊢ P a ⟶ (∃x. Q x)
  ------------------------------------------------------------------ *}

lemma ej9: "∃x. P a ⟶ Q x ⟹ P a ⟶ (∃x. Q x)"
  apply (rule impI)         (* ⟦∃x. P a ⟶ Q x; P a⟧ ⟹ ∃x. Q x *)
  apply (erule exE)         (* ⋀x. ⟦P a; P a ⟶ Q x⟧ ⟹ ∃x. Q x *)
  apply (rule_tac x=x in exI)   (* ⋀x. ⟦P a; P a ⟶ Q x⟧ ⟹ Q x *)
  apply (erule impE)            (* ⋀x. P a ⟹ P a
                                   ⋀x. ⟦P a; Q x⟧ ⟹ Q x *)
   apply assumption+            (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 10. Demostrar
       P a ⟶ (∃x. Q x) ⊢ ∃x. P a ⟶ Q x 
  ------------------------------------------------------------------ *}

lemma ej10: "P a ⟶ (∃x. Q x) ⟹ ∃x. P a ⟶ Q x"
  apply (case_tac "P a") 
                    (* ⟦P a ⟶ (∃x. Q x); P a⟧ ⟹ ∃x. P a ⟶ Q x
                       ⟦P a ⟶ (∃x. Q x); ¬ P a⟧ ⟹ ∃x. P a ⟶ Q x *)
   apply (erule impE)     
                    (* P a ⟹ P a
                       ⟦P a; ∃x. Q x⟧ ⟹ ∃x. P a ⟶ Q x
                       ⟦P a ⟶ (∃x. Q x); ¬ P a⟧ ⟹ ∃x. P a ⟶ Q x *)
    apply assumption      
                    (* ⟦P a; ∃x. Q x⟧ ⟹ ∃x. P a ⟶ Q x
                       ⟦P a ⟶ (∃x. Q x); ¬ P a⟧ ⟹ ∃x. P a ⟶ Q x *)
   apply (erule exE)      
                    (* ⋀x. ⟦P a; Q x⟧ ⟹ ∃x. P a ⟶ Q x
                       ⟦P a ⟶ (∃x. Q x); ¬ P a⟧ ⟹ ∃x. P a ⟶ Q x *)
   apply (rule_tac x=x in exI)
                    (* ⋀x. ⟦P a; Q x⟧ ⟹ P a ⟶ Q x
                       ⟦P a ⟶ (∃x. Q x); ¬ P a⟧ ⟹ ∃x. P a ⟶ Q x *)
   apply (rule impI)
                    (* ⋀x. ⟦P a; Q x; P a⟧ ⟹ Q x
                       ⟦P a ⟶ (∃x. Q x); ¬ P a⟧ ⟹ ∃x. P a ⟶ Q x *)
   apply assumption       
                    (* ⟦P a ⟶ (∃x. Q x); ¬ P a⟧ ⟹ ∃x. P a ⟶ Q x *)
  apply (rule_tac x=x in exI)
                    (* ⟦P a ⟶ (∃x. Q x); ¬ P a⟧ ⟹ P a ⟶ Q x*)
  apply (rule impI) (* ⟦P a ⟶ (∃x. Q x); ¬ P a; P a⟧ ⟹ Q x *)
  apply (erule notE)
                    (* ⟦P a ⟶ (∃x. Q x); P a⟧ ⟹ P a *)
  apply assumption  (* *)    
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 11. Demostrar
       (∃x. P x) ⟶ Q a ⊢ ∀x. P x ⟶ Q a
  ------------------------------------------------------------------ *}

lemma ej11: "(∃x. P x) ⟶ Q a ⟹ ∀x. P x ⟶ Q a"
  apply (rule allI)   (* ⋀x. (∃x. P x) ⟶ Q a ⟹ P x ⟶ Q a *)
  apply (rule impI)   (* ⋀x. ⟦(∃x. P x) ⟶ Q a; P x⟧ ⟹ Q a *)
  apply (erule mp)    (* ⋀x. P x ⟹ ∃x. P x *) 
   apply (erule exI)  (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 12. Demostrar
       ∀x. P x ⟶ Q a ⊢ ∃ x. P x ⟶ Q a
  ------------------------------------------------------------------ *}

lemma ej12: "∀x. P x ⟶ Q a ⟹ ∃x. P x ⟶ Q a"
  apply (erule allE) (*  P ?x ⟶ Q a ⟹ ∃x. P x ⟶ Q a *)
  apply (erule exI)  (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 13. Demostrar
       (∀x. P x) ∨ (∀x. Q x) ⊢ ∀x. P x ∨ Q x
  ------------------------------------------------------------------ *}

lemma ej13: "(∀x. P x) ∨ (∀x. Q x) ⟹ ∀x. P x ∨ Q x"
  apply (rule allI)       (* ⋀x. (∀x. P x) ∨ (∀x. Q x) ⟹ P x ∨ Q x *)
  apply (erule disjE)     (* ⋀x. ∀x. P x ⟹ P x ∨ Q x
                             ⋀x. ∀x. Q x ⟹ P x ∨ Q x *)
   apply (erule allE)     (* ⋀x. P (?x5 x) ⟹ P x ∨ Q x
                             ⋀x. ∀x. Q x ⟹ P x ∨ Q x *)
   apply (erule disjI1)   (* ⋀x. ∀x. Q x ⟹ P x ∨ Q x *)
  apply (erule allE)      (* ⋀x. Q (?x8 x) ⟹ P x ∨ Q x *)
  apply (erule disjI2)    (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 14. Demostrar
       ∃x. P x ∧ Q x ⊢ (∃x. P x) ∧ (∃x. Q x)
  ------------------------------------------------------------------ *}

lemma ej14: "∃x. P x ∧ Q x ⟹ (∃x. P x) ∧ (∃x. Q x)"
  apply (erule exE)         (* ⋀x. P x ∧ Q x ⟹ (∃x. P x) ∧ (∃x. Q x) *)
  apply (rule conjI)        (* ⋀x. P x ∧ Q x ⟹ ∃x. P x
                               ⋀x. P x ∧ Q x ⟹ ∃x. Q x *)
   apply (drule conjunct1)  (* ⋀x. P x ⟹ ∃x. P x
                               ⋀x. P x ∧ Q x ⟹ ∃x. Q x *)
   apply (erule exI)        (* ⋀x. P x ∧ Q x ⟹ ∃x. Q x *)
  apply (drule conjunct2)   (* ⋀x. Q x ⟹ ∃x. Q x *)
  apply (erule exI)         (* *)
  done

text {* --------------------------------------------------------------- 
  Ejercicio 15. Demostrar
       ∀x y. P y ⟶ Q x ⊢ (∃y. P y) ⟶ (∀x. Q x)
  ------------------------------------------------------------------ *}

lemma ej15: "∀x y. P y ⟶ Q x ⟹ (∃y. P y) ⟶ (∀x. Q x)"
  apply (rule impI)       (* ⟦∀x y. P y ⟶ Q x; ∃y. P y⟧ ⟹ ∀x. Q x *)
  apply (rule allI)       (* ⋀x. ⟦∀x y. P y ⟶ Q x; ∃y. P y⟧ ⟹ Q x *)
  apply (erule exE)       (* ⋀x y. ⟦∀x y. P y ⟶ Q x; P y⟧ ⟹ Q x *)
  apply (erule_tac x=x in allE) 
                          (* ⋀x y. ⟦P y; ∀y. P y ⟶ Q x⟧ ⟹ Q x *)
  apply (erule_tac x=y in allE) 
                          (* ⋀x y. ⟦P y; P y ⟶ Q x⟧ ⟹ Q x *)
  apply (erule mp)        (* ⋀x y. P y ⟹ P y *)
   apply assumption       (* *) 
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 16. Demostrar
       ¬(∀x. ¬(P x)) ⊢ ∃x. P x
  ------------------------------------------------------------------ *}

lemma ej16: "¬(∀x. ¬(P x)) ⟹ ∃x. P x"
  apply (rule ccontr)   (* ⟦¬ (∀x. ¬ P x); ∄x. P x⟧ ⟹ False *)
  apply (erule notE)    (* ∄x. P x ⟹ ∀x. ¬ P x *)
  apply (rule allI)     (* ⋀x. ∄x. P x ⟹ ¬ P x *)
  apply (rule notI)     (* ⋀x. ⟦∄x. P x; P x⟧ ⟹ False *)
  apply (erule notE)    (* ⋀x. P x ⟹ ∃x. P x *)
  apply (erule exI)     (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 17. Demostrar
       ∀x. ¬(P x) ⊢ ¬(∃x. P x)
  ------------------------------------------------------------------ *}

lemma ej17: "∀x. ¬(P x) ⟹ ¬(∃x. P x)"
  apply (rule notI)             (* ⟦∀x. ¬ P x; ∃x. P x⟧ ⟹ False *)
  apply (erule exE)             (* ⋀x. ⟦∀x. ¬ P x; P x⟧ ⟹ False *)
  apply (erule_tac x=x in allE) (* ⋀x. ⟦P x; ¬ P x⟧ ⟹ False *)
  apply (erule notE)            (* ⋀x. P x ⟹ P x *)
  apply assumption              (* *) 
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 18. Demostrar
       ∃x. P x ⊢ ¬(∀x. ¬(P x))
  ------------------------------------------------------------------ *}

lemma ej18: "∃x. P x ⟹ ¬(∀x. ¬(P x))"
  apply (rule notI)  (* ⟦∃x. P x; ∀x. ¬ P x⟧ ⟹ False *)
  apply (erule exE)  (* ⋀x. ⟦∀x. ¬ P x; P x⟧ ⟹ False *)
  apply (erule allE) (* ⋀x. ⟦P x; ¬ P (?x4 x)⟧ ⟹ False *)
  apply (erule notE) (* ⋀x. P x ⟹ P (?x4 x) *)
  apply assumption   (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 19. Demostrar
       P a ⟶ (∀x. Q x) ⊢ ∀x. P a ⟶ Q x
  ------------------------------------------------------------------ *}

lemma ej19: "P a ⟶ (∀x. Q x) ⟹ ∀x. P a ⟶ Q x"
  apply (rule allI)   (* ⋀x. P a ⟶ (∀x. Q x) ⟹ P a ⟶ Q x *)
  apply (rule impI)   (* ⋀x. ⟦P a ⟶ (∀x. Q x); P a⟧ ⟹ Q x *)
  apply (drule mp)    (* ⋀x. P a ⟹ P a
                         ⋀x. ⟦P a; ∀x. Q x⟧ ⟹ Q x *)
   apply assumption   (* ⋀x. ⟦P a; ∀x. Q x⟧ ⟹ Q x *)
  apply (erule allE)  (* ⋀x. ⟦P a; Q (?x7 x)⟧ ⟹ Q x *)
  apply assumption    (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 20. 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)
  ------------------------------------------------------------------ *}

lemma ej20: "⟦∀x y z. R x y ∧ R y z ⟶ R x z;
              ∀x. ¬(R x x)⟧
             ⟹ ∀x y. R x y ⟶ ¬(R y x)"
  apply (rule allI)+            (* ⋀x y. ⟦∀x y z. R x y ∧ R y z ⟶ R x z;
                                          ∀x. ¬ R x x⟧
                                         ⟹ R x y ⟶ ¬ R y x *)
  apply (rule impI)             (* ⋀x y. ⟦∀x y z. R x y ∧ R y z ⟶ R x z;
                                          ∀x. ¬ R x x; 
                                          R x y⟧
                                         ⟹ ¬ R y x *)
  apply (rule notI)             (* ⋀x y. ⟦∀x y z. R x y ∧ R y z ⟶ R x z;
                                          ∀x. ¬ R x x; 
                                          R x y; 
                                          R y x⟧
                                         ⟹ False *)
  apply (erule_tac x=x in allE) (* ⋀x y. ⟦∀x. ¬ R x x; 
                                          R x y; 
                                          R y x;
                                          ∀y z. R x y ∧ R y z ⟶ R x z⟧
                                          ⟹ False *)
  apply (erule_tac x=x in allE) (* ⋀x y. ⟦R x y; 
                                          R y x;
                                          ∀y z. R x y ∧ R y z ⟶ R x z;
                                          ¬ R x x⟧
                                         ⟹ False *)
  apply (erule_tac x=y in allE) (* ⋀x y. ⟦R x y; 
                                          R y x; 
                                          ¬ R x x;
                                          ∀z. R x y ∧ R y z ⟶ R x z⟧
                                         ⟹ False *) 
  apply (erule_tac x=x in allE) (* ⋀x y. ⟦R x y; 
                                          R y x; 
                                          ¬ R x x;
                                          R x y ∧ R y x ⟶ R x x⟧
                                         ⟹ False *)
  apply (erule notE)            (* ⋀x y. ⟦R x y; 
                                          R y x; 
                                          R x y ∧ R y x ⟶ R x x⟧
                                         ⟹ R x x *)
  apply (erule mp)              (* ⋀x y. ⟦R x y; 
                                          R y x⟧ 
                                         ⟹ R x y ∧ R y x*)
   apply (erule conjI)          (* ⋀x y. R y x ⟹ R y x *)
   apply assumption             (* *)
  done
    
text {* ---------------------------------------------------------------
  Ejercicio 21. Demostrar
     {∀x. P x ∨ Q x, ∃x. ¬(Q x), ∀x. R x ⟶ ¬(P x)} ⊢ ∃x. ¬(R x)
  ------------------------------------------------------------------ *}

lemma ej21: "⟦ ∀x. P x ∨ Q x; 
              ∃x. ¬(Q x); 
              ∀x. R x ⟶ ¬(P x) ⟧
             ⟹ ∃x. ¬(R x)"
  apply (erule exE)    (* ⋀x. ⟦∀x. P x ∨ Q x; ∀x. R x ⟶ ¬ P x; ¬ Q x⟧
                              ⟹ ∃x. ¬ R x*)
  apply (erule_tac x=x in allE)+
                       (* ⋀x. ⟦¬ Q x; P x ∨ Q x; R x ⟶ ¬ P x⟧
                              ⟹ ∃x. ¬ R x *)
  apply (erule disjE)  (* ⋀x. ⟦¬ Q x; R x ⟶ ¬ P x; P x⟧ ⟹ ∃x. ¬ R x
                          ⋀x. ⟦¬ Q x; R x ⟶ ¬ P x; Q x⟧ ⟹ ∃x. ¬ R x*) 
   apply (rule_tac x=x in exI)
                       (* ⋀x. ⟦¬ Q x; R x ⟶ ¬ P x; P x⟧ ⟹ ¬ R x
                          ⋀x. ⟦¬ Q x; R x ⟶ ¬ P x; Q x⟧ ⟹ ∃x. ¬ R x *)
   apply (rule notI)   (* ⋀x. ⟦¬ Q x; R x ⟶ ¬ P x; P x; R x⟧ ⟹ False
                          ⋀x. ⟦¬ Q x; R x ⟶ ¬ P x; Q x⟧ ⟹ ∃x. ¬ R x *)
   apply (drule mp)    (* ⋀x. ⟦¬ Q x; P x; R x⟧ ⟹ R x
                          ⋀x. ⟦¬ Q x; P x; R x; ¬ P x⟧ ⟹ False
                          ⋀x. ⟦¬ Q x; R x ⟶ ¬ P x; Q x⟧ ⟹ ∃x. ¬ R x *)
    apply assumption   (* ⋀x. ⟦¬ Q x; P x; R x; ¬ P x⟧ ⟹ False
                          ⋀x. ⟦¬ Q x; R x ⟶ ¬ P x; Q x⟧ ⟹ ∃x. ¬ R x *)
   apply (erule_tac P="P x" in notE)  
                       (* ⋀x. ⟦¬ Q x; P x; R x⟧ ⟹ P x
                          ⋀x. ⟦¬ Q x; R x ⟶ ¬ P x; Q x⟧ ⟹ ∃x. ¬ R x *)
   apply assumption    (* ⋀x. ⟦¬ Q x; R x ⟶ ¬ P x; Q x⟧ ⟹ ∃x. ¬ R x *)
  apply (erule notE)   (* ⋀x. ⟦R x ⟶ ¬ P x; Q x⟧ ⟹ Q x *)
  apply assumption     (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 22. Demostrar
     {∀x. P x ⟶ Q x ∨ R x, ¬(∃x. P x ∧ R x)} ⊢ ∀x. P x ⟶ Q x
  ------------------------------------------------------------------ *}

lemma ej22: "⟦ ∀x. P x ⟶ Q x ∨ R x;  
              ¬(∃x. P x ∧ R x) ⟧
             ⟹ ∀x. P x ⟶ Q x"
  apply (rule allI)   (* ⋀x. ⟦∀x. P x ⟶ Q x ∨ R x; ∄x. P x ∧ R x⟧
                             ⟹ P x ⟶ Q x *)
  apply (rule impI)   (* ⋀x. ⟦∀x. P x ⟶ Q x ∨ R x; ∄x. P x ∧ R x; P x⟧
                             ⟹ Q x*)
  apply (erule_tac x=x in allE)
                      (* ⋀x. ⟦∄x. P x ∧ R x; P x; P x ⟶ Q x ∨ R x⟧
                             ⟹ Q x *)
  apply (drule mp)    (* ⋀x. ⟦∄x. P x ∧ R x; P x⟧ ⟹ P x
                         ⋀x. ⟦∄x. P x ∧ R x; P x; Q x ∨ R x⟧ ⟹ Q x *)
   apply assumption   (* ⋀x. ⟦∄x. P x ∧ R x; P x; Q x ∨ R x⟧ ⟹ Q x *)
  apply (erule disjE) (* ⋀x. ⟦∄x. P x ∧ R x; P x; Q x⟧ ⟹ Q x
                         ⋀x. ⟦∄x. P x ∧ R x; P x; R x⟧ ⟹ Q x *)
   apply assumption   (* ⋀x. ⟦∄x. P x ∧ R x; P x; R x⟧ ⟹ Q x *)
  apply (erule notE)  (* ⋀x. ⟦P x; R x⟧ ⟹ ∃x. P x ∧ R x *)
  apply (rule_tac x=x in exI)
                      (* ⋀x. ⟦P x; R x⟧ ⟹ P x ∧ R x *) 
  apply (erule conjI) (* ⋀x. R x ⟹ R x *)
   apply assumption   (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 23. Demostrar
     ∃x y. R x y ∨ R y x ⊢ ∃x y. R x y
  ------------------------------------------------------------------ *}

lemma ej23a: "∃x y. R x y ∨ R y x ⟹ ∃x y. R x y"
  apply (erule exE)+   (* ⋀x y. R x y ∨ R y x ⟹ ∃x y. R x y *)
  apply (erule disjE)  (* ⋀x y. R x y ⟹ ∃x y. R x y
                          ⋀x y. R y x ⟹ ∃x y. R x y *)
   apply (rule_tac x=x in exI)
                       (* ⋀x y. R x y ⟹ ∃y. R x y
                          ⋀x y. R y x ⟹ ∃x y. R x y *) 
   apply (rule_tac x=y in exI)
                       (* ⋀x y. R x y ⟹ R x y
                          ⋀x y. R y x ⟹ ∃x y. R x y *)
    apply assumption   (* ⋀x y. R y x ⟹ ∃x y. R x y  *)
  apply (rule_tac x=y in exI)
                       (* ⋀x y. R y x ⟹ ∃ya. R y ya *)
  apply (erule_tac x=x in exI)
                       (* *)
  done
    
lemma ej23b: "∃x y. R x y ∨ R y x ⟹ ∃x y. R x y"
  apply (erule exE)+   (* ⋀x y. R x y ∨ R y x ⟹ ∃x y. R x y *)
  apply (erule disjE)  (* ⋀x y. R x y ⟹ ∃x y. R x y
                          ⋀x y. R y x ⟹ ∃x y. R x y *)
   apply (rule exI)+   (* ⋀x y. R x y ⟹ R (?x7 x y) (?y9 x y)
                          ⋀x y. R y x ⟹ ∃x y. R x y *) 
   apply assumption    (* ⋀x y. R y x ⟹ ∃x y. R x y *)
  apply (rule exI)+    (* ⋀x y. R y x ⟹ R (?x11 x y) (?y13 x y) *)
  apply assumption     (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 24. Demostrar
       (∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)
  ------------------------------------------------------------------ *}

lemma ej24: "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
  apply (rule impI)   (* ∃x. ∀y. P x y ⟹ ∀y. ∃x. P x y *)
  apply (rule allI)   (* ⋀y. ∃x. ∀y. P x y ⟹ ∃x. P x y *)
  apply (erule exE)   (* ⋀y x. ∀y. P x y ⟹ ∃x. P x y *)
  apply (erule allE)  (* ⋀y x. P x (?y6 y x) ⟹ ∃x. P x y *)
  apply (erule exI)   (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 25. Demostrar
       (∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)
  ------------------------------------------------------------------ *}

lemma ej25a: "(∀x. P x ⟶ Q) ⟹ ((∃x. P x) ⟶ Q)"
  apply (rule impI)   (* ∀x. P x ⟶ Q; ∃x. P x⟧ ⟹ Q *)
   apply (erule exE)  (* ⋀x. ⟦∀x. P x ⟶ Q; P x⟧ ⟹ Q *)
  apply (erule allE)  (* ⋀x. ⟦P x; P (?x7 x) ⟶ Q⟧ ⟹ Q *)
   apply (erule mp)   (* ⋀x. P x ⟹ P (?x7 x) *)
    apply assumption  (* *)
  done
    
lemma ej25b: "((∃x. P x) ⟶ Q) ⟹ (∀x. P x ⟶ Q)"
  apply (rule allI)   (* ⋀x. (∃x. P x) ⟶ Q ⟹ P x ⟶ Q *)
  apply (rule impI)   (* ⋀x. ⟦(∃x. P x) ⟶ Q; P x⟧ ⟹ Q *)
  apply (erule mp)    (* ⋀x. P x ⟹ ∃x. P x *)
  apply (erule exI)   (* *)
  done
    
lemma ej25: "(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)"
  apply (rule iffI)   (* ∀x. P x ⟶ Q ⟹ (∃x. P x) ⟶ Q
                         (∃x. P x) ⟶ Q ⟹ ∀x. P x ⟶ Q *)
  apply (erule ej25a) (* (∃x. P x) ⟶ Q ⟹ ∀x. P x ⟶ Q *)
  apply (erule ej25b) (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 26. Demostrar
       ((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)
  ------------------------------------------------------------------ *}

lemma ej26a: "((∀x. P x) ∧ (∀x. Q x)) ⟹ (∀x. P x ∧ Q x)"
  apply (rule allI)         (* ⋀x. (∀x. P x) ∧ (∀x. Q x) ⟹ P x ∧ Q x *)
  apply (rule conjI)        (* ⋀x. (∀x. P x) ∧ (∀x. Q x) ⟹ P x
                               ⋀x. (∀x. P x) ∧ (∀x. Q x) ⟹ Q x *)
   apply (drule conjunct1)  (* ⋀x. ∀x. P x ⟹ P x
                               ⋀x. (∀x. P x) ∧ (∀x. Q x) ⟹ Q x *)
   apply (erule spec)       (* ⋀x. (∀x. P x) ∧ (∀x. Q x) ⟹ Q x *)
   apply (drule conjunct2)  (* ⋀x. ∀x. Q x ⟹ Q x *)
   apply (erule spec)       (* *)
  done
    
lemma ej26b: "(∀x. P x ∧ Q x) ⟹ ((∀x. P x) ∧ (∀x. Q x))"
  apply (rule conjI)        (* ∀x. P x ∧ Q x ⟹ ∀x. P x
                               ∀x. P x ∧ Q x ⟹ ∀x. Q x *)
  apply (rule allI)         (* ⋀x. ∀x. P x ∧ Q x ⟹ P x
                               ∀x. P x ∧ Q x ⟹ ∀x. Q x *)   
   apply (drule spec)       (* ⋀x. P (?x19 x) ∧ Q (?x19 x) ⟹ P x
                               ∀x. P x ∧ Q x ⟹ ∀x. Q x *)
   apply (erule conjunct1)  (* ∀x. P x ∧ Q x ⟹ ∀x. Q x *)
  apply (rule allI)         (* ⋀x. ∀x. P x ∧ Q x ⟹ Q x *)
  apply (drule spec)        (* ⋀x. P (?x24 x) ∧ Q (?x24 x) ⟹ Q x *)
  apply (erule conjunct2)   (* *)
  done
    
lemma ej26: "((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)"
  apply (rule iffI)      (* (∀x. P x) ∧ (∀x. Q x) ⟹ ∀x. P x ∧ Q x
                            ∀x. P x ∧ Q x ⟹ (∀x. P x) ∧ (∀x. Q x) *)
  apply (erule ej26a)    (* ∀x. P x ∧ Q x ⟹ (∀x. P x) ∧ (∀x. Q x) *)
  apply (erule ej26b)    (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 27. Demostrar o refutar
       ((∀x. P x) ∨ (∀x. Q x)) ⟷ (∀x. P x ∨ Q x)
  ------------------------------------------------------------------ *}

lemma ej27: "((∀x. P x) ∨ (∀x. Q x)) ⟷ (∀x. P x ∨ Q x)"
  oops
    
(* Auto Quickcheck found a counterexample:
    P = {a1}
    Q = {a2}
   Evaluated terms:
    ∀x xa. P x ∨ Q xa = False
    ∀x. P x ∨ Q x = True *)    

text {* --------------------------------------------------------------- 
  Ejercicio 28. Demostrar o refutar
       ((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)
  ------------------------------------------------------------------ *}

lemma ej28a: "((∃x. P x) ∨ (∃x. Q x)) ⟹ (∃x. P x ∨ Q x)"
  apply (erule disjE)    (* ∃x. P x ⟹ ∃x. P x ∨ Q x
                             ∃x. Q x ⟹ ∃x. P x ∨ Q x *)
   apply (erule exE)     (* ⋀x. P x ⟹ ∃x. P x ∨ Q x
                            ∃x. Q x ⟹ ∃x. P x ∨ Q x *)
  apply (rule exI)        (* ⋀x. P x ⟹ P (?x8 x) ∨ Q (?x8 x)
                             ∃x. Q x ⟹ ∃x. P x ∨ Q x *)
    apply (erule disjI1)  (* ∃x. Q x ⟹ ∃x. P x ∨ Q x *)
  apply (erule exE)       (* ⋀x. Q x ⟹ ∃x. P x ∨ Q x *) 
  apply (rule exI)        (* ⋀x. Q x ⟹ P (?x13 x) ∨ Q (?x13 x) *)
   apply (erule disjI2)   (* *)
  done
    
lemma ej28b: "(∃x. P x ∨ Q x) ⟹ ((∃x. P x) ∨ (∃x. Q x))"
  apply (erule exE)       (* ⋀x. P x ∨ Q x ⟹ (∃x. P x) ∨ (∃x. Q x) *)
  apply (erule disjE)     (* ⋀x. P x ⟹ (∃x. P x) ∨ (∃x. Q x)
                             ⋀x. Q x ⟹ (∃x. P x) ∨ (∃x. Q x) *)
   apply (rule disjI1)    (* ⋀x. P x ⟹ ∃x. P x
                             ⋀x. Q x ⟹ (∃x. P x) ∨ (∃x. Q x) *)
   apply (erule exI)      (* ⋀x. Q x ⟹ (∃x. P x) ∨ (∃x. Q x) *)
  apply (rule disjI2)     (* ⋀x. Q x ⟹ ∃x. Q x *) 
  apply (erule exI)       (* *)
  done
    
lemma ej28: "((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"
  apply (rule iffI)       (* (∃x. P x) ∨ (∃x. Q x) ⟹ ∃x. P x ∨ Q x
                             ∃x. P x ∨ Q x ⟹ (∃x. P x) ∨ (∃x. Q x) *)
   apply (erule ej28a)    (* ∃x. P x ∨ Q x ⟹ (∃x. P x) ∨ (∃x. Q x) *)
   apply (erule ej28b)    (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 29. Demostrar o refutar
       (∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)
  ------------------------------------------------------------------ *}

lemma ej29: "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
  oops

(* Auto Quickcheck found a counterexample:
      P = (λx. undefined)(a⇩1 := {a⇩2}, a⇩2 := {a⇩1})
*)    

text {* --------------------------------------------------------------- 
  Ejercicio 30. Demostrar o refutar
       (¬(∀x. P x)) ⟷ (∃x. ¬P x)
  ------------------------------------------------------------------ *}

lemma ej30a: "¬(∀x. P x) ⟹ (∃x. ¬P x)"
  apply (rule ccontr)  (* ⟦¬ (∀x. P x); ∄x. ¬ P x⟧ ⟹ False *)
  apply (erule notE)   (* ∄x. ¬ P x ⟹ ∀x. P x *)
  apply (rule allI)    (* ⋀x. ∄x. ¬ P x ⟹ P x *)
  apply (rule ccontr)  (* ⋀x. ⟦∄x. ¬ P x; ¬ P x⟧ ⟹ False *)
  apply (erule notE)   (* ⋀x. ¬ P x ⟹ ∃x. ¬ P x *)
  apply (erule exI)    (* *)
  done

lemma ej30b: "(∃x. ¬P x) ⟹ ¬(∀x. P x)"
  apply (rule notI)     (* ⟦¬ (∀x. P x); ∄x. ¬ P x⟧ ⟹ False *)
  apply (erule exE)     (* ⋀x. ⟦∀x. P x; ¬ P x⟧ ⟹ False *)
  apply (drule spec)    (* ⋀x. ⟦¬ P x; P (?x4 x)⟧ ⟹ False *)
  apply (erule notE)    (* ⋀x. P (?x4 x) ⟹ P x *)
  apply assumption      (* *)
  done
    
lemma ej30: "(¬(∀x. P x)) ⟷ (∃x. ¬P x)"
  apply (rule iffI)     (* ¬ (∀x. P x) ⟹ ∃x. ¬ P x
                           ∃x. ¬ P x ⟹ ¬ (∀x. P x) *)
   apply (erule ej30a)  (* ∃x. ¬ P x ⟹ ¬ (∀x. P x) *)
   apply (erule ej30b)  (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 31. Demostrar o refutar
     {∀x. P a x x, 
      ∀x y z. P x y z ⟶ P (f x) y (f z)} 
     ⊢ P (f a) a (f a)
  ------------------------------------------------------------------ *}

lemma ej31: "⟦ ∀x. P a x x;
              ∀x y z. P x y z ⟶ P (f x) y (f z) ⟧
             ⟹ P (f a) a (f a)"
  apply (erule allE)+   (* ⟦P a ?x ?x;
                            P ?x2 ?y4 ?z6 ⟶ P (f ?x2) ?y4 (f ?z6)⟧
                           ⟹ P (f a) a (f a) *)
  apply (erule mp)      (* P a ?x ?x ⟹ P a a a *)
   apply assumption     (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 32. 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))
  ------------------------------------------------------------------ *}

lemma ej32: "⟦ ∀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))"
  apply (erule allE)+  (* ⟦P a ?x ?x;
                           P ?x2 ?y4 ?z6 ⟶ P (f ?x2) ?y4 (f ?z6)⟧
                          ⟹ ∃z. P (f a) z (f (f a)) *)
  apply (drule mp)     (* P a ?x ?x ⟹ P ?x2 ?y4 ?z6
                          ⟦P a ?x ?x; P (f ?x2) ?y4 (f ?z6)⟧
                          ⟹ ∃z. P (f a) z (f (f a)) *)
   apply assumption    (* ⟦P a ?x ?x; P (f a) ?x (f ?x)⟧
                          ⟹ ∃z. P (f a) z (f (f a)) *)
  apply (erule exI)    (* *)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 33. 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))
  ------------------------------------------------------------------ *}

lemma ej33: "⟦ ∀y. Q a y;
               ∀x y. Q x y ⟶ Q (s x) (s y) ⟧
             ⟹ ∃z. Q a z ∧ Q z (s (s a))"
  apply (erule allE)+   (* ⟦Q a ?y; 
                            Q ?x2 ?y4 ⟶ Q (s ?x2) (s ?y4)⟧
                           ⟹ ∃z. Q a z ∧ Q z (s (s a)) *)
  apply (drule mp)      (* Q a ?y ⟹ Q ?x2 ?y4
                           ⟦Q a ?y; Q (s ?x2) (s ?y4)⟧
                           ⟹ ∃z. Q a z ∧ Q z (s (s a)) *)
   apply assumption     (* ⟦Q a ?y; Q (s ?x2) (s ?y4)⟧
                           ⟹ ∃z. Q a z ∧ Q z (s (s a))*)
  apply (rule exI)      (* ⟦Q a ?y; Q (s a) (s ?y)⟧
                           ⟹ Q a ?z9 ∧ Q ?z9 (s (s a)) *) 
  apply (rule conjI)    (* ⟦Q a ?y; Q (s a) (s ?y)⟧ ⟹ Q a ?z9
                           ⟦Q a ?y; Q (s a) (s ?y)⟧ ⟹ Q ?z9 (s (s a)) *) 
   apply assumption+    (* *)
  done

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

lemma ejercicio_34a:
  "⟦∀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))"
  apply (erule allE)+  (* ⟦P a ?x ?x;
                           P ?x2 ?y4 ?z6 ⟶ P (f ?x2) ?y4 (f ?z6)⟧
                          ⟹ ∃z. P (f a) z (f (f a)) *)
  apply (drule mp)     (* P a ?x ?x ⟹ P ?x2 ?y4 ?z6
                          ⟦P a ?x ?x; P (f ?x2) ?y4 (f ?z6)⟧
                          ⟹ ∃z. P (f a) z (f (f a)) *)
   apply assumption    (* ⟦P a ?x ?x; P (f ?x2) ?y4 (f ?z6)⟧
                          ⟹ ∃z. P (f a) z (f (f a)) *)
  apply (erule exI)    (* *)
  done

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

lemma ejercicio_35a:
  "⟦∀y. Q a y; 
    ∀x y. Q x y ⟶ Q (s x) (s y)⟧ 
   ⟹ ∃z. Q a z ∧ Q z (s (s a))"
  apply (erule allE)+  (* ⟦Q a ?y; Q ?x2 ?y4 ⟶ Q (s ?x2) (s ?y4)⟧
                          ⟹ ∃z. Q a z ∧ Q z (s (s a)) *)
  apply (drule mp)     (* Q a ?y ⟹ Q ?x2 ?y4
                          ⟦Q a ?y; Q (s ?x2) (s ?y4)⟧
                          ⟹ ∃z. Q a z ∧ Q z (s (s a)) *)
   apply assumption    (* ⟦Q a ?y; Q (s ?x2) (s ?y4)⟧
                          ⟹ ∃z. Q a z ∧ Q z (s (s a)) *)
  apply (rule exI)     (* ⟦Q a ?y; Q (s a) (s ?y)⟧
                          ⟹ Q a ?z9 ∧ Q ?z9 (s (s a)) *)
  apply (rule conjI)   (* ⟦Q a ?y; Q (s a) (s ?y)⟧ ⟹ Q a ?z9
                          ⟦Q a ?y; Q (s a) (s ?y)⟧ ⟹ Q ?z9 (s (s a)) *)
   apply assumption+   (* *)
  done

text {* --------------------------------------------------------------- 
  Ejercicio 36. Demostrar o refutar
     {x = f x, odd (f x)} ⊢ odd x
  ------------------------------------------------------------------ *}

lemma ejercicio_36a:
  "⟦x = f x; odd (f x)⟧ ⟹ odd x"
  apply(drule sym)     (* ⟦odd (f x); f x = x⟧ ⟹ odd x *)
  apply (drule subst)  (* odd (f x) ⟹ ?P2 (f x)
                          ⟦odd (f x); ?P2 x⟧ ⟹ odd x *)
   apply assumption    (* ⟦odd (f x); odd x⟧ ⟹ odd x*)
  apply assumption     (* *)
  done

lemma ejercicio_36b:
  "⟦x = f x; odd (f x)⟧ ⟹ odd x"
  apply (erule ssubst) (* odd (f x) ⟹ odd (f x) *)
  apply assumption     (* *)
  done

lemma ejercicio_36c:
  "⟦x = f x; odd (f x)⟧ ⟹ odd x"
by (rule ssubst)

text {* --------------------------------------------------------------- 
  Ejercicio 37. Demostrar o refutar
     {x = f x, triple (f x) (f x) x} ⊢ triple x x x
  ------------------------------------------------------------------ *}

lemma ejercicio_37a:
  "⟦x = f x; triple (f x) (f x) x⟧ ⟹ triple x x x"
  apply (drule sym)   (* ⟦triple (f x) (f x) x; f x = x⟧
                         ⟹ triple x x x *)
  apply (drule subst) (* triple (f x) (f x) x ⟹ ?P2 (f x)
                         ⟦triple (f x) (f x) x; ?P2 x⟧ ⟹ triple x x x *)
   apply assumption   (* ⟦triple (f x) (f x) x; triple x x x⟧
                         ⟹ triple x x x *)
  apply assumption    (* *)
  done                

lemma ejercicio_37b:
  "⟦x = f x; triple (f x) (f x) x⟧ ⟹ triple x x x"
  apply (drule_tac s="f x" in ssubst)
                      (* triple (f x) (f x) x ⟹ ?P (f x)
                         ⟦triple (f x) (f x) x; ?P x⟧ ⟹ triple x x x *)
   apply assumption   (* ⟦triple (f x) (f x) x; triple x x x⟧
                         ⟹ triple x x x *)
  apply assumption    (* *)
  done                

lemma ejercicio_37c:
  "⟦x = f x; triple (f x) (f x) x⟧ ⟹ triple x x x"
  by (rule ssubst)

end
</source>