[STATEMENT]
theorem C10: "\<lfloor>\<^bold>\<exists>x. Godlike x\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>mexistsB Godlike\<rfloor>
[PROOF STEP]
using  P2 P3 P4 P5
[PROOF STATE]
proof (prove)
using this:
\<lfloor>\<lambda>w. \<exists>x. (Necessary x \<^bold>\<and> Abstract x) w\<rfloor>
\<lfloor>\<lambda>w. \<forall>x. (Abstract x \<^bold>\<rightarrow> Dependent x) w\<rfloor>
\<lfloor>\<lambda>w. \<forall>x. Dependent x w \<longrightarrow> (\<exists>xa. (Independent xa \<^bold>\<and> xa explains x) w)\<rfloor>
\<lfloor>\<lambda>w. \<nexists>x xa. (Contingent xa \<^bold>\<and> Necessary x \<^bold>\<and> xa explains x) w\<rfloor>

goal (1 subgoal):
 1. \<lfloor>mexistsB Godlike\<rfloor>
[PROOF STEP]
by blast


[STATEMENT]
lemma True
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
nitpick[satisfy, user_axioms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
oops


[STATEMENT]
lemma "\<lfloor>Necessary x\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>Necessary x\<rfloor>
[PROOF STEP]
nitpick[user_axioms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>Necessary x\<rfloor>
[PROOF STEP]
oops


[STATEMENT]
lemma "\<lfloor>\<phi> \<^bold>\<rightarrow> \<^bold>\<box>\<phi>\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<phi> \<^bold>\<rightarrow> \<^bold>\<box>\<phi>\<rfloor>
[PROOF STEP]
nitpick[user_axioms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>\<phi> \<^bold>\<rightarrow> \<^bold>\<box>\<phi>\<rfloor>
[PROOF STEP]
oops


[STATEMENT]
lemma min_distI2:
    "\<lbrakk> conn v v' ; \<And>d. \<lbrakk> dist v d v'; \<And>d'. dist v d' v' \<Longrightarrow> d \<le> d' \<rbrakk> \<Longrightarrow> Q d \<rbrakk>
      \<Longrightarrow> Q (min_dist v v')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>conn v v'; \<And>d. \<lbrakk>dist v d v'; \<And>d'. dist v d' v' \<Longrightarrow> d \<le> d'\<rbrakk> \<Longrightarrow> Q d\<rbrakk> \<Longrightarrow> Q (min_dist v v')
[PROOF STEP]
unfolding min_dist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>conn v v'; \<And>d. \<lbrakk>dist v d v'; \<And>d'. dist v d' v' \<Longrightarrow> d \<le> d'\<rbrakk> \<Longrightarrow> Q d\<rbrakk> \<Longrightarrow> Q (LEAST d. dist v d v')
[PROOF STEP]
by (rule LeastI2_wellorder[where Q=Q and a="SOME d. dist v d v'"])
       (auto simp: conn_def intro: someI)


[STATEMENT]
lemma min_distI_eq:
    "\<lbrakk> dist v d v'; \<And>d'. dist v d' v' \<Longrightarrow> d \<le> d' \<rbrakk> \<Longrightarrow> min_dist v v' = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dist v d v'; \<And>d'. dist v d' v' \<Longrightarrow> d \<le> d'\<rbrakk> \<Longrightarrow> min_dist v v' = d
[PROOF STEP]
by (force intro: min_distI2 simp: conn_def)


[STATEMENT]
lemma dist_z_iff[simp]: "dist v 0 v' \<longleftrightarrow> v'=v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist v 0 v' = (v' = v)
[PROOF STEP]
by (auto elim: dist.cases intro: dist.intros)


[STATEMENT]
lemma min_dist_z[simp]: "min_dist v v = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min_dist v v = 0
[PROOF STEP]
by (rule min_distI2) (auto intro: dist_z)


[STATEMENT]
lemma min_dist_is_dist: "conn v v' \<Longrightarrow> dist v (min_dist v v') v'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conn v v' \<Longrightarrow> dist v (min_dist v v') v'
[PROOF STEP]
by (auto intro: min_distI2)


[STATEMENT]
lemma min_dist_minD: "dist v d v' \<Longrightarrow> min_dist v v' \<le> d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist v d v' \<Longrightarrow> min_dist v v' \<le> d
[PROOF STEP]
by (auto intro: min_distI2)


[STATEMENT]
lemma min_dist_succ:
    "\<lbrakk> conn v v'; v'' \<in> succ v' \<rbrakk> \<Longrightarrow> min_dist v v'' \<le> Suc (min_dist v v') "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>conn v v'; v'' \<in> succ v'\<rbrakk> \<Longrightarrow> min_dist v v'' \<le> Suc (min_dist v v')
[PROOF STEP]
by (rule min_distI2[where v'=v'])
       (auto elim: dist.cases intro!: min_dist_minD dist_suc)


[STATEMENT]
lemma min_dist_suc:
    assumes c: "conn v v'" "min_dist v v' = Suc d"
    shows "\<exists>v''. conn v v'' \<and> v' \<in> succ v'' \<and> min_dist v v'' = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v''. conn v v'' \<and> v' \<in> succ v'' \<and> min_dist v v'' = d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>v''. conn v v'' \<and> v' \<in> succ v'' \<and> min_dist v v'' = d
[PROOF STEP]
from min_dist_is_dist[OF c(1)]
[PROOF STATE]
proof (chain)
picking this:
dist v (min_dist v v') v'
[PROOF STEP]
have "min_dist v v' = Suc d \<longrightarrow> ?thesis"
[PROOF STATE]
proof (prove)
using this:
dist v (min_dist v v') v'

goal (1 subgoal):
 1. min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. conn v v'' \<and> v' \<in> succ v'' \<and> min_dist v v'' = d)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>min_dist v v' = 0; v' = v\<rbrakk> \<Longrightarrow> min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. conn v v'' \<and> v' \<in> succ v'' \<and> min_dist v v'' = d)
 2. \<And>da vh. \<lbrakk>min_dist v v' = Suc da; dist v da vh; v' \<in> succ vh\<rbrakk> \<Longrightarrow> min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. conn v v'' \<and> v' \<in> succ v'' \<and> min_dist v v'' = d)
[PROOF STEP]
case (dist_suc d' v'')
[PROOF STATE]
proof (state)
this:
min_dist v v' = Suc d'
dist v d' v''
v' \<in> succ v''

goal (2 subgoals):
 1. \<lbrakk>min_dist v v' = 0; v' = v\<rbrakk> \<Longrightarrow> min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. conn v v'' \<and> v' \<in> succ v'' \<and> min_dist v v'' = d)
 2. \<And>da vh. \<lbrakk>min_dist v v' = Suc da; dist v da vh; v' \<in> succ vh\<rbrakk> \<Longrightarrow> min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. conn v v'' \<and> v' \<in> succ v'' \<and> min_dist v v'' = d)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
min_dist v v' = Suc d'
dist v d' v''
v' \<in> succ v''
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
min_dist v v' = Suc d'
dist v d' v''
v' \<in> succ v''

goal (1 subgoal):
 1. min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. conn v v'' \<and> v' \<in> succ v'' \<and> min_dist v v'' = d)
[PROOF STEP]
using min_dist_succ[of v v'' v'] min_dist_minD[of v d v'']
[PROOF STATE]
proof (prove)
using this:
min_dist v v' = Suc d'
dist v d' v''
v' \<in> succ v''
\<lbrakk>conn v v''; v' \<in> succ v''\<rbrakk> \<Longrightarrow> min_dist v v' \<le> Suc (min_dist v v'')
dist v d v'' \<Longrightarrow> min_dist v v'' \<le> d

goal (1 subgoal):
 1. min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. conn v v'' \<and> v' \<in> succ v'' \<and> min_dist v v'' = d)
[PROOF STEP]
by (auto simp: connI)
[PROOF STATE]
proof (state)
this:
min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. conn v v'' \<and> v' \<in> succ v'' \<and> min_dist v v'' = d)

goal (1 subgoal):
 1. \<lbrakk>min_dist v v' = 0; v' = v\<rbrakk> \<Longrightarrow> min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. conn v v'' \<and> v' \<in> succ v'' \<and> min_dist v v'' = d)
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. conn v v'' \<and> v' \<in> succ v'' \<and> min_dist v v'' = d)

goal (1 subgoal):
 1. \<exists>v''. conn v v'' \<and> v' \<in> succ v'' \<and> min_dist v v'' = d
[PROOF STEP]
with c
[PROOF STATE]
proof (chain)
picking this:
conn v v'
min_dist v v' = Suc d
min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. conn v v'' \<and> v' \<in> succ v'' \<and> min_dist v v'' = d)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
conn v v'
min_dist v v' = Suc d
min_dist v v' = Suc d \<longrightarrow> (\<exists>v''. conn v v'' \<and> v' \<in> succ v'' \<and> min_dist v v'' = d)

goal (1 subgoal):
 1. \<exists>v''. conn v v'' \<and> v' \<in> succ v'' \<and> min_dist v v'' = d
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>v''. conn v v'' \<and> v' \<in> succ v'' \<and> min_dist v v'' = d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma min_dist_less:
    assumes "conn src v" "min_dist src v = d" and "d' < d"
    shows "\<exists>v'. conn src v' \<and> min_dist src v' = d'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v'. conn src v' \<and> min_dist src v' = d'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
conn src v
min_dist src v = d
d' < d

goal (1 subgoal):
 1. \<exists>v'. conn src v' \<and> min_dist src v' = d'
[PROOF STEP]
proof (induct d arbitrary: v)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v. \<lbrakk>conn src v; min_dist src v = 0; d' < 0\<rbrakk> \<Longrightarrow> \<exists>v'. conn src v' \<and> min_dist src v' = d'
 2. \<And>d v. \<lbrakk>\<And>v. \<lbrakk>conn src v; min_dist src v = d; d' < d\<rbrakk> \<Longrightarrow> \<exists>v'. conn src v' \<and> min_dist src v' = d'; conn src v; min_dist src v = Suc d; d' < Suc d\<rbrakk> \<Longrightarrow> \<exists>v'. conn src v' \<and> min_dist src v' = d'
[PROOF STEP]
case (Suc d)
[PROOF STATE]
proof (state)
this:
\<lbrakk>conn src ?v; min_dist src ?v = d; d' < d\<rbrakk> \<Longrightarrow> \<exists>v'. conn src v' \<and> min_dist src v' = d'
conn src v
min_dist src v = Suc d
d' < Suc d

goal (2 subgoals):
 1. \<And>v. \<lbrakk>conn src v; min_dist src v = 0; d' < 0\<rbrakk> \<Longrightarrow> \<exists>v'. conn src v' \<and> min_dist src v' = d'
 2. \<And>d v. \<lbrakk>\<And>v. \<lbrakk>conn src v; min_dist src v = d; d' < d\<rbrakk> \<Longrightarrow> \<exists>v'. conn src v' \<and> min_dist src v' = d'; conn src v; min_dist src v = Suc d; d' < Suc d\<rbrakk> \<Longrightarrow> \<exists>v'. conn src v' \<and> min_dist src v' = d'
[PROOF STEP]
with min_dist_suc[of src v]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>conn src v; min_dist src v = Suc ?d\<rbrakk> \<Longrightarrow> \<exists>v''. conn src v'' \<and> v \<in> succ v'' \<and> min_dist src v'' = ?d
\<lbrakk>conn src ?v; min_dist src ?v = d; d' < d\<rbrakk> \<Longrightarrow> \<exists>v'. conn src v' \<and> min_dist src v' = d'
conn src v
min_dist src v = Suc d
d' < Suc d
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>conn src v; min_dist src v = Suc ?d\<rbrakk> \<Longrightarrow> \<exists>v''. conn src v'' \<and> v \<in> succ v'' \<and> min_dist src v'' = ?d
\<lbrakk>conn src ?v; min_dist src ?v = d; d' < d\<rbrakk> \<Longrightarrow> \<exists>v'. conn src v' \<and> min_dist src v' = d'
conn src v
min_dist src v = Suc d
d' < Suc d

goal (1 subgoal):
 1. \<exists>v'. conn src v' \<and> min_dist src v' = d'
[PROOF STEP]
by (cases "d' = d") auto
[PROOF STATE]
proof (state)
this:
\<exists>v'. conn src v' \<and> min_dist src v' = d'

goal (1 subgoal):
 1. \<And>v. \<lbrakk>conn src v; min_dist src v = 0; d' < 0\<rbrakk> \<Longrightarrow> \<exists>v'. conn src v' \<and> min_dist src v' = d'
[PROOF STEP]
qed auto


[STATEMENT]
lemma invar_succ_step:
    assumes "bfs_invar' src dst (False, V, C, N, d)"
    assumes "v\<in>C"
    assumes "v\<noteq>dst"
    shows "bfs_invar' src dst
            (False, V \<union> succ v, C - {v}, N \<union> (succ v - V), d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bfs_invar' src dst (False, V \<union> succ v, C - {v}, N \<union> (succ v - V), d)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bfs_invar' src dst (False, V, C, N, d)
v \<in> C
v \<noteq> dst

goal (1 subgoal):
 1. bfs_invar' src dst (False, V \<union> succ v, C - {v}, N \<union> (succ v - V), d)
[PROOF STEP]
proof (simp (no_asm_use) add: bfs_invar'_def, intro conjI, goal_cases)
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> N \<subseteq> V \<union> succ v
 2. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> succ v - V \<subseteq> V \<union> succ v
 3. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> dst \<in> V \<longrightarrow> dst \<in> C \<and> dst \<noteq> v \<or> dst \<in> N
 4. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> dst \<in> succ v \<longrightarrow> dst \<in> C \<and> dst \<noteq> v \<or> dst \<in> N \<or> dst \<notin> V
 5. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>v\<in>C - {v}. conn src v \<and> min_dist src v = d
 6. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>v\<in>N \<union> (succ v - V). conn src v \<and> min_dist src v = Suc d
 7. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>v\<in>V \<union> succ v. conn src v \<and> min_dist src v \<le> Suc d
 8. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>va. conn src va \<and> min_dist src va \<le> d \<longrightarrow> va \<in> V \<or> va \<in> succ v
 9. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>va. conn src va \<and> min_dist src va = Suc d \<longrightarrow> va \<in> N \<or> va \<in> succ v \<and> va \<notin> V \<or> (\<exists>x\<in>C - {v}. va \<in> succ x) \<and> va \<notin> V \<and> va \<notin> succ v
[PROOF STEP]
case 6
[PROOF STATE]
proof (state)
this:
N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V)
v \<in> C
v \<noteq> dst
bfs_invar' src dst (False, V, C, N, d)
v \<in> C
v \<noteq> dst

goal (9 subgoals):
 1. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> N \<subseteq> V \<union> succ v
 2. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> succ v - V \<subseteq> V \<union> succ v
 3. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> dst \<in> V \<longrightarrow> dst \<in> C \<and> dst \<noteq> v \<or> dst \<in> N
 4. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> dst \<in> succ v \<longrightarrow> dst \<in> C \<and> dst \<noteq> v \<or> dst \<in> N \<or> dst \<notin> V
 5. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>v\<in>C - {v}. conn src v \<and> min_dist src v = d
 6. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>v\<in>N \<union> (succ v - V). conn src v \<and> min_dist src v = Suc d
 7. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>v\<in>V \<union> succ v. conn src v \<and> min_dist src v \<le> Suc d
 8. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>va. conn src va \<and> min_dist src va \<le> d \<longrightarrow> va \<in> V \<or> va \<in> succ v
 9. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>va. conn src va \<and> min_dist src va = Suc d \<longrightarrow> va \<in> N \<or> va \<in> succ v \<and> va \<notin> V \<or> (\<exists>x\<in>C - {v}. va \<in> succ x) \<and> va \<notin> V \<and> va \<notin> succ v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V)
v \<in> C
v \<noteq> dst
bfs_invar' src dst (False, V, C, N, d)
v \<in> C
v \<noteq> dst
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V)
v \<in> C
v \<noteq> dst
bfs_invar' src dst (False, V, C, N, d)
v \<in> C
v \<noteq> dst

goal (1 subgoal):
 1. \<forall>v\<in>N \<union> (succ v - V). conn src v \<and> min_dist src v = Suc d
[PROOF STEP]
by (metis Un_iff Diff_iff connI_succ le_SucE min_dist_succ)
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>N \<union> (succ v - V). conn src v \<and> min_dist src v = Suc d

goal (8 subgoals):
 1. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> N \<subseteq> V \<union> succ v
 2. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> succ v - V \<subseteq> V \<union> succ v
 3. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> dst \<in> V \<longrightarrow> dst \<in> C \<and> dst \<noteq> v \<or> dst \<in> N
 4. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> dst \<in> succ v \<longrightarrow> dst \<in> C \<and> dst \<noteq> v \<or> dst \<in> N \<or> dst \<notin> V
 5. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>v\<in>C - {v}. conn src v \<and> min_dist src v = d
 6. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>v\<in>V \<union> succ v. conn src v \<and> min_dist src v \<le> Suc d
 7. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>va. conn src va \<and> min_dist src va \<le> d \<longrightarrow> va \<in> V \<or> va \<in> succ v
 8. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>va. conn src va \<and> min_dist src va = Suc d \<longrightarrow> va \<in> N \<or> va \<in> succ v \<and> va \<notin> V \<or> (\<exists>x\<in>C - {v}. va \<in> succ x) \<and> va \<notin> V \<and> va \<notin> succ v
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> N \<subseteq> V \<union> succ v
 2. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> succ v - V \<subseteq> V \<union> succ v
 3. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> dst \<in> V \<longrightarrow> dst \<in> C \<and> dst \<noteq> v \<or> dst \<in> N
 4. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> dst \<in> succ v \<longrightarrow> dst \<in> C \<and> dst \<noteq> v \<or> dst \<in> N \<or> dst \<notin> V
 5. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>v\<in>C - {v}. conn src v \<and> min_dist src v = d
 6. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>v\<in>V \<union> succ v. conn src v \<and> min_dist src v \<le> Suc d
 7. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>va. conn src va \<and> min_dist src va \<le> d \<longrightarrow> va \<in> V \<or> va \<in> succ v
 8. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>va. conn src va \<and> min_dist src va = Suc d \<longrightarrow> va \<in> N \<or> va \<in> succ v \<and> va \<notin> V \<or> (\<exists>x\<in>C - {v}. va \<in> succ x) \<and> va \<notin> V \<and> va \<notin> succ v
[PROOF STEP]
case 7
[PROOF STATE]
proof (state)
this:
N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V)
v \<in> C
v \<noteq> dst
bfs_invar' src dst (False, V, C, N, d)
v \<in> C
v \<noteq> dst

goal (8 subgoals):
 1. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> N \<subseteq> V \<union> succ v
 2. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> succ v - V \<subseteq> V \<union> succ v
 3. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> dst \<in> V \<longrightarrow> dst \<in> C \<and> dst \<noteq> v \<or> dst \<in> N
 4. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> dst \<in> succ v \<longrightarrow> dst \<in> C \<and> dst \<noteq> v \<or> dst \<in> N \<or> dst \<notin> V
 5. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>v\<in>C - {v}. conn src v \<and> min_dist src v = d
 6. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>v\<in>V \<union> succ v. conn src v \<and> min_dist src v \<le> Suc d
 7. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>va. conn src va \<and> min_dist src va \<le> d \<longrightarrow> va \<in> V \<or> va \<in> succ v
 8. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>va. conn src va \<and> min_dist src va = Suc d \<longrightarrow> va \<in> N \<or> va \<in> succ v \<and> va \<notin> V \<or> (\<exists>x\<in>C - {v}. va \<in> succ x) \<and> va \<notin> V \<and> va \<notin> succ v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V)
v \<in> C
v \<noteq> dst
bfs_invar' src dst (False, V, C, N, d)
v \<in> C
v \<noteq> dst
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V)
v \<in> C
v \<noteq> dst
bfs_invar' src dst (False, V, C, N, d)
v \<in> C
v \<noteq> dst

goal (1 subgoal):
 1. \<forall>v\<in>V \<union> succ v. conn src v \<and> min_dist src v \<le> Suc d
[PROOF STEP]
by (metis Un_iff connI_succ min_dist_succ)
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>V \<union> succ v. conn src v \<and> min_dist src v \<le> Suc d

goal (7 subgoals):
 1. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> N \<subseteq> V \<union> succ v
 2. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> succ v - V \<subseteq> V \<union> succ v
 3. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> dst \<in> V \<longrightarrow> dst \<in> C \<and> dst \<noteq> v \<or> dst \<in> N
 4. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> dst \<in> succ v \<longrightarrow> dst \<in> C \<and> dst \<noteq> v \<or> dst \<in> N \<or> dst \<notin> V
 5. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>v\<in>C - {v}. conn src v \<and> min_dist src v = d
 6. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>va. conn src va \<and> min_dist src va \<le> d \<longrightarrow> va \<in> V \<or> va \<in> succ v
 7. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> C \<or> dst \<in> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<or> (\<exists>x\<in>C. v \<in> succ x) \<and> v \<notin> V); v \<in> C; v \<noteq> dst; bfs_invar' src dst (False, V, C, N, d); v \<in> C; v \<noteq> dst\<rbrakk> \<Longrightarrow> \<forall>va. conn src va \<and> min_dist src va = Suc d \<longrightarrow> va \<in> N \<or> va \<in> succ v \<and> va \<notin> V \<or> (\<exists>x\<in>C - {v}. va \<in> succ x) \<and> va \<notin> V \<and> va \<notin> succ v
[PROOF STEP]
qed blast+


[STATEMENT]
lemma invar_empty_step:
    assumes "bfs_invar' src dst (False, V, {}, N, d)"
    shows "bfs_invar' src dst (False, V, N, {}, Suc d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bfs_invar' src dst (False, V, N, {}, Suc d)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bfs_invar' src dst (False, V, {}, N, d)

goal (1 subgoal):
 1. bfs_invar' src dst (False, V, N, {}, Suc d)
[PROOF STEP]
proof (simp (no_asm_use) add: bfs_invar'_def, intro conjI impI allI, goal_cases)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); dst \<in> V\<rbrakk> \<Longrightarrow> dst \<in> N
 2. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d)\<rbrakk> \<Longrightarrow> \<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d
 3. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d)\<rbrakk> \<Longrightarrow> \<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc (Suc d)
 4. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v \<le> Suc d\<rbrakk> \<Longrightarrow> v \<in> V
 5. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v = Suc (Suc d)\<rbrakk> \<Longrightarrow> \<exists>x\<in>N. v \<in> succ x
 6. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v = Suc (Suc d)\<rbrakk> \<Longrightarrow> v \<notin> V
[PROOF STEP]
case 3
[PROOF STATE]
proof (state)
this:
N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N)
bfs_invar' src dst (False, V, {}, N, d)

