[STATEMENT]
theorem red_dfs_correct:
  fixes v0 u0 :: 'v
  assumes PRE:
    "red_dfs_inv E U reds onstack"
    "u0\<in>U"
    "u0\<notin>reds"
  shows "red_dfs E onstack reds u0
    \<le> SPEC (\<lambda>(reds',cyc). case cyc of
      Some (p,v) \<Rightarrow> v\<in>onstack \<and> p\<noteq>[] \<and> path E u0 p v
    | None \<Rightarrow>
        red_dfs_inv E U reds' onstack
        \<and> u0\<in>reds'
        \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0}
  )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. red_dfs E onstack reds u0 \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. red_dfs E onstack reds u0 \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)
[PROOF STEP]
let ?dfs_red = "
    REC\<^sub>T (\<lambda>D (V,u). do {
      let V=insert u V;
      NDFS_SI_Statistics.vis_red_nres;

      \<comment> \<open>Check whether we have a successor on stack\<close>
      brk \<leftarrow> FOREACH\<^sub>C (E``{u}) (\<lambda>brk. brk=None)
        (\<lambda>t _. if t\<in>onstack then
            RETURN (red_init_witness u t)
          else RETURN None)
        None;

      \<comment> \<open>Recurse for successors\<close>
      case brk of
        None \<Rightarrow>
          FOREACH\<^sub>C (E``{u}) (\<lambda>(V,brk). brk=None)
            (\<lambda>t (V,_).
              if t\<notin>V then do {
                (V,brk) \<leftarrow> D (V,t);
                RETURN (V,prep_wit_red u brk)
              } else RETURN (V,None))
            (V,None)
      | _ \<Rightarrow> RETURN (V,brk)
    }) (V,u)
"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. red_dfs E onstack reds u0 \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)
[PROOF STEP]
let "REC\<^sub>T ?body ?init" = "?dfs_red"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. red_dfs E onstack reds u0 \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)
[PROOF STEP]
define pre where "pre = (\<lambda>S (V,u0). gen_dfs_pre E U S V u0 \<and> E``V \<inter> onstack = {})"
[PROOF STATE]
proof (state)
this:
pre = (\<lambda>S (V, u0). gen_dfs_pre E U S V u0 \<and> E `` V \<inter> onstack = {})

goal (1 subgoal):
 1. red_dfs E onstack reds u0 \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)
[PROOF STEP]
define post where "post = (\<lambda>S (V0,u0) (V,cyc). gen_dfs_post E U S V0 u0 V (cyc\<noteq>None)
    \<and> (case cyc of None \<Rightarrow> E``V \<inter> onstack = {}
      | Some (p,v) \<Rightarrow> v\<in>onstack \<and> p\<noteq>[] \<and> path E u0 p v))
    "
[PROOF STATE]
proof (state)
this:
post = (\<lambda>S (V0, u0) (V, cyc). gen_dfs_post E U S V0 u0 V (cyc \<noteq> None) \<and> (case cyc of None \<Rightarrow> E `` V \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v))

goal (1 subgoal):
 1. red_dfs E onstack reds u0 \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)
[PROOF STEP]
define fe_inv where "fe_inv = (\<lambda>S V0 u0 it (V,cyc).
    gen_dfs_fe_inv E U S V0 u0 it V (cyc\<noteq>None)
    \<and> (case cyc of None \<Rightarrow> E``V \<inter> onstack = {}
      | Some (p,v) \<Rightarrow> v\<in>onstack \<and> p\<noteq>[] \<and> path E u0 p v))
    "
[PROOF STATE]
proof (state)
this:
fe_inv = (\<lambda>S V0 u0 it (V, cyc). gen_dfs_fe_inv E U S V0 u0 it V (cyc \<noteq> None) \<and> (case cyc of None \<Rightarrow> E `` V \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v))

goal (1 subgoal):
 1. red_dfs E onstack reds u0 \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)
[PROOF STEP]
from PRE
[PROOF STATE]
proof (chain)
picking this:
red_dfs_inv E U reds onstack
u0 \<in> U
u0 \<notin> reds
[PROOF STEP]
have GENPRE: "gen_dfs_pre E U {} reds u0"
[PROOF STATE]
proof (prove)
using this:
red_dfs_inv E U reds onstack
u0 \<in> U
u0 \<notin> reds

goal (1 subgoal):
 1. gen_dfs_pre E U {} reds u0
[PROOF STEP]
unfolding red_dfs_inv_def gen_dfs_pre_def
[PROOF STATE]
proof (prove)
using this:
E `` U \<subseteq> U \<and> finite U \<and> reds \<subseteq> U \<and> E `` reds \<subseteq> reds \<and> E `` reds \<inter> onstack = {}
u0 \<in> U
u0 \<notin> reds

goal (1 subgoal):
 1. E `` U \<subseteq> U \<and> finite U \<and> reds \<subseteq> U \<and> u0 \<in> U \<and> E `` (reds - {}) \<subseteq> reds \<and> u0 \<notin> reds \<and> {} \<subseteq> reds \<and> (\<forall>v\<in>{}. (v, u0) \<in> (E \<inter> {} \<times> UNIV)\<^sup>*)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
gen_dfs_pre E U {} reds u0

goal (1 subgoal):
 1. red_dfs E onstack reds u0 \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)
[PROOF STEP]
with PRE
[PROOF STATE]
proof (chain)
picking this:
red_dfs_inv E U reds onstack
u0 \<in> U
u0 \<notin> reds
gen_dfs_pre E U {} reds u0
[PROOF STEP]
have PRE': "pre {} (reds,u0)"
[PROOF STATE]
proof (prove)
using this:
red_dfs_inv E U reds onstack
u0 \<in> U
u0 \<notin> reds
gen_dfs_pre E U {} reds u0

goal (1 subgoal):
 1. pre {} (reds, u0)
[PROOF STEP]
unfolding pre_def red_dfs_inv_def
[PROOF STATE]
proof (prove)
using this:
E `` U \<subseteq> U \<and> finite U \<and> reds \<subseteq> U \<and> E `` reds \<subseteq> reds \<and> E `` reds \<inter> onstack = {}
u0 \<in> U
u0 \<notin> reds
gen_dfs_pre E U {} reds u0

goal (1 subgoal):
 1. case (reds, u0) of (V, u0) \<Rightarrow> gen_dfs_pre E U {} V u0 \<and> E `` V \<inter> onstack = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pre {} (reds, u0)

goal (1 subgoal):
 1. red_dfs E onstack reds u0 \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)
