[STATEMENT]
lemma dep_biunion_imp_or_dep:
  fixes PROB vs S
  assumes "(dep_var_set PROB vs (\<Union>S))"
  shows "(\<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs vs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs vs'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs vs'
[PROOF STEP]
obtain v1 v2 where obtain_v1_v2: "v1 \<in> vs" "v2 \<in> (\<Union>S)" "disjnt vs (\<Union>S)" "dep PROB v1 v2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v1 v2. \<lbrakk>v1 \<in> vs; v2 \<in> \<Union> S; disjnt vs (\<Union> S); dep PROB v1 v2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms dep_var_set_def[of PROB vs "\<Union> S"]
[PROOF STATE]
proof (prove)
using this:
dep_var_set PROB vs (\<Union> S)
dep_var_set PROB vs (\<Union> S) \<equiv> disjnt vs (\<Union> S) \<and> (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> \<Union> S \<and> dep PROB v1 v2)

goal (1 subgoal):
 1. (\<And>v1 v2. \<lbrakk>v1 \<in> vs; v2 \<in> \<Union> S; disjnt vs (\<Union> S); dep PROB v1 v2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v1 \<in> vs
v2 \<in> \<Union> S
disjnt vs (\<Union> S)
dep PROB v1 v2

goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs vs'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v1 \<in> vs
v2 \<in> \<Union> S
disjnt vs (\<Union> S)
dep PROB v1 v2

goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs vs'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
v1 \<in> vs
v2 \<in> \<Union> S
disjnt vs (\<Union> S)
dep PROB v1 v2

goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs vs'
[PROOF STEP]
fix vs'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs vs'
[PROOF STEP]
assume "vs' \<in> S"
[PROOF STATE]
proof (state)
this:
vs' \<in> S

goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs vs'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vs' \<in> S
[PROOF STEP]
have "vs' \<subseteq> (\<Union>S)"
[PROOF STATE]
proof (prove)
using this:
vs' \<in> S

goal (1 subgoal):
 1. vs' \<subseteq> \<Union> S
[PROOF STEP]
using calculation Union_upper
[PROOF STATE]
proof (prove)
using this:
vs' \<in> S
v1 \<in> vs
v2 \<in> \<Union> S
disjnt vs (\<Union> S)
dep PROB v1 v2
?B \<in> ?A \<Longrightarrow> ?B \<subseteq> \<Union> ?A

goal (1 subgoal):
 1. vs' \<subseteq> \<Union> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vs' \<subseteq> \<Union> S

goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs vs'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vs' \<subseteq> \<Union> S

goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs vs'
[PROOF STEP]
have "disjnt (\<Union>S) vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. disjnt (\<Union> S) vs
[PROOF STEP]
using obtain_v1_v2(3) disjnt_sym
[PROOF STATE]
proof (prove)
using this:
disjnt vs (\<Union> S)
disjnt ?A ?B \<Longrightarrow> disjnt ?B ?A

goal (1 subgoal):
 1. disjnt (\<Union> S) vs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
disjnt (\<Union> S) vs

goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs vs'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
vs' \<subseteq> \<Union> S
disjnt (\<Union> S) vs
[PROOF STEP]
have "disjnt vs vs'"
[PROOF STATE]
proof (prove)
using this:
vs' \<subseteq> \<Union> S
disjnt (\<Union> S) vs

goal (1 subgoal):
 1. disjnt vs vs'
[PROOF STEP]
using obtain_v1_v2(3) disjnt_subset1 disjnt_sym
[PROOF STATE]
proof (prove)
using this:
vs' \<subseteq> \<Union> S
disjnt (\<Union> S) vs
disjnt vs (\<Union> S)
\<lbrakk>disjnt ?X ?Y; ?Z \<subseteq> ?X\<rbrakk> \<Longrightarrow> disjnt ?Z ?Y
disjnt ?A ?B \<Longrightarrow> disjnt ?B ?A

goal (1 subgoal):
 1. disjnt vs vs'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
disjnt vs vs'

goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs vs'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?vs'2 \<in> S \<Longrightarrow> disjnt vs ?vs'2

goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs vs'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
v1 \<in> vs
v2 \<in> \<Union> S
disjnt vs (\<Union> S)
dep PROB v1 v2
?vs'2 \<in> S \<Longrightarrow> disjnt vs ?vs'2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v1 \<in> vs
v2 \<in> \<Union> S
disjnt vs (\<Union> S)
dep PROB v1 v2
?vs'2 \<in> S \<Longrightarrow> disjnt vs ?vs'2

goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs vs'
[PROOF STEP]
unfolding dep_var_set_def
[PROOF STATE]
proof (prove)
using this:
v1 \<in> vs
v2 \<in> \<Union> S
disjnt vs (\<Union> S)
dep PROB v1 v2
?vs'2 \<in> S \<Longrightarrow> disjnt vs ?vs'2

goal (1 subgoal):
 1. \<exists>vs'. vs' \<in> S \<and> disjnt vs vs' \<and> (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> vs' \<and> dep PROB v1 v2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>vs'. vs' \<in> S \<and> dep_var_set PROB vs vs'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dep_tc_imp_in_dom:
  fixes PROB :: "(('a, 'b) fmap \<times> ('a, 'b) fmap) set" and v1 v2
  assumes "\<not>(v1 = v2)" "(dep_tc PROB v1 v2)"
  shows "(v1 \<in> prob_dom PROB)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v1 \<in> prob_dom PROB
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v1 \<in> prob_dom PROB
[PROOF STEP]
have "TC (dep PROB) v1 v2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TC (dep PROB) v1 v2
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
dep_tc PROB v1 v2

goal (1 subgoal):
 1. TC (dep PROB) v1 v2
[PROOF STEP]
unfolding dep_tc_def
[PROOF STATE]
proof (prove)
using this:
TC (dep PROB) v1 v2

goal (1 subgoal):
 1. TC (dep PROB) v1 v2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
TC (dep PROB) v1 v2

goal (1 subgoal):
 1. v1 \<in> prob_dom PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
TC (dep PROB) v1 v2
[PROOF STEP]
have "dep PROB v1 v2 \<or> (\<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2)"
[PROOF STATE]
proof (prove)
using this:
TC (dep PROB) v1 v2

goal (1 subgoal):
 1. dep PROB v1 v2 \<or> (\<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2)
[PROOF STEP]
using TC_CASES1_NEQ[where R = "(\<lambda>v1' v2'. dep PROB v1' v2')" and x = v1 and z = v2]
[PROOF STATE]
proof (prove)
using this:
TC (dep PROB) v1 v2
(dep PROB)\<^sup>+\<^sup>+ v1 v2 \<Longrightarrow> dep PROB v1 v2 \<or> (\<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> (dep PROB)\<^sup>+\<^sup>+ y v2)

goal (1 subgoal):
 1. dep PROB v1 v2 \<or> (\<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2)
[PROOF STEP]
by (simp add: TC_equiv_tranclp)
      \<comment> \<open>NOTE Split on the disjunction yielded by the previous step.\<close>
[PROOF STATE]
proof (state)
this:
dep PROB v1 v2 \<or> (\<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2)

goal (1 subgoal):
 1. v1 \<in> prob_dom PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dep PROB v1 v2 \<or> (\<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2)
[PROOF STEP]
consider
    (i) "dep PROB v1 v2"
    | (ii) "(\<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2)"
[PROOF STATE]
proof (prove)
using this:
dep PROB v1 v2 \<or> (\<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2)

goal (1 subgoal):
 1. \<lbrakk>dep PROB v1 v2 \<Longrightarrow> thesis; \<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2 \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<lbrakk>dep PROB v1 v2 \<Longrightarrow> ?thesis; \<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. v1 \<in> prob_dom PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>dep PROB v1 v2 \<Longrightarrow> ?thesis; \<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>dep PROB v1 v2 \<Longrightarrow> ?thesis; \<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. v1 \<in> prob_dom PROB
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dep PROB v1 v2 \<Longrightarrow> v1 \<in> prob_dom PROB
 2. \<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2 \<Longrightarrow> v1 \<in> prob_dom PROB
[PROOF STEP]
case i
[PROOF STATE]
proof (state)
this:
dep PROB v1 v2

goal (2 subgoals):
 1. dep PROB v1 v2 \<Longrightarrow> v1 \<in> prob_dom PROB
 2. \<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2 \<Longrightarrow> v1 \<in> prob_dom PROB
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
dep PROB v1 v2

goal (2 subgoals):
 1. dep PROB v1 v2 \<Longrightarrow> v1 \<in> prob_dom PROB
 2. \<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2 \<Longrightarrow> v1 \<in> prob_dom PROB
[PROOF STEP]
consider
        (II) "(\<exists>a.
            a \<in> PROB \<and>
            (
              v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a)
              \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a)))"
        | (III) "v1 = v2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a)) \<Longrightarrow> thesis; v1 = v2 \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
