[STATEMENT]
lemma eq_union_or:
  "simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g)
  = simplicial_complex_induced_by_monotone_boolean_function n f
    \<union> simplicial_complex_induced_by_monotone_boolean_function n g"
  (is "?sc n (?bf_or n f g) = ?sc n f \<union> ?sc n g")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g) = simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g) \<subseteq> simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g
 2. simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g \<subseteq> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g)
[PROOF STEP]
show "?sc n f \<union> ?sc n g \<subseteq> ?sc n (?bf_or n f g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g \<subseteq> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g)
[PROOF STEP]
fix \<sigma> :: "nat set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g)
[PROOF STEP]
assume "\<sigma> \<in> (?sc n f \<union> ?sc n g)"
[PROOF STATE]
proof (state)
this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g

goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g)
[PROOF STEP]
hence sigma: "\<sigma> \<in> ?sc n f \<or> \<sigma> \<in> ?sc n g"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g

goal (1 subgoal):
 1. \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<or> \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<or> \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n g

goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g)
[PROOF STEP]
have "f (simplicial_complex.bool_vec_from_simplice n \<sigma>)
           \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
proof (cases "\<sigma> \<in> ?sc n f")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<Longrightarrow> f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
 2. \<sigma> \<notin> simplicial_complex_induced_by_monotone_boolean_function n f \<Longrightarrow> f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f

goal (2 subgoals):
 1. \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<Longrightarrow> f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
 2. \<sigma> \<notin> simplicial_complex_induced_by_monotone_boolean_function n f \<Longrightarrow> f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
from simplicial_complex.simplicial_complex_implies_true [OF True]
[PROOF STATE]
proof (chain)
picking this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
show "f (simplicial_complex.bool_vec_from_simplice n \<sigma>)
           \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. \<sigma> \<notin> simplicial_complex_induced_by_monotone_boolean_function n f \<Longrightarrow> f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<sigma> \<notin> simplicial_complex_induced_by_monotone_boolean_function n f \<Longrightarrow> f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<sigma> \<notin> simplicial_complex_induced_by_monotone_boolean_function n f

goal (1 subgoal):
 1. \<sigma> \<notin> simplicial_complex_induced_by_monotone_boolean_function n f \<Longrightarrow> f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
hence sigmain: "\<sigma> \<in> ?sc n g"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<notin> simplicial_complex_induced_by_monotone_boolean_function n f

goal (1 subgoal):
 1. \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
using sigma
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<notin> simplicial_complex_induced_by_monotone_boolean_function n f
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<or> \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n g

goal (1 subgoal):
 1. \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n g

goal (1 subgoal):
 1. \<sigma> \<notin> simplicial_complex_induced_by_monotone_boolean_function n f \<Longrightarrow> f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
from simplicial_complex.simplicial_complex_implies_true [OF sigmain]
[PROOF STATE]
proof (chain)
picking this:
g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
show "f (simplicial_complex.bool_vec_from_simplice n \<sigma>)
           \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
g (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g)
[PROOF STEP]
thus "\<sigma> \<in> ?sc n (?bf_or n f g)"
[PROOF STATE]
proof (prove)
using this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g)
[PROOF STEP]
using simplicial_complex_induced_by_monotone_boolean_function_def
[PROOF STATE]
proof (prove)
using this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
simplicial_complex_induced_by_monotone_boolean_function ?n ?f = {y. \<exists>x. dim_vec x = ?n \<and> ?f x \<and> ceros_of_boolean_input x = y}

goal (1 subgoal):
 1. \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g)
[PROOF STEP]
using bool_fun_or_def sigma
[PROOF STATE]
proof (prove)
using this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
simplicial_complex_induced_by_monotone_boolean_function ?n ?f = {y. \<exists>x. dim_vec x = ?n \<and> ?f x \<and> ceros_of_boolean_input x = y}
bool_fun_or ?n ?f ?g \<equiv> \<lambda>x. ?f x \<or> ?g x
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<or> \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n g

goal (1 subgoal):
 1. \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g \<subseteq> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g)

goal (1 subgoal):
 1. simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g) \<subseteq> simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g) \<subseteq> simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
show "?sc n (?bf_or n f g) \<subseteq> ?sc n f \<union> ?sc n g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g) \<subseteq> simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g) \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
fix \<sigma>::"nat set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g) \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
assume sigma: "\<sigma> \<in> ?sc n (?bf_or n f g)"
[PROOF STATE]
proof (state)
this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g)

goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g) \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
hence "bool_fun_or n f g (simplicial_complex.bool_vec_from_simplice n \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g)

goal (1 subgoal):
 1. bool_fun_or n f g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
unfolding simplicial_complex.bool_vec_from_simplice_def
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g)

goal (1 subgoal):
 1. bool_fun_or n f g (vec n (\<lambda>i. i \<notin> \<sigma>))
[PROOF STEP]
unfolding simplicial_complex_induced_by_monotone_boolean_function_def
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<in> {y. \<exists>x. dim_vec x = n \<and> bool_fun_or n f g x \<and> ceros_of_boolean_input x = y}

goal (1 subgoal):
 1. bool_fun_or n f g (vec n (\<lambda>i. i \<notin> \<sigma>))
[PROOF STEP]
unfolding ceros_of_boolean_input_def
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<in> {y. \<exists>x. dim_vec x = n \<and> bool_fun_or n f g x \<and> {xa. xa < dim_vec x \<and> x $ xa = False} = y}

goal (1 subgoal):
 1. bool_fun_or n f g (vec n (\<lambda>i. i \<notin> \<sigma>))
[PROOF STEP]
by auto (smt (verit) dim_vec eq_vecI index_vec)+
[PROOF STATE]
proof (state)
this:
bool_fun_or n f g (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g) \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
hence "(f (simplicial_complex.bool_vec_from_simplice n \<sigma>))
            \<or> (g (simplicial_complex.bool_vec_from_simplice n \<sigma>))"
[PROOF STATE]
proof (prove)
using this:
bool_fun_or n f g (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
unfolding bool_fun_or_def
[PROOF STATE]
proof (prove)
using this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g) \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
hence "\<sigma> \<in> ?sc n f \<or> \<sigma> \<in> ?sc n g"
[PROOF STATE]
proof (prove)
using this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<or> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<or> \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
by (smt (z3) sigma bool_fun_or_def mem_Collect_eq
            simplicial_complex_induced_by_monotone_boolean_function_def)
[PROOF STATE]
proof (state)
this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<or> \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n g

goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g) \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
thus "\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f
          \<union> simplicial_complex_induced_by_monotone_boolean_function n g"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<or> \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n g

goal (1 subgoal):
 1. \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_or n f g) \<subseteq> simplicial_complex_induced_by_monotone_boolean_function n f \<union> simplicial_complex_induced_by_monotone_boolean_function n g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eq_inter_and:
  "simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g)
  = simplicial_complex_induced_by_monotone_boolean_function n f
    \<inter> simplicial_complex_induced_by_monotone_boolean_function n g"
  (is "?sc n (?bf_and n f g) = ?sc n f \<inter> ?sc n g")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g) = simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g) \<subseteq> simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g
 2. simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g \<subseteq> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g)
[PROOF STEP]
show "?sc n f \<inter> ?sc n g \<subseteq> ?sc n (?bf_and n f g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g \<subseteq> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g)
[PROOF STEP]
fix \<sigma> :: "nat set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g)
[PROOF STEP]
assume "\<sigma> \<in> (?sc n f \<inter> ?sc n g)"
[PROOF STATE]
proof (state)
this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g

goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g)
[PROOF STEP]
hence sigma: "\<sigma> \<in> ?sc n f \<and> \<sigma> \<in> ?sc n g"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g

goal (1 subgoal):
 1. \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<and> \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<and> \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n g

goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g)
[PROOF STEP]
have "f (simplicial_complex.bool_vec_from_simplice n \<sigma>)
           \<and> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<and> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<and> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
from sigma
[PROOF STATE]
proof (chain)
picking this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<and> \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
have sigmaf: "\<sigma> \<in> ?sc n f" and sigmag: "\<sigma> \<in> ?sc n g"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<and> \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n g

goal (1 subgoal):
 1. \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f &&& \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n g

goal (1 subgoal):
 1. f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<and> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
