[STATEMENT]
lemma sep_conv:
assumes mgp: "minGraphProps g" and "V \<subseteq> \<V> g"
shows "separated g V = (\<forall>u\<in>V.\<forall>v\<in>V. u \<noteq> v \<longrightarrow> \<not> close g u v)" (is "?P = ?Q")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. separated g V = (\<forall>u\<in>V. \<forall>v\<in>V. u \<noteq> v \<longrightarrow> \<not> close g u v)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. separated g V \<Longrightarrow> \<forall>u\<in>V. \<forall>v\<in>V. u \<noteq> v \<longrightarrow> \<not> close g u v
 2. \<forall>u\<in>V. \<forall>v\<in>V. u \<noteq> v \<longrightarrow> \<not> close g u v \<Longrightarrow> separated g V
[PROOF STEP]
assume sep: ?P
[PROOF STATE]
proof (state)
this:
separated g V

goal (2 subgoals):
 1. separated g V \<Longrightarrow> \<forall>u\<in>V. \<forall>v\<in>V. u \<noteq> v \<longrightarrow> \<not> close g u v
 2. \<forall>u\<in>V. \<forall>v\<in>V. u \<noteq> v \<longrightarrow> \<not> close g u v \<Longrightarrow> separated g V
[PROOF STEP]
show ?Q
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>u\<in>V. \<forall>v\<in>V. u \<noteq> v \<longrightarrow> \<not> close g u v
[PROOF STEP]
proof(clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> V; v \<in> V; u \<noteq> v; close g u v\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix u v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> V; v \<in> V; u \<noteq> v; close g u v\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume uv: "u \<in> V" "v \<in> V" "u \<noteq> v" and cl: "close g u v"
[PROOF STATE]
proof (state)
this:
u \<in> V
v \<in> V
u \<noteq> v
close g u v

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> V; v \<in> V; u \<noteq> v; close g u v\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from cl
[PROOF STATE]
proof (chain)
picking this:
close g u v
[PROOF STEP]
obtain f where f: "f \<in> set(facesAt g u)" and
      "if": "if |vertices f| = 4 then (v = f \<bullet> u) \<or> (v = f \<bullet> (f \<bullet> u))
                               else (v = f \<bullet> u)"
[PROOF STATE]
proof (prove)
using this:
close g u v

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in> set (facesAt g u); if |vertices f| = 4 then v = f \<bullet> u \<or> v = f \<bullet> (f \<bullet> u) else v = f \<bullet> u\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (unfold close_def) blast
[PROOF STATE]
proof (state)
this:
f \<in> set (facesAt g u)
if |vertices f| = 4 then v = f \<bullet> u \<or> v = f \<bullet> (f \<bullet> u) else v = f \<bullet> u

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> V; v \<in> V; u \<noteq> v; close g u v\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "u : \<V> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> \<V> g
[PROOF STEP]
using \<open>u : V\<close> \<open>V \<subseteq> \<V> g\<close>
[PROOF STATE]
proof (prove)
using this:
u \<in> V
V \<subseteq> \<V> g

goal (1 subgoal):
 1. u \<in> \<V> g
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u \<in> \<V> g

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> V; v \<in> V; u \<noteq> v; close g u v\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
note uf = minGraphProps6[OF mgp \<open>u : \<V> g\<close> f]
[PROOF STATE]
proof (state)
this:
u \<in> \<V> f

goal (1 subgoal):
 1. \<And>u v. \<lbrakk>u \<in> V; v \<in> V; u \<noteq> v; close g u v\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
assume 4: "|vertices f| = 4"
[PROOF STATE]
proof (state)
this:
|vertices f| = 4

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
hence "v = f \<bullet> u \<or> v = f \<bullet> (f \<bullet> u)"
[PROOF STATE]
proof (prove)
using this:
|vertices f| = 4

goal (1 subgoal):
 1. v = f \<bullet> u \<or> v = f \<bullet> (f \<bullet> u)
[PROOF STEP]
using "if"
[PROOF STATE]
proof (prove)
using this:
|vertices f| = 4
if |vertices f| = 4 then v = f \<bullet> u \<or> v = f \<bullet> (f \<bullet> u) else v = f \<bullet> u

goal (1 subgoal):
 1. v = f \<bullet> u \<or> v = f \<bullet> (f \<bullet> u)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v = f \<bullet> u \<or> v = f \<bullet> (f \<bullet> u)

goal (2 subgoals):
 1. ?P \<Longrightarrow> False
 2. \<not> ?P \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
v = f \<bullet> u \<or> v = f \<bullet> (f \<bullet> u)

goal (1 subgoal):
 1. False
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v = f \<bullet> u \<Longrightarrow> False
 2. v = f \<bullet> (f \<bullet> u) \<Longrightarrow> False
[PROOF STEP]
assume "v = f \<bullet> u"
[PROOF STATE]
proof (state)
this:
v = f \<bullet> u

goal (2 subgoals):
 1. v = f \<bullet> u \<Longrightarrow> False
 2. v = f \<bullet> (f \<bullet> u) \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
v = f \<bullet> u

goal (1 subgoal):
 1. False
[PROOF STEP]
using sep f uv
[PROOF STATE]
proof (prove)
using this:
v = f \<bullet> u
separated g V
f \<in> set (facesAt g u)
u \<in> V
v \<in> V
u \<noteq> v

goal (1 subgoal):
 1. False
[PROOF STEP]
by(simp add:separated_def separated\<^sub>2_def separated\<^sub>3_def)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. v = f \<bullet> (f \<bullet> u) \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v = f \<bullet> (f \<bullet> u) \<Longrightarrow> False
[PROOF STEP]
assume "v = f \<bullet> (f \<bullet> u)"
[PROOF STATE]
proof (state)
this:
v = f \<bullet> (f \<bullet> u)

goal (1 subgoal):
 1. v = f \<bullet> (f \<bullet> u) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v = f \<bullet> (f \<bullet> u)

goal (1 subgoal):
 1. v = f \<bullet> (f \<bullet> u) \<Longrightarrow> False
[PROOF STEP]
hence "v \<in> \<V> f"
[PROOF STATE]
proof (prove)
using this:
v = f \<bullet> (f \<bullet> u)

goal (1 subgoal):
 1. v \<in> \<V> f
[PROOF STEP]
using \<open>u \<in> \<V> f\<close>
[PROOF STATE]
proof (prove)
using this:
v = f \<bullet> (f \<bullet> u)
u \<in> \<V> f

goal (1 subgoal):
 1. v \<in> \<V> f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v \<in> \<V> f

goal (1 subgoal):
 1. v = f \<bullet> (f \<bullet> u) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v \<in> \<V> f

goal (1 subgoal):
 1. v = f \<bullet> (f \<bullet> u) \<Longrightarrow> False
[PROOF STEP]
have "|vertices f| \<le> 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |vertices f| \<le> 4
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
|vertices f| = 4

goal (1 subgoal):
 1. |vertices f| \<le> 4
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
|vertices f| \<le> 4

goal (1 subgoal):
 1. v = f \<bullet> (f \<bullet> u) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
v = f \<bullet> (f \<bullet> u)
v \<in> \<V> f
|vertices f| \<le> 4
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
v = f \<bullet> (f \<bullet> u)
v \<in> \<V> f
|vertices f| \<le> 4

goal (1 subgoal):
 1. False
[PROOF STEP]
using sep f uv \<open>u \<in> \<V> f\<close>
[PROOF STATE]
proof (prove)
using this:
v = f \<bullet> (f \<bullet> u)
v \<in> \<V> f
|vertices f| \<le> 4
separated g V
f \<in> set (facesAt g u)
u \<in> V
v \<in> V
u \<noteq> v
u \<in> \<V> f

goal (1 subgoal):
 1. False
[PROOF STEP]
apply(unfold separated_def separated\<^sub>2_def separated\<^sub>3_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v = f \<bullet> (f \<bullet> u); v \<in> \<V> f; |vertices f| \<le> 4; (\<forall>v\<in>V. \<forall>f\<in>set (facesAt g v). f \<bullet> v \<notin> V) \<and> (\<forall>v\<in>V. \<forall>f\<in>set (facesAt g v). |vertices f| \<le> 4 \<longrightarrow> \<V> f \<inter> V = {v}); f \<in> set (facesAt g u); u \<in> V; v \<in> V; u \<noteq> v; u \<in> \<V> f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
(* why does blast get stuck? *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v = f \<bullet> (f \<bullet> u); v \<in> \<V> f; |vertices f| \<le> 4; (\<forall>v\<in>V. \<forall>f\<in>set (facesAt g v). f \<bullet> v \<notin> V) \<and> (\<forall>v\<in>V. \<forall>f\<in>set (facesAt g v). |vertices f| \<le> 4 \<longrightarrow> \<V> f \<inter> V = {v}); f \<in> set (facesAt g u); u \<in> V; v \<in> V; u \<noteq> v; u \<in> \<V> f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(subgoal_tac "f \<bullet> (f \<bullet> u) \<in> \<V> f \<inter> V")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>v = f \<bullet> (f \<bullet> u); v \<in> \<V> f; |vertices f| \<le> 4; (\<forall>v\<in>V. \<forall>f\<in>set (facesAt g v). f \<bullet> v \<notin> V) \<and> (\<forall>v\<in>V. \<forall>f\<in>set (facesAt g v). |vertices f| \<le> 4 \<longrightarrow> \<V> f \<inter> V = {v}); f \<in> set (facesAt g u); u \<in> V; v \<in> V; u \<noteq> v; u \<in> \<V> f; f \<bullet> (f \<bullet> u) \<in> \<V> f \<inter> V\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>v = f \<bullet> (f \<bullet> u); v \<in> \<V> f; |vertices f| \<le> 4; (\<forall>v\<in>V. \<forall>f\<in>set (facesAt g v). f \<bullet> v \<notin> V) \<and> (\<forall>v\<in>V. \<forall>f\<in>set (facesAt g v). |vertices f| \<le> 4 \<longrightarrow> \<V> f \<inter> V = {v}); f \<in> set (facesAt g u); u \<in> V; v \<in> V; u \<noteq> v; u \<in> \<V> f\<rbrakk> \<Longrightarrow> f \<bullet> (f \<bullet> u) \<in> \<V> f \<inter> V
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>v = f \<bullet> (f \<bullet> u); v \<in> \<V> f; |vertices f| \<le> 4; (\<forall>v\<in>V. \<forall>f\<in>set (facesAt g v). f \<bullet> v \<notin> V) \<and> (\<forall>v\<in>V. \<forall>f\<in>set (facesAt g v). |vertices f| \<le> 4 \<longrightarrow> \<V> f \<inter> V = {v}); f \<in> set (facesAt g u); u \<in> V; v \<in> V; u \<noteq> v; u \<in> \<V> f\<rbrakk> \<Longrightarrow> f \<bullet> (f \<bullet> u) \<in> \<V> f \<inter> V
 2. \<lbrakk>v = f \<bullet> (f \<bullet> u); v \<in> \<V> f; |vertices f| \<le> 4; (\<forall>v\<in>V. \<forall>f\<in>set (facesAt g v). f \<bullet> v \<notin> V) \<and> (\<forall>v\<in>V. \<forall>f\<in>set (facesAt g v). |vertices f| \<le> 4 \<longrightarrow> \<V> f \<inter> V = {v}); f \<in> set (facesAt g u); u \<in> V; v \<in> V; u \<noteq> v; u \<in> \<V> f; f \<bullet> (f \<bullet> u) \<in> \<V> f \<inter> V\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v = f \<bullet> (f \<bullet> u); v \<in> \<V> f; |vertices f| \<le> 4; (\<forall>v\<in>V. \<forall>f\<in>set (facesAt g v). f \<bullet> v \<notin> V) \<and> (\<forall>v\<in>V. \<forall>f\<in>set (facesAt g v). |vertices f| \<le> 4 \<longrightarrow> \<V> f \<inter> V = {v}); f \<in> set (facesAt g u); u \<in> V; v \<in> V; u \<noteq> v; u \<in> \<V> f; f \<bullet> (f \<bullet> u) \<in> \<V> f \<inter> V\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. |vertices f| \<noteq> 4 \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. |vertices f| \<noteq> 4 \<Longrightarrow> False
[PROOF STEP]
assume 4: "|vertices f| \<noteq> 4"
[PROOF STATE]
proof (state)
this:
|vertices f| \<noteq> 4

goal (1 subgoal):
 1. |vertices f| \<noteq> 4 \<Longrightarrow> False
[PROOF STEP]
hence "v = f \<bullet> u"
[PROOF STATE]
proof (prove)
using this:
|vertices f| \<noteq> 4

goal (1 subgoal):
 1. v = f \<bullet> u
[PROOF STEP]
using "if"
[PROOF STATE]
proof (prove)
using this:
|vertices f| \<noteq> 4
if |vertices f| = 4 then v = f \<bullet> u \<or> v = f \<bullet> (f \<bullet> u) else v = f \<bullet> u

goal (1 subgoal):
 1. v = f \<bullet> u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v = f \<bullet> u

goal (1 subgoal):
 1. |vertices f| \<noteq> 4 \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
v = f \<bullet> u

goal (1 subgoal):
 1. False
[PROOF STEP]
using sep f uv
[PROOF STATE]
proof (prove)
using this:
v = f \<bullet> u
separated g V
f \<in> set (facesAt g u)
u \<in> V
v \<in> V
u \<noteq> v

goal (1 subgoal):
 1. False
[PROOF STEP]
by(simp add:separated_def separated\<^sub>2_def separated\<^sub>3_def)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>u\<in>V. \<forall>v\<in>V. u \<noteq> v \<longrightarrow> \<not> close g u v

goal (1 subgoal):
 1. \<forall>u\<in>V. \<forall>v\<in>V. u \<noteq> v \<longrightarrow> \<not> close g u v \<Longrightarrow> separated g V
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>u\<in>V. \<forall>v\<in>V. u \<noteq> v \<longrightarrow> \<not> close g u v \<Longrightarrow> separated g V
[PROOF STEP]
assume not_cl: ?Q
[PROOF STATE]
proof (state)
this:
\<forall>u\<in>V. \<forall>v\<in>V. u \<noteq> v \<longrightarrow> \<not> close g u v

goal (1 subgoal):
 1. \<forall>u\<in>V. \<forall>v\<in>V. u \<noteq> v \<longrightarrow> \<not> close g u v \<Longrightarrow> separated g V
[PROOF STEP]
show ?P
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. separated g V
[PROOF STEP]
proof(simp add:separated_def, rule conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. separated\<^sub>2 g V
 2. separated\<^sub>3 g V
[PROOF STEP]
show "separated\<^sub>2 g V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. separated\<^sub>2 g V
[PROOF STEP]
proof (clarsimp simp:separated\<^sub>2_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v f. \<lbrakk>v \<in> V; f \<in> set (facesAt g v); f \<bullet> v \<in> V\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix v f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v f. \<lbrakk>v \<in> V; f \<in> set (facesAt g v); f \<bullet> v \<in> V\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume a: "v \<in> V" "f \<in> set (facesAt g v)" "f \<bullet> v \<in> V"
[PROOF STATE]
proof (state)
this:
v \<in> V
f \<in> set (facesAt g v)
f \<bullet> v \<in> V

goal (1 subgoal):
 1. \<And>v f. \<lbrakk>v \<in> V; f \<in> set (facesAt g v); f \<bullet> v \<in> V\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "v : \<V> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> \<V> g
[PROOF STEP]
using a(1) \<open>V \<subseteq> \<V> g\<close>
[PROOF STATE]
proof (prove)
using this:
v \<in> V
V \<subseteq> \<V> g

goal (1 subgoal):
 1. v \<in> \<V> g
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v \<in> \<V> g

goal (1 subgoal):
 1. \<And>v f. \<lbrakk>v \<in> V; f \<in> set (facesAt g v); f \<bullet> v \<in> V\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using a not_cl mgp_facesAt_no_loop[OF mgp \<open>v : \<V> g\<close> a(2)]
[PROOF STATE]
proof (prove)
using this:
v \<in> V
f \<in> set (facesAt g v)
f \<bullet> v \<in> V
\<forall>u\<in>V. \<forall>v\<in>V. u \<noteq> v \<longrightarrow> \<not> close g u v
f \<bullet> v \<noteq> v

goal (1 subgoal):
 1. False
[PROOF STEP]
by(fastforce simp: close_def split:if_split_asm)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
separated\<^sub>2 g V

goal (1 subgoal):
 1. separated\<^sub>3 g V
[PROOF STEP]
show "separated\<^sub>3 g V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. separated\<^sub>3 g V
[PROOF STEP]
proof (clarsimp simp:separated\<^sub>3_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v f. \<lbrakk>v \<in> V; f \<in> set (facesAt g v); |vertices f| \<le> 4\<rbrakk> \<Longrightarrow> \<V> f \<inter> V = {v}
[PROOF STEP]
fix v f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v f. \<lbrakk>v \<in> V; f \<in> set (facesAt g v); |vertices f| \<le> 4\<rbrakk> \<Longrightarrow> \<V> f \<inter> V = {v}
[PROOF STEP]
assume "v \<in> V" and f: "f \<in> set (facesAt g v)" and len: "|vertices f| \<le> 4"
[PROOF STATE]
proof (state)
this:
v \<in> V
f \<in> set (facesAt g v)
|vertices f| \<le> 4

goal (1 subgoal):
 1. \<And>v f. \<lbrakk>v \<in> V; f \<in> set (facesAt g v); |vertices f| \<le> 4\<rbrakk> \<Longrightarrow> \<V> f \<inter> V = {v}
[PROOF STEP]
have vg: "v : \<V> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> \<V> g
[PROOF STEP]
using \<open>v : V\<close> \<open>V \<subseteq> \<V> g\<close>
[PROOF STATE]
proof (prove)
using this:
v \<in> V
V \<subseteq> \<V> g

goal (1 subgoal):
 1. v \<in> \<V> g
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v \<in> \<V> g

goal (1 subgoal):
 1. \<And>v f. \<lbrakk>v \<in> V; f \<in> set (facesAt g v); |vertices f| \<le> 4\<rbrakk> \<Longrightarrow> \<V> f \<inter> V = {v}
[PROOF STEP]
note distf = minGraphProps3[OF mgp minGraphProps5[OF mgp vg f]]
[PROOF STATE]
proof (state)
this:
distinct (vertices f)

goal (1 subgoal):
 1. \<And>v f. \<lbrakk>v \<in> V; f \<in> set (facesAt g v); |vertices f| \<le> 4\<rbrakk> \<Longrightarrow> \<V> f \<inter> V = {v}
[PROOF STEP]
note vf = minGraphProps6[OF mgp vg f]
[PROOF STATE]
proof (state)
this:
v \<in> \<V> f

goal (1 subgoal):
 1. \<And>v f. \<lbrakk>v \<in> V; f \<in> set (facesAt g v); |vertices f| \<le> 4\<rbrakk> \<Longrightarrow> \<V> f \<inter> V = {v}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
v \<in> \<V> f

goal (1 subgoal):
 1. \<And>v f. \<lbrakk>v \<in> V; f \<in> set (facesAt g v); |vertices f| \<le> 4\<rbrakk> \<Longrightarrow> \<V> f \<inter> V = {v}
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v f. \<lbrakk>v \<in> V; f \<in> set (facesAt g v); |vertices f| \<le> 4\<rbrakk> \<Longrightarrow> \<V> f \<inter> V = {v}
[PROOF STEP]
assume "u \<in> \<V> f" and "u \<in> V"
[PROOF STATE]
proof (state)
this:
u \<in> \<V> f
u \<in> V

goal (1 subgoal):
 1. \<And>v f. \<lbrakk>v \<in> V; f \<in> set (facesAt g v); |vertices f| \<le> 4\<rbrakk> \<Longrightarrow> \<V> f \<inter> V = {v}
[PROOF STEP]
have "u = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u = v
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> u = v
 2. \<not> ?P \<Longrightarrow> u = v
[PROOF STEP]
assume 3: "|vertices f| = 3"
[PROOF STATE]
proof (state)
this:
triangle f

goal (2 subgoals):
 1. ?P \<Longrightarrow> u = v
 2. \<not> ?P \<Longrightarrow> u = v
[PROOF STEP]
hence "\<V> f = {v, f \<bullet> v, f \<bullet> (f \<bullet> v)}"
[PROOF STATE]
proof (prove)
using this:
triangle f

goal (1 subgoal):
 1. \<V> f = {v, f \<bullet> v, f \<bullet> (f \<bullet> v)}
[PROOF STEP]
using vertices_triangle[OF _ vf distf]
[PROOF STATE]
proof (prove)
using this:
triangle f
triangle f \<Longrightarrow> \<V> f = {v, f \<bullet> v, f \<bullet> (f \<bullet> v)}

goal (1 subgoal):
 1. \<V> f = {v, f \<bullet> v, f \<bullet> (f \<bullet> v)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<V> f = {v, f \<bullet> v, f \<bullet> (f \<bullet> v)}

goal (2 subgoals):
 1. ?P \<Longrightarrow> u = v
 2. \<not> ?P \<Longrightarrow> u = v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<V> f = {v, f \<bullet> v, f \<bullet> (f \<bullet> v)}

goal (2 subgoals):
 1. ?P \<Longrightarrow> u = v
 2. \<not> ?P \<Longrightarrow> u = v
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<V> f = {v, f \<bullet> v, f \<bullet> (f \<bullet> v)}

goal (2 subgoals):
 1. ?P \<Longrightarrow> u = v
 2. \<not> ?P \<Longrightarrow> u = v
[PROOF STEP]
assume "u = f \<bullet> v"
[PROOF STATE]
proof (state)
this:
u = f \<bullet> v

goal (2 subgoals):
 1. ?P \<Longrightarrow> u = v
 2. \<not> ?P \<Longrightarrow> u = v
[PROOF STEP]
hence "u = v"
[PROOF STATE]
proof (prove)
using this:
u = f \<bullet> v

goal (1 subgoal):
 1. u = v
[PROOF STEP]
using not_cl f \<open>u \<in> V\<close> \<open>v \<in> V\<close> 3
[PROOF STATE]
proof (prove)
using this:
u = f \<bullet> v
\<forall>u\<in>V. \<forall>v\<in>V. u \<noteq> v \<longrightarrow> \<not> close g u v
f \<in> set (facesAt g v)
u \<in> V
v \<in> V
triangle f

goal (1 subgoal):
 1. u = v
[PROOF STEP]
by(force simp:close_def split:if_split_asm)
[PROOF STATE]
proof (state)
this:
u = v

goal (2 subgoals):
 1. ?P \<Longrightarrow> u = v
 2. \<not> ?P \<Longrightarrow> u = v
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
u = f \<bullet> v \<Longrightarrow> u = v

goal (2 subgoals):
 1. ?P \<Longrightarrow> u = v
 2. \<not> ?P \<Longrightarrow> u = v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u = f \<bullet> v \<Longrightarrow> u = v

goal (2 subgoals):
 1. ?P \<Longrightarrow> u = v
 2. \<not> ?P \<Longrightarrow> u = v
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
u = f \<bullet> v \<Longrightarrow> u = v

goal (2 subgoals):
 1. ?P \<Longrightarrow> u = v
 2. \<not> ?P \<Longrightarrow> u = v
[PROOF STEP]
assume "u = f \<bullet> (f \<bullet> v)"
[PROOF STATE]
proof (state)
this:
u = f \<bullet> (f \<bullet> v)

goal (2 subgoals):
 1. ?P \<Longrightarrow> u = v
 2. \<not> ?P \<Longrightarrow> u = v
[PROOF STEP]
hence fu: "f \<bullet> u = v"
[PROOF STATE]
proof (prove)
using this:
u = f \<bullet> (f \<bullet> v)

goal (1 subgoal):
 1. f \<bullet> u = v
[PROOF STEP]
by(simp add: tri_next3_id[OF 3 distf \<open>v \<in> \<V> f\<close>])
[PROOF STATE]
proof (state)
this:
f \<bullet> u = v

goal (2 subgoals):
 1. ?P \<Longrightarrow> u = v
 2. \<not> ?P \<Longrightarrow> u = v
[PROOF STEP]
hence "(u,v) \<in> \<E> f"
[PROOF STATE]
proof (prove)
using this:
f \<bullet> u = v

goal (1 subgoal):
 1. (u, v) \<in> \<E> f
[PROOF STEP]
using nextVertex_in_edges[OF \<open>u \<in> \<V> f\<close>]
[PROOF STATE]
proof (prove)
using this:
f \<bullet> u = v
(u, f \<bullet> u) \<in> \<E> f

goal (1 subgoal):
 1. (u, v) \<in> \<E> f
[PROOF STEP]
by(simp add:fu)
[PROOF STATE]
proof (state)
this:
(u, v) \<in> \<E> f

goal (2 subgoals):
 1. ?P \<Longrightarrow> u = v
 2. \<not> ?P \<Longrightarrow> u = v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(u, v) \<in> \<E> f
[PROOF STEP]
obtain f' where "f' \<in> set(facesAt g v)" "(v,u) \<in>  \<E> f'"
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> \<E> f

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>f' \<in> set (facesAt g v); (v, u) \<in> \<E> f'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using mgp_edge_face_ex[OF mgp vg f]
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> \<E> f
(?u, v) \<in> \<E> f \<Longrightarrow> \<exists>f'\<in>set (facesAt g v). (v, ?u) \<in> \<E> f'

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>f' \<in> set (facesAt g v); (v, u) \<in> \<E> f'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f' \<in> set (facesAt g v)
(v, u) \<in> \<E> f'

goal (2 subgoals):
 1. ?P \<Longrightarrow> u = v
 2. \<not> ?P \<Longrightarrow> u = v
[PROOF STEP]
hence "u = v"
[PROOF STATE]
proof (prove)
using this:
f' \<in> set (facesAt g v)
(v, u) \<in> \<E> f'

goal (1 subgoal):
 1. u = v
[PROOF STEP]
using not_cl \<open>u \<in> V\<close> \<open>v \<in> V\<close> 3
[PROOF STATE]
proof (prove)
using this:
f' \<in> set (facesAt g v)
(v, u) \<in> \<E> f'
\<forall>u\<in>V. \<forall>v\<in>V. u \<noteq> v \<longrightarrow> \<not> close g u v
u \<in> V
v \<in> V
triangle f

goal (1 subgoal):
 1. u = v
[PROOF STEP]
by(force simp:close_def edges_face_eq split:if_split_asm)
[PROOF STATE]
proof (state)
this:
u = v

goal (2 subgoals):
 1. ?P \<Longrightarrow> u = v
 2. \<not> ?P \<Longrightarrow> u = v
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
u = f \<bullet> (f \<bullet> v) \<Longrightarrow> u = v

goal (2 subgoals):
 1. ?P \<Longrightarrow> u = v
 2. \<not> ?P \<Longrightarrow> u = v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<V> f = {v, f \<bullet> v, f \<bullet> (f \<bullet> v)}
u = f \<bullet> v \<Longrightarrow> u = v
u = f \<bullet> (f \<bullet> v) \<Longrightarrow> u = v
[PROOF STEP]
show "u=v"
[PROOF STATE]
proof (prove)
using this:
\<V> f = {v, f \<bullet> v, f \<bullet> (f \<bullet> v)}
u = f \<bullet> v \<Longrightarrow> u = v
u = f \<bullet> (f \<bullet> v) \<Longrightarrow> u = v

goal (1 subgoal):
 1. u = v
[PROOF STEP]
using \<open>u \<in> \<V> f\<close>
[PROOF STATE]
proof (prove)
using this:
\<V> f = {v, f \<bullet> v, f \<bullet> (f \<bullet> v)}
u = f \<bullet> v \<Longrightarrow> u = v
u = f \<bullet> (f \<bullet> v) \<Longrightarrow> u = v
u \<in> \<V> f

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

goal (1 subgoal):
 1. |vertices f| \<noteq> 3 \<Longrightarrow> u = v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. |vertices f| \<noteq> 3 \<Longrightarrow> u = v
[PROOF STEP]
assume 3: "|vertices f| \<noteq> 3"
[PROOF STATE]
proof (state)
this:
|vertices f| \<noteq> 3

goal (1 subgoal):
 1. |vertices f| \<noteq> 3 \<Longrightarrow> u = v
[PROOF STEP]
hence 4: "|vertices f| = 4"
[PROOF STATE]
proof (prove)
using this:
|vertices f| \<noteq> 3

goal (1 subgoal):
 1. |vertices f| = 4
[PROOF STEP]
using len mgp_vertices3[OF mgp minGraphProps5[OF mgp vg f]]
[PROOF STATE]
proof (prove)
using this:
|vertices f| \<noteq> 3
|vertices f| \<le> 4
3 \<le> |vertices f|

goal (1 subgoal):
 1. |vertices f| = 4
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
|vertices f| = 4

goal (1 subgoal):
 1. |vertices f| \<noteq> 3 \<Longrightarrow> u = v
[PROOF STEP]
hence "\<V> f = {v, f \<bullet> v, f \<bullet> (f \<bullet> v), f \<bullet> (f \<bullet> (f \<bullet> v))}"
[PROOF STATE]
proof (prove)
using this:
|vertices f| = 4

goal (1 subgoal):
 1. \<V> f = {v, f \<bullet> v, f \<bullet> (f \<bullet> v), f \<bullet> (f \<bullet> (f \<bullet> v))}
[PROOF STEP]
using vertices_quad[OF _ vf distf]
[PROOF STATE]
proof (prove)
using this:
|vertices f| = 4
|vertices f| = 4 \<Longrightarrow> \<V> f = {v, f \<bullet> v, f \<bullet> (f \<bullet> v), f \<bullet> (f \<bullet> (f \<bullet> v))}

goal (1 subgoal):
 1. \<V> f = {v, f \<bullet> v, f \<bullet> (f \<bullet> v), f \<bullet> (f \<bullet> (f \<bullet> v))}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<V> f = {v, f \<bullet> v, f \<bullet> (f \<bullet> v), f \<bullet> (f \<bullet> (f \<bullet> v))}

goal (1 subgoal):
 1. |vertices f| \<noteq> 3 \<Longrightarrow> u = v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<V> f = {v, f \<bullet> v, f \<bullet> (f \<bullet> v), f \<bullet> (f \<bullet> (f \<bullet> v))}

goal (1 subgoal):
 1. |vertices f| \<noteq> 3 \<Longrightarrow> u = v
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<V> f = {v, f \<bullet> v, f \<bullet> (f \<bullet> v), f \<bullet> (f \<bullet> (f \<bullet> v))}

goal (1 subgoal):
 1. |vertices f| \<noteq> 3 \<Longrightarrow> u = v
[PROOF STEP]
assume "u = f \<bullet> v"
[PROOF STATE]
proof (state)
this:
u = f \<bullet> v

goal (1 subgoal):
 1. |vertices f| \<noteq> 3 \<Longrightarrow> u = v
[PROOF STEP]
hence "u = v"
[PROOF STATE]
proof (prove)
using this:
u = f \<bullet> v

goal (1 subgoal):
 1. u = v
[PROOF STEP]
using not_cl f \<open>u \<in> V\<close> \<open>v \<in> V\<close> 4
[PROOF STATE]
proof (prove)
using this:
u = f \<bullet> v
\<forall>u\<in>V. \<forall>v\<in>V. u \<noteq> v \<longrightarrow> \<not> close g u v
f \<in> set (facesAt g v)
u \<in> V
v \<in> V
|vertices f| = 4

goal (1 subgoal):
 1. u = v
[PROOF STEP]
by(force simp:close_def split:if_split_asm)
[PROOF STATE]
proof (state)
this:
u = v

goal (1 subgoal):
 1. |vertices f| \<noteq> 3 \<Longrightarrow> u = v
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
u = f \<bullet> v \<Longrightarrow> u = v

goal (1 subgoal):
 1. |vertices f| \<noteq> 3 \<Longrightarrow> u = v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u = f \<bullet> v \<Longrightarrow> u = v

goal (1 subgoal):
 1. |vertices f| \<noteq> 3 \<Longrightarrow> u = v
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
u = f \<bullet> v \<Longrightarrow> u = v

goal (1 subgoal):
 1. |vertices f| \<noteq> 3 \<Longrightarrow> u = v
[PROOF STEP]
assume "u = f \<bullet> (f \<bullet> v)"
[PROOF STATE]
proof (state)
this:
u = f \<bullet> (f \<bullet> v)

goal (1 subgoal):
 1. |vertices f| \<noteq> 3 \<Longrightarrow> u = v
[PROOF STEP]
hence "u = v"
[PROOF STATE]
proof (prove)
using this:
u = f \<bullet> (f \<bullet> v)

goal (1 subgoal):
 1. u = v
[PROOF STEP]
using not_cl f \<open>u \<in> V\<close> \<open>v \<in> V\<close> 4
[PROOF STATE]
proof (prove)
using this:
u = f \<bullet> (f \<bullet> v)
\<forall>u\<in>V. \<forall>v\<in>V. u \<noteq> v \<longrightarrow> \<not> close g u v
f \<in> set (facesAt g v)
u \<in> V
v \<in> V
|vertices f| = 4

goal (1 subgoal):
 1. u = v
[PROOF STEP]
by(force simp:close_def split:if_split_asm)
[PROOF STATE]
proof (state)
this:
u = v

goal (1 subgoal):
 1. |vertices f| \<noteq> 3 \<Longrightarrow> u = v
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
u = f \<bullet> (f \<bullet> v) \<Longrightarrow> u = v

goal (1 subgoal):
 1. |vertices f| \<noteq> 3 \<Longrightarrow> u = v
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u = f \<bullet> (f \<bullet> v) \<Longrightarrow> u = v

goal (1 subgoal):
 1. |vertices f| \<noteq> 3 \<Longrightarrow> u = v
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
u = f \<bullet> (f \<bullet> v) \<Longrightarrow> u = v

goal (1 subgoal):
 1. |vertices f| \<noteq> 3 \<Longrightarrow> u = v
[PROOF STEP]
assume "u = f \<bullet> (f \<bullet> (f \<bullet> v))"
[PROOF STATE]
proof (state)
this:
u = f \<bullet> (f \<bullet> (f \<bullet> v))

goal (1 subgoal):
 1. |vertices f| \<noteq> 3 \<Longrightarrow> u = v
[PROOF STEP]
hence fu: "f \<bullet> u = v"
[PROOF STATE]
proof (prove)
using this:
u = f \<bullet> (f \<bullet> (f \<bullet> v))

goal (1 subgoal):
 1. f \<bullet> u = v
[PROOF STEP]
by(simp add: quad_next4_id[OF 4 distf \<open>v \<in> \<V> f\<close>])
[PROOF STATE]
proof (state)
this:
f \<bullet> u = v

goal (1 subgoal):
 1. |vertices f| \<noteq> 3 \<Longrightarrow> u = v
[PROOF STEP]
hence "(u,v) \<in> \<E> f"
[PROOF STATE]
proof (prove)
using this:
f \<bullet> u = v

goal (1 subgoal):
 1. (u, v) \<in> \<E> f
[PROOF STEP]
using nextVertex_in_edges[OF \<open>u \<in> \<V> f\<close>]
[PROOF STATE]
proof (prove)
using this:
f \<bullet> u = v
(u, f \<bullet> u) \<in> \<E> f

goal (1 subgoal):
 1. (u, v) \<in> \<E> f
[PROOF STEP]
by(simp add:fu)
[PROOF STATE]
proof (state)
this:
(u, v) \<in> \<E> f

goal (1 subgoal):
 1. |vertices f| \<noteq> 3 \<Longrightarrow> u = v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(u, v) \<in> \<E> f
[PROOF STEP]
obtain f' where "f' \<in> set(facesAt g v)" "(v,u) \<in>  \<E> f'"
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> \<E> f

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>f' \<in> set (facesAt g v); (v, u) \<in> \<E> f'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using mgp_edge_face_ex[OF mgp vg f]
[PROOF STATE]
proof (prove)
using this:
(u, v) \<in> \<E> f
(?u, v) \<in> \<E> f \<Longrightarrow> \<exists>f'\<in>set (facesAt g v). (v, ?u) \<in> \<E> f'

goal (1 subgoal):
 1. (\<And>f'. \<lbrakk>f' \<in> set (facesAt g v); (v, u) \<in> \<E> f'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f' \<in> set (facesAt g v)
(v, u) \<in> \<E> f'

goal (1 subgoal):
 1. |vertices f| \<noteq> 3 \<Longrightarrow> u = v
[PROOF STEP]
hence "u = v"
[PROOF STATE]
proof (prove)
using this:
f' \<in> set (facesAt g v)
(v, u) \<in> \<E> f'

goal (1 subgoal):
 1. u = v
[PROOF STEP]
using not_cl \<open>u \<in> V\<close> \<open>v \<in> V\<close> 4
[PROOF STATE]
proof (prove)
using this:
f' \<in> set (facesAt g v)
(v, u) \<in> \<E> f'
\<forall>u\<in>V. \<forall>v\<in>V. u \<noteq> v \<longrightarrow> \<not> close g u v
u \<in> V
v \<in> V
|vertices f| = 4

goal (1 subgoal):
 1. u = v
[PROOF STEP]
by(force simp:close_def edges_face_eq split:if_split_asm)
[PROOF STATE]
proof (state)
this:
u = v

goal (1 subgoal):
 1. |vertices f| \<noteq> 3 \<Longrightarrow> u = v
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
u = f \<bullet> (f \<bullet> (f \<bullet> v)) \<Longrightarrow> u = v

goal (1 subgoal):
 1. |vertices f| \<noteq> 3 \<Longrightarrow> u = v
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<V> f = {v, f \<bullet> v, f \<bullet> (f \<bullet> v), f \<bullet> (f \<bullet> (f \<bullet> v))}
u = f \<bullet> v \<Longrightarrow> u = v
u = f \<bullet> (f \<bullet> v) \<Longrightarrow> u = v
u = f \<bullet> (f \<bullet> (f \<bullet> v)) \<Longrightarrow> u = v
[PROOF STEP]
show "u=v"
[PROOF STATE]
proof (prove)
using this:
\<V> f = {v, f \<bullet> v, f \<bullet> (f \<bullet> v), f \<bullet> (f \<bullet> (f \<bullet> v))}
u = f \<bullet> v \<Longrightarrow> u = v
u = f \<bullet> (f \<bullet> v) \<Longrightarrow> u = v
u = f \<bullet> (f \<bullet> (f \<bullet> v)) \<Longrightarrow> u = v

goal (1 subgoal):
 1. u = v
[PROOF STEP]
using \<open>u \<in> \<V> f\<close>
[PROOF STATE]
proof (prove)
using this:
\<V> f = {v, f \<bullet> v, f \<bullet> (f \<bullet> v), f \<bullet> (f \<bullet> (f \<bullet> v))}
u = f \<bullet> v \<Longrightarrow> u = v
u = f \<bullet> (f \<bullet> v) \<Longrightarrow> u = v
u = f \<bullet> (f \<bullet> (f \<bullet> v)) \<Longrightarrow> u = v
u \<in> \<V> f

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
u = v

goal (1 subgoal):
 1. \<And>v f. \<lbrakk>v \<in> V; f \<in> set (facesAt g v); |vertices f| \<le> 4\<rbrakk> \<Longrightarrow> \<V> f \<inter> V = {v}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?u2 \<in> \<V> f; ?u2 \<in> V\<rbrakk> \<Longrightarrow> ?u2 = v

goal (1 subgoal):
 1. \<And>v f. \<lbrakk>v \<in> V; f \<in> set (facesAt g v); |vertices f| \<le> 4\<rbrakk> \<Longrightarrow> \<V> f \<inter> V = {v}
[PROOF STEP]
thus "\<V> f \<inter> V = {v}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?u2 \<in> \<V> f; ?u2 \<in> V\<rbrakk> \<Longrightarrow> ?u2 = v

goal (1 subgoal):
 1. \<V> f \<inter> V = {v}
[PROOF STEP]
using \<open>v \<in> V\<close> vf
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?u2 \<in> \<V> f; ?u2 \<in> V\<rbrakk> \<Longrightarrow> ?u2 = v
v \<in> V
v \<in> \<V> f

goal (1 subgoal):
 1. \<V> f \<inter> V = {v}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<V> f \<inter> V = {v}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
separated\<^sub>3 g V

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
separated g V

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sep_ne: "\<exists>P \<subseteq> M. separated g (fst ` P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P\<subseteq>M. separated g (fst ` P)
[PROOF STEP]
by(unfold separated_def separated\<^sub>2_def separated\<^sub>3_def) blast


[STATEMENT]
lemma ExcessNotAtRec_conv_Max:
assumes mgp: "minGraphProps g"
shows "set(map fst ps) \<subseteq> \<V> g \<Longrightarrow> distinct(map fst ps) \<Longrightarrow>
  ExcessNotAtRec ps g =
  Max{ \<Sum>p\<in>P. snd p |P. P \<subseteq> set ps \<and> separated g (fst ` P)}"
  (is "_ \<Longrightarrow> _ \<Longrightarrow> _ = Max(?M ps)" is "_ \<Longrightarrow> _ \<Longrightarrow> _ = Max{_ |P. ?S ps P}")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set (map fst ps) \<subseteq> \<V> g; distinct (map fst ps)\<rbrakk> \<Longrightarrow> ExcessNotAtRec ps g = Max {sum snd P |P. P \<subseteq> set ps \<and> separated g (fst ` P)}
[PROOF STEP]
proof(induct ps rule: length_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<forall>ys. |ys| < |xs| \<longrightarrow> set (map fst ys) \<subseteq> \<V> g \<longrightarrow> distinct (map fst ys) \<longrightarrow> ExcessNotAtRec ys g = Max {sum snd P |P. P \<subseteq> set ys \<and> separated g (fst ` P)}; set (map fst xs) \<subseteq> \<V> g; distinct (map fst xs)\<rbrakk> \<Longrightarrow> ExcessNotAtRec xs g = Max {sum snd P |P. P \<subseteq> set xs \<and> separated g (fst ` P)}
[PROOF STEP]
case (1 ps0)
[PROOF STATE]
proof (state)
this:
\<forall>ys. |ys| < |ps0| \<longrightarrow> set (map fst ys) \<subseteq> \<V> g \<longrightarrow> distinct (map fst ys) \<longrightarrow> ExcessNotAtRec ys g = Max {sum snd P |P. P \<subseteq> set ys \<and> separated g (fst ` P)}
set (map fst ps0) \<subseteq> \<V> g
distinct (map fst ps0)

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<forall>ys. |ys| < |xs| \<longrightarrow> set (map fst ys) \<subseteq> \<V> g \<longrightarrow> distinct (map fst ys) \<longrightarrow> ExcessNotAtRec ys g = Max {sum snd P |P. P \<subseteq> set ys \<and> separated g (fst ` P)}; set (map fst xs) \<subseteq> \<V> g; distinct (map fst xs)\<rbrakk> \<Longrightarrow> ExcessNotAtRec xs g = Max {sum snd P |P. P \<subseteq> set xs \<and> separated g (fst ` P)}
[PROOF STEP]
note IH = 1(1) and subset = 1(2) and dist = 1(3)
[PROOF STATE]
proof (state)
this:
\<forall>ys. |ys| < |ps0| \<longrightarrow> set (map fst ys) \<subseteq> \<V> g \<longrightarrow> distinct (map fst ys) \<longrightarrow> ExcessNotAtRec ys g = Max {sum snd P |P. P \<subseteq> set ys \<and> separated g (fst ` P)}
set (map fst ps0) \<subseteq> \<V> g
distinct (map fst ps0)

goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<forall>ys. |ys| < |xs| \<longrightarrow> set (map fst ys) \<subseteq> \<V> g \<longrightarrow> distinct (map fst ys) \<longrightarrow> ExcessNotAtRec ys g = Max {sum snd P |P. P \<subseteq> set ys \<and> separated g (fst ` P)}; set (map fst xs) \<subseteq> \<V> g; distinct (map fst xs)\<rbrakk> \<Longrightarrow> ExcessNotAtRec xs g = Max {sum snd P |P. P \<subseteq> set xs \<and> separated g (fst ` P)}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
proof (cases ps0)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ps0 = [] \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
 2. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
ps0 = []

goal (2 subgoals):
 1. ps0 = [] \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
 2. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ps0 = []

goal (1 subgoal):
 1. ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}

goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
case (Cons p ps)
[PROOF STATE]
proof (state)
this:
ps0 = p # ps

goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
let ?ps = "deleteAround g (fst p) ps"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
have le: "|?ps| \<le> |ps|"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |deleteAround g (fst p) ps| \<le> |ps|
[PROOF STEP]
by(simp add:delAround_def)
[PROOF STATE]
proof (state)
this:
|deleteAround g (fst p) ps| \<le> |ps|

goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
have dist': "distinct(map fst ?ps)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst (deleteAround g (fst p) ps))
[PROOF STEP]
using dist Cons
[PROOF STATE]
proof (prove)
using this:
distinct (map fst ps0)
ps0 = p # ps

goal (1 subgoal):
 1. distinct (map fst (deleteAround g (fst p) ps))
[PROOF STEP]
apply (clarsimp simp:delAround_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps0 = p # ps; fst p \<notin> fst ` set ps; distinct (map fst ps)\<rbrakk> \<Longrightarrow> distinct (map fst (filter (\<lambda>pa. \<not> close g (fst p) (fst pa)) ps))
[PROOF STEP]
apply(drule distinct_filter[where P = "Not \<circ> close g (fst p)"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ps0 = p # ps; fst p \<notin> fst ` set ps; distinct (filter (Not \<circ> close g (fst p)) (map fst ps))\<rbrakk> \<Longrightarrow> distinct (map fst (filter (\<lambda>pa. \<not> close g (fst p) (fst pa)) ps))
[PROOF STEP]
apply(simp add: filter_map o_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
distinct (map fst (deleteAround g (fst p) ps))

goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
have "fst p : \<V> g" and "fst ` set ps \<subseteq> \<V> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst p \<in> \<V> g &&& fst ` set ps \<subseteq> \<V> g
[PROOF STEP]
using subset Cons
[PROOF STATE]
proof (prove)
using this:
set (map fst ps0) \<subseteq> \<V> g
ps0 = p # ps

goal (1 subgoal):
 1. fst p \<in> \<V> g &&& fst ` set ps \<subseteq> \<V> g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst p \<in> \<V> g
fst ` set ps \<subseteq> \<V> g

goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
have sub1: "\<And>P Q. P \<subseteq> {x : set ps. Q x} \<Longrightarrow> fst ` P \<subseteq> \<V> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P Q. P \<subseteq> {x \<in> set ps. Q x} \<Longrightarrow> fst ` P \<subseteq> \<V> g
[PROOF STEP]
using subset Cons
[PROOF STATE]
proof (prove)
using this:
set (map fst ps0) \<subseteq> \<V> g
ps0 = p # ps

goal (1 subgoal):
 1. \<And>P Q. P \<subseteq> {x \<in> set ps. Q x} \<Longrightarrow> fst ` P \<subseteq> \<V> g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?P \<subseteq> {x \<in> set ps. ?Q x} \<Longrightarrow> fst ` ?P \<subseteq> \<V> g

goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
have sub2: "\<And>P Q. P \<subseteq> insert p {x : set ps. Q x} \<Longrightarrow> fst ` P \<subseteq> \<V> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P Q. P \<subseteq> insert p {x \<in> set ps. Q x} \<Longrightarrow> fst ` P \<subseteq> \<V> g
[PROOF STEP]
using subset Cons
[PROOF STATE]
proof (prove)
using this:
set (map fst ps0) \<subseteq> \<V> g
ps0 = p # ps

goal (1 subgoal):
 1. \<And>P Q. P \<subseteq> insert p {x \<in> set ps. Q x} \<Longrightarrow> fst ` P \<subseteq> \<V> g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?P \<subseteq> insert p {x \<in> set ps. ?Q x} \<Longrightarrow> fst ` ?P \<subseteq> \<V> g

goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
have sub3: "\<And>P. P \<subseteq> insert p (set ps) \<Longrightarrow> fst ` P \<subseteq> \<V> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. P \<subseteq> insert p (set ps) \<Longrightarrow> fst ` P \<subseteq> \<V> g
[PROOF STEP]
using subset Cons
[PROOF STATE]
proof (prove)
using this:
set (map fst ps0) \<subseteq> \<V> g
ps0 = p # ps

goal (1 subgoal):
 1. \<And>P. P \<subseteq> insert p (set ps) \<Longrightarrow> fst ` P \<subseteq> \<V> g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?P \<subseteq> insert p (set ps) \<Longrightarrow> fst ` ?P \<subseteq> \<V> g

goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
have "\<And>a. set (map fst (deleteAround g a ps)) \<subseteq> \<V> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. set (map fst (deleteAround g a ps)) \<subseteq> \<V> g
[PROOF STEP]
using deleteAround_subset[of g _ ps] subset Cons
[PROOF STATE]
proof (prove)
using this:
set (deleteAround g ?a ps) \<subseteq> set ps
set (map fst ps0) \<subseteq> \<V> g
ps0 = p # ps

goal (1 subgoal):
 1. \<And>a. set (map fst (deleteAround g a ps)) \<subseteq> \<V> g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (map fst (deleteAround g ?a ps)) \<subseteq> \<V> g

goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
hence "ExcessNotAtRec ps0 g = max (Max(?M ps)) (Max(?M ?ps) + snd p)"
[PROOF STATE]
proof (prove)
using this:
set (map fst (deleteAround g ?a ps)) \<subseteq> \<V> g

goal (1 subgoal):
 1. ExcessNotAtRec ps0 g = max (Max {sum snd P |P. P \<subseteq> set ps \<and> separated g (fst ` P)}) (Max {sum snd P |P. P \<subseteq> set (deleteAround g (fst p) ps) \<and> separated g (fst ` P)} + snd p)
[PROOF STEP]
using Cons IH subset le dist dist'
[PROOF STATE]
proof (prove)
using this:
set (map fst (deleteAround g ?a ps)) \<subseteq> \<V> g
ps0 = p # ps
\<forall>ys. |ys| < |ps0| \<longrightarrow> set (map fst ys) \<subseteq> \<V> g \<longrightarrow> distinct (map fst ys) \<longrightarrow> ExcessNotAtRec ys g = Max {sum snd P |P. P \<subseteq> set ys \<and> separated g (fst ` P)}
set (map fst ps0) \<subseteq> \<V> g
|deleteAround g (fst p) ps| \<le> |ps|
distinct (map fst ps0)
distinct (map fst (deleteAround g (fst p) ps))

goal (1 subgoal):
 1. ExcessNotAtRec ps0 g = max (Max {sum snd P |P. P \<subseteq> set ps \<and> separated g (fst ` P)}) (Max {sum snd P |P. P \<subseteq> set (deleteAround g (fst p) ps) \<and> separated g (fst ` P)} + snd p)
[PROOF STEP]
by (cases p) simp
[PROOF STATE]
proof (state)
this:
ExcessNotAtRec ps0 g = max (Max {sum snd P |P. P \<subseteq> set ps \<and> separated g (fst ` P)}) (Max {sum snd P |P. P \<subseteq> set (deleteAround g (fst p) ps) \<and> separated g (fst ` P)} + snd p)

goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ExcessNotAtRec ps0 g = max (Max {sum snd P |P. P \<subseteq> set ps \<and> separated g (fst ` P)}) (Max {sum snd P |P. P \<subseteq> set (deleteAround g (fst p) ps) \<and> separated g (fst ` P)} + snd p)

goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
have "Max (?M ?ps) + snd p =
      Max {(\<Sum>p\<in>P. snd p) + snd p | P. ?S ?ps P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max {sum snd P |P. P \<subseteq> set (deleteAround g (fst p) ps) \<and> separated g (fst ` P)} + snd p = Max {sum snd P + snd p |P. P \<subseteq> set (deleteAround g (fst p) ps) \<and> separated g (fst ` P)}
[PROOF STEP]
by (auto simp add:setcompr_eq_image Max_add_commute[symmetric] sep_ne intro!: arg_cong [where f=Max])
[PROOF STATE]
proof (state)
this:
Max {sum snd P |P. P \<subseteq> set (deleteAround g (fst p) ps) \<and> separated g (fst ` P)} + snd p = Max {sum snd P + snd p |P. P \<subseteq> set (deleteAround g (fst p) ps) \<and> separated g (fst ` P)}

goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Max {sum snd P |P. P \<subseteq> set (deleteAround g (fst p) ps) \<and> separated g (fst ` P)} + snd p = Max {sum snd P + snd p |P. P \<subseteq> set (deleteAround g (fst p) ps) \<and> separated g (fst ` P)}

goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
have "{(\<Sum>p\<in>P. snd p) + snd p |P. ?S ?ps P} =
      {sum snd (insert p P) |P. ?S ?ps P}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {sum snd P + snd p |P. P \<subseteq> set (deleteAround g (fst p) ps) \<and> separated g (fst ` P)} = {sum snd (insert p P) |P. P \<subseteq> set (deleteAround g (fst p) ps) \<and> separated g (fst ` P)}
[PROOF STEP]
using dist Cons
[PROOF STATE]
proof (prove)
using this:
distinct (map fst ps0)
ps0 = p # ps

goal (1 subgoal):
 1. {sum snd P + snd p |P. P \<subseteq> set (deleteAround g (fst p) ps) \<and> separated g (fst ` P)} = {sum snd (insert p P) |P. P \<subseteq> set (deleteAround g (fst p) ps) \<and> separated g (fst ` P)}
[PROOF STEP]
apply (auto simp:delAround_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrakk>ps0 = p # ps; fst p \<notin> fst ` set ps; distinct (map fst ps); P \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)}; separated g (fst ` P)\<rbrakk> \<Longrightarrow> \<exists>Pa. sum snd P + snd p = sum snd (insert p Pa) \<and> Pa \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)} \<and> separated g (fst ` Pa)
 2. \<And>P. \<lbrakk>ps0 = p # ps; fst p \<notin> fst ` set ps; distinct (map fst ps); P \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)}; separated g (fst ` P)\<rbrakk> \<Longrightarrow> \<exists>Pa. sum snd (insert p P) = sum snd Pa + snd p \<and> Pa \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)} \<and> separated g (fst ` Pa)
[PROOF STEP]
apply(rule_tac x=P in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrakk>ps0 = p # ps; fst p \<notin> fst ` set ps; distinct (map fst ps); P \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)}; separated g (fst ` P)\<rbrakk> \<Longrightarrow> sum snd P + snd p = sum snd (insert p P) \<and> P \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)} \<and> separated g (fst ` P)
 2. \<And>P. \<lbrakk>ps0 = p # ps; fst p \<notin> fst ` set ps; distinct (map fst ps); P \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)}; separated g (fst ` P)\<rbrakk> \<Longrightarrow> \<exists>Pa. sum snd (insert p P) = sum snd Pa + snd p \<and> Pa \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)} \<and> separated g (fst ` Pa)
[PROOF STEP]
apply(fastforce intro!: sum.insert[THEN trans,symmetric] elim: finite_subset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>ps0 = p # ps; fst p \<notin> fst ` set ps; distinct (map fst ps); P \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)}; separated g (fst ` P)\<rbrakk> \<Longrightarrow> \<exists>Pa. sum snd (insert p P) = sum snd Pa + snd p \<and> Pa \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)} \<and> separated g (fst ` Pa)
[PROOF STEP]
apply(rule_tac x=P in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>ps0 = p # ps; fst p \<notin> fst ` set ps; distinct (map fst ps); P \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)}; separated g (fst ` P)\<rbrakk> \<Longrightarrow> sum snd (insert p P) = sum snd P + snd p \<and> P \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)} \<and> separated g (fst ` P)
[PROOF STEP]
apply(fastforce intro!: sum.insert[THEN trans] elim: finite_subset)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
{sum snd P + snd p |P. P \<subseteq> set (deleteAround g (fst p) ps) \<and> separated g (fst ` P)} = {sum snd (insert p P) |P. P \<subseteq> set (deleteAround g (fst p) ps) \<and> separated g (fst ` P)}

goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{sum snd P + snd p |P. P \<subseteq> set (deleteAround g (fst p) ps) \<and> separated g (fst ` P)} = {sum snd (insert p P) |P. P \<subseteq> set (deleteAround g (fst p) ps) \<and> separated g (fst ` P)}

goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
have "\<dots> = {sum snd P |P.
            P \<subseteq> insert p (set ?ps) \<and> p \<in> P \<and> separated g (fst ` P)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {sum snd (insert p P) |P. P \<subseteq> set (deleteAround g (fst p) ps) \<and> separated g (fst ` P)} = {sum snd P |P. P \<subseteq> insert p (set (deleteAround g (fst p) ps)) \<and> p \<in> P \<and> separated g (fst ` P)}
[PROOF STEP]
apply(auto simp add:sep_conv[OF mgp] sub1 sub2 delAround_def cong: conj_cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrakk>P \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)}; \<forall>u\<in>P. \<forall>v\<in>P. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v)\<rbrakk> \<Longrightarrow> \<exists>Pa. sum snd (insert p P) = sum snd Pa \<and> Pa \<subseteq> insert p {x \<in> set ps. \<not> close g (fst p) (fst x)} \<and> p \<in> Pa \<and> (\<forall>u\<in>Pa. \<forall>v\<in>Pa. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v))
 2. \<And>P. \<lbrakk>P \<subseteq> insert p {x \<in> set ps. \<not> close g (fst p) (fst x)}; p \<in> P; \<forall>u\<in>P. \<forall>v\<in>P. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v)\<rbrakk> \<Longrightarrow> \<exists>Pa. sum snd P = sum snd (insert p Pa) \<and> Pa \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)} \<and> (\<forall>u\<in>Pa. \<forall>v\<in>Pa. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v))
[PROOF STEP]
apply(rule_tac x = "insert p P" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrakk>P \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)}; \<forall>u\<in>P. \<forall>v\<in>P. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v)\<rbrakk> \<Longrightarrow> sum snd (insert p P) = sum snd (insert p P) \<and> insert p P \<subseteq> insert p {x \<in> set ps. \<not> close g (fst p) (fst x)} \<and> p \<in> insert p P \<and> (\<forall>u\<in>insert p P. \<forall>v\<in>insert p P. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v))
 2. \<And>P. \<lbrakk>P \<subseteq> insert p {x \<in> set ps. \<not> close g (fst p) (fst x)}; p \<in> P; \<forall>u\<in>P. \<forall>v\<in>P. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v)\<rbrakk> \<Longrightarrow> \<exists>Pa. sum snd P = sum snd (insert p Pa) \<and> Pa \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)} \<and> (\<forall>u\<in>Pa. \<forall>v\<in>Pa. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrakk>P \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)}; \<forall>u\<in>P. \<forall>v\<in>P. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v)\<rbrakk> \<Longrightarrow> P \<subseteq> insert p {x \<in> set ps. \<not> close g (fst p) (fst x)} \<and> (\<forall>v\<in>P. fst p \<noteq> fst v \<longrightarrow> \<not> close g (fst p) (fst v)) \<and> (\<forall>u\<in>P. fst u \<noteq> fst p \<longrightarrow> \<not> close g (fst u) (fst p))
 2. \<And>P. \<lbrakk>P \<subseteq> insert p {x \<in> set ps. \<not> close g (fst p) (fst x)}; p \<in> P; \<forall>u\<in>P. \<forall>v\<in>P. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v)\<rbrakk> \<Longrightarrow> \<exists>Pa. sum snd P = sum snd (insert p Pa) \<and> Pa \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)} \<and> (\<forall>u\<in>Pa. \<forall>v\<in>Pa. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v))
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>P. \<lbrakk>P \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)}; \<forall>u\<in>P. \<forall>v\<in>P. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v)\<rbrakk> \<Longrightarrow> P \<subseteq> insert p {x \<in> set ps. \<not> close g (fst p) (fst x)}
 2. \<And>P. \<lbrakk>P \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)}; \<forall>u\<in>P. \<forall>v\<in>P. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v)\<rbrakk> \<Longrightarrow> (\<forall>v\<in>P. fst p \<noteq> fst v \<longrightarrow> \<not> close g (fst p) (fst v)) \<and> (\<forall>u\<in>P. fst u \<noteq> fst p \<longrightarrow> \<not> close g (fst u) (fst p))
 3. \<And>P. \<lbrakk>P \<subseteq> insert p {x \<in> set ps. \<not> close g (fst p) (fst x)}; p \<in> P; \<forall>u\<in>P. \<forall>v\<in>P. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v)\<rbrakk> \<Longrightarrow> \<exists>Pa. sum snd P = sum snd (insert p Pa) \<and> Pa \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)} \<and> (\<forall>u\<in>Pa. \<forall>v\<in>Pa. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrakk>P \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)}; \<forall>u\<in>P. \<forall>v\<in>P. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v)\<rbrakk> \<Longrightarrow> (\<forall>v\<in>P. fst p \<noteq> fst v \<longrightarrow> \<not> close g (fst p) (fst v)) \<and> (\<forall>u\<in>P. fst u \<noteq> fst p \<longrightarrow> \<not> close g (fst u) (fst p))
 2. \<And>P. \<lbrakk>P \<subseteq> insert p {x \<in> set ps. \<not> close g (fst p) (fst x)}; p \<in> P; \<forall>u\<in>P. \<forall>v\<in>P. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v)\<rbrakk> \<Longrightarrow> \<exists>Pa. sum snd P = sum snd (insert p Pa) \<and> Pa \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)} \<and> (\<forall>u\<in>Pa. \<forall>v\<in>Pa. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v))
[PROOF STEP]
using \<open>image fst (set ps) \<subseteq> \<V> g\<close> \<open>fst p : \<V> g\<close>
[PROOF STATE]
proof (prove)
using this:
fst ` set ps \<subseteq> \<V> g
fst p \<in> \<V> g

goal (2 subgoals):
 1. \<And>P. \<lbrakk>P \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)}; \<forall>u\<in>P. \<forall>v\<in>P. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v)\<rbrakk> \<Longrightarrow> (\<forall>v\<in>P. fst p \<noteq> fst v \<longrightarrow> \<not> close g (fst p) (fst v)) \<and> (\<forall>u\<in>P. fst u \<noteq> fst p \<longrightarrow> \<not> close g (fst u) (fst p))
 2. \<And>P. \<lbrakk>P \<subseteq> insert p {x \<in> set ps. \<not> close g (fst p) (fst x)}; p \<in> P; \<forall>u\<in>P. \<forall>v\<in>P. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v)\<rbrakk> \<Longrightarrow> \<exists>Pa. sum snd P = sum snd (insert p Pa) \<and> Pa \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)} \<and> (\<forall>u\<in>Pa. \<forall>v\<in>Pa. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v))
[PROOF STEP]
apply (blast intro:close_sym[OF mgp])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>P \<subseteq> insert p {x \<in> set ps. \<not> close g (fst p) (fst x)}; p \<in> P; \<forall>u\<in>P. \<forall>v\<in>P. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v)\<rbrakk> \<Longrightarrow> \<exists>Pa. sum snd P = sum snd (insert p Pa) \<and> Pa \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)} \<and> (\<forall>u\<in>Pa. \<forall>v\<in>Pa. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v))
[PROOF STEP]
apply(rule_tac x = "P-{p}" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>P \<subseteq> insert p {x \<in> set ps. \<not> close g (fst p) (fst x)}; p \<in> P; \<forall>u\<in>P. \<forall>v\<in>P. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v)\<rbrakk> \<Longrightarrow> sum snd P = sum snd (insert p (P - {p})) \<and> P - {p} \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)} \<and> (\<forall>u\<in>P - {p}. \<forall>v\<in>P - {p}. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v))
[PROOF STEP]
apply (simp add:insert_absorb)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>P \<subseteq> insert p {x \<in> set ps. \<not> close g (fst p) (fst x)}; p \<in> P; \<forall>u\<in>P. \<forall>v\<in>P. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v)\<rbrakk> \<Longrightarrow> P - {p} \<subseteq> {x \<in> set ps. \<not> close g (fst p) (fst x)}
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
{sum snd (insert p P) |P. P \<subseteq> set (deleteAround g (fst p) ps) \<and> separated g (fst ` P)} = {sum snd P |P. P \<subseteq> insert p (set (deleteAround g (fst p) ps)) \<and> p \<in> P \<and> separated g (fst ` P)}

goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{sum snd (insert p P) |P. P \<subseteq> set (deleteAround g (fst p) ps) \<and> separated g (fst ` P)} = {sum snd P |P. P \<subseteq> insert p (set (deleteAround g (fst p) ps)) \<and> p \<in> P \<and> separated g (fst ` P)}

goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
have "\<dots> = {sum snd P |P.
            P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {sum snd P |P. P \<subseteq> insert p (set (deleteAround g (fst p) ps)) \<and> p \<in> P \<and> separated g (fst ` P)} = {sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)}
[PROOF STEP]
using Cons dist
[PROOF STATE]
proof (prove)
using this:
ps0 = p # ps
distinct (map fst ps0)

goal (1 subgoal):
 1. {sum snd P |P. P \<subseteq> insert p (set (deleteAround g (fst p) ps)) \<and> p \<in> P \<and> separated g (fst ` P)} = {sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)}