dep PROB v1 v2

goal (1 subgoal):
 1. \<lbrakk>\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a)) \<Longrightarrow> thesis; v1 = v2 \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding dep_def
[PROOF STATE]
proof (prove)
using this:
(\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2

goal (1 subgoal):
 1. \<lbrakk>\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a)) \<Longrightarrow> thesis; v1 = v2 \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a)) \<Longrightarrow> ?thesis; v1 = v2 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (2 subgoals):
 1. dep PROB v1 v2 \<Longrightarrow> v1 \<in> prob_dom PROB
 2. \<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2 \<Longrightarrow> v1 \<in> prob_dom PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a)) \<Longrightarrow> ?thesis; v1 = v2 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a)) \<Longrightarrow> ?thesis; v1 = v2 \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. v1 \<in> prob_dom PROB
[PROOF STEP]
proof (cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a)) \<Longrightarrow> v1 \<in> prob_dom PROB
 2. v1 = v2 \<Longrightarrow> v1 \<in> prob_dom PROB
[PROOF STEP]
case II
[PROOF STATE]
proof (state)
this:
\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))

goal (2 subgoals):
 1. \<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a)) \<Longrightarrow> v1 \<in> prob_dom PROB
 2. v1 = v2 \<Longrightarrow> v1 \<in> prob_dom PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))
[PROOF STEP]
obtain a where 1:
          "a \<in> PROB" "(v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a)
              \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))"
[PROOF STATE]
proof (prove)
using this:
\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> PROB; v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in> PROB
v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a)

goal (2 subgoals):
 1. \<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a)) \<Longrightarrow> v1 \<in> prob_dom PROB
 2. v1 = v2 \<Longrightarrow> v1 \<in> prob_dom PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> PROB
v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a)
[PROOF STEP]
have "v1 \<in> fmdom' (fst a) \<union> fmdom' (snd a)"
[PROOF STATE]
proof (prove)
using this:
a \<in> PROB
v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a)

goal (1 subgoal):
 1. v1 \<in> fmdom' (fst a) \<union> fmdom' (snd a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v1 \<in> fmdom' (fst a) \<union> fmdom' (snd a)

goal (2 subgoals):
 1. \<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a)) \<Longrightarrow> v1 \<in> prob_dom PROB
 2. v1 = v2 \<Longrightarrow> v1 \<in> prob_dom PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v1 \<in> fmdom' (fst a) \<union> fmdom' (snd a)
[PROOF STEP]
have 2: "v1 \<in> action_dom (fst a) (snd a)"
[PROOF STATE]
proof (prove)
using this:
v1 \<in> fmdom' (fst a) \<union> fmdom' (snd a)

goal (1 subgoal):
 1. v1 \<in> action_dom (fst a) (snd a)
[PROOF STEP]
unfolding action_dom_def
[PROOF STATE]
proof (prove)
using this:
v1 \<in> fmdom' (fst a) \<union> fmdom' (snd a)

goal (1 subgoal):
 1. v1 \<in> fmdom' (fst a) \<union> fmdom' (snd a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v1 \<in> action_dom (fst a) (snd a)

goal (2 subgoals):
 1. \<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a)) \<Longrightarrow> v1 \<in> prob_dom PROB
 2. v1 = v2 \<Longrightarrow> v1 \<in> prob_dom PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v1 \<in> action_dom (fst a) (snd a)
[PROOF STEP]
have "action_dom (fst a) (snd a) \<subseteq> prob_dom PROB"
[PROOF STATE]
proof (prove)
using this:
v1 \<in> action_dom (fst a) (snd a)

goal (1 subgoal):
 1. action_dom (fst a) (snd a) \<subseteq> prob_dom PROB
[PROOF STEP]
using 1(1) exec_as_proj_valid_2
[PROOF STATE]
proof (prove)
using this:
v1 \<in> action_dom (fst a) (snd a)
a \<in> PROB
?a \<in> ?PROB \<Longrightarrow> action_dom (fst ?a) (snd ?a) \<subseteq> prob_dom ?PROB

goal (1 subgoal):
 1. action_dom (fst a) (snd a) \<subseteq> prob_dom PROB
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
action_dom (fst a) (snd a) \<subseteq> prob_dom PROB

goal (2 subgoals):
 1. \<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a)) \<Longrightarrow> v1 \<in> prob_dom PROB
 2. v1 = v2 \<Longrightarrow> v1 \<in> prob_dom PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
action_dom (fst a) (snd a) \<subseteq> prob_dom PROB
[PROOF STEP]
have "v1 \<in> prob_dom PROB"
[PROOF STATE]
proof (prove)
using this:
action_dom (fst a) (snd a) \<subseteq> prob_dom PROB

goal (1 subgoal):
 1. v1 \<in> prob_dom PROB
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
action_dom (fst a) (snd a) \<subseteq> prob_dom PROB
a \<in> PROB
v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a)
v1 \<in> action_dom (fst a) (snd a)

goal (1 subgoal):
 1. v1 \<in> prob_dom PROB
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
v1 \<in> prob_dom PROB

goal (2 subgoals):
 1. \<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a)) \<Longrightarrow> v1 \<in> prob_dom PROB
 2. v1 = v2 \<Longrightarrow> v1 \<in> prob_dom PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v1 \<in> prob_dom PROB
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v1 \<in> prob_dom PROB

goal (1 subgoal):
 1. v1 \<in> prob_dom PROB
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v1 \<in> prob_dom PROB

goal (1 subgoal):
 1. v1 = v2 \<Longrightarrow> v1 \<in> prob_dom PROB
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v1 = v2 \<Longrightarrow> v1 \<in> prob_dom PROB
[PROOF STEP]
case III
[PROOF STATE]
proof (state)
this:
v1 = v2

goal (1 subgoal):
 1. v1 = v2 \<Longrightarrow> v1 \<in> prob_dom PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v1 = v2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v1 = v2

goal (1 subgoal):
 1. v1 \<in> prob_dom PROB
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
v1 = v2
v1 \<noteq> v2

goal (1 subgoal):
 1. v1 \<in> prob_dom PROB
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v1 \<in> prob_dom PROB

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v1 \<in> prob_dom PROB

goal (2 subgoals):
 1. dep PROB v1 v2 \<Longrightarrow> v1 \<in> prob_dom PROB
 2. \<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2 \<Longrightarrow> v1 \<in> prob_dom PROB
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
v1 \<in> prob_dom PROB

goal (2 subgoals):
 1. dep PROB v1 v2 \<Longrightarrow> v1 \<in> prob_dom PROB
 2. \<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2 \<Longrightarrow> v1 \<in> prob_dom PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v1 \<in> prob_dom PROB
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v1 \<in> prob_dom PROB

goal (1 subgoal):
 1. v1 \<in> prob_dom PROB
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v1 \<in> prob_dom PROB

goal (1 subgoal):
 1. \<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2 \<Longrightarrow> v1 \<in> prob_dom PROB
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2 \<Longrightarrow> v1 \<in> prob_dom PROB
[PROOF STEP]
case ii
[PROOF STATE]
proof (state)
this:
\<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2

goal (1 subgoal):
 1. \<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2 \<Longrightarrow> v1 \<in> prob_dom PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2
[PROOF STEP]
obtain y where "v1 \<noteq> y" "y \<noteq> v2" "dep PROB v1 y" "TC (dep PROB) y v2"
[PROOF STATE]
proof (prove)
using this:
\<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>v1 \<noteq> y; y \<noteq> v2; dep PROB v1 y; TC (dep PROB) y v2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ii
[PROOF STATE]
proof (prove)
using this:
\<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2
\<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>v1 \<noteq> y; y \<noteq> v2; dep PROB v1 y; TC (dep PROB) y v2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v1 \<noteq> y
y \<noteq> v2
dep PROB v1 y
TC (dep PROB) y v2

