[STATEMENT]
lemma SDG_edge_valid_SDG_node:
  assumes "SDG_edge n Vopt popt n'"
  shows "valid_SDG_node n" and "valid_SDG_node n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_SDG_node n &&& valid_SDG_node n'
[PROOF STEP]
using \<open>SDG_edge n Vopt popt n'\<close>
[PROOF STATE]
proof (prove)
using this:
SDG_edge n Vopt popt n'

goal (1 subgoal):
 1. valid_SDG_node n &&& valid_SDG_node n'
[PROOF STEP]
proof(induct rule:SDG_edge.induct)
[PROOF STATE]
proof (state)
goal (16 subgoals):
 1. \<And>n m n' m'. \<lbrakk>n = CFG_node m; n' = CFG_node m'; m controls m'\<rbrakk> \<Longrightarrow> valid_SDG_node n
 2. \<And>n m n' m'. \<lbrakk>n = CFG_node m; n' = CFG_node m'; m controls m'\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 3. \<And>a Q r p fs n a' n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; n' = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> valid_SDG_node n
 4. \<And>a Q r p fs n a' n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; n' = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 5. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n
 6. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 7. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n
 8. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n'
 9. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 10. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
A total of 16 subgoals...
[PROOF STEP]
case (SDG_cdep_edge n m n' m')
[PROOF STATE]
proof (state)
this:
n = CFG_node m
n' = CFG_node m'
m controls m'

goal (16 subgoals):
 1. \<And>n m n' m'. \<lbrakk>n = CFG_node m; n' = CFG_node m'; m controls m'\<rbrakk> \<Longrightarrow> valid_SDG_node n
 2. \<And>n m n' m'. \<lbrakk>n = CFG_node m; n' = CFG_node m'; m controls m'\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 3. \<And>a Q r p fs n a' n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; n' = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> valid_SDG_node n
 4. \<And>a Q r p fs n a' n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; n' = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 5. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n
 6. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 7. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n
 8. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n'
 9. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 10. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
A total of 16 subgoals...
[PROOF STEP]
thus "valid_SDG_node n" "valid_SDG_node n'"
[PROOF STATE]
proof (prove)
using this:
n = CFG_node m
n' = CFG_node m'
m controls m'

goal (1 subgoal):
 1. valid_SDG_node n &&& valid_SDG_node n'
[PROOF STEP]
by(fastforce elim:control_dependence_path elim:path_valid_node
                simp:intra_path_def)+
[PROOF STATE]
proof (state)
this:
valid_SDG_node n
valid_SDG_node n'

goal (14 subgoals):
 1. \<And>a Q r p fs n a' n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; n' = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> valid_SDG_node n
 2. \<And>a Q r p fs n a' n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; n' = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 3. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n
 4. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 5. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n
 6. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n'
 7. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 8. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 9. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 10. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
A total of 14 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (14 subgoals):
 1. \<And>a Q r p fs n a' n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; n' = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> valid_SDG_node n
 2. \<And>a Q r p fs n a' n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; n' = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 3. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n
 4. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 5. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n
 6. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n'
 7. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 8. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 9. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 10. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
A total of 14 subgoals...
[PROOF STEP]
case (SDG_proc_entry_exit_cdep a Q r p f n a' n')
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>f
n = CFG_node (targetnode a)
a' \<in> get_return_edges a
n' = CFG_node (sourcenode a')

goal (14 subgoals):
 1. \<And>a Q r p fs n a' n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; n' = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> valid_SDG_node n
 2. \<And>a Q r p fs n a' n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; n' = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 3. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n
 4. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 5. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n
 6. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n'
 7. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 8. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 9. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 10. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
A total of 14 subgoals...
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (14 subgoals):
 1. \<And>a Q r p fs n a' n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; n' = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> valid_SDG_node n
 2. \<And>a Q r p fs n a' n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; n' = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 3. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n
 4. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 5. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n
 6. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n'
 7. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 8. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 9. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 10. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
