theory a1
imports Main
begin

text \<open> Question 1 \<close>

text \<open>
Insert your answer here, or in a separate .pdf or .txt file
\<close>

text \<open> Question 2 \<close>

text \<open>
Insert your answer here, or in a separate .pdf or .txt file
\<close>


text \<open> Question 3 \<close>

lemma prop_a:
  "B \<longrightarrow> A \<or> B \<or> C"
  sorry

lemma prop_b:
  "(A \<longrightarrow> B) \<and> (B \<longrightarrow> C) \<and> (C \<longrightarrow> D) \<longrightarrow> A \<longrightarrow> D"
  sorry

lemma prop_c:
  "((A \<or> B) \<and> C) = (A \<and> C \<or> C \<and> B)"
  sorry

lemma prop_d:
  "(\<not>P) = (\<not>\<not>\<not>P)"
  sorry

lemma prop_e:
  "(A\<longrightarrow>B) = (\<not> (\<not>B \<and> A))"
  sorry

lemma prop_f:
  "((A\<or>C)\<and>(C\<longrightarrow>A)\<and>(A\<longrightarrow>D))\<longrightarrow>D"
  sorry


text \<open> Question 4 \<close>

lemma hol_a:
  "(\<forall>x. P x) \<and> (\<forall>x. Q x) \<longrightarrow> (\<forall>x. Q x \<and> P x)"
  sorry


lemma hol_b:
  "(\<forall>x. P x \<longrightarrow> Q x) \<and> (\<forall>x. P x)  \<longrightarrow> (\<forall>x. Q x)"
  sorry


lemma hol_c:
  "(\<forall>x. P x \<or> Q x) \<and> ((\<exists>x. Q x) \<longrightarrow> W) \<and> ((\<exists>x. P x)\<longrightarrow> Z) \<longrightarrow> W \<or> Z"
  sorry


lemma hol_d:
  "(\<forall>x. R x x) \<longrightarrow>\<not>(\<forall> x y. R y x \<longrightarrow> \<not> R x y)"
  sorry

end