have "f (simplicial_complex.bool_vec_from_simplice n \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
using simplicial_complex.simplicial_complex_implies_true [OF sigmaf]
[PROOF STATE]
proof (prove)
using this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. f (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<and> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<and> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
have "g (simplicial_complex.bool_vec_from_simplice n \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
using simplicial_complex.simplicial_complex_implies_true [OF sigmag]
[PROOF STATE]
proof (prove)
using this:
g (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
g (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<and> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>)
g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>)
g (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<and> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<and> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<and> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g)
[PROOF STEP]
thus "\<sigma> \<in> ?sc n (?bf_and n f g)"
[PROOF STATE]
proof (prove)
using this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<and> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g)
[PROOF STEP]
unfolding simplicial_complex_induced_by_monotone_boolean_function_def
[PROOF STATE]
proof (prove)
using this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<and> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. \<sigma> \<in> {y. \<exists>x. dim_vec x = n \<and> bool_fun_and n f g x \<and> ceros_of_boolean_input x = y}
[PROOF STEP]
unfolding bool_fun_and_def
[PROOF STATE]
proof (prove)
using this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<and> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. \<sigma> \<in> {y. \<exists>x. dim_vec x = n \<and> (f x \<and> g x) \<and> ceros_of_boolean_input x = y}
[PROOF STEP]
using sigma
[PROOF STATE]
proof (prove)
using this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<and> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<and> \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n g

goal (1 subgoal):
 1. \<sigma> \<in> {y. \<exists>x. dim_vec x = n \<and> (f x \<and> g x) \<and> ceros_of_boolean_input x = y}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f (simplicial_complex.bool_vec_from_simplice n \<sigma>); g (simplicial_complex.bool_vec_from_simplice n \<sigma>); \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f; \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n g\<rbrakk> \<Longrightarrow> \<exists>x. dim_vec x = n \<and> f x \<and> g x \<and> ceros_of_boolean_input x = \<sigma>
[PROOF STEP]
by (smt (z3) Collect_cong ceros_of_boolean_input_def dim_vec index_vec mem_Collect_eq
          simplicial_complex.bool_vec_from_simplice_def
          simplicial_complex_induced_by_monotone_boolean_function_def)
[PROOF STATE]
proof (state)
this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g \<subseteq> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g)

goal (1 subgoal):
 1. simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g) \<subseteq> simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g) \<subseteq> simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
show "?sc n (?bf_and n f g) \<subseteq> ?sc n f \<inter> ?sc n g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g) \<subseteq> simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g) \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
fix \<sigma> :: "nat set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g) \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
assume sigma: "\<sigma> \<in> ?sc n (?bf_and n f g)"
[PROOF STATE]
proof (state)
this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g)

goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g) \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
hence "bool_fun_and n f g (simplicial_complex.bool_vec_from_simplice n \<sigma>)"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g)

goal (1 subgoal):
 1. bool_fun_and n f g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
unfolding simplicial_complex.bool_vec_from_simplice_def
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g)

goal (1 subgoal):
 1. bool_fun_and n f g (vec n (\<lambda>i. i \<notin> \<sigma>))
[PROOF STEP]
unfolding simplicial_complex_induced_by_monotone_boolean_function_def
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<in> {y. \<exists>x. dim_vec x = n \<and> bool_fun_and n f g x \<and> ceros_of_boolean_input x = y}

goal (1 subgoal):
 1. bool_fun_and n f g (vec n (\<lambda>i. i \<notin> \<sigma>))
[PROOF STEP]
unfolding ceros_of_boolean_input_def
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<in> {y. \<exists>x. dim_vec x = n \<and> bool_fun_and n f g x \<and> {xa. xa < dim_vec x \<and> x $ xa = False} = y}

goal (1 subgoal):
 1. bool_fun_and n f g (vec n (\<lambda>i. i \<notin> \<sigma>))
[PROOF STEP]
by auto (smt (verit) dim_vec eq_vecI index_vec)+
[PROOF STATE]
proof (state)
this:
bool_fun_and n f g (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g) \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
hence "(f (simplicial_complex.bool_vec_from_simplice n \<sigma>))
          \<and> (g (simplicial_complex.bool_vec_from_simplice n \<sigma>))"
[PROOF STATE]
proof (prove)
using this:
bool_fun_and n f g (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<and> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
unfolding bool_fun_and_def
[PROOF STATE]
proof (prove)
using this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<and> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<and> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<and> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g) \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
hence "\<sigma> \<in> ?sc n f \<and> \<sigma> \<in> ?sc n g"
[PROOF STATE]
proof (prove)
using this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<and> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)

goal (1 subgoal):
 1. \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<and> \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
using bool_fun_and_def sigma simplicial_complex_induced_by_monotone_boolean_function_def
[PROOF STATE]
proof (prove)
using this:
f (simplicial_complex.bool_vec_from_simplice n \<sigma>) \<and> g (simplicial_complex.bool_vec_from_simplice n \<sigma>)
bool_fun_and ?n ?f ?g \<equiv> \<lambda>x. ?f x \<and> ?g x
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g)
simplicial_complex_induced_by_monotone_boolean_function ?n ?f = {y. \<exists>x. dim_vec x = ?n \<and> ?f x \<and> ceros_of_boolean_input x = y}

goal (1 subgoal):
 1. \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<and> \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<and> \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n g

goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g) \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
thus "\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f
          \<inter> simplicial_complex_induced_by_monotone_boolean_function n g"
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<and> \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n g

goal (1 subgoal):
 1. \<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<sigma> \<in> simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
simplicial_complex_induced_by_monotone_boolean_function n (bool_fun_and n f g) \<subseteq> simplicial_complex_induced_by_monotone_boolean_function n f \<inter> simplicial_complex_induced_by_monotone_boolean_function n g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fst_es_simplice:
  "a \<in> simplicial_complex_induced_by_monotone_boolean_function_ast n f
    \<Longrightarrow> (\<exists>x y. f (x, y) \<and> (ceros_of_boolean_input x) = fst(a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> simplicial_complex_induced_by_monotone_boolean_function_ast n f \<Longrightarrow> \<exists>x y. f (x, y) \<and> ceros_of_boolean_input x = fst a
[PROOF STEP]
by (smt (verit) fst_conv mem_Collect_eq
        simplicial_complex_induced_by_monotone_boolean_function_ast_def)


[STATEMENT]
lemma snd_es_simplice:
  "a \<in> simplicial_complex_induced_by_monotone_boolean_function_ast n f
    \<Longrightarrow> (\<exists>x y. f (x, y) \<and> (ceros_of_boolean_input y) = snd(a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> simplicial_complex_induced_by_monotone_boolean_function_ast n f \<Longrightarrow> \<exists>x y. f (x, y) \<and> ceros_of_boolean_input y = snd a
[PROOF STEP]
by (smt (verit) snd_conv mem_Collect_eq
      simplicial_complex_induced_by_monotone_boolean_function_ast_def)


[STATEMENT]
lemma set_fst_simp [simp]:
  assumes "y \<noteq> {}"
  shows "set_fst (x \<times> y) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_fst (x \<times> y) = x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set_fst (x \<times> y) \<subseteq> x
 2. x \<subseteq> set_fst (x \<times> y)
[PROOF STEP]
show "set_fst (x \<times> y) \<subseteq> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_fst (x \<times> y) \<subseteq> x
[PROOF STEP]
by (smt (verit) SigmaE mem_Collect_eq prod.sel(1) set_fst_def subsetI)
[PROOF STATE]
proof (state)
this:
set_fst (x \<times> y) \<subseteq> x

goal (1 subgoal):
 1. x \<subseteq> set_fst (x \<times> y)
[PROOF STEP]
show "x \<subseteq> set_fst (x \<times> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<subseteq> set_fst (x \<times> y)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> x \<Longrightarrow> xa \<in> set_fst (x \<times> y)
[PROOF STEP]
fix a::"nat"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> x \<Longrightarrow> xa \<in> set_fst (x \<times> y)
[PROOF STEP]
assume "a \<in> x"
[PROOF STATE]
proof (state)
this:
a \<in> x

goal (1 subgoal):
 1. \<And>xa. xa \<in> x \<Longrightarrow> xa \<in> set_fst (x \<times> y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> x
[PROOF STEP]
obtain b where "b \<in> y" and "(a,b) \<in> (x\<times>y)"
[PROOF STATE]
proof (prove)
using this:
a \<in> x

goal (1 subgoal):
 1. (\<And>b. \<lbrakk>b \<in> y; (a, b) \<in> x \<times> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in> x
y \<noteq> {}

goal (1 subgoal):
 1. (\<And>b. \<lbrakk>b \<in> y; (a, b) \<in> x \<times> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b \<in> y
(a, b) \<in> x \<times> y

goal (1 subgoal):
 1. \<And>xa. xa \<in> x \<Longrightarrow> xa \<in> set_fst (x \<times> y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in> y
(a, b) \<in> x \<times> y
[PROOF STEP]
show "a \<in> set_fst (x \<times> y)"
[PROOF STATE]
proof (prove)
using this:
b \<in> y
(a, b) \<in> x \<times> y

goal (1 subgoal):
 1. a \<in> set_fst (x \<times> y)
[PROOF STEP]
using set_fst_def
[PROOF STATE]
proof (prove)
using this:
b \<in> y
(a, b) \<in> x \<times> y
set_fst ?AB = {a. \<exists>ab\<in>?AB. a = fst ab}

goal (1 subgoal):
 1. a \<in> set_fst (x \<times> y)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
a \<in> set_fst (x \<times> y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<subseteq> set_fst (x \<times> y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eq_ast:
"simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f)
= set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f))
          (simplicial_complex_induced_by_monotone_boolean_function m (snd f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f) = set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f) \<subseteq> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f))
 2. set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f)) \<subseteq> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f)
[PROOF STEP]
show "set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f))
     (simplicial_complex_induced_by_monotone_boolean_function m (snd f))
    \<subseteq> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m)
        (bool_fun_ast (n, m) f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f)) \<subseteq> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f)) \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f)