[PROOF STEP]
apply(auto simp add:sep_conv[OF mgp] sub2 sub3 delAround_def cong: conj_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>ps0 = p # ps; fst p \<notin> fst ` set ps; distinct (map fst ps); P \<subseteq> insert p (set ps); p \<in> P; \<forall>u\<in>P. \<forall>v\<in>P. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v)\<rbrakk> \<Longrightarrow> \<exists>Pa. sum snd P = sum snd Pa \<and> Pa \<subseteq> insert p {x \<in> set ps. \<not> close g (fst p) (fst x)} \<and> p \<in> Pa \<and> (\<forall>u\<in>Pa. \<forall>v\<in>Pa. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v))
[PROOF STEP]
apply(rule_tac x = "P" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>ps0 = p # ps; fst p \<notin> fst ` set ps; distinct (map fst ps); P \<subseteq> insert p (set ps); p \<in> P; \<forall>u\<in>P. \<forall>v\<in>P. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v)\<rbrakk> \<Longrightarrow> sum snd P = sum snd P \<and> P \<subseteq> insert p {x \<in> set ps. \<not> close g (fst p) (fst x)} \<and> p \<in> P \<and> (\<forall>u\<in>P. \<forall>v\<in>P. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>ps0 = p # ps; fst p \<notin> fst ` set ps; distinct (map fst ps); P \<subseteq> insert p (set ps); p \<in> P; \<forall>u\<in>P. \<forall>v\<in>P. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v)\<rbrakk> \<Longrightarrow> P \<subseteq> insert p {x \<in> set ps. \<not> close g (fst p) (fst x)}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
{sum snd P |P. P \<subseteq> insert p (set (deleteAround g (fst p) ps)) \<and> p \<in> P \<and> separated g (fst ` P)} = {sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)}

goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{sum snd P |P. P \<subseteq> insert p (set (deleteAround g (fst p) ps)) \<and> p \<in> P \<and> separated g (fst ` P)} = {sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)}

goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
have "max (Max(?M ps)) (Max \<dots>) = Max(?M ps \<union> {sum snd P |P.
            P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)})"
      (is "_ = Max ?U")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max (Max {sum snd P |P. P \<subseteq> set ps \<and> separated g (fst ` P)}) (Max {sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)}) = Max ({sum snd P |P. P \<subseteq> set ps \<and> separated g (fst ` P)} \<union> {sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. max (Max {sum snd P |P. P \<subseteq> set ps \<and> separated g (fst ` P)}) (Max {sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)}) = Max ({sum snd P |P. P \<subseteq> set ps \<and> separated g (fst ` P)} \<union> {sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)})
[PROOF STEP]
have "{sum snd P |P.
            P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)} \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)} \<noteq> {}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P. p \<in> P \<and> P \<subseteq> insert p (set ps) \<and> separated g (fst ` P)
[PROOF STEP]
apply(rule_tac x="{p}" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> {p} \<and> {p} \<subseteq> insert p (set ps) \<and> separated g (fst ` {p})
[PROOF STEP]
using \<open>fst p : \<V> g\<close>
[PROOF STATE]
proof (prove)
using this:
fst p \<in> \<V> g

