[STATEMENT]
lemma slice_tom_preds_vp:
  assumes "S,slice_kind S \<turnstile> (m#ms,s) =as\<Rightarrow>* (m'#ms',s')" and "valid_node m"
  and "valid_call_list cs m" and "\<forall>i < length rs. rs!i \<in> get_return_edges (cs!i)"
  and "valid_return_list rs m" and "length rs = length cs" and "ms = targetnodes rs"
  and "\<forall>mx \<in> set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
  obtains as' cs' rs' where "preds (slice_kinds S as') s"
  and "slice_edges S cs as' = as" and "m -as'\<rightarrow>* m'" and "valid_path_aux cs as'"
  and "upd_cs cs as' = cs'" and "valid_node m'" and "valid_call_list cs' m'"
  and "\<forall>i < length rs'. rs'!i \<in> get_return_edges (cs'!i)"
  and "valid_return_list rs' m'" and "length rs' = length cs'"
  and "ms' = targetnodes rs'" and "transfers (slice_kinds S as') s \<noteq> []"
  and "transfers (slice_kinds S (slice_edges S cs as')) s =
    transfers (slice_kinds S as') s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>as' cs' rs'. \<lbrakk>preds (slice_kinds S as') s; slice_edges S cs as' = as; m -as'\<rightarrow>* m'; valid_path_aux cs as'; upd_cs cs as' = cs'; valid_node m'; valid_call_list cs' m'; \<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i); valid_return_list rs' m'; length rs' = length cs'; ms' = targetnodes rs'; transfers (slice_kinds S as') s \<noteq> []; transfers (slice_kinds S (slice_edges S cs as')) s = transfers (slice_kinds S as') s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>as' cs' rs'. preds (slice_kinds S as') s \<and> slice_edges S cs as' = as \<and> m -as'\<rightarrow>* m' \<and> valid_path_aux cs as' \<and> upd_cs cs as' = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as') s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as')) s = transfers (slice_kinds S as') s
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow>* (m' # ms',s')
valid_node m
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs
\<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]
show "\<exists>as' cs' rs'. preds (slice_kinds S as') s \<and>
    slice_edges S cs as' = as \<and> m -as'\<rightarrow>* m' \<and> valid_path_aux cs as' \<and>
    upd_cs cs as' = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and>
    (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and>
    length rs' = length cs' \<and> ms' = targetnodes rs' \<and>
    transfers (slice_kinds S as') s \<noteq> [] \<and>
    transfers (slice_kinds S (slice_edges S cs as')) s =
    transfers (slice_kinds S as') s"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow>* (m' # ms',s')
valid_node m
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs
\<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. \<exists>as' cs' rs'. preds (slice_kinds S as') s \<and> slice_edges S cs as' = as \<and> m -as'\<rightarrow>* m' \<and> valid_path_aux cs as' \<and> upd_cs cs as' = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as') s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as')) s = transfers (slice_kinds S as') s
[PROOF STEP]
proof(induct S "slice_kind S" "m#ms" s as "m'#ms'" s'
    arbitrary:m ms cs rs rule:trans_observable_moves.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s S cs rs. \<lbrakk>length (m' # ms') = length s; valid_node m'; valid_call_list cs m'; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m'; length rs = length cs; ms' = targetnodes rs; \<forall>mx\<in>set ms'. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as' cs' rs'. preds (slice_kinds S as') s \<and> slice_edges S cs as' = [] \<and> m' -as'\<rightarrow>* m' \<and> valid_path_aux cs as' \<and> upd_cs cs as' = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as') s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as')) s = transfers (slice_kinds S as') s
 2. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
case (tom_Nil s n\<^sub>c)
[PROOF STATE]
proof (state)
this:
length (m' # ms') = length s
valid_node m'
valid_call_list cs m'
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m'
length rs = length cs
ms' = targetnodes rs
\<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>

goal (2 subgoals):
 1. \<And>s S cs rs. \<lbrakk>length (m' # ms') = length s; valid_node m'; valid_call_list cs m'; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m'; length rs = length cs; ms' = targetnodes rs; \<forall>mx\<in>set ms'. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as' cs' rs'. preds (slice_kinds S as') s \<and> slice_edges S cs as' = [] \<and> m' -as'\<rightarrow>* m' \<and> valid_path_aux cs as' \<and> upd_cs cs as' = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as') s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as')) s = transfers (slice_kinds S as') s
 2. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from \<open>length (m' # ms') = length s\<close>
[PROOF STATE]
proof (chain)
picking this:
length (m' # ms') = length s
[PROOF STEP]
have "s \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
length (m' # ms') = length s

goal (1 subgoal):
 1. s \<noteq> []
[PROOF STEP]
by(cases s) auto
[PROOF STATE]
proof (state)
this:
s \<noteq> []

goal (2 subgoals):
 1. \<And>s S cs rs. \<lbrakk>length (m' # ms') = length s; valid_node m'; valid_call_list cs m'; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m'; length rs = length cs; ms' = targetnodes rs; \<forall>mx\<in>set ms'. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as' cs' rs'. preds (slice_kinds S as') s \<and> slice_edges S cs as' = [] \<and> m' -as'\<rightarrow>* m' \<and> valid_path_aux cs as' \<and> upd_cs cs as' = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as') s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as')) s = transfers (slice_kinds S as') s
 2. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
have "preds (slice_kinds S []) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. preds (slice_kinds S []) s
[PROOF STEP]
by(fastforce simp:slice_kinds_def)
[PROOF STATE]
proof (state)
this:
preds (slice_kinds S []) s

goal (2 subgoals):
 1. \<And>s S cs rs. \<lbrakk>length (m' # ms') = length s; valid_node m'; valid_call_list cs m'; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m'; length rs = length cs; ms' = targetnodes rs; \<forall>mx\<in>set ms'. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as' cs' rs'. preds (slice_kinds S as') s \<and> slice_edges S cs as' = [] \<and> m' -as'\<rightarrow>* m' \<and> valid_path_aux cs as' \<and> upd_cs cs as' = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as') s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as')) s = transfers (slice_kinds S as') s
 2. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
preds (slice_kinds S []) s

goal (2 subgoals):
 1. \<And>s S cs rs. \<lbrakk>length (m' # ms') = length s; valid_node m'; valid_call_list cs m'; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m'; length rs = length cs; ms' = targetnodes rs; \<forall>mx\<in>set ms'. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as' cs' rs'. preds (slice_kinds S as') s \<and> slice_edges S cs as' = [] \<and> m' -as'\<rightarrow>* m' \<and> valid_path_aux cs as' \<and> upd_cs cs as' = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as') s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as')) s = transfers (slice_kinds S as') s
 2. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
have "slice_edges S cs [] = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. slice_edges S cs [] = []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
slice_edges S cs [] = []

