# Theory DynPDG

```chapter ‹Dynamic Slicing›

section ‹Dynamic Program Dependence Graph›

theory DynPDG imports
"../Basic/CFGExit_wf"
"../Basic/DynStandardControlDependence"
"../Basic/DynWeakControlDependence"
begin

subsection ‹The dynamic PDG›

locale DynPDG =
CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
and Entry :: "'node" ("'('_Entry'_')") and Def :: "'node ⇒ 'var set"
and Use :: "'node ⇒ 'var set" and state_val :: "'state ⇒ 'var ⇒ 'val"
and Exit :: "'node" ("'('_Exit'_')") +
fixes dyn_control_dependence :: "'node ⇒ 'node ⇒ 'edge list ⇒ bool"
("_ controls _ via _" [51,0,0])
assumes Exit_not_dyn_control_dependent:"n controls n' via as ⟹ n' ≠ (_Exit_)"
assumes dyn_control_dependence_path:
"n controls n' via as  ⟹ n -as→* n' ∧ as ≠ []"

begin

inductive cdep_edge :: "'node ⇒ 'edge list ⇒ 'node ⇒ bool"
("_ -_→⇩c⇩d _" [51,0,0] 80)
and ddep_edge :: "'node ⇒ 'var ⇒ 'edge list ⇒ 'node ⇒ bool"
("_ -'{_'}_→⇩d⇩d _" [51,0,0,0] 80)
and DynPDG_edge :: "'node ⇒ 'var option ⇒ 'edge list ⇒ 'node ⇒ bool"

where
― ‹Syntax›
"n -as→⇩c⇩d n' == DynPDG_edge n None as n'"
| "n -{V}as→⇩d⇩d n' == DynPDG_edge n (Some V) as n'"

― ‹Rules›
| DynPDG_cdep_edge:
"n controls n' via as ⟹ n -as→⇩c⇩d n'"

| DynPDG_ddep_edge:
"n influences V in n' via as ⟹ n -{V}as→⇩d⇩d n'"

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

where DynPDG_path_Nil:
"valid_node n ⟹ n -[]→⇩d* n"

| DynPDG_path_Append_cdep:
"⟦n -as→⇩d* n''; n'' -as'→⇩c⇩d n'⟧ ⟹ n -as@as'→⇩d* n'"

| DynPDG_path_Append_ddep:
"⟦n -as→⇩d* n''; n'' -{V}as'→⇩d⇩d n'⟧ ⟹ n -as@as'→⇩d* n'"

lemma DynPDG_empty_path_eq_nodes:"n -[]→⇩d* n' ⟹ n = n'"
apply - apply(erule DynPDG_path.cases)
apply simp
apply(auto elim:DynPDG_edge.cases dest:dyn_control_dependence_path)
by(auto elim:DynPDG_edge.cases simp:dyn_data_dependence_def)

lemma DynPDG_path_cdep:"n -as→⇩c⇩d n' ⟹ n -as→⇩d* n'"
apply(subgoal_tac "n -[]@as→⇩d* n'")
apply simp
apply(rule DynPDG_path_Append_cdep, rule DynPDG_path_Nil)
by(auto elim!:DynPDG_edge.cases dest:dyn_control_dependence_path path_valid_node)

lemma DynPDG_path_ddep:"n -{V}as→⇩d⇩d n' ⟹ n -as→⇩d* n'"
apply(subgoal_tac "n -[]@as→⇩d* n'")
apply simp
apply(rule DynPDG_path_Append_ddep, rule DynPDG_path_Nil)
by(auto elim!:DynPDG_edge.cases dest:path_valid_node simp:dyn_data_dependence_def)

lemma DynPDG_path_Append:
"⟦n'' -as'→⇩d* n'; n -as→⇩d* n''⟧ ⟹ n -as@as'→⇩d* n'"
apply(induct rule:DynPDG_path.induct)
apply(auto intro:DynPDG_path.intros)
apply(rotate_tac 1,drule DynPDG_path_Append_cdep,simp+)
apply(rotate_tac 1,drule DynPDG_path_Append_ddep,simp+)
done

lemma DynPDG_path_Exit:"⟦n -as→⇩d* n'; n' = (_Exit_)⟧ ⟹ n = (_Exit_)"
apply(induct rule:DynPDG_path.induct)
by(auto elim:DynPDG_edge.cases dest:Exit_not_dyn_control_dependent
simp:dyn_data_dependence_def)

lemma DynPDG_path_not_inner:
"⟦n -as→⇩d* n'; ¬ inner_node n'⟧ ⟹ n = n'"
proof(induct rule:DynPDG_path.induct)
case (DynPDG_path_Nil n)
thus ?case by simp
next
case (DynPDG_path_Append_cdep n as n'' as' n')
from ‹n'' -as'→⇩c⇩d n'› ‹¬ inner_node n'› have False
apply -
apply(erule DynPDG_edge.cases) apply(auto simp:inner_node_def)
apply(fastforce dest:dyn_control_dependence_path path_valid_node)
apply(fastforce dest:dyn_control_dependence_path path_valid_node)
by(fastforce dest:Exit_not_dyn_control_dependent)
thus ?case by simp
next
case (DynPDG_path_Append_ddep n as n'' V as' n')
from ‹n'' -{V}as'→⇩d⇩d n'› ‹¬ inner_node n'› have False
apply -
apply(erule DynPDG_edge.cases)
by(auto dest:path_valid_node simp:inner_node_def dyn_data_dependence_def)
thus ?case by simp
qed

lemma DynPDG_cdep_edge_CFG_path:
assumes "n -as→⇩c⇩d n'" shows "n -as→* n'" and "as ≠ []"
using ‹n -as→⇩c⇩d n'›
by(auto elim:DynPDG_edge.cases dest:dyn_control_dependence_path)

lemma DynPDG_ddep_edge_CFG_path:
assumes "n -{V}as→⇩d⇩d n'" shows "n -as→* n'" and "as ≠ []"
using ‹n -{V}as→⇩d⇩d n'›
by(auto elim:DynPDG_edge.cases simp:dyn_data_dependence_def)

lemma DynPDG_path_CFG_path:
"n -as→⇩d* n' ⟹ n -as→* n'"
proof(induct rule:DynPDG_path.induct)
case DynPDG_path_Nil thus ?case by(rule empty_path)
next
case (DynPDG_path_Append_cdep n as n'' as' n')
from ‹n'' -as'→⇩c⇩d n'› have "n'' -as'→* n'"
by(rule DynPDG_cdep_edge_CFG_path(1))
with ‹n -as→* n''› show ?case by(rule path_Append)
next
case (DynPDG_path_Append_ddep n as n'' V as' n')
from ‹n'' -{V}as'→⇩d⇩d n'› have "n'' -as'→* n'"
by(rule DynPDG_ddep_edge_CFG_path(1))
with ‹n -as→* n''› show ?case by(rule path_Append)
qed

lemma DynPDG_path_split:
"n -as→⇩d* n' ⟹
(as = [] ∧ n = n') ∨
(∃n'' asx asx'. (n -asx→⇩c⇩d n'') ∧ (n'' -asx'→⇩d* n') ∧
(as = asx@asx')) ∨
(∃n'' V asx asx'. (n -{V}asx→⇩d⇩d n'') ∧ (n'' -asx'→⇩d* n') ∧
(as = asx@asx'))"
proof(induct rule:DynPDG_path.induct)
case (DynPDG_path_Nil n) thus ?case by auto
next
case (DynPDG_path_Append_cdep n as n'' as' n')
note IH = ‹as = [] ∧ n = n'' ∨
(∃nx asx asx'. n -asx→⇩c⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx') ∨
(∃nx V asx asx'. n -{V}asx→⇩d⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx')›
from IH show ?case
proof
assume "as = [] ∧ n = n''"
with ‹n'' -as'→⇩c⇩d n'› have "valid_node n'"
by(fastforce intro:path_valid_node(2) DynPDG_path_CFG_path
DynPDG_path_cdep)
with ‹as = [] ∧ n = n''› ‹n'' -as'→⇩c⇩d n'›
have "∃n'' asx asx'. n -asx→⇩c⇩d n'' ∧ n'' -asx'→⇩d* n' ∧ as@as' = asx@asx'"
by(auto intro:DynPDG_path_Nil)
thus ?thesis by simp
next
assume "(∃nx asx asx'. n -asx→⇩c⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx') ∨
(∃nx V asx asx'. n -{V}asx→⇩d⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx')"
thus ?thesis
proof
assume "∃nx asx asx'. n -asx→⇩c⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx'"
then obtain nx asx asx' where "n -asx→⇩c⇩d nx" and "nx -asx'→⇩d* n''"
and "as = asx@asx'" by auto
from ‹n'' -as'→⇩c⇩d n'› have "n'' -as'→⇩d* n'" by(rule DynPDG_path_cdep)
with ‹nx -asx'→⇩d* n''› have "nx -asx'@as'→⇩d* n'"
by(fastforce intro:DynPDG_path_Append)
with ‹n -asx→⇩c⇩d nx› ‹as = asx@asx'›
have "∃n'' asx asx'. n -asx→⇩c⇩d n'' ∧ n'' -asx'→⇩d* n' ∧ as@as' = asx@asx'"
by auto
thus ?thesis by simp
next
assume "∃nx V asx asx'. n -{V}asx→⇩d⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx'"
then obtain nx V asx asx' where "n -{V}asx→⇩d⇩d nx" and "nx -asx'→⇩d* n''"
and "as = asx@asx'" by auto
from ‹n'' -as'→⇩c⇩d n'› have "n'' -as'→⇩d* n'" by(rule DynPDG_path_cdep)
with ‹nx -asx'→⇩d* n''› have "nx -asx'@as'→⇩d* n'"
by(fastforce intro:DynPDG_path_Append)
with ‹n -{V}asx→⇩d⇩d nx› ‹as = asx@asx'›
have "∃n'' V asx asx'. n -{V}asx→⇩d⇩d n'' ∧ n'' -asx'→⇩d* n' ∧ as@as' = asx@asx'"
by auto
thus ?thesis by simp
qed
qed
next
case (DynPDG_path_Append_ddep n as n'' V as' n')
note IH = ‹as = [] ∧ n = n'' ∨
(∃nx asx asx'. n -asx→⇩c⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx') ∨
(∃nx V asx asx'. n -{V}asx→⇩d⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx')›
from IH show ?case
proof
assume "as = [] ∧ n = n''"
with ‹n'' -{V}as'→⇩d⇩d n'› have "valid_node n'"
by(fastforce intro:path_valid_node(2) DynPDG_path_CFG_path
DynPDG_path_ddep)
with ‹as = [] ∧ n = n''› ‹n'' -{V}as'→⇩d⇩d n'›
have "∃n'' V asx asx'. n -{V}asx→⇩d⇩d n'' ∧ n'' -asx'→⇩d* n' ∧ as@as' = asx@asx'"
by(fastforce intro:DynPDG_path_Nil)
thus ?thesis by simp
next
assume "(∃nx asx asx'. n -asx→⇩c⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx') ∨
(∃nx V asx asx'. n -{V}asx→⇩d⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx')"
thus ?thesis
proof
assume "∃nx asx asx'. n -asx→⇩c⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx'"
then obtain nx asx asx' where "n -asx→⇩c⇩d nx" and "nx -asx'→⇩d* n''"
and "as = asx@asx'" by auto
from ‹n'' -{V}as'→⇩d⇩d n'› have "n'' -as'→⇩d* n'" by(rule DynPDG_path_ddep)
with ‹nx -asx'→⇩d* n''› have "nx -asx'@as'→⇩d* n'"
by(fastforce intro:DynPDG_path_Append)
with ‹n -asx→⇩c⇩d nx› ‹as = asx@asx'›
have "∃n'' asx asx'. n -asx→⇩c⇩d n'' ∧ n'' -asx'→⇩d* n' ∧ as@as' = asx@asx'"
by auto
thus ?thesis by simp
next
assume "∃nx V asx asx'. n -{V}asx→⇩d⇩d nx ∧ nx -asx'→⇩d* n'' ∧ as = asx@asx'"
then obtain nx V' asx asx' where "n -{V'}asx→⇩d⇩d nx" and "nx -asx'→⇩d* n''"
and "as = asx@asx'" by auto
from ‹n'' -{V}as'→⇩d⇩d n'› have "n'' -as'→⇩d* n'" by(rule DynPDG_path_ddep)
with ‹nx -asx'→⇩d* n''› have "nx -asx'@as'→⇩d* n'"
by(fastforce intro:DynPDG_path_Append)
with ‹n -{V'}asx→⇩d⇩d nx› ‹as = asx@asx'›
have "∃n'' V asx asx'. n -{V}asx→⇩d⇩d n'' ∧ n'' -asx'→⇩d* n' ∧ as@as' = asx@asx'"
by auto
thus ?thesis by simp
qed
qed
qed

lemma DynPDG_path_rev_cases [consumes 1,
case_names DynPDG_path_Nil DynPDG_path_cdep_Append DynPDG_path_ddep_Append]:
"⟦n -as→⇩d* n'; ⟦as = []; n = n'⟧ ⟹ Q;
⋀n'' asx asx'. ⟦n -asx→⇩c⇩d n''; n'' -asx'→⇩d* n';
as = asx@asx'⟧ ⟹ Q;
⋀V n'' asx asx'. ⟦n -{V}asx→⇩d⇩d n''; n'' -asx'→⇩d* n';
as = asx@asx'⟧ ⟹ Q⟧
⟹ Q"
by(blast dest:DynPDG_path_split)

lemma DynPDG_ddep_edge_no_shorter_ddep_edge:
assumes ddep:"n -{V}as→⇩d⇩d n'"
shows "∀as' a as''. tl as = as'@a#as'' ⟶ ¬ sourcenode a -{V}a#as''→⇩d⇩d n'"
proof -
from ddep have influence:"n influences V in n' via as"
by(auto elim!:DynPDG_edge.cases)
then obtain  a asx where as:"as = a#asx"
and notin:"n ∉ set (sourcenodes asx)"
by(auto dest:dyn_influence_source_notin_tl_edges simp:dyn_data_dependence_def)
from influence as
have imp:"∀nx ∈ set (sourcenodes asx). V ∉ Def nx"
by(auto simp:dyn_data_dependence_def)
{ fix as' a' as''
assume eq:"tl as = as'@a'#as''"
and ddep':"sourcenode a' -{V}a'#as''→⇩d⇩d n'"
from eq as notin have noteq:"sourcenode a' ≠ n" by(auto simp:sourcenodes_def)
from ddep' have "V ∈ Def (sourcenode a')"
by(auto elim!:DynPDG_edge.cases simp:dyn_data_dependence_def)
with eq as noteq imp have False by(auto simp:sourcenodes_def) }
thus ?thesis by blast
qed

lemma no_ddep_same_state:
assumes path:"n -as→* n'" and Uses:"V ∈ Use n'" and preds:"preds (kinds as) s"
and no_dep:"∀as' a as''. as = as'@a#as'' ⟶ ¬ sourcenode a -{V}a#as''→⇩d⇩d n'"
shows "state_val (transfers (kinds as) s) V = state_val s V"
proof -
{ fix n''
assume inset:"n'' ∈ set (sourcenodes as)" and Defs:"V ∈ Def n''"
hence "∃nx ∈ set (sourcenodes as). V ∈ Def nx" by auto
then obtain nx ns' ns'' where nodes:"sourcenodes as = ns'@nx#ns''"
and Defs':"V ∈ Def nx" and notDef:"∀nx' ∈ set ns''. V ∉ Def nx'"
by(fastforce elim!:rightmost_element_property)
from nodes obtain as' a as''
where as'':"sourcenodes as'' = ns''" and as:"as=as'@a#as''"
and source:"sourcenode a = nx"
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
from as path have path':"sourcenode a -a#as''→* n'"
by(fastforce dest:path_split_second)
from notDef as'' source
have "∀n'' ∈ set (sourcenodes as''). V ∉ Def n''"
by(auto simp:sourcenodes_def)
with path' Defs' Uses source
have influence:"nx influences V in n' via (a#as'')"
hence "nx ∉ set (sourcenodes as'')" by(rule dyn_influence_source_notin_tl_edges)
with influence source
have "∃asx a'. sourcenode a' -{V}a'#asx→⇩d⇩d n' ∧ sourcenode a' = nx ∧
(∃asx'. a#as'' = asx'@a'#asx)"
by(fastforce intro:DynPDG_ddep_edge)
with nodes no_dep as have False by(auto simp:sourcenodes_def) }
hence "∀n ∈ set (sourcenodes as). V ∉ Def n" by auto
with wf path preds show ?thesis by(fastforce intro:CFG_path_no_Def_equal)
qed

lemma DynPDG_ddep_edge_only_first_edge:
"⟦n -{V}a#as→⇩d⇩d n'; preds (kinds (a#as)) s⟧ ⟹
state_val (transfers (kinds (a#as)) s) V = state_val (transfer (kind a) s) V"
apply -
apply(erule DynPDG_edge.cases)
apply auto
apply(frule dyn_influence_Cons_source)
apply(frule dyn_influence_source_notin_tl_edges)
by(erule dyn_influence_only_first_edge)

lemma Use_value_change_implies_DynPDG_ddep_edge:
assumes "n -as→* n'" and "V ∈ Use n'" and "preds (kinds as) s"
and "preds (kinds as) s'" and "state_val s V = state_val s' V"
and "state_val (transfers (kinds as) s) V ≠
state_val (transfers (kinds as) s') V"
obtains as' a as'' where "as = as'@a#as''"
and "sourcenode a -{V}a#as''→⇩d⇩d n'"
and "state_val (transfers (kinds as) s) V =
state_val (transfers (kinds (as'@[a])) s) V"
and "state_val (transfers (kinds as) s') V =
state_val (transfers (kinds (as'@[a])) s') V"
proof(atomize_elim)
show "∃as' a as''. as = as'@a#as'' ∧
sourcenode a -{V}a#as''→⇩d⇩d n' ∧
state_val (transfers (kinds as) s) V =
state_val (transfers (kinds (as'@[a])) s) V ∧
state_val (transfers (kinds as) s') V =
state_val (transfers (kinds (as'@[a])) s') V"
proof(cases "∀as' a as''. as = as'@a#as'' ⟶
¬ sourcenode a -{V}a#as''→⇩d⇩d n'")
case True
with ‹n -as→* n'› ‹V ∈ Use n'› ‹preds (kinds as) s› ‹preds (kinds as) s'›
have "state_val (transfers (kinds as) s) V = state_val s V"
and "state_val (transfers (kinds as) s') V = state_val s' V"
by(auto intro:no_ddep_same_state)
with ‹state_val s V = state_val s' V›
‹state_val (transfers (kinds as) s) V ≠ state_val (transfers (kinds as) s') V›
show ?thesis by simp
next
case False
then obtain as' a as'' where [simp]:"as = as'@a#as''"
and "sourcenode a -{V}a#as''→⇩d⇩d n'" by auto
from ‹preds (kinds as) s› have "preds (kinds (a#as'')) (transfers (kinds as') s)"
with ‹sourcenode a -{V}a#as''→⇩d⇩d n'› have all:
"state_val (transfers (kinds (a#as'')) (transfers (kinds as') s)) V =
state_val (transfer (kind a) (transfers (kinds as') s)) V"
by(auto dest!:DynPDG_ddep_edge_only_first_edge)
from ‹preds (kinds as) s'›
have "preds (kinds (a#as'')) (transfers (kinds as') s')"
with ‹sourcenode a -{V}a#as''→⇩d⇩d n'› have all':
"state_val (transfers (kinds (a#as'')) (transfers (kinds as') s')) V =
state_val (transfer (kind a) (transfers (kinds as') s')) V"
by(auto dest!:DynPDG_ddep_edge_only_first_edge)
hence eq:"⋀s. transfers (kinds as) s =
transfers (kinds (a#as'')) (transfers (kinds as') s)"
with all have "state_val (transfers (kinds as) s) V =
state_val (transfers (kinds (as'@[a])) s) V"
moreover
from eq all' have "state_val (transfers (kinds as) s') V =
state_val (transfers (kinds (as'@[a])) s') V"
ultimately show ?thesis using ‹sourcenode a -{V}a#as''→⇩d⇩d n'› by simp blast
qed
qed

end

subsection ‹Instantiate dynamic PDG›

subsubsection ‹Standard control dependence›

locale DynStandardControlDependencePDG =
Postdomination sourcenode targetnode kind valid_edge Entry Exit +
CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
and Entry :: "'node" ("'('_Entry'_')") and Def :: "'node ⇒ 'var set"
and Use :: "'node ⇒ 'var set" and state_val :: "'state ⇒ 'var ⇒ 'val"
and Exit :: "'node" ("'('_Exit'_')")

begin

lemma DynPDG_scd:
"DynPDG sourcenode targetnode kind valid_edge (_Entry_)
Def Use state_val (_Exit_) dyn_standard_control_dependence"
proof(unfold_locales)
fix n n' as assume "n controls⇩s n' via as"
show "n' ≠ (_Exit_)"
proof
assume "n' = (_Exit_)"
with ‹n controls⇩s n' via as› show False
by(fastforce intro:Exit_not_dyn_standard_control_dependent)
qed
next
fix n n' as assume "n controls⇩s n' via as"
thus "n -as→* n' ∧ as ≠ []"
by(fastforce simp:dyn_standard_control_dependence_def)
qed

end

subsubsection ‹Weak control dependence›

locale DynWeakControlDependencePDG =
StrongPostdomination sourcenode targetnode kind valid_edge Entry Exit +
CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
for sourcenode :: "'edge ⇒ 'node" and targetnode :: "'edge ⇒ 'node"
and kind :: "'edge ⇒ 'state edge_kind" and valid_edge :: "'edge ⇒ bool"
and Entry :: "'node" ("'('_Entry'_')") and Def :: "'node ⇒ 'var set"
and Use :: "'node ⇒ 'var set" and state_val :: "'state ⇒ 'var ⇒ 'val"
and Exit :: "'node" ("'('_Exit'_')")

begin

lemma DynPDG_wcd:
"DynPDG sourcenode targetnode kind valid_edge (_Entry_)
Def Use state_val (_Exit_) dyn_weak_control_dependence"
proof(unfold_locales)
fix n n' as assume "n weakly controls n' via as"
show "n' ≠ (_Exit_)"
proof
assume "n' = (_Exit_)"
with ‹n weakly controls n' via as› show False
by(fastforce intro:Exit_not_dyn_weak_control_dependent)
qed
next
fix n n' as assume "n weakly controls n' via as"
thus "n -as→* n' ∧ as ≠ []"
by(fastforce simp:dyn_weak_control_dependence_def)
qed

end

subsection ‹Data slice›

definition (in CFG) empty_control_dependence :: "'node ⇒ 'node ⇒ 'edge list ⇒ bool"
where "empty_control_dependence n n' as ≡ False"

lemma (in CFGExit_wf) DynPDG_scd:
"DynPDG sourcenode targetnode kind valid_edge (_Entry_)
Def Use state_val  (_Exit_) empty_control_dependence"
proof(unfold_locales)
fix n n' as assume "empty_control_dependence n n' as"
thus "n' ≠ (_Exit_)" by(simp add:empty_control_dependence_def)
next
fix n n' as assume "empty_control_dependence n n' as"
thus "n -as→* n' ∧ as ≠ []" by(simp add:empty_control_dependence_def)
qed

end
```