[PROOF STEP]
fix \<gamma>::"nat set*nat set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f)) \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f)
[PROOF STEP]
assume pert: "\<gamma> \<in> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f))
     (simplicial_complex_induced_by_monotone_boolean_function m (snd f))"
[PROOF STATE]
proof (state)
this:
\<gamma> \<in> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f))

goal (1 subgoal):
 1. \<And>x. x \<in> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f)) \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f)
[PROOF STEP]
hence f: "(fst \<gamma>) \<in> simplicial_complex_induced_by_monotone_boolean_function n (fst f)"
[PROOF STATE]
proof (prove)
using this:
\<gamma> \<in> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f))

goal (1 subgoal):
 1. fst \<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function n (fst f)
[PROOF STEP]
unfolding set_ast_def
[PROOF STATE]
proof (prove)
using this:
\<gamma> \<in> {c. \<exists>a\<in>simplicial_complex_induced_by_monotone_boolean_function n (fst f). \<exists>b\<in>simplicial_complex_induced_by_monotone_boolean_function m (snd f). c = (a, b)}

goal (1 subgoal):
 1. fst \<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function n (fst f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst \<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function n (fst f)

goal (1 subgoal):
 1. \<And>x. x \<in> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f)) \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f)
[PROOF STEP]
have sigma: "fst f (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst f (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>))
[PROOF STEP]
using simplicial_complex.simplicial_complex_implies_true [OF f]
[PROOF STATE]
proof (prove)
using this:
fst f (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>))

goal (1 subgoal):
 1. fst f (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
fst f (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>))

goal (1 subgoal):
 1. \<And>x. x \<in> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f)) \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f)
[PROOF STEP]
from pert
[PROOF STATE]
proof (chain)
picking this:
\<gamma> \<in> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f))
[PROOF STEP]
have g: "(snd \<gamma>) \<in> simplicial_complex_induced_by_monotone_boolean_function m (snd f)"
[PROOF STATE]
proof (prove)
using this:
\<gamma> \<in> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f))

goal (1 subgoal):
 1. snd \<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function m (snd f)
[PROOF STEP]
unfolding set_ast_def
[PROOF STATE]
proof (prove)
using this:
\<gamma> \<in> {c. \<exists>a\<in>simplicial_complex_induced_by_monotone_boolean_function n (fst f). \<exists>b\<in>simplicial_complex_induced_by_monotone_boolean_function m (snd f). c = (a, b)}

goal (1 subgoal):
 1. snd \<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function m (snd f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
snd \<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function m (snd f)

goal (1 subgoal):
 1. \<And>x. x \<in> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f)) \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f)
[PROOF STEP]
have tau: "(snd f) (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd f (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))
[PROOF STEP]
using simplicial_complex.simplicial_complex_implies_true [OF g]
[PROOF STATE]
proof (prove)
using this:
snd f (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))

goal (1 subgoal):
 1. snd f (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
snd f (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))

goal (1 subgoal):
 1. \<And>x. x \<in> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f)) \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f)
[PROOF STEP]
from sigma and tau
[PROOF STATE]
proof (chain)
picking this:
fst f (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>))
snd f (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))
[PROOF STEP]
have sigtau: "bool_fun_ast (n, m) f
        ((simplicial_complex.bool_vec_from_simplice n (fst \<gamma>)),
         (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>)))"
[PROOF STATE]
proof (prove)
using this:
fst f (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>))
snd f (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))

goal (1 subgoal):
 1. bool_fun_ast (n, m) f (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>), simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))
[PROOF STEP]
unfolding bool_fun_ast_def
[PROOF STATE]
proof (prove)
using this:
fst f (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>))
snd f (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))

goal (1 subgoal):
 1. case (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>), simplicial_complex.bool_vec_from_simplice m (snd \<gamma>)) of (x, y) \<Rightarrow> fst f x \<and> snd f y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bool_fun_ast (n, m) f (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>), simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))

goal (1 subgoal):
 1. \<And>x. x \<in> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f)) \<Longrightarrow> x \<in> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f)
[PROOF STEP]
from sigtau
[PROOF STATE]
proof (chain)
picking this:
bool_fun_ast (n, m) f (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>), simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))
[PROOF STEP]
show "\<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m)
              (bool_fun_ast (n, m) f)"
[PROOF STATE]
proof (prove)
using this:
bool_fun_ast (n, m) f (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>), simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))

goal (1 subgoal):
 1. \<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f)
[PROOF STEP]
unfolding simplicial_complex_induced_by_monotone_boolean_function_ast_def
[PROOF STATE]
proof (prove)
using this:
bool_fun_ast (n, m) f (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>), simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))

goal (1 subgoal):
 1. \<gamma> \<in> {z. \<exists>x y. dim_vec x = fst (n, m) \<and> dim_vec y = snd (n, m) \<and> bool_fun_ast (n, m) f (x, y) \<and> (ceros_of_boolean_input x, ceros_of_boolean_input y) = z}
[PROOF STEP]
unfolding bool_fun_ast_def
[PROOF STATE]
proof (prove)
using this:
case (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>), simplicial_complex.bool_vec_from_simplice m (snd \<gamma>)) of (x, y) \<Rightarrow> fst f x \<and> snd f y

goal (1 subgoal):
 1. \<gamma> \<in> {z. \<exists>x y. dim_vec x = fst (n, m) \<and> dim_vec y = snd (n, m) \<and> (case (x, y) of (x, y) \<Rightarrow> fst f x \<and> snd f y) \<and> (ceros_of_boolean_input x, ceros_of_boolean_input y) = z}
[PROOF STEP]
using sigma
[PROOF STATE]
proof (prove)
using this:
case (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>), simplicial_complex.bool_vec_from_simplice m (snd \<gamma>)) of (x, y) \<Rightarrow> fst f x \<and> snd f y
fst f (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>))

goal (1 subgoal):
 1. \<gamma> \<in> {z. \<exists>x y. dim_vec x = fst (n, m) \<and> dim_vec y = snd (n, m) \<and> (case (x, y) of (x, y) \<Rightarrow> fst f x \<and> snd f y) \<and> (ceros_of_boolean_input x, ceros_of_boolean_input y) = z}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>snd f (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>)); fst f (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>))\<rbrakk> \<Longrightarrow> \<exists>x. dim_vec x = n \<and> (\<exists>y. dim_vec y = m \<and> fst f x \<and> snd f y \<and> (ceros_of_boolean_input x, ceros_of_boolean_input y) = \<gamma>)
