[STATEMENT]
lemma SDG_Use_parent_Use:
  "V \<in> Use\<^bsub>SDG\<^esub> n \<Longrightarrow> V \<in> Use (parent_node n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<in> Use\<^bsub>SDG\<^esub> n \<Longrightarrow> V \<in> Use (parent_node n)
[PROOF STEP]
proof(induct rule:SDG_Use.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>m V n. \<lbrakk>valid_node m; V \<in> Use m; n = CFG_node m\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
 2. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_in (m, x); V \<in> ParamUses m ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
 3. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_out (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = outs ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
[PROOF STEP]
case CFG_Use_SDG_Use
[PROOF STATE]
proof (state)
this:
valid_node m_
V_ \<in> Use m_
n_ = CFG_node m_

goal (3 subgoals):
 1. \<And>m V n. \<lbrakk>valid_node m; V \<in> Use m; n = CFG_node m\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
 2. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_in (m, x); V \<in> ParamUses m ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
 3. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_out (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = outs ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
valid_node m_
V_ \<in> Use m_
n_ = CFG_node m_

goal (1 subgoal):
 1. V_ \<in> Use (parent_node n_)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
V_ \<in> Use (parent_node n_)

goal (2 subgoals):
 1. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_in (m, x); V \<in> ParamUses m ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
 2. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_out (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = outs ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_in (m, x); V \<in> ParamUses m ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
 2. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_out (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = outs ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
[PROOF STEP]
case (Actual_in_SDG_Use n m x V)
[PROOF STATE]
proof (state)
this:
valid_SDG_node n
n = Actual_in (m, x)
V \<in> ParamUses m ! x

goal (2 subgoals):
 1. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_in (m, x); V \<in> ParamUses m ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
 2. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_out (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = outs ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
[PROOF STEP]
from \<open>valid_SDG_node n\<close> \<open>n = Actual_in (m, x)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
n = Actual_in (m, x)
[PROOF STEP]
obtain a Q r p fs ins outs
    where "valid_edge a" and "kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs" and "sourcenode a = m"
    and "(p,ins,outs) \<in> set procs" and "x < length ins"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n
n = Actual_in (m, x)

goal (1 subgoal):
 1. (\<And>a Q r p fs ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; sourcenode a = m; (p, ins, outs) \<in> set procs; x < length ins\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
sourcenode a = m
(p, ins, outs) \<in> set procs
x < length ins

goal (2 subgoals):
 1. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_in (m, x); V \<in> ParamUses m ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
 2. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_out (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = outs ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>(p,ins,outs) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
(p, ins, outs) \<in> set procs
[PROOF STEP]
have "length(ParamUses (sourcenode a)) = length ins"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
(p, ins, outs) \<in> set procs

goal (1 subgoal):
 1. length (ParamUses (sourcenode a)) = length ins
[PROOF STEP]
by(fastforce intro:ParamUses_call_source_length)
[PROOF STATE]
proof (state)
this:
length (ParamUses (sourcenode a)) = length ins

goal (2 subgoals):
 1. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_in (m, x); V \<in> ParamUses m ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
 2. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_out (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = outs ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
[PROOF STEP]
with \<open>x < length ins\<close>
[PROOF STATE]
proof (chain)
picking this:
x < length ins
length (ParamUses (sourcenode a)) = length ins
[PROOF STEP]
have "(ParamUses (sourcenode a))!x \<in> set (ParamUses (sourcenode a))"
[PROOF STATE]
proof (prove)
using this:
x < length ins
length (ParamUses (sourcenode a)) = length ins

goal (1 subgoal):
 1. ParamUses (sourcenode a) ! x \<in> set (ParamUses (sourcenode a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ParamUses (sourcenode a) ! x \<in> set (ParamUses (sourcenode a))

goal (2 subgoals):
 1. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_in (m, x); V \<in> ParamUses m ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
 2. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_out (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = outs ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
[PROOF STEP]
with \<open>V \<in> (ParamUses m)!x\<close> \<open>sourcenode a = m\<close>
[PROOF STATE]
proof (chain)
picking this:
V \<in> ParamUses m ! x
sourcenode a = m
ParamUses (sourcenode a) ! x \<in> set (ParamUses (sourcenode a))
[PROOF STEP]
have "V \<in> Union (set (ParamUses m))"
[PROOF STATE]
proof (prove)
using this:
V \<in> ParamUses m ! x
sourcenode a = m
ParamUses (sourcenode a) ! x \<in> set (ParamUses (sourcenode a))

goal (1 subgoal):
 1. V \<in> \<Union> (set (ParamUses m))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
V \<in> \<Union> (set (ParamUses m))

goal (2 subgoals):
 1. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_in (m, x); V \<in> ParamUses m ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
 2. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_out (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = outs ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
[PROOF STEP]
with \<open>valid_edge a\<close> \<open>sourcenode a = m\<close> \<open>n = Actual_in (m, x)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
sourcenode a = m
n = Actual_in (m, x)
V \<in> \<Union> (set (ParamUses m))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
valid_edge a
sourcenode a = m
n = Actual_in (m, x)
V \<in> \<Union> (set (ParamUses m))

goal (1 subgoal):
 1. V \<in> Use (parent_node n)
[PROOF STEP]
by(fastforce intro:ParamUses_in_Use)
[PROOF STATE]
proof (state)
this:
V \<in> Use (parent_node n)

goal (1 subgoal):
 1. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_out (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = outs ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_out (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = outs ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
[PROOF STEP]
case (Formal_out_SDG_Use n m x p ins outs V)
[PROOF STATE]
proof (state)
this:
valid_SDG_node n
n = Formal_out (m, x)
get_proc m = p
(p, ins, outs) \<in> set procs
V = outs ! x

goal (1 subgoal):
 1. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_out (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = outs ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
[PROOF STEP]
from \<open>valid_SDG_node n\<close> \<open>n = Formal_out (m, x)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
n = Formal_out (m, x)
[PROOF STEP]
obtain a Q p' f ins' outs'
    where "valid_edge a" and "kind a = Q\<hookleftarrow>\<^bsub>p'\<^esub>f" and "sourcenode a = m"
    and "(p',ins',outs') \<in> set procs" and "x < length outs'"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n
n = Formal_out (m, x)

goal (1 subgoal):
 1. (\<And>a Q p' f ins' outs'. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p'\<^esub>f; sourcenode a = m; (p', ins', outs') \<in> set procs; x < length outs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p'\<^esub>f
sourcenode a = m
(p', ins', outs') \<in> set procs
x < length outs'

goal (1 subgoal):
 1. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_out (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = outs ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
[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>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_out (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = outs ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
[PROOF STEP]
with \<open>get_proc m = p\<close> \<open>sourcenode a = m\<close>
[PROOF STATE]
proof (chain)
picking this:
get_proc m = p
sourcenode a = m
get_proc (sourcenode a) = p'
[PROOF STEP]
have [simp]:"p = p'"
[PROOF STATE]
proof (prove)
using this:
get_proc m = p
sourcenode a = m
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>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_out (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = outs ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
[PROOF STEP]
with \<open>(p',ins',outs') \<in> set procs\<close> \<open>(p,ins,outs) \<in> set procs\<close> unique_callers
[PROOF STATE]
proof (chain)
picking this:
(p', ins', outs') \<in> set procs
(p, ins, outs) \<in> set procs
distinct_fst procs
p = p'
[PROOF STEP]
have [simp]:"ins' = ins" "outs' = outs"
[PROOF STATE]
proof (prove)
using this:
(p', ins', outs') \<in> set procs
(p, ins, outs) \<in> set procs
distinct_fst procs
p = p'

goal (1 subgoal):
 1. ins' = ins &&& outs' = outs
[PROOF STEP]
by(auto dest:distinct_fst_isin_same_fst)
[PROOF STATE]
proof (state)
this:
ins' = ins
outs' = outs

goal (1 subgoal):
 1. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_out (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = outs ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
[PROOF STEP]
from \<open>x < length outs'\<close> \<open>V = outs ! x\<close>
[PROOF STATE]
proof (chain)
picking this:
x < length outs'
V = outs ! x
[PROOF STEP]
have "V \<in> set outs"
[PROOF STATE]
proof (prove)
using this:
x < length outs'
V = outs ! x

goal (1 subgoal):
 1. V \<in> set outs
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
V \<in> set outs

goal (1 subgoal):
 1. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_out (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = outs ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
[PROOF STEP]
with \<open>valid_edge a\<close> \<open>kind a = Q\<hookleftarrow>\<^bsub>p'\<^esub>f\<close> \<open>(p,ins,outs) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p'\<^esub>f
(p, ins, outs) \<in> set procs
V \<in> set outs
[PROOF STEP]
have "V \<in> Use (sourcenode a)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p'\<^esub>f
(p, ins, outs) \<in> set procs
V \<in> set outs

goal (1 subgoal):
 1. V \<in> Use (sourcenode a)
[PROOF STEP]
by(fastforce intro:outs_in_Use)
[PROOF STATE]
proof (state)
this:
V \<in> Use (sourcenode a)

goal (1 subgoal):
 1. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_out (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = outs ! x\<rbrakk> \<Longrightarrow> V \<in> Use (parent_node n)
[PROOF STEP]
with \<open>sourcenode a = m\<close> \<open>valid_SDG_node n\<close> \<open>n = Formal_out (m, x)\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode a = m
valid_SDG_node n
n = Formal_out (m, x)
V \<in> Use (sourcenode a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sourcenode a = m
valid_SDG_node n
n = Formal_out (m, x)
V \<in> Use (sourcenode a)

goal (1 subgoal):
 1. V \<in> Use (parent_node n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
V \<in> Use (parent_node n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma in_Def_valid_SDG_node:
  "V \<in> Def\<^bsub>SDG\<^esub> n \<Longrightarrow> valid_SDG_node n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<in> Def\<^bsub>SDG\<^esub> n \<Longrightarrow> valid_SDG_node n
[PROOF STEP]
by(induct rule:SDG_Def.induct,auto intro:valid_SDG_CFG_node)


[STATEMENT]
lemma SDG_Def_parent_Def:
  "V \<in> Def\<^bsub>SDG\<^esub> n \<Longrightarrow> V \<in> Def (parent_node n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V \<in> Def\<^bsub>SDG\<^esub> n \<Longrightarrow> V \<in> Def (parent_node n)
[PROOF STEP]
proof(induct rule:SDG_Def.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>m V n. \<lbrakk>valid_node m; V \<in> Def m; n = CFG_node m\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
 2. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_in (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = ins ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
 3. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_out (m, x); V = ParamDefs m ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
[PROOF STEP]
case CFG_Def_SDG_Def
[PROOF STATE]
proof (state)
this:
valid_node m_
V_ \<in> Def m_
n_ = CFG_node m_

goal (3 subgoals):
 1. \<And>m V n. \<lbrakk>valid_node m; V \<in> Def m; n = CFG_node m\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
 2. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_in (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = ins ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
 3. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_out (m, x); V = ParamDefs m ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
valid_node m_
V_ \<in> Def m_
n_ = CFG_node m_

goal (1 subgoal):
 1. V_ \<in> Def (parent_node n_)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
V_ \<in> Def (parent_node n_)

goal (2 subgoals):
 1. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_in (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = ins ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
 2. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_out (m, x); V = ParamDefs m ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_in (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = ins ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
 2. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_out (m, x); V = ParamDefs m ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
[PROOF STEP]
case (Formal_in_SDG_Def n m x p ins outs V)
[PROOF STATE]
proof (state)
this:
valid_SDG_node n
n = Formal_in (m, x)
get_proc m = p
(p, ins, outs) \<in> set procs
V = ins ! x

goal (2 subgoals):
 1. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_in (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = ins ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
 2. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_out (m, x); V = ParamDefs m ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
[PROOF STEP]
from \<open>valid_SDG_node n\<close> \<open>n = Formal_in (m, x)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
n = Formal_in (m, x)
[PROOF STEP]
obtain a Q r p' fs ins' outs'
    where "valid_edge a" and "kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs" and "targetnode a = m"
    and "(p',ins',outs') \<in> set procs" and "x < length ins'"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n
n = Formal_in (m, x)

goal (1 subgoal):
 1. (\<And>a Q r p' fs ins' outs'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs; targetnode a = m; (p', ins', outs') \<in> set procs; x < length ins'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs
targetnode a = m
(p', ins', outs') \<in> set procs
x < length ins'

goal (2 subgoals):
 1. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_in (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = ins ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
 2. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_out (m, x); V = ParamDefs m ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
[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 (2 subgoals):
 1. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_in (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = ins ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
 2. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_out (m, x); V = ParamDefs m ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
[PROOF STEP]
with \<open>get_proc m = p\<close> \<open>targetnode a = m\<close>
[PROOF STATE]
proof (chain)
picking this:
get_proc m = p
targetnode a = m
get_proc (targetnode a) = p'
[PROOF STEP]
have [simp]:"p = p'"
[PROOF STATE]
proof (prove)
using this:
get_proc m = p
targetnode a = m
get_proc (targetnode a) = p'

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

goal (2 subgoals):
 1. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_in (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = ins ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
 2. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_out (m, x); V = ParamDefs m ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
[PROOF STEP]
with \<open>(p',ins',outs') \<in> set procs\<close> \<open>(p,ins,outs) \<in> set procs\<close> unique_callers
[PROOF STATE]
proof (chain)
picking this:
(p', ins', outs') \<in> set procs
(p, ins, outs) \<in> set procs
distinct_fst procs
p = p'
[PROOF STEP]
have [simp]:"ins' = ins" "outs' = outs"
[PROOF STATE]
proof (prove)
using this:
(p', ins', outs') \<in> set procs
(p, ins, outs) \<in> set procs
distinct_fst procs
p = p'

goal (1 subgoal):
 1. ins' = ins &&& outs' = outs
[PROOF STEP]
by(auto dest:distinct_fst_isin_same_fst)
[PROOF STATE]
proof (state)
this:
ins' = ins
outs' = outs

goal (2 subgoals):
 1. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_in (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = ins ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
 2. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_out (m, x); V = ParamDefs m ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
[PROOF STEP]
from \<open>x < length ins'\<close> \<open>V = ins ! x\<close>
[PROOF STATE]
proof (chain)
picking this:
x < length ins'
V = ins ! x
[PROOF STEP]
have "V \<in> set ins"
[PROOF STATE]
proof (prove)
using this:
x < length ins'
V = ins ! x

goal (1 subgoal):
 1. V \<in> set ins
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
V \<in> set ins

goal (2 subgoals):
 1. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_in (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = ins ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
 2. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_out (m, x); V = ParamDefs m ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
[PROOF STEP]
with \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs\<close> \<open>(p,ins,outs) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs
(p, ins, outs) \<in> set procs
V \<in> set ins
[PROOF STEP]
have "V \<in> Def (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs
(p, ins, outs) \<in> set procs
V \<in> set ins

goal (1 subgoal):
 1. V \<in> Def (targetnode a)
[PROOF STEP]
by(fastforce intro:ins_in_Def)
[PROOF STATE]
proof (state)
this:
V \<in> Def (targetnode a)

goal (2 subgoals):
 1. \<And>n m x p ins outs V. \<lbrakk>valid_SDG_node n; n = Formal_in (m, x); get_proc m = p; (p, ins, outs) \<in> set procs; V = ins ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
 2. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_out (m, x); V = ParamDefs m ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
[PROOF STEP]
with \<open>targetnode a = m\<close> \<open>valid_SDG_node n\<close> \<open>n = Formal_in (m, x)\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a = m
valid_SDG_node n
n = Formal_in (m, x)
V \<in> Def (targetnode a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
targetnode a = m
valid_SDG_node n
n = Formal_in (m, x)
V \<in> Def (targetnode a)

goal (1 subgoal):
 1. V \<in> Def (parent_node n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
V \<in> Def (parent_node n)

goal (1 subgoal):
 1. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_out (m, x); V = ParamDefs m ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_out (m, x); V = ParamDefs m ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
[PROOF STEP]
case (Actual_out_SDG_Def n m x V)
[PROOF STATE]
proof (state)
this:
valid_SDG_node n
n = Actual_out (m, x)
V = ParamDefs m ! x

goal (1 subgoal):
 1. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_out (m, x); V = ParamDefs m ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
[PROOF STEP]
from \<open>valid_SDG_node n\<close> \<open>n = Actual_out (m, x)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
n = Actual_out (m, x)
[PROOF STEP]
obtain a Q p f ins outs
    where "valid_edge a" and "kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f" and "targetnode a = m"
    and "(p,ins,outs) \<in> set procs" and "x < length outs"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n
n = Actual_out (m, x)

goal (1 subgoal):
 1. (\<And>a Q p f ins outs. \<lbrakk>valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f; targetnode a = m; (p, ins, outs) \<in> set procs; x < length outs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
targetnode a = m
(p, ins, outs) \<in> set procs
x < length outs

goal (1 subgoal):
 1. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_out (m, x); V = ParamDefs m ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<close> \<open>(p,ins,outs) \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
(p, ins, outs) \<in> set procs
[PROOF STEP]
have "length(ParamDefs (targetnode a)) = length outs"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f
(p, ins, outs) \<in> set procs

goal (1 subgoal):
 1. length (ParamDefs (targetnode a)) = length outs
[PROOF STEP]
by(rule ParamDefs_return_target_length)
[PROOF STATE]
proof (state)
this:
length (ParamDefs (targetnode a)) = length outs

goal (1 subgoal):
 1. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_out (m, x); V = ParamDefs m ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
[PROOF STEP]
with \<open>x < length outs\<close> \<open>V = ParamDefs m ! x\<close> \<open>targetnode a = m\<close>
[PROOF STATE]
proof (chain)
picking this:
x < length outs
V = ParamDefs m ! x
targetnode a = m
length (ParamDefs (targetnode a)) = length outs
[PROOF STEP]
have "V \<in> set (ParamDefs (targetnode a))"
[PROOF STATE]
proof (prove)
using this:
x < length outs
V = ParamDefs m ! x
targetnode a = m
length (ParamDefs (targetnode a)) = length outs

goal (1 subgoal):
 1. V \<in> set (ParamDefs (targetnode a))
[PROOF STEP]
by(fastforce simp:set_conv_nth)
[PROOF STATE]
proof (state)
this:
V \<in> set (ParamDefs (targetnode a))

goal (1 subgoal):
 1. \<And>n m x V. \<lbrakk>valid_SDG_node n; n = Actual_out (m, x); V = ParamDefs m ! x\<rbrakk> \<Longrightarrow> V \<in> Def (parent_node n)
[PROOF STEP]
with \<open>n = Actual_out (m, x)\<close> \<open>targetnode a = m\<close> \<open>valid_edge a\<close>
[PROOF STATE]
proof (chain)
picking this:
n = Actual_out (m, x)
targetnode a = m
valid_edge a
V \<in> set (ParamDefs (targetnode a))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n = Actual_out (m, x)
targetnode a = m
valid_edge a
V \<in> set (ParamDefs (targetnode a))

goal (1 subgoal):
 1. V \<in> Def (parent_node n)
[PROOF STEP]
by(fastforce intro:ParamDefs_in_Def)
[PROOF STATE]
proof (state)
this:
V \<in> Def (parent_node n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma control_dependence_path:
  assumes "n controls n'" obtains as where "n -as\<rightarrow>\<^sub>\<iota>* n'" and "as \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>as. \<lbrakk>n -as\<rightarrow>\<^sub>\<iota>* n'; as \<noteq> []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>n controls n'\<close>
[PROOF STATE]
proof (prove)
using this:
n controls n'

goal (1 subgoal):
 1. (\<And>as. \<lbrakk>n -as\<rightarrow>\<^sub>\<iota>* n'; as \<noteq> []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce simp:control_dependence_def)


[STATEMENT]
lemma Exit_does_not_control [dest]:
  assumes "(_Exit_) controls n'" shows "False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. False
[PROOF STEP]
from \<open>(_Exit_) controls n'\<close>
[PROOF STATE]
proof (chain)
picking this:
(_Exit_) controls n'
[PROOF STEP]
obtain a where "valid_edge a"
    and "sourcenode a = (_Exit_)"
[PROOF STATE]
proof (prove)
using this:
(_Exit_) controls n'

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

goal (1 subgoal):
 1. False
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
valid_edge a
sourcenode a = (_Exit_)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Exit_not_control_dependent:
  assumes "n controls n'" shows "n' \<noteq> (_Exit_)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n' \<noteq> (_Exit_)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n' \<noteq> (_Exit_)
[PROOF STEP]
from \<open>n controls n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n controls n'
[PROOF STEP]
obtain a as where "n -a#as\<rightarrow>\<^sub>\<iota>* n'"
    and "n' postdominates (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
n controls n'

goal (1 subgoal):
 1. (\<And>a as. \<lbrakk>n -a # as\<rightarrow>\<^sub>\<iota>* n'; n' postdominates targetnode a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp:control_dependence_def)
[PROOF STATE]
proof (state)
this:
n -a # as\<rightarrow>\<^sub>\<iota>* n'
n' postdominates targetnode a

goal (1 subgoal):
 1. n' \<noteq> (_Exit_)
[PROOF STEP]
from \<open>n -a#as\<rightarrow>\<^sub>\<iota>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -a # as\<rightarrow>\<^sub>\<iota>* n'
[PROOF STEP]
have "valid_edge a"
[PROOF STATE]
proof (prove)
using this:
n -a # as\<rightarrow>\<^sub>\<iota>* n'

goal (1 subgoal):
 1. valid_edge a
[PROOF STEP]
by(fastforce elim:path.cases simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
valid_edge a

goal (1 subgoal):
 1. n' \<noteq> (_Exit_)
[PROOF STEP]
hence "valid_node (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a

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

goal (1 subgoal):
 1. n' \<noteq> (_Exit_)
[PROOF STEP]
with \<open>n' postdominates (targetnode a)\<close> \<open>n -a#as\<rightarrow>\<^sub>\<iota>* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n' postdominates targetnode a
n -a # as\<rightarrow>\<^sub>\<iota>* n'
valid_node (targetnode a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n' postdominates targetnode a
n -a # as\<rightarrow>\<^sub>\<iota>* n'
valid_node (targetnode a)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma which_node_intra_standard_control_dependence_source:
  assumes "nx -as@a#as'\<rightarrow>\<^sub>\<iota>* n" and "sourcenode a = n'" and "sourcenode a' = n'"
  and "n \<notin> set(sourcenodes (a#as'))" and "valid_edge a'" and "intra_kind(kind a')"
  and "inner_node n" and "\<not> method_exit n" and "\<not> n postdominates (targetnode a')"
  and last:"\<forall>ax ax'. ax \<in> set as' \<and> sourcenode ax = sourcenode ax' \<and>
    valid_edge ax' \<and> intra_kind(kind ax') \<longrightarrow> n postdominates targetnode ax'"
  shows "n' controls n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n' controls n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n' controls n
[PROOF STEP]
from \<open>nx -as@a#as'\<rightarrow>\<^sub>\<iota>* n\<close> \<open>sourcenode a = n'\<close>
[PROOF STATE]
proof (chain)
picking this:
nx -as @ a # as'\<rightarrow>\<^sub>\<iota>* n
sourcenode a = n'
[PROOF STEP]
have "n' -a#as'\<rightarrow>\<^sub>\<iota>* n"
[PROOF STATE]
proof (prove)
using this:
nx -as @ a # as'\<rightarrow>\<^sub>\<iota>* n
sourcenode a = n'

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

goal (1 subgoal):
 1. n' controls n
[PROOF STEP]
from \<open>nx -as@a#as'\<rightarrow>\<^sub>\<iota>* n\<close>
[PROOF STATE]
proof (chain)
picking this:
nx -as @ a # as'\<rightarrow>\<^sub>\<iota>* n
[PROOF STEP]
have "valid_edge a"
[PROOF STATE]
proof (prove)
using this:
nx -as @ a # as'\<rightarrow>\<^sub>\<iota>* n

goal (1 subgoal):
 1. valid_edge a
[PROOF STEP]
by(fastforce intro:path_split simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
valid_edge a

goal (1 subgoal):
 1. n' controls n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n' controls n
[PROOF STEP]
proof(cases "n postdominates (targetnode a)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n postdominates targetnode a \<Longrightarrow> n' controls n
 2. \<not> n postdominates targetnode a \<Longrightarrow> n' controls n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n postdominates targetnode a

goal (2 subgoals):
 1. n postdominates targetnode a \<Longrightarrow> n' controls n
 2. \<not> n postdominates targetnode a \<Longrightarrow> n' controls n
[PROOF STEP]
with \<open>n' -a#as'\<rightarrow>\<^sub>\<iota>* n\<close> \<open>n \<notin> set(sourcenodes (a#as'))\<close>
      \<open>valid_edge a'\<close> \<open>intra_kind(kind a')\<close> \<open>sourcenode a' = n'\<close>
      \<open>\<not> n postdominates (targetnode a')\<close>
[PROOF STATE]
proof (chain)
picking this:
n' -a # as'\<rightarrow>\<^sub>\<iota>* n
n \<notin> set (sourcenodes (a # as'))
valid_edge a'
intra_kind (kind a')
sourcenode a' = n'
\<not> n postdominates targetnode a'
n postdominates targetnode a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n' -a # as'\<rightarrow>\<^sub>\<iota>* n
n \<notin> set (sourcenodes (a # as'))
valid_edge a'
intra_kind (kind a')
sourcenode a' = n'
\<not> n postdominates targetnode a'
n postdominates targetnode a

goal (1 subgoal):
 1. n' controls n
[PROOF STEP]
by(fastforce simp:control_dependence_def intra_path_def)
[PROOF STATE]
proof (state)
this:
n' controls n

goal (1 subgoal):
 1. \<not> n postdominates targetnode a \<Longrightarrow> n' controls n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> n postdominates targetnode a \<Longrightarrow> n' controls n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> n postdominates targetnode a

goal (1 subgoal):
 1. \<not> n postdominates targetnode a \<Longrightarrow> n' controls n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n' controls n
[PROOF STEP]
proof(cases "as' = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. as' = [] \<Longrightarrow> n' controls n
 2. as' \<noteq> [] \<Longrightarrow> n' controls n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
as' = []

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> n' controls n
 2. as' \<noteq> [] \<Longrightarrow> n' controls n
[PROOF STEP]
with \<open>n' -a#as'\<rightarrow>\<^sub>\<iota>* n\<close>
[PROOF STATE]
proof (chain)
picking this:
n' -a # as'\<rightarrow>\<^sub>\<iota>* n
as' = []
[PROOF STEP]
have "targetnode a = n"
[PROOF STATE]
proof (prove)
using this:
n' -a # as'\<rightarrow>\<^sub>\<iota>* n
as' = []

goal (1 subgoal):
 1. targetnode a = n
[PROOF STEP]
by(fastforce elim:path.cases simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
targetnode a = n

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> n' controls n
 2. as' \<noteq> [] \<Longrightarrow> n' controls n
[PROOF STEP]
with \<open>inner_node n\<close> \<open>\<not> method_exit n\<close>
[PROOF STATE]
proof (chain)
picking this:
inner_node n
\<not> method_exit n
targetnode a = n
[PROOF STEP]
have "n postdominates (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
inner_node n
\<not> method_exit n
targetnode a = n

goal (1 subgoal):
 1. n postdominates targetnode a
[PROOF STEP]
by(fastforce dest:inner_is_valid intro:postdominate_refl)
[PROOF STATE]
proof (state)
this:
n postdominates targetnode a

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> n' controls n
 2. as' \<noteq> [] \<Longrightarrow> n' controls n
[PROOF STEP]
with \<open>\<not> n postdominates (targetnode a)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> n postdominates targetnode a
n postdominates targetnode a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> n postdominates targetnode a
n postdominates targetnode a

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

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> n' controls n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> n' controls n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
as' \<noteq> []

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> n' controls n
[PROOF STEP]
with \<open>nx -as@a#as'\<rightarrow>\<^sub>\<iota>* n\<close>
[PROOF STATE]
proof (chain)
picking this:
nx -as @ a # as'\<rightarrow>\<^sub>\<iota>* n
as' \<noteq> []
[PROOF STEP]
have "targetnode a -as'\<rightarrow>\<^sub>\<iota>* n"
[PROOF STATE]
proof (prove)
using this:
nx -as @ a # as'\<rightarrow>\<^sub>\<iota>* n
as' \<noteq> []

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

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> n' controls n
[PROOF STEP]
with \<open>\<not> n postdominates (targetnode a)\<close> \<open>valid_edge a\<close> \<open>inner_node n\<close>
        \<open>targetnode a -as'\<rightarrow>\<^sub>\<iota>* n\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> n postdominates targetnode a
valid_edge a
inner_node n
targetnode a -as'\<rightarrow>\<^sub>\<iota>* n
targetnode a -as'\<rightarrow>\<^sub>\<iota>* n
[PROOF STEP]
obtain asx pex where "targetnode a -asx\<rightarrow>\<^sub>\<iota>* pex" and "method_exit pex"
        and "n \<notin> set (sourcenodes asx)"
[PROOF STATE]
proof (prove)
using this:
\<not> n postdominates targetnode a
valid_edge a
inner_node n
targetnode a -as'\<rightarrow>\<^sub>\<iota>* n
targetnode a -as'\<rightarrow>\<^sub>\<iota>* n

goal (1 subgoal):
 1. (\<And>asx pex. \<lbrakk>targetnode a -asx\<rightarrow>\<^sub>\<iota>* pex; method_exit pex; n \<notin> set (sourcenodes asx)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce dest:inner_is_valid simp:postdominate_def)
[PROOF STATE]
proof (state)
this:
targetnode a -asx\<rightarrow>\<^sub>\<iota>* pex
method_exit pex
n \<notin> set (sourcenodes asx)

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> n' controls n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n' controls n
[PROOF STEP]
proof(cases "\<exists>asx'. asx = as'@asx'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
 2. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>asx'. asx = as' @ asx'

goal (2 subgoals):
 1. \<exists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
 2. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>asx'. asx = as' @ asx'
[PROOF STEP]
obtain asx' where [simp]:"asx = as'@asx'"
[PROOF STATE]
proof (prove)
using this:
\<exists>asx'. asx = as' @ asx'

goal (1 subgoal):
 1. (\<And>asx'. asx = as' @ asx' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
asx = as' @ asx'

goal (2 subgoals):
 1. \<exists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
 2. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
from \<open>targetnode a -asx\<rightarrow>\<^sub>\<iota>* pex\<close> \<open>targetnode a -as'\<rightarrow>\<^sub>\<iota>* n\<close>
          \<open>as' \<noteq> []\<close> \<open>method_exit pex\<close> \<open>\<not> method_exit n\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a -asx\<rightarrow>\<^sub>\<iota>* pex
targetnode a -as'\<rightarrow>\<^sub>\<iota>* n
as' \<noteq> []
method_exit pex
\<not> method_exit n
[PROOF STEP]
obtain a'' as'' where "asx' = a''#as'' \<and> sourcenode a'' = n"
[PROOF STATE]
proof (prove)
using this:
targetnode a -asx\<rightarrow>\<^sub>\<iota>* pex
targetnode a -as'\<rightarrow>\<^sub>\<iota>* n
as' \<noteq> []
method_exit pex
\<not> method_exit n

goal (1 subgoal):
 1. (\<And>a'' as''. asx' = a'' # as'' \<and> sourcenode a'' = n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases asx')(auto dest:path_split path_det simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
asx' = a'' # as'' \<and> sourcenode a'' = n

goal (2 subgoals):
 1. \<exists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
 2. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
hence "n \<in> set(sourcenodes asx)"
[PROOF STATE]
proof (prove)
using this:
asx' = a'' # as'' \<and> sourcenode a'' = n

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

goal (2 subgoals):
 1. \<exists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
 2. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
with \<open>n \<notin> set (sourcenodes asx)\<close>
[PROOF STATE]
proof (chain)
picking this:
n \<notin> set (sourcenodes asx)
n \<in> set (sourcenodes asx)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
n \<notin> set (sourcenodes asx)
n \<in> set (sourcenodes asx)

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

goal (2 subgoals):
 1. \<exists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
 2. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

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

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>asx'. asx = as' @ asx'

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
hence "\<forall>asx'. asx \<noteq> as'@asx'"
[PROOF STATE]
proof (prove)
using this:
\<nexists>asx'. asx = as' @ asx'

goal (1 subgoal):
 1. \<forall>asx'. asx \<noteq> as' @ asx'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>asx'. asx \<noteq> as' @ asx'

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>asx'. asx \<noteq> as' @ asx'
[PROOF STEP]
obtain j asx' where "asx = (take j as')@asx'"
          and "j < length as'" and "\<forall>k > j. \<forall>asx''. asx \<noteq> (take k as')@asx''"
[PROOF STATE]
proof (prove)
using this:
\<forall>asx'. asx \<noteq> as' @ asx'

goal (1 subgoal):
 1. (\<And>j asx'. \<lbrakk>asx = take j as' @ asx'; j < length as'; \<forall>k>j. \<forall>asx''. asx \<noteq> take k as' @ asx''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto elim:path_split_general)
[PROOF STATE]
proof (state)
this:
asx = take j as' @ asx'
j < length as'
\<forall>k>j. \<forall>asx''. asx \<noteq> take k as' @ asx''

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
from \<open>asx = (take j as')@asx'\<close> \<open>j < length as'\<close>
[PROOF STATE]
proof (chain)
picking this:
asx = take j as' @ asx'
j < length as'
[PROOF STEP]
have "\<exists>as'1 as'2. asx = as'1@asx' \<and>
          as' = as'1@as'2 \<and> as'2 \<noteq> [] \<and> as'1 = take j as'"
[PROOF STATE]
proof (prove)
using this:
asx = take j as' @ asx'
j < length as'

goal (1 subgoal):
 1. \<exists>as'1 as'2. asx = as'1 @ asx' \<and> as' = as'1 @ as'2 \<and> as'2 \<noteq> [] \<and> as'1 = take j as'
[PROOF STEP]
by simp(rule_tac x= "drop j as'" in exI,simp)
[PROOF STATE]
proof (state)
this:
\<exists>as'1 as'2. asx = as'1 @ asx' \<and> as' = as'1 @ as'2 \<and> as'2 \<noteq> [] \<and> as'1 = take j as'

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>as'1 as'2. asx = as'1 @ asx' \<and> as' = as'1 @ as'2 \<and> as'2 \<noteq> [] \<and> as'1 = take j as'
[PROOF STEP]
obtain as'1 as'' where "asx = as'1@asx'"
          and "as'1 = take j as'"
          and "as' = as'1@as''" and "as'' \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
\<exists>as'1 as'2. asx = as'1 @ asx' \<and> as' = as'1 @ as'2 \<and> as'2 \<noteq> [] \<and> as'1 = take j as'

goal (1 subgoal):
 1. (\<And>as'1 as''. \<lbrakk>asx = as'1 @ asx'; as'1 = take j as'; as' = as'1 @ as''; as'' \<noteq> []\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
asx = as'1 @ asx'
as'1 = take j as'
as' = as'1 @ as''
as'' \<noteq> []

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
from \<open>as' = as'1@as''\<close> \<open>as'' \<noteq> []\<close>
[PROOF STATE]
proof (chain)
picking this:
as' = as'1 @ as''
as'' \<noteq> []
[PROOF STEP]
obtain a1 as'2
          where "as' = as'1@a1#as'2" and "as'' = a1#as'2"
[PROOF STATE]
proof (prove)
using this:
as' = as'1 @ as''
as'' \<noteq> []

goal (1 subgoal):
 1. (\<And>a1 as'2. \<lbrakk>as' = as'1 @ a1 # as'2; as'' = a1 # as'2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases as'') auto
[PROOF STATE]
proof (state)
this:
as' = as'1 @ a1 # as'2
as'' = a1 # as'2

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
have "asx' \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. asx' \<noteq> []
[PROOF STEP]
proof(cases "asx' = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. asx' = [] \<Longrightarrow> asx' \<noteq> []
 2. asx' \<noteq> [] \<Longrightarrow> asx' \<noteq> []
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
asx' = []

goal (2 subgoals):
 1. asx' = [] \<Longrightarrow> asx' \<noteq> []
 2. asx' \<noteq> [] \<Longrightarrow> asx' \<noteq> []
[PROOF STEP]
with \<open>asx = as'1@asx'\<close> \<open>as' = as'1@as''\<close> \<open>as'' = a1#as'2\<close>
[PROOF STATE]
proof (chain)
picking this:
asx = as'1 @ asx'
as' = as'1 @ as''
as'' = a1 # as'2
asx' = []
[PROOF STEP]
have "as' = asx@a1#as'2"
[PROOF STATE]
proof (prove)
using this:
asx = as'1 @ asx'
as' = as'1 @ as''
as'' = a1 # as'2
asx' = []

goal (1 subgoal):
 1. as' = asx @ a1 # as'2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
as' = asx @ a1 # as'2

goal (2 subgoals):
 1. asx' = [] \<Longrightarrow> asx' \<noteq> []
 2. asx' \<noteq> [] \<Longrightarrow> asx' \<noteq> []
[PROOF STEP]
with \<open>n' -a#as'\<rightarrow>\<^sub>\<iota>* n\<close>
[PROOF STATE]
proof (chain)
picking this:
n' -a # as'\<rightarrow>\<^sub>\<iota>* n
as' = asx @ a1 # as'2
[PROOF STEP]
have "n' -(a#asx)@a1#as'2\<rightarrow>\<^sub>\<iota>* n"
[PROOF STATE]
proof (prove)
using this:
n' -a # as'\<rightarrow>\<^sub>\<iota>* n
as' = asx @ a1 # as'2

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

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

goal (1 subgoal):
 1. n' -(a # asx) @ a1 # as'2\<rightarrow>* n &&& \<forall>ax\<in>set ((a # asx) @ a1 # as'2). intra_kind (kind ax)
[PROOF STEP]
by(simp_all add:intra_path_def)
[PROOF STATE]
proof (state)
this:
n' -(a # asx) @ a1 # as'2\<rightarrow>* n
\<forall>ax\<in>set ((a # asx) @ a1 # as'2). intra_kind (kind ax)

goal (2 subgoals):
 1. asx' = [] \<Longrightarrow> asx' \<noteq> []
 2. asx' \<noteq> [] \<Longrightarrow> asx' \<noteq> []
[PROOF STEP]
from \<open>n' -(a#asx)@a1#as'2\<rightarrow>* n\<close>
[PROOF STATE]
proof (chain)
picking this:
n' -(a # asx) @ a1 # as'2\<rightarrow>* n
[PROOF STEP]
have "n' -a#asx\<rightarrow>* sourcenode a1" and "valid_edge a1"
[PROOF STATE]
proof (prove)
using this:
n' -(a # asx) @ a1 # as'2\<rightarrow>* n

goal (1 subgoal):
 1. n' -a # asx\<rightarrow>* sourcenode a1 &&& valid_edge a1
[PROOF STEP]
by -(erule path_split)+
[PROOF STATE]
proof (state)
this:
n' -a # asx\<rightarrow>* sourcenode a1
valid_edge a1

goal (2 subgoals):
 1. asx' = [] \<Longrightarrow> asx' \<noteq> []
 2. asx' \<noteq> [] \<Longrightarrow> asx' \<noteq> []
[PROOF STEP]
from \<open>\<forall>ax \<in> set((a#asx)@a1#as'2). intra_kind(kind ax)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>ax\<in>set ((a # asx) @ a1 # as'2). intra_kind (kind ax)
[PROOF STEP]
have "\<forall>ax \<in> set(a#asx). intra_kind(kind ax)"
[PROOF STATE]
proof (prove)
using this:
\<forall>ax\<in>set ((a # asx) @ a1 # as'2). intra_kind (kind ax)

goal (1 subgoal):
 1. \<forall>ax\<in>set (a # asx). intra_kind (kind ax)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>ax\<in>set (a # asx). intra_kind (kind ax)

goal (2 subgoals):
 1. asx' = [] \<Longrightarrow> asx' \<noteq> []
 2. asx' \<noteq> [] \<Longrightarrow> asx' \<noteq> []
[PROOF STEP]
with \<open>n' -a#asx\<rightarrow>* sourcenode a1\<close>
[PROOF STATE]
proof (chain)
picking this:
n' -a # asx\<rightarrow>* sourcenode a1
\<forall>ax\<in>set (a # asx). intra_kind (kind ax)
[PROOF STEP]
have "n' -a#asx\<rightarrow>\<^sub>\<iota>* sourcenode a1"
[PROOF STATE]
proof (prove)
using this:
n' -a # asx\<rightarrow>* sourcenode a1
\<forall>ax\<in>set (a # asx). intra_kind (kind ax)

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

goal (2 subgoals):
 1. asx' = [] \<Longrightarrow> asx' \<noteq> []
 2. asx' \<noteq> [] \<Longrightarrow> asx' \<noteq> []
[PROOF STEP]
hence "targetnode a -asx\<rightarrow>\<^sub>\<iota>* sourcenode a1"
[PROOF STATE]
proof (prove)
using this:
n' -a # asx\<rightarrow>\<^sub>\<iota>* sourcenode a1

goal (1 subgoal):
 1. targetnode a -asx\<rightarrow>\<^sub>\<iota>* sourcenode a1
[PROOF STEP]
by(fastforce intro:path_split_Cons simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
targetnode a -asx\<rightarrow>\<^sub>\<iota>* sourcenode a1

goal (2 subgoals):
 1. asx' = [] \<Longrightarrow> asx' \<noteq> []
 2. asx' \<noteq> [] \<Longrightarrow> asx' \<noteq> []
[PROOF STEP]
with \<open>targetnode a -asx\<rightarrow>\<^sub>\<iota>* pex\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a -asx\<rightarrow>\<^sub>\<iota>* pex
targetnode a -asx\<rightarrow>\<^sub>\<iota>* sourcenode a1
[PROOF STEP]
have "pex = sourcenode a1"
[PROOF STATE]
proof (prove)
using this:
targetnode a -asx\<rightarrow>\<^sub>\<iota>* pex
targetnode a -asx\<rightarrow>\<^sub>\<iota>* sourcenode a1

goal (1 subgoal):
 1. pex = sourcenode a1
[PROOF STEP]
by(fastforce intro:path_det simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
pex = sourcenode a1

goal (2 subgoals):
 1. asx' = [] \<Longrightarrow> asx' \<noteq> []
 2. asx' \<noteq> [] \<Longrightarrow> asx' \<noteq> []
[PROOF STEP]
from \<open>\<forall>ax \<in> set((a#asx)@a1#as'2). intra_kind(kind ax)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>ax\<in>set ((a # asx) @ a1 # as'2). intra_kind (kind ax)
[PROOF STEP]
have "intra_kind (kind a1)"
[PROOF STATE]
proof (prove)
using this:
\<forall>ax\<in>set ((a # asx) @ a1 # as'2). intra_kind (kind ax)

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

goal (2 subgoals):
 1. asx' = [] \<Longrightarrow> asx' \<noteq> []
 2. asx' \<noteq> [] \<Longrightarrow> asx' \<noteq> []
[PROOF STEP]
from \<open>method_exit pex\<close>
[PROOF STATE]
proof (chain)
picking this:
method_exit pex
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
method_exit pex

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

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

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

goal (2 subgoals):
 1. pex = (_Exit_) \<Longrightarrow> False
 2. \<And>a Q f p. \<lbrakk>pex = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with \<open>valid_edge a1\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a1
sourcenode a1 = (_Exit_)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
valid_edge a1
sourcenode a1 = (_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>pex = 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>pex = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix a Q f p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a Q f p. \<lbrakk>pex = sourcenode a; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "pex = sourcenode a" and "valid_edge a"
              and "kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f"
[PROOF STATE]
proof (state)
this:
pex = sourcenode a
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f

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

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 (2 subgoals):
 1. asx' = [] \<Longrightarrow> asx' \<noteq> []
 2. asx' \<noteq> [] \<Longrightarrow> asx' \<noteq> []
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

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

goal (1 subgoal):
 1. asx' \<noteq> [] \<Longrightarrow> asx' \<noteq> []
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
asx' \<noteq> []

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
with \<open>asx = as'1@asx'\<close>
[PROOF STATE]
proof (chain)
picking this:
asx = as'1 @ asx'
asx' \<noteq> []
[PROOF STEP]
obtain a2 asx'1
          where "asx = as'1@a2#asx'1"
          and "asx' = a2#asx'1"
[PROOF STATE]
proof (prove)
using this:
asx = as'1 @ asx'
asx' \<noteq> []

goal (1 subgoal):
 1. (\<And>a2 asx'1. \<lbrakk>asx = as'1 @ a2 # asx'1; asx' = a2 # asx'1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases asx') auto
[PROOF STATE]
proof (state)
this:
asx = as'1 @ a2 # asx'1
asx' = a2 # asx'1

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
from \<open>n' -a#as'\<rightarrow>\<^sub>\<iota>* n\<close> \<open>as' = as'1@a1#as'2\<close>
[PROOF STATE]
proof (chain)
picking this:
n' -a # as'\<rightarrow>\<^sub>\<iota>* n
as' = as'1 @ a1 # as'2
[PROOF STEP]
have "n' -(a#as'1)@a1#as'2\<rightarrow>\<^sub>\<iota>* n"
[PROOF STATE]
proof (prove)
using this:
n' -a # as'\<rightarrow>\<^sub>\<iota>* n
as' = as'1 @ a1 # as'2

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

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
hence "n' -(a#as'1)@a1#as'2\<rightarrow>* n"
          and "\<forall>ax \<in> set((a#as'1)@a1#as'2). intra_kind(kind ax)"
[PROOF STATE]
proof (prove)
using this:
n' -(a # as'1) @ a1 # as'2\<rightarrow>\<^sub>\<iota>* n

goal (1 subgoal):
 1. n' -(a # as'1) @ a1 # as'2\<rightarrow>* n &&& \<forall>ax\<in>set ((a # as'1) @ a1 # as'2). intra_kind (kind ax)
[PROOF STEP]
by(simp_all add: intra_path_def)
[PROOF STATE]
proof (state)
this:
n' -(a # as'1) @ a1 # as'2\<rightarrow>* n
\<forall>ax\<in>set ((a # as'1) @ a1 # as'2). intra_kind (kind ax)

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
from \<open>n' -(a#as'1)@a1#as'2\<rightarrow>* n\<close>
[PROOF STATE]
proof (chain)
picking this:
n' -(a # as'1) @ a1 # as'2\<rightarrow>* n
[PROOF STEP]
have "n' -a#as'1\<rightarrow>* sourcenode a1"
          and "valid_edge a1"
[PROOF STATE]
proof (prove)
using this:
n' -(a # as'1) @ a1 # as'2\<rightarrow>* n

goal (1 subgoal):
 1. n' -a # as'1\<rightarrow>* sourcenode a1 &&& valid_edge a1
[PROOF STEP]
by -(erule path_split)+
[PROOF STATE]
proof (state)
this:
n' -a # as'1\<rightarrow>* sourcenode a1
valid_edge a1

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
from \<open>\<forall>ax \<in> set((a#as'1)@a1#as'2). intra_kind(kind ax)\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>ax\<in>set ((a # as'1) @ a1 # as'2). intra_kind (kind ax)
[PROOF STEP]
have "\<forall>ax \<in> set(a#as'1). intra_kind(kind ax)"
[PROOF STATE]
proof (prove)
using this:
\<forall>ax\<in>set ((a # as'1) @ a1 # as'2). intra_kind (kind ax)

goal (1 subgoal):
 1. \<forall>ax\<in>set (a # as'1). intra_kind (kind ax)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>ax\<in>set (a # as'1). intra_kind (kind ax)

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
with \<open>n' -a#as'1\<rightarrow>* sourcenode a1\<close>
[PROOF STATE]
proof (chain)
picking this:
n' -a # as'1\<rightarrow>* sourcenode a1
\<forall>ax\<in>set (a # as'1). intra_kind (kind ax)
[PROOF STEP]
have "n' -a#as'1\<rightarrow>\<^sub>\<iota>* sourcenode a1"
[PROOF STATE]
proof (prove)
using this:
n' -a # as'1\<rightarrow>* sourcenode a1
\<forall>ax\<in>set (a # as'1). intra_kind (kind ax)

goal (1 subgoal):
 1. n' -a # as'1\<rightarrow>\<^sub>\<iota>* sourcenode a1
[PROOF STEP]
by(simp add:intra_path_def)
[PROOF STATE]
proof (state)
this:
n' -a # as'1\<rightarrow>\<^sub>\<iota>* sourcenode a1

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
hence "targetnode a -as'1\<rightarrow>\<^sub>\<iota>* sourcenode a1"
[PROOF STATE]
proof (prove)
using this:
n' -a # as'1\<rightarrow>\<^sub>\<iota>* sourcenode a1

goal (1 subgoal):
 1. targetnode a -as'1\<rightarrow>\<^sub>\<iota>* sourcenode a1
[PROOF STEP]
by(fastforce intro:path_split_Cons simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
targetnode a -as'1\<rightarrow>\<^sub>\<iota>* sourcenode a1

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
from \<open>targetnode a -asx\<rightarrow>\<^sub>\<iota>* pex\<close> \<open>asx = as'1@a2#asx'1\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a -asx\<rightarrow>\<^sub>\<iota>* pex
asx = as'1 @ a2 # asx'1
[PROOF STEP]
have "targetnode a -as'1@a2#asx'1\<rightarrow>* pex"
[PROOF STATE]
proof (prove)
using this:
targetnode a -asx\<rightarrow>\<^sub>\<iota>* pex
asx = as'1 @ a2 # asx'1

goal (1 subgoal):
 1. targetnode a -as'1 @ a2 # asx'1\<rightarrow>* pex
[PROOF STEP]
by(simp add:intra_path_def)
[PROOF STATE]
proof (state)
this:
targetnode a -as'1 @ a2 # asx'1\<rightarrow>* pex

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
hence "targetnode a -as'1\<rightarrow>* sourcenode a2" and "valid_edge a2"
          and "targetnode a2 -asx'1\<rightarrow>* pex"
[PROOF STATE]
proof (prove)
using this:
targetnode a -as'1 @ a2 # asx'1\<rightarrow>* pex

goal (1 subgoal):
 1. targetnode a -as'1\<rightarrow>* sourcenode a2 &&& valid_edge a2 &&& targetnode a2 -asx'1\<rightarrow>* pex
[PROOF STEP]
by(auto intro:path_split)
[PROOF STATE]
proof (state)
this:
targetnode a -as'1\<rightarrow>* sourcenode a2
valid_edge a2
targetnode a2 -asx'1\<rightarrow>* pex

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
from \<open>targetnode a2 -asx'1\<rightarrow>* pex\<close> \<open>asx = as'1@a2#asx'1\<close>
          \<open>targetnode a -asx\<rightarrow>\<^sub>\<iota>* pex\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a2 -asx'1\<rightarrow>* pex
asx = as'1 @ a2 # asx'1
targetnode a -asx\<rightarrow>\<^sub>\<iota>* pex
[PROOF STEP]
have "targetnode a2 -asx'1\<rightarrow>\<^sub>\<iota>* pex"
[PROOF STATE]
proof (prove)
using this:
targetnode a2 -asx'1\<rightarrow>* pex
asx = as'1 @ a2 # asx'1
targetnode a -asx\<rightarrow>\<^sub>\<iota>* pex

goal (1 subgoal):
 1. targetnode a2 -asx'1\<rightarrow>\<^sub>\<iota>* pex
[PROOF STEP]
by(simp add:intra_path_def)
[PROOF STATE]
proof (state)
this:
targetnode a2 -asx'1\<rightarrow>\<^sub>\<iota>* pex

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
from \<open>targetnode a -as'1\<rightarrow>* sourcenode a2\<close>
          \<open>targetnode a -as'1\<rightarrow>\<^sub>\<iota>* sourcenode a1\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a -as'1\<rightarrow>* sourcenode a2
targetnode a -as'1\<rightarrow>\<^sub>\<iota>* sourcenode a1
[PROOF STEP]
have "sourcenode a1 = sourcenode a2"
[PROOF STATE]
proof (prove)
using this:
targetnode a -as'1\<rightarrow>* sourcenode a2
targetnode a -as'1\<rightarrow>\<^sub>\<iota>* sourcenode a1

goal (1 subgoal):
 1. sourcenode a1 = sourcenode a2
[PROOF STEP]
by(fastforce intro:path_det simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
sourcenode a1 = sourcenode a2

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
from \<open>asx = as'1@a2#asx'1\<close> \<open>n \<notin> set (sourcenodes asx)\<close>
[PROOF STATE]
proof (chain)
picking this:
asx = as'1 @ a2 # asx'1
n \<notin> set (sourcenodes asx)
[PROOF STEP]
have "n \<notin> set (sourcenodes asx'1)"
[PROOF STATE]
proof (prove)
using this:
asx = as'1 @ a2 # asx'1
n \<notin> set (sourcenodes asx)

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

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
with \<open>targetnode a2 -asx'1\<rightarrow>\<^sub>\<iota>* pex\<close> \<open>method_exit pex\<close>
          \<open>asx = as'1@a2#asx'1\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode a2 -asx'1\<rightarrow>\<^sub>\<iota>* pex
method_exit pex
asx = as'1 @ a2 # asx'1
n \<notin> set (sourcenodes asx'1)
[PROOF STEP]
have "\<not> n postdominates targetnode a2"
[PROOF STATE]
proof (prove)
using this:
targetnode a2 -asx'1\<rightarrow>\<^sub>\<iota>* pex
method_exit pex
asx = as'1 @ a2 # asx'1
n \<notin> set (sourcenodes asx'1)

goal (1 subgoal):
 1. \<not> n postdominates targetnode a2
[PROOF STEP]
by(fastforce simp:postdominate_def)
[PROOF STATE]
proof (state)
this:
\<not> n postdominates targetnode a2

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
from \<open>asx = as'1@a2#asx'1\<close> \<open>targetnode a -asx\<rightarrow>\<^sub>\<iota>* pex\<close>
[PROOF STATE]
proof (chain)
picking this:
asx = as'1 @ a2 # asx'1
targetnode a -asx\<rightarrow>\<^sub>\<iota>* pex
[PROOF STEP]
have "intra_kind (kind a2)"
[PROOF STATE]
proof (prove)
using this:
asx = as'1 @ a2 # asx'1
targetnode a -asx\<rightarrow>\<^sub>\<iota>* pex

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

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
from \<open>as' = as'1@a1#as'2\<close>
[PROOF STATE]
proof (chain)
picking this:
as' = as'1 @ a1 # as'2
[PROOF STEP]
have "a1 \<in> set as'"
[PROOF STATE]
proof (prove)
using this:
as' = as'1 @ a1 # as'2

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

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
with \<open>sourcenode a1 = sourcenode a2\<close> last \<open>valid_edge a2\<close>
          \<open>intra_kind (kind a2)\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode a1 = sourcenode a2
\<forall>ax ax'. ax \<in> set as' \<and> sourcenode ax = sourcenode ax' \<and> valid_edge ax' \<and> intra_kind (kind ax') \<longrightarrow> n postdominates targetnode ax'
valid_edge a2
intra_kind (kind a2)
a1 \<in> set as'
[PROOF STEP]
have "n postdominates targetnode a2"
[PROOF STATE]
proof (prove)
using this:
sourcenode a1 = sourcenode a2
\<forall>ax ax'. ax \<in> set as' \<and> sourcenode ax = sourcenode ax' \<and> valid_edge ax' \<and> intra_kind (kind ax') \<longrightarrow> n postdominates targetnode ax'
valid_edge a2
intra_kind (kind a2)
a1 \<in> set as'

goal (1 subgoal):
 1. n postdominates targetnode a2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n postdominates targetnode a2

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
with \<open>\<not> n postdominates targetnode a2\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> n postdominates targetnode a2
n postdominates targetnode a2
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
\<not> n postdominates targetnode a2
n postdominates targetnode a2

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

goal (1 subgoal):
 1. \<nexists>asx'. asx = as' @ asx' \<Longrightarrow> n' controls n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cdep_edge_cases:
  "\<lbrakk>n \<longrightarrow>\<^bsub>cd\<^esub> n'; (parent_node n) controls (parent_node n') \<Longrightarrow> P;
    \<And>a Q r p fs a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a;
                  parent_node n = targetnode a; parent_node n' = sourcenode a'\<rbrakk> \<Longrightarrow> P;
    \<And>m. \<lbrakk>n = CFG_node m; m = parent_node n'; n \<noteq> n'\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<longrightarrow>\<^bsub>cd\<^esub> n'; parent_node n controls parent_node n' \<Longrightarrow> P; \<And>a Q r p fs a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; parent_node n = targetnode a; parent_node n' = sourcenode a'\<rbrakk> \<Longrightarrow> P; \<And>m. \<lbrakk>n = CFG_node m; m = parent_node n'; n \<noteq> n'\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by -(erule SDG_edge.cases,auto)