A total of 14 subgoals...
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>n = CFG_node (targetnode a)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
n = CFG_node (targetnode a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
valid_edge a
n = CFG_node (targetnode a)

goal (1 subgoal):
 1. valid_SDG_node n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
valid_SDG_node n

goal (13 subgoals):
 1. \<And>a Q r p fs n a' n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; n' = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 2. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n
 3. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 4. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n
 5. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n'
 6. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 7. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 8. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 9. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 10. \<And>a Q r p fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> valid_SDG_node n
A total of 13 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<And>a Q r p fs n a' n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; n' = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 2. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n
 3. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 4. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n
 5. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n'
 6. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 7. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 8. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 9. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 10. \<And>a Q r p fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> valid_SDG_node n
A total of 13 subgoals...
[PROOF STEP]
case (SDG_proc_entry_exit_cdep a Q r p f n a' n')
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>f
n = CFG_node (targetnode a)
a' \<in> get_return_edges a
n' = CFG_node (sourcenode a')

goal (13 subgoals):
 1. \<And>a Q r p fs n a' n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; n' = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 2. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n
 3. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 4. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n
 5. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n'
 6. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 7. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 8. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 9. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 10. \<And>a Q r p fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> valid_SDG_node n
A total of 13 subgoals...
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:

goal (13 subgoals):
 1. \<And>a Q r p fs n a' n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; n' = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 2. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n
 3. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 4. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n
 5. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n'
 6. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 7. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 8. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 9. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 10. \<And>a Q r p fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> valid_SDG_node n
A total of 13 subgoals...
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>a' \<in> get_return_edges a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
a' \<in> get_return_edges a
[PROOF STEP]
have "valid_edge a'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
a' \<in> get_return_edges a

goal (1 subgoal):
 1. valid_edge a'
[PROOF STEP]
by(rule get_return_edges_valid)
[PROOF STATE]
proof (state)
this:
valid_edge a'

goal (13 subgoals):
 1. \<And>a Q r p fs n a' n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; n' = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 2. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n
 3. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 4. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n
 5. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n'
 6. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 7. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 8. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 9. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 10. \<And>a Q r p fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> valid_SDG_node n