goal (6 subgoals):
 1. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); dst \<in> V\<rbrakk> \<Longrightarrow> dst \<in> N
 2. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d)\<rbrakk> \<Longrightarrow> \<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d
 3. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d)\<rbrakk> \<Longrightarrow> \<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc (Suc d)
 4. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v \<le> Suc d\<rbrakk> \<Longrightarrow> v \<in> V
 5. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v = Suc (Suc d)\<rbrakk> \<Longrightarrow> \<exists>x\<in>N. v \<in> succ x
 6. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v = Suc (Suc d)\<rbrakk> \<Longrightarrow> v \<notin> V
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N)
bfs_invar' src dst (False, V, {}, N, d)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N)
bfs_invar' src dst (False, V, {}, N, d)

goal (1 subgoal):
 1. \<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc (Suc d)
[PROOF STEP]
by (metis le_SucI)
[PROOF STATE]
proof (state)
this:
\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc (Suc d)

goal (5 subgoals):
 1. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); dst \<in> V\<rbrakk> \<Longrightarrow> dst \<in> N
 2. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d)\<rbrakk> \<Longrightarrow> \<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d
 3. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v \<le> Suc d\<rbrakk> \<Longrightarrow> v \<in> V
 4. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v = Suc (Suc d)\<rbrakk> \<Longrightarrow> \<exists>x\<in>N. v \<in> succ x
 5. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v = Suc (Suc d)\<rbrakk> \<Longrightarrow> v \<notin> V
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); dst \<in> V\<rbrakk> \<Longrightarrow> dst \<in> N
 2. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d)\<rbrakk> \<Longrightarrow> \<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d
 3. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v \<le> Suc d\<rbrakk> \<Longrightarrow> v \<in> V
 4. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v = Suc (Suc d)\<rbrakk> \<Longrightarrow> \<exists>x\<in>N. v \<in> succ x
 5. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v = Suc (Suc d)\<rbrakk> \<Longrightarrow> v \<notin> V
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:
N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N)
bfs_invar' src dst (False, V, {}, N, d)
conn src v_ \<and> min_dist src v_ \<le> Suc d

