[STATEMENT]
lemma valid_path_trans_observable_moves:
  assumes "m -as\<rightarrow>\<^sub>\<surd>* m'" and "preds (kinds as) [cf]"
  and "transfers (kinds as) [cf] = s'"
  obtains ms'' s'' ms' as' as''
  where "S,kind \<turnstile> ([m],[cf]) =slice_edges S [] as\<Rightarrow>* (ms'',s'')"
  and "S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m'#ms',s')"
  and "slice_edges S [] as = slice_edges S [] as''"
  and "m -as''@as'\<rightarrow>\<^sub>\<surd>* m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ms'' s'' as' ms' as''. \<lbrakk>S,kind \<turnstile> ([m],[cf]) =slice_edges S [] as\<Rightarrow>* (ms'',s''); S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); slice_edges S [] as = slice_edges S [] as''; m -as'' @ as'\<rightarrow>\<^sub>\<surd>* m'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>ms'' s'' as' ms' as''. S,kind \<turnstile> ([m],[cf]) =slice_edges S [] as\<Rightarrow>* (ms'',s'') \<and> S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',s') \<and> slice_edges S [] as = slice_edges S [] as'' \<and> m -as'' @ as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from \<open>m -as\<rightarrow>\<^sub>\<surd>* m'\<close>
[PROOF STATE]
proof (chain)
picking this:
m -as\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
have "valid_path_aux [] as" and "m -as\<rightarrow>* m'"
[PROOF STATE]
proof (prove)
using this:
m -as\<rightarrow>\<^sub>\<surd>* m'

goal (1 subgoal):
 1. valid_path_aux [] as &&& m -as\<rightarrow>* m'
[PROOF STEP]
by(simp_all add:vp_def valid_path_def)
[PROOF STATE]
proof (state)
this:
valid_path_aux [] as
m -as\<rightarrow>* m'

goal (1 subgoal):
 1. \<exists>ms'' s'' as' ms' as''. S,kind \<turnstile> ([m],[cf]) =slice_edges S [] as\<Rightarrow>* (ms'',s'') \<and> S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',s') \<and> slice_edges S [] as = slice_edges S [] as'' \<and> m -as'' @ as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
from this \<open>preds (kinds as) [cf]\<close> \<open>transfers (kinds as) [cf] = s'\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_path_aux [] as
m -as\<rightarrow>* m'
preds (kinds as) [cf]
transfers (kinds as) [cf] = s'
[PROOF STEP]
show "\<exists>ms'' s'' as' ms' as''.
    S,kind \<turnstile> ([m],[cf]) =slice_edges S [] as\<Rightarrow>* (ms'',s'') \<and>
    S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',s') \<and>
    slice_edges S [] as = slice_edges S [] as'' \<and> m -as'' @ as'\<rightarrow>\<^sub>\<surd>* m'"
[PROOF STATE]
proof (prove)
using this:
valid_path_aux [] as
m -as\<rightarrow>* m'
preds (kinds as) [cf]
transfers (kinds as) [cf] = s'

goal (1 subgoal):
 1. \<exists>ms'' s'' as' ms' as''. S,kind \<turnstile> ([m],[cf]) =slice_edges S [] as\<Rightarrow>* (ms'',s'') \<and> S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',s') \<and> slice_edges S [] as = slice_edges S [] as'' \<and> m -as'' @ as'\<rightarrow>\<^sub>\<surd>* m'
[PROOF STEP]
by -(erule vpa_trans_observable_moves[of _ _ _ _ _ _ "[]" S],
      auto simp:valid_call_list_def valid_return_list_def vp_def valid_path_def)
