[STATEMENT]
lemma matched_Append:
  "\<lbrakk>matched n'' ns' n'; matched n ns n''\<rbrakk> \<Longrightarrow> matched n (ns@ns') n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>matched n'' ns' n'; matched n ns n''\<rbrakk> \<Longrightarrow> matched n (ns @ ns') n'
[PROOF STEP]
by(induct rule:matched.induct,
   auto intro:matched.intros simp:append_assoc[THEN sym] simp del:append_assoc)


[STATEMENT]
lemma intra_SDG_path_matched:
  assumes "n i-ns\<rightarrow>\<^sub>d* n'" shows "matched n ns n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matched n ns n'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matched n ns n'
[PROOF STEP]
from \<open>n i-ns\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n i-ns\<rightarrow>\<^sub>d* n'
[PROOF STEP]
have "valid_SDG_node n"
[PROOF STATE]
proof (prove)
using this:
n i-ns\<rightarrow>\<^sub>d* n'

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

goal (1 subgoal):
 1. matched n ns 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. matched n ns n'
[PROOF STEP]
with \<open>n i-ns\<rightarrow>\<^sub>d* n'\<close>
[PROOF STATE]
proof (chain)
picking this:
n i-ns\<rightarrow>\<^sub>d* n'
matched n [] n
[PROOF STEP]
have "matched n ([]@ns) n'"
[PROOF STATE]
proof (prove)
using this:
n i-ns\<rightarrow>\<^sub>d* n'
matched n [] n

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