goal (5 subgoals):
 1. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); dst \<in> V\<rbrakk> \<Longrightarrow> dst \<in> N
 2. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d)\<rbrakk> \<Longrightarrow> \<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d
 3. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v \<le> Suc d\<rbrakk> \<Longrightarrow> v \<in> V
 4. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v = Suc (Suc d)\<rbrakk> \<Longrightarrow> \<exists>x\<in>N. v \<in> succ x
 5. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v = Suc (Suc d)\<rbrakk> \<Longrightarrow> v \<notin> V
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N)
bfs_invar' src dst (False, V, {}, N, d)
conn src v_ \<and> min_dist src v_ \<le> Suc d
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N)
bfs_invar' src dst (False, V, {}, N, d)
conn src v_ \<and> min_dist src v_ \<le> Suc d

goal (1 subgoal):
 1. v_ \<in> V
[PROOF STEP]
by (metis le_SucE subsetD)
[PROOF STATE]
proof (state)
this:
v_ \<in> V

goal (4 subgoals):
 1. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); dst \<in> V\<rbrakk> \<Longrightarrow> dst \<in> N
 2. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d)\<rbrakk> \<Longrightarrow> \<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d
 3. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v = Suc (Suc d)\<rbrakk> \<Longrightarrow> \<exists>x\<in>N. v \<in> succ x
 4. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v = Suc (Suc d)\<rbrakk> \<Longrightarrow> v \<notin> V
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); dst \<in> V\<rbrakk> \<Longrightarrow> dst \<in> N
 2. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d)\<rbrakk> \<Longrightarrow> \<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d
 3. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v = Suc (Suc d)\<rbrakk> \<Longrightarrow> \<exists>x\<in>N. v \<in> succ x
 4. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v = Suc (Suc d)\<rbrakk> \<Longrightarrow> v \<notin> V