goal (1 subgoal):
 1. \<exists>y. v1 \<noteq> y \<and> y \<noteq> v2 \<and> dep PROB v1 y \<and> TC (dep PROB) y v2 \<Longrightarrow> v1 \<in> prob_dom PROB
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v1 \<noteq> y
y \<noteq> v2
dep PROB v1 y
TC (dep PROB) y v2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v1 \<noteq> y
y \<noteq> v2
dep PROB v1 y
TC (dep PROB) y v2

goal (1 subgoal):
 1. v1 \<in> prob_dom PROB
[PROOF STEP]
using NEQ_DEP_IMP_IN_DOM
[PROOF STATE]
proof (prove)
using this:
v1 \<noteq> y
y \<noteq> v2
dep PROB v1 y
TC (dep PROB) y v2
\<lbrakk>?v \<noteq> ?v'; dep ?PROB ?v ?v'\<rbrakk> \<Longrightarrow> ?v \<in> prob_dom ?PROB \<and> ?v' \<in> prob_dom ?PROB

goal (1 subgoal):
 1. v1 \<in> prob_dom PROB
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
v1 \<in> prob_dom PROB

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v1 \<in> prob_dom PROB

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma not_dep_disj_imp_not_dep:
  fixes PROB vs_1 vs_2 vs_3
  assumes "((vs_1 \<inter> vs_2) = {})" "(vs_3 \<subseteq> vs_2)" "\<not>(dep_var_set PROB vs_1 vs_2)"
  shows "\<not>(dep_var_set PROB vs_1 vs_3)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> dep_var_set PROB vs_1 vs_3
[PROOF STEP]
using assms subset_eq
[PROOF STATE]
proof (prove)
using this:
vs_1 \<inter> vs_2 = {}
vs_3 \<subseteq> vs_2
\<not> dep_var_set PROB vs_1 vs_2
(?A \<subseteq> ?B) = (\<forall>x\<in>?A. x \<in> ?B)

goal (1 subgoal):
 1. \<not> dep_var_set PROB vs_1 vs_3
[PROOF STEP]
unfolding dep_var_set_def disjnt_def
[PROOF STATE]
proof (prove)
using this:
vs_1 \<inter> vs_2 = {}
vs_3 \<subseteq> vs_2
\<not> (vs_1 \<inter> vs_2 = {} \<and> (\<exists>v1 v2. v1 \<in> vs_1 \<and> v2 \<in> vs_2 \<and> dep PROB v1 v2))
(?A \<subseteq> ?B) = (\<forall>x\<in>?A. x \<in> ?B)

goal (1 subgoal):
 1. \<not> (vs_1 \<inter> vs_3 = {} \<and> (\<exists>v1 v2. v1 \<in> vs_1 \<and> v2 \<in> vs_3 \<and> dep PROB v1 v2))
[PROOF STEP]
by blast


[STATEMENT]
lemma dep_slist_imp_mem_dep:
  fixes PROB vs lvs
  assumes "(dep_var_set PROB (\<Union> (set lvs)) vs)"
  shows "(\<exists>vs'. ListMem vs' lvs \<and> dep_var_set PROB vs' vs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>vs'. ListMem vs' lvs \<and> dep_var_set PROB vs' vs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>vs'. ListMem vs' lvs \<and> dep_var_set PROB vs' vs
[PROOF STEP]
obtain v1 v2 where
    obtain_v1_v2: "v1 \<in> \<Union>(set lvs)" "v2 \<in> vs" "disjnt (\<Union>(set lvs)) vs" "dep PROB v1 v2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v1 v2. \<lbrakk>v1 \<in> \<Union> (set lvs); v2 \<in> vs; disjnt (\<Union> (set lvs)) vs; dep PROB v1 v2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms dep_var_set_def[of PROB "\<Union> (set lvs)" vs]
[PROOF STATE]
proof (prove)
using this:
dep_var_set PROB (\<Union> (set lvs)) vs
dep_var_set PROB (\<Union> (set lvs)) vs \<equiv> disjnt (\<Union> (set lvs)) vs \<and> (\<exists>v1 v2. v1 \<in> \<Union> (set lvs) \<and> v2 \<in> vs \<and> dep PROB v1 v2)

goal (1 subgoal):
 1. (\<And>v1 v2. \<lbrakk>v1 \<in> \<Union> (set lvs); v2 \<in> vs; disjnt (\<Union> (set lvs)) vs; dep PROB v1 v2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v1 \<in> \<Union> (set lvs)
v2 \<in> vs
disjnt (\<Union> (set lvs)) vs
dep PROB v1 v2

goal (1 subgoal):
 1. \<exists>vs'. ListMem vs' lvs \<and> dep_var_set PROB vs' vs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v1 \<in> \<Union> (set lvs)
v2 \<in> vs
disjnt (\<Union> (set lvs)) vs
dep PROB v1 v2
[PROOF STEP]
obtain vs' where obtain_vs': "vs' \<in> set lvs" "v1 \<in> vs'"
[PROOF STATE]
proof (prove)
using this:
v1 \<in> \<Union> (set lvs)
v2 \<in> vs
disjnt (\<Union> (set lvs)) vs
dep PROB v1 v2

goal (1 subgoal):
 1. (\<And>vs'. \<lbrakk>vs' \<in> set lvs; v1 \<in> vs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
vs' \<in> set lvs
v1 \<in> vs'

goal (1 subgoal):
 1. \<exists>vs'. ListMem vs' lvs \<and> dep_var_set PROB vs' vs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vs' \<in> set lvs
v1 \<in> vs'
[PROOF STEP]
have "ListMem vs' lvs"
[PROOF STATE]
proof (prove)
using this:
vs' \<in> set lvs
v1 \<in> vs'

goal (1 subgoal):
 1. ListMem vs' lvs
[PROOF STEP]
using ListMem_iff
[PROOF STATE]
proof (prove)
using this:
vs' \<in> set lvs
v1 \<in> vs'
ListMem ?x ?xs = (?x \<in> set ?xs)

goal (1 subgoal):
 1. ListMem vs' lvs
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
ListMem vs' lvs

goal (1 subgoal):
 1. \<exists>vs'. ListMem vs' lvs \<and> dep_var_set PROB vs' vs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ListMem vs' lvs

goal (1 subgoal):
 1. \<exists>vs'. ListMem vs' lvs \<and> dep_var_set PROB vs' vs
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
ListMem vs' lvs

goal (1 subgoal):
 1. \<exists>vs'. ListMem vs' lvs \<and> dep_var_set PROB vs' vs
[PROOF STEP]
have "disjnt vs' vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. disjnt vs' vs
[PROOF STEP]
using obtain_v1_v2(3) obtain_vs'(1)
[PROOF STATE]
proof (prove)
using this:
disjnt (\<Union> (set lvs)) vs
vs' \<in> set lvs

goal (1 subgoal):
 1. disjnt vs' vs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
disjnt vs' vs

goal (1 subgoal):
 1. \<exists>vs'. ListMem vs' lvs \<and> dep_var_set PROB vs' vs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
disjnt vs' vs
[PROOF STEP]
have "dep_var_set PROB vs' vs"
[PROOF STATE]
proof (prove)
using this:
disjnt vs' vs

goal (1 subgoal):
 1. dep_var_set PROB vs' vs
[PROOF STEP]
unfolding dep_var_set_def
[PROOF STATE]
proof (prove)
using this:
disjnt vs' vs

goal (1 subgoal):
 1. disjnt vs' vs \<and> (\<exists>v1 v2. v1 \<in> vs' \<and> v2 \<in> vs \<and> dep PROB v1 v2)
[PROOF STEP]
using obtain_v1_v2(1, 2, 4) obtain_vs'(2)
[PROOF STATE]
proof (prove)
using this:
disjnt vs' vs
v1 \<in> \<Union> (set lvs)
v2 \<in> vs
dep PROB v1 v2
v1 \<in> vs'

goal (1 subgoal):
 1. disjnt vs' vs \<and> (\<exists>v1 v2. v1 \<in> vs' \<and> v2 \<in> vs \<and> dep PROB v1 v2)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