[PROOF STATE]
proof (state)
this:
\<exists>ms'' s'' as' ms' as''. S,kind \<turnstile> ([m],[cf]) =slice_edges S [] as\<Rightarrow>* (ms'',s'') \<and> S,kind \<turnstile> (ms'',s'') =as'\<Rightarrow>\<^sub>\<tau> (m' # ms',s') \<and> slice_edges S [] as = slice_edges S [] as'' \<and> m -as'' @ as'\<rightarrow>\<^sub>\<surd>* m'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma WS_weak_sim_trans:
  assumes "((ms\<^sub>1,s\<^sub>1),(ms\<^sub>2,s\<^sub>2)) \<in> WS S"
  and "S,kind \<turnstile> (ms\<^sub>1,s\<^sub>1) =as\<Rightarrow>* (ms\<^sub>1',s\<^sub>1')" and "as \<noteq> []"
  shows "((ms\<^sub>1',s\<^sub>1'),(ms\<^sub>1',transfers (slice_kinds S as) s\<^sub>2)) \<in> WS S \<and>
         S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =as\<Rightarrow>* (ms\<^sub>1',transfers (slice_kinds S as) s\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((ms\<^sub>1', s\<^sub>1'), ms\<^sub>1', transfers (slice_kinds S as) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =as\<Rightarrow>* (ms\<^sub>1',transfers (slice_kinds S as) s\<^sub>2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((ms\<^sub>1', s\<^sub>1'), ms\<^sub>1', transfers (slice_kinds S as) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =as\<Rightarrow>* (ms\<^sub>1',transfers (slice_kinds S as) s\<^sub>2)
[PROOF STEP]
obtain f where "f = kind"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f. f = kind \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f = kind

goal (1 subgoal):
 1. ((ms\<^sub>1', s\<^sub>1'), ms\<^sub>1', transfers (slice_kinds S as) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =as\<Rightarrow>* (ms\<^sub>1',transfers (slice_kinds S as) s\<^sub>2)
[PROOF STEP]
with \<open>S,kind \<turnstile> (ms\<^sub>1,s\<^sub>1) =as\<Rightarrow>* (ms\<^sub>1',s\<^sub>1')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,kind \<turnstile> (ms\<^sub>1,s\<^sub>1) =as\<Rightarrow>* (ms\<^sub>1',s\<^sub>1')
f = kind
[PROOF STEP]
have "S,f \<turnstile> (ms\<^sub>1,s\<^sub>1) =as\<Rightarrow>* (ms\<^sub>1',s\<^sub>1')"
[PROOF STATE]
proof (prove)
using this:
S,kind \<turnstile> (ms\<^sub>1,s\<^sub>1) =as\<Rightarrow>* (ms\<^sub>1',s\<^sub>1')
f = kind

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

goal (1 subgoal):
 1. ((ms\<^sub>1', s\<^sub>1'), ms\<^sub>1', transfers (slice_kinds S as) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =as\<Rightarrow>* (ms\<^sub>1',transfers (slice_kinds S as) s\<^sub>2)
[PROOF STEP]
from \<open>S,f \<turnstile> (ms\<^sub>1,s\<^sub>1) =as\<Rightarrow>* (ms\<^sub>1',s\<^sub>1')\<close> \<open>((ms\<^sub>1,s\<^sub>1),(ms\<^sub>2,s\<^sub>2)) \<in> WS S\<close>
    \<open>as \<noteq> []\<close> \<open>f = kind\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (ms\<^sub>1,s\<^sub>1) =as\<Rightarrow>* (ms\<^sub>1',s\<^sub>1')
((ms\<^sub>1, s\<^sub>1), ms\<^sub>2, s\<^sub>2) \<in> WS S
as \<noteq> []
f = kind
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (ms\<^sub>1,s\<^sub>1) =as\<Rightarrow>* (ms\<^sub>1',s\<^sub>1')
((ms\<^sub>1, s\<^sub>1), ms\<^sub>2, s\<^sub>2) \<in> WS S
as \<noteq> []
f = kind

goal (1 subgoal):
 1. ((ms\<^sub>1', s\<^sub>1'), ms\<^sub>1', transfers (slice_kinds S as) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =as\<Rightarrow>* (ms\<^sub>1',transfers (slice_kinds S as) s\<^sub>2)
[PROOF STEP]
proof(induct arbitrary:ms\<^sub>2 s\<^sub>2 rule:trans_observable_moves.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ms s S f ms\<^sub>2 s\<^sub>2. \<lbrakk>length ms = length s; ((ms, s), ms\<^sub>2, s\<^sub>2) \<in> WS S; [] \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms, s), ms, transfers (slice_kinds S []) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =[]\<Rightarrow>* (ms,transfers (slice_kinds S []) s\<^sub>2)
 2. \<And>S f ms s as ms' s' as' ms'' s'' ms\<^sub>2 s\<^sub>2. \<lbrakk>S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s'); S,f \<turnstile> (ms',s') =as'\<Rightarrow>* (ms'',s''); \<And>ms\<^sub>2 s\<^sub>2. \<lbrakk>((ms', s'), ms\<^sub>2, s\<^sub>2) \<in> WS S; as' \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S as') s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =as'\<Rightarrow>* (ms'',transfers (slice_kinds S as') s\<^sub>2); ((ms, s), ms\<^sub>2, s\<^sub>2) \<in> WS S; last as # as' \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
[PROOF STEP]
case tom_Nil
[PROOF STATE]
proof (state)
this:
length ms_ = length s_
((ms_, s_), ms\<^sub>2, s\<^sub>2) \<in> WS S_
[] \<noteq> []
f_ = kind

goal (2 subgoals):
 1. \<And>ms s S f ms\<^sub>2 s\<^sub>2. \<lbrakk>length ms = length s; ((ms, s), ms\<^sub>2, s\<^sub>2) \<in> WS S; [] \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms, s), ms, transfers (slice_kinds S []) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =[]\<Rightarrow>* (ms,transfers (slice_kinds S []) s\<^sub>2)
 2. \<And>S f ms s as ms' s' as' ms'' s'' ms\<^sub>2 s\<^sub>2. \<lbrakk>S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s'); S,f \<turnstile> (ms',s') =as'\<Rightarrow>* (ms'',s''); \<And>ms\<^sub>2 s\<^sub>2. \<lbrakk>((ms', s'), ms\<^sub>2, s\<^sub>2) \<in> WS S; as' \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S as') s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =as'\<Rightarrow>* (ms'',transfers (slice_kinds S as') s\<^sub>2); ((ms, s), ms\<^sub>2, s\<^sub>2) \<in> WS S; last as # as' \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
length ms_ = length s_
((ms_, s_), ms\<^sub>2, s\<^sub>2) \<in> WS S_
[] \<noteq> []
f_ = kind

goal (1 subgoal):
 1. ((ms_, s_), ms_, transfers (slice_kinds S_ []) s\<^sub>2) \<in> WS S_ \<and> S_,slice_kind S_ \<turnstile> (ms\<^sub>2,s\<^sub>2) =[]\<Rightarrow>* (ms_,transfers (slice_kinds S_ []) s\<^sub>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((ms_, s_), ms_, transfers (slice_kinds S_ []) s\<^sub>2) \<in> WS S_ \<and> S_,slice_kind S_ \<turnstile> (ms\<^sub>2,s\<^sub>2) =[]\<Rightarrow>* (ms_,transfers (slice_kinds S_ []) s\<^sub>2)

goal (1 subgoal):
 1. \<And>S f ms s as ms' s' as' ms'' s'' ms\<^sub>2 s\<^sub>2. \<lbrakk>S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s'); S,f \<turnstile> (ms',s') =as'\<Rightarrow>* (ms'',s''); \<And>ms\<^sub>2 s\<^sub>2. \<lbrakk>((ms', s'), ms\<^sub>2, s\<^sub>2) \<in> WS S; as' \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S as') s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =as'\<Rightarrow>* (ms'',transfers (slice_kinds S as') s\<^sub>2); ((ms, s), ms\<^sub>2, s\<^sub>2) \<in> WS S; last as # as' \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S f ms s as ms' s' as' ms'' s'' ms\<^sub>2 s\<^sub>2. \<lbrakk>S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s'); S,f \<turnstile> (ms',s') =as'\<Rightarrow>* (ms'',s''); \<And>ms\<^sub>2 s\<^sub>2. \<lbrakk>((ms', s'), ms\<^sub>2, s\<^sub>2) \<in> WS S; as' \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S as') s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =as'\<Rightarrow>* (ms'',transfers (slice_kinds S as') s\<^sub>2); ((ms, s), ms\<^sub>2, s\<^sub>2) \<in> WS S; last as # as' \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
[PROOF STEP]
case (tom_Cons S f ms s as ms' s' as' ms'' s'')
[PROOF STATE]
proof (state)
this:
S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s')
S,f \<turnstile> (ms',s') =as'\<Rightarrow>* (ms'',s'')
\<lbrakk>((ms', s'), ?ms\<^sub>2, ?s\<^sub>2) \<in> WS S; as' \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S as') ?s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (?ms\<^sub>2,?s\<^sub>2) =as'\<Rightarrow>* (ms'',transfers (slice_kinds S as') ?s\<^sub>2)
((ms, s), ms\<^sub>2, s\<^sub>2) \<in> WS S
last as # as' \<noteq> []
f = kind

goal (1 subgoal):
 1. \<And>S f ms s as ms' s' as' ms'' s'' ms\<^sub>2 s\<^sub>2. \<lbrakk>S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s'); S,f \<turnstile> (ms',s') =as'\<Rightarrow>* (ms'',s''); \<And>ms\<^sub>2 s\<^sub>2. \<lbrakk>((ms', s'), ms\<^sub>2, s\<^sub>2) \<in> WS S; as' \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S as') s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =as'\<Rightarrow>* (ms'',transfers (slice_kinds S as') s\<^sub>2); ((ms, s), ms\<^sub>2, s\<^sub>2) \<in> WS S; last as # as' \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
[PROOF STEP]
note IH = \<open>\<And>ms\<^sub>2 s\<^sub>2. \<lbrakk>((ms',s'),(ms\<^sub>2,s\<^sub>2)) \<in> WS S; as' \<noteq> []; f = kind\<rbrakk>
      \<Longrightarrow> ((ms'',s''),(ms'',transfers (slice_kinds S as') s\<^sub>2)) \<in> WS S \<and>
      S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =as'\<Rightarrow>* (ms'',transfers (slice_kinds S as') s\<^sub>2)\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>((ms', s'), ?ms\<^sub>2, ?s\<^sub>2) \<in> WS S; as' \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S as') ?s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (?ms\<^sub>2,?s\<^sub>2) =as'\<Rightarrow>* (ms'',transfers (slice_kinds S as') ?s\<^sub>2)

goal (1 subgoal):
 1. \<And>S f ms s as ms' s' as' ms'' s'' ms\<^sub>2 s\<^sub>2. \<lbrakk>S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s'); S,f \<turnstile> (ms',s') =as'\<Rightarrow>* (ms'',s''); \<And>ms\<^sub>2 s\<^sub>2. \<lbrakk>((ms', s'), ms\<^sub>2, s\<^sub>2) \<in> WS S; as' \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S as') s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =as'\<Rightarrow>* (ms'',transfers (slice_kinds S as') s\<^sub>2); ((ms, s), ms\<^sub>2, s\<^sub>2) \<in> WS S; last as # as' \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
[PROOF STEP]
from \<open>S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s')
[PROOF STEP]
have "s' \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s')

goal (1 subgoal):
 1. s' \<noteq> []
[PROOF STEP]
by(fastforce elim:observable_moves.cases observable_move.cases)
[PROOF STATE]
proof (state)
this:
s' \<noteq> []

goal (1 subgoal):
 1. \<And>S f ms s as ms' s' as' ms'' s'' ms\<^sub>2 s\<^sub>2. \<lbrakk>S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s'); S,f \<turnstile> (ms',s') =as'\<Rightarrow>* (ms'',s''); \<And>ms\<^sub>2 s\<^sub>2. \<lbrakk>((ms', s'), ms\<^sub>2, s\<^sub>2) \<in> WS S; as' \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S as') s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =as'\<Rightarrow>* (ms'',transfers (slice_kinds S as') s\<^sub>2); ((ms, s), ms\<^sub>2, s\<^sub>2) \<in> WS S; last as # as' \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
[PROOF STEP]
from \<open>S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s')
[PROOF STEP]
obtain asx ax msx sx where "S,f \<turnstile> (ms,s) =asx\<Rightarrow>\<^sub>\<tau> (msx,sx)"
      and "S,f \<turnstile> (msx,sx) -ax\<rightarrow> (ms',s')" and "as = asx@[ax]"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s')

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

goal (1 subgoal):
 1. \<And>S f ms s as ms' s' as' ms'' s'' ms\<^sub>2 s\<^sub>2. \<lbrakk>S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s'); S,f \<turnstile> (ms',s') =as'\<Rightarrow>* (ms'',s''); \<And>ms\<^sub>2 s\<^sub>2. \<lbrakk>((ms', s'), ms\<^sub>2, s\<^sub>2) \<in> WS S; as' \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S as') s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =as'\<Rightarrow>* (ms'',transfers (slice_kinds S as') s\<^sub>2); ((ms, s), ms\<^sub>2, s\<^sub>2) \<in> WS S; last as # as' \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
[PROOF STEP]
from \<open>S,f \<turnstile> (ms,s) =asx\<Rightarrow>\<^sub>\<tau> (msx,sx)\<close> \<open>((ms,s),(ms\<^sub>2,s\<^sub>2)) \<in> WS S\<close> \<open>f = kind\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (ms,s) =asx\<Rightarrow>\<^sub>\<tau> (msx,sx)
((ms, s), ms\<^sub>2, s\<^sub>2) \<in> WS S
f = kind
[PROOF STEP]
have "((msx,sx),(ms\<^sub>2,s\<^sub>2)) \<in> WS S"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (ms,s) =asx\<Rightarrow>\<^sub>\<tau> (msx,sx)
((ms, s), ms\<^sub>2, s\<^sub>2) \<in> WS S
f = kind

goal (1 subgoal):
 1. ((msx, sx), ms\<^sub>2, s\<^sub>2) \<in> WS S
[PROOF STEP]
by(fastforce intro:WS_silent_moves)
[PROOF STATE]
proof (state)
this:
((msx, sx), ms\<^sub>2, s\<^sub>2) \<in> WS S

goal (1 subgoal):
 1. \<And>S f ms s as ms' s' as' ms'' s'' ms\<^sub>2 s\<^sub>2. \<lbrakk>S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s'); S,f \<turnstile> (ms',s') =as'\<Rightarrow>* (ms'',s''); \<And>ms\<^sub>2 s\<^sub>2. \<lbrakk>((ms', s'), ms\<^sub>2, s\<^sub>2) \<in> WS S; as' \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S as') s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =as'\<Rightarrow>* (ms'',transfers (slice_kinds S as') s\<^sub>2); ((ms, s), ms\<^sub>2, s\<^sub>2) \<in> WS S; last as # as' \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
[PROOF STEP]
from \<open>((msx,sx),(ms\<^sub>2,s\<^sub>2)) \<in> WS S\<close> \<open>S,f \<turnstile> (msx,sx) -ax\<rightarrow> (ms',s')\<close> \<open>s' \<noteq> []\<close>
      \<open>f = kind\<close>
[PROOF STATE]
proof (chain)
picking this:
((msx, sx), ms\<^sub>2, s\<^sub>2) \<in> WS S
S,f \<turnstile> (msx,sx) -ax\<rightarrow> (ms',s')
s' \<noteq> []
f = kind
[PROOF STEP]
obtain asx' where "((ms',s'),(ms',transfer (slice_kind S ax) s\<^sub>2)) \<in> WS S"
      and "S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =asx'@[ax]\<Rightarrow>
      (ms',transfer (slice_kind S ax) s\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
((msx, sx), ms\<^sub>2, s\<^sub>2) \<in> WS S
S,f \<turnstile> (msx,sx) -ax\<rightarrow> (ms',s')
s' \<noteq> []
f = kind

goal (1 subgoal):
 1. (\<And>asx'. \<lbrakk>((ms', s'), ms', transfer (slice_kind S ax) s\<^sub>2) \<in> WS S; S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =asx' @ [ax]\<Rightarrow> (ms',transfer (slice_kind S ax) s\<^sub>2)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(fastforce elim:WS_observable_move)
[PROOF STATE]
proof (state)
this:
((ms', s'), ms', transfer (slice_kind S ax) s\<^sub>2) \<in> WS S
S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =asx' @ [ax]\<Rightarrow> (ms',transfer (slice_kind S ax) s\<^sub>2)

goal (1 subgoal):
 1. \<And>S f ms s as ms' s' as' ms'' s'' ms\<^sub>2 s\<^sub>2. \<lbrakk>S,f \<turnstile> (ms,s) =as\<Rightarrow> (ms',s'); S,f \<turnstile> (ms',s') =as'\<Rightarrow>* (ms'',s''); \<And>ms\<^sub>2 s\<^sub>2. \<lbrakk>((ms', s'), ms\<^sub>2, s\<^sub>2) \<in> WS S; as' \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S as') s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =as'\<Rightarrow>* (ms'',transfers (slice_kinds S as') s\<^sub>2); ((ms, s), ms\<^sub>2, s\<^sub>2) \<in> WS S; last as # as' \<noteq> []; f = kind\<rbrakk> \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
[PROOF STEP]
proof(cases "as' = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. as' = [] \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
 2. as' \<noteq> [] \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
as' = []

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
 2. as' \<noteq> [] \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
[PROOF STEP]
with \<open>S,f \<turnstile> (ms',s') =as'\<Rightarrow>* (ms'',s'')\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (ms',s') =as'\<Rightarrow>* (ms'',s'')
as' = []
[PROOF STEP]
have "ms' = ms'' \<and> s' = s''"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (ms',s') =as'\<Rightarrow>* (ms'',s'')
as' = []

goal (1 subgoal):
 1. ms' = ms'' \<and> s' = s''
[PROOF STEP]
by(fastforce elim:trans_observable_moves.cases dest:observable_move_notempty)
[PROOF STATE]
proof (state)
this:
ms' = ms'' \<and> s' = s''

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
 2. as' \<noteq> [] \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
[PROOF STEP]
from \<open>((ms',s'),(ms',transfer (slice_kind S ax) s\<^sub>2)) \<in> WS S\<close>
[PROOF STATE]
proof (chain)
picking this:
((ms', s'), ms', transfer (slice_kind S ax) s\<^sub>2) \<in> WS S
[PROOF STEP]
have "length ms' = length (transfer (slice_kind S ax) s\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
((ms', s'), ms', transfer (slice_kind S ax) s\<^sub>2) \<in> WS S

goal (1 subgoal):
 1. length ms' = length (transfer (slice_kind S ax) s\<^sub>2)
[PROOF STEP]
by(fastforce elim:WS.cases)
[PROOF STATE]
proof (state)
this:
length ms' = length (transfer (slice_kind S ax) s\<^sub>2)

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
 2. as' \<noteq> [] \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
[PROOF STEP]
with \<open>S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =asx'@[ax]\<Rightarrow>
        (ms',transfer (slice_kind S ax) s\<^sub>2)\<close>
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =asx' @ [ax]\<Rightarrow> (ms',transfer (slice_kind S ax) s\<^sub>2)
length ms' = length (transfer (slice_kind S ax) s\<^sub>2)
[PROOF STEP]
have "S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =(last (asx'@[ax]))#[]\<Rightarrow>*
        (ms',transfer (slice_kind S ax) s\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =asx' @ [ax]\<Rightarrow> (ms',transfer (slice_kind S ax) s\<^sub>2)
length ms' = length (transfer (slice_kind S ax) s\<^sub>2)

goal (1 subgoal):
 1. S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =[last (asx' @ [ax])]\<Rightarrow>* (ms',transfer (slice_kind S ax) s\<^sub>2)
[PROOF STEP]
by(fastforce intro:trans_observable_moves.intros)
[PROOF STATE]
proof (state)
this:
S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =[last (asx' @ [ax])]\<Rightarrow>* (ms',transfer (slice_kind S ax) s\<^sub>2)

goal (2 subgoals):
 1. as' = [] \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
 2. as' \<noteq> [] \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
[PROOF STEP]
with \<open>((ms',s'),(ms',transfer (slice_kind S ax) s\<^sub>2)) \<in> WS S\<close> \<open>as = asx@[ax]\<close>
        \<open>ms' = ms'' \<and> s' = s''\<close> True
[PROOF STATE]
proof (chain)
picking this:
((ms', s'), ms', transfer (slice_kind S ax) s\<^sub>2) \<in> WS S
as = asx @ [ax]
ms' = ms'' \<and> s' = s''
as' = []
S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =[last (asx' @ [ax])]\<Rightarrow>* (ms',transfer (slice_kind S ax) s\<^sub>2)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((ms', s'), ms', transfer (slice_kind S ax) s\<^sub>2) \<in> WS S
as = asx @ [ax]
ms' = ms'' \<and> s' = s''
as' = []
S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =[last (asx' @ [ax])]\<Rightarrow>* (ms',transfer (slice_kind S ax) s\<^sub>2)

goal (1 subgoal):
 1. ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
[PROOF STEP]
by(fastforce simp:slice_kinds_def)
[PROOF STATE]
proof (state)
this:
((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
as' \<noteq> []

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
[PROOF STEP]
from IH[OF \<open>((ms',s'),(ms',transfer (slice_kind S ax) s\<^sub>2)) \<in> WS S\<close> this
        \<open>f = kind\<close>]
[PROOF STATE]
proof (chain)
picking this:
((ms'', s''), ms'', transfers (slice_kinds S as') (transfer (slice_kind S ax) s\<^sub>2)) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms',transfer (slice_kind S ax) s\<^sub>2) =as'\<Rightarrow>* (ms'',transfers (slice_kinds S as') (transfer (slice_kind S ax) s\<^sub>2))
[PROOF STEP]
have "((ms'',s''),(ms'',transfers (slice_kinds S as')
        (transfer (slice_kind S ax) s\<^sub>2))) \<in> WS S"
        and "S,slice_kind S \<turnstile> (ms',transfer (slice_kind S ax) s\<^sub>2) =as'\<Rightarrow>*
        (ms'',transfers (slice_kinds S as') (transfer (slice_kind S ax) s\<^sub>2))"
[PROOF STATE]
proof (prove)
using this:
((ms'', s''), ms'', transfers (slice_kinds S as') (transfer (slice_kind S ax) s\<^sub>2)) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms',transfer (slice_kind S ax) s\<^sub>2) =as'\<Rightarrow>* (ms'',transfers (slice_kinds S as') (transfer (slice_kind S ax) s\<^sub>2))

goal (1 subgoal):
 1. ((ms'', s''), ms'', transfers (slice_kinds S as') (transfer (slice_kind S ax) s\<^sub>2)) \<in> WS S &&& S,slice_kind S \<turnstile> (ms',transfer (slice_kind S ax) s\<^sub>2) =as'\<Rightarrow>* (ms'',transfers (slice_kinds S as') (transfer (slice_kind S ax) s\<^sub>2))
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
((ms'', s''), ms'', transfers (slice_kinds S as') (transfer (slice_kind S ax) s\<^sub>2)) \<in> WS S
S,slice_kind S \<turnstile> (ms',transfer (slice_kind S ax) s\<^sub>2) =as'\<Rightarrow>* (ms'',transfers (slice_kinds S as') (transfer (slice_kind S ax) s\<^sub>2))

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
[PROOF STEP]
with \<open>S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =asx'@[ax]\<Rightarrow>
                               (ms',transfer (slice_kind S ax) s\<^sub>2)\<close>
[PROOF STATE]
proof (chain)
picking this:
S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =asx' @ [ax]\<Rightarrow> (ms',transfer (slice_kind S ax) s\<^sub>2)
((ms'', s''), ms'', transfers (slice_kinds S as') (transfer (slice_kind S ax) s\<^sub>2)) \<in> WS S
S,slice_kind S \<turnstile> (ms',transfer (slice_kind S ax) s\<^sub>2) =as'\<Rightarrow>* (ms'',transfers (slice_kinds S as') (transfer (slice_kind S ax) s\<^sub>2))
[PROOF STEP]
have "S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =(last (asx'@[ax]))#as'\<Rightarrow>*
        (ms'',transfers (slice_kinds S as') (transfer (slice_kind S ax) s\<^sub>2))"
[PROOF STATE]
proof (prove)
using this:
S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =asx' @ [ax]\<Rightarrow> (ms',transfer (slice_kind S ax) s\<^sub>2)
((ms'', s''), ms'', transfers (slice_kinds S as') (transfer (slice_kind S ax) s\<^sub>2)) \<in> WS S
S,slice_kind S \<turnstile> (ms',transfer (slice_kind S ax) s\<^sub>2) =as'\<Rightarrow>* (ms'',transfers (slice_kinds S as') (transfer (slice_kind S ax) s\<^sub>2))

goal (1 subgoal):
 1. S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last (asx' @ [ax]) # as'\<Rightarrow>* (ms'',transfers (slice_kinds S as') (transfer (slice_kind S ax) s\<^sub>2))
[PROOF STEP]
by(fastforce intro:trans_observable_moves.tom_Cons)
[PROOF STATE]
proof (state)
this:
S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last (asx' @ [ax]) # as'\<Rightarrow>* (ms'',transfers (slice_kinds S as') (transfer (slice_kind S ax) s\<^sub>2))

goal (1 subgoal):
 1. as' \<noteq> [] \<Longrightarrow> ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
[PROOF STEP]
with \<open>((ms'',s''),(ms'',transfers (slice_kinds S as')
        (transfer (slice_kind S ax) s\<^sub>2))) \<in> WS S\<close> False \<open>as = asx@[ax]\<close>
[PROOF STATE]
proof (chain)
picking this:
((ms'', s''), ms'', transfers (slice_kinds S as') (transfer (slice_kind S ax) s\<^sub>2)) \<in> WS S
as' \<noteq> []
as = asx @ [ax]
S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last (asx' @ [ax]) # as'\<Rightarrow>* (ms'',transfers (slice_kinds S as') (transfer (slice_kind S ax) s\<^sub>2))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((ms'', s''), ms'', transfers (slice_kinds S as') (transfer (slice_kind S ax) s\<^sub>2)) \<in> WS S
as' \<noteq> []
as = asx @ [ax]
S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last (asx' @ [ax]) # as'\<Rightarrow>* (ms'',transfers (slice_kinds S as') (transfer (slice_kind S ax) s\<^sub>2))

goal (1 subgoal):
 1. ((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)
[PROOF STEP]
by(fastforce simp:slice_kinds_def)
[PROOF STATE]
proof (state)
this:
((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((ms'', s''), ms'', transfers (slice_kinds S (last as # as')) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =last as # as'\<Rightarrow>* (ms'',transfers (slice_kinds S (last as # as')) s\<^sub>2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
((ms\<^sub>1', s\<^sub>1'), ms\<^sub>1', transfers (slice_kinds S as) s\<^sub>2) \<in> WS S \<and> S,slice_kind S \<turnstile> (ms\<^sub>2,s\<^sub>2) =as\<Rightarrow>* (ms\<^sub>1',transfers (slice_kinds S as) s\<^sub>2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stacks_rewrite:
  assumes "valid_call_list cs m" and "valid_return_list rs m"
  and "\<forall>i < length rs. rs!i \<in> get_return_edges (cs!i)"
  and "length rs = length cs" and "ms = targetnodes rs"
  shows "\<forall>i<length cs. call_of_return_node (ms!i) (sourcenode (cs!i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<length cs. call_of_return_node (ms ! i) (sourcenode (cs ! i))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < length cs \<longrightarrow> call_of_return_node (ms ! i) (sourcenode (cs ! i))
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < length cs \<longrightarrow> call_of_return_node (ms ! i) (sourcenode (cs ! i))
[PROOF STEP]
show "i < length cs \<longrightarrow>
    call_of_return_node (ms ! i) (sourcenode (cs ! i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length cs \<longrightarrow> call_of_return_node (ms ! i) (sourcenode (cs ! i))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i < length cs \<Longrightarrow> call_of_return_node (ms ! i) (sourcenode (cs ! i))
[PROOF STEP]
assume "i < length cs"
[PROOF STATE]
proof (state)
this:
i < length cs

goal (1 subgoal):
 1. i < length cs \<Longrightarrow> call_of_return_node (ms ! i) (sourcenode (cs ! i))
[PROOF STEP]
with \<open>\<forall>i < length rs. rs!i \<in> get_return_edges (cs!i)\<close> \<open>length rs = length cs\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
length rs = length cs
i < length cs
[PROOF STEP]
have "rs!i \<in> get_return_edges (cs!i)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
length rs = length cs
i < length cs

goal (1 subgoal):
 1. rs ! i \<in> get_return_edges (cs ! i)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
rs ! i \<in> get_return_edges (cs ! i)

goal (1 subgoal):
 1. i < length cs \<Longrightarrow> call_of_return_node (ms ! i) (sourcenode (cs ! i))
[PROOF STEP]
from \<open>valid_return_list rs m\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_return_list rs m
[PROOF STEP]
have "\<forall>r \<in> set rs. valid_edge r"
[PROOF STATE]
proof (prove)
using this:
valid_return_list rs m

goal (1 subgoal):
 1. \<forall>r\<in>set rs. valid_edge r
[PROOF STEP]
by(rule valid_return_list_valid_edges)
[PROOF STATE]
proof (state)
this:
\<forall>r\<in>set rs. valid_edge r

goal (1 subgoal):
 1. i < length cs \<Longrightarrow> call_of_return_node (ms ! i) (sourcenode (cs ! i))
[PROOF STEP]
with \<open>i < length cs\<close> \<open>length rs = length cs\<close>
[PROOF STATE]
proof (chain)
picking this:
i < length cs
length rs = length cs
\<forall>r\<in>set rs. valid_edge r
[PROOF STEP]
have "valid_edge (rs!i)"
[PROOF STATE]
proof (prove)
using this:
i < length cs
length rs = length cs
\<forall>r\<in>set rs. valid_edge r

goal (1 subgoal):
 1. valid_edge (rs ! i)
[PROOF STEP]
by(simp add:all_set_conv_all_nth)
[PROOF STATE]
proof (state)
this:
valid_edge (rs ! i)

goal (1 subgoal):
 1. i < length cs \<Longrightarrow> call_of_return_node (ms ! i) (sourcenode (cs ! i))
[PROOF STEP]
from \<open>valid_call_list cs m\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_call_list cs m
[PROOF STEP]
have "\<forall>c \<in> set cs. valid_edge c"
[PROOF STATE]
proof (prove)
using this:
valid_call_list cs m

goal (1 subgoal):
 1. \<forall>c\<in>set cs. valid_edge c
[PROOF STEP]
by(rule valid_call_list_valid_edges)
[PROOF STATE]
proof (state)
this:
\<forall>c\<in>set cs. valid_edge c

goal (1 subgoal):
 1. i < length cs \<Longrightarrow> call_of_return_node (ms ! i) (sourcenode (cs ! i))
[PROOF STEP]
with \<open>i < length cs\<close>
[PROOF STATE]
proof (chain)
picking this:
i < length cs
\<forall>c\<in>set cs. valid_edge c
[PROOF STEP]
have "valid_edge (cs!i)"
[PROOF STATE]
proof (prove)
using this:
i < length cs
\<forall>c\<in>set cs. valid_edge c

goal (1 subgoal):
 1. valid_edge (cs ! i)
[PROOF STEP]
by(simp add:all_set_conv_all_nth)
[PROOF STATE]
proof (state)
this:
valid_edge (cs ! i)

goal (1 subgoal):
 1. i < length cs \<Longrightarrow> call_of_return_node (ms ! i) (sourcenode (cs ! i))
[PROOF STEP]
with \<open>valid_edge (rs!i)\<close> \<open>rs!i \<in> get_return_edges (cs!i)\<close> \<open>ms = targetnodes rs\<close>
      \<open>i < length cs\<close> \<open>length rs = length cs\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge (rs ! i)
rs ! i \<in> get_return_edges (cs ! i)
ms = targetnodes rs
i < length cs
length rs = length cs
valid_edge (cs ! i)
[PROOF STEP]
show "call_of_return_node (ms ! i) (sourcenode (cs ! i))"
[PROOF STATE]
proof (prove)
using this:
valid_edge (rs ! i)
rs ! i \<in> get_return_edges (cs ! i)
ms = targetnodes rs
i < length cs
length rs = length cs
valid_edge (cs ! i)

goal (1 subgoal):
 1. call_of_return_node (ms ! i) (sourcenode (cs ! i))
[PROOF STEP]
by(fastforce simp:call_of_return_node_def return_node_def targetnodes_def)
[PROOF STATE]
proof (state)
this:
call_of_return_node (ms ! i) (sourcenode (cs ! i))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i < length cs \<longrightarrow> call_of_return_node (ms ! i) (sourcenode (cs ! i))

goal:
No subgoals!
[PROOF STEP]
qed