[STATEMENT]
lemma silent_moves_called_node_in_slice1_hd_nodestack_in_slice1:
  assumes "S,kind \<turnstile> (m#ms,s) =as\<Rightarrow>\<^sub>\<tau> (m'#ms',s')" and "valid_node m"
  and "CFG_node m' \<in> sum_SDG_slice1 nx"
  and "\<forall>mx \<in> set ms. \<exists>mx'. call_of_return_node mx mx' \<and>
      mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
  and "\<forall>i < length rs. rs!i \<in> get_return_edges (cs!i)" and "ms = targetnodes rs"
  and "valid_return_list rs m" and "length rs = length cs"
  obtains as' a as'' where "as = as'@a#as''" and "\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs"
  and "call_of_return_node (hd ms') (sourcenode a)"
  and "targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'" and "CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx"
  | "ms' = ms"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>as' a as''. \<lbrakk>as = as' @ a # as''; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; call_of_return_node (hd ms') (sourcenode a); targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'; CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> thesis; ms' = ms \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
from \<open>S,kind \<turnstile> (m#ms,s) =as\<Rightarrow>\<^sub>\<tau> (m'#ms',s')\<close> \<open>valid_node m\<close>
    \<open>\<forall>i < length rs. rs!i \<in> get_return_edges (cs!i)\<close> \<open>ms = targetnodes rs\<close>
    \<open>valid_return_list rs m\<close> \<open>length rs = length cs\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
valid_node m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
ms = targetnodes rs
valid_return_list rs m
length rs = length cs
[PROOF STEP]
have "m -as\<rightarrow>* m'"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
valid_node m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
ms = targetnodes rs
valid_return_list rs m
length rs = length cs

goal (1 subgoal):
 1. m -as\<rightarrow>* m'
[PROOF STEP]
by(auto dest:silent_moves_vpa_path[of _ _ _ _ _ _ _ _ _ rs cs]
            simp:valid_call_list_def valid_return_list_def targetnodes_def)
[PROOF STATE]
proof (state)
this:
m -as\<rightarrow>* m'

goal (1 subgoal):
 1. (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
from \<open>S,kind \<turnstile> (m#ms,s) =as\<Rightarrow>\<^sub>\<tau> (m'#ms',s')\<close> \<open>valid_node m\<close>
    \<open>\<forall>mx \<in> set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>
    \<open>\<forall>i < length rs. rs!i \<in> get_return_edges (cs!i)\<close> \<open>ms = targetnodes rs\<close>
    \<open>valid_return_list rs m\<close> \<open>length rs = length cs\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
valid_node m
\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
ms = targetnodes rs
valid_return_list rs m
length rs = length cs
[PROOF STEP]
show "(\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and>
    call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and>
    CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
valid_node m
\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
ms = targetnodes rs
valid_return_list rs m
length rs = length cs

goal (1 subgoal):
 1. (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
proof(rule silent_moves_call_edge)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>as' a as''. \<lbrakk>as = as' @ a # as''; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; call_of_return_node (hd ms') (sourcenode a); targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'\<rbrakk> \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
 2. ms' = ms \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
fix as' a as''
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>as' a as''. \<lbrakk>as = as' @ a # as''; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; call_of_return_node (hd ms') (sourcenode a); targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'\<rbrakk> \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
 2. ms' = ms \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
assume "as = as'@a#as''" and "\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs"
      and "call_of_return_node (hd ms') (sourcenode a)"
      and "targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'"
[PROOF STATE]
proof (state)
this:
as = as' @ a # as''
\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
call_of_return_node (hd ms') (sourcenode a)
targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'

goal (2 subgoals):
 1. \<And>as' a as''. \<lbrakk>as = as' @ a # as''; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; call_of_return_node (hd ms') (sourcenode a); targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'\<rbrakk> \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
 2. ms' = ms \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
from \<open>\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
obtain Q r p fs
      where "kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs"
[PROOF STATE]
proof (prove)
using this:
\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. (\<And>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (2 subgoals):
 1. \<And>as' a as''. \<lbrakk>as = as' @ a # as''; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; call_of_return_node (hd ms') (sourcenode a); targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'\<rbrakk> \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
 2. ms' = ms \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
from \<open>targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'
[PROOF STEP]
obtain asx where "targetnode a -asx\<rightarrow>\<^sub>\<iota>* m'"
[PROOF STATE]
proof (prove)
using this:
targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'

goal (1 subgoal):
 1. (\<And>asx. targetnode a -asx\<rightarrow>\<^sub>\<iota>* m' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by -(erule same_level_path_inner_path)
[PROOF STATE]
proof (state)
this:
targetnode a -asx\<rightarrow>\<^sub>\<iota>* m'

goal (2 subgoals):
 1. \<And>as' a as''. \<lbrakk>as = as' @ a # as''; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; call_of_return_node (hd ms') (sourcenode a); targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'\<rbrakk> \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
 2. ms' = ms \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
from \<open>m -as\<rightarrow>* m'\<close> \<open>as = as'@a#as''\<close>
[PROOF STATE]
proof (chain)
picking this:
m -as\<rightarrow>* m'
as = as' @ a # as''
[PROOF STEP]
have "valid_edge a"
[PROOF STATE]
proof (prove)
using this:
m -as\<rightarrow>* m'
as = as' @ a # as''

goal (1 subgoal):
 1. valid_edge a
[PROOF STEP]
by(fastforce dest:path_split simp:vp_def)
[PROOF STATE]
proof (state)
this:
valid_edge a

goal (2 subgoals):
 1. \<And>as' a as''. \<lbrakk>as = as' @ a # as''; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; call_of_return_node (hd ms') (sourcenode a); targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'\<rbrakk> \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
 2. ms' = ms \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
have "m' \<noteq> (_Exit_)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<noteq> (_Exit_)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m' = (_Exit_) \<Longrightarrow> False
[PROOF STEP]
assume "m' = (_Exit_)"
[PROOF STATE]
proof (state)
this:
m' = (_Exit_)

goal (1 subgoal):
 1. m' = (_Exit_) \<Longrightarrow> False
[PROOF STEP]
have "get_proc (_Exit_) = Main"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get_proc (_Exit_) = Main
[PROOF STEP]
by(rule get_proc_Exit)
[PROOF STATE]
proof (state)
this:
get_proc (_Exit_) = Main

goal (1 subgoal):
 1. m' = (_Exit_) \<Longrightarrow> False
[PROOF STEP]
from \<open>targetnode a -asx\<rightarrow>\<^sub>\<iota>* m'\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a -asx\<rightarrow>\<^sub>\<iota>* m'
[PROOF STEP]
have "get_proc (targetnode a) = get_proc m'"
[PROOF STATE]
proof (prove)
using this:
targetnode a -asx\<rightarrow>\<^sub>\<iota>* m'

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

goal (1 subgoal):
 1. m' = (_Exit_) \<Longrightarrow> False
[PROOF STEP]
with \<open>m' = (_Exit_)\<close> \<open>get_proc (_Exit_) = Main\<close>
[PROOF STATE]
proof (chain)
picking this:
m' = (_Exit_)
get_proc (_Exit_) = Main
get_proc (targetnode a) = get_proc m'
[PROOF STEP]
have "get_proc (targetnode a) = Main"
[PROOF STATE]
proof (prove)
using this:
m' = (_Exit_)
get_proc (_Exit_) = Main
get_proc (targetnode a) = get_proc m'

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

goal (1 subgoal):
 1. m' = (_Exit_) \<Longrightarrow> False
[PROOF STEP]
with \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>valid_edge a\<close>
[PROOF STATE]
proof (chain)
picking this:
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
valid_edge a
get_proc (targetnode a) = Main
[PROOF STEP]
have "kind a = Q:r\<hookrightarrow>\<^bsub>Main\<^esub>fs"
[PROOF STATE]
proof (prove)
using this:
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
valid_edge a
get_proc (targetnode a) = Main

goal (1 subgoal):
 1. kind a = Q:r\<hookrightarrow>\<^bsub>Main\<^esub>fs
[PROOF STEP]
by(fastforce dest:get_proc_call)
[PROOF STATE]
proof (state)
this:
kind a = Q:r\<hookrightarrow>\<^bsub>Main\<^esub>fs

goal (1 subgoal):
 1. m' = (_Exit_) \<Longrightarrow> False
[PROOF STEP]
with \<open>valid_edge a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>Main\<^esub>fs
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>Main\<^esub>fs

goal (1 subgoal):
 1. False
[PROOF STEP]
by(rule Main_no_call_target)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
m' \<noteq> (_Exit_)

goal (2 subgoals):
 1. \<And>as' a as''. \<lbrakk>as = as' @ a # as''; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; call_of_return_node (hd ms') (sourcenode a); targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'\<rbrakk> \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
 2. ms' = ms \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
proof(cases "targetnode a = m'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. targetnode a = m' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
 2. targetnode a \<noteq> m' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
targetnode a = m'

goal (2 subgoals):
 1. targetnode a = m' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
 2. targetnode a \<noteq> m' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
with \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
targetnode a = m'
[PROOF STEP]
have "CFG_node (sourcenode a) s-p\<rightarrow>\<^bsub>call\<^esub> CFG_node m'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
targetnode a = m'

goal (1 subgoal):
 1. CFG_node (sourcenode a) s-p\<rightarrow>\<^bsub>call\<^esub> CFG_node m'
[PROOF STEP]
by(fastforce intro:sum_SDG_call_edge)
[PROOF STATE]
proof (state)
this:
CFG_node (sourcenode a) s-p\<rightarrow>\<^bsub>call\<^esub> CFG_node m'

goal (2 subgoals):
 1. targetnode a = m' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
 2. targetnode a \<noteq> m' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
with \<open>CFG_node m' \<in> sum_SDG_slice1 nx\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node m' \<in> sum_SDG_slice1 nx
CFG_node (sourcenode a) s-p\<rightarrow>\<^bsub>call\<^esub> CFG_node m'
[PROOF STEP]
have "CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx"
[PROOF STATE]
proof (prove)
using this:
CFG_node m' \<in> sum_SDG_slice1 nx
CFG_node (sourcenode a) s-p\<rightarrow>\<^bsub>call\<^esub> CFG_node m'

goal (1 subgoal):
 1. CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx
[PROOF STEP]
by -(rule call_slice1)
[PROOF STATE]
proof (state)
this:
CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx

goal (2 subgoals):
 1. targetnode a = m' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
 2. targetnode a \<noteq> m' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
with \<open>as = as'@a#as''\<close> \<open>\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
        \<open>call_of_return_node (hd ms') (sourcenode a)\<close>
        \<open>targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'\<close>
[PROOF STATE]
proof (chain)
picking this:
as = as' @ a # as''
\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
call_of_return_node (hd ms') (sourcenode a)
targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'
CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
as = as' @ a # as''
\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
call_of_return_node (hd ms') (sourcenode a)
targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'
CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx

goal (1 subgoal):
 1. (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms

goal (1 subgoal):
 1. targetnode a \<noteq> m' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. targetnode a \<noteq> m' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
targetnode a \<noteq> m'

goal (1 subgoal):
 1. targetnode a \<noteq> m' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
with \<open>targetnode a -asx\<rightarrow>\<^sub>\<iota>* m'\<close> \<open>m' \<noteq> (_Exit_)\<close> \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a -asx\<rightarrow>\<^sub>\<iota>* m'
m' \<noteq> (_Exit_)
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
targetnode a \<noteq> m'
[PROOF STEP]
obtain ns where "CFG_node (targetnode a) cd-ns\<rightarrow>\<^sub>d* CFG_node m'"
[PROOF STATE]
proof (prove)
using this:
targetnode a -asx\<rightarrow>\<^sub>\<iota>* m'
m' \<noteq> (_Exit_)
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
targetnode a \<noteq> m'

goal (1 subgoal):
 1. (\<And>ns. CFG_node (targetnode a) cd-ns\<rightarrow>\<^sub>d* CFG_node m' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim!:in_proc_cdep_SDG_path)
[PROOF STATE]
proof (state)
this:
CFG_node (targetnode a) cd-ns\<rightarrow>\<^sub>d* CFG_node m'

goal (1 subgoal):
 1. targetnode a \<noteq> m' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
hence "CFG_node (targetnode a) is-ns\<rightarrow>\<^sub>d* CFG_node m'"
[PROOF STATE]
proof (prove)
using this:
CFG_node (targetnode a) cd-ns\<rightarrow>\<^sub>d* CFG_node m'

goal (1 subgoal):
 1. CFG_node (targetnode a) is-ns\<rightarrow>\<^sub>d* CFG_node m'
[PROOF STEP]
by(fastforce intro:intra_SDG_path_is_SDG_path cdep_SDG_path_intra_SDG_path)
[PROOF STATE]
proof (state)
this:
CFG_node (targetnode a) is-ns\<rightarrow>\<^sub>d* CFG_node m'

goal (1 subgoal):
 1. targetnode a \<noteq> m' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
with \<open>CFG_node m' \<in> sum_SDG_slice1 nx\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node m' \<in> sum_SDG_slice1 nx
CFG_node (targetnode a) is-ns\<rightarrow>\<^sub>d* CFG_node m'
[PROOF STEP]
have "CFG_node (targetnode a) \<in> sum_SDG_slice1 nx"
[PROOF STATE]
proof (prove)
using this:
CFG_node m' \<in> sum_SDG_slice1 nx
CFG_node (targetnode a) is-ns\<rightarrow>\<^sub>d* CFG_node m'

goal (1 subgoal):
 1. CFG_node (targetnode a) \<in> sum_SDG_slice1 nx
[PROOF STEP]
by -(rule is_SDG_path_slice1)
[PROOF STATE]
proof (state)
this:
CFG_node (targetnode a) \<in> sum_SDG_slice1 nx

goal (1 subgoal):
 1. targetnode a \<noteq> m' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
have "CFG_node (sourcenode a) s-p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. CFG_node (sourcenode a) s-p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a)
[PROOF STEP]
by(fastforce intro:sum_SDG_call_edge)
[PROOF STATE]
proof (state)
this:
CFG_node (sourcenode a) s-p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a)

goal (1 subgoal):
 1. targetnode a \<noteq> m' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
with \<open>CFG_node (targetnode a) \<in> sum_SDG_slice1 nx\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (targetnode a) \<in> sum_SDG_slice1 nx
CFG_node (sourcenode a) s-p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a)
[PROOF STEP]
have "CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx"
[PROOF STATE]
proof (prove)
using this:
CFG_node (targetnode a) \<in> sum_SDG_slice1 nx
CFG_node (sourcenode a) s-p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a)

goal (1 subgoal):
 1. CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx
[PROOF STEP]
by -(rule call_slice1)
[PROOF STATE]
proof (state)
this:
CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx

goal (1 subgoal):
 1. targetnode a \<noteq> m' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
with \<open>as = as'@a#as''\<close> \<open>\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
        \<open>call_of_return_node (hd ms') (sourcenode a)\<close>
        \<open>targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'\<close>
[PROOF STATE]
proof (chain)
picking this:
as = as' @ a # as''
\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
call_of_return_node (hd ms') (sourcenode a)
targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'
CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
as = as' @ a # as''
\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
call_of_return_node (hd ms') (sourcenode a)
targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'
CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx

goal (1 subgoal):
 1. (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms

goal (1 subgoal):
 1. ms' = ms \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ms' = ms \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
assume "ms' = ms"
[PROOF STATE]
proof (state)
this:
ms' = ms

goal (1 subgoal):
 1. ms' = ms \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ms' = ms

goal (1 subgoal):
 1. (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx) \<or> ms' = ms

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma silent_moves_called_node_in_slice1_nodestack_in_slice1:
  "\<lbrakk>S,kind \<turnstile> (m#ms,s) =as\<Rightarrow>\<^sub>\<tau> (m'#ms',s'); valid_node m;
   CFG_node m' \<in> sum_SDG_slice1 nx; nx \<in> S;
   \<forall>mx \<in> set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>;
   \<forall>i < length rs. rs!i \<in> get_return_edges (cs!i); ms = targetnodes rs;
   valid_return_list rs m; length rs = length cs\<rbrakk>
  \<Longrightarrow> \<forall>mx \<in> set ms'. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); valid_node m; CFG_node m' \<in> sum_SDG_slice1 nx; nx \<in> S; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); ms = targetnodes rs; valid_return_list rs m; length rs = length cs\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set ms'. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
proof(induct ms' arbitrary:as m' s')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>as m' s'. \<lbrakk>S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> ([m'],s'); valid_node m; CFG_node m' \<in> sum_SDG_slice1 nx; nx \<in> S; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); ms = targetnodes rs; valid_return_list rs m; length rs = length cs\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set []. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
 2. \<And>a ms' as m' s'. \<lbrakk>\<And>as m' s'. \<lbrakk>S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); valid_node m; CFG_node m' \<in> sum_SDG_slice1 nx; nx \<in> S; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); ms = targetnodes rs; valid_return_list rs m; length rs = length cs\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set ms'. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # a # ms',s'); valid_node m; CFG_node m' \<in> sum_SDG_slice1 nx; nx \<in> S; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); ms = targetnodes rs; valid_return_list rs m; length rs = length cs\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (a # ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
case (Cons mx msx)
[PROOF STATE]
proof (state)
this:
\<lbrakk>S,kind \<turnstile> (m # ms,s) =?as\<Rightarrow>\<^sub>\<tau> (?m' # msx,?s'); valid_node m; CFG_node ?m' \<in> sum_SDG_slice1 nx; nx \<in> S; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); ms = targetnodes rs; valid_return_list rs m; length rs = length cs\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set msx. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')
valid_node m
CFG_node m' \<in> sum_SDG_slice1 nx
nx \<in> S
\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
ms = targetnodes rs
valid_return_list rs m
length rs = length cs

goal (2 subgoals):
 1. \<And>as m' s'. \<lbrakk>S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> ([m'],s'); valid_node m; CFG_node m' \<in> sum_SDG_slice1 nx; nx \<in> S; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); ms = targetnodes rs; valid_return_list rs m; length rs = length cs\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set []. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
 2. \<And>a ms' as m' s'. \<lbrakk>\<And>as m' s'. \<lbrakk>S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); valid_node m; CFG_node m' \<in> sum_SDG_slice1 nx; nx \<in> S; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); ms = targetnodes rs; valid_return_list rs m; length rs = length cs\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set ms'. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # a # ms',s'); valid_node m; CFG_node m' \<in> sum_SDG_slice1 nx; nx \<in> S; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); ms = targetnodes rs; valid_return_list rs m; length rs = length cs\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (a # ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
note IH = \<open>\<And>as m' s'. \<lbrakk>S,kind \<turnstile> (m#ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # msx,s'); valid_node m;
    CFG_node m' \<in> sum_SDG_slice1 nx; nx \<in> S;
   \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>;
   \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); ms = targetnodes rs;
   valid_return_list rs m; length rs = length cs\<rbrakk>
    \<Longrightarrow> \<forall>mx\<in>set msx. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>S,kind \<turnstile> (m # ms,s) =?as\<Rightarrow>\<^sub>\<tau> (?m' # msx,?s'); valid_node m; CFG_node ?m' \<in> sum_SDG_slice1 nx; nx \<in> S; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); ms = targetnodes rs; valid_return_list rs m; length rs = length cs\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set msx. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (2 subgoals):
 1. \<And>as m' s'. \<lbrakk>S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> ([m'],s'); valid_node m; CFG_node m' \<in> sum_SDG_slice1 nx; nx \<in> S; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); ms = targetnodes rs; valid_return_list rs m; length rs = length cs\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set []. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
 2. \<And>a ms' as m' s'. \<lbrakk>\<And>as m' s'. \<lbrakk>S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); valid_node m; CFG_node m' \<in> sum_SDG_slice1 nx; nx \<in> S; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); ms = targetnodes rs; valid_return_list rs m; length rs = length cs\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set ms'. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # a # ms',s'); valid_node m; CFG_node m' \<in> sum_SDG_slice1 nx; nx \<in> S; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); ms = targetnodes rs; valid_return_list rs m; length rs = length cs\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (a # ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
from \<open>S,kind \<turnstile> (m#ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')\<close> \<open>valid_node m\<close>
    \<open>CFG_node m' \<in> sum_SDG_slice1 nx\<close>
    \<open>\<forall>mx \<in> set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>
    \<open>\<forall>i < length rs. rs!i \<in> get_return_edges (cs!i)\<close> \<open>ms = targetnodes rs\<close>
    \<open>valid_return_list rs m\<close> \<open>length rs = length cs\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')
valid_node m
CFG_node m' \<in> sum_SDG_slice1 nx
\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
ms = targetnodes rs
valid_return_list rs m
length rs = length cs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')
valid_node m
CFG_node m' \<in> sum_SDG_slice1 nx
\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
ms = targetnodes rs
valid_return_list rs m
length rs = length cs

goal (1 subgoal):
 1. \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
proof(rule silent_moves_called_node_in_slice1_hd_nodestack_in_slice1)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>as' a as''. \<lbrakk>as = as' @ a # as''; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; call_of_return_node (hd (mx # msx)) (sourcenode a); targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'; CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
 2. mx # msx = ms \<Longrightarrow> \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
fix as' a as''
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>as' a as''. \<lbrakk>as = as' @ a # as''; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; call_of_return_node (hd (mx # msx)) (sourcenode a); targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'; CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
 2. mx # msx = ms \<Longrightarrow> \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
assume "as = as'@a#as''" and "\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs"
      and "call_of_return_node (hd (mx # msx)) (sourcenode a)"
      and "CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx"
      and "targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'"
[PROOF STATE]
proof (state)
this:
as = as' @ a # as''
\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
call_of_return_node (hd (mx # msx)) (sourcenode a)
CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx
targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'

goal (2 subgoals):
 1. \<And>as' a as''. \<lbrakk>as = as' @ a # as''; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; call_of_return_node (hd (mx # msx)) (sourcenode a); targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'; CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
 2. mx # msx = ms \<Longrightarrow> \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
from \<open>CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx\<close> \<open>nx \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx
nx \<in> S
[PROOF STEP]
have "sourcenode a \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
[PROOF STATE]
proof (prove)
using this:
CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx
nx \<in> S

goal (1 subgoal):
 1. sourcenode a \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
by(fastforce intro:combSlice_refl simp:SDG_to_CFG_set_def HRB_slice_def)
[PROOF STATE]
proof (state)
this:
sourcenode a \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (2 subgoals):
 1. \<And>as' a as''. \<lbrakk>as = as' @ a # as''; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; call_of_return_node (hd (mx # msx)) (sourcenode a); targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'; CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
 2. mx # msx = ms \<Longrightarrow> \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
from \<open>S,kind \<turnstile> (m#ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')\<close> \<open>as = as'@a#as''\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')
as = as' @ a # as''
[PROOF STEP]
obtain xs x where "S,kind \<turnstile> (m#ms,s) =as'\<Rightarrow>\<^sub>\<tau> (xs,x)"
      and "S,kind \<turnstile> (xs,x) =a#as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')
as = as' @ a # as''

goal (1 subgoal):
 1. (\<And>xs x. \<lbrakk>S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (xs,x); S,kind \<turnstile> (xs,x) =a # as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:silent_moves_split)
[PROOF STATE]
proof (state)
this:
S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (xs,x)
S,kind \<turnstile> (xs,x) =a # as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')

goal (2 subgoals):
 1. \<And>as' a as''. \<lbrakk>as = as' @ a # as''; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; call_of_return_node (hd (mx # msx)) (sourcenode a); targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'; CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
 2. mx # msx = ms \<Longrightarrow> \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
from \<open>S,kind \<turnstile> (xs,x) =a#as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (xs,x) =a # as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')
[PROOF STEP]
obtain ys y where "S,kind \<turnstile> (xs,x) -a\<rightarrow>\<^sub>\<tau> (ys,y)"
      and "S,kind \<turnstile> (ys,y) =as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (xs,x) =a # as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')

goal (1 subgoal):
 1. (\<And>ys y. \<lbrakk>S,kind \<turnstile> (xs,x) -a\<rightarrow>\<^sub>\<tau> (ys,y); S,kind \<turnstile> (ys,y) =as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:silent_moves.cases)
[PROOF STATE]
proof (state)
this:
S,kind \<turnstile> (xs,x) -a\<rightarrow>\<^sub>\<tau> (ys,y)
S,kind \<turnstile> (ys,y) =as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')

goal (2 subgoals):
 1. \<And>as' a as''. \<lbrakk>as = as' @ a # as''; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; call_of_return_node (hd (mx # msx)) (sourcenode a); targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'; CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
 2. mx # msx = ms \<Longrightarrow> \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
from \<open>S,kind \<turnstile> (xs,x) -a\<rightarrow>\<^sub>\<tau> (ys,y)\<close> \<open>\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (xs,x) -a\<rightarrow>\<^sub>\<tau> (ys,y)
\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
obtain xs' a' where "xs = sourcenode a#xs'"
      and "ys = targetnode a#targetnode a'#xs'"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (xs,x) -a\<rightarrow>\<^sub>\<tau> (ys,y)
\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. (\<And>xs' a'. \<lbrakk>xs = sourcenode a # xs'; ys = targetnode a # targetnode a' # xs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>xs' a'. \<lbrakk>xs = sourcenode a # xs'; ys = targetnode a # targetnode a' # xs'\<rbrakk> \<Longrightarrow> thesis; S,kind \<turnstile> (xs,x) -a\<rightarrow>\<^sub>\<tau> (ys,y); \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(erule silent_move.cases)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>f aa s s' ms Sa ms'. \<lbrakk>\<And>xs' a'. \<lbrakk>xs = sourcenode a # xs'; ys = targetnode a # targetnode a' # xs'\<rbrakk> \<Longrightarrow> thesis; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; S = Sa; kind = f; xs = ms; x = s; a = aa; ys = ms'; y = s'; pred (f aa) s; transfer (f aa) s = s'; valid_edge aa; intra_kind (kind aa); (\<exists>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice Sa\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice Sa\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length s' = length s; length ms = length s; hd ms = sourcenode aa; ms' = targetnode aa # tl ms\<rbrakk> \<Longrightarrow> thesis
 2. \<And>f aa s s' Q r p fs a' ms Sa ms'. \<lbrakk>\<And>xs' a'. \<lbrakk>xs = sourcenode a # xs'; ys = targetnode a # targetnode a' # xs'\<rbrakk> \<Longrightarrow> thesis; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; S = Sa; kind = f; xs = ms; x = s; a = aa; ys = ms'; y = s'; pred (f aa) s; transfer (f aa) s = s'; valid_edge aa; kind aa = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges aa; (\<exists>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice Sa\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice Sa\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s' = Suc (length s); hd ms = sourcenode aa; ms' = targetnode aa # targetnode a' # tl ms\<rbrakk> \<Longrightarrow> thesis
 3. \<And>f aa s s' Q p f' ms Sa ms'. \<lbrakk>\<And>xs' a'. \<lbrakk>xs = sourcenode a # xs'; ys = targetnode a # targetnode a' # xs'\<rbrakk> \<Longrightarrow> thesis; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; S = Sa; kind = f; xs = ms; x = s; a = aa; ys = ms'; y = s'; pred (f aa) s; transfer (f aa) s = s'; valid_edge aa; kind aa = 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 Sa\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode aa; hd (tl ms) = targetnode aa; ms' = tl ms\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(auto simp:intra_kind_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Q r p fs a' m m'. \<lbrakk>\<And>xs' a'a. \<lbrakk>xs = sourcenode a # xs'; targetnode a' = targetnode a'a\<rbrakk> \<Longrightarrow> thesis; ys = targetnode a # targetnode a' # tl xs; pred (Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) x; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; Ball (set (tl xs)) return_node; length xs = length x; length (transfer (Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) x) = Suc (length x); hd xs = sourcenode a; y = transfer (Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) x; m \<in> set (tl xs); call_of_return_node m m'; m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> thesis
 2. \<And>Q r p fs a'. \<lbrakk>\<And>xs' a'a. \<lbrakk>xs = sourcenode a # xs'; targetnode a' = targetnode a'a\<rbrakk> \<Longrightarrow> thesis; ys = targetnode a # targetnode a' # tl xs; pred (Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) x; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; Ball (set (tl xs)) return_node; length xs = length x; length (transfer (Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) x) = Suc (length x); hd xs = sourcenode a; y = transfer (Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) x; sourcenode a \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by(cases xs,auto)+
[PROOF STATE]
proof (state)
this:
xs = sourcenode a # xs'
ys = targetnode a # targetnode a' # xs'

goal (2 subgoals):
 1. \<And>as' a as''. \<lbrakk>as = as' @ a # as''; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; call_of_return_node (hd (mx # msx)) (sourcenode a); targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'; CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
 2. mx # msx = ms \<Longrightarrow> \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
from \<open>S,kind \<turnstile> (ys,y) =as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')\<close>
      \<open>ys = targetnode a#targetnode a'#xs'\<close> \<open>targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (ys,y) =as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')
ys = targetnode a # targetnode a' # xs'
targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'
[PROOF STEP]
have "mx = targetnode a'" and "xs' = msx"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (ys,y) =as''\<Rightarrow>\<^sub>\<tau> (m' # mx # msx,s')
ys = targetnode a # targetnode a' # xs'
targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'

goal (1 subgoal):
 1. mx = targetnode a' &&& xs' = msx
[PROOF STEP]
by(auto dest:silent_moves_same_level_path)
[PROOF STATE]
proof (state)
this:
mx = targetnode a'
xs' = msx

goal (2 subgoals):
 1. \<And>as' a as''. \<lbrakk>as = as' @ a # as''; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; call_of_return_node (hd (mx # msx)) (sourcenode a); targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'; CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
 2. mx # msx = ms \<Longrightarrow> \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
with \<open>xs = sourcenode a#xs'\<close> \<open>S,kind \<turnstile> (m#ms,s) =as'\<Rightarrow>\<^sub>\<tau> (xs,x)\<close>
[PROOF STATE]
proof (chain)
picking this:
xs = sourcenode a # xs'
S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (xs,x)
mx = targetnode a'
xs' = msx
[PROOF STEP]
have "S,kind \<turnstile> (m#ms,s) =as'\<Rightarrow>\<^sub>\<tau> (sourcenode a#msx,x)"
[PROOF STATE]
proof (prove)
using this:
xs = sourcenode a # xs'
S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (xs,x)
mx = targetnode a'
xs' = msx

goal (1 subgoal):
 1. S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (sourcenode a # msx,x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (sourcenode a # msx,x)

goal (2 subgoals):
 1. \<And>as' a as''. \<lbrakk>as = as' @ a # as''; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; call_of_return_node (hd (mx # msx)) (sourcenode a); targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'; CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
 2. mx # msx = ms \<Longrightarrow> \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
from IH[OF \<open>S,kind \<turnstile> (m#ms,s) =as'\<Rightarrow>\<^sub>\<tau> (sourcenode a#msx,x)\<close>
      \<open>valid_node m\<close> \<open>CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx\<close> \<open>nx \<in> S\<close>
      \<open>\<forall>mx \<in> set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>
      \<open>\<forall>i < length rs. rs!i \<in> get_return_edges (cs!i)\<close> \<open>ms = targetnodes rs\<close>
      \<open>valid_return_list rs m\<close> \<open>length rs = length cs\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<forall>mx\<in>set msx. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
have callstack:"\<forall>mx\<in>set msx.
      \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<forall>mx\<in>set msx. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. \<forall>mx\<in>set msx. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<forall>mx\<in>set msx. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (2 subgoals):
 1. \<And>as' a as''. \<lbrakk>as = as' @ a # as''; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; call_of_return_node (hd (mx # msx)) (sourcenode a); targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'; CFG_node (sourcenode a) \<in> sum_SDG_slice1 nx\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
 2. mx # msx = ms \<Longrightarrow> \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
with \<open>as = as'@a#as''\<close> \<open>call_of_return_node (hd (mx # msx)) (sourcenode a)\<close>
      \<open>sourcenode a \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
as = as' @ a # as''
call_of_return_node (hd (mx # msx)) (sourcenode a)
sourcenode a \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
\<forall>mx\<in>set msx. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
as = as' @ a # as''
call_of_return_node (hd (mx # msx)) (sourcenode a)
sourcenode a \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
\<forall>mx\<in>set msx. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. mx # msx = ms \<Longrightarrow> \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mx # msx = ms \<Longrightarrow> \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
assume "mx # msx = ms"
[PROOF STATE]
proof (state)
this:
mx # msx = ms

goal (1 subgoal):
 1. mx # msx = ms \<Longrightarrow> \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
with \<open>\<forall>mx \<in> set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
mx # msx = ms
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
mx # msx = ms

goal (1 subgoal):
 1. \<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>mx\<in>set (mx # msx). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. \<And>as m' s'. \<lbrakk>S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> ([m'],s'); valid_node m; CFG_node m' \<in> sum_SDG_slice1 nx; nx \<in> S; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); ms = targetnodes rs; valid_return_list rs m; length rs = length cs\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set []. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
qed simp


[STATEMENT]
lemma silent_moves_slice_intra_path:
  assumes "S,slice_kind S \<turnstile> (m#ms,s) =as\<Rightarrow>\<^sub>\<tau> (m'#ms',s')"
  and "\<forall>mx \<in> set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
  shows "\<forall>a \<in> set as. intra_kind (kind a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a\<in>set as. intra_kind (kind a)
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>a\<in>set as. intra_kind (kind a)) \<Longrightarrow> False
[PROOF STEP]
assume "\<not> (\<forall>a\<in>set as. intra_kind (kind a))"
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>a\<in>set as. intra_kind (kind a))

goal (1 subgoal):
 1. \<not> (\<forall>a\<in>set as. intra_kind (kind a)) \<Longrightarrow> False
[PROOF STEP]
hence "\<exists>a \<in> set as. \<not> intra_kind (kind a)"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>a\<in>set as. intra_kind (kind a))

goal (1 subgoal):
 1. \<exists>a\<in>set as. \<not> intra_kind (kind a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>a\<in>set as. \<not> intra_kind (kind a)

goal (1 subgoal):
 1. \<not> (\<forall>a\<in>set as. intra_kind (kind a)) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a\<in>set as. \<not> intra_kind (kind a)
[PROOF STEP]
obtain asx ax asx' where "as = asx@ax#asx'"
    and "\<forall>a\<in>set asx. intra_kind (kind a)" and "\<not> intra_kind (kind ax)"
[PROOF STATE]
proof (prove)
using this:
\<exists>a\<in>set as. \<not> intra_kind (kind a)

goal (1 subgoal):
 1. (\<And>asx ax asx'. \<lbrakk>as = asx @ ax # asx'; \<forall>a\<in>set asx. intra_kind (kind a); \<not> intra_kind (kind ax)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim!:split_list_first_propE)
[PROOF STATE]
proof (state)
this:
as = asx @ ax # asx'
\<forall>a\<in>set asx. intra_kind (kind a)
\<not> intra_kind (kind ax)

goal (1 subgoal):
 1. \<not> (\<forall>a\<in>set as. intra_kind (kind a)) \<Longrightarrow> False
[PROOF STEP]
from \<open>S,slice_kind S \<turnstile> (m#ms,s) =as\<Rightarrow>\<^sub>\<tau> (m'#ms',s')\<close> \<open>as = asx@ax#asx'\<close>
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
as = asx @ ax # asx'
[PROOF STEP]
obtain msx sx msx' sx' where "S,slice_kind S \<turnstile> (m#ms,s) =asx\<Rightarrow>\<^sub>\<tau> (msx,sx)"
    and "S,slice_kind S \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (msx',sx')"
    and "S,slice_kind S \<turnstile> (msx',sx') =asx'\<Rightarrow>\<^sub>\<tau> (m'#ms',s')"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
as = asx @ ax # asx'

goal (1 subgoal):
 1. (\<And>msx sx msx' sx'. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =asx\<Rightarrow>\<^sub>\<tau> (msx,sx); S,slice_kind S \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (msx',sx'); S,slice_kind S \<turnstile> (msx',sx') =asx'\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto elim!:silent_moves_split elim:silent_moves.cases)
[PROOF STATE]
proof (state)
this:
S,slice_kind S \<turnstile> (m # ms,s) =asx\<Rightarrow>\<^sub>\<tau> (msx,sx)
S,slice_kind S \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (msx',sx')
S,slice_kind S \<turnstile> (msx',sx') =asx'\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (1 subgoal):
 1. \<not> (\<forall>a\<in>set as. intra_kind (kind a)) \<Longrightarrow> False
[PROOF STEP]
from \<open>S,slice_kind S \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (msx',sx')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (msx',sx')
[PROOF STEP]
obtain xs
    where [simp]:"msx = sourcenode ax#xs"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (msx',sx')

goal (1 subgoal):
 1. (\<And>xs. msx = sourcenode ax # xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases msx)(auto elim:silent_move.cases)
[PROOF STATE]
proof (state)
this:
msx = sourcenode ax # xs

goal (1 subgoal):
 1. \<not> (\<forall>a\<in>set as. intra_kind (kind a)) \<Longrightarrow> False
[PROOF STEP]
from \<open>S,slice_kind S \<turnstile> (m#ms,s) =asx\<Rightarrow>\<^sub>\<tau> (msx,sx)\<close> \<open>\<forall>a\<in>set asx. intra_kind (kind a)\<close>
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (m # ms,s) =asx\<Rightarrow>\<^sub>\<tau> (msx,sx)
\<forall>a\<in>set asx. intra_kind (kind a)
[PROOF STEP]
have [simp]:"xs = ms"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (m # ms,s) =asx\<Rightarrow>\<^sub>\<tau> (msx,sx)
\<forall>a\<in>set asx. intra_kind (kind a)

goal (1 subgoal):
 1. xs = ms
[PROOF STEP]
by(fastforce dest:silent_moves_intra_path)
[PROOF STATE]
proof (state)
this:
xs = ms

goal (1 subgoal):
 1. \<not> (\<forall>a\<in>set as. intra_kind (kind a)) \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof(cases "kind ax" rule:edge_kind_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. intra_kind (kind ax) \<Longrightarrow> False
 2. \<And>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> False
 3. \<And>Q p f. kind ax = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> False
[PROOF STEP]
case Intra
[PROOF STATE]
proof (state)
this:
intra_kind (kind ax)

goal (3 subgoals):
 1. intra_kind (kind ax) \<Longrightarrow> False
 2. \<And>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> False
 3. \<And>Q p f. kind ax = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> False
[PROOF STEP]
with \<open>\<not> intra_kind (kind ax)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> intra_kind (kind ax)
intra_kind (kind ax)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> intra_kind (kind ax)
intra_kind (kind ax)

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

goal (2 subgoals):
 1. \<And>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> False
 2. \<And>Q p f. kind ax = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> False
 2. \<And>Q p f. kind ax = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> False
[PROOF STEP]
case (Call Q r p fs)
[PROOF STATE]
proof (state)
this:
kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (2 subgoals):
 1. \<And>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> False
 2. \<And>Q p f. kind ax = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> False
[PROOF STEP]
with \<open>S,slice_kind S \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (msx',sx')\<close>
      \<open>\<forall>mx \<in> set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (msx',sx')
\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
have "sourcenode ax \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>" and "pred (slice_kind S ax) sx"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (msx',sx')
\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. sourcenode ax \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> &&& pred (slice_kind S ax) sx
[PROOF STEP]
by(auto elim!:silent_move.cases simp:intra_kind_def)
[PROOF STATE]
proof (state)
this:
sourcenode ax \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
pred (slice_kind S ax) sx

goal (2 subgoals):
 1. \<And>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> False
 2. \<And>Q p f. kind ax = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> False
[PROOF STEP]
from \<open>sourcenode ax \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close> \<open>kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode ax \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
have "slice_kind S ax = (\<lambda>cf. False):r\<hookrightarrow>\<^bsub>p\<^esub>fs"
[PROOF STATE]
proof (prove)
using this:
sourcenode ax \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. slice_kind S ax = \<lambda>cf. False:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
by(rule slice_kind_Call)
[PROOF STATE]
proof (state)
this:
slice_kind S ax = \<lambda>cf. False:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (2 subgoals):
 1. \<And>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> False
 2. \<And>Q p f. kind ax = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> False
[PROOF STEP]
with \<open>pred (slice_kind S ax) sx\<close>
[PROOF STATE]
proof (chain)
picking this:
pred (slice_kind S ax) sx
slice_kind S ax = \<lambda>cf. False:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
pred (slice_kind S ax) sx
slice_kind S ax = \<lambda>cf. False:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. False
[PROOF STEP]
by(cases sx) auto
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<And>Q p f. kind ax = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q p f. kind ax = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> False
[PROOF STEP]
case (Return Q p f)
[PROOF STATE]
proof (state)
this:
kind ax = Q\<hookleftarrow>\<^bsub>p\<^esub>f

goal (1 subgoal):
 1. \<And>Q p f. kind ax = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> False
[PROOF STEP]
with \<open>S,slice_kind S \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (msx',sx')\<close>
      \<open>\<forall>mx \<in> set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (msx',sx')
\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
kind ax = Q\<hookleftarrow>\<^bsub>p\<^esub>f
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (msx',sx')
\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
kind ax = Q\<hookleftarrow>\<^bsub>p\<^esub>f

goal (1 subgoal):
 1. False
[PROOF STEP]
by(fastforce elim!:silent_move.cases simp:intra_kind_def)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma silent_moves_slice_keeps_state:
  assumes "S,slice_kind S \<turnstile> (m#ms,s) =as\<Rightarrow>\<^sub>\<tau> (m'#ms',s')"
  and "\<forall>mx \<in> set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
  shows "s = s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = s'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s = s'
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
have "\<forall>a \<in> set as. intra_kind (kind a)"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. \<forall>a\<in>set as. intra_kind (kind a)
[PROOF STEP]
by(rule silent_moves_slice_intra_path)
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set as. intra_kind (kind a)

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
\<forall>a\<in>set as. intra_kind (kind a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
\<forall>a\<in>set as. intra_kind (kind a)

goal (1 subgoal):
 1. s = s'
[PROOF STEP]
proof(induct S "slice_kind S" "m#ms" s as "m'#ms'" s'
        arbitrary:m rule:silent_moves.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s S. \<lbrakk>length (m' # ms) = length s; ms = ms'; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set []. intra_kind (kind a)\<rbrakk> \<Longrightarrow> s = s
 2. \<And>S s a ms'a s' as s'' m. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s''); \<And>m. \<lbrakk>ms'a = m # ms; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set as. intra_kind (kind a)\<rbrakk> \<Longrightarrow> s' = s''; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set (a # as). intra_kind (kind a)\<rbrakk> \<Longrightarrow> s = s''
[PROOF STEP]
case (silent_moves_Nil sx n\<^sub>c)
[PROOF STATE]
proof (state)
this:
length (m' # ms) = length sx
ms = ms'
\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice n\<^sub>c\<rfloor>\<^bsub>CFG\<^esub>
\<forall>a\<in>set []. intra_kind (kind a)

goal (2 subgoals):
 1. \<And>s S. \<lbrakk>length (m' # ms) = length s; ms = ms'; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set []. intra_kind (kind a)\<rbrakk> \<Longrightarrow> s = s
 2. \<And>S s a ms'a s' as s'' m. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s''); \<And>m. \<lbrakk>ms'a = m # ms; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set as. intra_kind (kind a)\<rbrakk> \<Longrightarrow> s' = s''; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set (a # as). intra_kind (kind a)\<rbrakk> \<Longrightarrow> s = s''
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
length (m' # ms) = length sx
ms = ms'
\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice n\<^sub>c\<rfloor>\<^bsub>CFG\<^esub>
\<forall>a\<in>set []. intra_kind (kind a)

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

goal (1 subgoal):
 1. \<And>S s a ms'a s' as s'' m. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s''); \<And>m. \<lbrakk>ms'a = m # ms; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set as. intra_kind (kind a)\<rbrakk> \<Longrightarrow> s' = s''; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set (a # as). intra_kind (kind a)\<rbrakk> \<Longrightarrow> s = s''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S s a ms'a s' as s'' m. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s''); \<And>m. \<lbrakk>ms'a = m # ms; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set as. intra_kind (kind a)\<rbrakk> \<Longrightarrow> s' = s''; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set (a # as). intra_kind (kind a)\<rbrakk> \<Longrightarrow> s = s''
[PROOF STEP]
case (silent_moves_Cons S sx a msx' sx' as s'')
[PROOF STATE]
proof (state)
this:
S,slice_kind S \<turnstile> (m # ms,sx) -a\<rightarrow>\<^sub>\<tau> (msx',sx')
S,slice_kind S \<turnstile> (msx',sx') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'')
\<lbrakk>msx' = ?m # ms; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set as. intra_kind (kind a)\<rbrakk> \<Longrightarrow> sx' = s''
\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
\<forall>a\<in>set (a # as). intra_kind (kind a)

goal (1 subgoal):
 1. \<And>S s a ms'a s' as s'' m. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s''); \<And>m. \<lbrakk>ms'a = m # ms; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set as. intra_kind (kind a)\<rbrakk> \<Longrightarrow> s' = s''; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set (a # as). intra_kind (kind a)\<rbrakk> \<Longrightarrow> s = s''
[PROOF STEP]
note IH = \<open>\<And>m.
      \<lbrakk>msx' = m # ms;
      \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>;
      \<forall>a\<in>set as. intra_kind (kind a)\<rbrakk> \<Longrightarrow> sx' = s''\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>msx' = ?m # ms; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set as. intra_kind (kind a)\<rbrakk> \<Longrightarrow> sx' = s''

goal (1 subgoal):
 1. \<And>S s a ms'a s' as s'' m. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s''); \<And>m. \<lbrakk>ms'a = m # ms; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set as. intra_kind (kind a)\<rbrakk> \<Longrightarrow> s' = s''; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set (a # as). intra_kind (kind a)\<rbrakk> \<Longrightarrow> s = s''
[PROOF STEP]
note callstack = \<open>\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and>
      mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>
[PROOF STATE]
proof (state)
this:
\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. \<And>S s a ms'a s' as s'' m. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s''); \<And>m. \<lbrakk>ms'a = m # ms; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set as. intra_kind (kind a)\<rbrakk> \<Longrightarrow> s' = s''; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set (a # as). intra_kind (kind a)\<rbrakk> \<Longrightarrow> s = s''
[PROOF STEP]
from \<open>\<forall>a\<in>set (a # as). intra_kind (kind a)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>set (a # as). intra_kind (kind a)
[PROOF STEP]
have "intra_kind (kind a)"
      and "\<forall>a\<in>set as. intra_kind (kind a)"
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set (a # as). intra_kind (kind a)

goal (1 subgoal):
 1. intra_kind (kind a) &&& \<forall>a\<in>set as. intra_kind (kind a)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
intra_kind (kind a)
\<forall>a\<in>set as. intra_kind (kind a)

goal (1 subgoal):
 1. \<And>S s a ms'a s' as s'' m. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s''); \<And>m. \<lbrakk>ms'a = m # ms; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set as. intra_kind (kind a)\<rbrakk> \<Longrightarrow> s' = s''; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set (a # as). intra_kind (kind a)\<rbrakk> \<Longrightarrow> s = s''
[PROOF STEP]
from \<open>S,slice_kind S \<turnstile> (m # ms,sx) -a\<rightarrow>\<^sub>\<tau> (msx',sx')\<close> \<open>intra_kind (kind a)\<close>
      callstack
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (m # ms,sx) -a\<rightarrow>\<^sub>\<tau> (msx',sx')
intra_kind (kind a)
\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
have [simp]:"msx' = targetnode a#ms" and "sx' = transfer (slice_kind S a) sx"
      and "sourcenode a \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>" and "valid_edge a" and "sx \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (m # ms,sx) -a\<rightarrow>\<^sub>\<tau> (msx',sx')
intra_kind (kind a)
\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. (msx' = targetnode a # ms &&& sx' = transfer (slice_kind S a) sx) &&& sourcenode a \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> &&& valid_edge a &&& sx \<noteq> []
[PROOF STEP]
by(auto elim!:silent_move.cases simp:intra_kind_def)
[PROOF STATE]
proof (state)
this:
msx' = targetnode a # ms
sx' = transfer (slice_kind S a) sx
sourcenode a \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
valid_edge a
sx \<noteq> []

goal (1 subgoal):
 1. \<And>S s a ms'a s' as s'' m. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s''); \<And>m. \<lbrakk>ms'a = m # ms; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set as. intra_kind (kind a)\<rbrakk> \<Longrightarrow> s' = s''; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set (a # as). intra_kind (kind a)\<rbrakk> \<Longrightarrow> s = s''
[PROOF STEP]
from IH[OF \<open>msx' = targetnode a#ms\<close> callstack \<open>\<forall>a\<in>set as. intra_kind (kind a)\<close>]
[PROOF STATE]
proof (chain)
picking this:
sx' = s''
[PROOF STEP]
have "sx' = s''"
[PROOF STATE]
proof (prove)
using this:
sx' = s''

goal (1 subgoal):
 1. sx' = s''
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sx' = s''

goal (1 subgoal):
 1. \<And>S s a ms'a s' as s'' m. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s''); \<And>m. \<lbrakk>ms'a = m # ms; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set as. intra_kind (kind a)\<rbrakk> \<Longrightarrow> s' = s''; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set (a # as). intra_kind (kind a)\<rbrakk> \<Longrightarrow> s = s''
[PROOF STEP]
from \<open>intra_kind (kind a)\<close>
[PROOF STATE]
proof (chain)
picking this:
intra_kind (kind a)
[PROOF STEP]
have "sx = sx'"
[PROOF STATE]
proof (prove)
using this:
intra_kind (kind a)

goal (1 subgoal):
 1. sx = sx'
[PROOF STEP]
proof(cases "kind a")
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1. \<lbrakk>intra_kind (kind a); kind a = \<Up>x1\<rbrakk> \<Longrightarrow> sx = sx'
 2. \<And>x2. \<lbrakk>intra_kind (kind a); kind a = (x2)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> sx = sx'
 3. \<And>x31 x32 x33 x34. \<lbrakk>intra_kind (kind a); kind a = x31:x32\<hookrightarrow>\<^bsub>x33\<^esub>x34\<rbrakk> \<Longrightarrow> sx = sx'
 4. \<And>x41 x42 x43. \<lbrakk>intra_kind (kind a); kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43\<rbrakk> \<Longrightarrow> sx = sx'
[PROOF STEP]
case (UpdateEdge f')
[PROOF STATE]
proof (state)
this:
kind a = \<Up>f'

goal (4 subgoals):
 1. \<And>x1. \<lbrakk>intra_kind (kind a); kind a = \<Up>x1\<rbrakk> \<Longrightarrow> sx = sx'
 2. \<And>x2. \<lbrakk>intra_kind (kind a); kind a = (x2)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> sx = sx'
 3. \<And>x31 x32 x33 x34. \<lbrakk>intra_kind (kind a); kind a = x31:x32\<hookrightarrow>\<^bsub>x33\<^esub>x34\<rbrakk> \<Longrightarrow> sx = sx'
 4. \<And>x41 x42 x43. \<lbrakk>intra_kind (kind a); kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43\<rbrakk> \<Longrightarrow> sx = sx'
[PROOF STEP]
with \<open>sourcenode a \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode a \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
kind a = \<Up>f'
[PROOF STEP]
have "slice_kind S a = \<Up>id"
[PROOF STATE]
proof (prove)
using this:
sourcenode a \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
kind a = \<Up>f'

goal (1 subgoal):
 1. slice_kind S a = \<Up>id
[PROOF STEP]
by(rule slice_kind_Upd)
[PROOF STATE]
proof (state)
this:
slice_kind S a = \<Up>id

goal (4 subgoals):
 1. \<And>x1. \<lbrakk>intra_kind (kind a); kind a = \<Up>x1\<rbrakk> \<Longrightarrow> sx = sx'
 2. \<And>x2. \<lbrakk>intra_kind (kind a); kind a = (x2)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> sx = sx'
 3. \<And>x31 x32 x33 x34. \<lbrakk>intra_kind (kind a); kind a = x31:x32\<hookrightarrow>\<^bsub>x33\<^esub>x34\<rbrakk> \<Longrightarrow> sx = sx'
 4. \<And>x41 x42 x43. \<lbrakk>intra_kind (kind a); kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43\<rbrakk> \<Longrightarrow> sx = sx'
[PROOF STEP]
with \<open>sx' = transfer (slice_kind S a) sx\<close> \<open>sx \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
sx' = transfer (slice_kind S a) sx
sx \<noteq> []
slice_kind S a = \<Up>id
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sx' = transfer (slice_kind S a) sx
sx \<noteq> []
slice_kind S a = \<Up>id

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

goal (3 subgoals):
 1. \<And>x2. \<lbrakk>intra_kind (kind a); kind a = (x2)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> sx = sx'
 2. \<And>x31 x32 x33 x34. \<lbrakk>intra_kind (kind a); kind a = x31:x32\<hookrightarrow>\<^bsub>x33\<^esub>x34\<rbrakk> \<Longrightarrow> sx = sx'
 3. \<And>x41 x42 x43. \<lbrakk>intra_kind (kind a); kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43\<rbrakk> \<Longrightarrow> sx = sx'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>intra_kind (kind a); kind a = (x2)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> sx = sx'
 2. \<And>x31 x32 x33 x34. \<lbrakk>intra_kind (kind a); kind a = x31:x32\<hookrightarrow>\<^bsub>x33\<^esub>x34\<rbrakk> \<Longrightarrow> sx = sx'
 3. \<And>x41 x42 x43. \<lbrakk>intra_kind (kind a); kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43\<rbrakk> \<Longrightarrow> sx = sx'
[PROOF STEP]
case (PredicateEdge Q)
[PROOF STATE]
proof (state)
this:
kind a = (Q)\<^sub>\<surd>

goal (3 subgoals):
 1. \<And>x2. \<lbrakk>intra_kind (kind a); kind a = (x2)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> sx = sx'
 2. \<And>x31 x32 x33 x34. \<lbrakk>intra_kind (kind a); kind a = x31:x32\<hookrightarrow>\<^bsub>x33\<^esub>x34\<rbrakk> \<Longrightarrow> sx = sx'
 3. \<And>x41 x42 x43. \<lbrakk>intra_kind (kind a); kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43\<rbrakk> \<Longrightarrow> sx = sx'
[PROOF STEP]
with \<open>sourcenode a \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close> \<open>valid_edge a\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode a \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
valid_edge a
kind a = (Q)\<^sub>\<surd>
[PROOF STEP]
obtain Q' where "slice_kind S a = (Q')\<^sub>\<surd>"
[PROOF STATE]
proof (prove)
using this:
sourcenode a \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
valid_edge a
kind a = (Q)\<^sub>\<surd>

goal (1 subgoal):
 1. (\<And>Q'. slice_kind S a = (Q')\<^sub>\<surd> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by -(erule kind_Predicate_notin_slice_slice_kind_Predicate)
[PROOF STATE]
proof (state)
this:
slice_kind S a = (Q')\<^sub>\<surd>

goal (3 subgoals):
 1. \<And>x2. \<lbrakk>intra_kind (kind a); kind a = (x2)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> sx = sx'
 2. \<And>x31 x32 x33 x34. \<lbrakk>intra_kind (kind a); kind a = x31:x32\<hookrightarrow>\<^bsub>x33\<^esub>x34\<rbrakk> \<Longrightarrow> sx = sx'
 3. \<And>x41 x42 x43. \<lbrakk>intra_kind (kind a); kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43\<rbrakk> \<Longrightarrow> sx = sx'
[PROOF STEP]
with \<open>sx' = transfer (slice_kind S a) sx\<close> \<open>sx \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
sx' = transfer (slice_kind S a) sx
sx \<noteq> []
slice_kind S a = (Q')\<^sub>\<surd>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sx' = transfer (slice_kind S a) sx
sx \<noteq> []
slice_kind S a = (Q')\<^sub>\<surd>

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

goal (2 subgoals):
 1. \<And>x31 x32 x33 x34. \<lbrakk>intra_kind (kind a); kind a = x31:x32\<hookrightarrow>\<^bsub>x33\<^esub>x34\<rbrakk> \<Longrightarrow> sx = sx'
 2. \<And>x41 x42 x43. \<lbrakk>intra_kind (kind a); kind a = x41\<hookleftarrow>\<^bsub>x42\<^esub>x43\<rbrakk> \<Longrightarrow> sx = sx'
[PROOF STEP]
qed (auto simp:intra_kind_def)
[PROOF STATE]
proof (state)
this:
sx = sx'

goal (1 subgoal):
 1. \<And>S s a ms'a s' as s'' m. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s''); \<And>m. \<lbrakk>ms'a = m # ms; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set as. intra_kind (kind a)\<rbrakk> \<Longrightarrow> s' = s''; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>a\<in>set (a # as). intra_kind (kind a)\<rbrakk> \<Longrightarrow> s = s''
[PROOF STEP]
with \<open>sx' = s''\<close>
[PROOF STATE]
proof (chain)
picking this:
sx' = s''
sx = sx'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sx' = s''
sx = sx'

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s = s'

goal:
No subgoals!
[PROOF STEP]
qed