[STATEMENT]
lemma param_dfs_variant_step:
    assumes A: "DFS_invar G param s" "cond s" "nofail it_dfs"
    shows "step s \<le> SPEC (\<lambda>s'. (s',s)\<in>param_dfs_variant)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step s \<le> SPEC (\<lambda>s'. (s', s) \<in> param_dfs_variant)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. step s \<le> SPEC (\<lambda>s'. (s', s) \<in> param_dfs_variant)
[PROOF STEP]
interpret DFS_invar G param s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DFS_invar G param s
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. step s \<le> SPEC (\<lambda>s'. (s', s) \<in> param_dfs_variant)
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
DFS_invar G param s
cond s
nofail it_dfs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
DFS_invar G param s
cond s
nofail it_dfs

goal (1 subgoal):
 1. step s \<le> SPEC (\<lambda>s'. (s', s) \<in> param_dfs_variant)
[PROOF STEP]
unfolding rwof_eq_DFS_invar[symmetric] it_dfs_def
[PROOF STATE]
proof (prove)
using this:
rwof init cond step s
cond s
nofail (init \<bind> WHILE cond step)

goal (1 subgoal):
 1. step s \<le> SPEC (\<lambda>s'. (s', s) \<in> param_dfs_variant)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rwof init cond step s; cond s; nofail (init \<bind> WHILE cond step)\<rbrakk> \<Longrightarrow> step s \<le> SPEC (\<lambda>s'. (s', s) \<in> param_dfs_variant)
