Theory WeakSimulation

section ‹The weak simulation›

theory WeakSimulation imports Slice begin

context SDG begin

lemma call_node_notin_slice_return_node_neither:
  assumes "call_of_return_node n n'" and "n'  HRB_slice SCFG"
  shows "n  HRB_slice SCFG"
proof -
  from call_of_return_node n n' obtain a a' where "return_node n"
    and "valid_edge a" and "n' = sourcenode a"
    and "valid_edge a'" and "a'  get_return_edges a" 
    and "n = targetnode a'" by(fastforce simp:call_of_return_node_def)
  from valid_edge a a'  get_return_edges a obtain Q p r fs 
    where "kind a = Q:r↪⇘pfs" by(fastforce dest!:only_call_get_return_edges)
  with valid_edge a a'  get_return_edges a obtain Q' f' where "kind a' = Q'↩⇘pf'"
    by(fastforce dest!:call_return_edges)
  from valid_edge a kind a = Q:r↪⇘pfs a'  get_return_edges a
  have "CFG_node (sourcenode a) s-psum CFG_node (targetnode a')"
    by(fastforce intro:sum_SDG_call_summary_edge)
  show ?thesis
  proof
    assume "n  HRB_slice SCFG"
    with n = targetnode a' have "CFG_node (targetnode a')  HRB_slice S"
      by(simp add:SDG_to_CFG_set_def)
    hence "CFG_node (sourcenode a)  HRB_slice S"
    proof(induct "CFG_node (targetnode a')" rule:HRB_slice_cases)
      case (phase1 nx)
      with CFG_node (sourcenode a) s-psum CFG_node (targetnode a')
      show ?case by(fastforce intro:combine_SDG_slices.combSlice_refl sum_slice1 
                              simp:HRB_slice_def)
    next
      case (phase2 nx n' n'' p')
      from CFG_node (targetnode a')  sum_SDG_slice2 n' 
        CFG_node (sourcenode a) s-psum CFG_node (targetnode a') valid_edge a
      have "CFG_node (sourcenode a)  sum_SDG_slice2 n'"
        by(fastforce intro:sum_slice2)
      with n'  sum_SDG_slice1 nx n'' s-p'ret CFG_node (parent_node n') nx  S
      show ?case by(fastforce intro:combine_SDG_slices.combSlice_Return_parent_node
                              simp:HRB_slice_def)
    qed
    with n'  HRB_slice SCFG n' = sourcenode a show False 
      by(simp add:SDG_to_CFG_set_def HRB_slice_def)
  qed
qed


lemma edge_obs_intra_slice_eq:
assumes "valid_edge a" and "intra_kind (kind a)" and "sourcenode a  HRB_slice SCFG"
  shows "obs_intra (targetnode a) HRB_slice SCFG = 
         obs_intra (sourcenode a) HRB_slice SCFG"
proof -
  from assms have "obs_intra (targetnode a) HRB_slice SCFG 
                   obs_intra (sourcenode a) HRB_slice SCFG"
    by(rule edge_obs_intra_subset)
  from valid_edge a have "valid_node (sourcenode a)" by simp
  { fix x assume "x  obs_intra (sourcenode a) HRB_slice SCFG"
    and "obs_intra (targetnode a) HRB_slice SCFG = {}"
    have "as. targetnode a -asι* x"
    proof(cases "method_exit x")
      case True
      from valid_edge a have "valid_node (targetnode a)" by simp
      then obtain asx where "targetnode a -asx* (_Exit_)" 
        by(fastforce dest:Exit_path)
      then obtain as pex where "targetnode a -asι* pex" and "method_exit pex"
        by -(erule valid_Exit_path_intra_path)
      hence "get_proc pex = get_proc (targetnode a)"
        by -(rule intra_path_get_procs[THEN sym])
      also from valid_edge a intra_kind (kind a) 
      have " = get_proc (sourcenode a)"
        by -(rule get_proc_intra[THEN sym])
      also from x  obs_intra (sourcenode a) HRB_slice SCFG True
      have " = get_proc x"
        by(fastforce elim:obs_intraE intro:intra_path_get_procs)
      finally have "pex = x" using method_exit pex True
        by -(rule method_exit_unique)
      with targetnode a -asι* pex show ?thesis by fastforce
    next
      case False
      with x  obs_intra (sourcenode a) HRB_slice SCFG
      have "x postdominates (sourcenode a)" by(rule obs_intra_postdominate)
      with valid_edge a intra_kind (kind a) sourcenode a  HRB_slice SCFG
        x  obs_intra (sourcenode a) HRB_slice SCFG
      have "x postdominates (targetnode a)"
        by(fastforce elim:postdominate_inner_path_targetnode path_edge obs_intraE 
                    simp:intra_path_def sourcenodes_def)
      thus ?thesis by(fastforce elim:postdominate_implies_inner_path)
    qed
    then obtain as where "targetnode a -asι* x" by blast
    from x  obs_intra (sourcenode a) HRB_slice SCFG
    have "x  HRB_slice SCFG" by -(erule obs_intraE)
    have "x'  HRB_slice SCFG. as'. targetnode a -as'ι* x'  
      (a'  set (sourcenodes as'). a'  HRB_slice SCFG)"
    proof(cases "a'  set (sourcenodes as). a'  HRB_slice SCFG")
      case True
      then obtain zs z zs' where "sourcenodes as = zs@z#zs'"
        and "z  HRB_slice SCFG" and "z'  set zs. z'  HRB_slice SCFG"
        by(erule split_list_first_propE)
      then obtain ys y ys'
        where "sourcenodes ys = zs" and "as = ys@y#ys'"
        and "sourcenode y = z"
        by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
      from targetnode a -asι* x as = ys@y#ys'
      have "targetnode a -ys@y#ys'→* x" and "y'  set ys. intra_kind (kind y')"
        by(simp_all add:intra_path_def)
      from targetnode a -ys@y#ys'→* x have "targetnode a -ys→* sourcenode y"
        by(rule path_split)
      with y'  set ys. intra_kind (kind y') sourcenode y = z
        z'  set zs. z'  HRB_slice SCFG z  HRB_slice SCFG
        sourcenodes ys = zs
      show ?thesis by(fastforce simp:intra_path_def)
    next
      case False
      with targetnode a -asι* x x  HRB_slice SCFG
      show ?thesis by fastforce
    qed
    hence "y. y  obs_intra (targetnode a) HRB_slice SCFG"
      by(fastforce intro:obs_intra_elem)
    with obs_intra (targetnode a) HRB_slice SCFG = {} 
    have False by simp }
  with obs_intra (targetnode a) HRB_slice SCFG 
        obs_intra (sourcenode a) HRB_slice SCFG valid_node (sourcenode a)
  show ?thesis by(cases "obs_intra (targetnode a) HRB_slice SCFG = {}") 
                 (auto dest!:obs_intra_singleton_disj)
qed


lemma intra_edge_obs_slice:
  assumes "ms  []" and "ms''  obs ms' HRB_slice SCFG" and "valid_edge a" 
  and "intra_kind (kind a)" 
  and disj:"(m  set (tl ms). m'. call_of_return_node m m'  
                               m'  HRB_slice SCFG)  hd ms  HRB_slice SCFG"
  and "hd ms = sourcenode a" and "ms' = targetnode a#tl ms" 
  and "n  set (tl ms'). return_node n"
  shows "ms''  obs ms HRB_slice SCFG"
proof -
  from ms''  obs ms' HRB_slice SCFG n  set (tl ms'). return_node n
  obtain msx m msx' mx m' where "ms' = msx@m#msx'" and "ms'' = mx#msx'"
    and "mx  obs_intra m HRB_slice SCFG"
    and "nx  set msx'. nx'. call_of_return_node nx nx'  nx'  HRB_slice SCFG"
    and imp:"xs x xs'. msx = xs@x#xs'  obs_intra x HRB_slice SCFG  {}
     (x''  set (xs'@[m]). mx. call_of_return_node x'' mx  
                                   mx  HRB_slice SCFG)"
    by(erule obsE)
  show ?thesis
  proof(cases msx)
    case Nil
    with nx  set msx'. nx'. call_of_return_node nx nx'  nx'  HRB_slice SCFG
      disj ms' = msx@m#msx' hd ms = sourcenode a ms' = targetnode a#tl ms
    have "sourcenode a  HRB_slice SCFG" by(cases ms) auto
    from ms' = msx@m#msx' ms' = targetnode a#tl ms Nil 
    have "m = targetnode a" by simp
    with valid_edge a intra_kind (kind a) sourcenode a  HRB_slice SCFG
      mx  obs_intra m HRB_slice SCFG
    have "mx  obs_intra (sourcenode a) HRB_slice SCFG"
      by(fastforce dest:edge_obs_intra_subset)
    from ms' = msx@m#msx' Nil ms' = targetnode a # tl ms 
      hd ms = sourcenode a ms  []
    have "ms = []@sourcenode a#msx'" by(cases ms) auto
    with ms'' = mx#msx' mx  obs_intra (sourcenode a) HRB_slice SCFG  
      nx  set msx'. nx'. call_of_return_node nx nx'  nx'  HRB_slice SCFG Nil
    show ?thesis by(fastforce intro!:obsI)
  next
    case (Cons x xs)
    with ms' = msx@m#msx' ms' = targetnode a # tl ms
    have "msx = targetnode a#xs" by simp
    from Cons ms' = msx@m#msx' ms' = targetnode a # tl ms hd ms = sourcenode a
    have "ms = (sourcenode a#xs)@m#msx'" by(cases ms) auto
    from disj ms = (sourcenode a#xs)@m#msx' 
      nx  set msx'. nx'. call_of_return_node nx nx'  nx'  HRB_slice SCFG
    have disj2:"(m  set (xs@[m]). m'. call_of_return_node m m'  
                            m'  HRB_slice SCFG)  hd ms  HRB_slice SCFG"
      by fastforce
    hence "zs z zs'. sourcenode a#xs = zs@z#zs'  obs_intra z HRB_slice SCFG  {}
       (z''  set (zs'@[m]). mx. call_of_return_node z'' mx  
                                   mx  HRB_slice SCFG)"
    proof(cases "hd ms  HRB_slice SCFG")
      case True
      with hd ms = sourcenode a have "sourcenode a  HRB_slice SCFG" by simp
      with valid_edge a intra_kind (kind a)
      have "obs_intra (targetnode a) HRB_slice SCFG = 
        obs_intra (sourcenode a) HRB_slice SCFG"
        by(rule edge_obs_intra_slice_eq)
      with imp msx = targetnode a#xs show ?thesis
        by auto(case_tac zs,fastforce,erule_tac x="targetnode a#list" in allE,fastforce)
    next
      case False
      with hd ms = sourcenode a valid_edge a 
      have "obs_intra (sourcenode a) HRB_slice SCFG = {sourcenode a}"
        by(fastforce intro!:n_in_obs_intra)
      from False disj2 
      have "m  set (xs@[m]). m'. call_of_return_node m m'  m'  HRB_slice SCFG"
        by simp
      with imp obs_intra (sourcenode a) HRB_slice SCFG = {sourcenode a}
        msx = targetnode a#xs show ?thesis
        by auto(case_tac zs,fastforce,erule_tac x="targetnode a#list" in allE,fastforce)
    qed
    with ms' = msx@m#msx' ms' = targetnode a # tl ms hd ms = sourcenode a
      ms'' = mx#msx' mx  obs_intra m HRB_slice SCFG 
      nx  set msx'. nx'. call_of_return_node nx nx'  nx'  HRB_slice SCFG
      ms = (sourcenode a#xs)@m#msx'
    show ?thesis by(simp del:obs.simps)(rule obsI,auto)
  qed
qed



subsection ‹Silent moves›

inductive silent_move :: 
  "'node SDG_node set  ('edge  ('var,'val,'ret,'pname) edge_kind)  'node list  
  (('var  'val) × 'ret) list  'edge  'node list  (('var  'val) × 'ret) list  bool"
("_,_  '(_,_') -_τ '(_,_')" [51,50,0,0,50,0,0] 51) 

where silent_move_intra:
  "pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind(kind a);
    (m  set (tl ms). m'. call_of_return_node m m'  m'  HRB_slice SCFG) 
    hd ms  HRB_slice SCFG; m  set (tl ms). return_node m;
    length s' = length s; length ms = length s;
    hd ms = sourcenode a; ms' = (targetnode a)#tl ms  
   S,f  (ms,s) -aτ (ms',s')"

  | silent_move_call:
  "pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r↪⇘pfs; 
    valid_edge a'; a'  get_return_edges a;
    (m  set (tl ms). m'. call_of_return_node m m'  m'  HRB_slice SCFG) 
    hd ms  HRB_slice SCFG; m  set (tl ms). return_node m;
    length ms = length s; length s' = Suc(length s); 
    hd ms = sourcenode a; ms' = (targetnode a)#(targetnode a')#tl ms  
   S,f  (ms,s) -aτ (ms',s')"

  | silent_move_return:
  "pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q↩⇘pf'; 
    m  set (tl ms). m'. call_of_return_node m m'  m'  HRB_slice SCFG;
    m  set (tl ms). return_node m; length ms = length s; length s = Suc(length s');
    s'  []; hd ms = sourcenode a; hd(tl ms) = targetnode a; ms' = tl ms  
   S,f  (ms,s) -aτ (ms',s')"


lemma silent_move_valid_nodes:
  "S,f  (ms,s) -aτ (ms',s'); m  set ms'. valid_node m
   m  set ms. valid_node m"
by(induct rule:silent_move.induct)(case_tac ms,auto)+


lemma silent_move_return_node:
  "S,f  (ms,s) -aτ (ms',s')  m  set (tl ms'). return_node m"
proof(induct rule:silent_move.induct)
  case (silent_move_intra f a s s' ms nc ms')
  thus ?case by simp
next
  case (silent_move_call f a s s' Q r p fs a' ms nc ms')
  from valid_edge a' valid_edge a a'  get_return_edges a
  have "return_node (targetnode a')" by(fastforce simp:return_node_def)
  with mset (tl ms). return_node m ms' = targetnode a # targetnode a' # tl ms
  show ?case by simp
next
  case (silent_move_return f a s s' Q p f' ms nc ms')
  thus ?case by(cases "tl ms") auto
qed


lemma silent_move_equal_length:
  assumes "S,f  (ms,s) -aτ (ms',s')" 
  shows "length ms = length s" and "length ms' = length s'"
proof -
  from S,f  (ms,s) -aτ (ms',s')
  have "length ms = length s  length ms' = length s'"
  proof(induct rule:silent_move.induct)
    case (silent_move_intra f a s s' ms nc ms')
    from pred (f a) s obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
    from length ms = length s ms' = targetnode a # tl ms
      length s' = length s show ?case by simp
  next
    case (silent_move_call f a s s' Q r p fs a' ms nc ms')
    from pred (f a) s obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
    from length ms = length s length s' = Suc (length s) 
      ms' = targetnode a # targetnode a' # tl ms show ?case by simp
  next
    case (silent_move_return f a s s' Q p f' ms nc ms')
    from length ms = length s length s = Suc (length s') ms' = tl ms s'  []
    show ?case by simp
  qed
  thus "length ms = length s" and "length ms' = length s'" by simp_all
qed


lemma silent_move_obs_slice:
  "S,kind  (ms,s) -aτ (ms',s'); msx  obs ms' HRB_slice SCFG; 
    n  set (tl ms'). return_node n
   msx  obs ms HRB_slice SCFG"
proof(induct S f"kind" ms s a ms' s' rule:silent_move.induct)
  case (silent_move_intra a s s' ms nc ms')
  from pred (kind a) s length ms = length s have "ms  []"
    by(cases s) auto
  with silent_move_intra show ?case by -(rule intra_edge_obs_slice)
next
  case (silent_move_call a s s' Q r p fs a' ms S ms')
  note disj = (mset (tl ms). m'. call_of_return_node m m'  
    m'  HRB_slice SCFG)  hd ms  HRB_slice SCFG
  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 a'  get_return_edges a valid_edge a'
  have "call_of_return_node (targetnode a') (sourcenode a)"
    by(simp add:call_of_return_node_def) blast
  from pred (kind a) s length ms = length s
  have "ms  []" by(cases s) auto
  from disj
  show ?case
  proof
    assume "hd ms  HRB_slice SCFG"
    with hd ms = sourcenode a have "sourcenode a  HRB_slice SCFG" by simp
    with call_of_return_node (targetnode a') (sourcenode a)
      ms' = targetnode a # targetnode a' # tl ms
    have "n'  set (tl ms'). nx. call_of_return_node n' nx  nx  HRB_slice SCFG"
      by fastforce
    with msx  obs ms' HRB_slice SCFG ms' = targetnode a # targetnode a' # tl ms
    have "msx  obs (targetnode a' # tl ms) HRB_slice SCFG" by simp
    from valid_edge a a'  get_return_edges a
    obtain a'' where "valid_edge a''" and [simp]:"sourcenode a'' = sourcenode a"
      and [simp]:"targetnode a'' = targetnode a'" and "intra_kind(kind a'')"
      by -(drule call_return_node_edge,auto simp:intra_kind_def)
    from mset (tl ms'). return_node m ms' = targetnode a # targetnode a' # tl ms
    have "mset (tl ms). return_node m" by simp
    with ms  [] msx  obs (targetnode a'#tl ms) HRB_slice SCFG
      valid_edge a'' intra_kind(kind a'') disj
      hd ms = sourcenode a
    show ?case by -(rule intra_edge_obs_slice,fastforce+)
  next
    assume "mset (tl ms).
      m'. call_of_return_node m m'  m'  HRB_slice SCFG"
    with ms  [] msx  obs ms' HRB_slice SCFG
      ms' = targetnode a # targetnode a' # tl ms
    show ?thesis by(cases ms) auto
  qed
next
  case (silent_move_return a s s' Q p f' ms S ms')
  from length ms = length s length s = Suc (length s') s'  []
  have "ms  []" and "tl ms  []" by(auto simp:length_Suc_conv)
  from mset (tl ms).
    m'. call_of_return_node m m'  m'  HRB_slice SCFG
    tl ms  [] hd (tl ms) = targetnode a
  have "(m'. call_of_return_node (targetnode a) m'  m'  HRB_slice SCFG) 
    (mset (tl (tl ms)). m'. call_of_return_node m m'  m'  HRB_slice SCFG)"
    by(cases "tl ms") auto
  hence "obs ms HRB_slice SCFG = obs (tl ms) HRB_slice SCFG"
  proof
    assume "m'. call_of_return_node (targetnode a) m'  m'  HRB_slice SCFG"
    from tl ms  [] have "hd (tl ms)  set (tl ms)" by simp
    with hd (tl ms) = targetnode a have "targetnode a  set (tl ms)" by simp
    with ms  [] 
      m'. call_of_return_node (targetnode a) m'  m'  HRB_slice SCFG
    have "mset (tl ms). m'. call_of_return_node m m'  
      m'  HRB_slice SCFG" by(cases ms) auto
    with ms  [] show ?thesis by(cases ms) auto
  next
    assume "mset (tl (tl ms)). m'. call_of_return_node m m'  
      m'  HRB_slice SCFG"
    with ms  [] tl ms  [] show ?thesis
      by(cases ms,auto simp:Let_def)(case_tac list,auto)+
  qed
  with ms' = tl ms msx  obs ms' HRB_slice SCFG show ?case by simp
qed



lemma silent_move_empty_obs_slice:
  assumes "S,f  (ms,s) -aτ (ms',s')" and "obs ms' HRB_slice SCFG = {}"
  shows "obs ms HRB_slice SCFG = {}"
proof(rule ccontr)
  assume "obs ms HRB_slice SCFG  {}"
  then obtain xs where "xs  obs ms HRB_slice SCFG" by fastforce
  from S,f  (ms,s) -aτ (ms',s')
  have "m  set (tl ms). return_node m"
    by(fastforce elim!:silent_move.cases simp:call_of_return_node_def)
  with xs  obs ms HRB_slice SCFG
  obtain msx m msx' m' where assms:"ms = msx@m#msx'" "xs = m'#msx'"
    "m'  obs_intra m HRB_slice SCFG" 
    "mx  set msx'. mx'. call_of_return_node mx mx'  mx'  HRB_slice SCFG"
    "xs x xs'. msx = xs@x#xs'  obs_intra x HRB_slice SCFG  {}
     (x''  set (xs'@[m]). mx. call_of_return_node x'' mx  
                              mx  HRB_slice SCFG)"
    by(erule obsE)
  from S,f  (ms,s) -aτ (ms',s') obs ms' HRB_slice SCFG = {} assms
  show False
  proof(induct rule:silent_move.induct)
    case (silent_move_intra f a s s' ms S ms')
    note disj = (mset (tl ms). m'. call_of_return_node m m'  
      m'  HRB_slice SCFG)  hd ms  HRB_slice SCFG
    note msx = xs x xs'. msx = xs@x#xs'  obs_intra x HRB_slice SCFG  {}  
      (x''set (xs' @ [m]). mx. call_of_return_node x'' mx  mx  HRB_slice SCFG)
    note msx' = mxset msx'. mx'. call_of_return_node mx mx'  
      mx'  HRB_slice SCFG
    show False
    proof(cases msx)
      case Nil
      with ms = msx @ m # msx' hd ms = sourcenode a have [simp]:"m = sourcenode a"
        and "tl ms = msx'" by simp_all
      from Nil ms' = targetnode a # tl ms ms = msx @ m # msx'
      have "ms' = msx @ targetnode a # msx'" by simp
      from msx' disj tl ms = msx' hd ms = sourcenode a
      have "sourcenode a  HRB_slice SCFG" by fastforce
      with valid_edge a intra_kind (kind a)
      have "obs_intra (targetnode a) HRB_slice SCFG =
        obs_intra (sourcenode a) HRB_slice SCFG" by(rule edge_obs_intra_slice_eq)
      with m'  obs_intra m HRB_slice SCFG
      have "m'  obs_intra (targetnode a) HRB_slice SCFG" by simp
      from msx Nil have "xs x xs'. msx = xs@x#xs'   
        obs_intra x HRB_slice SCFG  {}  
        (x''set (xs' @ [targetnode a]). mx. call_of_return_node x'' mx  
        mx  HRB_slice SCFG)" by simp
      with m'  obs_intra (targetnode a) HRB_slice SCFG msx' 
        ms' = msx @ targetnode a # msx'
      have "m'#msx'  obs ms' HRB_slice SCFG" by(rule obsI)
      with obs ms' HRB_slice SCFG = {} show False by simp
    next
      case (Cons y ys)
      with ms = msx @ m # msx' ms' = targetnode a # tl ms hd ms = sourcenode a
      have "ms' = targetnode a # ys @ m # msx'" and "y = sourcenode a" 
        and "tl ms = ys @ m # msx'" by simp_all
      { fix x assume "x  obs_intra (targetnode a) HRB_slice SCFG"
        have "obs_intra (sourcenode a) HRB_slice SCFG  {}"
        proof(cases "sourcenode a  HRB_slice SCFG")
          case True
          from valid_edge a have "valid_node (sourcenode a)" by simp
          from this True 
          have "obs_intra (sourcenode a) HRB_slice SCFG = {sourcenode a}"
            by(rule n_in_obs_intra)
          thus ?thesis by simp
        next
          case False
          from valid_edge a intra_kind (kind a) False
          have "obs_intra (targetnode a) HRB_slice SCFG = 
            obs_intra (sourcenode a) HRB_slice SCFG"
            by(rule edge_obs_intra_slice_eq)
          with x  obs_intra (targetnode a) HRB_slice SCFG show ?thesis
            by fastforce
        qed }
      with msx Cons y = sourcenode a 
      have "xs x xs'. targetnode a # ys = xs@x#xs'  
        obs_intra x HRB_slice SCFG  {}  (x''set (xs' @ [m]). 
        mx. call_of_return_node x'' mx  mx  HRB_slice SCFG)"
        apply clarsimp apply(case_tac xs) apply auto
        apply(erule_tac x="[]" in allE) apply clarsimp
        apply(erule_tac x="sourcenode a # list" in allE) apply auto
        done
      with m'  obs_intra m HRB_slice SCFG msx' 
        ms' = targetnode a # ys @ m # msx'
      have "m'#msx'  obs ms' HRB_slice SCFG" by -(rule obsI,auto)
      with obs ms' HRB_slice SCFG = {} show False by simp
    qed
  next
    case (silent_move_call f a s s' Q r p fs a' ms S ms')
    note disj = (mset (tl ms). m'. call_of_return_node m m'  
      m'  HRB_slice SCFG)  hd ms  HRB_slice SCFG
    note msx = xs x xs'. msx = xs@x#xs'  obs_intra x HRB_slice SCFG  {}  
      (x''set (xs' @ [m]). mx. call_of_return_node x'' mx  mx  HRB_slice SCFG)
    note msx' = mxset msx'. mx'. call_of_return_node mx mx'  
      mx'  HRB_slice SCFG
    from valid_edge a a'  get_return_edges a obtain a'' where "valid_edge a''"
      and "sourcenode a'' = sourcenode a" and "targetnode a'' = targetnode a'"
      and "intra_kind (kind a'')" 
      by(fastforce dest:call_return_node_edge simp:intra_kind_def)
    from valid_edge a' 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)
    show False
    proof(cases msx)
      case Nil
      with ms = msx @ m # msx' hd ms = sourcenode a have [simp]:"m = sourcenode a"
        and "tl ms = msx'" by simp_all
      from Nil ms' = targetnode a # targetnode a' # tl ms ms = msx @ m # msx'
      have "ms' = targetnode a # targetnode a' # msx'" by simp
      from msx' disj tl ms = msx' hd ms = sourcenode a
      have "sourcenode a  HRB_slice SCFG" by fastforce
      from valid_edge a'' intra_kind (kind a'') sourcenode a  HRB_slice SCFG
        sourcenode a'' = sourcenode a targetnode a'' = targetnode a'
      have "obs_intra (targetnode a') HRB_slice SCFG = 
         obs_intra (sourcenode a) HRB_slice SCFG"
        by(fastforce dest:edge_obs_intra_slice_eq)
      with m'  obs_intra m HRB_slice SCFG 
      have "m'  obs_intra (targetnode a') HRB_slice SCFG" by simp
      from this msx' have "m'#msx'  obs (targetnode a'#msx') HRB_slice SCFG"
        by(fastforce intro:obsI)
      from call_of_return_node (targetnode a') (sourcenode a)
        sourcenode a  HRB_slice SCFG
      have "m'  set (targetnode a'#msx').
        mx. call_of_return_node m' mx  mx  HRB_slice SCFG"
        by fastforce
      with m'#msx'  obs (targetnode a'#msx') HRB_slice SCFG
      have "m'#msx'  obs (targetnode a#targetnode a'#msx') HRB_slice SCFG"
        by simp
      with ms' = targetnode a # targetnode a' # msx' obs ms' HRB_slice SCFG = {}
      show False by simp
    next
      case (Cons y ys)
      with ms = msx @ m # msx' ms' = targetnode a # targetnode a' # tl ms 
        hd ms = sourcenode a
      have "ms' = targetnode a # targetnode a' # ys @ m # msx'" 
        and "y = sourcenode a" and "tl ms = ys @ m # msx'" by simp_all
      show False
      proof(cases "obs_intra (targetnode a) HRB_slice SCFG  {}  
          (x''set (targetnode a' # ys @ [m]).
          mx. call_of_return_node x'' mx  mx  HRB_slice SCFG)")
        case True
        hence imp:"obs_intra (targetnode a) HRB_slice SCFG  {} 
          (x''set (targetnode a' # ys @ [m]).
          mx. call_of_return_node x'' mx  mx  HRB_slice SCFG)" .
        show False
        proof(cases "obs_intra (targetnode a') HRB_slice SCFG  {}  
            (x''set (ys @ [m]). mx. call_of_return_node x'' mx  
            mx  HRB_slice SCFG)")
          case True
          with imp msx Cons y = sourcenode a 
          have "xs x xs'. targetnode a # targetnode a' # ys = xs@x#xs'  
            obs_intra x HRB_slice SCFG  {}  (x''set (xs' @ [m]). 
            mx. call_of_return_node x'' mx  mx  HRB_slice SCFG)"
            apply clarsimp apply(case_tac xs) apply fastforce
            apply(case_tac list) apply fastforce apply clarsimp
            apply(erule_tac x="sourcenode a # lista" in allE) apply auto
            done
          with m'  obs_intra m HRB_slice SCFG msx' 
            ms' = targetnode a # targetnode a' # ys @ m # msx'
          have "m'#msx'  obs ms' HRB_slice SCFG" by -(rule obsI,auto)
          with obs ms' HRB_slice SCFG = {} show False by simp
        next
          case False
          hence "obs_intra (targetnode a') HRB_slice SCFG  {}"
            and all:"x''set (ys @ [m]). mx. call_of_return_node x'' mx  
            mx  HRB_slice SCFG"
            by fastforce+
          have "obs_intra (sourcenode a) HRB_slice SCFG  {}"
          proof(cases "sourcenode a  HRB_slice SCFG")
            case True
            from valid_edge a have "valid_node (sourcenode a)" by simp
            from this True 
            have "obs_intra (sourcenode a) HRB_slice SCFG = {sourcenode a}"
              by(rule n_in_obs_intra)
            thus ?thesis by simp
          next
            case False
            with sourcenode a'' = sourcenode a
            have "sourcenode a''  HRB_slice SCFG" by simp
            with valid_edge a'' intra_kind (kind a'')
            have "obs_intra (targetnode a'') HRB_slice SCFG = 
              obs_intra (sourcenode a'') HRB_slice SCFG"
              by(rule edge_obs_intra_slice_eq)
            with obs_intra (targetnode a') HRB_slice SCFG  {} 
              sourcenode a'' = sourcenode a targetnode a'' = targetnode a'
            show ?thesis by fastforce 
          qed
          with msx Cons y = sourcenode a all
          show False by simp blast
        qed
      next
        case False
        hence "obs_intra (targetnode a) HRB_slice SCFG  {}"
          and all:"x''set (targetnode a' # ys @ [m]). 
          mx. call_of_return_node x'' mx  mx  HRB_slice SCFG"
          by fastforce+
        with Cons y = sourcenode a msx 
        have "obs_intra (sourcenode a) HRB_slice SCFG = {}" by auto blast
        from call_of_return_node (targetnode a') (sourcenode a) all
        have "sourcenode a  HRB_slice SCFG" by fastforce
        from valid_edge a have "valid_node (sourcenode a)" by simp
        from this sourcenode a  HRB_slice SCFG 
        have "obs_intra (sourcenode a) HRB_slice SCFG = {sourcenode a}"
          by(rule n_in_obs_intra)
        with obs_intra (sourcenode a) HRB_slice SCFG = {} show False by simp
      qed
    qed
  next
    case (silent_move_return f a s s' Q p f' ms S ms')
    note msx = xs x xs'. msx = xs@x#xs'  obs_intra x HRB_slice SCFG  {}  
      (x''set (xs' @ [m]). mx. call_of_return_node x'' mx  mx  HRB_slice SCFG)
    note msx' = mxset msx'. mx'. call_of_return_node mx mx'  
      mx'  HRB_slice SCFG
    show False
    proof(cases msx)
      case Nil
      with ms = msx @ m # msx' hd ms = sourcenode a have  "tl ms = msx'" by simp
      with mset (tl ms). m'. call_of_return_node m m'  m'  HRB_slice SCFG
        msx'
      show False by fastforce
    next
      case (Cons y ys)
      with ms = msx @ m # msx' hd ms = sourcenode a ms' = tl ms
      have "ms' = ys @ m # msx'" and "y = sourcenode a" by simp_all
      from msx Cons have "xs x xs'. ys = xs@x#xs'  
        obs_intra x HRB_slice SCFG  {}   (x''set (xs' @ [m]). 
        mx. call_of_return_node x'' mx  mx  HRB_slice SCFG)"
        by auto (erule_tac x="y # xs" in allE,auto)
      with m'  obs_intra m HRB_slice SCFG msx' ms' = ys @ m # msx'
      have "m'#msx'  obs ms' HRB_slice SCFG" by(rule obsI)
      with obs ms' HRB_slice SCFG = {} show False by simp
    qed
  qed
qed



inductive silent_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 silent_moves_Nil: "length ms = length s  S,f  (ms,s) =[]τ (ms,s)"

  | silent_moves_Cons:
  "S,f  (ms,s) -aτ (ms',s'); S,f  (ms',s') =asτ (ms'',s'') 
   S,f  (ms,s) =a#asτ (ms'',s'')"


lemma silent_moves_equal_length:
  assumes "S,f  (ms,s) =asτ (ms',s')" 
  shows "length ms = length s" and "length ms' = length s'"
proof -
  from S,f  (ms,s) =asτ (ms',s') 
  have "length ms = length s  length ms' = length s'"
  proof(induct 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')
    have "length ms = length s" and "length ms' = length s'" 
      by(rule silent_move_equal_length)+
    with length ms' = length s'  length ms'' = length s''
    show ?case by simp
  qed simp
  thus "length ms = length s" "length ms' = length s'" by simp_all
qed


lemma silent_moves_Append:
  "S,f  (ms,s) =asτ (ms'',s''); S,f  (ms'',s'') =as'τ (ms',s')
   S,f  (ms,s) =as@as'τ (ms',s')"
by(induct rule:silent_moves.induct)(auto intro:silent_moves.intros)


lemma silent_moves_split:
  assumes "S,f  (ms,s) =as@as'τ (ms',s')"
  obtains ms'' s'' where "S,f  (ms,s) =asτ (ms'',s'')"
  and "S,f  (ms'',s'') =as'τ (ms',s')"
proof(atomize_elim)
  from S,f  (ms,s) =as@as'τ (ms',s')
  show "ms'' s''. S,f  (ms,s) =asτ (ms'',s'')  S,f  (ms'',s'') =as'τ (ms',s')"
  proof(induct as arbitrary:ms s)
    case Nil
    from S,f  (ms,s) =[] @ as'τ (ms',s') have "length ms = length s"
      by(fastforce intro:silent_moves_equal_length)
    hence "S,f  (ms,s) =[]τ (ms,s)" by(rule silent_moves_Nil)
    with S,f  (ms,s) =[] @ as'τ (ms',s') show ?case by fastforce
  next
    case (Cons ax asx)
    note IH = ms s. S,f  (ms,s) =asx @ as'τ (ms',s') 
      ms'' s''. S,f  (ms,s) =asxτ (ms'',s'')  S,f  (ms'',s'') =as'τ (ms',s')
    from S,f  (ms,s) =(ax # asx) @ as'τ (ms',s')
    obtain msx sx where "S,f  (ms,s) -axτ (msx,sx)"
      and "S,f  (msx,sx) =asx @ as'τ (ms',s')"
      by(auto elim:silent_moves.cases)
    from IH[OF this(2)] obtain ms'' s'' where "S,f  (msx,sx) =asxτ (ms'',s'')"
      and "S,f  (ms'',s'') =as'τ (ms',s')" by blast
    from S,f  (ms,s) -axτ (msx,sx) S,f  (msx,sx) =asxτ (ms'',s'')
    have "S,f  (ms,s) =ax#asxτ (ms'',s'')" by(rule silent_moves_Cons)
    with S,f  (ms'',s'') =as'τ (ms',s') show ?case by blast
  qed
qed


lemma valid_nodes_silent_moves:
  "S,f (ms,s) =as'τ (ms',s'); m  set ms. valid_node m
   m  set ms'. valid_node m"
proof(induct rule:silent_moves.induct)
  case (silent_moves_Cons S f ms s a ms' s' as ms'' s'')
  note IH = mset ms'. valid_node m  mset ms''. valid_node m
  from S,f  (ms,s) -aτ (ms',s') mset ms. valid_node m
  have "mset ms'. valid_node m"
    apply - apply(erule silent_move.cases) apply auto
    by(cases ms,auto dest:get_return_edges_valid)+
  from IH[OF this] show ?case .
qed simp


lemma return_nodes_silent_moves:
  "S,f  (ms,s) =as'τ (ms',s'); m  set (tl ms). return_node m
   m  set (tl ms'). return_node m"
by(induct rule:silent_moves.induct,auto dest:silent_move_return_node)


lemma silent_moves_intra_path:
  "S,f  (m#ms,s) =asτ (m'#ms',s'); a  set as. intra_kind(kind a)
   ms = ms'  get_proc m = get_proc m'"
proof(induct S f "m#ms" s as "m'#ms'" s' arbitrary:m
  rule:silent_moves.induct)
  case (silent_moves_Cons S f sx a msx' sx' as s'')
  thus ?case
  proof(induct _ _ "m # ms" _ _ _ _ rule:silent_move.induct)
    case (silent_move_intra f a s s' nc msx')
    note IH = m. msx' = m # ms; aset as. intra_kind (kind a)
       ms = ms'  get_proc m = get_proc m'
    from msx' = targetnode a # tl (m # ms)
    have "msx' = targetnode a # ms" by simp
    from aset (a # as). intra_kind (kind a) have "aset as. intra_kind (kind a)"
      by simp
    from IH[OF msx' = targetnode a # ms this]
    have "ms = ms'" and "get_proc (targetnode a) = get_proc m'" by simp_all
    moreover
    from valid_edge a intra_kind (kind a)
    have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
    moreover
    from hd (m # ms) = sourcenode a have "m = sourcenode a" by simp
    ultimately show ?case using ms = ms' by simp
  qed (auto simp:intra_kind_def)
qed simp


lemma silent_moves_nodestack_notempty: 
  "S,f  (ms,s) =asτ (ms',s'); ms  []  ms'  []"
apply(induct S f ms s as ms' s' rule:silent_moves.induct) apply auto
apply(erule silent_move.cases) apply auto
apply(case_tac "tl msa") by auto


lemma silent_moves_obs_slice:
  "S,kind  (ms,s) =asτ (ms',s'); mx  obs ms' HRB_slice SCFG; 
  n  set (tl ms'). return_node n
   mx  obs ms HRB_slice SCFG  (n  set (tl ms). return_node n)"
proof(induct S f"kind" ms s as ms' s' rule:silent_moves.induct)
  case silent_moves_Nil thus ?case by simp
next
  case (silent_moves_Cons S ms s a ms' s' as ms'' s'')
  note IH = mx  obs ms'' HRB_slice SCFG; mset (tl ms''). return_node m
     mx  obs ms' HRB_slice SCFG  (mset (tl ms'). return_node m)
  from IH[OF mx  obs ms'' HRB_slice SCFG mset (tl ms''). return_node m]
  have "mx  obs ms' HRB_slice SCFG" and "mset (tl ms'). return_node m"
    by simp_all
  with S,kind  (ms,s) -aτ (ms',s')
  have "mx  obs ms HRB_slice SCFG" by(fastforce intro:silent_move_obs_slice)
  moreover
  from S,kind  (ms,s) -aτ (ms',s') have "mset (tl ms). return_node m"
    by(fastforce elim:silent_move.cases)
  ultimately show ?case by simp
qed


lemma silent_moves_empty_obs_slice:
  "S,f  (ms,s) =asτ (ms',s'); obs ms' HRB_slice SCFG = {}
   obs ms HRB_slice SCFG = {}"
proof(induct rule:silent_moves.induct)
  case silent_moves_Nil thus ?case by simp
next
  case (silent_moves_Cons S f ms s a ms' s' as ms'' s'')
  note IH = obs ms'' HRB_slice SCFG = {}  obs ms' HRB_slice SCFG = {}
  from IH[OF obs ms'' HRB_slice SCFG = {}]
  have "obs ms' HRB_slice SCFG = {}" by simp
  with S,f  (ms,s) -aτ (ms',s')
  show ?case by -(rule silent_move_empty_obs_slice,fastforce)
qed


lemma silent_moves_preds_transfers:
  assumes "S,f  (ms,s) =asτ (ms',s')"
  shows "preds (map f as) s" and "transfers (map f as) s = s'"
proof -
  from S,f  (ms,s) =asτ (ms',s')
  have "preds (map f as) s  transfers (map f as) s = s'"
  proof(induct rule:silent_moves.induct)
    case silent_moves_Nil thus ?case by simp
  next
    case (silent_moves_Cons S f ms s a ms' s' as ms'' s'')
    from S,f  (ms,s) -aτ (ms',s')
    have "pred (f a) s" and "transfer (f a) s = s'" by(auto elim:silent_move.cases)
    with preds (map f as) s'  transfers (map f as) s' = s''
    show ?case by fastforce
  qed
  thus "preds (map f as) s" and "transfers (map f as) s = s'" by simp_all
qed



lemma silent_moves_intra_path_obs:
  assumes "m'  obs_intra m HRB_slice SCFG" and "length s = length (m#msx')"
  and "m  set msx'. return_node m"
  obtains as' where "S,slice_kind S  (m#msx',s) =as'τ (m'#msx',s)"
proof(atomize_elim)
  from m'  obs_intra m HRB_slice SCFG
  obtain as where "m -asι* m'" and "m'  HRB_slice SCFG"
    by -(erule obs_intraE)
  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 m'  obs_intra m HRB_slice SCFG
    length s = length (m#msx') m  set msx'. return_node m
  show "as. S,slice_kind S  (m#msx',s) =asτ (m'#msx',s)"
  proof(induct x arbitrary:m s rule:nat.induct)
    fix m fix s::"(('var  'val) × 'ret) list"
    assume "distance m m' 0" and "length s = length (m#msx')"
    then obtain as' where "m -as'ι* m'" and "length as' = 0"
      by(auto elim:distance.cases)
    hence "m -[]ι* m'" by(cases as) auto
    hence [simp]:"m = m'" by(fastforce elim:path.cases simp:intra_path_def)
    with length s = length (m#msx')[THEN sym]
    have "S,slice_kind S  (m#msx',s) =[]τ (m#msx',s)" 
      by -(rule silent_moves_Nil)
    thus "as. S,slice_kind S  (m#msx',s) =asτ (m'#msx',s)" by simp blast
  next
    fix x m fix s::"(('var  'val) × 'ret) list"
    assume "distance m m' (Suc x)" and "m'  obs_intra m HRB_slice SCFG"
      and "length s = length (m#msx')" and "m  set msx'. return_node m"
      and IH:"m s. distance m m' x; m'  obs_intra m HRB_slice SCFG;
                     length s = length (m#msx'); m  set msx'. return_node m
       as. S,slice_kind S  (m#msx',s) =asτ (m'#msx',s)"
    from m'  obs_intra m HRB_slice SCFG have "valid_node m"
      by(rule in_obs_intra_valid)
    with distance m m' (Suc x) have "m  m'"
      by(fastforce elim:distance.cases dest:empty_path simp:intra_path_def)
    have "m  HRB_slice SCFG"
    proof
      assume isin:"m  HRB_slice SCFG"
      with valid_node m have "obs_intra m HRB_slice SCFG = {m}"
        by(fastforce intro!:n_in_obs_intra)
      with m'  obs_intra m HRB_slice SCFG m  m' show False by simp
    qed
    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 mx. a'. sourcenode a = sourcenode a'  
                                               distance (targetnode a') m' x 
                                               valid_edge a'  intra_kind (kind a')  
                                               targetnode a' = mx)"
      by -(erule distance_successor_distance,simp+)
    from m'  obs_intra m HRB_slice SCFG 
    have "obs_intra m HRB_slice SCFG = {m'}"
      by(rule obs_intra_singleton_element)
    with valid_edge a m  HRB_slice SCFG m = sourcenode a intra_kind(kind a)
    have disj:"obs_intra (targetnode a) HRB_slice SCFG = {}  
               obs_intra (targetnode a) HRB_slice SCFG = {m'}"
      by -(drule_tac S="HRB_slice SCFG" in edge_obs_intra_subset,auto)
    from intra_kind(kind a) length s = length (m#msx') m  HRB_slice SCFG 
      m = sourcenode a
    have length:"length (transfer (slice_kind S a) s) = length (targetnode a#msx')"
      by(cases s)
    (auto split:if_split_asm simp add:Let_def slice_kind_def intra_kind_def)
    from distance (targetnode a) m' x obtain asx where "targetnode a -asxι* m'" 
      and "length asx = x" and "as'. targetnode a -as'ι* m'  x  length as'"
      by(auto elim:distance.cases)
    from targetnode a -asxι* m' m'  HRB_slice SCFG
    obtain mx where "mx  obs_intra (targetnode a) HRB_slice SCFG" 
      by(erule path_ex_obs_intra)
    with disj have "m'  obs_intra (targetnode a) HRB_slice SCFG" by fastforce
    from IH[OF distance (targetnode a) m' x this length 
      m  set msx'. return_node m]
    obtain asx' where moves:"S,slice_kind S  
      (targetnode a#msx',transfer (slice_kind S a) s) =asx'τ 
      (m'#msx',transfer (slice_kind S a) s)" by blast
    have "pred (slice_kind S a) s  transfer (slice_kind S a) s = s"
    proof(cases "kind a")
      fix f assume "kind a = f"
      with m  HRB_slice SCFG m = sourcenode a have "slice_kind S a = id"
        by(fastforce intro:slice_kind_Upd)
      with length s = length (m#msx') show ?thesis by(cases s) auto
    next
      fix Q assume "kind a = (Q)"
      with m  HRB_slice SCFG m = sourcenode a
        m'  obs_intra m HRB_slice SCFG distance (targetnode a) m' x
        distance m m' (Suc x) target
      have "slice_kind S a = (λs. True)"
        by(fastforce intro:slice_kind_Pred_obs_nearer_SOME)
      with length s = length (m#msx') show ?thesis by(cases s) auto
    next
      fix Q r p fs assume "kind a = Q:r↪⇘pfs"
      with intra_kind(kind a) have False by(simp add:intra_kind_def)
      thus ?thesis by simp
    next
      fix Q p f assume "kind a = Q↩⇘pf"
      with intra_kind(kind a) have False by(simp add:intra_kind_def)
      thus ?thesis by simp
    qed
    hence "pred (slice_kind S a) s" and "transfer (slice_kind S a) s = s"
      by simp_all
    with m  HRB_slice SCFG m = sourcenode a valid_edge a
      intra_kind(kind a) length s = length (m#msx') m  set msx'. return_node m
    have "S,slice_kind S  (sourcenode a#msx',s) -aτ 
                             (targetnode a#msx',transfer (slice_kind S a) s)"
      by(fastforce intro:silent_move_intra)
    with moves transfer (slice_kind S a) s = s m = sourcenode a
    have "S,slice_kind S  (m#msx',s) =a#asx'τ (m'#msx',s)"
      by(fastforce intro:silent_moves_Cons)
    thus "as. S,slice_kind S  (m#msx',s) =asτ (m'#msx',s)" by blast
  qed
qed


lemma silent_moves_intra_path_no_obs:
  assumes "obs_intra m HRB_slice SCFG = {}" and "method_exit m'"
  and "get_proc m = get_proc m'" and "valid_node m" and "length s = length (m#msx')"
  and "m  set msx'. return_node m"
  obtains as where "S,slice_kind S  (m#msx',s) =asτ (m'#msx',s)"
proof(atomize_elim)
  from method_exit m' get_proc m = get_proc m' valid_node m
  obtain as where "m -asι* m'" by(erule intra_path_to_matching_method_exit)
  then obtain x where "distance m m' x" and "x  length as"
    by(erule every_path_distance)
  from distance m m' x m -asι* m' obs_intra m HRB_slice SCFG = {}
    length s = length (m#msx') m  set msx'. return_node m
  show "as. S,slice_kind S  (m#msx',s) =asτ (m'#msx',s)"
  proof(induct x arbitrary:m as s rule:nat.induct)
    fix m fix s::"(('var  'val) × 'ret) list"
    assume "distance m m' 0" and "length s = length (m#msx')"
    then obtain as' where "m -as'ι* m'" and "length as' = 0"
      by(auto elim:distance.cases)
    hence "m -[]ι* m'" by(cases as) auto
    hence [simp]:"m = m'" by(fastforce elim:path.cases simp:intra_path_def)
    with length s = length (m#msx')[THEN sym]
    have "S,slice_kind S  (m#msx',s) =[]τ (m#msx',s)" 
      by(fastforce intro:silent_moves_Nil)
    thus "as. S,slice_kind S  (m#msx',s) =asτ (m'#msx',s)" by simp blast
  next
    fix x m as fix s::"(('var  'val) × 'ret) list"
    assume "distance m m' (Suc x)" and "m -asι* m'"
      and "obs_intra m HRB_slice SCFG = {}"
      and "length s = length (m#msx')" and "m  set msx'. return_node m"
      and IH:"m as s. distance m m' x; m -asι* m'; 
      obs_intra m HRB_slice SCFG = {}; length s = length (m#msx'); 
      m  set msx'. return_node m
       as. S,slice_kind S  (m#msx',s) =asτ (m'#msx',s)"
    from m -asι* m' have "valid_node m" 
      by(fastforce intro:path_valid_node simp:intra_path_def)
    from m -asι* m' have "get_proc m = get_proc m'" by(rule intra_path_get_procs)
    have "m  HRB_slice SCFG"
    proof
      assume "m  HRB_slice SCFG"
      with valid_node m have "obs_intra m HRB_slice SCFG = {m}"
        by(fastforce intro!:n_in_obs_intra)
      with obs_intra m HRB_slice SCFG = {} show False by simp
    qed
    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 mx. a'. sourcenode a = sourcenode a'  
                                               distance (targetnode a') m' x 
                                               valid_edge a'  intra_kind (kind a')  
                                               targetnode a' = mx)"
      by -(erule distance_successor_distance,simp+)
    from intra_kind(kind a) length s = length (m#msx') m  HRB_slice SCFG 
      m = sourcenode a
    have length:"length (transfer (slice_kind S a) s) = length (targetnode a#msx')"
      by(cases s)
    (auto split:if_split_asm simp add:Let_def slice_kind_def intra_kind_def)
    from distance (targetnode a) m' x obtain asx where "targetnode a -asxι* m'" 
      and "length asx = x" and "as'. targetnode a -as'ι* m'  x  length as'"
      by(auto elim:distance.cases)
    from valid_edge a intra_kind(kind a) m  HRB_slice SCFG 
      m = sourcenode a obs_intra m HRB_slice SCFG = {}
    have "obs_intra (targetnode a) HRB_slice SCFG = {}"
      by(fastforce dest:edge_obs_intra_subset)
    from IH[OF distance (targetnode a) m' x targetnode a -asxι* m' this
      length m  set msx'. return_node m] obtain as' 
      where moves:"S,slice_kind S  
      (targetnode a#msx',transfer (slice_kind S a) s) =as'τ 
      (m'#msx',transfer (slice_kind S a) s)" by blast
    have "pred (slice_kind S a) s  transfer (slice_kind S a) s = s"
    proof(cases "kind a")
      fix f assume "kind a = f"
      with m  HRB_slice SCFG m = sourcenode a have "slice_kind S a = id"
        by(fastforce intro:slice_kind_Upd)
      with length s = length (m#msx') show ?thesis by(cases s) auto
    next
      fix Q assume "kind a = (Q)"
      with m  HRB_slice SCFG m = sourcenode a
        obs_intra m HRB_slice SCFG = {} distance (targetnode a) m' x
        distance m m' (Suc x) method_exit m' get_proc m = get_proc m' target
      have "slice_kind S a = (λs. True)"
        by(fastforce intro:slice_kind_Pred_empty_obs_nearer_SOME)
     with length s = length (m#msx') show ?thesis by(cases s) auto
    next
      fix Q r p fs assume "kind a = Q:r↪⇘pfs"
      with intra_kind(kind a) have False by(simp add:intra_kind_def)
      thus ?thesis by simp
    next
      fix Q p f assume "kind a = Q↩⇘pf"
      with intra_kind(kind a) have False by(simp add:intra_kind_def)
      thus ?thesis by simp
    qed
    hence "pred (slice_kind S a) s" and "transfer (slice_kind S a) s = s"
      by simp_all
    with m  HRB_slice SCFG m = sourcenode a valid_edge a
      intra_kind(kind a) length s = length (m#msx') m  set msx'. return_node m
    have "S,slice_kind S  (sourcenode a#msx',s) -aτ 
                             (targetnode a#msx',transfer (slice_kind S a) s)"
      by(fastforce intro:silent_move_intra)
    with moves transfer (slice_kind S a) s = s m = sourcenode a
    have "S,slice_kind S  (m#msx',s) =a#as'τ (m'#msx',s)"
      by(fastforce intro:silent_moves_Cons)
    thus "as. S,slice_kind S  (m#msx',s) =asτ (m'#msx',s)" by blast
  qed
qed


lemma silent_moves_vpa_path:
  assumes "S,f  (m#ms,s) =asτ (m'#ms',s')" and "valid_node m"
  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"
  shows "m -as→* m'" and "valid_path_aux cs as"
proof -
  from assms have "m -as→* m'  valid_path_aux cs as"
  proof(induct S f "m#ms" s as "m'#ms'" s' arbitrary:m cs ms rs
      rule:silent_moves.induct)
    case (silent_moves_Nil msx sx nc f)
    from valid_node m' have "m' -[]→* m'"
      by (rule empty_path)
    thus ?case by fastforce
  next
    case (silent_moves_Cons S f sx a msx' sx' as s'')
    thus ?case
    proof(induct _ _ "m # ms" _ _ _ _ rule:silent_move.induct)
      case (silent_move_intra f a sx sx' nc msx')
      note IH = m cs ms rs. msx' = m # ms; 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
         m -as→* m'  valid_path_aux cs as
      from msx' = targetnode a # tl (m # ms)
      have "msx' = targetnode a # ms" by simp
      from valid_edge a intra_kind (kind a)
      have "get_proc (sourcenode a) = get_proc (targetnode a)"
        by(rule get_proc_intra)
      with valid_return_list rs m hd (m # ms) = sourcenode 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 valid_edge a have "valid_node (targetnode a)" by simp
      from IH[OF msx' = targetnode a # ms this 
        i<length rs. rs ! i  get_return_edges (cs ! i)
        ms = targetnodes rs valid_return_list rs (targetnode a)
        length rs = length cs]
      have "targetnode a -as→* m'" and "valid_path_aux cs as" by simp_all
      from valid_edge a targetnode a -as→* m' 
        hd (m # ms) = sourcenode a
      have "m -a#as→* m'" by(fastforce intro:Cons_path)
      moreover
      from intra_kind (kind a) valid_path_aux cs as
      have "valid_path_aux cs (a # as)" by(fastforce simp:intra_kind_def)
      ultimately show ?case by simp
    next
      case (silent_move_call f a sx sx' Q r p fs a' nc msx')
      note IH = m cs ms rs. msx' = m # ms; 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
         m -as→* m'  valid_path_aux cs as
      from valid_edge a have "valid_node (targetnode a)" by simp
      from length rs = length cs 
      have "length (a'#rs) = length (a#cs)" by simp
      from msx' = targetnode a # targetnode a' # tl (m # ms)
      have "msx' = targetnode a # targetnode a' # ms" by simp
      from ms = targetnodes rs have "targetnode a' # ms = targetnodes (a' # rs)"
        by(simp add:targetnodes_def)
      from valid_edge a kind a = Q:r↪⇘pfs have "get_proc (targetnode a) = p"
        by(rule get_proc_call)
      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↪⇘pfs a'  get_return_edges a
      obtain Q' f' where "kind a' = Q'↩⇘pf'" by(fastforce dest!:call_return_edges)
      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 hd (m # ms) = sourcenode a
        get_proc (targetnode a) = p valid_edge a' kind a' = Q'↩⇘pf'
      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) apply clarsimp
        by(case_tac list)(auto simp:targetnodes_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 IH[OF msx' = targetnode a # targetnode a' # ms valid_node (targetnode a) this 
        targetnode a' # ms = targetnodes (a' # rs) 
        valid_return_list (a' # rs) (targetnode a) length (a'#rs) = length (a#cs)]
      have "targetnode a -as→* m'" and "valid_path_aux (a # cs) as" by simp_all
      from valid_edge a targetnode a -as→* m' 
        hd (m # ms) = sourcenode a
      have "m -a#as→* m'" by(fastforce intro:Cons_path)
      moreover
      from valid_path_aux (a # cs) as kind a = Q:r↪⇘pfs
      have "valid_path_aux cs (a # as)" by simp
      ultimately show ?case by simp
    next
      case (silent_move_return f a sx sx' Q p f' nc msx')
      note IH = m cs ms rs. msx' = m # ms; 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
         m -as→* m'  valid_path_aux cs as
      from valid_edge a have "valid_node (targetnode a)" by simp
      from length (m # ms) = length sx length sx = Suc (length sx') 
        sx'  []
      obtain x xs where "ms = x#xs" by(cases ms) auto
      with ms = targetnodes rs obtain r' rs' where "rs = r'#rs'" 
        and "x = targetnode r'" and "xs = targetnodes rs'" 
        by(auto simp:targetnodes_def)
      with length rs = length cs obtain c' cs' where "cs = c'#cs'"
        and "length rs' = length cs'"
        by(cases cs) auto
      from ms = x#xs length (m # ms) = length sx 
        length sx = Suc (length sx')
      have "length sx' = Suc (length xs)" by simp
      from ms = x#xs msx' = tl (m # ms) hd (tl (m # ms)) = targetnode a
        length (m # ms) = length sx length sx = Suc (length sx') sx'  []
      have "msx' = targetnode a#xs" by simp
      from i<length rs. rs ! i  get_return_edges (cs ! i) 
        rs = r'#rs' cs = c'#cs'
      have "r'  get_return_edges c'" by fastforce
      from ms = x#xs hd (tl (m # ms)) = targetnode a
      have "x = targetnode a" by simp
      with valid_return_list rs m rs = r'#rs' x = targetnode r'
      have "valid_return_list rs' (targetnode a)"
        apply(clarsimp simp:valid_return_list_def)
        apply(erule_tac x="r'#cs'" in allE) apply clarsimp
        by(case_tac cs')(auto simp:targetnodes_def)
      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 IH[OF msx' = targetnode a#xs valid_node (targetnode a) 
        i<length rs'. rs' ! i  get_return_edges (cs' ! i) xs = targetnodes rs'
        valid_return_list rs' (targetnode a) length rs' = length cs']
      have "targetnode a -as→* m'" and "valid_path_aux cs' as" by simp_all
      from valid_edge a targetnode a -as→* m' 
        hd (m # ms) = sourcenode a
      have "m -a#as→* m'" by(fastforce intro:Cons_path)
      moreover
      from ms = x#xs hd (tl (m # ms)) = targetnode a
      have "x = targetnode a" by simp
      from valid_edge a kind a = Q↩⇘pf'
      have "method_exit (sourcenode a)" by(fastforce simp:method_exit_def)
      from valid_return_list rs m hd (m # ms) = sourcenode a 
        rs = r'#rs'
      have "get_proc (sourcenode a) = get_proc (sourcenode r') 
        method_exit (sourcenode r')  valid_edge r'"
        apply(clarsimp simp:valid_return_list_def method_exit_def)
        apply(erule_tac x="[]" in allE) 
        by(auto dest:get_proc_return)
      hence "get_proc (sourcenode a) = get_proc (sourcenode r')"
        and "method_exit (sourcenode r')" and "valid_edge r'" by simp_all
      with method_exit (sourcenode a) have "sourcenode r' = sourcenode a"
        by(fastforce intro:method_exit_unique)
      with valid_edge a valid_edge r' x = targetnode r' x = targetnode a
      have "r' = a" by(fastforce intro:edge_det)
      with r'  get_return_edges c' valid_path_aux cs' as cs = c'#cs' 
        kind a = Q↩⇘pf'
      have "valid_path_aux cs (a # as)" by simp
      ultimately show ?case by simp
    qed
  qed
  thus "m -as→* m'" and "valid_path_aux cs as" by simp_all
qed



subsection ‹Observable moves›


inductive observable_move ::
  "'node SDG_node set  ('edge  ('var,'val,'ret,'pname) edge_kind)  'node list  
   (('var  'val) × 'ret) list  'edge  'node list  (('var  'val) × 'ret) list  bool"
("_,_  '(_,_') -_ '(_,_')" [51,50,0,0,50,0,0] 51) 
 
  where observable_move_intra:
  "pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind(kind a); 
    m  set (tl ms). m'. call_of_return_node m m'  m'  HRB_slice SCFG;
    hd ms  HRB_slice SCFG; length s' = length s; length ms = length s;
    hd ms = sourcenode a; ms' = (targetnode a)#tl ms  
   S,f  (ms,s) -a (ms',s')"

  | observable_move_call:
  "pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r↪⇘pfs; 
    valid_edge a'; a'  get_return_edges a;
    m  set (tl ms). m'. call_of_return_node m m'  m'  HRB_slice SCFG;
    hd ms  HRB_slice SCFG; length ms = length s; length s' = Suc(length s); 
    hd ms = sourcenode a; ms' = (targetnode a)#(targetnode a')#tl ms  
   S,f  (ms,s) -a (ms',s')"

  | observable_move_return:
  "pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q↩⇘pf'; 
    m  set (tl ms). m'. call_of_return_node m m'  m'  HRB_slice SCFG;
    length ms = length s; length s = Suc(length s'); s'  [];
    hd ms = sourcenode a; hd(tl ms) = targetnode a; ms' = tl ms  
   S,f  (ms,s) -a (ms',s')"



inductive 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 observable_moves_snoc:
  "S,f  (ms,s) =asτ (ms',s'); S,f  (ms',s') -a (ms'',s'') 
   S,f  (ms,s) =as@[a] (ms'',s'')"


lemma observable_move_equal_length:
  assumes "S,f  (ms,s) -a (ms',s')" 
  shows "length ms = length s" and "length ms' = length s'"
proof -
  from S,f  (ms,s) -a (ms',s')
  have "length ms = length s  length ms' = length s'"
  proof(induct rule:observable_move.induct)
    case (observable_move_intra f a s s' ms S ms')
    from pred (f a) s obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
    from length ms = length s ms' = targetnode a # tl ms
      length s' = length s show ?case by simp
  next
    case (observable_move_call f a s s' Q r p fs a' ms S ms')
    from pred (f a) s obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
    from length ms = length s length s' = Suc (length s) 
      ms' = targetnode a # targetnode a' # tl ms show ?case by simp
  next
    case (observable_move_return f a s s' Q p f' ms S ms')
    from length ms = length s length s = Suc (length s') ms' = tl ms s'  []
    show ?case by simp
  qed
  thus "length ms = length s" and "length ms' = length s'" by simp_all
qed


lemma observable_moves_equal_length:
  assumes "S,f  (ms,s) =as (ms',s')" 
  shows "length ms = length s" and "length ms' = length s'"
  using S,f  (ms,s) =as (ms',s')
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') -a (ms'',s'')
  have "length ms' = length s'" "length ms'' = length s''"
    by(rule observable_move_equal_length)+
  moreover
  from S,f  (ms,s) =asτ (ms',s') 
  have "length ms = length s" and "length ms' = length s'"
    by(rule silent_moves_equal_length)+
  ultimately show "length ms = length s" "length ms'' = length s''" by simp_all
qed


lemma observable_move_notempty:
  "S,f  (ms,s) =as (ms',s'); as = []  False"
by(induct rule:observable_moves.induct,simp)


lemma silent_move_observable_moves:
  "S,f  (ms'',s'') =as (ms',s'); S,f  (ms,s) -aτ (ms'',s'')
   S,f  (ms,s) =a#as (ms',s')"
proof(induct rule:observable_moves.induct)
  case (observable_moves_snoc S f msx sx as ms' s' a' ms'' s'')
  from S,f  (ms,s) -aτ (msx,sx) S,f  (msx,sx) =asτ (ms',s')
  have "S,f  (ms,s) =a#asτ (ms',s')" by(fastforce intro:silent_moves_Cons)
  with S,f  (ms',s') -a' (ms'',s'')
  have "S,f  (ms,s) =(a#as)@[a'] (ms'',s'')"
    by(fastforce intro:observable_moves.observable_moves_snoc)
  thus ?case by simp
qed


lemma silent_append_observable_moves:
  "S,f  (ms,s) =asτ (ms'',s''); S,f  (ms'',s'') =as' (ms',s')
   S,f  (ms,s) =as@as' (ms',s')"
by(induct rule:silent_moves.induct)(auto elim:silent_move_observable_moves)


lemma observable_moves_preds_transfers:
  assumes "S,f  (ms,s) =as (ms',s')"
  shows "preds (map f as) s" and "transfers (map f as) s = s'"
proof -
  from S,f  (ms,s) =as (ms',s')
  have "preds (map f as) s  transfers (map f as) s = s'"
  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') 
    have "preds (map f as) s" and "transfers (map f as) s = s'"
      by(rule silent_moves_preds_transfers)+
    from S,f  (ms',s') -a (ms'',s'')
    have "pred (f a) s'" and "transfer (f a) s' = s''" 
      by(auto elim:observable_move.cases)
    with preds (map f as) s transfers (map f as) s = s'
    show ?case by(simp add:preds_split transfers_split)
  qed
  thus "preds (map f as) s" and "transfers (map f as) s = s'" by simp_all
qed


lemma observable_move_vpa_path:
  "S,f  (m#ms,s) -a (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  valid_path_aux cs [a]"
proof(induct S f "m#ms" s a "m'#ms'" s' rule:observable_move.induct)
  case (observable_move_return f a sx sx' Q p f' nc)
  from length (m # ms) = length sx length sx = Suc (length sx') 
    sx'  []
  obtain x xs where "ms = x#xs" by(cases ms) auto
  with ms = targetnodes rs obtain r' rs' where "rs = r'#rs'" 
    and "x = targetnode r'"     and "xs = targetnodes rs'" 
    by(auto simp:targetnodes_def)
  with 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 ms = x#xs hd (tl (m # ms)) = targetnode a
  have "x = targetnode a" by simp
  from valid_edge a kind a = Q↩⇘pf'
  have "method_exit (sourcenode a)" by(fastforce simp:method_exit_def)
  from valid_return_list rs m hd (m # ms) = sourcenode a 
    rs = r'#rs'
  have "get_proc (sourcenode a) = get_proc (sourcenode r') 
    method_exit (sourcenode r')  valid_edge r'"
    apply(clarsimp simp:valid_return_list_def method_exit_def)
    apply(erule_tac x="[]" in allE) 
    by(auto dest:get_proc_return)
  hence "get_proc (sourcenode a) = get_proc (sourcenode r')"
    and "method_exit (sourcenode r')" and "valid_edge r'" by simp_all
  with method_exit (sourcenode a) have "sourcenode r' = sourcenode a"
    by(fastforce intro:method_exit_unique)
  with valid_edge a valid_edge r' x = targetnode r' x = targetnode a
  have "r' = a" by(fastforce intro:edge_det)
  with r'  get_return_edges c' cs = c'#cs' kind a = Q↩⇘pf'
  show ?case by simp
qed(auto simp:intra_kind_def)
  


subsection ‹Relevant variables›

inductive_set relevant_vars ::
  "'node SDG_node set  'node SDG_node  'var set" ("rv _")
for S :: "'node SDG_node set" and n :: "'node SDG_node"

where rvI:
  "parent_node n -asι* parent_node n'; n'  HRB_slice S; V  UseSDG n';
    n''. valid_SDG_node n''  parent_node n''  set (sourcenodes as) 
           V  DefSDG n''
   V  rv S n"


lemma rvE:
  assumes rv:"V  rv S n"
  obtains as n' where "parent_node n -asι* parent_node n'"
  and "n'  HRB_slice S" and "V  UseSDG n'"
  and "n''. valid_SDG_node n''  parent_node n''  set (sourcenodes as) 
     V  DefSDG n''"
using rv
by(atomize_elim,auto elim!:relevant_vars.cases)


lemma rv_parent_node:
  "parent_node n = parent_node n'  rv (S::'node SDG_node set) n = rv S n'"
by(fastforce elim:rvE intro:rvI)


lemma obs_intra_empty_rv_empty:
  assumes "obs_intra m HRB_slice SCFG = {}" shows "rv S (CFG_node m) = {}"
proof(rule ccontr)
  assume "rv S (CFG_node m)  {}"
  then obtain x where "x  rv S (CFG_node m)" by fastforce
  then obtain n' as where "m -asι* parent_node n'" and "n'  HRB_slice S"
    by(fastforce elim:rvE)
  hence "parent_node n'  HRB_slice SCFG"
    by(fastforce intro:valid_SDG_node_in_slice_parent_node_in_slice 
                 simp:SDG_to_CFG_set_def)
  with m -asι* parent_node n' obtain mx where "mx  obs_intra m HRB_slice SCFG"
    by(erule path_ex_obs_intra)
  with obs_intra m HRB_slice SCFG = {} show False by simp
qed


lemma eq_obs_intra_in_rv:
  assumes obs_eq:"obs_intra (parent_node n) HRB_slice SCFG = 
                  obs_intra (parent_node n') HRB_slice SCFG"
  and "x  rv S n" shows "x  rv S n'"
proof -
  from x  rv S n obtain as n''
    where "parent_node n -asι* parent_node n''" and "n''  HRB_slice S" 
    and "x  UseSDG n''" 
    and "n''. valid_SDG_node n''  parent_node n''  set (sourcenodes as) 
       x  DefSDG n''"
    by(erule rvE)
  from parent_node n -asι* parent_node n'' have "valid_node (parent_node n'')"
    by(fastforce dest:path_valid_node simp:intra_path_def)
  from parent_node n -asι* parent_node n'' n''  HRB_slice S
  have "nx as' as''. parent_node nx  obs_intra (parent_node n) HRB_slice SCFG  
                      parent_node n -as'ι* parent_node nx 
                      parent_node nx -as''ι* parent_node n''  as = as'@as''"
  proof(cases "nx. parent_node nx  set (sourcenodes as)  nx  HRB_slice S")
    case True
    with parent_node n -asι* parent_node n'' n''  HRB_slice S
    have "parent_node n''  obs_intra (parent_node n) HRB_slice SCFG"
      by(fastforce intro:obs_intra_elem valid_SDG_node_in_slice_parent_node_in_slice 
                   simp:SDG_to_CFG_set_def)
    with parent_node n -asι* parent_node n'' valid_node (parent_node n'')
    show ?thesis by(fastforce intro:empty_path simp:intra_path_def)
  next
    case False
    hence "nx. parent_node nx  set (sourcenodes as)  nx  HRB_slice S" by simp
    hence "mx  set (sourcenodes as). nx. mx = parent_node nx  nx  HRB_slice S"
      by fastforce
    then obtain mx ms ms' where "sourcenodes as = ms@mx#ms'"
      and "nx. mx = parent_node nx  nx  HRB_slice S"
      and all:"x  set ms. ¬ (nx. x = parent_node nx  nx  HRB_slice S)"
      by(fastforce elim!:split_list_first_propE)
    then obtain nx' where "mx = parent_node nx'" and "nx'  HRB_slice S" by blast
    from sourcenodes as = ms@mx#ms'
    obtain as' a' as'' where "ms = sourcenodes as'"
      and [simp]:"as = as'@a'#as''" and "sourcenode a' = mx"
      by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
    from all ms = sourcenodes as' 
    have "nxset (sourcenodes as'). nx  HRB_slice SCFG"
      by(fastforce simp:SDG_to_CFG_set_def)
    from parent_node n -asι* parent_node n'' sourcenode a' = mx
    have "parent_node n  -as'ι* mx" and "valid_edge a'" and "intra_kind(kind a')"
      and "targetnode a' -as''ι* parent_node n''"
      by(fastforce dest:path_split simp:intra_path_def)+
    with sourcenode a' = mx have "mx -a'#as''ι* parent_node n''"
      by(fastforce intro:Cons_path simp:intra_path_def)
    from parent_node n -as'ι* mx mx = parent_node nx' nx'  HRB_slice S
      nxset (sourcenodes as'). nx  HRB_slice SCFG ms = sourcenodes as'
    have "mx  obs_intra (parent_node n) HRB_slice SCFG"
      by(fastforce intro:obs_intra_elem valid_SDG_node_in_slice_parent_node_in_slice
                   simp:SDG_to_CFG_set_def)
    with parent_node n -as'ι* mx mx -a'#as''ι* parent_node n''
      mx = parent_node nx'
    show ?thesis by simp blast
  qed
  then obtain nx as' as'' 
    where "parent_node nx  obs_intra (parent_node n) HRB_slice SCFG"
    and "parent_node n -as'ι* parent_node nx" 
    and "parent_node nx -as''ι* parent_node n''" and [simp]:"as = as'@as''"
    by blast
  from parent_node nx  obs_intra (parent_node n) HRB_slice SCFG obs_eq
  have "parent_node nx  obs_intra (parent_node n') HRB_slice SCFG" by auto
  then obtain asx where "parent_node n' -asxι* parent_node nx" 
    and "ni  set(sourcenodes asx). ni  HRB_slice SCFG" 
    and "parent_node nx  HRB_slice SCFG"
    by(erule obs_intraE)
  from n''. valid_SDG_node n''  parent_node n''  set (sourcenodes as) 
     x  DefSDG n''
  have "ni. valid_SDG_node ni  parent_node ni  set (sourcenodes as'') 
     x  DefSDG ni"
    by(auto simp:sourcenodes_def)
  from ni  set(sourcenodes asx). ni  HRB_slice SCFG
    parent_node n' -asxι* parent_node nx
  have "ni. valid_SDG_node ni  parent_node ni  set (sourcenodes asx) 
     x  DefSDG ni"
  proof(induct asx arbitrary:n')
    case Nil thus ?case by(simp add:sourcenodes_def)
  next
    case (Cons ax' asx')
    note IH = n'. niset (sourcenodes asx'). ni  HRB_slice SCFG;
      parent_node n' -asx'ι* parent_node nx
       ni. valid_SDG_node ni  parent_node ni  set (sourcenodes asx') 
               x  DefSDG ni
    from parent_node n' -ax'#asx'ι* parent_node nx
    have "parent_node n' -[]@ax'#asx'→* parent_node nx" 
      and "a  set (ax'#asx'). intra_kind(kind a)" by(simp_all add:intra_path_def)
    hence "targetnode ax' -asx'→* parent_node nx" and "valid_edge ax'"
      and "parent_node n' = sourcenode ax'" by(fastforce dest:path_split)+
    with a  set (ax'#asx'). intra_kind(kind a)
    have path:"parent_node (CFG_node (targetnode ax')) -asx'ι* parent_node nx"
      by(simp add:intra_path_def)
    from niset (sourcenodes (ax'#asx')). ni  HRB_slice SCFG
    have all:"niset (sourcenodes asx'). ni  HRB_slice SCFG"
      and "sourcenode ax'  HRB_slice SCFG"
      by(auto simp:sourcenodes_def)
    from IH[OF all path] 
    have "ni. valid_SDG_node ni  parent_node ni  set (sourcenodes asx') 
                x  DefSDG ni" .
    with ni. valid_SDG_node ni  parent_node ni  set (sourcenodes as'') 
                x  DefSDG ni
    have all:"ni. valid_SDG_node ni  parent_node ni  set (sourcenodes (asx'@as'')) 
                    x  DefSDG ni"
      by(auto simp:sourcenodes_def)
    from parent_node n' -ax'#asx'ι* parent_node nx 
      parent_node nx -as''ι* parent_node n''
    have path:"parent_node n' -ax'#asx'@as''ι* parent_node n''"
      by(fastforce intro:path_Append[of _ "ax'#asx'",simplified] simp:intra_path_def)
    have "nx'. parent_node nx' = sourcenode ax'  x  DefSDG nx'"
    proof
      fix nx' 
      show "parent_node nx' = sourcenode ax'  x  DefSDG nx'"
      proof
        assume "parent_node nx' = sourcenode ax'"
        show "x  DefSDG nx'"
        proof
          assume "x  DefSDG nx'"
          from parent_node n' = sourcenode ax' parent_node nx' = sourcenode ax'
          have "parent_node nx' = parent_node n'" by simp
          with x  DefSDG nx' x  UseSDG n'' all path
          have "nx' influences x in n''" by(fastforce simp:data_dependence_def)
          hence "nx' s-xdd n''" by(rule sum_SDG_ddep_edge)
          with n''  HRB_slice S have "nx'  HRB_slice S"
            by(fastforce elim:combine_SDG_slices.cases 
                       intro:combine_SDG_slices.intros ddep_slice1 ddep_slice2 
                        simp:HRB_slice_def)
          hence "CFG_node (parent_node nx')  HRB_slice S"
            by(rule valid_SDG_node_in_slice_parent_node_in_slice)
          with sourcenode ax'  HRB_slice SCFG parent_node n' = sourcenode ax'
            parent_node nx' = sourcenode ax' show False 
            by(simp add:SDG_to_CFG_set_def)
        qed
      qed
    qed
    with all show ?case by(auto simp add:sourcenodes_def)
  qed
  with ni. valid_SDG_node ni  parent_node ni  set (sourcenodes as'') 
              x  DefSDG ni
  have all:"ni. valid_SDG_node ni  parent_node ni  set (sourcenodes (asx@as'')) 
                  x  DefSDG ni"
    by(auto simp:sourcenodes_def)
  with parent_node n' -asxι* parent_node nx 
    parent_node nx -as''ι* parent_node n''
  have "parent_node n' -asx@as''ι* parent_node n''"
    by(fastforce intro:path_Append simp:intra_path_def)
  from this n''  HRB_slice S x  UseSDG n'' all
  show "x  rv S n'" by(rule rvI)
qed


lemma closed_eq_obs_eq_rvs:
  fixes S :: "'node SDG_node set"
  assumes obs_eq:"obs_intra (parent_node n) HRB_slice SCFG = 
  obs_intra (parent_node n') HRB_slice SCFG"
  shows "rv S n = rv S n'"
proof
  show "rv S n  rv S n'"
  proof
    fix x assume "x  rv S n"
    with obs_eq show "x  rv S n'" by(rule eq_obs_intra_in_rv)
  qed
next
  show "rv S n'  rv S n"
  proof
    fix x assume "x  rv S n'"
    with obs_eq[THEN sym] show "x  rv S n" by(rule eq_obs_intra_in_rv)
  qed
qed



lemma closed_eq_obs_eq_rvs':
  fixes S :: "'node SDG_node set"
  assumes obs_eq:"obs_intra m HRB_slice SCFG = obs_intra m' HRB_slice SCFG"
  shows "rv S (CFG_node m) = rv S (CFG_node m')"
proof
  show "rv S (CFG_node m)  rv S (CFG_node m')"
  proof
    fix x assume "x  rv S (CFG_node m)"
    with obs_eq show "x  rv S (CFG_node m')" 
      by -(rule eq_obs_intra_in_rv,auto)
  qed
next
  show "rv S (CFG_node m')  rv S (CFG_node m)"
  proof
    fix x assume "x  rv S (CFG_node m')"
    with obs_eq[THEN sym] show "x  rv S (CFG_node m)" 
      by -(rule eq_obs_intra_in_rv,auto)
  qed
qed


lemma rv_branching_edges_slice_kinds_False:
  assumes "valid_edge a" and "valid_edge ax" 
  and "sourcenode a = sourcenode ax" and "targetnode a  targetnode ax"
  and "intra_kind (kind a)" and "intra_kind (kind ax)"
  and "preds (slice_kinds S (a#as)) s" 
  and "preds (slice_kinds S (ax#asx)) s'"
  and "length s = length s'" and "snd (hd s) = snd (hd s')"
  and "Vrv S (CFG_node (sourcenode a)). state_val s V = state_val s' V"
  shows False
proof -
  from valid_edge a valid_edge ax sourcenode a = sourcenode ax 
    targetnode a  targetnode ax intra_kind (kind a) intra_kind (kind ax)
  obtain Q Q' where "kind a = (Q)" and "kind ax = (Q')"
    and "s. (Q s  ¬ Q' s)  (Q' s  ¬ Q s)"
    by(auto dest:deterministic)
  from valid_edge a valid_edge ax sourcenode a = sourcenode ax 
    targetnode a  targetnode ax intra_kind (kind a) intra_kind (kind ax)
  obtain P P' where "slice_kind S a = (P)" 
    and "slice_kind S ax = (P')"
    and "s. (P s  ¬ P' s)  (P' s  ¬ P s)"
    by -(erule slice_deterministic,auto)
  show ?thesis
  proof(cases "sourcenode a  HRB_slice SCFG")
    case True
    with intra_kind (kind a)
    have "slice_kind S a = kind a" by -(rule slice_intra_kind_in_slice)
    with preds (slice_kinds S (a#as)) s kind a = (Q) 
      slice_kind S a = (P) have "pred (kind a) s"
      by(simp add:slice_kinds_def)
    from True sourcenode a = sourcenode ax intra_kind (kind ax)
    have "slice_kind S ax = kind ax" 
      by(fastforce intro:slice_intra_kind_in_slice)
    with preds (slice_kinds S (ax#asx)) s' kind ax = (Q')
      slice_kind S ax = (P') have "pred (kind ax) s'" 
      by(simp add:slice_kinds_def)
    with kind ax = (Q') have "Q' (fst (hd s'))" by(cases s') auto
    from valid_edge a have "sourcenode a -[]ι* sourcenode a"
      by(fastforce intro:empty_path simp:intra_path_def)
    with True valid_edge a
    have "V  Use (sourcenode a). V  rv S (CFG_node (sourcenode a))"
      by(auto intro!:rvI CFG_Use_SDG_Use simp:sourcenodes_def SDG_to_CFG_set_def)
    with Vrv S (CFG_node (sourcenode a)). state_val s V = state_val s' V
    have "V  Use (sourcenode a). state_val s V = state_val s' V" by blast
    with valid_edge a pred (kind a) s pred (kind ax) s' length s = length s'
      snd (hd s) = snd (hd s')
    have "pred (kind a) s'" by(auto intro:CFG_edge_Uses_pred_equal)
    with kind a = (Q) have "Q (fst (hd s'))" by(cases s') auto
    with Q' (fst (hd s')) s. (Q s  ¬ Q' s)  (Q' s  ¬ Q s)
    have False by simp
    thus ?thesis by simp
  next
    case False
    with kind a = (Q) slice_kind S a = (P) valid_edge a
    have "P = (λs. False)  P = (λs. True)"
      by(fastforce elim:kind_Predicate_notin_slice_slice_kind_Predicate)
    with slice_kind S a = (P) 
      preds (slice_kinds S (a#as)) s
    have "P = (λs. True)" by(cases s)(auto simp:slice_kinds_def)
    from sourcenode a = sourcenode ax False
    have "sourcenode ax  HRB_slice SCFG" by simp
    with kind ax = (Q') slice_kind S ax = (P') valid_edge ax
    have "P' = (λs. False)  P' = (λs. True)"
      by(fastforce elim:kind_Predicate_notin_slice_slice_kind_Predicate)
    with slice_kind S ax = (P') 
      preds (slice_kinds S (ax#asx)) s'
    have "P' = (λs. True)" by(cases s')(auto simp:slice_kinds_def)
    with P = (λs. True) s. (P s  ¬ P' s)  (P' s  ¬ P s)
    have False by blast
    thus ?thesis by simp
  qed
qed


lemma rv_edge_slice_kinds:
  assumes "valid_edge a" and "intra_kind (kind a)"
  and "Vrv S (CFG_node (sourcenode a)). state_val s V = state_val s' V"
  and "preds (slice_kinds S (a#as)) s" and "preds (slice_kinds S (a#asx)) s'"
  shows "Vrv S (CFG_node (targetnode a)). 
  state_val (transfer (slice_kind S a) s) V = 
  state_val (transfer (slice_kind S a) s') V"
proof
  fix V assume "V  rv S (CFG_node (targetnode a))"
  from preds (slice_kinds S (a#as)) s
  have "s  []" by(cases s,auto simp:slice_kinds_def)
  from preds (slice_kinds S (a#asx)) s'
  have "s'  []" by(cases s',auto simp:slice_kinds_def)
  show "state_val (transfer (slice_kind S a) s) V =
    state_val (transfer (slice_kind S a) s') V"
  proof(cases "V  Def (sourcenode a)")
    case True
    show ?thesis
    proof(cases "sourcenode a  HRB_slice SCFG")
      case True
      with intra_kind (kind a) have "slice_kind S a = kind a"
        by -(rule slice_intra_kind_in_slice)
      with preds (slice_kinds S (a#as)) s have "pred (kind a) s"
        by(simp add:slice_kinds_def)
      from slice_kind S a = kind a 
        preds (slice_kinds S (a#asx)) s'
      have "pred (kind a) s'" by(simp add:slice_kinds_def)
      from valid_edge a have "sourcenode a -[]ι* sourcenode a"
        by(fastforce intro:empty_path simp:intra_path_def)
      with True valid_edge a
      have "V  Use (sourcenode a). V  rv S (CFG_node (sourcenode a))"
        by(auto intro!:rvI CFG_Use_SDG_Use simp:sourcenodes_def SDG_to_CFG_set_def)
      with Vrv S (CFG_node (sourcenode a)). state_val s V = state_val s' V
      have "V  Use (sourcenode a). state_val s V = state_val s' V" by blast
      from valid_edge a this pred (kind a) s pred (kind a) s'
        intra_kind (kind a)
      have "V  Def (sourcenode a). 
        state_val (transfer (kind a) s) V = state_val (transfer (kind a) s') V"
        by -(rule CFG_intra_edge_transfer_uses_only_Use,auto)
      with V  Def (sourcenode a) slice_kind S a = kind a
      show ?thesis by simp
    next
      case False
      from V  rv S (CFG_node (targetnode a)) 
      obtain xs nx where "targetnode a -xsι* parent_node nx"
        and "nx  HRB_slice S" and "V  UseSDG nx"
        and "n''. valid_SDG_node n''  parent_node n''  set (sourcenodes xs) 
           V  DefSDG n''" by(fastforce elim:rvE)
      from valid_edge a have "valid_node (sourcenode a)" by simp
      from valid_edge a targetnode a -xsι* parent_node nx intra_kind (kind a)
      have "sourcenode a -a#xs ι* parent_node nx"
        by(fastforce intro:path.Cons_path simp:intra_path_def)
      with V  Def (sourcenode a) V  UseSDG nx valid_node (sourcenode a)
        n''. valid_SDG_node n''  parent_node n''  set (sourcenodes xs) 
         V  DefSDG n''
      have "(CFG_node (sourcenode a)) influences V in nx"
        by(fastforce intro:CFG_Def_SDG_Def simp:data_dependence_def)
      hence "(CFG_node (sourcenode a)) s-Vdd nx" by(rule sum_SDG_ddep_edge)
      from nx  HRB_slice S (CFG_node (sourcenode a)) s-Vdd nx
      have "CFG_node (sourcenode a)  HRB_slice S"
      proof(induct rule:HRB_slice_cases)
        case (phase1 n nx')
        with (CFG_node (sourcenode a)) s-Vdd nx show ?case
          by(fastforce intro:intro:ddep_slice1 combine_SDG_slices.combSlice_refl 
                       simp:HRB_slice_def)
      next
        case (phase2 nx' n' n'' p n)
        from (CFG_node (sourcenode a)) s-Vdd n n  sum_SDG_slice2 n'
        have "CFG_node (sourcenode a)  sum_SDG_slice2 n'" by(rule ddep_slice2)
        with phase2 show ?thesis
          by(fastforce intro:combine_SDG_slices.combSlice_Return_parent_node 
                       simp:HRB_slice_def)
      qed
      with False have False by(simp add:SDG_to_CFG_set_def)
      thus ?thesis by simp
    qed
  next
    case False
    from V  rv S (CFG_node (targetnode a)) 
    obtain xs nx where "targetnode a -xsι* parent_node nx"
      and "nx  HRB_slice S" and "V  UseSDG nx"
      and all:"n''. valid_SDG_node n''  parent_node n''  set (sourcenodes xs) 
                  V  DefSDG n''" by(fastforce elim:rvE)
    from valid_edge a have "valid_node (sourcenode a)" by simp
    from valid_edge a targetnode a -xsι* parent_node nx intra_kind (kind a)
    have "sourcenode a -a#xs ι* parent_node nx"
      by(fastforce intro:path.Cons_path simp:intra_path_def)
    from False all
    have "n''. valid_SDG_node n''  parent_node n''  set (sourcenodes (a#xs)) 
                  V  DefSDG n''"
      by(fastforce dest:SDG_Def_parent_Def simp:sourcenodes_def)
    with sourcenode a -a#xs ι* parent_node nx nx  HRB_slice S
      V  UseSDG nx
    have "V  rv S (CFG_node (sourcenode a))" by(fastforce intro:rvI)
    from intra_kind (kind a) show ?thesis
    proof(cases "kind a")
      case(UpdateEdge f)
      show ?thesis
      proof(cases "sourcenode a  HRB_slice SCFG")
        case True
        with intra_kind (kind a) have "slice_kind S a = kind a"
          by(fastforce intro:slice_intra_kind_in_slice)
        from UpdateEdge s  [] have "pred (kind a) s" by(cases s) auto
        with valid_edge a V  Def (sourcenode a) intra_kind (kind a)
        have "state_val (transfer (kind a) s) V = state_val s V"
          by(fastforce intro:CFG_intra_edge_no_Def_equal)
        from UpdateEdge s'  [] have "pred (kind a) s'" by(cases s') auto
        with valid_edge a V  Def (sourcenode a) intra_kind (kind a)
        have "state_val (transfer (kind a) s') V = state_val s' V"
          by(fastforce intro:CFG_intra_edge_no_Def_equal)
        with Vrv S (CFG_node (sourcenode a)). state_val s V = state_val s' V
          state_val (transfer (kind a) s) V = state_val s V
          V  rv S (CFG_node (sourcenode a)) slice_kind S a = kind a
        show ?thesis by fastforce
      next
        case False
        with UpdateEdge have "slice_kind S a = id" 
          by -(rule slice_kind_Upd)
        with Vrv S (CFG_node (sourcenode a)). state_val s V = state_val s' V
          V  rv S (CFG_node (sourcenode a)) s  [] s'  []
        show ?thesis by(cases s,auto,cases s',auto)
      qed
    next
      case (PredicateEdge Q)
      show ?thesis
      proof(cases "sourcenode a  HRB_slice SCFG")
        case True
        with PredicateEdge intra_kind (kind a) 
        have "slice_kind S a = (Q)"
          by(simp add:slice_intra_kind_in_slice)
        with Vrv S (CFG_node (sourcenode a)). state_val s V = state_val s' V
          V  rv S (CFG_node (sourcenode a)) s  [] s'  []
        show ?thesis by(cases s,auto,cases s',auto)
      next
        case False
        with PredicateEdge valid_edge a 
        obtain Q' where "slice_kind S a = (Q')" 
          by -(erule kind_Predicate_notin_slice_slice_kind_Predicate)
        withVrv S (CFG_node (sourcenode a)). state_val s V = state_val s' V
          V  rv S (CFG_node (sourcenode a)) s  [] s'  []
        show ?thesis by(cases s,auto,cases s',auto)
      qed
    qed (auto simp:intra_kind_def)
  qed
qed



subsection ‹The weak simulation relational set WS›

inductive_set WS :: "'node SDG_node set  (('node list × (('var  'val) × 'ret) list) × 
  ('node list × (('var  'val) × 'ret) list)) set"
for S :: "'node SDG_node set"
  where WSI: "m  set ms. valid_node m; m'  set ms'. valid_node m'; 
  length ms = length s; length ms' = length s'; s  []; s'  []; ms = msx@mx#tl ms';
  get_proc mx = get_proc (hd ms'); 
  m  set (tl ms'). m'. call_of_return_node m m'  m'  HRB_slice SCFG;
  msx  []  (mx'. call_of_return_node mx mx'  mx'  HRB_slice SCFG);
  i < length ms'. snd (s!(length msx + i)) = snd (s'!i);
  m  set (tl ms). return_node m;
  i < length ms'. V  rv S (CFG_node ((mx#tl ms')!i)). 
    (fst (s!(length msx + i))) V = (fst (s'!i)) V;
  obs ms HRB_slice SCFG = obs ms' HRB_slice SCFG
   ((ms,s),(ms',s'))  WS S"


lemma WS_silent_move:
  assumes "S,kind  (ms1,s1) -aτ (ms1',s1')" and "((ms1,s1),(ms2,s2))  WS S"
  shows "((ms1',s1'),(ms2,s2))  WS S"
proof -
  from ((ms1,s1),(ms2,s2))  WS S obtain msx mx
    where WSE:"m  set ms1. valid_node m" "m  set ms2. valid_node m"
    "length ms1 = length s1" "length ms2 = length s2" "s1  []" "s2  []" 
    "ms1 = msx@mx#tl ms2" "get_proc mx = get_proc (hd ms2)"
    "m  set (tl ms2). m'. call_of_return_node m m'  m'  HRB_slice SCFG"
    "msx  []  (mx'. call_of_return_node mx mx'  mx'  HRB_slice SCFG)"
    "m  set (tl ms1). return_node m"
    "i < length ms2. snd (s1!(length msx + i)) = snd (s2!i)"
    "i < length ms2. V  rv S (CFG_node ((mx#tl ms2)!i)). 
      (fst (s1!(length msx + i))) V = (fst (s2!i)) V"
    "obs ms1 HRB_slice SCFG = obs ms2 HRB_slice SCFG"
    by(fastforce elim:WS.cases)
  { assume "m  set (tl ms1'). return_node m"
    have "obs ms1' HRB_slice SCFG = obs ms2 HRB_slice SCFG"
    proof(cases "obs ms1' HRB_slice SCFG = {}")
      case True
      with S,kind  (ms1,s1) -aτ (ms1',s1') have "obs ms1 HRB_slice SCFG = {}" 
        by(rule silent_move_empty_obs_slice)
      with obs ms1 HRB_slice SCFG = obs ms2 HRB_slice SCFG
        obs ms1' HRB_slice SCFG = {}
      show ?thesis by simp
    next
      case False
      from this m  set (tl ms1'). return_node m
      obtain ms' where "obs ms1' HRB_slice SCFG = {ms'}"
        by(fastforce dest:obs_singleton_element)
      hence "ms'  obs ms1' HRB_slice SCFG" by fastforce
      from S,kind  (ms1,s1) -aτ (ms1',s1') ms'  obs ms1' HRB_slice SCFG 
        m  set (tl ms1'). return_node m
      have "ms'  obs ms1 HRB_slice SCFG" by(fastforce intro:silent_move_obs_slice)
      from this m  set (tl ms1). return_node m
      have "obs ms1 HRB_slice SCFG = {ms'}" by(rule obs_singleton_element)
      with obs ms1' HRB_slice SCFG = {ms'} 
        obs ms1 HRB_slice SCFG = obs ms2 HRB_slice SCFG
      show ?thesis by simp
    qed }
  with S,kind  (ms1,s1) -aτ (ms1',s1') WSE
  show ?thesis
  proof(induct S f"kind" ms1 s1 a ms1' s1' rule:silent_move.induct)
    case (silent_move_intra a s1 s1' ms1 S ms1')
    note obs_eq = aset (tl ms1'). return_node a 
      obs ms1' HRB_slice SCFG = obs ms2 HRB_slice SCFG
    from s1  [] s2  [] obtain cf1 cfs1 cf2 cfs2 where [simp]:"s1 = cf1#cfs1" 
    and [simp]:"s2 = cf2#cfs2" by(cases s1,auto,cases s2,fastforce+)
    from transfer (kind a) s1 = s1' intra_kind (kind a)
    obtain cf1' where [simp]:"s1' = cf1'#cfs1"
      by(cases cf1,cases "kind a",auto simp:intra_kind_def)
    from m  set ms1. valid_node m ms1' = targetnode a # tl ms1 valid_edge a
    have "m  set ms1'. valid_node m" by(cases ms1) auto
    from length ms1 = length s1 length s1' = length s1 
      ms1' = targetnode a # tl ms1
    have "length ms1' = length s1'" by(cases ms1) auto
    from m  set (tl ms1). return_node m ms1' = targetnode a # tl ms1
    have "m  set (tl ms1'). return_node m" by simp
    from obs_eq[OF this] have "obs ms1' HRB_slice SCFG = obs ms2 HRB_slice SCFG" .
    from i < length ms2. V  rv S (CFG_node ((mx#tl ms2)!i)). 
      (fst (s1!(length msx + i))) V = (fst (s2!i)) V length ms2 = length s2
    have "Vrv S (CFG_node mx). (fst (s1 ! length msx)) V = state_val s2 V"
      by(cases ms2) auto
    show ?case
    proof(cases msx)
      case Nil
      with ms1 = msx@mx#tl ms2 hd ms1 = sourcenode a 
      have [simp]:"mx = sourcenode a" and [simp]:"tl ms1 = tl ms2" by simp_all
      from mset (tl ms2). m'. call_of_return_node m m'  m'  HRB_slice SCFG
        (mset (tl ms1). m'. call_of_return_node m m'  m'  HRB_slice SCFG) 
        hd ms1  HRB_slice SCFG
      have "hd ms1  HRB_slice SCFG" by fastforce
      with hd ms1 = sourcenode a have "sourcenode a  HRB_slice SCFG" by simp
      from ms1' = targetnode a # tl ms1 have "ms1' = [] @ targetnode a # tl ms2"
        by simp
      from valid_edge a intra_kind(kind a) 
      have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
      with get_proc mx = get_proc (hd ms2) 
      have "get_proc (targetnode a) = get_proc (hd ms2)" by simp
      from transfer (kind a) s1 = s1' intra_kind (kind a)
      have "snd cf1' = snd cf1" by(auto simp:intra_kind_def)
      with i<length ms2. snd (s1 ! (length msx + i)) = snd (s2 ! i) Nil
      have "i<length ms2. snd (s1' ! i) = snd (s2 ! i)"
        by auto(case_tac i,auto)
      have "V  rv S (CFG_node (targetnode a)). fst cf1' V = fst cf2 V"
      proof
        fix V assume "V  rv S (CFG_node (targetnode a))"
        from valid_edge a intra_kind (kind a) sourcenode a  HRB_slice SCFG
        have "obs_intra (targetnode a) HRB_slice SCFG = 
          obs_intra (sourcenode a) HRB_slice SCFG"
          by(rule edge_obs_intra_slice_eq)
        hence "rv S (CFG_node (targetnode a)) = rv S (CFG_node (sourcenode a))" 
          by(rule closed_eq_obs_eq_rvs')
        with V  rv S (CFG_node (targetnode a))
        have "V  rv S (CFG_node (sourcenode a))" by simp
        then obtain as n' where "sourcenode a -asι* parent_node n'" 
          and "n'  HRB_slice S" and "V  UseSDG n'"
          and "n''. valid_SDG_node n''  parent_node n''  set (sourcenodes as) 
                      V  DefSDG n''"
          by(fastforce elim:rvE)
        with sourcenode a  HRB_slice SCFG valid_edge a
        have "V  DefSDG (CFG_node (sourcenode a))"
          apply(clarsimp simp:intra_path_def)
          apply(erule path.cases)
          by(auto dest:valid_SDG_node_in_slice_parent_node_in_slice 
                  simp:sourcenodes_def SDG_to_CFG_set_def)
        from valid_edge a have "valid_node (sourcenode a)" by simp
        with V  DefSDG (CFG_node (sourcenode a)) have "V  Def (sourcenode a)"
          by(fastforce intro:CFG_Def_SDG_Def valid_SDG_CFG_node)
        with valid_edge a intra_kind (kind a) pred (kind a) s1
        have "state_val (transfer (kind a) s1) V = state_val s1 V"
          by(fastforce intro:CFG_intra_edge_no_Def_equal)
        with transfer (kind a) s1 = s1' have "fst cf1' V = fst cf1 V" by simp
        from V  rv S (CFG_node (sourcenode a)) msx = []
          Vrv S (CFG_node mx). (fst (s1 ! length msx)) V = state_val s2 V
        have "fst cf1 V = fst cf2 V" by simp
        with fst cf1' V = fst cf1 V show "fst cf1' V = fst cf2 V" by simp
      qed
      with i<length ms2. Vrv S (CFG_node ((mx # tl ms2) ! i)).
        (fst (s1 ! (length msx + i))) V = (fst (s2 ! i)) V Nil
      have "i<length ms2. Vrv S (CFG_node ((targetnode a # tl ms2) ! i)).
        (fst (s1' ! (length [] + i))) V = (fst (s2 ! i)) V"
        by auto (case_tac i,auto)
      with m  set ms1'. valid_node m m  set ms2. valid_node m
        length ms1' = length s1' length ms2 = length s2
        ms1' = [] @ targetnode a # tl ms2 
        get_proc (targetnode a) = get_proc (hd ms2)
        m  set (tl ms2). m'. call_of_return_node m m'  m'  HRB_slice SCFG
        m  set (tl ms1). return_node m
        obs ms1' HRB_slice SCFG = obs ms2 HRB_slice SCFG
        i<length ms2. snd (s1' ! i) = snd (s2 ! i)
      show ?thesis by(auto intro!:WSI)
    next
      case (Cons mx' msx')
      with ms1 = msx@mx#tl ms2 hd ms1 = sourcenode a
      have [simp]:"mx' = sourcenode a" and [simp]:"tl ms1 = msx'@mx#tl ms2" 
        by simp_all
     from ms1' = targetnode a # tl ms1 have "ms1' = ((targetnode a)#msx')@mx#tl ms2"
        by simp
      from Vrv S (CFG_node mx). (fst (s1 ! length msx)) V = state_val s2 V Cons
      have rv:"Vrv S (CFG_node mx).
        (fst (s1' ! length (targetnode a#msx'))) V = state_val s2 V" by fastforce
      from ms1 = msx@mx#tl ms2 Cons ms1' = targetnode a # tl ms1
      have "ms1' = ((targetnode a)#msx')@mx#tl ms2" by simp
      from i<length ms2. snd (s1 ! (length msx + i)) = snd (s2 ! i) Cons
      have "i<length ms2. snd (s1' ! (length msx + i)) = snd (s2 ! i)" by fastforce 
      from Vrv S (CFG_node mx). (fst (s1 ! length msx)) V = state_val s2 V Cons
      have "Vrv S (CFG_node mx). (fst (s1' ! length msx)) V = state_val s2 V"
        by simp
      with i < length ms2. V  rv S (CFG_node ((mx#tl ms2)!i)). 
        (fst (s1!(length msx + i))) V = (fst (s2!i)) V Cons
      have "i<length ms2. Vrv S (CFG_node ((mx # tl ms2)!i)).
             (fst (s1'!(length (targetnode a # msx') + i))) V = (fst (s2!i)) V"
        by clarsimp
      with mset ms1'. valid_node m mset ms2. valid_node m
        length ms1' = length s1' length ms2 = length s2 
        ms1' = ((targetnode a)#msx')@mx#tl ms2
        mset (tl ms2). m'. call_of_return_node m m'  m'  HRB_slice SCFG
        m  set (tl ms1'). return_node m get_proc mx = get_proc (hd ms2)
        msx  []  (mx'. call_of_return_node mx mx'  mx'  HRB_slice SCFG)
        obs ms1' HRB_slice SCFG = obs ms2 HRB_slice SCFG Cons
        i<length ms2. snd (s1' ! (length msx + i)) = snd (s2 ! i)
      show ?thesis by -(rule WSI,clarsimp+,fastforce,clarsimp+)
    qed
  next
    case (silent_move_call a s1 s1' Q r p fs a' ms1 S ms1')
    note obs_eq = aset (tl ms1'). return_node a 
      obs ms1' HRB_slice SCFG = obs ms2 HRB_slice SCFG
    from s1  [] s2  [] obtain cf1 cfs1 cf2 cfs2 where [simp]:"s1 = cf1#cfs1" 
      and [simp]:"s2 = cf2#cfs2" by(cases s1,auto,cases s2,fastforce+)
    from valid_edge a kind a = Q:r↪⇘pfs 
    obtain ins outs where "(p,ins,outs)  set procs"
      by(fastforce dest!:callee_in_procs)
    with transfer (kind a) s1 = s1' valid_edge a kind a = Q:r↪⇘pfs
    have [simp]:"s1' = (Map.empty(ins [:=] params fs (fst cf1)), r) # cf1 # cfs1"
      by simp(unfold formal_in_THE,simp)
    from length ms1 = length s1 ms1' = targetnode a # targetnode a' # tl ms1
    have "length ms1' = length s1'" by simp
    from valid_edge a a'  get_return_edges a have "valid_edge a'"
      by(rule get_return_edges_valid)
    with mset ms1. valid_node m valid_edge a 
      ms1' = targetnode a # targetnode a' # tl ms1
    have "mset ms1'. valid_node m" by(cases ms1) auto
    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 a'  get_return_edges a valid_edge a'
    have "call_of_return_node (targetnode a') (sourcenode a)"
      by(simp add:call_of_return_node_def) blast
    from m  set (tl ms1). return_node m return_node (targetnode a')
      ms1' = targetnode a # targetnode a' # tl ms1
    have "m  set (tl ms1'). return_node m" by simp
    from obs_eq[OF this] have "obs ms1' HRB_slice SCFG = obs ms2 HRB_slice SCFG" .
    from i < length ms2. V  rv S (CFG_node ((mx#tl ms2)!i)). 
      (fst (s1!(length msx + i))) V = (fst (s2!i)) V length ms2 = length s2
    have "Vrv S (CFG_node mx). (fst (s1 ! length msx)) V = state_val s2 V"
      by(erule_tac x="0" in allE) auto
    show ?case
    proof(cases msx)
      case Nil
      with ms1 = msx@mx#tl ms2 hd ms1 = sourcenode a 
      have [simp]:"mx = sourcenode a" and [simp]:"tl ms1 = tl ms2" by simp_all
      from mset (tl ms2). m'. call_of_return_node m m'  m'  HRB_slice SCFG
        (mset (tl ms1). m'. call_of_return_node m m'  m'  HRB_slice SCFG) 
        hd ms1  HRB_slice SCFG
      have "hd ms1  HRB_slice SCFG" by fastforce
      with hd ms1 = sourcenode a have "sourcenode a  HRB_slice SCFG" by simp
      from valid_edge a a'  get_return_edges a
      obtain a'' where "valid_edge a''" and "sourcenode a'' = sourcenode a"
        and "targetnode a'' = targetnode a'" and "intra_kind(kind a'')"
        by -(drule call_return_node_edge,auto 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)
      with sourcenode a'' = sourcenode a targetnode a'' = targetnode a'
        get_proc mx = get_proc (hd ms2) 
      have "get_proc (targetnode a') = get_proc (hd ms2)" by simp
      from valid_edge a kind a = Q:r↪⇘pfs a'  get_return_edges a
      have "CFG_node (sourcenode a) s-psum CFG_node (targetnode a')"
        by(fastforce intro:sum_SDG_call_summary_edge)
      have "targetnode a'  HRB_slice SCFG"
      proof
        assume "targetnode a'  HRB_slice SCFG"
        hence "CFG_node (targetnode a')  HRB_slice S" by(simp add:SDG_to_CFG_set_def)
        hence "CFG_node (sourcenode a)  HRB_slice S"
        proof(induct "CFG_node (targetnode a')" rule:HRB_slice_cases)
          case (phase1 nx)
          with CFG_node (sourcenode a) s-psum CFG_node (targetnode a')
          show ?case by(fastforce intro:combine_SDG_slices.combSlice_refl sum_slice1
                                  simp:HRB_slice_def)
        next
          case (phase2 nx n' n'' p')
          from CFG_node (targetnode a')  sum_SDG_slice2 n' 
            CFG_node (sourcenode a) s-psum CFG_node (targetnode a') valid_edge a
          have "CFG_node (sourcenode a)  sum_SDG_slice2 n'"
            by(fastforce intro:sum_slice2)
          with n'  sum_SDG_slice1 nx n'' s-p'ret CFG_node (parent_node n') 
            nx  S
          show ?case
            by(fastforce intro:combine_SDG_slices.combSlice_Return_parent_node 
                         simp:HRB_slice_def)
        qed
        with sourcenode a  HRB_slice SCFG show False
          by(simp add:SDG_to_CFG_set_def HRB_slice_def)
      qed
      from ms1' = targetnode a # targetnode a' # tl ms1
      have "ms1' = [targetnode a] @ targetnode a' # tl ms2" by simp
      from i<length ms2. snd (s1 ! (length msx + i)) = snd (s2 ! i) Nil
      have "i<length ms2. snd (s1' ! (length [targetnode a] + i)) = snd (s2 ! i)"
        by fastforce
      have "Vrv S (CFG_node (targetnode a')). (fst (s1' ! 1)) V = state_val s2 V"
      proof
        fix V assume "V  rv S (CFG_node (targetnode a'))"
        from valid_edge a a'  get_return_edges a
        obtain a'' where edge:"valid_edge a''" "sourcenode a'' = sourcenode a"
          "targetnode a'' = targetnode a'" "intra_kind(kind a'')"
          by -(drule call_return_node_edge,auto simp:intra_kind_def)
        from V  rv S (CFG_node (targetnode a'))
        obtain as n' where "targetnode a' -asι* parent_node n'"
          and "n'  HRB_slice S" and "V  UseSDG n'"
          and "n''. valid_SDG_node n''  parent_node n''  set (sourcenodes as) 
           V  DefSDG n''"
          by(fastforce elim:rvE)
        from targetnode a' -asι* parent_node n' edge
        have "sourcenode a -a''#asι* parent_node n'"
          by(fastforce intro:Cons_path simp:intra_path_def)
        from valid_edge a kind a = Q:r↪⇘pfs
        have "V  Def (sourcenode a)"
          by(fastforce dest:call_source_Def_empty)
        with n''. valid_SDG_node n''  parent_node n''  set (sourcenodes as) 
           V  DefSDG n'' sourcenode a'' = sourcenode a
        have "n''. valid_SDG_node n''  parent_node n''  set (sourcenodes (a''#as)) 
           V  DefSDG n''"
          by(fastforce dest:SDG_Def_parent_Def simp:sourcenodes_def)
        with sourcenode a -a''#asι* parent_node n' n'  HRB_slice S 
          V  UseSDG n'
        have "V  rv S (CFG_node (sourcenode a))" by(fastforce intro:rvI)
        from Vrv S (CFG_node mx). (fst (s1 ! length msx)) V = state_val s2 V Nil
        have "Vrv S (CFG_node (sourcenode a)). fst cf1 V = fst cf2 V" by simp
        with V  rv S (CFG_node (sourcenode a)) have "fst cf1 V = fst cf2 V" by simp
        thus "(fst (s1' ! 1)) V = state_val s2 V" by simp
      qed
      with i < length ms2. V  rv S (CFG_node ((mx#tl ms2)!i)). 
        (fst (s1!(length msx + i))) V = (fst (s2!i)) V Nil
      have "i<length ms2. Vrv S (CFG_node ((targetnode a' # tl ms2)!i)).
        (fst (s1'!(length [targetnode a] + i))) V = (fst (s2!i)) V"
        by clarsimp(case_tac i,auto)
      with mset ms1'. valid_node m mset ms2. valid_node m
        length ms1' = length s1' length ms2 = length s2
        mset (tl ms2). m'. call_of_return_node m m'  m'  HRB_slice SCFG
        ms1' = [targetnode a] @ targetnode a' # tl ms2
        targetnode a'  HRB_slice SCFG return_node (targetnode a')
        obs ms1' HRB_slice SCFG = obs ms2 HRB_slice SCFG
        get_proc (targetnode a') = get_proc (hd ms2)
        m  set (tl ms1'). return_node m sourcenode a  HRB_slice SCFG
        call_of_return_node (targetnode a') (sourcenode a)
        i<length ms2. snd (s1' ! (length [targetnode a] + i)) = snd (s2 ! i)
      show ?thesis by(auto intro!:WSI)
    next
      case (Cons mx' msx')
      with ms1 = msx@mx#tl ms2 hd ms1 = sourcenode a
      have [simp]:"mx' = sourcenode a" and [simp]:"tl ms1 = msx'@mx#tl ms2" 
        by simp_all
      from ms1' = targetnode a # targetnode a' # tl ms1 
      have "ms1' = (targetnode a # targetnode a' # msx')@mx#tl ms2"
        by simp
      from i<length ms2. snd (s1 ! (length msx + i)) = snd (s2 ! i) Cons
      have "i<length ms2.
        snd (s1' ! (length (targetnode a # targetnode a' # msx') + i)) = snd (s2 ! i)"
        by fastforce
      from Vrv S (CFG_node mx). (fst (s1 ! length msx)) V = state_val s2 V Cons
      have "Vrv S (CFG_node mx). 
        (fst (s1' ! length(targetnode a # targetnode a' # msx'))) V = state_val s2 V" 
        by simp
      with i < length ms2. V  rv S (CFG_node ((mx#tl ms2)!i)). 
        (fst (s1!(length msx + i))) V = (fst (s2!i)) V Cons
      have "i<length ms2. Vrv S (CFG_node ((mx # tl ms2)!i)).
        (fst (s1'!(length (targetnode a # targetnode a' # msx') + i))) V = 
        (fst (s2!i)) V"
        by clarsimp
      with mset ms1'. valid_node m mset ms2. valid_node m
        length ms1' = length s1' length ms2 = length s2 
        ms1' = (targetnode a # targetnode a' # msx')@mx#tl ms2
        return_node (targetnode a')
        mset (tl ms2). m'. call_of_return_node m m'  m'  HRB_slice SCFG
        msx  []  (mx'. call_of_return_node mx mx'  mx'  HRB_slice SCFG)
        obs ms1' HRB_slice SCFG = obs ms2 HRB_slice SCFG Cons
        get_proc mx = get_proc (hd ms2) m  set (tl ms1'). return_node m
        i<length ms2.
        snd (s1' ! (length (targetnode a # targetnode a' # msx') + i)) = snd (s2 ! i)
      show ?thesis by -(rule WSI,clarsimp+,fastforce,clarsimp+)
    qed
  next
    case (silent_move_return a s1 s1' Q p f' ms1 S ms1')
    note obs_eq = aset (tl ms1'). return_node a 
      obs ms1' HRB_slice SCFG = obs ms2 HRB_slice SCFG
    from transfer (kind a) s1 = s1' kind a = Q↩⇘pf' s1  [] s1'  []
    obtain cf1 cfx1 cfs1 cf1' where [simp]:"s1 = cf1#cfx1#cfs1"
      and "s1' = (f' (fst cf1) (fst cfx1),snd cfx1)#cfs1"
      by(cases s1,auto,case_tac list,fastforce+)
    from s2  [] obtain cf2 cfs2 where [simp]:"s2 = cf2#cfs2" by(cases s2) auto
    from length ms1 = length s1 have "ms1  []" and "tl ms1  []" by(cases ms1,auto)+
    from valid_edge a kind a = Q↩⇘pf'
    obtain a' Q' r' fs' where "valid_edge a'" and "kind a' = Q':r'↪⇘pfs'"
      and "a  get_return_edges a'"
      by -(drule return_needs_call,auto)
    then obtain ins outs where "(p,ins,outs)  set procs"
      by(fastforce dest!:callee_in_procs)
    with valid_edge a kind a = Q↩⇘pf'
    have "f' (fst cf1) (fst cfx1) = 
      (fst cfx1)(ParamDefs (targetnode a) [:=] map (fst cf1) outs)"
      by(rule CFG_return_edge_fun)
    with s1' = (f' (fst cf1) (fst cfx1),snd cfx1)#cfs1
    have [simp]:"s1' = ((fst cfx1)
      (ParamDefs (targetnode a) [:=] map (fst cf1) outs),snd cfx1)#cfs1" by simp
    from mset ms1. valid_node m ms1' = tl ms1 have "mset ms1'. valid_node m"
      by(cases ms1) auto
    from length ms1 = length s1 ms1' = tl ms1
    have "length ms1' = length s1'" by simp
    from mset (tl ms1). return_node m ms1' = tl ms1 ms1  [] tl ms1  []
    have "mset (tl ms1'). return_node m" by(cases ms1)(auto,cases ms1',auto)
    from obs_eq[OF this] have "obs ms1' HRB_slice SCFG = obs ms2 HRB_slice SCFG" .
    show ?case
    proof(cases msx)
      case Nil
      with ms1 = msx@mx#tl ms2 hd ms1 = sourcenode a 
      have "mx = sourcenode a" and "tl ms1 = tl ms2" by simp_all
      with mset (tl ms1). m'. call_of_return_node m m'  m'  HRB_slice SCFG
        mset (tl ms2). m'. call_of_return_node m m'  m'  HRB_slice SCFG
      have False by fastforce
      thus ?thesis by simp
    next
      case (Cons mx' msx')
      with ms1 = msx@mx#tl ms2 hd ms1 = sourcenode a
      have [simp]:"mx' = sourcenode a" and [simp]:"tl ms1 = msx'@mx#tl ms2"
        by simp_all
      from ms1' = tl ms1 have "ms1' = msx'@mx#tl ms2" by simp
      with ms1 = msx@mx#tl ms2 mset (tl ms1). return_node m Cons
      have "mset (tl ms1'). return_node m"
        by(cases msx') auto
      from i<length ms2. snd (s1 ! (length msx + i)) = snd (s2 ! i) Cons
      have "i<length ms2. snd (s1' ! (length msx' + i)) = snd (s2 ! i)"
        by auto(case_tac i,auto,cases msx',auto)
      from i<length ms2. Vrv S (CFG_node ((mx # tl ms2) ! i)).
        (fst (s1 ! (length msx + i))) V = (fst (s2 ! i)) V
        length ms2 = length s2 s2  []
      have "Vrv S (CFG_node mx). (fst (s1 ! length msx)) V = state_val s2 V"
        by fastforce
      have "Vrv S (CFG_node mx). (fst (s1' ! length msx')) V = state_val s2 V"
      proof(cases msx')
        case Nil
        with Vrv S (CFG_node mx). (fst (s1 ! length msx)) V = state_val s2 V
          msx = mx'#msx'
        have rv:"Vrv S (CFG_node mx). fst cfx1 V = fst cf2 V" by fastforce
        from Nil tl ms1 = msx'@mx#tl ms2 hd (tl ms1) = targetnode a
        have [simp]:"mx = targetnode a" by simp
        from Cons 
          msx  []  (mx'. call_of_return_node mx mx'  mx'  HRB_slice SCFG)
        obtain mx'' where "call_of_return_node mx mx''" and "mx''  HRB_slice SCFG"
          by blast
        hence "mx  HRB_slice SCFG" 
          by(rule call_node_notin_slice_return_node_neither)
        have "Vrv S (CFG_node mx). 
          (fst cfx1)(ParamDefs (targetnode a) [:=] map (fst cf1) outs) V = fst cf2 V"
        proof
          fix V assume "Vrv S (CFG_node mx)"
          show "(fst cfx1)(ParamDefs (targetnode a) [:=] map (fst cf1) outs) V = 
            fst cf2 V"
          proof(cases "V  set (ParamDefs (targetnode a))")
            case True
            with valid_edge a have "V  Def (targetnode a)"
              by(fastforce intro:ParamDefs_in_Def)
            with valid_edge a have "V  DefSDG (CFG_node (targetnode a))"
              by(auto intro!:CFG_Def_SDG_Def)
            from Vrv S (CFG_node mx) obtain as n' 
              where "targetnode a -asι* parent_node n'"
              and "n'  HRB_slice S" "V  UseSDG n'"
              and "n''. valid_SDG_node n''  parent_node n''  set (sourcenodes as) 
               V  DefSDG n''" by(fastforce elim:rvE)
            from targetnode a -asι* parent_node n' n'  HRB_slice S
              mx  HRB_slice SCFG
            obtain ax asx where "as = ax#asx"
              by(auto simp:intra_path_def)(erule path.cases,
                 auto dest:valid_SDG_node_in_slice_parent_node_in_slice 
                      simp:SDG_to_CFG_set_def)
            with targetnode a -asι* parent_node n' 
            have "targetnode a = sourcenode ax" and "valid_edge ax"
              by(auto elim:path.cases simp:intra_path_def)
            with n''. valid_SDG_node n''  parent_node n''  set (sourcenodes as) 
               V  DefSDG n'' as = ax#asx V  DefSDG (CFG_node (targetnode a))
            have False by(fastforce simp:sourcenodes_def)
            thus ?thesis by simp
          next
            case False
            with Vrv S (CFG_node mx) rv show ?thesis
              by(fastforce dest:fun_upds_notin[of  _ _ "fst cfx1"])
          qed
        qed
        with Nil msx = mx'#msx' show ?thesis by fastforce
      next
        case Cons
        with Vrv S (CFG_node mx). (fst (s1 ! length msx)) V = state_val s2 V
          msx = mx'#msx'
        show ?thesis by fastforce
      qed
      with Vrv S (CFG_node mx). (fst (s1 ! length msx)) V = state_val s2 V Cons
      have "Vrv S (CFG_node mx). (fst (s1' ! length msx')) V = state_val s2 V"
        by(cases msx') auto
      with i < length ms2. V  rv S (CFG_node ((mx#tl ms2)!i)). 
        (fst (s1!(length msx + i))) V = (fst (s2!i)) V Cons
      have "i<length ms2. Vrv S (CFG_node ((mx # tl ms2) ! i)).
        (fst (s1' ! (length msx' + i))) V = (fst (s2 ! i)) V"
        by clarsimp(case_tac i,auto)
      with mset ms1'. valid_node m mset ms2. valid_node m
        length ms1' = length s1' length ms2 = length s2 
        ms1' = msx'@mx#tl ms2 get_proc mx = get_proc (hd ms2)
        mset (tl ms2). m'. call_of_return_node m m'  m'  HRB_slice SCFG
        msx  []  (mx'. call_of_return_node mx mx'  mx'  HRB_slice SCFG)
        mset (tl ms1'). return_node m Cons get_proc mx = get_proc (hd ms2)
        mset (tl ms2). m'. call_of_return_node m m'  m'  HRB_slice SCFG
        obs ms1' HRB_slice SCFG = obs ms2 HRB_slice SCFG
        i<length ms2. snd (s1' ! (length msx' + i)) = snd (s2 ! i)
       show ?thesis by(auto intro!:WSI)
    qed
  qed
qed


lemma WS_silent_moves:
  "S,kind  (ms1,s1) =asτ (ms1',s1'); ((ms1,s1),(ms2,s2))  WS S
   ((ms1',s1'),(ms2,s2))  WS S"
by(induct S f"kind" ms1 s1 as ms1' s1' rule:silent_moves.induct,
  auto dest:WS_silent_move)


lemma WS_observable_move:
  assumes "((ms1,s1),(ms2,s2))  WS S"
  and "S,kind  (ms1,s1) -a (ms1',s1')" and "s1'  []"
  obtains as where "((ms1',s1'),(ms1',transfer (slice_kind S a) s2))  WS S"
  and "S,slice_kind S  (ms2,s2) =as@[a] (ms1',transfer (slice_kind S a) s2)"
proof(atomize_elim)
  from ((ms1,s1),(ms2,s2))  WS S obtain msx mx
    where assms:"m  set ms1. valid_node m" "m  set ms2. valid_node m"
    "length ms1 = length s1" "length ms2 = length s2" "s1  []" "s2  []" 
    "ms1 = msx@mx#tl ms2" "get_proc mx = get_proc (hd ms2)" 
    "m  set (tl ms2). m'. call_of_return_node m m'  m'  HRB_slice SCFG"
    "msx  []  (mx'. call_of_return_node mx mx'  mx'  HRB_slice SCFG)"
    "m  set (tl ms1). return_node m"
    "i < length ms2. snd (s1!(length msx + i)) = snd (s2!i)"
    "i < length ms2. V  rv S (CFG_node ((mx#tl ms2)!i)). 
      (fst (s1!(length msx + i))) V = (fst (s2!i)) V"
    "obs ms1 HRB_slice SCFG = obs ms2 HRB_slice SCFG"
    by(fastforce elim:WS.cases)
  from S,kind  (ms1,s1) -a (ms1',s1') assms
  show "as. ((ms1',s1'),(ms1',transfer (slice_kind S a) s2))  WS S 
    S,slice_kind S  (ms2,s2) =as @ [a] (ms1',transfer (slice_kind S a) s2)"
  proof(induct S f"kind" ms1 s1 a ms1' s1' rule:observable_move.induct)
    case (observable_move_intra a s1 s1' ms1 S ms1')
    from s1  [] s2  [] obtain cf1 cfs1 cf2 cfs2 where [simp]:"s1 = cf1#cfs1" 
      and [simp]:"s2 = cf2#cfs2" by(cases s1,auto,cases s2,fastforce+)
    from length ms1 = length s1 s1  [] have [simp]:"ms1  []" by(cases ms1) auto
    from length ms2 = length s2 s2  [] have [simp]:"ms2  []" by(cases ms2) auto
    from m  set (tl ms1). m'. call_of_return_node m m'  m'  HRB_slice SCFG
      hd ms1 = sourcenode a ms1 = msx@mx#tl ms2
      msx  []  (mx'. call_of_return_node mx mx'  mx'  HRB_slice SCFG)
    have [simp]:"mx = sourcenode a" "msx = []" and [simp]:"tl ms2 = tl ms1"
      by(cases msx,auto)+
    hence "length ms1 = length ms2" by(cases ms2) auto
    with length ms1 = length s1 length ms2 = length s2
    have "length s1 = length s2" by simp
    from hd ms1  HRB_slice SCFG hd ms1 = sourcenode a
    have "sourcenode a  HRB_slice SCFG" by simp
    with valid_edge a
    have "obs_intra (sourcenode a) HRB_slice SCFG = {sourcenode a}"
      by(fastforce intro!:n_in_obs_intra)
    from m  set (tl ms2). m'. call_of_return_node m m'  m'  HRB_slice SCFG
      obs_intra (sourcenode a) HRB_slice SCFG = {sourcenode a} 
      hd ms1 = sourcenode a 
    have "(hd ms1#tl ms1)  obs ([]@hd ms1#tl ms1) HRB_slice SCFG"
      by(cases ms1)(auto intro!:obsI)
    hence "ms1  obs ms1 HRB_slice SCFG" by simp
    with obs ms1 HRB_slice SCFG = obs ms2 HRB_slice SCFG
    have "ms1  obs ms2 HRB_slice SCFG" by simp
    from ms2  [] length ms2 = length s2 have "length s2 = length (hd ms2#tl ms2)"
      by(fastforce dest!:hd_Cons_tl)
    from m  set (tl ms1). return_node m have "m  set (tl ms2). return_node m"
      by simp
    with ms1  obs ms2 HRB_slice SCFG
    have "hd ms1  obs_intra (hd ms2) HRB_slice SCFG"
    proof(rule obsE)
      fix nsx n nsx' n'
      assume "ms2 = nsx @ n # nsx'" and "ms1 = n' # nsx'"
        and "n'  obs_intra n HRB_slice SCFG"
      from ms2 = nsx @ n # nsx' ms1 = n' # nsx' tl ms2 = tl ms1
      have [simp]:"nsx = []" by(cases nsx) auto
      with ms2 = nsx @ n # nsx' have [simp]:"n = hd ms2" by simp
      from ms1 = n' # nsx' have [simp]:"n' = hd ms1" by simp
      with n'  obs_intra n HRB_slice SCFG show ?thesis by simp
    qed
    with length s2 = length (hd ms2#tl ms2) m  set (tl ms2). return_node m
    obtain as where "S,slice_kind S  (hd ms2#tl ms2,s2) =asτ (hd ms1#tl ms1,s2)"
      by(fastforce elim:silent_moves_intra_path_obs[of _ _ _ s2 "tl ms2"])
    with ms2  [] have "S,slice_kind S  (ms2,s2) =asτ (ms1,s2)"
      by(fastforce dest!:hd_Cons_tl)
    from valid_edge a have "valid_node (sourcenode a)" by simp
    hence "sourcenode a -[]ι* sourcenode a"
      by(fastforce intro:empty_path simp:intra_path_def)
    with sourcenode a  HRB_slice SCFG
    have "V. V  UseSDG (CFG_node (sourcenode a)) 
       V  rv S (CFG_node (sourcenode a))"
      by auto(rule rvI,auto simp:SDG_to_CFG_set_def sourcenodes_def)
    with valid_node (sourcenode a)
    have "V  Use (sourcenode a). V  rv S (CFG_node (sourcenode a))"
      by(fastforce intro:CFG_Use_SDG_Use)
    from i < length ms2. V  rv S (CFG_node ((mx#tl ms2)!i)). 
      (fst (s1!(length msx + i))) V = (fst (s2!i)) V length ms2 = length s2
    have "Vrv S (CFG_node mx). (fst (s1 ! length msx)) V = state_val s2 V"
      by(cases ms2) auto
    with V  Use (sourcenode a). V  rv S (CFG_node (sourcenode a))
    have "V  Use (sourcenode a). fst cf1 V = fst cf2 V" by fastforce
    moreover
    from i<length ms2. snd (s1 ! (length msx + i)) = snd (s2 ! i)
    have "snd (hd s1) = snd (hd s2)" by(erule_tac x="0" in allE) auto
    ultimately have "pred (kind a) s2"
      using valid_edge a pred (kind a) s1 length s1 = length s2
      by(fastforce intro:CFG_edge_Uses_pred_equal)
    from ms1' = targetnode a # tl ms1 length s1' = length s1 
      length ms1 = length s1 have "length ms1' = length s1'" by simp
    from transfer (kind a) s1 = s1' intra_kind (kind a)
    obtain cf1' where [simp]:"s1' = cf1'#cfs1"
      by(cases cf1,cases "kind a",auto simp:intra_kind_def)
    from intra_kind (kind a) sourcenode a  HRB_slice SCFG pred (kind a) s2
    have "pred (slice_kind S a) s2" by(simp add:slice_intra_kind_in_slice)
    from valid_edge a length s1 = length s2 transfer (kind a) s1 = s1'
    have "length s1' = length (transfer (slice_kind S a) s2)"
      by(fastforce intro:length_transfer_kind_slice_kind)
    with length s1 = length s2
    have "length s2 = length (transfer (slice_kind S a) s2)" by simp
    with pred (slice_kind S a) s2 valid_edge a intra_kind (kind a)
      m  set (tl ms1). m'. call_of_return_node m m'  m'  HRB_slice SCFG
      hd ms1  HRB_slice SCFG hd ms1 = sourcenode a
      length ms1 = length s1 length s1 = length s2
      ms1' = targetnode a # tl ms1 m  set (tl ms2). return_node m
    have "S,slice_kind S  (ms1,s2) -a (ms1',transfer (slice_kind S a) s2)"
      by(auto intro:observable_move.observable_move_intra)
    with S,slice_kind S  (ms2,s2) =asτ (ms1,s2) 
    have "S,slice_kind S  (ms2,s2) =as@[a] (ms1',transfer (slice_kind S a) s2)"
      by(rule observable_moves_snoc)
    from m  set ms1. valid_node m ms1' = targetnode a # tl ms1 valid_edge a
    have "m  set ms1'. valid_node m" by(cases ms1) auto
    from m  set (tl ms2). return_node m ms1' = targetnode a # tl ms1
      ms1' = targetnode a # tl ms1
    have "m  set (tl ms1'). return_node m" by fastforce
    from ms1' = targetnode a # tl ms1 tl ms2 = tl ms1
    have "ms1' = [] @ targetnode a # tl ms2" by simp
    from intra_kind (kind a) sourcenode a  HRB_slice SCFG
    have cf2':"cf2'. transfer (slice_kind S a) s2 = cf2'#cfs2  snd cf2' = snd cf2"
      by(cases cf2)(auto dest:slice_intra_kind_in_slice simp:intra_kind_def)
    from transfer (kind a) s1 = s1' intra_kind (kind a)
    have "snd cf1' = snd cf1" by(auto simp:intra_kind_def)
    with i<length ms2. snd (s1 ! (length msx + i)) = snd (s2 ! i)
      snd (hd s1) = snd (hd s2) ms1' = [] @ targetnode a # tl ms2
      cf2' length ms1 = length ms2
    have "i<length ms1'. snd (s1' ! i) = snd (transfer (slice_kind S a) s2 ! i)"
      by auto(case_tac i,auto)
    have "V  rv S (CFG_node (targetnode a)). 
      fst cf1' V = state_val (transfer (slice_kind S a) s2) V" 
    proof
      fix V assume "V  rv S (CFG_node (targetnode a))"
      show "fst cf1' V = state_val (transfer (slice_kind S a) s2) V"
      proof(cases "V  Def (sourcenode a)")
        case True
        from intra_kind (kind a) have "(f. kind a = f)  (Q. kind a = (Q))" 
          by(simp add:intra_kind_def)
        thus ?thesis
        proof
          assume "f. kind a = f"
          then obtain f' where "kind a = f'" by blast
          with transfer (kind a) s1 = s1'
          have "s1' = (f' (fst cf1),snd cf1) # cfs1" by simp
          from sourcenode a  HRB_slice SCFG kind a = f'
          have "slice_kind S a = f'"
            by(fastforce dest:slice_intra_kind_in_slice simp:intra_kind_def)
          hence "transfer (slice_kind S a) s2 = (f' (fst cf2),snd cf2) # cfs2" by simp
          from valid_edge a V  Use (sourcenode a). fst cf1 V = fst cf2 V 
            intra_kind (kind a) pred (kind a) s1 pred (kind a) s2
          have "V  Def (sourcenode a). state_val (transfer (kind a) s1) V =
            state_val (transfer (kind a) s2) V"
            by -(erule CFG_intra_edge_transfer_uses_only_Use,auto)
          with kind a = f' s1' = (f' (fst cf1),snd cf1) # cfs1 True
            transfer (slice_kind S a) s2 = (f' (fst cf2),snd cf2) # cfs2
          show ?thesis by simp
        next
          assume "Q. kind a = (Q)"
          then obtain Q where "kind a = (Q)" by blast
          with transfer (kind a) s1 = s1' have "s1' = cf1 # cfs1" by simp
          from sourcenode a  HRB_slice SCFG kind a = (Q)
          have "slice_kind S a = (Q)"
            by(fastforce dest:slice_intra_kind_in_slice simp:intra_kind_def)
          hence "transfer (slice_kind S a) s2 = s2" by simp
          from valid_edge a V  Use (sourcenode a). fst cf1 V = fst cf2 V 
            intra_kind (kind a) pred (kind a) s1 pred (kind a) s2
          have "V  Def (sourcenode a). state_val (transfer (kind a) s1) V =
                                         state_val (transfer (kind a) s2) V"
            by -(erule CFG_intra_edge_transfer_uses_only_Use,auto simp:intra_kind_def)
          with True kind a = (Q) s1' = cf1 # cfs1
            transfer (slice_kind S a) s2 = s2 
          show ?thesis by simp
        qed
      next
        case False
        with valid_edge a intra_kind (kind a) pred (kind a) s1
        have "state_val (transfer (kind a) s1) V = state_val s1 V"
          by(fastforce intro:CFG_intra_edge_no_Def_equal)
        with transfer (kind a) s1 = s1' have "fst cf1' V = fst cf1 V" by simp
        from sourcenode a  HRB_slice SCFG intra_kind (kind a)
        have "slice_kind S a = kind a" by(fastforce intro:slice_intra_kind_in_slice)
        from False valid_edge a pred (kind a) s2 intra_kind (kind a)
        have "state_val (transfer (kind a) s2) V = state_val s2 V"
          by(fastforce intro:CFG_intra_edge_no_Def_equal)
        with slice_kind S a = kind a
        have "state_val (transfer (slice_kind S a) s2) V = fst cf2 V" by simp
        from V  rv S (CFG_node (targetnode a)) obtain as' nx 
          where "targetnode a -as'ι* parent_node nx" 
          and "nx  HRB_slice S" and "V  UseSDG nx"
          and "n''. valid_SDG_node n''  parent_node n''  set (sourcenodes as') 
                      V  DefSDG n''"
          by(fastforce elim:rvE)
        with n''. valid_SDG_node n''  parent_node n''  set (sourcenodes as') 
                     V  DefSDG n'' False
        have all:"n''. valid_SDG_node n''  
          parent_node n''  set (sourcenodes (a#as'))  V  DefSDG n''"
          by(fastforce dest:SDG_Def_parent_Def simp:sourcenodes_def)
        from  valid_edge a targetnode a -as'ι* parent_node nx 
          intra_kind (kind a)
        have "sourcenode a -a#as'ι* parent_node nx"
          by(fastforce intro:Cons_path simp:intra_path_def)
        with nx  HRB_slice S V  UseSDG nx all
        have "V  rv S (CFG_node (sourcenode a))" by(fastforce intro:rvI)
        with V  rv S (CFG_node mx). (fst (s1!(length msx))) V = state_val s2 V
          state_val (transfer (slice_kind S a) s2) V = fst cf2 V
          fst cf1' V = fst cf1 V
        show ?thesis by fastforce
      qed
    qed
    with i < length ms2. V  rv S (CFG_node ((mx#tl ms2)!i)). 
      (fst (s1!(length msx + i))) V = (fst (s2!i)) V cf2' 
      ms1' = [] @ targetnode a # tl ms2
      length ms1 = length s1 length ms2 = length s2 length s1 = length s2
    have "i<length ms1'. Vrv S (CFG_node ((targetnode a # tl ms1')!i)).
      (fst (s1'!(length [] + i))) V = (fst (transfer (slice_kind S a) s2 ! i)) V"
      by clarsimp(case_tac i,auto)
    with m  set ms2. valid_node m m  set ms1'. valid_node m 
      length ms2 = length s2 length s1' = length (transfer (slice_kind S a) s2)
      length ms1' = length s1' m  set (tl ms1'). return_node m
      ms1' = [] @ targetnode a # tl ms2 get_proc mx = get_proc (hd ms2)
      m  set (tl ms1). m'. call_of_return_node m m'  m'  HRB_slice SCFG
      i<length ms1'. snd (s1' ! i) = snd (transfer (slice_kind S a) s2 ! i)
    have "((ms1',s1'),(ms1',transfer (slice_kind S a) s2))  WS S"
      by(fastforce intro!:WSI)
    with S,slice_kind S  (ms2,s2) =as@[a] (ms1',transfer (slice_kind S a) s2)
    show ?case by blast
  next
    case (observable_move_call a s1 s1' Q r p fs a' ms1 S ms1')
    from s1  [] s2  [] obtain cf1 cfs1 cf2 cfs2 where [simp]:"s1 = cf1#cfs1" 
      and [simp]:"s2 = cf2#cfs2" by(cases s1,auto,cases s2,fastforce+)
    from length ms1 = length s1 s1  [] have [simp]:"ms1  []" by(cases ms1) auto
    from length ms2 = length s2 s2  [] have [simp]:"ms2  []" by(cases ms2) auto
    from m  set (tl ms1). m'. call_of_return_node m m'  m'  HRB_slice SCFG
      hd ms1 = sourcenode a ms1 = msx@mx#tl ms2
      msx  []  (mx'. call_of_return_node mx mx'  mx'  HRB_slice SCFG)
    have [simp]:"mx = sourcenode a" "msx = []" and [simp]:"tl ms2 = tl ms1"
      by(cases msx,auto)+
    hence "length ms1 = length ms2" by(cases ms2) auto
    with length ms1 = length s1 length ms2 = length s2
    have "length s1 = length s2" by simp
    from hd ms1  HRB_slice SCFG hd ms1 = sourcenode a
    have "sourcenode a  HRB_slice SCFG" by simp
    with valid_edge a 
    have "obs_intra (sourcenode a) HRB_slice SCFG = {sourcenode a}"
      by(fastforce intro!:n_in_obs_intra)
    from m  set (tl ms2). m'. call_of_return_node m m'  m'  HRB_slice SCFG
      obs_intra (sourcenode a) HRB_slice SCFG = {sourcenode a} 
      hd ms1 = sourcenode a 
    have "(hd ms1#tl ms1)  obs ([]@hd ms1#tl ms1) HRB_slice SCFG"
      by(cases ms1)(auto intro!:obsI)
    hence "ms1  obs ms1 HRB_slice SCFG" by simp
    with obs ms1 HRB_slice SCFG = obs ms2 HRB_slice SCFG
    have "ms1  obs ms2 HRB_slice SCFG" by simp
    from ms2  [] length ms2 = length s2 have "length s2 = length (hd ms2#tl ms2)"
      by(fastforce dest!:hd_Cons_tl)
    from m  set (tl ms1). return_node m have "m  set (tl ms2). return_node m"
      by simp
    with ms1  obs ms2 HRB_slice SCFG
    have "hd ms1  obs_intra (hd ms2) HRB_slice SCFG"
    proof(rule obsE)
      fix nsx n nsx' n'
      assume "ms2 = nsx @ n # nsx'" and "ms1 = n' # nsx'"
        and "n'  obs_intra n HRB_slice SCFG"
      from ms2 = nsx @ n # nsx' ms1 = n' # nsx' tl ms2 = tl ms1
      have [simp]:"nsx = []" by(cases nsx) auto
      with ms2 = nsx @ n # nsx' have [simp]:"n = hd ms2" by simp
      from ms1 = n' # nsx' have [simp]:"n' = hd ms1" by simp
      with n'  obs_intra n HRB_slice SCFG show ?thesis by simp
    qed
    with length s2 = length (hd ms2#tl ms2) m  set (tl ms2). return_node m
    obtain as where "S,slice_kind S  (hd ms2#tl ms2,s2) =asτ (hd ms1#tl ms1,s2)"
      by(fastforce elim:silent_moves_intra_path_obs[of _ _ _ s2 "tl ms2"])
    with ms2  [] have "S,slice_kind S  (ms2,s2) =asτ (ms1,s2)"
      by(fastforce dest!:hd_Cons_tl)
    from valid_edge a have "valid_node (sourcenode a)" by simp
    hence "sourcenode a -[]ι* sourcenode a"
      by(fastforce intro:empty_path simp:intra_path_def)
    with sourcenode a  HRB_slice SCFG
    have "V. V  UseSDG (CFG_node (sourcenode a)) 
       V  rv S (CFG_node (sourcenode a))"
      by auto(rule rvI,auto simp:SDG_to_CFG_set_def sourcenodes_def)
    with valid_node (sourcenode a)
    have "V  Use (sourcenode a). V  rv S (CFG_node (sourcenode a))"
      by(fastforce intro:CFG_Use_SDG_Use)
    from i < length ms2. V  rv S (CFG_node ((mx#tl ms2)!i)). 
      (fst (s1!(length msx + i))) V = (fst (s2!i)) V length ms2 = length s2
    have "Vrv S (CFG_node mx). (fst (s1 ! length msx)) V = state_val s2 V"
      by(cases ms2) auto
    with V  Use (sourcenode a). V  rv S (CFG_node (sourcenode a))
    have "V  Use (sourcenode a). fst cf1 V = fst cf2 V" by fastforce
    moreover
    from i<length ms2. snd (s1 ! (length msx + i)) = snd (s2 ! i)
    have "snd (hd s1) = snd (hd s2)" by(erule_tac x="0" in allE) auto
    ultimately have "pred (kind a) s2"
      using valid_edge a pred (kind a) s1 length s1 = length s2
      by(fastforce intro:CFG_edge_Uses_pred_equal)
    from ms1' = (targetnode a)#(targetnode a')#tl ms1 length s1' = Suc(length s1) 
      length ms1 = length s1 have "length ms1' = length s1'" by simp
    from valid_edge a kind a = Q:r↪⇘pfs obtain ins outs 
      where "(p,ins,outs)  set procs" by(fastforce dest!:callee_in_procs)
    with valid_edge a kind a = Q:r↪⇘pfs 
    have "(THE ins. outs. (p,ins,outs)  set procs) = ins"
      by(rule formal_in_THE)
    with transfer (kind a) s1 = s1' kind a = Q:r↪⇘pfs
    have [simp]:"s1' = (Map.empty(ins [:=] params fs (fst cf1)),r)#cf1#cfs1" by simp
    from valid_edge a' a'  get_return_edges a valid_edge 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
    from sourcenode a  HRB_slice SCFG pred (kind a) s2 kind a = Q:r↪⇘pfs
    have "pred (slice_kind S a) s2" by(fastforce dest:slice_kind_Call_in_slice)
    from valid_edge a length s1 = length s2 transfer (kind a) s1 = s1'
    have "length s1' = length (transfer (slice_kind S a) s2)"
      by(fastforce intro:length_transfer_kind_slice_kind)
    with pred (slice_kind S a) s2 valid_edge a kind a = Q:r↪⇘pfs
      m  set (tl ms1). m'. call_of_return_node m m'  m'  HRB_slice SCFG
      hd ms1  HRB_slice SCFG hd ms1 = sourcenode a
      length ms1 = length s1 length s1 = length s2 valid_edge a'
      ms1' = (targetnode a)#(targetnode a')#tl ms1 a'  get_return_edges a
      m  set (tl ms2). return_node m
    have "S,slice_kind S  (ms1,s2) -a (ms1',transfer (slice_kind S a) s2)"
      by(auto intro:observable_move.observable_move_call)
    with S,slice_kind S  (ms2,s2) =asτ (ms1,s2) 
    have "S,slice_kind S  (ms2,s2) =as@[a] (ms1',transfer (slice_kind S a) s2)"
      by(rule observable_moves_snoc)
    from m  set ms1. valid_node m ms1' = (targetnode a)#(targetnode a')#tl ms1
      valid_edge a valid_edge a'
    have "m  set ms1'. valid_node m" by(cases ms1) auto
    from kind a = Q:r↪⇘pfs sourcenode a  HRB_slice SCFG
    have cf2':"cf2'. transfer (slice_kind S a) s2 = cf2'#s2  snd cf2' = r"
      by(auto dest:slice_kind_Call_in_slice)
    with i<length ms2. snd (s1 ! (length msx + i)) = snd (s2 ! i) 
      length ms1' = length s1' msx = [] length ms1 = length ms2
      length ms1 = length s1
    have "i<length ms1'. snd (s1' ! i) = snd (transfer (slice_kind S a) s2 ! i)"
      by auto(case_tac i,auto)
    have "V  rv S (CFG_node (targetnode a')). 
      V  rv S (CFG_node (sourcenode a))"
    proof
      fix V assume "V  rv S (CFG_node (targetnode a'))"
      then obtain as n' where "targetnode a' -asι* parent_node n'"
        and "n'  HRB_slice S" and "V  UseSDG n'"
        and "n''. valid_SDG_node n''  parent_node n''  set (sourcenodes as) 
         V  DefSDG n''" by(fastforce elim:rvE)
      from valid_edge a a'  get_return_edges a
      obtain a'' where "valid_edge a''" and "sourcenode a'' = sourcenode a"
        and "targetnode a'' = targetnode a'" and "intra_kind(kind a'')"
        by -(drule call_return_node_edge,auto simp:intra_kind_def)
      with targetnode a' -asι* parent_node n' 
      have "sourcenode a -a''#asι* parent_node n'"
        by(fastforce intro:Cons_path simp:intra_path_def)
      from sourcenode a'' = sourcenode a valid_edge a kind a = Q:r↪⇘pfs
      have "n''. valid_SDG_node n''  parent_node n'' = sourcenode a''
         V  DefSDG n''"
        by(fastforce dest:SDG_Def_parent_Def call_source_Def_empty)
      with n''. valid_SDG_node n''  parent_node n''  set (sourcenodes as) 
         V  DefSDG n''
      have "n''. valid_SDG_node n''  parent_node n''  set (sourcenodes (a''#as)) 
         V  DefSDG n''" by(fastforce simp:sourcenodes_def)
      with sourcenode a -a''#asι* parent_node n' n'  HRB_slice S
        V  UseSDG n'
      show "V  rv S (CFG_node (sourcenode a))" by(fastforce intro:rvI)
    qed
    have "V  rv S (CFG_node (targetnode a)). 
      (Map.empty(ins [:=] params fs (fst cf1))) V = 
      state_val (transfer (slice_kind S a) s2) V"
    proof
      fix V assume "V  rv S (CFG_node (targetnode a))"
      from sourcenode a  HRB_slice SCFG kind a = Q:r↪⇘pfs
        (THE ins. outs. (p,ins,outs)  set procs) = ins
      have eq:"fst (hd (transfer (slice_kind S a) s2)) = 
        Map.empty(ins [:=] params (cspp (targetnode a) (HRB_slice S) fs) (fst cf2))"
        by(auto dest:slice_kind_Call_in_slice)
      show "(Map.empty(ins [:=] params fs (fst cf1))) V = 
        state_val (transfer (slice_kind S a) s2) V"
      proof(cases "V  set ins")
        case True
        then obtain i where "V = ins!i" and "i < length ins"
          by(auto simp:in_set_conv_nth)
        from valid_edge a kind a = Q:r↪⇘pfs (p,ins,outs)  set procs
          i < length ins
        have "valid_SDG_node (Formal_in (targetnode a,i))" by fastforce
        from valid_edge a kind a = Q:r↪⇘pfs have "get_proc(targetnode a) = p"
          by(rule get_proc_call)
        with valid_SDG_node (Formal_in (targetnode a,i)) 
          (p,ins,outs)  set procs V = ins!i
        have "V  DefSDG (Formal_in (targetnode a,i))"
          by(fastforce intro:Formal_in_SDG_Def)
        from V  rv S (CFG_node (targetnode a)) obtain as' nx 
          where "targetnode a -as'ι* parent_node nx" 
          and "nx  HRB_slice S" and "V  UseSDG nx"
          and "n''. valid_SDG_node n''  
          parent_node n''  set (sourcenodes as')  V  DefSDG n''"
          by(fastforce elim:rvE)
        with valid_SDG_node (Formal_in (targetnode a,i))
          V  DefSDG (Formal_in (targetnode a,i))
        have "targetnode a = parent_node nx" 
          apply(auto simp:intra_path_def sourcenodes_def)
          apply(erule path.cases) apply fastforce
          apply(erule_tac x="Formal_in (targetnode a,i)" in allE) by fastforce
        with V  UseSDG nx have "V  Use (targetnode a)"
          by(fastforce intro:SDG_Use_parent_Use)
        with valid_edge a have "V  UseSDG (CFG_node (targetnode a))"
          by(auto intro!:CFG_Use_SDG_Use)
        from targetnode a = parent_node nx[THEN sym] valid_edge a
        have "parent_node (Formal_in (targetnode a,i)) -[]ι* parent_node nx"
          by(fastforce intro:empty_path simp:intra_path_def)
        with V  DefSDG (Formal_in (targetnode a,i)) 
          V  UseSDG (CFG_node (targetnode a)) targetnode a = parent_node nx
        have "Formal_in (targetnode a,i) influences V in (CFG_node (targetnode a))"
          by(fastforce simp:data_dependence_def sourcenodes_def)
        hence ddep:"Formal_in (targetnode a,i) s-Vdd (CFG_node (targetnode a))"
          by(rule sum_SDG_ddep_edge)
        from targetnode a = parent_node nx nx  HRB_slice S
        have "CFG_node (targetnode a)  HRB_slice S"
          by(fastforce dest:valid_SDG_node_in_slice_parent_node_in_slice)
        hence "Formal_in (targetnode a,i)  HRB_slice S"
        proof(induct "CFG_node (targetnode a)" rule:HRB_slice_cases)
          case (phase1 nx)
          with ddep show ?case
            by(fastforce intro:ddep_slice1 combine_SDG_slices.combSlice_refl 
                         simp:HRB_slice_def)
        next
          case (phase2 nx n' n'' p)
          from CFG_node (targetnode a)  sum_SDG_slice2 n' ddep
          have "Formal_in (targetnode a,i)  sum_SDG_slice2 n'"
            by(fastforce intro:ddep_slice2)
          with n'' s-pret CFG_node (parent_node n') n'  sum_SDG_slice1 nx 
            nx  S
          show ?case by(fastforce intro:combine_SDG_slices.combSlice_Return_parent_node                                  simp:HRB_slice_def)
        qed
        from sourcenode a  HRB_slice SCFG kind a = Q:r↪⇘pfs
        have slice_kind:"slice_kind S a = 
          Q:r↪⇘p(cspp (targetnode a) (HRB_slice S) fs)"
          by(rule slice_kind_Call_in_slice)
        from valid_edge a kind a = Q:r↪⇘pfs (p,ins,outs)  set procs
        have "length fs = length ins" by(rule CFG_call_edge_length)
        from Formal_in (targetnode a,i)  HRB_slice S
          length fs = length ins i < length ins
        have cspp:"(cspp (targetnode a) (HRB_slice S) fs)!i = fs!i"
          by(fastforce intro:csppa_Formal_in_in_slice simp:cspp_def)
        from i < length ins length fs = length ins
        have "(params (cspp (targetnode a) (HRB_slice S) fs) (fst cf2))!i = 
          ((cspp (targetnode a) (HRB_slice S) fs)!i) (fst cf2)"
          by(fastforce intro:params_nth)
        with cspp 
        have eq:"(params (cspp (targetnode a) (HRB_slice S) fs) (fst cf2))!i =
          (fs!i) (fst cf2)" by simp
        from valid_edge a kind a = Q:r↪⇘pfs (p,ins,outs)  set procs
        have "(THE ins. outs. (p,ins,outs)  set procs) = ins"
          by(rule formal_in_THE)
        with slice_kind
        have "fst (hd (transfer (slice_kind S a) s2)) = 
          Map.empty(ins [:=] params (cspp (targetnode a) (HRB_slice S) fs) (fst cf2))"
          by simp
        moreover
        from (p,ins,outs)  set procs have "distinct ins" 
          by(rule distinct_formal_ins)
        ultimately have "state_val (transfer (slice_kind S a) s2) V = 
          (params (cspp (targetnode a) (HRB_slice S) fs) (fst cf2))!i"
          using V = ins!i i < length ins length fs = length ins
          by(fastforce intro:fun_upds_nth)
        with eq 
        have 2:"state_val (transfer (slice_kind S a) s2) V = (fs!i) (fst cf2)"
          by simp
        from V = ins!i i < length ins length fs = length ins
          distinct ins
        have "Map.empty(ins [:=] params fs (fst cf1)) V = (params fs (fst cf1))!i"
          by(fastforce intro:fun_upds_nth)
        with i < length ins length fs = length ins
        have 1:"Map.empty(ins [:=] params fs (fst cf1)) V = (fs!i) (fst cf1)"
          by(fastforce intro:params_nth)
        from i < length ms2. V  rv S (CFG_node ((mx#tl ms2)!i)). 
          (fst (s1!(length msx + i))) V = (fst (s2!i)) V
        have rv:"Vrv S (CFG_node (sourcenode a)). fst cf1 V = fst cf2 V"
          by(erule_tac x="0" in allE) auto
        from valid_edge a kind a = Q:r↪⇘pfs (p,ins,outs)  set procs 
          i < length ins have "V(ParamUses (sourcenode a)!i). 
          V  UseSDG (Actual_in (sourcenode a,i))"
          by(fastforce intro:Actual_in_SDG_Use)
        with valid_edge a have "V(ParamUses (sourcenode a)!i). 
          V  UseSDG (CFG_node (sourcenode a))"
          by(auto intro!:CFG_Use_SDG_Use dest:SDG_Use_parent_Use)
        moreover
        from valid_edge a have "parent_node (CFG_node (sourcenode a)) -[]ι* 
          parent_node (CFG_node (sourcenode a))"
          by(fastforce intro:empty_path simp:intra_path_def)
        ultimately 
        have "V(ParamUses (sourcenode a)!i). V  rv S (CFG_node (sourcenode a))"
          using sourcenode a  HRB_slice SCFG valid_edge a
          by(fastforce intro:rvI simp:SDG_to_CFG_set_def sourcenodes_def)
        with rv have "V  (ParamUses (sourcenode a))!i. fst cf1 V = fst cf2 V"
          by fastforce
        with valid_edge a kind a = Q:r↪⇘pfs i < length ins
          (p,ins,outs)  set procs pred (kind a) s1 pred (kind a) s2
        have "(params fs (fst cf1))!i = (params fs (fst cf2))!i"
          by(fastforce dest!:CFG_call_edge_params)
        moreover
        from i < length ins length fs = length ins
        have "(params fs (fst cf1))!i = (fs!i) (fst cf1)" 
          and "(params fs (fst cf2))!i = (fs!i) (fst cf2)"
          by(auto intro:params_nth)
        ultimately show ?thesis using 1 2 by simp
      next
        case False
        with eq show ?thesis by(fastforce simp:fun_upds_notin)
      qed
    qed
    with i < length ms2. V  rv S (CFG_node ((mx#tl ms2)!i)). 
      (fst (s1!(length msx + i))) V = (fst (s2!i)) V cf2' tl ms2 = tl ms1
      length ms2 = length s2 length ms1 = length s1 length s1 = length s2
      ms1' = (targetnode a)#(targetnode a')#tl ms1
      V  rv S (CFG_node (targetnode a')). V  rv S (CFG_node (sourcenode a))
    have "i<length ms1'. Vrv S (CFG_node ((targetnode a # tl ms1')!i)).
      (fst (s1'!(length [] + i))) V = (fst (transfer (slice_kind S a) s2!i)) V"
      apply clarsimp apply(case_tac i) apply auto
      apply(erule_tac x="nat" in allE)
      apply(case_tac nat) apply auto done
    with m  set ms2. valid_node m m  set ms1'. valid_node m 
      length ms2 = length s2 length s1' = length (transfer (slice_kind S a) s2)
      length ms1' = length s1' ms1' = (targetnode a)#(targetnode a')#tl ms1
      get_proc mx = get_proc (hd ms2) sourcenode a  HRB_slice SCFG
      m  set (tl ms1). m'. call_of_return_node m m'  m'  HRB_slice SCFG
      return_node (targetnode a') m  set (tl ms1). return_node m
      call_of_return_node (targetnode a') (sourcenode a)
      i<length ms1'. snd (s1' ! i) = snd (transfer (slice_kind S a) s2 ! i)
    have "((ms1',s1'),(ms1',transfer (slice_kind S a) s2))  WS S"
      by(fastforce intro!:WSI)
    with S,slice_kind S  (ms2,s2) =as@[a] (ms1',transfer (slice_kind S a) s2)
    show ?case by blast
  next
    case (observable_move_return a s1 s1' Q p f' ms1 S ms1')
    from s1  [] s2  [] obtain cf1 cfs1 cf2 cfs2 where [simp]:"s1 = cf1#cfs1" 
      and [simp]:"s2 = cf2#cfs2" by(cases s1,auto,cases s2,fastforce+)
    from length ms1 = length s1 s1  [] have [simp]:"ms1  []" by(cases ms1) auto
    from length ms2 = length s2 s2  [] have [simp]:"ms2  []" by(cases ms2) auto
    from m  set (tl ms1). m'. call_of_return_node m m'  m'  HRB_slice SCFG
      hd ms1 = sourcenode a ms1 = msx@mx#tl ms2
      msx  []  (mx'. call_of_return_node mx mx'  mx'  HRB_slice SCFG)
    have [simp]:"mx = sourcenode a" "msx = []" and [simp]:"tl ms2 = tl ms1"
      by(cases msx,auto)+
    hence "length ms1 = length ms2" by(cases ms2) auto
    with length ms1 = length s1 length ms2 = length s2
    have "length s1 = length s2" by simp
    have "as. S,slice_kind S  (ms2,s2) =asτ (ms1,s2)"
    proof(cases "obs_intra (hd ms2) HRB_slice SCFG = {}")
      case True
      from valid_edge a hd ms1 = sourcenode a kind a = Q↩⇘pf'
      have "method_exit (hd ms1)" by(fastforce simp:method_exit_def)
      from mset ms2. valid_node m have "valid_node (hd ms2)" by(cases ms2) auto
      then obtain asx where "hd ms2 -asx* (_Exit_)" by(fastforce dest!:Exit_path)
      then obtain as pex where "hd ms2 -asι* pex" and "method_exit pex"
        by(fastforce elim:valid_Exit_path_intra_path)
      from hd ms2 -asι* pex have "get_proc (hd ms2) = get_proc pex"
        by(rule intra_path_get_procs)
      with get_proc mx = get_proc (hd ms2)
      have "get_proc mx = get_proc pex" by simp
      with method_exit (hd ms1) hd ms1 = sourcenode a method_exit pex
      have [simp]:"pex = hd ms1" by(fastforce intro:method_exit_unique)
      from obs_intra (hd ms2) HRB_slice SCFG = {} method_exit pex
        get_proc (hd ms2) = get_proc pex valid_node (hd ms2)
        length ms2 = length s2 mset (tl ms1). return_node m ms2  []
      obtain as' 
        where "S,slice_kind S  (hd ms2#tl ms2,s2) =as'τ (hd ms1#tl ms1,s2)"
        by(fastforce elim!:silent_moves_intra_path_no_obs[of _ _ _ s2 "tl ms2"]
                     dest:hd_Cons_tl)
      with ms2  [] have "S,slice_kind S  (ms2,s2) =as'τ (ms1,s2)"
        by(fastforce dest!:hd_Cons_tl)
      thus ?thesis by blast
    next
      case False
      then obtain x where "x  obs_intra (hd ms2) HRB_slice SCFG" by fastforce
      hence "obs_intra (hd ms2) HRB_slice SCFG = {x}"
        by(rule obs_intra_singleton_element)
      with m  set (tl ms2). m'. call_of_return_node m m'  m'  HRB_slice SCFG
      have "x#tl ms1  obs ([]@hd ms2#tl ms2) HRB_slice SCFG"
        by(fastforce intro:obsI)
      with ms2  [] have "x#tl ms1  obs ms2 HRB_slice SCFG"
        by(fastforce dest:hd_Cons_tl simp del:obs.simps)
      with obs ms1 HRB_slice SCFG = obs ms2 HRB_slice SCFG
      have "x#tl ms1  obs ms1 HRB_slice SCFG" by simp
      from this mset (tl ms1). return_node m
      have "x  obs_intra (hd ms1) HRB_slice SCFG"
      proof(rule obsE)
        fix nsx n nsx' n'
        assume "ms1 = nsx @ n # nsx'" and "x # tl ms1 = n' # nsx'"
          and "n'  obs_intra n HRB_slice SCFG"
        from ms1 = nsx @ n # nsx' x # tl ms1 = n' # nsx' tl ms2 = tl ms1
        have [simp]:"nsx = []" by(cases nsx) auto
        with ms1 = nsx @ n # nsx' have [simp]:"n = hd ms1" by simp
        from x # tl ms1 = n' # nsx' have [simp]:"n' = x" by simp
        with n'  obs_intra n HRB_slice SCFG show ?thesis by simp
      qed
      { fix m as assume "hd ms1 -asι* m"
        hence "hd ms1 -as→* m" and "a  set as. intra_kind (kind a)"
          by(simp_all add:intra_path_def)
        hence "m = hd ms1"
        proof(induct "hd ms1" as m rule:path.induct)
          case (Cons_path m'' as' m' a')
          from aset (a' # as'). intra_kind (kind a)
          have "intra_kind (kind a')" by simp
          with valid_edge a kind a = Q↩⇘pf' valid_edge a' 
            sourcenode a' = hd ms1 hd ms1 = sourcenode a
          have False by(fastforce dest:return_edges_only simp:intra_kind_def)
          thus ?case by simp
        qed simp }
      with x  obs_intra (hd ms1) HRB_slice SCFG
      have "x = hd ms1" by(fastforce elim:obs_intraE)
      with x  obs_intra (hd ms2) HRB_slice SCFG length ms2 = length s2 
        mset (tl ms1). return_node m ms2  []
      obtain as where "S,slice_kind S  (hd ms2#tl ms2,s2) =asτ (hd ms1#tl ms1,s2)"
        by(fastforce elim!:silent_moves_intra_path_obs[of _ _ _ s2 "tl ms2"] 
                     dest:hd_Cons_tl)
      with ms2  [] have "S,slice_kind S  (ms2,s2) =asτ (ms1,s2)"
        by(fastforce dest!:hd_Cons_tl)
      thus ?thesis by blast
    qed
    then obtain as where "S,slice_kind S  (ms2,s2) =asτ (ms1,s2)" by blast
    from ms1' = tl ms1 length s1 = Suc(length s1') 
      length ms1 = length s1 have "length ms1' = length s1'" by simp
    from valid_edge a kind a = Q↩⇘pf' obtain a'' Q' r' fs' where "valid_edge a''"
      and "kind a'' = Q':r'↪⇘pfs'" and "a  get_return_edges a''"
      by -(drule return_needs_call,auto)
    then obtain ins outs where "(p,ins,outs)  set procs"
      by(fastforce dest!:callee_in_procs)
    from length s1 = Suc(length s1') s1'  []
    obtain cfx cfsx where [simp]:"cfs1 = cfx#cfsx" by(cases cfs1) auto
    with length s1 = length s2 obtain cfx' cfsx' where [simp]:"cfs2 = cfx'#cfsx'"
      by(cases cfs2) auto
    from length ms1 = length s1 have "tl ms1 = []@hd(tl ms1)#tl(tl ms1)"
      by(auto simp:length_Suc_conv)
    from kind a = Q↩⇘pf' transfer (kind a) s1 = s1'
    have "s1' = (f' (fst cf1) (fst cfx),snd cfx)#cfsx" by simp
    from valid_edge a kind a = Q↩⇘pf' (p,ins,outs)  set procs
    have "f' (fst cf1) (fst cfx) = 
      (fst cfx)(ParamDefs (targetnode a) [:=] map (fst cf1) outs)"
      by(rule CFG_return_edge_fun)
    with s1' = (f' (fst cf1) (fst cfx),snd cfx)#cfsx
    have [simp]:"s1' = 
      ((fst cfx)(ParamDefs (targetnode a) [:=] map (fst cf1) outs),snd cfx)#cfsx"
      by simp
    have "pred (slice_kind S a) s2"
    proof(cases "sourcenode a  HRB_slice SCFG")
      case True
      from valid_edge a have "valid_node (sourcenode a)" by simp
      hence "sourcenode a -[]ι* sourcenode a"
        by(fastforce intro:empty_path simp:intra_path_def)
      with sourcenode a  HRB_slice SCFG
      have "V. V  UseSDG (CFG_node (sourcenode a)) 
         V  rv S (CFG_node (sourcenode a))"
        by auto(rule rvI,auto simp:SDG_to_CFG_set_def sourcenodes_def)
      with valid_node (sourcenode a)
      have "V  Use (sourcenode a). V  rv S (CFG_node (sourcenode a))"
        by(fastforce intro:CFG_Use_SDG_Use)
      from i < length ms2. V  rv S (CFG_node ((mx#tl ms2)!i)). 
        (fst (s1!(length msx + i))) V = (fst (s2!i)) V length ms2 = length s2
      have "Vrv S (CFG_node mx). (fst (s1 ! length msx)) V = state_val s2 V"
        by(cases ms2) auto
      with V  Use (sourcenode a). V  rv S (CFG_node (sourcenode a))
      have "V  Use (sourcenode a). fst cf1 V = fst cf2 V" by fastforce
      moreover
      from i<length ms2. snd (s1 ! (length msx + i)) = snd (s2 ! i)
      have "snd (hd s1) = snd (hd s2)" by(erule_tac x="0" in allE) auto
      ultimately have "pred (kind a) s2"
        using valid_edge a pred (kind a) s1 length s1 = length s2
        by(fastforce intro:CFG_edge_Uses_pred_equal)
      with valid_edge a kind a = Q↩⇘pf' (p,ins,outs)  set procs 
        sourcenode a  HRB_slice SCFG
      show ?thesis by(fastforce dest:slice_kind_Return_in_slice)
    next
      case False
      with kind a = Q↩⇘pf' have "slice_kind S a = (λcf. True)↩⇘p(λcf cf'. cf')"
        by -(rule slice_kind_Return)
      thus ?thesis by simp
    qed
    from valid_edge a length s1 = length s2 transfer (kind a) s1 = s1'
    have "length s1' = length (transfer (slice_kind S a) s2)"
      by(fastforce intro:length_transfer_kind_slice_kind)
    with pred (slice_kind S a) s2 valid_edge a kind a = Q↩⇘pf'
      m  set (tl ms1). m'. call_of_return_node m m'  m'  HRB_slice SCFG
      hd ms1 = sourcenode a
      length ms1 = length s1 length s1 = length s2
      ms1' = tl ms1 hd(tl ms1) = targetnode a m  set (tl ms1). return_node m
    have "S,slice_kind S  (ms1,s2) -a (ms1',transfer (slice_kind S a) s2)"
      by(fastforce intro!:observable_move.observable_move_return)
    with S,slice_kind S  (ms2,s2) =asτ (ms1,s2)
    have "S,slice_kind S  (ms2,s2) =as@[a] (ms1',transfer (slice_kind S a) s2)"
      by(rule observable_moves_snoc)
    from m  set ms1. valid_node m ms1' = tl ms1
    have "m  set ms1'. valid_node m" by(cases ms1) auto
    from length ms1' = length s1' have "ms1' = []@hd ms1'#tl ms1'"
      by(cases ms1') auto
    from i<length ms2. snd (s1 ! (length msx + i)) = snd (s2 ! i)
      length ms1 = length ms2 length ms1 = length s1
    have "snd cfx = snd cfx'" by(erule_tac x="1" in allE) auto
    from valid_edge a kind a = Q↩⇘pf' (p,ins,outs)  set procs
    have cf2':"cf2'. transfer (slice_kind S a) s2 = cf2'#cfsx'  snd cf2' = snd cfx'"
      by(cases cfx',cases "sourcenode a  HRB_slice SCFG",
         auto dest:slice_kind_Return slice_kind_Return_in_slice)
    with i<length ms2. snd (s1 ! (length msx + i)) = snd (s2 ! i) 
      length ms1' = length s1' msx = [] length ms1 = length ms2
      length ms1 = length s1 snd cfx = snd cfx'
    have "i<length ms1'. snd (s1' ! i) = snd (transfer (slice_kind S a) s2 ! i)"
      apply auto apply(case_tac i) apply auto
      by(erule_tac x="Suc(Suc nat)" in allE) auto
    from m  set (tl ms1). m'. call_of_return_node m m'  m'  HRB_slice SCFG
    have "m  set (tl (tl ms1)). 
      m'. call_of_return_node m m'  m'  HRB_slice SCFG"
      by(cases "tl ms1") auto
    from m  set (tl ms1). return_node m
    have "m  set (tl (tl ms1)). return_node m" by(cases "tl ms1") auto
    have "Vrv S (CFG_node (hd (tl ms1))).
      (fst cfx)(ParamDefs (targetnode a) [:=] map (fst cf1) outs) V = 
      state_val (transfer (slice_kind S a) s2) V"
    proof
      fix V assume "Vrv S (CFG_node (hd (tl ms1)))"
      with hd(tl ms1) = targetnode a have "Vrv S (CFG_node (targetnode a))"
        by simp
      show "(fst cfx)(ParamDefs (targetnode a) [:=] map (fst cf1) outs) V = 
        state_val (transfer (slice_kind S a) s2) V"
      proof(cases "V  set (ParamDefs (targetnode a))")
        case True
        then obtain i where "V = (ParamDefs (targetnode a))!i" 
          and "i < length(ParamDefs (targetnode a))"
          by(auto simp:in_set_conv_nth)
        moreover
        from valid_edge a kind a = Q↩⇘pf' (p,ins,outs)  set procs
        have length:"length(ParamDefs (targetnode a)) = length outs"
          by(fastforce intro:ParamDefs_return_target_length)
        from valid_edge a kind a = Q↩⇘pf' (p,ins,outs)  set procs
          i < length(ParamDefs (targetnode a)) 
          length(ParamDefs (targetnode a)) = length outs
        have "valid_SDG_node (Actual_out(targetnode a,i))" by fastforce
        with V = (ParamDefs (targetnode a))!i
        have "V  DefSDG (Actual_out(targetnode a,i))"
          by(fastforce intro:Actual_out_SDG_Def)
        from V  rv S (CFG_node (targetnode a)) obtain as' nx 
          where "targetnode a -as'ι* parent_node nx" 
          and "nx  HRB_slice S" and "V  UseSDG nx"
          and "n''. valid_SDG_node n''  
                         parent_node n''  set (sourcenodes as')  V  DefSDG n''"
          by(fastforce elim:rvE)
        with valid_SDG_node (Actual_out(targetnode a,i))
          V  DefSDG (Actual_out(targetnode a,i))
        have "targetnode a = parent_node nx" 
          apply(auto simp:intra_path_def sourcenodes_def)
          apply(erule path.cases) apply fastforce
          apply(erule_tac x="(Actual_out(targetnode a,i))" in allE) by fastforce
        with V  UseSDG nx have "V  Use (targetnode a)"
          by(fastforce intro:SDG_Use_parent_Use)
        with valid_edge a have "V  UseSDG (CFG_node (targetnode a))"
          by(auto intro!:CFG_Use_SDG_Use)
        from targetnode a = parent_node nx[THEN sym] valid_edge a
        have "parent_node (Actual_out(targetnode a,i)) -[]ι* parent_node nx"
          by(fastforce intro:empty_path simp:intra_path_def)
        with V  DefSDG (Actual_out(targetnode a,i)) 
          V  UseSDG (CFG_node (targetnode a)) targetnode a = parent_node nx
        have "Actual_out(targetnode a,i) influences V in (CFG_node (targetnode a))"
          by(fastforce simp:data_dependence_def sourcenodes_def)
        hence ddep:"Actual_out(targetnode a,i) s-Vdd (CFG_node (targetnode a))"
          by(rule sum_SDG_ddep_edge)
        from targetnode a = parent_node nx nx  HRB_slice S
        have "CFG_node (targetnode a)  HRB_slice S"
          by(fastforce dest:valid_SDG_node_in_slice_parent_node_in_slice)
        hence "Actual_out(targetnode a,i)  HRB_slice S"
        proof(induct "CFG_node (targetnode a)" rule:HRB_slice_cases)
          case (phase1 nx')
          with ddep show ?case
            by(fastforce intro: ddep_slice1 combine_SDG_slices.combSlice_refl
                         simp:HRB_slice_def)
        next
          case (phase2 nx' n' n'' p)
          from CFG_node (targetnode a)  sum_SDG_slice2 n' ddep
          have "Actual_out(targetnode a,i)  sum_SDG_slice2 n'"
            by(fastforce intro:ddep_slice2)
          with n'' s-pret CFG_node (parent_node n') n'  sum_SDG_slice1 nx'
            nx'  S
          show ?case by(fastforce intro:combine_SDG_slices.combSlice_Return_parent_node
                                  simp:HRB_slice_def)
        qed
        from valid_edge a kind a = Q↩⇘pf' valid_edge a''
          kind a'' = Q':r'↪⇘pfs' a  get_return_edges a''
          CFG_node (targetnode a)  HRB_slice S
        have "CFG_node (sourcenode a)  HRB_slice S"
          by(rule call_return_nodes_in_slice)
        hence "sourcenode a  HRB_slice SCFG" by(simp add:SDG_to_CFG_set_def)
        from sourcenode a  HRB_slice SCFG valid_edge a kind a = Q↩⇘pf'
          (p,ins,outs)  set procs
        have slice_kind:"slice_kind S a = 
          Q↩⇘p(λcf cf'. rspp (targetnode a) (HRB_slice S) outs cf' cf)"
          by(rule slice_kind_Return_in_slice)
        from Actual_out(targetnode a,i)  HRB_slice S
          i < length(ParamDefs (targetnode a)) valid_edge a
          V = (ParamDefs (targetnode a))!i length
        have 2:"rspp (targetnode a) (HRB_slice S) outs (fst cfx') (fst cf2) V = 
          (fst cf2)(outs!i)"
          by(fastforce intro:rspp_Actual_out_in_slice)
        from i < length(ParamDefs (targetnode a)) length valid_edge a
        have "(fst cfx)(ParamDefs (targetnode a) [:=] map (fst cf1) outs) 
          ((ParamDefs (targetnode a))!i) = (map (fst cf1) outs)!i"
          by(fastforce intro:fun_upds_nth distinct_ParamDefs)
        with V = (ParamDefs (targetnode a))!i 
          i < length(ParamDefs (targetnode a)) length
        have 1:"(fst cfx)(ParamDefs (targetnode a) [:=] map (fst cf1) outs) V = 
          (fst cf1)(outs!i)" 
          by simp
        from valid_edge a kind a = Q↩⇘pf' (p,ins,outs)  set procs 
          i < length(ParamDefs (targetnode a)) length
        have po:"Formal_out(sourcenode a,i) s-p:outs!iout Actual_out(targetnode a,i)"
          by(fastforce intro:sum_SDG_param_out_edge)
        from valid_edge a kind a = Q↩⇘pf'
        have "CFG_node (sourcenode a) s-pret CFG_node (targetnode a)"
          by(fastforce intro:sum_SDG_return_edge)
        from Actual_out(targetnode a,i)  HRB_slice S
        have "Formal_out(sourcenode a,i)  HRB_slice S"
        proof(induct "Actual_out(targetnode a,i)" rule:HRB_slice_cases)
          case (phase1 nx')
          let ?AO = "Actual_out(targetnode a,i)"
          from valid_SDG_node ?AO have "?AO  sum_SDG_slice2 ?AO"
            by(rule refl_slice2)
          with po have "Formal_out(sourcenode a,i)  sum_SDG_slice2 ?AO"
            by(rule param_out_slice2)
          with CFG_node (sourcenode a) s-pret CFG_node (targetnode a)
            Actual_out (targetnode a, i)  sum_SDG_slice1 nx' nx'  S
          show ?case
            by(fastforce intro:combSlice_Return_parent_node simp:HRB_slice_def)
        next
          case (phase2 nx' n' n'' p)
          from Actual_out (targetnode a, i)  sum_SDG_slice2 n' po
          have "Formal_out(sourcenode a,i)  sum_SDG_slice2 n'"
            by(fastforce intro:param_out_slice2)
          with n'  sum_SDG_slice1 nx' n'' s-pret CFG_node (parent_node n') 
            nx'  S
          show ?case by(fastforce intro:combine_SDG_slices.combSlice_Return_parent_node
                                  simp:HRB_slice_def)
        qed
        with valid_edge a kind a = Q↩⇘pf' (p,ins,outs)  set procs 
          i < length(ParamDefs (targetnode a)) length
        have "outs!i  UseSDG Formal_out(sourcenode a,i)"
          by(fastforce intro!:Formal_out_SDG_Use get_proc_return)
        with valid_edge a have "outs!i  UseSDG (CFG_node (sourcenode a))"
          by(auto intro!:CFG_Use_SDG_Use dest:SDG_Use_parent_Use)
        moreover
        from valid_edge a have "parent_node (CFG_node (sourcenode a)) -[]ι* 
          parent_node (CFG_node (sourcenode a))"
          by(fastforce intro:empty_path simp:intra_path_def)
        ultimately have "outs!i  rv S (CFG_node (sourcenode a))"
          using sourcenode a  HRB_slice SCFG valid_edge a
          by(fastforce intro:rvI simp:SDG_to_CFG_set_def sourcenodes_def)
        with i < length ms2. V  rv S (CFG_node ((mx#tl ms2)!i)). 
          (fst (s1!(length msx + i))) V = (fst (s2!i)) V
        have "(fst cf1)(outs!i) = (fst cf2)(outs!i)"
          by auto(erule_tac x="0" in allE,auto)
        with 1 2 slice_kind show ?thesis by simp
      next
        case False
        with transfer (kind a) s1 = s1'
        have "(fst cfx)(ParamDefs (targetnode a) [:=] map (fst cf1) outs) =
          (fst (hd cfs1))(ParamDefs (targetnode a) [:=] map (fst cf1) outs)"
          by(cases cfs1,auto intro:CFG_return_edge_fun)
        show ?thesis
        proof(cases "sourcenode a  HRB_slice SCFG")
          case True
          from sourcenode a  HRB_slice SCFG valid_edge a kind a = Q↩⇘pf'
            (p,ins,outs)  set procs
          have "slice_kind S a = 
            Q↩⇘p(λcf cf'. rspp (targetnode a) (HRB_slice S) outs cf' cf)"
            by(rule slice_kind_Return_in_slice)
          with length s1' = length (transfer (slice_kind S a) s2) 
            length s1 = length s2
          have "state_val (transfer (slice_kind S a) s2) V = 
            rspp (targetnode a) (HRB_slice S) outs (fst cfx') (fst cf2) V"
            by simp
          with V  set (ParamDefs (targetnode a))
          have "state_val (transfer (slice_kind S a) s2) V = state_val cfs2 V"
            by(fastforce simp:rspp_def map_merge_def)
          with i < length ms2. V  rv S (CFG_node ((mx#tl ms2)!i)). 
            (fst (s1!(length msx + i))) V = (fst (s2!i)) V
            hd(tl ms1) = targetnode a
            length ms1 = length s1 length s1 = length s2[THEN sym] False
            tl ms2 = tl ms1 length ms2 = length s2
            Vrv S (CFG_node (targetnode a))
          show ?thesis by(fastforce simp:length_Suc_conv fun_upds_notin)
        next
          case False
          from sourcenode a  HRB_slice SCFG kind a = Q↩⇘pf'
          have "slice_kind S a = (λcf. True)↩⇘p(λcf cf'. cf')"
            by(rule slice_kind_Return)
          from length ms2 = length s2 have "1 < length ms2" by simp
          with i < length ms2. V  rv S (CFG_node ((mx#tl ms2)!i)). 
            (fst (s1!(length msx + i))) V = (fst (s2!i)) V
            Vrv S (CFG_node (hd (tl ms1)))
            ms1' = tl ms1 ms1' = []@hd ms1'#tl ms1'
          have "fst cfx V = fst cfx' V" apply auto
            apply(erule_tac x="1" in allE)
            by(cases "tl ms1") auto
          with i < length ms2. V  rv S (CFG_node ((mx#tl ms2)!i)). 
            (fst (s1!(length msx + i))) V = (fst (s2!i)) V 
            hd(tl ms1) = targetnode a
            length ms1 = length s1 length s1 = length s2[THEN sym] False
            tl ms2 = tl ms1 length ms2 = length s2
            Vrv S (CFG_node (targetnode a))
            V  set (ParamDefs (targetnode a))
            slice_kind S a = (λcf. True)↩⇘p(λcf cf'. cf')
          show ?thesis by(auto simp:fun_upds_notin)
        qed
      qed
    qed
    with hd(tl ms1) = targetnode a tl ms2 = tl ms1 ms1' = tl ms1
      i < length ms2. V  rv S (CFG_node ((mx#tl ms2)!i)). 
        (fst (s1!(length msx + i))) V = (fst (s2!i)) V length ms1' = length s1'
      length ms1 = length s1 length ms2 = length s2 length s1 = length s2 cf2'
    have "i<length ms1'. Vrv S (CFG_node ((hd (tl ms1) # tl ms1')!i)).
      (fst (s1'!(length [] + i))) V = (fst (transfer (slice_kind S a) s2!i)) V"
      apply(case_tac "tl ms1") apply auto 
      apply(cases ms2) apply auto
      apply(case_tac i) apply auto
      by(erule_tac x="Suc(Suc nat)" in allE,auto)
    with m  set ms2. valid_node m m  set ms1'. valid_node m 
      length ms2 = length s2 length s1' = length (transfer (slice_kind S a) s2)
      length ms1' = length s1' ms1' = tl ms1 ms1' = []@hd ms1'#tl ms1'
      tl ms1 = []@hd(tl ms1)#tl(tl ms1)
      get_proc mx = get_proc (hd ms2)
      m  set (tl (tl ms1)). m'. call_of_return_node m m'  m'  HRB_slice SCFG
      m  set (tl (tl ms1)). return_node m
      i<length ms1'. snd (s1' ! i) = snd (transfer (slice_kind S a) s2 ! i)
    have "((ms1',s1'),(ms1',transfer (slice_kind S a) s2))  WS S"
      by(auto intro!:WSI)
    with S,slice_kind S  (ms2,s2) =as@[a] (ms1',transfer (slice_kind S a) s2)
    show ?case by blast
  qed
qed



subsection ‹The weak simulation›

definition is_weak_sim :: 
  "(('node list × (('var  'val) × 'ret) list) × 
  ('node list × (('var  'val) × 'ret) list)) set  'node SDG_node set  bool"
  where "is_weak_sim R S  
  ms1 s1 ms2 s2 ms1' s1' as. 
    ((ms1,s1),(ms2,s2))  R  S,kind  (ms1,s1) =as (ms1',s1')  s1'  []
     (ms2' s2' as'. ((ms1',s1'),(ms2',s2'))  R  
                        S,slice_kind S  (ms2,s2) =as' (ms2',s2'))"


lemma WS_weak_sim:
  assumes "((ms1,s1),(ms2,s2))  WS S" 
  and "S,kind  (ms1,s1) =as (ms1',s1')" and "s1'  []"
  obtains as' where "((ms1',s1'),(ms1',transfer (slice_kind S (last as)) s2))  WS S"
  and "S,slice_kind S  (ms2,s2) =as'@[last as] 
                          (ms1',transfer (slice_kind S (last as)) s2)"
proof(atomize_elim)
  from S,kind  (ms1,s1) =as (ms1',s1') obtain ms' s' as' a'
    where "S,kind  (ms1,s1) =as'τ (ms',s')"
    and "S,kind  (ms',s') -a' (ms1',s1')" and "as = as'@[a']"
    by(fastforce elim:observable_moves.cases)
  from S,kind  (ms',s') -a' (ms1',s1')
  have "m  set (tl ms'). m'. call_of_return_node m m'  m'  HRB_slice SCFG"
    and "n  set (tl ms'). return_node n" and "ms'  []"
    by(auto elim:observable_move.cases simp:call_of_return_node_def)
  from S,kind  (ms1,s1) =as'τ (ms',s') ((ms1,s1),(ms2,s2))  WS S
  have "((ms',s'),(ms2,s2))  WS S" by(rule WS_silent_moves)
  with S,kind  (ms',s') -a' (ms1',s1') s1'  []
  obtain as'' where "((ms1',s1'),(ms1',transfer (slice_kind S a') s2))  WS S"
    and "S,slice_kind S  (ms2,s2) =as''@[a'] 
    (ms1',transfer (slice_kind S a') s2)"
    by(fastforce elim:WS_observable_move)
  with ((ms1',s1'),(ms1',transfer (slice_kind S a') s2))  WS S as = as'@[a']
  show "as'. ((ms1',s1'),(ms1',transfer (slice_kind S (last as)) s2))  WS S 
    S,slice_kind S  (ms2,s2) =as'@[last as] 
    (ms1',transfer (slice_kind S (last as)) s2)"
    by fastforce
qed



text ‹The following lemma states the correctness of static intraprocedural slicing:\\
  the simulation WS S› is a desired weak simulation›

theorem WS_is_weak_sim:"is_weak_sim (WS S) S"
by(fastforce elim:WS_weak_sim simp:is_weak_sim_def)

end

end