[STATEMENT]
lemma silent_moves_no_slice_edges:
  "\<lbrakk>S,f \<turnstile> (ms,s) =as\<Rightarrow>\<^sub>\<tau> (ms',s'); tl ms = targetnodes rs; length rs = length cs;
    \<forall>i<length cs. call_of_return_node (tl ms!i) (sourcenode (cs!i))\<rbrakk>
  \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms' = targetnodes rs' \<and>
  length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as).
  call_of_return_node (tl ms'!i) (sourcenode ((upd_cs cs as)!i))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S,f \<turnstile> (ms,s) =as\<Rightarrow>\<^sub>\<tau> (ms',s'); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms' ! i) (sourcenode (upd_cs cs as ! i))))
[PROOF STEP]
proof(induct arbitrary:rs cs rule:silent_moves.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ms s S f rs cs. \<lbrakk>length ms = length s; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs [] = [] \<and> (\<exists>rs'. tl ms = targetnodes rs' \<and> length rs' = length (upd_cs cs []) \<and> (\<forall>i<length (upd_cs cs []). call_of_return_node (tl ms ! i) (sourcenode (upd_cs cs [] ! i))))
 2. \<And>S f ms s a ms' s' as ms'' s'' rs cs. \<lbrakk>S,f \<turnstile> (ms,s) -a\<rightarrow>\<^sub>\<tau> (ms',s'); S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
case (silent_moves_Cons S f ms s a ms' s' as ms'' s'')
[PROOF STATE]
proof (state)
this:
S,f \<turnstile> (ms,s) -a\<rightarrow>\<^sub>\<tau> (ms',s')
S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s'')
\<lbrakk>tl ms' = targetnodes ?rs; length ?rs = length ?cs; \<forall>i<length ?cs. call_of_return_node (tl ms' ! i) (sourcenode (?cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S ?cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs ?cs as) \<and> (\<forall>i<length (upd_cs ?cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs ?cs as ! i))))
tl ms = targetnodes rs
length rs = length cs
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))

goal (2 subgoals):
 1. \<And>ms s S f rs cs. \<lbrakk>length ms = length s; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs [] = [] \<and> (\<exists>rs'. tl ms = targetnodes rs' \<and> length rs' = length (upd_cs cs []) \<and> (\<forall>i<length (upd_cs cs []). call_of_return_node (tl ms ! i) (sourcenode (upd_cs cs [] ! i))))
 2. \<And>S f ms s a ms' s' as ms'' s'' rs cs. \<lbrakk>S,f \<turnstile> (ms,s) -a\<rightarrow>\<^sub>\<tau> (ms',s'); S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
from \<open>S,f \<turnstile> (ms,s) -a\<rightarrow>\<^sub>\<tau> (ms',s')\<close> \<open>tl ms = targetnodes rs\<close> \<open>length rs = length cs\<close>
    \<open>\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (ms,s) -a\<rightarrow>\<^sub>\<tau> (ms',s')
tl ms = targetnodes rs
length rs = length cs
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
[PROOF STEP]
have "\<not> slice_edge S cs a"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (ms,s) -a\<rightarrow>\<^sub>\<tau> (ms',s')
tl ms = targetnodes rs
length rs = length cs
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))

goal (1 subgoal):
 1. \<not> slice_edge S cs a
[PROOF STEP]
by(rule silent_move_no_slice_edge)
[PROOF STATE]
proof (state)
this:
\<not> slice_edge S cs a

goal (2 subgoals):
 1. \<And>ms s S f rs cs. \<lbrakk>length ms = length s; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs [] = [] \<and> (\<exists>rs'. tl ms = targetnodes rs' \<and> length rs' = length (upd_cs cs []) \<and> (\<forall>i<length (upd_cs cs []). call_of_return_node (tl ms ! i) (sourcenode (upd_cs cs [] ! i))))
 2. \<And>S f ms s a ms' s' as ms'' s'' rs cs. \<lbrakk>S,f \<turnstile> (ms,s) -a\<rightarrow>\<^sub>\<tau> (ms',s'); S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
with silent_moves_Cons
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (ms,s) -a\<rightarrow>\<^sub>\<tau> (ms',s')
S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s'')
\<lbrakk>tl ms' = targetnodes ?rs; length ?rs = length ?cs; \<forall>i<length ?cs. call_of_return_node (tl ms' ! i) (sourcenode (?cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S ?cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs ?cs as) \<and> (\<forall>i<length (upd_cs ?cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs ?cs as ! i))))
tl ms = targetnodes rs
length rs = length cs
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
\<not> slice_edge S cs a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (ms,s) -a\<rightarrow>\<^sub>\<tau> (ms',s')
S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s'')
\<lbrakk>tl ms' = targetnodes ?rs; length ?rs = length ?cs; \<forall>i<length ?cs. call_of_return_node (tl ms' ! i) (sourcenode (?cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S ?cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs ?cs as) \<and> (\<forall>i<length (upd_cs ?cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs ?cs as ! i))))
tl ms = targetnodes rs
length rs = length cs
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
\<not> slice_edge S cs a