[PROOF STEP]
using f g simplicial_complex_induced_by_monotone_boolean_function_def
[PROOF STATE]
proof (prove)
using this:
fst \<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function n (fst f)
snd \<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function m (snd f)
simplicial_complex_induced_by_monotone_boolean_function ?n ?f = {y. \<exists>x. dim_vec x = ?n \<and> ?f x \<and> ceros_of_boolean_input x = y}

goal (1 subgoal):
 1. \<lbrakk>snd f (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>)); fst f (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>))\<rbrakk> \<Longrightarrow> \<exists>x. dim_vec x = n \<and> (\<exists>y. dim_vec y = m \<and> fst f x \<and> snd f y \<and> (ceros_of_boolean_input x, ceros_of_boolean_input y) = \<gamma>)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f)) \<subseteq> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f)

goal (1 subgoal):
 1. simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f) \<subseteq> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f) \<subseteq> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f))
[PROOF STEP]
show "simplicial_complex_induced_by_monotone_boolean_function_ast (n, m)
     (bool_fun_ast (n, m) f)
    \<subseteq> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f))
        (simplicial_complex_induced_by_monotone_boolean_function m (snd f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f) \<subseteq> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f) \<Longrightarrow> x \<in> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f))
[PROOF STEP]
fix \<gamma> :: "nat set*nat set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f) \<Longrightarrow> x \<in> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f))
[PROOF STEP]
assume pert: "\<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m)
     (bool_fun_ast (n, m) f)"
[PROOF STATE]
proof (state)
this:
\<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f)

goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f) \<Longrightarrow> x \<in> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f))
[PROOF STEP]
have sigma: "(fst \<gamma>) \<in> simplicial_complex_induced_by_monotone_boolean_function n (fst f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst \<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function n (fst f)
[PROOF STEP]
unfolding bool_fun_ast_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst \<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function n (fst f)
[PROOF STEP]
unfolding simplicial_complex_induced_by_monotone_boolean_function_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst \<gamma> \<in> {y. \<exists>x. dim_vec x = n \<and> fst f x \<and> ceros_of_boolean_input x = y}
[PROOF STEP]
unfolding simplicial_complex_induced_by_monotone_boolean_function_ast_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst \<gamma> \<in> {y. \<exists>x. dim_vec x = n \<and> fst f x \<and> ceros_of_boolean_input x = y}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. dim_vec x = n \<and> fst f x \<and> ceros_of_boolean_input x = fst \<gamma>
[PROOF STEP]
apply (rule exI [of _ "simplicial_complex.bool_vec_from_simplice n (fst \<gamma>)"], safe)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. dim_vec (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>)) = n
 2. fst f (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>))
 3. \<And>x. x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>)) \<Longrightarrow> x \<in> fst \<gamma>
 4. \<And>x. x \<in> fst \<gamma> \<Longrightarrow> x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>))
[PROOF STEP]
using simplicial_complex.bool_vec_from_simplice_def
[PROOF STATE]
proof (prove)
using this:
simplicial_complex.bool_vec_from_simplice ?n ?\<sigma> = vec ?n (\<lambda>i. i \<notin> ?\<sigma>)

goal (4 subgoals):
 1. dim_vec (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>)) = n
 2. fst f (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>))
 3. \<And>x. x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>)) \<Longrightarrow> x \<in> fst \<gamma>
 4. \<And>x. x \<in> fst \<gamma> \<Longrightarrow> x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>))
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. fst f (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>))
 2. \<And>x. x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>)) \<Longrightarrow> x \<in> fst \<gamma>
 3. \<And>x. x \<in> fst \<gamma> \<Longrightarrow> x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>))
[PROOF STEP]
apply (metis fst_conv pert simplicial_complex_ast_implies_fst_true)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>)) \<Longrightarrow> x \<in> fst \<gamma>
 2. \<And>x. x \<in> fst \<gamma> \<Longrightarrow> x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>))
[PROOF STEP]
using ceros_of_boolean_input_def simplicial_complex.bool_vec_from_simplice_def
[PROOF STATE]
proof (prove)
using this:
ceros_of_boolean_input ?v = {x. x < dim_vec ?v \<and> ?v $ x = False}
simplicial_complex.bool_vec_from_simplice ?n ?\<sigma> = vec ?n (\<lambda>i. i \<notin> ?\<sigma>)

goal (2 subgoals):
 1. \<And>x. x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>)) \<Longrightarrow> x \<in> fst \<gamma>
 2. \<And>x. x \<in> fst \<gamma> \<Longrightarrow> x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>))
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> fst \<gamma> \<Longrightarrow> x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>))
[PROOF STEP]
using ceros_of_boolean_input_def pert
          simplicial_complex.bool_vec_from_simplice_def
          simplicial_complex_induced_by_monotone_boolean_function_ast_def
[PROOF STATE]
proof (prove)
using this:
ceros_of_boolean_input ?v = {x. x < dim_vec ?v \<and> ?v $ x = False}
\<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f)
simplicial_complex.bool_vec_from_simplice ?n ?\<sigma> = vec ?n (\<lambda>i. i \<notin> ?\<sigma>)
simplicial_complex_induced_by_monotone_boolean_function_ast ?n ?f = {z. \<exists>x y. dim_vec x = fst ?n \<and> dim_vec y = snd ?n \<and> ?f (x, y) \<and> (ceros_of_boolean_input x, ceros_of_boolean_input y) = z}

goal (1 subgoal):
 1. \<And>x. x \<in> fst \<gamma> \<Longrightarrow> x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice n (fst \<gamma>))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
fst \<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function n (fst f)

goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f) \<Longrightarrow> x \<in> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f))
[PROOF STEP]
have tau: "(snd \<gamma>) \<in> simplicial_complex_induced_by_monotone_boolean_function m (snd f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd \<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function m (snd f)
[PROOF STEP]
unfolding bool_fun_ast_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd \<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function m (snd f)
[PROOF STEP]
unfolding simplicial_complex_induced_by_monotone_boolean_function_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd \<gamma> \<in> {y. \<exists>x. dim_vec x = m \<and> snd f x \<and> ceros_of_boolean_input x = y}
[PROOF STEP]
unfolding simplicial_complex_induced_by_monotone_boolean_function_ast_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd \<gamma> \<in> {y. \<exists>x. dim_vec x = m \<and> snd f x \<and> ceros_of_boolean_input x = y}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. dim_vec x = m \<and> snd f x \<and> ceros_of_boolean_input x = snd \<gamma>
[PROOF STEP]
apply (rule exI [of _ "simplicial_complex.bool_vec_from_simplice m (snd \<gamma>)"], safe)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. dim_vec (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>)) = m
 2. snd f (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))
 3. \<And>x. x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>)) \<Longrightarrow> x \<in> snd \<gamma>
 4. \<And>x. x \<in> snd \<gamma> \<Longrightarrow> x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))
[PROOF STEP]
using simplicial_complex.bool_vec_from_simplice_def
[PROOF STATE]
proof (prove)
using this:
simplicial_complex.bool_vec_from_simplice ?n ?\<sigma> = vec ?n (\<lambda>i. i \<notin> ?\<sigma>)

goal (4 subgoals):
 1. dim_vec (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>)) = m
 2. snd f (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))
 3. \<And>x. x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>)) \<Longrightarrow> x \<in> snd \<gamma>
 4. \<And>x. x \<in> snd \<gamma> \<Longrightarrow> x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. snd f (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))
 2. \<And>x. x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>)) \<Longrightarrow> x \<in> snd \<gamma>
 3. \<And>x. x \<in> snd \<gamma> \<Longrightarrow> x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))
[PROOF STEP]
apply (metis snd_conv pert simplicial_complex_ast_implies_snd_true)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>)) \<Longrightarrow> x \<in> snd \<gamma>
 2. \<And>x. x \<in> snd \<gamma> \<Longrightarrow> x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))
[PROOF STEP]
using ceros_of_boolean_input_def simplicial_complex.bool_vec_from_simplice_def
[PROOF STATE]
proof (prove)
using this:
ceros_of_boolean_input ?v = {x. x < dim_vec ?v \<and> ?v $ x = False}
simplicial_complex.bool_vec_from_simplice ?n ?\<sigma> = vec ?n (\<lambda>i. i \<notin> ?\<sigma>)

goal (2 subgoals):
 1. \<And>x. x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>)) \<Longrightarrow> x \<in> snd \<gamma>
 2. \<And>x. x \<in> snd \<gamma> \<Longrightarrow> x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> snd \<gamma> \<Longrightarrow> x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))
