theory a1 
imports Main 
begin


lemma p_a: "(A\<and>B)\<longrightarrow> (\<not>(C\<and>\<not>A))\<and>(C\<longrightarrow>B)"
sorry

lemma p_b: "(\<not> (a\<longrightarrow>b))=(a \<and> \<not> b)"
sorry

lemma p_c: " \<lbrakk>((\<not> a) = b)\<rbrakk> \<Longrightarrow> (a= (\<not> b)) "
sorry

lemma p_d: "(((f\<longrightarrow>g)\<longrightarrow>(h\<longrightarrow>f))\<longrightarrow>g) = ((f\<longrightarrow>g) \<and> (g\<or>h))"
sorry

lemma p_e: "(a\<longrightarrow>b)=(\<not> (a \<and> \<not> b))"
sorry

lemma p_f: "(a\<longrightarrow>b)=(\<not> (a \<and> \<not> b))"
sorry

end