[STATEMENT]
lemma silent_moves_call_edge:
  assumes "S,kind \<turnstile> (m#ms,s) =as\<Rightarrow>\<^sub>\<tau> (m'#ms',s')" and "valid_node m"
  and callstack:"\<forall>mx \<in> set ms. \<exists>mx'. call_of_return_node mx mx' \<and>
      mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
  and rest:"\<forall>i < length rs. rs!i \<in> get_return_edges (cs!i)"
  "ms = targetnodes rs" "valid_return_list rs m" "length rs = length cs"
  obtains as' a as'' where "as = as'@a#as''" and "\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs"
  and "call_of_return_node (hd ms') (sourcenode a)"
  and "targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'"
  | "ms' = ms"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>as' a as''. \<lbrakk>as = as' @ a # as''; \<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; call_of_return_node (hd ms') (sourcenode a); targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m'\<rbrakk> \<Longrightarrow> thesis; ms' = ms \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
from \<open>S,kind \<turnstile> (m#ms,s) =as\<Rightarrow>\<^sub>\<tau> (m'#ms',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
[PROOF STEP]
show "(\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and>
    call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or>
    ms' = ms"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (1 subgoal):
 1. (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
proof(induct as arbitrary:m' ms' s' rule:length_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs m' ms' s'. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x xa xb. S,kind \<turnstile> (m # ms,s) =ys\<Rightarrow>\<^sub>\<tau> (x # xa,xb) \<longrightarrow> (\<exists>as' a as''. ys = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd xa) (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* x) \<or> xa = ms); S,kind \<turnstile> (m # ms,s) =xs\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<rbrakk> \<Longrightarrow> (\<exists>as' a as''. xs = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
fix as m' ms' s'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs m' ms' s'. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x xa xb. S,kind \<turnstile> (m # ms,s) =ys\<Rightarrow>\<^sub>\<tau> (x # xa,xb) \<longrightarrow> (\<exists>as' a as''. ys = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd xa) (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* x) \<or> xa = ms); S,kind \<turnstile> (m # ms,s) =xs\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<rbrakk> \<Longrightarrow> (\<exists>as' a as''. xs = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
assume IH:"\<forall>as'. length as' < length as \<longrightarrow>
      (\<forall>mx msx sx. S,kind \<turnstile> (m#ms,s) =as'\<Rightarrow>\<^sub>\<tau> (mx#msx,sx) \<longrightarrow>
      (\<exists>asx a asx'. as' = asx @ a # asx' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and>
      call_of_return_node (hd msx) (sourcenode a) \<and> targetnode a -asx'\<rightarrow>\<^bsub>sl\<^esub>* mx) \<or>
      msx = ms)"
      and "S,kind \<turnstile> (m#ms,s) =as\<Rightarrow>\<^sub>\<tau> (m'#ms',s')"
[PROOF STATE]
proof (state)
this:
\<forall>as'. length as' < length as \<longrightarrow> (\<forall>mx msx sx. S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (mx # msx,sx) \<longrightarrow> (\<exists>asx a asx'. as' = asx @ a # asx' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd msx) (sourcenode a) \<and> targetnode a -asx'\<rightarrow>\<^bsub>sl\<^esub>* mx) \<or> msx = ms)
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (1 subgoal):
 1. \<And>xs m' ms' s'. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x xa xb. S,kind \<turnstile> (m # ms,s) =ys\<Rightarrow>\<^sub>\<tau> (x # xa,xb) \<longrightarrow> (\<exists>as' a as''. ys = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd xa) (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* x) \<or> xa = ms); S,kind \<turnstile> (m # ms,s) =xs\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<rbrakk> \<Longrightarrow> (\<exists>as' a as''. xs = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
show "(\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and>
      call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or>
      ms' = ms"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
proof(cases as rule:rev_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. as = [] \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. \<And>ys y. as = ys @ [y] \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
as = []

goal (2 subgoals):
 1. as = [] \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. \<And>ys y. as = ys @ [y] \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with \<open>S,kind \<turnstile> (m#ms,s) =as\<Rightarrow>\<^sub>\<tau> (m'#ms',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
as = []
[PROOF STEP]
have "ms = ms'"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
as = []

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

goal (2 subgoals):
 1. as = [] \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. \<And>ys y. as = ys @ [y] \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ms = ms'

goal (1 subgoal):
 1. (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms

goal (1 subgoal):
 1. \<And>ys y. as = ys @ [y] \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ys y. as = ys @ [y] \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
case (snoc as' a')
[PROOF STATE]
proof (state)
this:
as = as' @ [a']

goal (1 subgoal):
 1. \<And>ys y. as = ys @ [y] \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with \<open>S,kind \<turnstile> (m#ms,s) =as\<Rightarrow>\<^sub>\<tau> (m'#ms',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
as = as' @ [a']
[PROOF STEP]
obtain ms'' s'' where "S,kind \<turnstile> (m#ms,s) =as'\<Rightarrow>\<^sub>\<tau> (ms'',s'')"
        and "S,kind \<turnstile> (ms'',s'') =[a']\<Rightarrow>\<^sub>\<tau> (m'#ms',s')"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
as = as' @ [a']

goal (1 subgoal):
 1. (\<And>ms'' s''. \<lbrakk>S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (ms'',s''); S,kind \<turnstile> (ms'',s'') =[a']\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:silent_moves_split)
[PROOF STATE]
proof (state)
this:
S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (ms'',s'')
S,kind \<turnstile> (ms'',s'') =[a']\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (1 subgoal):
 1. \<And>ys y. as = ys @ [y] \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
from snoc
[PROOF STATE]
proof (chain)
picking this:
as = as' @ [a']
[PROOF STEP]
have "length as' < length as"
[PROOF STATE]
proof (prove)
using this:
as = as' @ [a']

goal (1 subgoal):
 1. length as' < length as
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length as' < length as

goal (1 subgoal):
 1. \<And>ys y. as = ys @ [y] \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
from \<open>S,kind \<turnstile> (ms'',s'') =[a']\<Rightarrow>\<^sub>\<tau> (m'#ms',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (ms'',s'') =[a']\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
[PROOF STEP]
have "S,kind \<turnstile> (ms'',s'') -a'\<rightarrow>\<^sub>\<tau> (m'#ms',s')"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (ms'',s'') =[a']\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (1 subgoal):
 1. S,kind \<turnstile> (ms'',s'') -a'\<rightarrow>\<^sub>\<tau> (m' # ms',s')
[PROOF STEP]
by(fastforce elim:silent_moves.cases)
[PROOF STATE]
proof (state)
this:
S,kind \<turnstile> (ms'',s'') -a'\<rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (1 subgoal):
 1. \<And>ys y. as = ys @ [y] \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
proof(cases "kind a'" rule:edge_kind_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. intra_kind (kind a') \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 3. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
case Intra
[PROOF STATE]
proof (state)
this:
intra_kind (kind a')

goal (3 subgoals):
 1. intra_kind (kind a') \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 3. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with \<open>S,kind \<turnstile> (ms'',s'') -a'\<rightarrow>\<^sub>\<tau> (m'#ms',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (ms'',s'') -a'\<rightarrow>\<^sub>\<tau> (m' # ms',s')
intra_kind (kind a')
[PROOF STEP]
have "valid_edge a'" and "m' = targetnode a'"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (ms'',s'') -a'\<rightarrow>\<^sub>\<tau> (m' # ms',s')
intra_kind (kind a')

goal (1 subgoal):
 1. valid_edge a' &&& m' = targetnode a'
[PROOF STEP]
by(auto elim:silent_move.cases simp:intra_kind_def)
[PROOF STATE]
proof (state)
this:
valid_edge a'
m' = targetnode a'

goal (3 subgoals):
 1. intra_kind (kind a') \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 3. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
from \<open>S,kind \<turnstile> (ms'',s'') -a'\<rightarrow>\<^sub>\<tau> (m'#ms',s')\<close> \<open>intra_kind (kind a')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (ms'',s'') -a'\<rightarrow>\<^sub>\<tau> (m' # ms',s')
intra_kind (kind a')
[PROOF STEP]
have "ms'' = sourcenode a'#ms'"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (ms'',s'') -a'\<rightarrow>\<^sub>\<tau> (m' # ms',s')
intra_kind (kind a')

goal (1 subgoal):
 1. ms'' = sourcenode a' # ms'
[PROOF STEP]
by -(erule silent_move.cases,auto simp:intra_kind_def,(cases ms'',auto)+)
[PROOF STATE]
proof (state)
this:
ms'' = sourcenode a' # ms'

goal (3 subgoals):
 1. intra_kind (kind a') \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 3. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with IH \<open>length as' < length as\<close> \<open>S,kind \<turnstile> (m#ms,s) =as'\<Rightarrow>\<^sub>\<tau> (ms'',s'')\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>as'. length as' < length as \<longrightarrow> (\<forall>mx msx sx. S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (mx # msx,sx) \<longrightarrow> (\<exists>asx a asx'. as' = asx @ a # asx' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd msx) (sourcenode a) \<and> targetnode a -asx'\<rightarrow>\<^bsub>sl\<^esub>* mx) \<or> msx = ms)
length as' < length as
S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (ms'',s'')
ms'' = sourcenode a' # ms'
[PROOF STEP]
have "(\<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and>
          call_of_return_node (hd ms') (sourcenode ax) \<and>
          targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a') \<or> ms' = ms"
[PROOF STATE]
proof (prove)
using this:
\<forall>as'. length as' < length as \<longrightarrow> (\<forall>mx msx sx. S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (mx # msx,sx) \<longrightarrow> (\<exists>asx a asx'. as' = asx @ a # asx' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd msx) (sourcenode a) \<and> targetnode a -asx'\<rightarrow>\<^bsub>sl\<^esub>* mx) \<or> msx = ms)
length as' < length as
S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (ms'',s'')
ms'' = sourcenode a' # ms'

goal (1 subgoal):
 1. (\<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a') \<or> ms' = ms
[PROOF STEP]
by simp blast
[PROOF STATE]
proof (state)
this:
(\<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a') \<or> ms' = ms

goal (3 subgoals):
 1. intra_kind (kind a') \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 3. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a') \<or> ms' = ms

goal (1 subgoal):
 1. (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms' = ms \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
assume "\<exists>asx ax asx'. as' = asx @ ax # asx' \<and>
            (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and>
            call_of_return_node (hd ms') (sourcenode ax) \<and>
            targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'"
[PROOF STATE]
proof (state)
this:
\<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'

goal (2 subgoals):
 1. \<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms' = ms \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'
[PROOF STEP]
obtain asx ax asx' where "as' = asx @ ax # asx'"
            and "\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs"
            and "call_of_return_node (hd ms') (sourcenode ax)"
            and "targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'"
[PROOF STATE]
proof (prove)
using this:
\<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'

goal (1 subgoal):
 1. (\<And>asx ax asx'. \<lbrakk>as' = asx @ ax # asx'; \<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; call_of_return_node (hd ms') (sourcenode ax); targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
as' = asx @ ax # asx'
\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
call_of_return_node (hd ms') (sourcenode ax)
targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'

goal (2 subgoals):
 1. \<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms' = ms \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
from \<open>as' = asx @ ax # asx'\<close>
[PROOF STATE]
proof (chain)
picking this:
as' = asx @ ax # asx'
[PROOF STEP]
have "as'@[a'] = asx @ ax # (asx' @ [a'])"
[PROOF STATE]
proof (prove)
using this:
as' = asx @ ax # asx'

goal (1 subgoal):
 1. as' @ [a'] = asx @ ax # asx' @ [a']
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
as' @ [a'] = asx @ ax # asx' @ [a']

goal (2 subgoals):
 1. \<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms' = ms \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
as' @ [a'] = asx @ ax # asx' @ [a']

goal (2 subgoals):
 1. \<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms' = ms \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
from \<open>targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'\<close> \<open>intra_kind (kind a')\<close>
            \<open>m' = targetnode a'\<close> \<open>valid_edge a'\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'
intra_kind (kind a')
m' = targetnode a'
valid_edge a'
[PROOF STEP]
have "targetnode ax -asx'@[a']\<rightarrow>\<^bsub>sl\<^esub>* m'"
[PROOF STATE]
proof (prove)
using this:
targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'
intra_kind (kind a')
m' = targetnode a'
valid_edge a'

goal (1 subgoal):
 1. targetnode ax -asx' @ [a']\<rightarrow>\<^bsub>sl\<^esub>* m'
[PROOF STEP]
by(fastforce intro:path_Append path_edge same_level_path_aux_Append
              upd_cs_Append simp:slp_def same_level_path_def intra_kind_def)
[PROOF STATE]
proof (state)
this:
targetnode ax -asx' @ [a']\<rightarrow>\<^bsub>sl\<^esub>* m'

goal (2 subgoals):
 1. \<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms' = ms \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
as' @ [a'] = asx @ ax # asx' @ [a']
targetnode ax -asx' @ [a']\<rightarrow>\<^bsub>sl\<^esub>* m'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
as' @ [a'] = asx @ ax # asx' @ [a']
targetnode ax -asx' @ [a']\<rightarrow>\<^bsub>sl\<^esub>* m'

goal (1 subgoal):
 1. (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
using \<open>\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
            \<open>call_of_return_node (hd ms') (sourcenode ax)\<close> snoc
[PROOF STATE]
proof (prove)
using this:
as' @ [a'] = asx @ ax # asx' @ [a']
targetnode ax -asx' @ [a']\<rightarrow>\<^bsub>sl\<^esub>* m'
\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
call_of_return_node (hd ms') (sourcenode ax)
as = as' @ [a']

goal (1 subgoal):
 1. (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms

goal (1 subgoal):
 1. ms' = ms \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ms' = ms \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
assume "ms' = ms"
[PROOF STATE]
proof (state)
this:
ms' = ms

goal (1 subgoal):
 1. ms' = ms \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ms' = ms

goal (1 subgoal):
 1. (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
case (Call Q r p fs)
[PROOF STATE]
proof (state)
this:
kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with \<open>S,kind \<turnstile> (ms'',s'') -a'\<rightarrow>\<^sub>\<tau> (m'#ms',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (ms'',s'') -a'\<rightarrow>\<^sub>\<tau> (m' # ms',s')
kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
obtain a''
          where "valid_edge a'" and "a'' \<in> get_return_edges a'"
          and "hd ms'' = sourcenode a'" and "m' = targetnode a'"
          and "ms' = (targetnode a'')#tl ms''" and "length ms'' = length s''"
          and "pred (kind a') s''"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (ms'',s'') -a'\<rightarrow>\<^sub>\<tau> (m' # ms',s')
kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. (\<And>a''. \<lbrakk>valid_edge a'; a'' \<in> get_return_edges a'; hd ms'' = sourcenode a'; m' = targetnode a'; ms' = targetnode a'' # tl ms''; length ms'' = length s''; pred (kind a') s''\<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'
a'' \<in> get_return_edges a'
hd ms'' = sourcenode a'
m' = targetnode a'
ms' = targetnode a'' # tl ms''
length ms'' = length s''
pred (kind a') s''

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> 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>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
from \<open>valid_edge a''\<close> \<open>valid_edge a'\<close> \<open>a'' \<in> get_return_edges a'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a''
valid_edge a'
a'' \<in> get_return_edges a'
[PROOF STEP]
have "return_node (targetnode a'')"
[PROOF STATE]
proof (prove)
using this:
valid_edge a''
valid_edge a'
a'' \<in> get_return_edges a'

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

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with \<open>valid_edge a'\<close> \<open>valid_edge a''\<close>
          \<open>a'' \<in> get_return_edges a'\<close> \<open>ms' = (targetnode a'')#tl ms''\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
valid_edge a''
a'' \<in> get_return_edges a'
ms' = targetnode a'' # tl ms''
return_node (targetnode a'')
[PROOF STEP]
have "call_of_return_node (hd ms') (sourcenode a')"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
valid_edge a''
a'' \<in> get_return_edges a'
ms' = targetnode a'' # tl ms''
return_node (targetnode a'')

goal (1 subgoal):
 1. call_of_return_node (hd ms') (sourcenode a')
[PROOF STEP]
by(simp add:call_of_return_node_def) blast
[PROOF STATE]
proof (state)
this:
call_of_return_node (hd ms') (sourcenode a')

goal (2 subgoals):
 1. \<And>Q r p fs. kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with snoc \<open>kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>m' = targetnode a'\<close> \<open>valid_edge a'\<close>
[PROOF STATE]
proof (chain)
picking this:
as = as' @ [a']
kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
m' = targetnode a'
valid_edge a'
call_of_return_node (hd ms') (sourcenode a')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
as = as' @ [a']
kind a' = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
m' = targetnode a'
valid_edge a'
call_of_return_node (hd ms') (sourcenode a')

goal (1 subgoal):
 1. (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
by(fastforce intro:empty_path simp:slp_def same_level_path_def)
[PROOF STATE]
proof (state)
this:
(\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms

goal (1 subgoal):
 1. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
case (Return Q p f)
[PROOF STATE]
proof (state)
this:
kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f

goal (1 subgoal):
 1. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with \<open>S,kind \<turnstile> (ms'',s'') -a'\<rightarrow>\<^sub>\<tau> (m'#ms',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (ms'',s'') -a'\<rightarrow>\<^sub>\<tau> (m' # ms',s')
kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f
[PROOF STEP]
have "valid_edge a'" and "hd ms'' = sourcenode a'"
          and "hd(tl ms'') = targetnode a'" and "m'#ms' = tl ms''"
          and "length ms'' = length s''" and "length s'' = Suc(length s')"
          and "s' \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (ms'',s'') -a'\<rightarrow>\<^sub>\<tau> (m' # ms',s')
kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f

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

goal (1 subgoal):
 1. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
hence "ms'' = sourcenode a' # targetnode a' # ms'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
hd ms'' = sourcenode a'
hd (tl ms'') = targetnode a'
m' # ms' = tl ms''
length ms'' = length s''
length s'' = Suc (length s')
s' \<noteq> []

goal (1 subgoal):
 1. ms'' = sourcenode a' # targetnode a' # ms'
[PROOF STEP]
by(cases ms'') auto
[PROOF STATE]
proof (state)
this:
ms'' = sourcenode a' # targetnode a' # ms'

goal (1 subgoal):
 1. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with \<open>length as' < length as\<close> \<open>S,kind \<turnstile> (m#ms,s) =as'\<Rightarrow>\<^sub>\<tau> (ms'',s'')\<close> IH
[PROOF STATE]
proof (chain)
picking this:
length as' < length as
S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (ms'',s'')
\<forall>as'. length as' < length as \<longrightarrow> (\<forall>mx msx sx. S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (mx # msx,sx) \<longrightarrow> (\<exists>asx a asx'. as' = asx @ a # asx' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd msx) (sourcenode a) \<and> targetnode a -asx'\<rightarrow>\<^bsub>sl\<^esub>* mx) \<or> msx = ms)
ms'' = sourcenode a' # targetnode a' # ms'
[PROOF STEP]
have "(\<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and>
          call_of_return_node (targetnode a') (sourcenode ax) \<and>
          targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a') \<or> ms = targetnode a' # ms'"
[PROOF STATE]
proof (prove)
using this:
length as' < length as
S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (ms'',s'')
\<forall>as'. length as' < length as \<longrightarrow> (\<forall>mx msx sx. S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (mx # msx,sx) \<longrightarrow> (\<exists>asx a asx'. as' = asx @ a # asx' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd msx) (sourcenode a) \<and> targetnode a -asx'\<rightarrow>\<^bsub>sl\<^esub>* mx) \<or> msx = ms)
ms'' = sourcenode a' # targetnode a' # ms'

goal (1 subgoal):
 1. (\<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a') \<or> ms = targetnode a' # ms'
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length as' < length as; S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (ms'',s''); \<forall>as'. length as' < length as \<longrightarrow> (\<forall>mx msx sx. S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (mx # msx,sx) \<longrightarrow> (\<exists>asx a asx'. as' = asx @ a # asx' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd msx) (sourcenode a) \<and> targetnode a -asx'\<rightarrow>\<^bsub>sl\<^esub>* mx) \<or> msx = ms); ms'' = sourcenode a' # targetnode a' # ms'\<rbrakk> \<Longrightarrow> (\<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a') \<or> ms = targetnode a' # ms'
[PROOF STEP]
apply(erule_tac x="as'" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length as' < length as; S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (ms'',s''); ms'' = sourcenode a' # targetnode a' # ms'; length as' < length as \<longrightarrow> (\<forall>mx msx sx. S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (mx # msx,sx) \<longrightarrow> (\<exists>asx a asx'. as' = asx @ a # asx' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd msx) (sourcenode a) \<and> targetnode a -asx'\<rightarrow>\<^bsub>sl\<^esub>* mx) \<or> msx = ms)\<rbrakk> \<Longrightarrow> (\<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a') \<or> ms = targetnode a' # ms'
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length as' < length as; S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (sourcenode a' # targetnode a' # ms',s''); ms'' = sourcenode a' # targetnode a' # ms'; \<forall>mx msx. Ex (silent_moves S kind (m # ms) s as' (mx # msx)) \<longrightarrow> (\<exists>asx a asx'. as' = asx @ a # asx' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd msx) (sourcenode a) \<and> targetnode a -asx'\<rightarrow>\<^bsub>sl\<^esub>* mx) \<or> msx = ms; ms \<noteq> targetnode a' # ms'\<rbrakk> \<Longrightarrow> \<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'
[PROOF STEP]
apply(erule_tac x="sourcenode a'" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length as' < length as; S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (sourcenode a' # targetnode a' # ms',s''); ms'' = sourcenode a' # targetnode a' # ms'; ms \<noteq> targetnode a' # ms'; \<forall>msx. Ex (silent_moves S kind (m # ms) s as' (sourcenode a' # msx)) \<longrightarrow> (\<exists>asx a asx'. as' = asx @ a # asx' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd msx) (sourcenode a) \<and> targetnode a -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a') \<or> msx = ms\<rbrakk> \<Longrightarrow> \<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'
[PROOF STEP]
apply(erule_tac x="targetnode a' # ms'" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length as' < length as; S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (sourcenode a' # targetnode a' # ms',s''); ms'' = sourcenode a' # targetnode a' # ms'; ms \<noteq> targetnode a' # ms'; Ex (silent_moves S kind (m # ms) s as' (sourcenode a' # targetnode a' # ms')) \<longrightarrow> (\<exists>asx a asx'. as' = asx @ a # asx' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd (targetnode a' # ms')) (sourcenode a) \<and> targetnode a -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a') \<or> targetnode a' # ms' = ms\<rbrakk> \<Longrightarrow> \<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(\<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a') \<or> ms = targetnode a' # ms'

goal (1 subgoal):
 1. \<And>Q p f. kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a') \<or> ms = targetnode a' # ms'

goal (1 subgoal):
 1. (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = targetnode a' # ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
assume "\<exists>asx ax asx'. as' = asx @ ax # asx' \<and>
            (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and>
            call_of_return_node (targetnode a') (sourcenode ax) \<and>
            targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'"
[PROOF STATE]
proof (state)
this:
\<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'

goal (2 subgoals):
 1. \<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = targetnode a' # ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'
[PROOF STEP]
obtain asx ax asx' where "as' = asx @ ax # asx'"
            and "\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs"
            and "call_of_return_node (targetnode a') (sourcenode ax)"
            and "targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'"
[PROOF STATE]
proof (prove)
using this:
\<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'

goal (1 subgoal):
 1. (\<And>asx ax asx'. \<lbrakk>as' = asx @ ax # asx'; \<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; call_of_return_node (targetnode a') (sourcenode ax); targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
as' = asx @ ax # asx'
\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
call_of_return_node (targetnode a') (sourcenode ax)
targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'

goal (2 subgoals):
 1. \<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = targetnode a' # ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
from \<open>as' = asx @ ax # asx'\<close> snoc
[PROOF STATE]
proof (chain)
picking this:
as' = asx @ ax # asx'
as = as' @ [a']
[PROOF STEP]
have"length asx < length as"
[PROOF STATE]
proof (prove)
using this:
as' = asx @ ax # asx'
as = as' @ [a']

goal (1 subgoal):
 1. length asx < length as
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length asx < length as

goal (2 subgoals):
 1. \<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = targetnode a' # ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length asx < length as

goal (2 subgoals):
 1. \<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = targetnode a' # ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
from \<open>S,kind \<turnstile> (m#ms,s) =as\<Rightarrow>\<^sub>\<tau> (m'#ms',s')\<close> snoc \<open>as' = asx @ ax # asx'\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
as = as' @ [a']
as' = asx @ ax # asx'
[PROOF STEP]
obtain msx sx where "S,kind \<turnstile> (m#ms,s) =asx\<Rightarrow>\<^sub>\<tau> (msx,sx)"
            and "S,kind \<turnstile> (msx,sx) =ax#asx'@[a']\<Rightarrow>\<^sub>\<tau> (m'#ms',s')"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
as = as' @ [a']
as' = asx @ ax # asx'

goal (1 subgoal):
 1. (\<And>msx sx. \<lbrakk>S,kind \<turnstile> (m # ms,s) =asx\<Rightarrow>\<^sub>\<tau> (msx,sx); S,kind \<turnstile> (msx,sx) =ax # asx' @ [a']\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:silent_moves_split)
[PROOF STATE]
proof (state)
this:
S,kind \<turnstile> (m # ms,s) =asx\<Rightarrow>\<^sub>\<tau> (msx,sx)
S,kind \<turnstile> (msx,sx) =ax # asx' @ [a']\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (2 subgoals):
 1. \<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = targetnode a' # ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
from \<open>S,kind \<turnstile> (msx,sx) =ax#asx'@[a']\<Rightarrow>\<^sub>\<tau> (m'#ms',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (msx,sx) =ax # asx' @ [a']\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
[PROOF STEP]
obtain xs x ys y where "S,kind \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (xs,x)"
            and "S,kind \<turnstile> (xs,x) =asx'\<Rightarrow>\<^sub>\<tau> (ys,y)"
            and "S,kind \<turnstile> (ys,y) =[a']\<Rightarrow>\<^sub>\<tau> (m'#ms',s')"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (msx,sx) =ax # asx' @ [a']\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (1 subgoal):
 1. (\<And>xs x ys y. \<lbrakk>S,kind \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (xs,x); S,kind \<turnstile> (xs,x) =asx'\<Rightarrow>\<^sub>\<tau> (ys,y); S,kind \<turnstile> (ys,y) =[a']\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>xs x ys y. \<lbrakk>S,kind \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (xs,x); S,kind \<turnstile> (xs,x) =asx'\<Rightarrow>\<^sub>\<tau> (ys,y); S,kind \<turnstile> (ys,y) =[a']\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<rbrakk> \<Longrightarrow> thesis; S,kind \<turnstile> (msx,sx) =ax # asx' @ [a']\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(erule silent_moves.cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ms s Sa f. \<lbrakk>\<And>xs x ys y. \<lbrakk>S,kind \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (xs,x); S,kind \<turnstile> (xs,x) =asx'\<Rightarrow>\<^sub>\<tau> (ys,y); S,kind \<turnstile> (ys,y) =[a']\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<rbrakk> \<Longrightarrow> thesis; S = Sa; kind = f; msx = ms; sx = s; ax # asx' @ [a'] = []; m' # ms' = ms; s' = s; length ms = length s\<rbrakk> \<Longrightarrow> thesis
 2. \<And>Sa f ms s a ms' s' as ms'' s''. \<lbrakk>\<And>xs x ys y. \<lbrakk>S,kind \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (xs,x); S,kind \<turnstile> (xs,x) =asx'\<Rightarrow>\<^sub>\<tau> (ys,y); S,kind \<turnstile> (ys,y) =[a']\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<rbrakk> \<Longrightarrow> thesis; S = Sa; kind = f; msx = ms; sx = s; ax # asx' @ [a'] = a # as; m' # ms' = ms''; s' = s''; Sa,f \<turnstile> (ms,s) -a\<rightarrow>\<^sub>\<tau> (ms',s'); Sa,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s'')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ms' s'. \<lbrakk>\<And>xs x ys y. \<lbrakk>S,kind \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (xs,x); S,kind \<turnstile> (xs,x) =asx'\<Rightarrow>\<^sub>\<tau> (ys,y); S,kind \<turnstile> (ys,y) =[a']\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<rbrakk> \<Longrightarrow> thesis; S,kind \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (ms',s'); S,kind \<turnstile> (ms',s') =asx' @ [a']\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by(erule silent_moves_split) auto
[PROOF STATE]
proof (state)
this:
S,kind \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (xs,x)
S,kind \<turnstile> (xs,x) =asx'\<Rightarrow>\<^sub>\<tau> (ys,y)
S,kind \<turnstile> (ys,y) =[a']\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (2 subgoals):
 1. \<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = targetnode a' # ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
from \<open>S,kind \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (xs,x)\<close> \<open>\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (xs,x)
\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
[PROOF STEP]
obtain msx' ax' where "msx = sourcenode ax#msx'"
            and "ax' \<in> get_return_edges ax"
            and [simp]:"xs = (targetnode ax)#(targetnode ax')#msx'"
            and "length x = Suc(length sx)" and "length msx = length sx"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (xs,x)
\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs

goal (1 subgoal):
 1. (\<And>msx' ax'. \<lbrakk>msx = sourcenode ax # msx'; ax' \<in> get_return_edges ax; xs = targetnode ax # targetnode ax' # msx'; length x = Suc (length sx); length msx = length sx\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>msx' ax'. \<lbrakk>msx = sourcenode ax # msx'; ax' \<in> get_return_edges ax; xs = targetnode ax # targetnode ax' # msx'; length x = Suc (length sx); length msx = length sx\<rbrakk> \<Longrightarrow> thesis; S,kind \<turnstile> (msx,sx) -ax\<rightarrow>\<^sub>\<tau> (xs,x); \<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(erule silent_move.cases)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>f a s s' ms Sa ms'. \<lbrakk>\<And>msx' ax'. \<lbrakk>msx = sourcenode ax # msx'; ax' \<in> get_return_edges ax; xs = targetnode ax # targetnode ax' # msx'; length x = Suc (length sx); length msx = length sx\<rbrakk> \<Longrightarrow> thesis; \<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; S = Sa; kind = f; msx = ms; sx = s; ax = a; xs = ms'; x = s'; pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind (kind a); (\<exists>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice Sa\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice Sa\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length s' = length s; length ms = length s; hd ms = sourcenode a; ms' = targetnode a # tl ms\<rbrakk> \<Longrightarrow> thesis
 2. \<And>f a s s' Q r p fs a' ms Sa ms'. \<lbrakk>\<And>msx' ax'. \<lbrakk>msx = sourcenode ax # msx'; ax' \<in> get_return_edges ax; xs = targetnode ax # targetnode ax' # msx'; length x = Suc (length sx); length msx = length sx\<rbrakk> \<Longrightarrow> thesis; \<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; S = Sa; kind = f; msx = ms; sx = s; ax = a; xs = ms'; x = s'; pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; (\<exists>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice Sa\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice Sa\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms\<rbrakk> \<Longrightarrow> thesis
 3. \<And>f a s s' Q p f' ms Sa ms'. \<lbrakk>\<And>msx' ax'. \<lbrakk>msx = sourcenode ax # msx'; ax' \<in> get_return_edges ax; xs = targetnode ax # targetnode ax' # msx'; length x = Suc (length sx); length msx = length sx\<rbrakk> \<Longrightarrow> thesis; \<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; S = Sa; kind = f; msx = ms; sx = s; ax = a; xs = ms'; x = s'; pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice Sa\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(auto simp:intra_kind_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Q r p fs a' m m'. \<lbrakk>\<And>msx' ax'. \<lbrakk>msx = sourcenode ax # msx'; ax' \<in> get_return_edges ax; targetnode a' = targetnode ax'; Suc (length msx') = length sx\<rbrakk> \<Longrightarrow> thesis; xs = targetnode ax # targetnode a' # tl msx; pred (Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) sx; valid_edge ax; kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges ax; Ball (set (tl msx)) return_node; length msx = length sx; length (transfer (Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) sx) = Suc (length sx); hd msx = sourcenode ax; x = transfer (Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) sx; m \<in> set (tl msx); call_of_return_node m m'; m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> thesis
 2. \<And>Q r p fs a'. \<lbrakk>\<And>msx' ax'. \<lbrakk>msx = sourcenode ax # msx'; ax' \<in> get_return_edges ax; targetnode a' = targetnode ax'; Suc (length msx') = length sx\<rbrakk> \<Longrightarrow> thesis; xs = targetnode ax # targetnode a' # tl msx; pred (Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) sx; valid_edge ax; kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges ax; Ball (set (tl msx)) return_node; length msx = length sx; length (transfer (Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) sx) = Suc (length sx); hd msx = sourcenode ax; x = transfer (Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) sx; sourcenode ax \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by(cases msx,auto)+
[PROOF STATE]
proof (state)
this:
msx = sourcenode ax # msx'
ax' \<in> get_return_edges ax
xs = targetnode ax # targetnode ax' # msx'
length x = Suc (length sx)
length msx = length sx

goal (2 subgoals):
 1. \<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = targetnode a' # ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
from \<open>S,kind \<turnstile> (ys,y) =[a']\<Rightarrow>\<^sub>\<tau> (m'#ms',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (ys,y) =[a']\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
[PROOF STEP]
obtain msy
            where "ys = sourcenode a'#msy"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (ys,y) =[a']\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (1 subgoal):
 1. (\<And>msy. ys = sourcenode a' # msy \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>msy. ys = sourcenode a' # msy \<Longrightarrow> thesis; S,kind \<turnstile> (ys,y) =[a']\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(erule silent_moves.cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ms s Sa f. \<lbrakk>\<And>msy. ys = sourcenode a' # msy \<Longrightarrow> thesis; S = Sa; kind = f; ys = ms; y = s; [a'] = []; m' # ms' = ms; s' = s; length ms = length s\<rbrakk> \<Longrightarrow> thesis
 2. \<And>Sa f ms s a ms' s' as ms'' s''. \<lbrakk>\<And>msy. ys = sourcenode a' # msy \<Longrightarrow> thesis; S = Sa; kind = f; ys = ms; y = s; [a'] = a # as; m' # ms' = ms''; s' = s''; Sa,f \<turnstile> (ms,s) -a\<rightarrow>\<^sub>\<tau> (ms',s'); Sa,f \<turnstile> (ms',s') =as\<Rightarrow>\<^sub>\<tau> (ms'',s'')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ms' s'. \<lbrakk>\<And>msy. ys = sourcenode a' # msy \<Longrightarrow> thesis; S,kind \<turnstile> (ys,y) -a'\<rightarrow>\<^sub>\<tau> (ms',s'); S,kind \<turnstile> (ms',s') =[]\<Rightarrow>\<^sub>\<tau> (m' # ms',s')\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply(erule silent_move.cases)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ms' s' f a s s'aa ms Sa ms'aa. \<lbrakk>\<And>msy. ys = sourcenode a' # msy \<Longrightarrow> thesis; S,kind \<turnstile> (ms',s') =[]\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); S = Sa; kind = f; ys = ms; y = s; a' = a; ms' = ms'aa; s' = s'aa; pred (f a) s; transfer (f a) s = s'aa; valid_edge a; intra_kind (kind a); (\<exists>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice Sa\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice Sa\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length s'aa = length s; length ms = length s; hd ms = sourcenode a; ms'aa = targetnode a # tl ms\<rbrakk> \<Longrightarrow> thesis
 2. \<And>ms' s' f a s s'aa Q r p fs a'a ms Sa ms'aa. \<lbrakk>\<And>msy. ys = sourcenode a' # msy \<Longrightarrow> thesis; S,kind \<turnstile> (ms',s') =[]\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); S = Sa; kind = f; ys = ms; y = s; a' = a; ms' = ms'aa; s' = s'aa; pred (f a) s; transfer (f a) s = s'aa; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'a; a'a \<in> get_return_edges a; (\<exists>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice Sa\<rfloor>\<^bsub>CFG\<^esub>) \<or> hd ms \<notin> \<lfloor>HRB_slice Sa\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s'aa = Suc (length s); hd ms = sourcenode a; ms'aa = targetnode a # targetnode a'a # tl ms\<rbrakk> \<Longrightarrow> thesis
 3. \<And>ms' s' f a s s'aa Q p f' ms Sa ms'aa. \<lbrakk>\<And>msy. ys = sourcenode a' # msy \<Longrightarrow> thesis; S,kind \<turnstile> (ms',s') =[]\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); S = Sa; kind = f; ys = ms; y = s; a' = a; ms' = ms'aa; s' = s'aa; pred (f a) s; transfer (f a) s = s'aa; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<exists>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice Sa\<rfloor>\<^bsub>CFG\<^esub>; Ball (set (tl ms)) return_node; length ms = length s; length s = Suc (length s'aa); s'aa \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms'aa = tl ms\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by(cases ys,auto)+
[PROOF STATE]
proof (state)
this:
ys = sourcenode a' # msy

goal (2 subgoals):
 1. \<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = targetnode a' # ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with \<open>S,kind \<turnstile> (xs,x) =asx'\<Rightarrow>\<^sub>\<tau> (ys,y)\<close>
            \<open>targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'\<close>
            \<open>xs = (targetnode ax)#(targetnode ax')#msx'\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (xs,x) =asx'\<Rightarrow>\<^sub>\<tau> (ys,y)
targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'
xs = targetnode ax # targetnode ax' # msx'
ys = sourcenode a' # msy
[PROOF STEP]
have "(targetnode ax')#msx' = msy"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (xs,x) =asx'\<Rightarrow>\<^sub>\<tau> (ys,y)
targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'
xs = targetnode ax # targetnode ax' # msx'
ys = sourcenode a' # msy

goal (1 subgoal):
 1. targetnode ax' # msx' = msy
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S,kind \<turnstile> (targetnode ax # targetnode ax' # msx',x) =asx'\<Rightarrow>\<^sub>\<tau> (sourcenode a' # msy,y); targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'; ys = sourcenode a' # msy\<rbrakk> \<Longrightarrow> targetnode ax' # msx' = msy
[PROOF STEP]
by(fastforce intro:silent_moves_same_level_path)
[PROOF STATE]
proof (state)
this:
targetnode ax' # msx' = msy

goal (2 subgoals):
 1. \<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = targetnode a' # ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with \<open>S,kind \<turnstile> (ys,y) =[a']\<Rightarrow>\<^sub>\<tau> (m'#ms',s')\<close> \<open>kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<close>
            \<open>ys = sourcenode a'#msy\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (ys,y) =[a']\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f
ys = sourcenode a' # msy
targetnode ax' # msx' = msy
[PROOF STEP]
have "m' = targetnode a'" and "msx' = ms'"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (ys,y) =[a']\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f
ys = sourcenode a' # msy
targetnode ax' # msx' = msy

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

goal (2 subgoals):
 1. \<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = targetnode a' # ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with \<open>S,kind \<turnstile> (m#ms,s) =asx\<Rightarrow>\<^sub>\<tau> (msx,sx)\<close> \<open>msx = sourcenode ax#msx'\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (m # ms,s) =asx\<Rightarrow>\<^sub>\<tau> (msx,sx)
msx = sourcenode ax # msx'
m' = targetnode a'
msx' = ms'
[PROOF STEP]
have "S,kind \<turnstile> (m#ms,s) =asx\<Rightarrow>\<^sub>\<tau> (sourcenode ax#ms',sx)"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (m # ms,s) =asx\<Rightarrow>\<^sub>\<tau> (msx,sx)
msx = sourcenode ax # msx'
m' = targetnode a'
msx' = ms'

goal (1 subgoal):
 1. S,kind \<turnstile> (m # ms,s) =asx\<Rightarrow>\<^sub>\<tau> (sourcenode ax # ms',sx)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
S,kind \<turnstile> (m # ms,s) =asx\<Rightarrow>\<^sub>\<tau> (sourcenode ax # ms',sx)

goal (2 subgoals):
 1. \<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = targetnode a' # ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length asx < length as
S,kind \<turnstile> (m # ms,s) =asx\<Rightarrow>\<^sub>\<tau> (sourcenode ax # ms',sx)
[PROOF STEP]
have "(\<exists>xs x xs'. asx = xs@x#xs' \<and>
            (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and>
            call_of_return_node (hd ms') (sourcenode x) \<and>
            targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax) \<or> ms = ms'"
[PROOF STATE]
proof (prove)
using this:
length asx < length as
S,kind \<turnstile> (m # ms,s) =asx\<Rightarrow>\<^sub>\<tau> (sourcenode ax # ms',sx)

goal (1 subgoal):
 1. (\<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax) \<or> ms = ms'
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
length asx < length as
S,kind \<turnstile> (m # ms,s) =asx\<Rightarrow>\<^sub>\<tau> (sourcenode ax # ms',sx)
\<forall>as'. length as' < length as \<longrightarrow> (\<forall>mx msx sx. S,kind \<turnstile> (m # ms,s) =as'\<Rightarrow>\<^sub>\<tau> (mx # msx,sx) \<longrightarrow> (\<exists>asx a asx'. as' = asx @ a # asx' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd msx) (sourcenode a) \<and> targetnode a -asx'\<rightarrow>\<^bsub>sl\<^esub>* mx) \<or> msx = ms)

goal (1 subgoal):
 1. (\<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax) \<or> ms = ms'
[PROOF STEP]
by simp blast
[PROOF STATE]
proof (state)
this:
(\<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax) \<or> ms = ms'

goal (2 subgoals):
 1. \<exists>asx ax asx'. as' = asx @ ax # asx' \<and> (\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (targetnode a') (sourcenode ax) \<and> targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = targetnode a' # ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax) \<or> ms = ms'

goal (1 subgoal):
 1. (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
assume "\<exists>xs x xs'. asx = xs@x#xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and>
              call_of_return_node (hd ms') (sourcenode x) \<and>
              targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax"
[PROOF STATE]
proof (state)
this:
\<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax
[PROOF STEP]
obtain xs x xs' where "asx = xs@x#xs'"
              and "\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs"
              and "call_of_return_node (hd ms') (sourcenode x)"
              and "targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax"
[PROOF STATE]
proof (prove)
using this:
\<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax

goal (1 subgoal):
 1. (\<And>xs x xs'. \<lbrakk>asx = xs @ x # xs'; \<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; call_of_return_node (hd ms') (sourcenode x); targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
asx = xs @ x # xs'
\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
call_of_return_node (hd ms') (sourcenode x)
targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
from \<open>asx = xs@x#xs'\<close> \<open>as' = asx @ ax # asx'\<close> snoc
[PROOF STATE]
proof (chain)
picking this:
asx = xs @ x # xs'
as' = asx @ ax # asx'
as = as' @ [a']
[PROOF STEP]
have "as = xs@x#(xs'@ax#asx'@[a'])"
[PROOF STATE]
proof (prove)
using this:
asx = xs @ x # xs'
as' = asx @ ax # asx'
as = as' @ [a']

goal (1 subgoal):
 1. as = xs @ x # xs' @ ax # asx' @ [a']
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
as = xs @ x # xs' @ ax # asx' @ [a']

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
from \<open>S,kind \<turnstile> (m#ms,s) =as\<Rightarrow>\<^sub>\<tau> (m'#ms',s')\<close> \<open>valid_node m\<close> rest
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
valid_node m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
ms = targetnodes rs
valid_return_list rs m
length rs = length cs
[PROOF STEP]
have "m -as\<rightarrow>* m'" and "valid_path_aux cs as"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
valid_node m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
ms = targetnodes rs
valid_return_list rs m
length rs = length cs

goal (1 subgoal):
 1. m -as\<rightarrow>* m' &&& valid_path_aux cs as
[PROOF STEP]
by(auto dest:silent_moves_vpa_path[of _ _ _ _ _ _ _ _ _ rs cs]
                      simp:valid_call_list_def valid_return_list_def targetnodes_def)
[PROOF STATE]
proof (state)
this:
m -as\<rightarrow>* m'
valid_path_aux cs as

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
hence "m -as\<rightarrow>\<^sub>\<surd>* m'"
[PROOF STATE]
proof (prove)
using this:
m -as\<rightarrow>* m'
valid_path_aux cs as

goal (1 subgoal):
 1. m -as\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
by(fastforce intro:valid_path_aux_valid_path simp:vp_def)
[PROOF STATE]
proof (state)
this:
m -as\<rightarrow>\<^sub>\<surd>* m'

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with snoc
[PROOF STATE]
proof (chain)
picking this:
as = as' @ [a']
m -as\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
have "m -as'\<rightarrow>\<^sub>\<surd>* sourcenode a'"
[PROOF STATE]
proof (prove)
using this:
as = as' @ [a']
m -as\<rightarrow>\<^sub>\<surd>* m'

goal (1 subgoal):
 1. m -as'\<rightarrow>\<^sub>\<surd>* sourcenode a'
[PROOF STEP]
by(auto elim:path_split_snoc dest:valid_path_aux_split
                simp:vp_def valid_path_def)
[PROOF STATE]
proof (state)
this:
m -as'\<rightarrow>\<^sub>\<surd>* sourcenode a'

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with \<open>as' = asx @ ax # asx'\<close>
[PROOF STATE]
proof (chain)
picking this:
as' = asx @ ax # asx'
m -as'\<rightarrow>\<^sub>\<surd>* sourcenode a'
[PROOF STEP]
have "valid_edge ax" and "targetnode ax -asx'\<rightarrow>* sourcenode a'"
[PROOF STATE]
proof (prove)
using this:
as' = asx @ ax # asx'
m -as'\<rightarrow>\<^sub>\<surd>* sourcenode a'

goal (1 subgoal):
 1. valid_edge ax &&& targetnode ax -asx'\<rightarrow>* sourcenode a'
[PROOF STEP]
by(auto dest:path_split simp:vp_def)
[PROOF STATE]
proof (state)
this:
valid_edge ax
targetnode ax -asx'\<rightarrow>* sourcenode a'

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
hence "sourcenode ax -ax#asx'\<rightarrow>* sourcenode a'"
[PROOF STATE]
proof (prove)
using this:
valid_edge ax
targetnode ax -asx'\<rightarrow>* sourcenode a'

goal (1 subgoal):
 1. sourcenode ax -ax # asx'\<rightarrow>* sourcenode a'
[PROOF STEP]
by(fastforce intro:Cons_path)
[PROOF STATE]
proof (state)
this:
sourcenode ax -ax # asx'\<rightarrow>* sourcenode a'

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
from \<open>valid_edge a'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
[PROOF STEP]
have "sourcenode a' -[a']\<rightarrow>* targetnode a'"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'

goal (1 subgoal):
 1. sourcenode a' -[a']\<rightarrow>* targetnode a'
[PROOF STEP]
by(rule path_edge)
[PROOF STATE]
proof (state)
this:
sourcenode a' -[a']\<rightarrow>* targetnode a'

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with \<open>sourcenode ax -ax#asx'\<rightarrow>* sourcenode a'\<close>
[PROOF STATE]
proof (chain)
picking this:
sourcenode ax -ax # asx'\<rightarrow>* sourcenode a'
sourcenode a' -[a']\<rightarrow>* targetnode a'
[PROOF STEP]
have "sourcenode ax -(ax#asx')@[a']\<rightarrow>* targetnode a'"
[PROOF STATE]
proof (prove)
using this:
sourcenode ax -ax # asx'\<rightarrow>* sourcenode a'
sourcenode a' -[a']\<rightarrow>* targetnode a'

goal (1 subgoal):
 1. sourcenode ax -(ax # asx') @ [a']\<rightarrow>* targetnode a'
[PROOF STEP]
by(rule path_Append)
[PROOF STATE]
proof (state)
this:
sourcenode ax -(ax # asx') @ [a']\<rightarrow>* targetnode a'

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
from \<open>m -as\<rightarrow>\<^sub>\<surd>* m'\<close> snoc \<open>as' = asx @ ax # asx'\<close> snoc
[PROOF STATE]
proof (chain)
picking this:
m -as\<rightarrow>\<^sub>\<surd>* m'
as = as' @ [a']
as' = asx @ ax # asx'
as = as' @ [a']
[PROOF STEP]
have "valid_path_aux ([]@(upd_cs [] asx)) (ax # asx' @ [a'])"
[PROOF STATE]
proof (prove)
using this:
m -as\<rightarrow>\<^sub>\<surd>* m'
as = as' @ [a']
as' = asx @ ax # asx'
as = as' @ [a']

goal (1 subgoal):
 1. valid_path_aux ([] @ upd_cs [] asx) (ax # asx' @ [a'])
[PROOF STEP]
by(fastforce dest:valid_path_aux_split simp:vp_def valid_path_def)
[PROOF STATE]
proof (state)
this:
valid_path_aux ([] @ upd_cs [] asx) (ax # asx' @ [a'])

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
hence "valid_path_aux [] (ax#asx'@[a'])"
[PROOF STATE]
proof (prove)
using this:
valid_path_aux ([] @ upd_cs [] asx) (ax # asx' @ [a'])

goal (1 subgoal):
 1. valid_path_aux [] (ax # asx' @ [a'])
[PROOF STEP]
by(rule valid_path_aux_callstack_prefix)
[PROOF STATE]
proof (state)
this:
valid_path_aux [] (ax # asx' @ [a'])

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with \<open>\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
valid_path_aux [] (ax # asx' @ [a'])
[PROOF STEP]
have "valid_path_aux [ax] (asx'@[a'])"
[PROOF STATE]
proof (prove)
using this:
\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
valid_path_aux [] (ax # asx' @ [a'])

goal (1 subgoal):
 1. valid_path_aux [ax] (asx' @ [a'])
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
valid_path_aux [ax] (asx' @ [a'])

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
hence "valid_path_aux (upd_cs [ax] asx') [a']"
[PROOF STATE]
proof (prove)
using this:
valid_path_aux [ax] (asx' @ [a'])

goal (1 subgoal):
 1. valid_path_aux (upd_cs [ax] asx') [a']
[PROOF STEP]
by(rule valid_path_aux_split)
[PROOF STATE]
proof (state)
this:
valid_path_aux (upd_cs [ax] asx') [a']

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
from \<open>targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'
[PROOF STEP]
have "same_level_path_aux [] asx'" and "upd_cs [] asx' = []"
[PROOF STATE]
proof (prove)
using this:
targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'

goal (1 subgoal):
 1. same_level_path_aux [] asx' &&& upd_cs [] asx' = []
[PROOF STEP]
by(simp_all add:slp_def same_level_path_def)
[PROOF STATE]
proof (state)
this:
same_level_path_aux [] asx'
upd_cs [] asx' = []

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
hence "upd_cs ([]@[ax]) asx' = []@[ax]"
[PROOF STATE]
proof (prove)
using this:
same_level_path_aux [] asx'
upd_cs [] asx' = []

goal (1 subgoal):
 1. upd_cs ([] @ [ax]) asx' = [] @ [ax]
[PROOF STEP]
by(rule same_level_path_upd_cs_callstack_Append)
[PROOF STATE]
proof (state)
this:
upd_cs ([] @ [ax]) asx' = [] @ [ax]

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with \<open>valid_path_aux (upd_cs [ax] asx') [a']\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_path_aux (upd_cs [ax] asx') [a']
upd_cs ([] @ [ax]) asx' = [] @ [ax]
[PROOF STEP]
have "valid_path_aux [ax] [a']"
[PROOF STATE]
proof (prove)
using this:
valid_path_aux (upd_cs [ax] asx') [a']
upd_cs ([] @ [ax]) asx' = [] @ [ax]

goal (1 subgoal):
 1. valid_path_aux [ax] [a']
[PROOF STEP]
by(simp del:valid_path_aux.simps)
[PROOF STATE]
proof (state)
this:
valid_path_aux [ax] [a']

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with \<open>\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f
valid_path_aux [ax] [a']
[PROOF STEP]
have "a' \<in> get_return_edges ax"
[PROOF STATE]
proof (prove)
using this:
\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f
valid_path_aux [ax] [a']

goal (1 subgoal):
 1. a' \<in> get_return_edges ax
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a' \<in> get_return_edges ax

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with \<open>upd_cs ([]@[ax]) asx' = []@[ax]\<close> \<open>kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<close>
[PROOF STATE]
proof (chain)
picking this:
upd_cs ([] @ [ax]) asx' = [] @ [ax]
kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f
a' \<in> get_return_edges ax
[PROOF STEP]
have "upd_cs [ax] (asx'@[a']) = []"
[PROOF STATE]
proof (prove)
using this:
upd_cs ([] @ [ax]) asx' = [] @ [ax]
kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f
a' \<in> get_return_edges ax

goal (1 subgoal):
 1. upd_cs [ax] (asx' @ [a']) = []
[PROOF STEP]
by(fastforce intro:upd_cs_Append)
[PROOF STATE]
proof (state)
this:
upd_cs [ax] (asx' @ [a']) = []

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with \<open>\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
upd_cs [ax] (asx' @ [a']) = []
[PROOF STEP]
have "upd_cs [] (ax#asx'@[a']) = []"
[PROOF STATE]
proof (prove)
using this:
\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
upd_cs [ax] (asx' @ [a']) = []

goal (1 subgoal):
 1. upd_cs [] (ax # asx' @ [a']) = []
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
upd_cs [] (ax # asx' @ [a']) = []

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
from \<open>targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'
[PROOF STEP]
have "same_level_path_aux [] asx'" and "upd_cs [] asx' = []"
[PROOF STATE]
proof (prove)
using this:
targetnode ax -asx'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode a'

goal (1 subgoal):
 1. same_level_path_aux [] asx' &&& upd_cs [] asx' = []
[PROOF STEP]
by(simp_all add:slp_def same_level_path_def)
[PROOF STATE]
proof (state)
this:
same_level_path_aux [] asx'
upd_cs [] asx' = []

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
hence "same_level_path_aux ([]@[ax]) asx'"
[PROOF STATE]
proof (prove)
using this:
same_level_path_aux [] asx'
upd_cs [] asx' = []

goal (1 subgoal):
 1. same_level_path_aux ([] @ [ax]) asx'
[PROOF STEP]
by -(rule same_level_path_aux_callstack_Append)
[PROOF STATE]
proof (state)
this:
same_level_path_aux ([] @ [ax]) asx'

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with \<open>\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close> \<open>kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<close>
              \<open>a' \<in> get_return_edges ax\<close> \<open>upd_cs ([]@[ax]) asx' = []@[ax]\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f
a' \<in> get_return_edges ax
upd_cs ([] @ [ax]) asx' = [] @ [ax]
same_level_path_aux ([] @ [ax]) asx'
[PROOF STEP]
have "same_level_path_aux [] ((ax#asx')@[a'])"
[PROOF STATE]
proof (prove)
using this:
\<exists>Q r p fs. kind ax = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f
a' \<in> get_return_edges ax
upd_cs ([] @ [ax]) asx' = [] @ [ax]
same_level_path_aux ([] @ [ax]) asx'

goal (1 subgoal):
 1. same_level_path_aux [] ((ax # asx') @ [a'])
[PROOF STEP]
by(fastforce intro:same_level_path_aux_Append)
[PROOF STATE]
proof (state)
this:
same_level_path_aux [] ((ax # asx') @ [a'])

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with \<open>upd_cs [] (ax#asx'@[a']) = []\<close>
              \<open>sourcenode ax -(ax#asx')@[a']\<rightarrow>* targetnode a'\<close>
[PROOF STATE]
proof (chain)
picking this:
upd_cs [] (ax # asx' @ [a']) = []
sourcenode ax -(ax # asx') @ [a']\<rightarrow>* targetnode a'
same_level_path_aux [] ((ax # asx') @ [a'])
[PROOF STEP]
have "sourcenode ax -(ax#asx')@[a']\<rightarrow>\<^bsub>sl\<^esub>* targetnode a'"
[PROOF STATE]
proof (prove)
using this:
upd_cs [] (ax # asx' @ [a']) = []
sourcenode ax -(ax # asx') @ [a']\<rightarrow>* targetnode a'
same_level_path_aux [] ((ax # asx') @ [a'])

goal (1 subgoal):
 1. sourcenode ax -(ax # asx') @ [a']\<rightarrow>\<^bsub>sl\<^esub>* targetnode a'
[PROOF STEP]
by(simp add:slp_def same_level_path_def)
[PROOF STATE]
proof (state)
this:
sourcenode ax -(ax # asx') @ [a']\<rightarrow>\<^bsub>sl\<^esub>* targetnode a'

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with \<open>targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax\<close>
[PROOF STATE]
proof (chain)
picking this:
targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax
sourcenode ax -(ax # asx') @ [a']\<rightarrow>\<^bsub>sl\<^esub>* targetnode a'
[PROOF STEP]
have "targetnode x -xs'@((ax#asx')@[a'])\<rightarrow>\<^bsub>sl\<^esub>* targetnode a'"
[PROOF STATE]
proof (prove)
using this:
targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax
sourcenode ax -(ax # asx') @ [a']\<rightarrow>\<^bsub>sl\<^esub>* targetnode a'

goal (1 subgoal):
 1. targetnode x -xs' @ (ax # asx') @ [a']\<rightarrow>\<^bsub>sl\<^esub>* targetnode a'
[PROOF STEP]
by(rule slp_Append)
[PROOF STATE]
proof (state)
this:
targetnode x -xs' @ (ax # asx') @ [a']\<rightarrow>\<^bsub>sl\<^esub>* targetnode a'

goal (2 subgoals):
 1. \<exists>xs x xs'. asx = xs @ x # xs' \<and> (\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode x) \<and> targetnode x -xs'\<rightarrow>\<^bsub>sl\<^esub>* sourcenode ax \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
 2. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with \<open>\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs\<close>
              \<open>call_of_return_node (hd ms') (sourcenode x)\<close>
              \<open>as = xs@x#(xs'@ax#asx'@[a'])\<close> \<open>m' = targetnode a'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
call_of_return_node (hd ms') (sourcenode x)
as = xs @ x # xs' @ ax # asx' @ [a']
m' = targetnode a'
targetnode x -xs' @ (ax # asx') @ [a']\<rightarrow>\<^bsub>sl\<^esub>* targetnode a'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>Q r p fs. kind x = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
call_of_return_node (hd ms') (sourcenode x)
as = xs @ x # xs' @ ax # asx' @ [a']
m' = targetnode a'
targetnode x -xs' @ (ax # asx') @ [a']\<rightarrow>\<^bsub>sl\<^esub>* targetnode a'

goal (1 subgoal):
 1. (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
by simp blast
[PROOF STATE]
proof (state)
this:
(\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms

goal (1 subgoal):
 1. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
assume "ms = ms'"
[PROOF STATE]
proof (state)
this:
ms = ms'

goal (1 subgoal):
 1. ms = ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ms = ms'

goal (1 subgoal):
 1. (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms

goal (1 subgoal):
 1. ms = targetnode a' # ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ms = targetnode a' # ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
assume "ms = targetnode a' # ms'"
[PROOF STATE]
proof (state)
this:
ms = targetnode a' # ms'

goal (1 subgoal):
 1. ms = targetnode a' # ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
from \<open>S,kind \<turnstile> (ms'',s'') -a'\<rightarrow>\<^sub>\<tau> (m'#ms',s')\<close> \<open>kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f\<close>
            \<open>ms'' = sourcenode a' # targetnode a' # ms'\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (ms'',s'') -a'\<rightarrow>\<^sub>\<tau> (m' # ms',s')
kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f
ms'' = sourcenode a' # targetnode a' # ms'
[PROOF STEP]
have "\<exists>m \<in> set (targetnode a' # ms'). \<exists>m'. call_of_return_node m m' \<and>
            m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (ms'',s'') -a'\<rightarrow>\<^sub>\<tau> (m' # ms',s')
kind a' = Q\<hookleftarrow>\<^bsub>p\<^esub>f
ms'' = sourcenode a' # targetnode a' # ms'

goal (1 subgoal):
 1. \<exists>m\<in>set (targetnode a' # ms'). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
by(fastforce elim!:silent_move.cases simp:intra_kind_def)
[PROOF STATE]
proof (state)
this:
\<exists>m\<in>set (targetnode a' # ms'). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. ms = targetnode a' # ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
with \<open>ms = targetnode a' # ms'\<close> callstack
[PROOF STATE]
proof (chain)
picking this:
ms = targetnode a' # ms'
\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
\<exists>m\<in>set (targetnode a' # ms'). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
ms = targetnode a' # ms'
\<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
\<exists>m\<in>set (targetnode a' # ms'). \<exists>m'. call_of_return_node m m' \<and> m' \<notin> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

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

goal (1 subgoal):
 1. ms = targetnode a' # ms' \<Longrightarrow> (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. (\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>as' a as''. as = as' @ a # as'' \<and> (\<exists>Q r p fs. kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs) \<and> call_of_return_node (hd ms') (sourcenode a) \<and> targetnode a -as''\<rightarrow>\<^bsub>sl\<^esub>* m') \<or> ms' = ms

goal:
No subgoals!
[PROOF STEP]
qed