[STATEMENT]
lemma gen_dfs_fe_inv_imp_pre:
  assumes "gen_dfs_pre E U S V u0"
  assumes "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 it V' False"
  assumes "t\<in>it" "it\<subseteq>E``{u0}" "t\<notin>V'"
  shows "gen_dfs_pre E U (insert u0 S) V' t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gen_dfs_pre E U (insert u0 S) V' t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
gen_dfs_pre E U S V u0
gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 it V' False
t \<in> it
it \<subseteq> E `` {u0}
t \<notin> V'

goal (1 subgoal):
 1. gen_dfs_pre E U (insert u0 S) V' t
[PROOF STEP]
unfolding gen_dfs_fe_inv_def gen_dfs_pre_def
[PROOF STATE]
proof (prove)
using this:
E `` U \<subseteq> U \<and> finite U \<and> V \<subseteq> U \<and> u0 \<in> U \<and> E `` (V - S) \<subseteq> V \<and> u0 \<notin> V \<and> S \<subseteq> V \<and> (\<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*)
(\<not> False \<longrightarrow> E `` (V' - insert u0 S) \<subseteq> V') \<and> E `` {u0} - it \<subseteq> V' \<and> insert u0 V \<subseteq> V' \<and> V' \<subseteq> insert u0 V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)
t \<in> it
it \<subseteq> E `` {u0}
t \<notin> V'

goal (1 subgoal):
 1. E `` U \<subseteq> U \<and> finite U \<and> V' \<subseteq> U \<and> t \<in> U \<and> E `` (V' - insert u0 S) \<subseteq> V' \<and> t \<notin> V' \<and> insert u0 S \<subseteq> V' \<and> (\<forall>v\<in>insert u0 S. (v, t) \<in> (E \<inter> insert u0 S \<times> UNIV)\<^sup>*)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> V' \<subseteq> U \<and> t \<in> U \<and> S \<subseteq> V' \<and> (u0, t) \<in> (E \<inter> insert u0 S \<times> UNIV)\<^sup>* \<and> (\<forall>v\<in>S. (v, t) \<in> (E \<inter> insert u0 S \<times> UNIV)\<^sup>*)
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> V' \<subseteq> U
 2. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> t \<in> U
 3. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> S \<subseteq> V'
 4. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> (u0, t) \<in> (E \<inter> insert u0 S \<times> UNIV)\<^sup>*
 5. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> \<forall>v\<in>S. (v, t) \<in> (E \<inter> insert u0 S \<times> UNIV)\<^sup>*
[PROOF STEP]
apply (blast dest: gen_dfs_upper_aux)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> t \<in> U
 2. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> S \<subseteq> V'
 3. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> (u0, t) \<in> (E \<inter> insert u0 S \<times> UNIV)\<^sup>*
 4. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> \<forall>v\<in>S. (v, t) \<in> (E \<inter> insert u0 S \<times> UNIV)\<^sup>*
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> S \<subseteq> V'
 2. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> (u0, t) \<in> (E \<inter> insert u0 S \<times> UNIV)\<^sup>*
 3. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> \<forall>v\<in>S. (v, t) \<in> (E \<inter> insert u0 S \<times> UNIV)\<^sup>*
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> (u0, t) \<in> (E \<inter> insert u0 S \<times> UNIV)\<^sup>*
 2. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> \<forall>v\<in>S. (v, t) \<in> (E \<inter> insert u0 S \<times> UNIV)\<^sup>*
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> \<forall>v\<in>S. (v, t) \<in> (E \<inter> insert u0 S \<times> UNIV)\<^sup>*
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*; v \<in> S\<rbrakk> \<Longrightarrow> (v, t) \<in> (E \<inter> insert u0 S \<times> UNIV)\<^sup>*
[PROOF STEP]
apply (rule rtrancl_into_rtrancl[where b=u0])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>v. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*; v \<in> S\<rbrakk> \<Longrightarrow> (v, u0) \<in> (E \<inter> insert u0 S \<times> UNIV)\<^sup>*
 2. \<And>v. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*; v \<in> S\<rbrakk> \<Longrightarrow> (u0, t) \<in> E \<inter> insert u0 S \<times> UNIV
[PROOF STEP]
apply (auto intro: rev_subsetD[OF _ rtrancl_mono[where r="E \<inter> S \<times> UNIV"]]) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*; v \<in> S\<rbrakk> \<Longrightarrow> (u0, t) \<in> E \<inter> insert u0 S \<times> UNIV
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma gen_dfs_post_imp_fe_inv:
  assumes "gen_dfs_pre E U S V u0"
  assumes "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 it V' False"
  assumes "t\<in>it" "it\<subseteq>E``{u0}" "t\<notin>V'"
  assumes "gen_dfs_post E U (insert u0 S) V' t V'' cyc"
  shows "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 (it-{t}) V'' cyc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 (it - {t}) V'' cyc
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
gen_dfs_pre E U S V u0
gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 it V' False
t \<in> it
it \<subseteq> E `` {u0}
t \<notin> V'
gen_dfs_post E U (insert u0 S) V' t V'' cyc