dep_var_set PROB vs' vs

goal (1 subgoal):
 1. \<exists>vs'. ListMem vs' lvs \<and> dep_var_set PROB vs' vs
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
dep_var_set PROB vs' vs

goal (1 subgoal):
 1. \<exists>vs'. ListMem vs' lvs \<and> dep_var_set PROB vs' vs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ListMem vs' lvs
dep_var_set PROB vs' vs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ListMem vs' lvs
dep_var_set PROB vs' vs

goal (1 subgoal):
 1. \<exists>vs'. ListMem vs' lvs \<and> dep_var_set PROB vs' vs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>vs'. ListMem vs' lvs \<and> dep_var_set PROB vs' vs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma n_bigunion_le_sum_3:
  fixes PROB vs svs
  assumes "(\<forall> vs'. vs' \<in> svs \<longrightarrow> \<not>(dep_var_set PROB vs' vs))"
  shows "\<not>(dep_var_set PROB (\<Union>svs) vs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> dep_var_set PROB (\<Union> svs) vs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> dep_var_set PROB (\<Union> svs) vs
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> dep_var_set PROB (\<Union> svs) vs
[PROOF STEP]
assume "(dep_var_set PROB (\<Union>svs) vs)"
[PROOF STATE]
proof (state)
this:
dep_var_set PROB (\<Union> svs) vs

goal (1 subgoal):
 1. \<not> dep_var_set PROB (\<Union> svs) vs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dep_var_set PROB (\<Union> svs) vs
[PROOF STEP]
obtain v1 v2 where obtain_vs: "v1 \<in> \<Union>svs" "v2 \<in> vs" "disjnt (\<Union>svs) vs" "dep PROB v1 v2"
[PROOF STATE]
proof (prove)
using this:
dep_var_set PROB (\<Union> svs) vs

goal (1 subgoal):
 1. (\<And>v1 v2. \<lbrakk>v1 \<in> \<Union> svs; v2 \<in> vs; disjnt (\<Union> svs) vs; dep PROB v1 v2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dep_var_set_def
[PROOF STATE]
proof (prove)
using this:
disjnt (\<Union> svs) vs \<and> (\<exists>v1 v2. v1 \<in> \<Union> svs \<and> v2 \<in> vs \<and> dep PROB v1 v2)

goal (1 subgoal):
 1. (\<And>v1 v2. \<lbrakk>v1 \<in> \<Union> svs; v2 \<in> vs; disjnt (\<Union> svs) vs; dep PROB v1 v2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v1 \<in> \<Union> svs
v2 \<in> vs
disjnt (\<Union> svs) vs
dep PROB v1 v2

goal (1 subgoal):
 1. \<not> dep_var_set PROB (\<Union> svs) vs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v1 \<in> \<Union> svs
v2 \<in> vs
disjnt (\<Union> svs) vs
dep PROB v1 v2
[PROOF STEP]
obtain vs' where obtain_vs': "v1 \<in> vs'" "vs' \<in> svs"
[PROOF STATE]
proof (prove)
using this:
v1 \<in> \<Union> svs
v2 \<in> vs
disjnt (\<Union> svs) vs
dep PROB v1 v2

goal (1 subgoal):
 1. (\<And>vs'. \<lbrakk>v1 \<in> vs'; vs' \<in> svs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v1 \<in> vs'
vs' \<in> svs

goal (1 subgoal):
 1. \<not> dep_var_set PROB (\<Union> svs) vs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v1 \<in> vs'
vs' \<in> svs
[PROOF STEP]
have a: "disjnt vs' vs"
[PROOF STATE]
proof (prove)
using this:
v1 \<in> vs'
vs' \<in> svs

goal (1 subgoal):
 1. disjnt vs' vs
[PROOF STEP]
using obtain_vs(3) obtain_vs'(2) disjnt_subset1
[PROOF STATE]
proof (prove)
using this:
v1 \<in> vs'
vs' \<in> svs
disjnt (\<Union> svs) vs
vs' \<in> svs
\<lbrakk>disjnt ?X ?Y; ?Z \<subseteq> ?X\<rbrakk> \<Longrightarrow> disjnt ?Z ?Y

goal (1 subgoal):
 1. disjnt vs' vs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
disjnt vs' vs

goal (1 subgoal):
 1. \<not> dep_var_set PROB (\<Union> svs) vs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
disjnt vs' vs
[PROOF STEP]
have "\<forall>v1 v2. \<not>(v1 \<in> vs') \<or> \<not>(v2 \<in> vs) \<or> \<not>disjnt vs' vs \<or> \<not>dep PROB v1 v2"
[PROOF STATE]
proof (prove)
using this:
disjnt vs' vs

goal (1 subgoal):
 1. \<forall>v1 v2. v1 \<notin> vs' \<or> v2 \<notin> vs \<or> \<not> disjnt vs' vs \<or> \<not> dep PROB v1 v2
[PROOF STEP]
using assms obtain_vs'(2) dep_var_set_def
[PROOF STATE]
proof (prove)
using this:
disjnt vs' vs
\<forall>vs'. vs' \<in> svs \<longrightarrow> \<not> dep_var_set PROB vs' vs
vs' \<in> svs
dep_var_set ?PROB ?vs1.0 ?vs2.0 \<equiv> disjnt ?vs1.0 ?vs2.0 \<and> (\<exists>v1 v2. v1 \<in> ?vs1.0 \<and> v2 \<in> ?vs2.0 \<and> dep ?PROB v1 v2)

goal (1 subgoal):
 1. \<forall>v1 v2. v1 \<notin> vs' \<or> v2 \<notin> vs \<or> \<not> disjnt vs' vs \<or> \<not> dep PROB v1 v2
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<forall>v1 v2. v1 \<notin> vs' \<or> v2 \<notin> vs \<or> \<not> disjnt vs' vs \<or> \<not> dep PROB v1 v2

goal (1 subgoal):
 1. \<not> dep_var_set PROB (\<Union> svs) vs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>v1 v2. v1 \<notin> vs' \<or> v2 \<notin> vs \<or> \<not> disjnt vs' vs \<or> \<not> dep PROB v1 v2
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
\<forall>v1 v2. v1 \<notin> vs' \<or> v2 \<notin> vs \<or> \<not> disjnt vs' vs \<or> \<not> dep PROB v1 v2

goal (1 subgoal):
 1. False
[PROOF STEP]
using a obtain_vs'(1) obtain_vs(2, 4)
[PROOF STATE]
proof (prove)
using this:
\<forall>v1 v2. v1 \<notin> vs' \<or> v2 \<notin> vs \<or> \<not> disjnt vs' vs \<or> \<not> dep PROB v1 v2
disjnt vs' vs
v1 \<in> vs'
v2 \<in> vs
dep PROB v1 v2

goal (1 subgoal):
 1. False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<not> dep_var_set PROB (\<Union> svs) vs
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
dep_var_set PROB (\<Union> svs) vs \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> dep_var_set PROB (\<Union> svs) vs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dep_var_set PROB (\<Union> svs) vs \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dep_var_set PROB (\<Union> svs) vs \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> dep_var_set PROB (\<Union> svs) vs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> dep_var_set PROB (\<Union> svs) vs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma disj_not_dep_vset_union_imp_or:
  fixes PROB a vs vs'
  assumes "(a \<in> PROB)" "(disjnt vs vs')"
    "(\<not>(dep_var_set PROB vs' vs) \<or> \<not>(dep_var_set PROB vs vs'))"
    "(varset_action a (vs \<union> vs'))"
  shows "(varset_action a vs \<or> varset_action a vs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. varset_action a vs \<or> varset_action a vs'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in> PROB
disjnt vs vs'
\<not> dep_var_set PROB vs' vs \<or> \<not> dep_var_set PROB vs vs'
varset_action a (vs \<union> vs')

goal (1 subgoal):
 1. varset_action a vs \<or> varset_action a vs'
[PROOF STEP]
unfolding varset_action_def dep_var_set_def dep_def
[PROOF STATE]
proof (prove)
using this:
a \<in> PROB
disjnt vs vs'
\<not> (disjnt vs' vs \<and> (\<exists>v1 v2. v1 \<in> vs' \<and> v2 \<in> vs \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2))) \<or> \<not> (disjnt vs vs' \<and> (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> vs' \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2)))
fmdom' (snd a) \<subseteq> vs \<union> vs'

