[STATEMENT]
lemma silent_move_no_slice_edge:
  "\<lbrakk>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))\<rbrakk>
  \<Longrightarrow> \<not> slice_edge S cs a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>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))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
[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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
 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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
 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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
[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
tl ms = targetnodes rs
length rs = length cs
\<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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
 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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
 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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
note disj = \<open>(\<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>\<close>
[PROOF STATE]
proof (state)
this:
(\<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>

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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
 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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
 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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
from \<open>pred (f a) s\<close> \<open>length ms = length s\<close>
[PROOF STATE]
proof (chain)
picking this:
pred (f a) s
length ms = length s
[PROOF STEP]
obtain x xs where "ms = x#xs"
[PROOF STATE]
proof (prove)
using this:
pred (f a) s
length ms = length s

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

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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
 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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
 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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
from \<open>length rs = length cs\<close> \<open>tl ms = targetnodes rs\<close>
[PROOF STATE]
proof (chain)
picking this:
length rs = length cs
tl ms = targetnodes rs
[PROOF STEP]
have "length (tl ms) = length cs"
[PROOF STATE]
proof (prove)
using this:
length rs = length cs
tl ms = targetnodes rs

goal (1 subgoal):
 1. length (tl ms) = length cs
[PROOF STEP]
by(simp add:targetnodes_def)
[PROOF STATE]
proof (state)
this:
length (tl ms) = length cs

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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
 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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
 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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
from disj
[PROOF STATE]
proof (chain)
picking this:
(\<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>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<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>

goal (1 subgoal):
 1. \<not> slice_edge S cs a
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<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> \<Longrightarrow> \<not> slice_edge S cs a
 2. hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
assume "\<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>"
[PROOF STATE]
proof (state)
this:
\<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>

goal (2 subgoals):
 1. \<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> \<Longrightarrow> \<not> slice_edge S cs a
 2. hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
with \<open>\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<close>
      \<open>length (tl ms) = length cs\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
length (tl ms) = length cs
\<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>
[PROOF STEP]
have "\<exists>c \<in> set cs. sourcenode c \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
length (tl ms) = length cs
\<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>

goal (1 subgoal):
 1. \<exists>c\<in>set cs. sourcenode c \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
apply(auto simp:in_set_conv_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m' i. \<lbrakk>\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); length ms - Suc 0 = length cs; call_of_return_node (tl ms ! i) m'; m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; i < length cs\<rbrakk> \<Longrightarrow> \<exists>c\<in>set cs. sourcenode c \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
by(erule_tac x="i" in allE) auto
[PROOF STATE]
proof (state)
this:
\<exists>c\<in>set cs. sourcenode c \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (2 subgoals):
 1. \<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> \<Longrightarrow> \<not> slice_edge S cs a
 2. hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>c\<in>set cs. sourcenode c \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

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

goal (1 subgoal):
 1. hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
assume "hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
[PROOF STATE]
proof (state)
this:
hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
with \<open>hd ms = sourcenode a\<close> \<open>intra_kind (kind a)\<close>
[PROOF STATE]
proof (chain)
picking this:
hd ms = sourcenode a
intra_kind (kind a)
hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
hd ms = sourcenode a
intra_kind (kind a)
hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
 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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
[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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
 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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
[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
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>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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
 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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
note disj = \<open>(\<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>\<close>
[PROOF STATE]
proof (state)
this:
(\<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>

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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
 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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
from \<open>pred (f a) s\<close> \<open>length ms = length s\<close>
[PROOF STATE]
proof (chain)
picking this:
pred (f a) s
length ms = length s
[PROOF STEP]
obtain x xs where "ms = x#xs"
[PROOF STATE]
proof (prove)
using this:
pred (f a) s
length ms = length s

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

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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
 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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
from \<open>length rs = length cs\<close> \<open>tl ms = targetnodes rs\<close>
[PROOF STATE]
proof (chain)
picking this:
length rs = length cs
tl ms = targetnodes rs
[PROOF STEP]
have "length (tl ms) = length cs"
[PROOF STATE]
proof (prove)
using this:
length rs = length cs
tl ms = targetnodes rs

goal (1 subgoal):
 1. length (tl ms) = length cs
[PROOF STEP]
by(simp add:targetnodes_def)
[PROOF STATE]
proof (state)
this:
length (tl ms) = length 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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
 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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
from disj
[PROOF STATE]
proof (chain)
picking this:
(\<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>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<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>

goal (1 subgoal):
 1. \<not> slice_edge S cs a
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<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> \<Longrightarrow> \<not> slice_edge S cs a
 2. hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
assume "\<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>"
[PROOF STATE]
proof (state)
this:
\<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>

goal (2 subgoals):
 1. \<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> \<Longrightarrow> \<not> slice_edge S cs a
 2. hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
with \<open>\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<close>
      \<open>length (tl ms) = length cs\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
length (tl ms) = length cs
\<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>
[PROOF STEP]
have "\<exists>c \<in> set cs. sourcenode c \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
length (tl ms) = length cs
\<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>

goal (1 subgoal):
 1. \<exists>c\<in>set cs. sourcenode c \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
apply(auto simp:in_set_conv_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m' i. \<lbrakk>\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); length ms - Suc 0 = length cs; call_of_return_node (tl ms ! i) m'; m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; i < length cs\<rbrakk> \<Longrightarrow> \<exists>c\<in>set cs. sourcenode c \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
by(erule_tac x="i" in allE) auto
[PROOF STATE]
proof (state)
this:
\<exists>c\<in>set cs. sourcenode c \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (2 subgoals):
 1. \<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> \<Longrightarrow> \<not> slice_edge S cs a
 2. hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>c\<in>set cs. sourcenode c \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

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

goal (1 subgoal):
 1. hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
assume "hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
[PROOF STATE]
proof (state)
this:
hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
with \<open>hd ms = sourcenode a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
hd ms = sourcenode a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
hd ms = sourcenode a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
hd ms \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
[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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
[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
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. \<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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
from \<open>pred (f a) s\<close> \<open>length ms = length s\<close>
[PROOF STATE]
proof (chain)
picking this:
pred (f a) s
length ms = length s
[PROOF STEP]
obtain x xs where "ms = x#xs"
[PROOF STATE]
proof (prove)
using this:
pred (f a) s
length ms = length s

goal (1 subgoal):
 1. (\<And>x xs. ms = x # xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases 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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
from \<open>length rs = length cs\<close> \<open>tl ms = targetnodes rs\<close>
[PROOF STATE]
proof (chain)
picking this:
length rs = length cs
tl ms = targetnodes rs
[PROOF STEP]
have "length (tl ms) = length cs"
[PROOF STATE]
proof (prove)
using this:
length rs = length cs
tl ms = targetnodes rs

goal (1 subgoal):
 1. length (tl ms) = length cs
[PROOF STEP]
by(simp add:targetnodes_def)
[PROOF STATE]
proof (state)
this:
length (tl ms) = 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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
from \<open>\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<close>
    \<open>\<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>\<close>
    \<open>length (tl ms) = length cs\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
\<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>
length (tl ms) = length cs
[PROOF STEP]
have "\<exists>c \<in> set cs. sourcenode c \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
\<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>
length (tl ms) = length cs

goal (1 subgoal):
 1. \<exists>c\<in>set cs. sourcenode c \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
apply(auto simp:in_set_conv_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m' i. \<lbrakk>\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); length ms - Suc 0 = length cs; call_of_return_node (tl ms ! i) m'; m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; i < length cs\<rbrakk> \<Longrightarrow> \<exists>c\<in>set cs. sourcenode c \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
by(erule_tac x="i" in allE) auto
[PROOF STATE]
proof (state)
this:
\<exists>c\<in>set cs. sourcenode c \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

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; tl ms = targetnodes rs; length rs = length cs; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))\<rbrakk> \<Longrightarrow> \<not> slice_edge S cs a
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>c\<in>set cs. sourcenode c \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma observable_move_slice_edge:
  "\<lbrakk>S,f \<turnstile> (ms,s) -a\<rightarrow> (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_edge S cs a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S,f \<turnstile> (ms,s) -a\<rightarrow> (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_edge S cs a
[PROOF STEP]
proof(induct rule:observable_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); \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length s' = length s; length ms = length s; hd ms = sourcenode a; ms' = targetnode a # tl ms; 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_edge S cs a
 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; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; 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_edge S cs a
 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'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; 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_edge S cs a
[PROOF STEP]
case (observable_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)
\<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
length s' = length s
length ms = length s
hd ms = sourcenode a
ms' = targetnode a # tl ms
tl ms = targetnodes rs
length rs = length cs
\<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); \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length s' = length s; length ms = length s; hd ms = sourcenode a; ms' = targetnode a # tl ms; 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_edge S cs a
 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; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; 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_edge S cs a
 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'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; 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_edge S cs a
[PROOF STEP]
from \<open>pred (f a) s\<close> \<open>length ms = length s\<close>
[PROOF STATE]
proof (chain)
picking this:
pred (f a) s
length ms = length s
[PROOF STEP]
obtain x xs where "ms = x#xs"
[PROOF STATE]
proof (prove)
using this:
pred (f a) s
length ms = length s

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

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); \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length s' = length s; length ms = length s; hd ms = sourcenode a; ms' = targetnode a # tl ms; 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_edge S cs a
 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; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; 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_edge S cs a
 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'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; 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_edge S cs a
[PROOF STEP]
from \<open>length rs = length cs\<close> \<open>tl ms = targetnodes rs\<close>
[PROOF STATE]
proof (chain)
picking this:
length rs = length cs
tl ms = targetnodes rs
[PROOF STEP]
have "length (tl ms) = length cs"
[PROOF STATE]
proof (prove)
using this:
length rs = length cs
tl ms = targetnodes rs

goal (1 subgoal):
 1. length (tl ms) = length cs
[PROOF STEP]
by(simp add:targetnodes_def)
[PROOF STATE]
proof (state)
this:
length (tl ms) = length cs

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); \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length s' = length s; length ms = length s; hd ms = sourcenode a; ms' = targetnode a # tl ms; 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_edge S cs a
 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; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; 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_edge S cs a
 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'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; 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_edge S cs a
[PROOF STEP]
with \<open>\<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>
    \<open>\<forall>i<length cs. call_of_return_node (tl ms!i) (sourcenode (cs!i))\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
length (tl ms) = length cs
[PROOF STEP]
have "\<forall>c \<in> set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
length (tl ms) = length cs

goal (1 subgoal):
 1. \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
apply(auto simp:in_set_conv_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); length ms - Suc 0 = length cs; i < length cs\<rbrakk> \<Longrightarrow> sourcenode (cs ! i) \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
by(erule_tac x="i" in allE) auto
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

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); \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length s' = length s; length ms = length s; hd ms = sourcenode a; ms' = targetnode a # tl ms; 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_edge S cs a
 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; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; 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_edge S cs a
 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'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; 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_edge S cs a
[PROOF STEP]
with \<open>hd ms = sourcenode a\<close> \<open>hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close> \<open>intra_kind (kind a)\<close>
[PROOF STATE]
proof (chain)
picking this:
hd ms = sourcenode a
hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
intra_kind (kind a)
\<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
hd ms = sourcenode a
hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
intra_kind (kind a)
\<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. slice_edge S cs a
[PROOF STEP]
by(auto simp:slice_edge_def simp:intra_kind_def)
[PROOF STATE]
proof (state)
this:
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; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; 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_edge S cs a
 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'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; 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_edge S cs a
[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; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; 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_edge S cs a
 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'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; 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_edge S cs a
[PROOF STEP]
case (observable_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
\<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
length ms = length s
length s' = Suc (length s)
hd ms = sourcenode a
ms' = targetnode a # targetnode a' # tl ms
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>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; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; 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_edge S cs a
 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'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; 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_edge S cs a
[PROOF STEP]
from \<open>pred (f a) s\<close> \<open>length ms = length s\<close>
[PROOF STATE]
proof (chain)
picking this:
pred (f a) s
length ms = length s
[PROOF STEP]
obtain x xs where "ms = x#xs"
[PROOF STATE]
proof (prove)
using this:
pred (f a) s
length ms = length s

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

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; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; 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_edge S cs a
 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'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; 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_edge S cs a
[PROOF STEP]
from \<open>length rs = length cs\<close> \<open>tl ms = targetnodes rs\<close>
[PROOF STATE]
proof (chain)
picking this:
length rs = length cs
tl ms = targetnodes rs
[PROOF STEP]
have "length (tl ms) = length cs"
[PROOF STATE]
proof (prove)
using this:
length rs = length cs
tl ms = targetnodes rs

goal (1 subgoal):
 1. length (tl ms) = length cs
[PROOF STEP]
by(simp add:targetnodes_def)
[PROOF STATE]
proof (state)
this:
length (tl ms) = length 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; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; 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_edge S cs a
 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'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; 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_edge S cs a
[PROOF STEP]
with \<open>\<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>
    \<open>\<forall>i<length cs. call_of_return_node (tl ms!i) (sourcenode (cs!i))\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
length (tl ms) = length cs
[PROOF STEP]
have "\<forall>c \<in> set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
length (tl ms) = length cs

goal (1 subgoal):
 1. \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
apply(auto simp:in_set_conv_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); length ms - Suc 0 = length cs; i < length cs\<rbrakk> \<Longrightarrow> sourcenode (cs ! i) \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
by(erule_tac x="i" in allE) auto
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

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; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms; 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_edge S cs a
 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'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; 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_edge S cs a
[PROOF STEP]
with \<open>hd ms = sourcenode a\<close> \<open>hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
hd ms = sourcenode a
hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
\<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
hd ms = sourcenode a
hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
\<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. slice_edge S cs a
[PROOF STEP]
by(auto simp:slice_edge_def)
[PROOF STATE]
proof (state)
this:
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'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; 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_edge S cs a
[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'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; 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_edge S cs a
[PROOF STEP]
case (observable_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'
\<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
length ms = length s
length s = Suc (length s')
s' \<noteq> []
hd ms = sourcenode a
hd (tl ms) = targetnode a
ms' = tl ms
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. \<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'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; 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_edge S cs a
[PROOF STEP]
from \<open>pred (f a) s\<close> \<open>length ms = length s\<close>
[PROOF STATE]
proof (chain)
picking this:
pred (f a) s
length ms = length s
[PROOF STEP]
obtain x xs where "ms = x#xs"
[PROOF STATE]
proof (prove)
using this:
pred (f a) s
length ms = length s

goal (1 subgoal):
 1. (\<And>x xs. ms = x # xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases 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'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; 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_edge S cs a
[PROOF STEP]
from \<open>length rs = length cs\<close> \<open>tl ms = targetnodes rs\<close>
[PROOF STATE]
proof (chain)
picking this:
length rs = length cs
tl ms = targetnodes rs
[PROOF STEP]
have "length (tl ms) = length cs"
[PROOF STATE]
proof (prove)
using this:
length rs = length cs
tl ms = targetnodes rs

goal (1 subgoal):
 1. length (tl ms) = length cs
[PROOF STEP]
by(simp add:targetnodes_def)
[PROOF STATE]
proof (state)
this:
length (tl ms) = 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'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; 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_edge S cs a
[PROOF STEP]
with \<open>\<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>
    \<open>\<forall>i<length cs. call_of_return_node (tl ms!i) (sourcenode (cs!i))\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
length (tl ms) = length cs
[PROOF STEP]
have "\<forall>c \<in> set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
\<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))
length (tl ms) = length cs

goal (1 subgoal):
 1. \<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
apply(auto simp:in_set_conv_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i)); length ms - Suc 0 = length cs; i < length cs\<rbrakk> \<Longrightarrow> sourcenode (cs ! i) \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
by(erule_tac x="i" in allE) auto
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

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'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms; 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_edge S cs a
[PROOF STEP]
with \<open>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'\<close>
[PROOF STATE]
proof (chain)
picking this:
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'
\<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'
\<forall>c\<in>set cs. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. slice_edge S cs a
[PROOF STEP]
by(auto simp:slice_edge_def)
[PROOF STATE]
proof (state)
this:
slice_edge S cs a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma slice_edges_Append:
  "\<lbrakk>slice_edges S cs as = as'; slice_edges S (upd_cs cs as) asx = asx'\<rbrakk>
  \<Longrightarrow> slice_edges S cs (as@asx) = as'@asx'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slice_edges S cs as = as'; slice_edges S (upd_cs cs as) asx = asx'\<rbrakk> \<Longrightarrow> slice_edges S cs (as @ asx) = as' @ asx'
[PROOF STEP]
proof(induct as arbitrary:cs as')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>cs as'. \<lbrakk>slice_edges S cs [] = as'; slice_edges S (upd_cs cs []) asx = asx'\<rbrakk> \<Longrightarrow> slice_edges S cs ([] @ asx) = as' @ asx'
 2. \<And>a as cs as'. \<lbrakk>\<And>cs as'. \<lbrakk>slice_edges S cs as = as'; slice_edges S (upd_cs cs as) asx = asx'\<rbrakk> \<Longrightarrow> slice_edges S cs (as @ asx) = as' @ asx'; slice_edges S cs (a # as) = as'; slice_edges S (upd_cs cs (a # as)) asx = asx'\<rbrakk> \<Longrightarrow> slice_edges S cs ((a # as) @ asx) = as' @ asx'
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
slice_edges S cs [] = as'
slice_edges S (upd_cs cs []) asx = asx'

goal (2 subgoals):
 1. \<And>cs as'. \<lbrakk>slice_edges S cs [] = as'; slice_edges S (upd_cs cs []) asx = asx'\<rbrakk> \<Longrightarrow> slice_edges S cs ([] @ asx) = as' @ asx'
 2. \<And>a as cs as'. \<lbrakk>\<And>cs as'. \<lbrakk>slice_edges S cs as = as'; slice_edges S (upd_cs cs as) asx = asx'\<rbrakk> \<Longrightarrow> slice_edges S cs (as @ asx) = as' @ asx'; slice_edges S cs (a # as) = as'; slice_edges S (upd_cs cs (a # as)) asx = asx'\<rbrakk> \<Longrightarrow> slice_edges S cs ((a # as) @ asx) = as' @ asx'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
slice_edges S cs [] = as'
slice_edges S (upd_cs cs []) asx = asx'

goal (1 subgoal):
 1. slice_edges S cs ([] @ asx) = as' @ asx'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
slice_edges S cs ([] @ asx) = as' @ asx'

goal (1 subgoal):
 1. \<And>a as cs as'. \<lbrakk>\<And>cs as'. \<lbrakk>slice_edges S cs as = as'; slice_edges S (upd_cs cs as) asx = asx'\<rbrakk> \<Longrightarrow> slice_edges S cs (as @ asx) = as' @ asx'; slice_edges S cs (a # as) = as'; slice_edges S (upd_cs cs (a # as)) asx = asx'\<rbrakk> \<Longrightarrow> slice_edges S cs ((a # as) @ asx) = as' @ asx'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a as cs as'. \<lbrakk>\<And>cs as'. \<lbrakk>slice_edges S cs as = as'; slice_edges S (upd_cs cs as) asx = asx'\<rbrakk> \<Longrightarrow> slice_edges S cs (as @ asx) = as' @ asx'; slice_edges S cs (a # as) = as'; slice_edges S (upd_cs cs (a # as)) asx = asx'\<rbrakk> \<Longrightarrow> slice_edges S cs ((a # as) @ asx) = as' @ asx'
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>slice_edges S ?cs xs = ?as'; slice_edges S (upd_cs ?cs xs) asx = asx'\<rbrakk> \<Longrightarrow> slice_edges S ?cs (xs @ asx) = ?as' @ asx'
slice_edges S cs (x # xs) = as'
slice_edges S (upd_cs cs (x # xs)) asx = asx'

goal (1 subgoal):
 1. \<And>a as cs as'. \<lbrakk>\<And>cs as'. \<lbrakk>slice_edges S cs as = as'; slice_edges S (upd_cs cs as) asx = asx'\<rbrakk> \<Longrightarrow> slice_edges S cs (as @ asx) = as' @ asx'; slice_edges S cs (a # as) = as'; slice_edges S (upd_cs cs (a # as)) asx = asx'\<rbrakk> \<Longrightarrow> slice_edges S cs ((a # as) @ asx) = as' @ asx'
[PROOF STEP]
note IH = \<open>\<And>cs as'. \<lbrakk>slice_edges S cs xs = as';
    slice_edges S (upd_cs cs xs) asx = asx'\<rbrakk>
    \<Longrightarrow> slice_edges S cs (xs @ asx) = as' @ asx'\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>slice_edges S ?cs xs = ?as'; slice_edges S (upd_cs ?cs xs) asx = asx'\<rbrakk> \<Longrightarrow> slice_edges S ?cs (xs @ asx) = ?as' @ asx'

goal (1 subgoal):
 1. \<And>a as cs as'. \<lbrakk>\<And>cs as'. \<lbrakk>slice_edges S cs as = as'; slice_edges S (upd_cs cs as) asx = asx'\<rbrakk> \<Longrightarrow> slice_edges S cs (as @ asx) = as' @ asx'; slice_edges S cs (a # as) = as'; slice_edges S (upd_cs cs (a # as)) asx = asx'\<rbrakk> \<Longrightarrow> slice_edges S cs ((a # as) @ asx) = as' @ asx'
[PROOF STEP]
from \<open>slice_edges S (upd_cs cs (x # xs)) asx = asx'\<close>
[PROOF STATE]
proof (chain)
picking this:
slice_edges S (upd_cs cs (x # xs)) asx = asx'
[PROOF STEP]
have "slice_edges S (upd_cs (upd_cs cs [x]) xs) asx = asx'"
[PROOF STATE]
proof (prove)
using this:
slice_edges S (upd_cs cs (x # xs)) asx = asx'

goal (1 subgoal):
 1. slice_edges S (upd_cs (upd_cs cs [x]) xs) asx = asx'
[PROOF STEP]
by(cases "kind x")(auto,cases cs,auto)
[PROOF STATE]
proof (state)
this:
slice_edges S (upd_cs (upd_cs cs [x]) xs) asx = asx'

goal (1 subgoal):
 1. \<And>a as cs as'. \<lbrakk>\<And>cs as'. \<lbrakk>slice_edges S cs as = as'; slice_edges S (upd_cs cs as) asx = asx'\<rbrakk> \<Longrightarrow> slice_edges S cs (as @ asx) = as' @ asx'; slice_edges S cs (a # as) = as'; slice_edges S (upd_cs cs (a # as)) asx = asx'\<rbrakk> \<Longrightarrow> slice_edges S cs ((a # as) @ asx) = as' @ asx'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slice_edges S cs ((x # xs) @ asx) = as' @ asx'
[PROOF STEP]
proof(cases "slice_edge S cs x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. slice_edge S cs x \<Longrightarrow> slice_edges S cs ((x # xs) @ asx) = as' @ asx'
 2. \<not> slice_edge S cs x \<Longrightarrow> slice_edges S cs ((x # xs) @ asx) = as' @ asx'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
slice_edge S cs x

goal (2 subgoals):
 1. slice_edge S cs x \<Longrightarrow> slice_edges S cs ((x # xs) @ asx) = as' @ asx'
 2. \<not> slice_edge S cs x \<Longrightarrow> slice_edges S cs ((x # xs) @ asx) = as' @ asx'
[PROOF STEP]
with \<open>slice_edges S cs (x # xs) = as'\<close>
[PROOF STATE]
proof (chain)
picking this:
slice_edges S cs (x # xs) = as'
slice_edge S cs x
[PROOF STEP]
have "x#slice_edges S (upd_cs cs [x]) xs = as'"
[PROOF STATE]
proof (prove)
using this:
slice_edges S cs (x # xs) = as'
slice_edge S cs x

goal (1 subgoal):
 1. x # slice_edges S (upd_cs cs [x]) xs = as'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x # slice_edges S (upd_cs cs [x]) xs = as'

goal (2 subgoals):
 1. slice_edge S cs x \<Longrightarrow> slice_edges S cs ((x # xs) @ asx) = as' @ asx'
 2. \<not> slice_edge S cs x \<Longrightarrow> slice_edges S cs ((x # xs) @ asx) = as' @ asx'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x # slice_edges S (upd_cs cs [x]) xs = as'
[PROOF STEP]
obtain xs' where "as' = x#xs'"
      and "slice_edges S (upd_cs cs [x]) xs = xs'"
[PROOF STATE]
proof (prove)
using this:
x # slice_edges S (upd_cs cs [x]) xs = as'

goal (1 subgoal):
 1. (\<And>xs'. \<lbrakk>as' = x # xs'; slice_edges S (upd_cs cs [x]) xs = xs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases as') auto
[PROOF STATE]
proof (state)
this:
as' = x # xs'
slice_edges S (upd_cs cs [x]) xs = xs'

goal (2 subgoals):
 1. slice_edge S cs x \<Longrightarrow> slice_edges S cs ((x # xs) @ asx) = as' @ asx'
 2. \<not> slice_edge S cs x \<Longrightarrow> slice_edges S cs ((x # xs) @ asx) = as' @ asx'
[PROOF STEP]
from IH[OF \<open>slice_edges S (upd_cs cs [x]) xs = xs'\<close>
      \<open>slice_edges S (upd_cs (upd_cs cs [x]) xs) asx = asx'\<close>]
[PROOF STATE]
proof (chain)
picking this:
slice_edges S (upd_cs cs [x]) (xs @ asx) = xs' @ asx'
[PROOF STEP]
have "slice_edges S (upd_cs cs [x]) (xs @ asx) = xs' @ asx'"
[PROOF STATE]
proof (prove)
using this:
slice_edges S (upd_cs cs [x]) (xs @ asx) = xs' @ asx'

goal (1 subgoal):
 1. slice_edges S (upd_cs cs [x]) (xs @ asx) = xs' @ asx'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
slice_edges S (upd_cs cs [x]) (xs @ asx) = xs' @ asx'

goal (2 subgoals):
 1. slice_edge S cs x \<Longrightarrow> slice_edges S cs ((x # xs) @ asx) = as' @ asx'
 2. \<not> slice_edge S cs x \<Longrightarrow> slice_edges S cs ((x # xs) @ asx) = as' @ asx'
[PROOF STEP]
with True \<open>as' = x#xs'\<close>
[PROOF STATE]
proof (chain)
picking this:
slice_edge S cs x
as' = x # xs'
slice_edges S (upd_cs cs [x]) (xs @ asx) = xs' @ asx'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
slice_edge S cs x
as' = x # xs'
slice_edges S (upd_cs cs [x]) (xs @ asx) = xs' @ asx'

goal (1 subgoal):
 1. slice_edges S cs ((x # xs) @ asx) = as' @ asx'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
slice_edges S cs ((x # xs) @ asx) = as' @ asx'

goal (1 subgoal):
 1. \<not> slice_edge S cs x \<Longrightarrow> slice_edges S cs ((x # xs) @ asx) = as' @ asx'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> slice_edge S cs x \<Longrightarrow> slice_edges S cs ((x # xs) @ asx) = as' @ asx'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> slice_edge S cs x

goal (1 subgoal):
 1. \<not> slice_edge S cs x \<Longrightarrow> slice_edges S cs ((x # xs) @ asx) = as' @ asx'
[PROOF STEP]
with \<open>slice_edges S cs (x # xs) = as'\<close>
[PROOF STATE]
proof (chain)
picking this:
slice_edges S cs (x # xs) = as'
\<not> slice_edge S cs x
[PROOF STEP]
have "slice_edges S (upd_cs cs [x]) xs = as'"
[PROOF STATE]
proof (prove)
using this:
slice_edges S cs (x # xs) = as'
\<not> slice_edge S cs x

goal (1 subgoal):
 1. slice_edges S (upd_cs cs [x]) xs = as'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
slice_edges S (upd_cs cs [x]) xs = as'

goal (1 subgoal):
 1. \<not> slice_edge S cs x \<Longrightarrow> slice_edges S cs ((x # xs) @ asx) = as' @ asx'
[PROOF STEP]
from IH[OF this \<open>slice_edges S (upd_cs (upd_cs cs [x]) xs) asx = asx'\<close>]
[PROOF STATE]
proof (chain)
picking this:
slice_edges S (upd_cs cs [x]) (xs @ asx) = as' @ asx'
[PROOF STEP]
have "slice_edges S (upd_cs cs [x]) (xs @ asx) = as' @ asx'"
[PROOF STATE]
proof (prove)
using this:
slice_edges S (upd_cs cs [x]) (xs @ asx) = as' @ asx'

goal (1 subgoal):
 1. slice_edges S (upd_cs cs [x]) (xs @ asx) = as' @ asx'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
slice_edges S (upd_cs cs [x]) (xs @ asx) = as' @ asx'

goal (1 subgoal):
 1. \<not> slice_edge S cs x \<Longrightarrow> slice_edges S cs ((x # xs) @ asx) = as' @ asx'
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
\<not> slice_edge S cs x
slice_edges S (upd_cs cs [x]) (xs @ asx) = as' @ asx'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> slice_edge S cs x
slice_edges S (upd_cs cs [x]) (xs @ asx) = as' @ asx'

goal (1 subgoal):
 1. slice_edges S cs ((x # xs) @ asx) = as' @ asx'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
slice_edges S cs ((x # xs) @ asx) = as' @ asx'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
slice_edges S cs ((x # xs) @ asx) = as' @ asx'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma slice_edges_Nil_split:
  "slice_edges S cs (as@as') = []
  \<Longrightarrow> slice_edges S cs as = [] \<and> slice_edges S (upd_cs cs as) as' = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slice_edges S cs (as @ as') = [] \<Longrightarrow> slice_edges S cs as = [] \<and> slice_edges S (upd_cs cs as) as' = []
[PROOF STEP]
apply(induct as arbitrary:cs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>cs. slice_edges S cs ([] @ as') = [] \<Longrightarrow> slice_edges S cs [] = [] \<and> slice_edges S (upd_cs cs []) as' = []
 2. \<And>a as cs. \<lbrakk>\<And>cs. slice_edges S cs (as @ as') = [] \<Longrightarrow> slice_edges S cs as = [] \<and> slice_edges S (upd_cs cs as) as' = []; slice_edges S cs ((a # as) @ as') = []\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> slice_edges S (upd_cs cs (a # as)) as' = []
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as cs. \<lbrakk>\<And>cs. slice_edges S cs (as @ as') = [] \<Longrightarrow> slice_edges S cs as = [] \<and> slice_edges S (upd_cs cs as) as' = []; slice_edges S cs ((a # as) @ as') = []\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> slice_edges S (upd_cs cs (a # as)) as' = []
[PROOF STEP]
apply(case_tac "slice_edge S cs a")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a as cs. \<lbrakk>\<And>cs. slice_edges S cs (as @ as') = [] \<Longrightarrow> slice_edges S cs as = [] \<and> slice_edges S (upd_cs cs as) as' = []; slice_edges S cs ((a # as) @ as') = []; slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> slice_edges S (upd_cs cs (a # as)) as' = []
 2. \<And>a as cs. \<lbrakk>\<And>cs. slice_edges S cs (as @ as') = [] \<Longrightarrow> slice_edges S cs as = [] \<and> slice_edges S (upd_cs cs as) as' = []; slice_edges S cs ((a # as) @ as') = []; \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S cs (a # as) = [] \<and> slice_edges S (upd_cs cs (a # as)) as' = []
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as cs. \<lbrakk>\<And>cs. slice_edges S cs (as @ as') = [] \<Longrightarrow> slice_edges S cs as = [] \<and> slice_edges S (upd_cs cs as) as' = []; slice_edges S (case kind a of Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Rightarrow> upd_cs (a # cs) [] | Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Rightarrow> case cs of [] \<Rightarrow> upd_cs cs [] | c' # cs' \<Rightarrow> upd_cs cs' [] | _ \<Rightarrow> upd_cs cs []) (as @ as') = []; \<not> slice_edge S cs a\<rbrakk> \<Longrightarrow> slice_edges S (case kind a of Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Rightarrow> upd_cs (a # cs) as | Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Rightarrow> case cs of [] \<Rightarrow> upd_cs cs as | c' # cs' \<Rightarrow> upd_cs cs' as | _ \<Rightarrow> upd_cs cs as) as' = []
[PROOF STEP]
apply(case_tac "kind a")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a as cs x1. \<lbrakk>\<And>cs. slice_edges S cs (as @ as') = [] \<Longrightarrow> slice_edges S cs as = [] \<and> slice_edges S (upd_cs cs as) as' = []; slice_edges S (case kind a of Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Rightarrow> upd_cs (a # cs) [] | Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Rightarrow> case cs of [] \<Rightarrow> upd_cs cs [] | c' # cs' \<Rightarrow> upd_cs cs' [] | _ \<Rightarrow> upd_cs cs []) (as @ as') = []; \<not> slice_edge S cs a; kind a = \<Up>x1\<rbrakk> \<Longrightarrow> slice_edges S (case kind a of Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Rightarrow> upd_cs (a # cs) as | Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Rightarrow> case cs of [] \<Rightarrow> upd_cs cs as | c' # cs' \<Rightarrow> upd_cs cs' as | _ \<Rightarrow> upd_cs cs as) as' = []
 2. \<And>a as cs x2. \<lbrakk>\<And>cs. slice_edges S cs (as @ as') = [] \<Longrightarrow> slice_edges S cs as = [] \<and> slice_edges S (upd_cs cs as) as' = []; slice_edges S (case kind a of Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Rightarrow> upd_cs (a # cs) [] | Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Rightarrow> case cs of [] \<Rightarrow> upd_cs cs [] | c' # cs' \<Rightarrow> upd_cs cs' [] | _ \<Rightarrow> upd_cs cs []) (as @ as') = []; \<not> slice_edge S cs a; kind a = (x2)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> slice_edges S (case kind a of Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Rightarrow> upd_cs (a # cs) as | Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Rightarrow> case cs of [] \<Rightarrow> upd_cs cs as | c' # cs' \<Rightarrow> upd_cs cs' as | _ \<Rightarrow> upd_cs cs as) as' = []
 3. \<And>a as cs x31 x32 x33 x34. \<lbrakk>\<And>cs. slice_edges S cs (as @ as') = [] \<Longrightarrow> slice_edges S cs as = [] \<and> slice_edges S (upd_cs cs as) as' = []; slice_edges S (case kind a of Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Rightarrow> upd_cs (a # cs) [] | Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Rightarrow> case cs of [] \<Rightarrow> upd_cs cs [] | c' # cs' \<Rightarrow> upd_cs cs' [] | _ \<Rightarrow> upd_cs cs []) (as @ as') = []; \<not> slice_edge S cs a; kind a = x31:x32\<hookrightarrow>\<^bsub>x33\<^esub>x34\<rbrakk> \<Longrightarrow> slice_edges S (case kind a of Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Rightarrow> upd_cs (a # cs) as | Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Rightarrow> case cs of [] \<Rightarrow> upd_cs cs as | c' # cs' \<Rightarrow> upd_cs cs' as | _ \<Rightarrow> upd_cs cs as) as' = []
 4. \<And>a as cs x41 x42 x43. \<lbrakk>\<And>cs. slice_edges S cs (as @ as') = [] \<Longrightarrow> slice_edges S cs as = [] \<and> slice_edges S (upd_cs cs as) as' = []; slice_edges S (case kind a of Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Rightarrow> upd_cs (a # cs) [] | Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Rightarrow> case cs of [] \<Rightarrow> upd_cs cs [] | c' # cs' \<Rightarrow> upd_cs cs' [] | _ \<Rightarrow> upd_cs cs []) (as @ as') = []; \<not> slice_edge S cs a; kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43\<rbrakk> \<Longrightarrow> slice_edges S (case kind a of Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Rightarrow> upd_cs (a # cs) as | Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Rightarrow> case cs of [] \<Rightarrow> upd_cs cs as | c' # cs' \<Rightarrow> upd_cs cs' as | _ \<Rightarrow> upd_cs cs as) as' = []
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as cs x41 x42 x43. \<lbrakk>\<And>cs. slice_edges S cs (as @ as') = [] \<Longrightarrow> slice_edges S cs as = [] \<and> slice_edges S (upd_cs cs as) as' = []; slice_edges S (case cs of [] \<Rightarrow> upd_cs cs [] | c' # cs' \<Rightarrow> upd_cs cs' []) (as @ as') = []; \<not> slice_edge S cs a; kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43\<rbrakk> \<Longrightarrow> slice_edges S (case cs of [] \<Rightarrow> upd_cs cs as | c' # cs' \<Rightarrow> upd_cs cs' as) as' = []
[PROOF STEP]
apply(case_tac cs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a as cs x41 x42 x43. \<lbrakk>\<And>cs. slice_edges S cs (as @ as') = [] \<Longrightarrow> slice_edges S cs as = [] \<and> slice_edges S (upd_cs cs as) as' = []; slice_edges S (case cs of [] \<Rightarrow> upd_cs cs [] | c' # cs' \<Rightarrow> upd_cs cs' []) (as @ as') = []; \<not> slice_edge S cs a; kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43; cs = []\<rbrakk> \<Longrightarrow> slice_edges S (case cs of [] \<Rightarrow> upd_cs cs as | c' # cs' \<Rightarrow> upd_cs cs' as) as' = []
 2. \<And>a as cs x41 x42 x43 aa list. \<lbrakk>\<And>cs. slice_edges S cs (as @ as') = [] \<Longrightarrow> slice_edges S cs as = [] \<and> slice_edges S (upd_cs cs as) as' = []; slice_edges S (case cs of [] \<Rightarrow> upd_cs cs [] | c' # cs' \<Rightarrow> upd_cs cs' []) (as @ as') = []; \<not> slice_edge S cs a; kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43; cs = aa # list\<rbrakk> \<Longrightarrow> slice_edges S (case cs of [] \<Rightarrow> upd_cs cs as | c' # cs' \<Rightarrow> upd_cs cs' as) as' = []
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done