Theory HRBSlice

header {* \isaheader{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->⇘dd⇙ 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->⇘dd⇙ 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->⇘dd⇙ 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->⇘dd⇙ 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->⇘dd⇙ 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->⇘dd⇙ 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->⇘dd⇙ 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->⇘dd⇙ 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->⇘dd⇙ 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\<hookleftarrow>⇘p⇙f"
  and "valid_edge a'" and "kind a' = Q':r'\<hookrightarrow>⇘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'\<hookrightarrow>⇘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\<hookleftarrow>⇘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\<hookleftarrow>⇘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'\<hookrightarrow>⇘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->⇘dd⇙ n'` show ?thesis
      by(fastforce intro:slice2_ddep_slice2 SDG_edge_sum_SDG_edge)
  next
    assume "n'' = nx"
    from `nx -V->⇘dd⇙ 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->⇘dd⇙ 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->⇘dd⇙ 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->⇘dd⇙ 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->⇘dd⇙ 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->⇘dd⇙ 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->⇘dd⇙ n` have False by(fastforce intro:Exit_no_sum_SDG_edge_source)
      thus ?thesis by simp
    next
      case False
      from `n'' s-V->⇘dd⇙ 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->⇘dd⇙ 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