theory a2 imports Main begin

(* use this template for questions 1, 2, and 4. Use a different file
with theory Demo5 from Wed, week 4, as a base theory for question 3 *)

lemma "(\<forall>x. \<forall>y. R x y) = (\<forall>y. \<forall>x. R x y)" 
  oops

lemma "((\<exists>x. P x) \<or> (\<exists>x. Q x)) = (\<exists>x. (P x \<or> Q x))"
  oops

lemma "((\<forall>x. P x) \<and> (\<forall>x. Q x)) = (\<forall>x. (P x \<and> Q x))" 
  oops

lemma "\<not>(\<forall>x. P x) \<Longrightarrow> \<exists>x. \<not> P x" 
  oops

lemma "\<not>(\<exists>x. P x) \<Longrightarrow> \<forall>x. \<not> P x" 
  oops

lemma "(\<forall>x. P x \<longrightarrow> Q) = ((\<exists>x. P x) \<longrightarrow> Q)"
  oops

end