goal (1 subgoal):
 1. slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
proof(induct rule:silent_move.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>f a s s' ms S ms'. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind (kind a); (\<exists>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length s' = length s; length ms = length s; hd ms = sourcenode a; ms' = targetnode a # tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
 2. \<And>f a s s' Q r p fs a' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
 3. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
case (silent_move_intra f a s s' ms S ms')
[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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
Ball (set (tl ms)) return_node
length s' = length s
length ms = length s
hd ms = sourcenode a
ms' = targetnode a # tl ms
S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s'')
\<lbrakk>tl ms' = targetnodes ?rs; length ?rs = length ?cs; \<forall>i<length ?cs. call_of_return_node (tl ms' ! i) (sourcenode (?cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S ?cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs ?cs as) \<and> (\<forall>i<length (upd_cs ?cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs ?cs as ! i))))
tl ms = targetnodes rs
length rs = length cs
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
\<not> slice_edge S cs a

goal (3 subgoals):
 1. \<And>f a s s' ms S ms'. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind (kind a); (\<exists>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length s' = length s; length ms = length s; hd ms = sourcenode a; ms' = targetnode a # tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
 2. \<And>f a s s' Q r p fs a' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
 3. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
note IH = \<open>\<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs;
      \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk>
      \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and>
      length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as).
      call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i))))\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>tl ms' = targetnodes ?rs; length ?rs = length ?cs; \<forall>i<length ?cs. call_of_return_node (tl ms' ! i) (sourcenode (?cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S ?cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs ?cs as) \<and> (\<forall>i<length (upd_cs ?cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs ?cs as ! i))))

goal (3 subgoals):
 1. \<And>f a s s' ms S ms'. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind (kind a); (\<exists>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length s' = length s; length ms = length s; hd ms = sourcenode a; ms' = targetnode a # tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
 2. \<And>f a s s' Q r p fs a' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
 3. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
from \<open>ms' = targetnode a # tl ms\<close> \<open>tl ms = targetnodes rs\<close>
[PROOF STATE]
proof (chain)
picking this:
ms' = targetnode a # tl ms
tl ms = targetnodes rs
[PROOF STEP]
have "tl ms' = targetnodes rs"
[PROOF STATE]
proof (prove)
using this:
ms' = targetnode a # tl ms
tl ms = targetnodes rs

goal (1 subgoal):
 1. tl ms' = targetnodes rs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
tl ms' = targetnodes rs

goal (3 subgoals):
 1. \<And>f a s s' ms S ms'. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind (kind a); (\<exists>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length s' = length s; length ms = length s; hd ms = sourcenode a; ms' = targetnode a # tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
 2. \<And>f a s s' Q r p fs a' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
 3. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
from \<open>ms' = targetnode a # tl ms\<close> \<open>tl ms = targetnodes rs\<close>
      \<open>\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<close>
[PROOF STATE]
proof (chain)
picking this:
ms' = targetnode a # tl ms
tl ms = targetnodes rs
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
[PROOF STEP]
have "\<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))"
[PROOF STATE]
proof (prove)
using this:
ms' = targetnode a # tl ms
tl ms = targetnodes rs
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))

goal (1 subgoal):
 1. \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))

goal (3 subgoals):
 1. \<And>f a s s' ms S ms'. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind (kind a); (\<exists>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length s' = length s; length ms = length s; hd ms = sourcenode a; ms' = targetnode a # tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
 2. \<And>f a s s' Q r p fs a' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
 3. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
from IH[OF \<open>tl ms' = targetnodes rs\<close> \<open>length rs = length cs\<close> this]
[PROOF STATE]
proof (chain)
picking this:
slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i))))
[PROOF STEP]
have "slice_edges S cs as = []"
      and "\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and>
      (\<forall>i<length (upd_cs cs as).
      call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))"