goal (1 subgoal):
 1. matched n ns n'
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
matched n ([] @ ns) n'

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma intra_proc_matched:
  assumes "valid_edge a" and "kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs" and "a' \<in> get_return_edges a"
  shows "matched (CFG_node (targetnode a)) [CFG_node (targetnode a)]
                 (CFG_node (sourcenode a'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matched (CFG_node (targetnode a)) [CFG_node (targetnode a)] (CFG_node (sourcenode a'))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matched (CFG_node (targetnode a)) [CFG_node (targetnode a)] (CFG_node (sourcenode a'))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
a' \<in> get_return_edges a
[PROOF STEP]
have "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
a' \<in> get_return_edges a

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

goal (1 subgoal):
 1. matched (CFG_node (targetnode a)) [CFG_node (targetnode a)] (CFG_node (sourcenode a'))
[PROOF STEP]
with \<open>valid_edge a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
CFG_node (targetnode a) \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (sourcenode a')
[PROOF STEP]
have "CFG_node (targetnode a) i-[]@[CFG_node (targetnode a)]\<rightarrow>\<^sub>d*
        CFG_node (sourcenode a')"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
CFG_node (targetnode a) \<longrightarrow>\<^bsub>cd\<^esub> CFG_node (sourcenode a')

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

goal (1 subgoal):
 1. matched (CFG_node (targetnode a)) [CFG_node (targetnode a)] (CFG_node (sourcenode a'))
[PROOF STEP]
with \<open>valid_edge a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
CFG_node (targetnode a) i-[] @ [CFG_node (targetnode a)]\<rightarrow>\<^sub>d* CFG_node (sourcenode a')
[PROOF STEP]
have "matched (CFG_node (targetnode a)) ([]@[CFG_node (targetnode a)])
    (CFG_node (sourcenode a'))"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
CFG_node (targetnode a) i-[] @ [CFG_node (targetnode a)]\<rightarrow>\<^sub>d* CFG_node (sourcenode a')

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

goal (1 subgoal):
 1. matched (CFG_node (targetnode a)) [CFG_node (targetnode a)] (CFG_node (sourcenode a'))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
matched (CFG_node (targetnode a)) ([] @ [CFG_node (targetnode a)]) (CFG_node (sourcenode a'))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matched_intra_CFG_path:
  assumes "matched n ns n'"
  obtains as where "parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* 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>\<iota>* parent_node n'
[PROOF STEP]
from \<open>matched n ns n'\<close>
[PROOF STATE]
proof (chain)
picking this:
matched n ns n'
[PROOF STEP]
show "\<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'"
[PROOF STATE]
proof (prove)
using this:
matched n ns n'

goal (1 subgoal):
 1. \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
proof(induct rule:matched.induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>n. valid_SDG_node n \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n
 2. \<And>n ns n'' ns' n'. \<lbrakk>matched n ns n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' i-ns'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n
 2. \<And>n ns n'' ns' n'. \<lbrakk>matched n ns n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' i-ns'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
valid_SDG_node n_

goal (1 subgoal):
 1. \<exists>as. parent_node n_ -as\<rightarrow>\<^sub>\<iota>* parent_node n_
[PROOF STEP]
by(fastforce dest:empty_path valid_SDG_CFG_node simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
\<exists>as. parent_node n_ -as\<rightarrow>\<^sub>\<iota>* parent_node n_

goal (3 subgoals):
 1. \<And>n ns n'' ns' n'. \<lbrakk>matched n ns n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' i-ns'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' i-ns'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4
[PROOF STEP]
case (matched_Append_intra_SDG_path n ns n'' ns' n')
[PROOF STATE]
proof (state)
this:
matched n ns n''
\<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''
n'' i-ns'\<rightarrow>\<^sub>d* n'

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

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

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

goal (1 subgoal):
 1. (\<And>as'. parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:intra_SDG_path_intra_CFG_path)
[PROOF STATE]
proof (state)
this:
parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'

goal (3 subgoals):
 1. \<And>n ns n'' ns' n'. \<lbrakk>matched n ns n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' i-ns'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4
[PROOF STEP]
with \<open>parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''
parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
have "parent_node n -as@as'\<rightarrow>\<^sub>\<iota>* parent_node n'"
[PROOF STATE]
proof (prove)
using this:
parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''
parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'

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

goal (3 subgoals):
 1. \<And>n ns n'' ns' n'. \<lbrakk>matched n ns n''; \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n''; n'' i-ns'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
parent_node n -as @ as'\<rightarrow>\<^sub>\<iota>* parent_node n'

goal (1 subgoal):
 1. \<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node n'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>as. parent_node n -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1
n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2
matched n\<^sub>2 ns' n\<^sub>3
\<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>a' \<in> get_return_edges a\<close> \<open>sourcenode a = parent_node n\<^sub>1\<close>
      \<open>targetnode a' = parent_node n\<^sub>4\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
a' \<in> get_return_edges a
sourcenode a = parent_node n\<^sub>1
targetnode a' = parent_node n\<^sub>4
[PROOF STEP]
obtain a'' where "valid_edge a''" and "sourcenode a'' = parent_node n\<^sub>1"
      and "targetnode a'' = parent_node n\<^sub>4" and "kind a'' = (\<lambda>cf. False)\<^sub>\<surd>"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
a' \<in> get_return_edges a
sourcenode a = parent_node n\<^sub>1
targetnode a' = parent_node n\<^sub>4

goal (1 subgoal):
 1. (\<And>a''. \<lbrakk>valid_edge a''; sourcenode a'' = parent_node n\<^sub>1; targetnode a'' = parent_node n\<^sub>4; kind a'' = (\<lambda>cf. False)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce dest:call_return_node_edge)
[PROOF STATE]
proof (state)
this:
valid_edge a''
sourcenode a'' = parent_node n\<^sub>1
targetnode a'' = parent_node n\<^sub>4
kind a'' = (\<lambda>cf. False)\<^sub>\<surd>

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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4
[PROOF STEP]
hence "parent_node n\<^sub>1 -[a'']\<rightarrow>* parent_node n\<^sub>4"
[PROOF STATE]
proof (prove)
using this:
valid_edge a''
sourcenode a'' = parent_node n\<^sub>1
targetnode a'' = parent_node n\<^sub>4
kind a'' = (\<lambda>cf. False)\<^sub>\<surd>

goal (1 subgoal):
 1. parent_node n\<^sub>1 -[a'']\<rightarrow>* parent_node n\<^sub>4
[PROOF STEP]
by(fastforce dest:path_edge)
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>1 -[a'']\<rightarrow>* 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>1 -[a'']\<rightarrow>* 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4
[PROOF STEP]
from \<open>kind a'' = (\<lambda>cf. False)\<^sub>\<surd>\<close>
[PROOF STATE]
proof (chain)
picking this:
kind a'' = (\<lambda>cf. False)\<^sub>\<surd>
[PROOF STEP]
have "\<forall>a \<in> set [a'']. intra_kind(kind a)"
[PROOF STATE]
proof (prove)
using this:
kind a'' = (\<lambda>cf. False)\<^sub>\<surd>

goal (1 subgoal):
 1. \<forall>a\<in>set [a'']. intra_kind (kind a)
[PROOF STEP]
by(fastforce simp:intra_kind_def)
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set [a'']. intra_kind (kind 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
parent_node n\<^sub>1 -[a'']\<rightarrow>* parent_node n\<^sub>4
\<forall>a\<in>set [a'']. intra_kind (kind a)
[PROOF STEP]
have "parent_node n\<^sub>1 -[a'']\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4"
[PROOF STATE]
proof (prove)
using this:
parent_node n\<^sub>1 -[a'']\<rightarrow>* parent_node n\<^sub>4
\<forall>a\<in>set [a'']. intra_kind (kind a)

goal (1 subgoal):
 1. parent_node n\<^sub>1 -[a'']\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4
[PROOF STEP]
by(auto simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>1 -[a'']\<rightarrow>\<^sub>\<iota>* 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4
[PROOF STEP]
with \<open>\<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1
parent_node n\<^sub>1 -[a'']\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1
parent_node n\<^sub>1 -[a'']\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4

goal (1 subgoal):
 1. \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4
[PROOF STEP]
by(fastforce intro:intra_path_Append)
[PROOF STATE]
proof (state)
this:
\<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1
n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2
matched n\<^sub>2 ns' n\<^sub>3
\<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>a' \<in> get_return_edges a\<close> \<open>sourcenode a = parent_node n\<^sub>1\<close>
      \<open>targetnode a' = parent_node n\<^sub>4\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
a' \<in> get_return_edges a
sourcenode a = parent_node n\<^sub>1
targetnode a' = parent_node n\<^sub>4
[PROOF STEP]
obtain a'' where "valid_edge a''" and "sourcenode a'' = parent_node n\<^sub>1"
      and "targetnode a'' = parent_node n\<^sub>4" and "kind a'' = (\<lambda>cf. False)\<^sub>\<surd>"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
a' \<in> get_return_edges a
sourcenode a = parent_node n\<^sub>1
targetnode a' = parent_node n\<^sub>4

goal (1 subgoal):
 1. (\<And>a''. \<lbrakk>valid_edge a''; sourcenode a'' = parent_node n\<^sub>1; targetnode a'' = parent_node n\<^sub>4; kind a'' = (\<lambda>cf. False)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce dest:call_return_node_edge)
[PROOF STATE]
proof (state)
this:
valid_edge a''
sourcenode a'' = parent_node n\<^sub>1
targetnode a'' = parent_node n\<^sub>4
kind a'' = (\<lambda>cf. False)\<^sub>\<surd>

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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4
[PROOF STEP]
hence "parent_node n\<^sub>1 -[a'']\<rightarrow>* parent_node n\<^sub>4"
[PROOF STATE]
proof (prove)
using this:
valid_edge a''
sourcenode a'' = parent_node n\<^sub>1
targetnode a'' = parent_node n\<^sub>4
kind a'' = (\<lambda>cf. False)\<^sub>\<surd>

goal (1 subgoal):
 1. parent_node n\<^sub>1 -[a'']\<rightarrow>* parent_node n\<^sub>4
[PROOF STEP]
by(fastforce dest:path_edge)
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>1 -[a'']\<rightarrow>* 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>1 -[a'']\<rightarrow>* 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4
[PROOF STEP]
from \<open>kind a'' = (\<lambda>cf. False)\<^sub>\<surd>\<close>
[PROOF STATE]
proof (chain)
picking this:
kind a'' = (\<lambda>cf. False)\<^sub>\<surd>
[PROOF STEP]
have "\<forall>a \<in> set [a'']. intra_kind(kind a)"
[PROOF STATE]
proof (prove)
using this:
kind a'' = (\<lambda>cf. False)\<^sub>\<surd>

goal (1 subgoal):
 1. \<forall>a\<in>set [a'']. intra_kind (kind a)
[PROOF STEP]
by(fastforce simp:intra_kind_def)
[PROOF STATE]
proof (state)
this:
\<forall>a\<in>set [a'']. intra_kind (kind 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
parent_node n\<^sub>1 -[a'']\<rightarrow>* parent_node n\<^sub>4
\<forall>a\<in>set [a'']. intra_kind (kind a)
[PROOF STEP]
have "parent_node n\<^sub>1 -[a'']\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4"
[PROOF STATE]
proof (prove)
using this:
parent_node n\<^sub>1 -[a'']\<rightarrow>* parent_node n\<^sub>4
\<forall>a\<in>set [a'']. intra_kind (kind a)

goal (1 subgoal):
 1. parent_node n\<^sub>1 -[a'']\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4
[PROOF STEP]
by(auto simp:intra_path_def)
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>1 -[a'']\<rightarrow>\<^sub>\<iota>* 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1; n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns' n\<^sub>3; \<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^sub>\<iota>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4
[PROOF STEP]
with \<open>\<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1
parent_node n\<^sub>1 -[a'']\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>1
parent_node n\<^sub>1 -[a'']\<rightarrow>\<^sub>\<iota>* parent_node n\<^sub>4

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

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

goal:
No subgoals!
[PROOF STEP]
qed