[PROOF STEP]
using ceros_of_boolean_input_def pert
        simplicial_complex.bool_vec_from_simplice_def
        simplicial_complex_induced_by_monotone_boolean_function_ast_def
[PROOF STATE]
proof (prove)
using this:
ceros_of_boolean_input ?v = {x. x < dim_vec ?v \<and> ?v $ x = False}
\<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f)
simplicial_complex.bool_vec_from_simplice ?n ?\<sigma> = vec ?n (\<lambda>i. i \<notin> ?\<sigma>)
simplicial_complex_induced_by_monotone_boolean_function_ast ?n ?f = {z. \<exists>x y. dim_vec x = fst ?n \<and> dim_vec y = snd ?n \<and> ?f (x, y) \<and> (ceros_of_boolean_input x, ceros_of_boolean_input y) = z}

goal (1 subgoal):
 1. \<And>x. x \<in> snd \<gamma> \<Longrightarrow> x \<in> ceros_of_boolean_input (simplicial_complex.bool_vec_from_simplice m (snd \<gamma>))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
snd \<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function m (snd f)

goal (1 subgoal):
 1. \<And>x. x \<in> simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f) \<Longrightarrow> x \<in> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f))
[PROOF STEP]
from sigma and tau
[PROOF STATE]
proof (chain)
picking this:
fst \<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function n (fst f)
snd \<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function m (snd f)
[PROOF STEP]
show "\<gamma> \<in> set_ast
        (simplicial_complex_induced_by_monotone_boolean_function n (fst f))
        (simplicial_complex_induced_by_monotone_boolean_function m (snd f))"
[PROOF STATE]
proof (prove)
using this:
fst \<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function n (fst f)
snd \<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function m (snd f)

goal (1 subgoal):
 1. \<gamma> \<in> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f))
[PROOF STEP]
using set_ast_def
[PROOF STATE]
proof (prove)
using this:
fst \<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function n (fst f)
snd \<gamma> \<in> simplicial_complex_induced_by_monotone_boolean_function m (snd f)
set_ast ?A ?B \<equiv> {c. \<exists>a\<in>?A. \<exists>b\<in>?B. c = (a, b)}

goal (1 subgoal):
 1. \<gamma> \<in> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f))
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<gamma> \<in> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
simplicial_complex_induced_by_monotone_boolean_function_ast (n, m) (bool_fun_ast (n, m) f) \<subseteq> set_ast (simplicial_complex_induced_by_monotone_boolean_function n (fst f)) (simplicial_complex_induced_by_monotone_boolean_function m (snd f))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ufa_invarD:
  "ufa_invar l \<Longrightarrow> i < length l \<Longrightarrow> rep_of_dom (l, i) \<and> l ! i < length l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> rep_of_dom (l, i) \<and> l ! i < length l
[PROOF STEP]
by auto2


[STATEMENT]
lemma rep_of_id [rewrite]: "ufa_invar l \<Longrightarrow> i < length l \<Longrightarrow> l ! i = i \<Longrightarrow> rep_of l i = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l; l ! i = i\<rbrakk> \<Longrightarrow> rep_of l i = i
[PROOF STEP]
by auto2


[STATEMENT]
lemma rep_of_iff [rewrite]:
  "ufa_invar l \<Longrightarrow> i < length l \<Longrightarrow> rep_of l i = (if l ! i = i then i else rep_of l (l ! i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> rep_of l i = (if l ! i = i then i else rep_of l (l ! i))
[PROOF STEP]
by auto2


[STATEMENT]
lemma rep_of_min [rewrite]:
  "ufa_invar l \<Longrightarrow> i < length l \<Longrightarrow> l ! (rep_of l i) = rep_of l i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> l ! rep_of l i = rep_of l i
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> l ! rep_of l i = rep_of l i
[PROOF STEP]
@prop_induct "rep_of_dom (l, i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> l ! rep_of l i = rep_of l i
[PROOF STEP]
@qed


[STATEMENT]
lemma rep_of_induct:
  "ufa_invar l \<and> i < length l \<Longrightarrow>
   \<forall>i<length l. l ! i = i \<longrightarrow> P l i \<Longrightarrow>
   \<forall>i<length l. l ! i \<noteq> i \<longrightarrow> P l (l ! i) \<longrightarrow> P l i \<Longrightarrow> P l i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l \<and> i < length l; \<forall>i<length l. l ! i = i \<longrightarrow> P l i; \<forall>i<length l. l ! i \<noteq> i \<longrightarrow> P l (l ! i) \<longrightarrow> P l i\<rbrakk> \<Longrightarrow> P l i
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l \<and> i < length l; \<forall>i<length l. l ! i = i \<longrightarrow> P l i; \<forall>i<length l. l ! i \<noteq> i \<longrightarrow> P l (l ! i) \<longrightarrow> P l i\<rbrakk> \<Longrightarrow> P l i
[PROOF STEP]
@prop_induct "rep_of_dom (l, i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l \<and> i < length l; \<forall>i<length l. l ! i = i \<longrightarrow> P l i; \<forall>i<length l. l ! i \<noteq> i \<longrightarrow> P l (l ! i) \<longrightarrow> P l i\<rbrakk> \<Longrightarrow> P l i
[PROOF STEP]
@qed


[STATEMENT]
lemma rep_of_bound [forward_arg1]:
  "ufa_invar l \<Longrightarrow> i < length l \<Longrightarrow> rep_of l i < length l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> rep_of l i < length l
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> rep_of l i < length l
[PROOF STEP]
@prop_induct "ufa_invar l \<and> i < length l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> rep_of l i < length l
[PROOF STEP]
@qed


[STATEMENT]
lemma rep_of_idem [rewrite]:
  "ufa_invar l \<Longrightarrow> i < length l \<Longrightarrow> rep_of l (rep_of l i) = rep_of l i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> rep_of l (rep_of l i) = rep_of l i
[PROOF STEP]
by auto2


[STATEMENT]
lemma rep_of_idx [rewrite]:
  "ufa_invar l \<Longrightarrow> i < length l \<Longrightarrow> rep_of l (l ! i) = rep_of l i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; i < length l\<rbrakk> \<Longrightarrow> rep_of l (l ! i) = rep_of l i
[PROOF STEP]
by auto2


[STATEMENT]
lemma ufa_\<alpha>_memI [backward, forward_arg]:
  "x < length l \<Longrightarrow> y < length l \<Longrightarrow> rep_of l x = rep_of l y \<Longrightarrow> (x, y) \<in> ufa_\<alpha> l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < length l; y < length l; rep_of l x = rep_of l y\<rbrakk> \<Longrightarrow> (x, y) \<in> ufa_\<alpha> l
[PROOF STEP]
by (simp add: ufa_\<alpha>_def)


[STATEMENT]
lemma ufa_\<alpha>_memD [forward]:
  "(x, y) \<in> ufa_\<alpha> l \<Longrightarrow> x < length l \<and> y < length l \<and> rep_of l x = rep_of l y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> ufa_\<alpha> l \<Longrightarrow> x < length l \<and> y < length l \<and> rep_of l x = rep_of l y
[PROOF STEP]
by (simp add: ufa_\<alpha>_def)


[STATEMENT]
lemma ufa_\<alpha>_equiv [forward]: "part_equiv (ufa_\<alpha> l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. part_equiv (ufa_\<alpha> l)
[PROOF STEP]
by auto2


[STATEMENT]
lemma ufa_\<alpha>_refl [rewrite]: "(i, i) \<in> ufa_\<alpha> l \<longleftrightarrow> i < length l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((i, i) \<in> ufa_\<alpha> l) = (i < length l)
[PROOF STEP]
by auto2


[STATEMENT]
lemma ufa_init_invar [resolve]: "ufa_invar [0..<n]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ufa_invar [0..<n]
[PROOF STEP]
by auto2


[STATEMENT]
lemma ufa_init_correct [rewrite]:
  "(x, y) \<in> uf_init_rel n \<longleftrightarrow> (x = y \<and> x < n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x, y) \<in> uf_init_rel n) = (x = y \<and> x < n)
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x, y) \<in> uf_init_rel n) = (x = y \<and> x < n)
[PROOF STEP]
@have "ufa_invar [0..<n]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x, y) \<in> uf_init_rel n) = (x = y \<and> x < n)
[PROOF STEP]
@qed


