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