goal (1 subgoal):
 1. gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 (it - {t}) V'' cyc
[PROOF STEP]
unfolding gen_dfs_fe_inv_def gen_dfs_post_def gen_dfs_pre_def
[PROOF STATE]
proof (prove)
using this:
E `` U \<subseteq> U \<and> finite U \<and> V \<subseteq> U \<and> u0 \<in> U \<and> E `` (V - S) \<subseteq> V \<and> u0 \<notin> V \<and> S \<subseteq> V \<and> (\<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*)
(\<not> False \<longrightarrow> E `` (V' - insert u0 S) \<subseteq> V') \<and> E `` {u0} - it \<subseteq> V' \<and> insert u0 V \<subseteq> V' \<and> V' \<subseteq> insert u0 V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)
t \<in> it
it \<subseteq> E `` {u0}
t \<notin> V'
(\<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V'') \<and> t \<in> V'' \<and> V' \<subseteq> V'' \<and> V'' \<subseteq> V' \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` {t}

goal (1 subgoal):
 1. (\<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V'') \<and> E `` {u0} - (it - {t}) \<subseteq> V'' \<and> insert u0 V \<subseteq> V'' \<and> V'' \<subseteq> insert u0 V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - (it - {t}) - insert u0 S)
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; \<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V''; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; V'' \<subseteq> V' \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` {t}; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> E `` {u0} - (it - {t}) \<subseteq> V'' \<and> u0 \<in> V'' \<and> V \<subseteq> V'' \<and> V'' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - (it - {t}) - insert u0 S))
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; \<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V''; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; V'' \<subseteq> V' \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` {t}; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> E `` {u0} - (it - {t}) \<subseteq> V''
 2. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; \<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V''; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; V'' \<subseteq> V' \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` {t}; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> u0 \<in> V''
 3. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; \<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V''; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; V'' \<subseteq> V' \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` {t}; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> V \<subseteq> V''
 4. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; \<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V''; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; V'' \<subseteq> V' \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` {t}; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> V'' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - (it - {t}) - insert u0 S))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; \<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V''; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; V'' \<subseteq> V' \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` {t}; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> u0 \<in> V''
 2. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; \<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V''; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; V'' \<subseteq> V' \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` {t}; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> V \<subseteq> V''
 3. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; \<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V''; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; V'' \<subseteq> V' \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` {t}; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> V'' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - (it - {t}) - insert u0 S))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; \<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V''; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; V'' \<subseteq> V' \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` {t}; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> V \<subseteq> V''
 2. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; \<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V''; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; V'' \<subseteq> V' \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` {t}; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> V'' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - (it - {t}) - insert u0 S))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; \<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V''; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; V'' \<subseteq> V' \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` {t}; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> V'' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - (it - {t}) - insert u0 S))
[PROOF STEP]
apply (erule order_trans)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; \<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V''; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> V' \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` {t} \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - (it - {t}) - insert u0 S))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; \<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V''; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - (it - {t}) - insert u0 S)) \<and> (E - UNIV \<times> insert u0 S)\<^sup>* `` {t} \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - (it - {t}) - insert u0 S))
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; \<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V''; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - (it - {t}) - insert u0 S))
 2. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; \<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V''; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> (E - UNIV \<times> insert u0 S)\<^sup>* `` {t} \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - (it - {t}) - insert u0 S))
[PROOF STEP]
apply (erule order_trans[
      where y="insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>*
        `` (E `` {u0} - it - insert u0 S))"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; \<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V''; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; u0 \<in> U; V \<subseteq> V'; E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)) \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - (it - {t}) - insert u0 S))
 2. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; \<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V''; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> (E - UNIV \<times> insert u0 S)\<^sup>* `` {t} \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - (it - {t}) - insert u0 S))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; \<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V''; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> (E - UNIV \<times> insert u0 S)\<^sup>* `` {t} \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - (it - {t}) - insert u0 S))
