Theory HRBSlice

section ‹Horwitz-Reps-Binkley Slice›

theory HRBSlice imports SDG begin

context SDG begin

subsection ‹Set describing phase 1 of the two-phase slicer›

inductive_set sum_SDG_slice1 :: "'node SDG_node ⇒ 'node SDG_node set"
  for n::"'node SDG_node"
  where refl_slice1:"valid_SDG_node n ⟹ n ∈ sum_SDG_slice1 n"
  | cdep_slice1:
  "⟦n'' s⟶⇘cd⇙ n'; n' ∈ sum_SDG_slice1 n⟧ ⟹ n'' ∈ sum_SDG_slice1 n"
  | ddep_slice1: 
  "⟦n'' s-V→⇩d⇩d n'; n' ∈ sum_SDG_slice1 n⟧ ⟹ n'' ∈ sum_SDG_slice1 n"
  | call_slice1:
  "⟦n'' s-p→⇘call⇙ n'; n' ∈ sum_SDG_slice1 n⟧ ⟹ n'' ∈ sum_SDG_slice1 n"
  | param_in_slice1: 
  "⟦n'' s-p:V→⇘in⇙ n'; n' ∈ sum_SDG_slice1 n⟧ ⟹ n'' ∈ sum_SDG_slice1 n"
  | sum_slice1:
  "⟦n'' s-p→⇘sum⇙ n'; n' ∈ sum_SDG_slice1 n⟧ ⟹ n'' ∈ sum_SDG_slice1 n"


lemma slice1_cdep_slice1:
  "⟦nx ∈ sum_SDG_slice1 n; n s⟶⇘cd⇙ n'⟧ ⟹ nx ∈ sum_SDG_slice1 n'"
by(induct rule:sum_SDG_slice1.induct,
   auto intro:sum_SDG_slice1.intros sum_SDG_edge_valid_SDG_node)

lemma slice1_ddep_slice1:
  "⟦nx ∈ sum_SDG_slice1 n; n s-V→⇩d⇩d n'⟧ ⟹ nx ∈ sum_SDG_slice1 n'"
by(induct rule:sum_SDG_slice1.induct,
   auto intro:sum_SDG_slice1.intros sum_SDG_edge_valid_SDG_node)

lemma slice1_sum_slice1:
  "⟦nx ∈ sum_SDG_slice1 n; n s-p→⇘sum⇙ n'⟧ ⟹ nx ∈ sum_SDG_slice1 n'"
by(induct rule:sum_SDG_slice1.induct,
   auto intro:sum_SDG_slice1.intros sum_SDG_edge_valid_SDG_node)

lemma slice1_call_slice1:
  "⟦nx ∈ sum_SDG_slice1 n; n s-p→⇘call⇙ n'⟧ ⟹ nx ∈ sum_SDG_slice1 n'"
by(induct rule:sum_SDG_slice1.induct,
   auto intro:sum_SDG_slice1.intros sum_SDG_edge_valid_SDG_node)

lemma slice1_param_in_slice1:
  "⟦nx ∈ sum_SDG_slice1 n; n s-p:V→⇘in⇙ n'⟧ ⟹ nx ∈ sum_SDG_slice1 n'"
by(induct rule:sum_SDG_slice1.induct,
   auto intro:sum_SDG_slice1.intros sum_SDG_edge_valid_SDG_node)


lemma is_SDG_path_slice1:
  "⟦n is-ns→⇩d* n'; n' ∈ sum_SDG_slice1 n''⟧ ⟹ n ∈ sum_SDG_slice1 n''"
proof(induct rule:intra_sum_SDG_path.induct)
  case isSp_Nil thus ?case by simp