goal (1 subgoal):
 1. fmdom' (snd a) \<subseteq> vs \<or> fmdom' (snd a) \<subseteq> vs'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>a \<in> PROB; disjnt vs vs'; \<not> (disjnt vs' vs \<and> (\<exists>v1 v2. v1 \<in> vs' \<and> v2 \<in> vs \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2))) \<or> \<not> (disjnt vs vs' \<and> (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> vs' \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2))); fmdom' (snd a) \<subseteq> vs \<union> vs'\<rbrakk> \<Longrightarrow> fmdom' (snd a) \<subseteq> vs \<or> fmdom' (snd a) \<subseteq> vs'
[PROOF STEP]
assume a1: "fmdom' (snd a) \<subseteq> vs \<union> vs'"
[PROOF STATE]
proof (state)
this:
fmdom' (snd a) \<subseteq> vs \<union> vs'

goal (1 subgoal):
 1. \<lbrakk>a \<in> PROB; disjnt vs vs'; \<not> (disjnt vs' vs \<and> (\<exists>v1 v2. v1 \<in> vs' \<and> v2 \<in> vs \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2))) \<or> \<not> (disjnt vs vs' \<and> (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> vs' \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2))); fmdom' (snd a) \<subseteq> vs \<union> vs'\<rbrakk> \<Longrightarrow> fmdom' (snd a) \<subseteq> vs \<or> fmdom' (snd a) \<subseteq> vs'
[PROOF STEP]
assume "disjnt vs vs'"
[PROOF STATE]
proof (state)
this:
disjnt vs vs'

goal (1 subgoal):
 1. \<lbrakk>a \<in> PROB; disjnt vs vs'; \<not> (disjnt vs' vs \<and> (\<exists>v1 v2. v1 \<in> vs' \<and> v2 \<in> vs \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2))) \<or> \<not> (disjnt vs vs' \<and> (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> vs' \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2))); fmdom' (snd a) \<subseteq> vs \<union> vs'\<rbrakk> \<Longrightarrow> fmdom' (snd a) \<subseteq> vs \<or> fmdom' (snd a) \<subseteq> vs'
[PROOF STEP]
assume " \<not> (disjnt vs' vs \<and>
        (\<exists>v1 v2. v1 \<in> vs' \<and> v2 \<in> vs \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2))) \<or>
       \<not> (disjnt vs vs' \<and>
        (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> vs' \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2))) "
[PROOF STATE]
proof (state)
this:
\<not> (disjnt vs' vs \<and> (\<exists>v1 v2. v1 \<in> vs' \<and> v2 \<in> vs \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2))) \<or> \<not> (disjnt vs vs' \<and> (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> vs' \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2)))

goal (1 subgoal):
 1. \<lbrakk>a \<in> PROB; disjnt vs vs'; \<not> (disjnt vs' vs \<and> (\<exists>v1 v2. v1 \<in> vs' \<and> v2 \<in> vs \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2))) \<or> \<not> (disjnt vs vs' \<and> (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> vs' \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2))); fmdom' (snd a) \<subseteq> vs \<union> vs'\<rbrakk> \<Longrightarrow> fmdom' (snd a) \<subseteq> vs \<or> fmdom' (snd a) \<subseteq> vs'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (disjnt vs' vs \<and> (\<exists>v1 v2. v1 \<in> vs' \<and> v2 \<in> vs \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2))) \<or> \<not> (disjnt vs vs' \<and> (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> vs' \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2)))
[PROOF STEP]
have f2: "\<And>aa ab. aa \<notin> vs \<or> ab \<notin> vs' \<or> aa \<notin> fmdom' (snd a) \<or> ab \<notin> fmdom' (snd a)"
[PROOF STATE]
proof (prove)
using this:
\<not> (disjnt vs' vs \<and> (\<exists>v1 v2. v1 \<in> vs' \<and> v2 \<in> vs \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2))) \<or> \<not> (disjnt vs vs' \<and> (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> vs' \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2)))

goal (1 subgoal):
 1. \<And>aa ab. aa \<notin> vs \<or> ab \<notin> vs' \<or> aa \<notin> fmdom' (snd a) \<or> ab \<notin> fmdom' (snd a)
[PROOF STEP]
using \<open>a \<in> PROB\<close> \<open>disjnt vs vs'\<close> disjnt_sym
[PROOF STATE]
proof (prove)
using this:
\<not> (disjnt vs' vs \<and> (\<exists>v1 v2. v1 \<in> vs' \<and> v2 \<in> vs \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2))) \<or> \<not> (disjnt vs vs' \<and> (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> vs' \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2)))
a \<in> PROB
disjnt vs vs'
disjnt ?A ?B \<Longrightarrow> disjnt ?B ?A

goal (1 subgoal):
 1. \<And>aa ab. aa \<notin> vs \<or> ab \<notin> vs' \<or> aa \<notin> fmdom' (snd a) \<or> ab \<notin> fmdom' (snd a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?aa \<notin> vs \<or> ?ab \<notin> vs' \<or> ?aa \<notin> fmdom' (snd a) \<or> ?ab \<notin> fmdom' (snd a)