[PROOF STEP]
case (5 v)
[PROOF STATE]
proof (state)
this:
N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N)
bfs_invar' src dst (False, V, {}, N, d)
conn src v \<and> min_dist src v = Suc (Suc d)

goal (4 subgoals):
 1. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); dst \<in> V\<rbrakk> \<Longrightarrow> dst \<in> N
 2. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d)\<rbrakk> \<Longrightarrow> \<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d
 3. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v = Suc (Suc d)\<rbrakk> \<Longrightarrow> \<exists>x\<in>N. v \<in> succ x
 4. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v = Suc (Suc d)\<rbrakk> \<Longrightarrow> v \<notin> V
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N)
bfs_invar' src dst (False, V, {}, N, d)
conn src v \<and> min_dist src v = Suc (Suc d)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N)
bfs_invar' src dst (False, V, {}, N, d)
conn src v \<and> min_dist src v = Suc (Suc d)

goal (1 subgoal):
 1. \<exists>x\<in>N. v \<in> succ x
[PROOF STEP]
using min_dist_suc[of src v "Suc d"]
[PROOF STATE]
proof (prove)
using this:
N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N)
bfs_invar' src dst (False, V, {}, N, d)
conn src v \<and> min_dist src v = Suc (Suc d)
\<lbrakk>conn src v; min_dist src v = Suc (Suc d)\<rbrakk> \<Longrightarrow> \<exists>v''. conn src v'' \<and> v \<in> succ v'' \<and> min_dist src v'' = Suc d

