[STATEMENT]
lemma SDG_return_or_param_out_edge_unique_CFG_return_edge:
  "SDG_edge n Vopt (Some(p,False)) n'
  \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and>
          targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SDG_edge n Vopt (Some (p, False)) n' \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[PROOF STEP]
proof(induct n Vopt "Some(p,False)" 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[PROOF STEP]
case (SDG_return_edge a Q f n n')
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[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\<hookleftarrow>\<^bsub>p\<^esub>f\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
n = CFG_node (sourcenode a)
n' = CFG_node (targetnode a)
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
\<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\<hookleftarrow>\<^bsub>p\<^esub>f
\<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 f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[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 f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)

goal (3 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[PROOF STEP]
case (SDG_param_out_edge a Q f ins outs V x n n')
[PROOF STATE]
proof (state)
this:
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)

goal (3 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
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)

goal (3 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[PROOF STEP]
fix a'
[PROOF STATE]
proof (state)
goal (3 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[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 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[PROOF STEP]
from \<open>sourcenode a' = parent_node n\<close> \<open>n = Formal_out (sourcenode a,x)\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode a' = parent_node n
n = Formal_out (sourcenode a, x)
[PROOF STEP]
have "sourcenode a' = sourcenode a"
[PROOF STATE]
proof (prove)
using this:
sourcenode a' = parent_node n
n = Formal_out (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 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sourcenode a' = sourcenode a

goal (3 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[PROOF STEP]
from \<open>targetnode a' = parent_node n'\<close> \<open>n' = Actual_out (targetnode a,x)\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a' = parent_node n'
n' = Actual_out (targetnode a, x)
[PROOF STEP]
have "targetnode a' = targetnode a"
[PROOF STATE]
proof (prove)
using this:
targetnode a' = parent_node n'
n' = Actual_out (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 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[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 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[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 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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)\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[PROOF STEP]
with \<open>valid_edge a\<close> \<open>n = Formal_out (sourcenode a,x)\<close>
    \<open>n' = Actual_out (targetnode a,x)\<close> \<open>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
n = Formal_out (sourcenode a, x)
n' = Actual_out (targetnode a, x)
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
\<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 = Formal_out (sourcenode a, x)
n' = Actual_out (targetnode a, x)
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
\<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 f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[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 f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)

goal (2 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
 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); True = False\<rbrakk> \<Longrightarrow> \<exists>!a. valid_edge a \<and> sourcenode a = parent_node n \<and> targetnode a = parent_node n' \<and> (\<exists>Q f. kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f)
[PROOF STEP]
qed simp_all


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

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

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

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

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

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

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

goal (1 subgoal):
 1. get_proc (targetnode a) = p
[PROOF STEP]
by(rule get_proc_call)
[PROOF STATE]
proof (state)
this:
get_proc (targetnode a) = p

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

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

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

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

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

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

goal (1 subgoal):
 1. False
[PROOF STEP]
by -(drule valid_SDG_node_parent_Exit,simp+)
[PROOF STATE]
proof (state)
this:
False

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

goal (5 subgoals):
 1. \<And>V n'. CFG_node (_Exit_) influences V in n' \<Longrightarrow> False
 2. \<And>a Q r p fs n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; CFG_node (_Exit_) = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 3. \<And>a Q p f n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; CFG_node (_Exit_) = CFG_node (sourcenode a); n' = 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; CFG_node (_Exit_) = Actual_in (sourcenode a, x); n' = 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; CFG_node (_Exit_) = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "(CFG_node (_Exit_)) influences V in n'"
[PROOF STATE]
proof (prove)
using this:
CFG_node (_Exit_) influences V in n'

goal (1 subgoal):
 1. CFG_node (_Exit_) influences V in n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
CFG_node (_Exit_) influences V in n'

goal (5 subgoals):
 1. \<And>V n'. CFG_node (_Exit_) influences V in n' \<Longrightarrow> False
 2. \<And>a Q r p fs n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; CFG_node (_Exit_) = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 3. \<And>a Q p f n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; CFG_node (_Exit_) = CFG_node (sourcenode a); n' = 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; CFG_node (_Exit_) = Actual_in (sourcenode a, x); n' = 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; CFG_node (_Exit_) = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with Exit_empty
[PROOF STATE]
proof (chain)
picking this:
Def (_Exit_) = {} \<and> Use (_Exit_) = {}
CFG_node (_Exit_) influences V in n'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Def (_Exit_) = {} \<and> Use (_Exit_) = {}
CFG_node (_Exit_) influences V in n'

goal (1 subgoal):
 1. False
[PROOF STEP]
by(fastforce dest:path_Exit_source SDG_Def_parent_Def
                simp:data_dependence_def intra_path_def)
[PROOF STATE]
proof (state)
this:
False

goal (4 subgoals):
 1. \<And>a Q r p fs n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; CFG_node (_Exit_) = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q p f n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; CFG_node (_Exit_) = CFG_node (sourcenode a); n' = 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; CFG_node (_Exit_) = Actual_in (sourcenode a, x); n' = 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; CFG_node (_Exit_) = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>a Q r p fs n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; CFG_node (_Exit_) = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q p f n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; CFG_node (_Exit_) = CFG_node (sourcenode a); n' = 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; CFG_node (_Exit_) = Actual_in (sourcenode a, x); n' = 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; CFG_node (_Exit_) = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (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
CFG_node (_Exit_) = CFG_node (sourcenode a)
n' = CFG_node (targetnode a)

goal (4 subgoals):
 1. \<And>a Q r p fs n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; CFG_node (_Exit_) = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q p f n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; CFG_node (_Exit_) = CFG_node (sourcenode a); n' = 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; CFG_node (_Exit_) = Actual_in (sourcenode a, x); n' = 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; CFG_node (_Exit_) = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x)\<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 (4 subgoals):
 1. \<And>a Q r p fs n'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; CFG_node (_Exit_) = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> False
 2. \<And>a Q p f n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; CFG_node (_Exit_) = CFG_node (sourcenode a); n' = 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; CFG_node (_Exit_) = Actual_in (sourcenode a, x); n' = 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; CFG_node (_Exit_) = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with \<open>valid_edge a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
sourcenode a = (_Exit_)
[PROOF STEP]
show ?case
[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 (3 subgoals):
 1. \<And>a Q p f n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; CFG_node (_Exit_) = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<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; CFG_node (_Exit_) = Actual_in (sourcenode a, x); n' = 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; CFG_node (_Exit_) = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a Q p f n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; CFG_node (_Exit_) = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<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; CFG_node (_Exit_) = Actual_in (sourcenode a, x); n' = 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; CFG_node (_Exit_) = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case (SDG_return_edge a Q p f n')
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
CFG_node (_Exit_) = CFG_node (sourcenode a)
n' = CFG_node (targetnode a)

goal (3 subgoals):
 1. \<And>a Q p f n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; CFG_node (_Exit_) = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<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; CFG_node (_Exit_) = Actual_in (sourcenode a, x); n' = 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; CFG_node (_Exit_) = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x)\<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 (3 subgoals):
 1. \<And>a Q p f n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; CFG_node (_Exit_) = CFG_node (sourcenode a); n' = CFG_node (targetnode a)\<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; CFG_node (_Exit_) = Actual_in (sourcenode a, x); n' = 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; CFG_node (_Exit_) = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with \<open>valid_edge a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
sourcenode a = (_Exit_)
[PROOF STEP]
show ?case
[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 (2 subgoals):
 1. \<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; CFG_node (_Exit_) = Actual_in (sourcenode a, x); n' = Formal_in (targetnode a, x)\<rbrakk> \<Longrightarrow> False
 2. \<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; CFG_node (_Exit_) = Formal_out (sourcenode a, x); n' = Actual_out (targetnode a, x)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma intra_SDG_path_Append:
  "\<lbrakk>n'' i-ns'\<rightarrow>\<^sub>d* n'; n i-ns\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> n i-ns@ns'\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n'' i-ns'\<rightarrow>\<^sub>d* n'; n i-ns\<rightarrow>\<^sub>d* n''\<rbrakk> \<Longrightarrow> n i-ns @ ns'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(induct rule:intra_SDG_path.induct,
   auto intro:intra_SDG_path.intros simp:append_assoc[THEN sym] simp del:append_assoc)


[STATEMENT]
lemma intra_SDG_path_valid_SDG_node:
  assumes "n i-ns\<rightarrow>\<^sub>d* 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>n i-ns\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (prove)
using this:
n i-ns\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. valid_SDG_node n &&& valid_SDG_node n'
[PROOF STEP]
by(induct rule:intra_SDG_path.induct,
   auto intro:SDG_edge_valid_SDG_node valid_SDG_CFG_node)