[STATEMENT]
lemma
  "\<Gamma> \<Rightarrow> \<Delta> \<Longrightarrow> is_mini_mset \<Gamma> \<Longrightarrow> is_mini_mset \<Delta> \<Longrightarrow>
  (set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1) \<turnstile>\<^sub>H \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> \<Rightarrow> \<Delta>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
proof(induction "\<Gamma>" "\<Delta>" rule: SCp.induct)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>k \<Gamma> \<Delta>. \<lbrakk>Atom k \<in># \<Gamma>; Atom k \<in># \<Delta>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 8. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 9. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<rightarrow> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 10. \<And>F \<Gamma> G \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<rightarrow> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
case (ImpL \<Gamma> F \<Delta> G)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<Rightarrow> F, \<Delta>
G, \<Gamma> \<Rightarrow> \<Delta>
\<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
\<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
is_mini_mset (F \<^bold>\<rightarrow> G, \<Gamma>)
is_mini_mset \<Delta>

goal (10 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>k \<Gamma> \<Delta>. \<lbrakk>Atom k \<in># \<Gamma>; Atom k \<in># \<Delta>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 8. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 9. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<rightarrow> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 10. \<And>F \<Gamma> G \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<rightarrow> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
from ImpL.prems
[PROOF STATE]
proof (chain)
picking this:
is_mini_mset (F \<^bold>\<rightarrow> G, \<Gamma>)
is_mini_mset \<Delta>
[PROOF STEP]
have "is_mini_mset \<Gamma>" "is_mini_mset (F, \<Delta>)"
[PROOF STATE]
proof (prove)
using this:
is_mini_mset (F \<^bold>\<rightarrow> G, \<Gamma>)
is_mini_mset \<Delta>

goal (1 subgoal):
 1. is_mini_mset \<Gamma> &&& is_mini_mset (F, \<Delta>)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
is_mini_mset \<Gamma>
is_mini_mset (F, \<Delta>)

goal (10 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>k \<Gamma> \<Delta>. \<lbrakk>Atom k \<in># \<Gamma>; Atom k \<in># \<Delta>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 8. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 9. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<rightarrow> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 10. \<And>F \<Gamma> G \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<rightarrow> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
with ImpL.IH(1)
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
is_mini_mset \<Gamma>
is_mini_mset (F, \<Delta>)
[PROOF STEP]
have IH1: "set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
is_mini_mset \<Gamma>
is_mini_mset (F, \<Delta>)

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

goal (10 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>k \<Gamma> \<Delta>. \<lbrakk>Atom k \<in># \<Gamma>; Atom k \<in># \<Delta>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 8. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 9. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<rightarrow> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 10. \<And>F \<Gamma> G \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<rightarrow> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
hence IH1: "F \<^bold>\<rightarrow> \<bottom> \<triangleright> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>"
[PROOF STATE]
proof (prove)
using this:
set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>

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

goal (10 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>k \<Gamma> \<Delta>. \<lbrakk>Atom k \<in># \<Gamma>; Atom k \<in># \<Delta>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 8. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 9. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<rightarrow> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 10. \<And>F \<Gamma> G \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<rightarrow> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
from ImpL.prems
[PROOF STATE]
proof (chain)
picking this:
is_mini_mset (F \<^bold>\<rightarrow> G, \<Gamma>)
is_mini_mset \<Delta>
[PROOF STEP]
have "is_mini_mset (G, \<Gamma>)" "is_mini_mset \<Delta>"
[PROOF STATE]
proof (prove)
using this:
is_mini_mset (F \<^bold>\<rightarrow> G, \<Gamma>)
is_mini_mset \<Delta>

goal (1 subgoal):
 1. is_mini_mset (G, \<Gamma>) &&& is_mini_mset \<Delta>
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
is_mini_mset (G, \<Gamma>)
is_mini_mset \<Delta>

goal (10 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>k \<Gamma> \<Delta>. \<lbrakk>Atom k \<in># \<Gamma>; Atom k \<in># \<Delta>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 8. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 9. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<rightarrow> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 10. \<And>F \<Gamma> G \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<rightarrow> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
with ImpL.IH(2)
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
is_mini_mset (G, \<Gamma>)
is_mini_mset \<Delta>
[PROOF STEP]
have IH2: "set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
is_mini_mset (G, \<Gamma>)
is_mini_mset \<Delta>

goal (1 subgoal):
 1. set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>

goal (10 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>k \<Gamma> \<Delta>. \<lbrakk>Atom k \<in># \<Gamma>; Atom k \<in># \<Delta>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 8. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 9. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<rightarrow> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 10. \<And>F \<Gamma> G \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<rightarrow> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
hence IH2: "G \<triangleright> (set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1) \<turnstile>\<^sub>H \<bottom>"
[PROOF STATE]
proof (prove)
using this:
set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>

goal (1 subgoal):
 1. G \<triangleright> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
G \<triangleright> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>

goal (10 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>k \<Gamma> \<Delta>. \<lbrakk>Atom k \<in># \<Gamma>; Atom k \<in># \<Delta>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 8. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 9. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<rightarrow> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 10. \<And>F \<Gamma> G \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<rightarrow> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
have R: "F \<^bold>\<rightarrow> G \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom>" if "G \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom>" "F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom>" for \<Gamma>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<^bold>\<rightarrow> G \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
G \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom>
F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom>

goal (1 subgoal):
 1. F \<^bold>\<rightarrow> G \<triangleright> AX1 \<union> \<Gamma> \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
by (metis Ax Deduction1 Deduction2 HC_mono MP insertI1 subset_insertI)
[PROOF STATE]
proof (state)
this:
\<lbrakk>G \<triangleright> AX1 \<union> ?\<Gamma> \<turnstile>\<^sub>H \<bottom>; F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> ?\<Gamma> \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> F \<^bold>\<rightarrow> G \<triangleright> AX1 \<union> ?\<Gamma> \<turnstile>\<^sub>H \<bottom>

goal (10 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>k \<Gamma> \<Delta>. \<lbrakk>Atom k \<in># \<Gamma>; Atom k \<in># \<Delta>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 8. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 9. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<rightarrow> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 10. \<And>F \<Gamma> G \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<rightarrow> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
(* I don't construct the actual proofs for the Rs. Sledgehammer is doing all the interesting work. :/ *)
[PROOF STATE]
proof (state)
this:
\<lbrakk>G \<triangleright> AX1 \<union> ?\<Gamma> \<turnstile>\<^sub>H \<bottom>; F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> ?\<Gamma> \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> F \<^bold>\<rightarrow> G \<triangleright> AX1 \<union> ?\<Gamma> \<turnstile>\<^sub>H \<bottom>

goal (10 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>k \<Gamma> \<Delta>. \<lbrakk>Atom k \<in># \<Gamma>; Atom k \<in># \<Delta>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 8. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 9. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<rightarrow> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 10. \<And>F \<Gamma> G \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<rightarrow> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
from R[where \<Gamma>="set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta>"]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>G \<triangleright> AX1 \<union> (set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta>) \<turnstile>\<^sub>H \<bottom>; F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> (set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta>) \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> F \<^bold>\<rightarrow> G \<triangleright> AX1 \<union> (set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta>) \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
have "F \<^bold>\<rightarrow> G \<triangleright> (set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1) \<turnstile>\<^sub>H \<bottom>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>G \<triangleright> AX1 \<union> (set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta>) \<turnstile>\<^sub>H \<bottom>; F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> (set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta>) \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> F \<^bold>\<rightarrow> G \<triangleright> AX1 \<union> (set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta>) \<turnstile>\<^sub>H \<bottom>

goal (1 subgoal):
 1. F \<^bold>\<rightarrow> G \<triangleright> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
using IH2 IH1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>G \<triangleright> AX1 \<union> (set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta>) \<turnstile>\<^sub>H \<bottom>; F \<^bold>\<rightarrow> \<bottom> \<triangleright> AX1 \<union> (set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta>) \<turnstile>\<^sub>H \<bottom>\<rbrakk> \<Longrightarrow> F \<^bold>\<rightarrow> G \<triangleright> AX1 \<union> (set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta>) \<turnstile>\<^sub>H \<bottom>
G \<triangleright> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
F \<^bold>\<rightarrow> \<bottom> \<triangleright> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>

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

goal (10 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>k \<Gamma> \<Delta>. \<lbrakk>Atom k \<in># \<Gamma>; Atom k \<in># \<Delta>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 8. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 9. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<rightarrow> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 10. \<And>F \<Gamma> G \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<rightarrow> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
F \<^bold>\<rightarrow> G \<triangleright> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>

goal (1 subgoal):
 1. set_mset (F \<^bold>\<rightarrow> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set_mset (F \<^bold>\<rightarrow> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>

goal (9 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>k \<Gamma> \<Delta>. \<lbrakk>Atom k \<in># \<Gamma>; Atom k \<in># \<Delta>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 8. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 9. \<And>F \<Gamma> G \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<rightarrow> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>k \<Gamma> \<Delta>. \<lbrakk>Atom k \<in># \<Gamma>; Atom k \<in># \<Delta>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 8. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 9. \<And>F \<Gamma> G \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<rightarrow> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
case (ImpR F \<Gamma> G \<Delta>)
[PROOF STATE]
proof (state)
this:
F, \<Gamma> \<Rightarrow> G, \<Delta>
\<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
is_mini_mset \<Gamma>
is_mini_mset (F \<^bold>\<rightarrow> G, \<Delta>)

goal (9 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>k \<Gamma> \<Delta>. \<lbrakk>Atom k \<in># \<Gamma>; Atom k \<in># \<Delta>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 8. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 9. \<And>F \<Gamma> G \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<rightarrow> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
hence "is_mini_mset (F, \<Gamma>)" "is_mini_mset (G, \<Delta>)"
[PROOF STATE]
proof (prove)
using this:
F, \<Gamma> \<Rightarrow> G, \<Delta>
\<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
is_mini_mset \<Gamma>
is_mini_mset (F \<^bold>\<rightarrow> G, \<Delta>)

goal (1 subgoal):
 1. is_mini_mset (F, \<Gamma>) &&& is_mini_mset (G, \<Delta>)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
is_mini_mset (F, \<Gamma>)
is_mini_mset (G, \<Delta>)

goal (9 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>k \<Gamma> \<Delta>. \<lbrakk>Atom k \<in># \<Gamma>; Atom k \<in># \<Delta>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 8. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 9. \<And>F \<Gamma> G \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<rightarrow> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
with ImpR.IH
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
is_mini_mset (F, \<Gamma>)
is_mini_mset (G, \<Delta>)
[PROOF STEP]
have IH: "F \<triangleright> G \<^bold>\<rightarrow> \<bottom> \<triangleright> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
is_mini_mset (F, \<Gamma>)
is_mini_mset (G, \<Delta>)

goal (1 subgoal):
 1. F \<triangleright> G \<^bold>\<rightarrow> \<bottom> \<triangleright> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
by(simp add: insert_commute)
[PROOF STATE]
proof (state)
this:
F \<triangleright> G \<^bold>\<rightarrow> \<bottom> \<triangleright> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>

goal (9 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>k \<Gamma> \<Delta>. \<lbrakk>Atom k \<in># \<Gamma>; Atom k \<in># \<Delta>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 8. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 9. \<And>F \<Gamma> G \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<rightarrow> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
have R: "(F \<^bold>\<rightarrow> G) \<^bold>\<rightarrow> \<bottom> \<triangleright> \<Gamma> \<union> AX1 \<turnstile>\<^sub>H \<bottom>" if "F \<triangleright> G \<^bold>\<rightarrow> \<bottom> \<triangleright> \<Gamma> \<union> AX1 \<turnstile>\<^sub>H \<bottom>" for \<Gamma>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (F \<^bold>\<rightarrow> G) \<^bold>\<rightarrow> \<bottom> \<triangleright> \<Gamma> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
F \<triangleright> G \<^bold>\<rightarrow> \<bottom> \<triangleright> \<Gamma> \<union> AX1 \<turnstile>\<^sub>H \<bottom>

goal (1 subgoal):
 1. (F \<^bold>\<rightarrow> G) \<^bold>\<rightarrow> \<bottom> \<triangleright> \<Gamma> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
by (metis AX1_away Deduction2 Deduction_theorem Un_commute Un_insert_right)
[PROOF STATE]
proof (state)
this:
F \<triangleright> G \<^bold>\<rightarrow> \<bottom> \<triangleright> ?\<Gamma> \<union> AX1 \<turnstile>\<^sub>H \<bottom> \<Longrightarrow> (F \<^bold>\<rightarrow> G) \<^bold>\<rightarrow> \<bottom> \<triangleright> ?\<Gamma> \<union> AX1 \<turnstile>\<^sub>H \<bottom>

goal (9 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>k \<Gamma> \<Delta>. \<lbrakk>Atom k \<in># \<Gamma>; Atom k \<in># \<Delta>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 8. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 9. \<And>F \<Gamma> G \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<rightarrow> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<rightarrow> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
F \<triangleright> G \<^bold>\<rightarrow> \<bottom> \<triangleright> ?\<Gamma> \<union> AX1 \<turnstile>\<^sub>H \<bottom> \<Longrightarrow> (F \<^bold>\<rightarrow> G) \<^bold>\<rightarrow> \<bottom> \<triangleright> ?\<Gamma> \<union> AX1 \<turnstile>\<^sub>H \<bottom>

goal (1 subgoal):
 1. set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<rightarrow> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
F \<triangleright> G \<^bold>\<rightarrow> \<bottom> \<triangleright> ?\<Gamma> \<union> AX1 \<turnstile>\<^sub>H \<bottom> \<Longrightarrow> (F \<^bold>\<rightarrow> G) \<^bold>\<rightarrow> \<bottom> \<triangleright> ?\<Gamma> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
F \<triangleright> G \<^bold>\<rightarrow> \<bottom> \<triangleright> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>

goal (1 subgoal):
 1. set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<rightarrow> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<rightarrow> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>

goal (8 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>k \<Gamma> \<Delta>. \<lbrakk>Atom k \<in># \<Gamma>; Atom k \<in># \<Delta>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 8. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>k \<Gamma> \<Delta>. \<lbrakk>Atom k \<in># \<Gamma>; Atom k \<in># \<Delta>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 8. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
case (Ax k \<Gamma> \<Delta>)
[PROOF STATE]
proof (state)
this:
Atom k \<in># \<Gamma>
Atom k \<in># \<Delta>
is_mini_mset \<Gamma>
is_mini_mset \<Delta>

goal (8 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>k \<Gamma> \<Delta>. \<lbrakk>Atom k \<in># \<Gamma>; Atom k \<in># \<Delta>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 8. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
have R: "F \<triangleright> F \<^bold>\<rightarrow> \<bottom> \<triangleright> \<Gamma> \<union> AX1 \<turnstile>\<^sub>H \<bottom>" for F :: "'a formula" and \<Gamma>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<triangleright> F \<^bold>\<rightarrow> \<bottom> \<triangleright> \<Gamma> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
by (meson HC.simps insert_iff)
[PROOF STATE]
proof (state)
this:
?F \<triangleright> ?F \<^bold>\<rightarrow> \<bottom> \<triangleright> ?\<Gamma> \<union> AX1 \<turnstile>\<^sub>H \<bottom>

goal (8 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>k \<Gamma> \<Delta>. \<lbrakk>Atom k \<in># \<Gamma>; Atom k \<in># \<Delta>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 8. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
from R[where F="Atom k" and \<Gamma>="set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta>"]
[PROOF STATE]
proof (chain)
picking this:
Atom k \<triangleright> Atom k \<^bold>\<rightarrow> \<bottom> \<triangleright> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Atom k \<triangleright> Atom k \<^bold>\<rightarrow> \<bottom> \<triangleright> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>

goal (1 subgoal):
 1. set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
using Ax.hyps
[PROOF STATE]
proof (prove)
using this:
Atom k \<triangleright> Atom k \<^bold>\<rightarrow> \<bottom> \<triangleright> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
Atom k \<in># \<Gamma>
Atom k \<in># \<Delta>

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

goal (7 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
case BotL
[PROOF STATE]
proof (state)
this:
\<bottom> \<in># \<Gamma>_
is_mini_mset \<Gamma>_
is_mini_mset \<Delta>_

goal (7 subgoals):
 1. \<And>\<Gamma> \<Delta>. \<lbrakk>\<bottom> \<in># \<Gamma>; is_mini_mset \<Gamma>; is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 7. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<bottom> \<in># \<Gamma>_
is_mini_mset \<Gamma>_
is_mini_mset \<Delta>_

goal (1 subgoal):
 1. set_mset \<Gamma>_ \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta>_ \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
by (simp add: HC.Ax)
[PROOF STATE]
proof (state)
this:
set_mset \<Gamma>_ \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta>_ \<union> AX1 \<turnstile>\<^sub>H \<bottom>

goal (6 subgoals):
 1. \<And>\<Gamma> F \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (\<^bold>\<not> F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (\<^bold>\<not> F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 2. \<And>F \<Gamma> \<Delta>. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (\<^bold>\<not> F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (\<^bold>\<not> F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 3. \<And>F G \<Gamma> \<Delta>. \<lbrakk>F, G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<and> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<and> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 4. \<And>\<Gamma> F \<Delta> G. \<lbrakk>\<Gamma> \<Rightarrow> F, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; \<Gamma> \<Rightarrow> G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<and> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<and> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 5. \<And>F \<Gamma> \<Delta> G. \<lbrakk>F, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (F, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; G, \<Gamma> \<Rightarrow> \<Delta>; \<lbrakk>is_mini_mset (G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset (F \<^bold>\<or> G, \<Gamma>); is_mini_mset \<Delta>\<rbrakk> \<Longrightarrow> set_mset (F \<^bold>\<or> G, \<Gamma>) \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset \<Delta> \<union> AX1 \<turnstile>\<^sub>H \<bottom>
 6. \<And>\<Gamma> F G \<Delta>. \<lbrakk>\<Gamma> \<Rightarrow> F, G, \<Delta>; \<lbrakk>is_mini_mset \<Gamma>; is_mini_mset (F, G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F, G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>; is_mini_mset \<Gamma>; is_mini_mset (F \<^bold>\<or> G, \<Delta>)\<rbrakk> \<Longrightarrow> set_mset \<Gamma> \<union> (\<lambda>F. F \<^bold>\<rightarrow> \<bottom>) ` set_mset (F \<^bold>\<or> G, \<Delta>) \<union> AX1 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
qed simp_all