[STATEMENT]
lemma slpa_silent_moves_callstacks_eq:
  "\<lbrakk>same_level_path_aux cs as; S,f \<turnstile> (m#msx@ms,s) =as\<Rightarrow>\<^sub>\<tau> (m'#ms',s');
  length ms = length ms'; valid_call_list cs m;
  \<forall>i < length rs. rs!i \<in> get_return_edges (cs!i); valid_return_list rs m;
  length rs = length cs; msx = targetnodes rs\<rbrakk>
  \<Longrightarrow> ms = ms'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>same_level_path_aux cs as; S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
proof(induct arbitrary:m msx s rs rule:slpa_induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>cs m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =[]\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as m msx s rs. \<lbrakk>intra_kind (kind a); same_level_path_aux cs as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 3. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 4. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
case (slpa_empty cs)
[PROOF STATE]
proof (state)
this:
S,f \<turnstile> (m # msx @ ms,s) =[]\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
length ms = length ms'
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
msx = targetnodes rs

goal (4 subgoals):
 1. \<And>cs m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =[]\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as m msx s rs. \<lbrakk>intra_kind (kind a); same_level_path_aux cs as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 3. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 4. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>S,f \<turnstile> (m # msx @ ms,s) =[]\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (m # msx @ ms,s) =[]\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
[PROOF STEP]
have "msx@ms = ms'"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (m # msx @ ms,s) =[]\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (1 subgoal):
 1. msx @ ms = ms'
[PROOF STEP]
by(fastforce elim:silent_moves.cases)
[PROOF STATE]
proof (state)
this:
msx @ ms = ms'

goal (4 subgoals):
 1. \<And>cs m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =[]\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as m msx s rs. \<lbrakk>intra_kind (kind a); same_level_path_aux cs as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 3. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 4. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
with \<open>length ms = length ms'\<close>
[PROOF STATE]
proof (chain)
picking this:
length ms = length ms'
msx @ ms = ms'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length ms = length ms'
msx @ ms = ms'

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

goal (3 subgoals):
 1. \<And>cs a as m msx s rs. \<lbrakk>intra_kind (kind a); same_level_path_aux cs as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 3. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>cs a as m msx s rs. \<lbrakk>intra_kind (kind a); same_level_path_aux cs as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 3. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
case (slpa_intra cs a as)
[PROOF STATE]
proof (state)
this:
intra_kind (kind a)
same_level_path_aux cs as
\<lbrakk>S,f \<turnstile> (?m # ?msx @ ms,?s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs ?m; \<forall>i<length ?rs. ?rs ! i \<in> get_return_edges (cs ! i); valid_return_list ?rs ?m; length ?rs = length cs; ?msx = targetnodes ?rs\<rbrakk> \<Longrightarrow> ms = ms'
S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
length ms = length ms'
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
msx = targetnodes rs

goal (3 subgoals):
 1. \<And>cs a as m msx s rs. \<lbrakk>intra_kind (kind a); same_level_path_aux cs as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 3. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
note IH = \<open>\<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s');
    length ms = length ms'; valid_call_list cs m;
    \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i);
    valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk>
    \<Longrightarrow> ms = ms'\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>S,f \<turnstile> (?m # ?msx @ ms,?s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs ?m; \<forall>i<length ?rs. ?rs ! i \<in> get_return_edges (cs ! i); valid_return_list ?rs ?m; length ?rs = length cs; ?msx = targetnodes ?rs\<rbrakk> \<Longrightarrow> ms = ms'

goal (3 subgoals):
 1. \<And>cs a as m msx s rs. \<lbrakk>intra_kind (kind a); same_level_path_aux cs as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 3. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
[PROOF STEP]
obtain ms'' s''
  where "S,f \<turnstile> (m # msx @ ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'',s'')"
    and "S,f \<turnstile> (ms'',s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (1 subgoal):
 1. (\<And>ms'' s''. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'',s''); S,f \<turnstile> (ms'',s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto elim:silent_moves.cases)
[PROOF STATE]
proof (state)
this:
S,f \<turnstile> (m # msx @ ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'',s'')
S,f \<turnstile> (ms'',s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (3 subgoals):
 1. \<And>cs a as m msx s rs. \<lbrakk>intra_kind (kind a); same_level_path_aux cs as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 3. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>S,f \<turnstile> (m # msx @ ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'',s'')\<close> \<open>intra_kind (kind a)\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (m # msx @ ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'',s'')
intra_kind (kind a)
[PROOF STEP]
have "valid_edge a" and [simp]:"m = sourcenode a" "ms'' = targetnode a # msx @ ms"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (m # msx @ ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'',s'')
intra_kind (kind a)

goal (1 subgoal):
 1. valid_edge a &&& m = sourcenode a &&& ms'' = targetnode a # msx @ ms
[PROOF STEP]
by(fastforce elim:silent_move.cases simp:intra_kind_def)+
[PROOF STATE]
proof (state)
this:
valid_edge a
m = sourcenode a
ms'' = targetnode a # msx @ ms

goal (3 subgoals):
 1. \<And>cs a as m msx s rs. \<lbrakk>intra_kind (kind a); same_level_path_aux cs as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 3. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>intra_kind (kind a)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
intra_kind (kind a)
[PROOF STEP]
have "get_proc (sourcenode a) = get_proc (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
intra_kind (kind a)

goal (1 subgoal):
 1. get_proc (sourcenode a) = get_proc (targetnode a)
[PROOF STEP]
by(rule get_proc_intra)
[PROOF STATE]
proof (state)
this:
get_proc (sourcenode a) = get_proc (targetnode a)

goal (3 subgoals):
 1. \<And>cs a as m msx s rs. \<lbrakk>intra_kind (kind a); same_level_path_aux cs as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 3. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>valid_call_list cs m\<close> \<open>m = sourcenode a\<close>
    \<open>get_proc (sourcenode a) = get_proc (targetnode a)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_call_list cs m
m = sourcenode a
get_proc (sourcenode a) = get_proc (targetnode a)
[PROOF STEP]
have "valid_call_list cs (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_call_list cs m
m = sourcenode a
get_proc (sourcenode a) = get_proc (targetnode a)

goal (1 subgoal):
 1. valid_call_list cs (targetnode a)
[PROOF STEP]
apply(clarsimp simp:valid_call_list_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs''. \<lbrakk>\<forall>cs'a ca. (\<exists>cs''a. cs' @ c # cs'' = cs'a @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q r fs. kind ca = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs'a of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (sourcenodes cs'a))\<^esub>fs); get_proc (sourcenode a) = get_proc (targetnode a); cs = cs' @ c # cs''\<rbrakk> \<Longrightarrow> \<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs
[PROOF STEP]
apply(erule_tac x="cs'" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs''. \<lbrakk>get_proc (sourcenode a) = get_proc (targetnode a); cs = cs' @ c # cs''; \<forall>ca. (\<exists>cs''a. cs' @ c # cs'' = cs' @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q r fs. kind ca = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs)\<rbrakk> \<Longrightarrow> \<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs
[PROOF STEP]
apply(erule_tac x="c" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs''. \<lbrakk>get_proc (sourcenode a) = get_proc (targetnode a); cs = cs' @ c # cs''; (\<exists>cs''a. cs' @ c # cs'' = cs' @ c # cs''a) \<longrightarrow> valid_edge c \<and> (\<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs)\<rbrakk> \<Longrightarrow> \<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs
[PROOF STEP]
by(auto split:list.split)
[PROOF STATE]
proof (state)
this:
valid_call_list cs (targetnode a)

goal (3 subgoals):
 1. \<And>cs a as m msx s rs. \<lbrakk>intra_kind (kind a); same_level_path_aux cs as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 3. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>valid_return_list rs m\<close> \<open>m = sourcenode a\<close>
    \<open>get_proc (sourcenode a) = get_proc (targetnode a)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_return_list rs m
m = sourcenode a
get_proc (sourcenode a) = get_proc (targetnode a)
[PROOF STEP]
have "valid_return_list rs (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_return_list rs m
m = sourcenode a
get_proc (sourcenode a) = get_proc (targetnode a)

goal (1 subgoal):
 1. valid_return_list rs (targetnode a)
[PROOF STEP]
apply(clarsimp simp:valid_return_list_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs''. \<lbrakk>\<forall>cs'a ca. (\<exists>cs''a. cs' @ c # cs'' = cs'a @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q f. kind ca = Q\<hookleftarrow>\<^bsub>get_proc (case cs'a of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (targetnodes cs'a))\<^esub>f); get_proc (sourcenode a) = get_proc (targetnode a); rs = cs' @ c # cs''\<rbrakk> \<Longrightarrow> \<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f
[PROOF STEP]
apply(erule_tac x="cs'" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs''. \<lbrakk>get_proc (sourcenode a) = get_proc (targetnode a); rs = cs' @ c # cs''; \<forall>ca. (\<exists>cs''a. cs' @ c # cs'' = cs' @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q f. kind ca = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f)\<rbrakk> \<Longrightarrow> \<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs'' Q f. \<lbrakk>get_proc (sourcenode a) = get_proc (targetnode a); rs = cs' @ c # cs''; valid_edge c; kind c = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f\<rbrakk> \<Longrightarrow> get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (targetnodes cs')) = get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (targetnodes cs'))
[PROOF STEP]
by(case_tac cs') auto
[PROOF STATE]
proof (state)
this:
valid_return_list rs (targetnode a)

goal (3 subgoals):
 1. \<And>cs a as m msx s rs. \<lbrakk>intra_kind (kind a); same_level_path_aux cs as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 3. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>S,f \<turnstile> (ms'',s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (ms'',s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
[PROOF STEP]
have "S,f \<turnstile> (targetnode a # msx @ ms,s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (ms'',s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (1 subgoal):
 1. S,f \<turnstile> (targetnode a # msx @ ms,s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
S,f \<turnstile> (targetnode a # msx @ ms,s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (3 subgoals):
 1. \<And>cs a as m msx s rs. \<lbrakk>intra_kind (kind a); same_level_path_aux cs as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 3. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from IH[OF this \<open>length ms = length ms'\<close> \<open>valid_call_list cs (targetnode a)\<close>
    \<open>\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)\<close>
    \<open>valid_return_list rs (targetnode a)\<close> \<open>length rs = length cs\<close>
    \<open>msx = targetnodes rs\<close>]
[PROOF STATE]
proof (chain)
picking this:
ms = ms'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ms = ms'

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

goal (2 subgoals):
 1. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
case (slpa_Call cs a as Q r p fs)
[PROOF STATE]
proof (state)
this:
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
same_level_path_aux (a # cs) as
\<lbrakk>S,f \<turnstile> (?m # ?msx @ ms,?s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) ?m; \<forall>i<length ?rs. ?rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list ?rs ?m; length ?rs = length (a # cs); ?msx = targetnodes ?rs\<rbrakk> \<Longrightarrow> ms = ms'
S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
length ms = length ms'
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
msx = targetnodes rs

goal (2 subgoals):
 1. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
note IH = \<open>\<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s');
    length ms = length ms'; valid_call_list (a # cs) m;
    \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i);
    valid_return_list rs m; length rs = length (a # cs);
    msx = targetnodes rs\<rbrakk>
    \<Longrightarrow> ms = ms'\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>S,f \<turnstile> (?m # ?msx @ ms,?s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) ?m; \<forall>i<length ?rs. ?rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list ?rs ?m; length ?rs = length (a # cs); ?msx = targetnodes ?rs\<rbrakk> \<Longrightarrow> ms = ms'

goal (2 subgoals):
 1. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
[PROOF STEP]
obtain ms'' s''
    where "S,f \<turnstile> (m # msx @ ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'',s'')"
    and "S,f \<turnstile> (ms'',s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (1 subgoal):
 1. (\<And>ms'' s''. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'',s''); S,f \<turnstile> (ms'',s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto elim:silent_moves.cases)
[PROOF STATE]
proof (state)
this:
S,f \<turnstile> (m # msx @ ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'',s'')
S,f \<turnstile> (ms'',s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (2 subgoals):
 1. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>S,f \<turnstile> (m # msx @ ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'',s'')\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (m # msx @ ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'',s'')
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
obtain a' where "valid_edge a" and [simp]:"m = sourcenode a"
    and [simp]:"ms'' = targetnode a # targetnode a' # msx @ ms"
    and "a' \<in> get_return_edges a"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (m # msx @ ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'',s'')
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. (\<And>a'. \<lbrakk>valid_edge a; m = sourcenode a; ms'' = targetnode a # targetnode a' # msx @ ms; a' \<in> get_return_edges a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto elim:silent_move.cases simp:intra_kind_def)
[PROOF STATE]
proof (state)
this:
valid_edge a
m = sourcenode a
ms'' = targetnode a # targetnode a' # msx @ ms
a' \<in> get_return_edges a

goal (2 subgoals):
 1. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
have "get_proc (targetnode a) = p"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. get_proc (targetnode a) = p
[PROOF STEP]
by(rule get_proc_call)
[PROOF STATE]
proof (state)
this:
get_proc (targetnode a) = p

goal (2 subgoals):
 1. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
with \<open>valid_call_list cs m\<close> \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>m = sourcenode a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_call_list cs m
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
m = sourcenode a
get_proc (targetnode a) = p
[PROOF STEP]
have "valid_call_list (a # cs) (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_call_list cs m
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
m = sourcenode a
get_proc (targetnode a) = p

goal (1 subgoal):
 1. valid_call_list (a # cs) (targetnode a)
[PROOF STEP]
apply(clarsimp simp:valid_call_list_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs''. \<lbrakk>\<forall>cs' c. (\<exists>cs''. cs = cs' @ c # cs'') \<longrightarrow> valid_edge c \<and> (\<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs); valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>get_proc (targetnode a)\<^esub>fs; p = get_proc (targetnode a); a # cs = cs' @ c # cs''\<rbrakk> \<Longrightarrow> valid_edge c \<and> (\<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs)
[PROOF STEP]
apply(case_tac cs')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>cs' c cs''. \<lbrakk>\<forall>cs' c. (\<exists>cs''. cs = cs' @ c # cs'') \<longrightarrow> valid_edge c \<and> (\<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs); valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>get_proc (targetnode a)\<^esub>fs; p = get_proc (targetnode a); a # cs = cs' @ c # cs''; cs' = []\<rbrakk> \<Longrightarrow> valid_edge c \<and> (\<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs)
 2. \<And>cs' c cs'' aa list. \<lbrakk>\<forall>cs' c. (\<exists>cs''. cs = cs' @ c # cs'') \<longrightarrow> valid_edge c \<and> (\<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs); valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>get_proc (targetnode a)\<^esub>fs; p = get_proc (targetnode a); a # cs = cs' @ c # cs''; cs' = aa # list\<rbrakk> \<Longrightarrow> valid_edge c \<and> (\<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c cs'' list. \<lbrakk>\<forall>cs' ca. (\<exists>cs''a. list @ c # cs'' = cs' @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q r fs. kind ca = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs); valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>get_proc (targetnode a)\<^esub>fs; p = get_proc (targetnode a); cs = list @ c # cs''\<rbrakk> \<Longrightarrow> \<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (last (sourcenodes (a # list)))\<^esub>fs
[PROOF STEP]
apply(erule_tac x="list" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c cs'' list. \<lbrakk>valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>get_proc (targetnode a)\<^esub>fs; p = get_proc (targetnode a); cs = list @ c # cs''; \<forall>ca. (\<exists>cs''a. list @ c # cs'' = list @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q r fs. kind ca = Q:r\<hookrightarrow>\<^bsub>get_proc (case list of [] \<Rightarrow> sourcenode a | a # lista \<Rightarrow> last (sourcenodes list))\<^esub>fs)\<rbrakk> \<Longrightarrow> \<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (last (sourcenodes (a # list)))\<^esub>fs
[PROOF STEP]
by(case_tac list)(auto simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
valid_call_list (a # cs) (targetnode a)

goal (2 subgoals):
 1. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)\<close> \<open>a' \<in> get_return_edges a\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
a' \<in> get_return_edges a
[PROOF STEP]
have "\<forall>i<length (a'#rs). (a'#rs) ! i \<in> get_return_edges ((a#cs) ! i)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
a' \<in> get_return_edges a

goal (1 subgoal):
 1. \<forall>i<length (a' # rs). (a' # rs) ! i \<in> get_return_edges ((a # cs) ! i)
[PROOF STEP]
by auto(case_tac i,auto)
[PROOF STATE]
proof (state)
this:
\<forall>i<length (a' # rs). (a' # rs) ! i \<in> get_return_edges ((a # cs) ! i)

goal (2 subgoals):
 1. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[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>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>a' \<in> get_return_edges a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
a' \<in> get_return_edges a
[PROOF STEP]
obtain Q' f' where "kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
a' \<in> get_return_edges a

goal (1 subgoal):
 1. (\<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>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>valid_edge a'\<close> \<open>kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
[PROOF STEP]
have "get_proc (sourcenode a') = p"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'

goal (1 subgoal):
 1. get_proc (sourcenode a') = p
[PROOF STEP]
by(rule get_proc_return)
[PROOF STATE]
proof (state)
this:
get_proc (sourcenode a') = p

goal (2 subgoals):
 1. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[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 "get_proc (sourcenode a) = get_proc (targetnode a')"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
a' \<in> get_return_edges a

goal (1 subgoal):
 1. get_proc (sourcenode a) = get_proc (targetnode a')
[PROOF STEP]
by(rule get_proc_get_return_edge)
[PROOF STATE]
proof (state)
this:
get_proc (sourcenode a) = get_proc (targetnode a')

goal (2 subgoals):
 1. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
with \<open>valid_return_list rs m\<close> \<open>valid_edge a'\<close> \<open>kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'\<close>
    \<open>get_proc (sourcenode a') = p\<close> \<open>get_proc (targetnode a) = p\<close> \<open>m = sourcenode a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_return_list rs m
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
get_proc (sourcenode a') = p
get_proc (targetnode a) = p
m = sourcenode a
get_proc (sourcenode a) = get_proc (targetnode a')
[PROOF STEP]
have "valid_return_list (a'#rs) (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_return_list rs m
valid_edge a'
kind a' = Q'\<hookleftarrow>\<^bsub>p\<^esub>f'
get_proc (sourcenode a') = p
get_proc (targetnode a) = p
m = sourcenode a
get_proc (sourcenode a) = get_proc (targetnode a')

goal (1 subgoal):
 1. valid_return_list (a' # rs) (targetnode a)
[PROOF STEP]
apply(clarsimp simp:valid_return_list_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs''. \<lbrakk>\<forall>cs' c. (\<exists>cs''. rs = cs' @ c # cs'') \<longrightarrow> valid_edge c \<and> (\<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f); valid_edge a'; kind a' = Q'\<hookleftarrow>\<^bsub>get_proc (sourcenode a')\<^esub>f'; get_proc (targetnode a) = get_proc (sourcenode a'); get_proc (sourcenode a) = get_proc (targetnode a'); p = get_proc (sourcenode a'); a' # rs = cs' @ c # cs''\<rbrakk> \<Longrightarrow> valid_edge c \<and> (\<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f)
[PROOF STEP]
apply(case_tac cs')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>cs' c cs''. \<lbrakk>\<forall>cs' c. (\<exists>cs''. rs = cs' @ c # cs'') \<longrightarrow> valid_edge c \<and> (\<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f); valid_edge a'; kind a' = Q'\<hookleftarrow>\<^bsub>get_proc (sourcenode a')\<^esub>f'; get_proc (targetnode a) = get_proc (sourcenode a'); get_proc (sourcenode a) = get_proc (targetnode a'); p = get_proc (sourcenode a'); a' # rs = cs' @ c # cs''; cs' = []\<rbrakk> \<Longrightarrow> valid_edge c \<and> (\<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f)
 2. \<And>cs' c cs'' aa list. \<lbrakk>\<forall>cs' c. (\<exists>cs''. rs = cs' @ c # cs'') \<longrightarrow> valid_edge c \<and> (\<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f); valid_edge a'; kind a' = Q'\<hookleftarrow>\<^bsub>get_proc (sourcenode a')\<^esub>f'; get_proc (targetnode a) = get_proc (sourcenode a'); get_proc (sourcenode a) = get_proc (targetnode a'); p = get_proc (sourcenode a'); a' # rs = cs' @ c # cs''; cs' = aa # list\<rbrakk> \<Longrightarrow> valid_edge c \<and> (\<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c cs'' list. \<lbrakk>\<forall>cs' ca. (\<exists>cs''a. list @ c # cs'' = cs' @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q f. kind ca = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> sourcenode a | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f); valid_edge a'; kind a' = Q'\<hookleftarrow>\<^bsub>get_proc (sourcenode a')\<^esub>f'; get_proc (targetnode a) = get_proc (sourcenode a'); get_proc (sourcenode a) = get_proc (targetnode a'); p = get_proc (sourcenode a'); rs = list @ c # cs''\<rbrakk> \<Longrightarrow> \<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (last (targetnodes (a' # list)))\<^esub>f
[PROOF STEP]
apply(erule_tac x="list" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c cs'' list. \<lbrakk>valid_edge a'; kind a' = Q'\<hookleftarrow>\<^bsub>get_proc (sourcenode a')\<^esub>f'; get_proc (targetnode a) = get_proc (sourcenode a'); get_proc (sourcenode a) = get_proc (targetnode a'); p = get_proc (sourcenode a'); rs = list @ c # cs''; \<forall>ca. (\<exists>cs''a. list @ c # cs'' = list @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q f. kind ca = Q\<hookleftarrow>\<^bsub>get_proc (case list of [] \<Rightarrow> sourcenode a | a # lista \<Rightarrow> last (targetnodes list))\<^esub>f)\<rbrakk> \<Longrightarrow> \<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (last (targetnodes (a' # list)))\<^esub>f
[PROOF STEP]
by(case_tac list)(auto simp:targetnodes_def)
[PROOF STATE]
proof (state)
this:
valid_return_list (a' # rs) (targetnode a)

goal (2 subgoals):
 1. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>length rs = length cs\<close>
[PROOF STATE]
proof (chain)
picking this:
length rs = length cs
[PROOF STEP]
have "length (a'#rs) = length (a#cs)"
[PROOF STATE]
proof (prove)
using this:
length rs = length cs

goal (1 subgoal):
 1. length (a' # rs) = length (a # cs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (a' # rs) = length (a # cs)

goal (2 subgoals):
 1. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>msx = targetnodes rs\<close>
[PROOF STATE]
proof (chain)
picking this:
msx = targetnodes rs
[PROOF STEP]
have "targetnode a' # msx = targetnodes (a' # rs)"
[PROOF STATE]
proof (prove)
using this:
msx = targetnodes rs

goal (1 subgoal):
 1. targetnode a' # msx = targetnodes (a' # rs)
[PROOF STEP]
by(simp add:targetnodes_def)
[PROOF STATE]
proof (state)
this:
targetnode a' # msx = targetnodes (a' # rs)

goal (2 subgoals):
 1. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>S,f \<turnstile> (ms'',s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (ms'',s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
[PROOF STEP]
have "S,f \<turnstile> (targetnode a # (targetnode a' # msx) @ ms,s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (ms'',s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (1 subgoal):
 1. S,f \<turnstile> (targetnode a # (targetnode a' # msx) @ ms,s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
S,f \<turnstile> (targetnode a # (targetnode a' # msx) @ ms,s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (2 subgoals):
 1. \<And>cs a as Q r p fs m msx s rs. \<lbrakk>kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; same_level_path_aux (a # cs) as; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list (a # cs) m; \<forall>i<length rs. rs ! i \<in> get_return_edges ((a # cs) ! i); valid_return_list rs m; length rs = length (a # cs); msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
 2. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from IH[OF this \<open>length ms = length ms'\<close> \<open>valid_call_list (a # cs) (targetnode a)\<close>
    \<open>\<forall>i<length (a'#rs). (a'#rs) ! i \<in> get_return_edges ((a#cs) ! i)\<close>
    \<open>valid_return_list (a'#rs) (targetnode a)\<close> \<open>length (a'#rs) = length (a#cs)\<close>
    \<open>targetnode a' # msx = targetnodes (a' # rs)\<close>]
[PROOF STATE]
proof (chain)
picking this:
ms = ms'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ms = ms'

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

goal (1 subgoal):
 1. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
case (slpa_Return cs a as Q p f' c' cs')
[PROOF STATE]
proof (state)
this:
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'
cs = c' # cs'
same_level_path_aux cs' as
a \<in> get_return_edges c'
\<lbrakk>S,f \<turnstile> (?m # ?msx @ ms,?s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' ?m; \<forall>i<length ?rs. ?rs ! i \<in> get_return_edges (cs' ! i); valid_return_list ?rs ?m; length ?rs = length cs'; ?msx = targetnodes ?rs\<rbrakk> \<Longrightarrow> ms = ms'
S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
length ms = length ms'
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
msx = targetnodes rs

goal (1 subgoal):
 1. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
note IH = \<open>\<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s');
    length ms = length ms'; valid_call_list cs' m;
    \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m;
    length rs = length cs'; msx = targetnodes rs\<rbrakk>
    \<Longrightarrow> ms = ms'\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>S,f \<turnstile> (?m # ?msx @ ms,?s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' ?m; \<forall>i<length ?rs. ?rs ! i \<in> get_return_edges (cs' ! i); valid_return_list ?rs ?m; length ?rs = length cs'; ?msx = targetnodes ?rs\<rbrakk> \<Longrightarrow> ms = ms'

goal (1 subgoal):
 1. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
[PROOF STEP]
obtain ms'' s''
    where "S,f \<turnstile> (m # msx @ ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'',s'')"
    and "S,f \<turnstile> (ms'',s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (1 subgoal):
 1. (\<And>ms'' s''. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'',s''); S,f \<turnstile> (ms'',s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto elim:silent_moves.cases)
[PROOF STATE]
proof (state)
this:
S,f \<turnstile> (m # msx @ ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'',s'')
S,f \<turnstile> (ms'',s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (1 subgoal):
 1. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>S,f \<turnstile> (m # msx @ ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'',s'')\<close> \<open>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (m # msx @ ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'',s'')
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'
[PROOF STEP]
have "valid_edge a" and "m = sourcenode a" and "hd (msx @ ms) = targetnode a"
    and "ms'' = msx @ ms" and "s'' \<noteq> []" and "length s = Suc(length s'')"
    and "length (m # msx @ ms) = length s"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (m # msx @ ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'',s'')
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'

goal (1 subgoal):
 1. (valid_edge a &&& m = sourcenode a &&& hd (msx @ ms) = targetnode a) &&& (ms'' = msx @ ms &&& s'' \<noteq> []) &&& length s = Suc (length s'') &&& length (m # msx @ ms) = length s
[PROOF STEP]
by(auto elim:silent_move.cases simp:intra_kind_def)
[PROOF STATE]
proof (state)
this:
valid_edge a
m = sourcenode a
hd (msx @ ms) = targetnode a
ms'' = msx @ ms
s'' \<noteq> []
length s = Suc (length s'')
length (m # msx @ ms) = length s

goal (1 subgoal):
 1. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>msx = targetnodes rs\<close> \<open>length rs = length cs\<close> \<open>cs = c' # cs'\<close>
[PROOF STATE]
proof (chain)
picking this:
msx = targetnodes rs
length rs = length cs
cs = c' # cs'
[PROOF STEP]
obtain mx' msx' where "msx = mx'#msx'"
[PROOF STATE]
proof (prove)
using this:
msx = targetnodes rs
length rs = length cs
cs = c' # cs'

goal (1 subgoal):
 1. (\<And>mx' msx'. msx = mx' # msx' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases msx)(fastforce simp:targetnodes_def)+
[PROOF STATE]
proof (state)
this:
msx = mx' # msx'

goal (1 subgoal):
 1. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
with \<open>hd (msx @ ms) = targetnode a\<close>
[PROOF STATE]
proof (chain)
picking this:
hd (msx @ ms) = targetnode a
msx = mx' # msx'
[PROOF STEP]
have "mx' = targetnode a"
[PROOF STATE]
proof (prove)
using this:
hd (msx @ ms) = targetnode a
msx = mx' # msx'

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

goal (1 subgoal):
 1. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>valid_call_list cs m\<close> \<open>cs = c' # cs'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_call_list cs m
cs = c' # cs'
[PROOF STEP]
have "valid_edge c'"
[PROOF STATE]
proof (prove)
using this:
valid_call_list cs m
cs = c' # cs'

goal (1 subgoal):
 1. valid_edge c'
[PROOF STEP]
by(fastforce simp:valid_call_list_def)
[PROOF STATE]
proof (state)
this:
valid_edge c'

goal (1 subgoal):
 1. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>valid_edge c'\<close> \<open>a \<in> get_return_edges c'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge c'
a \<in> get_return_edges c'
[PROOF STEP]
have "get_proc (sourcenode c') = get_proc (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_edge c'
a \<in> get_return_edges c'

goal (1 subgoal):
 1. get_proc (sourcenode c') = get_proc (targetnode a)
[PROOF STEP]
by(rule get_proc_get_return_edge)
[PROOF STATE]
proof (state)
this:
get_proc (sourcenode c') = get_proc (targetnode a)

goal (1 subgoal):
 1. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>valid_call_list cs m\<close> \<open>cs = c' # cs'\<close>
    \<open>get_proc (sourcenode c') = get_proc (targetnode a)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_call_list cs m
cs = c' # cs'
get_proc (sourcenode c') = get_proc (targetnode a)
[PROOF STEP]
have "valid_call_list cs' (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_call_list cs m
cs = c' # cs'
get_proc (sourcenode c') = get_proc (targetnode a)

goal (1 subgoal):
 1. valid_call_list cs' (targetnode a)
[PROOF STEP]
apply(clarsimp simp:valid_call_list_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs'a c cs''. \<lbrakk>\<forall>cs'aa ca. (\<exists>cs''a. c' # cs'a @ c # cs'' = cs'aa @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q r fs. kind ca = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs'aa of [] \<Rightarrow> m | a # list \<Rightarrow> last (sourcenodes cs'aa))\<^esub>fs); cs = c' # cs'a @ c # cs''; get_proc (sourcenode c') = get_proc (targetnode a); cs' = cs'a @ c # cs''\<rbrakk> \<Longrightarrow> valid_edge c \<and> (\<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs'a of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (sourcenodes cs'a))\<^esub>fs)
[PROOF STEP]
apply(hypsubst_thin)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs''. \<lbrakk>\<forall>cs'a ca. (\<exists>cs''a. c' # cs' @ c # cs'' = cs'a @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q r fs. kind ca = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs'a of [] \<Rightarrow> m | a # list \<Rightarrow> last (sourcenodes cs'a))\<^esub>fs); get_proc (sourcenode c') = get_proc (targetnode a)\<rbrakk> \<Longrightarrow> valid_edge c \<and> (\<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs)
[PROOF STEP]
apply(erule_tac x="c' # cs'" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs''. \<lbrakk>get_proc (sourcenode c') = get_proc (targetnode a); \<forall>ca. (\<exists>cs''a. c' # cs' @ c # cs'' = (c' # cs') @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q r fs. kind ca = Q:r\<hookrightarrow>\<^bsub>get_proc (case c' # cs' of [] \<Rightarrow> m | a # list \<Rightarrow> last (sourcenodes (c' # cs')))\<^esub>fs)\<rbrakk> \<Longrightarrow> valid_edge c \<and> (\<exists>Q r fs. kind c = Q:r\<hookrightarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode a | a # list \<Rightarrow> last (sourcenodes cs'))\<^esub>fs)
[PROOF STEP]
by(case_tac cs')(auto simp:sourcenodes_def)
[PROOF STATE]
proof (state)
this:
valid_call_list cs' (targetnode a)

goal (1 subgoal):
 1. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>length rs = length cs\<close> \<open>cs = c' # cs'\<close>
[PROOF STATE]
proof (chain)
picking this:
length rs = length cs
cs = c' # cs'
[PROOF STEP]
obtain r' rs'
    where [simp]:"rs = r'#rs'" and "length rs' = length cs'"
[PROOF STATE]
proof (prove)
using this:
length rs = length cs
cs = c' # cs'

goal (1 subgoal):
 1. (\<And>r' rs'. \<lbrakk>rs = r' # rs'; length rs' = length cs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases rs) auto
[PROOF STATE]
proof (state)
this:
rs = r' # rs'
length rs' = length cs'

goal (1 subgoal):
 1. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)\<close> \<open>cs = c' # cs'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
cs = c' # cs'
[PROOF STEP]
have "\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)"
    and "r' \<in> get_return_edges c'"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
cs = c' # cs'

goal (1 subgoal):
 1. \<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i) &&& r' \<in> get_return_edges c'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)
r' \<in> get_return_edges c'

goal (1 subgoal):
 1. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
with \<open>valid_edge c'\<close> \<open>a \<in> get_return_edges c'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge c'
a \<in> get_return_edges c'
\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)
r' \<in> get_return_edges c'
[PROOF STEP]
have [simp]:"a = r'"
[PROOF STATE]
proof (prove)
using this:
valid_edge c'
a \<in> get_return_edges c'
\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)
r' \<in> get_return_edges c'

goal (1 subgoal):
 1. a = r'
[PROOF STEP]
by -(rule get_return_edges_unique)
[PROOF STATE]
proof (state)
this:
a = r'

goal (1 subgoal):
 1. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
with \<open>valid_return_list rs m\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_return_list rs m
a = r'
[PROOF STEP]
have "valid_return_list rs' (targetnode a)"
[PROOF STATE]
proof (prove)
using this:
valid_return_list rs m
a = r'

goal (1 subgoal):
 1. valid_return_list rs' (targetnode a)
[PROOF STEP]
apply(clarsimp simp:valid_return_list_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs''. \<lbrakk>\<forall>cs'a ca. (\<exists>cs''a. r' # cs' @ c # cs'' = cs'a @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q f. kind ca = Q\<hookleftarrow>\<^bsub>get_proc (case cs'a of [] \<Rightarrow> m | a # list \<Rightarrow> last (targetnodes cs'a))\<^esub>f); rs' = cs' @ c # cs''\<rbrakk> \<Longrightarrow> valid_edge c \<and> (\<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode r' | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f)
[PROOF STEP]
apply(erule_tac x="r' # cs'" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>cs' c cs''. \<lbrakk>rs' = cs' @ c # cs''; \<forall>ca. (\<exists>cs''a. r' # cs' @ c # cs'' = (r' # cs') @ ca # cs''a) \<longrightarrow> valid_edge ca \<and> (\<exists>Q f. kind ca = Q\<hookleftarrow>\<^bsub>get_proc (case r' # cs' of [] \<Rightarrow> m | a # list \<Rightarrow> last (targetnodes (r' # cs')))\<^esub>f)\<rbrakk> \<Longrightarrow> valid_edge c \<and> (\<exists>Q f. kind c = Q\<hookleftarrow>\<^bsub>get_proc (case cs' of [] \<Rightarrow> targetnode r' | a # list \<Rightarrow> last (targetnodes cs'))\<^esub>f)
[PROOF STEP]
by(case_tac cs')(auto simp:targetnodes_def)
[PROOF STATE]
proof (state)
this:
valid_return_list rs' (targetnode a)

goal (1 subgoal):
 1. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>msx = targetnodes rs\<close> \<open>msx = mx'#msx'\<close> \<open>rs = r'#rs'\<close>
[PROOF STATE]
proof (chain)
picking this:
msx = targetnodes rs
msx = mx' # msx'
rs = r' # rs'
[PROOF STEP]
have "msx' = targetnodes rs'"
[PROOF STATE]
proof (prove)
using this:
msx = targetnodes rs
msx = mx' # msx'
rs = r' # rs'

goal (1 subgoal):
 1. msx' = targetnodes rs'
[PROOF STEP]
by(simp add:targetnodes_def)
[PROOF STATE]
proof (state)
this:
msx' = targetnodes rs'

goal (1 subgoal):
 1. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from \<open>S,f \<turnstile> (ms'',s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<close> \<open>msx = mx'#msx'\<close>
    \<open>ms'' = msx @ ms\<close> \<open>mx' = targetnode a\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (ms'',s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
msx = mx' # msx'
ms'' = msx @ ms
mx' = targetnode a
[PROOF STEP]
have "S,f \<turnstile> (targetnode a # msx' @ ms,s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (ms'',s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
msx = mx' # msx'
ms'' = msx @ ms
mx' = targetnode a

goal (1 subgoal):
 1. S,f \<turnstile> (targetnode a # msx' @ ms,s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
S,f \<turnstile> (targetnode a # msx' @ ms,s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (1 subgoal):
 1. \<And>cs a as Q p fa c' cs' m msx s rs. \<lbrakk>kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>fa; cs = c' # cs'; same_level_path_aux cs' as; a \<in> get_return_edges c'; \<And>m msx s rs. \<lbrakk>S,f \<turnstile> (m # msx @ ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs' m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs' ! i); valid_return_list rs m; length rs = length cs'; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'; S,f \<turnstile> (m # msx @ ms,s) =a # as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); length ms = length ms'; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; msx = targetnodes rs\<rbrakk> \<Longrightarrow> ms = ms'
[PROOF STEP]
from IH[OF this \<open>length ms = length ms'\<close> \<open>valid_call_list cs' (targetnode a)\<close>
    \<open>\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)\<close>
    \<open>valid_return_list rs' (targetnode a)\<close> \<open>length rs' = length cs'\<close>
    \<open>msx' = targetnodes rs'\<close>]
[PROOF STATE]
proof (chain)
picking this:
ms = ms'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ms = ms'

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

goal:
No subgoals!
[PROOF STEP]
qed