[STATEMENT]
lemma sum_SDG_summary_edge_matched:
  assumes "n s-p\<rightarrow>\<^bsub>sum\<^esub> n'"
  obtains ns where "matched n ns n'" and "n \<in> set ns"
  and "get_proc (parent_node(last ns)) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ns. \<lbrakk>matched n ns n'; n \<in> set ns; get_proc (parent_node (last ns)) = p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[PROOF STEP]
from \<open>n s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n s-p\<rightarrow>\<^bsub>sum\<^esub> n'
[PROOF STEP]
show "\<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node(last ns)) = p"
[PROOF STATE]
proof (prove)
using this:
n s-p\<rightarrow>\<^bsub>sum\<^esub> n'

goal (1 subgoal):
 1. \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[PROOF STEP]
proof(induct n "None::'var option" "Some(p,True)" "True" n'
               rule:sum_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); False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 2. \<And>a Q fs n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True; False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 3. \<And>a Q r fs a' n 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); n' = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 4. \<And>a Q r fs a' x ns x' n 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); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[PROOF STEP]
case (sum_SDG_call_summary_edge a Q r fs a' n 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)
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); False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 2. \<And>a Q fs n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True; False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 3. \<And>a Q r fs a' n 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); n' = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 4. \<And>a Q r fs a' x ns x' n 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); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>n = CFG_node (sourcenode a)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
n = CFG_node (sourcenode a)
[PROOF STEP]
have "n -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
n = CFG_node (sourcenode a)

goal (1 subgoal):
 1. n -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a)
[PROOF STEP]
by(fastforce intro:SDG_call_edge)
[PROOF STATE]
proof (state)
this:
n -p\<rightarrow>\<^bsub>call\<^esub> 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); False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 2. \<And>a Q fs n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True; False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 3. \<And>a Q r fs a' n 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); n' = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 4. \<And>a Q r fs a' x ns x' n 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); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[PROOF STEP]
hence "valid_SDG_node n"
[PROOF STATE]
proof (prove)
using this:
n -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a)

goal (1 subgoal):
 1. valid_SDG_node n
[PROOF STEP]
by(rule SDG_edge_valid_SDG_node)
[PROOF STATE]
proof (state)
this:
valid_SDG_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); False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 2. \<And>a Q fs n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True; False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 3. \<And>a Q r fs a' n 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); n' = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 4. \<And>a Q r fs a' x ns x' n 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); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[PROOF STEP]
hence "matched n [] n"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n

goal (1 subgoal):
 1. matched n [] n
[PROOF STEP]
by(rule matched_Nil)
[PROOF STATE]
proof (state)
this:
matched n [] 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); False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 2. \<And>a Q fs n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True; False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 3. \<And>a Q r fs a' n 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); n' = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 4. \<And>a Q r fs a' x ns x' n 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); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[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 (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); False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 2. \<And>a Q fs n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True; False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 3. \<And>a Q r fs a' n 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); n' = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 4. \<And>a Q r fs a' x ns x' n 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); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[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]
have matched:"matched (CFG_node (targetnode a)) [CFG_node (targetnode a)]
      (CFG_node (sourcenode a'))"
[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. matched (CFG_node (targetnode a)) [CFG_node (targetnode a)] (CFG_node (sourcenode a'))
[PROOF STEP]
by(rule intra_proc_matched)
[PROOF STATE]
proof (state)
this:
matched (CFG_node (targetnode a)) [CFG_node (targetnode a)] (CFG_node (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); False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 2. \<And>a Q fs n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True; False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 3. \<And>a Q r fs a' n 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); n' = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 4. \<And>a Q r fs a' x ns x' n 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); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>a' \<in> get_return_edges a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
a' \<in> get_return_edges a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
obtain Q' f' where "kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
a' \<in> get_return_edges a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

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 (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); False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 2. \<And>a Q fs n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True; False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 3. \<And>a Q r fs a' n 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); n' = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 4. \<And>a Q r fs a' x ns x' n 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); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[PROOF STEP]
with \<open>valid_edge a'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
[PROOF STEP]
have "get_proc (sourcenode a') = p"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'

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

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); False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 2. \<And>a Q fs n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True; False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 3. \<And>a Q r fs a' n 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); n' = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 4. \<And>a Q r fs a' x ns x' n 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); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[PROOF STEP]
from \<open>valid_edge a'\<close> \<open>kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'\<close> \<open>n' = CFG_node (targetnode a')\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
n' = CFG_node (targetnode a')
[PROOF STEP]
have "CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>ret\<^esub> n'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
n' = CFG_node (targetnode a')