[PROOF STEP]
have IMP_POST: "SPEC (post {} (reds,u0))
    \<le> SPEC (\<lambda>(reds',cyc). case cyc of
      Some (p,v) \<Rightarrow> v\<in>onstack \<and> p\<noteq>[] \<and> path E u0 p v
    | None \<Rightarrow>
        red_dfs_inv E U reds' onstack
        \<and> u0\<in>reds'
        \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SPEC (post {} (reds, u0)) \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)
[PROOF STEP]
apply (clarsimp split: option.split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. post {} (reds, u0) (a, b) \<Longrightarrow> (b = None \<longrightarrow> red_dfs_inv E U a onstack \<and> u0 \<in> a \<and> a \<subseteq> reds \<union> E\<^sup>* `` {u0}) \<and> (\<forall>a ba. b = Some (a, ba) \<longrightarrow> ba \<in> onstack \<and> a \<noteq> [] \<and> path E u0 a ba)
[PROOF STEP]
apply (intro impI conjI allI)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a b. \<lbrakk>post {} (reds, u0) (a, b); b = None\<rbrakk> \<Longrightarrow> red_dfs_inv E U a onstack
 2. \<And>a b. \<lbrakk>post {} (reds, u0) (a, b); b = None\<rbrakk> \<Longrightarrow> u0 \<in> a
 3. \<And>a b. \<lbrakk>post {} (reds, u0) (a, b); b = None\<rbrakk> \<Longrightarrow> a \<subseteq> reds \<union> E\<^sup>* `` {u0}
 4. \<And>a b aa ba. \<lbrakk>post {} (reds, u0) (a, b); b = Some (aa, ba)\<rbrakk> \<Longrightarrow> ba \<in> onstack
 5. \<And>a b aa ba. \<lbrakk>post {} (reds, u0) (a, b); b = Some (aa, ba)\<rbrakk> \<Longrightarrow> aa \<noteq> []
 6. \<And>a b aa ba. \<lbrakk>post {} (reds, u0) (a, b); b = Some (aa, ba)\<rbrakk> \<Longrightarrow> path E u0 aa ba
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> red_dfs_inv E U a onstack
 2. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> u0 \<in> a
 3. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> a \<subseteq> reds \<union> E\<^sup>* `` {u0}
 4. \<And>a b aa ba. \<lbrakk>post {} (reds, u0) (a, Some (aa, ba)); b = Some (aa, ba)\<rbrakk> \<Longrightarrow> ba \<in> onstack
 5. \<And>a b aa ba. \<lbrakk>post {} (reds, u0) (a, Some (aa, ba)); b = Some (aa, ba)\<rbrakk> \<Longrightarrow> aa \<noteq> []
 6. \<And>a b aa ba. \<lbrakk>post {} (reds, u0) (a, Some (aa, ba)); b = Some (aa, ba)\<rbrakk> \<Longrightarrow> path E u0 aa ba
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> red_dfs_inv E U a onstack
 2. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> u0 \<in> a
 3. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> a \<subseteq> reds \<union> E\<^sup>* `` {u0}
 4. \<And>a b aa ba. \<lbrakk>post {} (reds, u0) (a, Some (aa, ba)); b = Some (aa, ba)\<rbrakk> \<Longrightarrow> ba \<in> onstack
 5. \<And>a b aa ba. \<lbrakk>post {} (reds, u0) (a, Some (aa, ba)); b = Some (aa, ba)\<rbrakk> \<Longrightarrow> aa \<noteq> []
 6. \<And>a b aa ba. \<lbrakk>post {} (reds, u0) (a, Some (aa, ba)); b = Some (aa, ba)\<rbrakk> \<Longrightarrow> path E u0 aa ba
[PROOF STEP]
fix reds' p v
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> red_dfs_inv E U a onstack
 2. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> u0 \<in> a
 3. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> a \<subseteq> reds \<union> E\<^sup>* `` {u0}
 4. \<And>a b aa ba. \<lbrakk>post {} (reds, u0) (a, Some (aa, ba)); b = Some (aa, ba)\<rbrakk> \<Longrightarrow> ba \<in> onstack
 5. \<And>a b aa ba. \<lbrakk>post {} (reds, u0) (a, Some (aa, ba)); b = Some (aa, ba)\<rbrakk> \<Longrightarrow> aa \<noteq> []
 6. \<And>a b aa ba. \<lbrakk>post {} (reds, u0) (a, Some (aa, ba)); b = Some (aa, ba)\<rbrakk> \<Longrightarrow> path E u0 aa ba
[PROOF STEP]
assume "post {} (reds,u0) (reds',Some (p,v))"
[PROOF STATE]
proof (state)
this:
post {} (reds, u0) (reds', Some (p, v))

goal (6 subgoals):
 1. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> red_dfs_inv E U a onstack
 2. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> u0 \<in> a
 3. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> a \<subseteq> reds \<union> E\<^sup>* `` {u0}
 4. \<And>a b aa ba. \<lbrakk>post {} (reds, u0) (a, Some (aa, ba)); b = Some (aa, ba)\<rbrakk> \<Longrightarrow> ba \<in> onstack
 5. \<And>a b aa ba. \<lbrakk>post {} (reds, u0) (a, Some (aa, ba)); b = Some (aa, ba)\<rbrakk> \<Longrightarrow> aa \<noteq> []
 6. \<And>a b aa ba. \<lbrakk>post {} (reds, u0) (a, Some (aa, ba)); b = Some (aa, ba)\<rbrakk> \<Longrightarrow> path E u0 aa ba
[PROOF STEP]
thus "v\<in>onstack" and "p\<noteq>[]" and "path E u0 p v"
[PROOF STATE]
proof (prove)
using this:
post {} (reds, u0) (reds', Some (p, v))

goal (1 subgoal):
 1. v \<in> onstack &&& p \<noteq> [] &&& path E u0 p v
[PROOF STEP]
unfolding post_def
[PROOF STATE]
proof (prove)
using this:
(case (reds, u0) of (V0, u0) \<Rightarrow> \<lambda>(V, cyc). gen_dfs_post E U {} V0 u0 V (cyc \<noteq> None) \<and> (case cyc of None \<Rightarrow> E `` V \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)) (reds', Some (p, v))

goal (1 subgoal):
 1. v \<in> onstack &&& p \<noteq> [] &&& path E u0 p v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> onstack
p \<noteq> []
path E u0 p v

goal (3 subgoals):
 1. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> red_dfs_inv E U a onstack
 2. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> u0 \<in> a
 3. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> a \<subseteq> reds \<union> E\<^sup>* `` {u0}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> red_dfs_inv E U a onstack
 2. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> u0 \<in> a
 3. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> a \<subseteq> reds \<union> E\<^sup>* `` {u0}
[PROOF STEP]
fix reds'
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> red_dfs_inv E U a onstack
 2. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> u0 \<in> a
 3. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> a \<subseteq> reds \<union> E\<^sup>* `` {u0}
[PROOF STEP]
assume "post {} (reds, u0) (reds', None)"
[PROOF STATE]
proof (state)
this:
post {} (reds, u0) (reds', None)

goal (3 subgoals):
 1. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> red_dfs_inv E U a onstack
 2. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> u0 \<in> a
 3. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> a \<subseteq> reds \<union> E\<^sup>* `` {u0}
[PROOF STEP]
hence GPOST: "gen_dfs_post E U {} reds u0 reds' False"
      and NS: "E``reds' \<inter> onstack = {}"
[PROOF STATE]
proof (prove)
using this:
post {} (reds, u0) (reds', None)

goal (1 subgoal):
 1. gen_dfs_post E U {} reds u0 reds' False &&& E `` reds' \<inter> onstack = {}
[PROOF STEP]
unfolding post_def
[PROOF STATE]
proof (prove)
using this:
(case (reds, u0) of (V0, u0) \<Rightarrow> \<lambda>(V, cyc). gen_dfs_post E U {} V0 u0 V (cyc \<noteq> None) \<and> (case cyc of None \<Rightarrow> E `` V \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)) (reds', None)

goal (1 subgoal):
 1. gen_dfs_post E U {} reds u0 reds' False &&& E `` reds' \<inter> onstack = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
gen_dfs_post E U {} reds u0 reds' False
E `` reds' \<inter> onstack = {}

goal (3 subgoals):
 1. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> red_dfs_inv E U a onstack
 2. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> u0 \<in> a
 3. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> a \<subseteq> reds \<union> E\<^sup>* `` {u0}
[PROOF STEP]
from GPOST
[PROOF STATE]
proof (chain)
picking this:
gen_dfs_post E U {} reds u0 reds' False
[PROOF STEP]
show "u0\<in>reds'"
[PROOF STATE]
proof (prove)
using this:
gen_dfs_post E U {} reds u0 reds' False

goal (1 subgoal):
 1. u0 \<in> reds'
[PROOF STEP]
unfolding gen_dfs_post_def
[PROOF STATE]
proof (prove)
using this:
(\<not> False \<longrightarrow> E `` (reds' - {}) \<subseteq> reds') \<and> u0 \<in> reds' \<and> reds \<subseteq> reds' \<and> reds' \<subseteq> reds \<union> (E - UNIV \<times> {})\<^sup>* `` {u0}

goal (1 subgoal):
 1. u0 \<in> reds'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u0 \<in> reds'

goal (2 subgoals):
 1. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> red_dfs_inv E U a onstack
 2. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> a \<subseteq> reds \<union> E\<^sup>* `` {u0}
[PROOF STEP]
show "red_dfs_inv E U reds' onstack"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. red_dfs_inv E U reds' onstack
[PROOF STEP]
unfolding red_dfs_inv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E `` U \<subseteq> U \<and> finite U \<and> reds' \<subseteq> U \<and> E `` reds' \<subseteq> reds' \<and> E `` reds' \<inter> onstack = {}
[PROOF STEP]
apply (intro conjI)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. E `` U \<subseteq> U
 2. finite U
 3. reds' \<subseteq> U
 4. E `` reds' \<subseteq> reds'
 5. E `` reds' \<inter> onstack = {}
[PROOF STEP]
using GENPRE[unfolded gen_dfs_pre_def]
[PROOF STATE]
proof (prove)
using this:
E `` U \<subseteq> U \<and> finite U \<and> reds \<subseteq> U \<and> u0 \<in> U \<and> E `` (reds - {}) \<subseteq> reds \<and> u0 \<notin> reds \<and> {} \<subseteq> reds \<and> (\<forall>v\<in>{}. (v, u0) \<in> (E \<inter> {} \<times> UNIV)\<^sup>*)

goal (5 subgoals):
 1. E `` U \<subseteq> U
 2. finite U
 3. reds' \<subseteq> U
 4. E `` reds' \<subseteq> reds'
 5. E `` reds' \<inter> onstack = {}
[PROOF STEP]
apply (simp_all) [2]
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. reds' \<subseteq> U
 2. E `` reds' \<subseteq> reds'
 3. E `` reds' \<inter> onstack = {}
[PROOF STEP]
apply (rule gen_dfs_post_imp_below_U[OF GENPRE GPOST])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. E `` reds' \<subseteq> reds'
 2. E `` reds' \<inter> onstack = {}
[PROOF STEP]
using GPOST[unfolded gen_dfs_post_def]
[PROOF STATE]
proof (prove)
using this:
(\<not> False \<longrightarrow> E `` (reds' - {}) \<subseteq> reds') \<and> u0 \<in> reds' \<and> reds \<subseteq> reds' \<and> reds' \<subseteq> reds \<union> (E - UNIV \<times> {})\<^sup>* `` {u0}

goal (2 subgoals):
 1. E `` reds' \<subseteq> reds'
 2. E `` reds' \<inter> onstack = {}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E `` reds' \<inter> onstack = {}
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
red_dfs_inv E U reds' onstack

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>post {} (reds, u0) (a, None); b = None\<rbrakk> \<Longrightarrow> a \<subseteq> reds \<union> E\<^sup>* `` {u0}
[PROOF STEP]
from GPOST
[PROOF STATE]
proof (chain)
picking this:
gen_dfs_post E U {} reds u0 reds' False
[PROOF STEP]
show "reds' \<subseteq> reds \<union> E\<^sup>* `` {u0}"
[PROOF STATE]
proof (prove)
using this:
gen_dfs_post E U {} reds u0 reds' False

goal (1 subgoal):
 1. reds' \<subseteq> reds \<union> E\<^sup>* `` {u0}
[PROOF STEP]
unfolding gen_dfs_post_def
[PROOF STATE]
proof (prove)
using this:
(\<not> False \<longrightarrow> E `` (reds' - {}) \<subseteq> reds') \<and> u0 \<in> reds' \<and> reds \<subseteq> reds' \<and> reds' \<subseteq> reds \<union> (E - UNIV \<times> {})\<^sup>* `` {u0}

goal (1 subgoal):
 1. reds' \<subseteq> reds \<union> E\<^sup>* `` {u0}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
reds' \<subseteq> reds \<union> E\<^sup>* `` {u0}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
SPEC (post {} (reds, u0)) \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)

goal (1 subgoal):
 1. red_dfs E onstack reds u0 \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
SPEC (post {} (reds, u0)) \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)

goal (1 subgoal):
 1. red_dfs E onstack reds u0 \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)
[PROOF STEP]
fix \<sigma> S
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. red_dfs E onstack reds u0 \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)
[PROOF STEP]
assume INV0: "pre S \<sigma>"
[PROOF STATE]
proof (state)
this:
pre S \<sigma>

goal (1 subgoal):
 1. red_dfs E onstack reds u0 \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)
[PROOF STEP]
have "REC\<^sub>T ?body \<sigma>
      \<le> SPEC (post S \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. REC\<^sub>T (\<lambda>D (V, u). let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) \<sigma> \<le> SPEC (post S \<sigma>)
[PROOF STEP]
apply (rule RECT_rule_arb[where
        pre="pre" and
        V="gen_dfs_var U <*lex*> {}" and
        arb="S"
        ])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. trimono (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk))))
 2. wf (gen_dfs_var U <*lex*> {})
 3. pre S \<sigma>
 4. \<And>f arb x. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', x) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> f x' \<le> SPEC (post arb' x'); pre arb x; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = f\<rbrakk> \<Longrightarrow> (case x of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then f (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) \<le> SPEC (post arb x)
[PROOF STEP]
apply refine_mono
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. wf (gen_dfs_var U <*lex*> {})
 2. pre S \<sigma>
 3. \<And>f arb x. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', x) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> f x' \<le> SPEC (post arb' x'); pre arb x; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = f\<rbrakk> \<Longrightarrow> (case x of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then f (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) \<le> SPEC (post arb x)
[PROOF STEP]
using INV0[unfolded pre_def]
[PROOF STATE]
proof (prove)
using this:
case \<sigma> of (V, u0) \<Rightarrow> gen_dfs_pre E U S V u0 \<and> E `` V \<inter> onstack = {}

goal (3 subgoals):
 1. wf (gen_dfs_var U <*lex*> {})
 2. pre S \<sigma>
 3. \<And>f arb x. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', x) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> f x' \<le> SPEC (post arb' x'); pre arb x; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = f\<rbrakk> \<Longrightarrow> (case x of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then f (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) \<le> SPEC (post arb x)
[PROOF STEP]
apply (auto intro: gen_dfs_pre_imp_wf) []
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. pre S \<sigma>
 2. \<And>f arb x. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', x) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> f x' \<le> SPEC (post arb' x'); pre arb x; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = f\<rbrakk> \<Longrightarrow> (case x of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then f (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) \<le> SPEC (post arb x)
[PROOF STEP]
apply fact
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f arb x. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', x) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> f x' \<le> SPEC (post arb' x'); pre arb x; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = f\<rbrakk> \<Longrightarrow> (case x of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then f (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) \<le> SPEC (post arb x)
[PROOF STEP]
apply (rename_tac D S u)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>D S u. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D\<rbrakk> \<Longrightarrow> (case u of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) \<le> SPEC (post S u)
[PROOF STEP]
apply (intro refine_vcg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>D S u a b. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b)\<rbrakk> \<Longrightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness b t) else RETURN None) None \<le> SPEC (\<lambda>brk. (case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, brk)) \<le> SPEC (post S u))
[PROOF STEP]
(* First foreach loop, checking for onstack-successor*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>D S u a b. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b)\<rbrakk> \<Longrightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness b t) else RETURN None) None \<le> SPEC (\<lambda>brk. (case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, brk)) \<le> SPEC (post S u))
[PROOF STEP]
apply (rule_tac I="\<lambda>it cyc.
        (case cyc of None \<Rightarrow> (E``{b} - it) \<inter> onstack = {}
          | Some (p,v) \<Rightarrow> (v\<in>onstack \<and> p\<noteq>[] \<and> path E b p v))"
        in FOREACHc_rule)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>D S u a b. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b)\<rbrakk> \<Longrightarrow> finite (E `` {b})
 2. \<And>D S u a b. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b)\<rbrakk> \<Longrightarrow> case None of None \<Rightarrow> (E `` {b} - E `` {b}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v
 3. \<And>D S u a b x it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); x \<in> it; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None\<rbrakk> \<Longrightarrow> (if x \<in> onstack then RETURN (red_init_witness b x) else RETURN None) \<le> SPEC (\<lambda>cyc. case cyc of None \<Rightarrow> (E `` {b} - (it - {x})) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v)
 4. \<And>D S u a b \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
 5. \<And>D S u a b it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); it \<noteq> {}; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> \<noteq> None\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