goal (1 subgoal):
 1. \<lbrakk>a \<in> PROB; disjnt vs vs'; \<not> (disjnt vs' vs \<and> (\<exists>v1 v2. v1 \<in> vs' \<and> v2 \<in> vs \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2))) \<or> \<not> (disjnt vs vs' \<and> (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> vs' \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2))); fmdom' (snd a) \<subseteq> vs \<union> vs'\<rbrakk> \<Longrightarrow> fmdom' (snd a) \<subseteq> vs \<or> fmdom' (snd a) \<subseteq> vs'
[PROOF STEP]
obtain aa :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a" where
    f3: "\<And>A Aa a Ab Ac. (A \<subseteq> Aa \<or> aa A Aa \<in> A) \<and> (aa A Aa \<notin> Aa \<or> A \<subseteq> Aa)
      \<and> ((a::'a) \<notin> Ab \<or> \<not> Ab \<subseteq> Ac \<or> a \<in> Ac)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>aa. (\<And>A Aa a Ab Ac. (A \<subseteq> Aa \<or> aa A Aa \<in> A) \<and> (aa A Aa \<notin> Aa \<or> A \<subseteq> Aa) \<and> (a \<notin> Ab \<or> \<not> Ab \<subseteq> Ac \<or> a \<in> Ac)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by moura
[PROOF STATE]
proof (state)
this:
(?A \<subseteq> ?Aa \<or> aa ?A ?Aa \<in> ?A) \<and> (aa ?A ?Aa \<notin> ?Aa \<or> ?A \<subseteq> ?Aa) \<and> (?a \<notin> ?Ab \<or> \<not> ?Ab \<subseteq> ?Ac \<or> ?a \<in> ?Ac)

goal (1 subgoal):
 1. \<lbrakk>a \<in> PROB; disjnt vs vs'; \<not> (disjnt vs' vs \<and> (\<exists>v1 v2. v1 \<in> vs' \<and> v2 \<in> vs \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2))) \<or> \<not> (disjnt vs vs' \<and> (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> vs' \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2))); fmdom' (snd a) \<subseteq> vs \<union> vs'\<rbrakk> \<Longrightarrow> fmdom' (snd a) \<subseteq> vs \<or> fmdom' (snd a) \<subseteq> vs'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?A \<subseteq> ?Aa \<or> aa ?A ?Aa \<in> ?A) \<and> (aa ?A ?Aa \<notin> ?Aa \<or> ?A \<subseteq> ?Aa) \<and> (?a \<notin> ?Ab \<or> \<not> ?Ab \<subseteq> ?Ac \<or> ?a \<in> ?Ac)
[PROOF STEP]
have "\<And>A. fmdom' (snd a) \<subseteq> A \<or> aa (fmdom' (snd a)) A \<in> vs \<or> aa (fmdom' (snd a)) A \<in> vs'"
[PROOF STATE]
proof (prove)
using this:
(?A \<subseteq> ?Aa \<or> aa ?A ?Aa \<in> ?A) \<and> (aa ?A ?Aa \<notin> ?Aa \<or> ?A \<subseteq> ?Aa) \<and> (?a \<notin> ?Ab \<or> \<not> ?Ab \<subseteq> ?Ac \<or> ?a \<in> ?Ac)

goal (1 subgoal):
 1. \<And>A. fmdom' (snd a) \<subseteq> A \<or> aa (fmdom' (snd a)) A \<in> vs \<or> aa (fmdom' (snd a)) A \<in> vs'
[PROOF STEP]
using a1
[PROOF STATE]
proof (prove)
using this:
(?A \<subseteq> ?Aa \<or> aa ?A ?Aa \<in> ?A) \<and> (aa ?A ?Aa \<notin> ?Aa \<or> ?A \<subseteq> ?Aa) \<and> (?a \<notin> ?Ab \<or> \<not> ?Ab \<subseteq> ?Ac \<or> ?a \<in> ?Ac)
fmdom' (snd a) \<subseteq> vs \<union> vs'

goal (1 subgoal):
 1. \<And>A. fmdom' (snd a) \<subseteq> A \<or> aa (fmdom' (snd a)) A \<in> vs \<or> aa (fmdom' (snd a)) A \<in> vs'
[PROOF STEP]
by (meson Un_iff)
[PROOF STATE]
proof (state)
this:
fmdom' (snd a) \<subseteq> ?A \<or> aa (fmdom' (snd a)) ?A \<in> vs \<or> aa (fmdom' (snd a)) ?A \<in> vs'

goal (1 subgoal):
 1. \<lbrakk>a \<in> PROB; disjnt vs vs'; \<not> (disjnt vs' vs \<and> (\<exists>v1 v2. v1 \<in> vs' \<and> v2 \<in> vs \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2))) \<or> \<not> (disjnt vs vs' \<and> (\<exists>v1 v2. v1 \<in> vs \<and> v2 \<in> vs' \<and> ((\<exists>a. a \<in> PROB \<and> (v1 \<in> fmdom' (fst a) \<and> v2 \<in> fmdom' (snd a) \<or> v1 \<in> fmdom' (snd a) \<and> v2 \<in> fmdom' (snd a))) \<or> v1 = v2))); fmdom' (snd a) \<subseteq> vs \<union> vs'\<rbrakk> \<Longrightarrow> fmdom' (snd a) \<subseteq> vs \<or> fmdom' (snd a) \<subseteq> vs'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fmdom' (snd a) \<subseteq> ?A \<or> aa (fmdom' (snd a)) ?A \<in> vs \<or> aa (fmdom' (snd a)) ?A \<in> vs'
[PROOF STEP]
show "fmdom' (snd a) \<subseteq> vs \<or> fmdom' (snd a) \<subseteq> vs'"
[PROOF STATE]
proof (prove)
using this:
fmdom' (snd a) \<subseteq> ?A \<or> aa (fmdom' (snd a)) ?A \<in> vs \<or> aa (fmdom' (snd a)) ?A \<in> vs'

goal (1 subgoal):
 1. fmdom' (snd a) \<subseteq> vs \<or> fmdom' (snd a) \<subseteq> vs'
[PROOF STEP]
using f3 f2
[PROOF STATE]
proof (prove)
using this:
fmdom' (snd a) \<subseteq> ?A \<or> aa (fmdom' (snd a)) ?A \<in> vs \<or> aa (fmdom' (snd a)) ?A \<in> vs'
(?A \<subseteq> ?Aa \<or> aa ?A ?Aa \<in> ?A) \<and> (aa ?A ?Aa \<notin> ?Aa \<or> ?A \<subseteq> ?Aa) \<and> (?a \<notin> ?Ab \<or> \<not> ?Ab \<subseteq> ?Ac \<or> ?a \<in> ?Ac)
?aa \<notin> vs \<or> ?ab \<notin> vs' \<or> ?aa \<notin> fmdom' (snd a) \<or> ?ab \<notin> fmdom' (snd a)

goal (1 subgoal):
 1. fmdom' (snd a) \<subseteq> vs \<or> fmdom' (snd a) \<subseteq> vs'
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
fmdom' (snd a) \<subseteq> vs \<or> fmdom' (snd a) \<subseteq> vs'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dt: "F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> G
[PROOF STEP]
by (metis AX100 Deduction_theorem Un_insert_right sup_left_commute)


[STATEMENT]
lemma sim: "\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<Longrightarrow> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F; F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G
[PROOF STEP]
using MP dt
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<Gamma> \<turnstile>\<^sub>H ?F; ?\<Gamma> \<turnstile>\<^sub>H ?F \<^bold>\<rightarrow> ?G\<rbrakk> \<Longrightarrow> ?\<Gamma> \<turnstile>\<^sub>H ?G
?F \<triangleright> ?\<Gamma> \<union> AX10 \<turnstile>\<^sub>H ?G \<Longrightarrow> ?\<Gamma> \<union> AX10 \<turnstile>\<^sub>H ?F \<^bold>\<rightarrow> ?G

goal (1 subgoal):
 1. \<lbrakk>\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F; F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G
[PROOF STEP]
by blast


[STATEMENT]
lemma sim_conj: "F \<triangleright> G \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<triangleright> G \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H; \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F; \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H
[PROOF STEP]
using MP dt
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<Gamma> \<turnstile>\<^sub>H ?F; ?\<Gamma> \<turnstile>\<^sub>H ?F \<^bold>\<rightarrow> ?G\<rbrakk> \<Longrightarrow> ?\<Gamma> \<turnstile>\<^sub>H ?G
?F \<triangleright> ?\<Gamma> \<union> AX10 \<turnstile>\<^sub>H ?G \<Longrightarrow> ?\<Gamma> \<union> AX10 \<turnstile>\<^sub>H ?F \<^bold>\<rightarrow> ?G

goal (1 subgoal):
 1. \<lbrakk>F \<triangleright> G \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H; \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F; \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H
[PROOF STEP]
by (metis Un_insert_left)


[STATEMENT]
lemma sim_disj: "\<lbrakk>F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H; G \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H; \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<or> G\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H; G \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H; \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<or> G\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H
[PROOF STEP]
proof goal_cases
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H; G \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H; \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<or> G\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H
G \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<or> G

goal (1 subgoal):
 1. \<lbrakk>F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H; G \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H; \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<or> G\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H
[PROOF STEP]
have 2: "\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> H
[PROOF STEP]
by (simp add: 1 dt)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> H

goal (1 subgoal):
 1. \<lbrakk>F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H; G \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H; \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<or> G\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H
[PROOF STEP]
have 3: "\<Gamma> \<union> AX10 \<turnstile>\<^sub>H G \<^bold>\<rightarrow> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G \<^bold>\<rightarrow> H
[PROOF STEP]
by (simp add: 1 dt)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H G \<^bold>\<rightarrow> H

goal (1 subgoal):
 1. \<lbrakk>F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H; G \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H; \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<or> G\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H
[PROOF STEP]
have 4: "\<Gamma> \<union> AX10 \<turnstile>\<^sub>H (F \<^bold>\<or> G) \<^bold>\<rightarrow> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H (F \<^bold>\<or> G) \<^bold>\<rightarrow> H
[PROOF STEP]
by (meson 2 3 HC.simps HC_intros(7) HC_mono sup_ge2)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H (F \<^bold>\<or> G) \<^bold>\<rightarrow> H

goal (1 subgoal):
 1. \<lbrakk>F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H; G \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H; \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<or> G\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H H
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H (F \<^bold>\<or> G) \<^bold>\<rightarrow> H

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma someax: "\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<rightarrow> \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<rightarrow> \<bottom>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<rightarrow> \<bottom>
[PROOF STEP]
have "F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> F \<^bold>\<rightarrow> \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> F \<^bold>\<rightarrow> \<bottom>
[PROOF STEP]
by (meson HC_intros(12) HC_mono subset_insertI sup_ge2)
[PROOF STATE]
proof (state)
this:
F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> F \<^bold>\<rightarrow> \<bottom>

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<rightarrow> \<bottom>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> F \<^bold>\<rightarrow> \<bottom>
[PROOF STEP]
have "\<^bold>\<not> F \<triangleright> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>"
[PROOF STATE]
proof (prove)
using this:
F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> F \<^bold>\<rightarrow> \<bottom>

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

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<rightarrow> \<bottom>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<^bold>\<not> F \<triangleright> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> F \<triangleright> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<rightarrow> \<bottom>
[PROOF STEP]
by (metis (no_types) Un_insert_left dt)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<rightarrow> \<bottom>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lem: "\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F
[PROOF STEP]
thm HC_intros(7)[of F \<bottom> "Not F"]
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F
[PROOF STEP]
have "F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H ( \<^bold>\<not> F \<^bold>\<or> F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F
[PROOF STEP]
by (metis AX10.intros(3) Ax HC_mono MP Un_commute Un_insert_left insertI1 sup_ge1)
[PROOF STATE]
proof (state)
this:
F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F
[PROOF STEP]
hence "F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> ( \<^bold>\<not> F \<^bold>\<or> F) \<^bold>\<rightarrow> \<bottom>"
[PROOF STATE]
proof (prove)
using this:
F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F

goal (1 subgoal):
 1. F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> (\<^bold>\<not> F \<^bold>\<or> F) \<^bold>\<rightarrow> \<bottom>
[PROOF STEP]
using someax
[PROOF STATE]
proof (prove)
using this:
F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F
?\<Gamma> \<union> AX10 \<turnstile>\<^sub>H ?F \<^bold>\<rightarrow> \<^bold>\<not> ?F \<^bold>\<rightarrow> \<bottom>

goal (1 subgoal):
 1. F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> (\<^bold>\<not> F \<^bold>\<or> F) \<^bold>\<rightarrow> \<bottom>
[PROOF STEP]
by (metis HC.simps Un_insert_left)
[PROOF STATE]
proof (state)
this:
F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> (\<^bold>\<not> F \<^bold>\<or> F) \<^bold>\<rightarrow> \<bottom>

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F
[PROOF STEP]
hence "\<^bold>\<not> ( \<^bold>\<not> F \<^bold>\<or> F) \<triangleright> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>"
[PROOF STATE]
proof (prove)
using this:
F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> (\<^bold>\<not> F \<^bold>\<or> F) \<^bold>\<rightarrow> \<bottom>

goal (1 subgoal):
 1. \<^bold>\<not> (\<^bold>\<not> F \<^bold>\<or> F) \<triangleright> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
by (meson Ax HC_mono MP insertI1 subset_insertI)
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> (\<^bold>\<not> F \<^bold>\<or> F) \<triangleright> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F
[PROOF STEP]
hence "\<^bold>\<not> ( \<^bold>\<not> F \<^bold>\<or> F) \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<bottom>"
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> (\<^bold>\<not> F \<^bold>\<or> F) \<triangleright> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>

goal (1 subgoal):
 1. \<^bold>\<not> (\<^bold>\<not> F \<^bold>\<or> F) \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<bottom>
[PROOF STEP]
by (metis Un_insert_left dt insert_commute)
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> (\<^bold>\<not> F \<^bold>\<or> F) \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<bottom>

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F
[PROOF STEP]
have "\<^bold>\<not>F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H ( \<^bold>\<not> F \<^bold>\<or> F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<^bold>\<not> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F
[PROOF STEP]
by (metis HC.simps HC_intros(5) HC_mono inf_sup_ord(4) insertI1 insert_is_Un)
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F
[PROOF STEP]
hence "\<^bold>\<not>F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> ( \<^bold>\<not> F \<^bold>\<or> F) \<^bold>\<rightarrow> \<bottom>"
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F

goal (1 subgoal):
 1. \<^bold>\<not> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> (\<^bold>\<not> F \<^bold>\<or> F) \<^bold>\<rightarrow> \<bottom>
[PROOF STEP]
using someax
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F
?\<Gamma> \<union> AX10 \<turnstile>\<^sub>H ?F \<^bold>\<rightarrow> \<^bold>\<not> ?F \<^bold>\<rightarrow> \<bottom>

goal (1 subgoal):
 1. \<^bold>\<not> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> (\<^bold>\<not> F \<^bold>\<or> F) \<^bold>\<rightarrow> \<bottom>
[PROOF STEP]
by (metis HC.simps Un_insert_left)
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> (\<^bold>\<not> F \<^bold>\<or> F) \<^bold>\<rightarrow> \<bottom>

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F
[PROOF STEP]
hence "\<^bold>\<not> ( \<^bold>\<not> F \<^bold>\<or> F) \<triangleright> \<^bold>\<not>F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>"
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> (\<^bold>\<not> F \<^bold>\<or> F) \<^bold>\<rightarrow> \<bottom>

goal (1 subgoal):
 1. \<^bold>\<not> (\<^bold>\<not> F \<^bold>\<or> F) \<triangleright> \<^bold>\<not> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>
[PROOF STEP]
by (meson Ax HC_mono MP insertI1 subset_insertI)
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> (\<^bold>\<not> F \<^bold>\<or> F) \<triangleright> \<^bold>\<not> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F
[PROOF STEP]
hence "\<^bold>\<not> ( \<^bold>\<not> F \<^bold>\<or> F) \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not>F \<^bold>\<rightarrow> \<bottom>"
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> (\<^bold>\<not> F \<^bold>\<or> F) \<triangleright> \<^bold>\<not> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>

goal (1 subgoal):
 1. \<^bold>\<not> (\<^bold>\<not> F \<^bold>\<or> F) \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> \<bottom>
[PROOF STEP]
by (metis Un_insert_left dt insert_commute)
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> (\<^bold>\<not> F \<^bold>\<or> F) \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> \<bottom>

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F
[PROOF STEP]
hence "\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> ( \<^bold>\<not> F \<^bold>\<or> F) \<^bold>\<rightarrow> \<bottom>"
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> (\<^bold>\<not> F \<^bold>\<or> F) \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> \<bottom>

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> (\<^bold>\<not> F \<^bold>\<or> F) \<^bold>\<rightarrow> \<bottom>
[PROOF STEP]
by (meson HC_intros(13) HC_mono MP \<open>\<^bold>\<not> (\<^bold>\<not> F \<^bold>\<or> F) \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<bottom>\<close> dt subset_insertI sup_ge2)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> (\<^bold>\<not> F \<^bold>\<or> F) \<^bold>\<rightarrow> \<bottom>

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> (\<^bold>\<not> F \<^bold>\<or> F) \<^bold>\<rightarrow> \<bottom>

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F
[PROOF STEP]
by (meson HC.simps HC_intros(13) HC_mono sup_ge2)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F

goal:
No subgoals!
[PROOF STEP]
(*    apply(insert HC_mono dt HC_intros(3-)[THEN HC_mono, OF sup_ge2] sim HC.intros)
    sledgehammer[debug,max_facts=50,timeout=120]*)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> F

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exchg: "\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<or> G \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G \<^bold>\<or> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<or> G \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G \<^bold>\<or> F
[PROOF STEP]
by (meson AX10.intros(3) HC.simps HC_intros(5) HC_intros(7) HC_mono sup_ge2)


[STATEMENT]
lemma lem2: "\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<or> \<^bold>\<not> F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<or> \<^bold>\<not> F
[PROOF STEP]
by (simp add: exchg lem)


[STATEMENT]
lemma imp_sim: "\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> G \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> G \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> G
[PROOF STEP]
proof goal_cases
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> G \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> G
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> G

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> G \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> G
[PROOF STEP]
have "\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G
[PROOF STEP]
have f1: "\<forall>F f Fa. \<not> (F \<turnstile>\<^sub>H f) \<or> \<not> F \<subseteq> Fa \<or> Fa \<turnstile>\<^sub>H f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>F f Fa. \<not> (F \<turnstile>\<^sub>H f) \<or> \<not> F \<subseteq> Fa \<or> Fa \<turnstile>\<^sub>H f
[PROOF STEP]
using HC_mono
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?S \<turnstile>\<^sub>H ?F; ?S \<subseteq> ?T\<rbrakk> \<Longrightarrow> ?T \<turnstile>\<^sub>H ?F

goal (1 subgoal):
 1. \<forall>F f Fa. \<not> (F \<turnstile>\<^sub>H f) \<or> \<not> F \<subseteq> Fa \<or> Fa \<turnstile>\<^sub>H f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>F f Fa. \<not> (F \<turnstile>\<^sub>H f) \<or> \<not> F \<subseteq> Fa \<or> Fa \<turnstile>\<^sub>H f

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>F f Fa. \<not> (F \<turnstile>\<^sub>H f) \<or> \<not> F \<subseteq> Fa \<or> Fa \<turnstile>\<^sub>H f
[PROOF STEP]
have f2: "F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> G"
[PROOF STATE]
proof (prove)
using this:
\<forall>F f Fa. \<not> (F \<turnstile>\<^sub>H f) \<or> \<not> F \<subseteq> Fa \<or> Fa \<turnstile>\<^sub>H f

goal (1 subgoal):
 1. F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> G
[PROOF STEP]
by (metis "1" subset_insertI)
[PROOF STATE]
proof (state)
this:
F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> G

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G
[PROOF STEP]
(* > 1.0 s, timed out *)
[PROOF STATE]
proof (state)
this:
F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> G

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G
[PROOF STEP]
have "\<Gamma> \<union> AX10 \<turnstile>\<^sub>H G \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
\<forall>F f Fa. \<not> (F \<turnstile>\<^sub>H f) \<or> \<not> F \<subseteq> Fa \<or> Fa \<turnstile>\<^sub>H f

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

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H G \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H G \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G
[PROOF STEP]
using f2 f1
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H G \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G
F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> G
\<forall>F f Fa. \<not> (F \<turnstile>\<^sub>H f) \<or> \<not> F \<subseteq> Fa \<or> Fa \<turnstile>\<^sub>H f

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G
[PROOF STEP]
by (metis (no_types) HC.simps dt insertI1 subset_insertI)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> G \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> G
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> G \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> G
[PROOF STEP]
have "\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not>F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G
[PROOF STEP]
by (simp add: AX10.intros(2) Ax)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> G \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> G
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G; \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> G
[PROOF STEP]
have "\<And>F f fa fb. \<not> (F \<turnstile>\<^sub>H f \<^bold>\<rightarrow> fa) \<or> \<not> (fb \<triangleright> F \<turnstile>\<^sub>H f) \<or> fb \<triangleright> F \<turnstile>\<^sub>H fa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>F f fa fb. \<not> (F \<turnstile>\<^sub>H f \<^bold>\<rightarrow> fa) \<or> \<not> (fb \<triangleright> F \<turnstile>\<^sub>H f) \<or> fb \<triangleright> F \<turnstile>\<^sub>H fa
[PROOF STEP]
by (meson HC_mono MP subset_insertI)
[PROOF STATE]
proof (state)
this:
\<not> (?F \<turnstile>\<^sub>H ?f \<^bold>\<rightarrow> ?fa) \<or> \<not> (?fb \<triangleright> ?F \<turnstile>\<^sub>H ?f) \<or> ?fb \<triangleright> ?F \<turnstile>\<^sub>H ?fa

goal (1 subgoal):
 1. \<lbrakk>\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G; \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> G
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (?F \<turnstile>\<^sub>H ?f \<^bold>\<rightarrow> ?fa) \<or> \<not> (?fb \<triangleright> ?F \<turnstile>\<^sub>H ?f) \<or> ?fb \<triangleright> ?F \<turnstile>\<^sub>H ?fa
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (?F \<turnstile>\<^sub>H ?f \<^bold>\<rightarrow> ?fa) \<or> \<not> (?fb \<triangleright> ?F \<turnstile>\<^sub>H ?f) \<or> ?fb \<triangleright> ?F \<turnstile>\<^sub>H ?fa

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> G
[PROOF STEP]
by (metis Ax \<open>\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G\<close> \<open>\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> \<^bold>\<not> F \<^bold>\<or> G\<close> insertI1 lem sim_disj)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> G

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<or> G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inpcp: "\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F
[PROOF STEP]
by (meson HC_intros(13) HC_mono MP dt subset_insertI sup_ge2)


[STATEMENT]
lemma HC_case_distinction: "\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> G \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> G \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> G; \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> G\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G
[PROOF STEP]
using HC_intros(7)[of F G "Not F"] lem2
[PROOF STATE]
proof (prove)
using this:
AX10 \<turnstile>\<^sub>H (F \<^bold>\<rightarrow> G) \<^bold>\<rightarrow> (\<^bold>\<not> F \<^bold>\<rightarrow> G) \<^bold>\<rightarrow> (F \<^bold>\<or> \<^bold>\<not> F) \<^bold>\<rightarrow> G
?\<Gamma> \<union> AX10 \<turnstile>\<^sub>H ?F \<^bold>\<or> \<^bold>\<not> ?F

goal (1 subgoal):
 1. \<lbrakk>\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> G; \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> G\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G
[PROOF STEP]
by (metis (no_types, opaque_lifting) HC.simps HC_mono insertI1 sim_disj subset_insertI)


[STATEMENT]
lemma HC_contrapos_nn:
  "\<lbrakk>\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F; \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G \<^bold>\<rightarrow> F\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F; \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G \<^bold>\<rightarrow> F\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> G
[PROOF STEP]
proof goal_cases
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F; \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G \<^bold>\<rightarrow> F\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> G
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H G \<^bold>\<rightarrow> F

goal (1 subgoal):
 1. \<lbrakk>\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F; \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G \<^bold>\<rightarrow> F\<rbrakk> \<Longrightarrow> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> G
[PROOF STEP]
from 1(1)
[PROOF STATE]
proof (chain)
picking this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F
[PROOF STEP]
have "\<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<bottom>"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H F \<^bold>\<rightarrow> \<bottom>
[PROOF STEP]
using HC_intros(12)
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F
AX10 \<turnstile>\<^sub>H \<^bold>\<not> ?F \<^bold>\<rightarrow> ?F \<^bold>\<rightarrow> \<bottom>

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

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

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

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G \<^bold>\<rightarrow> \<bottom>
[PROOF STEP]
by (meson 1(2) HC.intros(1) HC_mono MP dt insertI1 subset_insertI)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H G \<^bold>\<rightarrow> \<bottom>

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

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> G
[PROOF STEP]
by(meson HC_intros(11) HC_intros(3) HC_mono MP sup_ge2)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nor_sim:
assumes "\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> (F \<^bold>\<or> G)"
shows "\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F" " \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F &&& \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> G
[PROOF STEP]
using HC_contrapos_nn assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> ?F; ?\<Gamma> \<union> AX10 \<turnstile>\<^sub>H ?G \<^bold>\<rightarrow> ?F\<rbrakk> \<Longrightarrow> ?\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> ?G
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> (F \<^bold>\<or> G)

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F &&& \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> G
[PROOF STEP]
by (metis HC_intros(5,6) HC_mono sup_ge2)+


[STATEMENT]
lemma not_imp: "\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> F \<^bold>\<rightarrow> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> F \<^bold>\<rightarrow> G
[PROOF STEP]
proof goal_cases
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> F \<^bold>\<rightarrow> G
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> F \<^bold>\<rightarrow> G
[PROOF STEP]
have "\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> F \<^bold>\<rightarrow> \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> F \<^bold>\<rightarrow> \<bottom>
[PROOF STEP]
by (simp add: AX10.intros(9) Ax)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> F \<^bold>\<rightarrow> \<bottom>

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> F \<^bold>\<rightarrow> G
[PROOF STEP]
hence "\<^bold>\<not> F \<triangleright> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>"
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> F \<^bold>\<rightarrow> \<bottom>

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

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> F \<^bold>\<rightarrow> G
[PROOF STEP]
hence "\<^bold>\<not> F \<triangleright> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G"
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> F \<triangleright> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<bottom>

goal (1 subgoal):
 1. \<^bold>\<not> F \<triangleright> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G
[PROOF STEP]
by (metis (no_types, opaque_lifting) Un_commute Un_insert_right inpcp)
[PROOF STATE]
proof (state)
this:
\<^bold>\<not> F \<triangleright> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> F \<^bold>\<rightarrow> G
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<^bold>\<not> F \<triangleright> F \<triangleright> \<Gamma> \<union> AX10 \<turnstile>\<^sub>H G

goal (1 subgoal):
 1. \<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> F \<^bold>\<rightarrow> G
[PROOF STEP]
by (metis Un_insert_left dt insert_commute)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<union> AX10 \<turnstile>\<^sub>H \<^bold>\<not> F \<^bold>\<rightarrow> F \<^bold>\<rightarrow> G

goal:
No subgoals!
[PROOF STEP]
qed