[STATEMENT]
lemma ufa_union_invar [forward_arg]:
  "ufa_invar l \<Longrightarrow> x < length l \<Longrightarrow> y < length l \<Longrightarrow> l' = ufa_union l x y \<Longrightarrow> ufa_invar l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; y < length l; l' = ufa_union l x y\<rbrakk> \<Longrightarrow> ufa_invar l'
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; y < length l; l' = ufa_union l x y\<rbrakk> \<Longrightarrow> ufa_invar l'
[PROOF STEP]
@have "\<forall>i<length l'. rep_of_dom (l', i) \<and> l' ! i < length l'" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; y < length l; l' = ufa_union l x y\<rbrakk> \<Longrightarrow> ufa_invar l'
[PROOF STEP]
@prop_induct "ufa_invar l \<and> i < length l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; y < length l; l' = ufa_union l x y\<rbrakk> \<Longrightarrow> ufa_invar l'
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; y < length l; l' = ufa_union l x y\<rbrakk> \<Longrightarrow> ufa_invar l'
[PROOF STEP]
@qed


[STATEMENT]
lemma ufa_union_aux [rewrite]:
  "ufa_invar l \<Longrightarrow> x < length l \<Longrightarrow> y < length l \<Longrightarrow> l' = ufa_union l x y \<Longrightarrow>
   i < length l' \<Longrightarrow> rep_of l' i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; y < length l; l' = ufa_union l x y; i < length l'\<rbrakk> \<Longrightarrow> rep_of l' i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; y < length l; l' = ufa_union l x y; i < length l'\<rbrakk> \<Longrightarrow> rep_of l' i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
@prop_induct "ufa_invar l \<and> i < length l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; y < length l; l' = ufa_union l x y; i < length l'\<rbrakk> \<Longrightarrow> rep_of l' i = (if rep_of l i = rep_of l x then rep_of l y else rep_of l i)
[PROOF STEP]
@qed


[STATEMENT]
theorem ufa_union_correct [rewrite]:
  "ufa_invar l \<Longrightarrow> x < length l \<Longrightarrow> y < length l \<Longrightarrow> l' = ufa_union l x y \<Longrightarrow>
   ufa_\<alpha> l' = per_union (ufa_\<alpha> l) x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; y < length l; l' = ufa_union l x y\<rbrakk> \<Longrightarrow> ufa_\<alpha> l' = per_union (ufa_\<alpha> l) x y
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; y < length l; l' = ufa_union l x y\<rbrakk> \<Longrightarrow> ufa_\<alpha> l' = per_union (ufa_\<alpha> l) x y
[PROOF STEP]
@have "\<forall>a b. (a,b) \<in> ufa_\<alpha> l' \<longleftrightarrow> (a,b) \<in> per_union (ufa_\<alpha> l) x y" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; y < length l; l' = ufa_union l x y\<rbrakk> \<Longrightarrow> ufa_\<alpha> l' = per_union (ufa_\<alpha> l) x y
[PROOF STEP]
@case "(a,b) \<in> ufa_\<alpha> l'" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; y < length l; l' = ufa_union l x y\<rbrakk> \<Longrightarrow> ufa_\<alpha> l' = per_union (ufa_\<alpha> l) x y
[PROOF STEP]
@case "rep_of l a = rep_of l x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; y < length l; l' = ufa_union l x y\<rbrakk> \<Longrightarrow> ufa_\<alpha> l' = per_union (ufa_\<alpha> l) x y
[PROOF STEP]
@case "rep_of l a = rep_of l y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; y < length l; l' = ufa_union l x y\<rbrakk> \<Longrightarrow> ufa_\<alpha> l' = per_union (ufa_\<alpha> l) x y
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; y < length l; l' = ufa_union l x y\<rbrakk> \<Longrightarrow> ufa_\<alpha> l' = per_union (ufa_\<alpha> l) x y
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; y < length l; l' = ufa_union l x y\<rbrakk> \<Longrightarrow> ufa_\<alpha> l' = per_union (ufa_\<alpha> l) x y
[PROOF STEP]
@qed


[STATEMENT]
lemma ufa_compress_invar [forward_arg]:
  "ufa_invar l \<Longrightarrow> x < length l \<Longrightarrow> l' = ufa_compress l x \<Longrightarrow> ufa_invar l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; l' = ufa_compress l x\<rbrakk> \<Longrightarrow> ufa_invar l'
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; l' = ufa_compress l x\<rbrakk> \<Longrightarrow> ufa_invar l'
[PROOF STEP]
@have "\<forall>i<length l'. rep_of_dom (l', i) \<and> l' ! i < length l'" @with
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; l' = ufa_compress l x\<rbrakk> \<Longrightarrow> ufa_invar l'
[PROOF STEP]
@prop_induct "ufa_invar l \<and> i < length l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; l' = ufa_compress l x\<rbrakk> \<Longrightarrow> ufa_invar l'
[PROOF STEP]
@end
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; l' = ufa_compress l x\<rbrakk> \<Longrightarrow> ufa_invar l'
[PROOF STEP]
@qed


[STATEMENT]
lemma ufa_compress_aux [rewrite]:
  "ufa_invar l \<Longrightarrow> x < length l \<Longrightarrow> l' = ufa_compress l x \<Longrightarrow> i < length l' \<Longrightarrow>
   rep_of l' i = rep_of l i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; l' = ufa_compress l x; i < length l'\<rbrakk> \<Longrightarrow> rep_of l' i = rep_of l i
[PROOF STEP]
@proof
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; l' = ufa_compress l x; i < length l'\<rbrakk> \<Longrightarrow> rep_of l' i = rep_of l i
[PROOF STEP]
@prop_induct "ufa_invar l \<and> i < length l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l; l' = ufa_compress l x; i < length l'\<rbrakk> \<Longrightarrow> rep_of l' i = rep_of l i
[PROOF STEP]
@qed


[STATEMENT]
theorem ufa_compress_correct [rewrite]:
  "ufa_invar l \<Longrightarrow> x < length l \<Longrightarrow> ufa_\<alpha> (ufa_compress l x) = ufa_\<alpha> l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ufa_invar l; x < length l\<rbrakk> \<Longrightarrow> ufa_\<alpha> (ufa_compress l x) = ufa_\<alpha> l
[PROOF STEP]
by auto2


[STATEMENT]
lemma ball_single [rewrite]: "(\<forall>x\<in>{x}. P x) = P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>{x}. P x) = P x
[PROOF STEP]
by auto


[STATEMENT]
lemma set_membership_distinct [forward]: "x \<in> s \<Longrightarrow> y \<notin> s \<Longrightarrow> x \<noteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> s; y \<notin> s\<rbrakk> \<Longrightarrow> x \<noteq> y
[PROOF STEP]
by auto


[STATEMENT]
lemma non_empty_exist_elt [backward]: "U \<noteq> {} \<Longrightarrow> \<exists>x. x \<in> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U \<noteq> {} \<Longrightarrow> \<exists>x. x \<in> U
[PROOF STEP]
by blast


[STATEMENT]
lemma non_univ_exist_compl [backward]: "U \<noteq> UNIV \<Longrightarrow> \<exists>x. x \<notin> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U \<noteq> UNIV \<Longrightarrow> \<exists>x. x \<notin> U
[PROOF STEP]
by blast


[STATEMENT]
lemma set_ext [forward]: "\<forall>a. a \<in> S \<longleftrightarrow> a \<in> T \<Longrightarrow> S = T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a. (a \<in> S) = (a \<in> T) \<Longrightarrow> S = T
[PROOF STEP]
by auto


[STATEMENT]
lemma set_pair_ext [forward]: "\<forall>a b. (a, b) \<in> S \<longleftrightarrow> (a, b) \<in> T \<Longrightarrow> S = T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a b. ((a, b) \<in> S) = ((a, b) \<in> T) \<Longrightarrow> S = T
[PROOF STEP]
by auto


[STATEMENT]
lemma UnD1 [forward]: "c \<in> A \<union> B \<Longrightarrow> c \<notin> A \<Longrightarrow> c \<in> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> A \<union> B; c \<notin> A\<rbrakk> \<Longrightarrow> c \<in> B
[PROOF STEP]
by auto


