[STATEMENT]
theorem fundamental_property_of_static_slicing:
  assumes "m -as\<rightarrow>\<^sub>\<surd>* m'" and "preds (kinds as) [cf]" and "CFG_node m' \<in> S"
  obtains as' where "preds (slice_kinds S as') [cf]"
  and "\<forall>V \<in> Use m'. state_val (transfers (slice_kinds S as') [cf]) V =
                    state_val (transfers (kinds as) [cf]) V"
  and "slice_edges S [] as = slice_edges S [] as'"
  and "transfers (kinds as) [cf] \<noteq> []" and "m -as'\<rightarrow>\<^sub>\<surd>* m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>as'. \<lbrakk>preds (slice_kinds S as') [cf]; \<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V; slice_edges S [] as = slice_edges S [] as'; transfers (kinds as) [cf] \<noteq> []; m -as'\<rightarrow>\<^sub>\<surd>* m'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from \<open>m -as\<rightarrow>\<^sub>\<surd>* m'\<close> \<open>preds (kinds as) [cf]\<close>
[PROOF STATE]
proof (chain)
picking this:
m -as\<rightarrow>\<^sub>\<surd>* m'
preds (kinds as) [cf]
[PROOF STEP]
obtain ms'' s'' ms' as' as''
    where "S,kind \<turnstile> ([m],[cf]) =slice_edges S [] as\<Rightarrow>*
                              (ms'',s'')"
    and "S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m'#ms',transfers (kinds as) [cf])"
    and "slice_edges S [] as = slice_edges S [] as''"
    and "m -as''@as'\<rightarrow>\<^sub>\<surd>* m'"
[PROOF STATE]
proof (prove)
using this:
m -as\<rightarrow>\<^sub>\<surd>* m'
preds (kinds as) [cf]

goal (1 subgoal):
 1. (\<And>ms'' s'' as' ms' as''. \<lbrakk>S,kind \<turnstile> ([m],[cf]) =slice_edges S [] as\<Rightarrow>* (ms'',s''); S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf]); slice_edges S [] as = slice_edges S [] as''; m -as'' @ as'\<rightarrow>\<^sub>\<surd>* m'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto elim:valid_path_trans_observable_moves[of _ _ _ _ _ "S"])
[PROOF STATE]
proof (state)
this:
S,kind \<turnstile> ([m],[cf]) =slice_edges S [] as\<Rightarrow>* (ms'',s'')
S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf])
slice_edges S [] as = slice_edges S [] as''
m -as'' @ as'\<rightarrow>\<^sub>\<surd>* m'

goal (1 subgoal):
 1. \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from \<open>m -as\<rightarrow>\<^sub>\<surd>* m'\<close>
[PROOF STATE]
proof (chain)
picking this:
m -as\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
have "valid_node m" and "valid_node m'"
[PROOF STATE]
proof (prove)
using this:
m -as\<rightarrow>\<^sub>\<surd>* m'

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

goal (1 subgoal):
 1. \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with \<open>CFG_node m' \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node m' \<in> S
valid_node m
valid_node m'
[PROOF STEP]
have "CFG_node m' \<in> HRB_slice S"
[PROOF STATE]
proof (prove)
using this:
CFG_node m' \<in> S
valid_node m
valid_node m'

goal (1 subgoal):
 1. CFG_node m' \<in> HRB_slice S
[PROOF STEP]
by -(rule HRB_slice_refl)
[PROOF STATE]
proof (state)
this:
CFG_node m' \<in> HRB_slice S

goal (1 subgoal):
 1. \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from \<open>valid_node m\<close> \<open>CFG_node m' \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_node m
CFG_node m' \<in> S
[PROOF STEP]
have "(([m],[cf]),([m],[cf])) \<in> WS S"
[PROOF STATE]
proof (prove)
using this:
valid_node m
CFG_node m' \<in> S

goal (1 subgoal):
 1. (([m], [cf]), [m], [cf]) \<in> WS S
[PROOF STEP]
by(fastforce intro:WSI)
[PROOF STATE]
proof (state)
this:
(([m], [cf]), [m], [cf]) \<in> WS S

goal (1 subgoal):
 1. \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(([m], [cf]), [m], [cf]) \<in> WS S

goal (1 subgoal):
 1. \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
fix V
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
assume "V \<in> Use m'"
[PROOF STATE]
proof (state)
this:
V \<in> Use m'

goal (1 subgoal):
 1. \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with \<open>valid_node m'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_node m'
V \<in> Use m'
[PROOF STEP]
have "V \<in> Use\<^bsub>SDG\<^esub> (CFG_node m')"
[PROOF STATE]
proof (prove)
using this:
valid_node m'
V \<in> Use m'

goal (1 subgoal):
 1. V \<in> Use\<^bsub>SDG\<^esub> CFG_node m'
[PROOF STEP]
by(fastforce intro:CFG_Use_SDG_Use)
[PROOF STATE]
proof (state)
this:
V \<in> Use\<^bsub>SDG\<^esub> CFG_node m'

goal (1 subgoal):
 1. \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
V \<in> Use\<^bsub>SDG\<^esub> CFG_node m'

goal (1 subgoal):
 1. \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from \<open>valid_node m'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_node m'
[PROOF STEP]
have "parent_node (CFG_node m') -[]\<rightarrow>\<^sub>\<iota>* parent_node (CFG_node m')"
[PROOF STATE]
proof (prove)
using this:
valid_node m'

goal (1 subgoal):
 1. parent_node (CFG_node m') -[]\<rightarrow>\<^sub>\<iota>* parent_node (CFG_node m')
