[STATEMENT]
lemma realizable_valid_CFG_path:
  assumes "realizable n ns n'"
  obtains as where "parent_node n -as\<rightarrow>\<^sub>\<surd>* parent_node n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>as. parent_node n -as\<rightarrow>\<^sub>\<surd>* parent_node n' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<surd>* parent_node n'
[PROOF STEP]
from \<open>realizable n ns n'\<close>
[PROOF STATE]
proof (chain)
picking this:
realizable n ns n'
[PROOF STEP]
show "\<exists>as. parent_node n -as\<rightarrow>\<^sub>\<surd>* parent_node n'"
[PROOF STATE]
proof (prove)
using this:
realizable n ns n'

goal (1 subgoal):
 1. \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<surd>* parent_node n'
[PROOF STEP]
proof(induct rule:realizable.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n ns n'. matched n ns n' \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<surd>* parent_node n'
 2. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns' n\<^sub>3. \<lbrakk>realizable n\<^sub>0 ns n\<^sub>1; \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>3
[PROOF STEP]
case (realizable_matched n ns n')
[PROOF STATE]
proof (state)
this:
matched n ns n'

goal (2 subgoals):
 1. \<And>n ns n'. matched n ns n' \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<surd>* parent_node n'
 2. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns' n\<^sub>3. \<lbrakk>realizable n\<^sub>0 ns n\<^sub>1; \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>3
[PROOF STEP]
from \<open>matched n ns n'\<close>
[PROOF STATE]
proof (chain)
picking this:
matched n ns n'
[PROOF STEP]
obtain as where "parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n'"
[PROOF STATE]
proof (prove)
using this:
matched n ns n'

goal (1 subgoal):
 1. (\<And>as. parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule matched_same_level_CFG_path)
[PROOF STATE]
proof (state)
this:
parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n'

goal (2 subgoals):
 1. \<And>n ns n'. matched n ns n' \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<surd>* parent_node n'
 2. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns' n\<^sub>3. \<lbrakk>realizable n\<^sub>0 ns n\<^sub>1; \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>3
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n'

goal (1 subgoal):
 1. \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<surd>* parent_node n'
[PROOF STEP]
by(fastforce intro:slp_vp)
[PROOF STATE]
proof (state)
this:
\<exists>as. parent_node n -as\<rightarrow>\<^sub>\<surd>* parent_node n'

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns' n\<^sub>3. \<lbrakk>realizable n\<^sub>0 ns n\<^sub>1; \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>3
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns' n\<^sub>3. \<lbrakk>realizable n\<^sub>0 ns n\<^sub>1; \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>3
[PROOF STEP]
case (realizable_call n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns' n\<^sub>3)
[PROOF STATE]
proof (state)
this:
realizable n\<^sub>0 ns n\<^sub>1
\<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1
n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2
matched n\<^sub>2 ns' n\<^sub>3

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns' n\<^sub>3. \<lbrakk>realizable n\<^sub>0 ns n\<^sub>1; \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>3
[PROOF STEP]
from \<open>\<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1
[PROOF STEP]
obtain as where "parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
\<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1

goal (1 subgoal):
 1. (\<And>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns' n\<^sub>3. \<lbrakk>realizable n\<^sub>0 ns n\<^sub>1; \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>3
[PROOF STEP]
from \<open>matched n\<^sub>2 ns' n\<^sub>3\<close>
[PROOF STATE]
proof (chain)
picking this:
matched n\<^sub>2 ns' n\<^sub>3
[PROOF STEP]
obtain as' where "parent_node n\<^sub>2 -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3"
[PROOF STATE]
proof (prove)
using this:
matched n\<^sub>2 ns' n\<^sub>3

goal (1 subgoal):
 1. (\<And>as'. parent_node n\<^sub>2 -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(erule matched_same_level_CFG_path)
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>2 -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns' n\<^sub>3. \<lbrakk>realizable n\<^sub>0 ns n\<^sub>1; \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>3
[PROOF STEP]
from \<open>n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2\<close>
[PROOF STATE]
proof (chain)
picking this:
n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2
[PROOF STEP]
obtain a Q r fs where "valid_edge a"
      and "sourcenode a = parent_node n\<^sub>1" and "targetnode a = parent_node n\<^sub>2"
      and "kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs"
[PROOF STATE]
proof (prove)
using this:
n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2

goal (1 subgoal):
 1. (\<And>a Q r fs. \<lbrakk>valid_edge a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:SDG_edge.cases)+
[PROOF STATE]
proof (state)
this:
valid_edge a
sourcenode a = parent_node n\<^sub>1
targetnode a = parent_node n\<^sub>2
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns' n\<^sub>3. \<lbrakk>realizable n\<^sub>0 ns n\<^sub>1; \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>3
[PROOF STEP]
hence "parent_node n\<^sub>1 -[a]\<rightarrow>* parent_node n\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
sourcenode a = parent_node n\<^sub>1
targetnode a = parent_node n\<^sub>2
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. parent_node n\<^sub>1 -[a]\<rightarrow>* parent_node n\<^sub>2
[PROOF STEP]
by(fastforce dest:path_edge)
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>1 -[a]\<rightarrow>* parent_node n\<^sub>2

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns' n\<^sub>3. \<lbrakk>realizable n\<^sub>0 ns n\<^sub>1; \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>3
[PROOF STEP]
from \<open>parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1
[PROOF STEP]
have "parent_node n\<^sub>0 -as\<rightarrow>* parent_node n\<^sub>1" and "valid_path as"
[PROOF STATE]
proof (prove)
using this:
parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1

goal (1 subgoal):
 1. parent_node n\<^sub>0 -as\<rightarrow>* parent_node n\<^sub>1 &&& valid_path as
[PROOF STEP]
by(simp_all add:vp_def)
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>0 -as\<rightarrow>* parent_node n\<^sub>1
valid_path as

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns' n\<^sub>3. \<lbrakk>realizable n\<^sub>0 ns n\<^sub>1; \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>3
[PROOF STEP]
with \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
parent_node n\<^sub>0 -as\<rightarrow>* parent_node n\<^sub>1
valid_path as
[PROOF STEP]
have "valid_path (as@[a])"
[PROOF STATE]
proof (prove)
using this:
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
parent_node n\<^sub>0 -as\<rightarrow>* parent_node n\<^sub>1
valid_path as

goal (1 subgoal):
 1. valid_path (as @ [a])
[PROOF STEP]
by(fastforce elim:valid_path_aux_Append simp:valid_path_def)
[PROOF STATE]
proof (state)
this:
valid_path (as @ [a])

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns' n\<^sub>3. \<lbrakk>realizable n\<^sub>0 ns n\<^sub>1; \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>3
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
valid_path (as @ [a])

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns' n\<^sub>3. \<lbrakk>realizable n\<^sub>0 ns n\<^sub>1; \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>3
[PROOF STEP]
from \<open>parent_node n\<^sub>0 -as\<rightarrow>* parent_node n\<^sub>1\<close> \<open>parent_node n\<^sub>1 -[a]\<rightarrow>* parent_node n\<^sub>2\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n\<^sub>0 -as\<rightarrow>* parent_node n\<^sub>1
parent_node n\<^sub>1 -[a]\<rightarrow>* parent_node n\<^sub>2
[PROOF STEP]
have "parent_node n\<^sub>0 -as@[a]\<rightarrow>* parent_node n\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
parent_node n\<^sub>0 -as\<rightarrow>* parent_node n\<^sub>1
parent_node n\<^sub>1 -[a]\<rightarrow>* parent_node n\<^sub>2

goal (1 subgoal):
 1. parent_node n\<^sub>0 -as @ [a]\<rightarrow>* parent_node n\<^sub>2
[PROOF STEP]
by(rule path_Append)
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>0 -as @ [a]\<rightarrow>* parent_node n\<^sub>2

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns' n\<^sub>3. \<lbrakk>realizable n\<^sub>0 ns n\<^sub>1; \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>3
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
valid_path (as @ [a])
parent_node n\<^sub>0 -as @ [a]\<rightarrow>* parent_node n\<^sub>2
[PROOF STEP]
have "parent_node n\<^sub>0 -as@[a]\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>2"
[PROOF STATE]
proof (prove)
using this:
valid_path (as @ [a])
parent_node n\<^sub>0 -as @ [a]\<rightarrow>* parent_node n\<^sub>2

goal (1 subgoal):
 1. parent_node n\<^sub>0 -as @ [a]\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>2
[PROOF STEP]
by(simp add:vp_def)
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>0 -as @ [a]\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>2

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns' n\<^sub>3. \<lbrakk>realizable n\<^sub>0 ns n\<^sub>1; \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>3
[PROOF STEP]
with \<open>parent_node n\<^sub>2 -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n\<^sub>2 -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3
parent_node n\<^sub>0 -as @ [a]\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>2
[PROOF STEP]
have "parent_node n\<^sub>0 -(as@[a])@as'\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>3"
[PROOF STATE]
proof (prove)
using this:
parent_node n\<^sub>2 -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3
parent_node n\<^sub>0 -as @ [a]\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>2

goal (1 subgoal):
 1. parent_node n\<^sub>0 -(as @ [a]) @ as'\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>3
[PROOF STEP]
by -(rule vp_slp_Append)
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>0 -(as @ [a]) @ as'\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>3

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns' n\<^sub>3. \<lbrakk>realizable n\<^sub>0 ns n\<^sub>1; \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>3
[PROOF STEP]
with \<open>sourcenode a = parent_node n\<^sub>1\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode a = parent_node n\<^sub>1
parent_node n\<^sub>0 -(as @ [a]) @ as'\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>3
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sourcenode a = parent_node n\<^sub>1
parent_node n\<^sub>0 -(as @ [a]) @ as'\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>3

goal (1 subgoal):
 1. \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>3
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<surd>* parent_node n\<^sub>3

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>as. parent_node n -as\<rightarrow>\<^sub>\<surd>* parent_node n'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cdep_SDG_path_realizable:
  "n cc-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> realizable n ns n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n cc-ns\<rightarrow>\<^sub>d* n' \<Longrightarrow> realizable n ns n'
[PROOF STEP]
proof(induct rule:call_cdep_SDG_path.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n. valid_SDG_node n \<Longrightarrow> realizable n [] n
 2. \<And>n ns n'' n'. \<lbrakk>n cc-ns\<rightarrow>\<^sub>d* n''; realizable n ns n''; n'' \<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> realizable n (ns @ [n'']) n'
 3. \<And>n ns n'' p n'. \<lbrakk>n cc-ns\<rightarrow>\<^sub>d* n''; realizable n ns n''; n'' -p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> realizable n (ns @ [n'']) n'
[PROOF STEP]
case (ccSp_Nil n)
[PROOF STATE]
proof (state)
this:
valid_SDG_node n

goal (3 subgoals):
 1. \<And>n. valid_SDG_node n \<Longrightarrow> realizable n [] n
 2. \<And>n ns n'' n'. \<lbrakk>n cc-ns\<rightarrow>\<^sub>d* n''; realizable n ns n''; n'' \<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> realizable n (ns @ [n'']) n'
 3. \<And>n ns n'' p n'. \<lbrakk>n cc-ns\<rightarrow>\<^sub>d* n''; realizable n ns n''; n'' -p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> realizable n (ns @ [n'']) n'
[PROOF STEP]
from \<open>valid_SDG_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n

goal (1 subgoal):
 1. realizable n [] n
[PROOF STEP]
by(fastforce intro:realizable_matched matched_Nil)
[PROOF STATE]
proof (state)
this:
realizable n [] n

goal (2 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n cc-ns\<rightarrow>\<^sub>d* n''; realizable n ns n''; n'' \<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> realizable n (ns @ [n'']) n'
 2. \<And>n ns n'' p n'. \<lbrakk>n cc-ns\<rightarrow>\<^sub>d* n''; realizable n ns n''; n'' -p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> realizable n (ns @ [n'']) n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n cc-ns\<rightarrow>\<^sub>d* n''; realizable n ns n''; n'' \<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> realizable n (ns @ [n'']) n'
 2. \<And>n ns n'' p n'. \<lbrakk>n cc-ns\<rightarrow>\<^sub>d* n''; realizable n ns n''; n'' -p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> realizable n (ns @ [n'']) n'
[PROOF STEP]
case (ccSp_Append_cdep n ns n'' n')
[PROOF STATE]
proof (state)
this:
n cc-ns\<rightarrow>\<^sub>d* n''
realizable n ns n''
n'' \<longrightarrow>\<^bsub>cd\<^esub> n'

goal (2 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n cc-ns\<rightarrow>\<^sub>d* n''; realizable n ns n''; n'' \<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> realizable n (ns @ [n'']) n'
 2. \<And>n ns n'' p n'. \<lbrakk>n cc-ns\<rightarrow>\<^sub>d* n''; realizable n ns n''; n'' -p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> realizable n (ns @ [n'']) n'
[PROOF STEP]
from \<open>n'' \<longrightarrow>\<^bsub>cd\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' \<longrightarrow>\<^bsub>cd\<^esub> n'
[PROOF STEP]
have "valid_SDG_node n''"
[PROOF STATE]
proof (prove)
using this:
n'' \<longrightarrow>\<^bsub>cd\<^esub> n'

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

goal (2 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n cc-ns\<rightarrow>\<^sub>d* n''; realizable n ns n''; n'' \<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> realizable n (ns @ [n'']) n'
 2. \<And>n ns n'' p n'. \<lbrakk>n cc-ns\<rightarrow>\<^sub>d* n''; realizable n ns n''; n'' -p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> realizable n (ns @ [n'']) n'
[PROOF STEP]
hence "matched n'' [] n''"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n''

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

goal (2 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n cc-ns\<rightarrow>\<^sub>d* n''; realizable n ns n''; n'' \<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> realizable n (ns @ [n'']) n'
 2. \<And>n ns n'' p n'. \<lbrakk>n cc-ns\<rightarrow>\<^sub>d* n''; realizable n ns n''; n'' -p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> realizable n (ns @ [n'']) n'
[PROOF STEP]
from \<open>n'' \<longrightarrow>\<^bsub>cd\<^esub> n'\<close> \<open>valid_SDG_node n''\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' \<longrightarrow>\<^bsub>cd\<^esub> n'
valid_SDG_node n''
[PROOF STEP]
have "n'' i-[]@[n'']\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
n'' \<longrightarrow>\<^bsub>cd\<^esub> n'
valid_SDG_node n''

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

goal (2 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n cc-ns\<rightarrow>\<^sub>d* n''; realizable n ns n''; n'' \<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> realizable n (ns @ [n'']) n'
 2. \<And>n ns n'' p n'. \<lbrakk>n cc-ns\<rightarrow>\<^sub>d* n''; realizable n ns n''; n'' -p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> realizable n (ns @ [n'']) n'
[PROOF STEP]
with \<open>matched n'' [] n''\<close>
[PROOF STATE]
proof (chain)
picking this:
matched n'' [] n''
n'' i-[] @ [n'']\<rightarrow>\<^sub>d* n'
[PROOF STEP]
have "matched n'' ([]@[n'']) n'"
[PROOF STATE]
proof (prove)
using this:
matched n'' [] n''
n'' i-[] @ [n'']\<rightarrow>\<^sub>d* n'

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

goal (2 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n cc-ns\<rightarrow>\<^sub>d* n''; realizable n ns n''; n'' \<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> realizable n (ns @ [n'']) n'
 2. \<And>n ns n'' p n'. \<lbrakk>n cc-ns\<rightarrow>\<^sub>d* n''; realizable n ns n''; n'' -p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> realizable n (ns @ [n'']) n'
[PROOF STEP]
with \<open>realizable n ns n''\<close>
[PROOF STATE]
proof (chain)
picking this:
realizable n ns n''
matched n'' ([] @ [n'']) n'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
realizable n ns n''
matched n'' ([] @ [n'']) n'

goal (1 subgoal):
 1. realizable n (ns @ [n'']) n'
[PROOF STEP]
by(fastforce intro:realizable_Append_matched)
[PROOF STATE]
proof (state)
this:
realizable n (ns @ [n'']) n'

goal (1 subgoal):
 1. \<And>n ns n'' p n'. \<lbrakk>n cc-ns\<rightarrow>\<^sub>d* n''; realizable n ns n''; n'' -p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> realizable n (ns @ [n'']) n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n ns n'' p n'. \<lbrakk>n cc-ns\<rightarrow>\<^sub>d* n''; realizable n ns n''; n'' -p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> realizable n (ns @ [n'']) n'
[PROOF STEP]
case (ccSp_Append_call n ns n'' p n')
[PROOF STATE]
proof (state)
this:
n cc-ns\<rightarrow>\<^sub>d* n''
realizable n ns n''
n'' -p\<rightarrow>\<^bsub>call\<^esub> n'

goal (1 subgoal):
 1. \<And>n ns n'' p n'. \<lbrakk>n cc-ns\<rightarrow>\<^sub>d* n''; realizable n ns n''; n'' -p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> realizable n (ns @ [n'']) n'
[PROOF STEP]
from \<open>n'' -p\<rightarrow>\<^bsub>call\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' -p\<rightarrow>\<^bsub>call\<^esub> n'
[PROOF STEP]
have "valid_SDG_node n'"
[PROOF STATE]
proof (prove)
using this:
n'' -p\<rightarrow>\<^bsub>call\<^esub> n'

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

goal (1 subgoal):
 1. \<And>n ns n'' p n'. \<lbrakk>n cc-ns\<rightarrow>\<^sub>d* n''; realizable n ns n''; n'' -p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> realizable n (ns @ [n'']) n'
[PROOF STEP]
hence "matched n' [] n'"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n'

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

goal (1 subgoal):
 1. \<And>n ns n'' p n'. \<lbrakk>n cc-ns\<rightarrow>\<^sub>d* n''; realizable n ns n''; n'' -p\<rightarrow>\<^bsub>call\<^esub> n'\<rbrakk> \<Longrightarrow> realizable n (ns @ [n'']) n'
[PROOF STEP]
with \<open>realizable n ns n''\<close> \<open>n'' -p\<rightarrow>\<^bsub>call\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
realizable n ns n''
n'' -p\<rightarrow>\<^bsub>call\<^esub> n'
matched n' [] n'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
realizable n ns n''
n'' -p\<rightarrow>\<^bsub>call\<^esub> n'
matched n' [] n'

goal (1 subgoal):
 1. realizable n (ns @ [n'']) n'
[PROOF STEP]
by(fastforce intro:realizable_call)
[PROOF STATE]
proof (state)
this:
realizable n (ns @ [n'']) n'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_edge_cases:
  "\<lbrakk>n s-p\<rightarrow>\<^bsub>sum\<^esub> n';
    \<And>a Q r fs a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a;
                n = CFG_node (sourcenode a); n' = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> P;
    \<And>a Q p r fs a' ns x x' ins outs.
      \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a;
       matched (Formal_in (targetnode a,x)) ns (Formal_out (sourcenode a',x'));
       n = Actual_in (sourcenode a,x); n' = Actual_out (targetnode a',x');
       (p,ins,outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> P\<rbrakk>
  \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n s-p\<rightarrow>\<^bsub>sum\<^esub> n'; \<And>a Q r fs a'. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; n = CFG_node (sourcenode a); n' = CFG_node (targetnode a')\<rbrakk> \<Longrightarrow> P; \<And>a Q p r fs a' ns x x' ins outs. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; a' \<in> get_return_edges a; matched (Formal_in (targetnode a, x)) ns (Formal_out (sourcenode a', x')); n = Actual_in (sourcenode a, x); n' = Actual_out (targetnode a', x'); (p, ins, outs) \<in> set procs; x < length ins; x' < length outs\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by -(erule sum_SDG_edge.cases,auto)


[STATEMENT]
lemma SDG_edge_sum_SDG_edge:
  "SDG_edge n Vopt popt n' \<Longrightarrow> sum_SDG_edge n Vopt popt False n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SDG_edge n Vopt popt n' \<Longrightarrow> sum_SDG_edge n Vopt popt False n'
[PROOF STEP]
by(induct rule:SDG_edge.induct,auto intro:sum_SDG_edge.intros)


[STATEMENT]
lemma sum_SDG_edge_SDG_edge:
  "sum_SDG_edge n Vopt popt False n' \<Longrightarrow> SDG_edge n Vopt popt n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_SDG_edge n Vopt popt False n' \<Longrightarrow> SDG_edge n Vopt popt n'
[PROOF STEP]
by(induct n Vopt popt x\<equiv>"False" n' rule:sum_SDG_edge.induct,
   auto intro:SDG_edge.intros)


[STATEMENT]
lemma sum_SDG_edge_valid_SDG_node:
  assumes "sum_SDG_edge n Vopt popt b n'"
  shows "valid_SDG_node n" and "valid_SDG_node n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_SDG_node n &&& valid_SDG_node n'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. valid_SDG_node n
 2. valid_SDG_node n'
[PROOF STEP]
have "valid_SDG_node n \<and> valid_SDG_node n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. valid_SDG_node n \<and> valid_SDG_node n'
[PROOF STEP]
proof(cases b)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b \<Longrightarrow> valid_SDG_node n \<and> valid_SDG_node n'
 2. \<not> b \<Longrightarrow> valid_SDG_node n \<and> valid_SDG_node n'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b

goal (2 subgoals):
 1. b \<Longrightarrow> valid_SDG_node n \<and> valid_SDG_node n'
 2. \<not> b \<Longrightarrow> valid_SDG_node n \<and> valid_SDG_node n'
[PROOF STEP]
with \<open>sum_SDG_edge n Vopt popt b n'\<close>
[PROOF STATE]
proof (chain)
picking this:
sum_SDG_edge n Vopt popt b n'
b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum_SDG_edge n Vopt popt b n'
b

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. valid_edge a'
[PROOF STEP]
by(rule get_return_edges_valid)
[PROOF STATE]
proof (state)
this:
valid_edge a'

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> b \<Longrightarrow> valid_SDG_node n \<and> valid_SDG_node n'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> b \<Longrightarrow> valid_SDG_node n \<and> valid_SDG_node n'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> b

goal (1 subgoal):
 1. \<not> b \<Longrightarrow> valid_SDG_node n \<and> valid_SDG_node n'
[PROOF STEP]
with \<open>sum_SDG_edge n Vopt popt b n'\<close>
[PROOF STATE]
proof (chain)
picking this:
sum_SDG_edge n Vopt popt b n'
\<not> b
[PROOF STEP]
have "SDG_edge n Vopt popt n'"
[PROOF STATE]
proof (prove)
using this:
sum_SDG_edge n Vopt popt b n'
\<not> b

goal (1 subgoal):
 1. SDG_edge n Vopt popt n'
[PROOF STEP]
by(fastforce intro:sum_SDG_edge_SDG_edge)
[PROOF STATE]
proof (state)
this:
SDG_edge n Vopt popt n'

goal (1 subgoal):
 1. \<not> b \<Longrightarrow> valid_SDG_node n \<and> valid_SDG_node n'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
SDG_edge n Vopt popt n'

goal (1 subgoal):
 1. valid_SDG_node n \<and> valid_SDG_node n'
[PROOF STEP]
by(fastforce intro:SDG_edge_valid_SDG_node)
[PROOF STATE]
proof (state)
this:
valid_SDG_node n \<and> valid_SDG_node n'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
valid_SDG_node n \<and> valid_SDG_node n'

goal (2 subgoals):
 1. valid_SDG_node n
 2. valid_SDG_node n'
[PROOF STEP]
thus "valid_SDG_node n" and "valid_SDG_node n'"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n \<and> valid_SDG_node n'

goal (1 subgoal):
 1. valid_SDG_node n &&& valid_SDG_node n'
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
valid_SDG_node n
valid_SDG_node n'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Exit_no_sum_SDG_edge_source:
  assumes "sum_SDG_edge (CFG_node (_Exit_)) Vopt popt b n'" shows "False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
proof(cases b)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. b \<Longrightarrow> False
 2. \<not> b \<Longrightarrow> False
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
b

goal (2 subgoals):
 1. b \<Longrightarrow> False
 2. \<not> b \<Longrightarrow> False
[PROOF STEP]
with \<open>sum_SDG_edge (CFG_node (_Exit_)) Vopt popt b n'\<close>
[PROOF STATE]
proof (chain)
picking this:
sum_SDG_edge (CFG_node (_Exit_)) Vopt popt b n'
b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum_SDG_edge (CFG_node (_Exit_)) Vopt popt b n'
b

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> b \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> b \<Longrightarrow> False
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> b

goal (1 subgoal):
 1. \<not> b \<Longrightarrow> False
[PROOF STEP]
with \<open>sum_SDG_edge (CFG_node (_Exit_)) Vopt popt b n'\<close>
[PROOF STATE]
proof (chain)
picking this:
sum_SDG_edge (CFG_node (_Exit_)) Vopt popt b n'
\<not> b
[PROOF STEP]
have "SDG_edge (CFG_node (_Exit_)) Vopt popt n'"
[PROOF STATE]
proof (prove)
using this:
sum_SDG_edge (CFG_node (_Exit_)) Vopt popt b n'
\<not> b

goal (1 subgoal):
 1. SDG_edge (CFG_node (_Exit_)) Vopt popt n'
[PROOF STEP]
by(fastforce intro:sum_SDG_edge_SDG_edge)
[PROOF STATE]
proof (state)
this:
SDG_edge (CFG_node (_Exit_)) Vopt popt n'

goal (1 subgoal):
 1. \<not> b \<Longrightarrow> False
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
SDG_edge (CFG_node (_Exit_)) Vopt popt n'

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

goal:
No subgoals!
[PROOF STEP]
qed