goal (2 subgoals):
 1. \<And>s S cs rs. \<lbrakk>length (m' # ms') = length s; valid_node m'; valid_call_list cs m'; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m'; length rs = length cs; ms' = targetnodes rs; \<forall>mx\<in>set ms'. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as' cs' rs'. preds (slice_kinds S as') s \<and> slice_edges S cs as' = [] \<and> m' -as'\<rightarrow>* m' \<and> valid_path_aux cs as' \<and> upd_cs cs as' = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as') s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as')) s = transfers (slice_kinds S as') s
 2. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
slice_edges S cs [] = []

goal (2 subgoals):
 1. \<And>s S cs rs. \<lbrakk>length (m' # ms') = length s; valid_node m'; valid_call_list cs m'; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m'; length rs = length cs; ms' = targetnodes rs; \<forall>mx\<in>set ms'. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as' cs' rs'. preds (slice_kinds S as') s \<and> slice_edges S cs as' = [] \<and> m' -as'\<rightarrow>* m' \<and> valid_path_aux cs as' \<and> upd_cs cs as' = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as') s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as')) s = transfers (slice_kinds S as') s
 2. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from \<open>valid_node m'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_node m'
[PROOF STEP]
have "m' -[]\<rightarrow>* m'"
[PROOF STATE]
proof (prove)
using this:
valid_node m'

goal (1 subgoal):
 1. m' -[]\<rightarrow>* m'
[PROOF STEP]
by(fastforce intro:empty_path)
[PROOF STATE]
proof (state)
this:
m' -[]\<rightarrow>* m'

goal (2 subgoals):
 1. \<And>s S cs rs. \<lbrakk>length (m' # ms') = length s; valid_node m'; valid_call_list cs m'; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m'; length rs = length cs; ms' = targetnodes rs; \<forall>mx\<in>set ms'. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as' cs' rs'. preds (slice_kinds S as') s \<and> slice_edges S cs as' = [] \<and> m' -as'\<rightarrow>* m' \<and> valid_path_aux cs as' \<and> upd_cs cs as' = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as') s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as')) s = transfers (slice_kinds S as') s
 2. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
m' -[]\<rightarrow>* m'

goal (2 subgoals):
 1. \<And>s S cs rs. \<lbrakk>length (m' # ms') = length s; valid_node m'; valid_call_list cs m'; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m'; length rs = length cs; ms' = targetnodes rs; \<forall>mx\<in>set ms'. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as' cs' rs'. preds (slice_kinds S as') s \<and> slice_edges S cs as' = [] \<and> m' -as'\<rightarrow>* m' \<and> valid_path_aux cs as' \<and> upd_cs cs as' = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as') s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as')) s = transfers (slice_kinds S as') s
 2. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
have "valid_path_aux cs []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_path_aux cs []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
valid_path_aux cs []

goal (2 subgoals):
 1. \<And>s S cs rs. \<lbrakk>length (m' # ms') = length s; valid_node m'; valid_call_list cs m'; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m'; length rs = length cs; ms' = targetnodes rs; \<forall>mx\<in>set ms'. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as' cs' rs'. preds (slice_kinds S as') s \<and> slice_edges S cs as' = [] \<and> m' -as'\<rightarrow>* m' \<and> valid_path_aux cs as' \<and> upd_cs cs as' = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as') s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as')) s = transfers (slice_kinds S as') s
 2. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_path_aux cs []

goal (2 subgoals):
 1. \<And>s S cs rs. \<lbrakk>length (m' # ms') = length s; valid_node m'; valid_call_list cs m'; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m'; length rs = length cs; ms' = targetnodes rs; \<forall>mx\<in>set ms'. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as' cs' rs'. preds (slice_kinds S as') s \<and> slice_edges S cs as' = [] \<and> m' -as'\<rightarrow>* m' \<and> valid_path_aux cs as' \<and> upd_cs cs as' = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as') s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as')) s = transfers (slice_kinds S as') s
 2. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
have "upd_cs cs [] = cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upd_cs cs [] = cs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
upd_cs cs [] = cs

goal (2 subgoals):
 1. \<And>s S cs rs. \<lbrakk>length (m' # ms') = length s; valid_node m'; valid_call_list cs m'; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m'; length rs = length cs; ms' = targetnodes rs; \<forall>mx\<in>set ms'. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as' cs' rs'. preds (slice_kinds S as') s \<and> slice_edges S cs as' = [] \<and> m' -as'\<rightarrow>* m' \<and> valid_path_aux cs as' \<and> upd_cs cs as' = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as') s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as')) s = transfers (slice_kinds S as') s
 2. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
preds (slice_kinds S []) s
slice_edges S cs [] = []
m' -[]\<rightarrow>* m'
valid_path_aux cs []
upd_cs cs [] = cs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
preds (slice_kinds S []) s
slice_edges S cs [] = []
m' -[]\<rightarrow>* m'
valid_path_aux cs []
upd_cs cs [] = cs

goal (1 subgoal):
 1. \<exists>as' cs' rs'. preds (slice_kinds n\<^sub>c as') s \<and> slice_edges n\<^sub>c cs as' = [] \<and> m' -as'\<rightarrow>* m' \<and> valid_path_aux cs as' \<and> upd_cs cs as' = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds n\<^sub>c as') s \<noteq> [] \<and> transfers (slice_kinds n\<^sub>c (slice_edges n\<^sub>c cs as')) s = transfers (slice_kinds n\<^sub>c as') s
[PROOF STEP]
using \<open>valid_call_list cs m'\<close> \<open>valid_return_list rs m'\<close>
      \<open>\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)\<close> \<open>length rs = length cs\<close>
      \<open>ms' = targetnodes rs\<close> \<open>s \<noteq> []\<close> \<open>valid_node m'\<close>
[PROOF STATE]
proof (prove)
using this:
preds (slice_kinds S []) s
slice_edges S cs [] = []
m' -[]\<rightarrow>* m'
valid_path_aux cs []
upd_cs cs [] = cs
valid_call_list cs m'
valid_return_list rs m'
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
length rs = length cs
ms' = targetnodes rs
s \<noteq> []
valid_node m'