goal (1 subgoal):
 1. \<exists>x\<in>N. v \<in> succ x
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>N. v \<in> succ x

goal (3 subgoals):
 1. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); dst \<in> V\<rbrakk> \<Longrightarrow> dst \<in> N
 2. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d)\<rbrakk> \<Longrightarrow> \<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d
 3. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v = Suc (Suc d)\<rbrakk> \<Longrightarrow> v \<notin> V
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); dst \<in> V\<rbrakk> \<Longrightarrow> dst \<in> N
 2. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d)\<rbrakk> \<Longrightarrow> \<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d
 3. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v = Suc (Suc d)\<rbrakk> \<Longrightarrow> v \<notin> V
[PROOF STEP]
case 6
[PROOF STATE]
proof (state)
this:
N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N)
bfs_invar' src dst (False, V, {}, N, d)
conn src v_ \<and> min_dist src v_ = Suc (Suc d)

goal (3 subgoals):
 1. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); dst \<in> V\<rbrakk> \<Longrightarrow> dst \<in> N
 2. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d)\<rbrakk> \<Longrightarrow> \<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d
 3. \<And>v. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); conn src v \<and> min_dist src v = Suc (Suc d)\<rbrakk> \<Longrightarrow> v \<notin> V
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N)
bfs_invar' src dst (False, V, {}, N, d)
conn src v_ \<and> min_dist src v_ = Suc (Suc d)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N)
bfs_invar' src dst (False, V, {}, N, d)
conn src v_ \<and> min_dist src v_ = Suc (Suc d)