[PROOF STEP]
apply (auto simp add: pre_def gen_dfs_pre_imp_fin) []
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>D S u a b. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b)\<rbrakk> \<Longrightarrow> case None of None \<Rightarrow> (E `` {b} - E `` {b}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v
 2. \<And>D S u a b x it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); x \<in> it; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None\<rbrakk> \<Longrightarrow> (if x \<in> onstack then RETURN (red_init_witness b x) else RETURN None) \<le> SPEC (\<lambda>cyc. case cyc of None \<Rightarrow> (E `` {b} - (it - {x})) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v)
 3. \<And>D S u a b \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
 4. \<And>D S u a b it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); it \<noteq> {}; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> \<noteq> None\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
[PROOF STEP]
apply auto []
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>D S u a b x it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); x \<in> it; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None\<rbrakk> \<Longrightarrow> (if x \<in> onstack then RETURN (red_init_witness b x) else RETURN None) \<le> SPEC (\<lambda>cyc. case cyc of None \<Rightarrow> (E `` {b} - (it - {x})) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v)
 2. \<And>D S u a b \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
 3. \<And>D S u a b it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); it \<noteq> {}; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> \<noteq> None\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
[PROOF STEP]
apply (auto
        split: option.split
        simp: red_init_witness_def intro: path1) []
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>D S u a b \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
 2. \<And>D S u a b it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); it \<noteq> {}; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> \<noteq> None\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