[PROOF STEP]
apply (cases cyc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; \<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V''; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*; cyc\<rbrakk> \<Longrightarrow> (E - UNIV \<times> insert u0 S)\<^sup>* `` {t} \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - (it - {t}) - insert u0 S))
 2. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; \<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V''; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*; \<not> cyc\<rbrakk> \<Longrightarrow> (E - UNIV \<times> insert u0 S)\<^sup>* `` {t} \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - (it - {t}) - insert u0 S))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*; cyc\<rbrakk> \<Longrightarrow> (E - UNIV \<times> insert u0 S)\<^sup>* `` {t} \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - (it - {t}) - insert u0 S))
 2. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; \<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V''; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*; \<not> cyc\<rbrakk> \<Longrightarrow> (E - UNIV \<times> insert u0 S)\<^sup>* `` {t} \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - (it - {t}) - insert u0 S))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; \<not> cyc \<longrightarrow> E `` (V'' - insert u0 S) \<subseteq> V''; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*; \<not> cyc\<rbrakk> \<Longrightarrow> (E - UNIV \<times> insert u0 S)\<^sup>* `` {t} \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - (it - {t}) - insert u0 S))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> it; it \<subseteq> E `` {u0}; t \<notin> V'; E `` U \<subseteq> U; E `` (V' - insert u0 S) \<subseteq> V'; E `` (V'' - insert u0 S) \<subseteq> V''; finite U; E `` {u0} - it \<subseteq> V'; t \<in> V''; V \<subseteq> U; u0 \<in> V'; V' \<subseteq> V''; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*; \<not> cyc\<rbrakk> \<Longrightarrow> (E - UNIV \<times> insert u0 S)\<^sup>* `` {t} \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - (it - {t}) - insert u0 S))
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma gen_dfs_post_aux:
  assumes 1: "(u0,x)\<in>E"
  assumes 2: "(x,y)\<in>(E - UNIV \<times> insert u0 S)\<^sup>*"
  assumes 3: "S\<subseteq>V" "x\<notin>V"
  shows "(u0, y) \<in> (E - UNIV \<times> S)\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u0, y) \<in> (E - UNIV \<times> S)\<^sup>*
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (u0, y) \<in> (E - UNIV \<times> S)\<^sup>*
[PROOF STEP]
from 1 3
[PROOF STATE]
proof (chain)
picking this:
(u0, x) \<in> E
S \<subseteq> V
x \<notin> V
[PROOF STEP]
have "(u0,x)\<in>(E - UNIV \<times> S)"
[PROOF STATE]
proof (prove)
using this:
(u0, x) \<in> E
S \<subseteq> V
x \<notin> V

goal (1 subgoal):
 1. (u0, x) \<in> E - UNIV \<times> S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(u0, x) \<in> E - UNIV \<times> S

goal (1 subgoal):
 1. (u0, y) \<in> (E - UNIV \<times> S)\<^sup>*
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(u0, x) \<in> E - UNIV \<times> S

goal (1 subgoal):
 1. (u0, y) \<in> (E - UNIV \<times> S)\<^sup>*
[PROOF STEP]
have "(x,y)\<in>(E - UNIV \<times> S)\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> (E - UNIV \<times> S)\<^sup>*
[PROOF STEP]
apply (rule_tac rev_subsetD[OF 2 rtrancl_mono])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E - UNIV \<times> insert u0 S \<subseteq> E - UNIV \<times> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, y) \<in> (E - UNIV \<times> S)\<^sup>*

goal (1 subgoal):
 1. (u0, y) \<in> (E - UNIV \<times> S)\<^sup>*
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(u0, y) \<in> (E - UNIV \<times> S)\<^sup>*
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(u0, y) \<in> (E - UNIV \<times> S)\<^sup>*

goal (1 subgoal):
 1. (u0, y) \<in> (E - UNIV \<times> S)\<^sup>*
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(u0, y) \<in> (E - UNIV \<times> S)\<^sup>*

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gen_dfs_fe_imp_post_brk:
  assumes "gen_dfs_pre E U S V u0"
  assumes "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 it V' True"
  assumes "it\<subseteq>E``{u0}"
  shows "gen_dfs_post E U S V u0 V' True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gen_dfs_post E U S V u0 V' True
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
gen_dfs_pre E U S V u0
gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 it V' True
it \<subseteq> E `` {u0}

goal (1 subgoal):
 1. gen_dfs_post E U S V u0 V' True
