[STATEMENT]
lemma in_proc_cdep_SDG_path:
  assumes "n -as\<rightarrow>\<^sub>\<iota>* n'" and "n \<noteq> n'" and "n' \<noteq> (_Exit_)" and "valid_edge a"
  and "kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs" and "targetnode a = n"
  obtains ns where "CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n'"
  and "ns \<noteq> []" and "\<forall>n'' \<in> set ns. parent_node n'' \<in> set(sourcenodes as)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ns. \<lbrakk>CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n'; ns \<noteq> []; \<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
show "\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and>
             ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
proof(cases "\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow>
                    ax \<notin> get_return_edges a")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a

goal (2 subgoals):
 1. \<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>n -as\<rightarrow>\<^sub>\<iota>* n'\<close> \<open>n \<noteq> n'\<close> \<open>n' \<noteq> (_Exit_)\<close>
      \<open>\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>\<^sub>\<iota>* n'
n \<noteq> n'
n' \<noteq> (_Exit_)
\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a
[PROOF STEP]
show "\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and>
      (\<forall>n'' \<in> set ns. parent_node n'' \<in> set(sourcenodes as))"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>\<^sub>\<iota>* n'
n \<noteq> n'
n' \<noteq> (_Exit_)
\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a

goal (1 subgoal):
 1. \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
proof(induct as arbitrary:n' rule:length_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs n'. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. n -ys\<rightarrow>\<^sub>\<iota>* x \<longrightarrow> n \<noteq> x \<longrightarrow> x \<noteq> (_Exit_) \<longrightarrow> (\<forall>ax. valid_edge ax \<and> sourcenode ax = x \<longrightarrow> ax \<notin> get_return_edges a) \<longrightarrow> (\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node x \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes ys)))); n -xs\<rightarrow>\<^sub>\<iota>* n'; n \<noteq> n'; n' \<noteq> (_Exit_); \<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes xs))
[PROOF STEP]
fix as n'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs n'. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. n -ys\<rightarrow>\<^sub>\<iota>* x \<longrightarrow> n \<noteq> x \<longrightarrow> x \<noteq> (_Exit_) \<longrightarrow> (\<forall>ax. valid_edge ax \<and> sourcenode ax = x \<longrightarrow> ax \<notin> get_return_edges a) \<longrightarrow> (\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node x \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes ys)))); n -xs\<rightarrow>\<^sub>\<iota>* n'; n \<noteq> n'; n' \<noteq> (_Exit_); \<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes xs))
[PROOF STEP]
assume IH:"\<forall>as'. length as' < length as \<longrightarrow>
        (\<forall>n''. n -as'\<rightarrow>\<^sub>\<iota>* n'' \<longrightarrow> n \<noteq> n'' \<longrightarrow> n'' \<noteq> (_Exit_) \<longrightarrow>
          (\<forall>ax. valid_edge ax \<and> sourcenode ax = n'' \<longrightarrow> ax \<notin> get_return_edges a) \<longrightarrow>
            (\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n'' \<and> ns \<noteq> [] \<and>
                  (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as'))))"
        and "n -as\<rightarrow>\<^sub>\<iota>* n'" and "n \<noteq> n'" and "n' \<noteq> (_Exit_)"
        and "\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a"
[PROOF STATE]
proof (state)
this:
\<forall>as'. length as' < length as \<longrightarrow> (\<forall>n''. n -as'\<rightarrow>\<^sub>\<iota>* n'' \<longrightarrow> n \<noteq> n'' \<longrightarrow> n'' \<noteq> (_Exit_) \<longrightarrow> (\<forall>ax. valid_edge ax \<and> sourcenode ax = n'' \<longrightarrow> ax \<notin> get_return_edges a) \<longrightarrow> (\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n'' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as'))))
n -as\<rightarrow>\<^sub>\<iota>* n'
n \<noteq> n'
n' \<noteq> (_Exit_)
\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a

goal (1 subgoal):
 1. \<And>xs n'. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. n -ys\<rightarrow>\<^sub>\<iota>* x \<longrightarrow> n \<noteq> x \<longrightarrow> x \<noteq> (_Exit_) \<longrightarrow> (\<forall>ax. valid_edge ax \<and> sourcenode ax = x \<longrightarrow> ax \<notin> get_return_edges a) \<longrightarrow> (\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node x \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes ys)))); n -xs\<rightarrow>\<^sub>\<iota>* n'; n \<noteq> n'; n' \<noteq> (_Exit_); \<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes xs))