[PROOF STEP]
apply (intro refine_vcg)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>D S u a b \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None\<rbrakk> \<Longrightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) \<le> SPEC (post S u)
 2. \<And>D S u a b \<sigma> x. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = Some x\<rbrakk> \<Longrightarrow> post S u (insert b a, \<sigma>)
 3. \<And>D S u a b it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); it \<noteq> {}; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> \<noteq> None\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
[PROOF STEP]
(* Second foreach loop, iterating over sucessors *)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>D S u a b \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None\<rbrakk> \<Longrightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) \<le> SPEC (post S u)
 2. \<And>D S u a b \<sigma> x. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = Some x\<rbrakk> \<Longrightarrow> post S u (insert b a, \<sigma>)
 3. \<And>D S u a b it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); it \<noteq> {}; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> \<noteq> None\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
[PROOF STEP]
apply (rule_tac I="fe_inv (insert b S) (insert b a) b" in
        FOREACHc_rule
      )
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>D S u a b \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None\<rbrakk> \<Longrightarrow> finite (E `` {b})
 2. \<And>D S u a b \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None\<rbrakk> \<Longrightarrow> fe_inv (insert b S) (insert b a) b (E `` {b}) (insert b a, None)
 3. \<And>D S u a b \<sigma> x it \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None\<rbrakk> \<Longrightarrow> (case \<sigma>' of (V, uu_) \<Rightarrow> if x \<notin> V then D (V, x) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) \<le> SPEC (fe_inv (insert b S) (insert b a) b (it - {x}))
 4. \<And>D S u a b \<sigma> \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; fe_inv (insert b S) (insert b a) b {} \<sigma>'\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 5. \<And>D S u a b \<sigma> it \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; it \<noteq> {}; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; \<not> (case \<sigma>' of (V, brk) \<Rightarrow> brk = None)\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 6. \<And>D S u a b \<sigma> x. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = Some x\<rbrakk> \<Longrightarrow> post S u (insert b a, \<sigma>)
 7. \<And>D S u a b it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); it \<noteq> {}; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> \<noteq> None\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