goal (1 subgoal):
 1. v_ \<notin> V
[PROOF STEP]
by (metis Suc_n_not_le_n)
[PROOF STATE]
proof (state)
this:
v_ \<notin> V

goal (2 subgoals):
 1. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d); dst \<in> V\<rbrakk> \<Longrightarrow> dst \<in> N
 2. \<lbrakk>N \<subseteq> V \<and> (dst \<in> V \<longrightarrow> dst \<in> N) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N); bfs_invar' src dst (False, V, {}, N, d)\<rbrakk> \<Longrightarrow> \<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d
[PROOF STEP]
qed blast+


[STATEMENT]
lemma invar_init: "bfs_invar src dst (False, {src}, {src}, {}, 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bfs_invar src dst (False, {src}, {src}, {}, 0)
[PROOF STEP]
by (auto simp: bfs_invar_def bfs_invar'_def empty_assm_def)
       (metis min_dist_suc min_dist_z_iff)


[STATEMENT]
lemma invar_break:
    assumes "bfs_invar src dst (False, V, C, N, d)"
    assumes "dst\<in>C"
    shows "bfs_invar src dst (True, {}, {}, {}, d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bfs_invar src dst (True, {}, {}, {}, d)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bfs_invar src dst (False, V, C, N, d)
dst \<in> C

goal (1 subgoal):
 1. bfs_invar src dst (True, {}, {}, {}, d)
[PROOF STEP]
unfolding bfs_invar_def bfs_invar'_def empty_assm_def
[PROOF STATE]
proof (prove)
using this:
(let (f, V, C, N, d) = (False, V, C, N, d) in (\<not> f \<longrightarrow> N \<subseteq> V \<and> dst \<notin> V - (C \<union> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<union> (\<Union> (succ ` C) - V))) \<and> (f \<longrightarrow> conn src dst \<and> min_dist src dst = d)) \<and> (let (f, V, C, N, d) = (False, V, C, N, d) in C = {} \<longrightarrow> N = {})
dst \<in> C

goal (1 subgoal):
 1. (let (f, V, C, N, d) = (True, {}, {}, {}, d) in (\<not> f \<longrightarrow> N \<subseteq> V \<and> dst \<notin> V - (C \<union> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<union> (\<Union> (succ ` C) - V))) \<and> (f \<longrightarrow> conn src dst \<and> min_dist src dst = d)) \<and> (let (f, V, C, N, d) = (True, {}, {}, {}, d) in C = {} \<longrightarrow> N = {})
[PROOF STEP]
by auto


[STATEMENT]
lemma invar_final_succeed:
    assumes "bfs_invar' src dst (True, V, C, N, d)"
    shows "min_dist src dst = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min_dist src dst = d
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bfs_invar' src dst (True, V, C, N, d)

goal (1 subgoal):
 1. min_dist src dst = d
[PROOF STEP]
unfolding bfs_invar'_def
[PROOF STATE]
proof (prove)
using this:
let (f, V, C, N, d) = (True, V, C, N, d) in (\<not> f \<longrightarrow> N \<subseteq> V \<and> dst \<notin> V - (C \<union> N) \<and> (\<forall>v\<in>C. conn src v \<and> min_dist src v = d) \<and> (\<forall>v\<in>N. conn src v \<and> min_dist src v = Suc d) \<and> (\<forall>v\<in>V. conn src v \<and> min_dist src v \<le> Suc d) \<and> (\<forall>v. conn src v \<and> min_dist src v \<le> d \<longrightarrow> v \<in> V) \<and> (\<forall>v. conn src v \<and> min_dist src v = Suc d \<longrightarrow> v \<in> N \<union> (\<Union> (succ ` C) - V))) \<and> (f \<longrightarrow> conn src dst \<and> min_dist src dst = d)

goal (1 subgoal):
 1. min_dist src dst = d
[PROOF STEP]
by auto