[PROOF STEP]
show "\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and>
                 (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
proof(cases "method_exit n'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. method_exit n' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> method_exit n' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
method_exit n'

goal (2 subgoals):
 1. method_exit n' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> method_exit n' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
method_exit n'

goal (1 subgoal):
 1. \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
proof(rule method_exit_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n' = (_Exit_) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<And>a Q f p. \<lbrakk>n' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
assume "n' = (_Exit_)"
[PROOF STATE]
proof (state)
this:
n' = (_Exit_)

goal (2 subgoals):
 1. n' = (_Exit_) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<And>a Q f p. \<lbrakk>n' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>n' \<noteq> (_Exit_)\<close>
[PROOF STATE]
proof (chain)
picking this:
n' \<noteq> (_Exit_)
n' = (_Exit_)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
n' \<noteq> (_Exit_)
n' = (_Exit_)

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

goal (2 subgoals):
 1. n' = (_Exit_) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<And>a Q f p. \<lbrakk>n' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))

goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>n' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>n' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
fix a' Q' f' p'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>n' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
assume "n' = sourcenode a'" and "valid_edge a'" and "kind a' = Q'\<hookleftarrow>\<^bsub>p'\<^esub>f'"
[PROOF STATE]
proof (state)
this:
n' = sourcenode a'
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p'\<^esub>f'

goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>n' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[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 (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>n' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>n -as\<rightarrow>\<^sub>\<iota>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>\<^sub>\<iota>* n'
[PROOF STEP]
have "get_proc n = get_proc n'"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>\<^sub>\<iota>* n'

goal (1 subgoal):
 1. get_proc n = get_proc n'
[PROOF STEP]
by(rule intra_path_get_procs)
[PROOF STATE]
proof (state)
this:
get_proc n = get_proc n'

goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>n' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>get_proc(targetnode a) = p\<close> \<open>targetnode a = n\<close>
[PROOF STATE]
proof (chain)
picking this:
get_proc (targetnode a) = p
targetnode a = n
get_proc n = get_proc n'
[PROOF STEP]
have "get_proc (targetnode a) = get_proc n'"
[PROOF STATE]
proof (prove)
using this:
get_proc (targetnode a) = p
targetnode a = n
get_proc n = get_proc n'

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

goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>n' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[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 "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 (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>n' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>n' = sourcenode a'\<close> \<open>get_proc (targetnode a) = get_proc n'\<close>
            \<open>get_proc (targetnode a) = p\<close>
[PROOF STATE]
proof (chain)
picking this:
n' = sourcenode a'
get_proc (targetnode a) = get_proc n'
get_proc (targetnode a) = p
get_proc (sourcenode a') = p'
[PROOF STEP]
have "p = p'"
[PROOF STATE]
proof (prove)
using this:
n' = sourcenode a'
get_proc (targetnode a) = get_proc n'
get_proc (targetnode a) = p
get_proc (sourcenode a') = p'

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

goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>n' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>valid_edge a'\<close> \<open>kind a' = Q'\<hookleftarrow>\<^bsub>p'\<^esub>f'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p'\<^esub>f'
p = p'
[PROOF STEP]
obtain ax where "valid_edge ax" and "\<exists>Q r fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs"
            and "a' \<in> get_return_edges ax"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p'\<^esub>f'
p = p'

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

goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>n' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
hence "CFG_node (targetnode ax) \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (sourcenode a')"
[PROOF STATE]
proof (prove)
using this:
valid_edge ax
\<exists>Q r fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
a' \<in> get_return_edges ax

goal (1 subgoal):
 1. CFG_node (targetnode ax) \<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 ax) \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (sourcenode a')

goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>n' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>valid_edge ax\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge ax
CFG_node (targetnode ax) \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (sourcenode a')
[PROOF STEP]
have "CFG_node (targetnode ax) cd-[]@[CFG_node (targetnode ax)]\<rightarrow>\<^sub>d*
            CFG_node (sourcenode a')"
[PROOF STATE]
proof (prove)
using this:
valid_edge ax
CFG_node (targetnode ax) \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (sourcenode a')

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

goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>n' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>valid_edge ax\<close>
            \<open>\<exists>Q r fs. kind ax = 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
valid_edge ax
\<exists>Q r fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
have "targetnode a = targetnode ax"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
valid_edge ax
\<exists>Q r fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

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

goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>n' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>n -as\<rightarrow>\<^sub>\<iota>* n'\<close> \<open>n \<noteq> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>\<^sub>\<iota>* n'
n \<noteq> n'
[PROOF STEP]
have "as \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>\<^sub>\<iota>* n'
n \<noteq> n'

goal (1 subgoal):
 1. as \<noteq> []
[PROOF STEP]
by(fastforce elim:path.cases simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
as \<noteq> []

goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>n' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>n -as\<rightarrow>\<^sub>\<iota>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>\<^sub>\<iota>* n'
as \<noteq> []
[PROOF STEP]
have "hd (sourcenodes as) = n"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>\<^sub>\<iota>* n'
as \<noteq> []

goal (1 subgoal):
 1. hd (sourcenodes as) = n
[PROOF STEP]
by(fastforce intro:path_sourcenode simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
hd (sourcenodes as) = n

goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>n' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
hd (sourcenodes as) = n

goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>n' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>as \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
as \<noteq> []
[PROOF STEP]
have "hd (sourcenodes as) \<in> set (sourcenodes as)"
[PROOF STATE]
proof (prove)
using this:
as \<noteq> []

goal (1 subgoal):
 1. hd (sourcenodes as) \<in> set (sourcenodes as)
[PROOF STEP]
by(fastforce intro:hd_in_set simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
hd (sourcenodes as) \<in> set (sourcenodes as)

goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>n' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
hd (sourcenodes as) = n
hd (sourcenodes as) \<in> set (sourcenodes as)
[PROOF STEP]
have "n \<in> set (sourcenodes as)"
[PROOF STATE]
proof (prove)
using this:
hd (sourcenodes as) = n
hd (sourcenodes as) \<in> set (sourcenodes as)

goal (1 subgoal):
 1. n \<in> set (sourcenodes as)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n \<in> set (sourcenodes as)

goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>n' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>n' = sourcenode a'\<close> \<open>targetnode a = targetnode ax\<close>
            \<open>targetnode a = n\<close>
            \<open>CFG_node (targetnode ax) cd-[]@[CFG_node (targetnode ax)]\<rightarrow>\<^sub>d*
            CFG_node (sourcenode a')\<close>
[PROOF STATE]
proof (chain)
picking this:
n' = sourcenode a'
targetnode a = targetnode ax
targetnode a = n
CFG_node (targetnode ax) cd-[] @ [CFG_node (targetnode ax)]\<rightarrow>\<^sub>d* CFG_node (sourcenode a')
n \<in> set (sourcenodes as)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n' = sourcenode a'
targetnode a = targetnode ax
targetnode a = n
CFG_node (targetnode ax) cd-[] @ [CFG_node (targetnode ax)]\<rightarrow>\<^sub>d* CFG_node (sourcenode a')
n \<in> set (sourcenodes as)

goal (1 subgoal):
 1. \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))

goal (1 subgoal):
 1. \<not> method_exit n' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> method_exit n' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> method_exit n'

goal (1 subgoal):
 1. \<not> method_exit n' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[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]
obtain a'
          where "a' \<in> get_return_edges a"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. (\<And>a'. a' \<in> get_return_edges a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce dest:get_return_edge_call)
[PROOF STATE]
proof (state)
this:
a' \<in> get_return_edges a

goal (1 subgoal):
 1. \<not> method_exit n' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[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
a' \<in> get_return_edges a
[PROOF STEP]
obtain Q' f' where "kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
a' \<in> get_return_edges a

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

goal (1 subgoal):
 1. \<not> method_exit n' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<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
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
[PROOF STEP]
obtain a''
          where "valid_edge a''" and "sourcenode a'' = targetnode a"
          and "targetnode a'' = sourcenode a'" and "kind a'' = (\<lambda>cf. False)\<^sub>\<surd>"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
a' \<in> get_return_edges a
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'

goal (1 subgoal):
 1. (\<And>a''. \<lbrakk>valid_edge a''; sourcenode a'' = targetnode a; targetnode a'' = sourcenode a'; kind a'' = (\<lambda>cf. False)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by -(drule intra_proc_additional_edge,auto)
[PROOF STATE]
proof (state)
this:
valid_edge a''
sourcenode a'' = targetnode a
targetnode a'' = sourcenode a'
kind a'' = (\<lambda>cf. False)\<^sub>\<surd>

goal (1 subgoal):
 1. \<not> method_exit n' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[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 (1 subgoal):
 1. \<not> method_exit n' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
have "\<exists>ax asx zs. n -ax#asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax#asx)) \<and>
                          as = (ax#asx)@zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
proof(cases "n' \<in> set (sourcenodes as)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n' \<in> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
 2. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n' \<in> set (sourcenodes as)

goal (2 subgoals):
 1. n' \<in> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
 2. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
hence "\<exists>n'' \<in> set(sourcenodes as). n' = n''"
[PROOF STATE]
proof (prove)
using this:
n' \<in> set (sourcenodes as)

goal (1 subgoal):
 1. \<exists>n''\<in>set (sourcenodes as). n' = n''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>n''\<in>set (sourcenodes as). n' = n''

goal (2 subgoals):
 1. n' \<in> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
 2. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>n''\<in>set (sourcenodes as). n' = n''
[PROOF STEP]
obtain ns' ns'' where "sourcenodes as = ns'@n'#ns''"
            and "\<forall>n'' \<in> set ns'. n' \<noteq> n''"
[PROOF STATE]
proof (prove)
using this:
\<exists>n''\<in>set (sourcenodes as). n' = n''

goal (1 subgoal):
 1. (\<And>ns' ns''. \<lbrakk>sourcenodes as = ns' @ n' # ns''; \<forall>n''\<in>set ns'. n' \<noteq> n''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim!:split_list_first_propE)
[PROOF STATE]
proof (state)
this:
sourcenodes as = ns' @ n' # ns''
\<forall>n''\<in>set ns'. n' \<noteq> n''

goal (2 subgoals):
 1. n' \<in> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
 2. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
from \<open>sourcenodes as = ns'@n'#ns''\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenodes as = ns' @ n' # ns''
[PROOF STEP]
obtain xs ys ax
            where "sourcenodes xs = ns'" and "as = xs@ax#ys"
            and "sourcenode ax = n'"
[PROOF STATE]
proof (prove)
using this:
sourcenodes as = ns' @ n' # ns''

goal (1 subgoal):
 1. (\<And>xs ax ys. \<lbrakk>sourcenodes xs = ns'; as = xs @ ax # ys; sourcenode ax = n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:map_append_append_maps simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
sourcenodes xs = ns'
as = xs @ ax # ys
sourcenode ax = n'

goal (2 subgoals):
 1. n' \<in> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
 2. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
from \<open>\<forall>n'' \<in> set ns'. n' \<noteq> n''\<close> \<open>sourcenodes xs = ns'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>n''\<in>set ns'. n' \<noteq> n''
sourcenodes xs = ns'
[PROOF STEP]
have "n' \<notin> set(sourcenodes xs)"
[PROOF STATE]
proof (prove)
using this:
\<forall>n''\<in>set ns'. n' \<noteq> n''
sourcenodes xs = ns'

goal (1 subgoal):
 1. n' \<notin> set (sourcenodes xs)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
n' \<notin> set (sourcenodes xs)

goal (2 subgoals):
 1. n' \<in> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
 2. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
from \<open>n -as\<rightarrow>\<^sub>\<iota>* n'\<close> \<open>as = xs@ax#ys\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>\<^sub>\<iota>* n'
as = xs @ ax # ys
[PROOF STEP]
have "n -xs@ax#ys\<rightarrow>\<^sub>\<iota>* n'"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>\<^sub>\<iota>* n'
as = xs @ ax # ys

goal (1 subgoal):
 1. n -xs @ ax # ys\<rightarrow>\<^sub>\<iota>* n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n -xs @ ax # ys\<rightarrow>\<^sub>\<iota>* n'

goal (2 subgoals):
 1. n' \<in> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
 2. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
with \<open>sourcenode ax = n'\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode ax = n'
n -xs @ ax # ys\<rightarrow>\<^sub>\<iota>* n'
[PROOF STEP]
have "n -xs\<rightarrow>\<^sub>\<iota>* n'"
[PROOF STATE]
proof (prove)
using this:
sourcenode ax = n'
n -xs @ ax # ys\<rightarrow>\<^sub>\<iota>* n'

goal (1 subgoal):
 1. n -xs\<rightarrow>\<^sub>\<iota>* n'
[PROOF STEP]
by(fastforce dest:path_split simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
n -xs\<rightarrow>\<^sub>\<iota>* n'

goal (2 subgoals):
 1. n' \<in> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
 2. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
with \<open>n \<noteq> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> n'
n -xs\<rightarrow>\<^sub>\<iota>* n'
[PROOF STEP]
have "xs \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> n'
n -xs\<rightarrow>\<^sub>\<iota>* n'

goal (1 subgoal):
 1. xs \<noteq> []
[PROOF STEP]
by(fastforce simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
xs \<noteq> []

goal (2 subgoals):
 1. n' \<in> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
 2. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
with \<open>n' \<notin> set(sourcenodes xs)\<close> \<open>n -xs\<rightarrow>\<^sub>\<iota>* n'\<close> \<open>as = xs@ax#ys\<close>
[PROOF STATE]
proof (chain)
picking this:
n' \<notin> set (sourcenodes xs)
n -xs\<rightarrow>\<^sub>\<iota>* n'
as = xs @ ax # ys
xs \<noteq> []
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n' \<notin> set (sourcenodes xs)
n -xs\<rightarrow>\<^sub>\<iota>* n'
as = xs @ ax # ys
xs \<noteq> []

goal (1 subgoal):
 1. \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
by(cases xs) auto
[PROOF STATE]
proof (state)
this:
\<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs

goal (1 subgoal):
 1. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n' \<notin> set (sourcenodes as)

goal (1 subgoal):
 1. n' \<notin> set (sourcenodes as) \<Longrightarrow> \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
with \<open>n -as\<rightarrow>\<^sub>\<iota>* n'\<close> \<open>n \<noteq> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>\<^sub>\<iota>* n'
n \<noteq> n'
n' \<notin> set (sourcenodes as)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>\<^sub>\<iota>* n'
n \<noteq> n'
n' \<notin> set (sourcenodes as)

goal (1 subgoal):
 1. \<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
by(cases as)(auto simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
\<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs

goal (1 subgoal):
 1. \<not> method_exit n' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs
[PROOF STEP]
obtain ax asx zs where "n -ax#asx\<rightarrow>\<^sub>\<iota>* n'"
          and "n' \<notin> set (sourcenodes (ax#asx))" and "as = (ax#asx)@zs"
[PROOF STATE]
proof (prove)
using this:
\<exists>ax asx zs. n -ax # asx\<rightarrow>\<^sub>\<iota>* n' \<and> n' \<notin> set (sourcenodes (ax # asx)) \<and> as = (ax # asx) @ zs

goal (1 subgoal):
 1. (\<And>ax asx zs. \<lbrakk>n -ax # asx\<rightarrow>\<^sub>\<iota>* n'; n' \<notin> set (sourcenodes (ax # asx)); as = (ax # asx) @ zs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n -ax # asx\<rightarrow>\<^sub>\<iota>* n'
n' \<notin> set (sourcenodes (ax # asx))
as = (ax # asx) @ zs

goal (1 subgoal):
 1. \<not> method_exit n' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>n -ax#asx\<rightarrow>\<^sub>\<iota>* n'\<close> \<open>n' \<noteq> (_Exit_)\<close>
[PROOF STATE]
proof (chain)
picking this:
n -ax # asx\<rightarrow>\<^sub>\<iota>* n'
n' \<noteq> (_Exit_)
[PROOF STEP]
have "inner_node n'"
[PROOF STATE]
proof (prove)
using this:
n -ax # asx\<rightarrow>\<^sub>\<iota>* n'
n' \<noteq> (_Exit_)

goal (1 subgoal):
 1. inner_node n'
[PROOF STEP]
by(fastforce intro:path_valid_node simp:inner_node_def intra_path_def)
[PROOF STATE]
proof (state)
this:
inner_node n'

goal (1 subgoal):
 1. \<not> method_exit n' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>targetnode a = n\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
targetnode a = n
[PROOF STEP]
have "valid_node n"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
targetnode a = n

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

goal (1 subgoal):
 1. \<not> method_exit n' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
proof(cases "\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and>
            valid_edge a'' \<and> intra_kind(kind a'') \<longrightarrow>
            n' postdominates targetnode a''")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a''

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>targetnode a = n\<close> \<open>sourcenode a'' = targetnode a\<close>
            \<open>kind a'' = (\<lambda>cf. False)\<^sub>\<surd>\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a = n
sourcenode a'' = targetnode a
kind a'' = (\<lambda>cf. False)\<^sub>\<surd>
[PROOF STEP]
have "sourcenode a'' = n" and "intra_kind(kind a'')"
[PROOF STATE]
proof (prove)
using this:
targetnode a = n
sourcenode a'' = targetnode a
kind a'' = (\<lambda>cf. False)\<^sub>\<surd>

goal (1 subgoal):
 1. sourcenode a'' = n &&& intra_kind (kind a'')
[PROOF STEP]
by(auto simp:intra_kind_def)
[PROOF STATE]
proof (state)
this:
sourcenode a'' = n
intra_kind (kind a'')

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
sourcenode a'' = n
intra_kind (kind a'')

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
fix as'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
assume "targetnode a'' -as'\<rightarrow>\<^sub>\<iota>* n'"
[PROOF STATE]
proof (state)
this:
targetnode a'' -as'\<rightarrow>\<^sub>\<iota>* n'

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>valid_edge a'\<close> \<open>targetnode a'' = sourcenode a'\<close>
              \<open>a' \<in> get_return_edges a\<close>
              \<open>\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
targetnode a'' = sourcenode a'
a' \<in> get_return_edges a
\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a
[PROOF STEP]
have "targetnode a'' \<noteq> n'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
targetnode a'' = sourcenode a'
a' \<in> get_return_edges a
\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a

goal (1 subgoal):
 1. targetnode a'' \<noteq> n'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
targetnode a'' \<noteq> n'

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>targetnode a'' -as'\<rightarrow>\<^sub>\<iota>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a'' -as'\<rightarrow>\<^sub>\<iota>* n'
targetnode a'' \<noteq> n'
[PROOF STEP]
obtain ax' where "valid_edge ax'"
              and "targetnode a'' = sourcenode ax'" and "intra_kind(kind ax')"
[PROOF STATE]
proof (prove)
using this:
targetnode a'' -as'\<rightarrow>\<^sub>\<iota>* n'
targetnode a'' \<noteq> n'

goal (1 subgoal):
 1. (\<And>ax'. \<lbrakk>valid_edge ax'; targetnode a'' = sourcenode ax'; intra_kind (kind ax')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(clarsimp simp:intra_path_def)(erule path.cases,fastforce+)
[PROOF STATE]
proof (state)
this:
valid_edge ax'
targetnode a'' = sourcenode ax'
intra_kind (kind ax')

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>valid_edge a'\<close> \<open>kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'\<close> \<open>valid_edge ax'\<close>
              \<open>targetnode a'' = sourcenode a'\<close> \<open>targetnode a'' = sourcenode ax'\<close>
              \<open>intra_kind(kind ax')\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
valid_edge ax'
targetnode a'' = sourcenode a'
targetnode a'' = sourcenode ax'
intra_kind (kind ax')
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
valid_edge ax'
targetnode a'' = sourcenode a'
targetnode a'' = sourcenode ax'
intra_kind (kind ax')

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

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
targetnode a'' -?as'2\<rightarrow>\<^sub>\<iota>* n' \<Longrightarrow> False

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
hence "\<not> n' postdominates targetnode a''"
[PROOF STATE]
proof (prove)
using this:
targetnode a'' -?as'2\<rightarrow>\<^sub>\<iota>* n' \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> n' postdominates targetnode a''
[PROOF STEP]
by(fastforce elim:postdominate_implies_inner_path)
[PROOF STATE]
proof (state)
this:
\<not> n' postdominates targetnode a''

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>n -ax#asx\<rightarrow>\<^sub>\<iota>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -ax # asx\<rightarrow>\<^sub>\<iota>* n'
[PROOF STEP]
have "sourcenode ax = n"
[PROOF STATE]
proof (prove)
using this:
n -ax # asx\<rightarrow>\<^sub>\<iota>* n'

goal (1 subgoal):
 1. sourcenode ax = n
[PROOF STEP]
by(auto intro:path_split_Cons simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
sourcenode ax = n

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>n -ax#asx\<rightarrow>\<^sub>\<iota>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -ax # asx\<rightarrow>\<^sub>\<iota>* n'
[PROOF STEP]
have "n -[]@ax#asx\<rightarrow>\<^sub>\<iota>* n'"
[PROOF STATE]
proof (prove)
using this:
n -ax # asx\<rightarrow>\<^sub>\<iota>* n'

goal (1 subgoal):
 1. n -[] @ ax # asx\<rightarrow>\<^sub>\<iota>* n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n -[] @ ax # asx\<rightarrow>\<^sub>\<iota>* n'

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from this \<open>sourcenode a'' = n\<close> \<open>sourcenode ax = n\<close> True
            \<open>n' \<notin> set (sourcenodes (ax#asx))\<close> \<open>valid_edge a''\<close> \<open>intra_kind(kind a'')\<close>
            \<open>inner_node n'\<close> \<open>\<not> method_exit n'\<close> \<open>\<not> n' postdominates targetnode a''\<close>
[PROOF STATE]
proof (chain)
picking this:
n -[] @ ax # asx\<rightarrow>\<^sub>\<iota>* n'
sourcenode a'' = n
sourcenode ax = n
\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a''
n' \<notin> set (sourcenodes (ax # asx))
valid_edge a''
intra_kind (kind a'')
inner_node n'
\<not> method_exit n'
\<not> n' postdominates targetnode a''
[PROOF STEP]
have "n controls n'"
[PROOF STATE]
proof (prove)
using this:
n -[] @ ax # asx\<rightarrow>\<^sub>\<iota>* n'
sourcenode a'' = n
sourcenode ax = n
\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a''
n' \<notin> set (sourcenodes (ax # asx))
valid_edge a''
intra_kind (kind a'')
inner_node n'
\<not> method_exit n'
\<not> n' postdominates targetnode a''

goal (1 subgoal):
 1. n controls n'
[PROOF STEP]
by(fastforce intro!:which_node_intra_standard_control_dependence_source)
[PROOF STATE]
proof (state)
this:
n controls n'

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
hence "CFG_node n \<longrightarrow>\<^bsub>cd\<^esub> CFG_node n'"
[PROOF STATE]
proof (prove)
using this:
n controls n'

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

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>valid_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_node n
CFG_node n \<longrightarrow>\<^bsub>cd\<^esub> CFG_node n'
[PROOF STEP]
have "CFG_node n cd-[]@[CFG_node n]\<rightarrow>\<^sub>d* CFG_node n'"
[PROOF STATE]
proof (prove)
using this:
valid_node n
CFG_node n \<longrightarrow>\<^bsub>cd\<^esub> CFG_node n'

goal (1 subgoal):
 1. CFG_node n cd-[] @ [CFG_node n]\<rightarrow>\<^sub>d* CFG_node n'
[PROOF STEP]
by(fastforce intro:cdSp_Append_cdep cdSp_Nil)
[PROOF STATE]
proof (state)
this:
CFG_node n cd-[] @ [CFG_node n]\<rightarrow>\<^sub>d* CFG_node n'

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
CFG_node n cd-[] @ [CFG_node n]\<rightarrow>\<^sub>d* CFG_node n'

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>as = (ax#asx)@zs\<close> \<open>sourcenode ax = n\<close>
[PROOF STATE]
proof (chain)
picking this:
as = (ax # asx) @ zs
sourcenode ax = n
[PROOF STEP]
have "n \<in> set(sourcenodes as)"
[PROOF STATE]
proof (prove)
using this:
as = (ax # asx) @ zs
sourcenode ax = n

goal (1 subgoal):
 1. n \<in> set (sourcenodes as)
[PROOF STEP]
by(simp add:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
n \<in> set (sourcenodes as)

goal (2 subgoals):
 1. \<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
CFG_node n cd-[] @ [CFG_node n]\<rightarrow>\<^sub>d* CFG_node n'
n \<in> set (sourcenodes as)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node n cd-[] @ [CFG_node n]\<rightarrow>\<^sub>d* CFG_node n'
n \<in> set (sourcenodes as)

goal (1 subgoal):
 1. \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'')

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
hence "\<exists>a' \<in> set asx. \<exists>a''. sourcenode a' = sourcenode a'' \<and>
            valid_edge a'' \<and> intra_kind(kind a'') \<and>
            \<not> n' postdominates targetnode a''"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'')

goal (1 subgoal):
 1. \<exists>a'\<in>set asx. \<exists>a''. sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a''
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>a'\<in>set asx. \<exists>a''. sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a''

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a'\<in>set asx. \<exists>a''. sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a''
[PROOF STEP]
obtain ax' asx' asx'' where "asx = asx'@ax'#asx'' \<and>
            (\<exists>a''. sourcenode ax' = sourcenode a'' \<and> valid_edge a'' \<and>
            intra_kind(kind a'') \<and> \<not> n' postdominates targetnode a'') \<and>
            (\<forall>z \<in> set asx''. \<not> (\<exists>a''. sourcenode z = sourcenode a'' \<and>
            valid_edge a'' \<and> intra_kind(kind a'') \<and>
            \<not> n' postdominates targetnode a''))"
[PROOF STATE]
proof (prove)
using this:
\<exists>a'\<in>set asx. \<exists>a''. sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a''

goal (1 subgoal):
 1. (\<And>asx' ax' asx''. asx = asx' @ ax' # asx'' \<and> (\<exists>a''. sourcenode ax' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a'') \<and> (\<forall>z\<in>set asx''. \<nexists>a''. sourcenode z = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a'') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast elim!:split_list_last_propE)
[PROOF STATE]
proof (state)
this:
asx = asx' @ ax' # asx'' \<and> (\<exists>a''. sourcenode ax' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a'') \<and> (\<forall>z\<in>set asx''. \<nexists>a''. sourcenode z = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a'')

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
asx = asx' @ ax' # asx'' \<and> (\<exists>a''. sourcenode ax' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a'') \<and> (\<forall>z\<in>set asx''. \<nexists>a''. sourcenode z = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a'')
[PROOF STEP]
obtain ai where "asx = asx'@ax'#asx''"
            and "sourcenode ax' = sourcenode ai"
            and "valid_edge ai" and "intra_kind(kind ai)"
            and "\<not> n' postdominates targetnode ai"
            and "\<forall>z \<in> set asx''. \<not> (\<exists>a''. sourcenode z = sourcenode a'' \<and>
            valid_edge a'' \<and> intra_kind(kind a'') \<and>
            \<not> n' postdominates targetnode a'')"
[PROOF STATE]
proof (prove)
using this:
asx = asx' @ ax' # asx'' \<and> (\<exists>a''. sourcenode ax' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a'') \<and> (\<forall>z\<in>set asx''. \<nexists>a''. sourcenode z = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a'')

goal (1 subgoal):
 1. (\<And>ai. \<lbrakk>asx = asx' @ ax' # asx''; sourcenode ax' = sourcenode ai; valid_edge ai; intra_kind (kind ai); \<not> n' postdominates targetnode ai; \<forall>z\<in>set asx''. \<nexists>a''. sourcenode z = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
asx = asx' @ ax' # asx''
sourcenode ax' = sourcenode ai
valid_edge ai
intra_kind (kind ai)
\<not> n' postdominates targetnode ai
\<forall>z\<in>set asx''. \<nexists>a''. sourcenode z = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a''

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>asx = asx'@ax'#asx''\<close> \<open>n -ax#asx\<rightarrow>\<^sub>\<iota>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
asx = asx' @ ax' # asx''
n -ax # asx\<rightarrow>\<^sub>\<iota>* n'
[PROOF STEP]
have "n -(ax#asx')@ax'#asx''\<rightarrow>\<^sub>\<iota>* n'"
[PROOF STATE]
proof (prove)
using this:
asx = asx' @ ax' # asx''
n -ax # asx\<rightarrow>\<^sub>\<iota>* n'

goal (1 subgoal):
 1. n -(ax # asx') @ ax' # asx''\<rightarrow>\<^sub>\<iota>* n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n -(ax # asx') @ ax' # asx''\<rightarrow>\<^sub>\<iota>* n'

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>n' \<notin> set (sourcenodes (ax#asx))\<close> \<open>asx = asx'@ax'#asx''\<close>
[PROOF STATE]
proof (chain)
picking this:
n' \<notin> set (sourcenodes (ax # asx))
asx = asx' @ ax' # asx''
[PROOF STEP]
have "n' \<notin> set (sourcenodes (ax'#asx''))"
[PROOF STATE]
proof (prove)
using this:
n' \<notin> set (sourcenodes (ax # asx))
asx = asx' @ ax' # asx''

goal (1 subgoal):
 1. n' \<notin> set (sourcenodes (ax' # asx''))
[PROOF STEP]
by(auto simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
n' \<notin> set (sourcenodes (ax' # asx''))

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>inner_node n'\<close> \<open>\<not> n' postdominates targetnode ai\<close>
            \<open>n -(ax#asx')@ax'#asx''\<rightarrow>\<^sub>\<iota>* n'\<close> \<open>sourcenode ax' = sourcenode ai\<close>
            \<open>\<forall>z \<in> set asx''. \<not> (\<exists>a''. sourcenode z = sourcenode a'' \<and>
            valid_edge a'' \<and> intra_kind(kind a'') \<and>
            \<not> n' postdominates targetnode a'')\<close>
            \<open>valid_edge ai\<close> \<open>intra_kind(kind ai)\<close> \<open>\<not> method_exit n'\<close>
[PROOF STATE]
proof (chain)
picking this:
inner_node n'
\<not> n' postdominates targetnode ai
n -(ax # asx') @ ax' # asx''\<rightarrow>\<^sub>\<iota>* n'
sourcenode ax' = sourcenode ai
\<forall>z\<in>set asx''. \<nexists>a''. sourcenode z = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a''
valid_edge ai
intra_kind (kind ai)
\<not> method_exit n'
n' \<notin> set (sourcenodes (ax' # asx''))
[PROOF STEP]
have "sourcenode ax' controls n'"
[PROOF STATE]
proof (prove)
using this:
inner_node n'
\<not> n' postdominates targetnode ai
n -(ax # asx') @ ax' # asx''\<rightarrow>\<^sub>\<iota>* n'
sourcenode ax' = sourcenode ai
\<forall>z\<in>set asx''. \<nexists>a''. sourcenode z = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<and> \<not> n' postdominates targetnode a''
valid_edge ai
intra_kind (kind ai)
\<not> method_exit n'
n' \<notin> set (sourcenodes (ax' # asx''))

goal (1 subgoal):
 1. sourcenode ax' controls n'
[PROOF STEP]
by(fastforce intro!:which_node_intra_standard_control_dependence_source)
[PROOF STATE]
proof (state)
this:
sourcenode ax' controls n'

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
hence "CFG_node (sourcenode ax') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node n'"
[PROOF STATE]
proof (prove)
using this:
sourcenode ax' controls n'

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

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>n -(ax#asx')@ax'#asx''\<rightarrow>\<^sub>\<iota>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -(ax # asx') @ ax' # asx''\<rightarrow>\<^sub>\<iota>* n'
[PROOF STEP]
have "n -ax#asx'\<rightarrow>\<^sub>\<iota>* sourcenode ax'" and "valid_edge ax'"
[PROOF STATE]
proof (prove)
using this:
n -(ax # asx') @ ax' # asx''\<rightarrow>\<^sub>\<iota>* n'

goal (1 subgoal):
 1. n -ax # asx'\<rightarrow>\<^sub>\<iota>* sourcenode ax' &&& valid_edge ax'
[PROOF STEP]
by(auto intro:path_split simp:intra_path_def simp del:append_Cons)
[PROOF STATE]
proof (state)
this:
n -ax # asx'\<rightarrow>\<^sub>\<iota>* sourcenode ax'
valid_edge ax'

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>asx = asx'@ax'#asx''\<close> \<open>as = (ax#asx)@zs\<close>
[PROOF STATE]
proof (chain)
picking this:
asx = asx' @ ax' # asx''
as = (ax # asx) @ zs
[PROOF STEP]
have "length (ax#asx') < length as"
[PROOF STATE]
proof (prove)
using this:
asx = asx' @ ax' # asx''
as = (ax # asx) @ zs

goal (1 subgoal):
 1. length (ax # asx') < length as
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (ax # asx') < length as

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>as = (ax#asx)@zs\<close> \<open>asx = asx'@ax'#asx''\<close>
[PROOF STATE]
proof (chain)
picking this:
as = (ax # asx) @ zs
asx = asx' @ ax' # asx''
[PROOF STEP]
have "sourcenode ax' \<in> set(sourcenodes as)"
[PROOF STATE]
proof (prove)
using this:
as = (ax # asx) @ zs
asx = asx' @ ax' # asx''

goal (1 subgoal):
 1. sourcenode ax' \<in> set (sourcenodes as)
[PROOF STEP]
by(simp add:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
sourcenode ax' \<in> set (sourcenodes as)

goal (1 subgoal):
 1. \<not> (\<forall>a' a''. a' \<in> set asx \<and> sourcenode a' = sourcenode a'' \<and> valid_edge a'' \<and> intra_kind (kind a'') \<longrightarrow> n' postdominates targetnode a'') \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
proof(cases "n = sourcenode ax'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = sourcenode ax' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. n \<noteq> sourcenode ax' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = sourcenode ax'

goal (2 subgoals):
 1. n = sourcenode ax' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. n \<noteq> sourcenode ax' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>CFG_node (sourcenode ax') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node n'\<close> \<open>valid_edge ax'\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (sourcenode ax') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node n'
valid_edge ax'
n = sourcenode ax'
[PROOF STEP]
have "CFG_node n cd-[]@[CFG_node n]\<rightarrow>\<^sub>d* CFG_node n'"
[PROOF STATE]
proof (prove)
using this:
CFG_node (sourcenode ax') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node n'
valid_edge ax'
n = sourcenode ax'

goal (1 subgoal):
 1. CFG_node n cd-[] @ [CFG_node n]\<rightarrow>\<^sub>d* CFG_node n'
[PROOF STEP]
by(fastforce intro:cdSp_Append_cdep cdSp_Nil)
[PROOF STATE]
proof (state)
this:
CFG_node n cd-[] @ [CFG_node n]\<rightarrow>\<^sub>d* CFG_node n'

goal (2 subgoals):
 1. n = sourcenode ax' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. n \<noteq> sourcenode ax' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>sourcenode ax' \<in> set(sourcenodes as)\<close> True
[PROOF STATE]
proof (chain)
picking this:
sourcenode ax' \<in> set (sourcenodes as)
n = sourcenode ax'
CFG_node n cd-[] @ [CFG_node n]\<rightarrow>\<^sub>d* CFG_node n'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sourcenode ax' \<in> set (sourcenodes as)
n = sourcenode ax'
CFG_node n cd-[] @ [CFG_node n]\<rightarrow>\<^sub>d* CFG_node n'

goal (1 subgoal):
 1. \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))

goal (1 subgoal):
 1. n \<noteq> sourcenode ax' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> sourcenode ax' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> sourcenode ax'

goal (1 subgoal):
 1. n \<noteq> sourcenode ax' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>valid_edge ax'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge ax'
[PROOF STEP]
have "sourcenode ax' \<noteq> (_Exit_)"
[PROOF STATE]
proof (prove)
using this:
valid_edge ax'

goal (1 subgoal):
 1. sourcenode ax' \<noteq> (_Exit_)
[PROOF STEP]
by -(rule ccontr,fastforce elim!:Exit_source)
[PROOF STATE]
proof (state)
this:
sourcenode ax' \<noteq> (_Exit_)

goal (1 subgoal):
 1. n \<noteq> sourcenode ax' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>n -ax#asx'\<rightarrow>\<^sub>\<iota>* sourcenode ax'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -ax # asx'\<rightarrow>\<^sub>\<iota>* sourcenode ax'
[PROOF STEP]
have "n = sourcenode ax"
[PROOF STATE]
proof (prove)
using this:
n -ax # asx'\<rightarrow>\<^sub>\<iota>* sourcenode ax'

goal (1 subgoal):
 1. n = sourcenode ax
[PROOF STEP]
by(fastforce intro:path_split_Cons simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
n = sourcenode ax

goal (1 subgoal):
 1. n \<noteq> sourcenode ax' \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
proof(cases "\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow>
                ax \<notin> get_return_edges a")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a

goal (2 subgoals):
 1. \<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>asx = asx'@ax'#asx''\<close> \<open>n -ax#asx\<rightarrow>\<^sub>\<iota>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
asx = asx' @ ax' # asx''
n -ax # asx\<rightarrow>\<^sub>\<iota>* n'
[PROOF STEP]
have "intra_kind (kind ax')"
[PROOF STATE]
proof (prove)
using this:
asx = asx' @ ax' # asx''
n -ax # asx\<rightarrow>\<^sub>\<iota>* n'

goal (1 subgoal):
 1. intra_kind (kind ax')
[PROOF STEP]
by(simp add:intra_path_def)
[PROOF STATE]
proof (state)
this:
intra_kind (kind ax')

goal (2 subgoals):
 1. \<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
have "\<not> method_exit (sourcenode ax')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> method_exit (sourcenode ax')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. method_exit (sourcenode ax') \<Longrightarrow> False
[PROOF STEP]
assume "method_exit (sourcenode ax')"
[PROOF STATE]
proof (state)
this:
method_exit (sourcenode ax')

goal (1 subgoal):
 1. method_exit (sourcenode ax') \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
method_exit (sourcenode ax')

goal (1 subgoal):
 1. False
[PROOF STEP]
proof(rule method_exit_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sourcenode ax' = (_Exit_) \<Longrightarrow> False
 2. \<And>a Q f p. \<lbrakk>sourcenode ax' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "sourcenode ax' = (_Exit_)"
[PROOF STATE]
proof (state)
this:
sourcenode ax' = (_Exit_)

goal (2 subgoals):
 1. sourcenode ax' = (_Exit_) \<Longrightarrow> False
 2. \<And>a Q f p. \<lbrakk>sourcenode ax' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with \<open>valid_edge ax'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge ax'
sourcenode ax' = (_Exit_)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
valid_edge ax'
sourcenode ax' = (_Exit_)

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

goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>sourcenode ax' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>sourcenode ax' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix x Q f p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>sourcenode ax' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume " sourcenode ax' = sourcenode x"
                    and "valid_edge x" and "kind x = Q\<hookleftarrow>\<^bsub>p\<^esub>f"
[PROOF STATE]
proof (state)
this:
sourcenode ax' = sourcenode x
valid_edge x
kind x = Q\<hookleftarrow>\<^bsub>p\<^esub>f

goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>sourcenode ax' = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from \<open>valid_edge x\<close> \<open>kind x = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<close> \<open>sourcenode ax' = sourcenode x\<close>
                    \<open>valid_edge ax'\<close> \<open>intra_kind (kind ax')\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge x
kind x = Q\<hookleftarrow>\<^bsub>p\<^esub>f
sourcenode ax' = sourcenode x
valid_edge ax'
intra_kind (kind ax')
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
valid_edge x
kind x = Q\<hookleftarrow>\<^bsub>p\<^esub>f
sourcenode ax' = sourcenode x
valid_edge ax'
intra_kind (kind ax')

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> method_exit (sourcenode ax')

goal (2 subgoals):
 1. \<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with IH \<open>length (ax#asx') < length as\<close> \<open>n -ax#asx'\<rightarrow>\<^sub>\<iota>* sourcenode ax'\<close>
                \<open>n \<noteq> sourcenode ax'\<close> \<open>sourcenode ax' \<noteq> (_Exit_)\<close> True
[PROOF STATE]
proof (chain)
picking this:
\<forall>as'. length as' < length as \<longrightarrow> (\<forall>n''. n -as'\<rightarrow>\<^sub>\<iota>* n'' \<longrightarrow> n \<noteq> n'' \<longrightarrow> n'' \<noteq> (_Exit_) \<longrightarrow> (\<forall>ax. valid_edge ax \<and> sourcenode ax = n'' \<longrightarrow> ax \<notin> get_return_edges a) \<longrightarrow> (\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n'' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as'))))
length (ax # asx') < length as
n -ax # asx'\<rightarrow>\<^sub>\<iota>* sourcenode ax'
n \<noteq> sourcenode ax'
sourcenode ax' \<noteq> (_Exit_)
\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a
\<not> method_exit (sourcenode ax')
[PROOF STEP]
obtain ns where "CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode ax')"
                and "ns \<noteq> []"
                and "\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes (ax#asx'))"
[PROOF STATE]
proof (prove)
using this:
\<forall>as'. length as' < length as \<longrightarrow> (\<forall>n''. n -as'\<rightarrow>\<^sub>\<iota>* n'' \<longrightarrow> n \<noteq> n'' \<longrightarrow> n'' \<noteq> (_Exit_) \<longrightarrow> (\<forall>ax. valid_edge ax \<and> sourcenode ax = n'' \<longrightarrow> ax \<notin> get_return_edges a) \<longrightarrow> (\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n'' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as'))))
length (ax # asx') < length as
n -ax # asx'\<rightarrow>\<^sub>\<iota>* sourcenode ax'
n \<noteq> sourcenode ax'
sourcenode ax' \<noteq> (_Exit_)
\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a
\<not> method_exit (sourcenode ax')

goal (1 subgoal):
 1. (\<And>ns. \<lbrakk>CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode ax'); ns \<noteq> []; \<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes (ax # asx'))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode ax')
ns \<noteq> []
\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes (ax # asx'))

goal (2 subgoals):
 1. \<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode ax')\<close>
                \<open>CFG_node (sourcenode ax') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node n'\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode ax')
CFG_node (sourcenode ax') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node n'
[PROOF STEP]
have "CFG_node n cd-ns@[CFG_node (sourcenode ax')]\<rightarrow>\<^sub>d* CFG_node n'"
[PROOF STATE]
proof (prove)
using this:
CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node (sourcenode ax')
CFG_node (sourcenode ax') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node n'

goal (1 subgoal):
 1. CFG_node n cd-ns @ [CFG_node (sourcenode ax')]\<rightarrow>\<^sub>d* CFG_node n'
[PROOF STEP]
by(rule cdSp_Append_cdep)
[PROOF STATE]
proof (state)
this:
CFG_node n cd-ns @ [CFG_node (sourcenode ax')]\<rightarrow>\<^sub>d* CFG_node n'

goal (2 subgoals):
 1. \<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
CFG_node n cd-ns @ [CFG_node (sourcenode ax')]\<rightarrow>\<^sub>d* CFG_node n'

goal (2 subgoals):
 1. \<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes (ax#asx'))\<close>
                \<open>asx = asx'@ax'#asx''\<close> \<open>as = (ax#asx)@zs\<close>
                \<open>sourcenode ax' \<in> set(sourcenodes as)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes (ax # asx'))
asx = asx' @ ax' # asx''
as = (ax # asx) @ zs
sourcenode ax' \<in> set (sourcenodes as)
[PROOF STEP]
have "\<forall>n''\<in>set (ns@[CFG_node (sourcenode ax')]).
                parent_node n'' \<in> set (sourcenodes as)"
[PROOF STATE]
proof (prove)
using this:
\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes (ax # asx'))
asx = asx' @ ax' # asx''
as = (ax # asx) @ zs
sourcenode ax' \<in> set (sourcenodes as)

goal (1 subgoal):
 1. \<forall>n''\<in>set (ns @ [CFG_node (sourcenode ax')]). parent_node n'' \<in> set (sourcenodes as)
[PROOF STEP]
by(fastforce simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
\<forall>n''\<in>set (ns @ [CFG_node (sourcenode ax')]). parent_node n'' \<in> set (sourcenodes as)

goal (2 subgoals):
 1. \<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
 2. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
CFG_node n cd-ns @ [CFG_node (sourcenode ax')]\<rightarrow>\<^sub>d* CFG_node n'
\<forall>n''\<in>set (ns @ [CFG_node (sourcenode ax')]). parent_node n'' \<in> set (sourcenodes as)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node n cd-ns @ [CFG_node (sourcenode ax')]\<rightarrow>\<^sub>d* CFG_node n'
\<forall>n''\<in>set (ns @ [CFG_node (sourcenode ax')]). parent_node n'' \<in> set (sourcenodes as)

goal (1 subgoal):
 1. \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))

goal (1 subgoal):
 1. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a)

goal (1 subgoal):
 1. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a)
[PROOF STEP]
obtain ai' where "valid_edge ai'"
                and "sourcenode ai' = sourcenode ax'"
                and "ai' \<in> get_return_edges a"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a)

goal (1 subgoal):
 1. (\<And>ai'. \<lbrakk>valid_edge ai'; sourcenode ai' = sourcenode ax'; ai' \<in> get_return_edges a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
valid_edge ai'
sourcenode ai' = sourcenode ax'
ai' \<in> get_return_edges a

goal (1 subgoal):
 1. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>targetnode a = n\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
targetnode a = n
valid_edge ai'
sourcenode ai' = sourcenode ax'
ai' \<in> get_return_edges a
[PROOF STEP]
have "CFG_node n \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (sourcenode ax')"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
targetnode a = n
valid_edge ai'
sourcenode ai' = sourcenode ax'
ai' \<in> get_return_edges a

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

goal (1 subgoal):
 1. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>valid_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_node n
CFG_node n \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (sourcenode ax')
[PROOF STEP]
have "CFG_node n cd-[]@[CFG_node n]\<rightarrow>\<^sub>d* CFG_node (sourcenode ax')"
[PROOF STATE]
proof (prove)
using this:
valid_node n
CFG_node n \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (sourcenode ax')

goal (1 subgoal):
 1. CFG_node n cd-[] @ [CFG_node n]\<rightarrow>\<^sub>d* CFG_node (sourcenode ax')
[PROOF STEP]
by(fastforce intro:cdSp_Append_cdep cdSp_Nil)
[PROOF STATE]
proof (state)
this:
CFG_node n cd-[] @ [CFG_node n]\<rightarrow>\<^sub>d* CFG_node (sourcenode ax')

goal (1 subgoal):
 1. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>CFG_node (sourcenode ax') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node n'\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node (sourcenode ax') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node n'
CFG_node n cd-[] @ [CFG_node n]\<rightarrow>\<^sub>d* CFG_node (sourcenode ax')
[PROOF STEP]
have "CFG_node n cd-[CFG_node n]@[CFG_node (sourcenode ax')]\<rightarrow>\<^sub>d*
                CFG_node n'"
[PROOF STATE]
proof (prove)
using this:
CFG_node (sourcenode ax') \<longrightarrow>\<^bsub>cd\<^esub> CFG_node n'
CFG_node n cd-[] @ [CFG_node n]\<rightarrow>\<^sub>d* CFG_node (sourcenode ax')

goal (1 subgoal):
 1. CFG_node n cd-[CFG_node n] @ [CFG_node (sourcenode ax')]\<rightarrow>\<^sub>d* CFG_node n'
[PROOF STEP]
by(fastforce intro:cdSp_Append_cdep)
[PROOF STATE]
proof (state)
this:
CFG_node n cd-[CFG_node n] @ [CFG_node (sourcenode ax')]\<rightarrow>\<^sub>d* CFG_node n'

goal (1 subgoal):
 1. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
CFG_node n cd-[CFG_node n] @ [CFG_node (sourcenode ax')]\<rightarrow>\<^sub>d* CFG_node n'

goal (1 subgoal):
 1. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>sourcenode ax' \<in> set(sourcenodes as)\<close> \<open>n = sourcenode ax\<close>
                \<open>as = (ax#asx)@zs\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode ax' \<in> set (sourcenodes as)
n = sourcenode ax
as = (ax # asx) @ zs
[PROOF STEP]
have "\<forall>n''\<in>set ([CFG_node n]@[CFG_node (sourcenode ax')]).
                parent_node n'' \<in> set (sourcenodes as)"
[PROOF STATE]
proof (prove)
using this:
sourcenode ax' \<in> set (sourcenodes as)
n = sourcenode ax
as = (ax # asx) @ zs

goal (1 subgoal):
 1. \<forall>n''\<in>set ([CFG_node n] @ [CFG_node (sourcenode ax')]). parent_node n'' \<in> set (sourcenodes as)
[PROOF STEP]
by(fastforce simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
\<forall>n''\<in>set ([CFG_node n] @ [CFG_node (sourcenode ax')]). parent_node n'' \<in> set (sourcenodes as)

goal (1 subgoal):
 1. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = sourcenode ax' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
CFG_node n cd-[CFG_node n] @ [CFG_node (sourcenode ax')]\<rightarrow>\<^sub>d* CFG_node n'
\<forall>n''\<in>set ([CFG_node n] @ [CFG_node (sourcenode ax')]). parent_node n'' \<in> set (sourcenodes as)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node n cd-[CFG_node n] @ [CFG_node (sourcenode ax')]\<rightarrow>\<^sub>d* CFG_node n'
\<forall>n''\<in>set ([CFG_node n] @ [CFG_node (sourcenode ax')]). parent_node n'' \<in> set (sourcenodes as)

goal (1 subgoal):
 1. \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))

goal (1 subgoal):
 1. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a)

goal (1 subgoal):
 1. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a)
[PROOF STEP]
obtain a' where "valid_edge a'" and "sourcenode a' = n'"
      and "a' \<in> get_return_edges a"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a)

goal (1 subgoal):
 1. (\<And>a'. \<lbrakk>valid_edge a'; sourcenode a' = n'; a' \<in> get_return_edges a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
valid_edge a'
sourcenode a' = n'
a' \<in> get_return_edges a

goal (1 subgoal):
 1. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>targetnode a = n\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
targetnode a = n
valid_edge a'
sourcenode a' = n'
a' \<in> get_return_edges a
[PROOF STEP]
have "CFG_node n \<longrightarrow>\<^bsub>cd\<^esub> CFG_node n'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
targetnode a = n
valid_edge a'
sourcenode a' = n'
a' \<in> get_return_edges a

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

goal (1 subgoal):
 1. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>valid_edge a\<close> \<open>targetnode a = n\<close>[THEN sym]
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
n = targetnode a
CFG_node n \<longrightarrow>\<^bsub>cd\<^esub> CFG_node n'
[PROOF STEP]
have "CFG_node n cd-[]@[CFG_node n]\<rightarrow>\<^sub>d* CFG_node n'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
n = targetnode a
CFG_node n \<longrightarrow>\<^bsub>cd\<^esub> CFG_node n'

goal (1 subgoal):
 1. CFG_node n cd-[] @ [CFG_node n]\<rightarrow>\<^sub>d* CFG_node n'
[PROOF STEP]
by(fastforce intro:cdep_SDG_path.intros)
[PROOF STATE]
proof (state)
this:
CFG_node n cd-[] @ [CFG_node n]\<rightarrow>\<^sub>d* CFG_node n'

goal (1 subgoal):
 1. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
from \<open>n -as\<rightarrow>\<^sub>\<iota>* n'\<close> \<open>n \<noteq> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>\<^sub>\<iota>* n'
n \<noteq> n'
[PROOF STEP]
have "as \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>\<^sub>\<iota>* n'
n \<noteq> n'

goal (1 subgoal):
 1. as \<noteq> []
[PROOF STEP]
by(fastforce elim:path.cases simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
as \<noteq> []

goal (1 subgoal):
 1. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>n -as\<rightarrow>\<^sub>\<iota>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>\<^sub>\<iota>* n'
as \<noteq> []
[PROOF STEP]
have "hd (sourcenodes as) = n"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>\<^sub>\<iota>* n'
as \<noteq> []

goal (1 subgoal):
 1. hd (sourcenodes as) = n
[PROOF STEP]
by(fastforce intro:path_sourcenode simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
hd (sourcenodes as) = n

goal (1 subgoal):
 1. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>as \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
as \<noteq> []
hd (sourcenodes as) = n
[PROOF STEP]
have "n \<in> set (sourcenodes as)"
[PROOF STATE]
proof (prove)
using this:
as \<noteq> []
hd (sourcenodes as) = n

goal (1 subgoal):
 1. n \<in> set (sourcenodes as)
[PROOF STEP]
by(fastforce intro:hd_in_set simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
n \<in> set (sourcenodes as)

goal (1 subgoal):
 1. \<not> (\<forall>ax. valid_edge ax \<and> sourcenode ax = n' \<longrightarrow> ax \<notin> get_return_edges a) \<Longrightarrow> \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
with \<open>CFG_node n cd-[]@[CFG_node n]\<rightarrow>\<^sub>d* CFG_node n'\<close>
[PROOF STATE]
proof (chain)
picking this:
CFG_node n cd-[] @ [CFG_node n]\<rightarrow>\<^sub>d* CFG_node n'
n \<in> set (sourcenodes as)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
CFG_node n cd-[] @ [CFG_node n]\<rightarrow>\<^sub>d* CFG_node n'
n \<in> set (sourcenodes as)

goal (1 subgoal):
 1. \<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns. CFG_node n cd-ns\<rightarrow>\<^sub>d* CFG_node n' \<and> ns \<noteq> [] \<and> (\<forall>n''\<in>set ns. parent_node n'' \<in> set (sourcenodes as))

goal:
No subgoals!
[PROOF STEP]
qed