goal (1 subgoal):
 1. CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>ret\<^esub> n'
[PROOF STEP]
by(fastforce intro:SDG_return_edge)
[PROOF STATE]
proof (state)
this:
CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>ret\<^esub> 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); False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 2. \<And>a Q fs n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True; False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 3. \<And>a Q r fs a' n 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); n' = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 4. \<And>a Q r fs a' x ns x' n 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); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[PROOF STEP]
from \<open>matched n [] n\<close> \<open>n -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a)\<close> matched
      \<open>CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>ret\<^esub> n'\<close> \<open>a' \<in> get_return_edges a\<close>
      \<open>n = CFG_node (sourcenode a)\<close> \<open>n' = CFG_node (targetnode a')\<close> \<open>valid_edge a\<close>
[PROOF STATE]
proof (chain)
picking this:
matched n [] n
n -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a)
matched (CFG_node (targetnode a)) [CFG_node (targetnode a)] (CFG_node (sourcenode a'))
CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>ret\<^esub> n'
a' \<in> get_return_edges a
n = CFG_node (sourcenode a)
n' = CFG_node (targetnode a')
valid_edge a
[PROOF STEP]
have "matched n ([]@n#[CFG_node (targetnode a)]@[CFG_node (sourcenode a')]) n'"
[PROOF STATE]
proof (prove)
using this:
matched n [] n
n -p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a)
matched (CFG_node (targetnode a)) [CFG_node (targetnode a)] (CFG_node (sourcenode a'))
CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>ret\<^esub> n'
a' \<in> get_return_edges a
n = CFG_node (sourcenode a)
n' = CFG_node (targetnode a')
valid_edge a

goal (1 subgoal):
 1. matched n ([] @ n # [CFG_node (targetnode a)] @ [CFG_node (sourcenode a')]) n'
[PROOF STEP]
by(fastforce intro:matched_bracket_call)
[PROOF STATE]
proof (state)
this:
matched n ([] @ n # [CFG_node (targetnode a)] @ [CFG_node (sourcenode a')]) 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); False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 2. \<And>a Q fs n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True; False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 3. \<And>a Q r fs a' n 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); n' = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 4. \<And>a Q r fs a' x ns x' n 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); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[PROOF STEP]
with \<open>get_proc (sourcenode a') = p\<close>
[PROOF STATE]
proof (chain)
picking this:
get_proc (sourcenode a') = p
matched n ([] @ n # [CFG_node (targetnode a)] @ [CFG_node (sourcenode a')]) n'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
get_proc (sourcenode a') = p
matched n ([] @ n # [CFG_node (targetnode a)] @ [CFG_node (sourcenode a')]) n'

goal (1 subgoal):
 1. \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p

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); False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 2. \<And>a Q fs n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True; False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 3. \<And>a Q r fs a' x ns x' n 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); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[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); False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 2. \<And>a Q fs n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True; False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 3. \<And>a Q r fs a' x ns x' n 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); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[PROOF STEP]
case (sum_SDG_param_summary_edge a Q r fs a' x ns x' n n' ins outs)
[PROOF STATE]
proof (state)
this:
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)
n' = Actual_out (targetnode a', x')
(p, ins, outs) \<in> set procs
x < length ins
x' < length outs

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); False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 2. \<And>a Q fs n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True; False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 3. \<And>a Q r fs a' x ns x' n 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); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>(p,ins,outs) \<in> set procs\<close>
      \<open>x < length ins\<close> \<open>n = Actual_in (sourcenode a,x)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
(p, ins, outs) \<in> set procs
x < length ins
n = Actual_in (sourcenode a, x)
[PROOF STEP]
have "n -p:ins!x\<rightarrow>\<^bsub>in\<^esub> Formal_in (targetnode a,x)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
(p, ins, outs) \<in> set procs
x < length ins
n = Actual_in (sourcenode a, x)

goal (1 subgoal):
 1. n -p:ins ! x\<rightarrow>\<^bsub>in\<^esub> Formal_in (targetnode a, x)
[PROOF STEP]
by(fastforce intro:SDG_param_in_edge)
[PROOF STATE]
proof (state)
this:
n -p:ins ! x\<rightarrow>\<^bsub>in\<^esub> Formal_in (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); False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 2. \<And>a Q fs n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True; False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 3. \<And>a Q r fs a' x ns x' n 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); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[PROOF STEP]
hence "valid_SDG_node n"
[PROOF STATE]
proof (prove)
using this:
n -p:ins ! x\<rightarrow>\<^bsub>in\<^esub> Formal_in (targetnode a, x)

goal (1 subgoal):
 1. valid_SDG_node n
[PROOF STEP]
by(rule SDG_edge_valid_SDG_node)
[PROOF STATE]
proof (state)
this:
valid_SDG_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); False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 2. \<And>a Q fs n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True; False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 3. \<And>a Q r fs a' x ns x' n 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); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[PROOF STEP]
hence "matched n [] n"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n