[PROOF STEP]
by(fastforce intro:empty_path simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
parent_node (CFG_node m') -[]\<rightarrow>\<^sub>\<iota>* parent_node (CFG_node m')

goal (1 subgoal):
 1. \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
V \<in> Use\<^bsub>SDG\<^esub> CFG_node m'
parent_node (CFG_node m') -[]\<rightarrow>\<^sub>\<iota>* parent_node (CFG_node m')
[PROOF STEP]
have "V \<in> rv S (CFG_node m')"
[PROOF STATE]
proof (prove)
using this:
V \<in> Use\<^bsub>SDG\<^esub> CFG_node m'
parent_node (CFG_node m') -[]\<rightarrow>\<^sub>\<iota>* parent_node (CFG_node m')

goal (1 subgoal):
 1. V \<in> rv S (CFG_node m')
[PROOF STEP]
using \<open>CFG_node m' \<in> HRB_slice S\<close> \<open>CFG_node m' \<in> S\<close>
[PROOF STATE]
proof (prove)
using this:
V \<in> Use\<^bsub>SDG\<^esub> CFG_node m'
parent_node (CFG_node m') -[]\<rightarrow>\<^sub>\<iota>* parent_node (CFG_node m')
CFG_node m' \<in> HRB_slice S
CFG_node m' \<in> S

goal (1 subgoal):
 1. V \<in> rv S (CFG_node m')
[PROOF STEP]
by(fastforce intro:rvI simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
V \<in> rv S (CFG_node m')

goal (1 subgoal):
 1. \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?V2 \<in> Use m' \<Longrightarrow> ?V2 \<in> rv S (CFG_node m')

goal (1 subgoal):
 1. \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
hence "\<forall>V \<in> Use m'. V \<in> rv S (CFG_node m')"
[PROOF STATE]
proof (prove)
using this:
?V2 \<in> Use m' \<Longrightarrow> ?V2 \<in> rv S (CFG_node m')

goal (1 subgoal):
 1. \<forall>V\<in>Use m'. V \<in> rv S (CFG_node m')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>V\<in>Use m'. V \<in> rv S (CFG_node m')

goal (1 subgoal):
 1. \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
show "\<exists>as'. preds (slice_kinds S as') [cf] \<and>
    (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V =
    state_val (transfers (kinds as) [cf]) V) \<and>
    slice_edges S [] as = slice_edges S [] as' \<and>
     transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
proof(cases "slice_edges S [] as = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. slice_edges S [] as = [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
 2. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
slice_edges S [] as = []

goal (2 subgoals):
 1. slice_edges S [] as = [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
 2. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
hence "preds (slice_kinds S []) [cf]"
      and "slice_edges S [] [] = slice_edges S [] as"
[PROOF STATE]
proof (prove)
using this:
slice_edges S [] as = []

goal (1 subgoal):
 1. preds (slice_kinds S []) [cf] &&& slice_edges S [] [] = slice_edges S [] as
[PROOF STEP]
by(simp_all add:slice_kinds_def)
[PROOF STATE]
proof (state)
this:
preds (slice_kinds S []) [cf]
slice_edges S [] [] = slice_edges S [] as

goal (2 subgoals):
 1. slice_edges S [] as = [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
 2. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with \<open>S,kind \<turnstile> ([m],[cf]) =slice_edges S [] as\<Rightarrow>* (ms'',s'')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> ([m],[cf]) =slice_edges S [] as\<Rightarrow>* (ms'',s'')
preds (slice_kinds S []) [cf]
slice_edges S [] [] = slice_edges S [] as
[PROOF STEP]
have [simp]:"ms'' = [m]" "s'' = [cf]"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> ([m],[cf]) =slice_edges S [] as\<Rightarrow>* (ms'',s'')
preds (slice_kinds S []) [cf]
slice_edges S [] [] = slice_edges S [] as

goal (1 subgoal):
 1. ms'' = [m] &&& s'' = [cf]
[PROOF STEP]
by(auto elim:trans_observable_moves.cases)
[PROOF STATE]
proof (state)
this:
ms'' = [m]
s'' = [cf]

goal (2 subgoals):
 1. slice_edges S [] as = [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
 2. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with \<open>S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m'#ms',transfers (kinds as) [cf])\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf])
ms'' = [m]
s'' = [cf]
[PROOF STEP]
have "S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (m'#ms',transfers (kinds as) [cf])"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf])
ms'' = [m]
s'' = [cf]

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

goal (2 subgoals):
 1. slice_edges S [] as = [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
 2. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with \<open>valid_node m\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_node m
S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf])
[PROOF STEP]
have "m -as'\<rightarrow>* m'" and "valid_path_aux [] as'"
[PROOF STATE]
proof (prove)
using this:
valid_node m
S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf])

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

goal (2 subgoals):
 1. slice_edges S [] as = [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
 2. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
hence "m -as'\<rightarrow>\<^sub>\<surd>* m'"
[PROOF STATE]
proof (prove)
using this:
m -as'\<rightarrow>* m'
valid_path_aux [] as'

goal (1 subgoal):
 1. m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
by(simp add:vp_def valid_path_def)
[PROOF STATE]
proof (state)
this:
m -as'\<rightarrow>\<^sub>\<surd>* m'

goal (2 subgoals):
 1. slice_edges S [] as = [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
 2. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from \<open>S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (m'#ms',transfers (kinds as) [cf])\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf])
[PROOF STEP]
have "slice_edges S [] as' = []"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf])

goal (1 subgoal):
 1. slice_edges S [] as' = []
[PROOF STEP]
by(fastforce dest:silent_moves_no_slice_edges[where cs="[]" and rs="[]"]
                  simp:targetnodes_def)
[PROOF STATE]
proof (state)
this:
slice_edges S [] as' = []

goal (2 subgoals):
 1. slice_edges S [] as = [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
 2. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from \<open>S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (m'#ms',transfers (kinds as) [cf])\<close>
      \<open>valid_node m\<close> \<open>valid_node m'\<close> \<open>CFG_node m' \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf])
valid_node m
valid_node m'
CFG_node m' \<in> S
[PROOF STEP]
have returns:"\<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,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf])
valid_node m
valid_node m'
CFG_node m' \<in> 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 -(erule silent_moves_called_node_in_slice1_nodestack_in_slice1
        [of _ _ _ _ _ _ _ _ _ "[]" "[]"],
        auto intro:refl_slice1 simp:targetnodes_def valid_return_list_def)
[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 (2 subgoals):
 1. slice_edges S [] as = [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
 2. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from \<open>S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (m'#ms',transfers (kinds as) [cf])\<close>
      \<open>(([m],[cf]),([m],[cf])) \<in> WS S\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf])
(([m], [cf]), [m], [cf]) \<in> WS S
[PROOF STEP]
have WS:"((m'#ms',transfers (kinds as) [cf]),([m],[cf])) \<in> WS S"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf])
(([m], [cf]), [m], [cf]) \<in> WS S

goal (1 subgoal):
 1. ((m' # ms', transfers (kinds as) [cf]), [m], [cf]) \<in> WS S
[PROOF STEP]
by(rule WS_silent_moves)
[PROOF STATE]
proof (state)
this:
((m' # ms', transfers (kinds as) [cf]), [m], [cf]) \<in> WS S