[PROOF STEP]
apply (drule (2) WHILE_nofail_imp_rwof_nofail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rwof init cond step s; cond s; nofail (step s)\<rbrakk> \<Longrightarrow> step s \<le> SPEC (\<lambda>s'. (s', s) \<in> param_dfs_variant)
[PROOF STEP]
unfolding step_def get_new_root_def do_defs get_pending_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))))\<rbrakk> \<Longrightarrow> (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) \<le> SPEC (\<lambda>s'. (s', s) \<in> param_dfs_variant)
[PROOF STEP]
unfolding param_dfs_variant_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))))\<rbrakk> \<Longrightarrow> (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s))))
[PROOF STEP]
apply refine_vcg
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>x. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); is_empty_stack s; x \<in> V0 \<and> \<not> is_discovered x s\<rbrakk> \<Longrightarrow> on_new_root param x (new_root x s) \<le> SPEC (\<lambda>e. RETURN (new_root x s\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 2. \<And>a b aa ba. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} = {}; (hd (stack s), None, s) = (a, b); b = (aa, ba); aa = None\<rbrakk> \<Longrightarrow> on_finish param a (finish a ba) \<le> SPEC (\<lambda>e. RETURN (finish a ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 3. \<And>a b aa ba x. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} = {}; (hd (stack s), None, s) = (a, b); b = (aa, ba); aa = Some x; is_discovered x ba; is_finished x ba\<rbrakk> \<Longrightarrow> on_cross_edge param a x (cross_edge a x ba) \<le> SPEC (\<lambda>e. RETURN (cross_edge a x ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 4. \<And>a b aa ba x. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} = {}; (hd (stack s), None, s) = (a, b); b = (aa, ba); aa = Some x; is_discovered x ba; \<not> is_finished x ba\<rbrakk> \<Longrightarrow> on_back_edge param a x (back_edge a x ba) \<le> SPEC (\<lambda>e. RETURN (back_edge a x ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 5. \<And>a b aa ba x. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} = {}; (hd (stack s), None, s) = (a, b); b = (aa, ba); aa = Some x; \<not> is_discovered x ba\<rbrakk> \<Longrightarrow> on_discover param a x (discover a x ba) \<le> SPEC (\<lambda>e. RETURN (discover a x ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 6. \<And>x a b aa ba. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (a, b); b = (aa, ba); aa = None\<rbrakk> \<Longrightarrow> on_finish param a (finish a ba) \<le> SPEC (\<lambda>e. RETURN (finish a ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 7. \<And>x a b aa ba xa. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (a, b); b = (aa, ba); aa = Some xa; is_discovered xa ba; is_finished xa ba\<rbrakk> \<Longrightarrow> on_cross_edge param a xa (cross_edge a xa ba) \<le> SPEC (\<lambda>e. RETURN (cross_edge a xa ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 8. \<And>x a b aa ba xa. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (a, b); b = (aa, ba); aa = Some xa; is_discovered xa ba; \<not> is_finished xa ba\<rbrakk> \<Longrightarrow> on_back_edge param a xa (back_edge a xa ba) \<le> SPEC (\<lambda>e. RETURN (back_edge a xa ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 9. \<And>x a b aa ba xa. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (a, b); b = (aa, ba); aa = Some xa; \<not> is_discovered xa ba\<rbrakk> \<Longrightarrow> on_discover param a xa (discover a xa ba) \<le> SPEC (\<lambda>e. RETURN (discover a xa ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
[PROOF STEP]
using discovered_reachable
[PROOF STATE]
proof (prove)
using this:
dom (discovered s) \<subseteq> reachable

goal (9 subgoals):
 1. \<And>x. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); is_empty_stack s; x \<in> V0 \<and> \<not> is_discovered x s\<rbrakk> \<Longrightarrow> on_new_root param x (new_root x s) \<le> SPEC (\<lambda>e. RETURN (new_root x s\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 2. \<And>a b aa ba. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} = {}; (hd (stack s), None, s) = (a, b); b = (aa, ba); aa = None\<rbrakk> \<Longrightarrow> on_finish param a (finish a ba) \<le> SPEC (\<lambda>e. RETURN (finish a ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 3. \<And>a b aa ba x. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} = {}; (hd (stack s), None, s) = (a, b); b = (aa, ba); aa = Some x; is_discovered x ba; is_finished x ba\<rbrakk> \<Longrightarrow> on_cross_edge param a x (cross_edge a x ba) \<le> SPEC (\<lambda>e. RETURN (cross_edge a x ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 4. \<And>a b aa ba x. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} = {}; (hd (stack s), None, s) = (a, b); b = (aa, ba); aa = Some x; is_discovered x ba; \<not> is_finished x ba\<rbrakk> \<Longrightarrow> on_back_edge param a x (back_edge a x ba) \<le> SPEC (\<lambda>e. RETURN (back_edge a x ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 5. \<And>a b aa ba x. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} = {}; (hd (stack s), None, s) = (a, b); b = (aa, ba); aa = Some x; \<not> is_discovered x ba\<rbrakk> \<Longrightarrow> on_discover param a x (discover a x ba) \<le> SPEC (\<lambda>e. RETURN (discover a x ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 6. \<And>x a b aa ba. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (a, b); b = (aa, ba); aa = None\<rbrakk> \<Longrightarrow> on_finish param a (finish a ba) \<le> SPEC (\<lambda>e. RETURN (finish a ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 7. \<And>x a b aa ba xa. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (a, b); b = (aa, ba); aa = Some xa; is_discovered xa ba; is_finished xa ba\<rbrakk> \<Longrightarrow> on_cross_edge param a xa (cross_edge a xa ba) \<le> SPEC (\<lambda>e. RETURN (cross_edge a xa ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 8. \<And>x a b aa ba xa. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (a, b); b = (aa, ba); aa = Some xa; is_discovered xa ba; \<not> is_finished xa ba\<rbrakk> \<Longrightarrow> on_back_edge param a xa (back_edge a xa ba) \<le> SPEC (\<lambda>e. RETURN (back_edge a xa ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 9. \<And>x a b aa ba xa. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (a, b); b = (aa, ba); aa = Some xa; \<not> is_discovered xa ba\<rbrakk> \<Longrightarrow> on_discover param a xa (discover a xa ba) \<le> SPEC (\<lambda>e. RETURN (discover a xa ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
[PROOF STEP]
(* TODO: Clean, up. *)
        (* FIXME: auto-steps take loooong *)
[PROOF STATE]
proof (prove)
using this:
dom (discovered s) \<subseteq> reachable

goal (9 subgoals):
 1. \<And>x. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); is_empty_stack s; x \<in> V0 \<and> \<not> is_discovered x s\<rbrakk> \<Longrightarrow> on_new_root param x (new_root x s) \<le> SPEC (\<lambda>e. RETURN (new_root x s\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 2. \<And>a b aa ba. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} = {}; (hd (stack s), None, s) = (a, b); b = (aa, ba); aa = None\<rbrakk> \<Longrightarrow> on_finish param a (finish a ba) \<le> SPEC (\<lambda>e. RETURN (finish a ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 3. \<And>a b aa ba x. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} = {}; (hd (stack s), None, s) = (a, b); b = (aa, ba); aa = Some x; is_discovered x ba; is_finished x ba\<rbrakk> \<Longrightarrow> on_cross_edge param a x (cross_edge a x ba) \<le> SPEC (\<lambda>e. RETURN (cross_edge a x ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 4. \<And>a b aa ba x. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} = {}; (hd (stack s), None, s) = (a, b); b = (aa, ba); aa = Some x; is_discovered x ba; \<not> is_finished x ba\<rbrakk> \<Longrightarrow> on_back_edge param a x (back_edge a x ba) \<le> SPEC (\<lambda>e. RETURN (back_edge a x ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 5. \<And>a b aa ba x. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} = {}; (hd (stack s), None, s) = (a, b); b = (aa, ba); aa = Some x; \<not> is_discovered x ba\<rbrakk> \<Longrightarrow> on_discover param a x (discover a x ba) \<le> SPEC (\<lambda>e. RETURN (discover a x ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 6. \<And>x a b aa ba. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (a, b); b = (aa, ba); aa = None\<rbrakk> \<Longrightarrow> on_finish param a (finish a ba) \<le> SPEC (\<lambda>e. RETURN (finish a ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 7. \<And>x a b aa ba xa. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (a, b); b = (aa, ba); aa = Some xa; is_discovered xa ba; is_finished xa ba\<rbrakk> \<Longrightarrow> on_cross_edge param a xa (cross_edge a xa ba) \<le> SPEC (\<lambda>e. RETURN (cross_edge a xa ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 8. \<And>x a b aa ba xa. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (a, b); b = (aa, ba); aa = Some xa; is_discovered xa ba; \<not> is_finished xa ba\<rbrakk> \<Longrightarrow> on_back_edge param a xa (back_edge a xa ba) \<le> SPEC (\<lambda>e. RETURN (back_edge a xa ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 9. \<And>x a b aa ba xa. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (a, b); b = (aa, ba); aa = Some xa; \<not> is_discovered xa ba\<rbrakk> \<Longrightarrow> on_discover param a xa (discover a xa ba) \<le> SPEC (\<lambda>e. RETURN (discover a xa ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
[PROOF STEP]
apply (auto
        split: option.splits
        simp: refine_pw_simps pw_le_iff is_discovered_def finite_psupset_def
      ) [1]
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>a b aa ba. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} = {}; (hd (stack s), None, s) = (a, b); b = (aa, ba); aa = None\<rbrakk> \<Longrightarrow> on_finish param a (finish a ba) \<le> SPEC (\<lambda>e. RETURN (finish a ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 2. \<And>a b aa ba x. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} = {}; (hd (stack s), None, s) = (a, b); b = (aa, ba); aa = Some x; is_discovered x ba; is_finished x ba\<rbrakk> \<Longrightarrow> on_cross_edge param a x (cross_edge a x ba) \<le> SPEC (\<lambda>e. RETURN (cross_edge a x ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 3. \<And>a b aa ba x. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} = {}; (hd (stack s), None, s) = (a, b); b = (aa, ba); aa = Some x; is_discovered x ba; \<not> is_finished x ba\<rbrakk> \<Longrightarrow> on_back_edge param a x (back_edge a x ba) \<le> SPEC (\<lambda>e. RETURN (back_edge a x ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 4. \<And>a b aa ba x. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} = {}; (hd (stack s), None, s) = (a, b); b = (aa, ba); aa = Some x; \<not> is_discovered x ba\<rbrakk> \<Longrightarrow> on_discover param a x (discover a x ba) \<le> SPEC (\<lambda>e. RETURN (discover a x ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 5. \<And>x a b aa ba. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (a, b); b = (aa, ba); aa = None\<rbrakk> \<Longrightarrow> on_finish param a (finish a ba) \<le> SPEC (\<lambda>e. RETURN (finish a ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 6. \<And>x a b aa ba xa. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (a, b); b = (aa, ba); aa = Some xa; is_discovered xa ba; is_finished xa ba\<rbrakk> \<Longrightarrow> on_cross_edge param a xa (cross_edge a xa ba) \<le> SPEC (\<lambda>e. RETURN (cross_edge a xa ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 7. \<And>x a b aa ba xa. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (a, b); b = (aa, ba); aa = Some xa; is_discovered xa ba; \<not> is_finished xa ba\<rbrakk> \<Longrightarrow> on_back_edge param a xa (back_edge a xa ba) \<le> SPEC (\<lambda>e. RETURN (back_edge a xa ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 8. \<And>x a b aa ba xa. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (a, b); b = (aa, ba); aa = Some xa; \<not> is_discovered xa ba\<rbrakk> \<Longrightarrow> on_discover param a xa (discover a xa ba) \<le> SPEC (\<lambda>e. RETURN (discover a xa ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
[PROOF STEP]
apply (auto simp: refine_pw_simps pw_le_iff is_empty_stack_def) []
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>a b aa ba x. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} = {}; (hd (stack s), None, s) = (a, b); b = (aa, ba); aa = Some x; is_discovered x ba; is_finished x ba\<rbrakk> \<Longrightarrow> on_cross_edge param a x (cross_edge a x ba) \<le> SPEC (\<lambda>e. RETURN (cross_edge a x ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 2. \<And>a b aa ba x. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} = {}; (hd (stack s), None, s) = (a, b); b = (aa, ba); aa = Some x; is_discovered x ba; \<not> is_finished x ba\<rbrakk> \<Longrightarrow> on_back_edge param a x (back_edge a x ba) \<le> SPEC (\<lambda>e. RETURN (back_edge a x ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 3. \<And>a b aa ba x. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} = {}; (hd (stack s), None, s) = (a, b); b = (aa, ba); aa = Some x; \<not> is_discovered x ba\<rbrakk> \<Longrightarrow> on_discover param a x (discover a x ba) \<le> SPEC (\<lambda>e. RETURN (discover a x ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 4. \<And>x a b aa ba. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (a, b); b = (aa, ba); aa = None\<rbrakk> \<Longrightarrow> on_finish param a (finish a ba) \<le> SPEC (\<lambda>e. RETURN (finish a ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 5. \<And>x a b aa ba xa. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (a, b); b = (aa, ba); aa = Some xa; is_discovered xa ba; is_finished xa ba\<rbrakk> \<Longrightarrow> on_cross_edge param a xa (cross_edge a xa ba) \<le> SPEC (\<lambda>e. RETURN (cross_edge a xa ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 6. \<And>x a b aa ba xa. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (a, b); b = (aa, ba); aa = Some xa; is_discovered xa ba; \<not> is_finished xa ba\<rbrakk> \<Longrightarrow> on_back_edge param a xa (back_edge a xa ba) \<le> SPEC (\<lambda>e. RETURN (back_edge a xa ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
 7. \<And>x a b aa ba xa. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {hd (stack s)} \<noteq> {}; x \<in> pending s `` {hd (stack s)}; (hd (stack s), Some x, s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) = (a, b); b = (aa, ba); aa = Some xa; \<not> is_discovered xa ba\<rbrakk> \<Longrightarrow> on_discover param a xa (discover a xa ba) \<le> SPEC (\<lambda>e. RETURN (discover a xa ba\<lparr>state.more := e\<rparr>) \<le> SPEC (\<lambda>s'. (s', s) \<in> inv_image (finite_psupset reachable <*lex*> finite_psubset <*lex*> less_than) (\<lambda>s. (dom (discovered s), pending s, length (stack s)))))
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x a b aa. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (RES (pending s `` {a}) \<bind> (\<lambda>x. if is_discovered x (s\<lparr>pending := pending s - {(a, x)}\<rparr>) then if is_finished x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) then let sa = cross_edge (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) in on_cross_edge param (hd (stack s)) x sa \<bind> (\<lambda>e. RETURN (sa\<lparr>state.more := e\<rparr>)) else let sa = back_edge (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) in on_back_edge param (hd (stack s)) x sa \<bind> (\<lambda>e. RETURN (sa\<lparr>state.more := e\<rparr>)) else let sa = discover (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) in on_discover param (hd (stack s)) x sa \<bind> (\<lambda>e. RETURN (sa\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {a} \<noteq> {}; (a, x) \<in> pending s; hd (stack s) = a; b = (Some x, s\<lparr>pending := pending s - {(a, x)}\<rparr>); aa = Some x; is_discovered x (s\<lparr>pending := pending s - {(a, x)}\<rparr>); is_finished x (s\<lparr>pending := pending s - {(a, x)}\<rparr>)\<rbrakk> \<Longrightarrow> ((dom (discovered s), dom (discovered s)) \<in> finite_psupset reachable \<longrightarrow> on_cross_edge param a x (cross_edge a x (s\<lparr>pending := pending s - {(a, x)}\<rparr>)) \<le> RES UNIV) \<and> (pending s - {(a, x)} \<subset> pending s \<longrightarrow> on_cross_edge param a x (cross_edge a x (s\<lparr>pending := pending s - {(a, x)}\<rparr>)) \<le> RES UNIV) \<and> ((dom (discovered s), dom (discovered s)) \<notin> finite_psupset reachable \<and> \<not> pending s - {(a, x)} \<subset> pending s \<longrightarrow> on_cross_edge param a x (cross_edge a x (s\<lparr>pending := pending s - {(a, x)}\<rparr>)) = SUCCEED)
 2. \<And>x a b aa. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (RES (pending s `` {a}) \<bind> (\<lambda>x. if is_discovered x (s\<lparr>pending := pending s - {(a, x)}\<rparr>) then if is_finished x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) then let sa = cross_edge (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) in on_cross_edge param (hd (stack s)) x sa \<bind> (\<lambda>e. RETURN (sa\<lparr>state.more := e\<rparr>)) else let sa = back_edge (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) in on_back_edge param (hd (stack s)) x sa \<bind> (\<lambda>e. RETURN (sa\<lparr>state.more := e\<rparr>)) else let sa = discover (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) in on_discover param (hd (stack s)) x sa \<bind> (\<lambda>e. RETURN (sa\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {a} \<noteq> {}; (a, x) \<in> pending s; hd (stack s) = a; b = (Some x, s\<lparr>pending := pending s - {(a, x)}\<rparr>); aa = Some x; is_discovered x (s\<lparr>pending := pending s - {(a, x)}\<rparr>); \<not> is_finished x (s\<lparr>pending := pending s - {(a, x)}\<rparr>)\<rbrakk> \<Longrightarrow> ((dom (discovered s), dom (discovered s)) \<in> finite_psupset reachable \<longrightarrow> on_back_edge param a x (back_edge a x (s\<lparr>pending := pending s - {(a, x)}\<rparr>)) \<le> RES UNIV) \<and> (pending s - {(a, x)} \<subset> pending s \<longrightarrow> on_back_edge param a x (back_edge a x (s\<lparr>pending := pending s - {(a, x)}\<rparr>)) \<le> RES UNIV) \<and> ((dom (discovered s), dom (discovered s)) \<notin> finite_psupset reachable \<and> \<not> pending s - {(a, x)} \<subset> pending s \<longrightarrow> on_back_edge param a x (back_edge a x (s\<lparr>pending := pending s - {(a, x)}\<rparr>)) = SUCCEED)
 3. \<And>x a b aa. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (RES (pending s `` {a}) \<bind> (\<lambda>x. if is_discovered x (s\<lparr>pending := pending s - {(a, x)}\<rparr>) then if is_finished x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) then let sa = cross_edge (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) in on_cross_edge param (hd (stack s)) x sa \<bind> (\<lambda>e. RETURN (sa\<lparr>state.more := e\<rparr>)) else let sa = back_edge (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) in on_back_edge param (hd (stack s)) x sa \<bind> (\<lambda>e. RETURN (sa\<lparr>state.more := e\<rparr>)) else let sa = discover (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) in on_discover param (hd (stack s)) x sa \<bind> (\<lambda>e. RETURN (sa\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {a} \<noteq> {}; (a, x) \<in> pending s; hd (stack s) = a; b = (Some x, s\<lparr>pending := pending s - {(a, x)}\<rparr>); aa = Some x; \<not> is_discovered x (s\<lparr>pending := pending s - {(a, x)}\<rparr>)\<rbrakk> \<Longrightarrow> ((insert x (dom (discovered s)), dom (discovered s)) \<in> finite_psupset reachable \<longrightarrow> on_discover param a x (discover a x (s\<lparr>pending := pending s - {(a, x)}\<rparr>)) \<le> RES UNIV) \<and> (insert x (dom (discovered s)) = dom (discovered s) \<and> pending s - {(a, x)} \<union> {x} \<times> E `` {x} \<subset> pending s \<longrightarrow> on_discover param a x (discover a x (s\<lparr>pending := pending s - {(a, x)}\<rparr>)) \<le> RES UNIV) \<and> ((insert x (dom (discovered s)), dom (discovered s)) \<notin> finite_psupset reachable \<and> (insert x (dom (discovered s)) = dom (discovered s) \<longrightarrow> \<not> pending s - {(a, x)} \<union> {x} \<times> E `` {x} \<subset> pending s) \<longrightarrow> on_discover param a x (discover a x (s\<lparr>pending := pending s - {(a, x)}\<rparr>)) = SUCCEED)
[PROOF STEP]
apply (auto
        simp: refine_pw_simps pw_le_iff is_discovered_def
        split: if_split_asm
        ) [2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x a b aa. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; nofail (RES (pending s `` {a}) \<bind> (\<lambda>x. if is_discovered x (s\<lparr>pending := pending s - {(a, x)}\<rparr>) then if is_finished x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) then let sa = cross_edge (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) in on_cross_edge param (hd (stack s)) x sa \<bind> (\<lambda>e. RETURN (sa\<lparr>state.more := e\<rparr>)) else let sa = back_edge (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) in on_back_edge param (hd (stack s)) x sa \<bind> (\<lambda>e. RETURN (sa\<lparr>state.more := e\<rparr>)) else let sa = discover (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) in on_discover param (hd (stack s)) x sa \<bind> (\<lambda>e. RETURN (sa\<lparr>state.more := e\<rparr>)))); \<not> is_empty_stack s; pending s `` {a} \<noteq> {}; (a, x) \<in> pending s; hd (stack s) = a; b = (Some x, s\<lparr>pending := pending s - {(a, x)}\<rparr>); aa = Some x; \<not> is_discovered x (s\<lparr>pending := pending s - {(a, x)}\<rparr>)\<rbrakk> \<Longrightarrow> ((insert x (dom (discovered s)), dom (discovered s)) \<in> finite_psupset reachable \<longrightarrow> on_discover param a x (discover a x (s\<lparr>pending := pending s - {(a, x)}\<rparr>)) \<le> RES UNIV) \<and> (insert x (dom (discovered s)) = dom (discovered s) \<and> pending s - {(a, x)} \<union> {x} \<times> E `` {x} \<subset> pending s \<longrightarrow> on_discover param a x (discover a x (s\<lparr>pending := pending s - {(a, x)}\<rparr>)) \<le> RES UNIV) \<and> ((insert x (dom (discovered s)), dom (discovered s)) \<notin> finite_psupset reachable \<and> (insert x (dom (discovered s)) = dom (discovered s) \<longrightarrow> \<not> pending s - {(a, x)} \<union> {x} \<times> E `` {x} \<subset> pending s) \<longrightarrow> on_discover param a x (discover a x (s\<lparr>pending := pending s - {(a, x)}\<rparr>)) = SUCCEED)
[PROOF STEP]
apply (clarsimp simp: refine_pw_simps pw_le_iff is_discovered_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; \<forall>x. (hd (stack s), x) \<in> pending s \<longrightarrow> nofail (if x \<in> dom (discovered s) then if is_finished x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) then let sa = cross_edge (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) in on_cross_edge param (hd (stack s)) x sa \<bind> (\<lambda>e. RETURN (sa\<lparr>state.more := e\<rparr>)) else let sa = back_edge (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) in on_back_edge param (hd (stack s)) x sa \<bind> (\<lambda>e. RETURN (sa\<lparr>state.more := e\<rparr>)) else let sa = discover (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) in on_discover param (hd (stack s)) x sa \<bind> (\<lambda>e. RETURN (sa\<lparr>state.more := e\<rparr>))); \<not> is_empty_stack s; pending s `` {hd (stack s)} \<noteq> {}; (hd (stack s), x) \<in> pending s; (insert x (dom (discovered s)), dom (discovered s)) \<in> finite_psupset reachable \<and> \<not> nofail (on_discover param (hd (stack s)) x (discover (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>))) \<or> insert x (dom (discovered s)) = dom (discovered s) \<and> pending s - {(hd (stack s), x)} \<union> {x} \<times> E `` {x} \<subset> pending s \<and> \<not> nofail (on_discover param (hd (stack s)) x (discover (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>))) \<or> (insert x (dom (discovered s)), dom (discovered s)) \<notin> finite_psupset reachable \<and> (insert x (dom (discovered s)) = dom (discovered s) \<longrightarrow> \<not> pending s - {(hd (stack s), x)} \<union> {x} \<times> E `` {x} \<subset> pending s) \<and> on_discover param (hd (stack s)) x (discover (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>)) \<noteq> SUCCEED\<rbrakk> \<Longrightarrow> \<exists>y. discovered s x = Some y
[PROOF STEP]
using discovered_reachable pending_reachable
[PROOF STATE]
proof (prove)
using this:
dom (discovered s) \<subseteq> reachable
pending s \<subseteq> reachable \<times> reachable

goal (1 subgoal):
 1. \<And>x. \<lbrakk>rwof init cond (\<lambda>s. if is_empty_stack s then SPEC (\<lambda>v. v \<in> V0 \<and> \<not> is_discovered v s) \<bind> (\<lambda>v0. let s = new_root v0 s in on_new_root param v0 s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>))) else (let u = hd (stack s); Vs = pending s `` {u} in if Vs = {} then RETURN (u, None, s) else RES Vs \<bind> (\<lambda>v. let s = s\<lparr>pending := pending s - {(u, v)}\<rparr> in RETURN (u, Some v, s))) \<bind> (\<lambda>(u, Vs, s). case Vs of None \<Rightarrow> let s = finish u s in on_finish param u s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) | Some v \<Rightarrow> if is_discovered v s then if is_finished v s then let s = cross_edge u v s in on_cross_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = back_edge u v s in on_back_edge param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)) else let s = discover u v s in on_discover param u v s \<bind> (\<lambda>e. RETURN (s\<lparr>state.more := e\<rparr>)))) s; cond s; \<forall>x. (hd (stack s), x) \<in> pending s \<longrightarrow> nofail (if x \<in> dom (discovered s) then if is_finished x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) then let sa = cross_edge (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) in on_cross_edge param (hd (stack s)) x sa \<bind> (\<lambda>e. RETURN (sa\<lparr>state.more := e\<rparr>)) else let sa = back_edge (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) in on_back_edge param (hd (stack s)) x sa \<bind> (\<lambda>e. RETURN (sa\<lparr>state.more := e\<rparr>)) else let sa = discover (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>) in on_discover param (hd (stack s)) x sa \<bind> (\<lambda>e. RETURN (sa\<lparr>state.more := e\<rparr>))); \<not> is_empty_stack s; pending s `` {hd (stack s)} \<noteq> {}; (hd (stack s), x) \<in> pending s; (insert x (dom (discovered s)), dom (discovered s)) \<in> finite_psupset reachable \<and> \<not> nofail (on_discover param (hd (stack s)) x (discover (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>))) \<or> insert x (dom (discovered s)) = dom (discovered s) \<and> pending s - {(hd (stack s), x)} \<union> {x} \<times> E `` {x} \<subset> pending s \<and> \<not> nofail (on_discover param (hd (stack s)) x (discover (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>))) \<or> (insert x (dom (discovered s)), dom (discovered s)) \<notin> finite_psupset reachable \<and> (insert x (dom (discovered s)) = dom (discovered s) \<longrightarrow> \<not> pending s - {(hd (stack s), x)} \<union> {x} \<times> E `` {x} \<subset> pending s) \<and> on_discover param (hd (stack s)) x (discover (hd (stack s)) x (s\<lparr>pending := pending s - {(hd (stack s), x)}\<rparr>)) \<noteq> SUCCEED\<rbrakk> \<Longrightarrow> \<exists>y. discovered s x = Some y
[PROOF STEP]
apply (auto
        simp: is_discovered_def
        simp: refine_pw_simps pw_le_iff finite_psupset_def
        split: if_split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
step s \<le> SPEC (\<lambda>s'. (s', s) \<in> param_dfs_variant)

goal:
No subgoals!
[PROOF STEP]
qed