goal (1 subgoal):
 1. matched n [] n
[PROOF STEP]
by(rule matched_Nil)
[PROOF STATE]
proof (state)
this:
matched n [] 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); False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 2. \<And>a Q fs n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True; False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 3. \<And>a Q r fs a' x ns x' n 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); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[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 (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); False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 2. \<And>a Q fs n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True; False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 3. \<And>a Q r fs a' x ns x' n 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); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>a' \<in> get_return_edges a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
a' \<in> get_return_edges a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
obtain Q' f' where "kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
a' \<in> get_return_edges a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

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 (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); False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 2. \<And>a Q fs n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True; False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 3. \<And>a Q r fs a' x ns x' n 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); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[PROOF STEP]
with \<open>valid_edge a'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
[PROOF STEP]
have "get_proc (sourcenode a') = p"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'

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

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); False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 2. \<And>a Q fs n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True; False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 3. \<And>a Q r fs a' x ns x' n 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); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[PROOF STEP]
from \<open>valid_edge a'\<close> \<open>kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'\<close> \<open>(p,ins,outs) \<in> set procs\<close>
      \<open>x' < length outs\<close> \<open>n' = Actual_out (targetnode a',x')\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
(p, ins, outs) \<in> set procs
x' < length outs
n' = Actual_out (targetnode a', x')
[PROOF STEP]
have "Formal_out (sourcenode a',x') -p:outs!x'\<rightarrow>\<^bsub>out\<^esub> n'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
(p, ins, outs) \<in> set procs
x' < length outs
n' = Actual_out (targetnode a', x')

goal (1 subgoal):
 1. Formal_out (sourcenode a', x') -p:outs ! x'\<rightarrow>\<^bsub>out\<^esub> n'
[PROOF STEP]
by(fastforce intro:SDG_param_out_edge)
[PROOF STATE]
proof (state)
this:
Formal_out (sourcenode a', x') -p:outs ! x'\<rightarrow>\<^bsub>out\<^esub> 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); False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 2. \<And>a Q fs n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True; False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 3. \<And>a Q r fs a' x ns x' n 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); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[PROOF STEP]
from \<open>matched n [] n\<close> \<open>n -p:ins!x\<rightarrow>\<^bsub>in\<^esub> Formal_in (targetnode a,x)\<close>
      \<open>matched (Formal_in (targetnode a,x)) ns (Formal_out (sourcenode a',x'))\<close>
      \<open>Formal_out (sourcenode a',x') -p:outs!x'\<rightarrow>\<^bsub>out\<^esub> n'\<close>
      \<open>a' \<in> get_return_edges a\<close> \<open>n = Actual_in (sourcenode a,x)\<close>
      \<open>n' = Actual_out (targetnode a',x')\<close> \<open>valid_edge a\<close>
[PROOF STATE]
proof (chain)
picking this:
matched n [] n
n -p:ins ! x\<rightarrow>\<^bsub>in\<^esub> Formal_in (targetnode a, x)
matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x'))
Formal_out (sourcenode a', x') -p:outs ! x'\<rightarrow>\<^bsub>out\<^esub> n'
a' \<in> get_return_edges a
n = Actual_in (sourcenode a, x)
n' = Actual_out (targetnode a', x')
valid_edge a
[PROOF STEP]
have "matched n ([]@n#ns@[Formal_out (sourcenode a',x')]) n'"
[PROOF STATE]
proof (prove)
using this:
matched n [] n
n -p:ins ! x\<rightarrow>\<^bsub>in\<^esub> Formal_in (targetnode a, x)
matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x'))
Formal_out (sourcenode a', x') -p:outs ! x'\<rightarrow>\<^bsub>out\<^esub> n'
a' \<in> get_return_edges a
n = Actual_in (sourcenode a, x)
n' = Actual_out (targetnode a', x')
valid_edge a