goal (2 subgoals):
 1. slice_edges S [] as = [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
 2. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
hence "transfers (kinds as) [cf] \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
((m' # ms', transfers (kinds as) [cf]), [m], [cf]) \<in> WS S

goal (1 subgoal):
 1. transfers (kinds as) [cf] \<noteq> []
[PROOF STEP]
by(auto elim!:WS.cases)
[PROOF STATE]
proof (state)
this:
transfers (kinds as) [cf] \<noteq> []

goal (2 subgoals):
 1. slice_edges S [] as = [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
 2. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with WS returns \<open>transfers (kinds as) [cf] \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
((m' # ms', transfers (kinds as) [cf]), [m], [cf]) \<in> WS 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>
transfers (kinds as) [cf] \<noteq> []
transfers (kinds as) [cf] \<noteq> []
[PROOF STEP]
have "\<forall>V \<in> rv S (CFG_node m').
      state_val (transfers (kinds as) [cf]) V = fst cf V"
[PROOF STATE]
proof (prove)
using this:
((m' # ms', transfers (kinds as) [cf]), [m], [cf]) \<in> WS 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>
transfers (kinds as) [cf] \<noteq> []
transfers (kinds as) [cf] \<noteq> []

goal (1 subgoal):
 1. \<forall>V\<in>rv S (CFG_node m'). state_val (transfers (kinds as) [cf]) V = fst cf V
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((m' # ms', transfers (kinds as) [cf]), [m], [cf]) \<in> WS 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>; transfers (kinds as) [cf] \<noteq> []; transfers (kinds as) [cf] \<noteq> []\<rbrakk> \<Longrightarrow> \<forall>V\<in>rv S (CFG_node m'). state_val (transfers (kinds as) [cf]) V = fst cf V
[PROOF STEP]
apply(erule WS.cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ms ms'a s s' msx mx. \<lbrakk>\<forall>mx\<in>set ms'. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; transfers (kinds as) [cf] \<noteq> []; transfers (kinds as) [cf] \<noteq> []; m' # ms' = ms; transfers (kinds as) [cf] = s; [m] = ms'a; [cf] = s'; Ball (set ms) valid_node; Ball (set ms'a) valid_node; length ms = length s; length ms'a = length s'; s \<noteq> []; s' \<noteq> []; ms = msx @ mx # tl ms'a; get_proc mx = get_proc (hd ms'a); \<forall>m\<in>set (tl ms'a). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; msx \<noteq> [] \<longrightarrow> (\<exists>mx'. call_of_return_node mx mx' \<and> mx' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>); \<forall>i<length ms'a. snd (s ! (length msx + i)) = snd (s' ! i); Ball (set (tl ms)) return_node; \<forall>i<length ms'a. \<forall>V\<in>rv S (CFG_node ((mx # tl ms'a) ! i)). fst (s ! (length msx + i)) V = fst (s' ! i) V; obs ms \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = obs ms'a \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> \<forall>V\<in>rv S (CFG_node m'). state_val (transfers (kinds as) [cf]) V = fst cf V
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>msx mx V. \<lbrakk>\<forall>mx\<in>set ms'. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; m' # ms' = msx @ [mx]; valid_node m; Suc (length msx) = length (transfers (kinds as) [cf]); transfers (kinds as) [cf] \<noteq> []; get_proc mx = get_proc m; msx \<noteq> [] \<longrightarrow> (\<exists>mx'. call_of_return_node mx mx' \<and> mx' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>); snd (transfers (kinds as) [cf] ! length msx) = snd cf; Ball (set (tl (msx @ [mx]))) return_node; \<forall>V\<in>rv S (CFG_node mx). fst (transfers (kinds as) [cf] ! length msx) V = fst cf V; obs (msx @ [mx]) \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> = (let S' = obs_intra m \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> in if S' = {} then obs [] \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub> else (\<lambda>nx. [nx]) ` S'); V \<in> rv S (CFG_node m'); valid_node mx; Ball (set msx) valid_node\<rbrakk> \<Longrightarrow> state_val (transfers (kinds as) [cf]) V = fst cf V
[PROOF STEP]
by(case_tac msx)(auto simp:hd_conv_nth)
[PROOF STATE]
proof (state)
this:
\<forall>V\<in>rv S (CFG_node m'). state_val (transfers (kinds as) [cf]) V = fst cf V

goal (2 subgoals):
 1. slice_edges S [] as = [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
 2. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with \<open>\<forall>V \<in> Use m'. V \<in> rv S (CFG_node m')\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>V\<in>Use m'. V \<in> rv S (CFG_node m')
\<forall>V\<in>rv S (CFG_node m'). state_val (transfers (kinds as) [cf]) V = fst cf V
[PROOF STEP]
have Uses:"\<forall>V \<in> Use m'. state_val (transfers (kinds as) [cf]) V = fst cf V"
[PROOF STATE]
proof (prove)
using this:
\<forall>V\<in>Use m'. V \<in> rv S (CFG_node m')
\<forall>V\<in>rv S (CFG_node m'). state_val (transfers (kinds as) [cf]) V = fst cf V

goal (1 subgoal):
 1. \<forall>V\<in>Use m'. state_val (transfers (kinds as) [cf]) V = fst cf V
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>V\<in>Use m'. state_val (transfers (kinds as) [cf]) V = fst cf V

goal (2 subgoals):
 1. slice_edges S [] as = [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
 2. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
have [simp]:"ms' = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ms' = []
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ms' \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
assume "ms' \<noteq> []"
[PROOF STATE]
proof (state)
this:
ms' \<noteq> []

goal (1 subgoal):
 1. ms' \<noteq> [] \<Longrightarrow> False
[PROOF STEP]
with \<open>S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (m'#ms',transfers (kinds as) [cf])\<close>
        \<open>valid_node m\<close> \<open>valid_node m'\<close> \<open>CFG_node m' \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf])
valid_node m
valid_node m'
CFG_node m' \<in> S
ms' \<noteq> []
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf])
valid_node m
valid_node m'
CFG_node m' \<in> S
ms' \<noteq> []

goal (1 subgoal):
 1. False
[PROOF STEP]
by(fastforce elim:silent_moves_nonempty_nodestack_False intro:refl_slice1)
[PROOF STATE]
proof (state)
this:
False

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

goal (2 subgoals):
 1. slice_edges S [] as = [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
 2. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with \<open>S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (m'#ms',transfers (kinds as) [cf])\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf])
ms' = []
[PROOF STEP]
have "S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> ([m'],transfers (kinds as) [cf])"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf])
ms' = []

goal (1 subgoal):
 1. S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> ([m'],transfers (kinds as) [cf])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> ([m'],transfers (kinds as) [cf])

