[STATEMENT]
lemma matched_same_level_CFG_path:
  assumes "matched n ns n'"
  obtains as where "parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>as. parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n'"
[PROOF STATE]
proof (prove)
using this:
matched n ns n'

goal (1 subgoal):
 1. \<exists>as. parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n
 2. \<And>n ns n'' ns' n'. \<lbrakk>matched n ns n''; \<exists>as. parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n''; n'' i-ns'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n
 2. \<And>n ns n'' ns' n'. \<lbrakk>matched n ns n''; \<exists>as. parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n''; n'' i-ns'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n_
[PROOF STEP]
by(fastforce dest:empty_path valid_SDG_CFG_node simp:slp_def same_level_path_def)
[PROOF STATE]
proof (state)
this:
\<exists>as. parent_node n_ -as\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n''; n'' i-ns'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n''; n'' i-ns'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n''; n'' i-ns'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
from \<open>\<exists>as. parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n''\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>as. parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n''
[PROOF STEP]
obtain as where "parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n''"
[PROOF STATE]
proof (prove)
using this:
\<exists>as. parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n''

goal (1 subgoal):
 1. (\<And>as. parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n''; n'' i-ns'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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(erule 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>\<^bsub>sl\<^esub>* parent_node n''; n'' i-ns'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
from \<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'
[PROOF STEP]
have "parent_node n'' -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n'"
[PROOF STATE]
proof (prove)
using this:
parent_node n'' -as'\<rightarrow>\<^sub>\<iota>* parent_node n'

goal (1 subgoal):
 1. parent_node n'' -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n'
[PROOF STEP]
by(rule intra_path_slp)
[PROOF STATE]
proof (state)
this:
parent_node n'' -as'\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n''; n'' i-ns'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
with \<open>parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n''\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n''
parent_node n'' -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n'
[PROOF STEP]
have "parent_node n -as@as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n'"
[PROOF STATE]
proof (prove)
using this:
parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n''
parent_node n'' -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n'

goal (1 subgoal):
 1. parent_node n -as @ as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n'
[PROOF STEP]
by(rule slp_Append)
[PROOF STATE]
proof (state)
this:
parent_node n -as @ as'\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n''; n'' i-ns'\<rightarrow>\<^sub>d* n'\<rbrakk> \<Longrightarrow> \<exists>as. parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
parent_node n -as @ as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n'

goal (1 subgoal):
 1. \<exists>as. parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>as. parent_node n -as\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
from \<open>\<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>1\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>1
[PROOF STEP]
obtain as where "parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
\<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>1

goal (1 subgoal):
 1. (\<And>as. parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
from \<open>\<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3
[PROOF STEP]
obtain as' where "parent_node n\<^sub>2 -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3"
[PROOF STATE]
proof (prove)
using this:
\<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3

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

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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>a' \<in> get_return_edges a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
a' \<in> get_return_edges a
kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs
[PROOF STEP]
obtain Q' f' where "kind a' = Q'\<hookleftarrow>\<^bsub>p'\<^esub>f'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
a' \<in> get_return_edges a
kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs

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

goal (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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
from \<open>parent_node n\<^sub>2 -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n\<^sub>2 -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3
[PROOF STEP]
have "same_level_path as'"
[PROOF STATE]
proof (prove)
using this:
parent_node n\<^sub>2 -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3

goal (1 subgoal):
 1. same_level_path as'
[PROOF STEP]
by(simp add:slp_def)
[PROOF STATE]
proof (state)
this:
same_level_path as'

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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
hence "same_level_path_aux ([]@[a]) as'"
[PROOF STATE]
proof (prove)
using this:
same_level_path as'

goal (1 subgoal):
 1. same_level_path_aux ([] @ [a]) as'
[PROOF STEP]
by(fastforce intro:same_level_path_aux_callstack_Append simp:same_level_path_def)
[PROOF STATE]
proof (state)
this:
same_level_path_aux ([] @ [a]) as'

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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
from \<open>same_level_path as'\<close>
[PROOF STATE]
proof (chain)
picking this:
same_level_path as'
[PROOF STEP]
have "upd_cs ([]@[a]) as' = ([]@[a])"
[PROOF STATE]
proof (prove)
using this:
same_level_path as'

goal (1 subgoal):
 1. upd_cs ([] @ [a]) as' = [] @ [a]
[PROOF STEP]
by(fastforce intro:same_level_path_upd_cs_callstack_Append
                   simp:same_level_path_def)
[PROOF STATE]
proof (state)
this:
upd_cs ([] @ [a]) as' = [] @ [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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
with \<open>same_level_path_aux ([]@[a]) as'\<close> \<open>a' \<in> get_return_edges a\<close>
      \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs\<close> \<open>kind a' = Q'\<hookleftarrow>\<^bsub>p'\<^esub>f'\<close>
[PROOF STATE]
proof (chain)
picking this:
same_level_path_aux ([] @ [a]) as'
a' \<in> get_return_edges a
kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs
kind a' = Q'\<hookleftarrow>\<^bsub>p'\<^esub>f'
upd_cs ([] @ [a]) as' = [] @ [a]
[PROOF STEP]
have "same_level_path (a#as'@[a'])"
[PROOF STATE]
proof (prove)
using this:
same_level_path_aux ([] @ [a]) as'
a' \<in> get_return_edges a
kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs
kind a' = Q'\<hookleftarrow>\<^bsub>p'\<^esub>f'
upd_cs ([] @ [a]) as' = [] @ [a]

goal (1 subgoal):
 1. same_level_path (a # as' @ [a'])
[PROOF STEP]
by(fastforce intro:same_level_path_aux_Append upd_cs_Append
                   simp:same_level_path_def)
[PROOF STATE]
proof (state)
this:
same_level_path (a # as' @ [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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
from \<open>valid_edge a'\<close> \<open>sourcenode a' = parent_node n\<^sub>3\<close>
      \<open>targetnode a' = parent_node n\<^sub>4\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
sourcenode a' = parent_node n\<^sub>3
targetnode a' = parent_node n\<^sub>4
[PROOF STEP]
have "parent_node n\<^sub>3 -[a']\<rightarrow>* parent_node n\<^sub>4"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
sourcenode a' = parent_node n\<^sub>3
targetnode a' = parent_node n\<^sub>4

goal (1 subgoal):
 1. parent_node n\<^sub>3 -[a']\<rightarrow>* parent_node n\<^sub>4
[PROOF STEP]
by(fastforce dest:path_edge)
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>3 -[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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
with \<open>parent_node n\<^sub>2 -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n\<^sub>2 -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3
parent_node n\<^sub>3 -[a']\<rightarrow>* parent_node n\<^sub>4
[PROOF STEP]
have "parent_node n\<^sub>2 -as'@[a']\<rightarrow>* parent_node n\<^sub>4"
[PROOF STATE]
proof (prove)
using this:
parent_node n\<^sub>2 -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3
parent_node n\<^sub>3 -[a']\<rightarrow>* parent_node n\<^sub>4

goal (1 subgoal):
 1. parent_node n\<^sub>2 -as' @ [a']\<rightarrow>* parent_node n\<^sub>4
[PROOF STEP]
by(fastforce intro:path_Append simp:slp_def)
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>2 -as' @ [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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
with \<open>valid_edge a\<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:
valid_edge a
sourcenode a = parent_node n\<^sub>1
targetnode a = parent_node n\<^sub>2
parent_node n\<^sub>2 -as' @ [a']\<rightarrow>* parent_node n\<^sub>4
[PROOF STEP]
have "parent_node n\<^sub>1 -a#as'@[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>2
parent_node n\<^sub>2 -as' @ [a']\<rightarrow>* parent_node n\<^sub>4

goal (1 subgoal):
 1. parent_node n\<^sub>1 -a # as' @ [a']\<rightarrow>* parent_node n\<^sub>4
[PROOF STEP]
by -(rule Cons_path)
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>1 -a # as' @ [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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
with \<open>same_level_path (a#as'@[a'])\<close>
[PROOF STATE]
proof (chain)
picking this:
same_level_path (a # as' @ [a'])
parent_node n\<^sub>1 -a # as' @ [a']\<rightarrow>* parent_node n\<^sub>4
[PROOF STEP]
have "parent_node n\<^sub>1 -a#as'@[a']\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>4"
[PROOF STATE]
proof (prove)
using this:
same_level_path (a # as' @ [a'])
parent_node n\<^sub>1 -a # as' @ [a']\<rightarrow>* parent_node n\<^sub>4

goal (1 subgoal):
 1. parent_node n\<^sub>1 -a # as' @ [a']\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
by(simp add:slp_def)
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>1 -a # as' @ [a']\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
with \<open>parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>1\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>1
parent_node n\<^sub>1 -a # as' @ [a']\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
have "parent_node n\<^sub>0 -as@a#as'@[a']\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>4"
[PROOF STATE]
proof (prove)
using this:
parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>1
parent_node n\<^sub>1 -a # as' @ [a']\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>4

goal (1 subgoal):
 1. parent_node n\<^sub>0 -as @ a # as' @ [a']\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
by(rule slp_Append)
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>0 -as @ a # as' @ [a']\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
with \<open>sourcenode a = parent_node n\<^sub>1\<close> \<open>sourcenode a' = parent_node n\<^sub>3\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode a = parent_node n\<^sub>1
sourcenode a' = parent_node n\<^sub>3
parent_node n\<^sub>0 -as @ a # as' @ [a']\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sourcenode a = parent_node n\<^sub>1
sourcenode a' = parent_node n\<^sub>3
parent_node n\<^sub>0 -as @ a # as' @ [a']\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>4

goal (1 subgoal):
 1. \<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
from \<open>\<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>1\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>1
[PROOF STEP]
obtain as where "parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
\<exists>as. parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>1

goal (1 subgoal):
 1. (\<And>as. parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
from \<open>\<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3
[PROOF STEP]
obtain as' where "parent_node n\<^sub>2 -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3"
[PROOF STATE]
proof (prove)
using this:
\<exists>as. parent_node n\<^sub>2 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3

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

goal (1 subgoal):
 1. \<And>n\<^sub>0 ns n\<^sub>1 p 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>a' \<in> get_return_edges a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
a' \<in> get_return_edges a
kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs
[PROOF STEP]
obtain Q' f' where "kind a' = Q'\<hookleftarrow>\<^bsub>p'\<^esub>f'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
a' \<in> get_return_edges a
kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs

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

goal (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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node 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>as. parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
from \<open>parent_node n\<^sub>2 -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n\<^sub>2 -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3
[PROOF STEP]
have "same_level_path as'"
[PROOF STATE]
proof (prove)
using this:
parent_node n\<^sub>2 -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3

goal (1 subgoal):
 1. same_level_path as'
[PROOF STEP]
by(simp add:slp_def)
[PROOF STATE]
proof (state)
this:
same_level_path as'

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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
hence "same_level_path_aux ([]@[a]) as'"
[PROOF STATE]
proof (prove)
using this:
same_level_path as'

goal (1 subgoal):
 1. same_level_path_aux ([] @ [a]) as'
[PROOF STEP]
by(fastforce intro:same_level_path_aux_callstack_Append simp:same_level_path_def)
[PROOF STATE]
proof (state)
this:
same_level_path_aux ([] @ [a]) as'

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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
from \<open>same_level_path as'\<close>
[PROOF STATE]
proof (chain)
picking this:
same_level_path as'
[PROOF STEP]
have "upd_cs ([]@[a]) as' = ([]@[a])"
[PROOF STATE]
proof (prove)
using this:
same_level_path as'

goal (1 subgoal):
 1. upd_cs ([] @ [a]) as' = [] @ [a]
[PROOF STEP]
by(fastforce intro:same_level_path_upd_cs_callstack_Append
                   simp:same_level_path_def)
[PROOF STATE]
proof (state)
this:
upd_cs ([] @ [a]) as' = [] @ [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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
with \<open>same_level_path_aux ([]@[a]) as'\<close> \<open>a' \<in> get_return_edges a\<close>
      \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs\<close> \<open>kind a' = Q'\<hookleftarrow>\<^bsub>p'\<^esub>f'\<close>
[PROOF STATE]
proof (chain)
picking this:
same_level_path_aux ([] @ [a]) as'
a' \<in> get_return_edges a
kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs
kind a' = Q'\<hookleftarrow>\<^bsub>p'\<^esub>f'
upd_cs ([] @ [a]) as' = [] @ [a]
[PROOF STEP]
have "same_level_path (a#as'@[a'])"
[PROOF STATE]
proof (prove)
using this:
same_level_path_aux ([] @ [a]) as'
a' \<in> get_return_edges a
kind a = Q:r\<hookrightarrow>\<^bsub>p'\<^esub>fs
kind a' = Q'\<hookleftarrow>\<^bsub>p'\<^esub>f'
upd_cs ([] @ [a]) as' = [] @ [a]

goal (1 subgoal):
 1. same_level_path (a # as' @ [a'])
[PROOF STEP]
by(fastforce intro:same_level_path_aux_Append upd_cs_Append
                   simp:same_level_path_def)
[PROOF STATE]
proof (state)
this:
same_level_path (a # as' @ [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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
from \<open>valid_edge a'\<close> \<open>sourcenode a' = parent_node n\<^sub>3\<close>
      \<open>targetnode a' = parent_node n\<^sub>4\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
sourcenode a' = parent_node n\<^sub>3
targetnode a' = parent_node n\<^sub>4
[PROOF STEP]
have "parent_node n\<^sub>3 -[a']\<rightarrow>* parent_node n\<^sub>4"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
sourcenode a' = parent_node n\<^sub>3
targetnode a' = parent_node n\<^sub>4

goal (1 subgoal):
 1. parent_node n\<^sub>3 -[a']\<rightarrow>* parent_node n\<^sub>4
[PROOF STEP]
by(fastforce dest:path_edge)
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>3 -[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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
with \<open>parent_node n\<^sub>2 -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n\<^sub>2 -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3
parent_node n\<^sub>3 -[a']\<rightarrow>* parent_node n\<^sub>4
[PROOF STEP]
have "parent_node n\<^sub>2 -as'@[a']\<rightarrow>* parent_node n\<^sub>4"
[PROOF STATE]
proof (prove)
using this:
parent_node n\<^sub>2 -as'\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>3
parent_node n\<^sub>3 -[a']\<rightarrow>* parent_node n\<^sub>4

goal (1 subgoal):
 1. parent_node n\<^sub>2 -as' @ [a']\<rightarrow>* parent_node n\<^sub>4
[PROOF STEP]
by(fastforce intro:path_Append simp:slp_def)
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>2 -as' @ [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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
with \<open>valid_edge a\<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:
valid_edge a
sourcenode a = parent_node n\<^sub>1
targetnode a = parent_node n\<^sub>2
parent_node n\<^sub>2 -as' @ [a']\<rightarrow>* parent_node n\<^sub>4
[PROOF STEP]
have "parent_node n\<^sub>1 -a#as'@[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>2
parent_node n\<^sub>2 -as' @ [a']\<rightarrow>* parent_node n\<^sub>4

goal (1 subgoal):
 1. parent_node n\<^sub>1 -a # as' @ [a']\<rightarrow>* parent_node n\<^sub>4
[PROOF STEP]
by -(rule Cons_path)
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>1 -a # as' @ [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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
with \<open>same_level_path (a#as'@[a'])\<close>
[PROOF STATE]
proof (chain)
picking this:
same_level_path (a # as' @ [a'])
parent_node n\<^sub>1 -a # as' @ [a']\<rightarrow>* parent_node n\<^sub>4
[PROOF STEP]
have "parent_node n\<^sub>1 -a#as'@[a']\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>4"
[PROOF STATE]
proof (prove)
using this:
same_level_path (a # as' @ [a'])
parent_node n\<^sub>1 -a # as' @ [a']\<rightarrow>* parent_node n\<^sub>4

goal (1 subgoal):
 1. parent_node n\<^sub>1 -a # as' @ [a']\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
by(simp add:slp_def)
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>1 -a # as' @ [a']\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
with \<open>parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>1\<close>
[PROOF STATE]
proof (chain)
picking this:
parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>1
parent_node n\<^sub>1 -a # as' @ [a']\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
have "parent_node n\<^sub>0 -as@a#as'@[a']\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>4"
[PROOF STATE]
proof (prove)
using this:
parent_node n\<^sub>0 -as\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>1
parent_node n\<^sub>1 -a # as' @ [a']\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>4

goal (1 subgoal):
 1. parent_node n\<^sub>0 -as @ a # as' @ [a']\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
by(rule slp_Append)
[PROOF STATE]
proof (state)
this:
parent_node n\<^sub>0 -as @ a # as' @ [a']\<rightarrow>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* 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>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
with \<open>sourcenode a = parent_node n\<^sub>1\<close> \<open>sourcenode a' = parent_node n\<^sub>3\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode a = parent_node n\<^sub>1
sourcenode a' = parent_node n\<^sub>3
parent_node n\<^sub>0 -as @ a # as' @ [a']\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>4
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sourcenode a = parent_node n\<^sub>1
sourcenode a' = parent_node n\<^sub>3
parent_node n\<^sub>0 -as @ a # as' @ [a']\<rightarrow>\<^bsub>sl\<^esub>* parent_node n\<^sub>4

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma realizable_Append_matched:
  "\<lbrakk>realizable n ns n''; matched n'' ns' n'\<rbrakk> \<Longrightarrow> realizable n (ns@ns') n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>realizable n ns n''; matched n'' ns' n'\<rbrakk> \<Longrightarrow> realizable n (ns @ ns') n'
[PROOF STEP]
proof(induct rule:realizable.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n ns n'a. \<lbrakk>matched n ns n'a; matched n'a ns' n'\<rbrakk> \<Longrightarrow> realizable n (ns @ ns') n'
 2. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns'a n\<^sub>3. \<lbrakk>realizable n\<^sub>0 ns n\<^sub>1; matched n\<^sub>1 ns' n' \<Longrightarrow> realizable n\<^sub>0 (ns @ ns') n'; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns'a n\<^sub>3; matched n\<^sub>3 ns' n'\<rbrakk> \<Longrightarrow> realizable n\<^sub>0 ((ns @ n\<^sub>1 # ns'a) @ ns') n'
[PROOF STEP]
case (realizable_matched n ns n'')
[PROOF STATE]
proof (state)
this:
matched n ns n''
matched n'' ns' n'

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

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 (2 subgoals):
 1. \<And>n ns n'a. \<lbrakk>matched n ns n'a; matched n'a ns' n'\<rbrakk> \<Longrightarrow> realizable n (ns @ ns') n'
 2. \<And>n\<^sub>0 ns n\<^sub>1 p n\<^sub>2 V ns'a n\<^sub>3. \<lbrakk>realizable n\<^sub>0 ns n\<^sub>1; matched n\<^sub>1 ns' n' \<Longrightarrow> realizable n\<^sub>0 (ns @ ns') n'; n\<^sub>1 -p\<rightarrow>\<^bsub>call\<^esub> n\<^sub>2 \<or> n\<^sub>1 -p:V\<rightarrow>\<^bsub>in\<^esub> n\<^sub>2; matched n\<^sub>2 ns'a n\<^sub>3; matched n\<^sub>3 ns' n'\<rbrakk> \<Longrightarrow> realizable n\<^sub>0 ((ns @ n\<^sub>1 # ns'a) @ ns') n'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
matched n (ns @ ns') n'

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

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

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

goal (1 subgoal):
 1. matched n\<^sub>2 (ns'' @ ns') n'
[PROOF STEP]
by(rule matched_Append)
[PROOF STATE]
proof (state)
this:
matched n\<^sub>2 (ns'' @ ns') n'

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

goal (1 subgoal):
 1. realizable n\<^sub>0 (ns @ n\<^sub>1 # ns'' @ ns') n'
[PROOF STEP]
by(rule realizable.realizable_call)
[PROOF STATE]
proof (state)
this:
realizable n\<^sub>0 (ns @ n\<^sub>1 # ns'' @ ns') n'

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

goal (1 subgoal):
 1. realizable n\<^sub>0 ((ns @ n\<^sub>1 # ns'') @ ns') n'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
realizable n\<^sub>0 ((ns @ n\<^sub>1 # ns'') @ ns') n'

goal:
No subgoals!
[PROOF STEP]
qed