[STATEMENT]
lemma UnD2 [forward]: "c \<in> A \<union> B \<Longrightarrow> c \<notin> B \<Longrightarrow> c \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> A \<union> B; c \<notin> B\<rbrakk> \<Longrightarrow> c \<in> A
[PROOF STEP]
by auto


[STATEMENT]
lemma UnD1_single [forward]: "c \<in> {a} \<union> B \<Longrightarrow> c \<noteq> a \<Longrightarrow> c \<in> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> {a} \<union> B; c \<noteq> a\<rbrakk> \<Longrightarrow> c \<in> B
[PROOF STEP]
by auto


[STATEMENT]
lemma UnD2_single [forward]: "c \<in> A \<union> {b} \<Longrightarrow> c \<noteq> b \<Longrightarrow> c \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c \<in> A \<union> {b}; c \<noteq> b\<rbrakk> \<Longrightarrow> c \<in> A
[PROOF STEP]
by auto


[STATEMENT]
lemma UnI1_single: "a \<in> {a} \<union> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> {a} \<union> B
[PROOF STEP]
by auto


[STATEMENT]
lemma UnI2_single: "b \<in> A \<union> {b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<in> A \<union> {b}
[PROOF STEP]
by auto


[STATEMENT]
lemma union_single_eq [rewrite, backward]: "x \<in> p \<Longrightarrow> {x} \<union> p = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> p \<Longrightarrow> {x} \<union> p = p
[PROOF STEP]
by auto


[STATEMENT]
lemma set_disjoint_mp [forward, backward2]: "A \<inter> B = {} \<Longrightarrow> p \<in> A \<Longrightarrow> p \<notin> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<inter> B = {}; p \<in> A\<rbrakk> \<Longrightarrow> p \<notin> B
[PROOF STEP]
by auto


[STATEMENT]
lemma set_disjoint_single [rewrite]: "{x} \<inter> B = {} \<longleftrightarrow> x \<notin> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({x} \<inter> B = {}) = (x \<notin> B)
[PROOF STEP]
by simp


[STATEMENT]
lemma subset_single [rewrite]: "{a} \<subseteq> B \<longleftrightarrow> a \<in> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({a} \<subseteq> B) = (a \<in> B)
[PROOF STEP]
by simp


[STATEMENT]
lemma union_is_subset [forward]: "A \<union> B \<subseteq> C \<Longrightarrow> A \<subseteq> C \<and> B \<subseteq> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<union> B \<subseteq> C \<Longrightarrow> A \<subseteq> C \<and> B \<subseteq> C
[PROOF STEP]
by simp


[STATEMENT]
lemma subset_union_same1 [backward]: "B \<subseteq> C \<Longrightarrow> A \<union> B \<subseteq> A \<union> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<subseteq> C \<Longrightarrow> A \<union> B \<subseteq> A \<union> C
[PROOF STEP]
by auto


[STATEMENT]
lemma subset_union_same2 [backward]: "A \<subseteq> B \<Longrightarrow> A \<union> C \<subseteq> B \<union> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> B \<Longrightarrow> A \<union> C \<subseteq> B \<union> C
[PROOF STEP]
by auto


[STATEMENT]
lemma mem_diff [rewrite]: "x \<in> A - B \<longleftrightarrow> x \<in> A \<and> x \<notin> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in> A - B) = (x \<in> A \<and> x \<notin> B)
[PROOF STEP]
by simp


[STATEMENT]
lemma set_union_minus_same1 [rewrite]: "(A \<union> B) - B = A - B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<union> B - B = A - B
[PROOF STEP]
by auto


[STATEMENT]
lemma set_union_minus_same2 [rewrite]: "(B \<union> A) - B = A - B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<union> A - B = A - B
[PROOF STEP]
by auto


[STATEMENT]
lemma set_union_minus_distinct [rewrite]: "a \<noteq> c \<Longrightarrow> {a} \<union> (B - {c}) = {a} \<union> B - {c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<noteq> c \<Longrightarrow> {a} \<union> (B - {c}) = {a} \<union> B - {c}
[PROOF STEP]
by auto


[STATEMENT]
lemma union_subtract_elt1 [rewrite]: "x \<notin> B \<Longrightarrow> ({x} \<union> B) - {x} = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> B \<Longrightarrow> {x} \<union> B - {x} = B
[PROOF STEP]
by simp


[STATEMENT]
lemma union_subtract_elt2 [rewrite]: "x \<notin> B \<Longrightarrow> (B \<union> {x}) - {x} = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> B \<Longrightarrow> B \<union> {x} - {x} = B
[PROOF STEP]
by simp


[STATEMENT]
lemma subset_sub1 [backward]: "x \<in> A \<Longrightarrow> A - {x} \<subset> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> A \<Longrightarrow> A - {x} \<subset> A
[PROOF STEP]
by auto


[STATEMENT]
lemma member_notin [forward]: "x \<in> S - {y} \<Longrightarrow> x \<noteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> S - {y} \<Longrightarrow> x \<noteq> y
[PROOF STEP]
by simp


[STATEMENT]
lemma member_notin_contra: "x \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> x \<in> S - {y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> S; x \<noteq> y\<rbrakk> \<Longrightarrow> x \<in> S - {y}
[PROOF STEP]
by simp


[STATEMENT]
lemma set_finite_single [resolve]: "finite {x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {x}
[PROOF STEP]
by simp


[STATEMENT]
lemma Max_ge' [forward]: "finite A \<Longrightarrow> x > Max A \<Longrightarrow> \<not>(x \<in> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; Max A < x\<rbrakk> \<Longrightarrow> x \<notin> A
[PROOF STEP]
using Max_ge leD
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; ?x \<in> ?A\<rbrakk> \<Longrightarrow> ?x \<le> Max ?A
?y \<le> ?x \<Longrightarrow> \<not> ?x < ?y

goal (1 subgoal):
 1. \<lbrakk>finite A; Max A < x\<rbrakk> \<Longrightarrow> x \<notin> A
[PROOF STEP]
by auto


[STATEMENT]
lemma card_emptyD [rewrite]: "finite S \<Longrightarrow> card S = 0 \<Longrightarrow> S = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite S; card S = 0\<rbrakk> \<Longrightarrow> S = {}
[PROOF STEP]
by simp


[STATEMENT]
lemma card_minus1 [rewrite]: "x \<in> S \<Longrightarrow> card (S - {x}) = card S - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> S \<Longrightarrow> card (S - {x}) = card S - 1
[PROOF STEP]
by (simp add: card_Diff_subset)


[STATEMENT]
lemma mset_member_empty [resolve]: "\<not>p \<in># {#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<notin># {#}
[PROOF STEP]
by simp


[STATEMENT]
lemma mem_multiset_single [rewrite]: "x \<in># {#y#} \<longleftrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<in># {#y#}) = (x = y)
[PROOF STEP]
by simp


[STATEMENT]
lemma multi_contain_add_self1 [resolve]: "A \<subset># {#x#} + A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subset># {#x#} + A
[PROOF STEP]
by simp


[STATEMENT]
lemma multi_contain_add_self2 [resolve]: "A \<subset># A + {#x#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subset># A + {#x#}
[PROOF STEP]
by simp


[STATEMENT]
lemma multi_member_this2: "x \<in># XS + {#x#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in># XS + {#x#}
[PROOF STEP]
by simp