goal (1 subgoal):
 1. matched n ([] @ n # ns @ [Formal_out (sourcenode a', x')]) n'
[PROOF STEP]
by(fastforce intro:matched_bracket_param)
[PROOF STATE]
proof (state)
this:
matched n ([] @ n # ns @ [Formal_out (sourcenode a', x')]) 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); False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 2. \<And>a Q fs n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True; False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 3. \<And>a Q r fs a' x ns x' n 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); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[PROOF STEP]
with \<open>get_proc (sourcenode a') = p\<close>
[PROOF STATE]
proof (chain)
picking this:
get_proc (sourcenode a') = p
matched n ([] @ n # ns @ [Formal_out (sourcenode a', x')]) n'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
get_proc (sourcenode a') = p
matched n ([] @ n # ns @ [Formal_out (sourcenode a', x')]) n'

goal (1 subgoal):
 1. \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p

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); False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
 2. \<And>a Q fs n n'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fs; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a); False = True; False = True\<rbrakk> \<Longrightarrow> \<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p
[PROOF STEP]
qed simp_all
[PROOF STATE]
proof (state)
this:
\<exists>ns. matched n ns n' \<and> n \<in> set ns \<and> get_proc (parent_node (last ns)) = p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma return_edge_determines_call_and_sum_edge:
  assumes "valid_edge a" and "kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f"
  obtains a' Q' r' fs' where "a \<in> get_return_edges a'" and "valid_edge a'"
  and "kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'"
  and "CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a' Q' r' fs'. \<lbrakk>a \<in> get_return_edges a'; valid_edge a'; kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'; CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a' Q' r' fs'. a \<in> get_return_edges a' \<and> valid_edge a' \<and> kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs' \<and> CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)
[PROOF STEP]
from \<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
[PROOF STEP]
have "CFG_node (sourcenode a) s-p\<rightarrow>\<^bsub>ret\<^esub> CFG_node (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f

goal (1 subgoal):
 1. CFG_node (sourcenode a) s-p\<rightarrow>\<^bsub>ret\<^esub> CFG_node (targetnode a)
[PROOF STEP]
by(fastforce intro:sum_SDG_return_edge)
[PROOF STATE]
proof (state)
this:
CFG_node (sourcenode a) s-p\<rightarrow>\<^bsub>ret\<^esub> CFG_node (targetnode a)

goal (1 subgoal):
 1. \<exists>a' Q' r' fs'. a \<in> get_return_edges a' \<and> valid_edge a' \<and> kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs' \<and> CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)
[PROOF STEP]
from \<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
[PROOF STEP]
obtain a' Q' r' fs' where "valid_edge a'" and "kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'"
    and "a \<in> get_return_edges a'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f

goal (1 subgoal):
 1. (\<And>a' Q' r' fs'. \<lbrakk>valid_edge a'; kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'; a \<in> get_return_edges a'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest:return_needs_call)
[PROOF STATE]
proof (state)
this:
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'
a \<in> get_return_edges a'

goal (1 subgoal):
 1. \<exists>a' Q' r' fs'. a \<in> get_return_edges a' \<and> valid_edge a' \<and> kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs' \<and> CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)
[PROOF STEP]
hence "CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')"
[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. CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')
[PROOF STEP]
by(fastforce intro:sum_SDG_call_edge)
[PROOF STATE]
proof (state)
this:
CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>call\<^esub> CFG_node (targetnode a')

goal (1 subgoal):
 1. \<exists>a' Q' r' fs'. a \<in> get_return_edges a' \<and> valid_edge a' \<and> kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs' \<and> CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)
[PROOF STEP]
from \<open>valid_edge a'\<close> \<open>kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'\<close> \<open>valid_edge a\<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'
valid_edge a
a \<in> get_return_edges a'
[PROOF STEP]
have "CFG_node (targetnode a') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (sourcenode a)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'
valid_edge a
a \<in> get_return_edges a'

goal (1 subgoal):
 1. CFG_node (targetnode a') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (sourcenode a)
[PROOF STEP]
by(fastforce intro!:SDG_proc_entry_exit_cdep)
[PROOF STATE]
proof (state)
this:
CFG_node (targetnode a') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (sourcenode a)

goal (1 subgoal):
 1. \<exists>a' Q' r' fs'. a \<in> get_return_edges a' \<and> valid_edge a' \<and> kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs' \<and> CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)
[PROOF STEP]
hence "valid_SDG_node (CFG_node (targetnode a'))"
[PROOF STATE]
proof (prove)
using this:
CFG_node (targetnode a') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (sourcenode a)

goal (1 subgoal):
 1. valid_SDG_node (CFG_node (targetnode a'))
[PROOF STEP]
by(rule SDG_edge_valid_SDG_node)
[PROOF STATE]
proof (state)
this:
valid_SDG_node (CFG_node (targetnode a'))

goal (1 subgoal):
 1. \<exists>a' Q' r' fs'. a \<in> get_return_edges a' \<and> valid_edge a' \<and> kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs' \<and> CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)
[PROOF STEP]
with \<open>CFG_node (targetnode a') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (sourcenode a)\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (targetnode a') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (sourcenode a)
valid_SDG_node (CFG_node (targetnode a'))
[PROOF STEP]
have "CFG_node (targetnode a') i-[]@[CFG_node (targetnode a')]\<rightarrow>\<^sub>d*
        CFG_node (sourcenode a)"
[PROOF STATE]
proof (prove)
using this:
CFG_node (targetnode a') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (sourcenode a)
valid_SDG_node (CFG_node (targetnode a'))

goal (1 subgoal):
 1. CFG_node (targetnode a') i-[] @ [CFG_node (targetnode a')]\<rightarrow>\<^sub>d* CFG_node (sourcenode a)
[PROOF STEP]
by(fastforce intro:iSp_Append_cdep iSp_Nil)
[PROOF STATE]
proof (state)
this:
CFG_node (targetnode a') i-[] @ [CFG_node (targetnode a')]\<rightarrow>\<^sub>d* CFG_node (sourcenode a)

goal (1 subgoal):
 1. \<exists>a' Q' r' fs'. a \<in> get_return_edges a' \<and> valid_edge a' \<and> kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs' \<and> CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)
[PROOF STEP]
from \<open>valid_SDG_node (CFG_node (targetnode a'))\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node (CFG_node (targetnode a'))
[PROOF STEP]
have "matched (CFG_node (targetnode a')) [] (CFG_node (targetnode a'))"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node (CFG_node (targetnode a'))

goal (1 subgoal):
 1. matched (CFG_node (targetnode a')) [] (CFG_node (targetnode a'))
[PROOF STEP]
by(rule matched_Nil)
[PROOF STATE]
proof (state)
this:
matched (CFG_node (targetnode a')) [] (CFG_node (targetnode a'))

goal (1 subgoal):
 1. \<exists>a' Q' r' fs'. a \<in> get_return_edges a' \<and> valid_edge a' \<and> kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs' \<and> CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)
[PROOF STEP]
with \<open>CFG_node (targetnode a') i-[]@[CFG_node (targetnode a')]\<rightarrow>\<^sub>d*
        CFG_node (sourcenode a)\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (targetnode a') i-[] @ [CFG_node (targetnode a')]\<rightarrow>\<^sub>d* CFG_node (sourcenode a)
matched (CFG_node (targetnode a')) [] (CFG_node (targetnode a'))
[PROOF STEP]
have "matched (CFG_node (targetnode a')) ([]@[CFG_node (targetnode a')])
                (CFG_node (sourcenode a))"
[PROOF STATE]
proof (prove)
using this:
CFG_node (targetnode a') i-[] @ [CFG_node (targetnode a')]\<rightarrow>\<^sub>d* CFG_node (sourcenode a)
matched (CFG_node (targetnode a')) [] (CFG_node (targetnode a'))

goal (1 subgoal):
 1. matched (CFG_node (targetnode a')) ([] @ [CFG_node (targetnode a')]) (CFG_node (sourcenode a))
[PROOF STEP]
by(fastforce intro:matched_Append_intra_SDG_path)
[PROOF STATE]
proof (state)
this:
matched (CFG_node (targetnode a')) ([] @ [CFG_node (targetnode a')]) (CFG_node (sourcenode a))

goal (1 subgoal):
 1. \<exists>a' Q' r' fs'. a \<in> get_return_edges a' \<and> valid_edge a' \<and> kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs' \<and> CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)
[PROOF STEP]
with \<open>valid_edge a'\<close> \<open>kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'\<close> \<open>valid_edge a\<close> \<open>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<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'
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
a \<in> get_return_edges a'
matched (CFG_node (targetnode a')) ([] @ [CFG_node (targetnode a')]) (CFG_node (sourcenode a))
[PROOF STEP]
have "CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
a \<in> get_return_edges a'
matched (CFG_node (targetnode a')) ([] @ [CFG_node (targetnode a')]) (CFG_node (sourcenode a))

goal (1 subgoal):
 1. CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)
[PROOF STEP]
by(fastforce intro!:sum_SDG_call_summary_edge)
[PROOF STATE]
proof (state)
this:
CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)

goal (1 subgoal):
 1. \<exists>a' Q' r' fs'. a \<in> get_return_edges a' \<and> valid_edge a' \<and> kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs' \<and> CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)
[PROOF STEP]
with \<open>a \<in> get_return_edges a'\<close> \<open>valid_edge a'\<close> \<open>kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'\<close>
[PROOF STATE]
proof (chain)
picking this:
a \<in> get_return_edges a'
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'
CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)
[PROOF STEP]
show "\<exists>a' Q' r' fs'. a \<in> get_return_edges a' \<and> valid_edge a' \<and>
    kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs' \<and> CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
a \<in> get_return_edges a'
valid_edge a'
kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs'
CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)

goal (1 subgoal):
 1. \<exists>a' Q' r' fs'. a \<in> get_return_edges a' \<and> valid_edge a' \<and> kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs' \<and> CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>a' Q' r' fs'. a \<in> get_return_edges a' \<and> valid_edge a' \<and> kind a' = Q':r'\<hookrightarrow>\<^bsub>p\<^esub>fs' \<and> CFG_node (sourcenode a') s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a)

goal:
No subgoals!
[PROOF STEP]
qed


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


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

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


[STATEMENT]
lemma intra_SDG_path_is_SDG_path:
  "n i-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-ns\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n i-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> n is-ns\<rightarrow>\<^sub>d* n'
[PROOF STEP]
by(induct rule:intra_SDG_path.induct,
   auto intro:intra_sum_SDG_path.intros SDG_edge_sum_SDG_edge)


[STATEMENT]
lemma is_SDG_path_hd:"\<lbrakk>n is-ns\<rightarrow>\<^sub>d* n'; ns \<noteq> []\<rbrakk> \<Longrightarrow> hd ns = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n'; ns \<noteq> []\<rbrakk> \<Longrightarrow> hd ns = n
[PROOF STEP]
apply(induct rule:intra_sum_SDG_path.induct)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n. \<lbrakk>valid_SDG_node n; [] \<noteq> []\<rbrakk> \<Longrightarrow> hd [] = n
 2. \<And>n ns n'' n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; ns \<noteq> [] \<Longrightarrow> hd ns = n; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'; ns @ [n''] \<noteq> []\<rbrakk> \<Longrightarrow> hd (ns @ [n'']) = n
 3. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; ns \<noteq> [] \<Longrightarrow> hd ns = n; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'; ns @ [n''] \<noteq> []\<rbrakk> \<Longrightarrow> hd (ns @ [n'']) = n
 4. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; ns \<noteq> [] \<Longrightarrow> hd ns = n; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'; ns @ [n''] \<noteq> []\<rbrakk> \<Longrightarrow> hd (ns @ [n'']) = n
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; ns \<noteq> [] \<Longrightarrow> hd ns = n; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'; ns @ [n''] \<noteq> []\<rbrakk> \<Longrightarrow> hd (ns @ [n'']) = n
 2. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; ns \<noteq> [] \<Longrightarrow> hd ns = n; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'; ns @ [n''] \<noteq> []\<rbrakk> \<Longrightarrow> hd (ns @ [n'']) = n
 3. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; ns \<noteq> [] \<Longrightarrow> hd ns = n; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'; ns @ [n''] \<noteq> []\<rbrakk> \<Longrightarrow> hd (ns @ [n'']) = n
[PROOF STEP]
by(case_tac ns,auto elim:intra_sum_SDG_path.cases)+