[PROOF STEP]
apply (auto simp add: pre_def gen_dfs_pre_imp_fin) []
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>D S u a b \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None\<rbrakk> \<Longrightarrow> fe_inv (insert b S) (insert b a) b (E `` {b}) (insert b a, None)
 2. \<And>D S u a b \<sigma> x it \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None\<rbrakk> \<Longrightarrow> (case \<sigma>' of (V, uu_) \<Rightarrow> if x \<notin> V then D (V, x) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) \<le> SPEC (fe_inv (insert b S) (insert b a) b (it - {x}))
 3. \<And>D S u a b \<sigma> \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; fe_inv (insert b S) (insert b a) b {} \<sigma>'\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 4. \<And>D S u a b \<sigma> it \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; it \<noteq> {}; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; \<not> (case \<sigma>' of (V, brk) \<Rightarrow> brk = None)\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 5. \<And>D S u a b \<sigma> x. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = Some x\<rbrakk> \<Longrightarrow> post S u (insert b a, \<sigma>)
 6. \<And>D S u a b it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); it \<noteq> {}; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> \<noteq> None\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
[PROOF STEP]
apply (auto simp add: pre_def fe_inv_def gen_dfs_pre_imp_fe) []
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>D S u a b \<sigma> x it \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None\<rbrakk> \<Longrightarrow> (case \<sigma>' of (V, uu_) \<Rightarrow> if x \<notin> V then D (V, x) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) \<le> SPEC (fe_inv (insert b S) (insert b a) b (it - {x}))
 2. \<And>D S u a b \<sigma> \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; fe_inv (insert b S) (insert b a) b {} \<sigma>'\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 3. \<And>D S u a b \<sigma> it \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; it \<noteq> {}; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; \<not> (case \<sigma>' of (V, brk) \<Rightarrow> brk = None)\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 4. \<And>D S u a b \<sigma> x. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = Some x\<rbrakk> \<Longrightarrow> post S u (insert b a, \<sigma>)
 5. \<And>D S u a b it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); it \<noteq> {}; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> \<noteq> None\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
[PROOF STEP]
apply (intro refine_vcg)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>D S u a b \<sigma> x it \<sigma>' aa ba. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None; \<sigma>' = (aa, ba); x \<notin> aa\<rbrakk> \<Longrightarrow> D (aa, x) \<le> SPEC (\<lambda>xa. (case xa of (V, brk) \<Rightarrow> RETURN (V, prep_wit_red b brk)) \<le> SPEC (fe_inv (insert b S) (insert b a) b (it - {x})))
 2. \<And>D S u a b \<sigma> x it \<sigma>' aa ba. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None; \<sigma>' = (aa, ba); \<not> x \<notin> aa\<rbrakk> \<Longrightarrow> fe_inv (insert b S) (insert b a) b (it - {x}) (aa, None)
 3. \<And>D S u a b \<sigma> \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; fe_inv (insert b S) (insert b a) b {} \<sigma>'\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 4. \<And>D S u a b \<sigma> it \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; it \<noteq> {}; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; \<not> (case \<sigma>' of (V, brk) \<Rightarrow> brk = None)\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 5. \<And>D S u a b \<sigma> x. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = Some x\<rbrakk> \<Longrightarrow> post S u (insert b a, \<sigma>)
 6. \<And>D S u a b it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); it \<noteq> {}; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> \<noteq> None\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
[PROOF STEP]
(* Recursive call *)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>D S u a b \<sigma> x it \<sigma>' aa ba. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None; \<sigma>' = (aa, ba); x \<notin> aa\<rbrakk> \<Longrightarrow> D (aa, x) \<le> SPEC (\<lambda>xa. (case xa of (V, brk) \<Rightarrow> RETURN (V, prep_wit_red b brk)) \<le> SPEC (fe_inv (insert b S) (insert b a) b (it - {x})))
 2. \<And>D S u a b \<sigma> x it \<sigma>' aa ba. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None; \<sigma>' = (aa, ba); \<not> x \<notin> aa\<rbrakk> \<Longrightarrow> fe_inv (insert b S) (insert b a) b (it - {x}) (aa, None)
 3. \<And>D S u a b \<sigma> \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; fe_inv (insert b S) (insert b a) b {} \<sigma>'\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 4. \<And>D S u a b \<sigma> it \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; it \<noteq> {}; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; \<not> (case \<sigma>' of (V, brk) \<Rightarrow> brk = None)\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 5. \<And>D S u a b \<sigma> x. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = Some x\<rbrakk> \<Longrightarrow> post S u (insert b a, \<sigma>)
 6. \<And>D S u a b it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); it \<noteq> {}; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> \<noteq> None\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
[PROOF STEP]
apply (rule order_trans)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>D S u a b \<sigma> x it \<sigma>' aa ba. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None; \<sigma>' = (aa, ba); x \<notin> aa\<rbrakk> \<Longrightarrow> D (aa, x) \<le> ?y338 D S u a b \<sigma> x it \<sigma>' aa ba
 2. \<And>D S u a b \<sigma> x it \<sigma>' aa ba. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None; \<sigma>' = (aa, ba); x \<notin> aa\<rbrakk> \<Longrightarrow> ?y338 D S u a b \<sigma> x it \<sigma>' aa ba \<le> SPEC (\<lambda>xa. (case xa of (V, brk) \<Rightarrow> RETURN (V, prep_wit_red b brk)) \<le> SPEC (fe_inv (insert b S) (insert b a) b (it - {x})))
 3. \<And>D S u a b \<sigma> x it \<sigma>' aa ba. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None; \<sigma>' = (aa, ba); \<not> x \<notin> aa\<rbrakk> \<Longrightarrow> fe_inv (insert b S) (insert b a) b (it - {x}) (aa, None)
 4. \<And>D S u a b \<sigma> \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; fe_inv (insert b S) (insert b a) b {} \<sigma>'\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 5. \<And>D S u a b \<sigma> it \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; it \<noteq> {}; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; \<not> (case \<sigma>' of (V, brk) \<Rightarrow> brk = None)\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 6. \<And>D S u a b \<sigma> x. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = Some x\<rbrakk> \<Longrightarrow> post S u (insert b a, \<sigma>)
 7. \<And>D S u a b it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); it \<noteq> {}; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> \<noteq> None\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