[PROOF STEP]
unfolding gen_dfs_pre_def gen_dfs_fe_inv_def gen_dfs_post_def
[PROOF STATE]
proof (prove)
using this:
E `` U \<subseteq> U \<and> finite U \<and> V \<subseteq> U \<and> u0 \<in> U \<and> E `` (V - S) \<subseteq> V \<and> u0 \<notin> V \<and> S \<subseteq> V \<and> (\<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*)
(\<not> True \<longrightarrow> E `` (V' - insert u0 S) \<subseteq> V') \<and> E `` {u0} - it \<subseteq> V' \<and> insert u0 V \<subseteq> V' \<and> V' \<subseteq> insert u0 V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)
it \<subseteq> E `` {u0}

goal (1 subgoal):
 1. (\<not> True \<longrightarrow> E `` (V' - S) \<subseteq> V') \<and> u0 \<in> V' \<and> V \<subseteq> V' \<and> V' \<subseteq> V \<union> (E - UNIV \<times> S)\<^sup>* `` {u0}
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>it \<subseteq> E `` {u0}; E `` U \<subseteq> U; \<not> True \<longrightarrow> E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; insert u0 V \<subseteq> V'; V' \<subseteq> insert u0 V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S); u0 \<in> U; E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> (\<not> True \<longrightarrow> E `` (V' - S) \<subseteq> V') \<and> u0 \<in> V' \<and> V \<subseteq> V' \<and> V' \<subseteq> V \<union> (E - UNIV \<times> S)\<^sup>* `` {u0}
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>it \<subseteq> E `` {u0}; E `` U \<subseteq> U; \<not> True \<longrightarrow> E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; insert u0 V \<subseteq> V'; V' \<subseteq> insert u0 V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S); u0 \<in> U; E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> \<not> True \<longrightarrow> E `` (V' - S) \<subseteq> V'
 2. \<lbrakk>it \<subseteq> E `` {u0}; E `` U \<subseteq> U; \<not> True \<longrightarrow> E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; insert u0 V \<subseteq> V'; V' \<subseteq> insert u0 V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S); u0 \<in> U; E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> u0 \<in> V'
 3. \<lbrakk>it \<subseteq> E `` {u0}; E `` U \<subseteq> U; \<not> True \<longrightarrow> E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; insert u0 V \<subseteq> V'; V' \<subseteq> insert u0 V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S); u0 \<in> U; E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> V \<subseteq> V'
 4. \<lbrakk>it \<subseteq> E `` {u0}; E `` U \<subseteq> U; \<not> True \<longrightarrow> E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; insert u0 V \<subseteq> V'; V' \<subseteq> insert u0 V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S); u0 \<in> U; E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> V' \<subseteq> V \<union> (E - UNIV \<times> S)\<^sup>* `` {u0}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>it \<subseteq> E `` {u0}; E `` U \<subseteq> U; \<not> True \<longrightarrow> E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; insert u0 V \<subseteq> V'; V' \<subseteq> insert u0 V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S); u0 \<in> U; E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> u0 \<in> V'
 2. \<lbrakk>it \<subseteq> E `` {u0}; E `` U \<subseteq> U; \<not> True \<longrightarrow> E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; insert u0 V \<subseteq> V'; V' \<subseteq> insert u0 V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S); u0 \<in> U; E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> V \<subseteq> V'
 3. \<lbrakk>it \<subseteq> E `` {u0}; E `` U \<subseteq> U; \<not> True \<longrightarrow> E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; insert u0 V \<subseteq> V'; V' \<subseteq> insert u0 V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S); u0 \<in> U; E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> V' \<subseteq> V \<union> (E - UNIV \<times> S)\<^sup>* `` {u0}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>it \<subseteq> E `` {u0}; E `` U \<subseteq> U; \<not> True \<longrightarrow> E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; insert u0 V \<subseteq> V'; V' \<subseteq> insert u0 V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S); u0 \<in> U; E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> V \<subseteq> V'
 2. \<lbrakk>it \<subseteq> E `` {u0}; E `` U \<subseteq> U; \<not> True \<longrightarrow> E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; insert u0 V \<subseteq> V'; V' \<subseteq> insert u0 V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S); u0 \<in> U; E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> V' \<subseteq> V \<union> (E - UNIV \<times> S)\<^sup>* `` {u0}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>it \<subseteq> E `` {u0}; E `` U \<subseteq> U; \<not> True \<longrightarrow> E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; insert u0 V \<subseteq> V'; V' \<subseteq> insert u0 V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S); u0 \<in> U; E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> V' \<subseteq> V \<union> (E - UNIV \<times> S)\<^sup>* `` {u0}
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>it \<subseteq> E `` {u0}; E `` U \<subseteq> U; finite U; E `` {u0} - it \<subseteq> V'; V \<subseteq> U; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - it - insert u0 S)); u0 \<in> U; E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*; x \<in> V'; x \<notin> V; u0 \<in> V'; V \<subseteq> V'\<rbrakk> \<Longrightarrow> (u0, x) \<in> (E - UNIV \<times> S)\<^sup>*
[PROOF STEP]
apply (blast intro: gen_dfs_post_aux)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma gen_dfs_fe_inv_imp_post:
  assumes "gen_dfs_pre E U S V u0"
  assumes "gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 {} V' cyc"
  assumes "cyc\<longrightarrow>cyc'"
  shows "gen_dfs_post E U S V u0 V' cyc'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gen_dfs_post E U S V u0 V' cyc'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