next
  case (isSp_Append_cdep n ns nx n')
  note IH = ‹nx ∈ sum_SDG_slice1 n'' ⟹ n ∈ sum_SDG_slice1 n''›
  from ‹nx s⟶⇘cd⇙ n'› ‹n' ∈ sum_SDG_slice1 n''›
  have "nx ∈ sum_SDG_slice1 n''" by(rule cdep_slice1)
  from IH[OF this] show ?case .
next
  case (isSp_Append_ddep n ns nx V n')
  note IH = ‹nx ∈ sum_SDG_slice1 n'' ⟹ n ∈ sum_SDG_slice1 n''›
  from ‹nx s-V→⇩d⇩d n'› ‹n' ∈ sum_SDG_slice1 n''›
  have "nx ∈ sum_SDG_slice1 n''" by(rule ddep_slice1)
  from IH[OF this] show ?case .
next
  case (isSp_Append_sum n ns nx p n')
  note IH = ‹nx ∈ sum_SDG_slice1 n'' ⟹ n ∈ sum_SDG_slice1 n''›
  from ‹nx s-p→⇘sum⇙ n'› ‹n' ∈ sum_SDG_slice1 n''›
  have "nx ∈ sum_SDG_slice1 n''" by(rule sum_slice1)
  from IH[OF this] show ?case .
qed


subsection ‹Set describing phase 2 of the two-phase slicer›

inductive_set sum_SDG_slice2 :: "'node SDG_node ⇒ 'node SDG_node set"
  for n::"'node SDG_node"
  where refl_slice2:"valid_SDG_node n ⟹ n ∈ sum_SDG_slice2 n"
  | cdep_slice2:
  "⟦n'' s⟶⇘cd⇙ n'; n' ∈ sum_SDG_slice2 n⟧ ⟹ n'' ∈ sum_SDG_slice2 n"
  | ddep_slice2: 
  "⟦n'' s-V→⇩d⇩d n'; n' ∈ sum_SDG_slice2 n⟧ ⟹ n'' ∈ sum_SDG_slice2 n"
  | return_slice2:
  "⟦n'' s-p→⇘ret⇙ n'; n' ∈ sum_SDG_slice2 n⟧ ⟹ n'' ∈ sum_SDG_slice2 n"
  | param_out_slice2: 
  "⟦n'' s-p:V→⇘out⇙ n'; n' ∈ sum_SDG_slice2 n⟧ ⟹ n'' ∈ sum_SDG_slice2 n"
  | sum_slice2:
  "⟦n'' s-p→⇘sum⇙ n'; n' ∈ sum_SDG_slice2 n⟧ ⟹ n'' ∈ sum_SDG_slice2 n"


lemma slice2_cdep_slice2:
  "⟦nx ∈ sum_SDG_slice2 n; n s⟶⇘cd⇙ n'⟧ ⟹ nx ∈ sum_SDG_slice2 n'"
by(induct rule:sum_SDG_slice2.induct,
   auto intro:sum_SDG_slice2.intros sum_SDG_edge_valid_SDG_node)

lemma slice2_ddep_slice2:
  "⟦nx ∈ sum_SDG_slice2 n; n s-V→⇩d⇩d n'⟧ ⟹ nx ∈ sum_SDG_slice2 n'"
by(induct rule:sum_SDG_slice2.induct,
   auto intro:sum_SDG_slice2.intros sum_SDG_edge_valid_SDG_node)

lemma slice2_sum_slice2:
  "⟦nx ∈ sum_SDG_slice2 n; n s-p→⇘sum⇙ n'⟧ ⟹ nx ∈ sum_SDG_slice2 n'"
by(induct rule:sum_SDG_slice2.induct,
   auto intro:sum_SDG_slice2.intros sum_SDG_edge_valid_SDG_node)

lemma slice2_ret_slice2:
  "⟦nx ∈ sum_SDG_slice2 n; n s-p→⇘ret⇙ n'⟧ ⟹ nx ∈ sum_SDG_slice2 n'"
by(induct rule:sum_SDG_slice2.induct,
   auto intro:sum_SDG_slice2.intros sum_SDG_edge_valid_SDG_node)

lemma slice2_param_out_slice2:
  "⟦nx ∈ sum_SDG_slice2 n; n s-p:V→⇘out⇙ n'⟧ ⟹ nx ∈ sum_SDG_slice2 n'"
by(induct rule:sum_SDG_slice2.induct,
   auto intro:sum_SDG_slice2.intros sum_SDG_edge_valid_SDG_node)


lemma is_SDG_path_slice2:
  "⟦n is-ns→⇩d* n'; n' ∈ sum_SDG_slice2 n''⟧ ⟹ n ∈ sum_SDG_slice2 n''"
proof(induct rule:intra_sum_SDG_path.induct)
  case isSp_Nil thus ?case by simp
next
  case (isSp_Append_cdep n ns nx n')
  note IH = ‹nx ∈ sum_SDG_slice2 n'' ⟹ n ∈ sum_SDG_slice2 n''›
  from ‹nx s⟶⇘cd⇙ n'› ‹n' ∈ sum_SDG_slice2 n''›
  have "nx ∈ sum_SDG_slice2 n''" by(rule cdep_slice2)
  from IH[OF this] show ?case .
next
  case (isSp_Append_ddep n ns nx V n')
  note IH = ‹nx ∈ sum_SDG_slice2 n'' ⟹ n ∈ sum_SDG_slice2 n''›
  from ‹nx s-V→⇩d⇩d n'› ‹n' ∈ sum_SDG_slice2 n''›
  have "nx ∈ sum_SDG_slice2 n''" by(rule ddep_slice2)
  from IH[OF this] show ?case .
next
  case (isSp_Append_sum n ns nx p n')
  note IH = ‹nx ∈ sum_SDG_slice2 n'' ⟹ n ∈ sum_SDG_slice2 n''›
  from ‹nx s-p→⇘sum⇙ n'› ‹n' ∈ sum_SDG_slice2 n''›
  have "nx ∈ sum_SDG_slice2 n''" by(rule sum_slice2)
  from IH[OF this] show ?case .
qed



lemma slice2_is_SDG_path_slice2: 
  "⟦n is-ns→⇩d* n'; n'' ∈ sum_SDG_slice2 n⟧ ⟹ n'' ∈ sum_SDG_slice2 n'"
proof(induct rule:intra_sum_SDG_path.induct)
  case isSp_Nil thus ?case by simp
next
  case (isSp_Append_cdep n ns nx n')
  from ‹n'' ∈ sum_SDG_slice2 n ⟹ n'' ∈ sum_SDG_slice2 nx› ‹n'' ∈ sum_SDG_slice2 n›
  have "n'' ∈ sum_SDG_slice2 nx" .
  with ‹nx s⟶⇘cd⇙ n'› show ?case by -(rule slice2_cdep_slice2)
next
  case (isSp_Append_ddep n ns nx V n')
  from ‹n'' ∈ sum_SDG_slice2 n ⟹ n'' ∈ sum_SDG_slice2 nx› ‹n'' ∈ sum_SDG_slice2 n›
  have "n'' ∈ sum_SDG_slice2 nx" .
  with ‹nx s-V→⇩d⇩d n'› show ?case by -(rule slice2_ddep_slice2)
next
  case (isSp_Append_sum n ns nx p n')
  from ‹n'' ∈ sum_SDG_slice2 n ⟹ n'' ∈ sum_SDG_slice2 nx› ‹n'' ∈ sum_SDG_slice2 n›
  have "n'' ∈ sum_SDG_slice2 nx" .
  with ‹nx s-p→⇘sum⇙ n'› show ?case by -(rule slice2_sum_slice2)
qed


subsection ‹The backward slice using the Horwitz-Reps-Binkley slicer›

text ‹Note: our slicing criterion is a set of nodes, not a unique node.›

inductive_set combine_SDG_slices :: "'node SDG_node set ⇒ 'node SDG_node set"
  for S::"'node SDG_node set"
  where combSlice_refl:"n ∈ S ⟹ n ∈ combine_SDG_slices S" 
  | combSlice_Return_parent_node:
  "⟦n' ∈ S; n'' s-p→⇘ret⇙ CFG_node (parent_node n'); n ∈ sum_SDG_slice2 n'⟧ 
  ⟹ n ∈ combine_SDG_slices S"


definition HRB_slice :: "'node SDG_node set ⇒ 'node SDG_node set"
  where "HRB_slice S ≡ {n'. ∃n ∈ S. n' ∈ combine_SDG_slices (sum_SDG_slice1 n)}"


lemma HRB_slice_cases[consumes 1,case_names phase1 phase2]:
  "⟦x ∈ HRB_slice S; ⋀n nx. ⟦n ∈ sum_SDG_slice1 nx; nx ∈ S⟧ ⟹ P n;
   ⋀nx n' n'' p n. ⟦n' ∈ sum_SDG_slice1 nx; n'' s-p→⇘ret⇙ CFG_node (parent_node n'); 
                    n ∈ sum_SDG_slice2 n'; nx ∈ S⟧ ⟹ P n⟧
  ⟹ P x"
  by(fastforce elim:combine_SDG_slices.cases simp:HRB_slice_def)



lemma HRB_slice_refl:
  assumes "valid_node m" and "CFG_node m ∈ S" shows "CFG_node m ∈ HRB_slice S"
proof -
  from ‹valid_node m› have "CFG_node m ∈ sum_SDG_slice1 (CFG_node m)"
    by(fastforce intro:refl_slice1)
  with ‹CFG_node m ∈ S› show ?thesis
    by(simp add:HRB_slice_def)(blast intro:combSlice_refl)
qed


lemma HRB_slice_valid_node: "n ∈ HRB_slice S ⟹ valid_SDG_node n"
proof(induct rule:HRB_slice_cases)
  case (phase1 n nx) thus ?case
    by(induct rule:sum_SDG_slice1.induct,auto intro:sum_SDG_edge_valid_SDG_node)
next
  case (phase2 nx n' n'' p n)
  from ‹n ∈ sum_SDG_slice2 n'›
  show ?case
    by(induct rule:sum_SDG_slice2.induct,auto intro:sum_SDG_edge_valid_SDG_node)
qed


lemma valid_SDG_node_in_slice_parent_node_in_slice:
  assumes "n ∈ HRB_slice S" shows "CFG_node (parent_node n) ∈ HRB_slice S"
proof -
  from ‹n ∈ HRB_slice S› have "valid_SDG_node n" by(rule HRB_slice_valid_node)
  hence "n = CFG_node (parent_node n) ∨ CFG_node (parent_node n) ⟶⇘cd⇙ n"
    by(rule valid_SDG_node_cases)
  thus ?thesis
  proof
    assume "n = CFG_node (parent_node n)"
    with ‹n ∈ HRB_slice S› show ?thesis by simp
  next
    assume "CFG_node (parent_node n) ⟶⇘cd⇙ n"
    hence "CFG_node (parent_node n) s⟶⇘cd⇙ n" by(rule SDG_edge_sum_SDG_edge)
    with ‹n ∈ HRB_slice S› show ?thesis
      by(fastforce elim:combine_SDG_slices.cases 
                 intro:combine_SDG_slices.intros cdep_slice1 cdep_slice2 
                  simp:HRB_slice_def)
  qed
qed


lemma HRB_slice_is_SDG_path_HRB_slice: 
  "⟦n is-ns→⇩d* n'; n'' ∈ HRB_slice {n}; n' ∈ S⟧ ⟹ n'' ∈ HRB_slice S"
proof(induct arbitrary:S rule:intra_sum_SDG_path.induct)
  case (isSp_Nil n) thus ?case by(fastforce simp:HRB_slice_def)
next
  case (isSp_Append_cdep n ns nx n')
  note IH = ‹⋀S. ⟦n'' ∈ HRB_slice {n}; nx ∈ S⟧ ⟹ n'' ∈ HRB_slice S›
  from IH[OF ‹n'' ∈ HRB_slice {n}›] have "n'' ∈ HRB_slice {nx}" by simp
  thus ?case
  proof(induct rule:HRB_slice_cases)
    case (phase1 n nx') 
    from ‹nx' ∈ {nx}› have "nx' = nx" by simp
    with ‹n ∈ sum_SDG_slice1 nx'› ‹nx s⟶⇘cd⇙ n'› have "n ∈ sum_SDG_slice1 n'"
      by(fastforce intro:slice1_cdep_slice1)
    with ‹n' ∈ S› show ?case
      by(fastforce intro:combine_SDG_slices.combSlice_refl simp:HRB_slice_def)
  next
    case (phase2 nx'' nx' n'' p n)
    from ‹nx'' ∈ {nx}› have "nx'' = nx" by simp
    with ‹nx' ∈ sum_SDG_slice1 nx''› ‹nx s⟶⇘cd⇙ n'› have "nx' ∈ sum_SDG_slice1 n'"
      by(fastforce intro:slice1_cdep_slice1)
    with ‹n'' s-p→⇘ret⇙ CFG_node (parent_node nx')› ‹n ∈ sum_SDG_slice2 nx'› ‹n' ∈ S›
    show ?case by(fastforce intro:combine_SDG_slices.combSlice_Return_parent_node 
                            simp:HRB_slice_def)
  qed
next
  case (isSp_Append_ddep n ns nx V n')
  note IH = ‹⋀S. ⟦n'' ∈ HRB_slice {n}; nx ∈ S⟧ ⟹ n'' ∈ HRB_slice S›
  from IH[OF ‹n'' ∈ HRB_slice {n}›] have "n'' ∈ HRB_slice {nx}" by simp
  thus ?case
  proof(induct rule:HRB_slice_cases)
    case (phase1 n nx') 
    from ‹nx' ∈ {nx}› have "nx' = nx" by simp
    with ‹n ∈ sum_SDG_slice1 nx'› ‹nx s-V→⇩d⇩d n'› have "n ∈ sum_SDG_slice1 n'"
      by(fastforce intro:slice1_ddep_slice1)
    with ‹n' ∈ S› show ?case
      by(fastforce intro:combine_SDG_slices.combSlice_refl simp:HRB_slice_def)
  next
    case (phase2 nx'' nx' n'' p n)
    from ‹nx'' ∈ {nx}› have "nx'' = nx" by simp
    with ‹nx' ∈ sum_SDG_slice1 nx''› ‹nx s-V→⇩d⇩d n'› have "nx' ∈ sum_SDG_slice1 n'"
      by(fastforce intro:slice1_ddep_slice1)
    with ‹n'' s-p→⇘ret⇙ CFG_node (parent_node nx')› ‹n ∈ sum_SDG_slice2 nx'› ‹n' ∈ S›
    show ?case by(fastforce intro:combine_SDG_slices.combSlice_Return_parent_node 
                            simp:HRB_slice_def)
  qed
next
  case (isSp_Append_sum n ns nx p n')
  note IH = ‹⋀S. ⟦n'' ∈ HRB_slice {n}; nx ∈ S⟧ ⟹ n'' ∈ HRB_slice S›
  from IH[OF ‹n'' ∈ HRB_slice {n}›] have "n'' ∈ HRB_slice {nx}" by simp
  thus ?case
  proof(induct rule:HRB_slice_cases)
    case (phase1 n nx') 
    from ‹nx' ∈ {nx}› have "nx' = nx" by simp
    with ‹n ∈ sum_SDG_slice1 nx'› ‹nx s-p→⇘sum⇙ n'› have "n ∈ sum_SDG_slice1 n'"
      by(fastforce intro:slice1_sum_slice1)
    with ‹n' ∈ S› show ?case
      by(fastforce intro:combine_SDG_slices.combSlice_refl simp:HRB_slice_def)
  next
    case (phase2 nx'' nx' n'' p' n)
    from ‹nx'' ∈ {nx}› have "nx'' = nx" by simp
    with ‹nx' ∈ sum_SDG_slice1 nx''› ‹nx s-p→⇘sum⇙ n'› have "nx' ∈ sum_SDG_slice1 n'"
      by(fastforce intro:slice1_sum_slice1)
    with ‹n'' s-p'→⇘ret⇙ CFG_node (parent_node nx')› ‹n ∈ sum_SDG_slice2 nx'› ‹n' ∈ S›
    show ?case by(fastforce intro:combine_SDG_slices.combSlice_Return_parent_node 
                            simp:HRB_slice_def)
  qed
qed


lemma call_return_nodes_in_slice:
  assumes "valid_edge a" and "kind a = Q↩⇘p⇙f"
  and "valid_edge a'" and "kind a' = Q':r'↪⇘p⇙fs'" and "a ∈ get_return_edges a'"
  and "CFG_node (targetnode a) ∈ HRB_slice S"
  shows "CFG_node (sourcenode a) ∈ HRB_slice S"
  and "CFG_node (sourcenode a') ∈ HRB_slice S" 
  and "CFG_node (targetnode a') ∈ HRB_slice S"
proof -
  from ‹valid_edge a'› ‹kind a' = Q':r'↪⇘p⇙fs'› ‹a ∈ get_return_edges a'›
  have "CFG_node (sourcenode a') s-p→⇘sum⇙ CFG_node (targetnode a)"
    by(fastforce intro:sum_SDG_call_summary_edge)
  with ‹CFG_node (targetnode a) ∈ HRB_slice S›
  show "CFG_node (sourcenode a') ∈ HRB_slice S"
    by(fastforce elim!:combine_SDG_slices.cases 
                intro:combine_SDG_slices.intros sum_slice1 sum_slice2 
                 simp:HRB_slice_def)
  from ‹CFG_node (targetnode a) ∈ HRB_slice S›
  obtain n⇩c where "CFG_node (targetnode a) ∈ combine_SDG_slices (sum_SDG_slice1 n⇩c)"
    and "n⇩c ∈ S"
    by(simp add:HRB_slice_def) blast
  thus "CFG_node (sourcenode a) ∈ HRB_slice S"
  proof(induct "CFG_node (targetnode a)" rule:combine_SDG_slices.induct)
    case combSlice_refl
    from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f›
    have "CFG_node (sourcenode a) s-p→⇘ret⇙ CFG_node (targetnode a)"
      by(fastforce intro:sum_SDG_return_edge)
    with ‹valid_edge a› 
    have "CFG_node (sourcenode a) ∈ sum_SDG_slice2 (CFG_node (targetnode a))"
      by(fastforce intro:sum_SDG_slice2.intros)
    with ‹CFG_node (targetnode a) ∈ sum_SDG_slice1 n⇩c› ‹n⇩c ∈ S›
      ‹CFG_node (sourcenode a) s-p→⇘ret⇙ CFG_node (targetnode a)›
    show ?case by(fastforce intro:combSlice_Return_parent_node simp:HRB_slice_def)
  next
    case (combSlice_Return_parent_node n' n'' p')
    from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f›
    have "CFG_node (sourcenode a) s-p→⇘ret⇙ CFG_node (targetnode a)"
      by(fastforce intro:sum_SDG_return_edge)
    with ‹CFG_node (targetnode a) ∈ sum_SDG_slice2 n'›
    have "CFG_node (sourcenode a) ∈ sum_SDG_slice2 n'"
      by(fastforce intro:sum_SDG_slice2.intros)
    with ‹n' ∈ sum_SDG_slice1 n⇩c› ‹n'' s-p'→⇘ret⇙ CFG_node (parent_node n')› ‹n⇩c ∈ 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':r'↪⇘p⇙fs'› ‹a ∈ get_return_edges a'›
  have "CFG_node (targetnode a') s⟶⇘cd⇙ CFG_node (sourcenode a)"
    by(fastforce intro:sum_SDG_proc_entry_exit_cdep)
  with ‹CFG_node (sourcenode a) ∈ HRB_slice S› ‹n⇩c ∈ S›
  show "CFG_node (targetnode a') ∈ HRB_slice S"
    by(fastforce elim!:combine_SDG_slices.cases 
                intro:combine_SDG_slices.intros cdep_slice1 cdep_slice2 
                 simp:HRB_slice_def)
qed



subsection ‹Proof of Precision›


lemma in_intra_SDG_path_in_slice2:
  "⟦n i-ns→⇩d* n'; n'' ∈ set ns⟧ ⟹ n'' ∈ sum_SDG_slice2 n'"
proof(induct rule:intra_SDG_path.induct)
  case iSp_Nil thus ?case by simp
next
  case (iSp_Append_cdep n ns nx n')
  note IH = ‹n'' ∈ set ns ⟹ n'' ∈ sum_SDG_slice2 nx›
  from ‹n'' ∈ set (ns@[nx])› have "n'' ∈ set ns ∨ n'' = nx" by auto
  thus ?case
  proof
    assume "n'' ∈ set ns"
    from IH[OF this] have "n'' ∈ sum_SDG_slice2 nx" by simp
    with ‹nx ⟶⇘cd⇙ n'› show ?thesis
      by(fastforce intro:slice2_cdep_slice2 SDG_edge_sum_SDG_edge)
  next
    assume "n'' = nx"
    from ‹nx ⟶⇘cd⇙ n'› have "valid_SDG_node n'" by(rule SDG_edge_valid_SDG_node)
    hence "n' ∈ sum_SDG_slice2 n'" by(rule refl_slice2)
    with ‹nx ⟶⇘cd⇙ n'› have "nx ∈ sum_SDG_slice2 n'"
      by(fastforce intro:cdep_slice2 SDG_edge_sum_SDG_edge)
    with ‹n'' = nx› show ?thesis by simp
  qed
next
  case (iSp_Append_ddep n ns nx V n')
  note IH = ‹n'' ∈ set ns ⟹ n'' ∈ sum_SDG_slice2 nx›
  from ‹n'' ∈ set (ns@[nx])› have "n'' ∈ set ns ∨ n'' = nx" by auto
  thus ?case
  proof
    assume "n'' ∈ set ns"
    from IH[OF this] have "n'' ∈ sum_SDG_slice2 nx" by simp
    with ‹nx -V→⇩d⇩d n'› show ?thesis
      by(fastforce intro:slice2_ddep_slice2 SDG_edge_sum_SDG_edge)
  next
    assume "n'' = nx"
    from ‹nx -V→⇩d⇩d n'› have "valid_SDG_node n'" by(rule SDG_edge_valid_SDG_node)
    hence "n' ∈ sum_SDG_slice2 n'" by(rule refl_slice2)
    with ‹nx -V→⇩d⇩d n'› have "nx ∈ sum_SDG_slice2 n'"
      by(fastforce intro:ddep_slice2 SDG_edge_sum_SDG_edge)
    with ‹n'' = nx› show ?thesis by simp
  qed
qed


lemma in_intra_SDG_path_in_HRB_slice:
  "⟦n i-ns→⇩d* n'; n'' ∈ set ns; n' ∈ S⟧ ⟹ n'' ∈ HRB_slice S"
proof(induct arbitrary:S rule:intra_SDG_path.induct)
  case iSp_Nil thus ?case by simp
next
  case (iSp_Append_cdep n ns nx n')
  note IH = ‹⋀S. ⟦n'' ∈ set ns; nx ∈ S⟧ ⟹ n'' ∈ HRB_slice S›
  from ‹n'' ∈ set (ns@[nx])› have "n'' ∈ set ns ∨ n'' = nx" by auto
  thus ?case
  proof
    assume "n'' ∈ set ns"
    from IH[OF ‹n'' ∈ set ns›] have "n'' ∈ HRB_slice {nx}" by simp
    from this ‹nx ⟶⇘cd⇙ n'› ‹n' ∈ S› show ?case
      by(fastforce elim:HRB_slice_cases slice1_cdep_slice1
        intro:bexI[where x="n'"] combine_SDG_slices.intros SDG_edge_sum_SDG_edge 
        simp:HRB_slice_def)
  next
    assume "n'' = nx"
    from ‹nx ⟶⇘cd⇙ n'› have "valid_SDG_node n'" by(rule SDG_edge_valid_SDG_node)
    hence "n' ∈ sum_SDG_slice1 n'" by(rule refl_slice1)
    with ‹nx ⟶⇘cd⇙ n'› have "nx ∈ sum_SDG_slice1 n'" 
      by(fastforce intro:cdep_slice1 SDG_edge_sum_SDG_edge)
    with ‹n'' = nx› ‹n' ∈ S› show ?case
      by(fastforce intro:combSlice_refl simp:HRB_slice_def)
  qed
next
  case (iSp_Append_ddep n ns nx V n')
  note IH = ‹⋀S. ⟦n'' ∈ set ns; nx ∈ S⟧ ⟹ n'' ∈ HRB_slice S›
  from ‹n'' ∈ set (ns@[nx])› have "n'' ∈ set ns ∨ n'' = nx" by auto
  thus ?case
  proof
    assume "n'' ∈ set ns"
    from IH[OF ‹n'' ∈ set ns›] have "n'' ∈ HRB_slice {nx}" by simp
    from this ‹nx -V→⇩d⇩d n'› ‹n' ∈ S› show ?case
      by(fastforce elim:HRB_slice_cases slice1_ddep_slice1
        intro:bexI[where x="n'"] combine_SDG_slices.intros SDG_edge_sum_SDG_edge 
        simp:HRB_slice_def)
  next
    assume "n'' = nx"
    from ‹nx -V→⇩d⇩d n'› have "valid_SDG_node n'" by(rule SDG_edge_valid_SDG_node)
    hence "n' ∈ sum_SDG_slice1 n'" by(rule refl_slice1)
    with ‹nx -V→⇩d⇩d n'› have "nx ∈ sum_SDG_slice1 n'" 
      by(fastforce intro:ddep_slice1 SDG_edge_sum_SDG_edge)
    with ‹n'' = nx› ‹n' ∈ S› show ?case 
      by(fastforce intro:combSlice_refl simp:HRB_slice_def)
  qed
qed


lemma in_matched_in_slice2:
  "⟦matched n ns n'; n'' ∈ set ns⟧ ⟹ n'' ∈ sum_SDG_slice2 n'"
proof(induct rule:matched.induct)
  case matched_Nil thus ?case by simp
next
  case (matched_Append_intra_SDG_path n ns nx ns' n')
  note IH = ‹n'' ∈ set ns ⟹ n'' ∈ sum_SDG_slice2 nx›
  from ‹n'' ∈ set (ns@ns')› have "n'' ∈ set ns ∨ n'' ∈ set ns'" by simp
  thus ?case
  proof
    assume "n'' ∈ set ns"
    from IH[OF this] have "n'' ∈ sum_SDG_slice2 nx" .
    with ‹nx i-ns'→⇩d* n'› show ?thesis
      by(fastforce intro:slice2_is_SDG_path_slice2 
                        intra_SDG_path_is_SDG_path)
  next
    assume "n'' ∈ set ns'"
    with ‹nx i-ns'→⇩d* n'› show ?case by(rule in_intra_SDG_path_in_slice2)
  qed
next
  case (matched_bracket_call n⇩0 ns n⇩1 p n⇩2 ns' n⇩3 n⇩4 V a a')
  note IH1 = ‹n'' ∈ set ns ⟹ n'' ∈ sum_SDG_slice2 n⇩1›
  note IH2 = ‹n'' ∈ set ns' ⟹ n'' ∈ sum_SDG_slice2 n⇩3›
  from ‹n⇩1 -p→⇘call⇙ n⇩2› ‹matched n⇩2 ns' n⇩3› ‹n⇩3 -p→⇘ret⇙ n⇩4 ∨ n⇩3 -p:V→⇘out⇙ n⇩4› 
    ‹a' ∈ get_return_edges a› ‹valid_edge a›
    ‹sourcenode a = parent_node n⇩1› ‹targetnode a = parent_node n⇩2›
    ‹sourcenode a' = parent_node n⇩3› ‹targetnode a' = parent_node n⇩4›
  have "matched n⇩1 ([]@n⇩1#ns'@[n⇩3]) n⇩4"
    by(fastforce intro:matched.matched_bracket_call matched_Nil 
                 elim:SDG_edge_valid_SDG_node)
  then obtain nsx where "n⇩1 is-nsx→⇩d* n⇩4" by(erule matched_is_SDG_path)
  from ‹n'' ∈ set (ns@n⇩1#ns'@[n⇩3])› 
  have "((n'' ∈ set ns ∨ n'' = n⇩1) ∨ n'' ∈ set ns') ∨ n'' = n⇩3" by auto
  thus ?case apply -
  proof(erule disjE)+
    assume "n'' ∈ set ns"
    from IH1[OF this] have "n'' ∈ sum_SDG_slice2 n⇩1" .
    with ‹n⇩1 is-nsx→⇩d* n⇩4› show ?thesis 
      by -(rule slice2_is_SDG_path_slice2)
  next
    assume "n'' = n⇩1"
    from ‹n⇩1 is-nsx→⇩d* n⇩4› have "n⇩1 ∈ sum_SDG_slice2 n⇩4" 
      by(fastforce intro:is_SDG_path_slice2 refl_slice2 is_SDG_path_valid_SDG_node)
    with ‹n'' = n⇩1› show ?thesis by(fastforce intro:combSlice_refl simp:HRB_slice_def)
  next
    assume "n'' ∈ set ns'"
    from IH2[OF this] have "n'' ∈ sum_SDG_slice2 n⇩3" .
    with ‹n⇩3 -p→⇘ret⇙ n⇩4 ∨ n⇩3 -p:V→⇘out⇙ n⇩4› show ?thesis 
      by(fastforce intro:slice2_ret_slice2 slice2_param_out_slice2 
                        SDG_edge_sum_SDG_edge)
  next
    assume "n'' = n⇩3"
    from ‹n⇩3 -p→⇘ret⇙ n⇩4 ∨ n⇩3 -p:V→⇘out⇙ n⇩4› have "n⇩3 s-p→⇘ret⇙ n⇩4 ∨ n⇩3 s-p:V→⇘out⇙ n⇩4" 
      by(fastforce intro:SDG_edge_sum_SDG_edge)
    hence "n⇩3 ∈ sum_SDG_slice2 n⇩4"
      by(fastforce intro:return_slice2 param_out_slice2 refl_slice2 
                        sum_SDG_edge_valid_SDG_node)
    with ‹n'' = n⇩3› show ?thesis by simp
  qed
next
  case (matched_bracket_param n⇩0 ns n⇩1 p V n⇩2 ns' n⇩3 V' n⇩4 a a')
  note IH1 = ‹n'' ∈ set ns ⟹ n'' ∈ sum_SDG_slice2 n⇩1›
  note IH2 = ‹n'' ∈ set ns' ⟹ n'' ∈ sum_SDG_slice2 n⇩3›
  from ‹n⇩1 -p:V→⇘in⇙ n⇩2› ‹matched n⇩2 ns' n⇩3› ‹n⇩3 -p:V'→⇘out⇙ n⇩4› 
    ‹a' ∈ get_return_edges a› ‹valid_edge a›
    ‹sourcenode a = parent_node n⇩1› ‹targetnode a = parent_node n⇩2›
    ‹sourcenode a' = parent_node n⇩3› ‹targetnode a' = parent_node n⇩4›
  have "matched n⇩1 ([]@n⇩1#ns'@[n⇩3]) n⇩4"
    by(fastforce intro:matched.matched_bracket_param matched_Nil 
                 elim:SDG_edge_valid_SDG_node)
  then obtain nsx where "n⇩1 is-nsx→⇩d* n⇩4" by(erule matched_is_SDG_path)
  from ‹n'' ∈ set (ns@n⇩1#ns'@[n⇩3])› 
  have "((n'' ∈ set ns ∨ n'' = n⇩1) ∨ n'' ∈ set ns') ∨ n'' = n⇩3" by auto
  thus ?case apply -
  proof(erule disjE)+
    assume "n'' ∈ set ns"
    from IH1[OF this] have "n'' ∈ sum_SDG_slice2 n⇩1" .
    with ‹n⇩1 is-nsx→⇩d* n⇩4› show ?thesis 
      by -(rule slice2_is_SDG_path_slice2)
  next
    assume "n'' = n⇩1"
    from ‹n⇩1 is-nsx→⇩d* n⇩4› have "n⇩1 ∈ sum_SDG_slice2 n⇩4" 
      by(fastforce intro:is_SDG_path_slice2 refl_slice2 is_SDG_path_valid_SDG_node)
    with ‹n'' = n⇩1› show ?thesis by(fastforce intro:combSlice_refl simp:HRB_slice_def)
  next
    assume "n'' ∈ set ns'"
    from IH2[OF this] have "n'' ∈ sum_SDG_slice2 n⇩3" .
    with ‹n⇩3 -p:V'→⇘out⇙ n⇩4› show ?thesis 
      by(fastforce intro:slice2_param_out_slice2 SDG_edge_sum_SDG_edge)
  next
    assume "n'' = n⇩3"
    from ‹n⇩3 -p:V'→⇘out⇙ n⇩4› have "n⇩3 s-p:V'→⇘out⇙ n⇩4" by(rule SDG_edge_sum_SDG_edge)
    hence "n⇩3 ∈ sum_SDG_slice2 n⇩4"
      by(fastforce intro:param_out_slice2 refl_slice2 sum_SDG_edge_valid_SDG_node)
    with ‹n'' = n⇩3› show ?thesis by simp
  qed
qed


lemma in_matched_in_HRB_slice:
  "⟦matched n ns n'; n'' ∈ set ns; n' ∈ S⟧ ⟹ n'' ∈ HRB_slice S"
proof(induct arbitrary:S rule:matched.induct)
   case matched_Nil thus ?case by simp
next
  case (matched_Append_intra_SDG_path n ns nx ns' n')
  note IH = ‹⋀S. ⟦n'' ∈ set ns; nx ∈ S⟧ ⟹ n'' ∈ HRB_slice S›
  from ‹n'' ∈ set (ns@ns')› have "n'' ∈ set ns ∨ n'' ∈ set ns'" by simp
  thus ?case
  proof
    assume "n'' ∈ set ns"
    from IH[OF ‹n'' ∈ set ns›] have "n'' ∈ HRB_slice {nx}" by simp
    with ‹nx i-ns'→⇩d* n'› ‹n' ∈ S› show ?thesis
      by(fastforce intro:HRB_slice_is_SDG_path_HRB_slice 
                        intra_SDG_path_is_SDG_path)
  next
    assume "n'' ∈ set ns'"
    with ‹nx i-ns'→⇩d* n'› ‹n' ∈ S› show ?case 
      by(fastforce intro:in_intra_SDG_path_in_HRB_slice simp:HRB_slice_def)
  qed
next
  case (matched_bracket_call n⇩0 ns n⇩1 p n⇩2 ns' n⇩3 n⇩4 V a a')
  note IH1 = ‹⋀S. ⟦n'' ∈ set ns; n⇩1 ∈ S⟧ ⟹ n'' ∈ HRB_slice S›
  note IH2 = ‹⋀S. ⟦n'' ∈ set ns'; n⇩3 ∈ S⟧ ⟹ n'' ∈ HRB_slice S›
  from ‹n⇩1 -p→⇘call⇙ n⇩2› ‹matched n⇩2 ns' n⇩3› ‹n⇩3 -p→⇘ret⇙ n⇩4 ∨ n⇩3 -p:V→⇘out⇙ n⇩4› 
    ‹a' ∈ get_return_edges a› ‹valid_edge a›
    ‹sourcenode a = parent_node n⇩1› ‹targetnode a = parent_node n⇩2›
    ‹sourcenode a' = parent_node n⇩3› ‹targetnode a' = parent_node n⇩4›
  have "matched n⇩1 ([]@n⇩1#ns'@[n⇩3]) n⇩4"
    by(fastforce intro:matched.matched_bracket_call matched_Nil 
                 elim:SDG_edge_valid_SDG_node)
  then obtain nsx where "n⇩1 is-nsx→⇩d* n⇩4" by(erule matched_is_SDG_path)
  from ‹n'' ∈ set (ns@n⇩1#ns'@[n⇩3])› 
  have "((n'' ∈ set ns ∨ n'' = n⇩1) ∨ n'' ∈ set ns') ∨ n'' = n⇩3" by auto
  thus ?case apply -
  proof(erule disjE)+
    assume "n'' ∈ set ns"
    from IH1[OF this] have "n'' ∈ HRB_slice {n⇩1}" by simp
    with ‹n⇩1 is-nsx→⇩d* n⇩4› ‹n⇩4 ∈ S› show ?thesis 
      by -(rule HRB_slice_is_SDG_path_HRB_slice)
  next
    assume "n'' = n⇩1"
    from ‹n⇩1 is-nsx→⇩d* n⇩4› have "n⇩1 ∈ sum_SDG_slice1 n⇩4" 
      by(fastforce intro:is_SDG_path_slice1 refl_slice1 is_SDG_path_valid_SDG_node)
    with ‹n'' = n⇩1› ‹n⇩4 ∈ S› show ?thesis
      by(fastforce intro:combSlice_refl simp:HRB_slice_def)
  next
    assume "n'' ∈ set ns'"
    with ‹matched n⇩2 ns' n⇩3› have "n'' ∈ sum_SDG_slice2 n⇩3"
      by(rule in_matched_in_slice2)
    with ‹n⇩3 -p→⇘ret⇙ n⇩4 ∨ n⇩3 -p:V→⇘out⇙ n⇩4› have "n'' ∈ sum_SDG_slice2 n⇩4"
      by(fastforce intro:slice2_ret_slice2 slice2_param_out_slice2 
                        SDG_edge_sum_SDG_edge)
    from ‹n⇩3 -p→⇘ret⇙ n⇩4 ∨ n⇩3 -p:V→⇘out⇙ n⇩4› have "valid_SDG_node n⇩4"
      by(fastforce intro:SDG_edge_valid_SDG_node)
    hence "n⇩4 ∈ sum_SDG_slice1 n⇩4" by(rule refl_slice1)
    from ‹n⇩3 -p→⇘ret⇙ n⇩4 ∨ n⇩3 -p:V→⇘out⇙ n⇩4›
    have "CFG_node (parent_node n⇩3) -p→⇘ret⇙ CFG_node (parent_node n⇩4)"
      by(fastforce elim:SDG_edge.cases intro:SDG_return_edge)
    with ‹n'' ∈ sum_SDG_slice2 n⇩4› ‹n⇩4 ∈ sum_SDG_slice1 n⇩4› ‹n⇩4 ∈ S›
    show ?case by(fastforce intro:combSlice_Return_parent_node SDG_edge_sum_SDG_edge 
                            simp:HRB_slice_def)
  next
    assume "n'' = n⇩3"
    from ‹n⇩3 -p→⇘ret⇙ n⇩4 ∨ n⇩3 -p:V→⇘out⇙ n⇩4›
    have "CFG_node (parent_node n⇩3) -p→⇘ret⇙ CFG_node (parent_node n⇩4)"
      by(fastforce elim:SDG_edge.cases intro:SDG_return_edge)
    from ‹n⇩3 -p→⇘ret⇙ n⇩4 ∨ n⇩3 -p:V→⇘out⇙ n⇩4› have "valid_SDG_node n⇩4"
      by(fastforce intro:SDG_edge_valid_SDG_node)
    hence "n⇩4 ∈ sum_SDG_slice1 n⇩4" by(rule refl_slice1)
    from ‹valid_SDG_node n⇩4› have "n⇩4 ∈ sum_SDG_slice2 n⇩4" by(rule refl_slice2)
    with ‹n⇩3 -p→⇘ret⇙ n⇩4 ∨ n⇩3 -p:V→⇘out⇙ n⇩4› have "n⇩3 ∈ sum_SDG_slice2 n⇩4" 
      by(fastforce intro:return_slice2 param_out_slice2 SDG_edge_sum_SDG_edge)
    with ‹n⇩4 ∈ sum_SDG_slice1 n⇩4› 
      ‹CFG_node (parent_node n⇩3) -p→⇘ret⇙ CFG_node (parent_node n⇩4)› ‹n'' = n⇩3› ‹n⇩4 ∈ S›
    show ?case by(fastforce intro:combSlice_Return_parent_node SDG_edge_sum_SDG_edge
                            simp:HRB_slice_def)
  qed
next
  case (matched_bracket_param n⇩0 ns n⇩1 p V n⇩2 ns' n⇩3 V' n⇩4 a a')
  note IH1 = ‹⋀S. ⟦n'' ∈ set ns; n⇩1 ∈ S⟧ ⟹ n'' ∈ HRB_slice S›
  note IH2 = ‹⋀S. ⟦n'' ∈ set ns'; n⇩3 ∈ S⟧ ⟹ n'' ∈ HRB_slice S›
  from ‹n⇩1 -p:V→⇘in⇙ n⇩2› ‹matched n⇩2 ns' n⇩3› ‹n⇩3 -p:V'→⇘out⇙ n⇩4› 
    ‹a' ∈ get_return_edges a› ‹valid_edge a›
    ‹sourcenode a = parent_node n⇩1› ‹targetnode a = parent_node n⇩2›
    ‹sourcenode a' = parent_node n⇩3› ‹targetnode a' = parent_node n⇩4›
  have "matched n⇩1 ([]@n⇩1#ns'@[n⇩3]) n⇩4"
    by(fastforce intro:matched.matched_bracket_param matched_Nil 
                 elim:SDG_edge_valid_SDG_node)
  then obtain nsx where "n⇩1 is-nsx→⇩d* n⇩4" by(erule matched_is_SDG_path)
  from ‹n'' ∈ set (ns@n⇩1#ns'@[n⇩3])› 
  have "((n'' ∈ set ns ∨ n'' = n⇩1) ∨ n'' ∈ set ns') ∨ n'' = n⇩3" by auto
  thus ?case apply -
  proof(erule disjE)+
    assume "n'' ∈ set ns"
    from IH1[OF this] have "n'' ∈ HRB_slice {n⇩1}" by simp
    with ‹n⇩1 is-nsx→⇩d* n⇩4› ‹n⇩4 ∈ S› show ?thesis 
      by -(rule HRB_slice_is_SDG_path_HRB_slice)
  next
    assume "n'' = n⇩1"
    from ‹n⇩1 is-nsx→⇩d* n⇩4› have "n⇩1 ∈ sum_SDG_slice1 n⇩4"
      by(fastforce intro:is_SDG_path_slice1 refl_slice1 is_SDG_path_valid_SDG_node)
    with ‹n'' = n⇩1› ‹n⇩4 ∈ S› show ?thesis
      by(fastforce intro:combSlice_refl simp:HRB_slice_def)
  next
    assume "n'' ∈ set ns'"
    with ‹matched n⇩2 ns' n⇩3› have "n'' ∈ sum_SDG_slice2 n⇩3"
      by(rule in_matched_in_slice2)
    with ‹n⇩3 -p:V'→⇘out⇙ n⇩4› have "n'' ∈ sum_SDG_slice2 n⇩4"
      by(fastforce intro:slice2_param_out_slice2 SDG_edge_sum_SDG_edge)
    from ‹n⇩3 -p:V'→⇘out⇙ n⇩4› have "valid_SDG_node n⇩4" by(rule SDG_edge_valid_SDG_node)
    hence "n⇩4 ∈ sum_SDG_slice1 n⇩4" by(rule refl_slice1)
    from ‹n⇩3 -p:V'→⇘out⇙ n⇩4› 
    have "CFG_node (parent_node n⇩3) -p→⇘ret⇙ CFG_node (parent_node n⇩4)"
      by(fastforce elim:SDG_edge.cases intro:SDG_return_edge)
    with ‹n'' ∈ sum_SDG_slice2 n⇩4› ‹n⇩4 ∈ sum_SDG_slice1 n⇩4› ‹n⇩4 ∈ S›
    show ?case by(fastforce intro:combSlice_Return_parent_node SDG_edge_sum_SDG_edge 
                            simp:HRB_slice_def)
  next
    assume "n'' = n⇩3"
    from ‹n⇩3 -p:V'→⇘out⇙ n⇩4› have "n⇩3 s-p:V'→⇘out⇙ n⇩4" by(rule SDG_edge_sum_SDG_edge)
    from ‹n⇩3 -p:V'→⇘out⇙ n⇩4› have "valid_SDG_node n⇩4" by(rule SDG_edge_valid_SDG_node)
    hence "n⇩4 ∈ sum_SDG_slice1 n⇩4" by(rule refl_slice1)
    from ‹valid_SDG_node n⇩4› have "n⇩4 ∈ sum_SDG_slice2 n⇩4" by(rule refl_slice2)
    with ‹n⇩3 s-p:V'→⇘out⇙ n⇩4› have "n⇩3 ∈ sum_SDG_slice2 n⇩4" by(rule param_out_slice2)
    from ‹n⇩3 -p:V'→⇘out⇙ n⇩4› 
    have "CFG_node (parent_node n⇩3) -p→⇘ret⇙ CFG_node (parent_node n⇩4)"
      by(fastforce elim:SDG_edge.cases intro:SDG_return_edge)
    with ‹n⇩3 ∈ sum_SDG_slice2 n⇩4› ‹n⇩4 ∈ sum_SDG_slice1 n⇩4› ‹n'' = n⇩3› ‹n⇩4 ∈ S›
    show ?case by(fastforce intro:combSlice_Return_parent_node SDG_edge_sum_SDG_edge
                            simp:HRB_slice_def)
  qed
qed


theorem in_realizable_in_HRB_slice:
  "⟦realizable n ns n'; n'' ∈ set ns; n' ∈ S⟧ ⟹ n'' ∈ HRB_slice S"
proof(induct arbitrary:S rule:realizable.induct)
  case (realizable_matched n ns n') thus ?case by(rule in_matched_in_HRB_slice)
next
  case (realizable_call n⇩0 ns n⇩1 p n⇩2 V ns' n⇩3)
  note IH = ‹⋀S. ⟦n'' ∈ set ns; n⇩1 ∈ S⟧ ⟹ n'' ∈ HRB_slice S›
  from ‹n'' ∈ set (ns@n⇩1#ns')› have "(n'' ∈ set ns ∨ n'' = n⇩1) ∨ n'' ∈ set ns'"
    by auto
  thus ?case apply -
  proof(erule disjE)+
    assume "n'' ∈ set ns"
    from IH[OF this] have "n'' ∈ HRB_slice {n⇩1}" by simp
    hence "n'' ∈ HRB_slice {n⇩2}"
    proof(induct rule:HRB_slice_cases)
      case (phase1 n nx)
      from ‹nx ∈ {n⇩1}› have "nx = n⇩1" by simp
      with ‹n ∈ sum_SDG_slice1 nx› ‹n⇩1 -p→⇘call⇙ n⇩2 ∨ n⇩1 -p:V→⇘in⇙ n⇩2›
      have "n ∈ sum_SDG_slice1 n⇩2" 
        by(fastforce intro:slice1_call_slice1 slice1_param_in_slice1 
                          SDG_edge_sum_SDG_edge)
      thus ?case
        by(fastforce intro:combine_SDG_slices.combSlice_refl simp:HRB_slice_def)
    next
      case (phase2 nx n' n'' p' n)
      from ‹nx ∈ {n⇩1}› have "nx = n⇩1" by simp
      with ‹n' ∈ sum_SDG_slice1 nx› ‹n⇩1 -p→⇘call⇙ n⇩2 ∨ n⇩1 -p:V→⇘in⇙ n⇩2›
      have "n' ∈ sum_SDG_slice1 n⇩2" 
        by(fastforce intro:slice1_call_slice1 slice1_param_in_slice1 
                          SDG_edge_sum_SDG_edge)
      with ‹n'' s-p'→⇘ret⇙ CFG_node (parent_node n')› ‹n ∈ sum_SDG_slice2 n'› show ?case
        by(fastforce intro:combine_SDG_slices.combSlice_Return_parent_node 
                     simp:HRB_slice_def)
    qed
    from ‹matched n⇩2 ns' n⇩3› obtain nsx where "n⇩2 is-nsx→⇩d* n⇩3"
      by(erule matched_is_SDG_path)
    with ‹n'' ∈ HRB_slice {n⇩2}› ‹n⇩3 ∈ S› show ?thesis
      by(fastforce intro:HRB_slice_is_SDG_path_HRB_slice)
  next
    assume "n'' = n⇩1"
    from ‹matched n⇩2 ns' n⇩3› obtain nsx where "n⇩2 is-nsx→⇩d* n⇩3"
      by(erule matched_is_SDG_path)
    hence "n⇩2 ∈ sum_SDG_slice1 n⇩2" 
      by(fastforce intro:refl_slice1 is_SDG_path_valid_SDG_node)
    with ‹n⇩1 -p→⇘call⇙ n⇩2 ∨ n⇩1 -p:V→⇘in⇙ n⇩2›
    have "n⇩1 ∈ sum_SDG_slice1 n⇩2"
      by(fastforce intro:call_slice1 param_in_slice1 SDG_edge_sum_SDG_edge)
    hence "n⇩1 ∈ HRB_slice {n⇩2}" by(fastforce intro:combSlice_refl simp:HRB_slice_def)
    with ‹n⇩2 is-nsx→⇩d* n⇩3› ‹n'' = n⇩1› ‹n⇩3 ∈ S› show ?thesis
      by(fastforce intro:HRB_slice_is_SDG_path_HRB_slice)
  next
    assume "n'' ∈ set ns'"
    from ‹matched n⇩2 ns' n⇩3› this ‹n⇩3 ∈ S› show ?thesis
      by(rule in_matched_in_HRB_slice)
  qed
qed


lemma slice1_ics_SDG_path:
  assumes "n ∈ sum_SDG_slice1 n'" and "n ≠ n'"
  obtains ns where "CFG_node (_Entry_) ics-ns→⇩d* n'" and "n ∈ set ns"
proof(atomize_elim)
  from ‹n ∈ sum_SDG_slice1 n'› 
  have "n = n' ∨ (∃ns. CFG_node (_Entry_) ics-ns→⇩d* n' ∧ n ∈ set ns)"
  proof(induct rule:sum_SDG_slice1.induct)
    case refl_slice1 thus ?case by simp
  next
    case (cdep_slice1 n'' n)
    from ‹n'' s⟶⇘cd⇙ n› have "valid_SDG_node n''" by(rule sum_SDG_edge_valid_SDG_node)
    hence "n'' ics-[]→⇩d* n''" by(rule icsSp_Nil)
    from ‹valid_SDG_node n''› have "valid_node (parent_node n'')"
      by(rule valid_SDG_CFG_node)
    thus ?case
    proof(cases "parent_node n'' = (_Exit_)")
      case True
      with ‹valid_SDG_node n''› have "n'' = CFG_node (_Exit_)"
        by(rule valid_SDG_node_parent_Exit)
      with ‹n'' s⟶⇘cd⇙ n› have False by(fastforce intro:Exit_no_sum_SDG_edge_source)
      thus ?thesis by simp
    next
      case False
      from ‹n'' s⟶⇘cd⇙ n› have "valid_SDG_node n''"
        by(rule sum_SDG_edge_valid_SDG_node)
      from this False obtain ns 
        where "CFG_node (_Entry_) cc-ns→⇩d* n''"
        by(erule Entry_cc_SDG_path_to_inner_node)
      with ‹n'' s⟶⇘cd⇙ n› have "CFG_node (_Entry_) cc-ns@[n'']→⇩d* n"
        by(fastforce intro:ccSp_Append_cdep sum_SDG_edge_SDG_edge)
      hence "CFG_node (_Entry_) ics-ns@[n'']→⇩d* n"
        by(rule cc_SDG_path_ics_SDG_path)
      from ‹n = n' ∨ (∃ns. CFG_node (_Entry_) ics-ns→⇩d* n' ∧ n ∈ set ns)›
      show ?thesis
      proof
        assume "n = n'"
        with ‹CFG_node (_Entry_) ics-ns@[n'']→⇩d* n› show ?thesis by fastforce
      next
        assume "∃ns. CFG_node (_Entry_) ics-ns→⇩d* n' ∧ n ∈ set ns"
        then obtain nsx where "CFG_node (_Entry_) ics-nsx→⇩d* n'" and "n ∈ set nsx"
          by blast
        then obtain ns' ns'' where "nsx = ns'@ns''" and "n ics-ns''→⇩d* n'"
          by -(erule ics_SDG_path_split)
        with ‹CFG_node (_Entry_) ics-ns@[n'']→⇩d* n›
        show ?thesis by(fastforce intro:ics_SDG_path_Append)
      qed
    qed
  next
    case (ddep_slice1 n'' V n)
    from ‹n'' s-V→⇩d⇩d n› have "valid_SDG_node n''" by(rule sum_SDG_edge_valid_SDG_node)
    hence "n'' ics-[]→⇩d* n''" by(rule icsSp_Nil)
    from ‹valid_SDG_node n''› have "valid_node (parent_node n'')"
      by(rule valid_SDG_CFG_node)
    thus ?case
    proof(cases "parent_node n'' = (_Exit_)")
      case True
      with ‹valid_SDG_node n''› have "n'' = CFG_node (_Exit_)"
        by(rule valid_SDG_node_parent_Exit)
      with ‹n'' s-V→⇩d⇩d n› have False by(fastforce intro:Exit_no_sum_SDG_edge_source)
      thus ?thesis by simp
    next
      case False
      from ‹n'' s-V→⇩d⇩d n› have "valid_SDG_node n''"
        by(rule sum_SDG_edge_valid_SDG_node)
      from this False obtain ns 
        where "CFG_node (_Entry_) cc-ns→⇩d* n''"
        by(erule Entry_cc_SDG_path_to_inner_node)
     hence "CFG_node (_Entry_) ics-ns→⇩d* n''"
        by(rule cc_SDG_path_ics_SDG_path)
      show ?thesis
      proof(cases "n'' = n")
        case True
        from ‹n = n' ∨ (∃ns. CFG_node (_Entry_) ics-ns→⇩d* n' ∧ n ∈ set ns)›
        show ?thesis
        proof
          assume "n = n'"
          with ‹n'' = n› show ?thesis by simp
        next
          assume "∃ns. CFG_node (_Entry_) ics-ns→⇩d* n' ∧ n ∈ set ns"
          with ‹n'' = n› show ?thesis by fastforce
        qed
      next
        case False
        with ‹n'' s-V→⇩d⇩d n› ‹CFG_node (_Entry_) ics-ns→⇩d* n''›
        have "CFG_node (_Entry_) ics-ns@[n'']→⇩d* n"
          by -(rule icsSp_Append_ddep)
        from ‹n = n' ∨ (∃ns. CFG_node (_Entry_) ics-ns→⇩d* n' ∧ n ∈ set ns)›
        show ?thesis
        proof
          assume "n = n'"
          with ‹CFG_node (_Entry_) ics-ns@[n'']→⇩d* n› show ?thesis by fastforce
        next
          assume "∃ns. CFG_node (_Entry_) ics-ns→⇩d* n' ∧ n ∈ set ns"
          then obtain nsx where "CFG_node (_Entry_) ics-nsx→⇩d* n'" and "n ∈ set nsx"
            by blast
          then obtain ns' ns'' where "nsx = ns'@ns''" and "n ics-ns''→⇩d* n'"
            by -(erule ics_SDG_path_split)
          with ‹CFG_node (_Entry_) ics-ns@[n'']→⇩d* n›
          show ?thesis by(fastforce intro:ics_SDG_path_Append)
        qed
      qed
    qed
  next
    case (call_slice1 n'' p n)
    from ‹n'' s-p→⇘call⇙ n› have "valid_SDG_node n''" 
      by(rule sum_SDG_edge_valid_SDG_node)
    hence "n'' ics-[]→⇩d* n''" by(rule icsSp_Nil)
    from ‹valid_SDG_node n''› have "valid_node (parent_node n'')"
      by(rule valid_SDG_CFG_node)
    thus ?case
    proof(cases "parent_node n'' = (_Exit_)")
      case True
      with ‹valid_SDG_node n''› have "n'' = CFG_node (_Exit_)"
        by(rule valid_SDG_node_parent_Exit)
      with ‹n'' s-p→⇘call⇙ n› have False by(fastforce intro:Exit_no_sum_SDG_edge_source)
      thus ?thesis by simp
    next
      case False
      from ‹n'' s-p→⇘call⇙ n› have "valid_SDG_node n''"
        by(rule sum_SDG_edge_valid_SDG_node)
      from this False obtain ns 
        where "CFG_node (_Entry_) cc-ns→⇩d* n''"
        by(erule Entry_cc_SDG_path_to_inner_node)
      with ‹n'' s-p→⇘call⇙ n› have "CFG_node (_Entry_) cc-ns@[n'']→⇩d* n"
        by(fastforce intro:ccSp_Append_call sum_SDG_edge_SDG_edge)
      hence "CFG_node (_Entry_) ics-ns@[n'']→⇩d* n"
        by(rule cc_SDG_path_ics_SDG_path)
      from ‹n = n' ∨ (∃ns. CFG_node (_Entry_) ics-ns→⇩d* n' ∧ n ∈ set ns)›
      show ?thesis
      proof
        assume "n = n'"
        with ‹CFG_node (_Entry_) ics-ns@[n'']→⇩d* n› show ?thesis by fastforce
      next
        assume "∃ns. CFG_node (_Entry_) ics-ns→⇩d* n' ∧ n ∈ set ns"
        then obtain nsx where "CFG_node (_Entry_) ics-nsx→⇩d* n'" and "n ∈ set nsx"
          by blast
        then obtain ns' ns'' where "nsx = ns'@ns''" and "n ics-ns''→⇩d* n'"
          by -(erule ics_SDG_path_split)
        with ‹CFG_node (_Entry_) ics-ns@[n'']→⇩d* n›
        show ?thesis by(fastforce intro:ics_SDG_path_Append)
      qed
    qed
  next
    case (param_in_slice1 n'' p V n)
    from ‹n'' s-p:V→⇘in⇙ n› have "valid_SDG_node n''" 
      by(rule sum_SDG_edge_valid_SDG_node)
    hence "n'' ics-[]→⇩d* n''" by(rule icsSp_Nil)
    from ‹valid_SDG_node n''› have "valid_node (parent_node n'')"
      by(rule valid_SDG_CFG_node)
    thus ?case
    proof(cases "parent_node n'' = (_Exit_)")
      case True
      with ‹valid_SDG_node n''› have "n'' = CFG_node (_Exit_)"
        by(rule valid_SDG_node_parent_Exit)
      with ‹n'' s-p:V→⇘in⇙ n› have False by(fastforce intro:Exit_no_sum_SDG_edge_source)
      thus ?thesis by simp
    next
      case False
      from ‹n'' s-p:V→⇘in⇙ n› have "valid_SDG_node n''"
        by(rule sum_SDG_edge_valid_SDG_node)
      from this False obtain ns 
        where "CFG_node (_Entry_) cc-ns→⇩d* n''"
        by(erule Entry_cc_SDG_path_to_inner_node)
      hence "CFG_node (_Entry_) ics-ns→⇩d* n''"
        by(rule cc_SDG_path_ics_SDG_path)
      with ‹n'' s-p:V→⇘in⇙ n› have "CFG_node (_Entry_) ics-ns@[n'']→⇩d* n"
        by -(rule icsSp_Append_param_in)
      from ‹n = n' ∨ (∃ns. CFG_node (_Entry_) ics-ns→⇩d* n' ∧ n ∈ set ns)›
      show ?thesis
      proof
        assume "n = n'"
        with ‹CFG_node (_Entry_) ics-ns@[n'']→⇩d* n› show ?thesis by fastforce
      next
        assume "∃ns. CFG_node (_Entry_) ics-ns→⇩d* n' ∧ n ∈ set ns"
        then obtain nsx where "CFG_node (_Entry_) ics-nsx→⇩d* n'" and "n ∈ set nsx"
          by blast
        then obtain ns' ns'' where "nsx = ns'@ns''" and "n ics-ns''→⇩d* n'"
          by -(erule ics_SDG_path_split)
        with ‹CFG_node (_Entry_) ics-ns@[n'']→⇩d* n›
        show ?thesis by(fastforce intro:ics_SDG_path_Append)
      qed
    qed
  next
    case (sum_slice1 n'' p n)
    from ‹n'' s-p→⇘sum⇙ n› have "valid_SDG_node n''" 
      by(rule sum_SDG_edge_valid_SDG_node)
    hence "n'' ics-[]→⇩d* n''" by(rule icsSp_Nil)
    from ‹valid_SDG_node n''› have "valid_node (parent_node n'')"
      by(rule valid_SDG_CFG_node)
    thus ?case
    proof(cases "parent_node n'' = (_Exit_)")
      case True
      with ‹valid_SDG_node n''› have "n'' = CFG_node (_Exit_)"
        by(rule valid_SDG_node_parent_Exit)
      with ‹n'' s-p→⇘sum⇙ n› have False by(fastforce intro:Exit_no_sum_SDG_edge_source)
      thus ?thesis by simp
    next
      case False
      from ‹n'' s-p→⇘sum⇙ n› have "valid_SDG_node n''"
        by(rule sum_SDG_edge_valid_SDG_node)
      from this False obtain ns 
        where "CFG_node (_Entry_) cc-ns→⇩d* n''"
        by(erule Entry_cc_SDG_path_to_inner_node)
      hence "CFG_node (_Entry_) ics-ns→⇩d* n''"
        by(rule cc_SDG_path_ics_SDG_path)
      with ‹n'' s-p→⇘sum⇙ n› have "CFG_node (_Entry_) ics-ns@[n'']→⇩d* n"
        by -(rule icsSp_Append_sum)
      from ‹n = n' ∨ (∃ns. CFG_node (_Entry_) ics-ns→⇩d* n' ∧ n ∈ set ns)›
      show ?thesis
      proof
        assume "n = n'"
        with ‹CFG_node (_Entry_) ics-ns@[n'']→⇩d* n› show ?thesis by fastforce
      next
        assume "∃ns. CFG_node (_Entry_) ics-ns→⇩d* n' ∧ n ∈ set ns"
        then obtain nsx where "CFG_node (_Entry_) ics-nsx→⇩d* n'" and "n ∈ set nsx"
          by blast
        then obtain ns' ns'' where "nsx = ns'@ns''" and "n ics-ns''→⇩d* n'"
          by -(erule ics_SDG_path_split)
        with ‹CFG_node (_Entry_) ics-ns@[n'']→⇩d* n›
        show ?thesis by(fastforce intro:ics_SDG_path_Append)
      qed
    qed
  qed
  with ‹n ≠ n'› show "∃ns. CFG_node (_Entry_) ics-ns→⇩d* n' ∧ n ∈ set ns" by simp
qed


lemma slice2_irs_SDG_path:
  assumes "n ∈ sum_SDG_slice2 n'" and "valid_SDG_node n'"
  obtains ns where "n irs-ns→⇩d* n'"
using assms
by(induct rule:sum_SDG_slice2.induct,auto intro:intra_return_sum_SDG_path.intros)


theorem HRB_slice_realizable:
  assumes "n ∈ HRB_slice S" and "∀n' ∈ S. valid_SDG_node n'" and "n ∉ S"
  obtains n' ns where "n' ∈ S" and "realizable (CFG_node (_Entry_)) ns n'" 
  and "n ∈ set ns"
proof(atomize_elim)
  from ‹n ∈ HRB_slice S› ‹n ∉ S›
  show "∃n' ns. n' ∈ S ∧ realizable (CFG_node (_Entry_)) ns n' ∧ n ∈ set ns"
  proof(induct rule:HRB_slice_cases)
    case (phase1 n nx)
    with ‹n ∉ S› show ?case
      by(fastforce elim:slice1_ics_SDG_path ics_SDG_path_realizable)
  next
    case (phase2 n' nx n'' p n)
    from ‹∀n' ∈ S. valid_SDG_node n'› ‹n' ∈ S› have "valid_SDG_node n'" by simp
    with ‹nx ∈ sum_SDG_slice1 n'› have "valid_SDG_node nx"
      by(auto elim:slice1_ics_SDG_path ics_SDG_path_split 
              intro:ics_SDG_path_valid_SDG_node)
    with ‹n ∈ sum_SDG_slice2 nx›
    obtain nsx where "n irs-nsx→⇩d* nx" by(erule slice2_irs_SDG_path)
    show ?case
    proof(cases "n = nx")
      case True
      show ?thesis
      proof(cases "nx = n'")
        case True
        with ‹n = nx› ‹n ∉ S› ‹n' ∈ S› have False by simp
        thus ?thesis by simp
      next
        case False
        with ‹nx ∈ sum_SDG_slice1 n'› obtain ns 
          where "realizable (CFG_node (_Entry_)) ns n'" and "nx ∈ set ns"
          by(fastforce elim:slice1_ics_SDG_path ics_SDG_path_realizable)
        with ‹n = nx› ‹n' ∈ S› show ?thesis by blast
      qed
    next
      case False
      with ‹n irs-nsx→⇩d* nx› obtain ns
        where "realizable (CFG_node (_Entry_)) ns nx" and "n ∈ set ns"
        by(erule irs_SDG_path_realizable)
      show ?thesis
      proof(cases "nx = n'")
        case True
        with ‹realizable (CFG_node (_Entry_)) ns nx› ‹n ∈ set ns› ‹n' ∈ S›
        show ?thesis by blast
      next
        case False
        with ‹nx ∈ sum_SDG_slice1 n'› obtain nsx'
          where "CFG_node (_Entry_) ics-nsx'→⇩d* n'" and "nx ∈ set nsx'"
          by(erule slice1_ics_SDG_path)
        then obtain ns' where "nx ics-ns'→⇩d* n'" by -(erule ics_SDG_path_split)
        with ‹realizable (CFG_node (_Entry_)) ns nx›
        obtain ns'' where "realizable (CFG_node (_Entry_)) (ns@ns'') n'"
          by(erule realizable_Append_ics_SDG_path)
        with ‹n ∈ set ns› ‹n' ∈ S› show ?thesis by fastforce
      qed
    qed
  qed
qed


theorem HRB_slice_precise:
  "⟦∀n' ∈ S. valid_SDG_node n'; n ∉ S⟧ ⟹
    n ∈ HRB_slice S = 
    (∃n' ns. n' ∈ S ∧ realizable (CFG_node (_Entry_)) ns n' ∧ n ∈ set ns)"
  by(fastforce elim:HRB_slice_realizable intro:in_realizable_in_HRB_slice)

end

end