[STATEMENT]
lemma splitFace_holds_edges_sym:
assumes pre_F: "pre_splitFace g' v a f' ws"
and mgp: "minGraphProps g'"
shows "edges_sym (snd (snd (splitFace g' v a f' ws)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. edges_sym (snd (snd (splitFace g' v a f' ws)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. edges_sym (snd (snd (splitFace g' v a f' ws)))
[PROOF STEP]
define g'' where "g'' = (snd (snd (splitFace g' v a f' ws)))"
[PROOF STATE]
proof (state)
this:
g'' = snd (snd (splitFace g' v a f' ws))

goal (1 subgoal):
 1. edges_sym (snd (snd (splitFace g' v a f' ws)))
[PROOF STEP]
define f21 where "f21 = snd (split_face f' v a ws)"
[PROOF STATE]
proof (state)
this:
f21 = snd (split_face f' v a ws)

goal (1 subgoal):
 1. edges_sym (snd (snd (splitFace g' v a f' ws)))
[PROOF STEP]
define f12 where "f12 = fst (split_face f' v a ws)"
[PROOF STATE]
proof (state)
this:
f12 = fst (split_face f' v a ws)

goal (1 subgoal):
 1. edges_sym (snd (snd (splitFace g' v a f' ws)))
[PROOF STEP]
define vs1 where "vs1 = between (vertices f') v a"
[PROOF STATE]
proof (state)
this:
vs1 = between (vertices f') v a

goal (1 subgoal):
 1. edges_sym (snd (snd (splitFace g' v a f' ws)))
[PROOF STEP]
define vs2 where "vs2 = between (vertices f') a v"
[PROOF STATE]
proof (state)
this:
vs2 = between (vertices f') a v

goal (1 subgoal):
 1. edges_sym (snd (snd (splitFace g' v a f' ws)))
[PROOF STEP]
from f21_def [symmetric] f12_def [symmetric] g''_def
[PROOF STATE]
proof (chain)
picking this:
snd (split_face f' v a ws) = f21
fst (split_face f' v a ws) = f12
g'' = snd (snd (splitFace g' v a f' ws))
[PROOF STEP]
have fdg: "(f12, f21, g'') = splitFace g' v a f' ws"
[PROOF STATE]
proof (prove)
using this:
snd (split_face f' v a ws) = f21
fst (split_face f' v a ws) = f12
g'' = snd (snd (splitFace g' v a f' ws))

goal (1 subgoal):
 1. (f12, f21, g'') = splitFace g' v a f' ws
[PROOF STEP]
by (simp add: splitFace_def split_def)
[PROOF STATE]
proof (state)
this:
(f12, f21, g'') = splitFace g' v a f' ws

goal (1 subgoal):
 1. edges_sym (snd (snd (splitFace g' v a f' ws)))
[PROOF STEP]
from pre_F
[PROOF STATE]
proof (chain)
picking this:
pre_splitFace g' v a f' ws
[PROOF STEP]
have pre_F': "pre_splitFace g' v a f' ws"
[PROOF STATE]
proof (prove)
using this:
pre_splitFace g' v a f' ws

goal (1 subgoal):
 1. pre_splitFace g' v a f' ws
[PROOF STEP]
apply (unfold pre_splitFace_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' \<in> \<F> g' \<and> \<not> final f' \<and> distinct (vertices f') \<and> distinct ws \<and> \<V> g' \<inter> set ws = {} \<and> \<V> f' \<inter> set ws = {} \<and> v \<in> \<V> f' \<and> a \<in> \<V> f' \<and> v \<noteq> a \<and> ((v, a) \<notin> \<E> f' \<and> (a, v) \<notin> \<E> f' \<and> (v, a) \<notin> \<E> g' \<and> (a, v) \<notin> \<E> g' \<or> ws \<noteq> []) \<Longrightarrow> f' \<in> \<F> g' \<and> \<not> final f' \<and> distinct (vertices f') \<and> distinct ws \<and> \<V> g' \<inter> set ws = {} \<and> \<V> f' \<inter> set ws = {} \<and> v \<in> \<V> f' \<and> a \<in> \<V> f' \<and> v \<noteq> a \<and> ((v, a) \<notin> \<E> f' \<and> (a, v) \<notin> \<E> f' \<and> (v, a) \<notin> \<E> g' \<and> (a, v) \<notin> \<E> g' \<or> ws \<noteq> [])
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
pre_splitFace g' v a f' ws

goal (1 subgoal):
 1. edges_sym (snd (snd (splitFace g' v a f' ws)))
[PROOF STEP]
from f21_def f12_def
[PROOF STATE]
proof (chain)
picking this:
f21 = snd (split_face f' v a ws)
f12 = fst (split_face f' v a ws)
[PROOF STEP]
have faces:"faces g'' = (replace f' [f21]  (faces g')) @ [f12]"
[PROOF STATE]
proof (prove)
using this:
f21 = snd (split_face f' v a ws)
f12 = fst (split_face f' v a ws)

goal (1 subgoal):
 1. faces g'' = replace f' [f21] (faces g') @ [f12]
[PROOF STEP]
apply (simp add: g''_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f21 = snd (split_face f' v a ws); f12 = fst (split_face f' v a ws)\<rbrakk> \<Longrightarrow> faces (snd (snd (splitFace g' v a f' ws))) = replace f' [snd (split_face f' v a ws)] (faces g') @ [fst (split_face f' v a ws)]
[PROOF STEP]
by (simp add: splitFace_def split_def)
[PROOF STATE]
proof (state)
this:
faces g'' = replace f' [f21] (faces g') @ [f12]

goal (1 subgoal):
 1. edges_sym (snd (snd (splitFace g' v a f' ws)))
[PROOF STEP]
from f12_def f21_def
[PROOF STATE]
proof (chain)
picking this:
f12 = fst (split_face f' v a ws)
f21 = snd (split_face f' v a ws)
[PROOF STEP]
have split: "(f12, f21) = split_face f' v a ws"
[PROOF STATE]
proof (prove)
using this:
f12 = fst (split_face f' v a ws)
f21 = snd (split_face f' v a ws)

goal (1 subgoal):
 1. (f12, f21) = split_face f' v a ws
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(f12, f21) = split_face f' v a ws

goal (1 subgoal):
 1. edges_sym (snd (snd (splitFace g' v a f' ws)))
[PROOF STEP]
from pre_F mgp  g''_def [symmetric] split
[PROOF STATE]
proof (chain)
picking this:
pre_splitFace g' v a f' ws
minGraphProps g'
snd (snd (splitFace g' v a f' ws)) = g''
(f12, f21) = split_face f' v a ws
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pre_splitFace g' v a f' ws
minGraphProps g'
snd (snd (splitFace g' v a f' ws)) = g''
(f12, f21) = split_face f' v a ws

goal (1 subgoal):
 1. edges_sym (snd (snd (splitFace g' v a f' ws)))
[PROOF STEP]
apply (simp add: edges_sym_def edges_graph_def f21_def [symmetric] f12_def [symmetric]
    vs1_def [symmetric] vs2_def [symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws\<rbrakk> \<Longrightarrow> \<forall>a b. (\<exists>x\<in>\<F> g''. (a, b) \<in> \<E> x) \<longrightarrow> (\<exists>x\<in>\<F> g''. (b, a) \<in> \<E> x)
[PROOF STEP]
apply (intro allI impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; \<exists>x\<in>\<F> g''. (aa, b) \<in> \<E> x\<rbrakk> \<Longrightarrow> \<exists>x\<in>\<F> g''. (b, aa) \<in> \<E> x
[PROOF STEP]
apply (elim bexE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g''; (aa, b) \<in> \<E> x\<rbrakk> \<Longrightarrow> \<exists>x\<in>\<F> g''. (b, aa) \<in> \<E> x
[PROOF STEP]
apply (simp add: faces)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (case_tac "x = f12 \<or> x = f21")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (subgoal_tac "(aa,b) \<in> edges f'  \<or> ((b,aa) \<in> (edges f12 \<union> edges f21) \<and> (aa,b) \<in> (edges f12 \<union> edges f21))")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (case_tac "(aa, b) \<in> edges f'")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (subgoal_tac "(b,aa) \<in> edges g'")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<in> \<E> f'; (b, aa) \<in> \<E> g'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (simp add: edges_graph_def)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'; \<exists>x\<in>\<F> g'. (b, aa) \<in> \<E> x\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (elim bexE)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (rule disjI2)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa\<rbrakk> \<Longrightarrow> \<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (rule bexI)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> (?x22 aa b x xa)
 2. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa\<rbrakk> \<Longrightarrow> ?x22 aa b x xa \<in> set (replace f' [f21] (faces g'))
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 6. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa\<rbrakk> \<Longrightarrow> xa \<in> set (replace f' [f21] (faces g'))
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (subgoal_tac "xa \<noteq> f'")
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> xa \<in> set (replace f' [f21] (faces g'))
 2. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa\<rbrakk> \<Longrightarrow> xa \<noteq> f'
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 6. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (rule replace4)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> xa \<in> \<F> g'
 2. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> f' \<noteq> xa
 3. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa\<rbrakk> \<Longrightarrow> xa \<noteq> f'
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 6. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 7. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> f' \<noteq> xa
 2. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa\<rbrakk> \<Longrightarrow> xa \<noteq> f'
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 6. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa\<rbrakk> \<Longrightarrow> xa \<noteq> f'
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (drule minGraphProps12)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa\<rbrakk> \<Longrightarrow> ?f38 aa b x xa \<in> \<F> g'
 2. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa\<rbrakk> \<Longrightarrow> (?a38 aa b x xa, ?b38 aa b x xa) \<in> \<E> (?f38 aa b x xa)
 3. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; (?b38 aa b x xa, ?a38 aa b x xa) \<notin> \<E> (?f38 aa b x xa)\<rbrakk> \<Longrightarrow> xa \<noteq> f'
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 6. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 7. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa\<rbrakk> \<Longrightarrow> (?a38 aa b x xa, ?b38 aa b x xa) \<in> \<E> xa
 2. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; (?b38 aa b x xa, ?a38 aa b x xa) \<notin> \<E> xa\<rbrakk> \<Longrightarrow> xa \<noteq> f'
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 6. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; (aa, b) \<notin> \<E> xa\<rbrakk> \<Longrightarrow> xa \<noteq> f'
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (rule ccontr)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; (aa, b) \<notin> \<E> xa; \<not> xa \<noteq> f'\<rbrakk> \<Longrightarrow> False
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (rule minGraphProps10)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> minGraphProps g'
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> g'
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> g'
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (simp add: edges_graph_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> \<exists>x\<in>\<F> g'. (aa, b) \<in> \<E> x
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (rule bexI)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> (?x47 aa b x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> ?x47 aa b x \<in> \<F> g'
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (thin_tac "(aa, b) \<in> edges x")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> (?x47 aa b x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> ?x47 aa b x \<in> \<F> g'
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f'\<rbrakk> \<Longrightarrow> f' \<in> \<F> g'
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (case_tac "(b, aa) \<in> edges f12")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'; (b, aa) \<in> \<E> f12\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'; (b, aa) \<notin> \<E> f12\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'; (b, aa) \<notin> \<E> f12\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (b, aa) \<in> \<E> f21 \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'; (b, aa) \<notin> \<E> f12\<rbrakk> \<Longrightarrow> \<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (case_tac "(b, aa) \<in> edges f21")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (b, aa) \<in> \<E> f21 \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'; (b, aa) \<notin> \<E> f12; (b, aa) \<in> \<E> f21\<rbrakk> \<Longrightarrow> \<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (b, aa) \<in> \<E> f21 \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'; (b, aa) \<notin> \<E> f12; (b, aa) \<notin> \<E> f21\<rbrakk> \<Longrightarrow> \<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (rule bexI)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (b, aa) \<in> \<E> f21 \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'; (b, aa) \<notin> \<E> f12; (b, aa) \<in> \<E> f21\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> (?x53 aa b x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (b, aa) \<in> \<E> f21 \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'; (b, aa) \<notin> \<E> f12; (b, aa) \<in> \<E> f21\<rbrakk> \<Longrightarrow> ?x53 aa b x \<in> set (replace f' [f21] (faces g'))
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (b, aa) \<in> \<E> f21 \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'; (b, aa) \<notin> \<E> f12; (b, aa) \<notin> \<E> f21\<rbrakk> \<Longrightarrow> \<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (b, aa) \<in> \<E> f21 \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'; (b, aa) \<notin> \<E> f12; (b, aa) \<in> \<E> f21\<rbrakk> \<Longrightarrow> f21 \<in> set (replace f' [f21] (faces g'))
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (b, aa) \<in> \<E> f21 \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'; (b, aa) \<notin> \<E> f12; (b, aa) \<notin> \<E> f21\<rbrakk> \<Longrightarrow> \<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (rule replace3)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (b, aa) \<in> \<E> f21 \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'; (b, aa) \<notin> \<E> f12; (b, aa) \<in> \<E> f21\<rbrakk> \<Longrightarrow> f' \<in> \<F> g'
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (b, aa) \<in> \<E> f21 \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'; (b, aa) \<notin> \<E> f12; (b, aa) \<in> \<E> f21\<rbrakk> \<Longrightarrow> f21 \<in> set [f21]
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (b, aa) \<in> \<E> f21 \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'; (b, aa) \<notin> \<E> f12; (b, aa) \<notin> \<E> f21\<rbrakk> \<Longrightarrow> \<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (b, aa) \<in> \<E> f21 \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'; (b, aa) \<notin> \<E> f12; (b, aa) \<in> \<E> f21\<rbrakk> \<Longrightarrow> f21 \<in> set [f21]
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (b, aa) \<in> \<E> f21 \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'; (b, aa) \<notin> \<E> f12; (b, aa) \<notin> \<E> f21\<rbrakk> \<Longrightarrow> \<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; (b, aa) \<in> \<E> f21 \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21); (aa, b) \<notin> \<E> f'; (b, aa) \<notin> \<E> f12; (b, aa) \<notin> \<E> f21\<rbrakk> \<Longrightarrow> \<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (subgoal_tac "
     ((aa,b) \<in> edges f'  \<or> ((b,aa) \<in> (edges f12 \<union> edges f21) \<and> (aa,b) \<in> (edges f12 \<union> edges f21))) = ((aa,b) \<in> edges f12 \<or> (aa,b) \<in> edges f21)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; ((aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21) = ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21)\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> ((aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21) = ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21)
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> ((aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21) = ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (rule sym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21) = ((aa, b) \<in> \<E> f' \<or> (b, aa) \<in> \<E> f12 \<union> \<E> f21 \<and> (aa, b) \<in> \<E> f12 \<union> \<E> f21)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21) = ((aa, b) \<in> \<E> f' \<or> ((b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21) \<and> ((aa, b) \<in> \<E> f12 \<or> (aa, b) \<in> \<E> f21))
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (rule split_face_edges_f12_f21_sym)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> f' \<in> \<F> (?g150 aa b x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> pre_split_face f' (?ram1.150 aa b x) (?ram2.150 aa b x) (?vs150 aa b x)
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (f12, f21) = split_face f' (?ram1.150 aa b x) (?ram2.150 aa b x) (?vs150 aa b x)
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (erule pre_splitFace_oldF)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> pre_split_face f' (?ram1.150 aa b x) (?ram2.150 aa b x) (?vs150 aa b x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (f12, f21) = split_face f' (?ram1.150 aa b x) (?ram2.150 aa b x) (?vs150 aa b x)
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (subgoal_tac "pre_split_face f' v a ws")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21; pre_split_face f' v a ws\<rbrakk> \<Longrightarrow> pre_split_face f' (?ram1.150 aa b x) (?ram2.150 aa b x) (?vs150 aa b x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> pre_split_face f' v a ws
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (f12, f21) = split_face f' (?ram1.150 aa b x) (?ram2.150 aa b x) (?vs150 aa b x)
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> pre_split_face f' v a ws
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (f12, f21) = split_face f' v a ws
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x = f12 \<or> x = f21\<rbrakk> \<Longrightarrow> (f12, f21) = split_face f' v a ws
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (rule split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x = f12 \<or> x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; \<not> (x = f12 \<or> x = f21)\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
[PROOF STEP]
apply (subgoal_tac "distinct (faces g')")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g')\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply (simp add: replace6)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; (x = f' \<longrightarrow> f' = f21) \<and> x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g')\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply (case_tac "x = f'")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; (x = f' \<longrightarrow> f' = f21) \<and> x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x = f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; (x = f' \<longrightarrow> f' = f21) \<and> x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; (x = f' \<longrightarrow> f' = f21) \<and> x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply (subgoal_tac "(b,aa) \<in> edges g'")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; (b, aa) \<in> \<E> g'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply (simp add: edges_graph_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; \<exists>x\<in>\<F> g'. (b, aa) \<in> \<E> x\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply (elim bexE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply (case_tac "xa = f'")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa = f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; (b, aa) \<in> \<E> f'; xa = f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply (frule split_face_edges_or)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; (b, aa) \<in> \<E> f'; xa = f'\<rbrakk> \<Longrightarrow> pre_split_face f' v a ws
 2. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; (b, aa) \<in> \<E> f'; xa = f'\<rbrakk> \<Longrightarrow> (?a161 aa b x xa, ?b161 aa b x xa) \<in> \<E> f'
 3. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; (b, aa) \<in> \<E> f'; xa = f'; (?a161 aa b x xa, ?b161 aa b x xa) \<in> \<E> f12 \<or> (?a161 aa b x xa, ?b161 aa b x xa) \<in> \<E> f21\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 4. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 6. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; (b, aa) \<in> \<E> f'; xa = f'\<rbrakk> \<Longrightarrow> (?a161 aa b x xa, ?b161 aa b x xa) \<in> \<E> f'
 2. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; (b, aa) \<in> \<E> f'; xa = f'; (?a161 aa b x xa, ?b161 aa b x xa) \<in> \<E> f12 \<or> (?a161 aa b x xa, ?b161 aa b x xa) \<in> \<E> f21\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 3. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; (b, aa) \<in> \<E> f'; xa = f'; (b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply (case_tac "(b, aa) \<in> edges f12")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; (b, aa) \<in> \<E> f'; xa = f'; (b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21; (b, aa) \<in> \<E> f12\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; (b, aa) \<in> \<E> f'; xa = f'; (b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21; (b, aa) \<notin> \<E> f12\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 3. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; (b, aa) \<in> \<E> f'; xa = f'; (b, aa) \<in> \<E> f12 \<or> (b, aa) \<in> \<E> f21; (b, aa) \<notin> \<E> f12\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; (b, aa) \<in> \<E> f'; xa = f'; (b, aa) \<in> \<E> f21; (b, aa) \<notin> \<E> f12\<rbrakk> \<Longrightarrow> \<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x
 2. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply (rule bexI)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; (b, aa) \<in> \<E> f'; xa = f'; (b, aa) \<in> \<E> f21; (b, aa) \<notin> \<E> f12\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> (?x166 aa b x xa)
 2. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; (b, aa) \<in> \<E> f'; xa = f'; (b, aa) \<in> \<E> f21; (b, aa) \<notin> \<E> f12\<rbrakk> \<Longrightarrow> ?x166 aa b x xa \<in> set (replace f' [f21] (faces g'))
 3. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply (thin_tac "(b, aa) \<in> edges f'")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa = f'; (b, aa) \<in> \<E> f21; (b, aa) \<notin> \<E> f12\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> (?x166 aa b x xa)
 2. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; (b, aa) \<in> \<E> f'; xa = f'; (b, aa) \<in> \<E> f21; (b, aa) \<notin> \<E> f12\<rbrakk> \<Longrightarrow> ?x166 aa b x xa \<in> set (replace f' [f21] (faces g'))
 3. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; (b, aa) \<in> \<E> f'; xa = f'; (b, aa) \<in> \<E> f21; (b, aa) \<notin> \<E> f12\<rbrakk> \<Longrightarrow> f21 \<in> set (replace f' [f21] (faces g'))
 2. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply (rule replace3)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; (b, aa) \<in> \<E> f'; xa = f'; (b, aa) \<in> \<E> f21; (b, aa) \<notin> \<E> f12\<rbrakk> \<Longrightarrow> f' \<in> \<F> g'
 2. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; (b, aa) \<in> \<E> f'; xa = f'; (b, aa) \<in> \<E> f21; (b, aa) \<notin> \<E> f12\<rbrakk> \<Longrightarrow> f21 \<in> set [f21]
 3. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 5. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; (b, aa) \<in> \<E> f'; xa = f'; (b, aa) \<in> \<E> f21; (b, aa) \<notin> \<E> f12\<rbrakk> \<Longrightarrow> f21 \<in> set [f21]
 2. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> f12 \<or> (\<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply (rule disjI2)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> \<exists>x\<in>set (replace f' [f21] (faces g')). (b, aa) \<in> \<E> x
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply (rule bexI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> (?x175 aa b x xa)
 2. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> ?x175 aa b x xa \<in> set (replace f' [f21] (faces g'))
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> xa \<in> set (replace f' [f21] (faces g'))
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply (rule replace4)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> xa \<in> \<F> g'
 2. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> f' \<noteq> xa
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 4. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b x xa. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'; xa \<in> \<F> g'; (b, aa) \<in> \<E> xa; xa \<noteq> f'\<rbrakk> \<Longrightarrow> f' \<noteq> xa
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (b, aa) \<in> \<E> g'
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply (rule minGraphProps10)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> minGraphProps g'
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> g'
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> g'
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply (simp add: edges_graph_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> \<exists>x\<in>\<F> g'. (aa, b) \<in> \<E> x
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply (rule bexI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> (aa, b) \<in> \<E> (?x194 aa b x)
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> ?x194 aa b x \<in> \<F> g'
 3. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> \<F> g'; (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21; distinct (faces g'); x \<noteq> f'\<rbrakk> \<Longrightarrow> x \<in> \<F> g'
 2. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> distinct (faces g')
[PROOF STEP]
apply (rule minGraphProps11')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa b x. \<lbrakk>pre_splitFace g' v a f' ws; minGraphProps g'; snd (snd (splitFace g' v a f' ws)) = g''; (f12, f21) = split_face f' v a ws; x \<in> set (replace f' [f21] (faces g')); (aa, b) \<in> \<E> x; x \<noteq> f12 \<and> x \<noteq> f21\<rbrakk> \<Longrightarrow> minGraphProps g'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
edges_sym (snd (snd (splitFace g' v a f' ws)))

goal:
No subgoals!
[PROOF STEP]
qed