[STATEMENT]
lemma silent_moves_same_level_path:
  assumes "S,kind \<turnstile> (m#ms,s) =as\<Rightarrow>\<^sub>\<tau> (m'#ms',s')" and "m -as\<rightarrow>\<^bsub>sl\<^esub>* m'" shows "ms = ms'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ms = ms'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 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]
obtain cf cfs where "s = cf#cfs"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (1 subgoal):
 1. (\<And>cf cfs. s = cf # cfs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases s)(auto dest:silent_moves_equal_length)
[PROOF STATE]
proof (state)
this:
s = cf # cfs

goal (1 subgoal):
 1. 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')
s = cf # cfs
[PROOF STEP]
have "transfers (kinds as) (cf#cfs) = s'"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
s = cf # cfs

goal (1 subgoal):
 1. transfers (kinds as) (cf # cfs) = s'
[PROOF STEP]
by(fastforce intro:silent_moves_preds_transfers simp:kinds_def)
[PROOF STATE]
proof (state)
this:
transfers (kinds as) (cf # cfs) = s'

goal (1 subgoal):
 1. ms = ms'
[PROOF STEP]
with \<open>m -as\<rightarrow>\<^bsub>sl\<^esub>* m'\<close>
[PROOF STATE]
proof (chain)
picking this:
m -as\<rightarrow>\<^bsub>sl\<^esub>* m'
transfers (kinds as) (cf # cfs) = s'
[PROOF STEP]
obtain cf' where "s' = cf'#cfs"
[PROOF STATE]
proof (prove)
using this:
m -as\<rightarrow>\<^bsub>sl\<^esub>* m'
transfers (kinds as) (cf # cfs) = s'

goal (1 subgoal):
 1. (\<And>cf'. s' = cf' # cfs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by -(drule slp_callstack_length_equal,auto)
[PROOF STATE]
proof (state)
this:
s' = cf' # cfs

goal (1 subgoal):
 1. 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]
have "length (m#ms) = length s" and "length (m'#ms') = length s'"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')

goal (1 subgoal):
 1. length (m # ms) = length s &&& length (m' # ms') = length s'
[PROOF STEP]
by(rule silent_moves_equal_length)+
[PROOF STATE]
proof (state)
this:
length (m # ms) = length s
length (m' # ms') = length s'

goal (1 subgoal):
 1. ms = ms'
[PROOF STEP]
with \<open>s = cf#cfs\<close> \<open>s' = cf'#cfs\<close>
[PROOF STATE]
proof (chain)
picking this:
s = cf # cfs
s' = cf' # cfs
length (m # ms) = length s
length (m' # ms') = length s'
[PROOF STEP]
have "length ms = length ms'"
[PROOF STATE]
proof (prove)
using this:
s = cf # cfs
s' = cf' # cfs
length (m # ms) = length s
length (m' # ms') = length s'

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

goal (1 subgoal):
 1. ms = ms'
[PROOF STEP]
from \<open>m -as\<rightarrow>\<^bsub>sl\<^esub>* m'\<close>
[PROOF STATE]
proof (chain)
picking this:
m -as\<rightarrow>\<^bsub>sl\<^esub>* m'
[PROOF STEP]
have "same_level_path_aux [] as"
[PROOF STATE]
proof (prove)
using this:
m -as\<rightarrow>\<^bsub>sl\<^esub>* m'

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

goal (1 subgoal):
 1. ms = ms'
[PROOF STEP]
with \<open>S,kind \<turnstile> (m#ms,s) =as\<Rightarrow>\<^sub>\<tau> (m'#ms',s')\<close> \<open>length ms = length ms'\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
length ms = length ms'
same_level_path_aux [] as
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
length ms = length ms'
same_level_path_aux [] as

goal (1 subgoal):
 1. ms = ms'
[PROOF STEP]
by(auto elim!:slpa_silent_moves_callstacks_eq
    simp:targetnodes_def valid_call_list_def valid_return_list_def)
[PROOF STATE]
proof (state)
this:
ms = ms'

goal:
No subgoals!
[PROOF STEP]
qed