[STATEMENT]
lemma multi_nonempty_split' [resolve]: "M \<noteq> {#} \<Longrightarrow> \<exists>M' m. M = M' + {#m#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M \<noteq> {#} \<Longrightarrow> \<exists>M' m. M = M' + {#m#}
[PROOF STEP]
using multi_nonempty_split
[PROOF STATE]
proof (prove)
using this:
?M \<noteq> {#} \<Longrightarrow> \<exists>A a. ?M = add_mset a A

goal (1 subgoal):
 1. M \<noteq> {#} \<Longrightarrow> \<exists>M' m. M = M' + {#m#}
[PROOF STEP]
by auto


[STATEMENT]
lemma multi_member_split' [backward]: "x \<in># M \<Longrightarrow> \<exists>M'. M = M' + {#x#}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in># M \<Longrightarrow> \<exists>M'. M = M' + {#x#}
[PROOF STEP]
by (metis insert_DiffM2)


[STATEMENT]
lemma assumes wf:"wwf_prog P" and casts:"P \<turnstile> T casts v to v'"
  and typeof:"P \<turnstile> typeof\<^bsub>h\<^esub> v = Some T'" and leq:"P \<turnstile> T' \<le> T"
  shows casts_conf:"P,h \<turnstile> v' :\<le> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,h \<turnstile> v' :\<le> T
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P,h \<turnstile> v' :\<le> T
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P,h \<turnstile> v' :\<le> T
[PROOF STEP]
fix a' C Cs S'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P,h \<turnstile> v' :\<le> T
[PROOF STEP]
assume leq:"P \<turnstile> Class (last Cs) \<le> T" and subo:"Subobjs P C Cs"
      and casts':"P \<turnstile> T casts Ref (a',Cs) to v'" and h:"h a' = Some(C,S')"
[PROOF STATE]
proof (state)
this:
P \<turnstile> Class (last Cs) \<le> T
Subobjs P C Cs
P \<turnstile> T casts Ref (a', Cs) to v'
h a' = \<lfloor>(C, S')\<rfloor>

goal (1 subgoal):
 1. P,h \<turnstile> v' :\<le> T
[PROOF STEP]
from subo wf
[PROOF STATE]
proof (chain)
picking this:
Subobjs P C Cs
wwf_prog P
[PROOF STEP]
have "is_class P (last Cs)"
[PROOF STATE]
proof (prove)
using this:
Subobjs P C Cs
wwf_prog P

goal (1 subgoal):
 1. is_class P (last Cs)
[PROOF STEP]
by(fastforce intro:Subobj_last_isClass)
[PROOF STATE]
proof (state)
this:
is_class P (last Cs)

goal (1 subgoal):
 1. P,h \<turnstile> v' :\<le> T
[PROOF STEP]
with leq wf
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> Class (last Cs) \<le> T
wwf_prog P
is_class P (last Cs)
[PROOF STEP]
obtain C' where T:"T = Class C'"
      and path_unique:"P \<turnstile> Path (last Cs) to C' unique"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> Class (last Cs) \<le> T
wwf_prog P
is_class P (last Cs)

goal (1 subgoal):
 1. (\<And>C'. \<lbrakk>T = Class C'; P \<turnstile> Path last Cs to C' unique\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto dest:Class_widen)
[PROOF STATE]
proof (state)
this:
T = Class C'
P \<turnstile> Path last Cs to C' unique

goal (1 subgoal):
 1. P,h \<turnstile> v' :\<le> T
[PROOF STEP]
from path_unique
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> Path last Cs to C' unique
[PROOF STEP]
obtain Cs' where path_via:"P \<turnstile> Path (last Cs) to C' via Cs'"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> Path last Cs to C' unique

goal (1 subgoal):
 1. (\<And>Cs'. P \<turnstile> Path last Cs to C' via Cs'  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp:path_via_def path_unique_def)
[PROOF STATE]
proof (state)
this:
P \<turnstile> Path last Cs to C' via Cs'

goal (1 subgoal):
 1. P,h \<turnstile> v' :\<le> T
[PROOF STEP]
with T path_unique casts'
[PROOF STATE]
proof (chain)
picking this:
T = Class C'
P \<turnstile> Path last Cs to C' unique
P \<turnstile> T casts Ref (a', Cs) to v'
P \<turnstile> Path last Cs to C' via Cs'
[PROOF STEP]
have v':"v' = Ref (a',Cs@\<^sub>pCs')"
[PROOF STATE]
proof (prove)
using this:
T = Class C'
P \<turnstile> Path last Cs to C' unique
P \<turnstile> T casts Ref (a', Cs) to v'
P \<turnstile> Path last Cs to C' via Cs'

goal (1 subgoal):
 1. v' = Ref (a', Cs @\<^sub>p Cs')
[PROOF STEP]
by -(erule casts_to.cases,auto simp:path_unique_def path_via_def)
[PROOF STATE]
proof (state)
this:
v' = Ref (a', Cs @\<^sub>p Cs')

goal (1 subgoal):
 1. P,h \<turnstile> v' :\<le> T
[PROOF STEP]
from subo path_via wf
[PROOF STATE]
proof (chain)
picking this:
Subobjs P C Cs
P \<turnstile> Path last Cs to C' via Cs'
wwf_prog P
[PROOF STEP]
have "Subobjs P C (Cs@\<^sub>pCs')"
      and "last (Cs@\<^sub>pCs') = C'"
[PROOF STATE]
proof (prove)
using this:
Subobjs P C Cs
P \<turnstile> Path last Cs to C' via Cs'
wwf_prog P

goal (1 subgoal):
 1. Subobjs P C (Cs @\<^sub>p Cs') &&& last (Cs @\<^sub>p Cs') = C'
[PROOF STEP]
apply(auto intro:Subobjs_appendPath simp:path_via_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Subobjs P C Cs; wwf_prog P; Subobjs P (last Cs) Cs'; C' = last Cs'\<rbrakk> \<Longrightarrow> last (Cs @\<^sub>p Cs') = last Cs'
[PROOF STEP]
apply(drule_tac Cs="Cs'" in Subobjs_nonempty)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Subobjs P C Cs; wwf_prog P; C' = last Cs'; Cs' \<noteq> []\<rbrakk> \<Longrightarrow> last (Cs @\<^sub>p Cs') = last Cs'
[PROOF STEP]
by(rule sym[OF appendPath_last])
[PROOF STATE]
proof (state)
this:
Subobjs P C (Cs @\<^sub>p Cs')
last (Cs @\<^sub>p Cs') = C'

goal (1 subgoal):
 1. P,h \<turnstile> v' :\<le> T
[PROOF STEP]
with T h v'
[PROOF STATE]
proof (chain)
picking this:
T = Class C'
h a' = \<lfloor>(C, S')\<rfloor>
v' = Ref (a', Cs @\<^sub>p Cs')
Subobjs P C (Cs @\<^sub>p Cs')
last (Cs @\<^sub>p Cs') = C'
[PROOF STEP]
have ?thesis
[PROOF STATE]
proof (prove)
using this:
T = Class C'
h a' = \<lfloor>(C, S')\<rfloor>
v' = Ref (a', Cs @\<^sub>p Cs')
Subobjs P C (Cs @\<^sub>p Cs')
last (Cs @\<^sub>p Cs') = C'

goal (1 subgoal):
 1. P,h \<turnstile> v' :\<le> T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P,h \<turnstile> v' :\<le> T

goal (1 subgoal):
 1. P,h \<turnstile> v' :\<le> T
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>P \<turnstile> Class (last ?Cs2) \<le> T; Subobjs P ?C2 ?Cs2; P \<turnstile> T casts Ref (?a'2, ?Cs2) to v' ; h ?a'2 = \<lfloor>(?C2, ?S'2)\<rfloor>\<rbrakk> \<Longrightarrow> P,h \<turnstile> v' :\<le> T

goal (1 subgoal):
 1. P,h \<turnstile> v' :\<le> T
[PROOF STEP]
with casts typeof wf typeof leq
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> T casts v to v'
P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T'\<rfloor>
wwf_prog P
P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T'\<rfloor>
P \<turnstile> T' \<le> T
\<lbrakk>P \<turnstile> Class (last ?Cs2) \<le> T; Subobjs P ?C2 ?Cs2; P \<turnstile> T casts Ref (?a'2, ?Cs2) to v' ; h ?a'2 = \<lfloor>(?C2, ?S'2)\<rfloor>\<rbrakk> \<Longrightarrow> P,h \<turnstile> v' :\<le> T
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> T casts v to v'
P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T'\<rfloor>
wwf_prog P
P \<turnstile> typeof\<^bsub>h\<^esub> v = \<lfloor>T'\<rfloor>
P \<turnstile> T' \<le> T
\<lbrakk>P \<turnstile> Class (last ?Cs2) \<le> T; Subobjs P ?C2 ?Cs2; P \<turnstile> T casts Ref (?a'2, ?Cs2) to v' ; h ?a'2 = \<lfloor>(?C2, ?S'2)\<rfloor>\<rbrakk> \<Longrightarrow> P,h \<turnstile> v' :\<le> T

goal (1 subgoal):
 1. P,h \<turnstile> v' :\<le> T
[PROOF STEP]
by(cases v,auto elim:casts_to.cases split:if_split_asm)
[PROOF STATE]
proof (state)
this:
P,h \<turnstile> v' :\<le> T

goal:
No subgoals!
[PROOF STEP]
qed