[PROOF STEP]
apply (rprems)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>D S u a b \<sigma> x it \<sigma>' aa ba. \<lbrakk>pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None; \<sigma>' = (aa, ba); x \<notin> aa\<rbrakk> \<Longrightarrow> pre (?arb'687 D S u a b \<sigma> x it \<sigma>' aa ba) (aa, x)
 2. \<And>D S u a b \<sigma> x it \<sigma>' aa ba. \<lbrakk>pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None; \<sigma>' = (aa, ba); x \<notin> aa\<rbrakk> \<Longrightarrow> ((aa, x), u) \<in> gen_dfs_var U <*lex*> {}
 3. \<And>D S u a b \<sigma> x it \<sigma>' aa ba. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None; \<sigma>' = (aa, ba); x \<notin> aa\<rbrakk> \<Longrightarrow> SPEC (post (?arb'687 D S u a b \<sigma> x it \<sigma>' aa ba) (aa, x)) \<le> SPEC (\<lambda>xa. (case xa of (V, brk) \<Rightarrow> RETURN (V, prep_wit_red b brk)) \<le> SPEC (fe_inv (insert b S) (insert b a) b (it - {x})))
 4. \<And>D S u a b \<sigma> x it \<sigma>' aa ba. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None; \<sigma>' = (aa, ba); \<not> x \<notin> aa\<rbrakk> \<Longrightarrow> fe_inv (insert b S) (insert b a) b (it - {x}) (aa, None)
 5. \<And>D S u a b \<sigma> \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; fe_inv (insert b S) (insert b a) b {} \<sigma>'\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 6. \<And>D S u a b \<sigma> it \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; it \<noteq> {}; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; \<not> (case \<sigma>' of (V, brk) \<Rightarrow> brk = None)\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 7. \<And>D S u a b \<sigma> x. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = Some x\<rbrakk> \<Longrightarrow> post S u (insert b a, \<sigma>)
 8. \<And>D S u a b it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); it \<noteq> {}; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> \<noteq> None\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
[PROOF STEP]
apply (clarsimp simp add: pre_def fe_inv_def)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>S aa ba x it aaa. \<lbrakk>E `` {ba} \<inter> onstack = {}; x \<in> it; it \<subseteq> E `` {ba}; x \<notin> aaa; gen_dfs_pre E U S aa ba; E `` aa \<inter> onstack = {}; gen_dfs_fe_inv E U (insert ba S) (insert ba aa) ba it aaa False; E `` aaa \<inter> onstack = {}\<rbrakk> \<Longrightarrow> gen_dfs_pre E U (?arb'687 (REC\<^sub>T (\<lambda>D (V, u). FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (insert u V, None) | Some a \<Rightarrow> RETURN (insert u V, brk)))) S (aa, ba) aa ba None x it (aaa, None) aaa None) aaa x
 2. \<And>D S u a b \<sigma> x it \<sigma>' aa ba. \<lbrakk>pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None; \<sigma>' = (aa, ba); x \<notin> aa\<rbrakk> \<Longrightarrow> ((aa, x), u) \<in> gen_dfs_var U <*lex*> {}
 3. \<And>D S u a b \<sigma> x it \<sigma>' aa ba. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None; \<sigma>' = (aa, ba); x \<notin> aa\<rbrakk> \<Longrightarrow> SPEC (post (?arb'687 D S u a b \<sigma> x it \<sigma>' aa ba) (aa, x)) \<le> SPEC (\<lambda>xa. (case xa of (V, brk) \<Rightarrow> RETURN (V, prep_wit_red b brk)) \<le> SPEC (fe_inv (insert b S) (insert b a) b (it - {x})))
 4. \<And>D S u a b \<sigma> x it \<sigma>' aa ba. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None; \<sigma>' = (aa, ba); \<not> x \<notin> aa\<rbrakk> \<Longrightarrow> fe_inv (insert b S) (insert b a) b (it - {x}) (aa, None)
 5. \<And>D S u a b \<sigma> \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; fe_inv (insert b S) (insert b a) b {} \<sigma>'\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 6. \<And>D S u a b \<sigma> it \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; it \<noteq> {}; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; \<not> (case \<sigma>' of (V, brk) \<Rightarrow> brk = None)\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 7. \<And>D S u a b \<sigma> x. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = Some x\<rbrakk> \<Longrightarrow> post S u (insert b a, \<sigma>)
 8. \<And>D S u a b it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); it \<noteq> {}; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> \<noteq> None\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
[PROOF STEP]
apply (rule gen_dfs_fe_inv_imp_pre, assumption+) []
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>D S u a b \<sigma> x it \<sigma>' aa ba. \<lbrakk>pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None; \<sigma>' = (aa, ba); x \<notin> aa\<rbrakk> \<Longrightarrow> ((aa, x), u) \<in> gen_dfs_var U <*lex*> {}
 2. \<And>D S u a b \<sigma> x it \<sigma>' aa ba. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None; \<sigma>' = (aa, ba); x \<notin> aa\<rbrakk> \<Longrightarrow> SPEC (post (insert b S) (aa, x)) \<le> SPEC (\<lambda>xa. (case xa of (V, brk) \<Rightarrow> RETURN (V, prep_wit_red b brk)) \<le> SPEC (fe_inv (insert b S) (insert b a) b (it - {x})))
 3. \<And>D S u a b \<sigma> x it \<sigma>' aa ba. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None; \<sigma>' = (aa, ba); \<not> x \<notin> aa\<rbrakk> \<Longrightarrow> fe_inv (insert b S) (insert b a) b (it - {x}) (aa, None)
 4. \<And>D S u a b \<sigma> \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; fe_inv (insert b S) (insert b a) b {} \<sigma>'\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 5. \<And>D S u a b \<sigma> it \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; it \<noteq> {}; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; \<not> (case \<sigma>' of (V, brk) \<Rightarrow> brk = None)\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 6. \<And>D S u a b \<sigma> x. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = Some x\<rbrakk> \<Longrightarrow> post S u (insert b a, \<sigma>)
 7. \<And>D S u a b it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); it \<noteq> {}; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> \<noteq> None\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
[PROOF STEP]
apply (auto simp add: pre_def fe_inv_def intro: gen_dfs_fe_inv_imp_var) []
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>D S u a b \<sigma> x it \<sigma>' aa ba. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None; \<sigma>' = (aa, ba); x \<notin> aa\<rbrakk> \<Longrightarrow> SPEC (post (insert b S) (aa, x)) \<le> SPEC (\<lambda>xa. (case xa of (V, brk) \<Rightarrow> RETURN (V, prep_wit_red b brk)) \<le> SPEC (fe_inv (insert b S) (insert b a) b (it - {x})))
 2. \<And>D S u a b \<sigma> x it \<sigma>' aa ba. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None; \<sigma>' = (aa, ba); \<not> x \<notin> aa\<rbrakk> \<Longrightarrow> fe_inv (insert b S) (insert b a) b (it - {x}) (aa, None)
 3. \<And>D S u a b \<sigma> \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; fe_inv (insert b S) (insert b a) b {} \<sigma>'\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 4. \<And>D S u a b \<sigma> it \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; it \<noteq> {}; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; \<not> (case \<sigma>' of (V, brk) \<Rightarrow> brk = None)\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 5. \<And>D S u a b \<sigma> x. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = Some x\<rbrakk> \<Longrightarrow> post S u (insert b a, \<sigma>)
 6. \<And>D S u a b it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); it \<noteq> {}; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> \<noteq> None\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
