[STATEMENT]
lemma silent_move_preserves_stacks:
  assumes "S,f \<turnstile> (m#ms,s) -a\<rightarrow>\<^sub>\<tau> (m'#ms',s')" and "valid_call_list cs m"
  and "\<forall>i < length rs. rs!i \<in> get_return_edges (cs!i)" and "valid_return_list rs m"
  and "length rs = length cs" and "ms = targetnodes rs"
  obtains cs' rs' where "valid_node m'" and "valid_call_list cs' m'"
  and "\<forall>i < length rs'. rs'!i \<in> get_return_edges (cs'!i)"
  and "valid_return_list rs' m'" and "length rs' = length cs'"
  and "ms' = targetnodes rs'" and "upd_cs cs [a] = cs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>cs' rs'. \<lbrakk>valid_node m'; valid_call_list cs' m'; \<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i); valid_return_list rs' m'; length rs' = length cs'; ms' = targetnodes rs'; upd_cs cs [a] = cs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (m' # ms',s')
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs
[PROOF STEP]
show "\<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and>
    (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and>
    valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and>
    upd_cs cs [a] = cs'"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (m' # ms',s')
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs

goal (1 subgoal):
 1. \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
proof(induct S f "m#ms" s a "m'#ms'" s' rule:silent_move.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>f a s s' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind (kind a); (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length s' = length s; length (m # ms) = length s; hd (m # ms) = sourcenode a; m' # ms' = targetnode a # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 3. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
case (silent_move_intra f a s s' n\<^sub>c)
[PROOF STATE]
proof (state)
this:
pred (f a) s
transfer (f a) s = s'
valid_edge a
intra_kind (kind a)
(\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice n\<^sub>c\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice n\<^sub>c\<rfloor>\<^bsub>CFG\<^esub>
Ball (set (tl (m # ms))) return_node
length s' = length s
length (m # ms) = length s
hd (m # ms) = sourcenode a
m' # ms' = targetnode a # tl (m # ms)
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs

goal (3 subgoals):
 1. \<And>f a s s' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind (kind a); (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length s' = length s; length (m # ms) = length s; hd (m # ms) = sourcenode a; m' # ms' = targetnode a # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 3. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>hd (m # ms) = sourcenode a\<close>
[PROOF STATE]
proof (chain)
picking this:
hd (m # ms) = sourcenode a
[PROOF STEP]
have "m = sourcenode a"
[PROOF STATE]
proof (prove)
using this:
hd (m # ms) = sourcenode a

goal (1 subgoal):
 1. m = sourcenode a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m = sourcenode a

goal (3 subgoals):
 1. \<And>f a s s' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind (kind a); (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length s' = length s; length (m # ms) = length s; hd (m # ms) = sourcenode a; m' # ms' = targetnode a # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 3. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>m' # ms' = targetnode a # tl (m # ms)\<close>
[PROOF STATE]
proof (chain)
picking this:
m' # ms' = targetnode a # tl (m # ms)
[PROOF STEP]
have [simp]:"m' = targetnode a" "ms' = ms"
[PROOF STATE]
proof (prove)
using this:
m' # ms' = targetnode a # tl (m # ms)

goal (1 subgoal):
 1. m' = targetnode a &&& ms' = ms
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
m' = targetnode a
ms' = ms

goal (3 subgoals):
 1. \<And>f a s s' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind (kind a); (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length s' = length s; length (m # ms) = length s; hd (m # ms) = sourcenode a; m' # ms' = targetnode a # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 3. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>valid_edge a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
[PROOF STEP]
have "valid_node m'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a

goal (1 subgoal):
 1. valid_node m'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
valid_node m'

goal (3 subgoals):
 1. \<And>f a s s' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind (kind a); (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length s' = length s; length (m # ms) = length s; hd (m # ms) = sourcenode a; m' # ms' = targetnode a # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 3. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_node m'

goal (3 subgoals):
 1. \<And>f a s s' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind (kind a); (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length s' = length s; length (m # ms) = length s; hd (m # ms) = sourcenode a; m' # ms' = targetnode a # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 3. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>intra_kind (kind a)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
intra_kind (kind a)
[PROOF STEP]
have "get_proc (sourcenode a) = get_proc (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
intra_kind (kind a)

goal (1 subgoal):
 1. get_proc (sourcenode a) = get_proc (targetnode a)
[PROOF STEP]
by(rule get_proc_intra)
[PROOF STATE]
proof (state)
this:
get_proc (sourcenode a) = get_proc (targetnode a)

goal (3 subgoals):
 1. \<And>f a s s' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind (kind a); (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length s' = length s; length (m # ms) = length s; hd (m # ms) = sourcenode a; m' # ms' = targetnode a # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 3. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>valid_call_list cs m\<close> \<open>m = sourcenode a\<close>
      \<open>get_proc (sourcenode a) = get_proc (targetnode a)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_call_list cs m
m = sourcenode a
get_proc (sourcenode a) = get_proc (targetnode a)
[PROOF STEP]
have "valid_call_list cs m'"
[PROOF STATE]
proof (prove)
using this:
valid_call_list cs m
m = sourcenode a
get_proc (sourcenode a) = get_proc (targetnode a)

goal (1 subgoal):
 1. valid_call_list cs m'
[PROOF STEP]
apply(clarsimp simp:valid_call_list_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs''. \<lbrakk>\<forall>cs'a ca. (\<exists>cs''a. cs' @ c # cs'' = cs'a @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q r fs. kind ca = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs'a of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (sourcenodes cs'a))\<^esub>fs); m = sourcenode a; get_proc (sourcenode a) = get_proc (targetnode a); cs = cs' @ c # cs''\<rbrakk> \<Longrightarrow> \<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs
[PROOF STEP]
apply(erule_tac x="cs'" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs''. \<lbrakk>m = sourcenode a; get_proc (sourcenode a) = get_proc (targetnode a); cs = cs' @ c # cs''; \<forall>ca. (\<exists>cs''a. cs' @ c # cs'' = cs' @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q r fs. kind ca = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs)\<rbrakk> \<Longrightarrow> \<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs
[PROOF STEP]
apply(erule_tac x="c" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs''. \<lbrakk>m = sourcenode a; get_proc (sourcenode a) = get_proc (targetnode a); cs = cs' @ c # cs''; (\<exists>cs''a. cs' @ c # cs'' = cs' @ c # cs''a) \<longrightarrow> valid_edge c \<and> (\<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs)\<rbrakk> \<Longrightarrow> \<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs
[PROOF STEP]
by(auto split:list.split)
[PROOF STATE]
proof (state)
this:
valid_call_list cs m'

goal (3 subgoals):
 1. \<And>f a s s' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind (kind a); (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length s' = length s; length (m # ms) = length s; hd (m # ms) = sourcenode a; m' # ms' = targetnode a # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 3. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_call_list cs m'

goal (3 subgoals):
 1. \<And>f a s s' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind (kind a); (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length s' = length s; length (m # ms) = length s; hd (m # ms) = sourcenode a; m' # ms' = targetnode a # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 3. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>valid_return_list rs m\<close> \<open>m = sourcenode a\<close>
      \<open>get_proc (sourcenode a) = get_proc (targetnode a)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_return_list rs m
m = sourcenode a
get_proc (sourcenode a) = get_proc (targetnode a)
[PROOF STEP]
have "valid_return_list rs m'"
[PROOF STATE]
proof (prove)
using this:
valid_return_list rs m
m = sourcenode a
get_proc (sourcenode a) = get_proc (targetnode a)

goal (1 subgoal):
 1. valid_return_list rs m'
[PROOF STEP]
apply(clarsimp simp:valid_return_list_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs''. \<lbrakk>\<forall>cs'a ca. (\<exists>cs''a. cs' @ c # cs'' = cs'a @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q f. kind ca = Q\<hookleftarrow>\<^bsub>get_proc (case cs'a of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (targetnodes cs'a))\<^esub>f); m = sourcenode a; get_proc (sourcenode a) = get_proc (targetnode a); rs = cs' @ c # cs''\<rbrakk> \<Longrightarrow> \<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f
[PROOF STEP]
apply(erule_tac x="cs'" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs''. \<lbrakk>m = sourcenode a; get_proc (sourcenode a) = get_proc (targetnode a); rs = cs' @ c # cs''; \<forall>ca. (\<exists>cs''a. cs' @ c # cs'' = cs' @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q f. kind ca = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f)\<rbrakk> \<Longrightarrow> \<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs'' Q f. \<lbrakk>m = sourcenode a; get_proc (sourcenode a) = get_proc (targetnode a); rs = cs' @ c # cs''; valid_edge c; kind c = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f\<rbrakk> \<Longrightarrow> get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (targetnodes cs')) = get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (targetnodes cs'))
[PROOF STEP]
by(case_tac cs') auto
[PROOF STATE]
proof (state)
this:
valid_return_list rs m'

goal (3 subgoals):
 1. \<And>f a s s' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind (kind a); (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length s' = length s; length (m # ms) = length s; hd (m # ms) = sourcenode a; m' # ms' = targetnode a # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 3. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_return_list rs m'

goal (3 subgoals):
 1. \<And>f a s s' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind (kind a); (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length s' = length s; length (m # ms) = length s; hd (m # ms) = sourcenode a; m' # ms' = targetnode a # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 3. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>intra_kind (kind a)\<close>
[PROOF STATE]
proof (chain)
picking this:
intra_kind (kind a)
[PROOF STEP]
have "upd_cs cs [a] = cs"
[PROOF STATE]
proof (prove)
using this:
intra_kind (kind a)

goal (1 subgoal):
 1. upd_cs cs [a] = cs
[PROOF STEP]
by(fastforce simp:intra_kind_def)
[PROOF STATE]
proof (state)
this:
upd_cs cs [a] = cs

goal (3 subgoals):
 1. \<And>f a s s' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind (kind a); (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length s' = length s; length (m # ms) = length s; hd (m # ms) = sourcenode a; m' # ms' = targetnode a # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 3. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
valid_node m'
valid_call_list cs m'
valid_return_list rs m'
upd_cs cs [a] = cs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
valid_node m'
valid_call_list cs m'
valid_return_list rs m'
upd_cs cs [a] = cs

goal (1 subgoal):
 1. \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
using \<open>\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)\<close>
      \<open>length rs = length cs\<close> \<open>ms = targetnodes rs\<close>
[PROOF STATE]
proof (prove)
using this:
valid_node m'
valid_call_list cs m'
valid_return_list rs m'
upd_cs cs [a] = cs
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
length rs = length cs
ms = targetnodes rs

goal (1 subgoal):
 1. \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
apply(rule_tac x="cs" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_node m'; valid_call_list cs m'; valid_return_list rs m'; upd_cs cs [a] = cs; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>rs'. valid_node m' \<and> valid_call_list cs m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs
[PROOF STEP]
apply(rule_tac x="rs" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_node m'; valid_call_list cs m'; valid_return_list rs m'; upd_cs cs [a] = cs; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> valid_node m' \<and> valid_call_list cs m' \<and> (\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)) \<and> valid_return_list rs m' \<and> length rs = length cs \<and> ms' = targetnodes rs \<and> upd_cs cs [a] = cs
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
\<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
case (silent_move_call f a s s' Q r p fs a' S)
[PROOF STATE]
proof (state)
this:
pred (f a) s
transfer (f a) s = s'
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
valid_edge a'
a' \<in> get_return_edges a
(\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
Ball (set (tl (m # ms))) return_node
length (m # ms) = length s
length s' = Suc (length s)
hd (m # ms) = sourcenode a
m' # ms' = targetnode a # targetnode a' # tl (m # ms)
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>hd (m # ms) = sourcenode a\<close>
      \<open>m' # ms' = targetnode a # targetnode a' # tl (m # ms)\<close>
[PROOF STATE]
proof (chain)
picking this:
hd (m # ms) = sourcenode a
m' # ms' = targetnode a # targetnode a' # tl (m # ms)
[PROOF STEP]
have [simp]:"m = sourcenode a" "m' = targetnode a"
      "ms' = targetnode a' # tl (m # ms)"
[PROOF STATE]
proof (prove)
using this:
hd (m # ms) = sourcenode a
m' # ms' = targetnode a # targetnode a' # tl (m # ms)

goal (1 subgoal):
 1. m = sourcenode a &&& m' = targetnode a &&& ms' = targetnode a' # tl (m # ms)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
m = sourcenode a
m' = targetnode a
ms' = targetnode a' # tl (m # ms)

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>valid_edge a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
[PROOF STEP]
have "valid_node m'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a

goal (1 subgoal):
 1. valid_node m'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
valid_node m'

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_node m'

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
have "get_proc (targetnode a) = p"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. get_proc (targetnode a) = p
[PROOF STEP]
by(rule get_proc_call)
[PROOF STATE]
proof (state)
this:
get_proc (targetnode a) = p

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
with \<open>valid_call_list cs m\<close> \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>m = sourcenode a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_call_list cs m
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
m = sourcenode a
get_proc (targetnode a) = p
[PROOF STEP]
have "valid_call_list (a # cs) (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_call_list cs m
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
m = sourcenode a
get_proc (targetnode a) = p

goal (1 subgoal):
 1. valid_call_list (a # cs) (targetnode a)
[PROOF STEP]
apply(clarsimp simp:valid_call_list_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs''. \<lbrakk>\<forall>cs' c. (\<exists>cs''. cs = cs' @ c # cs'') \<longrightarrow> valid_edge c \<and> (\<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs); valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>get_proc (targetnode a)\<^esub>fs; p = get_proc (targetnode a); a # cs = cs' @ c # cs''\<rbrakk> \<Longrightarrow> valid_edge c \<and> (\<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs)
[PROOF STEP]
apply(case_tac cs')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>cs' c cs''. \<lbrakk>\<forall>cs' c. (\<exists>cs''. cs = cs' @ c # cs'') \<longrightarrow> valid_edge c \<and> (\<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs); valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>get_proc (targetnode a)\<^esub>fs; p = get_proc (targetnode a); a # cs = cs' @ c # cs''; cs' = []\<rbrakk> \<Longrightarrow> valid_edge c \<and> (\<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs)
 2. \<And>cs' c cs'' a list. \<lbrakk>\<forall>cs' c. (\<exists>cs''. cs = cs' @ c # cs'') \<longrightarrow> valid_edge c \<and> (\<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs); valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>get_proc (targetnode a)\<^esub>fs; p = get_proc (targetnode a); a # cs = cs' @ c # cs''; cs' = a # list\<rbrakk> \<Longrightarrow> valid_edge c \<and> (\<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c cs'' list. \<lbrakk>\<forall>cs' ca. (\<exists>cs''a. list @ c # cs'' = cs' @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q r fs. kind ca = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs); valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>get_proc (targetnode a)\<^esub>fs; p = get_proc (targetnode a); cs = list @ c # cs''\<rbrakk> \<Longrightarrow> \<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (last (sourcenodes (a # list)))\<^esub>fs
[PROOF STEP]
apply(erule_tac x="list" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c cs'' list. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>get_proc (targetnode a)\<^esub>fs; p = get_proc (targetnode a); cs = list @ c # cs''; \<forall>ca. (\<exists>cs''a. list @ c # cs'' = list @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q r fs. kind ca = Q:r\<hookrightarrow>\<^bsub>get_proc (case list of [] \<Rightarrow> sourcenode a | a # lista \<Rightarrow> last (sourcenodes list))\<^esub>fs)\<rbrakk> \<Longrightarrow> \<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (last (sourcenodes (a # list)))\<^esub>fs
[PROOF STEP]
by(case_tac list)(auto simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
valid_call_list (a # cs) (targetnode a)

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_call_list (a # cs) (targetnode a)

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)\<close> \<open>a' \<in> get_return_edges a\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
a' \<in> get_return_edges a
[PROOF STEP]
have "\<forall>i<length (a'#rs). (a'#rs) ! i \<in> get_return_edges ((a#cs) ! i)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
a' \<in> get_return_edges a

goal (1 subgoal):
 1. \<forall>i<length (a' # rs). (a' # rs) ! i \<in> get_return_edges ((a # cs) ! i)
[PROOF STEP]
by auto(case_tac i,auto)
[PROOF STATE]
proof (state)
this:
\<forall>i<length (a' # rs). (a' # rs) ! i \<in> get_return_edges ((a # cs) ! i)

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>i<length (a' # rs). (a' # rs) ! i \<in> get_return_edges ((a # cs) ! i)

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>a' \<in> get_return_edges a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
a' \<in> get_return_edges a
[PROOF STEP]
have "valid_edge a'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
a' \<in> get_return_edges a

goal (1 subgoal):
 1. valid_edge a'
[PROOF STEP]
by(rule get_return_edges_valid)
[PROOF STATE]
proof (state)
this:
valid_edge a'

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>a' \<in> get_return_edges a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
a' \<in> get_return_edges a
[PROOF STEP]
obtain Q' f' where "kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
a' \<in> get_return_edges a

goal (1 subgoal):
 1. (\<And>Q' f'. kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce dest!:call_return_edges)
[PROOF STATE]
proof (state)
this:
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>valid_edge a'\<close> \<open>kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
[PROOF STEP]
have "get_proc (sourcenode a') = p"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'

goal (1 subgoal):
 1. get_proc (sourcenode a') = p
[PROOF STEP]
by(rule get_proc_return)
[PROOF STATE]
proof (state)
this:
get_proc (sourcenode a') = p

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>a' \<in> get_return_edges a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
a' \<in> get_return_edges a
[PROOF STEP]
have "get_proc (sourcenode a) = get_proc (targetnode a')"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
a' \<in> get_return_edges a

goal (1 subgoal):
 1. get_proc (sourcenode a) = get_proc (targetnode a')
[PROOF STEP]
by(rule get_proc_get_return_edge)
[PROOF STATE]
proof (state)
this:
get_proc (sourcenode a) = get_proc (targetnode a')

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
with \<open>valid_return_list rs m\<close> \<open>valid_edge a'\<close> \<open>kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'\<close>
      \<open>get_proc (sourcenode a') = p\<close> \<open>get_proc (targetnode a) = p\<close> \<open>m = sourcenode a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_return_list rs m
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
get_proc (sourcenode a') = p
get_proc (targetnode a) = p
m = sourcenode a
get_proc (sourcenode a) = get_proc (targetnode a')
[PROOF STEP]
have "valid_return_list (a'#rs) (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_return_list rs m
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
get_proc (sourcenode a') = p
get_proc (targetnode a) = p
m = sourcenode a
get_proc (sourcenode a) = get_proc (targetnode a')

goal (1 subgoal):
 1. valid_return_list (a' # rs) (targetnode a)
[PROOF STEP]
apply(clarsimp simp:valid_return_list_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs''. \<lbrakk>\<forall>cs' c. (\<exists>cs''. rs = cs' @ c # cs'') \<longrightarrow> valid_edge c \<and> (\<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f); valid_edge a'; kind a' = Q'\<hookleftarrow>\<^bsub>get_proc (sourcenode a')\<^esub>f'; get_proc (targetnode a) = get_proc (sourcenode a'); get_proc (sourcenode a) = get_proc (targetnode a'); p = get_proc (sourcenode a'); a' # rs = cs' @ c # cs''\<rbrakk> \<Longrightarrow> valid_edge c \<and> (\<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f)
[PROOF STEP]
apply(case_tac cs')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>cs' c cs''. \<lbrakk>\<forall>cs' c. (\<exists>cs''. rs = cs' @ c # cs'') \<longrightarrow> valid_edge c \<and> (\<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f); valid_edge a'; kind a' = Q'\<hookleftarrow>\<^bsub>get_proc (sourcenode a')\<^esub>f'; get_proc (targetnode a) = get_proc (sourcenode a'); get_proc (sourcenode a) = get_proc (targetnode a'); p = get_proc (sourcenode a'); a' # rs = cs' @ c # cs''; cs' = []\<rbrakk> \<Longrightarrow> valid_edge c \<and> (\<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f)
 2. \<And>cs' c cs'' a list. \<lbrakk>\<forall>cs' c. (\<exists>cs''. rs = cs' @ c # cs'') \<longrightarrow> valid_edge c \<and> (\<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f); valid_edge a'; kind a' = Q'\<hookleftarrow>\<^bsub>get_proc (sourcenode a')\<^esub>f'; get_proc (targetnode a) = get_proc (sourcenode a'); get_proc (sourcenode a) = get_proc (targetnode a'); p = get_proc (sourcenode a'); a' # rs = cs' @ c # cs''; cs' = a # list\<rbrakk> \<Longrightarrow> valid_edge c \<and> (\<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c cs'' list. \<lbrakk>\<forall>cs' ca. (\<exists>cs''a. list @ c # cs'' = cs' @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q f. kind ca = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f); valid_edge a'; kind a' = Q'\<hookleftarrow>\<^bsub>get_proc (sourcenode a')\<^esub>f'; get_proc (targetnode a) = get_proc (sourcenode a'); get_proc (sourcenode a) = get_proc (targetnode a'); p = get_proc (sourcenode a'); rs = list @ c # cs''\<rbrakk> \<Longrightarrow> \<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (last (targetnodes (a' # list)))\<^esub>f
[PROOF STEP]
apply(erule_tac x="list" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c cs'' list. \<lbrakk>valid_edge a'; kind a' = Q'\<hookleftarrow>\<^bsub>get_proc (sourcenode a')\<^esub>f'; get_proc (targetnode a) = get_proc (sourcenode a'); get_proc (sourcenode a) = get_proc (targetnode a'); p = get_proc (sourcenode a'); rs = list @ c # cs''; \<forall>ca. (\<exists>cs''a. list @ c # cs'' = list @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q f. kind ca = Q\<hookleftarrow>\<^bsub>get_proc (case list of [] \<Rightarrow> sourcenode a | a # lista \<Rightarrow> last (targetnodes list))\<^esub>f)\<rbrakk> \<Longrightarrow> \<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (last (targetnodes (a' # list)))\<^esub>f
[PROOF STEP]
by(case_tac list)(auto simp:targetnodes_def)
[PROOF STATE]
proof (state)
this:
valid_return_list (a' # rs) (targetnode a)

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_return_list (a' # rs) (targetnode a)

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>length rs = length cs\<close>
[PROOF STATE]
proof (chain)
picking this:
length rs = length cs
[PROOF STEP]
have "length (a'#rs) = length (a#cs)"
[PROOF STATE]
proof (prove)
using this:
length rs = length cs

goal (1 subgoal):
 1. length (a' # rs) = length (a # cs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (a' # rs) = length (a # cs)

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length (a' # rs) = length (a # cs)

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>ms = targetnodes rs\<close>
[PROOF STATE]
proof (chain)
picking this:
ms = targetnodes rs
[PROOF STEP]
have "targetnode a' # ms = targetnodes (a' # rs)"
[PROOF STATE]
proof (prove)
using this:
ms = targetnodes rs

goal (1 subgoal):
 1. targetnode a' # ms = targetnodes (a' # rs)
[PROOF STEP]
by(simp add:targetnodes_def)
[PROOF STATE]
proof (state)
this:
targetnode a' # ms = targetnodes (a' # rs)

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
targetnode a' # ms = targetnodes (a' # rs)

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
have "upd_cs cs [a] = a#cs"
[PROOF STATE]
proof (prove)
using this:
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. upd_cs cs [a] = a # cs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
upd_cs cs [a] = a # cs

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd (m # ms) \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s' = Suc (length s); hd (m # ms) = sourcenode a; m' # ms' = targetnode a # targetnode a' # tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
 2. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
valid_node m'
valid_call_list (a # cs) (targetnode a)
\<forall>i<length (a' # rs). (a' # rs) ! i \<in> get_return_edges ((a # cs) ! i)
valid_return_list (a' # rs) (targetnode a)
length (a' # rs) = length (a # cs)
targetnode a' # ms = targetnodes (a' # rs)
upd_cs cs [a] = a # cs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
valid_node m'
valid_call_list (a # cs) (targetnode a)
\<forall>i<length (a' # rs). (a' # rs) ! i \<in> get_return_edges ((a # cs) ! i)
valid_return_list (a' # rs) (targetnode a)
length (a' # rs) = length (a # cs)
targetnode a' # ms = targetnodes (a' # rs)
upd_cs cs [a] = a # cs

goal (1 subgoal):
 1. \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
apply(rule_tac x="a#cs" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_node m'; valid_call_list (a # cs) (targetnode a); \<forall>i<length (a' # rs). (a' # rs) ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list (a' # rs) (targetnode a); length (a' # rs) = length (a # cs); targetnode a' # ms = targetnodes (a' # rs); upd_cs cs [a] = a # cs\<rbrakk> \<Longrightarrow> \<exists>rs'. valid_node m' \<and> valid_call_list (a # cs) m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges ((a # cs) ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length (a # cs) \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = a # cs
[PROOF STEP]
apply(rule_tac x="a'#rs" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_node m'; valid_call_list (a # cs) (targetnode a); \<forall>i<length (a' # rs). (a' # rs) ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list (a' # rs) (targetnode a); length (a' # rs) = length (a # cs); targetnode a' # ms = targetnodes (a' # rs); upd_cs cs [a] = a # cs\<rbrakk> \<Longrightarrow> valid_node m' \<and> valid_call_list (a # cs) m' \<and> (\<forall>i<length (a' # rs). (a' # rs) ! i \<in> get_return_edges ((a # cs) ! i)) \<and> valid_return_list (a' # rs) m' \<and> length (a' # rs) = length (a # cs) \<and> ms' = targetnodes (a' # rs) \<and> upd_cs cs [a] = a # cs
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
\<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
case (silent_move_return f a s s' Q p f' S)
[PROOF STATE]
proof (state)
this:
pred (f a) s
transfer (f a) s = s'
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'
\<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
Ball (set (tl (m # ms))) return_node
length (m # ms) = length s
length s = Suc (length s')
s' \<noteq> []
hd (m # ms) = sourcenode a
hd (tl (m # ms)) = targetnode a
m' # ms' = tl (m # ms)
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>hd (m # ms) = sourcenode a\<close>
      \<open>hd (tl (m # ms)) = targetnode a\<close> \<open>m' # ms' = tl (m # ms)\<close> [symmetric]
[PROOF STATE]
proof (chain)
picking this:
hd (m # ms) = sourcenode a
hd (tl (m # ms)) = targetnode a
tl (m # ms) = m' # ms'
[PROOF STEP]
have [simp]:"m = sourcenode a" "m' = targetnode a"
[PROOF STATE]
proof (prove)
using this:
hd (m # ms) = sourcenode a
hd (tl (m # ms)) = targetnode a
tl (m # ms) = m' # ms'

goal (1 subgoal):
 1. m = sourcenode a &&& m' = targetnode a
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
m = sourcenode a
m' = targetnode a

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>length (m # ms) = length s\<close> \<open>length s = Suc (length s')\<close> \<open>s' \<noteq> []\<close>
      \<open>hd (tl (m # ms)) = targetnode a\<close> \<open>m' # ms' = tl (m # ms)\<close>
[PROOF STATE]
proof (chain)
picking this:
length (m # ms) = length s
length s = Suc (length s')
s' \<noteq> []
hd (tl (m # ms)) = targetnode a
m' # ms' = tl (m # ms)
[PROOF STEP]
have "ms = targetnode a # ms'"
[PROOF STATE]
proof (prove)
using this:
length (m # ms) = length s
length s = Suc (length s')
s' \<noteq> []
hd (tl (m # ms)) = targetnode a
m' # ms' = tl (m # ms)

goal (1 subgoal):
 1. ms = targetnode a # ms'
[PROOF STEP]
by(cases ms) auto
[PROOF STATE]
proof (state)
this:
ms = targetnode a # ms'

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
with \<open>ms = targetnodes rs\<close>
[PROOF STATE]
proof (chain)
picking this:
ms = targetnodes rs
ms = targetnode a # ms'
[PROOF STEP]
obtain r' rs' where "rs = r' # rs'"
      and "targetnode a = targetnode r'" and "ms' = targetnodes rs'"
[PROOF STATE]
proof (prove)
using this:
ms = targetnodes rs
ms = targetnode a # ms'

goal (1 subgoal):
 1. (\<And>r' rs'. \<lbrakk>rs = r' # rs'; targetnode a = targetnode r'; ms' = targetnodes rs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases rs)(auto simp:targetnodes_def)
[PROOF STATE]
proof (state)
this:
rs = r' # rs'
targetnode a = targetnode r'
ms' = targetnodes rs'

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rs = r' # rs'
targetnode a = targetnode r'
ms' = targetnodes rs'

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>rs = r' # rs'\<close> \<open>length rs = length cs\<close>
[PROOF STATE]
proof (chain)
picking this:
rs = r' # rs'
length rs = length cs
[PROOF STEP]
obtain c' cs' where "cs = c' # cs'"
      and "length rs' = length cs'"
[PROOF STATE]
proof (prove)
using this:
rs = r' # rs'
length rs = length cs

goal (1 subgoal):
 1. (\<And>c' cs'. \<lbrakk>cs = c' # cs'; length rs' = length cs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases cs) auto
[PROOF STATE]
proof (state)
this:
cs = c' # cs'
length rs' = length cs'

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cs = c' # cs'
length rs' = length cs'

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)\<close>
      \<open>rs = r' # rs'\<close> \<open>cs = c' # cs'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
rs = r' # rs'
cs = c' # cs'
[PROOF STEP]
have "\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)"
      and "r' \<in> get_return_edges c'"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
rs = r' # rs'
cs = c' # cs'

goal (1 subgoal):
 1. \<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i) &&& r' \<in> get_return_edges c'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)
r' \<in> get_return_edges c'

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)
r' \<in> get_return_edges c'

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>valid_edge a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
[PROOF STEP]
have "valid_node (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a

goal (1 subgoal):
 1. valid_node (targetnode a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
valid_node (targetnode a)

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_node (targetnode a)

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>valid_call_list cs m\<close> \<open>cs = c' # cs'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_call_list cs m
cs = c' # cs'
[PROOF STEP]
obtain p' Q' r fs' where "valid_edge c'" and "kind c' = Q':r\<hookrightarrow>\<^bsub>p'\<^esub>fs'"
      and "p' = get_proc m"
[PROOF STATE]
proof (prove)
using this:
valid_call_list cs m
cs = c' # cs'

goal (1 subgoal):
 1. (\<And>Q' r p' fs'. \<lbrakk>valid_edge c'; kind c' = Q':r\<hookrightarrow>\<^bsub>p'\<^esub>fs'; p' = get_proc m\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply(auto simp:valid_call_list_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>Q' r p' fs'. \<lbrakk>valid_edge c'; kind c' = Q':r\<hookrightarrow>\<^bsub>get_proc (sourcenode a)\<^esub>fs'; p' = get_proc (sourcenode a)\<rbrakk> \<Longrightarrow> thesis; \<forall>cs'a c. (\<exists>cs''. c' # cs' = cs'a @ c # cs'') \<longrightarrow> valid_edge c \<and> (\<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs'a of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (sourcenodes cs'a))\<^esub>fs); cs = c' # cs'\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by(erule_tac x="[]" in allE) auto
[PROOF STATE]
proof (state)
this:
valid_edge c'
kind c' = Q':r\<hookrightarrow>\<^bsub>p'\<^esub>fs'
p' = get_proc m

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'
[PROOF STEP]
have "get_proc (sourcenode a) = p"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'

goal (1 subgoal):
 1. get_proc (sourcenode a) = p
[PROOF STEP]
by(rule get_proc_return)
[PROOF STATE]
proof (state)
this:
get_proc (sourcenode a) = p

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
with \<open>p' = get_proc m\<close>
[PROOF STATE]
proof (chain)
picking this:
p' = get_proc m
get_proc (sourcenode a) = p
[PROOF STEP]
have [simp]:"p' = p"
[PROOF STATE]
proof (prove)
using this:
p' = get_proc m
get_proc (sourcenode a) = p

goal (1 subgoal):
 1. p' = p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p' = p

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>valid_edge c'\<close> \<open>kind c' = Q':r\<hookrightarrow>\<^bsub>p'\<^esub>fs'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge c'
kind c' = Q':r\<hookrightarrow>\<^bsub>p'\<^esub>fs'
[PROOF STEP]
have "get_proc (targetnode c') = p"
[PROOF STATE]
proof (prove)
using this:
valid_edge c'
kind c' = Q':r\<hookrightarrow>\<^bsub>p'\<^esub>fs'

goal (1 subgoal):
 1. get_proc (targetnode c') = p
[PROOF STEP]
by(fastforce intro:get_proc_call)
[PROOF STATE]
proof (state)
this:
get_proc (targetnode c') = p

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>valid_edge c'\<close> \<open>r' \<in> get_return_edges c'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge c'
r' \<in> get_return_edges c'
[PROOF STEP]
have "valid_edge r'"
[PROOF STATE]
proof (prove)
using this:
valid_edge c'
r' \<in> get_return_edges c'

goal (1 subgoal):
 1. valid_edge r'
[PROOF STEP]
by(rule get_return_edges_valid)
[PROOF STATE]
proof (state)
this:
valid_edge r'

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>valid_edge c'\<close> \<open>kind c' = Q':r\<hookrightarrow>\<^bsub>p'\<^esub>fs'\<close> \<open>r' \<in> get_return_edges c'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge c'
kind c' = Q':r\<hookrightarrow>\<^bsub>p'\<^esub>fs'
r' \<in> get_return_edges c'
[PROOF STEP]
obtain Q'' f'' where "kind r' = Q''\<hookleftarrow>\<^bsub>p\<^esub>f''"
[PROOF STATE]
proof (prove)
using this:
valid_edge c'
kind c' = Q':r\<hookrightarrow>\<^bsub>p'\<^esub>fs'
r' \<in> get_return_edges c'

goal (1 subgoal):
 1. (\<And>Q'' f''. kind r' = Q''\<hookleftarrow>\<^bsub>p\<^esub>f'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce dest!:call_return_edges)
[PROOF STATE]
proof (state)
this:
kind r' = Q''\<hookleftarrow>\<^bsub>p\<^esub>f''

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
with \<open>valid_edge r'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge r'
kind r' = Q''\<hookleftarrow>\<^bsub>p\<^esub>f''
[PROOF STEP]
have "get_proc (sourcenode r') = p"
[PROOF STATE]
proof (prove)
using this:
valid_edge r'
kind r' = Q''\<hookleftarrow>\<^bsub>p\<^esub>f''

goal (1 subgoal):
 1. get_proc (sourcenode r') = p
[PROOF STEP]
by(rule get_proc_return)
[PROOF STATE]
proof (state)
this:
get_proc (sourcenode r') = p

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>valid_edge r'\<close> \<open>kind r' = Q''\<hookleftarrow>\<^bsub>p\<^esub>f''\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge r'
kind r' = Q''\<hookleftarrow>\<^bsub>p\<^esub>f''
[PROOF STEP]
have "method_exit (sourcenode r')"
[PROOF STATE]
proof (prove)
using this:
valid_edge r'
kind r' = Q''\<hookleftarrow>\<^bsub>p\<^esub>f''

goal (1 subgoal):
 1. method_exit (sourcenode r')
[PROOF STEP]
by(fastforce simp:method_exit_def)
[PROOF STATE]
proof (state)
this:
method_exit (sourcenode r')

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'
[PROOF STEP]
have "method_exit (sourcenode a)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'

goal (1 subgoal):
 1. method_exit (sourcenode a)
[PROOF STEP]
by(fastforce simp:method_exit_def)
[PROOF STATE]
proof (state)
this:
method_exit (sourcenode a)

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
with \<open>method_exit (sourcenode r')\<close> \<open>get_proc (sourcenode r') = p\<close>
      \<open>get_proc (sourcenode a) = p\<close>
[PROOF STATE]
proof (chain)
picking this:
method_exit (sourcenode r')
get_proc (sourcenode r') = p
get_proc (sourcenode a) = p
method_exit (sourcenode a)
[PROOF STEP]
have "sourcenode a = sourcenode r'"
[PROOF STATE]
proof (prove)
using this:
method_exit (sourcenode r')
get_proc (sourcenode r') = p
get_proc (sourcenode a) = p
method_exit (sourcenode a)

goal (1 subgoal):
 1. sourcenode a = sourcenode r'
[PROOF STEP]
by(fastforce intro:method_exit_unique)
[PROOF STATE]
proof (state)
this:
sourcenode a = sourcenode r'

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
with \<open>valid_edge a\<close> \<open>valid_edge r'\<close> \<open>targetnode a = targetnode r'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
valid_edge r'
targetnode a = targetnode r'
sourcenode a = sourcenode r'
[PROOF STEP]
have "a = r'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
valid_edge r'
targetnode a = targetnode r'
sourcenode a = sourcenode r'

goal (1 subgoal):
 1. a = r'
[PROOF STEP]
by(fastforce intro:edge_det)
[PROOF STATE]
proof (state)
this:
a = r'

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>valid_edge c'\<close> \<open>r' \<in> get_return_edges c'\<close> \<open>targetnode a = targetnode r'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge c'
r' \<in> get_return_edges c'
targetnode a = targetnode r'
[PROOF STEP]
have "get_proc (sourcenode c') = get_proc (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_edge c'
r' \<in> get_return_edges c'
targetnode a = targetnode r'

goal (1 subgoal):
 1. get_proc (sourcenode c') = get_proc (targetnode a)
[PROOF STEP]
by(fastforce intro:get_proc_get_return_edge)
[PROOF STATE]
proof (state)
this:
get_proc (sourcenode c') = get_proc (targetnode a)

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>valid_call_list cs m\<close> \<open>cs = c' # cs'\<close>
      \<open>get_proc (sourcenode c') = get_proc (targetnode a)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_call_list cs m
cs = c' # cs'
get_proc (sourcenode c') = get_proc (targetnode a)
[PROOF STEP]
have "valid_call_list cs' (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_call_list cs m
cs = c' # cs'
get_proc (sourcenode c') = get_proc (targetnode a)

goal (1 subgoal):
 1. valid_call_list cs' (targetnode a)
[PROOF STEP]
apply(clarsimp simp:valid_call_list_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs'a c cs''. \<lbrakk>\<forall>cs'aa ca. (\<exists>cs''a. c' # cs'a @ c # cs'' = cs'aa @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q r fs. kind ca = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs'aa of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (sourcenodes cs'aa))\<^esub>fs); cs = c' # cs'a @ c # cs''; get_proc (sourcenode c') = get_proc (targetnode a); cs' = cs'a @ c # cs''\<rbrakk> \<Longrightarrow> valid_edge c \<and> (\<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs'a of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (sourcenodes cs'a))\<^esub>fs)
[PROOF STEP]
apply(hypsubst_thin)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs''. \<lbrakk>\<forall>cs'a ca. (\<exists>cs''a. c' # cs' @ c # cs'' = cs'a @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q r fs. kind ca = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs'a of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (sourcenodes cs'a))\<^esub>fs); get_proc (sourcenode c') = get_proc (targetnode a)\<rbrakk> \<Longrightarrow> valid_edge c \<and> (\<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs)
[PROOF STEP]
apply(erule_tac x="c' # cs'" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs''. \<lbrakk>get_proc (sourcenode c') = get_proc (targetnode a); \<forall>ca. (\<exists>cs''a. c' # cs' @ c # cs'' = (c' # cs') @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q r fs. kind ca = Q:r\<hookrightarrow>\<^bsub>get_proc (case c' # cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (sourcenodes (c' # cs')))\<^esub>fs)\<rbrakk> \<Longrightarrow> valid_edge c \<and> (\<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs)
[PROOF STEP]
by(case_tac cs')(auto simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
valid_call_list cs' (targetnode a)

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_call_list cs' (targetnode a)

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>valid_return_list rs m\<close> \<open>rs = r' # rs'\<close> \<open>targetnode a = targetnode r'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_return_list rs m
rs = r' # rs'
targetnode a = targetnode r'
[PROOF STEP]
have "valid_return_list rs' (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_return_list rs m
rs = r' # rs'
targetnode a = targetnode r'

goal (1 subgoal):
 1. valid_return_list rs' (targetnode a)
[PROOF STEP]
apply(clarsimp simp:valid_return_list_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs''. \<lbrakk>\<forall>cs'a ca. (\<exists>cs''a. r' # cs' @ c # cs'' = cs'a @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q f. kind ca = Q\<hookleftarrow>\<^bsub>get_proc (case cs'a of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (targetnodes cs'a))\<^esub>f); rs = r' # cs' @ c # cs''; targetnode a = targetnode r'; rs' = cs' @ c # cs''\<rbrakk> \<Longrightarrow> valid_edge c \<and> (\<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode r' | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f)
[PROOF STEP]
apply(erule_tac x="r' # cs'" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs''. \<lbrakk>rs = r' # cs' @ c # cs''; targetnode a = targetnode r'; rs' = cs' @ c # cs''; \<forall>ca. (\<exists>cs''a. r' # cs' @ c # cs'' = (r' # cs') @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q f. kind ca = Q\<hookleftarrow>\<^bsub>get_proc (case r' # cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (targetnodes (r' # cs')))\<^esub>f)\<rbrakk> \<Longrightarrow> valid_edge c \<and> (\<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode r' | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f)
[PROOF STEP]
by(case_tac cs')(auto simp:targetnodes_def)
[PROOF STATE]
proof (state)
this:
valid_return_list rs' (targetnode a)

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_return_list rs' (targetnode a)

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
from \<open>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'\<close> \<open>cs = c' # cs'\<close>
[PROOF STATE]
proof (chain)
picking this:
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'
cs = c' # cs'
[PROOF STEP]
have "upd_cs cs [a] = cs'"
[PROOF STATE]
proof (prove)
using this:
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'
cs = c' # cs'

goal (1 subgoal):
 1. upd_cs cs [a] = cs'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
upd_cs cs [a] = cs'

goal (1 subgoal):
 1. \<And>f a s s' Q p f' S. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl (m # ms)). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl (m # ms))) return_node; length (m # ms) = length s; length s = Suc (length s'); s' \<noteq> []; hd (m # ms) = sourcenode a; hd (tl (m # ms)) = targetnode a; m' # ms' = tl (m # ms); valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rs = r' # rs'
targetnode a = targetnode r'
ms' = targetnodes rs'
cs = c' # cs'
length rs' = length cs'
\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)
r' \<in> get_return_edges c'
valid_node (targetnode a)
valid_call_list cs' (targetnode a)
valid_return_list rs' (targetnode a)
upd_cs cs [a] = cs'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
rs = r' # rs'
targetnode a = targetnode r'
ms' = targetnodes rs'
cs = c' # cs'
length rs' = length cs'
\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)
r' \<in> get_return_edges c'
valid_node (targetnode a)
valid_call_list cs' (targetnode a)
valid_return_list rs' (targetnode a)
upd_cs cs [a] = cs'

goal (1 subgoal):
 1. \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
apply(rule_tac x="cs'" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rs = r' # rs'; targetnode a = targetnode r'; ms' = targetnodes rs'; cs = c' # cs'; length rs' = length cs'; \<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i); r' \<in> get_return_edges c'; valid_node (targetnode a); valid_call_list cs' (targetnode a); valid_return_list rs' (targetnode a); upd_cs cs [a] = cs'\<rbrakk> \<Longrightarrow> \<exists>rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
apply(rule_tac x="rs'" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rs = r' # rs'; targetnode a = targetnode r'; ms' = targetnodes rs'; cs = c' # cs'; length rs' = length cs'; \<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i); r' \<in> get_return_edges c'; valid_node (targetnode a); valid_call_list cs' (targetnode a); valid_return_list rs' (targetnode a); upd_cs cs [a] = cs'\<rbrakk> \<Longrightarrow> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
\<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [a] = cs'

goal:
No subgoals!
[PROOF STEP]
qed