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

goal (1 subgoal):
 1. \<exists>ns'. n is-ns'\<rightarrow>\<^sub>d* n'
[PROOF STEP]
proof(induct rule:matched.induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>n. valid_SDG_node n \<Longrightarrow> \<exists>ns'. n is-ns'\<rightarrow>\<^sub>d* n
 2. \<And>n ns n'' ns' n'. \<lbrakk>matched n ns n''; \<exists>ns'. n is-ns'\<rightarrow>\<^sub>d* n''; n'' i-ns'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> \<exists>ns'. n is-ns'\<rightarrow>\<^sub>d* n'
 3. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 ns' n\<^sub>3 n\<^sub>4 V a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4 \<or> n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
 4. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
case matched_Nil
[PROOF STATE]
proof (state)
this:
valid_SDG_node n_

goal (4 subgoals):
 1. \<And>n. valid_SDG_node n \<Longrightarrow> \<exists>ns'. n is-ns'\<rightarrow>\<^sub>d* n
 2. \<And>n ns n'' ns' n'. \<lbrakk>matched n ns n''; \<exists>ns'. n is-ns'\<rightarrow>\<^sub>d* n''; n'' i-ns'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> \<exists>ns'. n is-ns'\<rightarrow>\<^sub>d* n'
 3. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 ns' n\<^sub>3 n\<^sub>4 V a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4 \<or> n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
 4. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n_

goal (1 subgoal):
 1. \<exists>ns'. n_ is-ns'\<rightarrow>\<^sub>d* n_
[PROOF STEP]
by(fastforce intro:isSp_Nil)
[PROOF STATE]
proof (state)
this:
\<exists>ns'. n_ is-ns'\<rightarrow>\<^sub>d* n_

goal (3 subgoals):
 1. \<And>n ns n'' ns' n'. \<lbrakk>matched n ns n''; \<exists>ns'. n is-ns'\<rightarrow>\<^sub>d* n''; n'' i-ns'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> \<exists>ns'. n is-ns'\<rightarrow>\<^sub>d* n'
 2. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 ns' n\<^sub>3 n\<^sub>4 V a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4 \<or> n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
 3. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n ns n'' ns' n'. \<lbrakk>matched n ns n''; \<exists>ns'. n is-ns'\<rightarrow>\<^sub>d* n''; n'' i-ns'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> \<exists>ns'. n is-ns'\<rightarrow>\<^sub>d* n'
 2. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 ns' n\<^sub>3 n\<^sub>4 V a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4 \<or> n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
 3. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
case matched_Append_intra_SDG_path
[PROOF STATE]
proof (state)
this:
matched n_ ns_ n''_
\<exists>ns'. n_ is-ns'\<rightarrow>\<^sub>d* n''_
n''_ i-ns'_\<rightarrow>\<^sub>d* n'_

goal (3 subgoals):
 1. \<And>n ns n'' ns' n'. \<lbrakk>matched n ns n''; \<exists>ns'. n is-ns'\<rightarrow>\<^sub>d* n''; n'' i-ns'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> \<exists>ns'. n is-ns'\<rightarrow>\<^sub>d* n'
 2. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 ns' n\<^sub>3 n\<^sub>4 V a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4 \<or> n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
 3. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
matched n_ ns_ n''_
\<exists>ns'. n_ is-ns'\<rightarrow>\<^sub>d* n''_
n''_ i-ns'_\<rightarrow>\<^sub>d* n'_

goal (1 subgoal):
 1. \<exists>ns'. n_ is-ns'\<rightarrow>\<^sub>d* n'_
[PROOF STEP]
by(fastforce intro:is_SDG_path_Append intra_SDG_path_is_SDG_path)
[PROOF STATE]
proof (state)
this:
\<exists>ns'. n_ is-ns'\<rightarrow>\<^sub>d* n'_

goal (2 subgoals):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 ns' n\<^sub>3 n\<^sub>4 V a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4 \<or> n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
 2. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 ns' n\<^sub>3 n\<^sub>4 V a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4 \<or> n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
 2. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
case (matched_bracket_call n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 ns' n\<^sub>3 n\<^sub>4 V a a')
[PROOF STATE]
proof (state)
this:
matched n\<^sub>0 ns n\<^sub>1
\<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1
n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2
matched n\<^sub>2 ns' n\<^sub>3
\<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3
n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4 \<or> n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4
valid_edge a
a' \<in> get_return_edges a
sourcenode a = parent_node n\<^sub>1
targetnode a = parent_node n\<^sub>2
sourcenode a' = parent_node n\<^sub>3
targetnode a' = parent_node n\<^sub>4

goal (2 subgoals):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 ns' n\<^sub>3 n\<^sub>4 V a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4 \<or> n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
 2. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
from \<open>\<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1
[PROOF STEP]
obtain nsx where "n\<^sub>0 is-nsx\<rightarrow>\<^sub>d* n\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
\<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1

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

goal (2 subgoals):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 ns' n\<^sub>3 n\<^sub>4 V a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4 \<or> n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
 2. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
from \<open>n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2\<close> \<open>sourcenode a = parent_node n\<^sub>1\<close> \<open>targetnode a = parent_node n\<^sub>2\<close>
[PROOF STATE]
proof (chain)
picking this:
n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2
sourcenode a = parent_node n\<^sub>1
targetnode a = parent_node n\<^sub>2
[PROOF STEP]
have "n\<^sub>1 = CFG_node (sourcenode a)" and "n\<^sub>2 = CFG_node (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2
sourcenode a = parent_node n\<^sub>1
targetnode a = parent_node n\<^sub>2

goal (1 subgoal):
 1. n\<^sub>1 = CFG_node (sourcenode a) &&& n\<^sub>2 = CFG_node (targetnode a)
[PROOF STEP]
by(auto elim:SDG_edge.cases)
[PROOF STATE]
proof (state)
this:
n\<^sub>1 = CFG_node (sourcenode a)
n\<^sub>2 = CFG_node (targetnode a)

goal (2 subgoals):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 ns' n\<^sub>3 n\<^sub>4 V a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4 \<or> n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
 2. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[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]
obtain Q r p' fs where "kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
a' \<in> get_return_edges a

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

goal (2 subgoals):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 ns' n\<^sub>3 n\<^sub>4 V a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4 \<or> n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
 2. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
with \<open>n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2\<close> \<open>valid_edge a\<close>
      \<open>n\<^sub>1 = CFG_node (sourcenode a)\<close> \<open>n\<^sub>2 = CFG_node (targetnode a)\<close>
[PROOF STATE]
proof (chain)
picking this:
n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2
valid_edge a
n\<^sub>1 = CFG_node (sourcenode a)
n\<^sub>2 = CFG_node (targetnode a)
kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs
[PROOF STEP]
have [simp]:"p' = p"
[PROOF STATE]
proof (prove)
using this:
n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2
valid_edge a
n\<^sub>1 = CFG_node (sourcenode a)
n\<^sub>2 = CFG_node (targetnode a)
kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs

goal (1 subgoal):
 1. p' = p
[PROOF STEP]
by -(erule SDG_edge.cases,(fastforce dest:edge_det)+)
[PROOF STATE]
proof (state)
this:
p' = p

goal (2 subgoals):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 ns' n\<^sub>3 n\<^sub>4 V a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4 \<or> n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
 2. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[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 (2 subgoals):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 ns' n\<^sub>3 n\<^sub>4 V a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4 \<or> n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
 2. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
from \<open>n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4 \<or> n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4\<close>
[PROOF STATE]
proof (chain)
picking this:
n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4 \<or> n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4 \<or> n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4

goal (1 subgoal):
 1. \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
 2. n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
assume "n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4"
[PROOF STATE]
proof (state)
this:
n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4

goal (2 subgoals):
 1. n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
 2. n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4
[PROOF STEP]
obtain ax Q' f' where "valid_edge ax" and "kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'"
        and "n\<^sub>3 = CFG_node (sourcenode ax)" and "n\<^sub>4 = CFG_node (targetnode ax)"
[PROOF STATE]
proof (prove)
using this:
n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4

goal (1 subgoal):
 1. (\<And>ax Q' f'. \<lbrakk>valid_edge ax; kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; n\<^sub>3 = CFG_node (sourcenode ax); n\<^sub>4 = CFG_node (targetnode ax)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:SDG_edge.cases)
[PROOF STATE]
proof (state)
this:
valid_edge ax
kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
n\<^sub>3 = CFG_node (sourcenode ax)
n\<^sub>4 = CFG_node (targetnode ax)

goal (2 subgoals):
 1. n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
 2. n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
with \<open>sourcenode a' = parent_node n\<^sub>3\<close> \<open>targetnode a' = parent_node n\<^sub>4\<close>
        \<open>valid_edge a'\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode a' = parent_node n\<^sub>3
targetnode a' = parent_node n\<^sub>4
valid_edge a'
valid_edge ax
kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
n\<^sub>3 = CFG_node (sourcenode ax)
n\<^sub>4 = CFG_node (targetnode ax)
[PROOF STEP]
have [simp]:"ax = a'"
[PROOF STATE]
proof (prove)
using this:
sourcenode a' = parent_node n\<^sub>3
targetnode a' = parent_node n\<^sub>4
valid_edge a'
valid_edge ax
kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
n\<^sub>3 = CFG_node (sourcenode ax)
n\<^sub>4 = CFG_node (targetnode ax)

goal (1 subgoal):
 1. ax = a'
[PROOF STEP]
by(fastforce dest:edge_det)
[PROOF STATE]
proof (state)
this:
ax = a'

goal (2 subgoals):
 1. n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
 2. n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs\<close> \<open>valid_edge ax\<close> \<open>kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'\<close>
        \<open>a' \<in> get_return_edges a\<close> \<open>matched n\<^sub>2 ns' n\<^sub>3\<close>
        \<open>n\<^sub>1 = CFG_node (sourcenode a)\<close> \<open>n\<^sub>2 = CFG_node (targetnode a)\<close>
        \<open>n\<^sub>3 = CFG_node (sourcenode ax)\<close> \<open>n\<^sub>4 = CFG_node (targetnode ax)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs
valid_edge ax
kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
a' \<in> get_return_edges a
matched n\<^sub>2 ns' n\<^sub>3
n\<^sub>1 = CFG_node (sourcenode a)
n\<^sub>2 = CFG_node (targetnode a)
n\<^sub>3 = CFG_node (sourcenode ax)
n\<^sub>4 = CFG_node (targetnode ax)
[PROOF STEP]
have "n\<^sub>1 s-p\<rightarrow>\<^bsub>sum\<^esub> n\<^sub>4"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs
valid_edge ax
kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
a' \<in> get_return_edges a
matched n\<^sub>2 ns' n\<^sub>3
n\<^sub>1 = CFG_node (sourcenode a)
n\<^sub>2 = CFG_node (targetnode a)
n\<^sub>3 = CFG_node (sourcenode ax)
n\<^sub>4 = CFG_node (targetnode ax)

goal (1 subgoal):
 1. n\<^sub>1 s-p\<rightarrow>\<^bsub>sum\<^esub> n\<^sub>4
[PROOF STEP]
by(fastforce intro!:sum_SDG_call_summary_edge[of a _ _ _ _ ax])
[PROOF STATE]
proof (state)
this:
n\<^sub>1 s-p\<rightarrow>\<^bsub>sum\<^esub> n\<^sub>4

goal (2 subgoals):
 1. n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
 2. n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
with \<open>n\<^sub>0 is-nsx\<rightarrow>\<^sub>d* n\<^sub>1\<close>
[PROOF STATE]
proof (chain)
picking this:
n\<^sub>0 is-nsx\<rightarrow>\<^sub>d* n\<^sub>1
n\<^sub>1 s-p\<rightarrow>\<^bsub>sum\<^esub> n\<^sub>4
[PROOF STEP]
have "n\<^sub>0 is-nsx@[n\<^sub>1]\<rightarrow>\<^sub>d* n\<^sub>4"
[PROOF STATE]
proof (prove)
using this:
n\<^sub>0 is-nsx\<rightarrow>\<^sub>d* n\<^sub>1
n\<^sub>1 s-p\<rightarrow>\<^bsub>sum\<^esub> n\<^sub>4

goal (1 subgoal):
 1. n\<^sub>0 is-nsx @ [n\<^sub>1]\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
by(rule isSp_Append_sum)
[PROOF STATE]
proof (state)
this:
n\<^sub>0 is-nsx @ [n\<^sub>1]\<rightarrow>\<^sub>d* n\<^sub>4

goal (2 subgoals):
 1. n\<^sub>3 -p\<rightarrow>\<^bsub>ret\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
 2. n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
n\<^sub>0 is-nsx @ [n\<^sub>1]\<rightarrow>\<^sub>d* n\<^sub>4

goal (1 subgoal):
 1. \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4

goal (1 subgoal):
 1. n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
assume "n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4"
[PROOF STATE]
proof (state)
this:
n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4

goal (1 subgoal):
 1. n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4
[PROOF STEP]
obtain ax Q' f' x where "valid_edge ax" and "kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'"
        and "n\<^sub>3 = Formal_out (sourcenode ax,x)"
        and "n\<^sub>4 = Actual_out (targetnode ax,x)"
[PROOF STATE]
proof (prove)
using this:
n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4

goal (1 subgoal):
 1. (\<And>ax Q' f' x. \<lbrakk>valid_edge ax; kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; n\<^sub>3 = Formal_out (sourcenode ax, x); n\<^sub>4 = Actual_out (targetnode ax, x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:SDG_edge.cases)
[PROOF STATE]
proof (state)
this:
valid_edge ax
kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
n\<^sub>3 = Formal_out (sourcenode ax, x)
n\<^sub>4 = Actual_out (targetnode ax, x)

goal (1 subgoal):
 1. n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
with \<open>sourcenode a' = parent_node n\<^sub>3\<close> \<open>targetnode a' = parent_node n\<^sub>4\<close>
        \<open>valid_edge a'\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode a' = parent_node n\<^sub>3
targetnode a' = parent_node n\<^sub>4
valid_edge a'
valid_edge ax
kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
n\<^sub>3 = Formal_out (sourcenode ax, x)
n\<^sub>4 = Actual_out (targetnode ax, x)
[PROOF STEP]
have [simp]:"ax = a'"
[PROOF STATE]
proof (prove)
using this:
sourcenode a' = parent_node n\<^sub>3
targetnode a' = parent_node n\<^sub>4
valid_edge a'
valid_edge ax
kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
n\<^sub>3 = Formal_out (sourcenode ax, x)
n\<^sub>4 = Actual_out (targetnode ax, x)

goal (1 subgoal):
 1. ax = a'
[PROOF STEP]
by(fastforce dest:edge_det)
[PROOF STATE]
proof (state)
this:
ax = a'

goal (1 subgoal):
 1. n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
from \<open>valid_edge ax\<close> \<open>kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'\<close> \<open>n\<^sub>3 = Formal_out (sourcenode ax,x)\<close>
        \<open>n\<^sub>4 = Actual_out (targetnode ax,x)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge ax
kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
n\<^sub>3 = Formal_out (sourcenode ax, x)
n\<^sub>4 = Actual_out (targetnode ax, x)
[PROOF STEP]
have "CFG_node (sourcenode a') -p\<rightarrow>\<^bsub>ret\<^esub> CFG_node (targetnode a')"
[PROOF STATE]
proof (prove)
using this:
valid_edge ax
kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
n\<^sub>3 = Formal_out (sourcenode ax, x)
n\<^sub>4 = Actual_out (targetnode ax, x)

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

goal (1 subgoal):
 1. n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs\<close> \<open>valid_edge a'\<close>
        \<open>a' \<in> get_return_edges a\<close> \<open>n\<^sub>4 = Actual_out (targetnode ax,x)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs
valid_edge a'
a' \<in> get_return_edges a
n\<^sub>4 = Actual_out (targetnode ax, x)
[PROOF STEP]
have "CFG_node (targetnode a) \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (sourcenode a')"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs
valid_edge a'
a' \<in> get_return_edges a
n\<^sub>4 = Actual_out (targetnode ax, x)

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

goal (1 subgoal):
 1. n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
with \<open>n\<^sub>2 = CFG_node (targetnode a)\<close>
[PROOF STATE]
proof (chain)
picking this:
n\<^sub>2 = CFG_node (targetnode a)
CFG_node (targetnode a) \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (sourcenode a')
[PROOF STEP]
have "matched n\<^sub>2 ([]@([]@[n\<^sub>2])) (CFG_node (sourcenode a'))"
[PROOF STATE]
proof (prove)
using this:
n\<^sub>2 = CFG_node (targetnode a)
CFG_node (targetnode a) \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (sourcenode a')

goal (1 subgoal):
 1. matched n\<^sub>2 ([] @ [] @ [n\<^sub>2]) (CFG_node (sourcenode a'))
[PROOF STEP]
by(fastforce intro:matched.intros intra_SDG_path.intros
                          SDG_edge_valid_SDG_node)
[PROOF STATE]
proof (state)
this:
matched n\<^sub>2 ([] @ [] @ [n\<^sub>2]) (CFG_node (sourcenode a'))

goal (1 subgoal):
 1. n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
with \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs\<close> \<open>valid_edge a'\<close> \<open>kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'\<close>
        \<open>a' \<in> get_return_edges a\<close> \<open>n\<^sub>1 = CFG_node (sourcenode a)\<close>
        \<open>n\<^sub>2 = CFG_node (targetnode a)\<close> \<open>n\<^sub>4 = Actual_out (targetnode ax,x)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs
valid_edge a'
kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
a' \<in> get_return_edges a
n\<^sub>1 = CFG_node (sourcenode a)
n\<^sub>2 = CFG_node (targetnode a)
n\<^sub>4 = Actual_out (targetnode ax, x)
matched n\<^sub>2 ([] @ [] @ [n\<^sub>2]) (CFG_node (sourcenode a'))
[PROOF STEP]
have "n\<^sub>1 s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a')"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs
valid_edge a'
kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
a' \<in> get_return_edges a
n\<^sub>1 = CFG_node (sourcenode a)
n\<^sub>2 = CFG_node (targetnode a)
n\<^sub>4 = Actual_out (targetnode ax, x)
matched n\<^sub>2 ([] @ [] @ [n\<^sub>2]) (CFG_node (sourcenode a'))

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

goal (1 subgoal):
 1. n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
with \<open>n\<^sub>0 is-nsx\<rightarrow>\<^sub>d* n\<^sub>1\<close>
[PROOF STATE]
proof (chain)
picking this:
n\<^sub>0 is-nsx\<rightarrow>\<^sub>d* n\<^sub>1
n\<^sub>1 s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a')
[PROOF STEP]
have "n\<^sub>0 is-nsx@[n\<^sub>1]\<rightarrow>\<^sub>d* CFG_node (targetnode a')"
[PROOF STATE]
proof (prove)
using this:
n\<^sub>0 is-nsx\<rightarrow>\<^sub>d* n\<^sub>1
n\<^sub>1 s-p\<rightarrow>\<^bsub>sum\<^esub> CFG_node (targetnode a')

goal (1 subgoal):
 1. n\<^sub>0 is-nsx @ [n\<^sub>1]\<rightarrow>\<^sub>d* CFG_node (targetnode a')
[PROOF STEP]
by(rule isSp_Append_sum)
[PROOF STATE]
proof (state)
this:
n\<^sub>0 is-nsx @ [n\<^sub>1]\<rightarrow>\<^sub>d* CFG_node (targetnode a')

goal (1 subgoal):
 1. n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
from \<open>n\<^sub>4 = Actual_out (targetnode ax,x)\<close> \<open>n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4\<close>
[PROOF STATE]
proof (chain)
picking this:
n\<^sub>4 = Actual_out (targetnode ax, x)
n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4
[PROOF STEP]
have "CFG_node (targetnode a') s\<longrightarrow>\<^bsub>cd\<^esub> n\<^sub>4"
[PROOF STATE]
proof (prove)
using this:
n\<^sub>4 = Actual_out (targetnode ax, x)
n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4

goal (1 subgoal):
 1. CFG_node (targetnode a') s\<longrightarrow>\<^bsub>cd\<^esub> n\<^sub>4
[PROOF STEP]
by(fastforce intro:sum_SDG_parent_cdep_edge SDG_edge_valid_SDG_node)
[PROOF STATE]
proof (state)
this:
CFG_node (targetnode a') s\<longrightarrow>\<^bsub>cd\<^esub> n\<^sub>4

goal (1 subgoal):
 1. n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
with \<open>n\<^sub>0 is-nsx@[n\<^sub>1]\<rightarrow>\<^sub>d* CFG_node (targetnode a')\<close>
[PROOF STATE]
proof (chain)
picking this:
n\<^sub>0 is-nsx @ [n\<^sub>1]\<rightarrow>\<^sub>d* CFG_node (targetnode a')
CFG_node (targetnode a') s\<longrightarrow>\<^bsub>cd\<^esub> n\<^sub>4
[PROOF STEP]
have "n\<^sub>0 is-(nsx@[n\<^sub>1])@[CFG_node (targetnode a')]\<rightarrow>\<^sub>d* n\<^sub>4"
[PROOF STATE]
proof (prove)
using this:
n\<^sub>0 is-nsx @ [n\<^sub>1]\<rightarrow>\<^sub>d* CFG_node (targetnode a')
CFG_node (targetnode a') s\<longrightarrow>\<^bsub>cd\<^esub> n\<^sub>4

goal (1 subgoal):
 1. n\<^sub>0 is-(nsx @ [n\<^sub>1]) @ [CFG_node (targetnode a')]\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
by(rule isSp_Append_cdep)
[PROOF STATE]
proof (state)
this:
n\<^sub>0 is-(nsx @ [n\<^sub>1]) @ [CFG_node (targetnode a')]\<rightarrow>\<^sub>d* n\<^sub>4

goal (1 subgoal):
 1. n\<^sub>3 -p:V\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4 \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
n\<^sub>0 is-(nsx @ [n\<^sub>1]) @ [CFG_node (targetnode a')]\<rightarrow>\<^sub>d* n\<^sub>4

goal (1 subgoal):
 1. \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
case (matched_bracket_param n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a')
[PROOF STATE]
proof (state)
this:
matched n\<^sub>0 ns n\<^sub>1
\<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1
n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2
matched n\<^sub>2 ns' n\<^sub>3
\<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3
n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4
valid_edge a
a' \<in> get_return_edges a
sourcenode a = parent_node n\<^sub>1
targetnode a = parent_node n\<^sub>2
sourcenode a' = parent_node n\<^sub>3
targetnode a' = parent_node n\<^sub>4

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
from \<open>\<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1
[PROOF STEP]
obtain nsx where "n\<^sub>0 is-nsx\<rightarrow>\<^sub>d* n\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
\<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1

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

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
from \<open>n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2\<close> \<open>sourcenode a = parent_node n\<^sub>1\<close>
      \<open>targetnode a = parent_node n\<^sub>2\<close>
[PROOF STATE]
proof (chain)
picking this:
n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2
sourcenode a = parent_node n\<^sub>1
targetnode a = parent_node n\<^sub>2
[PROOF STEP]
obtain x ins outs
      where "n\<^sub>1 = Actual_in (sourcenode a,x)" and "n\<^sub>2 = Formal_in (targetnode a,x)"
      and "(p,ins,outs) \<in> set procs" and "V = ins!x" and "x < length ins"
[PROOF STATE]
proof (prove)
using this:
n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2
sourcenode a = parent_node n\<^sub>1
targetnode a = parent_node n\<^sub>2

goal (1 subgoal):
 1. (\<And>x ins outs. \<lbrakk>n\<^sub>1 = Actual_in (sourcenode a, x); n\<^sub>2 = Formal_in (targetnode a, x); (p, ins, outs) \<in> set procs; V = ins ! x; x < length ins\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:SDG_edge.cases)
[PROOF STATE]
proof (state)
this:
n\<^sub>1 = Actual_in (sourcenode a, x)
n\<^sub>2 = Formal_in (targetnode a, x)
(p, ins, outs) \<in> set procs
V = ins ! x
x < length ins

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[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]
obtain Q r p' fs where "kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
a' \<in> get_return_edges a

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

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
with \<open>n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2\<close> \<open>valid_edge a\<close>
      \<open>n\<^sub>1 = Actual_in (sourcenode a,x)\<close> \<open>n\<^sub>2 = Formal_in (targetnode a,x)\<close>
[PROOF STATE]
proof (chain)
picking this:
n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2
valid_edge a
n\<^sub>1 = Actual_in (sourcenode a, x)
n\<^sub>2 = Formal_in (targetnode a, x)
kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs
[PROOF STEP]
have [simp]:"p' = p"
[PROOF STATE]
proof (prove)
using this:
n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2
valid_edge a
n\<^sub>1 = Actual_in (sourcenode a, x)
n\<^sub>2 = Formal_in (targetnode a, x)
kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs

goal (1 subgoal):
 1. p' = p
[PROOF STEP]
by -(erule SDG_edge.cases,(fastforce dest:edge_det)+)
[PROOF STATE]
proof (state)
this:
p' = p

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>a' \<in> get_return_edges a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
a' \<in> get_return_edges a
[PROOF STEP]
have "valid_edge a'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
a' \<in> get_return_edges a

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

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
from \<open>n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4\<close>
[PROOF STATE]
proof (chain)
picking this:
n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4
[PROOF STEP]
obtain ax Q' f' x' ins' outs' where "valid_edge ax"
      and "kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'" and "n\<^sub>3 = Formal_out (sourcenode ax,x')"
      and "n\<^sub>4 = Actual_out (targetnode ax,x')" and "(p,ins',outs') \<in> set procs"
      and "V' = outs'!x'" and "x' < length outs'"
[PROOF STATE]
proof (prove)
using this:
n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4

goal (1 subgoal):
 1. (\<And>ax Q' f' x' ins' outs'. \<lbrakk>valid_edge ax; kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'; n\<^sub>3 = Formal_out (sourcenode ax, x'); n\<^sub>4 = Actual_out (targetnode ax, x'); (p, ins', outs') \<in> set procs; V' = outs' ! x'; x' < length outs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:SDG_edge.cases)
[PROOF STATE]
proof (state)
this:
valid_edge ax
kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
n\<^sub>3 = Formal_out (sourcenode ax, x')
n\<^sub>4 = Actual_out (targetnode ax, x')
(p, ins', outs') \<in> set procs
V' = outs' ! x'
x' < length outs'

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
with \<open>sourcenode a' = parent_node n\<^sub>3\<close> \<open>targetnode a' = parent_node n\<^sub>4\<close>
      \<open>valid_edge a'\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode a' = parent_node n\<^sub>3
targetnode a' = parent_node n\<^sub>4
valid_edge a'
valid_edge ax
kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
n\<^sub>3 = Formal_out (sourcenode ax, x')
n\<^sub>4 = Actual_out (targetnode ax, x')
(p, ins', outs') \<in> set procs
V' = outs' ! x'
x' < length outs'
[PROOF STEP]
have [simp]:"ax = a'"
[PROOF STATE]
proof (prove)
using this:
sourcenode a' = parent_node n\<^sub>3
targetnode a' = parent_node n\<^sub>4
valid_edge a'
valid_edge ax
kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
n\<^sub>3 = Formal_out (sourcenode ax, x')
n\<^sub>4 = Actual_out (targetnode ax, x')
(p, ins', outs') \<in> set procs
V' = outs' ! x'
x' < length outs'

goal (1 subgoal):
 1. ax = a'
[PROOF STEP]
by(fastforce dest:edge_det)
[PROOF STATE]
proof (state)
this:
ax = a'

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
from unique_callers \<open>(p,ins,outs) \<in> set procs\<close> \<open>(p,ins',outs') \<in> set procs\<close>
[PROOF STATE]
proof (chain)
picking this:
distinct_fst procs
(p, ins, outs) \<in> set procs
(p, ins', outs') \<in> set procs
[PROOF STEP]
have [simp]:"ins = ins'" "outs = outs'"
[PROOF STATE]
proof (prove)
using this:
distinct_fst procs
(p, ins, outs) \<in> set procs
(p, ins', outs') \<in> set procs

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\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs\<close> \<open>valid_edge a'\<close> \<open>kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'\<close>
      \<open>a' \<in> get_return_edges a\<close> \<open>matched n\<^sub>2 ns' n\<^sub>3\<close> \<open>n\<^sub>1 = Actual_in (sourcenode a,x)\<close>
      \<open>n\<^sub>2 = Formal_in (targetnode a,x)\<close> \<open>n\<^sub>3 = Formal_out (sourcenode ax,x')\<close>
      \<open>n\<^sub>4 = Actual_out (targetnode ax,x')\<close> \<open>(p,ins,outs) \<in> set procs\<close>
      \<open>x < length ins\<close> \<open>x' < length outs'\<close> \<open>V = ins!x\<close> \<open>V' = outs'!x'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs
valid_edge a'
kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
a' \<in> get_return_edges a
matched n\<^sub>2 ns' n\<^sub>3
n\<^sub>1 = Actual_in (sourcenode a, x)
n\<^sub>2 = Formal_in (targetnode a, x)
n\<^sub>3 = Formal_out (sourcenode ax, x')
n\<^sub>4 = Actual_out (targetnode ax, x')
(p, ins, outs) \<in> set procs
x < length ins
x' < length outs'
V = ins ! x
V' = outs' ! x'
[PROOF STEP]
have "n\<^sub>1 s-p\<rightarrow>\<^bsub>sum\<^esub> n\<^sub>4"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs
valid_edge a'
kind ax = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
a' \<in> get_return_edges a
matched n\<^sub>2 ns' n\<^sub>3
n\<^sub>1 = Actual_in (sourcenode a, x)
n\<^sub>2 = Formal_in (targetnode a, x)
n\<^sub>3 = Formal_out (sourcenode ax, x')
n\<^sub>4 = Actual_out (targetnode ax, x')
(p, ins, outs) \<in> set procs
x < length ins
x' < length outs'
V = ins ! x
V' = outs' ! x'

goal (1 subgoal):
 1. n\<^sub>1 s-p\<rightarrow>\<^bsub>sum\<^esub> n\<^sub>4
[PROOF STEP]
by(fastforce intro!:sum_SDG_param_summary_edge[of a _ _ _ _ a'])
[PROOF STATE]
proof (state)
this:
n\<^sub>1 s-p\<rightarrow>\<^bsub>sum\<^esub> n\<^sub>4

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
with \<open>n\<^sub>0 is-nsx\<rightarrow>\<^sub>d* n\<^sub>1\<close>
[PROOF STATE]
proof (chain)
picking this:
n\<^sub>0 is-nsx\<rightarrow>\<^sub>d* n\<^sub>1
n\<^sub>1 s-p\<rightarrow>\<^bsub>sum\<^esub> n\<^sub>4
[PROOF STEP]
have "n\<^sub>0 is-nsx@[n\<^sub>1]\<rightarrow>\<^sub>d* n\<^sub>4"
[PROOF STATE]
proof (prove)
using this:
n\<^sub>0 is-nsx\<rightarrow>\<^sub>d* n\<^sub>1
n\<^sub>1 s-p\<rightarrow>\<^bsub>sum\<^esub> n\<^sub>4

goal (1 subgoal):
 1. n\<^sub>0 is-nsx @ [n\<^sub>1]\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
by(rule isSp_Append_sum)
[PROOF STATE]
proof (state)
this:
n\<^sub>0 is-nsx @ [n\<^sub>1]\<rightarrow>\<^sub>d* n\<^sub>4

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p V n\<^sub>2 ns' n\<^sub>3 V' n\<^sub>4 a a'. \<lbrakk>matched n\<^sub>0 ns n\<^sub>1; \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>ns'. n\<^sub>2 is-ns'\<rightarrow>\<^sub>d* n\<^sub>3; n\<^sub>3 -p:V'\<rightarrow>\<^bsub>out\<^esub> n\<^sub>4; valid_edge a; a' \<in> get_return_edges a; sourcenode a = parent_node n\<^sub>1; targetnode a = parent_node n\<^sub>2; sourcenode a' = parent_node n\<^sub>3; targetnode a' = parent_node n\<^sub>4\<rbrakk> \<Longrightarrow> \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
n\<^sub>0 is-nsx @ [n\<^sub>1]\<rightarrow>\<^sub>d* n\<^sub>4

goal (1 subgoal):
 1. \<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>ns'. n\<^sub>0 is-ns'\<rightarrow>\<^sub>d* n\<^sub>4

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_SDG_path_matched:
  assumes "n is-ns\<rightarrow>\<^sub>d* n'" obtains ns' where "matched n ns' n'" and "set ns \<subseteq> set ns'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ns'. \<lbrakk>matched n ns' n'; set ns \<subseteq> set ns'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>ns'. matched n ns' n' \<and> set ns \<subseteq> set ns'
[PROOF STEP]
from \<open>n is-ns\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n is-ns\<rightarrow>\<^sub>d* n'
[PROOF STEP]
show "\<exists>ns'. matched n ns' n' \<and> set ns \<subseteq> set ns'"
[PROOF STATE]
proof (prove)
using this:
n is-ns\<rightarrow>\<^sub>d* n'

goal (1 subgoal):
 1. \<exists>ns'. matched n ns' n' \<and> set ns \<subseteq> set ns'
[PROOF STEP]
proof(induct rule:intra_sum_SDG_path.induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>n. valid_SDG_node n \<Longrightarrow> \<exists>ns'. matched n ns' n \<and> set [] \<subseteq> set ns'
 2. \<And>n ns n'' n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
case (isSp_Nil n)
[PROOF STATE]
proof (state)
this:
valid_SDG_node n

goal (4 subgoals):
 1. \<And>n. valid_SDG_node n \<Longrightarrow> \<exists>ns'. matched n ns' n \<and> set [] \<subseteq> set ns'
 2. \<And>n ns n'' n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
from \<open>valid_SDG_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_SDG_node n
[PROOF STEP]
have "matched n [] n"
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n

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

goal (4 subgoals):
 1. \<And>n. valid_SDG_node n \<Longrightarrow> \<exists>ns'. matched n ns' n \<and> set [] \<subseteq> set ns'
 2. \<And>n ns n'' n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 4. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
matched n [] n

goal (1 subgoal):
 1. \<exists>ns'. matched n ns' n \<and> set [] \<subseteq> set ns'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns'. matched n ns' n \<and> set [] \<subseteq> set ns'

goal (3 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
case (isSp_Append_cdep n ns n'' n')
[PROOF STATE]
proof (state)
this:
n is-ns\<rightarrow>\<^sub>d* n''
\<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'
n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'

goal (3 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
from \<open>\<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'
[PROOF STEP]
obtain ns' where "matched n ns' n''" and "set ns \<subseteq> set ns'"
[PROOF STATE]
proof (prove)
using this:
\<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'

goal (1 subgoal):
 1. (\<And>ns'. \<lbrakk>matched n ns' n''; set ns \<subseteq> set ns'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
matched n ns' n''
set ns \<subseteq> set ns'

goal (3 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
from \<open>n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'
[PROOF STEP]
have "n'' i-[]@[n'']\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'

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

goal (3 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
with \<open>matched n ns' n''\<close>
[PROOF STATE]
proof (chain)
picking this:
matched n ns' n''
n'' i-[] @ [n'']\<rightarrow>\<^sub>d* n'
[PROOF STEP]
have "matched n (ns'@[n'']) n'"
[PROOF STATE]
proof (prove)
using this:
matched n ns' n''
n'' i-[] @ [n'']\<rightarrow>\<^sub>d* n'

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

goal (3 subgoals):
 1. \<And>n ns n'' n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s\<longrightarrow>\<^bsub>cd\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 3. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
with \<open>set ns \<subseteq> set ns'\<close>
[PROOF STATE]
proof (chain)
picking this:
set ns \<subseteq> set ns'
matched n (ns' @ [n'']) n'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set ns \<subseteq> set ns'
matched n (ns' @ [n'']) n'

goal (1 subgoal):
 1. \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'

goal (2 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
case (isSp_Append_ddep n ns n'' V n')
[PROOF STATE]
proof (state)
this:
n is-ns\<rightarrow>\<^sub>d* n''
\<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'
n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'
n'' \<noteq> n'

goal (2 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
from \<open>\<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'
[PROOF STEP]
obtain ns' where "matched n ns' n''" and "set ns \<subseteq> set ns'"
[PROOF STATE]
proof (prove)
using this:
\<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'

goal (1 subgoal):
 1. (\<And>ns'. \<lbrakk>matched n ns' n''; set ns \<subseteq> set ns'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
matched n ns' n''
set ns \<subseteq> set ns'

goal (2 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
from \<open>n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'\<close> \<open>n'' \<noteq> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'
n'' \<noteq> n'
[PROOF STEP]
have "n'' i-[]@[n'']\<rightarrow>\<^sub>d* n'"
[PROOF STATE]
proof (prove)
using this:
n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'
n'' \<noteq> n'

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

goal (2 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
with \<open>matched n ns' n''\<close>
[PROOF STATE]
proof (chain)
picking this:
matched n ns' n''
n'' i-[] @ [n'']\<rightarrow>\<^sub>d* n'
[PROOF STEP]
have "matched n (ns'@[n'']) n'"
[PROOF STATE]
proof (prove)
using this:
matched n ns' n''
n'' i-[] @ [n'']\<rightarrow>\<^sub>d* n'

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

goal (2 subgoals):
 1. \<And>n ns n'' V n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-V\<rightarrow>\<^sub>d\<^sub>d n'; n'' \<noteq> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
 2. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
with \<open>set ns \<subseteq> set ns'\<close>
[PROOF STATE]
proof (chain)
picking this:
set ns \<subseteq> set ns'
matched n (ns' @ [n'']) n'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set ns \<subseteq> set ns'
matched n (ns' @ [n'']) n'

goal (1 subgoal):
 1. \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'

goal (1 subgoal):
 1. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
case (isSp_Append_sum n ns n'' p n')
[PROOF STATE]
proof (state)
this:
n is-ns\<rightarrow>\<^sub>d* n''
\<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'
n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'

goal (1 subgoal):
 1. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
from \<open>\<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'
[PROOF STEP]
obtain ns' where "matched n ns' n''" and "set ns \<subseteq> set ns'"
[PROOF STATE]
proof (prove)
using this:
\<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'

goal (1 subgoal):
 1. (\<And>ns'. \<lbrakk>matched n ns' n''; set ns \<subseteq> set ns'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
matched n ns' n''
set ns \<subseteq> set ns'

goal (1 subgoal):
 1. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
from \<open>n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'
[PROOF STEP]
obtain ns'' where "matched n'' ns'' n'" and "n'' \<in> set ns''"
[PROOF STATE]
proof (prove)
using this:
n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'

goal (1 subgoal):
 1. (\<And>ns''. \<lbrakk>matched n'' ns'' n'; n'' \<in> set ns''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by -(erule sum_SDG_summary_edge_matched)
[PROOF STATE]
proof (state)
this:
matched n'' ns'' n'
n'' \<in> set ns''

goal (1 subgoal):
 1. \<And>n ns n'' p n'. \<lbrakk>n is-ns\<rightarrow>\<^sub>d* n''; \<exists>ns'. matched n ns' n'' \<and> set ns \<subseteq> set ns'; n'' s-p\<rightarrow>\<^bsub>sum\<^esub> n'\<rbrakk> \<Longrightarrow> \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
with \<open>matched n ns' n''\<close>
[PROOF STATE]
proof (chain)
picking this:
matched n ns' n''
matched n'' ns'' n'
n'' \<in> set ns''
[PROOF STEP]
have "matched n (ns'@ns'') n'"
[PROOF STATE]
proof (prove)
using this:
matched n ns' n''
matched n'' ns'' n'
n'' \<in> set ns''

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

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

goal (1 subgoal):
 1. \<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>ns'. matched n ns' n' \<and> set (ns @ [n'']) \<subseteq> set ns'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ns'. matched n ns' n' \<and> set ns \<subseteq> set ns'

goal:
No subgoals!
[PROOF STEP]
qed