[PROOF STEP]
apply (clarsimp simp add: pre_def post_def fe_inv_def
        split: option.split_asm prod.split_asm
        ) []
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>S aa ba x it aaa ac. \<lbrakk>\<And>arb' a b. \<lbrakk>gen_dfs_pre E U arb' a b \<and> E `` a \<inter> onstack = {}; (a, aa) \<in> gen_dfs_var U\<rbrakk> \<Longrightarrow> REC\<^sub>T (\<lambda>D (V, u). FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (insert u V, None) | Some a \<Rightarrow> RETURN (insert u V, brk))) (a, b) \<le> SPEC (\<lambda>(V, cyc). gen_dfs_post E U arb' a b V (\<exists>a b. cyc = Some (a, b)) \<and> (case cyc of None \<Rightarrow> E `` V \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v)); E `` {ba} \<inter> onstack = {}; x \<in> it; it \<subseteq> E `` {ba}; x \<notin> aaa; gen_dfs_pre E U S aa ba; E `` aa \<inter> onstack = {}; gen_dfs_fe_inv E U (insert ba S) (insert ba aa) ba it aaa False; E `` aaa \<inter> onstack = {}; gen_dfs_post E U (insert ba S) aaa x ac False; E `` ac \<inter> onstack = {}\<rbrakk> \<Longrightarrow> gen_dfs_fe_inv E U (insert ba S) (insert ba aa) ba (it - {x}) ac False
 2. \<And>S aa ba x it aaa ac bc x2 x1 x2a. \<lbrakk>\<And>arb' a b. \<lbrakk>gen_dfs_pre E U arb' a b \<and> E `` a \<inter> onstack = {}; (a, aa) \<in> gen_dfs_var U\<rbrakk> \<Longrightarrow> REC\<^sub>T (\<lambda>D (V, u). FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (insert u V, None) | Some a \<Rightarrow> RETURN (insert u V, brk))) (a, b) \<le> SPEC (\<lambda>(V, cyc). gen_dfs_post E U arb' a b V (\<exists>a b. cyc = Some (a, b)) \<and> (case cyc of None \<Rightarrow> E `` V \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v)); E `` {ba} \<inter> onstack = {}; x \<in> it; it \<subseteq> E `` {ba}; x \<notin> aaa; gen_dfs_pre E U S aa ba; E `` aa \<inter> onstack = {}; gen_dfs_fe_inv E U (insert ba S) (insert ba aa) ba it aaa False; E `` aaa \<inter> onstack = {}; gen_dfs_post E U (insert ba S) aaa x ac True; bc = Some (x1, x2a); x2 = (x1, x2a); x2a \<in> onstack \<and> x1 \<noteq> [] \<and> path E x x1 x2a\<rbrakk> \<Longrightarrow> gen_dfs_fe_inv E U (insert ba S) (insert ba aa) ba (it - {x}) ac True \<and> path E ba (ba # x1) x2a
 3. \<And>D S u a b \<sigma> x it \<sigma>' aa ba. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None; \<sigma>' = (aa, ba); \<not> x \<notin> aa\<rbrakk> \<Longrightarrow> fe_inv (insert b S) (insert b a) b (it - {x}) (aa, None)
 4. \<And>D S u a b \<sigma> \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; fe_inv (insert b S) (insert b a) b {} \<sigma>'\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 5. \<And>D S u a b \<sigma> it \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; it \<noteq> {}; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; \<not> (case \<sigma>' of (V, brk) \<Rightarrow> brk = None)\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 6. \<And>D S u a b \<sigma> x. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = Some x\<rbrakk> \<Longrightarrow> post S u (insert b a, \<sigma>)
 7. \<And>D S u a b it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); it \<noteq> {}; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> \<noteq> None\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
[PROOF STEP]
apply (blast intro: gen_dfs_post_imp_fe_inv)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>S aa ba x it aaa ac bc x2 x1 x2a. \<lbrakk>\<And>arb' a b. \<lbrakk>gen_dfs_pre E U arb' a b \<and> E `` a \<inter> onstack = {}; (a, aa) \<in> gen_dfs_var U\<rbrakk> \<Longrightarrow> REC\<^sub>T (\<lambda>D (V, u). FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (insert u V, None) | Some a \<Rightarrow> RETURN (insert u V, brk))) (a, b) \<le> SPEC (\<lambda>(V, cyc). gen_dfs_post E U arb' a b V (\<exists>a b. cyc = Some (a, b)) \<and> (case cyc of None \<Rightarrow> E `` V \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v)); E `` {ba} \<inter> onstack = {}; x \<in> it; it \<subseteq> E `` {ba}; x \<notin> aaa; gen_dfs_pre E U S aa ba; E `` aa \<inter> onstack = {}; gen_dfs_fe_inv E U (insert ba S) (insert ba aa) ba it aaa False; E `` aaa \<inter> onstack = {}; gen_dfs_post E U (insert ba S) aaa x ac True; bc = Some (x1, x2a); x2 = (x1, x2a); x2a \<in> onstack \<and> x1 \<noteq> [] \<and> path E x x1 x2a\<rbrakk> \<Longrightarrow> gen_dfs_fe_inv E U (insert ba S) (insert ba aa) ba (it - {x}) ac True \<and> path E ba (ba # x1) x2a
 2. \<And>D S u a b \<sigma> x it \<sigma>' aa ba. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None; \<sigma>' = (aa, ba); \<not> x \<notin> aa\<rbrakk> \<Longrightarrow> fe_inv (insert b S) (insert b a) b (it - {x}) (aa, None)
 3. \<And>D S u a b \<sigma> \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; fe_inv (insert b S) (insert b a) b {} \<sigma>'\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 4. \<And>D S u a b \<sigma> it \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; it \<noteq> {}; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; \<not> (case \<sigma>' of (V, brk) \<Rightarrow> brk = None)\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 5. \<And>D S u a b \<sigma> x. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = Some x\<rbrakk> \<Longrightarrow> post S u (insert b a, \<sigma>)
 6. \<And>D S u a b it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); it \<noteq> {}; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> \<noteq> None\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
[PROOF STEP]
apply (blast intro: gen_dfs_post_imp_fe_inv path_prepend)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>D S u a b \<sigma> x it \<sigma>' aa ba. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; x \<in> it; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; case \<sigma>' of (V, brk) \<Rightarrow> brk = None; \<sigma>' = (aa, ba); \<not> x \<notin> aa\<rbrakk> \<Longrightarrow> fe_inv (insert b S) (insert b a) b (it - {x}) (aa, None)
 2. \<And>D S u a b \<sigma> \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; fe_inv (insert b S) (insert b a) b {} \<sigma>'\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 3. \<And>D S u a b \<sigma> it \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; it \<noteq> {}; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; \<not> (case \<sigma>' of (V, brk) \<Rightarrow> brk = None)\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 4. \<And>D S u a b \<sigma> x. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = Some x\<rbrakk> \<Longrightarrow> post S u (insert b a, \<sigma>)
 5. \<And>D S u a b it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); it \<noteq> {}; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> \<noteq> None\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