A total of 13 subgoals...
[PROOF STEP]
with \<open>n' = CFG_node (sourcenode a')\<close>
[PROOF STATE]
proof (chain)
picking this:
n' = CFG_node (sourcenode a')
valid_edge a'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n' = CFG_node (sourcenode a')
valid_edge a'

goal (1 subgoal):
 1. valid_SDG_node n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
valid_SDG_node n'

goal (12 subgoals):
 1. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n
 2. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 3. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n
 4. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n'
 5. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 6. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 7. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 8. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 9. \<And>a Q r p fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 10. \<And>a Q r p fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
A total of 12 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (12 subgoals):
 1. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n
 2. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 3. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n
 4. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n'
 5. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 6. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 7. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 8. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 9. \<And>a Q r p fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 10. \<And>a Q r p fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
A total of 12 subgoals...
[PROOF STEP]
case (SDG_ddep_edge n V n')
[PROOF STATE]
proof (state)
this:
n influences V in n'

goal (12 subgoals):
 1. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n
 2. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 3. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n
 4. \<And>n V n'. n influences V in n' \<Longrightarrow> valid_SDG_node n'
 5. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 6. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 7. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 8. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 9. \<And>a Q r p fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 10. \<And>a Q r p fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
A total of 12 subgoals...
[PROOF STEP]
thus "valid_SDG_node n" "valid_SDG_node n'"
[PROOF STATE]
proof (prove)
using this:
n influences V in n'

goal (1 subgoal):
 1. valid_SDG_node n &&& valid_SDG_node n'
[PROOF STEP]
by(auto intro:in_Use_valid_SDG_node in_Def_valid_SDG_node
             simp:data_dependence_def)
[PROOF STATE]
proof (state)
this:
valid_SDG_node n
valid_SDG_node n'

goal (10 subgoals):
 1. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n
 2. \<And>n' m n. \<lbrakk>valid_SDG_node n'; m = parent_node n'; n = CFG_node m; n \<noteq> n'\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 3. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 4. \<And>a Q r p fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 5. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 6. \<And>a Q p f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 7. \<And>a Q r p fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 8. \<And>a Q r p fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
 9. \<And>a Q p f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> valid_SDG_node n
 10. \<And>a Q p f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> valid_SDG_node n'
[PROOF STEP]
qed(fastforce intro:valid_SDG_CFG_node)+


[STATEMENT]
lemma valid_SDG_node_cases:
  assumes "valid_SDG_node n"
  shows "n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
proof(cases n)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x1. n = CFG_node x1 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 2. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 3. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 4. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 5. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
case (CFG_node m)
[PROOF STATE]
proof (state)
this:
n = CFG_node m

goal (5 subgoals):
 1. \<And>x1. n = CFG_node x1 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 2. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 3. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 4. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 5. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
n = CFG_node m

goal (1 subgoal):
 1. n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n

goal (4 subgoals):
 1. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 2. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 3. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 4. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 2. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 3. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 4. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
case (Formal_in z)
[PROOF STATE]
proof (state)
this:
n = Formal_in z

goal (4 subgoals):
 1. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 2. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 3. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 4. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
from \<open>n = Formal_in z\<close>
[PROOF STATE]
proof (chain)
picking this:
n = Formal_in z
[PROOF STEP]
obtain m x where "z = (m,x)"
[PROOF STATE]
proof (prove)
using this:
n = Formal_in z

goal (1 subgoal):
 1. (\<And>m x. z = (m, x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases z) auto
[PROOF STATE]
proof (state)
this:
z = (m, x)

goal (4 subgoals):
 1. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 2. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 3. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 4. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
with \<open>valid_SDG_node n\<close> \<open>n = Formal_in z\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
n = Formal_in z
z = (m, x)
[PROOF STEP]
have "CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n
n = Formal_in z
z = (m, x)

goal (1 subgoal):
 1. CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
by -(rule SDG_parent_cdep_edge,auto)
[PROOF STATE]
proof (state)
this:
CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n

goal (4 subgoals):
 1. \<And>x2. n = Formal_in x2 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 2. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 3. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 4. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n

goal (1 subgoal):
 1. n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n

goal (3 subgoals):
 1. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 2. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 3. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 2. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 3. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
case (Formal_out z)
[PROOF STATE]
proof (state)
this:
n = Formal_out z

goal (3 subgoals):
 1. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 2. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 3. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
from \<open>n = Formal_out z\<close>
[PROOF STATE]
proof (chain)
picking this:
n = Formal_out z
[PROOF STEP]
obtain m x where "z = (m,x)"
[PROOF STATE]
proof (prove)
using this:
n = Formal_out z

goal (1 subgoal):
 1. (\<And>m x. z = (m, x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases z) auto
[PROOF STATE]
proof (state)
this:
z = (m, x)

goal (3 subgoals):
 1. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 2. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 3. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
with \<open>valid_SDG_node n\<close> \<open>n = Formal_out z\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
n = Formal_out z
z = (m, x)
[PROOF STEP]
have "CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n
n = Formal_out z
z = (m, x)

goal (1 subgoal):
 1. CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
by -(rule SDG_parent_cdep_edge,auto)
[PROOF STATE]
proof (state)
this:
CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n

goal (3 subgoals):
 1. \<And>x3. n = Formal_out x3 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 2. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 3. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n

goal (1 subgoal):
 1. n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n

goal (2 subgoals):
 1. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 2. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 2. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
case (Actual_in z)
[PROOF STATE]
proof (state)
this:
n = Actual_in z

goal (2 subgoals):
 1. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 2. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
from \<open>n = Actual_in z\<close>
[PROOF STATE]
proof (chain)
picking this:
n = Actual_in z
[PROOF STEP]
obtain m x where "z = (m,x)"
[PROOF STATE]
proof (prove)
using this:
n = Actual_in z

goal (1 subgoal):
 1. (\<And>m x. z = (m, x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases z) auto
[PROOF STATE]
proof (state)
this:
z = (m, x)

goal (2 subgoals):
 1. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 2. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
with \<open>valid_SDG_node n\<close> \<open>n = Actual_in z\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
n = Actual_in z
z = (m, x)
[PROOF STEP]
have "CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n
n = Actual_in z
z = (m, x)

goal (1 subgoal):
 1. CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
by -(rule SDG_parent_cdep_edge,auto)
[PROOF STATE]
proof (state)
this:
CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n

goal (2 subgoals):
 1. \<And>x4. n = Actual_in x4 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
 2. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n

goal (1 subgoal):
 1. n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n

goal (1 subgoal):
 1. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
case (Actual_out z)
[PROOF STATE]
proof (state)
this:
n = Actual_out z

goal (1 subgoal):
 1. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
from \<open>n = Actual_out z\<close>
[PROOF STATE]
proof (chain)
picking this:
n = Actual_out z
[PROOF STEP]
obtain m x where "z = (m,x)"
[PROOF STATE]
proof (prove)
using this:
n = Actual_out z

goal (1 subgoal):
 1. (\<And>m x. z = (m, x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases z) auto
[PROOF STATE]
proof (state)
this:
z = (m, x)

goal (1 subgoal):
 1. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
with \<open>valid_SDG_node n\<close> \<open>n = Actual_out z\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
n = Actual_out z
z = (m, x)
[PROOF STEP]
have "CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n
n = Actual_out z
z = (m, x)

goal (1 subgoal):
 1. CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
by -(rule SDG_parent_cdep_edge,auto)
[PROOF STATE]
proof (state)
this:
CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n

goal (1 subgoal):
 1. \<And>x5. n = Actual_out x5 \<Longrightarrow> n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n

goal (1 subgoal):
 1. n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n = CFG_node (parent_node n) \<or> CFG_node (parent_node n) \<longrightarrow>\<^bsub>cd\<^esub> n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma SDG_cdep_edge_CFG_node: "n \<longrightarrow>\<^bsub>cd\<^esub> n' \<Longrightarrow> \<exists>m. n = CFG_node m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<longrightarrow>\<^bsub>cd\<^esub> n' \<Longrightarrow> \<exists>m. n = CFG_node m
[PROOF STEP]
by(induct n Vopt\<equiv>"None::'var option" popt\<equiv>"None::('pname \<times> bool) option" n'
   rule:SDG_edge.induct) auto


[STATEMENT]
lemma SDG_call_edge_CFG_node: "n -p\<rightarrow>\<^bsub>call\<^esub> n' \<Longrightarrow> \<exists>m. n = CFG_node m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n -p\<rightarrow>\<^bsub>call\<^esub> n' \<Longrightarrow> \<exists>m. n = CFG_node m
[PROOF STEP]
by(induct n Vopt\<equiv>"None::'var option" popt\<equiv>"Some(p,True)" n'
   rule:SDG_edge.induct) auto


[STATEMENT]
lemma SDG_return_edge_CFG_node: "n -p\<rightarrow>\<^bsub>ret\<^esub> n' \<Longrightarrow> \<exists>m. n = CFG_node m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n -p\<rightarrow>\<^bsub>ret\<^esub> n' \<Longrightarrow> \<exists>m. n = CFG_node m
[PROOF STEP]
by(induct n Vopt\<equiv>"None::'var option" popt\<equiv>"Some(p,False)" n'
   rule:SDG_edge.induct) auto


[STATEMENT]
lemma SDG_call_or_param_in_edge_unique_CFG_call_edge:
  "SDG_edge n Vopt (Some(p,True)) n'
  \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and>
          targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SDG_edge n Vopt (Some (p, True)) n' \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
proof(induct n Vopt "Some(p,True)" n' rule:SDG_edge.induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>a Q r fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 2. \<And>a Q f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 3. \<And>a Q r fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 4. \<And>a Q f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
case (SDG_call_edge a Q r fs n n')
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
n = CFG_node (sourcenode a)
n' = CFG_node (targetnode a)

goal (4 subgoals):
 1. \<And>a Q r fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 2. \<And>a Q f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 3. \<And>a Q r fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 4. \<And>a Q f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
n = CFG_node (sourcenode a)
n' = CFG_node (targetnode a)

goal (4 subgoals):
 1. \<And>a Q r fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 2. \<And>a Q f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 3. \<And>a Q r fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 4. \<And>a Q f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
fix a'
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>a Q r fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 2. \<And>a Q f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 3. \<And>a Q r fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 4. \<And>a Q f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
assume "valid_edge a'" and "sourcenode a' = parent_node n"
      and "targetnode a' = parent_node n'"
[PROOF STATE]
proof (state)
this:
valid_edge a'
sourcenode a' = parent_node n
targetnode a' = parent_node n'

goal (4 subgoals):
 1. \<And>a Q r fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 2. \<And>a Q f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 3. \<And>a Q r fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 4. \<And>a Q f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
from \<open>sourcenode a' = parent_node n\<close> \<open>n = CFG_node (sourcenode a)\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode a' = parent_node n
n = CFG_node (sourcenode a)
[PROOF STEP]
have "sourcenode a' = sourcenode a"
[PROOF STATE]
proof (prove)
using this:
sourcenode a' = parent_node n
n = CFG_node (sourcenode a)

goal (1 subgoal):
 1. sourcenode a' = sourcenode a
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
sourcenode a' = sourcenode a

goal (4 subgoals):
 1. \<And>a Q r fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 2. \<And>a Q f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 3. \<And>a Q r fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 4. \<And>a Q f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sourcenode a' = sourcenode a

goal (4 subgoals):
 1. \<And>a Q r fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 2. \<And>a Q f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 3. \<And>a Q r fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 4. \<And>a Q f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
from \<open>targetnode a' = parent_node n'\<close> \<open>n' = CFG_node (targetnode a)\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a' = parent_node n'
n' = CFG_node (targetnode a)
[PROOF STEP]
have "targetnode a' = targetnode a"
[PROOF STATE]
proof (prove)
using this:
targetnode a' = parent_node n'
n' = CFG_node (targetnode a)

goal (1 subgoal):
 1. targetnode a' = targetnode a
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
targetnode a' = targetnode a

goal (4 subgoals):
 1. \<And>a Q r fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 2. \<And>a Q f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 3. \<And>a Q r fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 4. \<And>a Q f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sourcenode a' = sourcenode a
targetnode a' = targetnode a
[PROOF STEP]
have "a' = a"
[PROOF STATE]
proof (prove)
using this:
sourcenode a' = sourcenode a
targetnode a' = targetnode a

goal (1 subgoal):
 1. a' = a
[PROOF STEP]
using \<open>valid_edge a'\<close> \<open>valid_edge a\<close>
[PROOF STATE]
proof (prove)
using this:
sourcenode a' = sourcenode a
targetnode a' = targetnode a
valid_edge a'
valid_edge a

goal (1 subgoal):
 1. a' = a
[PROOF STEP]
by(fastforce intro:edge_det)
[PROOF STATE]
proof (state)
this:
a' = a

goal (4 subgoals):
 1. \<And>a Q r fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 2. \<And>a Q f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 3. \<And>a Q r fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 4. \<And>a Q f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>valid_edge ?a'2; sourcenode ?a'2 = parent_node n; targetnode ?a'2 = parent_node n'\<rbrakk> \<Longrightarrow> ?a'2 = a

goal (4 subgoals):
 1. \<And>a Q r fs n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 2. \<And>a Q f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 3. \<And>a Q r fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 4. \<And>a Q f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
with \<open>valid_edge a\<close> \<open>n = CFG_node (sourcenode a)\<close> \<open>n' = CFG_node (targetnode a)\<close>
    \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
n = CFG_node (sourcenode a)
n' = CFG_node (targetnode a)
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
\<lbrakk>valid_edge ?a'2; sourcenode ?a'2 = parent_node n; targetnode ?a'2 = parent_node n'\<rbrakk> \<Longrightarrow> ?a'2 = a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
valid_edge a
n = CFG_node (sourcenode a)
n' = CFG_node (targetnode a)
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
\<lbrakk>valid_edge ?a'2; sourcenode ?a'2 = parent_node n; targetnode ?a'2 = parent_node n'\<rbrakk> \<Longrightarrow> ?a'2 = a

goal (1 subgoal):
 1. \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
by(fastforce intro!:ex1I[of _ a])
[PROOF STATE]
proof (state)
this:
\<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)

goal (3 subgoals):
 1. \<And>a Q f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 2. \<And>a Q r fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 3. \<And>a Q f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a Q f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 2. \<And>a Q r fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 3. \<And>a Q f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
case (SDG_param_in_edge a Q r fs ins outs V x n n')
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
(p, ins, outs) \<in> set procs
V = ins ! x
x < length ins
n = Actual_in (sourcenode a, x)
n' = Formal_in (targetnode a, x)

goal (3 subgoals):
 1. \<And>a Q f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 2. \<And>a Q r fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 3. \<And>a Q f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
(p, ins, outs) \<in> set procs
V = ins ! x
x < length ins
n = Actual_in (sourcenode a, x)
n' = Formal_in (targetnode a, x)

goal (3 subgoals):
 1. \<And>a Q f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 2. \<And>a Q r fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 3. \<And>a Q f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
fix a'
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a Q f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 2. \<And>a Q r fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 3. \<And>a Q f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
assume "valid_edge a'" and "sourcenode a' = parent_node n"
      and "targetnode a' = parent_node n'"
[PROOF STATE]
proof (state)
this:
valid_edge a'
sourcenode a' = parent_node n
targetnode a' = parent_node n'

goal (3 subgoals):
 1. \<And>a Q f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 2. \<And>a Q r fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 3. \<And>a Q f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
from \<open>sourcenode a' = parent_node n\<close> \<open>n = Actual_in (sourcenode a,x)\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode a' = parent_node n
n = Actual_in (sourcenode a, x)
[PROOF STEP]
have "sourcenode a' = sourcenode a"
[PROOF STATE]
proof (prove)
using this:
sourcenode a' = parent_node n
n = Actual_in (sourcenode a, x)

goal (1 subgoal):
 1. sourcenode a' = sourcenode a
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
sourcenode a' = sourcenode a

goal (3 subgoals):
 1. \<And>a Q f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 2. \<And>a Q r fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 3. \<And>a Q f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sourcenode a' = sourcenode a

goal (3 subgoals):
 1. \<And>a Q f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 2. \<And>a Q r fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 3. \<And>a Q f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
from \<open>targetnode a' = parent_node n'\<close> \<open>n' = Formal_in (targetnode a,x)\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a' = parent_node n'
n' = Formal_in (targetnode a, x)
[PROOF STEP]
have "targetnode a' = targetnode a"
[PROOF STATE]
proof (prove)
using this:
targetnode a' = parent_node n'
n' = Formal_in (targetnode a, x)

goal (1 subgoal):
 1. targetnode a' = targetnode a
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
targetnode a' = targetnode a

goal (3 subgoals):
 1. \<And>a Q f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 2. \<And>a Q r fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 3. \<And>a Q f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sourcenode a' = sourcenode a
targetnode a' = targetnode a
[PROOF STEP]
have "a' = a"
[PROOF STATE]
proof (prove)
using this:
sourcenode a' = sourcenode a
targetnode a' = targetnode a

goal (1 subgoal):
 1. a' = a
[PROOF STEP]
using \<open>valid_edge a'\<close> \<open>valid_edge a\<close>
[PROOF STATE]
proof (prove)
using this:
sourcenode a' = sourcenode a
targetnode a' = targetnode a
valid_edge a'
valid_edge a

goal (1 subgoal):
 1. a' = a
[PROOF STEP]
by(fastforce intro:edge_det)
[PROOF STATE]
proof (state)
this:
a' = a

goal (3 subgoals):
 1. \<And>a Q f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 2. \<And>a Q r fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 3. \<And>a Q f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>valid_edge ?a'2; sourcenode ?a'2 = parent_node n; targetnode ?a'2 = parent_node n'\<rbrakk> \<Longrightarrow> ?a'2 = a

goal (3 subgoals):
 1. \<And>a Q f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 2. \<And>a Q r fs ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins; n = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 3. \<And>a Q f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
with \<open>valid_edge a\<close> \<open>n = Actual_in (sourcenode a,x)\<close>
    \<open>n' = Formal_in (targetnode a,x)\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
n = Actual_in (sourcenode a, x)
n' = Formal_in (targetnode a, x)
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
\<lbrakk>valid_edge ?a'2; sourcenode ?a'2 = parent_node n; targetnode ?a'2 = parent_node n'\<rbrakk> \<Longrightarrow> ?a'2 = a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
valid_edge a
n = Actual_in (sourcenode a, x)
n' = Formal_in (targetnode a, x)
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
\<lbrakk>valid_edge ?a'2; sourcenode ?a'2 = parent_node n; targetnode ?a'2 = parent_node n'\<rbrakk> \<Longrightarrow> ?a'2 = a

goal (1 subgoal):
 1. \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
by(fastforce intro!:ex1I[of _ a])
[PROOF STATE]
proof (state)
this:
\<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)

goal (2 subgoals):
 1. \<And>a Q f n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
 2. \<And>a Q f ins outs V x n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; (p, ins, outs) \<in> set procs; V = outs ! x; x < length outs; n = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x); False = True\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q r fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs)
[PROOF STEP]
qed simp_all