Theory FundamentalProperty

section ‹The fundamental property of slicing›

theory FundamentalProperty imports WeakSimulation SemanticsCFG begin

context SDG begin

subsection ‹Auxiliary lemmas for moves in the graph›

lemma observable_set_stack_in_slice:
  "S,f ⊢ (ms,s) -a→ (ms',s') 
  ⟹ ∀mx ∈ set (tl ms'). ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
proof(induct rule:observable_move.induct)
  case (observable_move_intra f a s s' ms S ms') thus ?case by simp
next
  case (observable_move_call f a s s' Q r p fs a' ms S ms')
  from ‹valid_edge a› ‹valid_edge a'› ‹a' ∈ get_return_edges a›
  have "call_of_return_node (targetnode a') (sourcenode a)"
    by(fastforce simp:return_node_def call_of_return_node_def)
  with ‹hd ms = sourcenode a› ‹hd ms ∈ ⌊HRB_slice S⌋⇘CFG⇙› 
    ‹ms' = targetnode a # targetnode a' # tl ms›
    ‹∀mx∈set (tl ms). ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
  show ?case by fastforce
next
  case (observable_move_return f a s s' Q p f' ms S ms')
  thus ?case by(cases "tl ms") auto
qed


lemma silent_move_preserves_stacks:
  assumes "S,f ⊢ (m#ms,s) -a→⇩τ (m'#ms',s')" and "valid_call_list cs m"
  and "∀i < length rs. rs!i ∈ get_return_edges (cs!i)" and "valid_return_list rs m"
  and "length rs = length cs" and "ms = targetnodes rs"
  obtains cs' rs' where "valid_node m'" and "valid_call_list cs' m'"
  and "∀i < length rs'. rs'!i ∈ get_return_edges (cs'!i)"
  and "valid_return_list rs' m'" and "length rs' = length cs'" 
  and "ms' = targetnodes rs'" and "upd_cs cs [a] = cs'"
proof(atomize_elim)
  from assms show "∃cs' rs'. valid_node m' ∧ valid_call_list cs' m' ∧
    (∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)) ∧
    valid_return_list rs' m' ∧ length rs' = length cs' ∧ ms' = targetnodes rs' ∧
    upd_cs cs [a] = cs'"
  proof(induct S f "m#ms" s a "m'#ms'" s' rule:silent_move.induct)
    case (silent_move_intra f a s s' n⇩c)
    from ‹hd (m # ms) = sourcenode a› have "m = sourcenode a" by simp
    from ‹m' # ms' = targetnode a # tl (m # ms)›
    have [simp]:"m' = targetnode a" "ms' = ms" by simp_all
    from ‹valid_edge a› have "valid_node m'" by simp
    moreover
    from ‹valid_edge a› ‹intra_kind (kind a)›
    have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
    from ‹valid_call_list cs m› ‹m = sourcenode a›
      ‹get_proc (sourcenode a) = get_proc (targetnode a)›
    have "valid_call_list cs m'"
      apply(clarsimp simp:valid_call_list_def)
      apply(erule_tac x="cs'" in allE)
      apply(erule_tac x="c" in allE)
      by(auto split:list.split)
    moreover
    from ‹valid_return_list rs m› ‹m = sourcenode a› 
      ‹get_proc (sourcenode a) = get_proc (targetnode a)›
    have "valid_return_list rs m'"
      apply(clarsimp simp:valid_return_list_def)
      apply(erule_tac x="cs'" in allE) apply clarsimp
      by(case_tac cs') auto
    moreover
    from ‹intra_kind (kind a)› have "upd_cs cs [a] = cs"
      by(fastforce simp:intra_kind_def)
    ultimately show ?case using ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)›
      ‹length rs = length cs› ‹ms = targetnodes rs›
      apply(rule_tac x="cs" in exI)
      apply(rule_tac x="rs" in exI) 
      by clarsimp
  next
    case (silent_move_call f a s s' Q r p fs a' S)
    from ‹hd (m # ms) = sourcenode a› 
      ‹m' # ms' = targetnode a # targetnode a' # tl (m # ms)›
    have [simp]:"m = sourcenode a" "m' = targetnode a" 
      "ms' = targetnode a' # tl (m # ms)"
      by simp_all
    from ‹valid_edge a› have "valid_node m'" by simp
    moreover
    from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc (targetnode a) = p"
      by(rule get_proc_call)
    with ‹valid_call_list cs m› ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹m = sourcenode a›
    have "valid_call_list (a # cs) (targetnode a)"
      apply(clarsimp simp:valid_call_list_def)
      apply(case_tac cs') apply auto
      apply(erule_tac x="list" in allE)
      by(case_tac list)(auto simp:sourcenodes_def)
    moreover
    from ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)› ‹a' ∈ get_return_edges a›
    have "∀i<length (a'#rs). (a'#rs) ! i ∈ get_return_edges ((a#cs) ! i)"
      by auto(case_tac i,auto)
    moreover
    from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'" 
      by(rule get_return_edges_valid)
    from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹a' ∈ get_return_edges a›
    obtain Q' f' where "kind a' = Q'↩⇘p⇙f'" by(fastforce dest!:call_return_edges)
    from ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'› have "get_proc (sourcenode a') = p"
      by(rule get_proc_return)
    from ‹valid_edge a› ‹a' ∈ get_return_edges a›
    have "get_proc (sourcenode a) = get_proc (targetnode a')" 
      by(rule get_proc_get_return_edge)
    with ‹valid_return_list rs m› ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'›
      ‹get_proc (sourcenode a') = p› ‹get_proc (targetnode a) = p› ‹m = sourcenode a›
    have "valid_return_list (a'#rs) (targetnode a)"
      apply(clarsimp simp:valid_return_list_def)
      apply(case_tac cs') apply auto
      apply(erule_tac x="list" in allE)
      by(case_tac list)(auto simp:targetnodes_def)
    moreover
    from ‹length rs = length cs› have "length (a'#rs) = length (a#cs)" by simp
    moreover
    from ‹ms = targetnodes rs› have "targetnode a' # ms = targetnodes (a' # rs)"
      by(simp add:targetnodes_def)
    moreover
    from ‹kind a = Q:r↪⇘p⇙fs› have "upd_cs cs [a] = a#cs" by simp
    ultimately show ?case
      apply(rule_tac x="a#cs" in exI)
      apply(rule_tac x="a'#rs" in exI)
      by clarsimp
  next
    case (silent_move_return f a s s' Q p f' S)
    from ‹hd (m # ms) = sourcenode a›
      ‹hd (tl (m # ms)) = targetnode a› ‹m' # ms' = tl (m # ms)› [symmetric]
    have [simp]:"m = sourcenode a" "m' = targetnode a" by simp_all
    from ‹length (m # ms) = length s› ‹length s = Suc (length s')› ‹s' ≠ []›
      ‹hd (tl (m # ms)) = targetnode a› ‹m' # ms' = tl (m # ms)›
    have "ms = targetnode a # ms'" 
      by(cases ms) auto
    with ‹ms = targetnodes rs›
    obtain r' rs' where "rs = r' # rs'" 
      and "targetnode a = targetnode r'" and "ms' = targetnodes rs'" 
      by(cases rs)(auto simp:targetnodes_def)
    moreover
    from ‹rs = r' # rs'› ‹length rs = length cs› obtain c' cs' where "cs = c' # cs'"
      and "length rs' = length cs'" by(cases cs) auto
    moreover
    from ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)› 
      ‹rs = r' # rs'› ‹cs = c' # cs'›
    have "∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)"
      and "r' ∈ get_return_edges c'" by auto
    moreover
    from ‹valid_edge a› have "valid_node (targetnode a)" by simp
    moreover
    from ‹valid_call_list cs m› ‹cs = c' # cs'›
    obtain p' Q' r fs' where "valid_edge c'" and "kind c' = Q':r↪⇘p'⇙fs'" 
      and "p' = get_proc m"
      apply(auto simp:valid_call_list_def)
      by(erule_tac x="[]" in allE) auto
    from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f'›
    have "get_proc (sourcenode a) = p" by(rule get_proc_return)
    with ‹p' = get_proc m› have [simp]:"p' = p" by simp
    from ‹valid_edge c'› ‹kind c' = Q':r↪⇘p'⇙fs'›
    have "get_proc (targetnode c') = p" by(fastforce intro:get_proc_call)
    from ‹valid_edge c'› ‹r' ∈ get_return_edges c'› have "valid_edge r'"
      by(rule get_return_edges_valid)
    from ‹valid_edge c'› ‹kind c' = Q':r↪⇘p'⇙fs'› ‹r' ∈ get_return_edges c'›
    obtain Q'' f'' where "kind r' = Q''↩⇘p⇙f''" by(fastforce dest!:call_return_edges)
    with ‹valid_edge r'› have "get_proc (sourcenode r') = p" by(rule get_proc_return)
    from ‹valid_edge r'› ‹kind r' = Q''↩⇘p⇙f''› have "method_exit (sourcenode r')" 
      by(fastforce simp:method_exit_def)
    from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f'› have "method_exit (sourcenode a)" 
      by(fastforce simp:method_exit_def)
    with ‹method_exit (sourcenode r')› ‹get_proc (sourcenode r') = p› 
      ‹get_proc (sourcenode a) = p›
    have "sourcenode a = sourcenode r'" by(fastforce intro:method_exit_unique)
    with ‹valid_edge a› ‹valid_edge r'› ‹targetnode a = targetnode r'›
    have "a = r'" by(fastforce intro:edge_det)
    from ‹valid_edge c'› ‹r' ∈ get_return_edges c'› ‹targetnode a = targetnode r'›
    have "get_proc (sourcenode c') = get_proc (targetnode a)"
      by(fastforce intro:get_proc_get_return_edge)
    from ‹valid_call_list cs m› ‹cs = c' # cs'›
      ‹get_proc (sourcenode c') = get_proc (targetnode a)›
    have "valid_call_list cs' (targetnode a)"
      apply(clarsimp simp:valid_call_list_def)
      apply(hypsubst_thin)
      apply(erule_tac x="c' # cs'" in allE)
      by(case_tac cs')(auto simp:sourcenodes_def)
    moreover
    from ‹valid_return_list rs m› ‹rs = r' # rs'› ‹targetnode a = targetnode r'›
    have "valid_return_list rs' (targetnode a)"
      apply(clarsimp simp:valid_return_list_def)
      apply(erule_tac x="r' # cs'" in allE)
      by(case_tac cs')(auto simp:targetnodes_def)
    moreover
    from ‹kind a = Q↩⇘p⇙f'› ‹cs = c' # cs'› have "upd_cs cs [a] = cs'" by simp
    ultimately show ?case
      apply(rule_tac x="cs'" in exI)
      apply(rule_tac x="rs'" in exI)
      by clarsimp
  qed
qed


lemma silent_moves_preserves_stacks:
  assumes "S,f ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')" 
  and "valid_node m" and "valid_call_list cs m"
  and "∀i < length rs. rs!i ∈ get_return_edges (cs!i)" and "valid_return_list rs m"
  and "length rs = length cs" and "ms = targetnodes rs"
  obtains cs' rs' where "valid_node m'" and "valid_call_list cs' m'"
  and "∀i < length rs'. rs'!i ∈ get_return_edges (cs'!i)"
  and "valid_return_list rs' m'" and "length rs' = length cs'" 
  and "ms' = targetnodes rs'" and "upd_cs cs as = cs'"
proof(atomize_elim)
  from assms show "∃cs' rs'. valid_node m' ∧ valid_call_list cs' m' ∧
    (∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)) ∧
    valid_return_list rs' m' ∧ length rs' = length cs' ∧ ms' = targetnodes rs' ∧
    upd_cs cs as = cs'"
  proof(induct S f "m#ms" s as "m'#ms'" s' 
      arbitrary:m ms cs rs rule:silent_moves.induct)
    case (silent_moves_Nil s n⇩c f)
    thus ?case
      apply(rule_tac x="cs" in exI)
      apply(rule_tac x="rs" in exI)
      by clarsimp
  next
    case (silent_moves_Cons S f s a msx'' s'' as sx')
    note IH = ‹⋀m ms cs rs. ⟦msx'' = m # ms; valid_node m; valid_call_list cs m;
      ∀i<length rs. rs ! i ∈ get_return_edges (cs ! i);
      valid_return_list rs m; length rs = length cs; ms = targetnodes rs⟧
      ⟹ ∃cs' rs'. valid_node m' ∧ valid_call_list cs' m' ∧
      (∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)) ∧
      valid_return_list rs' m' ∧ length rs' = length cs' ∧ ms' = targetnodes rs' ∧
      upd_cs cs as = cs'›
    from ‹S,f ⊢ (m # ms,s) -a→⇩τ (msx'',s'')›
    obtain m'' ms'' where "msx'' = m''#ms''"
      by(cases msx'')(auto elim:silent_move.cases)
    with ‹S,f ⊢ (m # ms,s) -a→⇩τ (msx'',s'')› ‹valid_call_list cs m›
      ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)› ‹valid_return_list rs m›
      ‹length rs = length cs› ‹ms = targetnodes rs›
    obtain cs'' rs'' where hyps:"valid_node m''" "valid_call_list cs'' m''"
      "∀i < length rs''. rs''!i ∈ get_return_edges (cs''!i)"
      "valid_return_list rs'' m''" "length rs'' = length cs''" 
      "ms'' = targetnodes rs''" and "upd_cs cs [a] = cs''"
      by(auto elim!:silent_move_preserves_stacks)
    from IH[OF _ hyps] ‹msx'' = m'' # ms''›
    obtain cs' rs' where results:"valid_node m'" "valid_call_list cs' m'"
      "∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)"
      "valid_return_list rs' m'" "length rs' = length cs'" "ms' = targetnodes rs'"
      and "upd_cs cs'' as = cs'" by blast
    from ‹upd_cs cs [a] = cs''› ‹upd_cs cs'' as = cs'› 
    have "upd_cs cs ([a] @ as) = cs'" by(rule upd_cs_Append)
    with results show ?case
      apply(rule_tac x="cs'" in exI)
      apply(rule_tac x="rs'" in exI)
      by clarsimp
  qed
qed


lemma observable_move_preserves_stacks:
  assumes "S,f ⊢ (m#ms,s) -a→ (m'#ms',s')" and "valid_call_list cs m"
  and "∀i < length rs. rs!i ∈ get_return_edges (cs!i)" and "valid_return_list rs m"
  and "length rs = length cs" and "ms = targetnodes rs"
  obtains cs' rs' where "valid_node m'" and "valid_call_list cs' m'"
  and "∀i < length rs'. rs'!i ∈ get_return_edges (cs'!i)"
  and "valid_return_list rs' m'" and "length rs' = length cs'" 
  and "ms' = targetnodes rs'" and "upd_cs cs [a] = cs'"
proof(atomize_elim)
  from assms show "∃cs' rs'. valid_node m' ∧ valid_call_list cs' m' ∧
    (∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)) ∧
    valid_return_list rs' m' ∧ length rs' = length cs' ∧ ms' = targetnodes rs' ∧
    upd_cs cs [a] = cs'"
  proof(induct S f "m#ms" s a "m'#ms'" s' rule:observable_move.induct)
    case (observable_move_intra f a s s' n⇩c)
    from ‹hd (m # ms) = sourcenode a› have "m = sourcenode a" by simp
    from ‹m' # ms' = targetnode a # tl (m # ms)›
    have [simp]:"m' = targetnode a" "ms' = ms" by simp_all
    from ‹valid_edge a› have "valid_node m'" by simp
    moreover
    from ‹valid_edge a› ‹intra_kind (kind a)›
    have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
    from ‹valid_call_list cs m› ‹m = sourcenode a›
      ‹get_proc (sourcenode a) = get_proc (targetnode a)›
    have "valid_call_list cs m'"
      apply(clarsimp simp:valid_call_list_def)
      apply(erule_tac x="cs'" in allE)
      apply(erule_tac x="c" in allE)
      by(auto split:list.split)
    moreover
    from ‹valid_return_list rs m› ‹m = sourcenode a› 
      ‹get_proc (sourcenode a) = get_proc (targetnode a)›
    have "valid_return_list rs m'"
      apply(clarsimp simp:valid_return_list_def)
      apply(erule_tac x="cs'" in allE) apply clarsimp
      by(case_tac cs') auto
    moreover
    from ‹intra_kind (kind a)› have "upd_cs cs [a] = cs"
      by(fastforce simp:intra_kind_def)
    ultimately show ?case using ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)›
      ‹length rs = length cs› ‹ms = targetnodes rs›
      apply(rule_tac x="cs" in exI)
      apply(rule_tac x="rs" in exI) 
      by clarsimp
  next
    case (observable_move_call f a s s' Q r p fs a' S)
    from ‹hd (m # ms) = sourcenode a› 
      ‹m' # ms' = targetnode a # targetnode a' # tl (m # ms)›
    have [simp]:"m = sourcenode a" "m' = targetnode a" 
      "ms' = targetnode a' # tl (m # ms)"
      by simp_all
    from ‹valid_edge a› have "valid_node m'" by simp
    moreover
    from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc (targetnode a) = p"
      by(rule get_proc_call)
    with ‹valid_call_list cs m› ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹m = sourcenode a›
    have "valid_call_list (a # cs) (targetnode a)"
      apply(clarsimp simp:valid_call_list_def)
      apply(case_tac cs') apply auto
      apply(erule_tac x="list" in allE)
      by(case_tac list)(auto simp:sourcenodes_def)
    moreover
    from ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)› ‹a' ∈ get_return_edges a›
    have "∀i<length (a'#rs). (a'#rs) ! i ∈ get_return_edges ((a#cs) ! i)"
      by auto(case_tac i,auto)
    moreover
    from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'" 
      by(rule get_return_edges_valid)
    from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹a' ∈ get_return_edges a›
    obtain Q' f' where "kind a' = Q'↩⇘p⇙f'" by(fastforce dest!:call_return_edges)
    from ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'› have "get_proc (sourcenode a') = p"
      by(rule get_proc_return)
    from ‹valid_edge a› ‹a' ∈ get_return_edges a›
    have "get_proc (sourcenode a) = get_proc (targetnode a')" 
      by(rule get_proc_get_return_edge)
    with ‹valid_return_list rs m› ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'›
      ‹get_proc (sourcenode a') = p› ‹get_proc (targetnode a) = p› ‹m = sourcenode a›
    have "valid_return_list (a'#rs) (targetnode a)"
      apply(clarsimp simp:valid_return_list_def)
      apply(case_tac cs') apply auto
      apply(erule_tac x="list" in allE)
      by(case_tac list)(auto simp:targetnodes_def)
    moreover
    from ‹length rs = length cs› have "length (a'#rs) = length (a#cs)" by simp
    moreover
    from ‹ms = targetnodes rs› have "targetnode a' # ms = targetnodes (a' # rs)"
      by(simp add:targetnodes_def)
    moreover
    from ‹kind a = Q:r↪⇘p⇙fs› have "upd_cs cs [a] = a#cs" by simp
    ultimately show ?case
      apply(rule_tac x="a#cs" in exI)
      apply(rule_tac x="a'#rs" in exI)
      by clarsimp
  next
    case (observable_move_return f a s s' Q p f' S)
    from ‹hd (m # ms) = sourcenode a›
      ‹hd (tl (m # ms)) = targetnode a› ‹m' # ms' = tl (m # ms)› [symmetric]
    have [simp]:"m = sourcenode a" "m' = targetnode a" by simp_all
    from ‹length (m # ms) = length s› ‹length s = Suc (length s')› ‹s' ≠ []›
      ‹hd (tl (m # ms)) = targetnode a› ‹m' # ms' = tl (m # ms)›
    have "ms = targetnode a # ms'" 
      by(cases ms) auto
    with ‹ms = targetnodes rs›
    obtain r' rs' where "rs = r' # rs'" 
      and "targetnode a = targetnode r'" and "ms' = targetnodes rs'" 
      by(cases rs)(auto simp:targetnodes_def)
    moreover
    from ‹rs = r' # rs'› ‹length rs = length cs› obtain c' cs' where "cs = c' # cs'"
      and "length rs' = length cs'" by(cases cs) auto
    moreover
    from ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)› 
      ‹rs = r' # rs'› ‹cs = c' # cs'›
    have "∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)"
      and "r' ∈ get_return_edges c'" by auto
    moreover
    from ‹valid_edge a› have "valid_node (targetnode a)" by simp
    moreover
    from ‹valid_call_list cs m› ‹cs = c' # cs'›
    obtain p' Q' r fs' where "valid_edge c'" and "kind c' = Q':r↪⇘p'⇙fs'" 
      and "p' = get_proc m"
      apply(auto simp:valid_call_list_def)
      by(erule_tac x="[]" in allE) auto
    from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f'›
    have "get_proc (sourcenode a) = p" by(rule get_proc_return)
    with ‹p' = get_proc m› have [simp]:"p' = p" by simp
    from ‹valid_edge c'› ‹kind c' = Q':r↪⇘p'⇙fs'›
    have "get_proc (targetnode c') = p" by(fastforce intro:get_proc_call)
    from ‹valid_edge c'› ‹r' ∈ get_return_edges c'› have "valid_edge r'"
      by(rule get_return_edges_valid)
    from ‹valid_edge c'› ‹kind c' = Q':r↪⇘p'⇙fs'› ‹r' ∈ get_return_edges c'›
    obtain Q'' f'' where "kind r' = Q''↩⇘p⇙f''" by(fastforce dest!:call_return_edges)
    with ‹valid_edge r'› have "get_proc (sourcenode r') = p" by(rule get_proc_return)
    from ‹valid_edge r'› ‹kind r' = Q''↩⇘p⇙f''› have "method_exit (sourcenode r')" 
      by(fastforce simp:method_exit_def)
    from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f'› have "method_exit (sourcenode a)" 
      by(fastforce simp:method_exit_def)
    with ‹method_exit (sourcenode r')› ‹get_proc (sourcenode r') = p› 
      ‹get_proc (sourcenode a) = p›
    have "sourcenode a = sourcenode r'" by(fastforce intro:method_exit_unique)
    with ‹valid_edge a› ‹valid_edge r'› ‹targetnode a = targetnode r'›
    have "a = r'" by(fastforce intro:edge_det)
    from ‹valid_edge c'› ‹r' ∈ get_return_edges c'› ‹targetnode a = targetnode r'›
    have "get_proc (sourcenode c') = get_proc (targetnode a)"
      by(fastforce intro:get_proc_get_return_edge)
    from ‹valid_call_list cs m› ‹cs = c' # cs'›
      ‹get_proc (sourcenode c') = get_proc (targetnode a)›
    have "valid_call_list cs' (targetnode a)"
      apply(clarsimp simp:valid_call_list_def)
      apply(hypsubst_thin)
      apply(erule_tac x="c' # cs'" in allE)
      by(case_tac cs')(auto simp:sourcenodes_def)
    moreover
    from ‹valid_return_list rs m› ‹rs = r' # rs'› ‹targetnode a = targetnode r'›
    have "valid_return_list rs' (targetnode a)"
      apply(clarsimp simp:valid_return_list_def)
      apply(erule_tac x="r' # cs'" in allE)
      by(case_tac cs')(auto simp:targetnodes_def)
    moreover
    from ‹kind a = Q↩⇘p⇙f'› ‹cs = c' # cs'› have "upd_cs cs [a] = cs'" by simp
    ultimately show ?case
      apply(rule_tac x="cs'" in exI)
      apply(rule_tac x="rs'" in exI)
      by clarsimp
  qed
qed


lemma observable_moves_preserves_stack:
  assumes "S,f ⊢ (m#ms,s) =as⇒ (m'#ms',s')" 
  and "valid_node m" and "valid_call_list cs m"
  and "∀i < length rs. rs!i ∈ get_return_edges (cs!i)" and "valid_return_list rs m"
  and "length rs = length cs" and "ms = targetnodes rs"
  obtains cs' rs' where "valid_node m'" and "valid_call_list cs' m'"
  and "∀i < length rs'. rs'!i ∈ get_return_edges (cs'!i)"
  and "valid_return_list rs' m'" and "length rs' = length cs'" 
  and "ms' = targetnodes rs'" and "upd_cs cs as = cs'"
proof(atomize_elim)
  from ‹S,f ⊢ (m#ms,s) =as⇒ (m'#ms',s')› obtain msx s'' as' a'
    where "as = as'@[a']" and "S,f ⊢ (m#ms,s) =as'⇒⇩τ (msx,s'')"
    and "S,f ⊢ (msx,s'') -a'→ (m'#ms',s')"
    by(fastforce elim:observable_moves.cases)
  from ‹S,f ⊢ (msx,s'') -a'→ (m'#ms',s')› obtain m'' ms''
    where [simp]:"msx = m''#ms''" by(cases msx)(auto elim:observable_move.cases)
  from ‹S,f ⊢ (m#ms,s) =as'⇒⇩τ (msx,s'')› ‹valid_node m› ‹valid_call_list cs m›
    ‹∀i < length rs. rs!i ∈ get_return_edges (cs!i)› ‹valid_return_list rs m›
    ‹length rs = length cs› ‹ms = targetnodes rs›
  obtain cs'' rs'' where "valid_node m''" and "valid_call_list cs'' m''"
    and "∀i < length rs''. rs''!i ∈ get_return_edges (cs''!i)"
    and "valid_return_list rs'' m''" and "length rs'' = length cs''" 
    and "ms'' = targetnodes rs''" and "upd_cs cs as' = cs''"
    by(auto elim!:silent_moves_preserves_stacks)
  with ‹S,f ⊢ (msx,s'') -a'→ (m'#ms',s')›
  obtain cs' rs' where results:"valid_node m'" "valid_call_list cs' m'"
    "∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)"
    "valid_return_list rs' m'" "length rs' = length cs'" "ms' = targetnodes rs'"
    and "upd_cs cs'' [a'] = cs'"
    by(auto elim!:observable_move_preserves_stacks)
  from ‹upd_cs cs as' = cs''› ‹upd_cs cs'' [a'] = cs'›
  have "upd_cs cs (as'@[a']) = cs'" by(rule upd_cs_Append)
  with ‹as = as'@[a']› results
  show "∃cs' rs'. valid_node m' ∧ valid_call_list cs' m' ∧
    (∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)) ∧
    valid_return_list rs' m' ∧ length rs' = length cs' ∧ ms' = targetnodes rs' ∧
    upd_cs cs as = cs'"
    apply(rule_tac x="cs'" in exI)
    apply(rule_tac x="rs'" in exI)
    by clarsimp
qed


lemma silent_moves_slpa_path:
  "⟦S,f ⊢ (m#ms''@ms,s) =as⇒⇩τ (m'#ms',s'); valid_node m; valid_call_list cs m;
  ∀i < length rs. rs!i ∈ get_return_edges (cs!i); valid_return_list rs m; 
  length rs = length cs; ms'' = targetnodes rs;
  ∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
  ms'' ≠ [] ⟶ (∃mx'. call_of_return_node (last ms'') mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙);
  ∀mx ∈ set ms'. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙⟧
  ⟹ same_level_path_aux cs as ∧ upd_cs cs as = [] ∧ m -as→* m' ∧ ms = ms'"
proof(induct S f "m#ms''@ms" s as "m'#ms'" s' arbitrary:m ms'' ms cs rs
    rule:silent_moves.induct)
  case (silent_moves_Nil sx S f) thus ?case
    apply(cases ms'' rule:rev_cases) apply(auto intro:empty_path simp:targetnodes_def)
    by(cases rs rule:rev_cases,auto)+
next
  case (silent_moves_Cons S f sx a msx' sx' as sx'')
  thus ?case
  proof(induct _ _ "m#ms''@ms" _ _ _ _ rule:silent_move.induct)
    case (silent_move_intra f a s s' S msx')
    note IH = ‹⋀m ms'' ms cs rs. ⟦msx' = m # ms'' @ ms; valid_node m; 
      valid_call_list cs m; ∀i<length rs. rs ! i ∈ get_return_edges (cs ! i);
      valid_return_list rs m; length rs = length cs; ms'' = targetnodes rs;
      ∀mx∈set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
      ms'' ≠ [] ⟶
        (∃mx'. call_of_return_node (last ms'') mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙);
      ∀mx∈set ms'. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙⟧
      ⟹ same_level_path_aux cs as ∧ upd_cs cs as = [] ∧ m -as→* m' ∧ ms = ms'›
    note callstack = ‹∀mx∈set ms. ∃mx'. call_of_return_node mx mx' ∧ 
      mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    note callstack'' = ‹ms'' ≠ [] ⟶
      (∃mx'. call_of_return_node (last ms'') mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙)›
    note callstack' = ‹∀mx∈set ms'. ∃mx'. call_of_return_node mx mx' ∧ 
      mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    from ‹valid_edge a› have "valid_node (targetnode a)" by simp
    from ‹valid_edge a› ‹intra_kind (kind a)›
    have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
    from ‹hd (m # ms'' @ ms) = sourcenode a› have "m = sourcenode a" 
      by simp
    from ‹valid_call_list cs m› ‹m = sourcenode a›
      ‹get_proc (sourcenode a) = get_proc (targetnode a)›
    have "valid_call_list cs (targetnode a)"
      apply(clarsimp simp:valid_call_list_def)
      apply(erule_tac x="cs'" in allE)
      apply(erule_tac x="c" in allE)
      by(auto split:list.split)
    from ‹valid_return_list rs m› ‹m = sourcenode a› 
      ‹get_proc (sourcenode a) = get_proc (targetnode a)›
    have "valid_return_list rs (targetnode a)"
      apply(clarsimp simp:valid_return_list_def)
      apply(erule_tac x="cs'" in allE) apply clarsimp
      by(case_tac cs') auto
    from ‹msx' = targetnode a # tl (m # ms'' @ ms)›
    have "msx' = targetnode a # ms'' @ ms" by simp
    from IH[OF this ‹valid_node (targetnode a)› ‹valid_call_list cs (targetnode a)›
      ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)› 
      ‹valid_return_list rs (targetnode a)› ‹length rs = length cs›
      ‹ms'' = targetnodes rs› callstack callstack'' callstack']
    have "same_level_path_aux cs as" and "upd_cs cs as = []"
      and "targetnode a -as→* m'" and "ms = ms'" by simp_all
    from ‹intra_kind (kind a)› ‹same_level_path_aux cs as›
    have "same_level_path_aux cs (a # as)" by(fastforce simp:intra_kind_def)
    moreover
    from ‹intra_kind (kind a)› ‹upd_cs cs as = []›
    have "upd_cs cs (a # as) = []" by(fastforce simp:intra_kind_def)
    moreover
    from ‹valid_edge a› ‹m = sourcenode a› ‹targetnode a -as→* m'›
    have "m -a # as→* m'" by(fastforce intro:Cons_path)
    ultimately show ?case using ‹ms = ms'› by simp
  next
    case (silent_move_call f a s s' Q r p fs a' S msx')
    note IH = ‹⋀m ms'' ms cs rs. ⟦msx' = m # ms'' @ ms; valid_node m; valid_call_list cs m;
      ∀i<length rs. rs ! i ∈ get_return_edges (cs ! i); valid_return_list rs m;
      length rs = length cs; ms'' = targetnodes rs;
      ∀mx∈set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
      ms'' ≠ [] ⟶
        (∃mx'. call_of_return_node (last ms'') mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙);
      ∀mx∈set ms'. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙⟧
      ⟹ same_level_path_aux cs as ∧ upd_cs cs as = [] ∧ m -as→* m' ∧ ms = ms'›
    note callstack = ‹∀mx∈set ms. ∃mx'. call_of_return_node mx mx' ∧ 
      mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    note callstack'' = ‹ms'' ≠ [] ⟶
      (∃mx'. call_of_return_node (last ms'') mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙)›
    note callstack' = ‹∀mx∈set ms'. ∃mx'. call_of_return_node mx mx' ∧ 
      mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    from ‹valid_edge a› have "valid_node (targetnode a)" by simp
    from ‹hd (m # ms'' @ ms) = sourcenode a› have "m = sourcenode a" 
      by simp
    from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc (targetnode a) = p"
      by(rule get_proc_call)
    with ‹valid_call_list cs m› ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹m = sourcenode a›
    have "valid_call_list (a # cs) (targetnode a)"
      apply(clarsimp simp:valid_call_list_def)
      apply(case_tac cs') apply auto
      apply(erule_tac x="list" in allE)
      by(case_tac list)(auto simp:sourcenodes_def)
    from ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)› ‹a' ∈ get_return_edges a›
    have "∀i<length (a'#rs). (a'#rs) ! i ∈ get_return_edges ((a#cs) ! i)"
      by auto(case_tac i,auto)
    from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'" 
      by(rule get_return_edges_valid)
    from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹a' ∈ get_return_edges a›
    obtain Q' f' where "kind a' = Q'↩⇘p⇙f'" by(fastforce dest!:call_return_edges)
    from ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'› have "get_proc (sourcenode a') = p"
      by(rule get_proc_return)
    from ‹valid_edge a› ‹a' ∈ get_return_edges a›
    have "get_proc (sourcenode a) = get_proc (targetnode a')" 
      by(rule get_proc_get_return_edge)
    with ‹valid_return_list rs m› ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'›
      ‹get_proc (sourcenode a') = p› ‹get_proc (targetnode a) = p› ‹m = sourcenode a›
    have "valid_return_list (a'#rs) (targetnode a)"
      apply(clarsimp simp:valid_return_list_def)
      apply(case_tac cs') apply auto
      apply(erule_tac x="list" in allE)
      by(case_tac list)(auto simp:targetnodes_def)
    from ‹length rs = length cs› have "length (a'#rs) = length (a # cs)" by simp
    from ‹ms'' = targetnodes rs›
    have "targetnode a' # ms'' = targetnodes (a'#rs)" by(simp add:targetnodes_def)
    from ‹msx' = targetnode a # targetnode a' # tl (m # ms'' @ ms)›
    have "msx' = targetnode a # targetnode a' # ms'' @ ms" by simp
    have "∃mx'. call_of_return_node (last (targetnode a' # ms'')) mx' ∧
      mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
    proof(cases "ms'' = []")
      case True
      with ‹(∃m∈set (tl (m # ms'' @ ms)).
        ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨
        hd (m # ms'' @ ms) ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a› callstack
      have "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
      from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'"
        by(rule get_return_edges_valid)
      with ‹valid_edge a› ‹a' ∈ get_return_edges a›
      have "call_of_return_node (targetnode a') (sourcenode a)"
        by(fastforce simp:call_of_return_node_def return_node_def)
      with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› True show ?thesis by fastforce
    next
      case False
      with callstack'' show ?thesis by fastforce
    qed
    hence "targetnode a' # ms'' ≠ [] ⟶
      (∃mx'. call_of_return_node (last (targetnode a' # ms'')) mx' ∧
      mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙)" by simp
    from IH[OF _ ‹valid_node (targetnode a)› ‹valid_call_list (a # cs) (targetnode a)›
      ‹∀i<length (a'#rs). (a'#rs) ! i ∈ get_return_edges ((a#cs) ! i)›
      ‹valid_return_list (a'#rs) (targetnode a)› ‹length (a'#rs) = length (a # cs)›
      ‹targetnode a' # ms'' = targetnodes (a'#rs)› callstack this callstack']
      ‹msx' = targetnode a # targetnode a' # ms'' @ ms›
    have "same_level_path_aux (a # cs) as" and "upd_cs (a # cs) as = []"
      and "targetnode a -as→* m'" and "ms = ms'" by simp_all
    from ‹kind a = Q:r↪⇘p⇙fs› ‹same_level_path_aux (a # cs) as›
    have "same_level_path_aux cs (a # as)" by simp
    moreover
    from ‹kind a = Q:r↪⇘p⇙fs› ‹upd_cs (a # cs) as = []› have "upd_cs cs (a # as) = []"
      by simp
    moreover
    from ‹valid_edge a› ‹m = sourcenode a› ‹targetnode a -as→* m'›
    have "m -a # as→* m'" by(fastforce intro:Cons_path)
    ultimately show ?case using ‹ms = ms'› by simp
  next
    case (silent_move_return f a s s' Q p f' S msx')
    note IH = ‹⋀m ms'' ms cs rs. ⟦msx' = m # ms'' @ ms; valid_node m; 
      valid_call_list cs m; ∀i<length rs. rs ! i ∈ get_return_edges (cs ! i); 
      valid_return_list rs m; length rs = length cs; ms'' = targetnodes rs;
      ∀mx∈set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
      ms'' ≠ [] ⟶
        (∃mx'. call_of_return_node (last ms'') mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙);
      ∀mx∈set ms'. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙⟧
      ⟹ same_level_path_aux cs as ∧ upd_cs cs as = [] ∧ m -as→* m' ∧ ms = ms'›
    note callstack = ‹∀mx∈set ms. ∃mx'. call_of_return_node mx mx' ∧ 
      mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    note callstack'' = ‹ms'' ≠ [] ⟶
      (∃mx'. call_of_return_node (last ms'') mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙)›
    note callstack' = ‹∀mx∈set ms'. ∃mx'. call_of_return_node mx mx' ∧ 
      mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    have "ms'' ≠ []"
    proof
      assume "ms'' = []"
      with callstack
        ‹∃m∈set (tl (m # ms'' @ ms)). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙›
      show False by fastforce
    qed
    with ‹hd (tl (m # ms'' @ ms)) = targetnode a›
    obtain xs where "ms'' = targetnode a # xs" by(cases ms'') auto
    with ‹ms'' = targetnodes rs› obtain r' rs' where "rs = r' # rs'" 
      and "targetnode a = targetnode r'" and "xs = targetnodes rs'" 
      by(cases rs)(auto simp:targetnodes_def)
    from ‹rs = r' # rs'› ‹length rs = length cs› obtain c' cs' where "cs = c' # cs'"
      and "length rs' = length cs'" by(cases cs) auto
    from ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)› 
      ‹rs = r' # rs'› ‹cs = c' # cs'›
    have "∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)"
      and "r' ∈ get_return_edges c'" by auto
    from ‹valid_edge a› have "valid_node (targetnode a)" by simp
    from ‹hd (m # ms'' @ ms) = sourcenode a› have "m = sourcenode a" 
      by simp
    from ‹valid_call_list cs m› ‹cs = c' # cs'›
    obtain p' Q' r fs' where "valid_edge c'" and "kind c' = Q':r↪⇘p'⇙fs'" 
      and "p' = get_proc m"
      apply(auto simp:valid_call_list_def)
      by(erule_tac x="[]" in allE) auto
    from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f'›
    have "get_proc (sourcenode a) = p" by(rule get_proc_return)
    with ‹m = sourcenode a› ‹p' = get_proc m› have [simp]:"p' = p" by simp
    from ‹valid_edge c'› ‹kind c' = Q':r↪⇘p'⇙fs'›
    have "get_proc (targetnode c') = p" by(fastforce intro:get_proc_call)
    from ‹valid_edge c'› ‹r' ∈ get_return_edges c'› have "valid_edge r'"
      by(rule get_return_edges_valid)
    from ‹valid_edge c'› ‹kind c' = Q':r↪⇘p'⇙fs'› ‹r' ∈ get_return_edges c'›
    obtain Q'' f'' where "kind r' = Q''↩⇘p⇙f''" by(fastforce dest!:call_return_edges)
    with ‹valid_edge r'› have "get_proc (sourcenode r') = p" by(rule get_proc_return)
    from ‹valid_edge r'› ‹kind r' = Q''↩⇘p⇙f''› have "method_exit (sourcenode r')" 
      by(fastforce simp:method_exit_def)
    from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f'› have "method_exit (sourcenode a)" 
      by(fastforce simp:method_exit_def)
    with ‹method_exit (sourcenode r')› ‹get_proc (sourcenode r') = p› 
      ‹get_proc (sourcenode a) = p›
    have "sourcenode a = sourcenode r'" by(fastforce intro:method_exit_unique)
    with ‹valid_edge a› ‹valid_edge r'› ‹targetnode a = targetnode r'›
    have "a = r'" by(fastforce intro:edge_det)
    from ‹valid_edge c'› ‹r' ∈ get_return_edges c'› ‹targetnode a = targetnode r'›
    have "get_proc (sourcenode c') = get_proc (targetnode a)"
      by(fastforce intro:get_proc_get_return_edge)
    from ‹valid_call_list cs m› ‹cs = c' # cs'›
      ‹get_proc (sourcenode c') = get_proc (targetnode a)›
    have "valid_call_list cs' (targetnode a)"
      apply(clarsimp simp:valid_call_list_def)
      apply(hypsubst_thin)
      apply(erule_tac x="c' # cs'" in allE)
      by(case_tac cs')(auto simp:sourcenodes_def)
    from ‹valid_return_list rs m› ‹rs = r' # rs'› ‹targetnode a = targetnode r'›
    have "valid_return_list rs' (targetnode a)"
      apply(clarsimp simp:valid_return_list_def)
      apply(erule_tac x="r' # cs'" in allE)
      by(case_tac cs')(auto simp:targetnodes_def)
    from ‹msx' = tl (m # ms'' @ ms)› ‹ms'' = targetnode a # xs›
    have "msx' = targetnode a # xs @ ms" by simp
    from callstack'' ‹ms'' = targetnode a # xs›
    have "xs ≠ [] ⟶
      (∃mx'. call_of_return_node (last xs) mx' ∧ mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
      by fastforce
    from IH[OF ‹msx' = targetnode a # xs @ ms› ‹valid_node (targetnode a)›
      ‹valid_call_list cs' (targetnode a)›
      ‹∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)› 
      ‹valid_return_list rs' (targetnode a)› ‹length rs' = length cs'›
      ‹xs = targetnodes rs'› callstack this callstack']
    have "same_level_path_aux cs' as" and "upd_cs cs' as = []"
      and "targetnode a -as→* m'" and "ms = ms'" by simp_all
    from ‹kind a = Q↩⇘p⇙f'› ‹same_level_path_aux cs' as› ‹cs = c' # cs'›
      ‹r' ∈ get_return_edges c'› ‹a = r'›
    have "same_level_path_aux cs (a # as)" by simp
    moreover
    from ‹upd_cs cs' as = []› ‹kind a = Q↩⇘p⇙f'› ‹cs = c' # cs'›
    have "upd_cs cs (a # as) = []" by simp
    moreover
    from ‹valid_edge a› ‹m = sourcenode a› ‹targetnode a -as→* m'›
    have "m -a # as→* m'" by(fastforce intro:Cons_path)
    ultimately show ?case using ‹ms = ms'› by simp
  qed
qed


lemma silent_moves_slp:
  "⟦S,f ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s'); valid_node m; 
  ∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
  ∀mx ∈ set ms'. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙⟧
  ⟹ m -as→⇘sl⇙* m' ∧ ms = ms'"
  by(fastforce dest!:silent_moves_slpa_path
                   [of _ _ _ "[]" _ _ _ _ _ _ "[]" "[]",simplified] 
              simp:targetnodes_def valid_call_list_def valid_return_list_def 
                   same_level_path_def slp_def)


lemma slpa_silent_moves_callstacks_eq:
  "⟦same_level_path_aux cs as; S,f ⊢ (m#msx@ms,s) =as⇒⇩τ (m'#ms',s');
  length ms = length ms'; valid_call_list cs m; 
  ∀i < length rs. rs!i ∈ get_return_edges (cs!i); valid_return_list rs m; 
  length rs = length cs; msx = targetnodes rs⟧
  ⟹ ms = ms'"
proof(induct arbitrary:m msx s rs rule:slpa_induct)
  case (slpa_empty cs)
  from ‹S,f ⊢ (m # msx @ ms,s) =[]⇒⇩τ (m' # ms',s')›
  have "msx@ms = ms'" by(fastforce elim:silent_moves.cases)
  with ‹length ms = length ms'› show ?case by fastforce
next
  case (slpa_intra cs a as)
  note IH = ‹⋀m msx s rs. ⟦S,f ⊢ (m # msx @ ms,s) =as⇒⇩τ (m' # ms',s');
    length ms = length ms'; valid_call_list cs m;
    ∀i<length rs. rs ! i ∈ get_return_edges (cs ! i);
    valid_return_list rs m; length rs = length cs; msx = targetnodes rs⟧
    ⟹ ms = ms'›
  from ‹S,f ⊢ (m # msx @ ms,s) =a # as⇒⇩τ (m' # ms',s')› obtain ms'' s''
  where "S,f ⊢ (m # msx @ ms,s) -a→⇩τ (ms'',s'')"
    and "S,f ⊢ (ms'',s'') =as⇒⇩τ (m' # ms',s')"
    by(auto elim:silent_moves.cases)
  from ‹S,f ⊢ (m # msx @ ms,s) -a→⇩τ (ms'',s'')› ‹intra_kind (kind a)›
  have "valid_edge a" and [simp]:"m = sourcenode a" "ms'' = targetnode a # msx @ ms"
    by(fastforce elim:silent_move.cases simp:intra_kind_def)+
  from ‹valid_edge a› ‹intra_kind (kind a)›
  have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
  from ‹valid_call_list cs m› ‹m = sourcenode a›
    ‹get_proc (sourcenode a) = get_proc (targetnode a)›
  have "valid_call_list cs (targetnode a)"
    apply(clarsimp simp:valid_call_list_def)
    apply(erule_tac x="cs'" in allE)
    apply(erule_tac x="c" in allE)
    by(auto split:list.split)
  from ‹valid_return_list rs m› ‹m = sourcenode a› 
    ‹get_proc (sourcenode a) = get_proc (targetnode a)›
  have "valid_return_list rs (targetnode a)"
    apply(clarsimp simp:valid_return_list_def)
    apply(erule_tac x="cs'" in allE) apply clarsimp
    by(case_tac cs') auto
  from ‹S,f ⊢ (ms'',s'') =as⇒⇩τ (m' # ms',s')›
  have "S,f ⊢ (targetnode a # msx @ ms,s'') =as⇒⇩τ (m' # ms',s')" by simp
  from IH[OF this ‹length ms = length ms'› ‹valid_call_list cs (targetnode a)›
    ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)› 
    ‹valid_return_list rs (targetnode a)› ‹length rs = length cs›
    ‹msx = targetnodes rs›] show ?case .
next
  case (slpa_Call cs a as Q r p fs)
  note IH = ‹⋀m msx s rs. ⟦S,f ⊢ (m # msx @ ms,s) =as⇒⇩τ (m' # ms',s');
    length ms = length ms'; valid_call_list (a # cs) m;
    ∀i<length rs. rs ! i ∈ get_return_edges ((a # cs) ! i);
    valid_return_list rs m; length rs = length (a # cs);
    msx = targetnodes rs⟧
    ⟹ ms = ms'›
  from ‹S,f ⊢ (m # msx @ ms,s) =a # as⇒⇩τ (m' # ms',s')› obtain ms'' s''
    where "S,f ⊢ (m # msx @ ms,s) -a→⇩τ (ms'',s'')"
    and "S,f ⊢ (ms'',s'') =as⇒⇩τ (m' # ms',s')"
    by(auto elim:silent_moves.cases)
  from ‹S,f ⊢ (m # msx @ ms,s) -a→⇩τ (ms'',s'')› ‹kind a = Q:r↪⇘p⇙fs›
  obtain a' where "valid_edge a" and [simp]:"m = sourcenode a"
    and [simp]:"ms'' = targetnode a # targetnode a' # msx @ ms"
    and "a' ∈ get_return_edges a"
    by(auto elim:silent_move.cases simp:intra_kind_def)
  from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc (targetnode a) = p"
    by(rule get_proc_call)
  with ‹valid_call_list cs m› ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹m = sourcenode a›
  have "valid_call_list (a # cs) (targetnode a)"
    apply(clarsimp simp:valid_call_list_def)
    apply(case_tac cs') apply auto
    apply(erule_tac x="list" in allE)
    by(case_tac list)(auto simp:sourcenodes_def)
  from ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)› ‹a' ∈ get_return_edges a›
  have "∀i<length (a'#rs). (a'#rs) ! i ∈ get_return_edges ((a#cs) ! i)"
    by auto(case_tac i,auto)
  from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'" 
    by(rule get_return_edges_valid)
  from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹a' ∈ get_return_edges a›
  obtain Q' f' where "kind a' = Q'↩⇘p⇙f'" by(fastforce dest!:call_return_edges)
  from ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'› have "get_proc (sourcenode a') = p"
    by(rule get_proc_return)
  from ‹valid_edge a› ‹a' ∈ get_return_edges a›
  have "get_proc (sourcenode a) = get_proc (targetnode a')" 
    by(rule get_proc_get_return_edge)
  with ‹valid_return_list rs m› ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'›
    ‹get_proc (sourcenode a') = p› ‹get_proc (targetnode a) = p› ‹m = sourcenode a›
  have "valid_return_list (a'#rs) (targetnode a)"
    apply(clarsimp simp:valid_return_list_def)
    apply(case_tac cs') apply auto
    apply(erule_tac x="list" in allE)
    by(case_tac list)(auto simp:targetnodes_def)
  from ‹length rs = length cs› have "length (a'#rs) = length (a#cs)" by simp
  from ‹msx = targetnodes rs› have "targetnode a' # msx = targetnodes (a' # rs)"
    by(simp add:targetnodes_def)
  from ‹S,f ⊢ (ms'',s'') =as⇒⇩τ (m' # ms',s')›
  have "S,f ⊢ (targetnode a # (targetnode a' # msx) @ ms,s'') =as⇒⇩τ (m' # ms',s')"
    by simp
  from IH[OF this ‹length ms = length ms'› ‹valid_call_list (a # cs) (targetnode a)›
    ‹∀i<length (a'#rs). (a'#rs) ! i ∈ get_return_edges ((a#cs) ! i)›
    ‹valid_return_list (a'#rs) (targetnode a)› ‹length (a'#rs) = length (a#cs)›
    ‹targetnode a' # msx = targetnodes (a' # rs)›] show ?case .
next
  case (slpa_Return cs a as Q p f' c' cs')
  note IH = ‹⋀m msx s rs. ⟦S,f ⊢ (m # msx @ ms,s) =as⇒⇩τ (m' # ms',s');
    length ms = length ms'; valid_call_list cs' m;
    ∀i<length rs. rs ! i ∈ get_return_edges (cs' ! i); valid_return_list rs m; 
    length rs = length cs'; msx = targetnodes rs⟧
    ⟹ ms = ms'›
  from ‹S,f ⊢ (m # msx @ ms,s) =a # as⇒⇩τ (m' # ms',s')› obtain ms'' s''
    where "S,f ⊢ (m # msx @ ms,s) -a→⇩τ (ms'',s'')"
    and "S,f ⊢ (ms'',s'') =as⇒⇩τ (m' # ms',s')"
    by(auto elim:silent_moves.cases)
  from ‹S,f ⊢ (m # msx @ ms,s) -a→⇩τ (ms'',s'')› ‹kind a = Q↩⇘p⇙f'›
  have "valid_edge a" and "m = sourcenode a" and "hd (msx @ ms) = targetnode a"
    and "ms'' = msx @ ms" and "s'' ≠ []" and "length s = Suc(length s'')"
    and "length (m # msx @ ms) = length s"
    by(auto elim:silent_move.cases simp:intra_kind_def)
  from ‹msx = targetnodes rs› ‹length rs = length cs› ‹cs = c' # cs'›
  obtain mx' msx' where "msx = mx'#msx'"
    by(cases msx)(fastforce simp:targetnodes_def)+
  with ‹hd (msx @ ms) = targetnode a› have "mx' = targetnode a" by simp
  from ‹valid_call_list cs m› ‹cs = c' # cs'› have "valid_edge c'"
    by(fastforce simp:valid_call_list_def)
  from ‹valid_edge c'› ‹a ∈ get_return_edges c'›
  have "get_proc (sourcenode c') = get_proc (targetnode a)"
    by(rule get_proc_get_return_edge)
  from ‹valid_call_list cs m› ‹cs = c' # cs'›
    ‹get_proc (sourcenode c') = get_proc (targetnode a)›
  have "valid_call_list cs' (targetnode a)"
    apply(clarsimp simp:valid_call_list_def)
    apply(hypsubst_thin)
    apply(erule_tac x="c' # cs'" in allE)
    by(case_tac cs')(auto simp:sourcenodes_def)
  from ‹length rs = length cs› ‹cs = c' # cs'› obtain r' rs' 
    where [simp]:"rs = r'#rs'" and "length rs' = length cs'" by(cases rs) auto
  from ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)› ‹cs = c' # cs'›
  have "∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)"
    and "r' ∈ get_return_edges c'" by auto
  with ‹valid_edge c'› ‹a ∈ get_return_edges c'› have [simp]:"a = r'" 
    by -(rule get_return_edges_unique)
  with ‹valid_return_list rs m› 
  have "valid_return_list rs' (targetnode a)"
    apply(clarsimp simp:valid_return_list_def)
    apply(erule_tac x="r' # cs'" in allE)
    by(case_tac cs')(auto simp:targetnodes_def)
  from ‹msx = targetnodes rs› ‹msx = mx'#msx'› ‹rs = r'#rs'›
  have "msx' = targetnodes rs'" by(simp add:targetnodes_def)
  from ‹S,f ⊢ (ms'',s'') =as⇒⇩τ (m' # ms',s')› ‹msx = mx'#msx'›
    ‹ms'' = msx @ ms› ‹mx' = targetnode a›
  have "S,f ⊢ (targetnode a # msx' @ ms,s'') =as⇒⇩τ (m' # ms',s')" by simp
  from IH[OF this ‹length ms = length ms'› ‹valid_call_list cs' (targetnode a)›
    ‹∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)›
    ‹valid_return_list rs' (targetnode a)› ‹length rs' = length cs'›
    ‹msx' = targetnodes rs'›] show ?case .
qed


lemma silent_moves_same_level_path:
  assumes "S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')" and "m -as→⇘sl⇙* m'" shows "ms = ms'"
proof -
  from ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')› obtain cf cfs where "s = cf#cfs"
    by(cases s)(auto dest:silent_moves_equal_length)
  with ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')› 
  have "transfers (kinds as) (cf#cfs) = s'"
    by(fastforce intro:silent_moves_preds_transfers simp:kinds_def)
  with ‹m -as→⇘sl⇙* m'› obtain cf' where "s' = cf'#cfs"
    by -(drule slp_callstack_length_equal,auto)
  from ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')›
  have "length (m#ms) = length s" and "length (m'#ms') = length s'" 
    by(rule silent_moves_equal_length)+
  with ‹s = cf#cfs› ‹s' = cf'#cfs› have "length ms = length ms'" by simp
  from ‹m -as→⇘sl⇙* m'› have "same_level_path_aux [] as"
    by(simp add:slp_def same_level_path_def)
  with ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')› ‹length ms = length ms'› 
  show ?thesis by(auto elim!:slpa_silent_moves_callstacks_eq 
    simp:targetnodes_def valid_call_list_def valid_return_list_def)
qed


lemma silent_moves_call_edge:
  assumes "S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')" and "valid_node m"
  and callstack:"∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ 
      mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
  and rest:"∀i < length rs. rs!i ∈ get_return_edges (cs!i)"
  "ms = targetnodes rs" "valid_return_list rs m" "length rs = length cs"
  obtains as' a as'' where "as = as'@a#as''" and "∃Q r p fs. kind a = Q:r↪⇘p⇙fs"
  and "call_of_return_node (hd ms') (sourcenode a)"
  and "targetnode a -as''→⇘sl⇙* m'"
  | "ms' = ms"
proof(atomize_elim)
  from ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')›
  show "(∃as' a as''. as = as' @ a # as'' ∧ (∃Q r p fs. kind a = Q:r↪⇘p⇙fs) ∧
    call_of_return_node (hd ms') (sourcenode a) ∧ targetnode a -as''→⇘sl⇙* m') ∨
    ms' = ms"
  proof(induct as arbitrary:m' ms' s' rule:length_induct)
    fix as m' ms' s'
    assume IH:"∀as'. length as' < length as ⟶
      (∀mx msx sx. S,kind ⊢ (m#ms,s) =as'⇒⇩τ (mx#msx,sx) ⟶ 
      (∃asx a asx'. as' = asx @ a # asx' ∧ (∃Q r p fs. kind a = Q:r↪⇘p⇙fs) ∧
      call_of_return_node (hd msx) (sourcenode a) ∧ targetnode a -asx'→⇘sl⇙* mx) ∨
      msx = ms)"
      and "S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')"
    show "(∃as' a as''. as = as' @ a # as'' ∧ (∃Q r p fs. kind a = Q:r↪⇘p⇙fs) ∧
      call_of_return_node (hd ms') (sourcenode a) ∧ targetnode a -as''→⇘sl⇙* m') ∨
      ms' = ms"
    proof(cases as rule:rev_cases)
      case Nil
      with ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')› have "ms = ms'"
        by(fastforce elim:silent_moves.cases)
      thus ?thesis by simp
    next
      case (snoc as' a')
      with ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')›
      obtain ms'' s'' where "S,kind ⊢ (m#ms,s) =as'⇒⇩τ (ms'',s'')"
        and "S,kind ⊢ (ms'',s'') =[a']⇒⇩τ (m'#ms',s')"
        by(fastforce elim:silent_moves_split)
      from snoc have "length as' < length as" by simp
      from ‹S,kind ⊢ (ms'',s'') =[a']⇒⇩τ (m'#ms',s')›
      have "S,kind ⊢ (ms'',s'') -a'→⇩τ (m'#ms',s')"
        by(fastforce elim:silent_moves.cases)
      show ?thesis
      proof(cases "kind a'" rule:edge_kind_cases)
        case Intra
        with ‹S,kind ⊢ (ms'',s'') -a'→⇩τ (m'#ms',s')›
        have "valid_edge a'" and "m' = targetnode a'"
          by(auto elim:silent_move.cases simp:intra_kind_def)
        from ‹S,kind ⊢ (ms'',s'') -a'→⇩τ (m'#ms',s')› ‹intra_kind (kind a')›
        have "ms'' = sourcenode a'#ms'"
          by -(erule silent_move.cases,auto simp:intra_kind_def,(cases ms'',auto)+)
        with IH ‹length as' < length as› ‹S,kind ⊢ (m#ms,s) =as'⇒⇩τ (ms'',s'')›
        have "(∃asx ax asx'. as' = asx @ ax # asx' ∧ (∃Q r p fs. kind ax = Q:r↪⇘p⇙fs) ∧
          call_of_return_node (hd ms') (sourcenode ax) ∧ 
          targetnode ax -asx'→⇘sl⇙* sourcenode a') ∨ ms' = ms"
          by simp blast
        thus ?thesis
        proof
          assume "∃asx ax asx'. as' = asx @ ax # asx' ∧ 
            (∃Q r p fs. kind ax = Q:r↪⇘p⇙fs) ∧
            call_of_return_node (hd ms') (sourcenode ax) ∧ 
            targetnode ax -asx'→⇘sl⇙* sourcenode a'"
          then obtain asx ax asx' where "as' = asx @ ax # asx'"
            and "∃Q r p fs. kind ax = Q:r↪⇘p⇙fs"
            and "call_of_return_node (hd ms') (sourcenode ax)"
            and "targetnode ax -asx'→⇘sl⇙* sourcenode a'"
            by blast
          from ‹as' = asx @ ax # asx'› have "as'@[a'] = asx @ ax # (asx' @ [a'])"
            by simp
          moreover
          from ‹targetnode ax -asx'→⇘sl⇙* sourcenode a'› ‹intra_kind (kind a')› 
            ‹m' = targetnode a'› ‹valid_edge a'›
          have "targetnode ax -asx'@[a']→⇘sl⇙* m'"
            by(fastforce intro:path_Append path_edge same_level_path_aux_Append 
              upd_cs_Append simp:slp_def same_level_path_def intra_kind_def)
          ultimately show ?thesis using ‹∃Q r p fs. kind ax = Q:r↪⇘p⇙fs› 
            ‹call_of_return_node (hd ms') (sourcenode ax)› snoc by blast
        next
          assume "ms' = ms" thus ?thesis by simp
        qed
      next
        case (Call Q r p fs)
        with ‹S,kind ⊢ (ms'',s'') -a'→⇩τ (m'#ms',s')› obtain a''
          where "valid_edge a'" and "a'' ∈ get_return_edges a'"
          and "hd ms'' = sourcenode a'" and "m' = targetnode a'"
          and "ms' = (targetnode a'')#tl ms''" and "length ms'' = length s''"
          and "pred (kind a') s''"
          by(auto elim:silent_move.cases simp:intra_kind_def)
        from ‹valid_edge a'› ‹a'' ∈ get_return_edges a'› have "valid_edge a''"
          by(rule get_return_edges_valid)
        from ‹valid_edge a''› ‹valid_edge a'› ‹a'' ∈ get_return_edges a'›
        have "return_node (targetnode a'')" by(fastforce simp:return_node_def)
        with ‹valid_edge a'› ‹valid_edge a''›
          ‹a'' ∈ get_return_edges a'› ‹ms' = (targetnode a'')#tl ms''›
        have "call_of_return_node (hd ms') (sourcenode a')"
          by(simp add:call_of_return_node_def) blast
        with snoc ‹kind a' = Q:r↪⇘p⇙fs› ‹m' = targetnode a'› ‹valid_edge a'›
        show ?thesis by(fastforce intro:empty_path simp:slp_def same_level_path_def)
      next
        case (Return Q p f)
        with ‹S,kind ⊢ (ms'',s'') -a'→⇩τ (m'#ms',s')› 
        have "valid_edge a'" and "hd ms'' = sourcenode a'"
          and "hd(tl ms'') = targetnode a'" and "m'#ms' = tl ms''"
          and "length ms'' = length s''" and "length s'' = Suc(length s')"
          and "s' ≠ []"
          by(auto elim:silent_move.cases simp:intra_kind_def)
        hence "ms'' = sourcenode a' # targetnode a' # ms'" by(cases ms'') auto
        with ‹length as' < length as› ‹S,kind ⊢ (m#ms,s) =as'⇒⇩τ (ms'',s'')› IH
        have "(∃asx ax asx'. as' = asx @ ax # asx' ∧ (∃Q r p fs. kind ax = Q:r↪⇘p⇙fs) ∧
          call_of_return_node (targetnode a') (sourcenode ax) ∧
          targetnode ax -asx'→⇘sl⇙* sourcenode a') ∨ ms = targetnode a' # ms'"
          apply - apply(erule_tac x="as'" in allE) apply clarsimp
          apply(erule_tac x="sourcenode a'" in allE)
          apply(erule_tac x="targetnode a' # ms'" in allE)
          by fastforce
        thus ?thesis
        proof
          assume "∃asx ax asx'. as' = asx @ ax # asx' ∧ 
            (∃Q r p fs. kind ax = Q:r↪⇘p⇙fs) ∧
            call_of_return_node (targetnode a') (sourcenode ax) ∧
            targetnode ax -asx'→⇘sl⇙* sourcenode a'"
          then obtain asx ax asx' where "as' = asx @ ax # asx'"
            and "∃Q r p fs. kind ax = Q:r↪⇘p⇙fs" 
            and "call_of_return_node (targetnode a') (sourcenode ax)"
            and "targetnode ax -asx'→⇘sl⇙* sourcenode a'" by blast
          from ‹as' = asx @ ax # asx'› snoc have"length asx < length as" by simp
          moreover
          from ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')› snoc ‹as' = asx @ ax # asx'›
          obtain msx sx where "S,kind ⊢ (m#ms,s) =asx⇒⇩τ (msx,sx)"
            and "S,kind ⊢ (msx,sx) =ax#asx'@[a']⇒⇩τ (m'#ms',s')"
            by(fastforce elim:silent_moves_split)
          from ‹S,kind ⊢ (msx,sx) =ax#asx'@[a']⇒⇩τ (m'#ms',s')›
          obtain xs x ys y where "S,kind ⊢ (msx,sx) -ax→⇩τ (xs,x)"
            and "S,kind ⊢ (xs,x) =asx'⇒⇩τ (ys,y)"
            and "S,kind ⊢ (ys,y) =[a']⇒⇩τ (m'#ms',s')"
            apply - apply(erule silent_moves.cases) apply auto
            by(erule silent_moves_split) auto
          from ‹S,kind ⊢ (msx,sx) -ax→⇩τ (xs,x)› ‹∃Q r p fs. kind ax = Q:r↪⇘p⇙fs›
          obtain msx' ax' where "msx = sourcenode ax#msx'" 
            and "ax' ∈ get_return_edges ax"
            and [simp]:"xs = (targetnode ax)#(targetnode ax')#msx'"
            and "length x = Suc(length sx)" and "length msx = length sx"
            apply - apply(erule silent_move.cases) apply(auto simp:intra_kind_def)
            by(cases msx,auto)+
          from ‹S,kind ⊢ (ys,y) =[a']⇒⇩τ (m'#ms',s')› obtain msy 
            where "ys = sourcenode a'#msy"
            apply - apply(erule silent_moves.cases) apply auto
            apply(erule silent_move.cases)
            by(cases ys,auto)+
          with ‹S,kind ⊢ (xs,x) =asx'⇒⇩τ (ys,y)› 
            ‹targetnode ax -asx'→⇘sl⇙* sourcenode a'›
            ‹xs = (targetnode ax)#(targetnode ax')#msx'›
          have "(targetnode ax')#msx' = msy" apply simp
            by(fastforce intro:silent_moves_same_level_path)
          with ‹S,kind ⊢ (ys,y) =[a']⇒⇩τ (m'#ms',s')› ‹kind a' = Q↩⇘p⇙f› 
            ‹ys = sourcenode a'#msy›
          have "m' = targetnode a'" and "msx' = ms'"
            by(fastforce elim:silent_moves.cases silent_move.cases 
                        simp:intra_kind_def)+
          with ‹S,kind ⊢ (m#ms,s) =asx⇒⇩τ (msx,sx)› ‹msx = sourcenode ax#msx'›
          have "S,kind ⊢ (m#ms,s) =asx⇒⇩τ (sourcenode ax#ms',sx)" by simp
          ultimately have "(∃xs x xs'. asx = xs@x#xs' ∧ 
            (∃Q r p fs. kind x = Q:r↪⇘p⇙fs) ∧
            call_of_return_node (hd ms') (sourcenode x) ∧
            targetnode x -xs'→⇘sl⇙* sourcenode ax) ∨ ms = ms'" using IH
            by simp blast
          thus ?thesis
          proof
            assume "∃xs x xs'. asx = xs@x#xs' ∧ (∃Q r p fs. kind x = Q:r↪⇘p⇙fs) ∧
              call_of_return_node (hd ms') (sourcenode x) ∧
              targetnode x -xs'→⇘sl⇙* sourcenode ax"
            then obtain xs x xs' where "asx = xs@x#xs'"
              and "∃Q r p fs. kind x = Q:r↪⇘p⇙fs" 
              and "call_of_return_node (hd ms') (sourcenode x)"
              and "targetnode x -xs'→⇘sl⇙* sourcenode ax" by blast
            from ‹asx = xs@x#xs'› ‹as' = asx @ ax # asx'› snoc
            have "as = xs@x#(xs'@ax#asx'@[a'])" by simp
            from ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')› ‹valid_node m› rest
            have "m -as→* m'" and "valid_path_aux cs as"
              by(auto dest:silent_moves_vpa_path[of _ _ _ _ _ _ _ _ _ rs cs]
                      simp:valid_call_list_def valid_return_list_def targetnodes_def)
            hence "m -as→⇩√* m'" 
              by(fastforce intro:valid_path_aux_valid_path simp:vp_def)
            with snoc have "m -as'→⇩√* sourcenode a'"
              by(auto elim:path_split_snoc dest:valid_path_aux_split 
                simp:vp_def valid_path_def)
            with ‹as' = asx @ ax # asx'›
            have "valid_edge ax" and "targetnode ax -asx'→* sourcenode a'"
              by(auto dest:path_split simp:vp_def)
            hence "sourcenode ax -ax#asx'→* sourcenode a'"
              by(fastforce intro:Cons_path)
            from ‹valid_edge a'› have "sourcenode a' -[a']→* targetnode a'"
              by(rule path_edge)
            with ‹sourcenode ax -ax#asx'→* sourcenode a'›
            have "sourcenode ax -(ax#asx')@[a']→* targetnode a'"
              by(rule path_Append)
            from ‹m -as→⇩√* m'› snoc ‹as' = asx @ ax # asx'› snoc
            have "valid_path_aux ([]@(upd_cs [] asx)) (ax # asx' @ [a'])"
              by(fastforce dest:valid_path_aux_split simp:vp_def valid_path_def)
            hence "valid_path_aux [] (ax#asx'@[a'])" 
              by(rule valid_path_aux_callstack_prefix)
            with ‹∃Q r p fs. kind ax = Q:r↪⇘p⇙fs›
            have "valid_path_aux [ax] (asx'@[a'])" by fastforce
            hence "valid_path_aux (upd_cs [ax] asx') [a']"
              by(rule valid_path_aux_split)
            from ‹targetnode ax -asx'→⇘sl⇙* sourcenode a'›
            have "same_level_path_aux [] asx'" and "upd_cs [] asx' = []" 
              by(simp_all add:slp_def same_level_path_def)
            hence "upd_cs ([]@[ax]) asx' = []@[ax]"
              by(rule same_level_path_upd_cs_callstack_Append)
            with ‹valid_path_aux (upd_cs [ax] asx') [a']›
            have "valid_path_aux [ax] [a']" by(simp del:valid_path_aux.simps)
            with ‹∃Q r p fs. kind ax = Q:r↪⇘p⇙fs› ‹kind a' = Q↩⇘p⇙f›
            have "a' ∈ get_return_edges ax" by simp
            with ‹upd_cs ([]@[ax]) asx' = []@[ax]› ‹kind a' = Q↩⇘p⇙f›
            have "upd_cs [ax] (asx'@[a']) = []" by(fastforce intro:upd_cs_Append)
            with ‹∃Q r p fs. kind ax = Q:r↪⇘p⇙fs›
            have "upd_cs [] (ax#asx'@[a']) = []" by fastforce
            from ‹targetnode ax -asx'→⇘sl⇙* sourcenode a'›
            have "same_level_path_aux [] asx'" and "upd_cs [] asx' = []" 
              by(simp_all add:slp_def same_level_path_def)
            hence "same_level_path_aux ([]@[ax]) asx'" 
              by -(rule same_level_path_aux_callstack_Append)
            with ‹∃Q r p fs. kind ax = Q:r↪⇘p⇙fs› ‹kind a' = Q↩⇘p⇙f› 
              ‹a' ∈ get_return_edges ax› ‹upd_cs ([]@[ax]) asx' = []@[ax]›
            have "same_level_path_aux [] ((ax#asx')@[a'])"
              by(fastforce intro:same_level_path_aux_Append)
            with ‹upd_cs [] (ax#asx'@[a']) = []›
              ‹sourcenode ax -(ax#asx')@[a']→* targetnode a'›
            have "sourcenode ax -(ax#asx')@[a']→⇘sl⇙* targetnode a'"
              by(simp add:slp_def same_level_path_def)
            with ‹targetnode x -xs'→⇘sl⇙* sourcenode ax›
            have "targetnode x -xs'@((ax#asx')@[a'])→⇘sl⇙* targetnode a'"
              by(rule slp_Append)
            with ‹∃Q r p fs. kind x = Q:r↪⇘p⇙fs› 
              ‹call_of_return_node (hd ms') (sourcenode x)›
              ‹as = xs@x#(xs'@ax#asx'@[a'])› ‹m' = targetnode a'›
            show ?thesis by simp blast
          next
            assume "ms = ms'" thus ?thesis by simp
          qed
        next
          assume "ms = targetnode a' # ms'"
          from ‹S,kind ⊢ (ms'',s'') -a'→⇩τ (m'#ms',s')› ‹kind a' = Q↩⇘p⇙f›
            ‹ms'' = sourcenode a' # targetnode a' # ms'›
          have "∃m ∈ set (targetnode a' # ms'). ∃m'. call_of_return_node m m' ∧ 
            m' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
            by(fastforce elim!:silent_move.cases simp:intra_kind_def)
          with ‹ms = targetnode a' # ms'› callstack
          have False by fastforce
          thus ?thesis by simp
        qed
      qed
    qed
  qed
qed


lemma silent_moves_called_node_in_slice1_hd_nodestack_in_slice1:
  assumes "S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')" and "valid_node m"
  and "CFG_node m' ∈ sum_SDG_slice1 nx"
  and "∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ 
      mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
  and "∀i < length rs. rs!i ∈ get_return_edges (cs!i)" and "ms = targetnodes rs"
  and "valid_return_list rs m" and "length rs = length cs"
  obtains as' a as'' where "as = as'@a#as''" and "∃Q r p fs. kind a = Q:r↪⇘p⇙fs"
  and "call_of_return_node (hd ms') (sourcenode a)"
  and "targetnode a -as''→⇘sl⇙* m'" and "CFG_node (sourcenode a) ∈ sum_SDG_slice1 nx"
  | "ms' = ms"
proof(atomize_elim)
  from ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')› ‹valid_node m›
    ‹∀i < length rs. rs!i ∈ get_return_edges (cs!i)› ‹ms = targetnodes rs›
    ‹valid_return_list rs m› ‹length rs = length cs›
  have "m -as→* m'"
    by(auto dest:silent_moves_vpa_path[of _ _ _ _ _ _ _ _ _ rs cs]
            simp:valid_call_list_def valid_return_list_def targetnodes_def)
  from ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')› ‹valid_node m›
    ‹∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    ‹∀i < length rs. rs!i ∈ get_return_edges (cs!i)› ‹ms = targetnodes rs›
    ‹valid_return_list rs m› ‹length rs = length cs›
  show "(∃as' a as''. as = as' @ a # as'' ∧ (∃Q r p fs. kind a = Q:r↪⇘p⇙fs) ∧
    call_of_return_node (hd ms') (sourcenode a) ∧ targetnode a -as''→⇘sl⇙* m' ∧
    CFG_node (sourcenode a) ∈ sum_SDG_slice1 nx) ∨ ms' = ms"
  proof(rule silent_moves_call_edge)
    fix as' a as'' assume "as = as'@a#as''" and "∃Q r p fs. kind a = Q:r↪⇘p⇙fs"
      and "call_of_return_node (hd ms') (sourcenode a)"
      and "targetnode a -as''→⇘sl⇙* m'"
    from ‹∃Q r p fs. kind a = Q:r↪⇘p⇙fs› obtain Q r p fs 
      where "kind a = Q:r↪⇘p⇙fs" by blast
    from ‹targetnode a -as''→⇘sl⇙* m'› obtain asx where "targetnode a -asx→⇩ι* m'"
      by -(erule same_level_path_inner_path)
    from ‹m -as→* m'› ‹as = as'@a#as''› have "valid_edge a"
      by(fastforce dest:path_split simp:vp_def)
    have "m' ≠ (_Exit_)"
    proof
      assume "m' = (_Exit_)"
      have "get_proc (_Exit_) = Main" by(rule get_proc_Exit)
      from ‹targetnode a -asx→⇩ι* m'›
      have "get_proc (targetnode a) = get_proc m'" by(rule intra_path_get_procs)
      with ‹m' = (_Exit_)› ‹get_proc (_Exit_) = Main›
      have "get_proc (targetnode a) = Main" by simp
      with ‹kind a = Q:r↪⇘p⇙fs› ‹valid_edge a›
      have "kind a = Q:r↪⇘Main⇙fs" by(fastforce dest:get_proc_call)
      with ‹valid_edge a› show False by(rule Main_no_call_target)
    qed
    show ?thesis
    proof(cases "targetnode a = m'")
      case True
      with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs›
      have "CFG_node (sourcenode a) s-p→⇘call⇙ CFG_node m'"
        by(fastforce intro:sum_SDG_call_edge)
      with ‹CFG_node m' ∈ sum_SDG_slice1 nx›
      have "CFG_node (sourcenode a) ∈ sum_SDG_slice1 nx" by -(rule call_slice1)
      with ‹as = as'@a#as''› ‹∃Q r p fs. kind a = Q:r↪⇘p⇙fs›
        ‹call_of_return_node (hd ms') (sourcenode a)›
        ‹targetnode a -as''→⇘sl⇙* m'› show ?thesis by blast
    next
      case False
      with ‹targetnode a -asx→⇩ι* m'› ‹m' ≠ (_Exit_)› ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs›
      obtain ns where "CFG_node (targetnode a) cd-ns→⇩d* CFG_node m'"
        by(fastforce elim!:in_proc_cdep_SDG_path)
      hence "CFG_node (targetnode a) is-ns→⇩d* CFG_node m'"
        by(fastforce intro:intra_SDG_path_is_SDG_path cdep_SDG_path_intra_SDG_path)
      with ‹CFG_node m' ∈ sum_SDG_slice1 nx›
      have "CFG_node (targetnode a) ∈ sum_SDG_slice1 nx"
        by -(rule is_SDG_path_slice1)
      from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs›
      have "CFG_node (sourcenode a) s-p→⇘call⇙ CFG_node (targetnode a)"
        by(fastforce intro:sum_SDG_call_edge)
      with ‹CFG_node (targetnode a) ∈ sum_SDG_slice1 nx›
      have "CFG_node (sourcenode a) ∈ sum_SDG_slice1 nx" by -(rule call_slice1)
      with ‹as = as'@a#as''› ‹∃Q r p fs. kind a = Q:r↪⇘p⇙fs›
        ‹call_of_return_node (hd ms') (sourcenode a)›
        ‹targetnode a -as''→⇘sl⇙* m'› show ?thesis by blast
    qed
  next
    assume "ms' = ms" thus ?thesis by simp
  qed
qed


lemma silent_moves_called_node_in_slice1_nodestack_in_slice1:
  "⟦S,kind ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s'); valid_node m; 
   CFG_node m' ∈ sum_SDG_slice1 nx; nx ∈ S;
   ∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
   ∀i < length rs. rs!i ∈ get_return_edges (cs!i); ms = targetnodes rs;
   valid_return_list rs m; length rs = length cs⟧
  ⟹ ∀mx ∈ set ms'. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
proof(induct ms' arbitrary:as m' s')
  case (Cons mx msx)
  note IH = ‹⋀as m' s'. ⟦S,kind ⊢ (m#ms,s) =as⇒⇩τ (m' # msx,s'); valid_node m; 
    CFG_node m' ∈ sum_SDG_slice1 nx; nx ∈ S;
   ∀mx∈set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
   ∀i<length rs. rs ! i ∈ get_return_edges (cs ! i); ms = targetnodes rs;
   valid_return_list rs m; length rs = length cs⟧
    ⟹ ∀mx∈set msx. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
  from ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m' # mx # msx,s')› ‹valid_node m›
    ‹CFG_node m' ∈ sum_SDG_slice1 nx›
    ‹∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    ‹∀i < length rs. rs!i ∈ get_return_edges (cs!i)› ‹ms = targetnodes rs›
    ‹valid_return_list rs m› ‹length rs = length cs›
  show ?case
  proof(rule silent_moves_called_node_in_slice1_hd_nodestack_in_slice1)
    fix as' a as'' assume "as = as'@a#as''" and "∃Q r p fs. kind a = Q:r↪⇘p⇙fs"
      and "call_of_return_node (hd (mx # msx)) (sourcenode a)" 
      and "CFG_node (sourcenode a) ∈ sum_SDG_slice1 nx"
      and "targetnode a -as''→⇘sl⇙* m'"
    from ‹CFG_node (sourcenode a) ∈ sum_SDG_slice1 nx› ‹nx ∈ S›
    have "sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙"
      by(fastforce intro:combSlice_refl simp:SDG_to_CFG_set_def HRB_slice_def)
    from ‹S,kind ⊢ (m#ms,s) =as⇒⇩τ (m' # mx # msx,s')› ‹as = as'@a#as''›
    obtain xs x where "S,kind ⊢ (m#ms,s) =as'⇒⇩τ (xs,x)"
      and "S,kind ⊢ (xs,x) =a#as''⇒⇩τ (m' # mx # msx,s')"
      by(fastforce elim:silent_moves_split)
    from ‹S,kind ⊢ (xs,x) =a#as''⇒⇩τ (m' # mx # msx,s')›
    obtain ys y where "S,kind ⊢ (xs,x) -a→⇩τ (ys,y)"
      and "S,kind ⊢ (ys,y) =as''⇒⇩τ (m' # mx # msx,s')"
      by(fastforce elim:silent_moves.cases)
    from ‹S,kind ⊢ (xs,x) -a→⇩τ (ys,y)› ‹∃Q r p fs. kind a = Q:r↪⇘p⇙fs›
    obtain xs' a' where "xs = sourcenode a#xs'" 
      and "ys = targetnode a#targetnode a'#xs'"
      apply - apply(erule silent_move.cases) apply(auto simp:intra_kind_def)
      by(cases xs,auto)+
    from ‹S,kind ⊢ (ys,y) =as''⇒⇩τ (m' # mx # msx,s')› 
      ‹ys = targetnode a#targetnode a'#xs'› ‹targetnode a -as''→⇘sl⇙* m'›
    have "mx = targetnode a'" and "xs' = msx" 
      by(auto dest:silent_moves_same_level_path)
    with ‹xs = sourcenode a#xs'› ‹S,kind ⊢ (m#ms,s) =as'⇒⇩τ (xs,x)›
    have "S,kind ⊢ (m#ms,s) =as'⇒⇩τ (sourcenode a#msx,x)" by simp
    from IH[OF ‹S,kind ⊢ (m#ms,s) =as'⇒⇩τ (sourcenode a#msx,x)› 
      ‹valid_node m› ‹CFG_node (sourcenode a) ∈ sum_SDG_slice1 nx› ‹nx ∈ S›
      ‹∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
      ‹∀i < length rs. rs!i ∈ get_return_edges (cs!i)› ‹ms = targetnodes rs›
      ‹valid_return_list rs m› ‹length rs = length cs›]
    have callstack:"∀mx∈set msx.
      ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙" .
    with ‹as = as'@a#as''› ‹call_of_return_node (hd (mx # msx)) (sourcenode a)› 
      ‹sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙› show ?thesis by fastforce
  next
    assume "mx # msx = ms"
    with ‹∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    show ?thesis by fastforce
  qed
qed simp


lemma silent_moves_slice_intra_path:
  assumes "S,slice_kind S ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')"
  and "∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
  shows "∀a ∈ set as. intra_kind (kind a)"
proof(rule ccontr)
  assume "¬ (∀a∈set as. intra_kind (kind a))"
  hence "∃a ∈ set as. ¬ intra_kind (kind a)" by fastforce
  then obtain asx ax asx' where "as = asx@ax#asx'" 
    and "∀a∈set asx. intra_kind (kind a)" and "¬ intra_kind (kind ax)"
    by(fastforce elim!:split_list_first_propE)
  from ‹S,slice_kind S ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')› ‹as = asx@ax#asx'›
  obtain msx sx msx' sx' where "S,slice_kind S ⊢ (m#ms,s) =asx⇒⇩τ (msx,sx)"
    and "S,slice_kind S ⊢ (msx,sx) -ax→⇩τ (msx',sx')"
    and "S,slice_kind S ⊢ (msx',sx') =asx'⇒⇩τ (m'#ms',s')"
    by(auto elim!:silent_moves_split elim:silent_moves.cases)
  from ‹S,slice_kind S ⊢ (msx,sx) -ax→⇩τ (msx',sx')› obtain xs
    where [simp]:"msx = sourcenode ax#xs" by(cases msx)(auto elim:silent_move.cases)
  from ‹S,slice_kind S ⊢ (m#ms,s) =asx⇒⇩τ (msx,sx)› ‹∀a∈set asx. intra_kind (kind a)›
  have [simp]:"xs = ms" by(fastforce dest:silent_moves_intra_path)
  show False
  proof(cases "kind ax" rule:edge_kind_cases)
    case Intra with ‹¬ intra_kind (kind ax)› show False by simp
  next
    case (Call Q r p fs)
    with ‹S,slice_kind S ⊢ (msx,sx) -ax→⇩τ (msx',sx')› 
      ‹∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    have "sourcenode ax ∉ ⌊HRB_slice S⌋⇘CFG⇙" and "pred (slice_kind S ax) sx"
      by(auto elim!:silent_move.cases simp:intra_kind_def)
    from ‹sourcenode ax ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind ax = Q:r↪⇘p⇙fs›
    have "slice_kind S ax = (λcf. False):r↪⇘p⇙fs"
      by(rule slice_kind_Call)
    with ‹pred (slice_kind S ax) sx› show False by(cases sx) auto
  next
    case (Return Q p f)
    with ‹S,slice_kind S ⊢ (msx,sx) -ax→⇩τ (msx',sx')› 
      ‹∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    show False by(fastforce elim!:silent_move.cases simp:intra_kind_def)
  qed
qed


lemma silent_moves_slice_keeps_state:
  assumes "S,slice_kind S ⊢ (m#ms,s) =as⇒⇩τ (m'#ms',s')"
  and "∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
  shows "s = s'"
proof -
  from assms have "∀a ∈ set as. intra_kind (kind a)"
    by(rule silent_moves_slice_intra_path)
  with assms show ?thesis
  proof(induct S "slice_kind S" "m#ms" s as "m'#ms'" s'
        arbitrary:m rule:silent_moves.induct)
    case (silent_moves_Nil sx n⇩c) thus ?case by simp
  next
    case (silent_moves_Cons S sx a msx' sx' as s'')
    note IH = ‹⋀m.
      ⟦msx' = m # ms;
      ∀mx∈set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙;
      ∀a∈set as. intra_kind (kind a)⟧ ⟹ sx' = s''›
    note callstack = ‹∀mx∈set ms. ∃mx'. call_of_return_node mx mx' ∧ 
      mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    from ‹∀a∈set (a # as). intra_kind (kind a)› have "intra_kind (kind a)"
      and "∀a∈set as. intra_kind (kind a)" by simp_all
    from ‹S,slice_kind S ⊢ (m # ms,sx) -a→⇩τ (msx',sx')› ‹intra_kind (kind a)›
      callstack
    have [simp]:"msx' = targetnode a#ms" and "sx' = transfer (slice_kind S a) sx"
      and "sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙" and "valid_edge a" and "sx ≠ []"
      by(auto elim!:silent_move.cases simp:intra_kind_def)
    from IH[OF ‹msx' = targetnode a#ms› callstack ‹∀a∈set as. intra_kind (kind a)›]
    have "sx' = s''" .
    from ‹intra_kind (kind a)›
    have "sx = sx'"
    proof(cases "kind a")
      case (UpdateEdge f')
      with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙›
      have "slice_kind S a = ⇑id" by(rule slice_kind_Upd)
      with ‹sx' = transfer (slice_kind S a) sx› ‹sx ≠ []›
      show ?thesis by(cases sx) auto
    next
      case (PredicateEdge Q)
      with ‹sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹valid_edge a›
      obtain Q' where "slice_kind S a = (Q')⇩√"
        by -(erule kind_Predicate_notin_slice_slice_kind_Predicate)
      with ‹sx' = transfer (slice_kind S a) sx› ‹sx ≠ []›
      show ?thesis by(cases sx) auto
    qed (auto simp:intra_kind_def)
    with ‹sx' = s''› show ?case by simp
  qed
qed


subsection ‹Definition of ‹slice_edges››

definition slice_edge :: "'node SDG_node set ⇒ 'edge list ⇒ 'edge ⇒ bool"
where "slice_edge S cs a ≡ (∀c ∈ set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙) ∧
  (case (kind a) of Q↩⇘p⇙f ⇒ True | _ ⇒ sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙)"


lemma silent_move_no_slice_edge:
  "⟦S,f ⊢ (ms,s) -a→⇩τ (ms',s'); tl ms = targetnodes rs; length rs = length cs;
    ∀i<length cs. call_of_return_node (tl ms!i) (sourcenode (cs!i))⟧
  ⟹ ¬ slice_edge S cs a"
proof(induct rule:silent_move.induct)
  case (silent_move_intra f a s s' ms S ms')
  note disj = ‹(∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙)
    ∨ hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙›
  from ‹pred (f a) s› ‹length ms = length s› obtain x xs where "ms = x#xs"
    by(cases ms) auto
  from ‹length rs = length cs› ‹tl ms = targetnodes rs›
  have "length (tl ms) = length cs" by(simp add:targetnodes_def)
  from disj show ?case
  proof
    assume "∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
    with ‹∀i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))›
      ‹length (tl ms) = length cs›
    have "∃c ∈ set cs. sourcenode c ∉ ⌊HRB_slice S⌋⇘CFG⇙"
      apply(auto simp:in_set_conv_nth)
      by(erule_tac x="i" in allE) auto
    thus ?thesis by(auto simp:slice_edge_def)
  next
    assume "hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙"
    with ‹hd ms = sourcenode a› ‹intra_kind (kind a)›
    show ?case by(auto simp:slice_edge_def simp:intra_kind_def)
  qed
next
  case (silent_move_call f a s s' Q r p fs a' ms S ms')
  note disj = ‹(∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙)
    ∨ hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙›
  from ‹pred (f a) s› ‹length ms = length s› obtain x xs where "ms = x#xs"
    by(cases ms) auto
  from ‹length rs = length cs› ‹tl ms = targetnodes rs›
  have "length (tl ms) = length cs" by(simp add:targetnodes_def)
  from disj show ?case
  proof
    assume "∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
    with ‹∀i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))›
      ‹length (tl ms) = length cs›
    have "∃c ∈ set cs. sourcenode c ∉ ⌊HRB_slice S⌋⇘CFG⇙"
      apply(auto simp:in_set_conv_nth)
      by(erule_tac x="i" in allE) auto
    thus ?thesis by(auto simp:slice_edge_def)
  next
    assume "hd ms ∉ ⌊HRB_slice S⌋⇘CFG⇙"
    with ‹hd ms = sourcenode a› ‹kind a = Q:r↪⇘p⇙fs›
    show ?case by(auto simp:slice_edge_def)
  qed
next
  case (silent_move_return f a s s' Q p f' ms S ms')
  from ‹pred (f a) s› ‹length ms = length s› obtain x xs where "ms = x#xs"
    by(cases ms) auto
  from ‹length rs = length cs› ‹tl ms = targetnodes rs›
  have "length (tl ms) = length cs" by(simp add:targetnodes_def)
  from ‹∀i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))›
    ‹∃m∈set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∉ ⌊HRB_slice S⌋⇘CFG⇙›
    ‹length (tl ms) = length cs›
  have "∃c ∈ set cs. sourcenode c ∉ ⌊HRB_slice S⌋⇘CFG⇙"
    apply(auto simp:in_set_conv_nth)
    by(erule_tac x="i" in allE) auto
  thus ?case by(auto simp:slice_edge_def)
qed


lemma observable_move_slice_edge:
  "⟦S,f ⊢ (ms,s) -a→ (ms',s'); tl ms = targetnodes rs; length rs = length cs;
    ∀i<length cs. call_of_return_node (tl ms!i) (sourcenode (cs!i))⟧
  ⟹ slice_edge S cs a"
proof(induct rule:observable_move.induct)
  case (observable_move_intra f a s s' ms S ms')
  from ‹pred (f a) s› ‹length ms = length s› obtain x xs where "ms = x#xs"
    by(cases ms) auto
  from ‹length rs = length cs› ‹tl ms = targetnodes rs›
  have "length (tl ms) = length cs" by(simp add:targetnodes_def)
  with ‹∀m∈set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    ‹∀i<length cs. call_of_return_node (tl ms!i) (sourcenode (cs!i))›
  have "∀c ∈ set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙"
    apply(auto simp:in_set_conv_nth)
    by(erule_tac x="i" in allE) auto
  with ‹hd ms = sourcenode a› ‹hd ms ∈ ⌊HRB_slice S⌋⇘CFG⇙› ‹intra_kind (kind a)›
  show ?case by(auto simp:slice_edge_def simp:intra_kind_def)
next
  case (observable_move_call f a s s' Q r p fs a' ms S ms')
  from ‹pred (f a) s› ‹length ms = length s› obtain x xs where "ms = x#xs"
    by(cases ms) auto
  from ‹length rs = length cs› ‹tl ms = targetnodes rs›
  have "length (tl ms) = length cs" by(simp add:targetnodes_def)
  with ‹∀m∈set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    ‹∀i<length cs. call_of_return_node (tl ms!i) (sourcenode (cs!i))›
  have "∀c ∈ set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙"
    apply(auto simp:in_set_conv_nth)
    by(erule_tac x="i" in allE) auto
  with ‹hd ms = sourcenode a› ‹hd ms ∈ ⌊HRB_slice S⌋⇘CFG⇙› ‹kind a = Q:r↪⇘p⇙fs›
  show ?case by(auto simp:slice_edge_def)
next
  case (observable_move_return f a s s' Q p f' ms S ms')
  from ‹pred (f a) s› ‹length ms = length s› obtain x xs where "ms = x#xs"
    by(cases ms) auto
  from ‹length rs = length cs› ‹tl ms = targetnodes rs›
  have "length (tl ms) = length cs" by(simp add:targetnodes_def)
  with ‹∀m∈set (tl ms). ∃m'. call_of_return_node m m' ∧ m' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    ‹∀i<length cs. call_of_return_node (tl ms!i) (sourcenode (cs!i))›
  have "∀c ∈ set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙"
    apply(auto simp:in_set_conv_nth)
    by(erule_tac x="i" in allE) auto
  with ‹kind a = Q↩⇘p⇙f'› show ?case by(auto simp:slice_edge_def)
qed



function slice_edges :: "'node SDG_node set ⇒ 'edge list ⇒ 'edge list ⇒ 'edge list"
where "slice_edges S cs [] = []"
  | "slice_edge S cs a ⟹ 
     slice_edges S cs (a#as) = a#slice_edges S (upd_cs cs [a]) as"
  | "¬ slice_edge S cs a ⟹ 
     slice_edges S cs (a#as) = slice_edges S (upd_cs cs [a]) as"
by(atomize_elim)(auto,case_tac b,auto)
termination by(lexicographic_order)


lemma slice_edges_Append:
  "⟦slice_edges S cs as = as'; slice_edges S (upd_cs cs as) asx = asx'⟧
  ⟹ slice_edges S cs (as@asx) = as'@asx'"
proof(induct as arbitrary:cs as')
  case Nil thus ?case by simp
next
  case (Cons x xs)
  note IH = ‹⋀cs as'. ⟦slice_edges S cs xs = as'; 
    slice_edges S (upd_cs cs xs) asx = asx'⟧
    ⟹ slice_edges S cs (xs @ asx) = as' @ asx'›
  from ‹slice_edges S (upd_cs cs (x # xs)) asx = asx'› 
  have "slice_edges S (upd_cs (upd_cs cs [x]) xs) asx = asx'"
    by(cases "kind x")(auto,cases cs,auto)
  show ?case
  proof(cases "slice_edge S cs x")
    case True
    with ‹slice_edges S cs (x # xs) = as'›
    have "x#slice_edges S (upd_cs cs [x]) xs = as'" by simp
    then obtain xs' where "as' = x#xs'"
      and "slice_edges S (upd_cs cs [x]) xs = xs'" by(cases as') auto
    from IH[OF ‹slice_edges S (upd_cs cs [x]) xs = xs'›
      ‹slice_edges S (upd_cs (upd_cs cs [x]) xs) asx = asx'›]
    have "slice_edges S (upd_cs cs [x]) (xs @ asx) = xs' @ asx'" .
    with True ‹as' = x#xs'› show ?thesis by simp
  next
    case False
    with ‹slice_edges S cs (x # xs) = as'›
    have "slice_edges S (upd_cs cs [x]) xs = as'" by simp
    from IH[OF this ‹slice_edges S (upd_cs (upd_cs cs [x]) xs) asx = asx'›]
    have "slice_edges S (upd_cs cs [x]) (xs @ asx) = as' @ asx'" .
    with False show ?thesis by simp
  qed
qed


lemma slice_edges_Nil_split:
  "slice_edges S cs (as@as') = []
  ⟹ slice_edges S cs as = [] ∧ slice_edges S (upd_cs cs as) as' = []"
apply(induct as arbitrary:cs)
 apply clarsimp
apply(case_tac "slice_edge S cs a") apply auto
apply(case_tac "kind a") apply auto
apply(case_tac cs) apply auto
done


lemma slice_intra_edges_no_nodes_in_slice:
  "⟦slice_edges S cs as = []; ∀a ∈ set as. intra_kind (kind a);
    ∀c ∈ set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙⟧
  ⟹ ∀nx ∈ set(sourcenodes as). nx ∉ ⌊HRB_slice S⌋⇘CFG⇙"
proof(induct as)
  case Nil thus ?case by(fastforce simp:sourcenodes_def)
next
  case (Cons a' as')
  note IH = ‹ ⟦slice_edges S cs as' = []; ∀a∈set as'. intra_kind (kind a);
    ∀c∈set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙⟧
    ⟹ ∀nx∈set (sourcenodes as'). nx ∉ ⌊HRB_slice S⌋⇘CFG⇙›
  from ‹∀a∈set (a' # as'). intra_kind (kind a)›
  have "intra_kind (kind a')" and "∀a∈set as'. intra_kind (kind a)" by simp_all
  from ‹slice_edges S cs (a' # as') = []› ‹intra_kind (kind a')›
    ‹∀c∈set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙›
  have "sourcenode a' ∉ ⌊HRB_slice S⌋⇘CFG⇙" and "slice_edges S cs as' = []"
    by(cases "slice_edge S cs a'",auto simp:intra_kind_def slice_edge_def)+
  from IH[OF ‹slice_edges S cs as' = []› ‹∀a∈set as'. intra_kind (kind a)›
    ‹∀c∈set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙›] 
  have "∀nx∈set (sourcenodes as'). nx ∉ ⌊HRB_slice S⌋⇘CFG⇙" .
  with ‹sourcenode a' ∉ ⌊HRB_slice S⌋⇘CFG⇙› show ?case by(simp add:sourcenodes_def)
qed


lemma silent_moves_no_slice_edges:
  "⟦S,f ⊢ (ms,s) =as⇒⇩τ (ms',s'); tl ms = targetnodes rs; length rs = length cs;
    ∀i<length cs. call_of_return_node (tl ms!i) (sourcenode (cs!i))⟧
  ⟹ slice_edges S cs as = [] ∧ (∃rs'. tl ms' = targetnodes rs' ∧
  length rs' = length (upd_cs cs as) ∧ (∀i<length (upd_cs cs as). 
  call_of_return_node (tl ms'!i) (sourcenode ((upd_cs cs as)!i))))"
proof(induct arbitrary:rs cs rule:silent_moves.induct)
  case (silent_moves_Cons S f ms s a ms' s' as ms'' s'')
  from ‹S,f ⊢ (ms,s) -a→⇩τ (ms',s')› ‹tl ms = targetnodes rs› ‹length rs = length cs›
    ‹∀i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))›
  have "¬ slice_edge S cs a" by(rule silent_move_no_slice_edge)
  with silent_moves_Cons show ?case
  proof(induct rule:silent_move.induct)
    case (silent_move_intra f a s s' ms S ms')
    note IH = ‹⋀rs cs. ⟦tl ms' = targetnodes rs; length rs = length cs;
      ∀i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))⟧
      ⟹ slice_edges S cs as = [] ∧ (∃rs'. tl ms'' = targetnodes rs' ∧
      length rs' = length (upd_cs cs as) ∧ (∀i<length (upd_cs cs as).
      call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i))))›
    from ‹ms' = targetnode a # tl ms› ‹tl ms = targetnodes rs›
    have "tl ms' = targetnodes rs" by simp
    from ‹ms' = targetnode a # tl ms› ‹tl ms = targetnodes rs›
      ‹∀i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))›
    have "∀i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))"
      by simp
    from IH[OF ‹tl ms' = targetnodes rs› ‹length rs = length cs› this]
    have "slice_edges S cs as = []" 
      and "∃rs'. tl ms'' = targetnodes rs' ∧ length rs' = length (upd_cs cs as) ∧
      (∀i<length (upd_cs cs as). 
      call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i)))" by simp_all
    with ‹intra_kind (kind a)› ‹¬ slice_edge S cs a›
    show ?case by(fastforce simp:intra_kind_def)
  next
    case (silent_move_call f a s s' Q r p fs a' ms S ms')
    note IH = ‹⋀rs cs. ⟦tl ms' = targetnodes rs; length rs = length cs;
      ∀i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))⟧
      ⟹ slice_edges S cs as = [] ∧ (∃rs'. tl ms'' = targetnodes rs' ∧
      length rs' = length (upd_cs cs as) ∧ (∀i<length (upd_cs cs as).
      call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i))))›
    from ‹tl ms = targetnodes rs› ‹ms' = targetnode a # targetnode a' # tl ms›
    have "tl ms' = targetnodes (a'#rs)" by(simp add:targetnodes_def)
    from ‹length rs = length cs› have "length (a'#rs) = length (a#cs)" by simp
    from ‹valid_edge a'› ‹valid_edge a› ‹a' ∈ get_return_edges a›
    have "return_node (targetnode a')" by(fastforce simp:return_node_def)
    with ‹valid_edge a› ‹valid_edge a'› ‹a' ∈ get_return_edges a›
    have "call_of_return_node (targetnode a') (sourcenode a)"
      by(simp add:call_of_return_node_def) blast
    with ‹∀i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))›
      ‹ms' = targetnode a # targetnode a' # tl ms›
    have "∀i<length (a#cs). 
      call_of_return_node (tl ms' ! i) (sourcenode ((a#cs) ! i))"
      by auto (case_tac i,auto)
    from IH[OF ‹tl ms' = targetnodes (a'#rs)› ‹length (a'#rs) = length (a#cs)› this]
    have "slice_edges S (a # cs) as = []"
      and "∃rs'. tl ms'' = targetnodes rs' ∧
      length rs' = length (upd_cs (a # cs) as) ∧
      (∀i<length (upd_cs (a # cs) as).
        call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs (a # cs) as ! i)))"
      by simp_all
    with ‹¬ slice_edge S cs a› ‹kind a = Q:r↪⇘p⇙fs› show ?case by simp
  next
    case (silent_move_return f a s s' Q p f' ms S ms')
    note IH = ‹⋀rs cs. ⟦tl ms' = targetnodes rs; length rs = length cs;
      ∀i<length cs. call_of_return_node (tl ms' ! i) (sourcenode (cs ! i))⟧
      ⟹ slice_edges S cs as = [] ∧ (∃rs'. tl ms'' = targetnodes rs' ∧
      length rs' = length (upd_cs cs as) ∧ (∀i<length (upd_cs cs as).
      call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs as ! i))))›
    from ‹length s = Suc (length s')› ‹s' ≠ []› ‹length ms = length s› ‹ms' = tl ms›
    obtain x xs where [simp]:"ms' = x#xs" by(cases ms)(auto,case_tac ms',auto)
    from ‹ms' = tl ms› ‹tl ms = targetnodes rs› obtain r' rs' where "rs = r'#rs'"
      and "x = targetnode r'" and "tl ms' = targetnodes rs'"
      by(cases rs)(auto simp:targetnodes_def)
    from ‹length rs = length cs› ‹rs = r'#rs'› obtain c' cs' where "cs = c'#cs'"
      and "length rs' = length cs'" by(cases cs) auto
    from ‹∀i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))›
      ‹cs = c'#cs'› ‹ms' = tl ms›
    have "∀i<length cs'. call_of_return_node (tl ms' ! i) (sourcenode (cs' ! i))"
      by auto(erule_tac x="Suc i" in allE,cases "tl ms",auto)
    from IH[OF ‹tl ms' = targetnodes rs'› ‹length rs' = length cs'› this]
    have "slice_edges S cs' as = []" and "∃rs'. tl ms'' = targetnodes rs' ∧
      length rs' = length (upd_cs cs' as) ∧ (∀i<length (upd_cs cs' as).
      call_of_return_node (tl ms'' ! i) (sourcenode (upd_cs cs' as ! i)))"
      by simp_all
    with ‹¬ slice_edge S cs a› ‹kind a = Q↩⇘p⇙f'› ‹cs = c'#cs'›
    show ?case by simp
  qed
qed fastforce



lemma observable_moves_singular_slice_edge:
  "⟦S,f ⊢ (ms,s) =as⇒ (ms',s'); tl ms = targetnodes rs; length rs = length cs;
    ∀i<length cs. call_of_return_node (tl ms!i) (sourcenode (cs!i))⟧
  ⟹ slice_edges S cs as = [last as]"
proof(induct rule:observable_moves.induct)
  case (observable_moves_snoc S f ms s as ms' s' a ms'' s'')
  from ‹S,f ⊢ (ms,s) =as⇒⇩τ (ms',s')› ‹tl ms = targetnodes rs› ‹length rs = length cs›
    ‹∀i<length cs. call_of_return_node (tl ms ! i) (sourcenode (cs ! i))›
  obtain rs' where "slice_edges S cs as = []" 
    and "tl ms' = targetnodes rs'" and "length rs' = length (upd_cs cs as)"
    and "∀i<length (upd_cs cs as). 
    call_of_return_node (tl ms'!i) (sourcenode ((upd_cs cs as)!i))"
    by(fastforce dest!:silent_moves_no_slice_edges)
  from ‹S,f ⊢ (ms',s') -a→ (ms'',s'')› this
  have "slice_edge S (upd_cs cs as) a" by -(rule observable_move_slice_edge)
  with ‹slice_edges S cs as = []› have "slice_edges S cs (as @ [a]) = []@[a]"
    by(fastforce intro:slice_edges_Append)
  thus ?case by simp
qed


lemma silent_moves_nonempty_nodestack_False:
  assumes "S,kind ⊢ ([m],[cf]) =as⇒⇩τ (m'#ms',s')" and "valid_node m"
  and "ms' ≠ []" and "CFG_node m' ∈ sum_SDG_slice1 nx" and "nx ∈ S"
  shows False
proof -
  from assms(1-4) have "slice_edges S [] as ≠ []"
  proof(induct ms' arbitrary:as m' s')
    case (Cons mx msx)
    note IH = ‹⋀as m' s'. ⟦S,kind ⊢ ([m],[cf]) =as⇒⇩τ (m' # msx,s'); valid_node m; 
      msx ≠ []; CFG_node m' ∈ sum_SDG_slice1 nx⟧
      ⟹ slice_edges S [] as ≠ []›
    from ‹S,kind ⊢ ([m],[cf]) =as⇒⇩τ (m' # mx # msx,s')› ‹valid_node m›
      ‹CFG_node m' ∈ sum_SDG_slice1 nx›
    obtain as' a as'' where "as = as'@a#as''" and "∃Q r p fs. kind a = Q:r↪⇘p⇙fs"
      and "call_of_return_node mx (sourcenode a)" 
      and "CFG_node (sourcenode a) ∈ sum_SDG_slice1 nx"
      and "targetnode a -as''→⇘sl⇙* m'"
      by(fastforce elim!:silent_moves_called_node_in_slice1_hd_nodestack_in_slice1
      [of _ _ _ _ _ _ _ _ _ "[]" "[]"] simp:targetnodes_def valid_return_list_def)
    from ‹S,kind ⊢ ([m],[cf]) =as⇒⇩τ (m' # mx # msx,s')› ‹as = as'@a#as''›
    obtain xs x where "S,kind ⊢ ([m],[cf]) =as'⇒⇩τ (xs,x)"
      and "S,kind ⊢ (xs,x) =a#as''⇒⇩τ (m' # mx # msx,s')"
      by(fastforce elim:silent_moves_split)
    from ‹S,kind ⊢ (xs,x) =a#as''⇒⇩τ (m' # mx # msx,s')›
    obtain ys y where "S,kind ⊢ (xs,x) -a→⇩τ (ys,y)"
      and "S,kind ⊢ (ys,y) =as''⇒⇩τ (m' # mx # msx,s')"
      by(fastforce elim:silent_moves.cases)
    from ‹S,kind ⊢ (xs,x) -a→⇩τ (ys,y)› ‹∃Q r p fs. kind a = Q:r↪⇘p⇙fs›
    obtain xs' a' where "xs = sourcenode a#xs'" 
      and "ys = targetnode a#targetnode a'#xs'"
      apply - apply(erule silent_move.cases) apply(auto simp:intra_kind_def)
      by(cases xs,auto)+
    from ‹S,kind ⊢ (ys,y) =as''⇒⇩τ (m' # mx # msx,s')› 
      ‹ys = targetnode a#targetnode a'#xs'› ‹targetnode a -as''→⇘sl⇙* m'›
    have "mx = targetnode a'" and "xs' = msx"
      by(auto dest:silent_moves_same_level_path)
    with ‹xs = sourcenode a#xs'› ‹S,kind ⊢ ([m],[cf]) =as'⇒⇩τ (xs,x)›
    have "S,kind ⊢ ([m],[cf]) =as'⇒⇩τ (sourcenode a#msx,x)" by simp
    show ?case
    proof(cases "msx = []")
      case True
      from ‹S,kind ⊢ ([m],[cf]) =as'⇒⇩τ (sourcenode a#msx,x)›
      obtain rs' where "msx = targetnodes rs' ∧ length rs' = length (upd_cs [] as')"
        by(fastforce dest!:silent_moves_no_slice_edges[where cs="[]" and rs="[]"]
                    simp:targetnodes_def)
      with True have "upd_cs [] as' = []"  by(cases rs')(auto simp:targetnodes_def)
      with ‹CFG_node (sourcenode a) ∈ sum_SDG_slice1 nx› ‹nx ∈ S›
      have "slice_edge S (upd_cs [] as') a"
        by(cases "kind a",auto intro:combSlice_refl 
          simp:slice_edge_def SDG_to_CFG_set_def HRB_slice_def)
      hence "slice_edges S (upd_cs [] as') (a#as'') ≠ []" by simp
      with ‹as = as'@a#as''› show ?thesis by(fastforce dest:slice_edges_Nil_split)
    next
      case False
      from IH[OF ‹S,kind ⊢ ([m],[cf]) =as'⇒⇩τ (sourcenode a#msx,x)› 
        ‹valid_node m› this ‹CFG_node (sourcenode a) ∈ sum_SDG_slice1 nx›]
      have "slice_edges S [] as' ≠ []" .
      with ‹as = as'@a#as''› show ?thesis by(fastforce dest:slice_edges_Nil_split)
    qed
  qed simp
  moreover
  from ‹S,kind ⊢ ([m],[cf]) =as⇒⇩τ (m'#ms',s')› have "slice_edges S [] as = []"
    by(fastforce dest!:silent_moves_no_slice_edges[where cs="[]" and rs="[]"] 
                simp:targetnodes_def)
  ultimately show False by simp
qed



lemma transfers_intra_slice_kinds_slice_edges:
  "⟦∀a ∈ set as. intra_kind (kind a); ∀c ∈ set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙⟧
  ⟹ transfers (slice_kinds S (slice_edges S cs as)) s =
  transfers (slice_kinds S as) s"
proof(induct as arbitrary:s)
  case Nil thus ?case by(simp add:slice_kinds_def)
next
  case (Cons a' as')
  note IH = ‹⋀s. ⟦∀a∈set as'. intra_kind (kind a);
    ∀c∈set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙⟧ ⟹
    transfers (slice_kinds S (slice_edges S cs as')) s =
    transfers (slice_kinds S as') s›
  from ‹∀a∈set (a' # as'). intra_kind (kind a)›
  have "intra_kind (kind a')" and "∀a∈set as'. intra_kind (kind a)"
    by simp_all
  show ?case
  proof(cases "slice_edge S cs a'")
    case True
    with ‹intra_kind (kind a')›
    have eq:"transfers (slice_kinds S (slice_edges S cs (a'#as'))) s
            = transfers (slice_kinds S (slice_edges S cs as')) 
                (transfer (slice_kind S a') s)"
      by(cases "kind a'")(auto simp:slice_kinds_def intra_kind_def)
    have "transfers (slice_kinds S (a'#as')) s
        = transfers (slice_kinds S as') (transfer (slice_kind S a') s)"
      by(simp add:slice_kinds_def)
    with eq IH[OF ‹∀a∈set as'. intra_kind (kind a)› 
      ‹∀c∈set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙›,
      of "transfer (slice_kind S a') s"]
    show ?thesis by simp
  next
    case False
    with ‹intra_kind (kind a')›
    have eq:"transfers (slice_kinds S (slice_edges S cs (a'#as'))) s
            = transfers (slice_kinds S (slice_edges S cs as')) s"
      by(cases "kind a'")(auto simp:slice_kinds_def intra_kind_def)
    from False ‹intra_kind (kind a')› ‹∀c∈set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    have "sourcenode a' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
      by(fastforce simp:slice_edge_def intra_kind_def)
    with ‹intra_kind (kind a')› have "transfer (slice_kind S a') s = s"
      by(cases s)(auto,cases "kind a'",
        auto simp:slice_kind_def Let_def intra_kind_def)
    hence "transfers (slice_kinds S (a'#as')) s
         = transfers (slice_kinds S as') s"
      by(simp add:slice_kinds_def)
    with eq IH[OF ‹∀a∈set as'. intra_kind (kind a)› 
      ‹∀c∈set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙›,of s] show ?thesis by simp
  qed
qed



lemma exists_sliced_intra_path_preds:
  assumes "m -as→⇩ι* m'" and "slice_edges S cs as = []" 
  and "m' ∈ ⌊HRB_slice S⌋⇘CFG⇙" and "∀c ∈ set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙"
  obtains as' where "m -as'→⇩ι* m'" and "preds (slice_kinds S as') (cf#cfs)"
  and "slice_edges S cs as' = []"
proof(atomize_elim)
  from ‹m -as→⇩ι* m'› have "m -as→* m'" and "∀a ∈ set as. intra_kind(kind a)"
    by(simp_all add:intra_path_def)
  from ‹slice_edges S cs as = []› ‹∀a ∈ set as. intra_kind(kind a)›
    ‹∀c ∈ set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙›
  have "∀nx ∈ set(sourcenodes as). nx ∉ ⌊HRB_slice S⌋⇘CFG⇙"
    by(rule slice_intra_edges_no_nodes_in_slice)
  with ‹m -as→⇩ι* m'› ‹m' ∈ ⌊HRB_slice S⌋⇘CFG⇙› have "m' ∈ obs_intra m ⌊HRB_slice S⌋⇘CFG⇙"
    by(fastforce intro:obs_intra_elem)
  hence "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m'}" by(rule obs_intra_singleton_element)
  from ‹m -as→* m'› have "valid_node m" and "valid_node m'"
    by(fastforce dest:path_valid_node)+
  from ‹m -as→⇩ι* m'› obtain x where "distance m m' x" and "x ≤ length as"
    by(erule every_path_distance)
  from ‹distance m m' x› ‹obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m'}›
  show "∃as'. m -as'→⇩ι* m' ∧ preds (slice_kinds S as') (cf#cfs) ∧ 
              slice_edges S cs as' = []"
  proof(induct x arbitrary:m rule:nat.induct)
    case zero
    from ‹distance m m' 0› have "m = m'"
      by(fastforce elim:distance.cases simp:intra_path_def)
    with ‹valid_node m'› show ?case
      by(rule_tac x="[]" in exI,
        auto intro:empty_path simp:slice_kinds_def intra_path_def)
  next
    case (Suc x)
    note IH = ‹⋀m. ⟦distance m m' x; obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m'}⟧
      ⟹ ∃as'. m -as'→⇩ι* m' ∧ preds (slice_kinds S as') (cf # cfs) ∧
               slice_edges S cs as' = []›
    from ‹distance m m' (Suc x)› obtain a 
      where "valid_edge a" and "m = sourcenode a" and "intra_kind(kind a)"
      and "distance (targetnode a) m' x"
      and target:"targetnode a = (SOME nx. ∃a'. sourcenode a = sourcenode a' ∧ 
      distance (targetnode a') m' x ∧
      valid_edge a' ∧ intra_kind(kind a') ∧ targetnode a' = nx)"
      by(auto elim:distance_successor_distance)
    have "m ∉ ⌊HRB_slice S⌋⇘CFG⇙"
    proof
      assume "m ∈ ⌊HRB_slice S⌋⇘CFG⇙"
      from ‹valid_edge a› ‹m = sourcenode a› have "valid_node m" by simp
      with ‹m ∈ ⌊HRB_slice S⌋⇘CFG⇙› have "obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m}"
        by -(rule n_in_obs_intra)
      with ‹obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m'}› have "m = m'" by simp
      with ‹valid_node m› have "m -[]→⇩ι* m'" 
        by(fastforce intro:empty_path simp:intra_path_def)
      with ‹distance m m' (Suc x)› show False
        by(fastforce elim:distance.cases)
    qed
    from ‹distance (targetnode a) m' x› ‹m' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    obtain mx where "mx ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙"
      by(fastforce elim:distance.cases path_ex_obs_intra)
    from ‹valid_edge a› ‹intra_kind(kind a)› ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a›
    have "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ ⊆ 
      obs_intra (sourcenode a) ⌊HRB_slice S⌋⇘CFG⇙"
      by -(rule edge_obs_intra_subset,auto)
    with ‹mx ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a›
      ‹obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m'}›
    have "m' ∈ obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙" by auto
    hence "obs_intra (targetnode a) ⌊HRB_slice S⌋⇘CFG⇙ = {m'}" 
      by(rule obs_intra_singleton_element)
    from IH[OF ‹distance (targetnode a) m' x› this]
    obtain as where "targetnode a -as→⇩ι* m'" and "preds (slice_kinds S as) (cf#cfs)"
      and "slice_edges S cs as = []" by blast
    from ‹targetnode a -as→⇩ι* m'› ‹valid_edge a› ‹intra_kind(kind a)› 
      ‹m = sourcenode a›
    have "m -a#as→⇩ι* m'" by(fastforce intro:Cons_path simp:intra_path_def)
    from ‹∀c ∈ set cs. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙› ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙›
      ‹m = sourcenode a› ‹intra_kind(kind a)›
    have "¬ slice_edge S cs a" by(fastforce simp:slice_edge_def intra_kind_def)
    with ‹slice_edges S cs as = []› ‹intra_kind(kind a)› 
    have "slice_edges S cs (a#as) = []" by(fastforce simp:intra_kind_def)
    from ‹intra_kind(kind a)›
    show ?case
    proof(cases "kind a")
      case (UpdateEdge f)
      with ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a› have "slice_kind S a = ⇑id"
        by(fastforce intro:slice_kind_Upd)
      hence "transfer (slice_kind S a) (cf#cfs) = (cf#cfs)" 
        and "pred (slice_kind S a) (cf#cfs)" by simp_all
      with ‹preds (slice_kinds S as) (cf#cfs)› 
      have "preds (slice_kinds S (a#as)) (cf#cfs)"
        by(simp add:slice_kinds_def)
      with ‹m -a#as→⇩ι* m'› ‹slice_edges S cs (a#as) = []› show ?thesis
        by blast
    next
      case (PredicateEdge Q)
      with ‹m ∉ ⌊HRB_slice S⌋⇘CFG⇙› ‹m = sourcenode a› ‹distance m m' (Suc x)›  
        ‹obs_intra m ⌊HRB_slice S⌋⇘CFG⇙ = {m'}› ‹distance (targetnode a) m' x›
        target
      have "slice_kind S a = (λs. True)⇩√"
        by(fastforce intro:slice_kind_Pred_obs_nearer_SOME)
      hence "transfer (slice_kind S a) (cf#cfs) = (cf#cfs)" 
        and "pred (slice_kind S a) (cf#cfs)" by simp_all
      with ‹preds (slice_kinds S as) (cf#cfs)› 
      have "preds (slice_kinds S (a#as)) (cf#cfs)"
        by(simp add:slice_kinds_def)
      with ‹m -a#as→⇩ι* m'› ‹slice_edges S cs (a#as) = []› show ?thesis by blast
    qed (auto simp:intra_kind_def)
  qed
qed


lemma slp_to_intra_path_with_slice_edges:
  assumes "n -as→⇘sl⇙* n'" and "slice_edges S cs as = []"
  obtains as' where "n -as'→⇩ι* n'" and "slice_edges S cs as' = []"
proof(atomize_elim)
  from ‹n -as→⇘sl⇙* n'› have "n -as→* n'" and "same_level_path as"
    by(simp_all add:slp_def)
  from ‹same_level_path as› have "same_level_path_aux [] as" and "upd_cs [] as = []"
    by(simp_all add:same_level_path_def)
  from ‹n -as→* n'› ‹same_level_path_aux [] as› ‹upd_cs [] as = []› 
    ‹slice_edges S cs as = []›
  show "∃as'. n -as'→⇩ι* n' ∧ slice_edges S cs as' = []"
  proof(induct as arbitrary:n cs rule:length_induct)
    fix as n cs
    assume IH:"∀as''. length as'' < length as ⟶
      (∀n''. n'' -as''→* n' ⟶ same_level_path_aux [] as'' ⟶
           upd_cs [] as'' = [] ⟶ (∀cs'. slice_edges S cs' as'' = [] ⟶
           (∃as'. n'' -as'→⇩ι* n' ∧ slice_edges S cs' as' = [])))"
      and "n -as→* n'" and "same_level_path_aux [] as" and "upd_cs [] as = []"
      and "slice_edges S cs as = []"
    show "∃as'. n -as'→⇩ι* n' ∧ slice_edges S cs as' = []"
    proof(cases as)
      case Nil
      with ‹n -as→* n'› show ?thesis by(fastforce simp:intra_path_def)
    next
      case (Cons a' as')
      with ‹n -as→* n'› Cons have "n = sourcenode a'" and "valid_edge a'" 
        and "targetnode a' -as'→* n'"
        by(auto intro:path_split_Cons)
      show ?thesis
      proof(cases "kind a'" rule:edge_kind_cases)
        case Intra
        with Cons ‹same_level_path_aux [] as› have "same_level_path_aux [] as'"
          by(fastforce simp:intra_kind_def)
        moreover
        from Intra Cons ‹upd_cs [] as = []› have "upd_cs [] as' = []"
          by(fastforce simp:intra_kind_def)
        moreover
        from ‹slice_edges S cs as = []› Cons Intra
        have "slice_edges S cs as' = []" and "¬ slice_edge S cs a'"
          by(cases "slice_edge S cs a'",auto simp:intra_kind_def)+
        ultimately obtain as'' where "targetnode a' -as''→⇩ι* n'"
          and "slice_edges S cs as'' = []"
          using IH Cons ‹targetnode a' -as'→* n'›
          by(erule_tac x="as'" in allE) auto
        from ‹n = sourcenode a'› ‹valid_edge a'› Intra ‹targetnode a' -as''→⇩ι* n'›
        have "n -a'#as''→⇩ι* n'" by(fastforce intro:Cons_path simp:intra_path_def)
        moreover
        from ‹slice_edges S cs as'' = []› ‹¬ slice_edge S cs a'› Intra
        have "slice_edges S cs (a'#as'') = []" by(auto simp:intra_kind_def)
        ultimately show ?thesis by blast
      next
        case (Call Q r p f)
        with Cons ‹same_level_path_aux [] as›
        have "same_level_path_aux [a'] as'" by simp
        from Call Cons ‹upd_cs [] as = []› have "upd_cs [a'] as' = []"
          by simp
        hence "as' ≠ []" by fastforce
        with ‹upd_cs [a'] as' = []› obtain xs ys where "as' = xs@ys" and "xs ≠ []"
        and "upd_cs [a'] xs = []" and "upd_cs [] ys = []"
        and "∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs [a'] xs' ≠ []"
          by -(erule upd_cs_empty_split,auto)
        from ‹same_level_path_aux [a'] as'› ‹as' = xs@ys› ‹upd_cs [a'] xs = []›
        have "same_level_path_aux [a'] xs"  and "same_level_path_aux [] ys"
          by(rule slpa_split)+
        with ‹upd_cs [a'] xs = []› have "upd_cs ([a']@cs) xs = []@cs"
          by(fastforce intro:same_level_path_upd_cs_callstack_Append)
        from ‹slice_edges S cs as = []› Cons Call
        have "slice_edges S (a'#cs) as' = []" and "¬ slice_edge S cs a'"
          by(cases "slice_edge S cs a'",auto)+
        from ‹slice_edges S (a'#cs) as' = []› ‹as' = xs@ys› 
          ‹upd_cs ([a']@cs) xs = []@cs›
        have "slice_edges S cs ys = []" 
          by(fastforce dest:slice_edges_Nil_split)
        from ‹same_level_path_aux [a'] xs› ‹upd_cs [a'] xs = []›
          ‹∀xs' ys'. xs = xs'@ys' ∧ ys' ≠ [] ⟶ upd_cs [a'] xs' ≠ []›
        have "last xs ∈ get_return_edges (last [a'])"
          by(fastforce intro!:slpa_get_return_edges)
        with ‹valid_edge a'› Call
        obtain a where "valid_edge a" and "sourcenode a = sourcenode a'"
          and "targetnode a = targetnode (last xs)" and "kind a = (λcf. False)⇩√"
          by -(drule call_return_node_edge,auto)
        from ‹targetnode a = targetnode (last xs)› ‹xs ≠ []›
        have "targetnode a = targetnode (last (a'#xs))" by simp
        from ‹as' = xs@ys› ‹xs ≠ []› Cons have "length ys < length as" by simp
        from ‹targetnode a' -as'→* n'› ‹as' = xs@ys› ‹xs ≠ []›
        have "targetnode (last (a'#xs)) -ys→* n'"
          by(cases xs rule:rev_cases,auto dest:path_split)
        with IH ‹length ys < length as› ‹same_level_path_aux [] ys›
          ‹upd_cs [] ys = []› ‹slice_edges S cs ys = []›
        obtain as'' where "targetnode (last (a'#xs)) -as''→⇩ι* n'"
          and "slice_edges S cs as'' = []"
          apply(erule_tac x="ys" in allE) apply clarsimp
          apply(erule_tac x="targetnode (last (a'#xs))" in allE) 
          apply clarsimp apply(erule_tac x="cs" in allE)
          by clarsimp
        from ‹sourcenode a = sourcenode a'› ‹n = sourcenode a'›
          ‹targetnode a = targetnode (last (a'#xs))› ‹valid_edge a›
          ‹kind a = (λcf. False)⇩√› ‹targetnode (last (a'#xs)) -as''→⇩ι* n'›
        have "n -a#as''→⇩ι* n'"
          by(fastforce intro:Cons_path simp:intra_path_def intra_kind_def)
        moreover
        from ‹kind a = (λcf. False)⇩√› ‹slice_edges S cs as'' = []›
          ‹¬ slice_edge S cs a'› ‹sourcenode a = sourcenode a'›
        have "slice_edges S cs (a#as'') = []" 
          by(cases "kind a'")(auto simp:slice_edge_def)
        ultimately show ?thesis by blast
      next
        case (Return Q p f)
        with Cons ‹same_level_path_aux [] as› have False by simp
        thus ?thesis by simp
      qed
    qed
  qed
qed


subsection ‹‹S,f ⊢ (ms,s) =as⇒* (ms',s')› : the reflexive transitive 
  closure of ‹S,f ⊢ (ms,s) =as⇒ (ms',s')››


inductive trans_observable_moves :: 
  "'node SDG_node set ⇒ ('edge ⇒ ('var,'val,'ret,'pname) edge_kind) ⇒ 'node list ⇒ 
   (('var ⇀ 'val) × 'ret) list ⇒ 'edge list ⇒ 'node list ⇒ 
  (('var ⇀ 'val) × 'ret) list ⇒ bool"
("_,_ ⊢ '(_,_') =_⇒* '(_,_')" [51,50,0,0,50,0,0] 51) 

where tom_Nil:
  "length ms = length s ⟹ S,f ⊢ (ms,s) =[]⇒* (ms,s)"

| tom_Cons:
  "⟦S,f ⊢ (ms,s) =as⇒ (ms',s'); S,f ⊢ (ms',s') =as'⇒* (ms'',s'')⟧
  ⟹ S,f ⊢ (ms,s) =(last as)#as'⇒* (ms'',s'')"


lemma tom_split_snoc:
  assumes "S,f ⊢ (ms,s) =as⇒* (ms',s')" and "as ≠ []"
  obtains asx asx' ms'' s'' where "as = asx@[last asx']" 
  and "S,f ⊢ (ms,s) =asx⇒* (ms'',s'')" and "S,f ⊢ (ms'',s'') =asx'⇒ (ms',s')"
proof(atomize_elim)
  from assms show "∃asx asx' ms'' s''. as = asx @ [last asx'] ∧
    S,f ⊢ (ms,s) =asx⇒* (ms'',s'') ∧ S,f ⊢ (ms'',s'') =asx'⇒ (ms',s')"
  proof(induct rule:trans_observable_moves.induct)
    case (tom_Cons S f ms s as ms' s' as' ms'' s'')
    note IH = ‹as' ≠ [] ⟹ ∃asx asx' msx sx. as' = asx @ [last asx'] ∧
      S,f ⊢ (ms',s') =asx⇒* (msx,sx) ∧ S,f ⊢ (msx,sx) =asx'⇒ (ms'',s'')›
    show ?case
    proof(cases "as' = []")
      case True
      with ‹S,f ⊢ (ms',s') =as'⇒* (ms'',s'')› have [simp]:"ms'' = ms'" "s'' = s'"
        by(auto elim:trans_observable_moves.cases)
      from ‹S,f ⊢ (ms,s) =as⇒ (ms',s')› have "length ms = length s"
        by(rule observable_moves_equal_length)
      hence "S,f ⊢ (ms,s) =[]⇒* (ms,s)" by(rule tom_Nil)
      with ‹S,f ⊢ (ms,s) =as⇒ (ms',s')› True show ?thesis by fastforce
    next
      case False
      from IH[OF this] obtain xs xs' msx sx where "as' = xs @ [last xs']"
        and "S,f ⊢ (ms',s') =xs⇒* (msx,sx)" 
        and "S,f ⊢ (msx,sx) =xs'⇒ (ms'',s'')" by blast
      from ‹S,f ⊢ (ms,s) =as⇒ (ms',s')› ‹S,f ⊢ (ms',s') =xs⇒* (msx,sx)›
      have "S,f ⊢ (ms,s) =(last as)#xs⇒* (msx,sx)"
        by(rule trans_observable_moves.tom_Cons)
      with ‹S,f ⊢ (msx,sx) =xs'⇒ (ms'',s'')› ‹as' = xs @ [last xs']›
      show ?thesis by fastforce
    qed
  qed simp
qed


lemma tom_preserves_stacks:
  assumes "S,f ⊢ (m#ms,s) =as⇒* (m'#ms',s')" and "valid_node m" 
  and "valid_call_list cs m" and "∀i < length rs. rs!i ∈ get_return_edges (cs!i)" 
  and "valid_return_list rs m" and "length rs = length cs" and "ms = targetnodes rs"
  obtains cs' rs' where "valid_node m'" and "valid_call_list cs' m'"
  and "∀i < length rs'. rs'!i ∈ get_return_edges (cs'!i)"
  and "valid_return_list rs' m'" and "length rs' = length cs'" 
  and "ms' = targetnodes rs'"
proof(atomize_elim)
  from assms show "∃cs' rs'. valid_node m' ∧ valid_call_list cs' m' ∧
    (∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)) ∧ valid_return_list rs' m' ∧
    length rs' = length cs' ∧ ms' = targetnodes rs'"
  proof(induct S f "m#ms" s as "m'#ms'" s' arbitrary:m ms cs rs
      rule:trans_observable_moves.induct)
    case (tom_Nil sx n⇩c f)
    thus ?case
      apply(rule_tac x="cs" in exI)
      apply(rule_tac x="rs" in exI)
      by clarsimp
  next
    case (tom_Cons S f sx as msx' sx' as' sx'')
    note IH = ‹⋀m ms cs rs. ⟦msx' = m # ms; valid_node m; valid_call_list cs m;
      ∀i<length rs. rs ! i ∈ get_return_edges (cs ! i); valid_return_list rs m;
      length rs = length cs; ms = targetnodes rs⟧
      ⟹ ∃cs' rs'. valid_node m' ∧ valid_call_list cs' m' ∧
      (∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)) ∧
      valid_return_list rs' m' ∧ length rs' = length cs' ∧
      ms' = targetnodes rs'›
    from ‹S,f ⊢ (m # ms,sx) =as⇒ (msx',sx')›
    obtain m'' ms'' where "msx' = m''#ms''"
      apply(cases msx') apply(auto elim!:observable_moves.cases observable_move.cases)
      by(case_tac "msaa") auto
    with ‹S,f ⊢ (m # ms,sx) =as⇒ (msx',sx')› ‹valid_node m›
      ‹valid_call_list cs m› ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)›
      ‹valid_return_list rs m› ‹length rs = length cs› ‹ms = targetnodes rs›
    obtain cs'' rs'' where "valid_node m''" and "valid_call_list cs'' m''"
      and "∀i < length rs''. rs''!i ∈ get_return_edges (cs''!i)"
      and "valid_return_list rs'' m''" and "length rs'' = length cs''" 
      and "ms'' = targetnodes rs''"
      by(auto elim!:observable_moves_preserves_stack)
    from IH[OF ‹msx' = m''#ms''› this(1-6)]
    show ?case by fastforce
  qed
qed




lemma vpa_trans_observable_moves:
  assumes "valid_path_aux cs as" and "m -as→* m'" and "preds (kinds as) s" 
  and "transfers (kinds as) s = s'" and "valid_call_list cs m"
  and "∀i < length rs. rs!i ∈ get_return_edges (cs!i)"
  and "valid_return_list rs m" 
  and "length rs = length cs" and "length s = Suc (length cs)" 
  obtains ms ms'' s'' ms' as' as''
  where "S,kind ⊢ (m#ms,s) =slice_edges S cs as⇒* (ms'',s'')"
  and "S,kind ⊢ (ms'',s'') =as'⇒⇩τ (m'#ms',s')" 
  and "ms = targetnodes rs" and "length ms = length cs"
  and "∀i<length cs. call_of_return_node (ms!i) (sourcenode (cs!i))"
  and "slice_edges S cs as = slice_edges S cs as''" 
  and "m -as''@as'→* m'" and "valid_path_aux cs (as''@as')"
proof(atomize_elim)
  from assms show "∃ms ms'' s'' as' ms' as''.
    S,kind ⊢ (m # ms,s) =slice_edges S cs as⇒* (ms'',s'') ∧
    S,kind ⊢ (ms'',s'') =as'⇒⇩τ (m' # ms',s') ∧ 
    ms = targetnodes rs ∧ length ms = length cs ∧
    (∀i<length cs. call_of_return_node (ms ! i) (sourcenode (cs ! i))) ∧
    slice_edges S cs as = slice_edges S cs as'' ∧
    m -as'' @ as'→* m' ∧ valid_path_aux cs (as'' @ as')"
  proof(induct arbitrary:m s rs rule:vpa_induct)
    case (vpa_empty cs)
    from ‹m -[]→* m'› have [simp]:"m' = m" by fastforce
    from ‹transfers (kinds []) s = s'› ‹length s = Suc (length cs)› 
    have [simp]:"s' = s" by(cases cs)(auto simp:kinds_def)
    from ‹valid_call_list cs m› ‹valid_return_list rs m›
      ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)› ‹length rs = length cs›
    have "∀i<length cs. call_of_return_node (targetnodes rs!i) (sourcenode (cs!i))"
      by(rule get_return_edges_call_of_return_nodes)
    with ‹length s = Suc (length cs)› ‹m -[]→* m'› ‹length rs = length cs› show ?case
      apply(rule_tac x="targetnodes rs" in exI)
      apply(rule_tac x="m#targetnodes rs" in exI)
      apply(rule_tac x="s" in exI)
      apply(rule_tac x="[]" in exI)
      apply(rule_tac x="targetnodes rs" in exI)
      apply(rule_tac x="[]" in exI)
      by(fastforce intro:tom_Nil silent_moves_Nil simp:targetnodes_def)
  next
    case (vpa_intra cs a as)
    note IH = ‹⋀m s rs. ⟦m -as→* m'; preds (kinds as) s; transfers (kinds as) s = s';
      valid_call_list cs m; ∀i<length rs. rs ! i ∈ get_return_edges (cs ! i);
      valid_return_list rs m; length rs = length cs; length s = Suc (length cs)⟧
      ⟹ ∃ms ms'' s'' as' ms' as''.
      S,kind ⊢ (m # ms,s) =slice_edges S cs as⇒* (ms'',s'') ∧
      S,kind ⊢ (ms'',s'') =as'⇒⇩τ (m' # ms',s') ∧ ms = targetnodes rs ∧
      length ms = length cs ∧
      (∀i<length cs. call_of_return_node (ms ! i) (sourcenode (cs ! i))) ∧
      slice_edges S cs as = slice_edges S cs as'' ∧
      m -as'' @ as'→* m' ∧ valid_path_aux cs (as'' @ as')›
    from ‹m -a # as→* m'› have "m = sourcenode a" and "valid_edge a"
      and "targetnode a -as→* m'" by(auto elim:path_split_Cons)
    from ‹preds (kinds (a # as)) s› have "pred (kind a) s"
      and "preds (kinds as) (transfer (kind a) s)" by(auto simp:kinds_def)
    from ‹transfers (kinds (a # as)) s = s'›
    have "transfers (kinds as) (transfer (kind a) s) = s'" by(fastforce simp:kinds_def)
    from ‹valid_edge a› ‹intra_kind (kind a)›
    have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
    from ‹valid_call_list cs m› ‹m = sourcenode a›
      ‹get_proc (sourcenode a) = get_proc (targetnode a)›
    have "valid_call_list cs (targetnode a)"
      apply(clarsimp simp:valid_call_list_def)
      apply(erule_tac x="cs'" in allE)
      apply(erule_tac x="c" in allE)
      by(auto split:list.split)
    from ‹intra_kind (kind a)› ‹length s = Suc (length cs)›
    have "length (transfer (kind a) s) = Suc (length cs)"
      by(cases s)(auto simp:intra_kind_def)
   from ‹valid_return_list rs m› ‹m = sourcenode a› 
     ‹get_proc (sourcenode a) = get_proc (targetnode a)›
    have "valid_return_list rs (targetnode a)"
      apply(clarsimp simp:valid_return_list_def)
      apply(erule_tac x="cs'" in allE) apply clarsimp
      by(case_tac cs') auto
    from IH[OF ‹targetnode a -as→* m'› ‹preds (kinds as) (transfer (kind a) s)›
      ‹transfers (kinds as) (transfer (kind a) s) = s'› 
      ‹valid_call_list cs (targetnode a)› 
      ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)› this ‹length rs = length cs›
      ‹length (transfer (kind a) s) = Suc (length cs)›]
    obtain ms ms'' s'' as' ms' as'' where "length ms = length cs"
      and "S,kind ⊢ (targetnode a # ms,transfer (kind a) s) =slice_edges S cs as⇒*
                       (ms'',s'')" 
      and paths:"S,kind ⊢ (ms'',s'') =as'⇒⇩τ (m' # ms',s')"
      "ms = targetnodes rs"
      "∀i<length cs. call_of_return_node (ms ! i) (sourcenode (cs ! i))"
      "slice_edges S cs as = slice_edges S cs as''"
      "targetnode a -as'' @ as'→* m'" "valid_path_aux cs (as'' @ as')"
      by blast
    from ‹∀i<length cs. call_of_return_node (ms ! i) (sourcenode (cs ! i))›
      ‹length ms = length cs›
    have "∀mx ∈ set ms. return_node mx"
      by(auto simp:call_of_return_node_def in_set_conv_nth)
    show ?case
    proof(cases "(∀m ∈ set ms. ∃m'. call_of_return_node m m' ∧ 
        m' ∈ ⌊HRB_slice S⌋⇘CFG⇙) ∧ m ∈ ⌊HRB_slice S⌋⇘CFG⇙")
      case True
      with ‹m = sourcenode a› ‹length ms = length cs› ‹intra_kind (kind a)›
        ‹∀i<length cs. call_of_return_node (ms ! i) (sourcenode (cs ! i))›
      have "slice_edge S cs a"
        by(fastforce simp:slice_edge_def in_set_conv_nth intra_kind_def)
      with ‹intra_kind (kind a)›
      have "slice_edges S cs (a#as) = a#slice_edges S cs as"
        by(fastforce simp:intra_kind_def)
      from True ‹pred (kind a) s› ‹valid_edge a› ‹intra_kind (kind a)›
        ‹∀mx ∈ set ms. return_node mx› ‹length ms = length cs› ‹m = sourcenode a›
        ‹length s = Suc (length cs)› ‹length (transfer (kind a) s) = Suc (length cs)›
      have "S,kind ⊢ (sourcenode a#ms,s) -a→ (targetnode a#ms,transfer (kind a) s)"
        by(fastforce intro!:observable_move_intra)
      with ‹length ms = length cs› ‹length s = Suc (length cs)›
      have "S,kind ⊢ (sourcenode a#ms,s) =[]@[a]⇒ 
                      (targetnode a#ms,transfer (kind a) s)"
        by(fastforce intro:observable_moves_snoc silent_moves_Nil)
      with ‹S,kind ⊢ (targetnode a # ms,transfer (kind a) s) =slice_edges S cs as⇒*
        (ms'',s'')›
      have "S,kind ⊢ (sourcenode a#ms,s) =last [a]#slice_edges S cs as⇒* (ms'',s'')"
        by(fastforce intro:tom_Cons)
      with ‹slice_edges S cs (a#as) = a#slice_edges S cs as›
      have "S,kind ⊢ (sourcenode a#ms,s) =slice_edges S cs (a#as)⇒* (ms'',s'')"
        by simp
      moreover
      from ‹slice_edges S cs as = slice_edges S cs as''› ‹slice_edge S cs a›
        ‹intra_kind (kind a)›
      have "slice_edges S cs (a#as) = slice_edges S cs (a#as'')"
        by(fastforce simp:intra_kind_def)
      ultimately show ?thesis 
        using paths ‹m = sourcenode a› ‹valid_edge a› ‹intra_kind (kind a)›
        ‹length ms = length cs› ‹slice_edges S cs (a#as) = a#slice_edges S cs as›
        apply(rule_tac x="ms" in exI)
        apply(rule_tac x="ms''" in exI)
        apply(rule_tac x="s''" in exI)
        apply(rule_tac x="as'" in exI)
        apply(rule_tac x="ms'" in exI)
        apply(rule_tac x="a#as''" in exI)
        by(auto intro:Cons_path simp:intra_kind_def)
    next
      case False
      with ‹∀mx ∈ set ms. return_node mx›
      have disj:"(∃m ∈ set ms. ∃m'. call_of_return_node m m' ∧ 
        m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨ m ∉ ⌊HRB_slice S⌋⇘CFG⇙"
        by(fastforce dest:return_node_call_of_return_node)
      with ‹m = sourcenode a› ‹length ms = length cs› ‹intra_kind (kind a)›
        ‹∀i<length cs. call_of_return_node (ms ! i) (sourcenode (cs ! i))›
      have "¬ slice_edge S cs a" 
        by(fastforce simp:slice_edge_def in_set_conv_nth intra_kind_def)
      with ‹intra_kind (kind a)›
      have "slice_edges S cs (a#as) = slice_edges S cs as"
        by(fastforce simp:intra_kind_def)
      from disj ‹pred (kind a) s› ‹valid_edge a› ‹intra_kind (kind a)›
        ‹∀mx ∈ set ms. return_node mx› ‹length ms = length cs› ‹m = sourcenode a›
        ‹length s = Suc (length cs)› ‹length (transfer (kind a) s) = Suc (length cs)›
      have "S,kind ⊢ (sourcenode a#ms,s) -a→⇩τ (targetnode a#ms,transfer (kind a) s)"
        by(fastforce intro!:silent_move_intra)
      from ‹S,kind ⊢ (targetnode a # ms,transfer (kind a) s) =slice_edges S cs as⇒*
                      (ms'',s'')›
      show ?thesis
      proof(rule trans_observable_moves.cases)
        fix msx sx n⇩c' f
        assume "targetnode a # ms = msx"
          and "transfer (kind a) s = sx" and "slice_edges S cs as = []"
          and [simp]:"ms'' = msx" "s'' = sx" and "length msx = length sx"
        from ‹slice_edges S cs (a#as) = slice_edges S cs as› 
          ‹slice_edges S cs as = []›
        have "slice_edges S cs (a#as) = []" by simp 
        with ‹length ms = length cs› ‹length s = Suc (length cs)›
        have "S,kind ⊢ (sourcenode a#ms,s) =slice_edges S cs (a#as)⇒*
                        (sourcenode a#ms,s)"
          by(fastforce intro:tom_Nil)
        moreover
        from ‹S,kind ⊢ (ms'',s'') =as'⇒⇩τ (m'#ms',s')› ‹targetnode a # ms = msx›
          ‹transfer (kind a) s = sx› ‹ms'' = msx› ‹s'' = sx›
          ‹S,kind ⊢ (sourcenode a#ms,s) -a→⇩τ (targetnode a#ms,transfer (kind a) s)›
        have "S,kind ⊢ (sourcenode a#ms,s) =a#as'⇒⇩τ (m'#ms',s')"
          by(fastforce intro:silent_moves_Cons)
        from this ‹valid_edge a› ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)›
          ‹ms = targetnodes rs› ‹valid_return_list rs m› ‹length rs = length cs›
          ‹length s = Suc (length cs)› ‹m = sourcenode a›
        have "sourcenode a -a#as'→* m'" and "valid_path_aux cs (a#as')"
          by -(rule silent_moves_vpa_path,(fastforce simp:targetnodes_def)+)+
        ultimately show ?thesis using ‹m = sourcenode a› ‹length ms = length cs›
          ‹∀i<length cs. call_of_return_node (ms ! i) (sourcenode (cs ! i))›
          ‹slice_edges S cs (a#as) = []› ‹intra_kind (kind a)›
          ‹S,kind ⊢ (sourcenode a#ms,s) =a#as'⇒⇩τ (m'#ms',s')›
          ‹ms = targetnodes rs›
          apply(rule_tac x="ms" in exI)
          apply(rule_tac x="sourcenode a#ms" in exI)
          apply(rule_tac x="s" in exI)
          apply(rule_tac x="a#as'" in exI)
          apply(rule_tac x="ms'" in exI)
          apply(rule_tac x="[]" in exI)
          by(auto simp:intra_kind_def)
      next
        fix S' f msx sx asx msx' sx' asx' msx'' sx''
        assume [simp]:"S = S'" and "kind = f" and "targetnode a # ms = msx"
          and "transfer (kind a) s = sx" and "slice_edges S cs as = last asx # asx'"
          and "ms'' = msx''" and "s'' = sx''" 
          and "S',f ⊢ (msx,sx) =asx⇒ (msx',sx')"
          and "S',f ⊢ (msx',sx') =asx'⇒* (msx'',sx'')"
        from ‹kind = f› have [simp]:"f = kind" by simp
        from ‹S,kind ⊢ (sourcenode a#ms,s) -a→⇩τ 
          (targetnode a#ms,transfer (kind a) s)› ‹S',f ⊢ (msx,sx) =asx⇒ (msx',sx')›
          ‹transfer (kind a) s = sx› ‹targetnode a # ms = msx›
        have "S,kind ⊢ (sourcenode a#ms,s) =a#asx⇒ (msx',sx')"
          by(fastforce intro:silent_move_observable_moves)
        with ‹S',f ⊢ (msx',sx') =asx'⇒* (msx'',sx'')› ‹ms'' = msx''› ‹s'' = sx''›
        have "S,kind ⊢ (sourcenode a#ms,s) =last (a#asx)#asx'⇒* (ms'',s'')"
          by(fastforce intro:trans_observable_moves.tom_Cons)
        moreover
        from ‹S',f ⊢ (msx,sx) =asx⇒ (msx',sx')› have "asx ≠ []"
          by(fastforce elim:observable_moves.cases)
        with ‹slice_edges S cs (a#as) = slice_edges S cs as›
          ‹slice_edges S cs as = last asx # asx'›
        have "slice_edges S cs (a#as) = last (a#asx)#asx'" by simp
        moreover
        from ‹¬ slice_edge S cs a› ‹slice_edges S cs as = slice_edges S cs as''›
          ‹intra_kind (kind a)›
        have "slice_edges S cs (a # as) = slice_edges S cs (a # as'')"
          by(fastforce simp:intra_kind_def)
        ultimately show ?thesis using paths ‹m = sourcenode a› ‹intra_kind (kind a)›
          ‹length ms = length cs› ‹ms = targetnodes rs› ‹valid_edge a›
          apply(rule_tac x="ms" in exI)
          apply(rule_tac x="ms''" in exI)
          apply(rule_tac x="s''" in exI)
          apply(rule_tac x="as'" in exI)
          apply(rule_tac x="ms'" in exI)
          apply(rule_tac x="a#as''" in exI)
          by(auto intro:Cons_path simp:intra_kind_def)
      qed
    qed
  next
    case (vpa_Call cs a as Q r p fs)
    note IH = ‹⋀m s rs. ⟦m -as→* m'; preds (kinds as) s; transfers (kinds as) s = s';
      valid_call_list (a # cs) m;
      ∀i<length rs. rs ! i ∈ get_return_edges ((a # cs) ! i);
      valid_return_list rs m; length rs = length (a # cs);
      length s = Suc (length (a # cs))⟧
      ⟹ ∃ms ms'' s'' as' ms' as''.
      S,kind ⊢ (m # ms,s) =slice_edges S (a # cs) as⇒* (ms'',s'') ∧
      S,kind ⊢ (ms'',s'') =as'⇒⇩τ (m' # ms',s') ∧ ms = targetnodes rs ∧
      length ms = length (a # cs) ∧
      (∀i<length (a # cs). call_of_return_node (ms ! i) (sourcenode ((a # cs) ! i))) ∧
      slice_edges S (a # cs) as = slice_edges S (a # cs) as'' ∧
      m -as'' @ as'→* m' ∧ valid_path_aux (a # cs) (as'' @ as')›
    from ‹m -a # as→* m'› have "m = sourcenode a" and "valid_edge a"
      and "targetnode a -as→* m'" by(auto elim:path_split_Cons)
    from ‹preds (kinds (a # as)) s› have "pred (kind a) s"
      and "preds (kinds as) (transfer (kind a) s)" by(auto simp:kinds_def)
    from ‹transfers (kinds (a # as)) s = s'›
    have "transfers (kinds as) (transfer (kind a) s) = s'" by(fastforce simp:kinds_def)
    from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc (targetnode a) = p"
      by(rule get_proc_call)
    with ‹valid_call_list cs m› ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹m = sourcenode a›
    have "valid_call_list (a # cs) (targetnode a)"
      apply(clarsimp simp:valid_call_list_def)
      apply(case_tac cs') apply auto
      apply(erule_tac x="list" in allE)
      by(case_tac list)(auto simp:sourcenodes_def)
    from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› obtain a' where "a' ∈ get_return_edges a"
      by(fastforce dest:get_return_edge_call)
    with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› obtain Q' f' where "kind a' = Q'↩⇘p⇙f'"
      by(fastforce dest!:call_return_edges)
    from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'" 
      by(rule get_return_edges_valid)
    from ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'› have "get_proc (sourcenode a') = p"
      by(rule get_proc_return)
    from ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)› ‹a' ∈ get_return_edges a›
    have "∀i<length (a'#rs). (a'#rs) ! i ∈ get_return_edges ((a#cs) ! i)"
      by auto(case_tac i,auto)
    from ‹valid_edge a› ‹a' ∈ get_return_edges a›
    have "get_proc (sourcenode a) = get_proc (targetnode a')" 
      by(rule get_proc_get_return_edge)
    with ‹valid_return_list rs m› ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'›
      ‹get_proc (sourcenode a') = p› ‹get_proc (targetnode a) = p› ‹m = sourcenode a›
    have "valid_return_list (a'#rs) (targetnode a)"
      apply(clarsimp simp:valid_return_list_def)
      apply(case_tac cs') apply auto
      apply(erule_tac x="list" in allE)
      by(case_tac list)(auto simp:targetnodes_def)
    from ‹length rs = length cs› have "length (a'#rs) = length (a#cs)" by simp
    from ‹length s = Suc (length cs)› ‹kind a = Q:r↪⇘p⇙fs›
    have "length (transfer (kind a) s) = Suc (length (a#cs))"
      by(cases s) auto
    from IH[OF ‹targetnode a -as→* m'› ‹preds (kinds as) (transfer (kind a) s)›
      ‹transfers (kinds as) (transfer (kind a) s) = s'› 
      ‹valid_call_list (a # cs) (targetnode a)› 
      ‹∀i<length (a'#rs). (a'#rs) ! i ∈ get_return_edges ((a#cs) ! i)›
      ‹valid_return_list (a'#rs) (targetnode a)› ‹length (a'#rs) = length (a#cs)›
      ‹length (transfer (kind a) s) = Suc (length (a#cs))›]
    obtain ms ms'' s'' as' ms' as'' where "length ms = length (a#cs)"
      and "S,kind ⊢ (targetnode a # ms,transfer (kind a) s) 
                     =slice_edges S (a#cs) as⇒* (ms'',s'')" 
      and paths:"S,kind ⊢ (ms'',s'') =as'⇒⇩τ (m' # ms',s')"
      "ms = targetnodes (a'#rs)"
      "∀i<length (a#cs). call_of_return_node (ms ! i) (sourcenode ((a#cs) ! i))"
      "slice_edges S (a#cs) as = slice_edges S (a#cs) as''"
      "targetnode a -as'' @ as'→* m'" "valid_path_aux (a#cs) (as'' @ as')"
      by blast
    from ‹ms = targetnodes (a'#rs)› obtain x xs where [simp]:"ms = x#xs"
      and "x = targetnode a'" and "xs = targetnodes rs"
      by(cases ms)(auto simp:targetnodes_def)
    from ‹∀i<length (a#cs). call_of_return_node (ms ! i) (sourcenode ((a#cs) ! i))›
      ‹length ms = length (a#cs)›
    have "∀mx ∈ set xs. return_node mx"
      apply(auto simp:in_set_conv_nth) apply(case_tac i)
      apply(erule_tac x="Suc 0" in allE)
      by(auto simp:call_of_return_node_def)
    show ?case
    proof(cases "(∀m ∈ set xs. ∃m'. call_of_return_node m m' ∧ 
        m' ∈ ⌊HRB_slice S⌋⇘CFG⇙) ∧ sourcenode a ∈ ⌊HRB_slice S⌋⇘CFG⇙")
      case True
      with ‹∀i<length (a#cs). call_of_return_node (ms ! i) (sourcenode ((a#cs) ! i))›
        ‹length ms = length (a#cs)› ‹kind a = Q:r↪⇘p⇙fs›
      have "slice_edge S cs a"
        apply(auto simp:slice_edge_def in_set_conv_nth)
        by(erule_tac x="Suc i" in allE) auto
      with ‹kind a = Q:r↪⇘p⇙fs›
      have "slice_edges S cs (a#as) = a#slice_edges S (a#cs) as" by simp
      from True ‹pred (kind a) s› ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs›
        ‹valid_edge a'› ‹a' ∈ get_return_edges a›
        ‹∀mx ∈ set xs. return_node mx› ‹length ms = length (a#cs)› ‹m = sourcenode a›
        ‹length s = Suc (length cs)› 
        ‹length (transfer (kind a) s) = Suc (length (a#cs))›
      have "S,kind ⊢ (sourcenode a#xs,s) -a→ 
        (targetnode a#targetnode a'#xs,transfer (kind a) s)"
        by -(rule_tac a'="a'" in observable_move_call,fastforce+)
      with ‹length ms = length (a#cs)› ‹length s = Suc (length cs)›
      have "S,kind ⊢ (sourcenode a#xs,s) =[]@[a]⇒ 
        (targetnode a#targetnode a'#xs,transfer (kind a) s)"
        by(fastforce intro:observable_moves_snoc silent_moves_Nil)
      with ‹S,kind ⊢ (targetnode a # ms,transfer (kind a) s) 
        =slice_edges S (a#cs) as⇒* (ms'',s'')› ‹x = targetnode a'›
      have "S,kind ⊢ (sourcenode a#xs,s) =last [a]#slice_edges S (a#cs) as⇒* 
        (ms'',s'')"
        by -(rule tom_Cons,auto)
      with ‹slice_edges S cs (a#as) = a#slice_edges S (a#cs) as›
      have "S,kind ⊢ (sourcenode a#xs,s) =slice_edges S cs (a#as)⇒* (ms'',s'')"
        by simp
      moreover
      from ‹slice_edges S (a#cs) as = slice_edges S (a#cs) as''›
        ‹slice_edge S cs a› ‹kind a = Q:r↪⇘p⇙fs›
      have "slice_edges S cs (a#as) = slice_edges S cs (a#as'')" by simp
      ultimately show ?thesis
        using paths ‹m = sourcenode a› ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs›
          ‹length ms = length (a#cs)› ‹xs = targetnodes rs›
          ‹slice_edges S cs (a#as) = a#slice_edges S (a#cs) as›
        apply(rule_tac x="xs" in exI)
        apply(rule_tac x="ms''" in exI)
        apply(rule_tac x="s''" in exI)
        apply(rule_tac x="as'" in exI)
        apply(rule_tac x="ms'" in exI)
        apply(rule_tac x="a#as''" in exI)
        by(auto intro:Cons_path simp:targetnodes_def)
    next
      case False
      with ‹∀mx ∈ set xs. return_node mx›
      have disj:"(∃m ∈ set xs. ∃m'. call_of_return_node m m' ∧ 
        m' ∉ ⌊HRB_slice S⌋⇘CFG⇙) ∨ sourcenode a ∉ ⌊HRB_slice S⌋⇘CFG⇙"
        by(fastforce dest:return_node_call_of_return_node)
      with ‹∀i<length (a#cs). call_of_return_node (ms ! i) (sourcenode ((a#cs) ! i))›
        ‹length ms = length (a#cs)› ‹kind a = Q:r↪⇘p⇙fs›
      have "¬ slice_edge S cs a"
        apply(auto simp:slice_edge_def in_set_conv_nth)
        by(erule_tac x="Suc i" in allE) auto
      with ‹kind a = Q:r↪⇘p⇙fs›
      have "slice_edges S cs (a#as) = slice_edges S (a#cs) as" by simp
      from disj ‹pred (kind a) s› ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs›
        ‹valid_edge a'› ‹a' ∈ get_return_edges a›
        ‹∀mx ∈ set xs. return_node mx› ‹length ms = length (a#cs)› ‹m = sourcenode a›
        ‹length s = Suc (length cs)› 
        ‹length (transfer (kind a) s) = Suc (length (a#cs))›
      have "S,kind ⊢ (sourcenode a#xs,s) -a→⇩τ
        (targetnode a#targetnode a'#xs,transfer (kind a) s)"
        by -(rule_tac a'="a'" in silent_move_call,fastforce+)
      from ‹S,kind ⊢ (targetnode a # ms,transfer (kind a) s) 
        =slice_edges S (a#cs) as⇒* (ms'',s'')›
      show ?thesis
      proof(rule trans_observable_moves.cases)
        fix msx sx S' f
        assume "targetnode a # ms = msx"
          and "transfer (kind a) s = sx" and "slice_edges S (a#cs) as = []"
          and [simp]:"ms'' = msx" "s'' = sx" and "length msx = length sx"
        from ‹slice_edges S cs (a#as) = slice_edges S (a#cs) as› 
          ‹slice_edges S (a#cs) as = []›
        have "slice_edges S cs (a#as) = []" by simp
        with ‹length ms = length (a#cs)› ‹length s = Suc (length cs)›
        have "S,kind ⊢ (sourcenode a#xs,s) =slice_edges S cs (a#as)⇒*
                        (sourcenode a#xs,s)"
          by(fastforce intro:tom_Nil)
        moreover
        from ‹S,kind ⊢ (ms'',s'') =as'⇒⇩τ (m'#ms',s')› ‹targetnode a # ms = msx›
          ‹transfer (kind a) s = sx› ‹ms'' = msx› ‹s'' = sx› ‹x = targetnode a'›
          ‹S,kind ⊢ (sourcenode a#xs,s) -a→⇩τ 
          (targetnode a#targetnode a'#xs,transfer (kind a) s)›
        have "S,kind ⊢ (sourcenode a#xs,s) =a#as'⇒⇩τ (m'#ms',s')"
          by(auto intro:silent_moves_Cons)
        from this ‹valid_edge a› 
          ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)›
          ‹xs = targetnodes rs› ‹valid_return_list rs m› ‹length rs = length cs›
          ‹length s = Suc (length cs)› ‹m = sourcenode a›
        have "sourcenode a -a#as'→* m'" and "valid_path_aux cs (a#as')"
          by -(rule silent_moves_vpa_path,(fastforce simp:targetnodes_def)+)+
        ultimately show ?thesis using ‹m = sourcenode a› ‹length ms = length (a#cs)›
          ‹∀i<length (a#cs). call_of_return_node (ms ! i) (sourcenode ((a#cs) ! i))›
          ‹slice_edges S cs (a#as) = []› ‹kind a = Q:r↪⇘p⇙fs›
          ‹S,kind ⊢ (sourcenode a#xs,s) =a#as'⇒⇩τ (m'#ms',s')›
          ‹xs = targetnodes rs›
          apply(rule_tac x="xs" in exI)
          apply(rule_tac x="sourcenode a#xs" in exI)
          apply(rule_tac x="s" in exI)
          apply(rule_tac x="a#as'" in exI)
          apply(rule_tac x="ms'" in exI)
          apply(rule_tac x="[]" in exI)
          by auto
      next
        fix S' f msx sx asx msx' sx' asx' msx'' sx''
        assume [simp]:"S = S'" and "kind = f" and "targetnode a # ms = msx"
          and "transfer (kind a) s = sx" 
          and "slice_edges S (a#cs) as = last asx # asx'"
          and "ms'' = msx''" and "s'' = sx''" 
          and "S',f ⊢ (msx,sx) =asx⇒ (msx',sx')"
          and "S',f ⊢ (msx',sx') =asx'⇒* (msx'',sx'')"
        from ‹kind = f› have [simp]:"f = kind" by simp
        from ‹S,kind ⊢ (sourcenode a#xs,s) -a→⇩τ 
          (targetnode a#targetnode a'#xs,transfer (kind a) s)›
          ‹S',f ⊢ (msx,sx) =asx⇒ (msx',sx')› ‹x = targetnode a'›
          ‹transfer (kind a) s = sx› ‹targetnode a # ms = msx›
        have "S,kind ⊢ (sourcenode a#xs,s) =a#asx⇒ (msx',sx')"
          by(auto intro:silent_move_observable_moves)
        with ‹S',f ⊢ (msx',sx') =asx'⇒* (msx'',sx'')› ‹ms'' = msx''› ‹s'' = sx''›
        have "S,kind ⊢ (sourcenode a#xs,s) =last (a#asx)#asx'⇒* (ms'',s'')"
          by(fastforce intro:trans_observable_moves.tom_Cons)
        moreover
        from ‹S',f ⊢ (msx,sx) =asx⇒ (msx',sx')› have "asx ≠ []"
          by(fastforce elim:observable_moves.cases)
        with ‹slice_edges S cs (a#as) = slice_edges S (a#cs) as›
          ‹slice_edges S (a#cs) as = last asx # asx'›
        have "slice_edges S cs (a#as) = last (a#asx)#asx'" by simp
        moreover
        from ‹¬ slice_edge S cs a› ‹kind a = Q:r↪⇘p⇙fs›
          ‹slice_edges S (a#cs) as = slice_edges S (a#cs) as''›
        have "slice_edges S cs (a # as) = slice_edges S cs (a # as'')" by simp
        ultimately show ?thesis using paths ‹m = sourcenode a› ‹kind a = Q:r↪⇘p⇙fs›
          ‹length ms = length (a#cs)› ‹xs = targetnodes rs› ‹valid_edge a›
          apply(rule_tac x="xs" in exI)
          apply(rule_tac x="ms''" in exI)
          apply(rule_tac x="s''" in exI)
          apply(rule_tac x="as'" in exI)
          apply(rule_tac x="ms'" in exI)
          apply(rule_tac x="a#as''" in exI)
          by(auto intro:Cons_path simp:targetnodes_def)
      qed
    qed
  next
    case (vpa_ReturnEmpty cs a as Q p f)
    from ‹preds (kinds (a # as)) s› ‹length s = Suc (length cs)› ‹kind a = Q↩⇘p⇙f›
      ‹cs = []›
    have False by(cases s)(auto simp:kinds_def)
    thus ?case by simp
  next
    case (vpa_ReturnCons cs a as Q p f c' cs')
    note IH = ‹⋀m s rs. ⟦m -as→* m'; preds (kinds as) s; transfers (kinds as) s = s';
      valid_call_list cs' m; ∀i<length rs. rs ! i ∈ get_return_edges (cs' ! i);
      valid_return_list rs m; length rs = length cs'; length s = Suc (length cs')⟧
      ⟹ ∃ms ms'' s'' as' ms' as''.
      S,kind ⊢ (m # ms,s) =slice_edges S cs' as⇒* (ms'',s'') ∧
      S,kind ⊢ (ms'',s'') =as'⇒⇩τ (m' # ms',s') ∧ ms = targetnodes rs ∧
      length ms = length cs' ∧
      (∀i<length cs'. call_of_return_node (ms ! i) (sourcenode (cs' ! i))) ∧
      slice_edges S cs' as = slice_edges S cs' as'' ∧
      m -as'' @ as'→* m' ∧ valid_path_aux cs' (as'' @ as')›
    from ‹m -a # as→* m'› have "m = sourcenode a" and "valid_edge a"
      and "targetnode a -as→* m'" by(auto elim:path_split_Cons)
    from ‹preds (kinds (a # as)) s› have "pred (kind a) s"
      and "preds (kinds as) (transfer (kind a) s)" by(auto simp:kinds_def)
    from ‹transfers (kinds (a # as)) s = s'›
    have "transfers (kinds as) (transfer (kind a) s) = s'" by(fastforce simp:kinds_def)
    from ‹valid_call_list cs m› ‹cs = c' # cs'› have "valid_edge c'"
      by(fastforce simp:valid_call_list_def)
    from ‹valid_edge c'› ‹a ∈ get_return_edges c'›
    have "get_proc (sourcenode c') = get_proc (targetnode a)"
      by(rule get_proc_get_return_edge)
    from ‹valid_call_list cs m› ‹cs = c' # cs'›
      ‹get_proc (sourcenode c') = get_proc (targetnode a)›
    have "valid_call_list cs' (targetnode a)"
      apply(clarsimp simp:valid_call_list_def)
      apply(hypsubst_thin)
      apply(erule_tac x="c' # cs'" in allE)
      by(case_tac cs')(auto simp:sourcenodes_def)
    from ‹length rs = length cs› ‹cs = c' # cs'› obtain r' rs' 
      where [simp]:"rs = r'#rs'" and "length rs' = length cs'" by(cases rs) auto
    from ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)› ‹cs = c' # cs'›
    have "∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)"
      and "r' ∈ get_return_edges c'" by auto
    with ‹valid_edge c'› ‹a ∈ get_return_edges c'› have [simp]:"a = r'" 
      by -(rule get_return_edges_unique)
    with ‹valid_return_list rs m› 
    have "valid_return_list rs' (targetnode a)"
      apply(clarsimp simp:valid_return_list_def)
      apply(erule_tac x="r' # cs'" in allE)
      by(case_tac cs')(auto simp:targetnodes_def)
    from ‹length s = Suc (length cs)› ‹cs = c' # cs'› ‹kind a = Q↩⇘p⇙f›
    have "length (transfer (kind a) s) = Suc (length cs')"
      by(cases s)(auto,case_tac list,auto)
    from IH[OF ‹targetnode a -as→* m'› ‹preds (kinds as) (transfer (kind a) s)›
      ‹transfers (kinds as) (transfer (kind a) s) = s'›
      ‹valid_call_list cs' (targetnode a)› 
      ‹∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)›
      ‹valid_return_list rs' (targetnode a)› ‹length rs' = length cs'› this]
    obtain ms ms'' s'' as' ms' as'' where "length ms = length cs'"
      and "S,kind ⊢ (targetnode a # ms,transfer (kind a) s) 
                     =slice_edges S cs' as⇒* (ms'',s'')" 
      and paths:"S,kind ⊢ (ms'',s'') =as'⇒⇩τ (m' # ms',s')"
      "ms = targetnodes rs'"
      "∀i<length cs'. call_of_return_node (ms ! i) (sourcenode (cs' ! i))"
      "slice_edges S cs' as = slice_edges S cs' as''"
      "targetnode a -as'' @ as'→* m'" "valid_path_aux cs' (as'' @ as')"
      by blast
    from ‹∀i<length cs'. call_of_return_node (ms ! i) (sourcenode (cs' ! i))›
      ‹length ms = length cs'›
    have "∀mx ∈ set ms. return_node mx"
      by(auto simp:in_set_conv_nth call_of_return_node_def)
    from ‹valid_edge a› ‹valid_edge c'› ‹a ∈ get_return_edges c'›
    have "return_node (targetnode a)" by(fastforce simp:return_node_def)
    with ‹valid_edge c'› ‹valid_edge a› ‹a ∈ get_return_edges c'›
    have "call_of_return_node (targetnode a) (sourcenode c')"
      by(simp add:call_of_return_node_def) blast
    show ?case
    proof(cases "(∀m ∈ set (targetnode a#ms). ∃m'. call_of_return_node m m' ∧ 
        m' ∈ ⌊HRB_slice S⌋⇘CFG⇙)")
      case True
      then obtain x where "call_of_return_node (targetnode a) x"
        and "x ∈ ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
      with ‹call_of_return_node (targetnode a) (sourcenode c')›
      have "sourcenode c' ∈ ⌊HRB_slice S⌋⇘CFG⇙" by fastforce
      with True ‹∀i<length cs'. call_of_return_node (ms ! i) (sourcenode (cs' ! i))›
        ‹length ms = length cs'› ‹cs = c' # cs'› ‹kind a = Q↩⇘p⇙f›
      have "slice_edge S cs a"
        apply(auto simp:slice_edge_def in_set_conv_nth) 
        by(erule_tac x="i" in allE) auto
      with ‹kind a = Q↩⇘p⇙f› ‹cs = c' # cs'›
      have "slice_edges S cs (a#as) = a#slice_edges S cs' as" by simp
      from True ‹pred (kind a) s› ‹valid_edge a› ‹kind a = Q↩⇘p⇙f›
        ‹∀mx ∈ set ms. return_node mx› ‹length ms = length cs'› 
        ‹length s = Suc (length cs)› ‹m = sourcenode a›
        ‹length (transfer (kind a) s) = Suc (length cs')›
        ‹return_node (targetnode a)› ‹cs = c' # cs'›
      have "S,kind ⊢ (sourcenode a#targetnode a#ms,s) -a→ 
        (targetnode a#ms,transfer (kind a) s)"
        by(auto intro!:observable_move_return)
      with ‹length ms = length cs'› ‹length s = Suc (length cs)› ‹cs = c' # cs'›
      have "S,kind ⊢ (sourcenode a#targetnode a#ms,s) =[]@[a]⇒
        (targetnode a#ms,transfer (kind a) s)"
        by(fastforce intro:observable_moves_snoc silent_moves_Nil)
      with ‹S,kind ⊢ (targetnode a # ms,transfer (kind a) s) 
                     =slice_edges S cs' as⇒* (ms'',s'')›
      have "S,kind ⊢ (sourcenode a#targetnode a#ms,s) 
        =last [a]#slice_edges S cs' as⇒* (ms'',s'')"
        by -(rule tom_Cons,auto)
      with ‹slice_edges S cs (a#as) = a#slice_edges S cs' as›
      have "S,kind ⊢ (sourcenode a#targetnode a#ms,s) =slice_edges S cs (a#as)⇒* 
        (ms'',s'')" by simp
      moreover
      from ‹slice_edges S cs' as = slice_edges S cs' as''›
        ‹slice_edge S cs a› ‹kind a = Q↩⇘p⇙f› ‹cs = c' # cs'›
      have "slice_edges S cs (a#as) = slice_edges S cs (a#as'')" by simp
      ultimately show ?thesis
        using paths ‹m = sourcenode a› ‹valid_edge a› ‹kind a = Q↩⇘p⇙f›
          ‹length ms = length cs'› ‹ms = targetnodes rs'› ‹cs = c' # cs'›
          ‹slice_edges S cs (a#as) = a#slice_edges S cs' as›
          ‹a ∈ get_return_edges c'› 
          ‹call_of_return_node (targetnode a) (sourcenode c')›
        apply(rule_tac x="targetnode a#ms" in exI)
        apply(rule_tac x="ms''" in exI)
        apply(rule_tac x="s''" in exI)
        apply(rule_tac x="as'" in exI)
        apply(rule_tac x="ms'" in exI)
        apply(rule_tac x="a#as''" in exI)
        apply(auto intro:Cons_path simp:targetnodes_def)
        by(case_tac i) auto
    next
      case False
      with ‹∀mx ∈ set ms. return_node mx› ‹return_node (targetnode a)›
      have "∃m ∈ set (targetnode a # ms). ∃m'. call_of_return_node m m' ∧ 
        m' ∉ ⌊HRB_slice S⌋⇘CFG⇙"
        by(fastforce dest:return_node_call_of_return_node)
      with ‹∀i<length cs'. call_of_return_node (ms ! i) (sourcenode (cs' ! i))›
        ‹length ms = length cs'› ‹cs = c' # cs'› ‹kind a = Q↩⇘p⇙f›
        ‹call_of_return_node (targetnode a) (sourcenode c')›
      have "¬ slice_edge S cs a"
        apply(auto simp:slice_edge_def in_set_conv_nth)
        by(erule_tac x="i" in allE) auto
      with ‹kind a = Q↩⇘p⇙f› ‹cs = c' # cs'›
      have "slice_edges S cs (a#as) = slice_edges S cs' as" by simp
      from ‹pred (kind a) s› ‹valid_edge a› ‹kind a = Q↩⇘p⇙f›
        ‹∀mx ∈ set ms. return_node mx› ‹length ms = length cs'› 
        ‹length s = Suc (length cs)› ‹m = sourcenode a›
        ‹length (transfer (kind a) s) = Suc (length cs')›
        ‹return_node (targetnode a)› ‹cs = c' # cs'›
        ‹∃m ∈ set (targetnode a # ms). ∃m'. call_of_return_node m m' ∧ 
        m' ∉ ⌊HRB_slice S⌋⇘CFG⇙›
      have "S,kind ⊢ (sourcenode a#targetnode a#ms,s) -a→⇩τ
        (targetnode a#ms,transfer (kind a) s)"
        by(auto intro!:silent_move_return)
      from ‹S,kind ⊢ (targetnode a # ms,transfer (kind a) s) 
                     =slice_edges S cs' as⇒* (ms'',s'')›
      show ?thesis
      proof(rule trans_observable_moves.cases)
        fix msx sx S' f'
        assume "targetnode a # ms = msx"
          and "transfer (kind a) s = sx" and "slice_edges S cs' as = []"
          and [simp]:"ms'' = msx" "s'' = sx" and "length msx = length sx"
        from ‹slice_edges S cs (a#as) = slice_edges S cs' as› 
          ‹slice_edges S cs' as = []›
        have "slice_edges S cs (a#as) = []" by simp
        with ‹length ms = length cs'› ‹length s = Suc (length cs)› ‹cs = c' # cs'›
        have "S,kind ⊢ (sourcenode a#targetnode a#ms,s) =slice_edges S cs (a#as)⇒*
                        (sourcenode a#targetnode a#ms,s)"
          by(fastforce intro:tom_Nil)
        moreover
        from ‹S,kind ⊢ (ms'',s'') =as'⇒⇩τ (m'#ms',s')› ‹targetnode a # ms = msx›
          ‹transfer (kind a) s = sx› ‹ms'' = msx› ‹s'' = sx›
          ‹S,kind ⊢ (sourcenode a#targetnode a#ms,s) -a→⇩τ 
          (targetnode a#ms,transfer (kind a) s)›
        have "S,kind ⊢ (sourcenode a#targetnode a#ms,s) =a#as'⇒⇩τ (m'#ms',s')"
          by(auto intro:silent_moves_Cons)
        from this ‹valid_edge a› 
          ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)›
          ‹valid_return_list rs m› ‹length rs = length cs›
          ‹length s = Suc (length cs)› ‹m = sourcenode a›
          ‹ms = targetnodes rs'› ‹rs = r'#rs'› ‹cs = c' # cs'›
        have "sourcenode a -a#as'→* m'" and "valid_path_aux cs (a#as')"
          by -(rule silent_moves_vpa_path,(fastforce simp:targetnodes_def)+)+
        ultimately show ?thesis using ‹m = sourcenode a› ‹length ms = length cs'›
          ‹∀i<length cs'. call_of_return_node (ms ! i) (sourcenode (cs' ! i))›
          ‹slice_edges S cs (a#as) = []› ‹kind a = Q↩⇘p⇙f›
          ‹S,kind ⊢ (sourcenode a#targetnode a#ms,s) =a#as'⇒⇩τ (m'#ms',s')›
          ‹ms = targetnodes rs'› ‹rs = r'#rs'› ‹cs = c' # cs'›
          ‹call_of_return_node (targetnode a) (sourcenode c')›
          apply(rule_tac x="targetnode a#ms" in exI)
          apply(rule_tac x="sourcenode a#targetnode a#ms" in exI)
          apply(rule_tac x="s" in exI)
          apply(rule_tac x="a#as'" in exI)
          apply(rule_tac x="ms'" in exI)
          apply(rule_tac x="[]" in exI)
          apply(auto simp:targetnodes_def)
          by(case_tac i) auto
      next
        fix S' f' msx sx asx msx' sx' asx' msx'' sx''
        assume [simp]:"S = S'" and "kind = f'" and "targetnode a # ms = msx"
          and "transfer (kind a) s = sx" 
          and "slice_edges S cs' as = last asx # asx'"
          and "ms'' = msx''" and "s'' = sx''" 
          and "S',f' ⊢ (msx,sx) =asx⇒ (msx',sx')"
          and "S',f' ⊢ (msx',sx') =asx'⇒* (msx'',sx'')"
        from ‹kind = f'› have [simp]:"f' = kind" by simp
        from ‹S,kind ⊢ (sourcenode a#targetnode a#ms,s) -a→⇩τ 
          (targetnode a#ms,transfer (kind a) s)›
          ‹S',f' ⊢ (msx,sx) =asx⇒ (msx',sx')›
          ‹transfer (kind a) s = sx› ‹targetnode a # ms = msx›
        have "S,kind ⊢ (sourcenode a#targetnode a#ms,s) =a#asx⇒ (msx',sx')"
          by(auto intro:silent_move_observable_moves)
        with ‹S',f' ⊢ (msx',sx') =asx'⇒* (msx'',sx'')› ‹ms'' = msx''› ‹s'' = sx''›
        have "S,kind ⊢ (sourcenode a#targetnode a#ms,s) =last (a#asx)#asx'⇒* 
          (ms'',s'')"
          by(fastforce intro:trans_observable_moves.tom_Cons)
        moreover
        from ‹S',f' ⊢ (msx,sx) =asx⇒ (msx',sx')› have "asx ≠ []"
          by(fastforce elim:observable_moves.cases)
        with ‹slice_edges S cs (a#as) = slice_edges S cs' as›
          ‹slice_edges S cs' as = last asx # asx'›
        have "slice_edges S cs (a#as) = last (a#asx)#asx'" by simp
        moreover
        from ‹¬ slice_edge S cs a› ‹kind a = Q↩⇘p⇙f›
          ‹slice_edges S cs' as = slice_edges S cs' as''› ‹cs = c' # cs'›
        have "slice_edges S cs (a # as) = slice_edges S cs (a # as'')" by simp
        ultimately show ?thesis using paths ‹m = sourcenode a› ‹kind a = Q↩⇘p⇙f›
          ‹length ms = length cs'› ‹ms = targetnodes rs'› ‹valid_edge a›
          ‹rs = r'#rs'› ‹cs = c' # cs'› ‹r' ∈ get_return_edges c'›
          ‹call_of_return_node (targetnode a) (sourcenode c')›
          apply(rule_tac x="targetnode a#ms" in exI)
          apply(rule_tac x="ms''" in exI)
          apply(rule_tac x="s''" in exI)
          apply(rule_tac x="as'" in exI)
          apply(rule_tac x="ms'" in exI)
          apply(rule_tac x="a#as''" in exI)
          apply(auto intro:Cons_path simp:targetnodes_def)
          by(case_tac i) auto
      qed
    qed
  qed
qed



lemma valid_path_trans_observable_moves:
  assumes "m -as→⇩√* m'" and "preds (kinds as) [cf]" 
  and "transfers (kinds as) [cf] = s'"
  obtains ms'' s'' ms' as' as'' 
  where "S,kind ⊢ ([m],[cf]) =slice_edges S [] as⇒* (ms'',s'')"
  and "S,kind ⊢ (ms'',s'') =as'⇒⇩τ (m'#ms',s')"
  and "slice_edges S [] as = slice_edges S [] as''"
  and "m -as''@as'→⇩√* m'"
proof(atomize_elim)
  from ‹m -as→⇩√* m'› have "valid_path_aux [] as" and "m -as→* m'"
    by(simp_all add:vp_def valid_path_def)
  from this ‹preds (kinds as) [cf]› ‹transfers (kinds as) [cf] = s'›
  show "∃ms'' s'' as' ms' as''. 
    S,kind ⊢ ([m],[cf]) =slice_edges S [] as⇒* (ms'',s'') ∧
    S,kind ⊢ (ms'',s'') =as'⇒⇩τ (m' # ms',s') ∧
    slice_edges S [] as = slice_edges S [] as'' ∧ m -as'' @ as'→⇩√* m'"
    by -(erule vpa_trans_observable_moves[of _ _ _ _ _ _ "[]" S],
      auto simp:valid_call_list_def valid_return_list_def vp_def valid_path_def)
qed


lemma WS_weak_sim_trans:
  assumes "((ms⇩1,s⇩1),(ms⇩2,s⇩2)) ∈ WS S"
  and "S,kind ⊢ (ms⇩1,s⇩1) =as⇒* (ms⇩1',s⇩1')" and "as ≠ []"
  shows "((ms⇩1',s⇩1'),(ms⇩1',transfers (slice_kinds S as) s⇩2)) ∈ WS S ∧ 
         S,slice_kind S ⊢ (ms⇩2,s⇩2) =as⇒* (ms⇩1',transfers (slice_kinds S as) s⇩2)"
proof -
  obtain f where "f = kind" by simp
  with ‹S,kind ⊢ (ms⇩1,s⇩1) =as⇒* (ms⇩1',s⇩1')› 
  have "S,f ⊢ (ms⇩1,s⇩1) =as⇒* (ms⇩1',s⇩1')" by simp
  from ‹S,f ⊢ (ms⇩1,s⇩1) =as⇒* (ms⇩1',s⇩1')› ‹((ms⇩1,s⇩1),(ms⇩2,s⇩2)) ∈ WS S› 
    ‹as ≠ []› ‹f = kind›
  show ?thesis
  proof(induct arbitrary:ms⇩2 s⇩2 rule:trans_observable_moves.induct)
    case tom_Nil thus ?case by simp
  next
    case (tom_Cons S f ms s as ms' s' as' ms'' s'')
    note IH = ‹⋀ms⇩2 s⇩2. ⟦((ms',s'),(ms⇩2,s⇩2)) ∈ WS S; as' ≠ []; f = kind⟧
      ⟹ ((ms'',s''),(ms'',transfers (slice_kinds S as') s⇩2)) ∈ WS S ∧
      S,slice_kind S ⊢ (ms⇩2,s⇩2) =as'⇒* (ms'',transfers (slice_kinds S as') s⇩2)›
    from ‹S,f ⊢ (ms,s) =as⇒ (ms',s')› have "s' ≠ []"
      by(fastforce elim:observable_moves.cases observable_move.cases)
    from ‹S,f ⊢ (ms,s) =as⇒ (ms',s')›
    obtain asx ax msx sx where "S,f ⊢ (ms,s) =asx⇒⇩τ (msx,sx)"
      and "S,f ⊢ (msx,sx) -ax→ (ms',s')" and "as = asx@[ax]"
      by(fastforce elim:observable_moves.cases)
    from ‹S,f ⊢ (ms,s) =asx⇒⇩τ (msx,sx)› ‹((ms,s),(ms⇩2,s⇩2)) ∈ WS S› ‹f = kind›
    have "((msx,sx),(ms⇩2,s⇩2)) ∈ WS S" by(fastforce intro:WS_silent_moves)
    from ‹((msx,sx),(ms⇩2,s⇩2)) ∈ WS S› ‹S,f ⊢ (msx,sx) -ax→ (ms',s')› ‹s' ≠ []›
      ‹f = kind›
    obtain asx' where "((ms',s'),(ms',transfer (slice_kind S ax) s⇩2)) ∈ WS S"
      and "S,slice_kind S ⊢ (ms⇩2,s⇩2) =asx'@[ax]⇒ 
      (ms',transfer (slice_kind S ax) s⇩2)"
      by(fastforce elim:WS_observable_move)
    show ?case
    proof(cases "as' = []")
      case True
      with ‹S,f ⊢ (ms',s') =as'⇒* (ms'',s'')› have "ms' = ms'' ∧ s' = s''"
        by(fastforce elim:trans_observable_moves.cases dest:observable_move_notempty)
      from ‹((ms',s'),(ms',transfer (slice_kind S ax) s⇩2)) ∈ WS S›
      have "length ms' = length (transfer (slice_kind S ax) s⇩2)"
        by(fastforce elim:WS.cases)
      with ‹S,slice_kind S ⊢ (ms⇩2,s⇩2) =asx'@[ax]⇒ 
        (ms',transfer (slice_kind S ax) s⇩2)›
      have "S,slice_kind S ⊢ (ms⇩2,s⇩2) =(last (asx'@[ax]))#[]⇒* 
        (ms',transfer (slice_kind S ax) s⇩2)"
        by(fastforce intro:trans_observable_moves.intros)
      with ‹((ms',s'),(ms',transfer (slice_kind S ax) s⇩2)) ∈ WS S› ‹as = asx@[ax]›
        ‹ms' = ms'' ∧ s' = s''› True
      show ?thesis by(fastforce simp:slice_kinds_def)
    next
      case False
      from IH[OF ‹((ms',s'),(ms',transfer (slice_kind S ax) s⇩2)) ∈ WS S› this 
        ‹f = kind›]
      have "((ms'',s''),(ms'',transfers (slice_kinds S as') 
        (transfer (slice_kind S ax) s⇩2))) ∈ WS S"
        and "S,slice_kind S ⊢ (ms',transfer (slice_kind S ax) s⇩2) =as'⇒* 
        (ms'',transfers (slice_kinds S as') (transfer (slice_kind S ax) s⇩2))" 
        by simp_all
      with ‹S,slice_kind S ⊢ (ms⇩2,s⇩2) =asx'@[ax]⇒ 
                               (ms',transfer (slice_kind S ax) s⇩2)›
      have "S,slice_kind S ⊢ (ms⇩2,s⇩2) =(last (asx'@[ax]))#as'⇒* 
        (ms'',transfers (slice_kinds S as') (transfer (slice_kind S ax) s⇩2))"
        by(fastforce intro:trans_observable_moves.tom_Cons)
      with ‹((ms'',s''),(ms'',transfers (slice_kinds S as') 
        (transfer (slice_kind S ax) s⇩2))) ∈ WS S› False ‹as = asx@[ax]›
      show ?thesis by(fastforce simp:slice_kinds_def)
    qed
  qed
qed


lemma stacks_rewrite:
  assumes "valid_call_list cs m" and "valid_return_list rs m"
  and "∀i < length rs. rs!i ∈ get_return_edges (cs!i)"
  and "length rs = length cs" and "ms = targetnodes rs"
  shows "∀i<length cs. call_of_return_node (ms!i) (sourcenode (cs!i))"
proof
  fix i show "i < length cs ⟶
    call_of_return_node (ms ! i) (sourcenode (cs ! i))"
  proof
    assume "i < length cs"
    with ‹∀i < length rs. rs!i ∈ get_return_edges (cs!i)› ‹length rs = length cs›
    have "rs!i ∈ get_return_edges (cs!i)" by fastforce
    from ‹valid_return_list rs m› have "∀r ∈ set rs. valid_edge r"
      by(rule valid_return_list_valid_edges)
    with ‹i < length cs› ‹length rs = length cs›
    have "valid_edge (rs!i)" by(simp add:all_set_conv_all_nth)
    from ‹valid_call_list cs m› have "∀c ∈ set cs. valid_edge c"
      by(rule valid_call_list_valid_edges)
    with ‹i < length cs› have "valid_edge (cs!i)" by(simp add:all_set_conv_all_nth)
    with ‹valid_edge (rs!i)› ‹rs!i ∈ get_return_edges (cs!i)› ‹ms = targetnodes rs›
      ‹i < length cs› ‹length rs = length cs›
    show "call_of_return_node (ms ! i) (sourcenode (cs ! i))"
      by(fastforce simp:call_of_return_node_def return_node_def targetnodes_def)
  qed
qed


lemma slice_tom_preds_vp:
  assumes "S,slice_kind S ⊢ (m#ms,s) =as⇒* (m'#ms',s')" and "valid_node m"
  and "valid_call_list cs m" and "∀i < length rs. rs!i ∈ get_return_edges (cs!i)"
  and "valid_return_list rs m" and "length rs = length cs" and "ms = targetnodes rs"
  and "∀mx ∈ set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
  obtains as' cs' rs' where "preds (slice_kinds S as') s" 
  and "slice_edges S cs as' = as" and "m -as'→* m'" and "valid_path_aux cs as'" 
  and "upd_cs cs as' = cs'" and "valid_node m'" and "valid_call_list cs' m'" 
  and "∀i < length rs'. rs'!i ∈ get_return_edges (cs'!i)"
  and "valid_return_list rs' m'" and "length rs' = length cs'" 
  and "ms' = targetnodes rs'" and "transfers (slice_kinds S as') s ≠ []"
  and "transfers (slice_kinds S (slice_edges S cs as')) s =
    transfers (slice_kinds S as') s"
proof(atomize_elim)
  from assms show "∃as' cs' rs'. preds (slice_kinds S as') s ∧
    slice_edges S cs as' = as ∧ m -as'→* m' ∧ valid_path_aux cs as' ∧
    upd_cs cs as' = cs' ∧ valid_node m' ∧ valid_call_list cs' m' ∧
    (∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)) ∧ valid_return_list rs' m' ∧
    length rs' = length cs' ∧ ms' = targetnodes rs' ∧ 
    transfers (slice_kinds S as') s ≠ [] ∧ 
    transfers (slice_kinds S (slice_edges S cs as')) s =
    transfers (slice_kinds S as') s"
  proof(induct S "slice_kind S" "m#ms" s as "m'#ms'" s'
    arbitrary:m ms cs rs rule:trans_observable_moves.induct)
    case (tom_Nil s n⇩c)
    from ‹length (m' # ms') = length s› have "s ≠ []" by(cases s) auto
    have "preds (slice_kinds S []) s" by(fastforce simp:slice_kinds_def)
    moreover
    have "slice_edges S cs [] = []" by simp
    moreover
    from ‹valid_node m'› have "m' -[]→* m'" by(fastforce intro:empty_path)
    moreover
    have "valid_path_aux cs []" by simp
    moreover
    have "upd_cs cs [] = cs" by simp
    ultimately show ?case using ‹valid_call_list cs m'› ‹valid_return_list rs m'› 
      ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)› ‹length rs = length cs›
      ‹ms' = targetnodes rs› ‹s ≠ []› ‹valid_node m'›
      apply(rule_tac x="[]" in exI)
      apply(rule_tac x="cs" in exI)
      apply(rule_tac x="rs" in exI)
      by(clarsimp simp:slice_kinds_def)
  next
    case (tom_Cons S s as msx' s' as' sx'')
    note IH = ‹⋀m ms cs rs. ⟦msx' = m # ms; valid_node m; valid_call_list cs m;
      ∀i<length rs. rs ! i ∈ get_return_edges (cs ! i); valid_return_list rs m;
      length rs = length cs; ms = targetnodes rs; 
      ∀mx∈set ms. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙⟧
      ⟹ ∃as'' cs' rs'. preds (slice_kinds S as'') s' ∧
      slice_edges S cs as'' = as' ∧ m -as''→* m' ∧ valid_path_aux cs as'' ∧
      upd_cs cs as'' = cs' ∧ valid_node m' ∧ valid_call_list cs' m' ∧
      (∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)) ∧
      valid_return_list rs' m' ∧ length rs' = length cs' ∧ ms' = targetnodes rs' ∧
      transfers (slice_kinds S as'') s' ≠ [] ∧ 
      transfers (slice_kinds S (slice_edges S cs as'')) s' =
      transfers (slice_kinds S as'') s'›
    note callstack = ‹∀mx∈set ms.
      ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    from ‹S,slice_kind S ⊢ (m # ms,s) =as⇒ (msx',s')›
    obtain asx ax xs s'' where "as = asx@[ax]" 
      and "S,slice_kind S ⊢ (m#ms,s) =asx⇒⇩τ (xs,s'')" 
      and "S,slice_kind S ⊢ (xs,s'') -ax→ (msx',s')"
      by(fastforce elim:observable_moves.cases)
    from ‹S,slice_kind S ⊢ (xs,s'') -ax→ (msx',s')›
    obtain xs' ms'' where [simp]:"xs = sourcenode ax#xs'" "msx' = targetnode ax#ms''"
      by (cases xs) (auto elim!:observable_move.cases, cases msx', auto)
    from ‹S,slice_kind S ⊢ (m # ms,s) =as⇒ (msx',s')› tom_Cons
    obtain cs'' rs'' where results:"valid_node (targetnode ax)"
      "valid_call_list cs'' (targetnode ax)"
      "∀i < length rs''. rs''!i ∈ get_return_edges (cs''!i)"
      "valid_return_list rs'' (targetnode ax)" "length rs'' = length cs''" 
      "ms'' = targetnodes rs''" and "upd_cs cs as = cs''"
      by(auto elim!:observable_moves_preserves_stack)
    from ‹S,slice_kind S ⊢ (m#ms,s) =asx⇒⇩τ (xs,s'')› callstack
    have "∀a ∈ set asx. intra_kind (kind a)"
      by simp(rule silent_moves_slice_intra_path)
    with ‹S,slice_kind S ⊢ (m#ms,s) =asx⇒⇩τ (xs,s'')›
    have [simp]:"xs' = ms" by(fastforce dest:silent_moves_intra_path)
    from ‹S,slice_kind S ⊢ (xs,s'') -ax→ (msx',s')›
    have "∀mx ∈ set ms''. ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
      by(fastforce dest:observable_set_stack_in_slice)
    from IH[OF ‹msx' = targetnode ax#ms''› results this]
    obtain asx' cs' rs' where "preds (slice_kinds S asx') s'" 
      and "slice_edges S cs'' asx' = as'" and "targetnode ax -asx'→* m'"
      and "valid_path_aux cs'' asx'" and "upd_cs cs'' asx' = cs'"
      and "valid_node m'" and "valid_call_list cs' m'" 
      and "∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)"
      and "valid_return_list rs' m'" and "length rs' = length cs'"
      and "ms' = targetnodes rs'" and "transfers (slice_kinds S asx') s' ≠ []"
      and trans_eq:"transfers (slice_kinds S (slice_edges S cs'' asx')) s' =
      transfers (slice_kinds S asx') s'"
      by blast
    from ‹S,slice_kind S ⊢ (m#ms,s) =asx⇒⇩τ (xs,s'')›
    have "preds (slice_kinds S asx) s" and "transfers (slice_kinds S asx) s = s''"
      by(auto intro:silent_moves_preds_transfers simp:slice_kinds_def)
    from ‹S,slice_kind S ⊢ (xs,s'') -ax→ (msx',s')›
    have "pred (slice_kind S ax) s''" and "transfer (slice_kind S ax) s'' = s'"
      by(auto elim:observable_move.cases)
    with ‹preds (slice_kinds S asx) s› ‹as = asx@[ax]›
      ‹transfers (slice_kinds S asx) s = s''›
    have "preds (slice_kinds S as) s" by(simp add:preds_split slice_kinds_def)
    from ‹transfers (slice_kinds S asx) s = s''› 
      ‹transfer (slice_kind S ax) s'' = s'› ‹as = asx@[ax]›
    have "transfers (slice_kinds S as) s = s'" 
      by(simp add:transfers_split slice_kinds_def)
    with ‹preds (slice_kinds S asx') s'› ‹preds (slice_kinds S as) s›
    have "preds (slice_kinds S (as@asx')) s" by(simp add:preds_split slice_kinds_def)
    moreover
    from ‹valid_call_list cs m› ‹valid_return_list rs m›
      ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)› ‹length rs = length cs›
      ‹ms = targetnodes rs›
    have "∀i<length cs. call_of_return_node (ms!i) (sourcenode (cs!i))"
      by(rule stacks_rewrite)
    with ‹S,slice_kind S ⊢ (m # ms,s) =as⇒ (msx',s')› ‹ms = targetnodes rs›
      ‹length rs = length cs›
    have "slice_edges S cs as = [last as]"
      by(fastforce elim:observable_moves_singular_slice_edge)
    with ‹slice_edges S cs'' asx' = as'› ‹upd_cs cs as = cs''›
    have "slice_edges S cs (as@asx') = [last as]@as'"
      by(fastforce intro:slice_edges_Append)
    moreover
    from ‹S,slice_kind S ⊢ (m#ms,s) =asx⇒⇩τ (xs,s'')› ‹valid_node m›
      ‹valid_call_list cs m› ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)›
      ‹valid_return_list rs m› ‹length rs = length cs› ‹ms = targetnodes rs›
    have "m -asx→* sourcenode ax" by(fastforce intro:silent_moves_vpa_path)
    from ‹S,slice_kind S ⊢ (xs,s'') -ax→ (msx',s')› have "valid_edge ax"
      by(fastforce elim:observable_move.cases)
    hence "sourcenode ax -[ax]→* targetnode ax" by(rule path_edge)
    with ‹m -asx→* sourcenode ax› ‹as = asx@[ax]›
    have "m -as→* targetnode ax" by(fastforce intro:path_Append)
    with ‹targetnode ax -asx'→* m'› have "m -as@asx'→* m'"
      by -(rule path_Append)
    moreover
    from ‹∀a ∈ set asx. intra_kind (kind a)› have "valid_path_aux cs asx"
      by(rule valid_path_aux_intra_path)
    from ‹∀a ∈ set asx. intra_kind (kind a)› have "upd_cs cs asx = cs"
      by(rule upd_cs_intra_path)
    from ‹m -asx→* sourcenode ax› ‹∀a ∈ set asx. intra_kind (kind a)›
    have "get_proc m = get_proc (sourcenode ax)"
      by(fastforce intro:intra_path_get_procs simp:intra_path_def)
    with ‹valid_return_list rs m› have "valid_return_list rs (sourcenode ax)"
      apply(clarsimp simp:valid_return_list_def)
      apply(erule_tac x="cs'" in allE) apply clarsimp
      by(case_tac cs') auto
    with ‹S,slice_kind S ⊢ (xs,s'') -ax→ (msx',s')› ‹valid_edge ax› 
      ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)› ‹ms = targetnodes rs›
      ‹length rs = length cs›
    have "valid_path_aux cs [ax]"
      by(auto intro!:observable_move_vpa_path simp del:valid_path_aux.simps)
    with ‹valid_path_aux cs asx› ‹upd_cs cs asx = cs› ‹as = asx@[ax]›
    have "valid_path_aux cs as" by(fastforce intro:valid_path_aux_Append)
    with ‹upd_cs cs as = cs''› ‹valid_path_aux cs'' asx'›
    have "valid_path_aux cs (as@asx')" by(fastforce intro:valid_path_aux_Append)
    moreover
    from ‹upd_cs cs as = cs''› ‹upd_cs cs'' asx' = cs'›
    have "upd_cs cs (as@asx') = cs'" by(rule upd_cs_Append)
    moreover
    from ‹transfers (slice_kinds S as) s = s'› 
      ‹transfers (slice_kinds S asx') s' ≠ []›
    have "transfers (slice_kinds S (as@asx')) s ≠ []"
      by(simp add:slice_kinds_def transfers_split)
    moreover
    from ‹S,slice_kind S ⊢ (m # ms,s) =as⇒ (msx',s')›
    have "transfers (map (slice_kind S) as) s = s'"
      by simp(rule observable_moves_preds_transfers)
    from ‹S,slice_kind S ⊢ (m # ms,s) =as⇒ (msx',s')› ‹ms = targetnodes rs›
      ‹length rs = length cs› ‹∀i<length rs. rs ! i ∈ get_return_edges (cs ! i)›
      ‹valid_call_list cs m› ‹valid_return_list rs m›
    have "slice_edges S cs as = [last as]"
      by(fastforce intro!:observable_moves_singular_slice_edge
      [OF _ _ _ stacks_rewrite])
    from ‹S,slice_kind S ⊢ (m#ms,s) =asx⇒⇩τ (xs,s'')› callstack
    have "s = s''" by(fastforce intro:silent_moves_slice_keeps_state)
    with ‹S,slice_kind S ⊢ (xs,s'') -ax→ (msx',s')›
    have "transfer (slice_kind S ax) s = s'" by(fastforce elim:observable_move.cases)
    with ‹slice_edges S cs as = [last as]› ‹as = asx@[ax]›
    have "s' = transfers (slice_kinds S (slice_edges S cs as)) s"
      by(simp add:slice_kinds_def)
    from ‹upd_cs cs as = cs''›
    have "slice_edges S cs (as @ asx') =
      (slice_edges S cs as)@(slice_edges S cs'' asx')"
      by(fastforce intro:slice_edges_Append)
    hence trans_eq':"transfers (slice_kinds S (slice_edges S cs (as @ asx'))) s =
      transfers (slice_kinds S (slice_edges S cs'' asx'))
        (transfers (slice_kinds S (slice_edges S cs as)) s)"
      by(simp add:slice_kinds_def transfers_split)
    from ‹s' = transfers (slice_kinds S (slice_edges S cs as)) s›
      ‹transfers (map (slice_kind S) as) s = s'›
    have "transfers (map (slice_kind S) (slice_edges S cs as)) s =
      transfers (map (slice_kind S) as) s"
      by(simp add:slice_kinds_def)
    with trans_eq trans_eq'
      ‹s' = transfers (slice_kinds S (slice_edges S cs as)) s›
    have "transfers (slice_kinds S (slice_edges S cs (as @ asx'))) s =
       transfers (slice_kinds S (as @ asx')) s" 
      by(simp add:slice_kinds_def transfers_split)
    ultimately show ?case
      using ‹valid_node m'› ‹valid_call_list cs' m'› 
        ‹∀i<length rs'. rs' ! i ∈ get_return_edges (cs' ! i)› 
        ‹valid_return_list rs' m'› ‹length rs' = length cs'› ‹ms' = targetnodes rs'›
      apply(rule_tac x="as@asx'" in exI)
      apply(rule_tac x="cs'" in exI)
      apply(rule_tac x="rs'" in exI)
      by clarsimp
  qed
qed


subsection ‹The fundamental property of static interprocedural slicing›

theorem fundamental_property_of_static_slicing:
  assumes "m -as→⇩√* m'" and "preds (kinds as) [cf]" and "CFG_node m' ∈ S"
  obtains as' where "preds (slice_kinds S as') [cf]"
  and "∀V ∈ 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] ≠ []" and "m -as'→⇩√* m'"
proof(atomize_elim)
  from ‹m -as→⇩√* m'› ‹preds (kinds as) [cf]› obtain ms'' s'' ms' as' as''
    where "S,kind ⊢ ([m],[cf]) =slice_edges S [] as⇒* 
                              (ms'',s'')"
    and "S,kind ⊢ (ms'',s'') =as'⇒⇩τ (m'#ms',transfers (kinds as) [cf])"
    and "slice_edges S [] as = slice_edges S [] as''"
    and "m -as''@as'→⇩√* m'"
    by(auto elim:valid_path_trans_observable_moves[of _ _ _ _ _ "S"])
  from ‹m -as→⇩√* m'› have "valid_node m" and "valid_node m'"
    by(auto intro:path_valid_node simp:vp_def)
  with ‹CFG_node m' ∈ S› have "CFG_node m' ∈ HRB_slice S" 
    by -(rule HRB_slice_refl)
  from ‹valid_node m› ‹CFG_node m' ∈ S› have "(([m],[cf]),([m],[cf])) ∈ WS S" 
    by(fastforce intro:WSI)
  { fix V assume "V ∈ Use m'"
    with ‹valid_node m'› have "V ∈ Use⇘SDG⇙ (CFG_node m')" 
      by(fastforce intro:CFG_Use_SDG_Use)
    moreover
    from ‹valid_node m'› 
    have "parent_node (CFG_node m') -[]→⇩ι* parent_node (CFG_node m')" 
      by(fastforce intro:empty_path simp:intra_path_def)
    ultimately have "V ∈ rv S (CFG_node m')"
      using ‹CFG_node m' ∈ HRB_slice S› ‹CFG_node m' ∈ S›
      by(fastforce intro:rvI simp:sourcenodes_def) }
  hence "∀V ∈ Use m'. V ∈ rv S (CFG_node m')" by simp
  show "∃as'. preds (slice_kinds S as') [cf] ∧
    (∀V∈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] ≠ [] ∧ m -as'→⇩√* m'"
  proof(cases "slice_edges S [] as = []")
    case True
    hence "preds (slice_kinds S []) [cf]" 
      and "slice_edges S [] [] = slice_edges S [] as"
      by(simp_all add:slice_kinds_def)
    with ‹S,kind ⊢ ([m],[cf]) =slice_edges S [] as⇒* (ms'',s'')›
    have [simp]:"ms'' = [m]" "s'' = [cf]" by(auto elim:trans_observable_moves.cases)
    with ‹S,kind ⊢ (ms'',s'') =as'⇒⇩τ (m'#ms',transfers (kinds as) [cf])›
    have "S,kind ⊢ ([m],[cf]) =as'⇒⇩τ (m'#ms',transfers (kinds as) [cf])"
      by simp
    with ‹valid_node m› have "m -as'→* m'" and "valid_path_aux [] as'"
      by(auto intro:silent_moves_vpa_path[of _ _ _ _ _ _ _ _ _ "[]"]
               simp:targetnodes_def valid_return_list_def)
    hence "m -as'→⇩√* m'" by(simp add:vp_def valid_path_def)
    from ‹S,kind ⊢ ([m],[cf]) =as'⇒⇩τ (m'#ms',transfers (kinds as) [cf])›
    have "slice_edges S [] as' = []"
      by(fastforce dest:silent_moves_no_slice_edges[where cs="[]" and rs="[]"]
                  simp:targetnodes_def)
    from ‹S,kind ⊢ ([m],[cf]) =as'⇒⇩τ (m'#ms',transfers (kinds as) [cf])›
      ‹valid_node m› ‹valid_node m'› ‹CFG_node m' ∈ S›
    have returns:"∀mx ∈ set ms'. 
      ∃mx'. call_of_return_node mx mx' ∧ mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
      by -(erule silent_moves_called_node_in_slice1_nodestack_in_slice1
        [of _ _ _ _ _ _ _ _ _ "[]" "[]"],
        auto intro:refl_slice1 simp:targetnodes_def valid_return_list_def)
    from ‹S,kind ⊢ ([m],[cf]) =as'⇒⇩τ (m'#ms',transfers (kinds as) [cf])›
      ‹(([m],[cf]),([m],[cf])) ∈ WS S›
    have WS:"((m'#ms',transfers (kinds as) [cf]),([m],[cf])) ∈ WS S"
      by(rule WS_silent_moves)
    hence "transfers (kinds as) [cf] ≠ []" by(auto elim!:WS.cases)
    with WS returns ‹transfers (kinds as) [cf] ≠ []› 
    have "∀V ∈ rv S (CFG_node m'). 
      state_val (transfers (kinds as) [cf]) V = fst cf V"
      apply - apply(erule WS.cases) apply clarsimp
      by(case_tac msx)(auto simp:hd_conv_nth)
    with ‹∀V ∈ Use m'. V ∈ rv S (CFG_node m')›
    have Uses:"∀V ∈ Use m'. state_val (transfers (kinds as) [cf]) V = fst cf V"
      by simp
    have [simp]:"ms' = []"
    proof(rule ccontr)
      assume "ms' ≠ []"
      with ‹S,kind ⊢ ([m],[cf]) =as'⇒⇩τ (m'#ms',transfers (kinds as) [cf])›
        ‹valid_node m› ‹valid_node m'› ‹CFG_node m' ∈ S›
      show False
        by(fastforce elim:silent_moves_nonempty_nodestack_False intro:refl_slice1)
    qed
    with ‹S,kind ⊢ ([m],[cf]) =as'⇒⇩τ (m'#ms',transfers (kinds as) [cf])›
    have "S,kind ⊢ ([m],[cf]) =as'⇒⇩τ ([m'],transfers (kinds as) [cf])"
      by simp
    with ‹valid_node m› have "m -as'→⇘sl⇙* m'" by(fastforce dest:silent_moves_slp)
    from this ‹slice_edges S [] as' = []› 
    obtain asx where "m -asx→⇩ι* m'" and "slice_edges S [] asx = []"
      by(erule slp_to_intra_path_with_slice_edges)
    with ‹CFG_node m' ∈ HRB_slice S›
    obtain asx' where "m -asx'→⇩ι* m'" 
      and "preds (slice_kinds S asx') [cf]"
      and "slice_edges S [] asx' = []"
      by -(erule exists_sliced_intra_path_preds,auto simp:SDG_to_CFG_set_def)
    from ‹m -asx'→⇩ι* m'› have "m -asx'→⇩√* m'" by(rule intra_path_vp)
    from Uses ‹slice_edges S [] asx' = []›
    have "hd (transfers (slice_kinds S 
      (slice_edges S [] asx')) [cf]) = cf" by(simp add:slice_kinds_def)
    from ‹m -asx'→⇩ι* m'› ‹CFG_node m' ∈ S›
    have "transfers (slice_kinds S (slice_edges S [] asx')) [cf] = 
      transfers (slice_kinds S asx') [cf]"
      by(fastforce intro:transfers_intra_slice_kinds_slice_edges simp:intra_path_def)
    with ‹hd (transfers (slice_kinds S (slice_edges S [] asx')) [cf]) = cf›
    have "hd (transfers (slice_kinds S asx') [cf]) = cf" by simp
    with Uses have "∀V∈Use m'. state_val (transfers (slice_kinds S asx') [cf]) V =
      state_val (transfers (kinds as) [cf]) V" by simp
    with ‹m -asx'→⇩√* m'› ‹preds (slice_kinds S asx') [cf]›
      ‹slice_edges S [] asx' = []› ‹transfers (kinds as) [cf] ≠ []› True
    show ?thesis by fastforce
  next
    case False
    with ‹(([m],[cf]),([m],[cf])) ∈ WS S›
      ‹S,kind ⊢ ([m],[cf]) =slice_edges S [] as⇒* (ms'',s'')›
    have WS:"((ms'',s''),(ms'',transfers (slice_kinds S (slice_edges S [] as)) [cf]))
      ∈ WS S"
      and tom:"S,slice_kind S ⊢ ([m],[cf]) =slice_edges S [] as⇒* 
      (ms'',transfers (slice_kinds S (slice_edges S [] as)) [cf])"
      by(fastforce dest:WS_weak_sim_trans)+
    from WS obtain mx msx where [simp]:"ms'' = mx#msx" and "valid_node mx"
      by -(erule WS.cases,cases ms'',auto)
    from ‹S,kind ⊢ (ms'',s'') =as'⇒⇩τ (m'#ms',transfers (kinds as) [cf])› WS 
    have WS':"((m'#ms',transfers (kinds as) [cf]),
      (mx#msx,transfers (slice_kinds S (slice_edges S [] as)) [cf])) ∈ WS S"
      by simp(rule WS_silent_moves)
    from tom ‹valid_node m›
    obtain asx csx rsx where "preds (slice_kinds S asx) [cf]"
      and "slice_edges S [] asx = slice_edges S [] as"
      and "m -asx→⇩√* mx" and "transfers (slice_kinds S asx) [cf] ≠ []"
      and "upd_cs [] asx = csx" and stack:"valid_node mx" "valid_call_list csx mx" 
      "∀i < length rsx. rsx!i ∈ 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]"
      by(auto elim:slice_tom_preds_vp[of _ _ _ _ _ _ _ _ "[]" "[]"]
              simp:valid_call_list_def valid_return_list_def targetnodes_def 
                   vp_def valid_path_def)
    from ‹transfers (slice_kinds S asx) [cf] ≠ []›
    obtain cf' cfs' where eq:"transfers (slice_kinds S asx) [cf] = 
      cf'#cfs'" by(cases "transfers (slice_kinds S asx) [cf]") auto
    from WS' have callstack:"∀mx ∈ set msx. ∃mx'. call_of_return_node mx mx' ∧ 
      mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
      by(fastforce elim:WS.cases)
    with ‹S,kind ⊢ (ms'',s'') =as'⇒⇩τ (m'#ms',transfers (kinds as) [cf])›
      ‹valid_node m'› stack ‹CFG_node m' ∈ S›
    have callstack':"∀mx ∈ set ms'. ∃mx'. call_of_return_node mx mx' ∧ 
      mx' ∈ ⌊HRB_slice S⌋⇘CFG⇙"
      by simp(erule silent_moves_called_node_in_slice1_nodestack_in_slice1
        [of _ _ _ _ _ _ _ _ _ rsx csx],auto intro:refl_slice1)
    with ‹S,kind ⊢ (ms'',s'') =as'⇒⇩τ (m'#ms',transfers (kinds as) [cf])›
      stack callstack
    have "mx -as'→⇘sl⇙* m'" and "msx = ms'" by(auto dest!:silent_moves_slp)
    from ‹S,kind ⊢ (ms'',s'') =as'⇒⇩τ (m'#ms',transfers (kinds as) [cf])›
      stack
    have "slice_edges S csx as' = []"
      by(auto dest:silent_moves_no_slice_edges[OF _ _ _ stacks_rewrite])
    with ‹mx -as'→⇘sl⇙* m'› obtain asx'' where "mx -asx''→⇩ι* m'"
      and "slice_edges S csx asx'' = []"
      by(erule slp_to_intra_path_with_slice_edges)
    from stack have "∀i<length csx. call_of_return_node (msx!i) (sourcenode (csx!i))"
      by -(rule stacks_rewrite)
    with callstack ‹msx = targetnodes rsx› ‹length rsx = length csx›
    have "∀c∈set csx. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙"
      by(auto simp:all_set_conv_all_nth targetnodes_def)
    with ‹mx -asx''→⇩ι* m'› ‹slice_edges S csx asx'' = []› ‹valid_node m'›
      eq ‹CFG_node m' ∈ S›
    obtain asx' where "mx -asx'→⇩ι* m'"
      and "preds (slice_kinds S asx') (cf'#cfs')"
      and "slice_edges S csx asx' = []"
      by -(erule exists_sliced_intra_path_preds,
        auto intro:HRB_slice_refl simp:SDG_to_CFG_set_def)
    with eq have "preds (slice_kinds S asx') 
      (transfers (slice_kinds S asx) [cf])" by simp
    with ‹preds (slice_kinds S asx) [cf]›
    have "preds (slice_kinds S (asx@asx')) [cf]"
      by(simp add:slice_kinds_def preds_split)
    from ‹m -asx→⇩√* mx› ‹mx -asx'→⇩ι* m'› have "m -asx@asx'→⇩√* m'"
      by(fastforce elim:vp_slp_Append intra_path_slp)
    from ‹upd_cs [] asx = csx› ‹slice_edges S csx asx' = []›
    have "slice_edges S [] (asx@asx') = 
      (slice_edges S [] asx)@[]"
      by(fastforce intro:slice_edges_Append)
    from ‹mx -asx'→⇩ι* m'› ‹∀c∈set csx. sourcenode c ∈ ⌊HRB_slice S⌋⇘CFG⇙›
    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])"
      by(fastforce intro:transfers_intra_slice_kinds_slice_edges simp:intra_path_def) 
    from ‹upd_cs [] asx = csx›
    have "slice_edges S [] (asx@asx') = 
      (slice_edges S [] asx)@(slice_edges S csx asx')"
      by(fastforce intro:slice_edges_Append)
    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])"
      by(simp add:slice_kinds_def transfers_split)
    with trans_eq 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])" by simp
    with trans_eq' have trans_eq'':
      "transfers (slice_kinds S (slice_edges S [] (asx@asx'))) [cf] =
      transfers (slice_kinds S (asx@asx')) [cf]" 
      by(simp add:slice_kinds_def transfers_split)
    from WS' obtain x xs where "m'#ms' = xs@x#msx"
      and "xs ≠ [] ⟶ (∃mx'. call_of_return_node x mx' ∧ 
      mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙)"
      and rest:"∀i < length (mx#msx). ∀V ∈ 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] ≠ []"
      "transfers (slice_kinds S 
      (slice_edges S [] as)) [cf] ≠ []"
      by(fastforce elim:WS.cases)
    from ‹m'#ms' = xs@x#msx› ‹xs ≠ [] ⟶ (∃mx'. call_of_return_node x mx' ∧ 
      mx' ∉ ⌊HRB_slice S⌋⇘CFG⇙)› callstack'
    have [simp]:"xs = []" "x = m'" "ms' = msx" by(cases xs,auto)+
    from rest have "∀V ∈ rv S (CFG_node m').
      state_val (transfers (kinds as) [cf]) V = 
      state_val (transfers (slice_kinds S (slice_edges S [] as)) [cf]) V"
      by(fastforce dest:hd_conv_nth)
    with ‹∀V ∈ Use m'. V ∈ rv S (CFG_node m')› 
      ‹slice_edges S [] asx = slice_edges S [] as›
    have "∀V ∈ Use m'. state_val (transfers (kinds as) [cf]) V = 
      state_val (transfers (slice_kinds S (slice_edges S [] asx)) [cf]) V"
      by simp
    with ‹slice_edges S [] (asx@asx') = (slice_edges S [] asx)@[]›
    have "∀V ∈ Use m'. state_val (transfers (kinds as) [cf]) V = 
      state_val (transfers (slice_kinds S (slice_edges S [] (asx@asx'))) [cf]) V"
      by simp
    with trans_eq'' have "∀V ∈ Use m'. state_val (transfers (kinds as) [cf]) V = 
      state_val (transfers (slice_kinds S (asx@asx')) [cf]) V"
      by simp
    with ‹preds (slice_kinds S (asx@asx')) [cf]›
      ‹m -asx@asx'→⇩√* m'› ‹slice_edges S [] (asx@asx') = 
      (slice_edges S [] asx)@[]› ‹transfers (kinds as) [cf] ≠ []›
      ‹slice_edges S [] asx = slice_edges S [] as›
    show ?thesis by fastforce
  qed
qed

end


subsection ‹The fundamental property of static interprocedural slicing related to the semantics›

locale SemanticsProperty = SDG sourcenode targetnode kind valid_edge Entry 
    get_proc get_return_edges procs Main Exit Def Use ParamDefs ParamUses +
  CFG_semantics_wf sourcenode targetnode kind valid_edge Entry 
    get_proc get_return_edges procs Main sem identifies
  for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
  and kind :: "'edge ⇒ ('var,'val,'ret,'pname) edge_kind" 
  and valid_edge :: "'edge ⇒ bool"
  and Entry :: "'node" ("'('_Entry'_')")  and get_proc :: "'node ⇒ 'pname"
  and get_return_edges :: "'edge ⇒ 'edge set"
  and procs :: "('pname × 'var list × 'var list) list" and Main :: "'pname"
  and Exit::"'node"  ("'('_Exit'_')") 
  and Def :: "'node ⇒ 'var set" and Use :: "'node ⇒ 'var set"
  and ParamDefs :: "'node ⇒ 'var list" and ParamUses :: "'node ⇒ 'var set list"
  and sem :: "'com ⇒ ('var ⇀ 'val) list ⇒ 'com ⇒ ('var ⇀ 'val) list ⇒ bool" 
    ("((1⟨_,/_⟩) ⇒/ (1⟨_,/_⟩))" [0,0,0,0] 81)
  and identifies :: "'node ⇒ 'com ⇒ bool" ("_ ≜ _" [51,0] 80)
begin


theorem fundamental_property_of_path_slicing_semantically:
  assumes "m ≜ c" and "⟨c,[cf]⟩ ⇒ ⟨c',s'⟩"
  obtains m' as cfs' where "m -as→⇩√* m'" and "m' ≜ c'"
  and "preds (slice_kinds {CFG_node m'} as) [(cf,undefined)]"
  and "∀V ∈ Use m'. 
  state_val (transfers (slice_kinds {CFG_node m'} as) [(cf,undefined)]) V = 
  state_val cfs' V" and "map fst cfs' = s'"
proof(atomize_elim) 
  from ‹m ≜ c› ‹⟨c,[cf]⟩ ⇒ ⟨c',s'⟩› obtain m' as cfs' where "m -as→⇩√* m'"
    and "transfers (kinds as) [(cf,undefined)] = cfs'"
    and "preds (kinds as) [(cf,undefined)]" and "m' ≜ c'" and "map fst cfs' = s'"
    by(fastforce dest:fundamental_property)
  from ‹m -as→⇩√* m'› ‹preds (kinds as) [(cf,undefined)]› obtain as'
    where "preds (slice_kinds {CFG_node m'} as') [(cf,undefined)]"
    and vals:"∀V ∈ Use m'. state_val (transfers (slice_kinds {CFG_node m'} as') 
    [(cf,undefined)]) V = state_val (transfers (kinds as) [(cf,undefined)]) V"
    and "m -as'→⇩√* m'"
    by -(erule fundamental_property_of_static_slicing,auto)
  from ‹transfers (kinds as) [(cf,undefined)] = cfs'› vals have "∀V ∈ Use m'. 
    state_val (transfers (slice_kinds {CFG_node m'} as') [(cf,undefined)]) V = 
    state_val cfs' V" by simp
  with ‹preds (slice_kinds {CFG_node m'} as') [(cf,undefined)]› ‹m -as'→⇩√* m'› 
    ‹m' ≜ c'› ‹map fst cfs' = s'›
  show "∃as m' cfs'. m -as→⇩√* m' ∧ m' ≜ c' ∧
    preds (slice_kinds {CFG_node m'} as) [(cf, undefined)] ∧
    (∀V∈Use m'. state_val (transfers (slice_kinds {CFG_node m'} as)
    [(cf, undefined)]) V = state_val cfs' V) ∧ map fst cfs' = s'"
    by blast
qed

end

end