[PROOF STATE]
proof (prove)
using this:
slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i))))

goal (1 subgoal):
 1. slice_edges S cs as = [] &&& \<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
slice_edges S cs as = []
\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))

goal (3 subgoals):
 1. \<And>f a s s' ms S ms'. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind (kind a); (\<exists>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length s' = length s; length ms = length s; hd ms = sourcenode a; ms' = targetnode a # tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
 2. \<And>f a s s' Q r p fs a' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
 3. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
with \<open>intra_kind (kind a)\<close> \<open>\<not> slice_edge S cs a\<close>
[PROOF STATE]
proof (chain)
picking this:
intra_kind (kind a)
\<not> slice_edge S cs a
slice_edges S cs as = []
\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
intra_kind (kind a)
\<not> slice_edge S cs a
slice_edges S cs as = []
\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))

goal (1 subgoal):
 1. slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
by(fastforce simp:intra_kind_def)
[PROOF STATE]
proof (state)
this:
slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
 2. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
 2. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
case (silent_move_call f a s s' Q r p fs a' ms S ms')
[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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
Ball (set (tl ms)) return_node
length ms = length s
length s' = Suc (length s)
hd ms = sourcenode a
ms' = targetnode a # targetnode a' # tl ms
S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s'')
\<lbrakk>tl ms' = targetnodes ?rs; length ?rs = length ?cs; \<forall>i<length ?cs. call_of_return_node (tl ms' ! i) (sourcenode (?cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S ?cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs ?cs as) \<and> (\<forall>i<length (upd_cs ?cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs ?cs as ! i))))
tl ms = targetnodes rs
length rs = length cs
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
\<not> slice_edge S cs a

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
 2. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
note IH = \<open>\<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs;
      \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk>
      \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and>
      length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as).
      call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i))))\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>tl ms' = targetnodes ?rs; length ?rs = length ?cs; \<forall>i<length ?cs. call_of_return_node (tl ms' ! i) (sourcenode (?cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S ?cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs ?cs as) \<and> (\<forall>i<length (upd_cs ?cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs ?cs as ! i))))

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
 2. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