[PROOF STEP]
apply (auto simp add: pre_def post_def fe_inv_def
        intro: gen_dfs_fe_inv_pres_visited) []
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>D S u a b \<sigma> \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; fe_inv (insert b S) (insert b a) b {} \<sigma>'\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 2. \<And>D S u a b \<sigma> it \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; it \<noteq> {}; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; \<not> (case \<sigma>' of (V, brk) \<Rightarrow> brk = None)\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 3. \<And>D S u a b \<sigma> x. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = Some x\<rbrakk> \<Longrightarrow> post S u (insert b a, \<sigma>)
 4. \<And>D S u a b it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); it \<noteq> {}; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> \<noteq> None\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
[PROOF STEP]
apply (auto simp add: pre_def post_def fe_inv_def
        intro: gen_dfs_fe_inv_imp_post) []
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>D S u a b \<sigma> it \<sigma>'. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = None; it \<noteq> {}; it \<subseteq> E `` {b}; fe_inv (insert b S) (insert b a) b it \<sigma>'; \<not> (case \<sigma>' of (V, brk) \<Rightarrow> brk = None)\<rbrakk> \<Longrightarrow> post S u \<sigma>'
 2. \<And>D S u a b \<sigma> x. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = Some x\<rbrakk> \<Longrightarrow> post S u (insert b a, \<sigma>)
 3. \<And>D S u a b it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); it \<noteq> {}; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> \<noteq> None\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
[PROOF STEP]
apply (auto simp add: pre_def post_def fe_inv_def
        intro: gen_dfs_fe_imp_post_brk) []
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>D S u a b \<sigma> x. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); case \<sigma> of None \<Rightarrow> (E `` {b} - {}) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> = Some x\<rbrakk> \<Longrightarrow> post S u (insert b a, \<sigma>)
 2. \<And>D S u a b it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); it \<noteq> {}; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> \<noteq> None\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
[PROOF STEP]
apply (auto simp add: pre_def post_def fe_inv_def
        intro: gen_dfs_pre_imp_post_brk) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>D S u a b it \<sigma>. \<lbrakk>\<And>arb' x'. \<lbrakk>pre arb' x'; (x', u) \<in> gen_dfs_var U <*lex*> {}\<rbrakk> \<Longrightarrow> D x' \<le> SPEC (post arb' x'); pre S u; REC\<^sub>T (\<lambda>D a. case a of (V, u) \<Rightarrow> let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) = D; u = (a, b); it \<noteq> {}; it \<subseteq> E `` {b}; case \<sigma> of None \<Rightarrow> (E `` {b} - it) \<inter> onstack = {} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E b p v; \<sigma> \<noteq> None\<rbrakk> \<Longrightarrow> (case \<sigma> of None \<Rightarrow> FOREACH\<^sub>C (E `` {b}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red b brk)) else RETURN (V, None)) (insert b a, None) | Some aa \<Rightarrow> RETURN (insert b a, \<sigma>)) \<le> SPEC (post S u)
[PROOF STEP]
apply (auto simp add: pre_def post_def fe_inv_def
        intro: gen_dfs_pre_imp_post_brk) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
REC\<^sub>T (\<lambda>D (V, u). let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) \<sigma> \<le> SPEC (post S \<sigma>)

goal (1 subgoal):
 1. red_dfs E onstack reds u0 \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
pre ?S2 ?\<sigma>2 \<Longrightarrow> REC\<^sub>T (\<lambda>D (V, u). let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) ?\<sigma>2 \<le> SPEC (post ?S2 ?\<sigma>2)

goal (1 subgoal):
 1. red_dfs E onstack reds u0 \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)
[PROOF STEP]
note GEN=this
[PROOF STATE]
proof (state)
this:
pre ?S2 ?\<sigma>2 \<Longrightarrow> REC\<^sub>T (\<lambda>D (V, u). let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) ?\<sigma>2 \<le> SPEC (post ?S2 ?\<sigma>2)

goal (1 subgoal):
 1. red_dfs E onstack reds u0 \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)
[PROOF STEP]
note GEN[OF PRE']
[PROOF STATE]
proof (state)
this:
REC\<^sub>T (\<lambda>D (V, u). let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) (reds, u0) \<le> SPEC (post {} (reds, u0))

goal (1 subgoal):
 1. red_dfs E onstack reds u0 \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
REC\<^sub>T (\<lambda>D (V, u). let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) (reds, u0) \<le> SPEC (post {} (reds, u0))

goal (1 subgoal):
 1. red_dfs E onstack reds u0 \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)
[PROOF STEP]
note IMP_POST
[PROOF STATE]
proof (state)
this:
SPEC (post {} (reds, u0)) \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)

goal (1 subgoal):
 1. red_dfs E onstack reds u0 \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
REC\<^sub>T (\<lambda>D (V, u). let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) (reds, u0) \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
REC\<^sub>T (\<lambda>D (V, u). let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) (reds, u0) \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)

goal (1 subgoal):
 1. red_dfs E onstack reds u0 \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)
[PROOF STEP]
unfolding red_dfs_def
[PROOF STATE]
proof (prove)
using this:
REC\<^sub>T (\<lambda>D (V, u). let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) (reds, u0) \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)

goal (1 subgoal):
 1. REC\<^sub>T (\<lambda>D (V, u). let V = insert u V in NDFS_SI_Statistics.vis_red_nres \<bind> (\<lambda>_. FOREACH\<^sub>C (E `` {u}) (\<lambda>brk. brk = None) (\<lambda>t _. if t \<in> onstack then RETURN (red_init_witness u t) else RETURN None) None \<bind> (\<lambda>brk. case brk of None \<Rightarrow> FOREACH\<^sub>C (E `` {u}) (\<lambda>(V, brk). brk = None) (\<lambda>t (V, uu_). if t \<notin> V then D (V, t) \<bind> (\<lambda>(V, brk). RETURN (V, prep_wit_red u brk)) else RETURN (V, None)) (V, None) | Some a \<Rightarrow> RETURN (V, brk)))) (reds, u0) \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
red_dfs E onstack reds u0 \<le> SPEC (\<lambda>(reds', cyc). case cyc of None \<Rightarrow> red_dfs_inv E U reds' onstack \<and> u0 \<in> reds' \<and> reds' \<subseteq> reds \<union> E\<^sup>* `` {u0} | Some (p, v) \<Rightarrow> v \<in> onstack \<and> p \<noteq> [] \<and> path E u0 p v)

goal:
No subgoals!
[PROOF STEP]
qed