theory Exercises1 imports Main begin

text {*
  Proof (in single steps:)
*}

lemma "\<not>A \<longrightarrow> \<not>B \<Longrightarrow> B \<longrightarrow> A"
  oops

lemma "(A \<longrightarrow> B) = (\<not>A \<or> B)" 
  oops

lemma "(P \<longrightarrow> Q) \<longrightarrow> ((Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> R))"
  oops

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

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

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

end