[STATEMENT]
lemma Exit_no_sum_SDG_edge_target:
  "sum_SDG_edge n Vopt popt b (CFG_node (_Exit_)) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_SDG_edge n Vopt popt b (CFG_node (_Exit_)) \<Longrightarrow> False
[PROOF STEP]
proof(induct "CFG_node (_Exit_)" rule:sum_SDG_edge.induct)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<And>n m m'. \<lbrakk>n = CFG_node m; CFG_node (_Exit_) = CFG_node m'; m controls m'\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q r p fs n a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; CFG_node (_Exit_) = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> False
 3. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 4. \<And>n V. n influences V in CFG_node (_Exit_) \<Longrightarrow> False
 5. \<And>a Q r p fs n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 7. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 8. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 9. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 10. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (sum_SDG_cdep_edge n m m')
[PROOF STATE]
proof (state)
this:
n = CFG_node m
CFG_node (_Exit_) = CFG_node m'
m controls m'

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

goal (1 subgoal):
 1. m controls (_Exit_)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m controls (_Exit_)

goal (10 subgoals):
 1. \<And>n m m'. \<lbrakk>n = CFG_node m; CFG_node (_Exit_) = CFG_node m'; m controls m'\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q r p fs n a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; CFG_node (_Exit_) = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> False
 3. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 4. \<And>n V. n influences V in CFG_node (_Exit_) \<Longrightarrow> False
 5. \<And>a Q r p fs n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 7. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 8. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 9. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 10. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
m controls (_Exit_)

goal (1 subgoal):
 1. False
[PROOF STEP]
by(fastforce dest:Exit_not_control_dependent)
[PROOF STATE]
proof (state)
this:
False

goal (10 subgoals):
 1. \<And>n m m'. \<lbrakk>n = CFG_node m; CFG_node (_Exit_) = CFG_node m'; m controls m'\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q r p fs n a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; CFG_node (_Exit_) = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> False
 3. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 4. \<And>n V. n influences V in CFG_node (_Exit_) \<Longrightarrow> False
 5. \<And>a Q r p fs n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 7. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 8. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 9. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 10. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
False

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

goal (9 subgoals):
 1. \<And>a Q r p fs n a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; CFG_node (_Exit_) = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> False
 2. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 3. \<And>n V. n influences V in CFG_node (_Exit_) \<Longrightarrow> False
 4. \<And>a Q r p fs n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 7. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 8. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 9. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>a Q r p fs n a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; CFG_node (_Exit_) = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> False
 2. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 3. \<And>n V. n influences V in CFG_node (_Exit_) \<Longrightarrow> False
 4. \<And>a Q r p fs n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 7. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 8. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 9. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (sum_SDG_proc_entry_exit_cdep a Q r p f n a')
[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
CFG_node (_Exit_) = CFG_node (sourcenode a')

goal (9 subgoals):
 1. \<And>a Q r p fs n a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; CFG_node (_Exit_) = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> False
 2. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 3. \<And>n V. n influences V in CFG_node (_Exit_) \<Longrightarrow> False
 4. \<And>a Q r p fs n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 7. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 8. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 9. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[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 (9 subgoals):
 1. \<And>a Q r p fs n a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; CFG_node (_Exit_) = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> False
 2. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 3. \<And>n V. n influences V in CFG_node (_Exit_) \<Longrightarrow> False
 4. \<And>a Q r p fs n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 7. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 8. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 9. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_edge a'

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

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

goal (9 subgoals):
 1. \<And>a Q r p fs n a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; CFG_node (_Exit_) = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> False
 2. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 3. \<And>n V. n influences V in CFG_node (_Exit_) \<Longrightarrow> False
 4. \<And>a Q r p fs n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 7. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 8. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 9. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
sourcenode a' = (_Exit_)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
sourcenode a' = (_Exit_)

goal (1 subgoal):
 1. False
[PROOF STEP]
by(rule Exit_source)
[PROOF STATE]
proof (state)
this:
False

goal (9 subgoals):
 1. \<And>a Q r p fs n a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (targetnode a); a' \<in> get_return_edges a; CFG_node (_Exit_) = CFG_node (sourcenode a')\<rbrakk> \<Longrightarrow> False
 2. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 3. \<And>n V. n influences V in CFG_node (_Exit_) \<Longrightarrow> False
 4. \<And>a Q r p fs n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 7. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 8. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 9. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
False

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

goal (8 subgoals):
 1. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 2. \<And>n V. n influences V in CFG_node (_Exit_) \<Longrightarrow> False
 3. \<And>a Q r p fs n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 4. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 7. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 8. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 2. \<And>n V. n influences V in CFG_node (_Exit_) \<Longrightarrow> False
 3. \<And>a Q r p fs n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 4. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 7. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 8. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (sum_SDG_ddep_edge n V)
[PROOF STATE]
proof (state)
this:
n influences V in CFG_node (_Exit_)

goal (8 subgoals):
 1. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 2. \<And>n V. n influences V in CFG_node (_Exit_) \<Longrightarrow> False
 3. \<And>a Q r p fs n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 4. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 7. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 8. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
n influences V in CFG_node (_Exit_)

goal (1 subgoal):
 1. False
[PROOF STEP]
by(fastforce elim:SDG_Use.cases simp:data_dependence_def)
[PROOF STATE]
proof (state)
this:
False

goal (7 subgoals):
 1. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q r p fs n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 3. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 4. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 7. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q r p fs n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 3. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 4. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 7. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (sum_SDG_call_edge a Q r p fs n)
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
n = CFG_node (sourcenode a)
CFG_node (_Exit_) = CFG_node (targetnode a)

goal (7 subgoals):
 1. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q r p fs n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 3. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 4. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 7. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from \<open>CFG_node (_Exit_) = CFG_node (targetnode a)\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (_Exit_) = CFG_node (targetnode a)
[PROOF STEP]
have "targetnode a = (_Exit_)"
[PROOF STATE]
proof (prove)
using this:
CFG_node (_Exit_) = CFG_node (targetnode a)

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

goal (7 subgoals):
 1. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q r p fs n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 3. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 4. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 7. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
targetnode a = (_Exit_)
[PROOF STEP]
have "get_proc (_Exit_) = p"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
targetnode a = (_Exit_)

goal (1 subgoal):
 1. get_proc (_Exit_) = p
[PROOF STEP]
by(fastforce intro:get_proc_call)
[PROOF STATE]
proof (state)
this:
get_proc (_Exit_) = p

goal (7 subgoals):
 1. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q r p fs n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 3. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 4. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 7. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "p = Main"
[PROOF STATE]
proof (prove)
using this:
get_proc (_Exit_) = p

goal (1 subgoal):
 1. p = Main
[PROOF STEP]
by(simp add:get_proc_Exit)
[PROOF STATE]
proof (state)
this:
p = Main

goal (7 subgoals):
 1. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q r p fs n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 3. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 4. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 7. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
p = Main
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
p = Main

goal (1 subgoal):
 1. False
[PROOF STEP]
by(fastforce intro:Main_no_call_target)
[PROOF STATE]
proof (state)
this:
False

goal (7 subgoals):
 1. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q r p fs n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 3. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 4. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 7. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
False

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

goal (6 subgoals):
 1. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 3. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 4. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 3. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 4. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (sum_SDG_return_edge a Q p f n)
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
n = CFG_node (sourcenode a)
CFG_node (_Exit_) = CFG_node (targetnode a)

goal (6 subgoals):
 1. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 3. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 4. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from \<open>CFG_node (_Exit_) = CFG_node (targetnode a)\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (_Exit_) = CFG_node (targetnode a)
[PROOF STEP]
have "targetnode a = (_Exit_)"
[PROOF STATE]
proof (prove)
using this:
CFG_node (_Exit_) = CFG_node (targetnode a)

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

goal (6 subgoals):
 1. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 3. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 4. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with \<open>valid_edge a\<close> \<open>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
targetnode a = (_Exit_)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
targetnode a = (_Exit_)

goal (1 subgoal):
 1. False
[PROOF STEP]
by(rule Exit_no_return_target)
[PROOF STATE]
proof (state)
this:
False

goal (6 subgoals):
 1. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q p fs n. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 3. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 4. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 6. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
False

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

goal (5 subgoals):
 1. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 3. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 4. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 3. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 4. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (sum_SDG_call_summary_edge a Q r p fs a' n)
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
a' \<in> get_return_edges a
n = CFG_node (sourcenode a)
CFG_node (_Exit_) = CFG_node (targetnode a')

goal (5 subgoals):
 1. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 3. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 4. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[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 (5 subgoals):
 1. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 3. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 4. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>a' \<in> get_return_edges a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
a' \<in> get_return_edges a
[PROOF STEP]
obtain Q' f' where "kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
a' \<in> get_return_edges a

goal (1 subgoal):
 1. (\<And>Q' f'. kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce dest!:call_return_edges)
[PROOF STATE]
proof (state)
this:
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'

goal (5 subgoals):
 1. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 3. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 4. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from \<open>CFG_node (_Exit_) = CFG_node (targetnode a')\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (_Exit_) = CFG_node (targetnode a')
[PROOF STEP]
have "targetnode a' = (_Exit_)"
[PROOF STATE]
proof (prove)
using this:
CFG_node (_Exit_) = CFG_node (targetnode a')

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

goal (5 subgoals):
 1. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 3. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 4. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with \<open>valid_edge a'\<close> \<open>kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
targetnode a' = (_Exit_)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
targetnode a' = (_Exit_)

goal (1 subgoal):
 1. False
[PROOF STEP]
by(rule Exit_no_return_target)
[PROOF STATE]
proof (state)
this:
False

goal (5 subgoals):
 1. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 3. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 4. \<And>a Q r p fs a' n. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); CFG_node (_Exit_) = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> False
 5. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
False

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

goal (4 subgoals):
 1. \<And>m n. \<lbrakk>valid_SDG_node (CFG_node (_Exit_)); m = parent_node (CFG_node (_Exit_)); n = CFG_node m; n \<noteq> CFG_node (_Exit_)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q r p fs ins outs V x 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); CFG_node (_Exit_) = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 3. \<And>a Q p f ins outs V x 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); CFG_node (_Exit_) = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 4. \<And>a Q r p fs a' x ns x' n ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); CFG_node (_Exit_) = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
qed simp+