goal (1 subgoal):
 1. p \<in> {p} \<and> {p} \<subseteq> insert p (set ps) \<and> separated g (fst ` {p})
[PROOF STEP]
by(simp add:sep_conv[OF mgp])
[PROOF STATE]
proof (state)
this:
{sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)} \<noteq> {}

goal (1 subgoal):
 1. max (Max {sum snd P |P. P \<subseteq> set ps \<and> separated g (fst ` P)}) (Max {sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)}) = Max ({sum snd P |P. P \<subseteq> set ps \<and> separated g (fst ` P)} \<union> {sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)})
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)} \<noteq> {}

goal (1 subgoal):
 1. max (Max {sum snd P |P. P \<subseteq> set ps \<and> separated g (fst ` P)}) (Max {sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)}) = Max ({sum snd P |P. P \<subseteq> set ps \<and> separated g (fst ` P)} \<union> {sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)})
[PROOF STEP]
by(simp add: Max_Un sep_ne)
[PROOF STATE]
proof (state)
this:
max (Max {sum snd P |P. P \<subseteq> set ps \<and> separated g (fst ` P)}) (Max {sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)}) = Max ({sum snd P |P. P \<subseteq> set ps \<and> separated g (fst ` P)} \<union> {sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
max (Max {sum snd P |P. P \<subseteq> set ps \<and> separated g (fst ` P)}) (Max {sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)}) = Max ({sum snd P |P. P \<subseteq> set ps \<and> separated g (fst ` P)} \<union> {sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)})

goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
max (Max {sum snd P |P. P \<subseteq> set ps \<and> separated g (fst ` P)}) (Max {sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)}) = Max ({sum snd P |P. P \<subseteq> set ps \<and> separated g (fst ` P)} \<union> {sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)})

goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
have "?U = ?M ps0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {sum snd P |P. P \<subseteq> set ps \<and> separated g (fst ` P)} \<union> {sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)} = {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
ps0 = p # ps

goal (1 subgoal):
 1. {sum snd P |P. P \<subseteq> set ps \<and> separated g (fst ` P)} \<union> {sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)} = {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
by simp blast
[PROOF STATE]
proof (state)
this:
{sum snd P |P. P \<subseteq> set ps \<and> separated g (fst ` P)} \<union> {sum snd P |P. P \<subseteq> insert p (set ps) \<and> p \<in> P \<and> separated g (fst ` P)} = {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}

goal (1 subgoal):
 1. \<And>a list. ps0 = a # list \<Longrightarrow> ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}

goal (1 subgoal):
 1. ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ExcessNotAtRec ps0 g = Max {sum snd P |P. P \<subseteq> set ps0 \<and> separated g (fst ` P)}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dist_ExcessTab: "distinct (map fst (ExcessTable g (vertices g)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst (ExcessTable g (vertices g)))
[PROOF STEP]
by(simp add:ExcessTable_def vertices_graph o_def)


[STATEMENT]
lemma mono_ExcessTab: "\<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); inv g \<rbrakk> \<Longrightarrow>
  set(ExcessTable g (vertices g)) \<subseteq> set(ExcessTable g' (vertices g'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g\<rbrakk> \<Longrightarrow> set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g'))
[PROOF STEP]
apply(clarsimp simp:ExcessTable_def image_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; x \<in> \<V> g; 0 < ExcessAt g x\<rbrakk> \<Longrightarrow> x \<in> \<V> g' \<and> 0 < ExcessAt g' x \<and> ExcessAt g x = ExcessAt g' x
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; x \<in> \<V> g; 0 < ExcessAt g x\<rbrakk> \<Longrightarrow> x \<in> \<V> g'
 2. \<And>x. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; x \<in> \<V> g; 0 < ExcessAt g x\<rbrakk> \<Longrightarrow> 0 < ExcessAt g' x \<and> ExcessAt g x = ExcessAt g' x
[PROOF STEP]
apply(blast dest:next_plane0_vertices_subset inv_mgp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; x \<in> \<V> g; 0 < ExcessAt g x\<rbrakk> \<Longrightarrow> 0 < ExcessAt g' x \<and> ExcessAt g x = ExcessAt g' x
[PROOF STEP]
apply (clarsimp simp:ExcessAt_def split:if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; x \<in> \<V> g; finalVertex g x; 0 < excessAtType (tri g x) (quad g x) (except g x)\<rbrakk> \<Longrightarrow> finalVertex g' x \<and> (finalVertex g' x \<longrightarrow> 0 < excessAtType (tri g' x) (quad g' x) (except g' x) \<and> excessAtType (tri g x) (quad g x) (except g x) = excessAtType (tri g' x) (quad g' x) (except g' x))
[PROOF STEP]
apply(frule (3) next_plane0_finalVertex_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; x \<in> \<V> g; finalVertex g x; 0 < excessAtType (tri g x) (quad g x) (except g x); finalVertex g' x\<rbrakk> \<Longrightarrow> finalVertex g' x \<and> (finalVertex g' x \<longrightarrow> 0 < excessAtType (tri g' x) (quad g' x) (except g' x) \<and> excessAtType (tri g x) (quad g x) (except g x) = excessAtType (tri g' x) (quad g' x) (except g' x))
[PROOF STEP]
apply(simp add: next_plane0_len_filter_eq tri_def quad_def except_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma close_antimono:
 "\<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); inv g; u \<in> \<V> g; finalVertex g u \<rbrakk> \<Longrightarrow>
  close g' u v \<Longrightarrow> close g u v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; u \<in> \<V> g; finalVertex g u; close g' u v\<rbrakk> \<Longrightarrow> close g u v
[PROOF STEP]
by(simp add:close_def next_plane0_finalVertex_facesAt_eq)


[STATEMENT]
lemma ExcessTab_final:
 "p \<in> set(ExcessTable g (vertices g)) \<Longrightarrow> finalVertex g (fst p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> set (ExcessTable g (vertices g)) \<Longrightarrow> finalVertex g (fst p)
[PROOF STEP]
by(clarsimp simp:ExcessTable_def image_def ExcessAt_def split:if_split_asm)


[STATEMENT]
lemma ExcessTab_vertex:
 "p \<in> set(ExcessTable g (vertices g)) \<Longrightarrow> fst p \<in> \<V> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> set (ExcessTable g (vertices g)) \<Longrightarrow> fst p \<in> \<V> g
[PROOF STEP]
by(clarsimp simp:ExcessTable_def image_def ExcessAt_def split:if_split_asm)


[STATEMENT]
lemma fst_set_ExcessTable_subset:
 "fst ` set (ExcessTable g (vertices g)) \<subseteq> \<V> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ` set (ExcessTable g (vertices g)) \<subseteq> \<V> g
[PROOF STEP]
by(clarsimp simp:ExcessTable_def image_def ExcessAt_def split:if_split_asm)


[STATEMENT]
lemma next_plane0_incr_ExcessNotAt:
 "\<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); inv g \<rbrakk> \<Longrightarrow>
  ExcessNotAt g None \<le> ExcessNotAt g' None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g\<rbrakk> \<Longrightarrow> ExcessNotAt g None \<le> ExcessNotAt g' None
[PROOF STEP]
apply(frule (1) invariantE[OF inv_inv_next_plane0])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'\<rbrakk> \<Longrightarrow> ExcessNotAt g None \<le> ExcessNotAt g' None
[PROOF STEP]
apply(frule (1) mono_ExcessTab)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g'))\<rbrakk> \<Longrightarrow> ExcessNotAt g None \<le> ExcessNotAt g' None
[PROOF STEP]
apply(simp add: ExcessNotAt_def ExcessNotAtRec_conv_Max[OF _ _ dist_ExcessTab]
  fst_set_ExcessTable_subset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g'))\<rbrakk> \<Longrightarrow> Max {sum snd P |P. P \<subseteq> set (ExcessTable g (vertices g)) \<and> separated g (fst ` P)} \<le> Max {sum snd P |P. P \<subseteq> set (ExcessTable g' (vertices g')) \<and> separated g' (fst ` P)}
[PROOF STEP]
apply(rule Max_mono)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g'))\<rbrakk> \<Longrightarrow> {sum snd P |P. P \<subseteq> set (ExcessTable g (vertices g)) \<and> separated g (fst ` P)} \<subseteq> {sum snd P |P. P \<subseteq> set (ExcessTable g' (vertices g')) \<and> separated g' (fst ` P)}
 2. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g'))\<rbrakk> \<Longrightarrow> {sum snd P |P. P \<subseteq> set (ExcessTable g (vertices g)) \<and> separated g (fst ` P)} \<noteq> {}
 3. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g'))\<rbrakk> \<Longrightarrow> finite {sum snd P |P. P \<subseteq> set (ExcessTable g' (vertices g')) \<and> separated g' (fst ` P)}
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g'))\<rbrakk> \<Longrightarrow> {sum snd P |P. P \<subseteq> set (ExcessTable g (vertices g)) \<and> separated g (fst ` P)} \<noteq> {}
 2. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g'))\<rbrakk> \<Longrightarrow> {sum snd P |P. P \<subseteq> set (ExcessTable g (vertices g)) \<and> separated g (fst ` P)} \<subseteq> {sum snd P |P. P \<subseteq> set (ExcessTable g' (vertices g')) \<and> separated g' (fst ` P)}
 3. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g'))\<rbrakk> \<Longrightarrow> finite {sum snd P |P. P \<subseteq> set (ExcessTable g' (vertices g')) \<and> separated g' (fst ` P)}
[PROOF STEP]
apply (simp add: sep_ne)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g'))\<rbrakk> \<Longrightarrow> {sum snd P |P. P \<subseteq> set (ExcessTable g (vertices g)) \<and> separated g (fst ` P)} \<subseteq> {sum snd P |P. P \<subseteq> set (ExcessTable g' (vertices g')) \<and> separated g' (fst ` P)}
 2. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g'))\<rbrakk> \<Longrightarrow> finite {sum snd P |P. P \<subseteq> set (ExcessTable g' (vertices g')) \<and> separated g' (fst ` P)}
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g'))\<rbrakk> \<Longrightarrow> finite {sum snd P |P. P \<subseteq> set (ExcessTable g' (vertices g')) \<and> separated g' (fst ` P)}
 2. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g'))\<rbrakk> \<Longrightarrow> {sum snd P |P. P \<subseteq> set (ExcessTable g (vertices g)) \<and> separated g (fst ` P)} \<subseteq> {sum snd P |P. P \<subseteq> set (ExcessTable g' (vertices g')) \<and> separated g' (fst ` P)}
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g'))\<rbrakk> \<Longrightarrow> {sum snd P |P. P \<subseteq> set (ExcessTable g (vertices g)) \<and> separated g (fst ` P)} \<subseteq> {sum snd P |P. P \<subseteq> set (ExcessTable g' (vertices g')) \<and> separated g' (fst ` P)}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g')); P \<subseteq> set (ExcessTable g (vertices g)); separated g (fst ` P)\<rbrakk> \<Longrightarrow> \<exists>Pa. sum snd P = sum snd Pa \<and> Pa \<subseteq> set (ExcessTable g' (vertices g')) \<and> separated g' (fst ` Pa)
[PROOF STEP]
apply(rule_tac x=P in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g')); P \<subseteq> set (ExcessTable g (vertices g)); separated g (fst ` P)\<rbrakk> \<Longrightarrow> sum snd P = sum snd P \<and> P \<subseteq> set (ExcessTable g' (vertices g')) \<and> separated g' (fst ` P)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g')); P \<subseteq> set (ExcessTable g (vertices g)); separated g (fst ` P)\<rbrakk> \<Longrightarrow> separated g' (fst ` P)
[PROOF STEP]
apply(subgoal_tac "fst ` P \<subseteq> \<V> g'")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g')); P \<subseteq> set (ExcessTable g (vertices g)); separated g (fst ` P); fst ` P \<subseteq> \<V> g'\<rbrakk> \<Longrightarrow> separated g' (fst ` P)
 2. \<And>P. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g')); P \<subseteq> set (ExcessTable g (vertices g)); separated g (fst ` P)\<rbrakk> \<Longrightarrow> fst ` P \<subseteq> \<V> g'
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g')); P \<subseteq> set (ExcessTable g (vertices g)); separated g (fst ` P)\<rbrakk> \<Longrightarrow> fst ` P \<subseteq> \<V> g'
 2. \<And>P. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g')); P \<subseteq> set (ExcessTable g (vertices g)); separated g (fst ` P); fst ` P \<subseteq> \<V> g'\<rbrakk> \<Longrightarrow> separated g' (fst ` P)
[PROOF STEP]
apply (blast dest: ExcessTab_vertex)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g')); P \<subseteq> set (ExcessTable g (vertices g)); separated g (fst ` P); fst ` P \<subseteq> \<V> g'\<rbrakk> \<Longrightarrow> separated g' (fst ` P)
[PROOF STEP]
apply(subgoal_tac "fst ` P \<subseteq> \<V> g")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g')); P \<subseteq> set (ExcessTable g (vertices g)); separated g (fst ` P); fst ` P \<subseteq> \<V> g'; fst ` P \<subseteq> \<V> g\<rbrakk> \<Longrightarrow> separated g' (fst ` P)
 2. \<And>P. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g')); P \<subseteq> set (ExcessTable g (vertices g)); separated g (fst ` P); fst ` P \<subseteq> \<V> g'\<rbrakk> \<Longrightarrow> fst ` P \<subseteq> \<V> g
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g')); P \<subseteq> set (ExcessTable g (vertices g)); separated g (fst ` P); fst ` P \<subseteq> \<V> g'\<rbrakk> \<Longrightarrow> fst ` P \<subseteq> \<V> g
 2. \<And>P. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g')); P \<subseteq> set (ExcessTable g (vertices g)); separated g (fst ` P); fst ` P \<subseteq> \<V> g'; fst ` P \<subseteq> \<V> g\<rbrakk> \<Longrightarrow> separated g' (fst ` P)
[PROOF STEP]
apply (blast dest: ExcessTab_vertex)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g')); P \<subseteq> set (ExcessTable g (vertices g)); separated g (fst ` P); fst ` P \<subseteq> \<V> g'; fst ` P \<subseteq> \<V> g\<rbrakk> \<Longrightarrow> separated g' (fst ` P)
[PROOF STEP]
apply(simp add:sep_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; Invariants.inv g'; set (ExcessTable g (vertices g)) \<subseteq> set (ExcessTable g' (vertices g')); P \<subseteq> set (ExcessTable g (vertices g)); \<forall>u\<in>P. \<forall>v\<in>P. fst u \<noteq> fst v \<longrightarrow> \<not> close g (fst u) (fst v); fst ` P \<subseteq> \<V> g'; fst ` P \<subseteq> \<V> g\<rbrakk> \<Longrightarrow> \<forall>u\<in>P. \<forall>v\<in>P. fst u \<noteq> fst v \<longrightarrow> \<not> close g' (fst u) (fst v)
[PROOF STEP]
apply (blast intro:close_antimono ExcessTab_final ExcessTab_vertex)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma next_plane0_incr_squander_lb:
 "\<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); inv g \<rbrakk> \<Longrightarrow>
  squanderLowerBound g \<le> squanderLowerBound g'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g\<rbrakk> \<Longrightarrow> squanderLowerBound g \<le> squanderLowerBound g'
[PROOF STEP]
apply(simp add:squanderLowerBound_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g\<rbrakk> \<Longrightarrow> faceSquanderLowerBound g + ExcessNotAt g None \<le> faceSquanderLowerBound g' + ExcessNotAt g' None
[PROOF STEP]
apply(frule (1) next_plane0_incr_ExcessNotAt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g' \<in> set (next_plane0\<^bsub>p\<^esub> g); Invariants.inv g; ExcessNotAt g None \<le> ExcessNotAt g' None\<rbrakk> \<Longrightarrow> faceSquanderLowerBound g + ExcessNotAt g None \<le> faceSquanderLowerBound g' + ExcessNotAt g' None
[PROOF STEP]
apply(clarsimp simp add:next_plane0_def split:if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>Invariants.inv g; ExcessNotAt g None \<le> ExcessNotAt g' None; \<not> final g; x \<in> set (nonFinals g); xa \<in> \<V> x; g' \<in> set (generatePolygon xb xa x g); 3 \<le> xb; xb < 4 + p\<rbrakk> \<Longrightarrow> faceSquanderLowerBound g + ExcessNotAt g None \<le> faceSquanderLowerBound g' + ExcessNotAt g' None
[PROOF STEP]
apply(drule (4) genPoly_incr_facesquander_lb)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>Invariants.inv g; ExcessNotAt g None \<le> ExcessNotAt g' None; \<not> final g; x \<in> set (nonFinals g); xa \<in> \<V> x; 3 \<le> xb; xb < 4 + p; faceSquanderLowerBound g + \<d> xb \<le> faceSquanderLowerBound g'\<rbrakk> \<Longrightarrow> faceSquanderLowerBound g + ExcessNotAt g None \<le> faceSquanderLowerBound g' + ExcessNotAt g' None
[PROOF STEP]
apply arith
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done