goal (2 subgoals):
 1. slice_edges S [] as = [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
 2. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with \<open>valid_node m\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_node m
S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> ([m'],transfers (kinds as) [cf])
[PROOF STEP]
have "m -as'\<rightarrow>\<^bsub>sl\<^esub>* m'"
[PROOF STATE]
proof (prove)
using this:
valid_node m
S,kind \<turnstile> ([m],[cf]) =as'\<Rightarrow>\<^sub>\<tau> ([m'],transfers (kinds as) [cf])

goal (1 subgoal):
 1. m -as'\<rightarrow>\<^bsub>sl\<^esub>* m'
[PROOF STEP]
by(fastforce dest:silent_moves_slp)
[PROOF STATE]
proof (state)
this:
m -as'\<rightarrow>\<^bsub>sl\<^esub>* m'

goal (2 subgoals):
 1. slice_edges S [] as = [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
 2. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from this \<open>slice_edges S [] as' = []\<close>
[PROOF STATE]
proof (chain)
picking this:
m -as'\<rightarrow>\<^bsub>sl\<^esub>* m'
slice_edges S [] as' = []
[PROOF STEP]
obtain asx where "m -asx\<rightarrow>\<^sub>\<iota>* m'" and "slice_edges S [] asx = []"
[PROOF STATE]
proof (prove)
using this:
m -as'\<rightarrow>\<^bsub>sl\<^esub>* m'
slice_edges S [] as' = []

goal (1 subgoal):
 1. (\<And>asx. \<lbrakk>m -asx\<rightarrow>\<^sub>\<iota>* m'; slice_edges S [] asx = []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule slp_to_intra_path_with_slice_edges)
[PROOF STATE]
proof (state)
this:
m -asx\<rightarrow>\<^sub>\<iota>* m'
slice_edges S [] asx = []

goal (2 subgoals):
 1. slice_edges S [] as = [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
 2. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with \<open>CFG_node m' \<in> HRB_slice S\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node m' \<in> HRB_slice S
m -asx\<rightarrow>\<^sub>\<iota>* m'
slice_edges S [] asx = []
[PROOF STEP]
obtain asx' where "m -asx'\<rightarrow>\<^sub>\<iota>* m'"
      and "preds (slice_kinds S asx') [cf]"
      and "slice_edges S [] asx' = []"
[PROOF STATE]
proof (prove)
using this:
CFG_node m' \<in> HRB_slice S
m -asx\<rightarrow>\<^sub>\<iota>* m'
slice_edges S [] asx = []

goal (1 subgoal):
 1. (\<And>asx'. \<lbrakk>m -asx'\<rightarrow>\<^sub>\<iota>* m'; preds (slice_kinds S asx') [cf]; slice_edges S [] asx' = []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by -(erule exists_sliced_intra_path_preds,auto simp:SDG_to_CFG_set_def)
[PROOF STATE]
proof (state)
this:
m -asx'\<rightarrow>\<^sub>\<iota>* m'
preds (slice_kinds S asx') [cf]
slice_edges S [] asx' = []

goal (2 subgoals):
 1. slice_edges S [] as = [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
 2. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from \<open>m -asx'\<rightarrow>\<^sub>\<iota>* m'\<close>
[PROOF STATE]
proof (chain)
picking this:
m -asx'\<rightarrow>\<^sub>\<iota>* m'
[PROOF STEP]
have "m -asx'\<rightarrow>\<^sub>\<surd>* m'"
[PROOF STATE]
proof (prove)
using this:
m -asx'\<rightarrow>\<^sub>\<iota>* m'

goal (1 subgoal):
 1. m -asx'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
by(rule intra_path_vp)
[PROOF STATE]
proof (state)
this:
m -asx'\<rightarrow>\<^sub>\<surd>* m'

goal (2 subgoals):
 1. slice_edges S [] as = [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
 2. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from Uses \<open>slice_edges S [] asx' = []\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>V\<in>Use m'. state_val (transfers (kinds as) [cf]) V = fst cf V
slice_edges S [] asx' = []
[PROOF STEP]
have "hd (transfers (slice_kinds S
      (slice_edges S [] asx')) [cf]) = cf"
[PROOF STATE]
proof (prove)
using this:
\<forall>V\<in>Use m'. state_val (transfers (kinds as) [cf]) V = fst cf V
slice_edges S [] asx' = []

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

goal (2 subgoals):
 1. slice_edges S [] as = [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
 2. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from \<open>m -asx'\<rightarrow>\<^sub>\<iota>* m'\<close> \<open>CFG_node m' \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
m -asx'\<rightarrow>\<^sub>\<iota>* m'
CFG_node m' \<in> S
[PROOF STEP]
have "transfers (slice_kinds S (slice_edges S [] asx')) [cf] =
      transfers (slice_kinds S asx') [cf]"
[PROOF STATE]
proof (prove)
using this:
m -asx'\<rightarrow>\<^sub>\<iota>* m'
CFG_node m' \<in> S

goal (1 subgoal):
 1. transfers (slice_kinds S (slice_edges S [] asx')) [cf] = transfers (slice_kinds S asx') [cf]
[PROOF STEP]
by(fastforce intro:transfers_intra_slice_kinds_slice_edges simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
transfers (slice_kinds S (slice_edges S [] asx')) [cf] = transfers (slice_kinds S asx') [cf]

goal (2 subgoals):
 1. slice_edges S [] as = [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
 2. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with \<open>hd (transfers (slice_kinds S (slice_edges S [] asx')) [cf]) = cf\<close>
[PROOF STATE]
proof (chain)
picking this:
hd (transfers (slice_kinds S (slice_edges S [] asx')) [cf]) = cf
transfers (slice_kinds S (slice_edges S [] asx')) [cf] = transfers (slice_kinds S asx') [cf]
[PROOF STEP]
have "hd (transfers (slice_kinds S asx') [cf]) = cf"
[PROOF STATE]
proof (prove)
using this:
hd (transfers (slice_kinds S (slice_edges S [] asx')) [cf]) = cf
transfers (slice_kinds S (slice_edges S [] asx')) [cf] = transfers (slice_kinds S asx') [cf]

goal (1 subgoal):
 1. hd (transfers (slice_kinds S asx') [cf]) = cf
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hd (transfers (slice_kinds S asx') [cf]) = cf

goal (2 subgoals):
 1. slice_edges S [] as = [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
 2. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with Uses
[PROOF STATE]
proof (chain)
picking this:
\<forall>V\<in>Use m'. state_val (transfers (kinds as) [cf]) V = fst cf V
hd (transfers (slice_kinds S asx') [cf]) = cf
[PROOF STEP]
have "\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S asx') [cf]) V =
      state_val (transfers (kinds as) [cf]) V"
[PROOF STATE]
proof (prove)
using this:
\<forall>V\<in>Use m'. state_val (transfers (kinds as) [cf]) V = fst cf V
hd (transfers (slice_kinds S asx') [cf]) = cf

goal (1 subgoal):
 1. \<forall>V\<in>Use m'. state_val (transfers (slice_kinds S asx') [cf]) V = state_val (transfers (kinds as) [cf]) V
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S asx') [cf]) V = state_val (transfers (kinds as) [cf]) V

goal (2 subgoals):
 1. slice_edges S [] as = [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
 2. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with \<open>m -asx'\<rightarrow>\<^sub>\<surd>* m'\<close> \<open>preds (slice_kinds S asx') [cf]\<close>
      \<open>slice_edges S [] asx' = []\<close> \<open>transfers (kinds as) [cf] \<noteq> []\<close> True
[PROOF STATE]
proof (chain)
picking this:
m -asx'\<rightarrow>\<^sub>\<surd>* m'
preds (slice_kinds S asx') [cf]
slice_edges S [] asx' = []
transfers (kinds as) [cf] \<noteq> []
slice_edges S [] as = []
\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S asx') [cf]) V = state_val (transfers (kinds as) [cf]) V
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
m -asx'\<rightarrow>\<^sub>\<surd>* m'
preds (slice_kinds S asx') [cf]
slice_edges S [] asx' = []
transfers (kinds as) [cf] \<noteq> []
slice_edges S [] as = []
\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S asx') [cf]) V = state_val (transfers (kinds as) [cf]) V

goal (1 subgoal):
 1. \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
slice_edges S [] as \<noteq> []

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with \<open>(([m],[cf]),([m],[cf])) \<in> WS S\<close>
      \<open>S,kind \<turnstile> ([m],[cf]) =slice_edges S [] as\<Rightarrow>* (ms'',s'')\<close>
[PROOF STATE]
proof (chain)
picking this:
(([m], [cf]), [m], [cf]) \<in> WS S
S,kind \<turnstile> ([m],[cf]) =slice_edges S [] as\<Rightarrow>* (ms'',s'')
slice_edges S [] as \<noteq> []
[PROOF STEP]
have WS:"((ms'',s''),(ms'',transfers (slice_kinds S (slice_edges S [] as)) [cf]))
      \<in> WS S"
      and tom:"S,slice_kind S \<turnstile> ([m],[cf]) =slice_edges S [] as\<Rightarrow>*
      (ms'',transfers (slice_kinds S (slice_edges S [] as)) [cf])"
[PROOF STATE]
proof (prove)
using this:
(([m], [cf]), [m], [cf]) \<in> WS S
S,kind \<turnstile> ([m],[cf]) =slice_edges S [] as\<Rightarrow>* (ms'',s'')
slice_edges S [] as \<noteq> []

goal (1 subgoal):
 1. ((ms'', s''), ms'', transfers (slice_kinds S (slice_edges S [] as)) [cf]) \<in> WS S &&& S,slice_kind S \<turnstile> ([m],[cf]) =slice_edges S [] as\<Rightarrow>* (ms'',transfers (slice_kinds S (slice_edges S [] as)) [cf])
[PROOF STEP]
by(fastforce dest:WS_weak_sim_trans)+
[PROOF STATE]
proof (state)
this:
((ms'', s''), ms'', transfers (slice_kinds S (slice_edges S [] as)) [cf]) \<in> WS S
S,slice_kind S \<turnstile> ([m],[cf]) =slice_edges S [] as\<Rightarrow>* (ms'',transfers (slice_kinds S (slice_edges S [] as)) [cf])

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from WS
[PROOF STATE]
proof (chain)
picking this:
((ms'', s''), ms'', transfers (slice_kinds S (slice_edges S [] as)) [cf]) \<in> WS S
[PROOF STEP]
obtain mx msx where [simp]:"ms'' = mx#msx" and "valid_node mx"
[PROOF STATE]
proof (prove)
using this:
((ms'', s''), ms'', transfers (slice_kinds S (slice_edges S [] as)) [cf]) \<in> WS S

goal (1 subgoal):
 1. (\<And>mx msx. \<lbrakk>ms'' = mx # msx; valid_node mx\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by -(erule WS.cases,cases ms'',auto)
[PROOF STATE]
proof (state)
this:
ms'' = mx # msx
valid_node mx

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from \<open>S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m'#ms',transfers (kinds as) [cf])\<close> WS
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf])
((ms'', s''), ms'', transfers (slice_kinds S (slice_edges S [] as)) [cf]) \<in> WS S
[PROOF STEP]
have WS':"((m'#ms',transfers (kinds as) [cf]),
      (mx#msx,transfers (slice_kinds S (slice_edges S [] as)) [cf])) \<in> WS S"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf])
((ms'', s''), ms'', transfers (slice_kinds S (slice_edges S [] as)) [cf]) \<in> WS S

goal (1 subgoal):
 1. ((m' # ms', transfers (kinds as) [cf]), mx # msx, transfers (slice_kinds S (slice_edges S [] as)) [cf]) \<in> WS S
[PROOF STEP]
by simp(rule WS_silent_moves)
[PROOF STATE]
proof (state)
this:
((m' # ms', transfers (kinds as) [cf]), mx # msx, transfers (slice_kinds S (slice_edges S [] as)) [cf]) \<in> WS S

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from tom \<open>valid_node m\<close>
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> ([m],[cf]) =slice_edges S [] as\<Rightarrow>* (ms'',transfers (slice_kinds S (slice_edges S [] as)) [cf])
valid_node m
[PROOF STEP]
obtain asx csx rsx where "preds (slice_kinds S asx) [cf]"
      and "slice_edges S [] asx = slice_edges S [] as"
      and "m -asx\<rightarrow>\<^sub>\<surd>* mx" and "transfers (slice_kinds S asx) [cf] \<noteq> []"
      and "upd_cs [] asx = csx" and stack:"valid_node mx" "valid_call_list csx mx"
      "\<forall>i < length rsx. rsx!i \<in> get_return_edges (csx!i)"
      "valid_return_list rsx mx" "length rsx = length csx"
      "msx = targetnodes rsx"
      and trans_eq:"transfers (slice_kinds S
      (slice_edges S [] asx)) [cf] =
      transfers (slice_kinds S asx) [cf]"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> ([m],[cf]) =slice_edges S [] as\<Rightarrow>* (ms'',transfers (slice_kinds S (slice_edges S [] as)) [cf])
valid_node m

goal (1 subgoal):
 1. (\<And>asx csx rsx. \<lbrakk>preds (slice_kinds S asx) [cf]; slice_edges S [] asx = slice_edges S [] as; m -asx\<rightarrow>\<^sub>\<surd>* mx; transfers (slice_kinds S asx) [cf] \<noteq> []; upd_cs [] asx = csx; valid_node mx; valid_call_list csx mx; \<forall>i<length rsx. rsx ! i \<in> get_return_edges (csx ! i); valid_return_list rsx mx; length rsx = length csx; msx = targetnodes rsx; transfers (slice_kinds S (slice_edges S [] asx)) [cf] = transfers (slice_kinds S asx) [cf]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto elim:slice_tom_preds_vp[of _ _ _ _ _ _ _ _ "[]" "[]"]
              simp:valid_call_list_def valid_return_list_def targetnodes_def
                   vp_def valid_path_def)
[PROOF STATE]
proof (state)
this:
preds (slice_kinds S asx) [cf]
slice_edges S [] asx = slice_edges S [] as
m -asx\<rightarrow>\<^sub>\<surd>* mx
transfers (slice_kinds S asx) [cf] \<noteq> []
upd_cs [] asx = csx
valid_node mx
valid_call_list csx mx
\<forall>i<length rsx. rsx ! i \<in> get_return_edges (csx ! i)
valid_return_list rsx mx
length rsx = length csx
msx = targetnodes rsx
transfers (slice_kinds S (slice_edges S [] asx)) [cf] = transfers (slice_kinds S asx) [cf]

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from \<open>transfers (slice_kinds S asx) [cf] \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
transfers (slice_kinds S asx) [cf] \<noteq> []
[PROOF STEP]
obtain cf' cfs' where eq:"transfers (slice_kinds S asx) [cf] =
      cf'#cfs'"
[PROOF STATE]
proof (prove)
using this:
transfers (slice_kinds S asx) [cf] \<noteq> []

goal (1 subgoal):
 1. (\<And>cf' cfs'. transfers (slice_kinds S asx) [cf] = cf' # cfs' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases "transfers (slice_kinds S asx) [cf]") auto
[PROOF STATE]
proof (state)
this:
transfers (slice_kinds S asx) [cf] = cf' # cfs'

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from WS'
[PROOF STATE]
proof (chain)
picking this:
((m' # ms', transfers (kinds as) [cf]), mx # msx, transfers (slice_kinds S (slice_edges S [] as)) [cf]) \<in> WS S
[PROOF STEP]
have callstack:"\<forall>mx \<in> set msx. \<exists>mx'. call_of_return_node mx mx' \<and>
      mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
[PROOF STATE]
proof (prove)
using this:
((m' # ms', transfers (kinds as) [cf]), mx # msx, transfers (slice_kinds S (slice_edges S [] as)) [cf]) \<in> WS S

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

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with \<open>S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m'#ms',transfers (kinds as) [cf])\<close>
      \<open>valid_node m'\<close> stack \<open>CFG_node m' \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf])
valid_node m'
valid_node mx
valid_call_list csx mx
\<forall>i<length rsx. rsx ! i \<in> get_return_edges (csx ! i)
valid_return_list rsx mx
length rsx = length csx
msx = targetnodes rsx
CFG_node m' \<in> S
\<forall>mx\<in>set msx. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
have callstack':"\<forall>mx \<in> set 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,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf])
valid_node m'
valid_node mx
valid_call_list csx mx
\<forall>i<length rsx. rsx ! i \<in> get_return_edges (csx ! i)
valid_return_list rsx mx
length rsx = length csx
msx = targetnodes rsx
CFG_node m' \<in> S
\<forall>mx\<in>set msx. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. \<forall>mx\<in>set ms'. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
by simp(erule silent_moves_called_node_in_slice1_nodestack_in_slice1
        [of _ _ _ _ _ _ _ _ _ rsx csx],auto intro:refl_slice1)
[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. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with \<open>S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m'#ms',transfers (kinds as) [cf])\<close>
      stack callstack
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf])
valid_node mx
valid_call_list csx mx
\<forall>i<length rsx. rsx ! i \<in> get_return_edges (csx ! i)
valid_return_list rsx mx
length rsx = length csx
msx = targetnodes rsx
\<forall>mx\<in>set msx. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
\<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 "mx -as'\<rightarrow>\<^bsub>sl\<^esub>* m'" and "msx = ms'"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf])
valid_node mx
valid_call_list csx mx
\<forall>i<length rsx. rsx ! i \<in> get_return_edges (csx ! i)
valid_return_list rsx mx
length rsx = length csx
msx = targetnodes rsx
\<forall>mx\<in>set msx. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
\<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. mx -as'\<rightarrow>\<^bsub>sl\<^esub>* m' &&& msx = ms'
[PROOF STEP]
by(auto dest!:silent_moves_slp)
[PROOF STATE]
proof (state)
this:
mx -as'\<rightarrow>\<^bsub>sl\<^esub>* m'
msx = ms'

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from \<open>S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m'#ms',transfers (kinds as) [cf])\<close>
      stack
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf])
valid_node mx
valid_call_list csx mx
\<forall>i<length rsx. rsx ! i \<in> get_return_edges (csx ! i)
valid_return_list rsx mx
length rsx = length csx
msx = targetnodes rsx
[PROOF STEP]
have "slice_edges S csx as' = []"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',transfers (kinds as) [cf])
valid_node mx
valid_call_list csx mx
\<forall>i<length rsx. rsx ! i \<in> get_return_edges (csx ! i)
valid_return_list rsx mx
length rsx = length csx
msx = targetnodes rsx

goal (1 subgoal):
 1. slice_edges S csx as' = []
[PROOF STEP]
by(auto dest:silent_moves_no_slice_edges[OF _ _ _ stacks_rewrite])
[PROOF STATE]
proof (state)
this:
slice_edges S csx as' = []

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with \<open>mx -as'\<rightarrow>\<^bsub>sl\<^esub>* m'\<close>
[PROOF STATE]
proof (chain)
picking this:
mx -as'\<rightarrow>\<^bsub>sl\<^esub>* m'
slice_edges S csx as' = []
[PROOF STEP]
obtain asx'' where "mx -asx''\<rightarrow>\<^sub>\<iota>* m'"
      and "slice_edges S csx asx'' = []"
[PROOF STATE]
proof (prove)
using this:
mx -as'\<rightarrow>\<^bsub>sl\<^esub>* m'
slice_edges S csx as' = []

goal (1 subgoal):
 1. (\<And>asx''. \<lbrakk>mx -asx''\<rightarrow>\<^sub>\<iota>* m'; slice_edges S csx asx'' = []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule slp_to_intra_path_with_slice_edges)
[PROOF STATE]
proof (state)
this:
mx -asx''\<rightarrow>\<^sub>\<iota>* m'
slice_edges S csx asx'' = []

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from stack
[PROOF STATE]
proof (chain)
picking this:
valid_node mx
valid_call_list csx mx
\<forall>i<length rsx. rsx ! i \<in> get_return_edges (csx ! i)
valid_return_list rsx mx
length rsx = length csx
msx = targetnodes rsx
[PROOF STEP]
have "\<forall>i<length csx. call_of_return_node (msx!i) (sourcenode (csx!i))"
[PROOF STATE]
proof (prove)
using this:
valid_node mx
valid_call_list csx mx
\<forall>i<length rsx. rsx ! i \<in> get_return_edges (csx ! i)
valid_return_list rsx mx
length rsx = length csx
msx = targetnodes rsx

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

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with callstack \<open>msx = targetnodes rsx\<close> \<open>length rsx = length csx\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>mx\<in>set msx. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
msx = targetnodes rsx
length rsx = length csx
\<forall>i<length csx. call_of_return_node (msx ! i) (sourcenode (csx ! i))
[PROOF STEP]
have "\<forall>c\<in>set csx. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<forall>mx\<in>set msx. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
msx = targetnodes rsx
length rsx = length csx
\<forall>i<length csx. call_of_return_node (msx ! i) (sourcenode (csx ! i))

goal (1 subgoal):
 1. \<forall>c\<in>set csx. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
by(auto simp:all_set_conv_all_nth targetnodes_def)
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>set csx. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with \<open>mx -asx''\<rightarrow>\<^sub>\<iota>* m'\<close> \<open>slice_edges S csx asx'' = []\<close> \<open>valid_node m'\<close>
      eq \<open>CFG_node m' \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
mx -asx''\<rightarrow>\<^sub>\<iota>* m'
slice_edges S csx asx'' = []
valid_node m'
transfers (slice_kinds S asx) [cf] = cf' # cfs'
CFG_node m' \<in> S
\<forall>c\<in>set csx. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
obtain asx' where "mx -asx'\<rightarrow>\<^sub>\<iota>* m'"
      and "preds (slice_kinds S asx') (cf'#cfs')"
      and "slice_edges S csx asx' = []"
[PROOF STATE]
proof (prove)
using this:
mx -asx''\<rightarrow>\<^sub>\<iota>* m'
slice_edges S csx asx'' = []
valid_node m'
transfers (slice_kinds S asx) [cf] = cf' # cfs'
CFG_node m' \<in> S
\<forall>c\<in>set csx. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. (\<And>asx'. \<lbrakk>mx -asx'\<rightarrow>\<^sub>\<iota>* m'; preds (slice_kinds S asx') (cf' # cfs'); slice_edges S csx asx' = []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by -(erule exists_sliced_intra_path_preds,
        auto intro:HRB_slice_refl simp:SDG_to_CFG_set_def)
[PROOF STATE]
proof (state)
this:
mx -asx'\<rightarrow>\<^sub>\<iota>* m'
preds (slice_kinds S asx') (cf' # cfs')
slice_edges S csx asx' = []

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with eq
[PROOF STATE]
proof (chain)
picking this:
transfers (slice_kinds S asx) [cf] = cf' # cfs'
mx -asx'\<rightarrow>\<^sub>\<iota>* m'
preds (slice_kinds S asx') (cf' # cfs')
slice_edges S csx asx' = []
[PROOF STEP]
have "preds (slice_kinds S asx')
      (transfers (slice_kinds S asx) [cf])"
[PROOF STATE]
proof (prove)
using this:
transfers (slice_kinds S asx) [cf] = cf' # cfs'
mx -asx'\<rightarrow>\<^sub>\<iota>* m'
preds (slice_kinds S asx') (cf' # cfs')
slice_edges S csx asx' = []

goal (1 subgoal):
 1. preds (slice_kinds S asx') (transfers (slice_kinds S asx) [cf])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
preds (slice_kinds S asx') (transfers (slice_kinds S asx) [cf])

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with \<open>preds (slice_kinds S asx) [cf]\<close>
[PROOF STATE]
proof (chain)
picking this:
preds (slice_kinds S asx) [cf]
preds (slice_kinds S asx') (transfers (slice_kinds S asx) [cf])
[PROOF STEP]
have "preds (slice_kinds S (asx@asx')) [cf]"
[PROOF STATE]
proof (prove)
using this:
preds (slice_kinds S asx) [cf]
preds (slice_kinds S asx') (transfers (slice_kinds S asx) [cf])

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

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from \<open>m -asx\<rightarrow>\<^sub>\<surd>* mx\<close> \<open>mx -asx'\<rightarrow>\<^sub>\<iota>* m'\<close>
[PROOF STATE]
proof (chain)
picking this:
m -asx\<rightarrow>\<^sub>\<surd>* mx
mx -asx'\<rightarrow>\<^sub>\<iota>* m'
[PROOF STEP]
have "m -asx@asx'\<rightarrow>\<^sub>\<surd>* m'"
[PROOF STATE]
proof (prove)
using this:
m -asx\<rightarrow>\<^sub>\<surd>* mx
mx -asx'\<rightarrow>\<^sub>\<iota>* m'

goal (1 subgoal):
 1. m -asx @ asx'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
by(fastforce elim:vp_slp_Append intra_path_slp)
[PROOF STATE]
proof (state)
this:
m -asx @ asx'\<rightarrow>\<^sub>\<surd>* m'

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from \<open>upd_cs [] asx = csx\<close> \<open>slice_edges S csx asx' = []\<close>
[PROOF STATE]
proof (chain)
picking this:
upd_cs [] asx = csx
slice_edges S csx asx' = []
[PROOF STEP]
have "slice_edges S [] (asx@asx') =
      (slice_edges S [] asx)@[]"
[PROOF STATE]
proof (prove)
using this:
upd_cs [] asx = csx
slice_edges S csx asx' = []

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

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from \<open>mx -asx'\<rightarrow>\<^sub>\<iota>* m'\<close> \<open>\<forall>c\<in>set csx. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
mx -asx'\<rightarrow>\<^sub>\<iota>* m'
\<forall>c\<in>set csx. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
have trans_eq':"transfers (slice_kinds S (slice_edges S csx asx'))
          (transfers (slice_kinds S asx) [cf]) =
      transfers (slice_kinds S asx') (transfers (slice_kinds S asx) [cf])"
[PROOF STATE]
proof (prove)
using this:
mx -asx'\<rightarrow>\<^sub>\<iota>* m'
\<forall>c\<in>set csx. sourcenode c \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. transfers (slice_kinds S (slice_edges S csx asx')) (transfers (slice_kinds S asx) [cf]) = transfers (slice_kinds S asx') (transfers (slice_kinds S asx) [cf])
[PROOF STEP]
by(fastforce intro:transfers_intra_slice_kinds_slice_edges simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
transfers (slice_kinds S (slice_edges S csx asx')) (transfers (slice_kinds S asx) [cf]) = transfers (slice_kinds S asx') (transfers (slice_kinds S asx) [cf])

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from \<open>upd_cs [] asx = csx\<close>
[PROOF STATE]
proof (chain)
picking this:
upd_cs [] asx = csx
[PROOF STEP]
have "slice_edges S [] (asx@asx') =
      (slice_edges S [] asx)@(slice_edges S csx asx')"
[PROOF STATE]
proof (prove)
using this:
upd_cs [] asx = csx

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

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
hence "transfers (slice_kinds S (slice_edges S [] (asx@asx'))) [cf] =
      transfers (slice_kinds S (slice_edges S csx asx'))
        (transfers (slice_kinds S (slice_edges S [] asx)) [cf])"
[PROOF STATE]
proof (prove)
using this:
slice_edges S [] (asx @ asx') = slice_edges S [] asx @ slice_edges S csx asx'

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

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with trans_eq
[PROOF STATE]
proof (chain)
picking this:
transfers (slice_kinds S (slice_edges S [] asx)) [cf] = transfers (slice_kinds S asx) [cf]
transfers (slice_kinds S (slice_edges S [] (asx @ asx'))) [cf] = transfers (slice_kinds S (slice_edges S csx asx')) (transfers (slice_kinds S (slice_edges S [] asx)) [cf])
[PROOF STEP]
have "transfers (slice_kinds S (slice_edges S [] (asx@asx'))) [cf] =
      transfers (slice_kinds S (slice_edges S csx asx'))
        (transfers (slice_kinds S asx) [cf])"
[PROOF STATE]
proof (prove)
using this:
transfers (slice_kinds S (slice_edges S [] asx)) [cf] = transfers (slice_kinds S asx) [cf]
transfers (slice_kinds S (slice_edges S [] (asx @ asx'))) [cf] = transfers (slice_kinds S (slice_edges S csx asx')) (transfers (slice_kinds S (slice_edges S [] asx)) [cf])

goal (1 subgoal):
 1. transfers (slice_kinds S (slice_edges S [] (asx @ asx'))) [cf] = transfers (slice_kinds S (slice_edges S csx asx')) (transfers (slice_kinds S asx) [cf])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
transfers (slice_kinds S (slice_edges S [] (asx @ asx'))) [cf] = transfers (slice_kinds S (slice_edges S csx asx')) (transfers (slice_kinds S asx) [cf])

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with trans_eq'
[PROOF STATE]
proof (chain)
picking this:
transfers (slice_kinds S (slice_edges S csx asx')) (transfers (slice_kinds S asx) [cf]) = transfers (slice_kinds S asx') (transfers (slice_kinds S asx) [cf])
transfers (slice_kinds S (slice_edges S [] (asx @ asx'))) [cf] = transfers (slice_kinds S (slice_edges S csx asx')) (transfers (slice_kinds S asx) [cf])
[PROOF STEP]
have trans_eq'':
      "transfers (slice_kinds S (slice_edges S [] (asx@asx'))) [cf] =
      transfers (slice_kinds S (asx@asx')) [cf]"
[PROOF STATE]
proof (prove)
using this:
transfers (slice_kinds S (slice_edges S csx asx')) (transfers (slice_kinds S asx) [cf]) = transfers (slice_kinds S asx') (transfers (slice_kinds S asx) [cf])
transfers (slice_kinds S (slice_edges S [] (asx @ asx'))) [cf] = transfers (slice_kinds S (slice_edges S csx asx')) (transfers (slice_kinds S asx) [cf])

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

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from WS'
[PROOF STATE]
proof (chain)
picking this:
((m' # ms', transfers (kinds as) [cf]), mx # msx, transfers (slice_kinds S (slice_edges S [] as)) [cf]) \<in> WS S
[PROOF STEP]
obtain x xs where "m'#ms' = xs@x#msx"
      and "xs \<noteq> [] \<longrightarrow> (\<exists>mx'. call_of_return_node x mx' \<and>
      mx' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>)"
      and rest:"\<forall>i < length (mx#msx). \<forall>V \<in> rv S (CFG_node ((x#msx)!i)).
      (fst ((transfers (kinds as) [cf])!(length xs + i))) V =
      (fst ((transfers (slice_kinds S
      (slice_edges S [] as)) [cf])!i)) V"
      "transfers (kinds as) [cf] \<noteq> []"
      "transfers (slice_kinds S
      (slice_edges S [] as)) [cf] \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
((m' # ms', transfers (kinds as) [cf]), mx # msx, transfers (slice_kinds S (slice_edges S [] as)) [cf]) \<in> WS S

goal (1 subgoal):
 1. (\<And>xs x. \<lbrakk>m' # ms' = xs @ x # msx; xs \<noteq> [] \<longrightarrow> (\<exists>mx'. call_of_return_node x mx' \<and> mx' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>); \<forall>i<length (mx # msx). \<forall>V\<in>rv S (CFG_node ((x # msx) ! i)). fst (transfers (kinds as) [cf] ! (length xs + i)) V = fst (transfers (slice_kinds S (slice_edges S [] as)) [cf] ! i) V; transfers (kinds as) [cf] \<noteq> []; transfers (slice_kinds S (slice_edges S [] as)) [cf] \<noteq> []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:WS.cases)
[PROOF STATE]
proof (state)
this:
m' # ms' = xs @ x # msx
xs \<noteq> [] \<longrightarrow> (\<exists>mx'. call_of_return_node x mx' \<and> mx' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>)
\<forall>i<length (mx # msx). \<forall>V\<in>rv S (CFG_node ((x # msx) ! i)). fst (transfers (kinds as) [cf] ! (length xs + i)) V = fst (transfers (slice_kinds S (slice_edges S [] as)) [cf] ! i) V
transfers (kinds as) [cf] \<noteq> []
transfers (slice_kinds S (slice_edges S [] as)) [cf] \<noteq> []

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from \<open>m'#ms' = xs@x#msx\<close> \<open>xs \<noteq> [] \<longrightarrow> (\<exists>mx'. call_of_return_node x mx' \<and>
      mx' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>)\<close> callstack'
[PROOF STATE]
proof (chain)
picking this:
m' # ms' = xs @ x # msx
xs \<noteq> [] \<longrightarrow> (\<exists>mx'. call_of_return_node x mx' \<and> mx' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>)
\<forall>mx\<in>set ms'. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
have [simp]:"xs = []" "x = m'" "ms' = msx"
[PROOF STATE]
proof (prove)
using this:
m' # ms' = xs @ x # msx
xs \<noteq> [] \<longrightarrow> (\<exists>mx'. call_of_return_node x mx' \<and> mx' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>)
\<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. xs = [] &&& x = m' &&& ms' = msx
[PROOF STEP]
by(cases xs,auto)+
[PROOF STATE]
proof (state)
this:
xs = []
x = m'
ms' = msx

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from rest
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length (mx # msx). \<forall>V\<in>rv S (CFG_node ((x # msx) ! i)). fst (transfers (kinds as) [cf] ! (length xs + i)) V = fst (transfers (slice_kinds S (slice_edges S [] as)) [cf] ! i) V
transfers (kinds as) [cf] \<noteq> []
transfers (slice_kinds S (slice_edges S [] as)) [cf] \<noteq> []
[PROOF STEP]
have "\<forall>V \<in> rv S (CFG_node m').
      state_val (transfers (kinds as) [cf]) V =
      state_val (transfers (slice_kinds S (slice_edges S [] as)) [cf]) V"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length (mx # msx). \<forall>V\<in>rv S (CFG_node ((x # msx) ! i)). fst (transfers (kinds as) [cf] ! (length xs + i)) V = fst (transfers (slice_kinds S (slice_edges S [] as)) [cf] ! i) V
transfers (kinds as) [cf] \<noteq> []
transfers (slice_kinds S (slice_edges S [] as)) [cf] \<noteq> []

goal (1 subgoal):
 1. \<forall>V\<in>rv S (CFG_node m'). state_val (transfers (kinds as) [cf]) V = state_val (transfers (slice_kinds S (slice_edges S [] as)) [cf]) V
[PROOF STEP]
by(fastforce dest:hd_conv_nth)
[PROOF STATE]
proof (state)
this:
\<forall>V\<in>rv S (CFG_node m'). state_val (transfers (kinds as) [cf]) V = state_val (transfers (slice_kinds S (slice_edges S [] as)) [cf]) V

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with \<open>\<forall>V \<in> Use m'. V \<in> rv S (CFG_node m')\<close>
      \<open>slice_edges S [] asx = slice_edges S [] as\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>V\<in>Use m'. V \<in> rv S (CFG_node m')
slice_edges S [] asx = slice_edges S [] as
\<forall>V\<in>rv S (CFG_node m'). state_val (transfers (kinds as) [cf]) V = state_val (transfers (slice_kinds S (slice_edges S [] as)) [cf]) V
[PROOF STEP]
have "\<forall>V \<in> Use m'. state_val (transfers (kinds as) [cf]) V =
      state_val (transfers (slice_kinds S (slice_edges S [] asx)) [cf]) V"
[PROOF STATE]
proof (prove)
using this:
\<forall>V\<in>Use m'. V \<in> rv S (CFG_node m')
slice_edges S [] asx = slice_edges S [] as
\<forall>V\<in>rv S (CFG_node m'). state_val (transfers (kinds as) [cf]) V = state_val (transfers (slice_kinds S (slice_edges S [] as)) [cf]) V

goal (1 subgoal):
 1. \<forall>V\<in>Use m'. state_val (transfers (kinds as) [cf]) V = state_val (transfers (slice_kinds S (slice_edges S [] asx)) [cf]) V
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>V\<in>Use m'. state_val (transfers (kinds as) [cf]) V = state_val (transfers (slice_kinds S (slice_edges S [] asx)) [cf]) V

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with \<open>slice_edges S [] (asx@asx') = (slice_edges S [] asx)@[]\<close>
[PROOF STATE]
proof (chain)
picking this:
slice_edges S [] (asx @ asx') = slice_edges S [] asx @ []
\<forall>V\<in>Use m'. state_val (transfers (kinds as) [cf]) V = state_val (transfers (slice_kinds S (slice_edges S [] asx)) [cf]) V
[PROOF STEP]
have "\<forall>V \<in> Use m'. state_val (transfers (kinds as) [cf]) V =
      state_val (transfers (slice_kinds S (slice_edges S [] (asx@asx'))) [cf]) V"
[PROOF STATE]
proof (prove)
using this:
slice_edges S [] (asx @ asx') = slice_edges S [] asx @ []
\<forall>V\<in>Use m'. state_val (transfers (kinds as) [cf]) V = state_val (transfers (slice_kinds S (slice_edges S [] asx)) [cf]) V

goal (1 subgoal):
 1. \<forall>V\<in>Use m'. state_val (transfers (kinds as) [cf]) V = state_val (transfers (slice_kinds S (slice_edges S [] (asx @ asx'))) [cf]) V
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>V\<in>Use m'. state_val (transfers (kinds as) [cf]) V = state_val (transfers (slice_kinds S (slice_edges S [] (asx @ asx'))) [cf]) V

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with trans_eq''
[PROOF STATE]
proof (chain)
picking this:
transfers (slice_kinds S (slice_edges S [] (asx @ asx'))) [cf] = transfers (slice_kinds S (asx @ asx')) [cf]
\<forall>V\<in>Use m'. state_val (transfers (kinds as) [cf]) V = state_val (transfers (slice_kinds S (slice_edges S [] (asx @ asx'))) [cf]) V
[PROOF STEP]
have "\<forall>V \<in> Use m'. state_val (transfers (kinds as) [cf]) V =
      state_val (transfers (slice_kinds S (asx@asx')) [cf]) V"
[PROOF STATE]
proof (prove)
using this:
transfers (slice_kinds S (slice_edges S [] (asx @ asx'))) [cf] = transfers (slice_kinds S (asx @ asx')) [cf]
\<forall>V\<in>Use m'. state_val (transfers (kinds as) [cf]) V = state_val (transfers (slice_kinds S (slice_edges S [] (asx @ asx'))) [cf]) V

goal (1 subgoal):
 1. \<forall>V\<in>Use m'. state_val (transfers (kinds as) [cf]) V = state_val (transfers (slice_kinds S (asx @ asx')) [cf]) V
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>V\<in>Use m'. state_val (transfers (kinds as) [cf]) V = state_val (transfers (slice_kinds S (asx @ asx')) [cf]) V

goal (1 subgoal):
 1. slice_edges S [] as \<noteq> [] \<Longrightarrow> \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
with \<open>preds (slice_kinds S (asx@asx')) [cf]\<close>
      \<open>m -asx@asx'\<rightarrow>\<^sub>\<surd>* m'\<close> \<open>slice_edges S [] (asx@asx') =
      (slice_edges S [] asx)@[]\<close> \<open>transfers (kinds as) [cf] \<noteq> []\<close>
      \<open>slice_edges S [] asx = slice_edges S [] as\<close>
[PROOF STATE]
proof (chain)
picking this:
preds (slice_kinds S (asx @ asx')) [cf]
m -asx @ asx'\<rightarrow>\<^sub>\<surd>* m'
slice_edges S [] (asx @ asx') = slice_edges S [] asx @ []
transfers (kinds as) [cf] \<noteq> []
slice_edges S [] asx = slice_edges S [] as
\<forall>V\<in>Use m'. state_val (transfers (kinds as) [cf]) V = state_val (transfers (slice_kinds S (asx @ asx')) [cf]) V
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
preds (slice_kinds S (asx @ asx')) [cf]
m -asx @ asx'\<rightarrow>\<^sub>\<surd>* m'
slice_edges S [] (asx @ asx') = slice_edges S [] asx @ []
transfers (kinds as) [cf] \<noteq> []
slice_edges S [] asx = slice_edges S [] as
\<forall>V\<in>Use m'. state_val (transfers (kinds as) [cf]) V = state_val (transfers (slice_kinds S (asx @ asx')) [cf]) V

goal (1 subgoal):
 1. \<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>as'. preds (slice_kinds S as') [cf] \<and> (\<forall>V\<in>Use m'. state_val (transfers (slice_kinds S as') [cf]) V = state_val (transfers (kinds as) [cf]) V) \<and> slice_edges S [] as = slice_edges S [] as' \<and> transfers (kinds as) [cf] \<noteq> [] \<and> m -as'\<rightarrow>\<^sub>\<surd>* m'

goal:
No subgoals!
[PROOF STEP]
qed