Theory SDG

section ‹SDG›

theory SDG imports CFGExit_wf Postdomination begin

subsection ‹The nodes of the SDG›

datatype 'node SDG_node = 
    CFG_node 'node
  | Formal_in  "'node × nat"
  | Formal_out "'node × nat"
  | Actual_in  "'node × nat"
  | Actual_out "'node × nat"

fun parent_node :: "'node SDG_node ⇒ 'node"
  where "parent_node (CFG_node n) = n"
  | "parent_node (Formal_in (m,x)) = m"
  | "parent_node (Formal_out (m,x)) = m"
  | "parent_node (Actual_in (m,x)) = m"
  | "parent_node (Actual_out (m,x)) = m"


locale SDG = CFGExit_wf sourcenode targetnode kind valid_edge Entry 
    get_proc get_return_edges procs Main Exit Def Use ParamDefs ParamUses +
  Postdomination sourcenode targetnode kind valid_edge Entry 
    get_proc get_return_edges procs Main Exit
  for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
  and kind :: "'edge ⇒ ('var,'val,'ret,'pname) edge_kind" 
  and valid_edge :: "'edge ⇒ bool"
  and Entry :: "'node" ("'('_Entry'_')")  and get_proc :: "'node ⇒ 'pname"
  and get_return_edges :: "'edge ⇒ 'edge set"
  and procs :: "('pname × 'var list × 'var list) list" and Main :: "'pname"
  and Exit::"'node"  ("'('_Exit'_')") 
  and Def :: "'node ⇒ 'var set" and Use :: "'node ⇒ 'var set"
  and ParamDefs :: "'node ⇒ 'var list" and ParamUses :: "'node ⇒ 'var set list"

begin


fun valid_SDG_node :: "'node SDG_node ⇒ bool"
  where "valid_SDG_node (CFG_node n) ⟷ valid_node n"
  | "valid_SDG_node (Formal_in (m,x)) ⟷
  (∃a Q r p fs ins outs. valid_edge a ∧ (kind a = Q:r↪⇘p⇙fs) ∧ targetnode a = m ∧ 
  (p,ins,outs) ∈ set procs ∧ x < length ins)"
  | "valid_SDG_node (Formal_out (m,x)) ⟷
  (∃a Q p f ins outs. valid_edge a ∧ (kind a = Q↩⇘p⇙f) ∧ sourcenode a = m ∧ 
  (p,ins,outs) ∈ set procs ∧ x < length outs)"
  | "valid_SDG_node (Actual_in (m,x)) ⟷
  (∃a Q r p fs ins outs. valid_edge a ∧ (kind a = Q:r↪⇘p⇙fs) ∧ sourcenode a = m ∧ 
  (p,ins,outs) ∈ set procs ∧ x < length ins)"
  | "valid_SDG_node (Actual_out (m,x)) ⟷
  (∃a Q p f ins outs. valid_edge a ∧ (kind a = Q↩⇘p⇙f) ∧ targetnode a = m ∧ 
  (p,ins,outs) ∈ set procs ∧ x < length outs)"


lemma valid_SDG_CFG_node: 
  "valid_SDG_node n ⟹ valid_node (parent_node n)"
by(cases n) auto


lemma Formal_in_parent_det:
  assumes "valid_SDG_node (Formal_in (m,x))" and "valid_SDG_node (Formal_in (m',x'))"
  and "get_proc m = get_proc m'"
  shows "m = m'"
proof -
  from ‹valid_SDG_node (Formal_in (m,x))› obtain a Q r p fs ins outs
    where "valid_edge a" and "kind a = Q:r↪⇘p⇙fs" and "targetnode a = m"
    and "(p,ins,outs) ∈ set procs" and "x < length ins" by fastforce
  from ‹valid_SDG_node (Formal_in (m',x'))› obtain a' Q' r' p' f' ins' outs'
    where "valid_edge a'" and "kind a' = Q':r'↪⇘p'⇙f'" and "targetnode a' = m'"
    and "(p',ins',outs') ∈ set procs" and "x' < length ins'" by fastforce
  from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹targetnode a = m›
  have "get_proc m = p" by(fastforce intro:get_proc_call)
  moreover
  from ‹valid_edge a'› ‹kind a' = Q':r'↪⇘p'⇙f'› ‹targetnode a' = m'›
  have "get_proc m' = p'" by(fastforce intro:get_proc_call)
  ultimately have "p = p'" using ‹get_proc m = get_proc m'› by simp
  with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹valid_edge a'› ‹kind a' = Q':r'↪⇘p'⇙f'›
    ‹targetnode a = m› ‹targetnode a' = m'›
  show ?thesis by(fastforce intro:same_proc_call_unique_target)
qed


lemma valid_SDG_node_parent_Entry:
  assumes "valid_SDG_node n" and "parent_node n = (_Entry_)"
  shows "n = CFG_node (_Entry_)"
proof(cases n)
  case CFG_node with ‹parent_node n = (_Entry_)› show ?thesis by simp
next
  case (Formal_in z)
  with ‹parent_node n = (_Entry_)› obtain x 
    where [simp]:"z = ((_Entry_),x)" by(cases z) auto
  with ‹valid_SDG_node n› Formal_in obtain a where "valid_edge a"
    and "targetnode a = (_Entry_)" by auto
  hence False by -(rule Entry_target,simp+)
  thus ?thesis by simp
next
  case (Formal_out z)
  with ‹parent_node n = (_Entry_)› obtain x 
    where [simp]:"z = ((_Entry_),x)" by(cases z) auto
  with ‹valid_SDG_node n› Formal_out obtain a Q p f where "valid_edge a"
    and "kind a = Q↩⇘p⇙f" and  "sourcenode a = (_Entry_)" by auto
  from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› have "get_proc (sourcenode a) = p"
    by(rule get_proc_return)
  with ‹sourcenode a = (_Entry_)› have "p = Main"
    by(auto simp:get_proc_Entry)
  with ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› have False
    by(fastforce intro:Main_no_return_source)
  thus ?thesis by simp
next
  case (Actual_in z)
  with ‹parent_node n = (_Entry_)› obtain x 
    where [simp]:"z = ((_Entry_),x)" by(cases z) auto
  with ‹valid_SDG_node n› Actual_in obtain a Q r p fs where "valid_edge a"
    and "kind a = Q:r↪⇘p⇙fs" and "sourcenode a = (_Entry_)" by fastforce
  hence False by -(rule Entry_no_call_source,auto)
  thus ?thesis by simp
next
  case (Actual_out z)
  with ‹parent_node n = (_Entry_)› obtain x 
    where [simp]:"z = ((_Entry_),x)" by(cases z) auto
  with ‹valid_SDG_node n› Actual_out obtain a where "valid_edge a"
    "targetnode a = (_Entry_)" by auto
  hence False by -(rule Entry_target,simp+)
  thus ?thesis by simp
qed


lemma valid_SDG_node_parent_Exit:
  assumes "valid_SDG_node n" and "parent_node n = (_Exit_)"
  shows "n = CFG_node (_Exit_)"
proof(cases n)
  case CFG_node with ‹parent_node n = (_Exit_)› show ?thesis by simp
next
  case (Formal_in z)
  with ‹parent_node n = (_Exit_)› obtain x 
    where [simp]:"z = ((_Exit_),x)" by(cases z) auto
  with ‹valid_SDG_node n› Formal_in obtain a Q r p fs where "valid_edge a"
    and "kind a = Q:r↪⇘p⇙fs" and "targetnode a = (_Exit_)" by fastforce
  from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc (targetnode a) = p"
    by(rule get_proc_call)
  with ‹targetnode a = (_Exit_)› have "p = Main"
    by(auto simp:get_proc_Exit)
  with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have False
    by(fastforce intro:Main_no_call_target)
  thus ?thesis by simp
next
  case (Formal_out z)
  with ‹parent_node n = (_Exit_)› obtain x 
    where [simp]:"z = ((_Exit_),x)" by(cases z) auto
  with ‹valid_SDG_node n› Formal_out obtain a where "valid_edge a"
    and "sourcenode a = (_Exit_)" by auto
  hence False by -(rule Exit_source,simp+)
  thus ?thesis by simp
next
  case (Actual_in z)
  with ‹parent_node n = (_Exit_)› obtain x 
    where [simp]:"z = ((_Exit_),x)" by(cases z) auto
  with ‹valid_SDG_node n› Actual_in obtain a where "valid_edge a"
    and "sourcenode a = (_Exit_)" by auto
  hence False by -(rule Exit_source,simp+)
  thus ?thesis by simp
next
  case (Actual_out z)
  with ‹parent_node n = (_Exit_)› obtain x 
    where [simp]:"z = ((_Exit_),x)" by(cases z) auto
  with ‹valid_SDG_node n› Actual_out obtain a Q p f where "valid_edge a"
    and "kind a = Q↩⇘p⇙f" and "targetnode a = (_Exit_)" by auto
  hence False by -(erule Exit_no_return_target,auto)
  thus ?thesis by simp
qed


subsection ‹Data dependence›

inductive SDG_Use :: "'var ⇒ 'node SDG_node ⇒ bool" ("_ ∈ Use⇘SDG⇙ _")
where CFG_Use_SDG_Use:
  "⟦valid_node m; V ∈ Use m; n = CFG_node m⟧ ⟹ V ∈ Use⇘SDG⇙ n"
  | Actual_in_SDG_Use:
  "⟦valid_SDG_node n; n = Actual_in (m,x); V ∈ (ParamUses m)!x⟧ ⟹ V ∈ Use⇘SDG⇙ n"
  | Formal_out_SDG_Use:
  "⟦valid_SDG_node n; n = Formal_out (m,x); get_proc m = p; (p,ins,outs) ∈ set procs;
    V = outs!x⟧ ⟹ V ∈ Use⇘SDG⇙ n"


abbreviation notin_SDG_Use :: "'var ⇒ 'node SDG_node ⇒ bool"  ("_ ∉ Use⇘SDG⇙ _")
  where "V ∉ Use⇘SDG⇙ n ≡ ¬ V ∈ Use⇘SDG⇙ n"


lemma in_Use_valid_SDG_node:
  "V ∈ Use⇘SDG⇙ n ⟹ valid_SDG_node n"
by(induct rule:SDG_Use.induct,auto intro:valid_SDG_CFG_node)


lemma SDG_Use_parent_Use: 
  "V ∈ Use⇘SDG⇙ n ⟹ V ∈ Use (parent_node n)"
proof(induct rule:SDG_Use.induct)
  case CFG_Use_SDG_Use thus ?case by simp
next
  case (Actual_in_SDG_Use n m x V)
  from ‹valid_SDG_node n› ‹n = Actual_in (m, x)› obtain a Q r p fs ins outs
    where "valid_edge a" and "kind a = Q:r↪⇘p⇙fs" and "sourcenode a = m"
    and "(p,ins,outs) ∈ set procs" and "x < length ins" by fastforce
  from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹(p,ins,outs) ∈ set procs›
  have "length(ParamUses (sourcenode a)) = length ins"
    by(fastforce intro:ParamUses_call_source_length)
  with ‹x < length ins›
  have "(ParamUses (sourcenode a))!x ∈ set (ParamUses (sourcenode a))" by simp
  with ‹V ∈ (ParamUses m)!x› ‹sourcenode a = m›
  have "V ∈ Union (set (ParamUses m))" by fastforce
  with ‹valid_edge a› ‹sourcenode a = m› ‹n = Actual_in (m, x)› show ?case
    by(fastforce intro:ParamUses_in_Use)
next
  case (Formal_out_SDG_Use n m x p ins outs V)
  from ‹valid_SDG_node n› ‹n = Formal_out (m, x)› obtain a Q p' f ins' outs'
    where "valid_edge a" and "kind a = Q↩⇘p'⇙f" and "sourcenode a = m"
    and "(p',ins',outs') ∈ set procs" and "x < length outs'" by fastforce
  from ‹valid_edge a› ‹kind a = Q↩⇘p'⇙f› have "get_proc (sourcenode a) = p'"
    by(rule get_proc_return)
  with ‹get_proc m = p› ‹sourcenode a = m› have [simp]:"p = p'" by simp
  with ‹(p',ins',outs') ∈ set procs› ‹(p,ins,outs) ∈ set procs› unique_callers
  have [simp]:"ins' = ins" "outs' = outs" by(auto dest:distinct_fst_isin_same_fst)
  from ‹x < length outs'› ‹V = outs ! x› have "V ∈ set outs" by fastforce
  with ‹valid_edge a› ‹kind a = Q↩⇘p'⇙f› ‹(p,ins,outs) ∈ set procs›
  have "V ∈ Use (sourcenode a)" by(fastforce intro:outs_in_Use)
  with ‹sourcenode a = m› ‹valid_SDG_node n› ‹n = Formal_out (m, x)›
  show ?case by simp
qed



inductive SDG_Def :: "'var ⇒ 'node SDG_node ⇒ bool" ("_ ∈ Def⇘SDG⇙ _")
where CFG_Def_SDG_Def:
  "⟦valid_node m; V ∈ Def m; n = CFG_node m⟧ ⟹ V ∈ Def⇘SDG⇙ n"
  | Formal_in_SDG_Def:
  "⟦valid_SDG_node n; n = Formal_in (m,x); get_proc m = p; (p,ins,outs) ∈ set procs;
    V = ins!x⟧ ⟹ V ∈ Def⇘SDG⇙ n"
  | Actual_out_SDG_Def:
  "⟦valid_SDG_node n; n = Actual_out (m,x); V = (ParamDefs m)!x⟧ ⟹ V ∈ Def⇘SDG⇙ n"

abbreviation notin_SDG_Def :: "'var ⇒ 'node SDG_node ⇒ bool"  ("_ ∉ Def⇘SDG⇙ _")
  where "V ∉ Def⇘SDG⇙ n ≡ ¬ V ∈ Def⇘SDG⇙ n"


lemma in_Def_valid_SDG_node:
  "V ∈ Def⇘SDG⇙ n ⟹ valid_SDG_node n"
by(induct rule:SDG_Def.induct,auto intro:valid_SDG_CFG_node)


lemma SDG_Def_parent_Def: 
  "V ∈ Def⇘SDG⇙ n ⟹ V ∈ Def (parent_node n)"
proof(induct rule:SDG_Def.induct)
  case CFG_Def_SDG_Def thus ?case by simp
next
  case (Formal_in_SDG_Def n m x p ins outs V)
  from ‹valid_SDG_node n› ‹n = Formal_in (m, x)› obtain a Q r p' fs ins' outs'
    where "valid_edge a" and "kind a = Q:r↪⇘p'⇙fs" and "targetnode a = m"
    and "(p',ins',outs') ∈ set procs" and "x < length ins'" by fastforce
  from ‹valid_edge a› ‹kind a = Q:r↪⇘p'⇙fs› have "get_proc (targetnode a) = p'"
    by(rule get_proc_call)
  with ‹get_proc m = p› ‹targetnode a = m› have [simp]:"p = p'" by simp
  with ‹(p',ins',outs') ∈ set procs› ‹(p,ins,outs) ∈ set procs› unique_callers
  have [simp]:"ins' = ins" "outs' = outs" by(auto dest:distinct_fst_isin_same_fst)
  from ‹x < length ins'› ‹V = ins ! x› have "V ∈ set ins" by fastforce
  with ‹valid_edge a› ‹kind a = Q:r↪⇘p'⇙fs› ‹(p,ins,outs) ∈ set procs›
  have "V ∈ Def (targetnode a)" by(fastforce intro:ins_in_Def)
  with ‹targetnode a = m› ‹valid_SDG_node n› ‹n = Formal_in (m, x)›
  show ?case by simp
next
  case (Actual_out_SDG_Def n m x V)
  from ‹valid_SDG_node n› ‹n = Actual_out (m, x)› obtain a Q p f ins outs
    where "valid_edge a" and "kind a = Q↩⇘p⇙f" and "targetnode a = m"
    and "(p,ins,outs) ∈ set procs" and "x < length outs" by fastforce
  from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› ‹(p,ins,outs) ∈ set procs›
  have "length(ParamDefs (targetnode a)) = length outs" 
    by(rule ParamDefs_return_target_length)
  with ‹x < length outs› ‹V = ParamDefs m ! x› ‹targetnode a = m›
  have "V ∈ set (ParamDefs (targetnode a))" by(fastforce simp:set_conv_nth)
  with ‹n = Actual_out (m, x)› ‹targetnode a = m› ‹valid_edge a›
  show ?case by(fastforce intro:ParamDefs_in_Def)
qed



definition data_dependence :: "'node SDG_node ⇒ 'var ⇒ 'node SDG_node ⇒ bool" 
("_ influences _ in _" [51,0,0])
  where "n influences V in n' ≡ ∃as. (V ∈ Def⇘SDG⇙ n) ∧ (V ∈ Use⇘SDG⇙ n') ∧ 
  (parent_node n -as→⇩ι* parent_node n') ∧
  (∀n''. valid_SDG_node n'' ∧ parent_node n'' ∈ set (sourcenodes (tl as))
         ⟶ V ∉ Def⇘SDG⇙ n'')"


subsection ‹Control dependence›

definition control_dependence :: "'node ⇒ 'node ⇒ bool" 
  ("_ controls _" [51,0])
where "n controls n' ≡ ∃a a' as. n -a#as→⇩ι* n' ∧ n' ∉ set(sourcenodes (a#as)) ∧
    intra_kind(kind a) ∧ n' postdominates (targetnode a) ∧ 
    valid_edge a' ∧ intra_kind(kind a') ∧ sourcenode a' = n ∧ 
    ¬ n' postdominates (targetnode a')"


lemma control_dependence_path:
  assumes "n controls n'" obtains as where "n -as→⇩ι* n'" and "as ≠ []"
using ‹n controls n'›
by(fastforce simp:control_dependence_def)


lemma Exit_does_not_control [dest]:
  assumes "(_Exit_) controls n'" shows "False"
proof -
  from ‹(_Exit_) controls n'› obtain a where "valid_edge a"
    and "sourcenode a = (_Exit_)" by(auto simp:control_dependence_def)
  thus ?thesis by(rule Exit_source)
qed


lemma Exit_not_control_dependent: 
  assumes "n controls n'" shows "n' ≠ (_Exit_)"
proof -
  from ‹n controls n'› obtain a as where "n -a#as→⇩ι* n'"
    and "n' postdominates (targetnode a)"
    by(auto simp:control_dependence_def)
  from ‹n -a#as→⇩ι* n'› have "valid_edge a" 
    by(fastforce elim:path.cases simp:intra_path_def)
  hence "valid_node (targetnode a)" by simp
  with ‹n' postdominates (targetnode a)› ‹n -a#as→⇩ι* n'› show ?thesis
    by(fastforce elim:Exit_no_postdominator)
qed


lemma which_node_intra_standard_control_dependence_source:
  assumes "nx -as@a#as'→⇩ι* n" and "sourcenode a = n'" and "sourcenode a' = n'"
  and "n ∉ set(sourcenodes (a#as'))" and "valid_edge a'" and "intra_kind(kind a')"
  and "inner_node n" and "¬ method_exit n" and "¬ n postdominates (targetnode a')"
  and last:"∀ax ax'. ax ∈ set as' ∧ sourcenode ax = sourcenode ax' ∧
    valid_edge ax' ∧ intra_kind(kind ax') ⟶ n postdominates targetnode ax'"
  shows "n' controls n"