from \<open>tl ms = targetnodes rs\<close> \<open>ms' = targetnode a # targetnode a' # tl ms\<close>
[PROOF STATE]
proof (chain)
picking this:
tl ms = targetnodes rs
ms' = targetnode a # targetnode a' # tl ms
[PROOF STEP]
have "tl ms' = targetnodes (a'#rs)"
[PROOF STATE]
proof (prove)
using this:
tl ms = targetnodes rs
ms' = targetnode a # targetnode a' # tl ms

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

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
 2. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[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' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
 2. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
from \<open>valid_edge a'\<close> \<open>valid_edge a\<close> \<open>a' \<in> get_return_edges a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
valid_edge a
a' \<in> get_return_edges a
[PROOF STEP]
have "return_node (targetnode a')"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
valid_edge a
a' \<in> get_return_edges a

goal (1 subgoal):
 1. return_node (targetnode a')
[PROOF STEP]
by(fastforce simp:return_node_def)
[PROOF STATE]
proof (state)
this:
return_node (targetnode a')

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
 2. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
with \<open>valid_edge a\<close> \<open>valid_edge a'\<close> \<open>a' \<in> get_return_edges a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
valid_edge a'
a' \<in> get_return_edges a
return_node (targetnode a')
[PROOF STEP]
have "call_of_return_node (targetnode a') (sourcenode a)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
valid_edge a'
a' \<in> get_return_edges a
return_node (targetnode a')

goal (1 subgoal):
 1. call_of_return_node (targetnode a') (sourcenode a)
[PROOF STEP]
by(simp add:call_of_return_node_def) blast
[PROOF STATE]
proof (state)
this:
call_of_return_node (targetnode a') (sourcenode a)

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
 2. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
with \<open>\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<close>
      \<open>ms' = targetnode a # targetnode a' # tl ms\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
ms' = targetnode a # targetnode a' # tl ms
call_of_return_node (targetnode a') (sourcenode a)
[PROOF STEP]
have "\<forall>i<length (a#cs).
      call_of_return_node (tl ms' ! i) (sourcenode ((a#cs) ! i))"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
ms' = targetnode a # targetnode a' # tl ms
call_of_return_node (targetnode a') (sourcenode a)

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

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
 2. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
from IH[OF \<open>tl ms' = targetnodes (a'#rs)\<close> \<open>length (a'#rs) = length (a#cs)\<close> this]
[PROOF STATE]
proof (chain)
picking this:
slice_edges S (a # cs) as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs (a # cs) as) \<and> (\<forall>i<length (upd_cs (a # cs) as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs (a # cs) as ! i))))
[PROOF STEP]
have "slice_edges S (a # cs) as = []"
      and "\<exists>rs'. tl ms'' = targetnodes rs' \<and>
      length rs' = length (upd_cs (a # cs) as) \<and>
      (\<forall>i<length (upd_cs (a # cs) as).
        call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs (a # cs) as ! i)))"
[PROOF STATE]
proof (prove)
using this:
slice_edges S (a # cs) as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs (a # cs) as) \<and> (\<forall>i<length (upd_cs (a # cs) as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs (a # cs) as ! i))))

goal (1 subgoal):
 1. slice_edges S (a # cs) as = [] &&& \<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs (a # cs) as) \<and> (\<forall>i<length (upd_cs (a # cs) as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs (a # cs) as ! i)))
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
slice_edges S (a # cs) as = []
\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs (a # cs) as) \<and> (\<forall>i<length (upd_cs (a # cs) as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs (a # cs) as ! i)))

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
 2. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
with \<open>\<not> slice_edge S cs a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> slice_edge S cs a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
slice_edges S (a # cs) as = []
\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs (a # cs) as) \<and> (\<forall>i<length (upd_cs (a # cs) as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs (a # cs) as ! i)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<not> slice_edge S cs a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
slice_edges S (a # cs) as = []
\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs (a # cs) as) \<and> (\<forall>i<length (upd_cs (a # cs) as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs (a # cs) as ! i)))

goal (1 subgoal):
 1. slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))

goal (1 subgoal):
 1. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
case (silent_move_return f a s s' Q p f' ms S ms')
[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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
Ball (set (tl ms)) return_node
length ms = length s
length s = Suc (length s')
s' \<noteq> []
hd ms = sourcenode a
hd (tl ms) = targetnode a
ms' = tl ms
S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s'')
\<lbrakk>tl ms' = targetnodes ?rs; length ?rs = length ?cs; \<forall>i<length ?cs. call_of_return_node (tl ms' ! i) (sourcenode (?cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S ?cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs ?cs as) \<and> (\<forall>i<length (upd_cs ?cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs ?cs as ! i))))
tl ms = targetnodes rs
length rs = length cs
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
\<not> slice_edge S cs a

goal (1 subgoal):
 1. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
note IH = \<open>\<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs;
      \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk>
      \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and>
      length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as).
      call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i))))\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>tl ms' = targetnodes ?rs; length ?rs = length ?cs; \<forall>i<length ?cs. call_of_return_node (tl ms' ! i) (sourcenode (?cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S ?cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs ?cs as) \<and> (\<forall>i<length (upd_cs ?cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs ?cs as ! i))))

goal (1 subgoal):
 1. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
from \<open>length s = Suc (length s')\<close> \<open>s' \<noteq> []\<close> \<open>length ms = length s\<close> \<open>ms' = tl ms\<close>
[PROOF STATE]
proof (chain)
picking this:
length s = Suc (length s')
s' \<noteq> []
length ms = length s
ms' = tl ms
[PROOF STEP]
obtain x xs where [simp]:"ms' = x#xs"
[PROOF STATE]
proof (prove)
using this:
length s = Suc (length s')
s' \<noteq> []
length ms = length s
ms' = tl ms

goal (1 subgoal):
 1. (\<And>x xs. ms' = x # xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases ms)(auto,case_tac ms',auto)
[PROOF STATE]
proof (state)
this:
ms' = x # xs

goal (1 subgoal):
 1. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
from \<open>ms' = tl ms\<close> \<open>tl ms = targetnodes rs\<close>
[PROOF STATE]
proof (chain)
picking this:
ms' = tl ms
tl ms = targetnodes rs
[PROOF STEP]
obtain r' rs' where "rs = r'#rs'"
      and "x = targetnode r'" and "tl ms' = targetnodes rs'"
[PROOF STATE]
proof (prove)
using this:
ms' = tl ms
tl ms = targetnodes rs

goal (1 subgoal):
 1. (\<And>r' rs'. \<lbrakk>rs = r' # rs'; x = targetnode r'; tl 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'
x = targetnode r'
tl ms' = targetnodes rs'

goal (1 subgoal):
 1. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
from \<open>length rs = length cs\<close> \<open>rs = r'#rs'\<close>
[PROOF STATE]
proof (chain)
picking this:
length rs = length cs
rs = r' # rs'
[PROOF STEP]
obtain c' cs' where "cs = c'#cs'"
      and "length rs' = length cs'"
[PROOF STATE]
proof (prove)
using this:
length rs = length cs
rs = r' # rs'

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' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
from \<open>\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<close>
      \<open>cs = c'#cs'\<close> \<open>ms' = tl ms\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
cs = c' # cs'
ms' = tl ms
[PROOF STEP]
have "\<forall>i<length cs'. call_of_return_node (tl ms' ! i) (sourcenode (cs' ! i))"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
cs = c' # cs'
ms' = tl ms

goal (1 subgoal):
 1. \<forall>i<length cs'. call_of_return_node (tl ms' ! i) (sourcenode (cs' ! i))
[PROOF STEP]
by auto(erule_tac x="Suc i" in allE,cases "tl ms",auto)
[PROOF STATE]
proof (state)
this:
\<forall>i<length cs'. call_of_return_node (tl ms' ! i) (sourcenode (cs' ! i))

goal (1 subgoal):
 1. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
from IH[OF \<open>tl ms' = targetnodes rs'\<close> \<open>length rs' = length cs'\<close> this]
[PROOF STATE]
proof (chain)
picking this:
slice_edges S cs' as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs' as) \<and> (\<forall>i<length (upd_cs cs' as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs' as ! i))))
[PROOF STEP]
have "slice_edges S cs' as = []" and "\<exists>rs'. tl ms'' = targetnodes rs' \<and>
      length rs' = length (upd_cs cs' as) \<and> (\<forall>i<length (upd_cs cs' as).
      call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs' as ! i)))"
[PROOF STATE]
proof (prove)
using this:
slice_edges S cs' as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs' as) \<and> (\<forall>i<length (upd_cs cs' as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs' as ! i))))

goal (1 subgoal):
 1. slice_edges S cs' as = [] &&& \<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs' as) \<and> (\<forall>i<length (upd_cs cs' as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs' as ! i)))
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
slice_edges S cs' as = []
\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs' as) \<and> (\<forall>i<length (upd_cs cs' as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs' as ! i)))

goal (1 subgoal):
 1. \<And>f a s s' Q p f' ms S ms'. \<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 ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; S,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<And>rs cs. \<lbrakk>tl ms' = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs as = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs as) \<and> (\<forall>i<length (upd_cs cs as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))); tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
with \<open>\<not> slice_edge S cs a\<close> \<open>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'\<close> \<open>cs = c'#cs'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> slice_edge S cs a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'
cs = c' # cs'
slice_edges S cs' as = []
\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs' as) \<and> (\<forall>i<length (upd_cs cs' as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs' as ! i)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<not> slice_edge S cs a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'
cs = c' # cs'
slice_edges S cs' as = []
\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs' as) \<and> (\<forall>i<length (upd_cs cs' as). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs' as ! i)))

goal (1 subgoal):
 1. slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
slice_edges S cs (a # as) = [] \<and> (\<exists>rs'. tl ms'' = targetnodes rs' \<and> length rs' = length (upd_cs cs (a # as)) \<and> (\<forall>i<length (upd_cs cs (a # as)). call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs (a # as) ! i))))

goal (1 subgoal):
 1. \<And>ms s S f rs cs. \<lbrakk>length ms = length s; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> slice_edges S cs [] = [] \<and> (\<exists>rs'. tl ms = targetnodes rs' \<and> length rs' = length (upd_cs cs []) \<and> (\<forall>i<length (upd_cs cs []). call_of_return_node (tl ms ! i) (sourcenode (upd_cs cs [] ! i))))
[PROOF STEP]
qed fastforce