gen_dfs_pre E U S V u0
gen_dfs_fe_inv E U (insert u0 S) (insert u0 V) u0 {} V' cyc
cyc \<longrightarrow> cyc'

goal (1 subgoal):
 1. gen_dfs_post E U S V u0 V' cyc'
[PROOF STEP]
unfolding gen_dfs_pre_def gen_dfs_fe_inv_def gen_dfs_post_def
[PROOF STATE]
proof (prove)
using this:
E `` U \<subseteq> U \<and> finite U \<and> V \<subseteq> U \<and> u0 \<in> U \<and> E `` (V - S) \<subseteq> V \<and> u0 \<notin> V \<and> S \<subseteq> V \<and> (\<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*)
(\<not> cyc \<longrightarrow> E `` (V' - insert u0 S) \<subseteq> V') \<and> E `` {u0} - {} \<subseteq> V' \<and> insert u0 V \<subseteq> V' \<and> V' \<subseteq> insert u0 V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - {} - insert u0 S)
cyc \<longrightarrow> cyc'

goal (1 subgoal):
 1. (\<not> cyc' \<longrightarrow> E `` (V' - S) \<subseteq> V') \<and> u0 \<in> V' \<and> V \<subseteq> V' \<and> V' \<subseteq> V \<union> (E - UNIV \<times> S)\<^sup>* `` {u0}
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cyc \<longrightarrow> cyc'; E `` U \<subseteq> U; \<not> cyc \<longrightarrow> E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> (\<not> cyc' \<longrightarrow> E `` (V' - S) \<subseteq> V') \<and> V' \<subseteq> V \<union> (E - UNIV \<times> S)\<^sup>* `` {u0}
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cyc \<longrightarrow> cyc'; E `` U \<subseteq> U; \<not> cyc \<longrightarrow> E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> \<not> cyc' \<longrightarrow> E `` (V' - S) \<subseteq> V'
 2. \<lbrakk>cyc \<longrightarrow> cyc'; E `` U \<subseteq> U; \<not> cyc \<longrightarrow> E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> V' \<subseteq> V \<union> (E - UNIV \<times> S)\<^sup>* `` {u0}
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cyc \<longrightarrow> cyc'; E `` U \<subseteq> U; \<not> cyc \<longrightarrow> E `` (V' - insert u0 S) \<subseteq> V'; finite U; E `` {u0} \<subseteq> V'; V \<subseteq> U; u0 \<in> V'; u0 \<in> U; V \<subseteq> V'; V' \<subseteq> insert u0 (V \<union> (E - UNIV \<times> insert u0 S)\<^sup>* `` (E `` {u0} - insert u0 S)); E `` (V - S) \<subseteq> V; u0 \<notin> V; S \<subseteq> V; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> V' \<subseteq> V \<union> (E - UNIV \<times> S)\<^sup>* `` {u0}
[PROOF STEP]
apply (auto intro: gen_dfs_post_aux) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma gen_dfs_pre_imp_post_brk:
  assumes "gen_dfs_pre E U S V u0"
  shows "gen_dfs_post E U S V u0 (insert u0 V) True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gen_dfs_post E U S V u0 (insert u0 V) True
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
gen_dfs_pre E U S V u0

goal (1 subgoal):
 1. gen_dfs_post E U S V u0 (insert u0 V) True
[PROOF STEP]
unfolding gen_dfs_pre_def gen_dfs_post_def
[PROOF STATE]
proof (prove)
using this:
E `` U \<subseteq> U \<and> finite U \<and> V \<subseteq> U \<and> u0 \<in> U \<and> E `` (V - S) \<subseteq> V \<and> u0 \<notin> V \<and> S \<subseteq> V \<and> (\<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*)

goal (1 subgoal):
 1. (\<not> True \<longrightarrow> E `` (insert u0 V - S) \<subseteq> insert u0 V) \<and> u0 \<in> insert u0 V \<and> V \<subseteq> insert u0 V \<and> insert u0 V \<subseteq> V \<union> (E - UNIV \<times> S)\<^sup>* `` {u0}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma gen_dfs_post_imp_reachable:
  assumes "gen_dfs_pre E U S V0 u0"
  assumes "gen_dfs_post E U S V0 u0 V brk"
  shows "V \<subseteq> V0 \<union> E\<^sup>*``{u0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<subseteq> V0 \<union> E\<^sup>* `` {u0}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
gen_dfs_pre E U S V0 u0
gen_dfs_post E U S V0 u0 V brk

goal (1 subgoal):
 1. V \<subseteq> V0 \<union> E\<^sup>* `` {u0}
[PROOF STEP]
unfolding gen_dfs_post_def gen_dfs_pre_def
[PROOF STATE]
proof (prove)
using this:
E `` U \<subseteq> U \<and> finite U \<and> V0 \<subseteq> U \<and> u0 \<in> U \<and> E `` (V0 - S) \<subseteq> V0 \<and> u0 \<notin> V0 \<and> S \<subseteq> V0 \<and> (\<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*)
(\<not> brk \<longrightarrow> E `` (V - S) \<subseteq> V) \<and> u0 \<in> V \<and> V0 \<subseteq> V \<and> V \<subseteq> V0 \<union> (E - UNIV \<times> S)\<^sup>* `` {u0}

goal (1 subgoal):
 1. V \<subseteq> V0 \<union> E\<^sup>* `` {u0}
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> V; x \<notin> V0; E `` U \<subseteq> U; \<not> brk \<longrightarrow> E `` (V - S) \<subseteq> V; finite U; u0 \<in> V; V0 \<subseteq> U; V0 \<subseteq> V; V \<subseteq> V0 \<union> (E - UNIV \<times> S)\<^sup>* `` {u0}; u0 \<in> U; E `` (V0 - S) \<subseteq> V0; u0 \<notin> V0; S \<subseteq> V0; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> (u0, x) \<in> E\<^sup>*
[PROOF STEP]
apply (blast intro: rev_subsetD[OF _ rtrancl_mono])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma gen_dfs_post_imp_complete:
  assumes "gen_dfs_pre E U {} V0 u0"
  assumes "gen_dfs_post E U {} V0 u0 V False"
  shows "V0 \<union> E\<^sup>*``{u0} \<subseteq> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V0 \<union> E\<^sup>* `` {u0} \<subseteq> V
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
gen_dfs_pre E U {} V0 u0
gen_dfs_post E U {} V0 u0 V False

goal (1 subgoal):
 1. V0 \<union> E\<^sup>* `` {u0} \<subseteq> V
[PROOF STEP]
unfolding gen_dfs_post_def gen_dfs_pre_def
[PROOF STATE]
proof (prove)
using this:
E `` U \<subseteq> U \<and> finite U \<and> V0 \<subseteq> U \<and> u0 \<in> U \<and> E `` (V0 - {}) \<subseteq> V0 \<and> u0 \<notin> V0 \<and> {} \<subseteq> V0 \<and> (\<forall>v\<in>{}. (v, u0) \<in> (E \<inter> {} \<times> UNIV)\<^sup>*)
(\<not> False \<longrightarrow> E `` (V - {}) \<subseteq> V) \<and> u0 \<in> V \<and> V0 \<subseteq> V \<and> V \<subseteq> V0 \<union> (E - UNIV \<times> {})\<^sup>* `` {u0}

goal (1 subgoal):
 1. V0 \<union> E\<^sup>* `` {u0} \<subseteq> V
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>(u0, x) \<in> E\<^sup>*; E `` U \<subseteq> U; E `` V \<subseteq> V; finite U; u0 \<in> V; V0 \<subseteq> U; V0 \<subseteq> V; V \<subseteq> V0 \<union> E\<^sup>* `` {u0}; u0 \<in> U; E `` V0 \<subseteq> V0; u0 \<notin> V0\<rbrakk> \<Longrightarrow> x \<in> V
[PROOF STEP]
apply (blast dest: Image_closed_trancl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma gen_dfs_post_imp_eq:
  assumes "gen_dfs_pre E U {} V0 u0"
  assumes "gen_dfs_post E U {} V0 u0 V False"
  shows "V = V0 \<union> E\<^sup>*``{u0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V = V0 \<union> E\<^sup>* `` {u0}
[PROOF STEP]
using gen_dfs_post_imp_reachable[OF assms] gen_dfs_post_imp_complete[OF assms]
[PROOF STATE]
proof (prove)
using this:
V \<subseteq> V0 \<union> E\<^sup>* `` {u0}
V0 \<union> E\<^sup>* `` {u0} \<subseteq> V

goal (1 subgoal):
 1. V = V0 \<union> E\<^sup>* `` {u0}
[PROOF STEP]
by blast


[STATEMENT]
lemma gen_dfs_post_imp_below_U:
  assumes "gen_dfs_pre E U S V0 u0"
  assumes "gen_dfs_post E U S V0 u0 V False"
  shows "V \<subseteq> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<subseteq> U
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
gen_dfs_pre E U S V0 u0
gen_dfs_post E U S V0 u0 V False

goal (1 subgoal):
 1. V \<subseteq> U
[PROOF STEP]
unfolding gen_dfs_pre_def gen_dfs_post_def
[PROOF STATE]
proof (prove)
using this:
E `` U \<subseteq> U \<and> finite U \<and> V0 \<subseteq> U \<and> u0 \<in> U \<and> E `` (V0 - S) \<subseteq> V0 \<and> u0 \<notin> V0 \<and> S \<subseteq> V0 \<and> (\<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*)
(\<not> False \<longrightarrow> E `` (V - S) \<subseteq> V) \<and> u0 \<in> V \<and> V0 \<subseteq> V \<and> V \<subseteq> V0 \<union> (E - UNIV \<times> S)\<^sup>* `` {u0}

goal (1 subgoal):
 1. V \<subseteq> U
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<in> V; E `` U \<subseteq> U; E `` (V - S) \<subseteq> V; finite U; u0 \<in> V; V0 \<subseteq> U; V0 \<subseteq> V; V \<subseteq> V0 \<union> (E - UNIV \<times> S)\<^sup>* `` {u0}; u0 \<in> U; E `` (V0 - S) \<subseteq> V0; u0 \<notin> V0; S \<subseteq> V0; \<forall>v\<in>S. (v, u0) \<in> (E \<inter> S \<times> UNIV)\<^sup>*\<rbrakk> \<Longrightarrow> x \<in> U
[PROOF STEP]
apply (blast intro: rev_subsetD[OF _ rtrancl_mono] dest: Image_closed_trancl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma gen_dfs_post_imp_outer:
  assumes "gen_dfs_outer E U V0 it Vis0 False"
  assumes "gen_dfs_post E U {} Vis0 v0 Vis False"
  assumes "v0 \<in> it" "it \<subseteq> V0" "v0 \<notin> Vis0"
  shows "gen_dfs_outer E U V0 (it - {v0}) Vis False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gen_dfs_outer E U V0 (it - {v0}) Vis False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gen_dfs_outer E U V0 (it - {v0}) Vis False
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gen_dfs_outer E U V0 (it - {v0}) Vis False
[PROOF STEP]
assume "v0 \<in> it" "it \<subseteq> V0" "V0 \<subseteq> U" "E `` U \<subseteq> U"
[PROOF STATE]
proof (state)
this:
v0 \<in> it
it \<subseteq> V0
V0 \<subseteq> U
E `` U \<subseteq> U

goal (1 subgoal):
 1. gen_dfs_outer E U V0 (it - {v0}) Vis False
[PROOF STEP]
hence "E\<^sup>* `` {v0} \<subseteq> U"
[PROOF STATE]
proof (prove)
using this:
v0 \<in> it
it \<subseteq> V0
V0 \<subseteq> U
E `` U \<subseteq> U

goal (1 subgoal):
 1. E\<^sup>* `` {v0} \<subseteq> U
[PROOF STEP]
by (metis (full_types) empty_subsetI insert_subset rtrancl_reachable_induct subset_trans)
[PROOF STATE]
proof (state)
this:
E\<^sup>* `` {v0} \<subseteq> U

goal (1 subgoal):
 1. gen_dfs_outer E U V0 (it - {v0}) Vis False
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>v0 \<in> it; it \<subseteq> V0; V0 \<subseteq> U; E `` U \<subseteq> U\<rbrakk> \<Longrightarrow> E\<^sup>* `` {v0} \<subseteq> U

goal (1 subgoal):
 1. gen_dfs_outer E U V0 (it - {v0}) Vis False
[PROOF STEP]
note AUX=this
[PROOF STATE]
proof (state)
this:
\<lbrakk>v0 \<in> it; it \<subseteq> V0; V0 \<subseteq> U; E `` U \<subseteq> U\<rbrakk> \<Longrightarrow> E\<^sup>* `` {v0} \<subseteq> U

goal (1 subgoal):
 1. gen_dfs_outer E U V0 (it - {v0}) Vis False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gen_dfs_outer E U V0 (it - {v0}) Vis False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
gen_dfs_outer E U V0 it Vis0 False
gen_dfs_post E U {} Vis0 v0 Vis False
v0 \<in> it
it \<subseteq> V0
v0 \<notin> Vis0

goal (1 subgoal):
 1. gen_dfs_outer E U V0 (it - {v0}) Vis False
[PROOF STEP]
unfolding gen_dfs_outer_def gen_dfs_post_def
[PROOF STATE]
proof (prove)
using this:
V0 \<subseteq> U \<and> E `` U \<subseteq> U \<and> finite U \<and> Vis0 \<subseteq> U \<and> (\<not> False \<longrightarrow> E `` Vis0 \<subseteq> Vis0) \<and> V0 - it \<subseteq> Vis0
(\<not> False \<longrightarrow> E `` (Vis - {}) \<subseteq> Vis) \<and> v0 \<in> Vis \<and> Vis0 \<subseteq> Vis \<and> Vis \<subseteq> Vis0 \<union> (E - UNIV \<times> {})\<^sup>* `` {v0}
v0 \<in> it
it \<subseteq> V0
v0 \<notin> Vis0

goal (1 subgoal):
 1. V0 \<subseteq> U \<and> E `` U \<subseteq> U \<and> finite U \<and> Vis \<subseteq> U \<and> (\<not> False \<longrightarrow> E `` Vis \<subseteq> Vis) \<and> V0 - (it - {v0}) \<subseteq> Vis
[PROOF STEP]
using AUX
[PROOF STATE]
proof (prove)
using this:
V0 \<subseteq> U \<and> E `` U \<subseteq> U \<and> finite U \<and> Vis0 \<subseteq> U \<and> (\<not> False \<longrightarrow> E `` Vis0 \<subseteq> Vis0) \<and> V0 - it \<subseteq> Vis0
(\<not> False \<longrightarrow> E `` (Vis - {}) \<subseteq> Vis) \<and> v0 \<in> Vis \<and> Vis0 \<subseteq> Vis \<and> Vis \<subseteq> Vis0 \<union> (E - UNIV \<times> {})\<^sup>* `` {v0}
v0 \<in> it
it \<subseteq> V0
v0 \<notin> Vis0
\<lbrakk>v0 \<in> it; it \<subseteq> V0; V0 \<subseteq> U; E `` U \<subseteq> U\<rbrakk> \<Longrightarrow> E\<^sup>* `` {v0} \<subseteq> U

goal (1 subgoal):
 1. V0 \<subseteq> U \<and> E `` U \<subseteq> U \<and> finite U \<and> Vis \<subseteq> U \<and> (\<not> False \<longrightarrow> E `` Vis \<subseteq> Vis) \<and> V0 - (it - {v0}) \<subseteq> Vis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
gen_dfs_outer E U V0 (it - {v0}) Vis False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gen_dfs_outer_already_vis:
  assumes "v0 \<in> it" "it \<subseteq> V0" "v0 \<in> V"
  assumes "gen_dfs_outer E U V0 it V False"
  shows "gen_dfs_outer E U V0 (it - {v0}) V False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gen_dfs_outer E U V0 (it - {v0}) V False
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
v0 \<in> it
it \<subseteq> V0
v0 \<in> V
gen_dfs_outer E U V0 it V False

goal (1 subgoal):
 1. gen_dfs_outer E U V0 (it - {v0}) V False
[PROOF STEP]
unfolding gen_dfs_outer_def
[PROOF STATE]
proof (prove)
using this:
v0 \<in> it
it \<subseteq> V0
v0 \<in> V
V0 \<subseteq> U \<and> E `` U \<subseteq> U \<and> finite U \<and> V \<subseteq> U \<and> (\<not> False \<longrightarrow> E `` V \<subseteq> V) \<and> V0 - it \<subseteq> V

goal (1 subgoal):
 1. V0 \<subseteq> U \<and> E `` U \<subseteq> U \<and> finite U \<and> V \<subseteq> U \<and> (\<not> False \<longrightarrow> E `` V \<subseteq> V) \<and> V0 - (it - {v0}) \<subseteq> V
[PROOF STEP]
by auto


[STATEMENT]
lemma red_dfs_inv_initial:
  assumes "finite (E\<^sup>*``V0)"
  shows "red_dfs_inv E (E\<^sup>*``V0) {} {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. red_dfs_inv E (E\<^sup>* `` V0) {} {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite (E\<^sup>* `` V0)

goal (1 subgoal):
 1. red_dfs_inv E (E\<^sup>* `` V0) {} {}
[PROOF STEP]
unfolding red_dfs_inv_def
[PROOF STATE]
proof (prove)
using this:
finite (E\<^sup>* `` V0)

goal (1 subgoal):
 1. E `` E\<^sup>* `` V0 \<subseteq> E\<^sup>* `` V0 \<and> finite (E\<^sup>* `` V0) \<and> {} \<subseteq> E\<^sup>* `` V0 \<and> E `` {} \<subseteq> {} \<and> E `` {} \<inter> {} = {}
[PROOF STEP]
apply (auto intro: rev_ImageI)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done