[STATEMENT]
lemma Deduction2: "(F \<^bold>\<rightarrow> \<bottom>) \<triangleright> (AX1 \<union> \<Gamma>) \<turnstile>\<^sub>H \<bottom> \<longleftrightarrow> (AX1 \<union> \<Gamma>) \<turnstile>\<^sub>H F" (is "?l \<longleftrightarrow> ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom>) = (AX1 \<union> \<Gamma> \<turnstile>\<^sub>H F)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom> \<Longrightarrow> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H F
 2. AX1 \<union> \<Gamma> \<turnstile>\<^sub>H F \<Longrightarrow> F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
assume l: ?l
[PROOF STATE]
proof (state)
this:
F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom>

goal (2 subgoals):
 1. F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom> \<Longrightarrow> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H F
 2. AX1 \<union> \<Gamma> \<turnstile>\<^sub>H F \<Longrightarrow> F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
with Deduction_theorem[where \<Gamma>="AX1 \<union> \<Gamma>" and F="F \<^bold>\<rightarrow> \<bottom>" and G=\<bottom>]
[PROOF STATE]
proof (chain)
picking this:
AX0 \<union> (F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> \<Gamma>) \<turnstile>\<^sub>H \<bottom> \<Longrightarrow> AX0 \<union> (AX1 \<union> \<Gamma>) \<turnstile>\<^sub>H (F \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> \<bottom>
F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
have "AX1 \<union> \<Gamma> \<turnstile>\<^sub>H (F \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> \<bottom>"
[PROOF STATE]
proof (prove)
using this:
AX0 \<union> (F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> \<Gamma>) \<turnstile>\<^sub>H \<bottom> \<Longrightarrow> AX0 \<union> (AX1 \<union> \<Gamma>) \<turnstile>\<^sub>H (F \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> \<bottom>
F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom>

goal (1 subgoal):
 1. AX1 \<union> \<Gamma> \<turnstile>\<^sub>H (F \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> \<bottom>
[PROOF STEP]
unfolding AX1_away
[PROOF STATE]
proof (prove)
using this:
AX0 \<union> (F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX0 \<union> (\<Gamma> \<union> AX1)) \<turnstile>\<^sub>H \<bottom> \<Longrightarrow> AX0 \<union> (AX0 \<union> (\<Gamma> \<union> AX1)) \<turnstile>\<^sub>H (F \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> \<bottom>
F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX0 \<union> (\<Gamma> \<union> AX1) \<turnstile>\<^sub>H \<bottom>

goal (1 subgoal):
 1. AX0 \<union> (\<Gamma> \<union> AX1) \<turnstile>\<^sub>H (F \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> \<bottom>
[PROOF STEP]
by(simp add: Un_commute)
[PROOF STATE]
proof (state)
this:
AX1 \<union> \<Gamma> \<turnstile>\<^sub>H (F \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> \<bottom>

goal (2 subgoals):
 1. F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom> \<Longrightarrow> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H F
 2. AX1 \<union> \<Gamma> \<turnstile>\<^sub>H F \<Longrightarrow> F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
AX1 \<union> \<Gamma> \<turnstile>\<^sub>H (F \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> \<bottom>

goal (2 subgoals):
 1. F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom> \<Longrightarrow> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H F
 2. AX1 \<union> \<Gamma> \<turnstile>\<^sub>H F \<Longrightarrow> F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
have "AX1 \<union> \<Gamma> \<turnstile>\<^sub>H ((F \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AX1 \<union> \<Gamma> \<turnstile>\<^sub>H ((F \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> F
[PROOF STEP]
using AX1.intros(2) HC.Ax
[PROOF STATE]
proof (prove)
using this:
((?F \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> ?F \<in> AX1
?F \<in> ?\<Gamma> \<Longrightarrow> ?\<Gamma> \<turnstile>\<^sub>H ?F

goal (1 subgoal):
 1. AX1 \<union> \<Gamma> \<turnstile>\<^sub>H ((F \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> F
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
AX1 \<union> \<Gamma> \<turnstile>\<^sub>H ((F \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> F

goal (2 subgoals):
 1. F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom> \<Longrightarrow> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H F
 2. AX1 \<union> \<Gamma> \<turnstile>\<^sub>H F \<Longrightarrow> F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
AX1 \<union> \<Gamma> \<turnstile>\<^sub>H (F \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> \<bottom>
AX1 \<union> \<Gamma> \<turnstile>\<^sub>H ((F \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> F
[PROOF STEP]
show ?r
[PROOF STATE]
proof (prove)
using this:
AX1 \<union> \<Gamma> \<turnstile>\<^sub>H (F \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> \<bottom>
AX1 \<union> \<Gamma> \<turnstile>\<^sub>H ((F \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> F

goal (1 subgoal):
 1. AX1 \<union> \<Gamma> \<turnstile>\<^sub>H F
[PROOF STEP]
using HC.MP
[PROOF STATE]
proof (prove)
using this:
AX1 \<union> \<Gamma> \<turnstile>\<^sub>H (F \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> \<bottom>
AX1 \<union> \<Gamma> \<turnstile>\<^sub>H ((F \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> \<bottom>) \<^bold>\<rightarrow> F
\<lbrakk>?\<Gamma> \<turnstile>\<^sub>H ?F; ?\<Gamma> \<turnstile>\<^sub>H ?F \<^bold>\<rightarrow> ?G\<rbrakk> \<Longrightarrow> ?\<Gamma> \<turnstile>\<^sub>H ?G

goal (1 subgoal):
 1. AX1 \<union> \<Gamma> \<turnstile>\<^sub>H F
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
AX1 \<union> \<Gamma> \<turnstile>\<^sub>H F

goal (1 subgoal):
 1. AX1 \<union> \<Gamma> \<turnstile>\<^sub>H F \<Longrightarrow> F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. AX1 \<union> \<Gamma> \<turnstile>\<^sub>H F \<Longrightarrow> F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
assume r: ?r
[PROOF STATE]
proof (state)
this:
AX1 \<union> \<Gamma> \<turnstile>\<^sub>H F

goal (1 subgoal):
 1. AX1 \<union> \<Gamma> \<turnstile>\<^sub>H F \<Longrightarrow> F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
thus ?l
[PROOF STATE]
proof (prove)
using this:
AX1 \<union> \<Gamma> \<turnstile>\<^sub>H F

goal (1 subgoal):
 1. F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
by (meson HC.simps HC_mono insertI1 subset_insertI)
[PROOF STATE]
proof (state)
this:
F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom>

goal:
No subgoals!
[PROOF STEP]
qed