goal (1 subgoal):
 1. \<exists>as' cs' rs'. preds (slice_kinds n\<^sub>c as') s \<and> slice_edges n\<^sub>c cs as' = [] \<and> m' -as'\<rightarrow>* m' \<and> valid_path_aux cs as' \<and> upd_cs cs as' = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds n\<^sub>c as') s \<noteq> [] \<and> transfers (slice_kinds n\<^sub>c (slice_edges n\<^sub>c cs as')) s = transfers (slice_kinds n\<^sub>c as') s
[PROOF STEP]
apply(rule_tac x="[]" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>preds (slice_kinds S []) s; slice_edges S cs [] = []; m' -[]\<rightarrow>* m'; valid_path_aux cs []; upd_cs cs [] = cs; valid_call_list cs m'; valid_return_list rs m'; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); length rs = length cs; ms' = targetnodes rs; s \<noteq> []; valid_node m'\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. preds (slice_kinds n\<^sub>c []) s \<and> slice_edges n\<^sub>c cs [] = [] \<and> m' -[]\<rightarrow>* m' \<and> valid_path_aux cs [] \<and> upd_cs cs [] = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds n\<^sub>c []) s \<noteq> [] \<and> transfers (slice_kinds n\<^sub>c (slice_edges n\<^sub>c cs [])) s = transfers (slice_kinds n\<^sub>c []) s
[PROOF STEP]
apply(rule_tac x="cs" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>preds (slice_kinds S []) s; slice_edges S cs [] = []; m' -[]\<rightarrow>* m'; valid_path_aux cs []; upd_cs cs [] = cs; valid_call_list cs m'; valid_return_list rs m'; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); length rs = length cs; ms' = targetnodes rs; s \<noteq> []; valid_node m'\<rbrakk> \<Longrightarrow> \<exists>rs'. preds (slice_kinds n\<^sub>c []) s \<and> slice_edges n\<^sub>c cs [] = [] \<and> m' -[]\<rightarrow>* m' \<and> valid_path_aux cs [] \<and> upd_cs cs [] = cs \<and> valid_node m' \<and> valid_call_list cs m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds n\<^sub>c []) s \<noteq> [] \<and> transfers (slice_kinds n\<^sub>c (slice_edges n\<^sub>c cs [])) s = transfers (slice_kinds n\<^sub>c []) s
[PROOF STEP]
apply(rule_tac x="rs" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>preds (slice_kinds S []) s; slice_edges S cs [] = []; m' -[]\<rightarrow>* m'; valid_path_aux cs []; upd_cs cs [] = cs; valid_call_list cs m'; valid_return_list rs m'; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); length rs = length cs; ms' = targetnodes rs; s \<noteq> []; valid_node m'\<rbrakk> \<Longrightarrow> preds (slice_kinds n\<^sub>c []) s \<and> slice_edges n\<^sub>c cs [] = [] \<and> m' -[]\<rightarrow>* m' \<and> valid_path_aux cs [] \<and> upd_cs cs [] = cs \<and> valid_node m' \<and> valid_call_list cs m' \<and> (\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)) \<and> valid_return_list rs m' \<and> length rs = length cs \<and> ms' = targetnodes rs \<and> transfers (slice_kinds n\<^sub>c []) s \<noteq> [] \<and> transfers (slice_kinds n\<^sub>c (slice_edges n\<^sub>c cs [])) s = transfers (slice_kinds n\<^sub>c []) s
[PROOF STEP]
by(clarsimp simp:slice_kinds_def)
[PROOF STATE]
proof (state)
this:
\<exists>as' cs' rs'. preds (slice_kinds n\<^sub>c as') s \<and> slice_edges n\<^sub>c cs as' = [] \<and> m' -as'\<rightarrow>* m' \<and> valid_path_aux cs as' \<and> upd_cs cs as' = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds n\<^sub>c as') s \<noteq> [] \<and> transfers (slice_kinds n\<^sub>c (slice_edges n\<^sub>c cs as')) s = transfers (slice_kinds n\<^sub>c as') s

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
case (tom_Cons S s as msx' s' as' sx'')
[PROOF STATE]
proof (state)
this:
S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (msx',s')
S,slice_kind S \<turnstile> (msx',s') =as'\<Rightarrow>* (m' # ms',sx'')
\<lbrakk>msx' = ?m # ?ms; valid_node ?m; valid_call_list ?cs ?m; \<forall>i<length ?rs. ?rs ! i \<in> get_return_edges (?cs ! i); valid_return_list ?rs ?m; length ?rs = length ?cs; ?ms = targetnodes ?rs; \<forall>mx\<in>set ?ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S ?cs as'a = as' \<and> ?m -as'a\<rightarrow>* m' \<and> valid_path_aux ?cs as'a \<and> upd_cs ?cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S ?cs as'a)) s' = transfers (slice_kinds S as'a) s'
valid_node m
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs
\<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 as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
note IH = \<open>\<And>m ms cs rs. \<lbrakk>msx' = m # ms; valid_node m; valid_call_list cs m;
      \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m;
      length rs = length cs; ms = targetnodes rs;
      \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk>
      \<Longrightarrow> \<exists>as'' cs' rs'. preds (slice_kinds S as'') s' \<and>
      slice_edges S cs as'' = as' \<and> m -as''\<rightarrow>* m' \<and> valid_path_aux cs as'' \<and>
      upd_cs cs as'' = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and>
      (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and>
      valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and>
      transfers (slice_kinds S as'') s' \<noteq> [] \<and>
      transfers (slice_kinds S (slice_edges S cs as'')) s' =
      transfers (slice_kinds S as'') s'\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>msx' = ?m # ?ms; valid_node ?m; valid_call_list ?cs ?m; \<forall>i<length ?rs. ?rs ! i \<in> get_return_edges (?cs ! i); valid_return_list ?rs ?m; length ?rs = length ?cs; ?ms = targetnodes ?rs; \<forall>mx\<in>set ?ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'' cs' rs'. preds (slice_kinds S as'') s' \<and> slice_edges S ?cs as'' = as' \<and> ?m -as''\<rightarrow>* m' \<and> valid_path_aux ?cs as'' \<and> upd_cs ?cs as'' = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'') s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S ?cs as'')) s' = transfers (slice_kinds S as'') s'

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) 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 as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from \<open>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (msx',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (msx',s')
[PROOF STEP]
obtain asx ax xs s'' where "as = asx@[ax]"
      and "S,slice_kind S \<turnstile> (m#ms,s) =asx\<Rightarrow>\<^sub>\<tau> (xs,s'')"
      and "S,slice_kind S \<turnstile> (xs,s'') -ax\<rightarrow> (msx',s')"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (msx',s')

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

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from \<open>S,slice_kind S \<turnstile> (xs,s'') -ax\<rightarrow> (msx',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (xs,s'') -ax\<rightarrow> (msx',s')
[PROOF STEP]
obtain xs' ms'' where [simp]:"xs = sourcenode ax#xs'" "msx' = targetnode ax#ms''"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (xs,s'') -ax\<rightarrow> (msx',s')

goal (1 subgoal):
 1. (\<And>xs' ms''. \<lbrakk>xs = sourcenode ax # xs'; msx' = targetnode ax # ms''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases xs) (auto elim!:observable_move.cases, cases msx', auto)
[PROOF STATE]
proof (state)
this:
xs = sourcenode ax # xs'
msx' = targetnode ax # ms''

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from \<open>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (msx',s')\<close> tom_Cons
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (msx',s')
S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (msx',s')
S,slice_kind S \<turnstile> (msx',s') =as'\<Rightarrow>* (m' # ms',sx'')
\<lbrakk>msx' = ?m # ?ms; valid_node ?m; valid_call_list ?cs ?m; \<forall>i<length ?rs. ?rs ! i \<in> get_return_edges (?cs ! i); valid_return_list ?rs ?m; length ?rs = length ?cs; ?ms = targetnodes ?rs; \<forall>mx\<in>set ?ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S ?cs as'a = as' \<and> ?m -as'a\<rightarrow>* m' \<and> valid_path_aux ?cs as'a \<and> upd_cs ?cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S ?cs as'a)) s' = transfers (slice_kinds S as'a) s'
valid_node m
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs
\<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]
obtain cs'' rs'' where results:"valid_node (targetnode ax)"
      "valid_call_list cs'' (targetnode ax)"
      "\<forall>i < length rs''. rs''!i \<in> get_return_edges (cs''!i)"
      "valid_return_list rs'' (targetnode ax)" "length rs'' = length cs''"
      "ms'' = targetnodes rs''" and "upd_cs cs as = cs''"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (msx',s')
S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (msx',s')
S,slice_kind S \<turnstile> (msx',s') =as'\<Rightarrow>* (m' # ms',sx'')
\<lbrakk>msx' = ?m # ?ms; valid_node ?m; valid_call_list ?cs ?m; \<forall>i<length ?rs. ?rs ! i \<in> get_return_edges (?cs ! i); valid_return_list ?rs ?m; length ?rs = length ?cs; ?ms = targetnodes ?rs; \<forall>mx\<in>set ?ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S ?cs as'a = as' \<and> ?m -as'a\<rightarrow>* m' \<and> valid_path_aux ?cs as'a \<and> upd_cs ?cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S ?cs as'a)) s' = transfers (slice_kinds S as'a) s'
valid_node m
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs
\<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>cs'' rs''. \<lbrakk>valid_node (targetnode ax); valid_call_list cs'' (targetnode ax); \<forall>i<length rs''. rs'' ! i \<in> get_return_edges (cs'' ! i); valid_return_list rs'' (targetnode ax); length rs'' = length cs''; ms'' = targetnodes rs''; upd_cs cs as = cs''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto elim!:observable_moves_preserves_stack)
[PROOF STATE]
proof (state)
this:
valid_node (targetnode ax)
valid_call_list cs'' (targetnode ax)
\<forall>i<length rs''. rs'' ! i \<in> get_return_edges (cs'' ! i)
valid_return_list rs'' (targetnode ax)
length rs'' = length cs''
ms'' = targetnodes rs''
upd_cs cs as = cs''

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from \<open>S,slice_kind S \<turnstile> (m#ms,s) =asx\<Rightarrow>\<^sub>\<tau> (xs,s'')\<close> callstack
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (m # ms,s) =asx\<Rightarrow>\<^sub>\<tau> (xs,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 asx. intra_kind (kind a)"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (m # ms,s) =asx\<Rightarrow>\<^sub>\<tau> (xs,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 asx. intra_kind (kind a)
[PROOF STEP]
by simp(rule silent_moves_slice_intra_path)
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set asx. intra_kind (kind a)

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
with \<open>S,slice_kind S \<turnstile> (m#ms,s) =asx\<Rightarrow>\<^sub>\<tau> (xs,s'')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (m # ms,s) =asx\<Rightarrow>\<^sub>\<tau> (xs,s'')
\<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> (xs,s'')
\<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. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from \<open>S,slice_kind S \<turnstile> (xs,s'') -ax\<rightarrow> (msx',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (xs,s'') -ax\<rightarrow> (msx',s')
[PROOF STEP]
have "\<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)
using this:
S,slice_kind S \<turnstile> (xs,s'') -ax\<rightarrow> (msx',s')

goal (1 subgoal):
 1. \<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]
by(fastforce dest:observable_set_stack_in_slice)
[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 as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from IH[OF \<open>msx' = targetnode ax#ms''\<close> results this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>as'' cs' rs'. preds (slice_kinds S as'') s' \<and> slice_edges S cs'' as'' = as' \<and> targetnode ax -as''\<rightarrow>* m' \<and> valid_path_aux cs'' as'' \<and> upd_cs cs'' as'' = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'') s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs'' as'')) s' = transfers (slice_kinds S as'') s'
[PROOF STEP]
obtain asx' cs' rs' where "preds (slice_kinds S asx') s'"
      and "slice_edges S cs'' asx' = as'" and "targetnode ax -asx'\<rightarrow>* m'"
      and "valid_path_aux cs'' asx'" and "upd_cs cs'' asx' = cs'"
      and "valid_node m'" and "valid_call_list cs' m'"
      and "\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)"
      and "valid_return_list rs' m'" and "length rs' = length cs'"
      and "ms' = targetnodes rs'" and "transfers (slice_kinds S asx') s' \<noteq> []"
      and trans_eq:"transfers (slice_kinds S (slice_edges S cs'' asx')) s' =
      transfers (slice_kinds S asx') s'"
[PROOF STATE]
proof (prove)
using this:
\<exists>as'' cs' rs'. preds (slice_kinds S as'') s' \<and> slice_edges S cs'' as'' = as' \<and> targetnode ax -as''\<rightarrow>* m' \<and> valid_path_aux cs'' as'' \<and> upd_cs cs'' as'' = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'') s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs'' as'')) s' = transfers (slice_kinds S as'') s'

goal (1 subgoal):
 1. (\<And>asx' cs' rs'. \<lbrakk>preds (slice_kinds S asx') s'; slice_edges S cs'' asx' = as'; targetnode ax -asx'\<rightarrow>* m'; valid_path_aux cs'' asx'; upd_cs cs'' asx' = cs'; valid_node m'; valid_call_list cs' m'; \<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i); valid_return_list rs' m'; length rs' = length cs'; ms' = targetnodes rs'; transfers (slice_kinds S asx') s' \<noteq> []; transfers (slice_kinds S (slice_edges S cs'' asx')) s' = transfers (slice_kinds S asx') s'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
preds (slice_kinds S asx') s'
slice_edges S cs'' asx' = as'
targetnode ax -asx'\<rightarrow>* m'
valid_path_aux cs'' asx'
upd_cs cs'' asx' = cs'
valid_node m'
valid_call_list cs' m'
\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)
valid_return_list rs' m'
length rs' = length cs'
ms' = targetnodes rs'
transfers (slice_kinds S asx') s' \<noteq> []
transfers (slice_kinds S (slice_edges S cs'' asx')) s' = transfers (slice_kinds S asx') s'

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from \<open>S,slice_kind S \<turnstile> (m#ms,s) =asx\<Rightarrow>\<^sub>\<tau> (xs,s'')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (m # ms,s) =asx\<Rightarrow>\<^sub>\<tau> (xs,s'')
[PROOF STEP]
have "preds (slice_kinds S asx) s" and "transfers (slice_kinds S asx) s = s''"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (m # ms,s) =asx\<Rightarrow>\<^sub>\<tau> (xs,s'')

goal (1 subgoal):
 1. preds (slice_kinds S asx) s &&& transfers (slice_kinds S asx) s = s''
[PROOF STEP]
by(auto intro:silent_moves_preds_transfers simp:slice_kinds_def)
[PROOF STATE]
proof (state)
this:
preds (slice_kinds S asx) s
transfers (slice_kinds S asx) s = s''

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from \<open>S,slice_kind S \<turnstile> (xs,s'') -ax\<rightarrow> (msx',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (xs,s'') -ax\<rightarrow> (msx',s')
[PROOF STEP]
have "pred (slice_kind S ax) s''" and "transfer (slice_kind S ax) s'' = s'"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (xs,s'') -ax\<rightarrow> (msx',s')

goal (1 subgoal):
 1. pred (slice_kind S ax) s'' &&& transfer (slice_kind S ax) s'' = s'
[PROOF STEP]
by(auto elim:observable_move.cases)
[PROOF STATE]
proof (state)
this:
pred (slice_kind S ax) s''
transfer (slice_kind S ax) s'' = s'

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
with \<open>preds (slice_kinds S asx) s\<close> \<open>as = asx@[ax]\<close>
      \<open>transfers (slice_kinds S asx) s = s''\<close>
[PROOF STATE]
proof (chain)
picking this:
preds (slice_kinds S asx) s
as = asx @ [ax]
transfers (slice_kinds S asx) s = s''
pred (slice_kind S ax) s''
transfer (slice_kind S ax) s'' = s'
[PROOF STEP]
have "preds (slice_kinds S as) s"
[PROOF STATE]
proof (prove)
using this:
preds (slice_kinds S asx) s
as = asx @ [ax]
transfers (slice_kinds S asx) s = s''
pred (slice_kind S ax) s''
transfer (slice_kind S ax) s'' = s'

goal (1 subgoal):
 1. preds (slice_kinds S as) s
[PROOF STEP]
by(simp add:preds_split slice_kinds_def)
[PROOF STATE]
proof (state)
this:
preds (slice_kinds S as) s

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from \<open>transfers (slice_kinds S asx) s = s''\<close>
      \<open>transfer (slice_kind S ax) s'' = s'\<close> \<open>as = asx@[ax]\<close>
[PROOF STATE]
proof (chain)
picking this:
transfers (slice_kinds S asx) s = s''
transfer (slice_kind S ax) s'' = s'
as = asx @ [ax]
[PROOF STEP]
have "transfers (slice_kinds S as) s = s'"
[PROOF STATE]
proof (prove)
using this:
transfers (slice_kinds S asx) s = s''
transfer (slice_kind S ax) s'' = s'
as = asx @ [ax]

goal (1 subgoal):
 1. transfers (slice_kinds S as) s = s'
[PROOF STEP]
by(simp add:transfers_split slice_kinds_def)
[PROOF STATE]
proof (state)
this:
transfers (slice_kinds S as) s = s'

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
with \<open>preds (slice_kinds S asx') s'\<close> \<open>preds (slice_kinds S as) s\<close>
[PROOF STATE]
proof (chain)
picking this:
preds (slice_kinds S asx') s'
preds (slice_kinds S as) s
transfers (slice_kinds S as) s = s'
[PROOF STEP]
have "preds (slice_kinds S (as@asx')) s"
[PROOF STATE]
proof (prove)
using this:
preds (slice_kinds S asx') s'
preds (slice_kinds S as) s
transfers (slice_kinds S as) s = s'

goal (1 subgoal):
 1. preds (slice_kinds S (as @ asx')) s
[PROOF STEP]
by(simp add:preds_split slice_kinds_def)
[PROOF STATE]
proof (state)
this:
preds (slice_kinds S (as @ asx')) s

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
preds (slice_kinds S (as @ asx')) s

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from \<open>valid_call_list cs m\<close> \<open>valid_return_list rs m\<close>
      \<open>\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)\<close> \<open>length rs = length cs\<close>
      \<open>ms = targetnodes rs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_call_list cs m
valid_return_list rs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
length rs = length cs
ms = targetnodes rs
[PROOF STEP]
have "\<forall>i<length cs. call_of_return_node (ms!i) (sourcenode (cs!i))"
[PROOF STATE]
proof (prove)
using this:
valid_call_list cs m
valid_return_list rs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
length rs = length cs
ms = targetnodes rs

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

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
with \<open>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (msx',s')\<close> \<open>ms = targetnodes rs\<close>
      \<open>length rs = length cs\<close>
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (msx',s')
ms = targetnodes rs
length rs = length cs
\<forall>i<length cs. call_of_return_node (ms ! i) (sourcenode (cs ! i))
[PROOF STEP]
have "slice_edges S cs as = [last as]"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (msx',s')
ms = targetnodes rs
length rs = length cs
\<forall>i<length cs. call_of_return_node (ms ! i) (sourcenode (cs ! i))

goal (1 subgoal):
 1. slice_edges S cs as = [last as]
[PROOF STEP]
by(fastforce elim:observable_moves_singular_slice_edge)
[PROOF STATE]
proof (state)
this:
slice_edges S cs as = [last as]

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
with \<open>slice_edges S cs'' asx' = as'\<close> \<open>upd_cs cs as = cs''\<close>
[PROOF STATE]
proof (chain)
picking this:
slice_edges S cs'' asx' = as'
upd_cs cs as = cs''
slice_edges S cs as = [last as]
[PROOF STEP]
have "slice_edges S cs (as@asx') = [last as]@as'"
[PROOF STATE]
proof (prove)
using this:
slice_edges S cs'' asx' = as'
upd_cs cs as = cs''
slice_edges S cs as = [last as]

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

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
slice_edges S cs (as @ asx') = [last as] @ as'

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from \<open>S,slice_kind S \<turnstile> (m#ms,s) =asx\<Rightarrow>\<^sub>\<tau> (xs,s'')\<close> \<open>valid_node m\<close>
      \<open>valid_call_list cs m\<close> \<open>\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)\<close>
      \<open>valid_return_list rs m\<close> \<open>length rs = length cs\<close> \<open>ms = targetnodes rs\<close>
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (m # ms,s) =asx\<Rightarrow>\<^sub>\<tau> (xs,s'')
valid_node m
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs
[PROOF STEP]
have "m -asx\<rightarrow>* sourcenode ax"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (m # ms,s) =asx\<Rightarrow>\<^sub>\<tau> (xs,s'')
valid_node m
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs

goal (1 subgoal):
 1. m -asx\<rightarrow>* sourcenode ax
[PROOF STEP]
by(fastforce intro:silent_moves_vpa_path)
[PROOF STATE]
proof (state)
this:
m -asx\<rightarrow>* sourcenode ax

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from \<open>S,slice_kind S \<turnstile> (xs,s'') -ax\<rightarrow> (msx',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (xs,s'') -ax\<rightarrow> (msx',s')
[PROOF STEP]
have "valid_edge ax"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (xs,s'') -ax\<rightarrow> (msx',s')

goal (1 subgoal):
 1. valid_edge ax
[PROOF STEP]
by(fastforce elim:observable_move.cases)
[PROOF STATE]
proof (state)
this:
valid_edge ax

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
hence "sourcenode ax -[ax]\<rightarrow>* targetnode ax"
[PROOF STATE]
proof (prove)
using this:
valid_edge ax

goal (1 subgoal):
 1. sourcenode ax -[ax]\<rightarrow>* targetnode ax
[PROOF STEP]
by(rule path_edge)
[PROOF STATE]
proof (state)
this:
sourcenode ax -[ax]\<rightarrow>* targetnode ax

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
with \<open>m -asx\<rightarrow>* sourcenode ax\<close> \<open>as = asx@[ax]\<close>
[PROOF STATE]
proof (chain)
picking this:
m -asx\<rightarrow>* sourcenode ax
as = asx @ [ax]
sourcenode ax -[ax]\<rightarrow>* targetnode ax
[PROOF STEP]
have "m -as\<rightarrow>* targetnode ax"
[PROOF STATE]
proof (prove)
using this:
m -asx\<rightarrow>* sourcenode ax
as = asx @ [ax]
sourcenode ax -[ax]\<rightarrow>* targetnode ax

goal (1 subgoal):
 1. m -as\<rightarrow>* targetnode ax
[PROOF STEP]
by(fastforce intro:path_Append)
[PROOF STATE]
proof (state)
this:
m -as\<rightarrow>* targetnode ax

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
with \<open>targetnode ax -asx'\<rightarrow>* m'\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode ax -asx'\<rightarrow>* m'
m -as\<rightarrow>* targetnode ax
[PROOF STEP]
have "m -as@asx'\<rightarrow>* m'"
[PROOF STATE]
proof (prove)
using this:
targetnode ax -asx'\<rightarrow>* m'
m -as\<rightarrow>* targetnode ax

goal (1 subgoal):
 1. m -as @ asx'\<rightarrow>* m'
[PROOF STEP]
by -(rule path_Append)
[PROOF STATE]
proof (state)
this:
m -as @ asx'\<rightarrow>* m'

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
m -as @ asx'\<rightarrow>* m'

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from \<open>\<forall>a \<in> set asx. intra_kind (kind a)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>set asx. intra_kind (kind a)
[PROOF STEP]
have "valid_path_aux cs asx"
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set asx. intra_kind (kind a)

goal (1 subgoal):
 1. valid_path_aux cs asx
[PROOF STEP]
by(rule valid_path_aux_intra_path)
[PROOF STATE]
proof (state)
this:
valid_path_aux cs asx

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from \<open>\<forall>a \<in> set asx. intra_kind (kind a)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>a\<in>set asx. intra_kind (kind a)
[PROOF STEP]
have "upd_cs cs asx = cs"
[PROOF STATE]
proof (prove)
using this:
\<forall>a\<in>set asx. intra_kind (kind a)

goal (1 subgoal):
 1. upd_cs cs asx = cs
[PROOF STEP]
by(rule upd_cs_intra_path)
[PROOF STATE]
proof (state)
this:
upd_cs cs asx = cs

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from \<open>m -asx\<rightarrow>* sourcenode ax\<close> \<open>\<forall>a \<in> set asx. intra_kind (kind a)\<close>
[PROOF STATE]
proof (chain)
picking this:
m -asx\<rightarrow>* sourcenode ax
\<forall>a\<in>set asx. intra_kind (kind a)
[PROOF STEP]
have "get_proc m = get_proc (sourcenode ax)"
[PROOF STATE]
proof (prove)
using this:
m -asx\<rightarrow>* sourcenode ax
\<forall>a\<in>set asx. intra_kind (kind a)

goal (1 subgoal):
 1. get_proc m = get_proc (sourcenode ax)
[PROOF STEP]
by(fastforce intro:intra_path_get_procs simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
get_proc m = get_proc (sourcenode ax)

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
with \<open>valid_return_list rs m\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_return_list rs m
get_proc m = get_proc (sourcenode ax)
[PROOF STEP]
have "valid_return_list rs (sourcenode ax)"
[PROOF STATE]
proof (prove)
using this:
valid_return_list rs m
get_proc m = get_proc (sourcenode ax)

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

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
with \<open>S,slice_kind S \<turnstile> (xs,s'') -ax\<rightarrow> (msx',s')\<close> \<open>valid_edge ax\<close>
      \<open>\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)\<close> \<open>ms = targetnodes rs\<close>
      \<open>length rs = length cs\<close>
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (xs,s'') -ax\<rightarrow> (msx',s')
valid_edge ax
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
ms = targetnodes rs
length rs = length cs
valid_return_list rs (sourcenode ax)
[PROOF STEP]
have "valid_path_aux cs [ax]"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (xs,s'') -ax\<rightarrow> (msx',s')
valid_edge ax
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
ms = targetnodes rs
length rs = length cs
valid_return_list rs (sourcenode ax)

goal (1 subgoal):
 1. valid_path_aux cs [ax]
[PROOF STEP]
by(auto intro!:observable_move_vpa_path simp del:valid_path_aux.simps)
[PROOF STATE]
proof (state)
this:
valid_path_aux cs [ax]

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
with \<open>valid_path_aux cs asx\<close> \<open>upd_cs cs asx = cs\<close> \<open>as = asx@[ax]\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_path_aux cs asx
upd_cs cs asx = cs
as = asx @ [ax]
valid_path_aux cs [ax]
[PROOF STEP]
have "valid_path_aux cs as"
[PROOF STATE]
proof (prove)
using this:
valid_path_aux cs asx
upd_cs cs asx = cs
as = asx @ [ax]
valid_path_aux cs [ax]

goal (1 subgoal):
 1. valid_path_aux cs as
[PROOF STEP]
by(fastforce intro:valid_path_aux_Append)
[PROOF STATE]
proof (state)
this:
valid_path_aux cs as

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
with \<open>upd_cs cs as = cs''\<close> \<open>valid_path_aux cs'' asx'\<close>
[PROOF STATE]
proof (chain)
picking this:
upd_cs cs as = cs''
valid_path_aux cs'' asx'
valid_path_aux cs as
[PROOF STEP]
have "valid_path_aux cs (as@asx')"
[PROOF STATE]
proof (prove)
using this:
upd_cs cs as = cs''
valid_path_aux cs'' asx'
valid_path_aux cs as

goal (1 subgoal):
 1. valid_path_aux cs (as @ asx')
[PROOF STEP]
by(fastforce intro:valid_path_aux_Append)
[PROOF STATE]
proof (state)
this:
valid_path_aux cs (as @ asx')

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_path_aux cs (as @ asx')

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from \<open>upd_cs cs as = cs''\<close> \<open>upd_cs cs'' asx' = cs'\<close>
[PROOF STATE]
proof (chain)
picking this:
upd_cs cs as = cs''
upd_cs cs'' asx' = cs'
[PROOF STEP]
have "upd_cs cs (as@asx') = cs'"
[PROOF STATE]
proof (prove)
using this:
upd_cs cs as = cs''
upd_cs cs'' asx' = cs'

goal (1 subgoal):
 1. upd_cs cs (as @ asx') = cs'
[PROOF STEP]
by(rule upd_cs_Append)
[PROOF STATE]
proof (state)
this:
upd_cs cs (as @ asx') = cs'

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
upd_cs cs (as @ asx') = cs'

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from \<open>transfers (slice_kinds S as) s = s'\<close>
      \<open>transfers (slice_kinds S asx') s' \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
transfers (slice_kinds S as) s = s'
transfers (slice_kinds S asx') s' \<noteq> []
[PROOF STEP]
have "transfers (slice_kinds S (as@asx')) s \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
transfers (slice_kinds S as) s = s'
transfers (slice_kinds S asx') s' \<noteq> []

goal (1 subgoal):
 1. transfers (slice_kinds S (as @ asx')) s \<noteq> []
[PROOF STEP]
by(simp add:slice_kinds_def transfers_split)
[PROOF STATE]
proof (state)
this:
transfers (slice_kinds S (as @ asx')) s \<noteq> []

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
transfers (slice_kinds S (as @ asx')) s \<noteq> []

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from \<open>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (msx',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (msx',s')
[PROOF STEP]
have "transfers (map (slice_kind S) as) s = s'"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (msx',s')

goal (1 subgoal):
 1. transfers (map (slice_kind S) as) s = s'
[PROOF STEP]
by simp(rule observable_moves_preds_transfers)
[PROOF STATE]
proof (state)
this:
transfers (map (slice_kind S) as) s = s'

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from \<open>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (msx',s')\<close> \<open>ms = targetnodes rs\<close>
      \<open>length rs = length cs\<close> \<open>\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)\<close>
      \<open>valid_call_list cs m\<close> \<open>valid_return_list rs m\<close>
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (msx',s')
ms = targetnodes rs
length rs = length cs
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_call_list cs m
valid_return_list rs m
[PROOF STEP]
have "slice_edges S cs as = [last as]"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (msx',s')
ms = targetnodes rs
length rs = length cs
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_call_list cs m
valid_return_list rs m

goal (1 subgoal):
 1. slice_edges S cs as = [last as]
[PROOF STEP]
by(fastforce intro!:observable_moves_singular_slice_edge
      [OF _ _ _ stacks_rewrite])
[PROOF STATE]
proof (state)
this:
slice_edges S cs as = [last as]

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from \<open>S,slice_kind S \<turnstile> (m#ms,s) =asx\<Rightarrow>\<^sub>\<tau> (xs,s'')\<close> callstack
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (m # ms,s) =asx\<Rightarrow>\<^sub>\<tau> (xs,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 "s = s''"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (m # ms,s) =asx\<Rightarrow>\<^sub>\<tau> (xs,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. s = s''
[PROOF STEP]
by(fastforce intro:silent_moves_slice_keeps_state)
[PROOF STATE]
proof (state)
this:
s = s''

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
with \<open>S,slice_kind S \<turnstile> (xs,s'') -ax\<rightarrow> (msx',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (xs,s'') -ax\<rightarrow> (msx',s')
s = s''
[PROOF STEP]
have "transfer (slice_kind S ax) s = s'"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (xs,s'') -ax\<rightarrow> (msx',s')
s = s''

goal (1 subgoal):
 1. transfer (slice_kind S ax) s = s'
[PROOF STEP]
by(fastforce elim:observable_move.cases)
[PROOF STATE]
proof (state)
this:
transfer (slice_kind S ax) s = s'

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
with \<open>slice_edges S cs as = [last as]\<close> \<open>as = asx@[ax]\<close>
[PROOF STATE]
proof (chain)
picking this:
slice_edges S cs as = [last as]
as = asx @ [ax]
transfer (slice_kind S ax) s = s'
[PROOF STEP]
have "s' = transfers (slice_kinds S (slice_edges S cs as)) s"
[PROOF STATE]
proof (prove)
using this:
slice_edges S cs as = [last as]
as = asx @ [ax]
transfer (slice_kind S ax) s = s'

goal (1 subgoal):
 1. s' = transfers (slice_kinds S (slice_edges S cs as)) s
[PROOF STEP]
by(simp add:slice_kinds_def)
[PROOF STATE]
proof (state)
this:
s' = transfers (slice_kinds S (slice_edges S cs as)) s

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from \<open>upd_cs cs as = cs''\<close>
[PROOF STATE]
proof (chain)
picking this:
upd_cs cs as = cs''
[PROOF STEP]
have "slice_edges S cs (as @ asx') =
      (slice_edges S cs as)@(slice_edges S cs'' asx')"
[PROOF STATE]
proof (prove)
using this:
upd_cs cs as = cs''

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

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
hence trans_eq':"transfers (slice_kinds S (slice_edges S cs (as @ asx'))) s =
      transfers (slice_kinds S (slice_edges S cs'' asx'))
        (transfers (slice_kinds S (slice_edges S cs as)) s)"
[PROOF STATE]
proof (prove)
using this:
slice_edges S cs (as @ asx') = slice_edges S cs as @ slice_edges S cs'' asx'

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

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
from \<open>s' = transfers (slice_kinds S (slice_edges S cs as)) s\<close>
      \<open>transfers (map (slice_kind S) as) s = s'\<close>
[PROOF STATE]
proof (chain)
picking this:
s' = transfers (slice_kinds S (slice_edges S cs as)) s
transfers (map (slice_kind S) as) s = s'
[PROOF STEP]
have "transfers (map (slice_kind S) (slice_edges S cs as)) s =
      transfers (map (slice_kind S) as) s"
[PROOF STATE]
proof (prove)
using this:
s' = transfers (slice_kinds S (slice_edges S cs as)) s
transfers (map (slice_kind S) as) s = s'

goal (1 subgoal):
 1. transfers (map (slice_kind S) (slice_edges S cs as)) s = transfers (map (slice_kind S) as) s
[PROOF STEP]
by(simp add:slice_kinds_def)
[PROOF STATE]
proof (state)
this:
transfers (map (slice_kind S) (slice_edges S cs as)) s = transfers (map (slice_kind S) as) s

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
with trans_eq trans_eq'
      \<open>s' = transfers (slice_kinds S (slice_edges S cs as)) s\<close>
[PROOF STATE]
proof (chain)
picking this:
transfers (slice_kinds S (slice_edges S cs'' asx')) s' = transfers (slice_kinds S asx') s'
transfers (slice_kinds S (slice_edges S cs (as @ asx'))) s = transfers (slice_kinds S (slice_edges S cs'' asx')) (transfers (slice_kinds S (slice_edges S cs as)) s)
s' = transfers (slice_kinds S (slice_edges S cs as)) s
transfers (map (slice_kind S) (slice_edges S cs as)) s = transfers (map (slice_kind S) as) s
[PROOF STEP]
have "transfers (slice_kinds S (slice_edges S cs (as @ asx'))) s =
       transfers (slice_kinds S (as @ asx')) s"
[PROOF STATE]
proof (prove)
using this:
transfers (slice_kinds S (slice_edges S cs'' asx')) s' = transfers (slice_kinds S asx') s'
transfers (slice_kinds S (slice_edges S cs (as @ asx'))) s = transfers (slice_kinds S (slice_edges S cs'' asx')) (transfers (slice_kinds S (slice_edges S cs as)) s)
s' = transfers (slice_kinds S (slice_edges S cs as)) s
transfers (map (slice_kind S) (slice_edges S cs as)) s = transfers (map (slice_kind S) as) s

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

goal (1 subgoal):
 1. \<And>S s as ms'a s' as' s'' m ms cs rs. \<lbrakk>S,slice_kind S \<turnstile> (m # ms,s) =as\<Rightarrow> (ms'a,s'); S,slice_kind S \<turnstile> (ms'a,s') =as'\<Rightarrow>* (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s' \<and> slice_edges S cs as'a = as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s' \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s' = transfers (slice_kinds S as'a) s'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
preds (slice_kinds S (as @ asx')) s
slice_edges S cs (as @ asx') = [last as] @ as'
m -as @ asx'\<rightarrow>* m'
valid_path_aux cs (as @ asx')
upd_cs cs (as @ asx') = cs'
transfers (slice_kinds S (as @ asx')) s \<noteq> []
transfers (slice_kinds S (slice_edges S cs (as @ asx'))) s = transfers (slice_kinds S (as @ asx')) s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
preds (slice_kinds S (as @ asx')) s
slice_edges S cs (as @ asx') = [last as] @ as'
m -as @ asx'\<rightarrow>* m'
valid_path_aux cs (as @ asx')
upd_cs cs (as @ asx') = cs'
transfers (slice_kinds S (as @ asx')) s \<noteq> []
transfers (slice_kinds S (slice_edges S cs (as @ asx'))) s = transfers (slice_kinds S (as @ asx')) s

goal (1 subgoal):
 1. \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
using \<open>valid_node m'\<close> \<open>valid_call_list cs' m'\<close>
        \<open>\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)\<close>
        \<open>valid_return_list rs' m'\<close> \<open>length rs' = length cs'\<close> \<open>ms' = targetnodes rs'\<close>
[PROOF STATE]
proof (prove)
using this:
preds (slice_kinds S (as @ asx')) s
slice_edges S cs (as @ asx') = [last as] @ as'
m -as @ asx'\<rightarrow>* m'
valid_path_aux cs (as @ asx')
upd_cs cs (as @ asx') = cs'
transfers (slice_kinds S (as @ asx')) s \<noteq> []
transfers (slice_kinds S (slice_edges S cs (as @ asx'))) s = transfers (slice_kinds S (as @ asx')) s
valid_node m'
valid_call_list cs' m'
\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)
valid_return_list rs' m'
length rs' = length cs'
ms' = targetnodes rs'

goal (1 subgoal):
 1. \<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s
[PROOF STEP]
apply(rule_tac x="as@asx'" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>preds (slice_kinds S (as @ asx')) s; slice_edges S cs (as @ asx') = [last as] @ as'; m -as @ asx'\<rightarrow>* m'; valid_path_aux cs (as @ asx'); upd_cs cs (as @ asx') = cs'; transfers (slice_kinds S (as @ asx')) s \<noteq> []; transfers (slice_kinds S (slice_edges S cs (as @ asx'))) s = transfers (slice_kinds S (as @ asx')) s; valid_node m'; valid_call_list cs' m'; \<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i); valid_return_list rs' m'; length rs' = length cs'; ms' = targetnodes rs'\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. preds (slice_kinds S (as @ asx')) s \<and> slice_edges S cs (as @ asx') = last as # as' \<and> m -as @ asx'\<rightarrow>* m' \<and> valid_path_aux cs (as @ asx') \<and> upd_cs cs (as @ asx') = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S (as @ asx')) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs (as @ asx'))) s = transfers (slice_kinds S (as @ asx')) s
[PROOF STEP]
apply(rule_tac x="cs'" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>preds (slice_kinds S (as @ asx')) s; slice_edges S cs (as @ asx') = [last as] @ as'; m -as @ asx'\<rightarrow>* m'; valid_path_aux cs (as @ asx'); upd_cs cs (as @ asx') = cs'; transfers (slice_kinds S (as @ asx')) s \<noteq> []; transfers (slice_kinds S (slice_edges S cs (as @ asx'))) s = transfers (slice_kinds S (as @ asx')) s; valid_node m'; valid_call_list cs' m'; \<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i); valid_return_list rs' m'; length rs' = length cs'; ms' = targetnodes rs'\<rbrakk> \<Longrightarrow> \<exists>rs'. preds (slice_kinds S (as @ asx')) s \<and> slice_edges S cs (as @ asx') = last as # as' \<and> m -as @ asx'\<rightarrow>* m' \<and> valid_path_aux cs (as @ asx') \<and> upd_cs cs (as @ asx') = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S (as @ asx')) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs (as @ asx'))) s = transfers (slice_kinds S (as @ asx')) s
[PROOF STEP]
apply(rule_tac x="rs'" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>preds (slice_kinds S (as @ asx')) s; slice_edges S cs (as @ asx') = [last as] @ as'; m -as @ asx'\<rightarrow>* m'; valid_path_aux cs (as @ asx'); upd_cs cs (as @ asx') = cs'; transfers (slice_kinds S (as @ asx')) s \<noteq> []; transfers (slice_kinds S (slice_edges S cs (as @ asx'))) s = transfers (slice_kinds S (as @ asx')) s; valid_node m'; valid_call_list cs' m'; \<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i); valid_return_list rs' m'; length rs' = length cs'; ms' = targetnodes rs'\<rbrakk> \<Longrightarrow> preds (slice_kinds S (as @ asx')) s \<and> slice_edges S cs (as @ asx') = last as # as' \<and> m -as @ asx'\<rightarrow>* m' \<and> valid_path_aux cs (as @ asx') \<and> upd_cs cs (as @ asx') = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S (as @ asx')) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs (as @ asx'))) s = transfers (slice_kinds S (as @ asx')) s
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
\<exists>as'a cs' rs'. preds (slice_kinds S as'a) s \<and> slice_edges S cs as'a = last as # as' \<and> m -as'a\<rightarrow>* m' \<and> valid_path_aux cs as'a \<and> upd_cs cs as'a = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as'a) s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as'a)) s = transfers (slice_kinds S as'a) s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>as' cs' rs'. preds (slice_kinds S as') s \<and> slice_edges S cs as' = as \<and> m -as'\<rightarrow>* m' \<and> valid_path_aux cs as' \<and> upd_cs cs as' = cs' \<and> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> transfers (slice_kinds S as') s \<noteq> [] \<and> transfers (slice_kinds S (slice_edges S cs as')) s = transfers (slice_kinds S as') s

goal:
No subgoals!
[PROOF STEP]
qed