proof -
  from ‹nx -as@a#as'→⇩ι* n› ‹sourcenode a = n'› have "n' -a#as'→⇩ι* n"
    by(fastforce dest:path_split_second simp:intra_path_def)
  from ‹nx -as@a#as'→⇩ι* n› have "valid_edge a"
    by(fastforce intro:path_split simp:intra_path_def)
  show ?thesis
  proof(cases "n postdominates (targetnode a)")
    case True
    with ‹n' -a#as'→⇩ι* n› ‹n ∉ set(sourcenodes (a#as'))›
      ‹valid_edge a'› ‹intra_kind(kind a')› ‹sourcenode a' = n'› 
      ‹¬ n postdominates (targetnode a')› show ?thesis
      by(fastforce simp:control_dependence_def intra_path_def)
  next
    case False
    show ?thesis
    proof(cases "as' = []")
      case True
      with ‹n' -a#as'→⇩ι* n› have "targetnode a = n" 
        by(fastforce elim:path.cases simp:intra_path_def)
      with ‹inner_node n› ‹¬ method_exit n› have "n postdominates (targetnode a)"
        by(fastforce dest:inner_is_valid intro:postdominate_refl)
      with ‹¬ n postdominates (targetnode a)› show ?thesis by simp
    next
      case False
      with ‹nx -as@a#as'→⇩ι* n› have "targetnode a -as'→⇩ι* n"
        by(fastforce intro:path_split simp:intra_path_def)
     with ‹¬ n postdominates (targetnode a)› ‹valid_edge a› ‹inner_node n›
        ‹targetnode a -as'→⇩ι* n›
      obtain asx pex where "targetnode a -asx→⇩ι* pex" and "method_exit pex"
        and "n ∉ set (sourcenodes asx)"
        by(fastforce dest:inner_is_valid simp:postdominate_def)
      show ?thesis
      proof(cases "∃asx'. asx = as'@asx'")
        case True
        then obtain asx' where [simp]:"asx = as'@asx'" by blast
        from ‹targetnode a -asx→⇩ι* pex› ‹targetnode a -as'→⇩ι* n›
          ‹as' ≠ []› ‹method_exit pex› ‹¬ method_exit n›
        obtain a'' as'' where "asx' = a''#as'' ∧ sourcenode a'' = n"
          by(cases asx')(auto dest:path_split path_det simp:intra_path_def)
        hence "n ∈ set(sourcenodes asx)" by(simp add:sourcenodes_def)
        with ‹n ∉ set (sourcenodes asx)› have False by simp
        thus ?thesis by simp
      next
        case False
        hence "∀asx'. asx ≠ as'@asx'" by simp
        then obtain j asx' where "asx = (take j as')@asx'"
          and "j < length as'" and "∀k > j. ∀asx''. asx ≠ (take k as')@asx''"
          by(auto elim:path_split_general)
        from ‹asx = (take j as')@asx'› ‹j < length as'›
        have "∃as'1 as'2. asx = as'1@asx' ∧ 
          as' = as'1@as'2 ∧ as'2 ≠ [] ∧ as'1 = take j as'"
          by simp(rule_tac x= "drop j as'" in exI,simp)
        then obtain as'1 as'' where "asx = as'1@asx'"
          and "as'1 = take j as'"
          and "as' = as'1@as''" and "as'' ≠ []" by blast
        from ‹as' = as'1@as''› ‹as'' ≠ []› obtain a1 as'2 
          where "as' = as'1@a1#as'2" and "as'' = a1#as'2"
          by(cases as'') auto
        have "asx' ≠ []"
        proof(cases "asx' = []")
          case True
          with ‹asx = as'1@asx'› ‹as' = as'1@as''› ‹as'' = a1#as'2›
          have "as' = asx@a1#as'2" by simp
          with ‹n' -a#as'→⇩ι* n› have "n' -(a#asx)@a1#as'2→⇩ι* n" by simp
          hence "n' -(a#asx)@a1#as'2→* n" 
            and "∀ax ∈ set((a#asx)@a1#as'2). intra_kind(kind ax)"
            by(simp_all add:intra_path_def)
          from ‹n' -(a#asx)@a1#as'2→* n›
          have "n' -a#asx→* sourcenode a1" and "valid_edge a1"
            by -(erule path_split)+
          from ‹∀ax ∈ set((a#asx)@a1#as'2). intra_kind(kind ax)› 
          have "∀ax ∈ set(a#asx). intra_kind(kind ax)" by simp
          with ‹n' -a#asx→* sourcenode a1› have "n' -a#asx→⇩ι* sourcenode a1"
            by(simp add:intra_path_def)
          hence "targetnode a -asx→⇩ι* sourcenode a1"
            by(fastforce intro:path_split_Cons simp:intra_path_def)
          with ‹targetnode a -asx→⇩ι* pex› have "pex = sourcenode a1"
            by(fastforce intro:path_det simp:intra_path_def)
          from ‹∀ax ∈ set((a#asx)@a1#as'2). intra_kind(kind ax)›
          have "intra_kind (kind a1)" by simp
          from ‹method_exit pex› have False
          proof(rule method_exit_cases)
            assume "pex = (_Exit_)"
            with ‹pex = sourcenode a1› have "sourcenode a1 = (_Exit_)" by simp
            with ‹valid_edge a1› show False by(rule Exit_source)
          next
            fix a Q f p assume "pex = sourcenode a" and "valid_edge a"
              and "kind a = Q↩⇘p⇙f"
            from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› ‹pex = sourcenode a› 
              ‹pex = sourcenode a1› ‹valid_edge a1› ‹intra_kind (kind a1)›
            show False by(fastforce dest:return_edges_only simp:intra_kind_def)
          qed
          thus ?thesis by simp
        qed simp
        with ‹asx = as'1@asx'› obtain a2 asx'1 
          where "asx = as'1@a2#asx'1"
          and "asx' = a2#asx'1" by(cases asx') auto
        from ‹n' -a#as'→⇩ι* n› ‹as' = as'1@a1#as'2› 
        have "n' -(a#as'1)@a1#as'2→⇩ι* n" by simp
        hence "n' -(a#as'1)@a1#as'2→* n" 
          and "∀ax ∈ set((a#as'1)@a1#as'2). intra_kind(kind ax)"
          by(simp_all add: intra_path_def)
        from ‹n' -(a#as'1)@a1#as'2→* n› have "n' -a#as'1→* sourcenode a1"
          and "valid_edge a1" by -(erule path_split)+
        from ‹∀ax ∈ set((a#as'1)@a1#as'2). intra_kind(kind ax)›
        have "∀ax ∈ set(a#as'1). intra_kind(kind ax)" by simp
        with ‹n' -a#as'1→* sourcenode a1› have "n' -a#as'1→⇩ι* sourcenode a1"
          by(simp add:intra_path_def)
        hence "targetnode a -as'1→⇩ι* sourcenode a1"
          by(fastforce intro:path_split_Cons simp:intra_path_def)
        from ‹targetnode a -asx→⇩ι* pex› ‹asx = as'1@a2#asx'1›
        have "targetnode a -as'1@a2#asx'1→* pex" by(simp add:intra_path_def)
        hence "targetnode a -as'1→* sourcenode a2" and "valid_edge a2"
          and "targetnode a2 -asx'1→* pex" by(auto intro:path_split)
        from ‹targetnode a2 -asx'1→* pex› ‹asx = as'1@a2#asx'1›
          ‹targetnode a -asx→⇩ι* pex›
        have "targetnode a2 -asx'1→⇩ι* pex" by(simp add:intra_path_def)
        from ‹targetnode a -as'1→* sourcenode a2› 
          ‹targetnode a -as'1→⇩ι* sourcenode a1› 
        have "sourcenode a1 = sourcenode a2"
          by(fastforce intro:path_det simp:intra_path_def)
        from ‹asx = as'1@a2#asx'1› ‹n ∉ set (sourcenodes asx)›
        have "n ∉ set (sourcenodes asx'1)" by(simp add:sourcenodes_def)
        with ‹targetnode a2 -asx'1→⇩ι* pex› ‹method_exit pex›
          ‹asx = as'1@a2#asx'1›
        have "¬ n postdominates targetnode a2" by(fastforce simp:postdominate_def)
        from ‹asx = as'1@a2#asx'1› ‹targetnode a -asx→⇩ι* pex›
        have "intra_kind (kind a2)" by(simp add:intra_path_def)
        from ‹as' = as'1@a1#as'2› have "a1 ∈ set as'" by simp
        with ‹sourcenode a1 = sourcenode a2› last ‹valid_edge a2› 
          ‹intra_kind (kind a2)›
        have "n postdominates targetnode a2" by blast
        with ‹¬ n postdominates targetnode a2› have False by simp
        thus ?thesis by simp
      qed
    qed
  qed
qed



subsection ‹SDG without summary edges›


inductive cdep_edge :: "'node SDG_node ⇒ 'node SDG_node ⇒ bool" 
    ("_ ⟶⇘cd⇙ _" [51,0] 80)
  and ddep_edge :: "'node SDG_node ⇒ 'var ⇒ 'node SDG_node ⇒ bool"
    ("_ -_→⇩d⇩d _" [51,0,0] 80)
  and call_edge :: "'node SDG_node ⇒ 'pname ⇒ 'node SDG_node ⇒ bool" 
    ("_ -_→⇘call⇙ _" [51,0,0] 80)
  and return_edge :: "'node SDG_node ⇒ 'pname ⇒ 'node SDG_node ⇒ bool" 
    ("_ -_→⇘ret⇙ _" [51,0,0] 80)
  and param_in_edge :: "'node SDG_node ⇒ 'pname ⇒ 'var ⇒ 'node SDG_node ⇒ bool"
    ("_ -_:_→⇘in⇙ _" [51,0,0,0] 80)
  and param_out_edge :: "'node SDG_node ⇒ 'pname ⇒ 'var ⇒ 'node SDG_node ⇒ bool"
    ("_ -_:_→⇘out⇙ _" [51,0,0,0] 80)
  and SDG_edge :: "'node SDG_node ⇒ 'var option ⇒ 
                          ('pname × bool) option ⇒ 'node SDG_node ⇒ bool"

where
    (* Syntax *)
  "n ⟶⇘cd⇙ n' == SDG_edge n None None n'"
  | "n -V→⇩d⇩d n' == SDG_edge n (Some V) None n'"
  | "n -p→⇘call⇙ n' == SDG_edge n None (Some(p,True)) n'"
  | "n -p→⇘ret⇙ n' == SDG_edge n None (Some(p,False)) n'"
  | "n -p:V→⇘in⇙ n' == SDG_edge n (Some V) (Some(p,True)) n'"
  | "n -p:V→⇘out⇙ n' == SDG_edge n (Some V) (Some(p,False)) n'"

    (* Rules *)
  | SDG_cdep_edge:
    "⟦n = CFG_node m; n' = CFG_node m'; m controls m'⟧ ⟹ n ⟶⇘cd⇙ n'"
  | SDG_proc_entry_exit_cdep:
    "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; n = CFG_node (targetnode a);
      a' ∈ get_return_edges a; n' = CFG_node (sourcenode a')⟧ ⟹ n ⟶⇘cd⇙ n'"
  | SDG_parent_cdep_edge:
    "⟦valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n ≠ n'⟧ 
      ⟹ n ⟶⇘cd⇙ n'"
  | SDG_ddep_edge:"n influences V in n' ⟹ n -V→⇩d⇩d n'"
  | SDG_call_edge:
    "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; n = CFG_node (sourcenode a); 
      n' = CFG_node (targetnode a)⟧ ⟹ n -p→⇘call⇙ n'"
  | SDG_return_edge:
    "⟦valid_edge a; kind a = Q↩⇘p⇙f; n = CFG_node (sourcenode a); 
      n' = CFG_node (targetnode a)⟧ ⟹ n -p→⇘ret⇙ n'"
  | SDG_param_in_edge:
    "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; (p,ins,outs) ∈ set procs; V = ins!x;
      x < length ins; n = Actual_in (sourcenode a,x); n' = Formal_in (targetnode a,x)⟧
      ⟹ n -p:V→⇘in⇙ n'"
  | SDG_param_out_edge:
    "⟦valid_edge a; kind a = Q↩⇘p⇙f; (p,ins,outs) ∈ set procs; V = outs!x;
      x < length outs; n = Formal_out (sourcenode a,x); 
      n' = Actual_out (targetnode a,x)⟧
      ⟹ n -p:V→⇘out⇙ n'"


lemma cdep_edge_cases:
  "⟦n ⟶⇘cd⇙ n'; (parent_node n) controls (parent_node n') ⟹ P;
    ⋀a Q r p fs a'. ⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; a' ∈ get_return_edges a;
                  parent_node n = targetnode a; parent_node n' = sourcenode a'⟧ ⟹ P;
    ⋀m. ⟦n = CFG_node m; m = parent_node n'; n ≠ n'⟧ ⟹ P⟧ ⟹ P"
by -(erule SDG_edge.cases,auto)


lemma SDG_edge_valid_SDG_node:
  assumes "SDG_edge n Vopt popt n'" 
  shows "valid_SDG_node n" and "valid_SDG_node n'"
using ‹SDG_edge n Vopt popt n'›
proof(induct rule:SDG_edge.induct)
  case (SDG_cdep_edge n m n' m') 
  thus "valid_SDG_node n" "valid_SDG_node n'"
    by(fastforce elim:control_dependence_path elim:path_valid_node 
                simp:intra_path_def)+
next
  case (SDG_proc_entry_exit_cdep a Q r p f n a' n') case 1
  from ‹valid_edge a› ‹n = CFG_node (targetnode a)› show ?case by simp
next
  case (SDG_proc_entry_exit_cdep a Q r p f n a' n') case 2
  from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'" 
    by(rule get_return_edges_valid)
  with ‹n' = CFG_node (sourcenode a')› show ?case by simp
next
  case (SDG_ddep_edge n V n')
  thus "valid_SDG_node n" "valid_SDG_node n'" 
    by(auto intro:in_Use_valid_SDG_node in_Def_valid_SDG_node
             simp:data_dependence_def)
qed(fastforce intro:valid_SDG_CFG_node)+


lemma valid_SDG_node_cases: 
  assumes "valid_SDG_node n"
  shows "n = CFG_node (parent_node n) ∨ CFG_node (parent_node n) ⟶⇘cd⇙ n"
proof(cases n)
  case (CFG_node m) thus ?thesis by simp
next
  case (Formal_in z)
  from ‹n = Formal_in z› obtain m x where "z = (m,x)" by(cases z) auto
  with ‹valid_SDG_node n› ‹n = Formal_in z› have "CFG_node (parent_node n) ⟶⇘cd⇙ n"
    by -(rule SDG_parent_cdep_edge,auto)
  thus ?thesis by fastforce
next
  case (Formal_out z)
  from ‹n = Formal_out z› obtain m x where "z = (m,x)" by(cases z) auto
  with ‹valid_SDG_node n› ‹n = Formal_out z› have "CFG_node (parent_node n) ⟶⇘cd⇙ n"
    by -(rule SDG_parent_cdep_edge,auto)
  thus ?thesis by fastforce
next
  case (Actual_in z)
  from ‹n = Actual_in z› obtain m x where "z = (m,x)" by(cases z) auto
  with ‹valid_SDG_node n› ‹n = Actual_in z› have "CFG_node (parent_node n) ⟶⇘cd⇙ n"
    by -(rule SDG_parent_cdep_edge,auto)
  thus ?thesis by fastforce
next
  case (Actual_out z)
  from ‹n = Actual_out z› obtain m x where "z = (m,x)" by(cases z) auto
  with ‹valid_SDG_node n› ‹n = Actual_out z› have "CFG_node (parent_node n) ⟶⇘cd⇙ n"
    by -(rule SDG_parent_cdep_edge,auto)
  thus ?thesis by fastforce
qed


lemma SDG_cdep_edge_CFG_node: "n ⟶⇘cd⇙ n' ⟹ ∃m. n = CFG_node m"
by(induct n Vopt≡"None::'var option" popt≡"None::('pname × bool) option" n' 
   rule:SDG_edge.induct) auto

lemma SDG_call_edge_CFG_node: "n -p→⇘call⇙ n' ⟹ ∃m. n = CFG_node m"
by(induct n Vopt≡"None::'var option" popt≡"Some(p,True)" n' 
   rule:SDG_edge.induct) auto

lemma SDG_return_edge_CFG_node: "n -p→⇘ret⇙ n' ⟹ ∃m. n = CFG_node m"
by(induct n Vopt≡"None::'var option" popt≡"Some(p,False)" n' 
   rule:SDG_edge.induct) auto



lemma SDG_call_or_param_in_edge_unique_CFG_call_edge:
  "SDG_edge n Vopt (Some(p,True)) n'
  ⟹ ∃!a. valid_edge a ∧ sourcenode a = parent_node n ∧ 
          targetnode a = parent_node n' ∧ (∃Q r fs. kind a = Q:r↪⇘p⇙fs)"
proof(induct n Vopt "Some(p,True)" n' rule:SDG_edge.induct)
  case (SDG_call_edge a Q r fs n n')
  { fix a' 
    assume "valid_edge a'" and "sourcenode a' = parent_node n"
      and "targetnode a' = parent_node n'"
    from ‹sourcenode a' = parent_node n› ‹n = CFG_node (sourcenode a)›
    have "sourcenode a' = sourcenode a" by fastforce
    moreover from ‹targetnode a' = parent_node n'› ‹n' = CFG_node (targetnode a)›
    have "targetnode a' = targetnode a" by fastforce
    ultimately have "a' = a" using ‹valid_edge a'› ‹valid_edge a›
      by(fastforce intro:edge_det) }
  with ‹valid_edge a› ‹n = CFG_node (sourcenode a)› ‹n' = CFG_node (targetnode a)›
    ‹kind a = Q:r↪⇘p⇙fs› show ?case by(fastforce intro!:ex1I[of _ a])
next
  case (SDG_param_in_edge a Q r fs ins outs V x n n')
  { fix a' 
    assume "valid_edge a'" and "sourcenode a' = parent_node n"
      and "targetnode a' = parent_node n'"
    from ‹sourcenode a' = parent_node n› ‹n = Actual_in (sourcenode a,x)›
    have "sourcenode a' = sourcenode a" by fastforce
    moreover from ‹targetnode a' = parent_node n'› ‹n' = Formal_in (targetnode a,x)›
    have "targetnode a' = targetnode a" by fastforce
    ultimately have "a' = a" using ‹valid_edge a'› ‹valid_edge a›
      by(fastforce intro:edge_det) }
  with ‹valid_edge a› ‹n = Actual_in (sourcenode a,x)› 
    ‹n' = Formal_in (targetnode a,x)› ‹kind a = Q:r↪⇘p⇙fs›
  show ?case by(fastforce intro!:ex1I[of _ a])
qed simp_all


lemma SDG_return_or_param_out_edge_unique_CFG_return_edge:
  "SDG_edge n Vopt (Some(p,False)) n'
  ⟹ ∃!a. valid_edge a ∧ sourcenode a = parent_node n ∧ 
          targetnode a = parent_node n' ∧ (∃Q f. kind a = Q↩⇘p⇙f)"
proof(induct n Vopt "Some(p,False)" n' rule:SDG_edge.induct)
  case (SDG_return_edge a Q f n n')
  { fix a' 
    assume "valid_edge a'" and "sourcenode a' = parent_node n" 
      and "targetnode a' = parent_node n'"
    from ‹sourcenode a' = parent_node n› ‹n = CFG_node (sourcenode a)›
    have "sourcenode a' = sourcenode a" by fastforce
    moreover from ‹targetnode a' = parent_node n'› ‹n' = CFG_node (targetnode a)›
    have "targetnode a' = targetnode a" by fastforce
    ultimately have "a' = a" using ‹valid_edge a'› ‹valid_edge a›
      by(fastforce intro:edge_det) }
  with ‹valid_edge a› ‹n = CFG_node (sourcenode a)› ‹n' = CFG_node (targetnode a)›
    ‹kind a = Q↩⇘p⇙f› show ?case by(fastforce intro!:ex1I[of _ a])
next
  case (SDG_param_out_edge a Q f ins outs V x n n')
  { fix a' 
    assume "valid_edge a'" and "sourcenode a' = parent_node n"
      and "targetnode a' = parent_node n'"
    from ‹sourcenode a' = parent_node n› ‹n = Formal_out (sourcenode a,x)›
    have "sourcenode a' = sourcenode a" by fastforce
    moreover from ‹targetnode a' = parent_node n'› ‹n' = Actual_out (targetnode a,x)›
    have "targetnode a' = targetnode a" by fastforce
    ultimately have "a' = a" using ‹valid_edge a'› ‹valid_edge a›
      by(fastforce intro:edge_det) }
  with ‹valid_edge a› ‹n = Formal_out (sourcenode a,x)›
    ‹n' = Actual_out (targetnode a,x)› ‹kind a = Q↩⇘p⇙f›
  show ?case by(fastforce intro!:ex1I[of _ a])
qed simp_all


lemma Exit_no_SDG_edge_source:
  "SDG_edge (CFG_node (_Exit_)) Vopt popt n' ⟹ False"
proof(induct "CFG_node (_Exit_)" Vopt popt n' rule:SDG_edge.induct)
  case (SDG_cdep_edge m n' m')
  hence "(_Exit_) controls m'" by simp
  thus ?case by fastforce
next
  case (SDG_proc_entry_exit_cdep a Q r p fs a' n')
  from ‹CFG_node (_Exit_) = CFG_node (targetnode a)›
  have "targetnode a = (_Exit_)" by simp
  from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc (targetnode a) = p"
    by(rule get_proc_call)
  with ‹targetnode a = (_Exit_)› have "p = Main"
    by(auto simp:get_proc_Exit)
  with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have False
    by(fastforce intro:Main_no_call_target)
  thus ?thesis by simp
next
  case (SDG_parent_cdep_edge n' m)
  from ‹CFG_node (_Exit_) = CFG_node m› 
  have [simp]:"m = (_Exit_)" by simp
  with ‹valid_SDG_node n'› ‹m = parent_node n'› ‹CFG_node (_Exit_) ≠ n'›
  have False by -(drule valid_SDG_node_parent_Exit,simp+)
  thus ?thesis by simp
next
  case (SDG_ddep_edge V n')
  hence "(CFG_node (_Exit_)) influences V in n'" by simp
  with Exit_empty show ?case
    by(fastforce dest:path_Exit_source SDG_Def_parent_Def 
                simp:data_dependence_def intra_path_def)
next
  case (SDG_call_edge a Q r p fs n')
  from ‹CFG_node (_Exit_) = CFG_node (sourcenode a)›
  have "sourcenode a = (_Exit_)" by simp
  with ‹valid_edge a› show ?case by(rule Exit_source)
next
  case (SDG_return_edge a Q p f n')
  from ‹CFG_node (_Exit_) = CFG_node (sourcenode a)›
  have "sourcenode a = (_Exit_)" by simp
  with ‹valid_edge a› show ?case by(rule Exit_source)
qed simp_all


subsection ‹Intraprocedural paths in the SDG›

inductive intra_SDG_path :: 
  "'node SDG_node ⇒ 'node SDG_node list ⇒ 'node SDG_node ⇒ bool"
("_ i-_→⇩d* _" [51,0,0] 80) 

where iSp_Nil:
  "valid_SDG_node n ⟹ n i-[]→⇩d* n"

  | iSp_Append_cdep:
  "⟦n i-ns→⇩d* n''; n'' ⟶⇘cd⇙ n'⟧ ⟹ n i-ns@[n'']→⇩d* n'"

  | iSp_Append_ddep:
  "⟦n i-ns→⇩d* n''; n'' -V→⇩d⇩d n'; n'' ≠ n'⟧ ⟹ n i-ns@[n'']→⇩d* n'"


lemma intra_SDG_path_Append:
  "⟦n'' i-ns'→⇩d* n'; n i-ns→⇩d* n''⟧ ⟹ n i-ns@ns'→⇩d* n'"
by(induct rule:intra_SDG_path.induct,
   auto intro:intra_SDG_path.intros simp:append_assoc[THEN sym] simp del:append_assoc)


lemma intra_SDG_path_valid_SDG_node:
  assumes "n i-ns→⇩d* n'" shows "valid_SDG_node n" and "valid_SDG_node n'"
using ‹n i-ns→⇩d* n'›
by(induct rule:intra_SDG_path.induct,
   auto intro:SDG_edge_valid_SDG_node valid_SDG_CFG_node)


lemma intra_SDG_path_intra_CFG_path:
  assumes "n i-ns→⇩d* n'"
  obtains as where "parent_node n -as→⇩ι* parent_node n'" 
proof(atomize_elim)
  from ‹n i-ns→⇩d* n'›
  show "∃as. parent_node n -as→⇩ι* parent_node n'"
  proof(induct rule:intra_SDG_path.induct)
    case (iSp_Nil n)
    from ‹valid_SDG_node n› have "valid_node (parent_node n)"
      by(rule valid_SDG_CFG_node)
    hence "parent_node n -[]→* parent_node n" by(rule empty_path)
    thus ?case by(auto simp:intra_path_def)
  next
    case (iSp_Append_cdep n ns n'' n')
    from ‹∃as. parent_node n -as→⇩ι* parent_node n''›
    obtain as where "parent_node n -as→⇩ι* parent_node n''" by blast
    from ‹n'' ⟶⇘cd⇙ n'› show ?case
    proof(rule cdep_edge_cases)
      assume "parent_node n'' controls parent_node n'"
      then obtain as' where "parent_node n'' -as'→⇩ι* parent_node n'" and "as' ≠ []"
        by(erule control_dependence_path)
      with ‹parent_node n -as→⇩ι* parent_node n''› 
      have "parent_node n -as@as'→⇩ι* parent_node n'" by -(rule intra_path_Append)
      thus ?thesis by blast
    next
      fix a Q r p fs a'
      assume "valid_edge a" and "kind a = Q:r↪⇘p⇙fs" and "a' ∈ get_return_edges a"
        and "parent_node n'' = targetnode a" and "parent_node n' = sourcenode a'"
      then obtain a'' where "valid_edge a''" and "sourcenode a'' = targetnode a"
        and "targetnode a'' = sourcenode a'" and "kind a'' = (λcf. False)⇩√"
        by(auto dest:intra_proc_additional_edge)
      hence "targetnode a -[a'']→⇩ι* sourcenode a'"
        by(fastforce dest:path_edge simp:intra_path_def intra_kind_def)
      with ‹parent_node n'' = targetnode a› ‹parent_node n' = sourcenode a'› 
      have "∃as'. parent_node n'' -as'→⇩ι* parent_node n' ∧ as' ≠ []" by fastforce
      then obtain as' where "parent_node n'' -as'→⇩ι* parent_node n'" and "as' ≠ []"
        by blast
      with ‹parent_node n -as→⇩ι* parent_node n''›
      have "parent_node n -as@as'→⇩ι* parent_node n'" by -(rule intra_path_Append)
      thus ?thesis by blast
    next
      fix m assume "n'' = CFG_node m" and "m = parent_node n'"
      with ‹parent_node n -as→⇩ι* parent_node n''› show ?thesis by fastforce
    qed
  next
    case (iSp_Append_ddep n ns n'' V n')
    from ‹∃as. parent_node n -as→⇩ι* parent_node n''›
    obtain as where "parent_node n -as→⇩ι* parent_node n''" by blast 
    from ‹n'' -V→⇩d⇩d n'› have "n'' influences V in n'"
      by(fastforce elim:SDG_edge.cases)
    then obtain as' where "parent_node n'' -as'→⇩ι* parent_node n'"
      by(auto simp:data_dependence_def)
    with ‹parent_node n -as→⇩ι* parent_node n''› 
    have "parent_node n -as@as'→⇩ι* parent_node n'" by -(rule intra_path_Append)
    thus ?case by blast
  qed
qed


subsection ‹Control dependence paths in the SDG›

inductive cdep_SDG_path :: 
  "'node SDG_node ⇒ 'node SDG_node list ⇒ 'node SDG_node ⇒ bool"
("_ cd-_→⇩d* _" [51,0,0] 80) 

where cdSp_Nil:
  "valid_SDG_node n ⟹ n cd-[]→⇩d* n"

  | cdSp_Append_cdep:
  "⟦n cd-ns→⇩d* n''; n'' ⟶⇘cd⇙ n'⟧ ⟹ n cd-ns@[n'']→⇩d* n'"


lemma cdep_SDG_path_intra_SDG_path:
  "n cd-ns→⇩d* n' ⟹ n i-ns→⇩d* n'"
by(induct rule:cdep_SDG_path.induct,auto intro:intra_SDG_path.intros)


lemma Entry_cdep_SDG_path:
  assumes "(_Entry_) -as→⇩ι* n'" and "inner_node n'" and "¬ method_exit n'"
  obtains ns where "CFG_node (_Entry_) cd-ns→⇩d* CFG_node n'"
  and "ns ≠ []" and "∀n'' ∈ set ns. parent_node n'' ∈ set(sourcenodes as)"
proof(atomize_elim)
  from ‹(_Entry_) -as→⇩ι* n'› ‹inner_node n'› ‹¬ method_exit n'›
  show "∃ns. CFG_node (_Entry_) cd-ns→⇩d* CFG_node n' ∧ ns ≠ [] ∧
    (∀n'' ∈ set ns. parent_node n'' ∈ set(sourcenodes as))"
  proof(induct as arbitrary:n' rule:length_induct)
    fix as n'
    assume IH:"∀as'. length as' < length as ⟶
      (∀n''. (_Entry_) -as'→⇩ι* n'' ⟶ inner_node n'' ⟶ ¬ method_exit n'' ⟶
        (∃ns. CFG_node (_Entry_) cd-ns→⇩d* CFG_node n'' ∧ ns ≠ [] ∧
              (∀nx∈set ns. parent_node nx ∈ set (sourcenodes as'))))"
      and "(_Entry_) -as→⇩ι* n'" and "inner_node n'" and "¬ method_exit n'"
    thus "∃ns. CFG_node (_Entry_) cd-ns→⇩d* CFG_node n' ∧ ns ≠ [] ∧
      (∀n''∈set ns. parent_node n'' ∈ set (sourcenodes as))"
    proof -
      have "∃ax asx zs. (_Entry_) -ax#asx→⇩ι* n' ∧ n' ∉ set (sourcenodes (ax#asx)) ∧ 
                        as = (ax#asx)@zs"
      proof(cases "n' ∈ set (sourcenodes as)")
        case True
        hence "∃n'' ∈ set(sourcenodes as). n' = n''" by simp
        then obtain ns' ns'' where "sourcenodes as = ns'@n'#ns''"
          and "∀n'' ∈ set ns'. n' ≠ n''"
          by(fastforce elim!:split_list_first_propE)
        from ‹sourcenodes as = ns'@n'#ns''› obtain xs ys ax
          where "sourcenodes xs = ns'" and "as = xs@ax#ys"
          and "sourcenode ax = n'"
          by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
        from ‹∀n'' ∈ set ns'. n' ≠ n''› ‹sourcenodes xs = ns'›
        have "n' ∉ set(sourcenodes xs)" by fastforce
        from ‹(_Entry_) -as→⇩ι* n'› ‹as = xs@ax#ys› have "(_Entry_) -xs@ax#ys→⇩ι* n'"
          by simp
        with ‹sourcenode ax = n'› have "(_Entry_) -xs→⇩ι* n'" 
          by(fastforce dest:path_split simp:intra_path_def)
        with ‹inner_node n'› have "xs ≠ []"
          by(fastforce elim:path.cases simp:intra_path_def)
        with ‹n' ∉ set(sourcenodes xs)› ‹(_Entry_) -xs→⇩ι* n'› ‹as = xs@ax#ys›
        show ?thesis by(cases xs) auto
      next
        case False
        with ‹(_Entry_) -as→⇩ι* n'› ‹inner_node n'›
        show ?thesis by(cases as)(auto elim:path.cases simp:intra_path_def)
      qed
      then obtain ax asx zs where "(_Entry_) -ax#asx→⇩ι* n'" 
        and "n' ∉ set (sourcenodes (ax#asx))" and "as = (ax#asx)@zs" by blast
      show ?thesis
      proof(cases "∀a' a''. a' ∈ set asx ∧ sourcenode a' = sourcenode a'' ∧ 
          valid_edge a'' ∧ intra_kind(kind a'') ⟶ n' postdominates targetnode a''")
        case True
        have "(_Exit_) -[]→⇩ι* (_Exit_)" 
          by(fastforce intro:empty_path simp:intra_path_def)
        hence "¬ n' postdominates (_Exit_)"
          by(fastforce simp:postdominate_def sourcenodes_def method_exit_def)
        from ‹(_Entry_) -ax#asx→⇩ι* n'› have "(_Entry_) -[]@ax#asx→⇩ι* n'" by simp
        from ‹(_Entry_) -ax#asx→⇩ι* n'› have [simp]:"sourcenode ax = (_Entry_)" 
          and "valid_edge ax"
          by(auto intro:path_split_Cons simp:intra_path_def)
        from Entry_Exit_edge obtain a' where "sourcenode a' = (_Entry_)"
          and "targetnode a' = (_Exit_)" and "valid_edge a'" 
          and "intra_kind(kind a')" by(auto simp:intra_kind_def)
        with ‹(_Entry_) -[]@ax#asx→⇩ι* n'› ‹¬ n' postdominates (_Exit_)›
          ‹valid_edge ax› True ‹sourcenode ax = (_Entry_)› 
          ‹n' ∉ set (sourcenodes (ax#asx))› ‹inner_node n'› ‹¬ method_exit n'›
        have "sourcenode ax controls n'"
          by -(erule which_node_intra_standard_control_dependence_source
                     [of _ _ _ _ _ _ a'],auto)
        hence "CFG_node (_Entry_) ⟶⇘cd⇙ CFG_node n'"
          by(fastforce intro:SDG_cdep_edge)
        hence "CFG_node (_Entry_) cd-[]@[CFG_node (_Entry_)]→⇩d* CFG_node n'"
          by(fastforce intro:cdSp_Append_cdep cdSp_Nil)
        moreover
        from ‹as = (ax#asx)@zs› have "(_Entry_) ∈ set(sourcenodes as)"
          by(simp add:sourcenodes_def)
        ultimately show ?thesis by fastforce
      next
        case False
        hence "∃a' ∈ set asx. ∃a''. sourcenode a' = sourcenode a'' ∧ valid_edge a'' ∧
          intra_kind(kind a'') ∧ ¬ n' postdominates targetnode a''"
          by fastforce
        then obtain ax' asx' asx'' where "asx = asx'@ax'#asx'' ∧
          (∃a''. sourcenode ax' = sourcenode a'' ∧ valid_edge a'' ∧
          intra_kind(kind a'') ∧ ¬ n' postdominates targetnode a'') ∧
          (∀z ∈ set asx''. ¬ (∃a''. sourcenode z = sourcenode a'' ∧ valid_edge a'' ∧
          intra_kind(kind a'') ∧ ¬ n' postdominates targetnode a''))"
          by(blast elim!:split_list_last_propE)
        then obtain ai where "asx = asx'@ax'#asx''"
          and "sourcenode ax' = sourcenode ai"
          and "valid_edge ai" and "intra_kind(kind ai)"
          and "¬ n' postdominates targetnode ai"
          and "∀z ∈ set asx''. ¬ (∃a''. sourcenode z = sourcenode a'' ∧ 
          valid_edge a'' ∧ intra_kind(kind a'') ∧ ¬ n' postdominates targetnode a'')"
          by blast
        from ‹(_Entry_) -ax#asx→⇩ι* n'› ‹asx = asx'@ax'#asx''›
        have "(_Entry_) -(ax#asx')@ax'#asx''→⇩ι* n'" by simp
        from ‹n' ∉ set (sourcenodes (ax#asx))› ‹asx = asx'@ax'#asx''›
        have "n' ∉ set (sourcenodes (ax'#asx''))"
          by(auto simp:sourcenodes_def)
        with ‹inner_node n'› ‹¬ n' postdominates targetnode ai›
          ‹n' ∉ set (sourcenodes (ax'#asx''))› ‹sourcenode ax' = sourcenode ai›
          ‹∀z ∈ set asx''. ¬ (∃a''. sourcenode z = sourcenode a'' ∧ 
          valid_edge a'' ∧ intra_kind(kind a'') ∧ ¬ n' postdominates targetnode a'')›
          ‹valid_edge ai› ‹intra_kind(kind ai)› ‹¬ method_exit n'›
          ‹(_Entry_) -(ax#asx')@ax'#asx''→⇩ι* n'›
        have "sourcenode ax' controls n'"
          by(fastforce intro!:which_node_intra_standard_control_dependence_source)
        hence "CFG_node (sourcenode ax') ⟶⇘cd⇙ CFG_node n'"
          by(fastforce intro:SDG_cdep_edge)
        from ‹(_Entry_) -(ax#asx')@ax'#asx''→⇩ι* n'›
        have "(_Entry_) -ax#asx'→⇩ι* sourcenode ax'" and "valid_edge ax'"
          by(auto intro:path_split simp:intra_path_def simp del:append_Cons)
        from ‹asx = asx'@ax'#asx''› ‹as = (ax#asx)@zs›
        have "length (ax#asx') < length as" by simp
        from ‹valid_edge ax'› have "valid_node (sourcenode ax')" by simp
        hence "inner_node (sourcenode ax')"
        proof(cases "sourcenode ax'" rule:valid_node_cases)
          case Entry 
          with ‹(_Entry_) -ax#asx'→⇩ι* sourcenode ax'›
          have "(_Entry_) -ax#asx'→* (_Entry_)" by(simp add:intra_path_def)
          hence False by(fastforce dest:path_Entry_target)
          thus ?thesis by simp
        next
          case Exit
          with ‹valid_edge ax'› have False by(rule Exit_source)
          thus ?thesis by simp
        qed simp
        from ‹asx = asx'@ax'#asx''› ‹(_Entry_) -ax#asx→⇩ι* n'›
        have "intra_kind (kind ax')" by(simp add:intra_path_def)
        have "¬ method_exit (sourcenode ax')"
        proof
          assume "method_exit (sourcenode ax')"
          thus False
          proof(rule method_exit_cases)
            assume "sourcenode ax' = (_Exit_)"
            with ‹valid_edge ax'› show False by(rule Exit_source)
          next
            fix x Q f p assume " sourcenode ax' = sourcenode x"
              and "valid_edge x" and "kind x = Q↩⇘p⇙f"
            from ‹valid_edge x› ‹kind x = Q↩⇘p⇙f› ‹sourcenode ax' = sourcenode x›
            ‹valid_edge ax'› ‹intra_kind (kind ax')› show False
              by(fastforce dest:return_edges_only simp:intra_kind_def)
          qed
        qed
        with IH ‹length (ax#asx') < length as› ‹(_Entry_) -ax#asx'→⇩ι* sourcenode ax'›
          ‹inner_node (sourcenode ax')›
        obtain ns where "CFG_node (_Entry_) cd-ns→⇩d* CFG_node (sourcenode ax')"
          and "ns ≠ []" 
          and "∀n'' ∈ set ns. parent_node n'' ∈ set(sourcenodes (ax#asx'))"
          by blast
        from ‹CFG_node (_Entry_) cd-ns→⇩d* CFG_node (sourcenode ax')›
          ‹CFG_node (sourcenode ax') ⟶⇘cd⇙ CFG_node n'›
        have "CFG_node (_Entry_) cd-ns@[CFG_node (sourcenode ax')]→⇩d* CFG_node n'"
          by(fastforce intro:cdSp_Append_cdep)
        from ‹as = (ax#asx)@zs› ‹asx = asx'@ax'#asx''›
        have "sourcenode ax' ∈ set(sourcenodes as)" by(simp add:sourcenodes_def)
        with ‹∀n'' ∈ set ns. parent_node n'' ∈ set(sourcenodes (ax#asx'))›
          ‹as = (ax#asx)@zs› ‹asx = asx'@ax'#asx''›
        have "∀n'' ∈ set (ns@[CFG_node (sourcenode ax')]).
          parent_node n'' ∈ set(sourcenodes as)"
          by(fastforce simp:sourcenodes_def)
        with ‹CFG_node (_Entry_) cd-ns@[CFG_node (sourcenode ax')]→⇩d* CFG_node n'›
        show ?thesis by fastforce
      qed
    qed
  qed
qed


lemma in_proc_cdep_SDG_path:
  assumes "n -as→⇩ι* n'" and "n ≠ n'" and "n' ≠ (_Exit_)" and "valid_edge a"
  and "kind a = Q:r↪⇘p⇙fs" and "targetnode a = n"
  obtains ns where "CFG_node n cd-ns→⇩d* CFG_node n'"
  and "ns ≠ []" and "∀n'' ∈ set ns. parent_node n'' ∈ set(sourcenodes as)"
proof(atomize_elim)
  show "∃ns. CFG_node n cd-ns→⇩d* CFG_node n' ∧
             ns ≠ [] ∧ (∀n''∈set ns. parent_node n'' ∈ set (sourcenodes as))"
  proof(cases "∀ax. valid_edge ax ∧ sourcenode ax = n' ⟶ 
                    ax ∉ get_return_edges a")
    case True
    from ‹n -as→⇩ι* n'› ‹n ≠ n'› ‹n' ≠ (_Exit_)›
      ‹∀ax. valid_edge ax ∧ sourcenode ax = n' ⟶ ax ∉ get_return_edges a›
    show "∃ns. CFG_node n cd-ns→⇩d* CFG_node n' ∧ ns ≠ [] ∧
      (∀n'' ∈ set ns. parent_node n'' ∈ set(sourcenodes as))"
    proof(induct as arbitrary:n' rule:length_induct)
      fix as n'
      assume IH:"∀as'. length as' < length as ⟶
        (∀n''. n -as'→⇩ι* n'' ⟶ n ≠ n'' ⟶ n'' ≠ (_Exit_) ⟶
          (∀ax. valid_edge ax ∧ sourcenode ax = n'' ⟶ ax ∉ get_return_edges a) ⟶
            (∃ns. CFG_node n cd-ns→⇩d* CFG_node n'' ∧ ns ≠ [] ∧
                  (∀n''∈set ns. parent_node n'' ∈ set (sourcenodes as'))))"
        and "n -as→⇩ι* n'" and "n ≠ n'" and "n' ≠ (_Exit_)"
        and "∀ax. valid_edge ax ∧ sourcenode ax = n' ⟶ ax ∉ get_return_edges a"
      show "∃ns. CFG_node n cd-ns→⇩d* CFG_node n' ∧ ns ≠ [] ∧
                 (∀n''∈set ns. parent_node n'' ∈ set (sourcenodes as))"
      proof(cases "method_exit n'")
        case True
        thus ?thesis
        proof(rule method_exit_cases)
          assume "n' = (_Exit_)"
          with ‹n' ≠ (_Exit_)› have False by simp
          thus ?thesis by simp
        next
          fix a' Q' f' p'
          assume "n' = sourcenode a'" and "valid_edge a'" and "kind a' = Q'↩⇘p'⇙f'"
          from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc(targetnode a) = p"
            by(rule get_proc_call)
          from ‹n -as→⇩ι* n'› have "get_proc n = get_proc n'" 
            by(rule intra_path_get_procs)
          with ‹get_proc(targetnode a) = p› ‹targetnode a = n›
          have "get_proc (targetnode a) = get_proc n'" by simp
          from ‹valid_edge a'› ‹kind a' = Q'↩⇘p'⇙f'›
          have "get_proc (sourcenode a') = p'" by(rule get_proc_return)
          with ‹n' = sourcenode a'› ‹get_proc (targetnode a) = get_proc n'› 
            ‹get_proc (targetnode a) = p› have "p = p'" by simp
          with ‹valid_edge a'› ‹kind a' = Q'↩⇘p'⇙f'›
          obtain ax where "valid_edge ax" and "∃Q r fs. kind ax = Q:r↪⇘p⇙fs"
            and "a' ∈ get_return_edges ax" by(auto dest:return_needs_call)
          hence "CFG_node (targetnode ax) ⟶⇘cd⇙ CFG_node (sourcenode a')"
            by(fastforce intro:SDG_proc_entry_exit_cdep)
          with ‹valid_edge ax› 
          have "CFG_node (targetnode ax) cd-[]@[CFG_node (targetnode ax)]→⇩d* 
            CFG_node (sourcenode a')"
            by(fastforce intro:cdep_SDG_path.intros)
          from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹valid_edge ax› 
            ‹∃Q r fs. kind ax = Q:r↪⇘p⇙fs› have "targetnode a = targetnode ax"
            by(fastforce intro:same_proc_call_unique_target)
          from ‹n -as→⇩ι* n'› ‹n ≠ n'›
          have "as ≠ []" by(fastforce elim:path.cases simp:intra_path_def)
          with ‹n -as→⇩ι* n'› have "hd (sourcenodes as) = n"
            by(fastforce intro:path_sourcenode simp:intra_path_def)
          moreover
          from ‹as ≠ []› have "hd (sourcenodes as) ∈ set (sourcenodes as)"
            by(fastforce intro:hd_in_set simp:sourcenodes_def)
          ultimately have "n ∈ set (sourcenodes as)" by simp
          with ‹n' = sourcenode a'› ‹targetnode a = targetnode ax›
            ‹targetnode a = n›
            ‹CFG_node (targetnode ax) cd-[]@[CFG_node (targetnode ax)]→⇩d* 
            CFG_node (sourcenode a')›
          show ?thesis by fastforce
        qed
      next
        case False
        from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› obtain a' 
          where "a' ∈ get_return_edges a"
          by(fastforce dest:get_return_edge_call)
        with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› obtain Q' f' where "kind a' = Q'↩⇘p⇙f'"
          by(fastforce dest!:call_return_edges)
        with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹a' ∈ get_return_edges a› obtain a''
          where "valid_edge a''" and "sourcenode a'' = targetnode a" 
          and "targetnode a'' = sourcenode a'" and "kind a'' = (λcf. False)⇩√"
          by -(drule intra_proc_additional_edge,auto)
        from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'"
          by(rule get_return_edges_valid)
        have "∃ax asx zs. n -ax#asx→⇩ι* n' ∧ n' ∉ set (sourcenodes (ax#asx)) ∧ 
                          as = (ax#asx)@zs"
        proof(cases "n' ∈ set (sourcenodes as)")
          case True
          hence "∃n'' ∈ set(sourcenodes as). n' = n''" by simp
          then obtain ns' ns'' where "sourcenodes as = ns'@n'#ns''"
            and "∀n'' ∈ set ns'. n' ≠ n''"
            by(fastforce elim!:split_list_first_propE)
          from ‹sourcenodes as = ns'@n'#ns''› obtain xs ys ax
            where "sourcenodes xs = ns'" and "as = xs@ax#ys"
            and "sourcenode ax = n'"
            by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
          from ‹∀n'' ∈ set ns'. n' ≠ n''› ‹sourcenodes xs = ns'›
          have "n' ∉ set(sourcenodes xs)" by fastforce
          from ‹n -as→⇩ι* n'› ‹as = xs@ax#ys› have "n -xs@ax#ys→⇩ι* n'" by simp
          with ‹sourcenode ax = n'› have "n -xs→⇩ι* n'" 
            by(fastforce dest:path_split simp:intra_path_def)
          with ‹n ≠ n'› have "xs ≠ []" by(fastforce simp:intra_path_def)
          with ‹n' ∉ set(sourcenodes xs)› ‹n -xs→⇩ι* n'› ‹as = xs@ax#ys› show ?thesis
            by(cases xs) auto
        next
          case False
          with ‹n -as→⇩ι* n'› ‹n ≠ n'› 
          show ?thesis by(cases as)(auto simp:intra_path_def)
        qed
        then obtain ax asx zs where "n -ax#asx→⇩ι* n'" 
          and "n' ∉ set (sourcenodes (ax#asx))" and "as = (ax#asx)@zs" by blast
        from ‹n -ax#asx→⇩ι* n'› ‹n' ≠ (_Exit_)› have "inner_node n'"
          by(fastforce intro:path_valid_node simp:inner_node_def intra_path_def)
        from ‹valid_edge a› ‹targetnode a = n› have "valid_node n" by fastforce
        show ?thesis
        proof(cases "∀a' a''. a' ∈ set asx ∧ sourcenode a' = sourcenode a'' ∧ 
            valid_edge a'' ∧ intra_kind(kind a'') ⟶ 
            n' postdominates targetnode a''")
          case True
          from ‹targetnode a = n› ‹sourcenode a'' = targetnode a› 
            ‹kind a'' = (λcf. False)⇩√›
          have "sourcenode a'' = n" and "intra_kind(kind a'')"
            by(auto simp:intra_kind_def)
          { fix as' assume "targetnode a'' -as'→⇩ι* n'"
            from ‹valid_edge a'› ‹targetnode a'' = sourcenode a'› 
              ‹a' ∈ get_return_edges a› 
              ‹∀ax. valid_edge ax ∧ sourcenode ax = n' ⟶ ax ∉ get_return_edges a›
            have "targetnode a'' ≠ n'" by fastforce
            with ‹targetnode a'' -as'→⇩ι* n'› obtain ax' where "valid_edge ax'"
              and "targetnode a'' = sourcenode ax'" and "intra_kind(kind ax')"
              by(clarsimp simp:intra_path_def)(erule path.cases,fastforce+)
            from ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'› ‹valid_edge ax'›
              ‹targetnode a'' = sourcenode a'› ‹targetnode a'' = sourcenode ax'›
              ‹intra_kind(kind ax')›
            have False by(fastforce dest:return_edges_only simp:intra_kind_def) }
          hence "¬ n' postdominates targetnode a''"
            by(fastforce elim:postdominate_implies_inner_path)
          from ‹n -ax#asx→⇩ι* n'› have "sourcenode ax = n"
            by(auto intro:path_split_Cons simp:intra_path_def)
          from ‹n -ax#asx→⇩ι* n'› have "n -[]@ax#asx→⇩ι* n'" by simp
          from this ‹sourcenode a'' = n› ‹sourcenode ax = n› True
            ‹n' ∉ set (sourcenodes (ax#asx))› ‹valid_edge a''› ‹intra_kind(kind a'')›
            ‹inner_node n'› ‹¬ method_exit n'› ‹¬ n' postdominates targetnode a''›
          have "n controls n'"
            by(fastforce intro!:which_node_intra_standard_control_dependence_source)
          hence "CFG_node n ⟶⇘cd⇙ CFG_node n'"
            by(fastforce intro:SDG_cdep_edge)
          with ‹valid_node n› have "CFG_node n cd-[]@[CFG_node n]→⇩d* CFG_node n'"
            by(fastforce intro:cdSp_Append_cdep cdSp_Nil)
          moreover
          from ‹as = (ax#asx)@zs› ‹sourcenode ax = n› have "n ∈ set(sourcenodes as)"
            by(simp add:sourcenodes_def)
          ultimately show ?thesis by fastforce
        next
          case False
          hence "∃a' ∈ set asx. ∃a''. sourcenode a' = sourcenode a'' ∧ 
            valid_edge a'' ∧ intra_kind(kind a'') ∧ 
            ¬ n' postdominates targetnode a''"
            by fastforce
          then obtain ax' asx' asx'' where "asx = asx'@ax'#asx'' ∧
            (∃a''. sourcenode ax' = sourcenode a'' ∧ valid_edge a'' ∧
            intra_kind(kind a'') ∧ ¬ n' postdominates targetnode a'') ∧
            (∀z ∈ set asx''. ¬ (∃a''. sourcenode z = sourcenode a'' ∧ 
            valid_edge a'' ∧ intra_kind(kind a'') ∧ 
            ¬ n' postdominates targetnode a''))"
            by(blast elim!:split_list_last_propE)
          then obtain ai where "asx = asx'@ax'#asx''"
            and "sourcenode ax' = sourcenode ai"
            and "valid_edge ai" and "intra_kind(kind ai)"
            and "¬ n' postdominates targetnode ai"
            and "∀z ∈ set asx''. ¬ (∃a''. sourcenode z = sourcenode a'' ∧ 
            valid_edge a'' ∧ intra_kind(kind a'') ∧ 
            ¬ n' postdominates targetnode a'')"
            by blast
          from ‹asx = asx'@ax'#asx''› ‹n -ax#asx→⇩ι* n'›
          have "n -(ax#asx')@ax'#asx''→⇩ι* n'" by simp
          from ‹n' ∉ set (sourcenodes (ax#asx))› ‹asx = asx'@ax'#asx''›
          have "n' ∉ set (sourcenodes (ax'#asx''))"
            by(auto simp:sourcenodes_def)
          with ‹inner_node n'› ‹¬ n' postdominates targetnode ai›
            ‹n -(ax#asx')@ax'#asx''→⇩ι* n'› ‹sourcenode ax' = sourcenode ai›
            ‹∀z ∈ set asx''. ¬ (∃a''. sourcenode z = sourcenode a'' ∧ 
            valid_edge a'' ∧ intra_kind(kind a'') ∧ 
            ¬ n' postdominates targetnode a'')›
            ‹valid_edge ai› ‹intra_kind(kind ai)› ‹¬ method_exit n'›
          have "sourcenode ax' controls n'"
            by(fastforce intro!:which_node_intra_standard_control_dependence_source)
          hence "CFG_node (sourcenode ax') ⟶⇘cd⇙ CFG_node n'"
            by(fastforce intro:SDG_cdep_edge)
          from ‹n -(ax#asx')@ax'#asx''→⇩ι* n'›
          have "n -ax#asx'→⇩ι* sourcenode ax'" and "valid_edge ax'"
            by(auto intro:path_split simp:intra_path_def simp del:append_Cons)
          from ‹asx = asx'@ax'#asx''› ‹as = (ax#asx)@zs›
          have "length (ax#asx') < length as" by simp
          from ‹as = (ax#asx)@zs› ‹asx = asx'@ax'#asx''›
          have "sourcenode ax' ∈ set(sourcenodes as)" by(simp add:sourcenodes_def)
          show ?thesis
          proof(cases "n = sourcenode ax'")
            case True
            with ‹CFG_node (sourcenode ax') ⟶⇘cd⇙ CFG_node n'› ‹valid_edge ax'›
            have "CFG_node n cd-[]@[CFG_node n]→⇩d* CFG_node n'"
              by(fastforce intro:cdSp_Append_cdep cdSp_Nil)
            with ‹sourcenode ax' ∈ set(sourcenodes as)› True show ?thesis by fastforce
          next
            case False
            from ‹valid_edge ax'› have "sourcenode ax' ≠ (_Exit_)"
              by -(rule ccontr,fastforce elim!:Exit_source)
            from ‹n -ax#asx'→⇩ι* sourcenode ax'› have "n = sourcenode ax"
              by(fastforce intro:path_split_Cons simp:intra_path_def)
            show ?thesis
            proof(cases "∀ax. valid_edge ax ∧ sourcenode ax = sourcenode ax' ⟶
                ax ∉ get_return_edges a")
              case True
              from ‹asx = asx'@ax'#asx''› ‹n -ax#asx→⇩ι* n'›
              have "intra_kind (kind ax')" by(simp add:intra_path_def)
              have "¬ method_exit (sourcenode ax')"
              proof
                assume "method_exit (sourcenode ax')"
                thus False
                proof(rule method_exit_cases)
                  assume "sourcenode ax' = (_Exit_)"
                  with ‹valid_edge ax'› show False by(rule Exit_source)
                next
                  fix x Q f p assume " sourcenode ax' = sourcenode x"
                    and "valid_edge x" and "kind x = Q↩⇘p⇙f"
                  from ‹valid_edge x› ‹kind x = Q↩⇘p⇙f› ‹sourcenode ax' = sourcenode x›
                    ‹valid_edge ax'› ‹intra_kind (kind ax')› show False
                    by(fastforce dest:return_edges_only simp:intra_kind_def)
                qed
              qed
              with IH ‹length (ax#asx') < length as› ‹n -ax#asx'→⇩ι* sourcenode ax'›
                ‹n ≠ sourcenode ax'› ‹sourcenode ax' ≠ (_Exit_)› True
              obtain ns where "CFG_node n cd-ns→⇩d* CFG_node (sourcenode ax')"
                and "ns ≠ []" 
                and "∀n''∈set ns. parent_node n'' ∈ set (sourcenodes (ax#asx'))"
                by blast
              from ‹CFG_node n cd-ns→⇩d* CFG_node (sourcenode ax')›
                ‹CFG_node (sourcenode ax') ⟶⇘cd⇙ CFG_node n'›
              have "CFG_node n cd-ns@[CFG_node (sourcenode ax')]→⇩d* CFG_node n'"
                by(rule cdSp_Append_cdep)
              moreover
              from ‹∀n''∈set ns. parent_node n'' ∈ set (sourcenodes (ax#asx'))›
                ‹asx = asx'@ax'#asx''› ‹as = (ax#asx)@zs›
                ‹sourcenode ax' ∈ set(sourcenodes as)›
              have "∀n''∈set (ns@[CFG_node (sourcenode ax')]). 
                parent_node n'' ∈ set (sourcenodes as)"
                by(fastforce simp:sourcenodes_def)
              ultimately show ?thesis by fastforce
            next
              case False
              then obtain ai' where "valid_edge ai'" 
                and "sourcenode ai' = sourcenode ax'" 
                and "ai' ∈ get_return_edges a" by blast
              with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹targetnode a = n›
              have "CFG_node n ⟶⇘cd⇙ CFG_node (sourcenode ax')"
                by(fastforce intro!:SDG_proc_entry_exit_cdep[of _ _ _ _ _ _ ai'])
              with ‹valid_node n›
              have "CFG_node n cd-[]@[CFG_node n]→⇩d* CFG_node (sourcenode ax')"
                by(fastforce intro:cdSp_Append_cdep cdSp_Nil)
              with ‹CFG_node (sourcenode ax') ⟶⇘cd⇙ CFG_node n'›
              have "CFG_node n cd-[CFG_node n]@[CFG_node (sourcenode ax')]→⇩d* 
                CFG_node n'"
                by(fastforce intro:cdSp_Append_cdep)
              moreover
              from ‹sourcenode ax' ∈ set(sourcenodes as)› ‹n = sourcenode ax›
                ‹as = (ax#asx)@zs›
              have "∀n''∈set ([CFG_node n]@[CFG_node (sourcenode ax')]). 
                parent_node n'' ∈ set (sourcenodes as)"
                by(fastforce simp:sourcenodes_def)
              ultimately show ?thesis by fastforce
            qed
          qed
        qed
      qed
    qed
  next
    case False
    then obtain a' where "valid_edge a'" and "sourcenode a' = n'"
      and "a' ∈ get_return_edges a" by auto
    with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹targetnode a = n›
    have "CFG_node n ⟶⇘cd⇙ CFG_node n'" by(fastforce intro:SDG_proc_entry_exit_cdep)
    with ‹valid_edge a› ‹targetnode a = n›[THEN sym] 
    have "CFG_node n cd-[]@[CFG_node n]→⇩d* CFG_node n'"
      by(fastforce intro:cdep_SDG_path.intros)
    from ‹n -as→⇩ι* n'› ‹n ≠ n'› have "as ≠ []"
      by(fastforce elim:path.cases simp:intra_path_def)
    with ‹n -as→⇩ι* n'› have "hd (sourcenodes as) = n"
      by(fastforce intro:path_sourcenode simp:intra_path_def)
    with ‹as ≠ []› have "n ∈ set (sourcenodes as)" 
      by(fastforce intro:hd_in_set simp:sourcenodes_def)
    with ‹CFG_node n cd-[]@[CFG_node n]→⇩d* CFG_node n'›
    show ?thesis by auto
  qed
qed


subsection ‹Paths consisting of calls and control dependences›

inductive call_cdep_SDG_path ::
  "'node SDG_node ⇒ 'node SDG_node list ⇒ 'node SDG_node ⇒ bool"
("_ cc-_→⇩d* _" [51,0,0] 80)
where ccSp_Nil:
  "valid_SDG_node n ⟹ n cc-[]→⇩d* n"

  | ccSp_Append_cdep:
  "⟦n cc-ns→⇩d* n''; n'' ⟶⇘cd⇙ n'⟧ ⟹ n cc-ns@[n'']→⇩d* n'"

  | ccSp_Append_call:
  "⟦n cc-ns→⇩d* n''; n'' -p→⇘call⇙ n'⟧ ⟹ n cc-ns@[n'']→⇩d* n'"


lemma cc_SDG_path_Append:
  "⟦n'' cc-ns'→⇩d* n'; n cc-ns→⇩d* n''⟧ ⟹ n cc-ns@ns'→⇩d* n'"
by(induct rule:call_cdep_SDG_path.induct,
   auto intro:call_cdep_SDG_path.intros simp:append_assoc[THEN sym] 
                                        simp del:append_assoc)


lemma cdep_SDG_path_cc_SDG_path:
  "n cd-ns→⇩d* n' ⟹ n cc-ns→⇩d* n'"
by(induct rule:cdep_SDG_path.induct,auto intro:call_cdep_SDG_path.intros)


lemma Entry_cc_SDG_path_to_inner_node:
  assumes "valid_SDG_node n" and "parent_node n ≠ (_Exit_)"
  obtains ns where "CFG_node (_Entry_) cc-ns→⇩d* n"
proof(atomize_elim)
  obtain m where "m = parent_node n" by simp
  from ‹valid_SDG_node n› have "valid_node (parent_node n)" 
    by(rule valid_SDG_CFG_node)
  thus "∃ns. CFG_node (_Entry_) cc-ns→⇩d* n"
  proof(cases "parent_node n" rule:valid_node_cases)
    case Entry
    with ‹valid_SDG_node n› have "n = CFG_node (_Entry_)" 
      by(rule valid_SDG_node_parent_Entry)
    with ‹valid_SDG_node n› show ?thesis by(fastforce intro:ccSp_Nil)
  next
    case Exit
    with ‹parent_node n ≠ (_Exit_)› have False by simp
    thus ?thesis by simp
  next
    case inner
    with ‹m = parent_node n› obtain asx where "(_Entry_) -asx→⇩√* m"
      by(fastforce dest:Entry_path inner_is_valid)
    then obtain as where "(_Entry_) -as→⇩√* m"
      and "∀a' ∈ set as. intra_kind(kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)"
      by -(erule valid_Entry_path_ascending_path,fastforce)
    from ‹inner_node (parent_node n)› ‹m = parent_node n›
    have "inner_node m" by simp
    with ‹(_Entry_) -as→⇩√* m› ‹m = parent_node n› ‹valid_SDG_node n›
      ‹∀a' ∈ set as. intra_kind(kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)›
    show ?thesis
    proof(induct as arbitrary:m n rule:length_induct)
      fix as m n
      assume IH:"∀as'. length as' < length as ⟶
        (∀m'. (_Entry_) -as'→⇩√* m' ⟶
        (∀n'. m' = parent_node n' ⟶ valid_SDG_node n' ⟶
        (∀a' ∈ set as'. intra_kind(kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)) ⟶
        inner_node m' ⟶ (∃ns. CFG_node (_Entry_) cc-ns→⇩d* n')))"
        and "(_Entry_) -as→⇩√* m" 
        and "m = parent_node n" and "valid_SDG_node n" and "inner_node m"
        and "∀a' ∈ set as. intra_kind(kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)"
      show "∃ns. CFG_node (_Entry_) cc-ns→⇩d* n"
      proof(cases "∀a' ∈ set as. intra_kind(kind a')")
        case True
        with ‹(_Entry_) -as→⇩√* m› have "(_Entry_) -as→⇩ι* m"
          by(fastforce simp:intra_path_def vp_def)
        have "¬ method_exit m"
        proof
          assume "method_exit m"
          thus False
          proof(rule method_exit_cases)
            assume "m = (_Exit_)"
            with ‹inner_node m› show False by(simp add:inner_node_def)
          next
            fix a Q f p assume "m = sourcenode a" and "valid_edge a"
              and "kind a = Q↩⇘p⇙f"
            from ‹(_Entry_) -as→⇩ι* m› have "get_proc m = Main"
              by(fastforce dest:intra_path_get_procs simp:get_proc_Entry)
            from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f›
            have "get_proc (sourcenode a) = p" by(rule get_proc_return)
            with ‹get_proc m = Main› ‹m = sourcenode a› have "p = Main" by simp
            with ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› show False
              by(fastforce intro:Main_no_return_source)
          qed
        qed
        with ‹inner_node m› ‹(_Entry_) -as→⇩ι* m›
        obtain ns where "CFG_node (_Entry_) cd-ns→⇩d* CFG_node m"
          and "ns ≠ []" and "∀n'' ∈ set ns. parent_node n'' ∈ set(sourcenodes as)"
          by -(erule Entry_cdep_SDG_path)
        then obtain n' where "n' ⟶⇘cd⇙ CFG_node m"
          and "parent_node n' ∈ set(sourcenodes as)"
          by -(erule cdep_SDG_path.cases,auto)
        from ‹parent_node n' ∈ set(sourcenodes as)› obtain ms ms' 
          where "sourcenodes as = ms@(parent_node n')#ms'"
          by(fastforce dest:split_list simp:sourcenodes_def)
        then obtain as' a as'' where "ms = sourcenodes as'" 
          and "ms' = sourcenodes as''" and "as = as'@a#as''" 
          and "parent_node n' = sourcenode a"
          by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
        with ‹(_Entry_) -as→⇩ι* m› have "(_Entry_) -as'→⇩ι* parent_node n'"
          by(fastforce intro:path_split simp:intra_path_def)
        from ‹n' ⟶⇘cd⇙ CFG_node m› have "valid_SDG_node n'"
          by(rule SDG_edge_valid_SDG_node)
        hence n'_cases:
          "n' = CFG_node (parent_node n') ∨ CFG_node (parent_node n') ⟶⇘cd⇙ n'"
          by(rule valid_SDG_node_cases)
        show ?thesis
        proof(cases "as' = []")
          case True
          with ‹(_Entry_) -as'→⇩ι* parent_node n'› have "parent_node n' = (_Entry_)"
            by(fastforce simp:intra_path_def)
          from n'_cases have "∃ns. CFG_node (_Entry_) cd-ns→⇩d* CFG_node m"
          proof
            assume "n' = CFG_node (parent_node n')"
            with ‹n' ⟶⇘cd⇙ CFG_node m› ‹parent_node n' = (_Entry_)›
            have "CFG_node (_Entry_) cd-[]@[CFG_node (_Entry_)]→⇩d* CFG_node m"
              by -(rule cdSp_Append_cdep,rule cdSp_Nil,auto)
            thus ?thesis by fastforce
          next
            assume "CFG_node (parent_node n') ⟶⇘cd⇙ n'"
            with ‹parent_node n' = (_Entry_)›
            have "CFG_node (_Entry_) cd-[]@[CFG_node (_Entry_)]→⇩d* n'"
              by -(rule cdSp_Append_cdep,rule cdSp_Nil,auto)
            with ‹n' ⟶⇘cd⇙ CFG_node m›
            have "CFG_node (_Entry_) cd-[CFG_node (_Entry_)]@[n']→⇩d* CFG_node m"
              by(fastforce intro:cdSp_Append_cdep)
            thus ?thesis by fastforce
          qed
          then obtain ns where "CFG_node (_Entry_) cc-ns→⇩d* CFG_node m"
            by(fastforce intro:cdep_SDG_path_cc_SDG_path)
          show ?thesis
          proof(cases "n = CFG_node m")
            case True
            with ‹CFG_node (_Entry_) cc-ns→⇩d* CFG_node m› 
            show ?thesis by fastforce
          next
            case False
            with ‹inner_node m› ‹valid_SDG_node n› ‹m = parent_node n›
            have "CFG_node m ⟶⇘cd⇙ n"
              by(fastforce intro:SDG_parent_cdep_edge inner_is_valid)
            with ‹CFG_node (_Entry_) cc-ns→⇩d* CFG_node m›
            have "CFG_node (_Entry_) cc-ns@[CFG_node m]→⇩d* n"
              by(fastforce intro:ccSp_Append_cdep)
            thus ?thesis by fastforce
          qed
        next
          case False
          with ‹as = as'@a#as''› have "length as' < length as" by simp
          from ‹(_Entry_) -as'→⇩ι* parent_node n'› have "valid_node (parent_node n')"
            by(fastforce intro:path_valid_node simp:intra_path_def)
          hence "inner_node (parent_node n')"
          proof(cases "parent_node n'" rule:valid_node_cases)
            case Entry
            with ‹(_Entry_) -as'→⇩ι* (parent_node n')›
            have "(_Entry_) -as'→* (_Entry_)" by(fastforce simp:intra_path_def)
            with False have False by fastforce
            thus ?thesis by simp
          next
            case Exit
            with ‹n' ⟶⇘cd⇙ CFG_node m› have "n' = CFG_node (_Exit_)"
              by -(rule valid_SDG_node_parent_Exit,erule SDG_edge_valid_SDG_node,simp)
            with ‹n' ⟶⇘cd⇙ CFG_node m› Exit have False
              by simp(erule Exit_no_SDG_edge_source)
            thus ?thesis by simp
          next
            case inner
            thus ?thesis by simp
          qed
          from ‹valid_node (parent_node n')› 
          have "valid_SDG_node (CFG_node (parent_node n'))" by simp
          from ‹(_Entry_) -as'→⇩ι* (parent_node n')› 
          have "(_Entry_) -as'→⇩√* (parent_node n')"
            by(rule intra_path_vp)
          from ‹∀a' ∈ set as. intra_kind(kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)›
            ‹as = as'@a#as''›
          have "∀a' ∈ set as'. intra_kind(kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)"
            by auto
          with IH ‹length as' < length as› ‹(_Entry_) -as'→⇩√* (parent_node n')›
            ‹valid_SDG_node (CFG_node (parent_node n'))› ‹inner_node (parent_node n')›
          obtain ns where "CFG_node (_Entry_) cc-ns→⇩d* CFG_node (parent_node n')"
            apply(erule_tac x="as'" in allE) apply clarsimp
            apply(erule_tac x="(parent_node n')" in allE) apply clarsimp
            apply(erule_tac x="CFG_node (parent_node n')" in allE) by clarsimp
          from n'_cases have "∃ns. CFG_node (_Entry_) cc-ns→⇩d* n'"
          proof
            assume "n' = CFG_node (parent_node n')"
            with ‹CFG_node (_Entry_) cc-ns→⇩d* CFG_node (parent_node n')›
            show ?thesis by fastforce
          next
            assume "CFG_node (parent_node n') ⟶⇘cd⇙ n'"
            with ‹CFG_node (_Entry_) cc-ns→⇩d* CFG_node (parent_node n')›
            have "CFG_node (_Entry_) cc-ns@[CFG_node (parent_node n')]→⇩d* n'"
              by(fastforce intro:ccSp_Append_cdep)
            thus ?thesis by fastforce
          qed
          then obtain ns' where "CFG_node (_Entry_) cc-ns'→⇩d* n'" by blast
          with ‹n' ⟶⇘cd⇙ CFG_node m› 
          have "CFG_node (_Entry_) cc-ns'@[n']→⇩d* CFG_node m"
            by(fastforce intro:ccSp_Append_cdep)
          show ?thesis
          proof(cases "n = CFG_node m")
            case True
            with ‹CFG_node (_Entry_) cc-ns'@[n']→⇩d* CFG_node m›
            show ?thesis by fastforce
          next
            case False
            with ‹inner_node m› ‹valid_SDG_node n› ‹m = parent_node n›
            have "CFG_node m ⟶⇘cd⇙ n"
              by(fastforce intro:SDG_parent_cdep_edge inner_is_valid)
            with ‹CFG_node (_Entry_) cc-ns'@[n']→⇩d* CFG_node m›
            have "CFG_node (_Entry_) cc-(ns'@[n'])@[CFG_node m]→⇩d* n"
              by(fastforce intro:ccSp_Append_cdep)
            thus ?thesis by fastforce
          qed
        qed
      next
        case False
        hence "∃a' ∈ set as. ¬ intra_kind (kind a')" by fastforce
        then obtain a as' as'' where "as = as'@a#as''" and "¬ intra_kind (kind a)"
          and "∀a' ∈ set as''. intra_kind (kind a')"
          by(fastforce elim!:split_list_last_propE)
        from ‹∀a' ∈ set as. intra_kind(kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)›
          ‹as = as'@a#as''› ‹¬ intra_kind (kind a)›
        obtain Q r p fs where "kind a = Q:r↪⇘p⇙fs" 
          and "∀a' ∈ set as'. intra_kind(kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)"
          by auto
        from ‹as = as'@a#as''› have "length as' < length as" by fastforce
        from ‹(_Entry_) -as→⇩√* m› ‹as = as'@a#as''›
        have "(_Entry_) -as'→⇩√* sourcenode a" and "valid_edge a"
          and "targetnode a -as''→⇩√* m"
          by(auto intro:vp_split)
        hence "valid_SDG_node (CFG_node (sourcenode a))" by simp
        have "∃ns'. CFG_node (_Entry_) cc-ns'→⇩d* CFG_node m"
        proof(cases "targetnode a = m")
          case True
          with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs›
          have "CFG_node (sourcenode a) -p→⇘call⇙ CFG_node m"
            by(fastforce intro:SDG_call_edge)
          have "∃ns. CFG_node (_Entry_) cc-ns→⇩d* CFG_node (sourcenode a)"
          proof(cases "as' = []")
            case True
            with ‹(_Entry_) -as'→⇩√* sourcenode a› have "(_Entry_) = sourcenode a"
              by(fastforce simp:vp_def)
            with ‹CFG_node (sourcenode a) -p→⇘call⇙ CFG_node m›
            have "CFG_node (_Entry_) cc-[]→⇩d* CFG_node (sourcenode a)"
              by(fastforce intro:ccSp_Nil SDG_edge_valid_SDG_node)
            thus ?thesis by fastforce
          next
            case False
            from ‹valid_edge a› have "valid_node (sourcenode a)" by simp
            hence "inner_node (sourcenode a)"
            proof(cases "sourcenode a" rule:valid_node_cases)
              case Entry
              with ‹(_Entry_) -as'→⇩√* sourcenode a›
              have "(_Entry_) -as'→* (_Entry_)" by(fastforce simp:vp_def)
              with False have False by fastforce
              thus ?thesis by simp
            next
              case Exit
              with ‹valid_edge a› have False by -(erule Exit_source)
              thus ?thesis by simp
            next
              case inner
              thus ?thesis by simp
            qed
            with IH ‹length as' < length as› ‹(_Entry_) -as'→⇩√* sourcenode a›
              ‹valid_SDG_node (CFG_node (sourcenode a))› 
              ‹∀a' ∈ set as'. intra_kind(kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)›
            obtain ns where "CFG_node (_Entry_) cc-ns→⇩d* CFG_node (sourcenode a)"
              apply(erule_tac x="as'" in allE) apply clarsimp
              apply(erule_tac x="sourcenode a" in allE) apply clarsimp
              apply(erule_tac x="CFG_node (sourcenode a)" in allE) by clarsimp
            thus ?thesis by fastforce
          qed
          then obtain ns where "CFG_node (_Entry_) cc-ns→⇩d* CFG_node (sourcenode a)"
            by blast
          with ‹CFG_node (sourcenode a) -p→⇘call⇙ CFG_node m›
          show ?thesis by(fastforce intro:ccSp_Append_call)
        next
          case False
          from ‹targetnode a -as''→⇩√* m› ‹∀a' ∈ set as''. intra_kind (kind a')›
          have "targetnode a -as''→⇩ι* m" by(fastforce simp:vp_def intra_path_def)
          hence "get_proc (targetnode a) = get_proc m" by(rule intra_path_get_procs)
          from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc (targetnode a) = p"
            by(rule get_proc_call)
          from ‹inner_node m› ‹valid_edge a› ‹targetnode a -as''→⇩ι* m›
            ‹kind a = Q:r↪⇘p⇙fs› ‹targetnode a ≠ m›
          obtain ns where "CFG_node (targetnode a) cd-ns→⇩d* CFG_node m"
            and "ns ≠ []" 
            and "∀n'' ∈ set ns. parent_node n'' ∈ set(sourcenodes as'')"
            by(fastforce elim!:in_proc_cdep_SDG_path)
          then obtain n' where "n' ⟶⇘cd⇙ CFG_node m"
            and "parent_node n' ∈ set(sourcenodes as'')"
            by -(erule cdep_SDG_path.cases,auto)
          from ‹(parent_node n') ∈ set(sourcenodes as'')› obtain ms ms' 
            where "sourcenodes as'' = ms@(parent_node n')#ms'"
            by(fastforce dest:split_list simp:sourcenodes_def)
          then obtain xs a' ys where "ms = sourcenodes xs" 
            and "ms' = sourcenodes ys" and "as'' = xs@a'#ys"
            and "parent_node n' = sourcenode a'"
            by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
          from ‹(_Entry_) -as→⇩√* m› ‹as = as'@a#as''› ‹as'' = xs@a'#ys›
          have "(_Entry_) -(as'@a#xs)@a'#ys→⇩√* m" by simp
          hence "(_Entry_) -as'@a#xs→⇩√* sourcenode a'"
            and "valid_edge a'" by(auto intro:vp_split)
          from ‹as = as'@a#as''› ‹as'' = xs@a'#ys› 
          have "length (as'@a#xs) < length as" by simp
          from ‹valid_edge a'› have "valid_node (sourcenode a')" by simp
          hence "inner_node (sourcenode a')"
          proof(cases "sourcenode a'" rule:valid_node_cases)
            case Entry
            with ‹(_Entry_) -as'@a#xs→⇩√* sourcenode a'›
            have "(_Entry_) -as'@a#xs→* (_Entry_)" by(fastforce simp:vp_def)
            hence False by fastforce
            thus ?thesis by simp
          next
            case Exit
            with ‹valid_edge a'› have False by -(erule Exit_source)
            thus ?thesis by simp
          next
            case inner
            thus ?thesis by simp
          qed
          from ‹valid_edge a'› have "valid_SDG_node (CFG_node (sourcenode a'))"
            by simp
          from ‹∀a' ∈ set as. intra_kind(kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)›
            ‹as = as'@a#as''› ‹as'' = xs@a'#ys›
          have "∀a' ∈ set (as'@a#xs). 
            intra_kind(kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)"
            by auto
          with IH ‹length (as'@a#xs) < length as› 
            ‹(_Entry_) -as'@a#xs→⇩√* sourcenode a'›
            ‹valid_SDG_node (CFG_node (sourcenode a'))›
            ‹inner_node (sourcenode a')› ‹parent_node n' = sourcenode a'›
          obtain ns where "CFG_node (_Entry_) cc-ns→⇩d* CFG_node (parent_node n')"
            apply(erule_tac x="as'@a#xs" in allE) apply clarsimp
            apply(erule_tac x="sourcenode a'" in allE) apply clarsimp
            apply(erule_tac x="CFG_node (sourcenode a')" in allE) by clarsimp
          from ‹n' ⟶⇘cd⇙ CFG_node m› have "valid_SDG_node n'"
            by(rule SDG_edge_valid_SDG_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 ‹CFG_node (_Entry_) cc-ns→⇩d* CFG_node (parent_node n')›
              ‹n' ⟶⇘cd⇙ CFG_node m› show ?thesis
              by(fastforce intro:ccSp_Append_cdep)
          next
            assume "CFG_node (parent_node n') ⟶⇘cd⇙ n'"
            with ‹CFG_node (_Entry_) cc-ns→⇩d* CFG_node (parent_node n')›
            have "CFG_node (_Entry_) cc-ns@[CFG_node (parent_node n')]→⇩d* n'"
              by(fastforce intro:ccSp_Append_cdep)
            with ‹n' ⟶⇘cd⇙ CFG_node m› show ?thesis
              by(fastforce intro:ccSp_Append_cdep)
          qed
        qed
        then obtain ns where "CFG_node (_Entry_) cc-ns→⇩d* CFG_node m" by blast
        show ?thesis
        proof(cases "n = CFG_node m")
          case True
          with ‹CFG_node (_Entry_) cc-ns→⇩d* CFG_node m› show ?thesis by fastforce
        next
          case False
          with ‹inner_node m› ‹valid_SDG_node n› ‹m = parent_node n›
          have "CFG_node m ⟶⇘cd⇙ n"
            by(fastforce intro:SDG_parent_cdep_edge inner_is_valid)
          with ‹CFG_node (_Entry_) cc-ns→⇩d* CFG_node m› show ?thesis
            by(fastforce dest:ccSp_Append_cdep)
        qed
      qed
    qed
  qed
qed


subsection ‹Same level paths in the SDG›

inductive matched :: "'node SDG_node ⇒ 'node SDG_node list ⇒ 'node SDG_node ⇒ bool"
  where matched_Nil:
  "valid_SDG_node n ⟹ matched n [] n"
  | matched_Append_intra_SDG_path:
  "⟦matched n ns n''; n'' i-ns'→⇩d* n'⟧ ⟹ matched n (ns@ns') n'"
  | matched_bracket_call:
  "⟦matched n⇩0 ns n⇩1; 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); valid_edge a; a' ∈ get_return_edges 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⟧
  ⟹ matched n⇩0 (ns@n⇩1#ns'@[n⇩3]) n⇩4"
  | matched_bracket_param:
  "⟦matched n⇩0 ns n⇩1; n⇩1 -p:V→⇘in⇙ n⇩2; matched n⇩2 ns' n⇩3; 
    n⇩3 -p:V'→⇘out⇙ n⇩4; valid_edge a; a' ∈ get_return_edges 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⟧
  ⟹ matched n⇩0 (ns@n⇩1#ns'@[n⇩3]) n⇩4"




lemma matched_Append:
  "⟦matched n'' ns' n'; matched n ns n''⟧ ⟹ matched n (ns@ns') n'"
by(induct rule:matched.induct,
   auto intro:matched.intros simp:append_assoc[THEN sym] simp del:append_assoc)


lemma intra_SDG_path_matched:
  assumes "n i-ns→⇩d* n'" shows "matched n ns n'"
proof -
  from ‹n i-ns→⇩d* n'› have "valid_SDG_node n"
    by(rule intra_SDG_path_valid_SDG_node)
  hence "matched n [] n" by(rule matched_Nil)
  with ‹n i-ns→⇩d* n'› have "matched n ([]@ns) n'"
    by -(rule matched_Append_intra_SDG_path)
  thus ?thesis by simp
qed


lemma intra_proc_matched:
  assumes "valid_edge a" and "kind a = Q:r↪⇘p⇙fs" and "a' ∈ get_return_edges a"
  shows "matched (CFG_node (targetnode a)) [CFG_node (targetnode a)]
                 (CFG_node (sourcenode a'))"
proof -
  from assms have "CFG_node (targetnode a) ⟶⇘cd⇙ CFG_node (sourcenode a')" 
    by(fastforce intro:SDG_proc_entry_exit_cdep)
  with ‹valid_edge a› 
  have "CFG_node (targetnode a) i-[]@[CFG_node (targetnode a)]→⇩d* 
        CFG_node (sourcenode a')" 
    by(fastforce intro:intra_SDG_path.intros)
  with ‹valid_edge a› 
  have "matched (CFG_node (targetnode a)) ([]@[CFG_node (targetnode a)])
    (CFG_node (sourcenode a'))"
    by(fastforce intro:matched.intros)
  thus ?thesis by simp
qed


lemma matched_intra_CFG_path:
  assumes "matched n ns n'"
  obtains as where "parent_node n -as→⇩ι* parent_node n'"
proof(atomize_elim)
  from ‹matched n ns n'› show "∃as. parent_node n -as→⇩ι* parent_node n'"
  proof(induct rule:matched.induct)
    case matched_Nil thus ?case
      by(fastforce dest:empty_path valid_SDG_CFG_node simp:intra_path_def)
  next
    case (matched_Append_intra_SDG_path n ns n'' ns' n')
    from ‹∃as. parent_node n -as→⇩ι* parent_node n''› obtain as 
      where "parent_node n -as→⇩ι* parent_node n''" by blast
    from ‹n'' i-ns'→⇩d* n'› obtain as' where "parent_node n'' -as'→⇩ι* parent_node n'"
      by(fastforce elim:intra_SDG_path_intra_CFG_path)
    with ‹parent_node n -as→⇩ι* parent_node n''›
    have "parent_node n -as@as'→⇩ι* parent_node n'"
      by(rule intra_path_Append)
    thus ?case by fastforce
  next
    case (matched_bracket_call n⇩0 ns n⇩1 p n⇩2 ns' n⇩3 n⇩4 V a a')
    from ‹valid_edge a› ‹a' ∈ get_return_edges a› ‹sourcenode a = parent_node n⇩1›
      ‹targetnode a' = parent_node n⇩4›
    obtain a'' where "valid_edge a''" and "sourcenode a'' = parent_node n⇩1" 
      and "targetnode a'' = parent_node n⇩4" and "kind a'' = (λcf. False)⇩√"
      by(fastforce dest:call_return_node_edge)
    hence "parent_node n⇩1 -[a'']→* parent_node n⇩4" by(fastforce dest:path_edge)
    moreover
    from ‹kind a'' = (λcf. False)⇩√› have "∀a ∈ set [a'']. intra_kind(kind a)"
      by(fastforce simp:intra_kind_def)
    ultimately have "parent_node n⇩1 -[a'']→⇩ι* parent_node n⇩4"
      by(auto simp:intra_path_def)
    with ‹∃as. parent_node n⇩0 -as→⇩ι* parent_node n⇩1› show ?case
      by(fastforce intro:intra_path_Append)
  next
    case (matched_bracket_param n⇩0 ns n⇩1 p V n⇩2 ns' n⇩3 V' n⇩4 a a')
    from ‹valid_edge a› ‹a' ∈ get_return_edges a› ‹sourcenode a = parent_node n⇩1›
      ‹targetnode a' = parent_node n⇩4›
    obtain a'' where "valid_edge a''" and "sourcenode a'' = parent_node n⇩1" 
      and "targetnode a'' = parent_node n⇩4" and "kind a'' = (λcf. False)⇩√"
      by(fastforce dest:call_return_node_edge)
    hence "parent_node n⇩1 -[a'']→* parent_node n⇩4" by(fastforce dest:path_edge)
    moreover
    from ‹kind a'' = (λcf. False)⇩√› have "∀a ∈ set [a'']. intra_kind(kind a)"
      by(fastforce simp:intra_kind_def)
    ultimately have "parent_node n⇩1 -[a'']→⇩ι* parent_node n⇩4"
      by(auto simp:intra_path_def)
    with ‹∃as. parent_node n⇩0 -as→⇩ι* parent_node n⇩1› show ?case
      by(fastforce intro:intra_path_Append)
  qed
qed


lemma matched_same_level_CFG_path:
  assumes "matched n ns n'"
  obtains as where "parent_node n -as→⇘sl⇙* parent_node n'"
proof(atomize_elim)
  from ‹matched n ns n'›
  show "∃as. parent_node n -as→⇘sl⇙* parent_node n'"
  proof(induct rule:matched.induct)
    case matched_Nil thus ?case 
      by(fastforce dest:empty_path valid_SDG_CFG_node simp:slp_def same_level_path_def)
  next
    case (matched_Append_intra_SDG_path n ns n'' ns' n')
    from ‹∃as. parent_node n -as→⇘sl⇙* parent_node n''›
    obtain as where "parent_node n -as→⇘sl⇙* parent_node n''" by blast
    from ‹n'' i-ns'→⇩d* n'› obtain as' where "parent_node n'' -as'→⇩ι* parent_node n'"
      by(erule intra_SDG_path_intra_CFG_path)
    from ‹parent_node n'' -as'→⇩ι* parent_node n'›
    have "parent_node n'' -as'→⇘sl⇙* parent_node n'" by(rule intra_path_slp)
    with ‹parent_node n -as→⇘sl⇙* parent_node n''›
    have "parent_node n -as@as'→⇘sl⇙* parent_node n'"
      by(rule slp_Append)
    thus ?case by fastforce
  next
    case (matched_bracket_call n⇩0 ns n⇩1 p n⇩2 ns' n⇩3 n⇩4 V a a')
    from ‹valid_edge a› ‹a' ∈ get_return_edges a›
    obtain Q r p' fs where "kind a = Q:r↪⇘p'⇙fs" 
      by(fastforce dest!:only_call_get_return_edges)
    from ‹∃as. parent_node n⇩0 -as→⇘sl⇙* parent_node n⇩1›
    obtain as where "parent_node n⇩0 -as→⇘sl⇙* parent_node n⇩1" by blast
    from ‹∃as. parent_node n⇩2 -as→⇘sl⇙* parent_node n⇩3›
    obtain as' where "parent_node n⇩2 -as'→⇘sl⇙* parent_node n⇩3" by blast
    from ‹valid_edge a› ‹a' ∈ get_return_edges a› ‹kind a = Q:r↪⇘p'⇙fs›
    obtain Q' f' where "kind a' = Q'↩⇘p'⇙f'" by(fastforce dest!:call_return_edges)
    from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'" 
      by(rule get_return_edges_valid)
    from ‹parent_node n⇩2 -as'→⇘sl⇙* parent_node n⇩3› have "same_level_path as'"
      by(simp add:slp_def)
    hence "same_level_path_aux ([]@[a]) as'"
      by(fastforce intro:same_level_path_aux_callstack_Append simp:same_level_path_def)
    from ‹same_level_path as'› have "upd_cs ([]@[a]) as' = ([]@[a])"
      by(fastforce intro:same_level_path_upd_cs_callstack_Append 
                   simp:same_level_path_def)
    with ‹same_level_path_aux ([]@[a]) as'› ‹a' ∈ get_return_edges a›
      ‹kind a = Q:r↪⇘p'⇙fs› ‹kind a' = Q'↩⇘p'⇙f'›
    have "same_level_path (a#as'@[a'])"
      by(fastforce intro:same_level_path_aux_Append upd_cs_Append 
                   simp:same_level_path_def)
    from ‹valid_edge a'› ‹sourcenode a' = parent_node n⇩3›
      ‹targetnode a' = parent_node n⇩4›
    have "parent_node n⇩3 -[a']→* parent_node n⇩4" by(fastforce dest:path_edge)
    with ‹parent_node n⇩2 -as'→⇘sl⇙* parent_node n⇩3› 
    have "parent_node n⇩2 -as'@[a']→* parent_node n⇩4"
      by(fastforce intro:path_Append simp:slp_def)
    with ‹valid_edge a› ‹sourcenode a = parent_node n⇩1›
      ‹targetnode a = parent_node n⇩2›
    have "parent_node n⇩1 -a#as'@[a']→* parent_node n⇩4" by -(rule Cons_path)
    with ‹same_level_path (a#as'@[a'])›
    have "parent_node n⇩1 -a#as'@[a']→⇘sl⇙* parent_node n⇩4" by(simp add:slp_def)
    with ‹parent_node n⇩0 -as→⇘sl⇙* parent_node n⇩1›
    have "parent_node n⇩0 -as@a#as'@[a']→⇘sl⇙* parent_node n⇩4" by(rule slp_Append)
    with ‹sourcenode a = parent_node n⇩1› ‹sourcenode a' = parent_node n⇩3›
    show ?case by fastforce
  next
    case (matched_bracket_param n⇩0 ns n⇩1 p V n⇩2 ns' n⇩3 V' n⇩4 a a')
    from ‹valid_edge a› ‹a' ∈ get_return_edges a›
    obtain Q r p' fs where "kind a = Q:r↪⇘p'⇙fs" 
      by(fastforce dest!:only_call_get_return_edges)
    from ‹∃as. parent_node n⇩0 -as→⇘sl⇙* parent_node n⇩1›
    obtain as where "parent_node n⇩0 -as→⇘sl⇙* parent_node n⇩1" by blast
    from ‹∃as. parent_node n⇩2 -as→⇘sl⇙* parent_node n⇩3›
    obtain as' where "parent_node n⇩2 -as'→⇘sl⇙* parent_node n⇩3" by blast
    from ‹valid_edge a› ‹a' ∈ get_return_edges a› ‹kind a = Q:r↪⇘p'⇙fs›
    obtain Q' f' where "kind a' = Q'↩⇘p'⇙f'" by(fastforce dest!:call_return_edges)
    from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'" 
      by(rule get_return_edges_valid)
    from ‹parent_node n⇩2 -as'→⇘sl⇙* parent_node n⇩3› have "same_level_path as'"
      by(simp add:slp_def)
    hence "same_level_path_aux ([]@[a]) as'"
      by(fastforce intro:same_level_path_aux_callstack_Append simp:same_level_path_def)
    from ‹same_level_path as'› have "upd_cs ([]@[a]) as' = ([]@[a])"
      by(fastforce intro:same_level_path_upd_cs_callstack_Append 
                   simp:same_level_path_def)
    with ‹same_level_path_aux ([]@[a]) as'› ‹a' ∈ get_return_edges a›
      ‹kind a = Q:r↪⇘p'⇙fs› ‹kind a' = Q'↩⇘p'⇙f'›
    have "same_level_path (a#as'@[a'])"
      by(fastforce intro:same_level_path_aux_Append upd_cs_Append 
                   simp:same_level_path_def)
    from ‹valid_edge a'› ‹sourcenode a' = parent_node n⇩3›
      ‹targetnode a' = parent_node n⇩4›
    have "parent_node n⇩3 -[a']→* parent_node n⇩4" by(fastforce dest:path_edge)
    with ‹parent_node n⇩2 -as'→⇘sl⇙* parent_node n⇩3› 
    have "parent_node n⇩2 -as'@[a']→* parent_node n⇩4"
      by(fastforce intro:path_Append simp:slp_def)
    with ‹valid_edge a› ‹sourcenode a = parent_node n⇩1›
      ‹targetnode a = parent_node n⇩2›
    have "parent_node n⇩1 -a#as'@[a']→* parent_node n⇩4" by -(rule Cons_path)
    with ‹same_level_path (a#as'@[a'])›
    have "parent_node n⇩1 -a#as'@[a']→⇘sl⇙* parent_node n⇩4" by(simp add:slp_def)
    with ‹parent_node n⇩0 -as→⇘sl⇙* parent_node n⇩1›
    have "parent_node n⇩0 -as@a#as'@[a']→⇘sl⇙* parent_node n⇩4" by(rule slp_Append)
    with ‹sourcenode a = parent_node n⇩1› ‹sourcenode a' = parent_node n⇩3›
    show ?case by fastforce
  qed
qed


subsection ‹Realizable paths in the SDG›

inductive realizable :: 
  "'node SDG_node ⇒ 'node SDG_node list ⇒ 'node SDG_node ⇒ bool"
  where realizable_matched:"matched n ns n' ⟹ realizable n ns n'"
  | realizable_call:
  "⟦realizable n⇩0 ns n⇩1; n⇩1 -p→⇘call⇙ n⇩2 ∨ n⇩1 -p:V→⇘in⇙ n⇩2; matched n⇩2 ns' n⇩3⟧
  ⟹ realizable n⇩0 (ns@n⇩1#ns') n⇩3"


lemma realizable_Append_matched:
  "⟦realizable n ns n''; matched n'' ns' n'⟧ ⟹ realizable n (ns@ns') n'"
proof(induct rule:realizable.induct)
  case (realizable_matched n ns n'')
  from ‹matched n'' ns' n'› ‹matched n ns n''› have "matched n (ns@ns') n'"
    by(rule matched_Append)
  thus ?case by(rule realizable.realizable_matched)
next
  case (realizable_call n⇩0 ns n⇩1 p n⇩2 V ns'' n⇩3)
  from ‹matched n⇩3 ns' n'› ‹matched n⇩2 ns'' n⇩3› have "matched n⇩2 (ns''@ns') n'"
    by(rule matched_Append)
  with ‹realizable n⇩0 ns n⇩1› ‹n⇩1 -p→⇘call⇙ n⇩2 ∨ n⇩1 -p:V→⇘in⇙ n⇩2›
  have "realizable n⇩0 (ns@n⇩1#(ns''@ns')) n'"
    by(rule realizable.realizable_call)
  thus ?case by simp
qed


lemma realizable_valid_CFG_path:
  assumes "realizable n ns n'" 
  obtains as where "parent_node n -as→⇩√* parent_node n'"
proof(atomize_elim)
  from ‹realizable n ns n'› 
  show "∃as. parent_node n -as→⇩√* parent_node n'"
  proof(induct rule:realizable.induct)
    case (realizable_matched n ns n')
    from ‹matched n ns n'› obtain as where "parent_node n -as→⇘sl⇙* parent_node n'"
      by(erule matched_same_level_CFG_path)
    thus ?case by(fastforce intro:slp_vp)
  next
    case (realizable_call n⇩0 ns n⇩1 p n⇩2 V ns' n⇩3)
    from ‹∃as. parent_node n⇩0 -as→⇩√* parent_node n⇩1›
    obtain as where "parent_node n⇩0 -as→⇩√* parent_node n⇩1" by blast
    from ‹matched n⇩2 ns' n⇩3› obtain as' where "parent_node n⇩2 -as'→⇘sl⇙* parent_node n⇩3"
      by(erule matched_same_level_CFG_path)
    from ‹n⇩1 -p→⇘call⇙ n⇩2 ∨ n⇩1 -p:V→⇘in⇙ n⇩2›
    obtain a Q r fs where "valid_edge a"
      and "sourcenode a = parent_node n⇩1" and "targetnode a = parent_node n⇩2"
      and "kind a = Q:r↪⇘p⇙fs" by(fastforce elim:SDG_edge.cases)+
    hence "parent_node n⇩1 -[a]→* parent_node n⇩2"
      by(fastforce dest:path_edge)
    from ‹parent_node n⇩0 -as→⇩√* parent_node n⇩1› 
    have "parent_node n⇩0 -as→* parent_node n⇩1" and "valid_path as"
      by(simp_all add:vp_def)
    with ‹kind a = Q:r↪⇘p⇙fs› have "valid_path (as@[a])"
      by(fastforce elim:valid_path_aux_Append simp:valid_path_def)
    moreover
    from ‹parent_node n⇩0 -as→* parent_node n⇩1› ‹parent_node n⇩1 -[a]→* parent_node n⇩2›
    have "parent_node n⇩0 -as@[a]→* parent_node n⇩2" by(rule path_Append)
    ultimately have "parent_node n⇩0 -as@[a]→⇩√* parent_node n⇩2" by(simp add:vp_def)
    with ‹parent_node n⇩2 -as'→⇘sl⇙* parent_node n⇩3› 
    have "parent_node n⇩0 -(as@[a])@as'→⇩√* parent_node n⇩3" by -(rule vp_slp_Append)
    with ‹sourcenode a = parent_node n⇩1› show ?case by fastforce
  qed
qed


lemma cdep_SDG_path_realizable:
  "n cc-ns→⇩d* n' ⟹ realizable n ns n'"
proof(induct rule:call_cdep_SDG_path.induct)
  case (ccSp_Nil n)
  from ‹valid_SDG_node n› show ?case
    by(fastforce intro:realizable_matched matched_Nil)
next
  case (ccSp_Append_cdep n ns n'' n')
  from ‹n'' ⟶⇘cd⇙ n'› have "valid_SDG_node n''" by(rule SDG_edge_valid_SDG_node)
  hence "matched n'' [] n''" by(rule matched_Nil)
  from ‹n'' ⟶⇘cd⇙ n'› ‹valid_SDG_node n''›
  have "n'' i-[]@[n'']→⇩d* n'" 
    by(fastforce intro:iSp_Append_cdep iSp_Nil)
  with ‹matched n'' [] n''› have "matched n'' ([]@[n'']) n'"
    by(fastforce intro:matched_Append_intra_SDG_path)
  with ‹realizable n ns n''› show ?case
    by(fastforce intro:realizable_Append_matched)
next
  case (ccSp_Append_call n ns n'' p n')
  from ‹n'' -p→⇘call⇙ n'› have "valid_SDG_node n'" by(rule SDG_edge_valid_SDG_node)
  hence "matched n' [] n'" by(rule matched_Nil)
  with ‹realizable n ns n''› ‹n'' -p→⇘call⇙ n'›
  show ?case by(fastforce intro:realizable_call)
qed


subsection ‹SDG with summary edges›


inductive sum_cdep_edge :: "'node SDG_node ⇒ 'node SDG_node ⇒ bool" 
    ("_ s⟶⇘cd⇙ _" [51,0] 80)
  and sum_ddep_edge :: "'node SDG_node ⇒ 'var ⇒ 'node SDG_node ⇒ bool"
    ("_ s-_→⇩d⇩d _" [51,0,0] 80)
  and sum_call_edge :: "'node SDG_node ⇒ 'pname ⇒ 'node SDG_node ⇒ bool" 
    ("_ s-_→⇘call⇙ _" [51,0,0] 80)
  and sum_return_edge :: "'node SDG_node ⇒ 'pname ⇒ 'node SDG_node ⇒ bool" 
    ("_ s-_→⇘ret⇙ _" [51,0,0] 80)
  and sum_param_in_edge :: "'node SDG_node ⇒ 'pname ⇒ 'var ⇒ 'node SDG_node ⇒ bool"
    ("_ s-_:_→⇘in⇙ _" [51,0,0,0] 80)
  and sum_param_out_edge :: "'node SDG_node ⇒ 'pname ⇒ 'var ⇒ 'node SDG_node ⇒ bool"
    ("_ s-_:_→⇘out⇙ _" [51,0,0,0] 80)
  and sum_summary_edge :: "'node SDG_node ⇒ 'pname ⇒ 'node SDG_node ⇒ bool" 
    ("_ s-_→⇘sum⇙ _" [51,0] 80)
  and sum_SDG_edge :: "'node SDG_node ⇒ 'var option ⇒ 
                          ('pname × bool) option ⇒ bool ⇒ 'node SDG_node ⇒ bool"

where
    (* Syntax *)
  "n s⟶⇘cd⇙ n' == sum_SDG_edge n None None False n'"
  | "n s-V→⇩d⇩d n' == sum_SDG_edge n (Some V) None False n'"
  | "n s-p→⇘call⇙ n' == sum_SDG_edge n None (Some(p,True)) False n'"
  | "n s-p→⇘ret⇙ n' == sum_SDG_edge n None (Some(p,False)) False n'"
  | "n s-p:V→⇘in⇙ n' == sum_SDG_edge n (Some V) (Some(p,True)) False n'"
  | "n s-p:V→⇘out⇙ n' == sum_SDG_edge n (Some V) (Some(p,False)) False n'"
  | "n s-p→⇘sum⇙ n' == sum_SDG_edge n None (Some(p,True)) True n'"

    (* Rules *)
  | sum_SDG_cdep_edge:
    "⟦n = CFG_node m; n' = CFG_node m'; m controls m'⟧ ⟹ n s⟶⇘cd⇙ n'"
  | sum_SDG_proc_entry_exit_cdep:
    "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; n = CFG_node (targetnode a);
      a' ∈ get_return_edges a; n' = CFG_node (sourcenode a')⟧ ⟹ n s⟶⇘cd⇙ n'"
  | sum_SDG_parent_cdep_edge:
    "⟦valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n ≠ n'⟧ 
      ⟹ n s⟶⇘cd⇙ n'"
  | sum_SDG_ddep_edge:"n influences V in n' ⟹ n s-V→⇩d⇩d n'"
  | sum_SDG_call_edge:
    "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; n = CFG_node (sourcenode a); 
      n' = CFG_node (targetnode a)⟧ ⟹ n s-p→⇘call⇙ n'"
  | sum_SDG_return_edge:
    "⟦valid_edge a; kind a = Q↩⇘p⇙fs; n = CFG_node (sourcenode a); 
      n' = CFG_node (targetnode a)⟧ ⟹ n s-p→⇘ret⇙ n'"
  | sum_SDG_param_in_edge:
    "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; (p,ins,outs) ∈ set procs; V = ins!x;
      x < length ins; n = Actual_in (sourcenode a,x); n' = Formal_in (targetnode a,x)⟧
      ⟹ n s-p:V→⇘in⇙ n'"
  | sum_SDG_param_out_edge:
    "⟦valid_edge a; kind a = Q↩⇘p⇙f; (p,ins,outs) ∈ set procs; V = outs!x;
      x < length outs; n = Formal_out (sourcenode a,x); 
      n' = Actual_out (targetnode a,x)⟧
      ⟹ n s-p:V→⇘out⇙ n'"
  | sum_SDG_call_summary_edge:
    "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; a' ∈ get_return_edges a; 
      n = CFG_node (sourcenode a); n' = CFG_node (targetnode a')⟧
      ⟹ n s-p→⇘sum⇙ n'"
  | sum_SDG_param_summary_edge:
    "⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; a' ∈ get_return_edges a;
      matched (Formal_in (targetnode a,x)) ns (Formal_out (sourcenode a',x'));
      n = Actual_in (sourcenode a,x); n' = Actual_out (targetnode a',x');
      (p,ins,outs) ∈ set procs; x < length ins; x' < length outs⟧
      ⟹ n s-p→⇘sum⇙ n'"



lemma sum_edge_cases:
  "⟦n s-p→⇘sum⇙ n'; 
    ⋀a Q r fs a'. ⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; a' ∈ get_return_edges a;
                n = CFG_node (sourcenode a); n' = CFG_node (targetnode a')⟧ ⟹ P;
    ⋀a Q p r fs a' ns x x' ins outs.
      ⟦valid_edge a; kind a = Q:r↪⇘p⇙fs; a' ∈ get_return_edges a;
       matched (Formal_in (targetnode a,x)) ns (Formal_out (sourcenode a',x'));
       n = Actual_in (sourcenode a,x); n' = Actual_out (targetnode a',x');
       (p,ins,outs) ∈ set procs; x < length ins; x' < length outs⟧ ⟹ P⟧
  ⟹ P"
by -(erule sum_SDG_edge.cases,auto)



lemma SDG_edge_sum_SDG_edge:
  "SDG_edge n Vopt popt n' ⟹ sum_SDG_edge n Vopt popt False n'"
  by(induct rule:SDG_edge.induct,auto intro:sum_SDG_edge.intros)


lemma sum_SDG_edge_SDG_edge:
  "sum_SDG_edge n Vopt popt False n' ⟹ SDG_edge n Vopt popt n'"
by(induct n Vopt popt x≡"False" n' rule:sum_SDG_edge.induct,
   auto intro:SDG_edge.intros)


lemma sum_SDG_edge_valid_SDG_node:
  assumes "sum_SDG_edge n Vopt popt b n'" 
  shows "valid_SDG_node n" and "valid_SDG_node n'"
proof -
  have "valid_SDG_node n ∧ valid_SDG_node n'"
  proof(cases b)
    case True
    with ‹sum_SDG_edge n Vopt popt b n'› show ?thesis
    proof(induct rule:sum_SDG_edge.induct)
      case (sum_SDG_call_summary_edge a Q r p f a' n n')
      from ‹valid_edge a› ‹n = CFG_node (sourcenode a)›
      have "valid_SDG_node n" by fastforce
      from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'"
        by(rule get_return_edges_valid)
      with ‹n' = CFG_node (targetnode a')› have "valid_SDG_node n'" by fastforce
      with ‹valid_SDG_node n› show ?case by simp
    next
      case (sum_SDG_param_summary_edge a Q r p fs a' x ns x' n n' ins outs)
      from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹n = Actual_in (sourcenode a,x)›
        ‹(p,ins,outs) ∈ set procs› ‹x < length ins›
      have "valid_SDG_node n" by fastforce
      from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'"
        by(rule get_return_edges_valid)
      from ‹valid_edge a› ‹a' ∈ get_return_edges a› ‹kind a = Q:r↪⇘p⇙fs›
      obtain Q' f' where "kind a' = Q'↩⇘p⇙f'" by(fastforce dest!:call_return_edges)
      with ‹valid_edge a'› ‹n' = Actual_out (targetnode a',x')›
        ‹(p,ins,outs) ∈ set procs› ‹x' < length outs›
      have "valid_SDG_node n'" by fastforce
      with ‹valid_SDG_node n› show ?case by simp
    qed simp_all
  next
    case False
    with ‹sum_SDG_edge n Vopt popt b n'› have "SDG_edge n Vopt popt n'"
      by(fastforce intro:sum_SDG_edge_SDG_edge)
    thus ?thesis by(fastforce intro:SDG_edge_valid_SDG_node)
  qed
  thus "valid_SDG_node n" and "valid_SDG_node n'" by simp_all
qed


lemma Exit_no_sum_SDG_edge_source:
  assumes "sum_SDG_edge (CFG_node (_Exit_)) Vopt popt b n'" shows "False"
proof(cases b)
  case True
  with ‹sum_SDG_edge (CFG_node (_Exit_)) Vopt popt b n'› show ?thesis
  proof(induct "CFG_node (_Exit_)" Vopt popt b n' rule:sum_SDG_edge.induct)
    case (sum_SDG_call_summary_edge a Q r p f a' n')
    from ‹CFG_node (_Exit_) = CFG_node (sourcenode a)›
    have "sourcenode a = (_Exit_)" by simp
    with ‹valid_edge a› show ?case by(rule Exit_source)
  next
    case (sum_SDG_param_summary_edge a Q r p f a' x ns x' n' ins outs)
    thus ?case by simp
  qed simp_all
next
  case False
  with ‹sum_SDG_edge (CFG_node (_Exit_)) Vopt popt b n'› 
  have "SDG_edge (CFG_node (_Exit_)) Vopt popt n'"
    by(fastforce intro:sum_SDG_edge_SDG_edge)
  thus ?thesis by(fastforce intro:Exit_no_SDG_edge_source)
qed


lemma Exit_no_sum_SDG_edge_target:
  "sum_SDG_edge n Vopt popt b (CFG_node (_Exit_)) ⟹ False"
proof(induct "CFG_node (_Exit_)" rule:sum_SDG_edge.induct)
  case (sum_SDG_cdep_edge n m m')
  from ‹m controls m'› ‹CFG_node (_Exit_) = CFG_node m'›
  have "m controls (_Exit_)" by simp
  hence False by(fastforce dest:Exit_not_control_dependent)
  thus ?case by simp
next
  case (sum_SDG_proc_entry_exit_cdep a Q r p f n a')
  from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'"
    by(rule get_return_edges_valid)
  moreover
  from ‹CFG_node (_Exit_) = CFG_node (sourcenode a')›
  have "sourcenode a' = (_Exit_)" by simp
  ultimately have False by(rule Exit_source)
  thus ?case by simp
next
  case (sum_SDG_ddep_edge n V) thus ?case
    by(fastforce elim:SDG_Use.cases simp:data_dependence_def)
next
  case (sum_SDG_call_edge a Q r p fs n)
  from ‹CFG_node (_Exit_) = CFG_node (targetnode a)›
  have "targetnode a = (_Exit_)" by simp
  with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have "get_proc (_Exit_) = p"
    by(fastforce intro:get_proc_call)
  hence "p = Main" by(simp add:get_proc_Exit)
  with ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› have False 
    by(fastforce intro:Main_no_call_target)
  thus ?case by simp
next
  case (sum_SDG_return_edge a Q p f n)
  from ‹CFG_node (_Exit_) = CFG_node (targetnode a)›
  have "targetnode a = (_Exit_)" by simp
  with ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› have False by(rule Exit_no_return_target)
  thus ?case by simp
next
  case (sum_SDG_call_summary_edge a Q r p fs a' n)
  from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'"
    by(rule get_return_edges_valid)
  from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹a' ∈ get_return_edges a›
  obtain Q' f' where "kind a' = Q'↩⇘p⇙f'" by(fastforce dest!:call_return_edges)
  from ‹CFG_node (_Exit_) = CFG_node (targetnode a')›
  have "targetnode a' = (_Exit_)" by simp
  with ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'› have False by(rule Exit_no_return_target)
  thus ?case by simp
qed simp+



lemma sum_SDG_summary_edge_matched:
  assumes "n s-p→⇘sum⇙ n'" 
  obtains ns where "matched n ns n'" and "n ∈ set ns"
  and "get_proc (parent_node(last ns)) = p"
proof(atomize_elim)
  from ‹n s-p→⇘sum⇙ n'› 
  show "∃ns. matched n ns n' ∧ n ∈ set ns ∧ get_proc (parent_node(last ns)) = p"
  proof(induct n "None::'var option" "Some(p,True)" "True" n'
               rule:sum_SDG_edge.induct)
    case (sum_SDG_call_summary_edge a Q r fs a' n n')
    from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹n = CFG_node (sourcenode a)›
    have "n -p→⇘call⇙ CFG_node (targetnode a)" by(fastforce intro:SDG_call_edge)
    hence "valid_SDG_node n" by(rule SDG_edge_valid_SDG_node)
    hence "matched n [] n" by(rule matched_Nil)
    from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'"
      by(rule get_return_edges_valid)
    from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹a' ∈ get_return_edges a› 
    have matched:"matched (CFG_node (targetnode a)) [CFG_node (targetnode a)]
      (CFG_node (sourcenode a'))" by(rule intra_proc_matched)
    from ‹valid_edge a› ‹a' ∈ get_return_edges a› ‹kind a = Q:r↪⇘p⇙fs›
    obtain Q' f' where "kind a' = Q'↩⇘p⇙f'" by(fastforce dest!:call_return_edges)
    with ‹valid_edge a'› have "get_proc (sourcenode a') = p" by(rule get_proc_return)
    from ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'› ‹n' = CFG_node (targetnode a')›
    have "CFG_node (sourcenode a') -p→⇘ret⇙ n'" by(fastforce intro:SDG_return_edge)
    from ‹matched n [] n› ‹n -p→⇘call⇙ CFG_node (targetnode a)› matched
      ‹CFG_node (sourcenode a') -p→⇘ret⇙ n'› ‹a' ∈ get_return_edges a›
      ‹n = CFG_node (sourcenode a)› ‹n' = CFG_node (targetnode a')› ‹valid_edge a›
    have "matched n ([]@n#[CFG_node (targetnode a)]@[CFG_node (sourcenode a')]) n'"
      by(fastforce intro:matched_bracket_call)
    with ‹get_proc (sourcenode a') = p› show ?case by auto
  next
    case (sum_SDG_param_summary_edge a Q r fs a' x ns x' n n' ins outs)
    from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹(p,ins,outs) ∈ set procs›
      ‹x < length ins› ‹n = Actual_in (sourcenode a,x)›
    have "n -p:ins!x→⇘in⇙ Formal_in (targetnode a,x)" 
      by(fastforce intro:SDG_param_in_edge)
    hence "valid_SDG_node n" by(rule SDG_edge_valid_SDG_node)
    hence "matched n [] n" by(rule matched_Nil)
    from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'"
      by(rule get_return_edges_valid)
    from ‹valid_edge a› ‹a' ∈ get_return_edges a› ‹kind a = Q:r↪⇘p⇙fs›
    obtain Q' f' where "kind a' = Q'↩⇘p⇙f'" by(fastforce dest!:call_return_edges)
    with ‹valid_edge a'› have "get_proc (sourcenode a') = p" by(rule get_proc_return)
    from ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'› ‹(p,ins,outs) ∈ set procs›
      ‹x' < length outs› ‹n' = Actual_out (targetnode a',x')›
    have "Formal_out (sourcenode a',x') -p:outs!x'→⇘out⇙ n'"
      by(fastforce intro:SDG_param_out_edge)
    from ‹matched n [] n› ‹n -p:ins!x→⇘in⇙ Formal_in (targetnode a,x)›
      ‹matched (Formal_in (targetnode a,x)) ns (Formal_out (sourcenode a',x'))›
      ‹Formal_out (sourcenode a',x') -p:outs!x'→⇘out⇙ n'› 
      ‹a' ∈ get_return_edges a› ‹n = Actual_in (sourcenode a,x)›
      ‹n' = Actual_out (targetnode a',x')› ‹valid_edge a›
    have "matched n ([]@n#ns@[Formal_out (sourcenode a',x')]) n'"
      by(fastforce intro:matched_bracket_param)
    with ‹get_proc (sourcenode a') = p› show ?case by auto
  qed simp_all
qed


lemma return_edge_determines_call_and_sum_edge:
  assumes "valid_edge a" and "kind a = Q↩⇘p⇙f"
  obtains a' Q' r' fs' where "a ∈ get_return_edges a'" and "valid_edge a'"
  and "kind a' = Q':r'↪⇘p⇙fs'" 
  and "CFG_node (sourcenode a') s-p→⇘sum⇙ CFG_node (targetnode a)"
proof(atomize_elim)
  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)
  from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f›
  obtain a' Q' r' fs' where "valid_edge a'" and "kind a' = Q':r'↪⇘p⇙fs'"
    and "a ∈ get_return_edges a'" by(blast dest:return_needs_call)
  hence "CFG_node (sourcenode a') s-p→⇘call⇙ CFG_node (targetnode a')"
    by(fastforce intro:sum_SDG_call_edge)
  from ‹valid_edge a'› ‹kind a' = Q':r'↪⇘p⇙fs'› ‹valid_edge a› ‹a ∈ get_return_edges a'›
  have "CFG_node (targetnode a') ⟶⇘cd⇙ CFG_node (sourcenode a)"
    by(fastforce intro!:SDG_proc_entry_exit_cdep)
  hence "valid_SDG_node (CFG_node (targetnode a'))"
    by(rule SDG_edge_valid_SDG_node)
  with ‹CFG_node (targetnode a') ⟶⇘cd⇙ CFG_node (sourcenode a)› 
  have "CFG_node (targetnode a') i-[]@[CFG_node (targetnode a')]→⇩d* 
        CFG_node (sourcenode a)"
    by(fastforce intro:iSp_Append_cdep iSp_Nil)
  from ‹valid_SDG_node (CFG_node (targetnode a'))› 
  have "matched (CFG_node (targetnode a')) [] (CFG_node (targetnode a'))"
    by(rule matched_Nil)
  with ‹CFG_node (targetnode a') i-[]@[CFG_node (targetnode a')]→⇩d* 
        CFG_node (sourcenode a)›
  have "matched (CFG_node (targetnode a')) ([]@[CFG_node (targetnode a')])
                (CFG_node (sourcenode a))"
    by(fastforce intro:matched_Append_intra_SDG_path)
  with ‹valid_edge a'› ‹kind a' = Q':r'↪⇘p⇙fs'› ‹valid_edge a› ‹kind a = Q↩⇘p⇙f›
    ‹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 ‹a ∈ get_return_edges a'› ‹valid_edge a'› ‹kind a' = Q':r'↪⇘p⇙fs'›
  show "∃a' Q' r' fs'. a ∈ get_return_edges a' ∧ valid_edge a' ∧ 
    kind a' = Q':r'↪⇘p⇙fs' ∧ CFG_node (sourcenode a') s-p→⇘sum⇙ CFG_node (targetnode a)"
    by fastforce
qed
  

subsection ‹Paths consisting of intraprocedural and summary edges in the SDG›

inductive intra_sum_SDG_path ::
  "'node SDG_node ⇒ 'node SDG_node list ⇒ 'node SDG_node ⇒ bool"
("_ is-_→⇩d* _" [51,0,0] 80)
where isSp_Nil:
  "valid_SDG_node n ⟹ n is-[]→⇩d* n"

  | isSp_Append_cdep:
  "⟦n is-ns→⇩d* n''; n'' s⟶⇘cd⇙ n'⟧ ⟹ n is-ns@[n'']→⇩d* n'"

  | isSp_Append_ddep:
  "⟦n is-ns→⇩d* n''; n'' s-V→⇩d⇩d n'; n'' ≠ n'⟧ ⟹ n is-ns@[n'']→⇩d* n'"

  | isSp_Append_sum:
  "⟦n is-ns→⇩d* n''; n'' s-p→⇘sum⇙ n'⟧ ⟹ n is-ns@[n'']→⇩d* n'"


lemma is_SDG_path_Append:
  "⟦n'' is-ns'→⇩d* n'; n is-ns→⇩d* n''⟧ ⟹ n is-ns@ns'→⇩d* n'"
by(induct rule:intra_sum_SDG_path.induct,
   auto intro:intra_sum_SDG_path.intros simp:append_assoc[THEN sym] 
                                        simp del:append_assoc)


lemma is_SDG_path_valid_SDG_node:
  assumes "n is-ns→⇩d* n'" shows "valid_SDG_node n" and "valid_SDG_node n'"
using ‹n is-ns→⇩d* n'›
by(induct rule:intra_sum_SDG_path.induct,
   auto intro:sum_SDG_edge_valid_SDG_node valid_SDG_CFG_node)


lemma intra_SDG_path_is_SDG_path:
  "n i-ns→⇩d* n' ⟹ n is-ns→⇩d* n'"
by(induct rule:intra_SDG_path.induct,
   auto intro:intra_sum_SDG_path.intros SDG_edge_sum_SDG_edge)


lemma is_SDG_path_hd:"⟦n is-ns→⇩d* n'; ns ≠ []⟧ ⟹ hd ns = n"
apply(induct rule:intra_sum_SDG_path.induct) apply clarsimp
by(case_tac ns,auto elim:intra_sum_SDG_path.cases)+


lemma intra_sum_SDG_path_rev_induct [consumes 1, case_names "isSp_Nil" 
  "isSp_Cons_cdep"  "isSp_Cons_ddep"  "isSp_Cons_sum"]: 
  assumes "n is-ns→⇩d* n'"
  and refl:"⋀n. valid_SDG_node n ⟹ P n [] n"
  and step_cdep:"⋀n ns n' n''. ⟦n s⟶⇘cd⇙ n''; n'' is-ns→⇩d* n'; P n'' ns n'⟧ 
                 ⟹ P n (n#ns) n'"
  and step_ddep:"⋀n ns n' V n''. ⟦n s-V→⇩d⇩d n''; n ≠ n''; n'' is-ns→⇩d* n'; 
                                  P n'' ns n'⟧ ⟹ P n (n#ns) n'"
  and step_sum:"⋀n ns n' p n''. ⟦n s-p→⇘sum⇙ n''; n'' is-ns→⇩d* n'; P n'' ns n'⟧ 
                 ⟹ P n (n#ns) n'"
  shows "P n ns n'"
using ‹n is-ns→⇩d* n'›
proof(induct ns arbitrary:n)
  case Nil thus ?case by(fastforce elim:intra_sum_SDG_path.cases intro:refl)
next
  case (Cons nx nsx)
  note IH = ‹⋀n. n is-nsx→⇩d* n' ⟹ P n nsx n'›
  from ‹n is-nx#nsx→⇩d* n'› have [simp]:"n = nx" 
    by(fastforce dest:is_SDG_path_hd)
  from ‹n is-nx#nsx→⇩d* n'›  have "((∃n''. n s⟶⇘cd⇙ n'' ∧ n'' is-nsx→⇩d* n') ∨
    (∃n'' V. n s-V→⇩d⇩d n'' ∧ n ≠ n'' ∧ n'' is-nsx→⇩d* n')) ∨
    (∃n'' p. n s-p→⇘sum⇙ n'' ∧ n'' is-nsx→⇩d* n')"
  proof(induct nsx arbitrary:n' rule:rev_induct)
    case Nil
    from ‹n is-[nx]→⇩d* n'› have "n is-[]→⇩d* nx" 
      and disj:"nx s⟶⇘cd⇙ n' ∨ (∃V. nx s-V→⇩d⇩d n' ∧ nx ≠ n') ∨ (∃p. nx s-p→⇘sum⇙ n')"
      by(induct n ns≡"[nx]" n' rule:intra_sum_SDG_path.induct,auto)
    from ‹n is-[]→⇩d* nx› have [simp]:"n = nx"
      by(fastforce elim:intra_sum_SDG_path.cases)
    from disj have "valid_SDG_node n'" by(fastforce intro:sum_SDG_edge_valid_SDG_node)
    hence "n' is-[]→⇩d* n'" by(rule isSp_Nil)
    with disj show ?case by fastforce
  next
    case (snoc x xs)
    note ‹⋀n'. n is-nx # xs→⇩d* n' ⟹
      ((∃n''. n s⟶⇘cd⇙ n'' ∧ n'' is-xs→⇩d* n') ∨
      (∃n'' V. n s-V→⇩d⇩d n'' ∧ n ≠ n'' ∧ n'' is-xs→⇩d* n')) ∨
      (∃n'' p. n s-p→⇘sum⇙ n'' ∧ n'' is-xs→⇩d* n')›
    with ‹n is-nx#xs@[x]→⇩d* n'› show ?case
    proof(induct n "nx#xs@[x]" n' rule:intra_sum_SDG_path.induct)
      case (isSp_Append_cdep m ms m'' n')
      note IH = ‹⋀n'. m is-nx # xs→⇩d* n' ⟹
        ((∃n''. m s⟶⇘cd⇙ n'' ∧ n'' is-xs→⇩d* n') ∨
        (∃n'' V. m s-V→⇩d⇩d n'' ∧ m ≠ n'' ∧ n'' is-xs→⇩d* n')) ∨
        (∃n'' p. m s-p→⇘sum⇙ n'' ∧ n'' is-xs→⇩d* n')›
      from ‹ms @ [m''] = nx#xs@[x]› have [simp]:"ms = nx#xs"
        and [simp]:"m'' = x" by simp_all
      from ‹m is-ms→⇩d* m''› have "m is-nx#xs→⇩d* m''" by simp
      from IH[OF this] obtain n'' where "n'' is-xs→⇩d* m''"
        and "(m s⟶⇘cd⇙ n'' ∨ (∃V. m s-V→⇩d⇩d n'' ∧ m ≠ n'')) ∨ (∃p. m s-p→⇘sum⇙ n'')"
        by fastforce
      from ‹n'' is-xs→⇩d* m''› ‹m'' s⟶⇘cd⇙ n'›
      have "n'' is-xs@[m'']→⇩d* n'" by(rule intra_sum_SDG_path.intros)
      with ‹(m s⟶⇘cd⇙ n'' ∨ (∃V. m s-V→⇩d⇩d n'' ∧ m ≠ n'')) ∨ (∃p. m s-p→⇘sum⇙ n'')›
      show ?case by fastforce
    next
      case (isSp_Append_ddep m ms m'' V n')
      note IH = ‹⋀n'. m is-nx # xs→⇩d* n' ⟹
        ((∃n''. m s⟶⇘cd⇙ n'' ∧ n'' is-xs→⇩d* n') ∨
        (∃n'' V. m s-V→⇩d⇩d n'' ∧ m ≠ n'' ∧ n'' is-xs→⇩d* n')) ∨
        (∃n'' p. m s-p→⇘sum⇙ n'' ∧ n'' is-xs→⇩d* n')›
      from ‹ms @ [m''] = nx#xs@[x]› have [simp]:"ms = nx#xs"
        and [simp]:"m'' = x" by simp_all
      from ‹m is-ms→⇩d* m''› have "m is-nx#xs→⇩d* m''" by simp
      from IH[OF this] obtain n'' where "n'' is-xs→⇩d* m''"
        and "(m s⟶⇘cd⇙ n'' ∨ (∃V. m s-V→⇩d⇩d n'' ∧ m ≠ n'')) ∨ (∃p. m s-p→⇘sum⇙ n'')"
        by fastforce
      from ‹n'' is-xs→⇩d* m''› ‹m'' s-V→⇩d⇩d n'› ‹m'' ≠ n'›
      have "n'' is-xs@[m'']→⇩d* n'" by(rule intra_sum_SDG_path.intros)
      with ‹(m s⟶⇘cd⇙ n'' ∨ (∃V. m s-V→⇩d⇩d n'' ∧ m ≠ n'')) ∨ (∃p. m s-p→⇘sum⇙ n'')›
      show ?case by fastforce
    next
      case (isSp_Append_sum m ms m'' p n')
      note IH = ‹⋀n'. m is-nx # xs→⇩d* n' ⟹
        ((∃n''. m s⟶⇘cd⇙ n'' ∧ n'' is-xs→⇩d* n') ∨
        (∃n'' V. m s-V→⇩d⇩d n'' ∧ m ≠ n'' ∧ n'' is-xs→⇩d* n')) ∨
        (∃n'' p. m s-p→⇘sum⇙ n'' ∧ n'' is-xs→⇩d* n')›
      from ‹ms @ [m''] = nx#xs@[x]› have [simp]:"ms = nx#xs"
        and [simp]:"m'' = x" by simp_all
      from ‹m is-ms→⇩d* m''› have "m is-nx#xs→⇩d* m''" by simp
      from IH[OF this] obtain n'' where "n'' is-xs→⇩d* m''"
        and "(m s⟶⇘cd⇙ n'' ∨ (∃V. m s-V→⇩d⇩d n'' ∧ m ≠ n'')) ∨ (∃p. m s-p→⇘sum⇙ n'')"
        by fastforce
      from ‹n'' is-xs→⇩d* m''› ‹m'' s-p→⇘sum⇙ n'›
      have "n'' is-xs@[m'']→⇩d* n'" by(rule intra_sum_SDG_path.intros)
      with ‹(m s⟶⇘cd⇙ n'' ∨ (∃V. m s-V→⇩d⇩d n'' ∧ m ≠ n'')) ∨ (∃p. m s-p→⇘sum⇙ n'')›
      show ?case by fastforce
    qed
  qed
  thus ?case apply -
  proof(erule disjE)+
    assume "∃n''. n s⟶⇘cd⇙ n'' ∧ n'' is-nsx→⇩d* n'"
    then obtain n'' where "n s⟶⇘cd⇙ n''" and "n'' is-nsx→⇩d* n'" by blast
    from IH[OF ‹n'' is-nsx→⇩d* n'›] have "P n'' nsx n'" .
    from step_cdep[OF ‹n s⟶⇘cd⇙ n''› ‹n'' is-nsx→⇩d* n'› this] show ?thesis by simp
  next
    assume "∃n'' V. n s-V→⇩d⇩d n'' ∧ n ≠ n'' ∧ n'' is-nsx→⇩d* n'"
    then obtain n'' V where "n s-V→⇩d⇩d n''" and "n ≠ n''" and "n'' is-nsx→⇩d* n'" 
      by blast
    from IH[OF ‹n'' is-nsx→⇩d* n'›] have "P n'' nsx n'" .
    from step_ddep[OF ‹n s-V→⇩d⇩d n''› ‹n ≠ n''› ‹n'' is-nsx→⇩d* n'› this] 
    show ?thesis by simp
  next
    assume "∃n'' p. n s-p→⇘sum⇙ n'' ∧ n'' is-nsx→⇩d* n'"
    then obtain n'' p where "n s-p→⇘sum⇙ n''" and "n'' is-nsx→⇩d* n'" by blast
    from IH[OF ‹n'' is-nsx→⇩d* n'›] have "P n'' nsx n'" .
    from step_sum[OF ‹n s-p→⇘sum⇙ n''› ‹n'' is-nsx→⇩d* n'› this] show ?thesis by simp
  qed
qed


lemma is_SDG_path_CFG_path:
  assumes "n is-ns→⇩d* n'"
  obtains as where "parent_node n -as→⇩ι* parent_node n'" 
proof(atomize_elim)
  from ‹n is-ns→⇩d* n'›
  show "∃as. parent_node n -as→⇩ι* parent_node n'"
  proof(induct rule:intra_sum_SDG_path.induct)
    case (isSp_Nil n)
    from ‹valid_SDG_node n› have "valid_node (parent_node n)"
      by(rule valid_SDG_CFG_node)
    hence "parent_node n -[]→* parent_node n" by(rule empty_path)
    thus ?case by(auto simp:intra_path_def)
  next
    case (isSp_Append_cdep n ns n'' n')
    from ‹∃as. parent_node n -as→⇩ι* parent_node n''›
    obtain as where "parent_node n -as→⇩ι* parent_node n''" by blast
    from ‹n'' s⟶⇘cd⇙ n'›  have "n'' ⟶⇘cd⇙ n'" by(rule sum_SDG_edge_SDG_edge)
    thus ?case
    proof(rule cdep_edge_cases)
      assume "parent_node n'' controls parent_node n'"
      then obtain as' where "parent_node n'' -as'→⇩ι* parent_node n'" and "as' ≠ []"
        by(erule control_dependence_path)
      with ‹parent_node n -as→⇩ι* parent_node n''› 
      have "parent_node n -as@as'→⇩ι* parent_node n'" by -(rule intra_path_Append)
      thus ?thesis by blast
    next
      fix a Q r p fs a'
      assume "valid_edge a" and "kind a = Q:r↪⇘p⇙fs" and "a' ∈ get_return_edges a"
        and "parent_node n'' = targetnode a" and "parent_node n' = sourcenode a'"
      then obtain a'' where "valid_edge a''" and "sourcenode a'' = targetnode a"
        and "targetnode a'' = sourcenode a'" and "kind a'' = (λcf. False)⇩√"
        by(auto dest:intra_proc_additional_edge)
      hence "targetnode a -[a'']→⇩ι* sourcenode a'"
        by(fastforce dest:path_edge simp:intra_path_def intra_kind_def)
      with ‹parent_node n'' = targetnode a› ‹parent_node n' = sourcenode a'› 
      have "∃as'. parent_node n'' -as'→⇩ι* parent_node n' ∧ as' ≠ []" by fastforce
      then obtain as' where "parent_node n'' -as'→⇩ι* parent_node n'" and "as' ≠ []"
        by blast
      with ‹parent_node n -as→⇩ι* parent_node n''›
      have "parent_node n -as@as'→⇩ι* parent_node n'" by -(rule intra_path_Append)
      thus ?thesis by blast
    next
      fix m assume "n'' = CFG_node m" and "m = parent_node n'"
      with ‹parent_node n -as→⇩ι* parent_node n''› show ?thesis by fastforce
    qed
  next
    case (isSp_Append_ddep n ns n'' V n')
    from ‹∃as. parent_node n -as→⇩ι* parent_node n''›
    obtain as where "parent_node n -as→⇩ι* parent_node n''" by blast 
    from ‹n'' s-V→⇩d⇩d n'› have "n'' influences V in n'"
      by(fastforce elim:sum_SDG_edge.cases)
    then obtain as' where "parent_node n'' -as'→⇩ι* parent_node n'"
      by(auto simp:data_dependence_def)
    with ‹parent_node n -as→⇩ι* parent_node n''› 
    have "parent_node n -as@as'→⇩ι* parent_node n'" by -(rule intra_path_Append)
    thus ?case by blast
  next
    case (isSp_Append_sum n ns n'' p n')
    from ‹∃as. parent_node n -as→⇩ι* parent_node n''›
    obtain as where "parent_node n -as→⇩ι* parent_node n''" by blast
    from ‹n'' s-p→⇘sum⇙ n'› have "∃as'. parent_node n'' -as'→⇩ι* parent_node n'"
    proof(rule sum_edge_cases)
      fix a Q fs a'
      assume "valid_edge a" and "a' ∈ get_return_edges a"
        and "n'' = CFG_node (sourcenode a)" and "n' = CFG_node (targetnode a')"
      from ‹valid_edge a› ‹a' ∈ get_return_edges a›
      obtain a'' where "sourcenode a -[a'']→⇩ι* targetnode a'"
        apply - apply(drule call_return_node_edge)
        apply(auto simp:intra_path_def) apply(drule path_edge)
        by(auto simp:intra_kind_def)
      with ‹n'' = CFG_node (sourcenode a)› ‹n' = CFG_node (targetnode a')›
      show ?thesis by simp blast
    next
      fix a Q p fs a' ns x x' ins outs
      assume "valid_edge a" and "a' ∈ get_return_edges a"
        and "n'' = Actual_in (sourcenode a, x)" 
        and "n' = Actual_out (targetnode a', x')"
      from ‹valid_edge a› ‹a' ∈ get_return_edges a›
      obtain a'' where "sourcenode a -[a'']→⇩ι* targetnode a'"
        apply - apply(drule call_return_node_edge)
        apply(auto simp:intra_path_def) apply(drule path_edge)
        by(auto simp:intra_kind_def)
      with ‹n'' = Actual_in (sourcenode a, x)› ‹n' = Actual_out (targetnode a', x')›
      show ?thesis by simp blast
    qed
    then obtain as' where "parent_node n'' -as'→⇩ι* parent_node n'" by blast
    with ‹parent_node n -as→⇩ι* parent_node n''› 
    have "parent_node n -as@as'→⇩ι* parent_node n'" by -(rule intra_path_Append)
    thus ?case by blast
  qed
qed


lemma matched_is_SDG_path:
  assumes "matched n ns n'" obtains ns' where "n is-ns'→⇩d* n'"
proof(atomize_elim)
  from ‹matched n ns n'› show "∃ns'. n is-ns'→⇩d* n'"
  proof(induct rule:matched.induct)
    case matched_Nil thus ?case by(fastforce intro:isSp_Nil)
  next
    case matched_Append_intra_SDG_path thus ?case
    by(fastforce intro:is_SDG_path_Append intra_SDG_path_is_SDG_path)
  next
    case (matched_bracket_call n⇩0 ns n⇩1 p n⇩2 ns' n⇩3 n⇩4 V a a')
    from ‹∃ns'. n⇩0 is-ns'→⇩d* n⇩1› obtain nsx where "n⇩0 is-nsx→⇩d* n⇩1" by blast
    from ‹n⇩1 -p→⇘call⇙ n⇩2› ‹sourcenode a = parent_node n⇩1› ‹targetnode a = parent_node n⇩2›
    have "n⇩1 = CFG_node (sourcenode a)" and "n⇩2 = CFG_node (targetnode a)"
      by(auto elim:SDG_edge.cases)
    from ‹valid_edge a› ‹a' ∈ get_return_edges a›
    obtain Q r p' fs where "kind a = Q:r↪⇘p'⇙fs" 
      by(fastforce dest!:only_call_get_return_edges)
    with ‹n⇩1 -p→⇘call⇙ n⇩2› ‹valid_edge a›
      ‹n⇩1 = CFG_node (sourcenode a)› ‹n⇩2 = CFG_node (targetnode a)›
    have [simp]:"p' = p" by -(erule SDG_edge.cases,(fastforce dest:edge_det)+)
    from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'"
      by(rule get_return_edges_valid)
    from ‹n⇩3 -p→⇘ret⇙ n⇩4 ∨ n⇩3 -p:V→⇘out⇙ n⇩4› show ?case
    proof
      assume "n⇩3 -p→⇘ret⇙ n⇩4"
      then obtain ax Q' f' where "valid_edge ax" and "kind ax = Q'↩⇘p⇙f'"
        and "n⇩3 = CFG_node (sourcenode ax)" and "n⇩4 = CFG_node (targetnode ax)"
        by(fastforce elim:SDG_edge.cases)
      with ‹sourcenode a' = parent_node n⇩3› ‹targetnode a' = parent_node n⇩4› 
        ‹valid_edge a'› have [simp]:"ax = a'" by(fastforce dest:edge_det)
      from ‹valid_edge a› ‹kind a = Q:r↪⇘p'⇙fs› ‹valid_edge ax› ‹kind ax = Q'↩⇘p⇙f'›
        ‹a' ∈ get_return_edges a› ‹matched n⇩2 ns' n⇩3›
        ‹n⇩1 = CFG_node (sourcenode a)› ‹n⇩2 = CFG_node (targetnode a)›
        ‹n⇩3 = CFG_node (sourcenode ax)› ‹n⇩4 = CFG_node (targetnode ax)›
      have "n⇩1 s-p→⇘sum⇙ n⇩4" 
        by(fastforce intro!:sum_SDG_call_summary_edge[of a _ _ _ _ ax])
      with ‹n⇩0 is-nsx→⇩d* n⇩1› have "n⇩0 is-nsx@[n⇩1]→⇩d* n⇩4" by(rule isSp_Append_sum)
      thus ?case by blast
    next
      assume "n⇩3 -p:V→⇘out⇙ n⇩4"
      then obtain ax Q' f' x where "valid_edge ax" and "kind ax = Q'↩⇘p⇙f'"
        and "n⇩3 = Formal_out (sourcenode ax,x)" 
        and "n⇩4 = Actual_out (targetnode ax,x)"
        by(fastforce elim:SDG_edge.cases)
      with ‹sourcenode a' = parent_node n⇩3› ‹targetnode a' = parent_node n⇩4› 
        ‹valid_edge a'› have [simp]:"ax = a'" by(fastforce dest:edge_det)
      from ‹valid_edge ax› ‹kind ax = Q'↩⇘p⇙f'› ‹n⇩3 = Formal_out (sourcenode ax,x)›
        ‹n⇩4 = Actual_out (targetnode ax,x)›
      have "CFG_node (sourcenode a') -p→⇘ret⇙ CFG_node (targetnode a')"
        by(fastforce intro:SDG_return_edge)
      from ‹valid_edge a› ‹kind a = Q:r↪⇘p'⇙fs› ‹valid_edge a'› 
        ‹a' ∈ get_return_edges a› ‹n⇩4 = Actual_out (targetnode ax,x)›
      have "CFG_node (targetnode a) ⟶⇘cd⇙ CFG_node (sourcenode a')"
        by(fastforce intro!:SDG_proc_entry_exit_cdep)
      with ‹n⇩2 = CFG_node (targetnode a)›
      have "matched n⇩2 ([]@([]@[n⇩2])) (CFG_node (sourcenode a'))"
        by(fastforce intro:matched.intros intra_SDG_path.intros 
                          SDG_edge_valid_SDG_node) 
      with ‹valid_edge a› ‹kind a = Q:r↪⇘p'⇙fs› ‹valid_edge a'› ‹kind ax = Q'↩⇘p⇙f'›
        ‹a' ∈ get_return_edges a› ‹n⇩1 = CFG_node (sourcenode a)› 
        ‹n⇩2 = CFG_node (targetnode a)› ‹n⇩4 = Actual_out (targetnode ax,x)›
      have "n⇩1 s-p→⇘sum⇙ CFG_node (targetnode a')"
        by(fastforce intro!:sum_SDG_call_summary_edge[of a _ _ _ _ a'])
      with ‹n⇩0 is-nsx→⇩d* n⇩1› have "n⇩0 is-nsx@[n⇩1]→⇩d* CFG_node (targetnode a')"
        by(rule isSp_Append_sum)
      from ‹n⇩4 = Actual_out (targetnode ax,x)› ‹n⇩3 -p:V→⇘out⇙ n⇩4›
      have "CFG_node (targetnode a') s⟶⇘cd⇙ n⇩4"
        by(fastforce intro:sum_SDG_parent_cdep_edge SDG_edge_valid_SDG_node)
      with ‹n⇩0 is-nsx@[n⇩1]→⇩d* CFG_node (targetnode a')›
      have "n⇩0 is-(nsx@[n⇩1])@[CFG_node (targetnode a')]→⇩d* n⇩4"
        by(rule isSp_Append_cdep)
      thus ?case by blast
    qed
  next
    case (matched_bracket_param n⇩0 ns n⇩1 p V n⇩2 ns' n⇩3 V' n⇩4 a a')
    from ‹∃ns'. n⇩0 is-ns'→⇩d* n⇩1› obtain nsx where "n⇩0 is-nsx→⇩d* n⇩1" by blast
    from ‹n⇩1 -p:V→⇘in⇙ n⇩2› ‹sourcenode a = parent_node n⇩1›
      ‹targetnode a = parent_node n⇩2› obtain x ins outs
      where "n⇩1 = Actual_in (sourcenode a,x)" and "n⇩2 = Formal_in (targetnode a,x)"
      and "(p,ins,outs) ∈ set procs" and "V = ins!x" and "x < length ins"
      by(fastforce elim:SDG_edge.cases)
    from ‹valid_edge a› ‹a' ∈ get_return_edges a›
    obtain Q r p' fs where "kind a = Q:r↪⇘p'⇙fs"
      by(fastforce dest!:only_call_get_return_edges)
    with ‹n⇩1 -p:V→⇘in⇙ n⇩2› ‹valid_edge a›
      ‹n⇩1 = Actual_in (sourcenode a,x)› ‹n⇩2 = Formal_in (targetnode a,x)›
    have [simp]:"p' = p" by -(erule SDG_edge.cases,(fastforce dest:edge_det)+)
    from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'"
      by(rule get_return_edges_valid)
    from ‹n⇩3 -p:V'→⇘out⇙ n⇩4› obtain ax Q' f' x' ins' outs' where "valid_edge ax" 
      and "kind ax = Q'↩⇘p⇙f'" and "n⇩3 = Formal_out (sourcenode ax,x')" 
      and "n⇩4 = Actual_out (targetnode ax,x')" and "(p,ins',outs') ∈ set procs"
      and "V' = outs'!x'" and "x' < length outs'"
      by(fastforce elim:SDG_edge.cases)
    with ‹sourcenode a' = parent_node n⇩3› ‹targetnode a' = parent_node n⇩4›
      ‹valid_edge a'› have [simp]:"ax = a'" by(fastforce dest:edge_det)
    from unique_callers ‹(p,ins,outs) ∈ set procs› ‹(p,ins',outs') ∈ set procs›
    have [simp]:"ins = ins'" "outs = outs'"
      by(auto dest:distinct_fst_isin_same_fst)
    from ‹valid_edge a› ‹kind a = Q:r↪⇘p'⇙fs› ‹valid_edge a'› ‹kind ax = Q'↩⇘p⇙f'›
      ‹a' ∈ get_return_edges a› ‹matched n⇩2 ns' n⇩3› ‹n⇩1 = Actual_in (sourcenode a,x)› 
      ‹n⇩2 = Formal_in (targetnode a,x)› ‹n⇩3 = Formal_out (sourcenode ax,x')›
      ‹n⇩4 = Actual_out (targetnode ax,x')› ‹(p,ins,outs) ∈ set procs›
      ‹x < length ins› ‹x' < length outs'› ‹V = ins!x› ‹V' = outs'!x'›
    have "n⇩1 s-p→⇘sum⇙ n⇩4" 
      by(fastforce intro!:sum_SDG_param_summary_edge[of a _ _ _ _ a'])
    with ‹n⇩0 is-nsx→⇩d* n⇩1› have "n⇩0 is-nsx@[n⇩1]→⇩d* n⇩4" by(rule isSp_Append_sum)
    thus ?case by blast
  qed
qed


lemma is_SDG_path_matched:
  assumes "n is-ns→⇩d* n'" obtains ns' where "matched n ns' n'" and "set ns ⊆ set ns'"
proof(atomize_elim)
  from ‹n is-ns→⇩d* n'› show "∃ns'. matched n ns' n' ∧ set ns ⊆ set ns'"
  proof(induct rule:intra_sum_SDG_path.induct)
    case (isSp_Nil n)
    from ‹valid_SDG_node n› have "matched n [] n" by(rule matched_Nil)
    thus ?case by fastforce
  next
    case (isSp_Append_cdep n ns n'' n')
    from ‹∃ns'. matched n ns' n'' ∧ set ns ⊆ set ns'›
    obtain ns' where "matched n ns' n''" and "set ns ⊆ set ns'" by blast
    from ‹n'' s⟶⇘cd⇙ n'› have "n'' i-[]@[n'']→⇩d* n'"
      by(fastforce intro:intra_SDG_path.intros sum_SDG_edge_valid_SDG_node 
                        sum_SDG_edge_SDG_edge)
    with ‹matched n ns' n''› have "matched n (ns'@[n'']) n'"
      by(fastforce intro!:matched_Append_intra_SDG_path)
    with ‹set ns ⊆ set ns'› show ?case by fastforce
  next
    case (isSp_Append_ddep n ns n'' V n')
    from ‹∃ns'. matched n ns' n'' ∧ set ns ⊆ set ns'›
    obtain ns' where "matched n ns' n''" and "set ns ⊆ set ns'" by blast
    from ‹n'' s-V→⇩d⇩d n'› ‹n'' ≠ n'› have "n'' i-[]@[n'']→⇩d* n'"
      by(fastforce intro:intra_SDG_path.intros sum_SDG_edge_valid_SDG_node 
                        sum_SDG_edge_SDG_edge)
    with ‹matched n ns' n''› have "matched n (ns'@[n'']) n'"
      by(fastforce intro!:matched_Append_intra_SDG_path)
    with ‹set ns ⊆ set ns'› show ?case by fastforce
  next
    case (isSp_Append_sum n ns n'' p n')
    from ‹∃ns'. matched n ns' n'' ∧ set ns ⊆ set ns'›
    obtain ns' where "matched n ns' n''" and "set ns ⊆ set ns'" by blast
    from ‹n'' s-p→⇘sum⇙ n'› obtain ns'' where "matched n'' ns'' n'" and "n'' ∈ set ns''"
      by -(erule sum_SDG_summary_edge_matched)
    with ‹matched n ns' n''› have "matched n (ns'@ns'') n'" by -(rule matched_Append)
    with ‹set ns ⊆ set ns'› ‹n'' ∈ set ns''› show ?case by fastforce
  qed
qed


lemma is_SDG_path_intra_CFG_path:
  assumes "n is-ns→⇩d* n'"
  obtains as where "parent_node n -as→⇩ι* parent_node n'" 
proof(atomize_elim)
  from ‹n is-ns→⇩d* n'›
  show "∃as. parent_node n -as→⇩ι* parent_node n'"
  proof(induct rule:intra_sum_SDG_path.induct)
    case (isSp_Nil n)
    from ‹valid_SDG_node n› have "parent_node n -[]→* parent_node n"
      by(fastforce intro:empty_path valid_SDG_CFG_node)
    thus ?case by(auto simp:intra_path_def)
  next
    case (isSp_Append_cdep n ns n'' n')
    from ‹∃as. parent_node n -as→⇩ι* parent_node n''›
    obtain as where "parent_node n -as→⇩ι* parent_node n''" by blast
    from ‹n'' s⟶⇘cd⇙ n'› have "n'' ⟶⇘cd⇙ n'" by(rule sum_SDG_edge_SDG_edge)
    thus ?case
    proof(rule cdep_edge_cases)
      assume "parent_node n'' controls parent_node n'"
      then obtain as' where "parent_node n'' -as'→⇩ι* parent_node n'" and "as' ≠ []"
        by(erule control_dependence_path)
      with ‹parent_node n -as→⇩ι* parent_node n''› 
      have "parent_node n -as@as'→⇩ι* parent_node n'" by -(rule intra_path_Append)
      thus ?thesis by blast
    next
      fix a Q r p fs a'
      assume "valid_edge a" and "kind a = Q:r↪⇘p⇙fs" "a' ∈ get_return_edges a"
        and "parent_node n'' = targetnode a" and "parent_node n' = sourcenode a'"
      then obtain a'' where "valid_edge a''" and "sourcenode a'' = targetnode a"
        and "targetnode a'' = sourcenode a'" and "kind a'' = (λcf. False)⇩√"
        by(auto dest:intra_proc_additional_edge)
      hence "targetnode a -[a'']→⇩ι* sourcenode a'"
        by(fastforce dest:path_edge simp:intra_path_def intra_kind_def)
      with ‹parent_node n'' = targetnode a› ‹parent_node n' = sourcenode a'› 
      have "∃as'. parent_node n'' -as'→⇩ι* parent_node n' ∧ as' ≠ []" by fastforce
      then obtain as' where "parent_node n'' -as'→⇩ι* parent_node n'" and "as' ≠ []"
        by blast
      with ‹parent_node n -as→⇩ι* parent_node n''› 
      have "parent_node n -as@as'→⇩ι* parent_node n'" by -(rule intra_path_Append)
      thus ?thesis by blast
    next
      fix m assume "n'' = CFG_node m" and "m = parent_node n'"
      with ‹parent_node n -as→⇩ι* parent_node n''› show ?thesis by fastforce
    qed
  next
    case (isSp_Append_ddep n ns n'' V n')
    from ‹∃as. parent_node n -as→⇩ι* parent_node n''›
    obtain as where "parent_node n -as→⇩ι* parent_node n''"  by blast
    from ‹n'' s-V→⇩d⇩d n'› have "n'' influences V in n'"
      by(fastforce elim:sum_SDG_edge.cases)
    then obtain as' where "parent_node n'' -as'→⇩ι* parent_node n'"
      by(auto simp:data_dependence_def)
    with ‹parent_node n -as→⇩ι* parent_node n''› 
    have "parent_node n -as@as'→⇩ι* parent_node n'" by -(rule intra_path_Append)
    thus ?case by blast
  next
    case (isSp_Append_sum n ns n'' p n')
    from ‹∃as. parent_node n -as→⇩ι* parent_node n''›
    obtain as where "parent_node n -as→⇩ι* parent_node n''"  by blast
    from ‹n'' s-p→⇘sum⇙ n'› obtain ns' where "matched n'' ns' n'"
      by -(erule sum_SDG_summary_edge_matched)
    then obtain as' where "parent_node n'' -as'→⇩ι* parent_node n'"
      by(erule matched_intra_CFG_path)
    with ‹parent_node n -as→⇩ι* parent_node n''› 
    have "parent_node n -as@as'→⇩ι* parent_node n'"
      by(fastforce intro:path_Append simp:intra_path_def)
    thus ?case by blast
  qed
qed


text ‹SDG paths without return edges›

inductive intra_call_sum_SDG_path ::
  "'node SDG_node ⇒ 'node SDG_node list ⇒ 'node SDG_node ⇒ bool"
("_ ics-_→⇩d* _" [51,0,0] 80)
where icsSp_Nil:
  "valid_SDG_node n ⟹ n ics-[]→⇩d* n"

  | icsSp_Append_cdep:
  "⟦n ics-ns→⇩d* n''; n'' s⟶⇘cd⇙ n'⟧ ⟹ n ics-ns@[n'']→⇩d* n'"

  | icsSp_Append_ddep:
  "⟦n ics-ns→⇩d* n''; n'' s-V→⇩d⇩d n'; n'' ≠ n'⟧ ⟹ n ics-ns@[n'']→⇩d* n'"

  | icsSp_Append_sum:
  "⟦n ics-ns→⇩d* n''; n'' s-p→⇘sum⇙ n'⟧ ⟹ n ics-ns@[n'']→⇩d* n'"

  | icsSp_Append_call:
  "⟦n ics-ns→⇩d* n''; n'' s-p→⇘call⇙ n'⟧ ⟹ n ics-ns@[n'']→⇩d* n'"

  | icsSp_Append_param_in:
  "⟦n ics-ns→⇩d* n''; n'' s-p:V→⇘in⇙ n'⟧ ⟹ n ics-ns@[n'']→⇩d* n'"


lemma ics_SDG_path_valid_SDG_node:
  assumes "n ics-ns→⇩d* n'" shows "valid_SDG_node n" and "valid_SDG_node n'"
using ‹n ics-ns→⇩d* n'›
by(induct rule:intra_call_sum_SDG_path.induct,
   auto intro:sum_SDG_edge_valid_SDG_node valid_SDG_CFG_node)


lemma ics_SDG_path_Append:
  "⟦n'' ics-ns'→⇩d* n'; n ics-ns→⇩d* n''⟧ ⟹ n ics-ns@ns'→⇩d* n'"
by(induct rule:intra_call_sum_SDG_path.induct,
   auto intro:intra_call_sum_SDG_path.intros simp:append_assoc[THEN sym] 
                                        simp del:append_assoc)


lemma is_SDG_path_ics_SDG_path:
  "n is-ns→⇩d* n' ⟹ n ics-ns→⇩d* n'"
by(induct rule:intra_sum_SDG_path.induct,auto intro:intra_call_sum_SDG_path.intros)


lemma cc_SDG_path_ics_SDG_path:
  "n cc-ns→⇩d* n' ⟹ n ics-ns→⇩d* n'"
by(induct rule:call_cdep_SDG_path.induct,
  auto intro:intra_call_sum_SDG_path.intros SDG_edge_sum_SDG_edge)


lemma ics_SDG_path_split:
  assumes "n ics-ns→⇩d* n'" and "n'' ∈ set ns" 
  obtains ns' ns'' where "ns = ns'@ns''" and "n ics-ns'→⇩d* n''" 
  and "n'' ics-ns''→⇩d* n'"
proof(atomize_elim)
  from ‹n ics-ns→⇩d* n'› ‹n'' ∈ set ns›
  show "∃ns' ns''. ns = ns'@ns'' ∧ n ics-ns'→⇩d* n'' ∧ n'' ics-ns''→⇩d* n'"
  proof(induct rule:intra_call_sum_SDG_path.induct)
    case icsSp_Nil thus ?case by simp
  next
    case (icsSp_Append_cdep n ns nx n')
    note IH = ‹n'' ∈ set ns ⟹
      ∃ns' ns''. ns = ns' @ ns'' ∧ n ics-ns'→⇩d* n'' ∧ n'' ics-ns''→⇩d* nx›
    from ‹n'' ∈ set (ns@[nx])› have "n'' ∈ set ns ∨ n'' = nx" by fastforce
    thus ?case
    proof
      assume "n'' ∈ set ns"
      from IH[OF this] obtain ns' ns'' where "ns = ns' @ ns''"
        and "n ics-ns'→⇩d* n''" and "n'' ics-ns''→⇩d* nx" by blast
      from ‹n'' ics-ns''→⇩d* nx› ‹nx s⟶⇘cd⇙ n'›
      have "n'' ics-ns''@[nx]→⇩d* n'"
        by(rule intra_call_sum_SDG_path.icsSp_Append_cdep)
      with ‹ns = ns'@ns''› ‹n ics-ns'→⇩d* n''› show ?thesis by fastforce
    next
      assume "n'' = nx"
      from ‹nx s⟶⇘cd⇙ n'› have "nx ics-[]→⇩d* nx"
        by(fastforce intro:icsSp_Nil SDG_edge_valid_SDG_node sum_SDG_edge_SDG_edge)
      with ‹nx s⟶⇘cd⇙ n'› have "nx ics-[]@[nx]→⇩d* n'"
        by -(rule intra_call_sum_SDG_path.icsSp_Append_cdep)
      with ‹n ics-ns→⇩d* nx› ‹n'' = nx› show ?thesis by fastforce
    qed
  next
    case (icsSp_Append_ddep n ns nx V n')
    note IH = ‹n'' ∈ set ns ⟹
      ∃ns' ns''. ns = ns' @ ns'' ∧ n ics-ns'→⇩d* n'' ∧ n'' ics-ns''→⇩d* nx›
    from ‹n'' ∈ set (ns@[nx])› have "n'' ∈ set ns ∨ n'' = nx" by fastforce
    thus ?case
    proof
      assume "n'' ∈ set ns"
      from IH[OF this] obtain ns' ns'' where "ns = ns' @ ns''"
        and "n ics-ns'→⇩d* n''" and "n'' ics-ns''→⇩d* nx" by blast
      from ‹n'' ics-ns''→⇩d* nx› ‹nx s-V→⇩d⇩d n'› ‹nx ≠ n'›
      have "n'' ics-ns''@[nx]→⇩d* n'"
        by(rule intra_call_sum_SDG_path.icsSp_Append_ddep)
      with ‹ns = ns'@ns''› ‹n ics-ns'→⇩d* n''› show ?thesis by fastforce
    next
      assume "n'' = nx"
      from ‹nx s-V→⇩d⇩d n'› have "nx ics-[]→⇩d* nx"
        by(fastforce intro:icsSp_Nil SDG_edge_valid_SDG_node sum_SDG_edge_SDG_edge)
      with ‹nx s-V→⇩d⇩d n'› ‹nx ≠ n'› have "nx ics-[]@[nx]→⇩d* n'"
        by -(rule intra_call_sum_SDG_path.icsSp_Append_ddep)
      with ‹n ics-ns→⇩d* nx› ‹n'' = nx› show ?thesis by fastforce
    qed
  next
    case (icsSp_Append_sum n ns nx p n')
    note IH = ‹n'' ∈ set ns ⟹
      ∃ns' ns''. ns = ns' @ ns'' ∧ n ics-ns'→⇩d* n'' ∧ n'' ics-ns''→⇩d* nx›
    from ‹n'' ∈ set (ns@[nx])› have "n'' ∈ set ns ∨ n'' = nx" by fastforce
    thus ?case
    proof
      assume "n'' ∈ set ns"
      from IH[OF this] obtain ns' ns'' where "ns = ns' @ ns''"
        and "n ics-ns'→⇩d* n''" and "n'' ics-ns''→⇩d* nx" by blast
      from ‹n'' ics-ns''→⇩d* nx› ‹nx s-p→⇘sum⇙ n'›
      have "n'' ics-ns''@[nx]→⇩d* n'"
        by(rule intra_call_sum_SDG_path.icsSp_Append_sum)
      with ‹ns = ns'@ns''› ‹n ics-ns'→⇩d* n''› show ?thesis by fastforce
    next
      assume "n'' = nx"
      from ‹nx s-p→⇘sum⇙ n'› have "valid_SDG_node nx"
        by(fastforce elim:sum_SDG_edge.cases)
      hence "nx ics-[]→⇩d* nx" by(fastforce intro:icsSp_Nil)
      with ‹nx s-p→⇘sum⇙ n'› have "nx ics-[]@[nx]→⇩d* n'"
        by -(rule intra_call_sum_SDG_path.icsSp_Append_sum)
      with ‹n ics-ns→⇩d* nx› ‹n'' = nx› show ?thesis by fastforce
    qed
  next
    case (icsSp_Append_call n ns nx p n')
    note IH = ‹n'' ∈ set ns ⟹
      ∃ns' ns''. ns = ns' @ ns'' ∧ n ics-ns'→⇩d* n'' ∧ n'' ics-ns''→⇩d* nx›
    from ‹n'' ∈ set (ns@[nx])› have "n'' ∈ set ns ∨ n'' = nx" by fastforce
    thus ?case
    proof
      assume "n'' ∈ set ns"
      from IH[OF this] obtain ns' ns'' where "ns = ns' @ ns''"
        and "n ics-ns'→⇩d* n''" and "n'' ics-ns''→⇩d* nx" by blast
      from ‹n'' ics-ns''→⇩d* nx› ‹nx s-p→⇘call⇙ n'›
      have "n'' ics-ns''@[nx]→⇩d* n'"
        by(rule intra_call_sum_SDG_path.icsSp_Append_call)
      with ‹ns = ns'@ns''› ‹n ics-ns'→⇩d* n''› show ?thesis by fastforce
    next
      assume "n'' = nx"
      from ‹nx s-p→⇘call⇙ n'› have "nx ics-[]→⇩d* nx"
        by(fastforce intro:icsSp_Nil SDG_edge_valid_SDG_node sum_SDG_edge_SDG_edge)
      with ‹nx s-p→⇘call⇙ n'› have "nx ics-[]@[nx]→⇩d* n'"
        by -(rule intra_call_sum_SDG_path.icsSp_Append_call)
      with ‹n ics-ns→⇩d* nx› ‹n'' = nx› show ?thesis by fastforce
    qed
  next
    case (icsSp_Append_param_in n ns nx p V n')
    note IH = ‹n'' ∈ set ns ⟹
      ∃ns' ns''. ns = ns' @ ns'' ∧ n ics-ns'→⇩d* n'' ∧ n'' ics-ns''→⇩d* nx›
    from ‹n'' ∈ set (ns@[nx])› have "n'' ∈ set ns ∨ n'' = nx" by fastforce
    thus ?case
    proof
      assume "n'' ∈ set ns"
      from IH[OF this] obtain ns' ns'' where "ns = ns' @ ns''"
        and "n ics-ns'→⇩d* n''" and "n'' ics-ns''→⇩d* nx" by blast
      from ‹n'' ics-ns''→⇩d* nx› ‹nx s-p:V→⇘in⇙ n'›
      have "n'' ics-ns''@[nx]→⇩d* n'"
        by(rule intra_call_sum_SDG_path.icsSp_Append_param_in)
      with ‹ns = ns'@ns''› ‹n ics-ns'→⇩d* n''› show ?thesis by fastforce
    next
      assume "n'' = nx"
      from ‹nx s-p:V→⇘in⇙ n'› have "nx ics-[]→⇩d* nx"
        by(fastforce intro:icsSp_Nil SDG_edge_valid_SDG_node sum_SDG_edge_SDG_edge)
      with ‹nx s-p:V→⇘in⇙ n'› have "nx ics-[]@[nx]→⇩d* n'"
        by -(rule intra_call_sum_SDG_path.icsSp_Append_param_in)
      with ‹n ics-ns→⇩d* nx› ‹n'' = nx› show ?thesis by fastforce
    qed
  qed
qed


lemma realizable_ics_SDG_path:
  assumes "realizable n ns n'" obtains ns' where "n ics-ns'→⇩d* n'"
proof(atomize_elim)
  from ‹realizable n ns n'› show "∃ns'. n ics-ns'→⇩d* n'"
  proof(induct rule:realizable.induct)
    case (realizable_matched n ns n')
    from ‹matched n ns n'› obtain ns' where "n is-ns'→⇩d* n'"
      by(erule matched_is_SDG_path)
    thus ?case by(fastforce intro:is_SDG_path_ics_SDG_path)
  next
    case (realizable_call n⇩0 ns n⇩1 p n⇩2 V ns' n⇩3)
    from ‹∃ns'. n⇩0 ics-ns'→⇩d* n⇩1› obtain nsx where "n⇩0 ics-nsx→⇩d* n⇩1" by blast
    with ‹n⇩1 -p→⇘call⇙ n⇩2 ∨ n⇩1 -p:V→⇘in⇙ n⇩2› have "n⇩0 ics-nsx@[n⇩1]→⇩d* n⇩2"
      by(fastforce intro:SDG_edge_sum_SDG_edge icsSp_Append_call icsSp_Append_param_in)
    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 ics-nsx'→⇩d* n⇩3" by(rule is_SDG_path_ics_SDG_path)
    from ‹n⇩2 ics-nsx'→⇩d* n⇩3› ‹n⇩0 ics-nsx@[n⇩1]→⇩d* n⇩2›
    have "n⇩0 ics-(nsx@[n⇩1])@nsx'→⇩d* n⇩3" by(rule ics_SDG_path_Append)
    thus ?case by blast
  qed
qed


lemma ics_SDG_path_realizable:
  assumes "n ics-ns→⇩d* n'" 
  obtains ns' where "realizable n ns' n'" and "set ns ⊆ set ns'"
proof(atomize_elim)
  from ‹n ics-ns→⇩d* n'› show "∃ns'. realizable n ns' n' ∧ set ns ⊆ set ns'"
  proof(induct rule:intra_call_sum_SDG_path.induct)
    case (icsSp_Nil n)
    hence "matched n [] n" by(rule matched_Nil)
    thus ?case by(fastforce intro:realizable_matched)
  next
    case (icsSp_Append_cdep n ns n'' n')
    from ‹∃ns'. realizable n ns' n'' ∧ set ns ⊆ set ns'›
    obtain ns' where "realizable n ns' n''" and "set ns ⊆ set ns'" by blast
    from ‹n'' s⟶⇘cd⇙ n'› have "valid_SDG_node n''" by(rule sum_SDG_edge_valid_SDG_node)
    hence "n'' i-[]→⇩d* n''" by(rule iSp_Nil)
    with ‹n'' s⟶⇘cd⇙ n'› have "n'' i-[]@[n'']→⇩d* n'"
      by(fastforce elim:iSp_Append_cdep sum_SDG_edge_SDG_edge)
    hence "matched n'' [n''] n'" by(fastforce intro:intra_SDG_path_matched)
    with ‹realizable n ns' n''› have "realizable n (ns'@[n'']) n'"
      by(rule realizable_Append_matched)
    with ‹set ns ⊆ set ns'› show ?case by fastforce
  next
    case (icsSp_Append_ddep n ns n'' V n')
    from ‹∃ns'. realizable n ns' n'' ∧ set ns ⊆ set ns'›
    obtain ns' where "realizable n ns' n''" and "set ns ⊆ set ns'" by blast
    from ‹n'' s-V→⇩d⇩d n'› have "valid_SDG_node n''"
      by(rule sum_SDG_edge_valid_SDG_node)
    hence "n'' i-[]→⇩d* n''" by(rule iSp_Nil)
    with ‹n'' s-V→⇩d⇩d n'› ‹n'' ≠ n'› have "n'' i-[]@[n'']→⇩d* n'"
      by(fastforce elim:iSp_Append_ddep sum_SDG_edge_SDG_edge)
    hence "matched n'' [n''] n'" by(fastforce intro:intra_SDG_path_matched)
    with ‹realizable n ns' n''› have "realizable n (ns'@[n'']) n'"
      by(fastforce intro:realizable_Append_matched)
    with ‹set ns ⊆ set ns'› show ?case by fastforce
  next
    case (icsSp_Append_sum n ns n'' p n')
    from ‹∃ns'. realizable n ns' n'' ∧ set ns ⊆ set ns'›
    obtain ns' where "realizable n ns' n''" and "set ns ⊆ set ns'" by blast
    from ‹n'' s-p→⇘sum⇙ n'› show ?case
    proof(rule sum_edge_cases)
      fix a Q r fs a'
      assume "valid_edge a" and "kind a = Q:r↪⇘p⇙fs" and "a' ∈ get_return_edges a"
        and "n'' = CFG_node (sourcenode a)" and "n' = CFG_node (targetnode a')"
      from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹a' ∈ get_return_edges a›
      have match':"matched (CFG_node (targetnode a)) [CFG_node (targetnode a)]
        (CFG_node (sourcenode a'))"
        by(rule intra_proc_matched)
      from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹n'' = CFG_node (sourcenode a)›
      have "n'' -p→⇘call⇙ CFG_node (targetnode a)"
        by(fastforce intro:SDG_call_edge)
      hence "matched n'' [] n''"
        by(fastforce intro:matched_Nil SDG_edge_valid_SDG_node)
      from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'"
        by(rule get_return_edges_valid)
      from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹a' ∈ get_return_edges a›
      obtain Q' f' where "kind a' = Q'↩⇘p⇙f'" by(fastforce dest!:call_return_edges)
      from ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'› ‹n' = CFG_node (targetnode a')›
      have "CFG_node (sourcenode a') -p→⇘ret⇙ n'"
        by(fastforce intro:SDG_return_edge)
      from ‹matched n'' [] n''› ‹n'' -p→⇘call⇙ CFG_node (targetnode a)›
        match' ‹CFG_node (sourcenode a') -p→⇘ret⇙ n'› ‹valid_edge a› 
        ‹a' ∈ get_return_edges a› ‹n' = CFG_node (targetnode a')› 
        ‹n'' = CFG_node (sourcenode a)›
      have "matched n'' ([]@n''#[CFG_node (targetnode a)]@[CFG_node (sourcenode a')])
        n'"
        by(fastforce intro:matched_bracket_call)
      with ‹realizable n ns' n''›
      have "realizable n 
        (ns'@(n''#[CFG_node (targetnode a),CFG_node (sourcenode a')])) n'"
        by(fastforce intro:realizable_Append_matched)
      with ‹set ns ⊆ set ns'› show ?thesis by fastforce
    next
      fix a Q r p fs a' ns'' x x' ins outs
      assume "valid_edge a" and "kind a = Q:r↪⇘p⇙fs" and "a' ∈ get_return_edges a"
        and match':"matched (Formal_in (targetnode a,x)) ns'' 
                            (Formal_out (sourcenode a',x'))"
        and "n'' = Actual_in (sourcenode a,x)" 
        and "n' = Actual_out (targetnode a',x')" and "(p,ins,outs) ∈ set procs" 
        and "x < length ins" and "x' < length outs"
      from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹n'' = Actual_in (sourcenode a,x)›
        ‹(p,ins,outs) ∈ set procs› ‹x < length ins›
      have "n'' -p:ins!x→⇘in⇙ Formal_in (targetnode a,x)"
        by(fastforce intro!:SDG_param_in_edge)
      hence "matched n'' [] n''" 
        by(fastforce intro:matched_Nil SDG_edge_valid_SDG_node)
      from ‹valid_edge a› ‹a' ∈ get_return_edges a› have "valid_edge a'"
        by(rule get_return_edges_valid)
      from ‹valid_edge a› ‹kind a = Q:r↪⇘p⇙fs› ‹a' ∈ get_return_edges a›
      obtain Q' f' where "kind a' = Q'↩⇘p⇙f'" by(fastforce dest!:call_return_edges)
      from ‹valid_edge a'› ‹kind a' = Q'↩⇘p⇙f'› ‹n' = Actual_out (targetnode a',x')›
        ‹(p,ins,outs) ∈ set procs› ‹x' < length outs›
      have "Formal_out (sourcenode a',x') -p:outs!x'→⇘out⇙ n'"
        by(fastforce intro:SDG_param_out_edge)
      from ‹matched n'' [] n''› ‹n'' -p:ins!x→⇘in⇙ Formal_in (targetnode a,x)›
        match' ‹Formal_out (sourcenode a',x') -p:outs!x'→⇘out⇙ n'› ‹valid_edge a› 
        ‹a' ∈ get_return_edges a› ‹n' = Actual_out (targetnode a',x')›
        ‹n'' = Actual_in (sourcenode a,x)›
      have "matched n'' ([]@n''#ns''@[Formal_out (sourcenode a',x')]) n'"
        by(fastforce intro:matched_bracket_param)
      with ‹realizable n ns' n''›
      have "realizable n (ns'@(n''#ns''@[Formal_out (sourcenode a',x')])) n'"
        by(fastforce intro:realizable_Append_matched)
      with ‹set ns ⊆ set ns'› show ?thesis by fastforce
    qed
  next
    case (icsSp_Append_call n ns n'' p n')
    from ‹∃ns'. realizable n ns' n'' ∧ set ns ⊆ set ns'›
    obtain ns' where "realizable n ns' n''" and "set ns ⊆ set ns'" by blast
    from ‹n'' s-p→⇘call⇙ n'› have "valid_SDG_node n'"
      by(rule sum_SDG_edge_valid_SDG_node)
    hence "matched n' [] n'" by(rule matched_Nil)
    with ‹realizable n ns' n''› ‹n'' s-p→⇘call⇙ n'›
    have "realizable n (ns'@n''#[]) n'"
      by(fastforce intro:realizable_call sum_SDG_edge_SDG_edge)
    with ‹set ns ⊆ set ns'› show ?case by fastforce
  next
    case (icsSp_Append_param_in n ns n'' p V n')
    from ‹∃ns'. realizable n ns' n'' ∧ set ns ⊆ set ns'›
    obtain ns' where "realizable n ns' n''" and "set ns ⊆ set ns'" by blast
    from ‹n'' s-p:V→⇘in⇙ n'› have "valid_SDG_node n'"
      by(rule sum_SDG_edge_valid_SDG_node)
    hence "matched n' [] n'" by(rule matched_Nil)
    with ‹realizable n ns' n''› ‹n'' s-p:V→⇘in⇙ n'›
    have "realizable n (ns'@n''#[]) n'"
      by(fastforce intro:realizable_call sum_SDG_edge_SDG_edge)
    with ‹set ns ⊆ set ns'› show ?case by fastforce
  qed
qed



lemma realizable_Append_ics_SDG_path:
  assumes "realizable n ns n''" and "n'' ics-ns'→⇩d* n'"
  obtains ns'' where "realizable n (ns@ns'') n'"
proof(atomize_elim)
  from ‹n'' ics-ns'→⇩d* n'› ‹realizable n ns n''›
  show "∃ns''. realizable n (ns@ns'') n'"
  proof(induct rule:intra_call_sum_SDG_path.induct)
    case (icsSp_Nil n'') thus ?case by(rule_tac x="[]" in exI) fastforce
  next
    case (icsSp_Append_cdep n'' ns' nx n')
    then obtain ns'' where "realizable n (ns@ns'') nx" by fastforce
    from ‹nx s⟶⇘cd⇙ n'› have "valid_SDG_node nx" by(rule sum_SDG_edge_valid_SDG_node)
    hence "matched nx [] nx" by(rule matched_Nil)
    from ‹nx s⟶⇘cd⇙ n'› ‹valid_SDG_node nx›
    have "nx i-[]@[nx]→⇩d* n'" 
      by(fastforce intro:iSp_Append_cdep iSp_Nil sum_SDG_edge_SDG_edge)
    with ‹matched nx [] nx› have "matched nx ([]@[nx]) n'"
      by(fastforce intro:matched_Append_intra_SDG_path)
    with ‹realizable n (ns@ns'') nx› have "realizable n ((ns@ns'')@[nx]) n'"
      by(fastforce intro:realizable_Append_matched)
    thus ?case by fastforce
  next
    case (icsSp_Append_ddep n'' ns' nx V n')
    then obtain ns'' where "realizable n (ns@ns'') nx" by fastforce
    from ‹nx s-V→⇩d⇩d n'› have "valid_SDG_node nx" by(rule sum_SDG_edge_valid_SDG_node)
    hence "matched nx [] nx" by(rule matched_Nil)
    from ‹nx s-V→⇩d⇩d n'› ‹nx ≠ n'› ‹valid_SDG_node nx›
    have "nx i-[]@[nx]→⇩d* n'" 
      by(fastforce intro:iSp_Append_ddep iSp_Nil sum_SDG_edge_SDG_edge)
    with ‹matched nx [] nx› have "matched nx ([]@[nx]) n'"
      by(fastforce intro:matched_Append_intra_SDG_path)
    with ‹realizable n (ns@ns'') nx› have "realizable n ((ns@ns'')@[nx]) n'"
      by(fastforce intro:realizable_Append_matched)
    thus ?case by fastforce
  next
    case (icsSp_Append_sum n'' ns' nx p n')
    then obtain ns'' where "realizable n (ns@ns'') nx" by fastforce
    from ‹nx s-p→⇘sum⇙ n'› obtain nsx where "matched nx nsx n'"
      by -(erule sum_SDG_summary_edge_matched)
    with ‹realizable n (ns@ns'') nx› have "realizable n ((ns@ns'')@nsx) n'"
      by(rule realizable_Append_matched)
    thus ?case by fastforce
  next
    case (icsSp_Append_call n'' ns' nx p n')
    then obtain ns'' where "realizable n (ns@ns'') nx" by fastforce
    from ‹nx s-p→⇘call⇙ n'› have "valid_SDG_node n'" by(rule sum_SDG_edge_valid_SDG_node)
    hence "matched n' [] n'" by(rule matched_Nil)
    with ‹realizable n (ns@ns'') nx› ‹nx s-p→⇘call⇙ n'› 
    have "realizable n ((ns@ns'')@[nx]) n'"
      by(fastforce intro:realizable_call sum_SDG_edge_SDG_edge)
    thus ?case by fastforce
  next
    case (icsSp_Append_param_in n'' ns' nx p V n')
    then obtain ns'' where "realizable n (ns@ns'') nx" by fastforce
    from ‹nx s-p:V→⇘in⇙ n'› have "valid_SDG_node n'"
      by(rule sum_SDG_edge_valid_SDG_node)
    hence "matched n' [] n'" by(rule matched_Nil)
    with ‹realizable n (ns@ns'') nx› ‹nx s-p:V→⇘in⇙ n'› 
    have "realizable n ((ns@ns'')@[nx]) n'"
      by(fastforce intro:realizable_call sum_SDG_edge_SDG_edge)
    thus ?case by fastforce
  qed
qed
      

subsection ‹SDG paths without call edges›

inductive intra_return_sum_SDG_path ::
  "'node SDG_node ⇒ 'node SDG_node list ⇒ 'node SDG_node ⇒ bool"
("_ irs-_→⇩d* _" [51,0,0] 80)
where irsSp_Nil:
  "valid_SDG_node n ⟹ n irs-[]→⇩d* n"

  | irsSp_Cons_cdep:
  "⟦n'' irs-ns→⇩d* n'; n s⟶⇘cd⇙ n''⟧ ⟹ n irs-n#ns→⇩d* n'"

  | irsSp_Cons_ddep:
  "⟦n'' irs-ns→⇩d* n'; n s-V→⇩d⇩d n''; n ≠ n''⟧ ⟹ n irs-n#ns→⇩d* n'"

  | irsSp_Cons_sum:
  "⟦n'' irs-ns→⇩d* n'; n s-p→⇘sum⇙ n''⟧ ⟹ n irs-n#ns→⇩d* n'"

  | irsSp_Cons_return:
  "⟦n'' irs-ns→⇩d* n'; n s-p→⇘ret⇙ n''⟧ ⟹ n irs-n#ns→⇩d* n'"

  | irsSp_Cons_param_out:
  "⟦n'' irs-ns→⇩d* n'; n s-p:V→⇘out⇙ n''⟧ ⟹ n irs-n#ns→⇩d* n'"



lemma irs_SDG_path_Append:
  "⟦n irs-ns→⇩d* n''; n'' irs-ns'→⇩d* n'⟧ ⟹ n irs-ns@ns'→⇩d* n'"
by(induct rule:intra_return_sum_SDG_path.induct,
   auto intro:intra_return_sum_SDG_path.intros)


lemma is_SDG_path_irs_SDG_path:
  "n is-ns→⇩d* n' ⟹ n irs-ns→⇩d* n'"
proof(induct rule:intra_sum_SDG_path.induct)
  case (isSp_Nil n)
  from ‹valid_SDG_node n› show ?case by(rule irsSp_Nil)
next
  case (isSp_Append_cdep n ns n'' n')
  from ‹n'' s⟶⇘cd⇙ n'› have "n'' irs-[n'']→⇩d* n'"
    by(fastforce intro:irsSp_Cons_cdep irsSp_Nil sum_SDG_edge_valid_SDG_node)
  with ‹n irs-ns→⇩d* n''› show ?case by(rule irs_SDG_path_Append)
next
  case (isSp_Append_ddep n ns n'' V n')
  from ‹n'' s-V→⇩d⇩d n'› ‹n'' ≠ n'› have "n'' irs-[n'']→⇩d* n'"
    by(fastforce intro:irsSp_Cons_ddep irsSp_Nil sum_SDG_edge_valid_SDG_node)
  with ‹n irs-ns→⇩d* n''› show ?case by(rule irs_SDG_path_Append)
next
  case (isSp_Append_sum n ns n'' p n')
  from ‹n'' s-p→⇘sum⇙ n'› have "n'' irs-[n'']→⇩d* n'"
    by(fastforce intro:irsSp_Cons_sum irsSp_Nil sum_SDG_edge_valid_SDG_node)
  with ‹n irs-ns→⇩d* n''› show ?case by(rule irs_SDG_path_Append)
qed


lemma irs_SDG_path_split:
  assumes "n irs-ns→⇩d* n'"
  obtains "n is-ns→⇩d* n'"
  | nsx nsx' nx nx' p where "ns = nsx@nx#nsx'" and "n irs-nsx→⇩d* nx"
  and "nx s-p→⇘ret⇙ nx' ∨ (∃V. nx s-p:V→⇘out⇙ nx')" and "nx' is-nsx'→⇩d* n'"
proof(atomize_elim)
  from ‹n irs-ns→⇩d* n'› show "n is-ns→⇩d* n' ∨
    (∃nsx nx nsx' p nx'. ns = nsx@nx#nsx' ∧ n irs-nsx→⇩d* nx ∧ 
                        (nx s-p→⇘ret⇙ nx' ∨ (∃V. nx s-p:V→⇘out⇙ nx')) ∧ nx' is-nsx'→⇩d* n')"
  proof(induct rule:intra_return_sum_SDG_path.induct)
    case (irsSp_Nil n)
    from ‹valid_SDG_node n› have "n is-[]→⇩d* n" by(rule isSp_Nil)
    thus ?case by simp
  next
    case (irsSp_Cons_cdep n'' ns n' n)
    from ‹n'' is-ns→⇩d* n' ∨ 
      (∃nsx nx nsx' p nx'. ns = nsx@nx#nsx' ∧ n'' irs-nsx→⇩d* nx ∧ 
                        (nx s-p→⇘ret⇙ nx' ∨ (∃V. nx s-p:V→⇘out⇙ nx')) ∧ nx' is-nsx'→⇩d* n')›
    show ?case
    proof
      assume "n'' is-ns→⇩d* n'"
      from ‹n s⟶⇘cd⇙ n''› have "n is-[]@[n]→⇩d* n''"
        by(fastforce intro:isSp_Append_cdep isSp_Nil sum_SDG_edge_valid_SDG_node)
      with ‹n'' is-ns→⇩d* n'› have "n is-[n]@ns→⇩d* n'"
        by(fastforce intro:is_SDG_path_Append)
      thus ?case by simp
    next
      assume "∃nsx nx nsx' p nx'. ns = nsx@nx#nsx' ∧ n'' irs-nsx→⇩d* nx ∧ 
                        (nx s-p→⇘ret⇙ nx' ∨ (∃V. nx s-p:V→⇘out⇙ nx')) ∧ nx' is-nsx'→⇩d* n'"
      then obtain nsx nsx' nx nx' p where "ns = nsx@nx#nsx'" and "n'' irs-nsx→⇩d* nx"
        and "nx s-p→⇘ret⇙ nx' ∨ (∃V. nx s-p:V→⇘out⇙ nx')" and "nx' is-nsx'→⇩d* n'" by blast
      from ‹n'' irs-nsx→⇩d* nx› ‹n s⟶⇘cd⇙ n''› have "n irs-n#nsx→⇩d* nx"
        by(rule intra_return_sum_SDG_path.irsSp_Cons_cdep)
      with ‹ns = nsx@nx#nsx'› ‹nx s-p→⇘ret⇙ nx' ∨ (∃V. nx s-p:V→⇘out⇙ nx')›
        ‹nx' is-nsx'→⇩d* n'›
      show ?case by fastforce
    qed
  next
    case (irsSp_Cons_ddep n'' ns n' n V)
    from ‹n'' is-ns→⇩d* n' ∨ 
      (∃nsx nx nsx' p nx'. ns = nsx@nx#nsx' ∧ n'' irs-nsx→⇩d* nx ∧ 
                        (nx s-p→⇘ret⇙ nx' ∨ (∃V. nx s-p:V→⇘out⇙ nx')) ∧ nx' is-nsx'→⇩d* n')›
    show ?case
    proof
      assume "n'' is-ns→⇩d* n'"
      from ‹n s-V→⇩d⇩d n''› ‹n ≠ n''› have "n is-[]@[n]→⇩d* n''"
        by(fastforce intro:isSp_Append_ddep isSp_Nil sum_SDG_edge_valid_SDG_node)
      with ‹n'' is-ns→⇩d* n'› have "n is-[n]@ns→⇩d* n'"
        by(fastforce intro:is_SDG_path_Append)
      thus ?case by simp
    next
      assume "∃nsx nx nsx' p nx'.  ns = nsx@nx#nsx' ∧ n'' irs-nsx→⇩d* nx ∧ 
                        (nx s-p→⇘ret⇙ nx' ∨ (∃V. nx s-p:V→⇘out⇙ nx')) ∧ nx' is-nsx'→⇩d* n'"
      then obtain nsx nsx' nx nx' p where "ns = nsx@nx#nsx'" and "n'' irs-nsx→⇩d* nx"
        and "nx s-p→⇘ret⇙ nx' ∨ (∃V. nx s-p:V→⇘out⇙ nx')" and "nx' is-nsx'→⇩d* n'" by blast
      from ‹n'' irs-nsx→⇩d* nx› ‹n s-V→⇩d⇩d n''› ‹n ≠ n''› have "n irs-n#nsx→⇩d* nx"
        by(rule intra_return_sum_SDG_path.irsSp_Cons_ddep)
      with ‹ns = nsx@nx#nsx'› ‹nx s-p→⇘ret⇙ nx' ∨ (∃V. nx s-p:V→⇘out⇙ nx')›
        ‹nx' is-nsx'→⇩d* n'›
      show ?case by fastforce
    qed
  next
    case (irsSp_Cons_sum n'' ns n' n p)
    from ‹n'' is-ns→⇩d* n' ∨ 
      (∃nsx nx nsx' p nx'. ns = nsx@nx#nsx' ∧ n'' irs-nsx→⇩d* nx ∧ 
                        (nx s-p→⇘ret⇙ nx' ∨ (∃V. nx s-p:V→⇘out⇙ nx')) ∧ nx' is-nsx'→⇩d* n')›
    show ?case
    proof
      assume "n'' is-ns→⇩d* n'"
      from ‹n s-p→⇘sum⇙ n''› have "n is-[]@[n]→⇩d* n''"
        by(fastforce intro:isSp_Append_sum isSp_Nil sum_SDG_edge_valid_SDG_node)
      with ‹n'' is-ns→⇩d* n'› have "n is-[n]@ns→⇩d* n'"
        by(fastforce intro:is_SDG_path_Append)
      thus ?case by simp
    next
      assume "∃nsx nx nsx' p nx'. ns = nsx@nx#nsx' ∧ n'' irs-nsx→⇩d* nx ∧ 
                        (nx s-p→⇘ret⇙ nx' ∨ (∃V. nx s-p:V→⇘out⇙ nx')) ∧ nx' is-nsx'→⇩d* n'"
      then obtain nsx nsx' nx nx' p' where "ns = nsx@nx#nsx'" and "n'' irs-nsx→⇩d* nx"
        and "nx s-p'→⇘ret⇙ nx' ∨ (∃V. nx s-p':V→⇘out⇙ nx')" 
        and "nx' is-nsx'→⇩d* n'" by blast
      from ‹n'' irs-nsx→⇩d* nx› ‹n s-p→⇘sum⇙ n''› have "n irs-n#nsx→⇩d* nx"
        by(rule intra_return_sum_SDG_path.irsSp_Cons_sum)
      with ‹ns = nsx@nx#nsx'› ‹nx s-p'→⇘ret⇙ nx' ∨ (∃V. nx s-p':V→⇘out⇙ nx')›
        ‹nx' is-nsx'→⇩d* n'›
      show ?case by fastforce
    qed
  next
    case (irsSp_Cons_return n'' ns n' n p)
    from ‹n'' is-ns→⇩d* n' ∨ 
      (∃nsx nx nsx' p nx'. ns = nsx@nx#nsx' ∧ n'' irs-nsx→⇩d* nx ∧ 
                        (nx s-p→⇘ret⇙ nx' ∨ (∃V. nx s-p:V→⇘out⇙ nx')) ∧ nx' is-nsx'→⇩d* n')›
    show ?case
    proof
      assume "n'' is-ns→⇩d* n'"
      from ‹n s-p→⇘ret⇙ n''› have "valid_SDG_node n" by(rule sum_SDG_edge_valid_SDG_node)
      hence "n irs-[]→⇩d* n" by(rule irsSp_Nil)
      with ‹n s-p→⇘ret⇙ n''› ‹n'' is-ns→⇩d* n'› show ?thesis by fastforce
    next
      assume "∃nsx nx nsx' p nx'. ns = nsx@nx#nsx' ∧ n'' irs-nsx→⇩d* nx ∧ 
                        (nx s-p→⇘ret⇙ nx' ∨ (∃V. nx s-p:V→⇘out⇙ nx')) ∧ nx' is-nsx'→⇩d* n'"
      then obtain nsx nsx' nx nx' p' where "ns = nsx@nx#nsx'" and "n'' irs-nsx→⇩d* nx"
        and "nx s-p'→⇘ret⇙ nx' ∨ (∃V. nx s-p':V→⇘out⇙ nx')"
        and "nx' is-nsx'→⇩d* n'" by blast
      from ‹n'' irs-nsx→⇩d* nx› ‹n s-p→⇘ret⇙ n''› have "n irs-n#nsx→⇩d* nx"
        by(rule intra_return_sum_SDG_path.irsSp_Cons_return)
      with ‹ns = nsx@nx#nsx'› ‹nx s-p'→⇘ret⇙ nx' ∨ (∃V. nx s-p':V→⇘out⇙ nx')›
        ‹nx' is-nsx'→⇩d* n'›
      show ?thesis by fastforce
    qed
  next
    case (irsSp_Cons_param_out n'' ns n' n p V)
    from ‹n'' is-ns→⇩d* n' ∨ 
      (∃nsx nx nsx' p nx'. ns = nsx@nx#nsx' ∧ n'' irs-nsx→⇩d* nx ∧ 
                        (nx s-p→⇘ret⇙ nx' ∨ (∃V. nx s-p:V→⇘out⇙ nx')) ∧ nx' is-nsx'→⇩d* n')›
    show ?case
    proof
      assume "n'' is-ns→⇩d* n'"
      from ‹n s-p:V→⇘out⇙ n''› have "valid_SDG_node n"
        by(rule sum_SDG_edge_valid_SDG_node)
      hence "n irs-[]→⇩d* n" by(rule irsSp_Nil)
      with ‹n s-p:V→⇘out⇙ n''› ‹n'' is-ns→⇩d* n'› show ?thesis by fastforce
    next
      assume "∃nsx nx nsx' p nx'. ns = nsx@nx#nsx' ∧ n'' irs-nsx→⇩d* nx ∧ 
                        (nx s-p→⇘ret⇙ nx' ∨ (∃V. nx s-p:V→⇘out⇙ nx')) ∧ nx' is-nsx'→⇩d* n'"
      then obtain nsx nsx' nx nx' p' where "ns = nsx@nx#nsx'" and "n'' irs-nsx→⇩d* nx"
        and "nx s-p'→⇘ret⇙ nx' ∨ (∃V. nx s-p':V→⇘out⇙ nx')" 
        and "nx' is-nsx'→⇩d* n'" by blast
      from ‹n'' irs-nsx→⇩d* nx› ‹n s-p:V→⇘out⇙ n''› have "n irs-n#nsx→⇩d* nx"
        by(rule intra_return_sum_SDG_path.irsSp_Cons_param_out)
      with ‹ns = nsx@nx#nsx'› ‹nx s-p'→⇘ret⇙ nx' ∨ (∃V. nx s-p':V→⇘out⇙ nx')›
        ‹nx' is-nsx'→⇩d* n'›
      show ?thesis by fastforce
    qed
  qed
qed


lemma irs_SDG_path_matched:
  assumes "n irs-ns→⇩d* n''" and "n'' s-p→⇘ret⇙ n' ∨ n'' s-p:V→⇘out⇙ n'"
  obtains nx nsx where "matched nx nsx n'" and "n ∈ set nsx" 
  and "nx s-p→⇘sum⇙ CFG_node (parent_node n')"
proof(atomize_elim)
  from assms
  show "∃nx nsx. matched nx nsx n' ∧ n ∈ set nsx ∧ 
                 nx s-p→⇘sum⇙ CFG_node (parent_node n')"
  proof(induct ns arbitrary:n'' n' p V rule:length_induct)
    fix ns n'' n' p V
    assume IH:"∀ns'. length ns' < length ns ⟶
      (∀n''. n irs-ns'→⇩d* n'' ⟶ 
      (∀nx' p' V'. (n'' s-p'→⇘ret⇙ nx' ∨ n'' s-p':V'→⇘out⇙ nx') ⟶ 
        (∃nx nsx. matched nx nsx nx' ∧ n ∈ set nsx ∧ 
                  nx s-p'→⇘sum⇙ CFG_node (parent_node nx'))))"
      and "n irs-ns→⇩d* n''" and "n'' s-p→⇘ret⇙ n' ∨ n'' s-p:V→⇘out⇙ n'"
    from ‹n'' s-p→⇘ret⇙ n' ∨ n'' s-p:V→⇘out⇙ n'› have "valid_SDG_node n''"
      by(fastforce intro:sum_SDG_edge_valid_SDG_node)
    from ‹n'' s-p→⇘ret⇙ n' ∨ n'' s-p:V→⇘out⇙ n'›
    have "n'' -p→⇘ret⇙ n' ∨ n'' -p:V→⇘out⇙ n'"
      by(fastforce intro:sum_SDG_edge_SDG_edge SDG_edge_sum_SDG_edge)
    from ‹n'' s-p→⇘ret⇙ n' ∨ n'' s-p:V→⇘out⇙ n'›
    have "CFG_node (parent_node n'') s-p→⇘ret⇙ CFG_node (parent_node n')"
      by(fastforce elim:sum_SDG_edge.cases intro:sum_SDG_return_edge)
    then obtain a Q f where "valid_edge a" and "kind a = Q↩⇘p⇙f"
      and "parent_node n'' = sourcenode a" and "parent_node n' = targetnode a"
      by(fastforce elim:sum_SDG_edge.cases)
    from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› obtain a' Q' r' fs' 
      where "a ∈ get_return_edges a'" and "valid_edge a'" and "kind a' = Q':r'↪⇘p⇙fs'"
      and "CFG_node (sourcenode a') s-p→⇘sum⇙ CFG_node (targetnode a)"
      by(erule return_edge_determines_call_and_sum_edge)
    from ‹valid_edge a'› ‹kind a' = Q':r'↪⇘p⇙fs'›
    have "CFG_node (sourcenode a') s-p→⇘call⇙ CFG_node (targetnode a')"
      by(fastforce intro:sum_SDG_call_edge)
    from ‹CFG_node (parent_node n'') s-p→⇘ret⇙ CFG_node (parent_node n')› 
    have "get_proc (parent_node n'') = p"
      by(auto elim!:sum_SDG_edge.cases intro:get_proc_return)
    from ‹n irs-ns→⇩d* n''›
    show "∃nx nsx. matched nx nsx n' ∧ n ∈ set nsx ∧ 
                   nx s-p→⇘sum⇙ CFG_node (parent_node n')"
    proof(rule irs_SDG_path_split)
      assume "n is-ns→⇩d* n''"
      hence "valid_SDG_node n" by(rule is_SDG_path_valid_SDG_node)
      then obtain asx where "(_Entry_) -asx→⇩√* parent_node n"
        by(fastforce dest:valid_SDG_CFG_node Entry_path)
      then obtain asx' where "(_Entry_) -asx'→⇩√* parent_node n"
        and "∀a' ∈ set asx'. intra_kind(kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)"
        by -(erule valid_Entry_path_ascending_path)
      from ‹n is-ns→⇩d* n''› obtain as where "parent_node n -as→⇩ι* parent_node n''"
        by(erule is_SDG_path_CFG_path)
      hence "get_proc (parent_node n) = get_proc (parent_node n'')"
        by(rule intra_path_get_procs)
      from ‹valid_SDG_node n› have "valid_node (parent_node n)"
        by(rule valid_SDG_CFG_node)
      hence "valid_SDG_node (CFG_node (parent_node n))" by simp
      have "∃a as. valid_edge a ∧ (∃Q p r fs. kind a = Q:r↪⇘p⇙fs) ∧
        targetnode a -as→⇩ι* parent_node n"
      proof(cases "∀a' ∈ set asx'. intra_kind(kind a')")
        case True
        with ‹(_Entry_) -asx'→⇩√* parent_node n›
        have "(_Entry_) -asx'→⇩ι* parent_node n"
          by(fastforce simp:intra_path_def vp_def)
        hence "get_proc (_Entry_) = get_proc (parent_node n)"
          by(rule intra_path_get_procs)
        with get_proc_Entry have "get_proc (parent_node n) = Main" by simp
        from ‹get_proc (parent_node n) = get_proc (parent_node n'')›
          ‹get_proc (parent_node n) = Main› 
        have "get_proc (parent_node n'') = Main" by simp
        from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› have "get_proc (sourcenode a) = p"
          by(rule get_proc_return)
        with ‹parent_node n'' = sourcenode a› ‹get_proc (parent_node n'') = Main›
        have "p = Main" by simp
        with ‹kind a = Q↩⇘p⇙f› have "kind a = Q↩⇘Main⇙f" by simp
        with ‹valid_edge a› have False by(rule Main_no_return_source)
        thus ?thesis by simp
      next
        assume "¬ (∀a'∈set asx'. intra_kind (kind a'))"
        with ‹∀a' ∈ set asx'. intra_kind(kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)›
        have "∃a' ∈ set asx'. ∃Q r p fs. kind a' = Q:r↪⇘p⇙fs" 
          by(fastforce simp:intra_kind_def)
        then obtain as a' as' where "asx' = as@a'#as'" 
          and "∃Q r p fs. kind a' = Q:r↪⇘p⇙fs"
          and "∀a' ∈ set as'. ¬ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)"
          by(erule split_list_last_propE)
        with ‹∀a' ∈ set asx'. intra_kind(kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)›
        have "∀a'∈set as'. intra_kind (kind a')" by(auto simp:intra_kind_def)
        from ‹(_Entry_) -asx'→⇩√* parent_node n› ‹asx' = as@a'#as'›
        have "valid_edge a'" and "targetnode a' -as'→* parent_node n"
          by(auto dest:path_split simp:vp_def)
        with ‹∀a'∈set as'. intra_kind (kind a')› ‹∃Q r p fs. kind a' = Q:r↪⇘p⇙fs›
        show ?thesis by(fastforce simp:intra_path_def)
      qed
      then obtain ax asx Qx rx fsx px where "valid_edge ax"
        and "kind ax = Qx:rx↪⇘px⇙fsx" and "targetnode ax -asx→⇩ι* parent_node n"
        by blast
      from ‹valid_edge ax› ‹kind ax = Qx:rx↪⇘px⇙fsx› 
      have "get_proc (targetnode ax) = px"
        by(rule get_proc_call)
      from ‹targetnode ax -asx→⇩ι* parent_node n› 
      have "get_proc (targetnode ax) = get_proc (parent_node n)" 
        by(rule intra_path_get_procs)
      with ‹get_proc (parent_node n) = get_proc (parent_node n'')› 
        ‹get_proc (targetnode ax) = px›
      have "get_proc (parent_node n'') = px" by simp
      with ‹get_proc (parent_node n'') = p› have [simp]:"px = p" by simp
      from ‹valid_edge a'› ‹valid_edge ax› ‹kind a' = Q':r'↪⇘p⇙fs'›
        ‹kind ax = Qx:rx↪⇘px⇙fsx›
      have "targetnode a' = targetnode ax" by simp(rule same_proc_call_unique_target)
      have "parent_node n ≠ (_Exit_)"
      proof
        assume "parent_node n = (_Exit_)"
        from ‹n is-ns→⇩d* n''› obtain as where "parent_node n -as→⇩ι* parent_node n''"
          by(erule is_SDG_path_CFG_path)
        with ‹parent_node n = (_Exit_)›
        have "(_Exit_) -as→* parent_node n''" by(simp add:intra_path_def)
        hence "parent_node n'' = (_Exit_)" by(fastforce dest:path_Exit_source)
        from ‹get_proc (parent_node n'') = p› ‹parent_node n'' = (_Exit_)›
          ‹parent_node n'' = sourcenode a› get_proc_Exit 
        have "p = Main" by simp
        with ‹kind a = Q↩⇘p⇙f› have "kind a = Q↩⇘Main⇙f" by simp
        with ‹valid_edge a› show False by(rule Main_no_return_source)
      qed
      have "∃nsx. CFG_node (targetnode a') cd-nsx→⇩d* CFG_node (parent_node n)"
      proof(cases "targetnode a' = parent_node n")
        case True
        with ‹valid_SDG_node (CFG_node (parent_node n))› 
        have "CFG_node (targetnode a') cd-[]→⇩d* CFG_node (parent_node n)"
          by(fastforce intro:cdSp_Nil)
        thus ?thesis by blast
      next
        case False
        with ‹targetnode ax -asx→⇩ι* parent_node n› ‹parent_node n ≠ (_Exit_)›
          ‹valid_edge ax› ‹kind ax = Qx:rx↪⇘px⇙fsx› ‹targetnode a' = targetnode ax›
        obtain nsx 
          where "CFG_node (targetnode a') cd-nsx→⇩d* CFG_node (parent_node n)"
          by(fastforce elim!:in_proc_cdep_SDG_path)
        thus ?thesis by blast
      qed
      then obtain nsx 
        where "CFG_node (targetnode a') cd-nsx→⇩d* CFG_node (parent_node n)" by blast
      hence "CFG_node (targetnode a') i-nsx→⇩d* CFG_node (parent_node n)"
        by(rule cdep_SDG_path_intra_SDG_path)
      show ?thesis
      proof(cases ns)
        case Nil
        with ‹n is-ns→⇩d* n''› have "n = n''"
          by(fastforce elim:intra_sum_SDG_path.cases)
        from ‹valid_edge a'› ‹kind a' = Q':r'↪⇘p⇙fs'› ‹a ∈ get_return_edges a'›
        have "matched (CFG_node (targetnode a')) [CFG_node (targetnode a')]
          (CFG_node (sourcenode a))" by(rule intra_proc_matched)
        from ‹valid_SDG_node n''›
        have "n'' = CFG_node (parent_node n'') ∨ CFG_node (parent_node n'') ⟶⇘cd⇙ n''"
          by(rule valid_SDG_node_cases)
        hence "∃nsx. CFG_node (parent_node n'') i-nsx→⇩d* n''"
        proof
          assume "n'' = CFG_node (parent_node n'')"
          with ‹valid_SDG_node n''› have "CFG_node (parent_node n'') i-[]→⇩d* n''"
            by(fastforce intro:iSp_Nil)
          thus ?thesis by blast
        next
          assume "CFG_node (parent_node n'') ⟶⇘cd⇙ n''"
          from ‹valid_SDG_node n''› have "valid_node (parent_node n'')"
            by(rule valid_SDG_CFG_node)
          hence "valid_SDG_node (CFG_node (parent_node n''))" by simp
          hence "CFG_node (parent_node n'') i-[]→⇩d* CFG_node (parent_node n'')"
            by(rule iSp_Nil)
          with ‹CFG_node (parent_node n'') ⟶⇘cd⇙ n''›
          have "CFG_node (parent_node n'') i-[]@[CFG_node (parent_node n'')]→⇩d* n''"
            by(fastforce intro:iSp_Append_cdep sum_SDG_edge_SDG_edge)
          thus ?thesis by blast
        qed
        with ‹parent_node n'' = sourcenode a›
        obtain nsx where "CFG_node (sourcenode a) i-nsx→⇩d* n''" by fastforce
        with ‹matched (CFG_node (targetnode a')) [CFG_node (targetnode a')]
          (CFG_node (sourcenode a))›
        have "matched (CFG_node (targetnode a')) ([CFG_node (targetnode a')]@nsx) n''"
          by(fastforce intro:matched_Append intra_SDG_path_matched)
        moreover
        from ‹valid_edge a'› ‹kind a' = Q':r'↪⇘p⇙fs'›
        have "CFG_node (sourcenode a') -p→⇘call⇙ CFG_node (targetnode a')"
          by(fastforce intro:SDG_call_edge)
        moreover
        from ‹valid_edge a'› have "valid_SDG_node (CFG_node (sourcenode a'))"
          by simp
        hence "matched (CFG_node (sourcenode a')) [] (CFG_node (sourcenode a'))"
          by(rule matched_Nil)
        ultimately have "matched (CFG_node (sourcenode a'))
          ([]@(CFG_node (sourcenode a'))#([CFG_node (targetnode a')]@nsx)@[n'']) n'"
          using ‹n'' s-p→⇘ret⇙ n' ∨ n'' s-p:V→⇘out⇙ n'› ‹parent_node n' = targetnode a›
            ‹parent_node n'' = sourcenode a› ‹valid_edge a'› ‹a ∈ get_return_edges a'›
          by(fastforce intro:matched_bracket_call dest:sum_SDG_edge_SDG_edge)
        with ‹n = n''› ‹CFG_node (sourcenode a') s-p→⇘sum⇙ CFG_node (targetnode a)›
          ‹parent_node n' = targetnode a›
        show ?thesis by fastforce
      next
        case Cons
        with ‹n is-ns→⇩d* n''› have "n ∈ set ns"
          by(induct rule:intra_sum_SDG_path_rev_induct) auto
        from ‹n is-ns→⇩d* n''› obtain ns' where "matched n ns' n''" 
          and "set ns ⊆ set ns'" by(erule is_SDG_path_matched)
        with ‹n ∈ set ns› have "n ∈ set ns'" by fastforce
        from ‹valid_SDG_node n›
        have "n = CFG_node (parent_node n) ∨ CFG_node (parent_node n) ⟶⇘cd⇙ n"
          by(rule valid_SDG_node_cases)
        hence "∃nsx. CFG_node (parent_node n) i-nsx→⇩d* n"
        proof
          assume "n = CFG_node (parent_node n)"
          with ‹valid_SDG_node n› have "CFG_node (parent_node n) i-[]→⇩d* n"
            by(fastforce intro:iSp_Nil)
          thus ?thesis by blast
        next
          assume "CFG_node (parent_node n) ⟶⇘cd⇙ n"
          from ‹valid_SDG_node (CFG_node (parent_node n))› 
          have "CFG_node (parent_node n) i-[]→⇩d* CFG_node (parent_node n)"
            by(rule iSp_Nil)
          with ‹CFG_node (parent_node n) ⟶⇘cd⇙ n›
          have "CFG_node (parent_node n) i-[]@[CFG_node (parent_node n)]→⇩d* n"
            by(fastforce intro:iSp_Append_cdep sum_SDG_edge_SDG_edge)
          thus ?thesis by blast
        qed
        then obtain nsx' where "CFG_node (parent_node n) i-nsx'→⇩d* n" by blast
        with ‹CFG_node (targetnode a') i-nsx→⇩d* CFG_node (parent_node n)›
        have "CFG_node (targetnode a') i-nsx@nsx'→⇩d* n"
          by -(rule intra_SDG_path_Append)
        hence "matched (CFG_node (targetnode a')) (nsx@nsx') n"
          by(rule intra_SDG_path_matched)
        with ‹matched n ns' n''› 
        have "matched (CFG_node (targetnode a')) ((nsx@nsx')@ns') n''"
          by(rule matched_Append)
        moreover
        from ‹valid_edge a'› ‹kind a' = Q':r'↪⇘p⇙fs'›
        have "CFG_node (sourcenode a') -p→⇘call⇙ CFG_node (targetnode a')"
          by(fastforce intro:SDG_call_edge)
        moreover
        from ‹valid_edge a'› have "valid_SDG_node (CFG_node (sourcenode a'))"
          by simp
        hence "matched (CFG_node (sourcenode a')) [] (CFG_node (sourcenode a'))"
          by(rule matched_Nil)
        ultimately have "matched (CFG_node (sourcenode a')) 
          ([]@(CFG_node (sourcenode a'))#((nsx@nsx')@ns')@[n'']) n'"
          using  ‹n'' s-p→⇘ret⇙ n' ∨ n'' s-p:V→⇘out⇙ n'› ‹parent_node n' = targetnode a›
            ‹parent_node n'' = sourcenode a› ‹valid_edge a'› ‹a ∈ get_return_edges a'›
          by(fastforce intro:matched_bracket_call dest:sum_SDG_edge_SDG_edge)
        with ‹CFG_node (sourcenode a') s-p→⇘sum⇙ CFG_node (targetnode a)›
          ‹parent_node n' = targetnode a› ‹n ∈ set ns'›
        show ?thesis by fastforce
      qed
    next
      fix ms ms' m m' px
      assume "ns = ms@m#ms'" and "n irs-ms→⇩d* m"
        and "m s-px→⇘ret⇙ m' ∨ (∃V. m s-px:V→⇘out⇙ m')" and "m' is-ms'→⇩d* n''"
      from ‹ns = ms@m#ms'› have "length ms < length ns" by simp
      with IH ‹n irs-ms→⇩d* m› ‹m s-px→⇘ret⇙ m' ∨ (∃V. m s-px:V→⇘out⇙ m')› obtain mx msx
        where "matched mx msx m'" and "n ∈ set msx" 
        and "mx s-px→⇘sum⇙ CFG_node (parent_node m')" by fastforce
      from ‹m' is-ms'→⇩d* n''› obtain msx' where "matched m' msx' n''"
        by -(erule is_SDG_path_matched)
      with ‹matched mx msx m'› have "matched mx (msx@msx') n''"
        by -(rule matched_Append)
      from ‹m s-px→⇘ret⇙ m' ∨ (∃V. m s-px:V→⇘out⇙ m')›
      have "m -px→⇘ret⇙ m' ∨ (∃V. m -px:V→⇘out⇙ m')"
        by(auto intro:sum_SDG_edge_SDG_edge SDG_edge_sum_SDG_edge)
      from ‹m s-px→⇘ret⇙ m' ∨ (∃V. m s-px:V→⇘out⇙ m')›
      have "CFG_node (parent_node m) s-px→⇘ret⇙ CFG_node (parent_node m')"
        by(fastforce elim:sum_SDG_edge.cases intro:sum_SDG_return_edge)
      then obtain ax Qx fx where "valid_edge ax" and "kind ax = Qx↩⇘px⇙fx"
      and "parent_node m = sourcenode ax" and "parent_node m' = targetnode ax"
        by(fastforce elim:sum_SDG_edge.cases)
      from ‹valid_edge ax› ‹kind ax = Qx↩⇘px⇙fx› obtain ax' Qx' rx' fsx' 
        where "ax ∈ get_return_edges ax'" and "valid_edge ax'" 
        and "kind ax' = Qx':rx'↪⇘px⇙fsx'"
        and "CFG_node (sourcenode ax') s-px→⇘sum⇙ CFG_node (targetnode ax)"
        by(erule return_edge_determines_call_and_sum_edge)
      from ‹valid_edge ax'› ‹kind ax' = Qx':rx'↪⇘px⇙fsx'›
      have "CFG_node (sourcenode ax') s-px→⇘call⇙ CFG_node (targetnode ax')"
        by(fastforce intro:sum_SDG_call_edge)
      from ‹mx s-px→⇘sum⇙ CFG_node (parent_node m')›
      have "valid_SDG_node mx" by(rule sum_SDG_edge_valid_SDG_node)
      have "∃msx''. CFG_node (targetnode a') cd-msx''→⇩d* mx"
      proof(cases "targetnode a' = parent_node mx")
        case True
        from ‹valid_SDG_node mx› 
        have "mx = CFG_node (parent_node mx) ∨ CFG_node (parent_node mx) ⟶⇘cd⇙ mx"
          by(rule valid_SDG_node_cases)
        thus ?thesis
        proof
          assume "mx = CFG_node (parent_node mx)"
          with ‹valid_SDG_node mx› True
          have "CFG_node (targetnode a') cd-[]→⇩d* mx" by(fastforce intro:cdSp_Nil)
          thus ?thesis by blast
        next
          assume "CFG_node (parent_node mx) ⟶⇘cd⇙ mx"
          with ‹valid_edge a'› True[THEN sym]
          have "CFG_node (targetnode a') cd-[]@[CFG_node (targetnode a')]→⇩d* mx"
            by(fastforce intro:cdep_SDG_path.intros)
          thus ?thesis by blast
        qed
      next
        case False
        show ?thesis
        proof(cases "∀ai. valid_edge ai ∧ sourcenode ai = parent_node mx
            ⟶ ai ∉ get_return_edges a'")
          case True
          { assume "parent_node mx = (_Exit_)"
            with ‹mx s-px→⇘sum⇙ CFG_node (parent_node m')›
            obtain ai where "valid_edge ai" and "sourcenode ai = (_Exit_)"
              by -(erule sum_SDG_edge.cases,auto)
            hence False by(rule Exit_source) }
          hence "parent_node mx ≠ (_Exit_)" by fastforce
          from ‹valid_SDG_node mx› have "valid_node (parent_node mx)"
            by(rule valid_SDG_CFG_node)
          then obtain asx where "(_Entry_) -asx→⇩√* parent_node mx"
            by(fastforce intro:Entry_path)
          then obtain asx' where "(_Entry_) -asx'→⇩√* parent_node mx"
            and "∀a' ∈ set asx'. intra_kind(kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)"
            by -(erule valid_Entry_path_ascending_path)
          from ‹mx s-px→⇘sum⇙ CFG_node (parent_node m')›
          obtain nsi where "matched mx nsi (CFG_node (parent_node m'))"
            by -(erule sum_SDG_summary_edge_matched)
          then obtain asi where "parent_node mx -asi→⇘sl⇙* parent_node m'"
            by(fastforce elim:matched_same_level_CFG_path)
          hence "get_proc (parent_node mx) = get_proc (parent_node m')"
            by(rule slp_get_proc)
          from ‹m' is-ms'→⇩d* n''› obtain nsi' where "matched m' nsi' n''"
            by -(erule is_SDG_path_matched)
          then obtain asi' where "parent_node m' -asi'→⇘sl⇙* parent_node n''"
            by -(erule matched_same_level_CFG_path)
          hence "get_proc (parent_node m') = get_proc (parent_node n'')"
            by(rule slp_get_proc)
          with ‹get_proc (parent_node mx) = get_proc (parent_node m')›
          have "get_proc (parent_node mx) = get_proc (parent_node n'')" by simp
          from ‹get_proc (parent_node n'') = p› 
            ‹get_proc (parent_node mx) = get_proc (parent_node n'')›
          have "get_proc (parent_node mx) = p" by simp
          have "∃asx. targetnode a' -asx→⇩ι* parent_node mx"
          proof(cases "∀a' ∈ set asx'. intra_kind(kind a')")
            case True
            with ‹(_Entry_) -asx'→⇩√* parent_node mx› 
            have "(_Entry_) -asx'→⇩ι* parent_node mx"
              by(simp add:vp_def intra_path_def)
            hence "get_proc (_Entry_) = get_proc (parent_node mx)"
              by(rule intra_path_get_procs)
            with ‹get_proc (parent_node mx) = p› have "get_proc (_Entry_) = p"
              by simp
            with ‹CFG_node (parent_node n'') s-p→⇘ret⇙ CFG_node (parent_node n')›
            have False
              by -(erule sum_SDG_edge.cases,
                auto intro:Main_no_return_source simp:get_proc_Entry)
            thus ?thesis by simp
          next
            case False
            hence "∃a' ∈ set asx'. ¬ intra_kind (kind a')" by fastforce
            then obtain ai as' as'' where "asx' = as'@ai#as''" 
              and "¬ intra_kind (kind ai)" and "∀a' ∈ set as''. intra_kind (kind a')"
              by(fastforce elim!:split_list_last_propE)
            from ‹asx' = as'@ai#as''› ‹¬ intra_kind (kind ai)›
              ‹∀a' ∈ set asx'. intra_kind(kind a') ∨ (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)›
            obtain Qi ri pi fsi where "kind ai = Qi:ri↪⇘pi⇙fsi" 
              and "∀a' ∈ set as'. intra_kind(kind a') ∨ 
              (∃Q r p fs. kind a' = Q:r↪⇘p⇙fs)"
              by auto
            from ‹(_Entry_) -asx'→⇩√* parent_node mx› ‹asx' = as'@ai#as''›
              ‹∀a' ∈ set as''. intra_kind (kind a')›
            have "valid_edge ai" and "targetnode ai -as''→⇩ι* parent_node mx"
              by(auto intro:path_split simp:vp_def intra_path_def)
            hence "get_proc (targetnode ai) = get_proc (parent_node mx)"
              by -(rule intra_path_get_procs)
            with ‹get_proc (parent_node mx) = p› ‹valid_edge ai›
              ‹kind ai = Qi:ri↪⇘pi⇙fsi›
            have [simp]:"pi = p" by(fastforce dest:get_proc_call)
            from ‹valid_edge ai› ‹valid_edge a'› 
              ‹kind ai = Qi:ri↪⇘pi⇙fsi› ‹kind a' = Q':r'↪⇘p⇙fs'›
            have "targetnode ai = targetnode a'" 
              by(fastforce intro:same_proc_call_unique_target)
            with ‹targetnode ai -as''→⇩ι* parent_node mx›
            show ?thesis by fastforce
          qed
          then obtain asx where "targetnode a' -asx→⇩ι* parent_node mx" by blast
          from this ‹valid_edge a'› ‹kind a' = Q':r'↪⇘p⇙fs'›
            ‹parent_node mx ≠ (_Exit_)› ‹targetnode a' ≠ parent_node mx› True
          obtain msi 
            where "CFG_node(targetnode a') cd-msi→⇩d* CFG_node(parent_node mx)"
            by(fastforce elim!:in_proc_cdep_SDG_path)
          from ‹valid_SDG_node mx› 
          have "mx = CFG_node (parent_node mx) ∨ CFG_node (parent_node mx) ⟶⇘cd⇙ mx"
            by(rule valid_SDG_node_cases)
          thus ?thesis
          proof
            assume "mx = CFG_node (parent_node mx)"
            with ‹CFG_node(targetnode a')cd-msi→⇩d* CFG_node(parent_node mx)›
            show ?thesis by fastforce
          next
            assume "CFG_node (parent_node mx) ⟶⇘cd⇙ mx"
            with ‹CFG_node(targetnode a')cd-msi→⇩d* CFG_node(parent_node mx)›
            have "CFG_node(targetnode a') cd-msi@[CFG_node(parent_node mx)]→⇩d* mx"
              by(fastforce intro:cdSp_Append_cdep)
            thus ?thesis by fastforce
          qed
        next
          case False
          then obtain ai where "valid_edge ai" and "sourcenode ai = parent_node mx"
            and "ai ∈ get_return_edges a'" by blast
          with ‹valid_edge a'› ‹kind a' = Q':r'↪⇘p⇙fs'›
          have "CFG_node (targetnode a') ⟶⇘cd⇙ CFG_node (parent_node mx)"
            by(auto intro:SDG_proc_entry_exit_cdep)       
          with ‹valid_edge a'› 
          have cd_path:"CFG_node (targetnode a') cd-[]@[CFG_node (targetnode a')]→⇩d* 
                        CFG_node (parent_node mx)"
            by(fastforce intro:cdSp_Append_cdep cdSp_Nil)
          from ‹valid_SDG_node mx› 
          have "mx = CFG_node (parent_node mx) ∨ CFG_node (parent_node mx) ⟶⇘cd⇙ mx"
            by(rule valid_SDG_node_cases)
          thus ?thesis
          proof
            assume "mx = CFG_node (parent_node mx)"
            with cd_path show ?thesis by fastforce
          next
            assume "CFG_node (parent_node mx) ⟶⇘cd⇙ mx"
            with cd_path have "CFG_node (targetnode a') 
              cd-[CFG_node (targetnode a')]@[CFG_node (parent_node mx)]→⇩d* mx"
              by(fastforce intro:cdSp_Append_cdep)
            thus ?thesis by fastforce
          qed
        qed
      qed
      then obtain msx'' 
        where "CFG_node (targetnode a') cd-msx''→⇩d* mx" by blast
      hence "CFG_node (targetnode a') i-msx''→⇩d* mx"
        by(rule cdep_SDG_path_intra_SDG_path)
      with ‹valid_edge a'› 
      have "matched (CFG_node (targetnode a')) ([]@msx'') mx"
        by(fastforce intro:matched_Append_intra_SDG_path matched_Nil)
      with ‹matched mx (msx@msx') n''›
      have "matched (CFG_node (targetnode a')) (msx''@(msx@msx')) n''"
        by(fastforce intro:matched_Append)
      with ‹valid_edge a'› ‹CFG_node (sourcenode a') s-p→⇘call⇙ CFG_node (targetnode a')›
        ‹n'' -p→⇘ret⇙ n' ∨ n'' -p:V→⇘out⇙ n'› ‹a ∈ get_return_edges a'›
        ‹parent_node n'' = sourcenode a› ‹parent_node n' = targetnode a›
      have "matched (CFG_node (sourcenode a')) 
        ([]@CFG_node (sourcenode a')#(msx''@(msx@msx'))@[n'']) n'"
        by(fastforce intro:matched_bracket_call matched_Nil sum_SDG_edge_SDG_edge)
      with ‹n ∈ set msx› ‹CFG_node (sourcenode a') s-p→⇘sum⇙ CFG_node (targetnode a)›
        ‹parent_node n' = targetnode a›
      show ?thesis by fastforce
    qed
  qed
qed


lemma irs_SDG_path_realizable:
  assumes "n irs-ns→⇩d* n'" and "n ≠ n'"
  obtains ns' where "realizable (CFG_node (_Entry_)) ns' n'" and "n ∈ set ns'"
proof(atomize_elim)
  from ‹n irs-ns→⇩d* n'›
  have "n = n' ∨ (∃ns'. realizable (CFG_node (_Entry_)) ns' n' ∧ n ∈ set ns')"
  proof(rule irs_SDG_path_split)
    assume "n is-ns→⇩d* n'"
    show ?thesis
    proof(cases "ns = []")
      case True
      with ‹n is-ns→⇩d* n'› have "n = n'" by(fastforce elim:intra_sum_SDG_path.cases)
      thus ?thesis by simp
    next
      case False
      with ‹n is-ns→⇩d* n'› have "n ∈ set ns" by(fastforce dest:is_SDG_path_hd)
      from ‹n is-ns→⇩d* n'› have "valid_SDG_node n" and "valid_SDG_node n'"
        by(rule is_SDG_path_valid_SDG_node)+
      hence "valid_node (parent_node n)" by -(rule valid_SDG_CFG_node)
      from ‹n is-ns→⇩d* n'› obtain ns' where "matched n ns' n'" and "set ns ⊆ set ns'"
        by(erule is_SDG_path_matched)
      with ‹n ∈ set ns› have "n ∈ set ns'" by fastforce
      from ‹valid_node (parent_node n)›
      show ?thesis
      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)
        from ‹n is-ns→⇩d* n'› obtain as where "parent_node n -as→⇩ι* parent_node n'"
          by -(erule is_SDG_path_intra_CFG_path)
        with ‹n = CFG_node (_Exit_)› have "parent_node n' = (_Exit_)"
          by(fastforce dest:path_Exit_source simp:intra_path_def)
        with ‹valid_SDG_node n'› have "n' = CFG_node (_Exit_)"
          by(rule valid_SDG_node_parent_Exit)
        with ‹n = CFG_node (_Exit_)› show ?thesis by simp
      next
        case False
        with ‹valid_SDG_node n›
        obtain nsx where "CFG_node (_Entry_) cc-nsx→⇩d* n"
          by(erule Entry_cc_SDG_path_to_inner_node)
        hence "realizable (CFG_node (_Entry_)) nsx n" 
          by(rule cdep_SDG_path_realizable)
        with ‹matched n ns' n'›
        have "realizable (CFG_node (_Entry_)) (nsx@ns') n'"
          by -(rule realizable_Append_matched)
        with ‹n ∈ set ns'› show ?thesis by fastforce
      qed
    qed
  next
    fix nsx nsx' nx nx' p
    assume "ns = nsx@nx#nsx'" and "n irs-nsx→⇩d* nx"
      and "nx s-p→⇘ret⇙ nx' ∨ (∃V. nx s-p:V→⇘out⇙ nx')" and "nx' is-nsx'→⇩d* n'"
    from ‹nx s-p→⇘ret⇙ nx' ∨ (∃V. nx s-p:V→⇘out⇙ nx')›
    have "CFG_node (parent_node nx) s-p→⇘ret⇙ CFG_node (parent_node nx')"
      by(fastforce elim:sum_SDG_edge.cases intro:sum_SDG_return_edge)
    then obtain a Q f where "valid_edge a" and "kind a = Q↩⇘p⇙f"
      and "parent_node nx = sourcenode a" and "parent_node nx' = targetnode a"
      by(fastforce elim:sum_SDG_edge.cases)
    from ‹valid_edge a› ‹kind a = Q↩⇘p⇙f› obtain a' Q' r' fs' 
      where "a ∈ get_return_edges a'" and "valid_edge a'" and "kind a' = Q':r'↪⇘p⇙fs'"
      and "CFG_node (sourcenode a') s-p→⇘sum⇙ CFG_node (targetnode a)"
      by(erule return_edge_determines_call_and_sum_edge)
    from ‹valid_edge a'› ‹kind a' = Q':r'↪⇘p⇙fs'›
    have "CFG_node (sourcenode a') s-p→⇘call⇙ CFG_node (targetnode a')"
      by(fastforce intro:sum_SDG_call_edge)
    from ‹n irs-nsx→⇩d* nx› ‹nx s-p→⇘ret⇙ nx' ∨ (∃V. nx s-p:V→⇘out⇙ nx')›
    obtain m ms where "matched m ms nx'" and "n ∈ set ms"
      and "m s-p→⇘sum⇙ CFG_node (parent_node nx')"
      by(fastforce elim:irs_SDG_path_matched)
    from ‹nx' is-nsx'→⇩d* n'› obtain ms' where "matched nx' ms' n'" 
      and "set nsx' ⊆ set ms'" by(erule is_SDG_path_matched)
    with ‹matched m ms nx'› have "matched m (ms@ms') n'" by -(rule matched_Append)
   from ‹m s-p→⇘sum⇙ CFG_node (parent_node nx')› have "valid_SDG_node m"
      by(rule sum_SDG_edge_valid_SDG_node)
    hence "valid_node (parent_node m)" by(rule valid_SDG_CFG_node)
    thus ?thesis
    proof(cases "parent_node m = (_Exit_)")
      case True
      from ‹m s-p→⇘sum⇙ CFG_node (parent_node nx')› obtain a where "valid_edge a" 
        and "sourcenode a = parent_node m"
        by(fastforce elim:sum_SDG_edge.cases)
      with True have False by -(rule Exit_source,simp_all)
      thus ?thesis by simp
    next
      case False
      with ‹valid_SDG_node m›
      obtain ms'' where "CFG_node (_Entry_) cc-ms''→⇩d* m"
        by(erule Entry_cc_SDG_path_to_inner_node)
      hence "realizable (CFG_node (_Entry_)) ms'' m" 
        by(rule cdep_SDG_path_realizable)
      with ‹matched m (ms@ms') n'›
      have "realizable (CFG_node (_Entry_)) (ms''@(ms@ms')) n'"
        by -(rule realizable_Append_matched)
      with ‹n ∈ set ms› show ?thesis by fastforce
    qed
  qed
  with ‹n ≠ n'› show "∃ns'. realizable (CFG_node (_Entry_)) ns' n' ∧ n ∈ set ns'"
    by simp
qed

end

end