[STATEMENT]
lemma silent_moves_preserves_stacks:
  assumes "S,f \<turnstile> (m#ms,s) =as\<Rightarrow>\<^sub>\<tau> (m'#ms',s')"
  and "valid_node m" and "valid_call_list cs m"
  and "\<forall>i < length rs. rs!i \<in> get_return_edges (cs!i)" and "valid_return_list rs m"
  and "length rs = length cs" and "ms = targetnodes rs"
  obtains cs' rs' where "valid_node m'" and "valid_call_list cs' m'"
  and "\<forall>i < length rs'. rs'!i \<in> get_return_edges (cs'!i)"
  and "valid_return_list rs' m'" and "length rs' = length cs'"
  and "ms' = targetnodes rs'" and "upd_cs cs as = cs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>cs' rs'. \<lbrakk>valid_node m'; valid_call_list cs' m'; \<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i); valid_return_list rs' m'; length rs' = length cs'; ms' = targetnodes rs'; upd_cs cs as = cs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs as = cs'
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
valid_node m
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs
[PROOF STEP]
show "\<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and>
    (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and>
    valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and>
    upd_cs cs as = cs'"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s')
valid_node m
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs

goal (1 subgoal):
 1. \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs as = cs'
[PROOF STEP]
proof(induct S f "m#ms" s as "m'#ms'" s'
      arbitrary:m ms cs rs rule:silent_moves.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s S f cs rs. \<lbrakk>length (m' # ms') = length s; valid_node m'; valid_call_list cs m'; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m'; length rs = length cs; ms' = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [] = cs'
 2. \<And>S f s a ms'a s' as s'' m ms cs rs. \<lbrakk>S,f \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'a,s'); S,f \<turnstile> (ms'a,s') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs as = cs'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs (a # as) = cs'
[PROOF STEP]
case (silent_moves_Nil s n\<^sub>c f)
[PROOF STATE]
proof (state)
this:
length (m' # ms') = length s
valid_node m'
valid_call_list cs m'
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m'
length rs = length cs
ms' = targetnodes rs

goal (2 subgoals):
 1. \<And>s S f cs rs. \<lbrakk>length (m' # ms') = length s; valid_node m'; valid_call_list cs m'; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m'; length rs = length cs; ms' = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [] = cs'
 2. \<And>S f s a ms'a s' as s'' m ms cs rs. \<lbrakk>S,f \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'a,s'); S,f \<turnstile> (ms'a,s') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs as = cs'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs (a # as) = cs'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
length (m' # ms') = length s
valid_node m'
valid_call_list cs m'
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m'
length rs = length cs
ms' = targetnodes rs

goal (1 subgoal):
 1. \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [] = cs'
[PROOF STEP]
apply(rule_tac x="cs" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length (m' # ms') = length s; valid_node m'; valid_call_list cs m'; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m'; length rs = length cs; ms' = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>rs'. valid_node m' \<and> valid_call_list cs m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs \<and> ms' = targetnodes rs' \<and> upd_cs cs [] = cs
[PROOF STEP]
apply(rule_tac x="rs" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length (m' # ms') = length s; valid_node m'; valid_call_list cs m'; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m'; length rs = length cs; ms' = targetnodes rs\<rbrakk> \<Longrightarrow> valid_node m' \<and> valid_call_list cs m' \<and> (\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)) \<and> valid_return_list rs m' \<and> length rs = length cs \<and> ms' = targetnodes rs \<and> upd_cs cs [] = cs
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
\<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs [] = cs'

goal (1 subgoal):
 1. \<And>S f s a ms'a s' as s'' m ms cs rs. \<lbrakk>S,f \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'a,s'); S,f \<turnstile> (ms'a,s') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs as = cs'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs (a # as) = cs'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S f s a ms'a s' as s'' m ms cs rs. \<lbrakk>S,f \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'a,s'); S,f \<turnstile> (ms'a,s') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs as = cs'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs (a # as) = cs'
[PROOF STEP]
case (silent_moves_Cons S f s a msx'' s'' as sx')
[PROOF STATE]
proof (state)
this:
S,f \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (msx'',s'')
S,f \<turnstile> (msx'',s'') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',sx')
\<lbrakk>msx'' = ?m # ?ms; valid_node ?m; valid_call_list ?cs ?m; \<forall>i<length ?rs. ?rs ! i \<in> get_return_edges (?cs ! i); valid_return_list ?rs ?m; length ?rs = length ?cs; ?ms = targetnodes ?rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs ?cs as = cs'
valid_node m
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs

goal (1 subgoal):
 1. \<And>S f s a ms'a s' as s'' m ms cs rs. \<lbrakk>S,f \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'a,s'); S,f \<turnstile> (ms'a,s') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs as = cs'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs (a # as) = cs'
[PROOF STEP]
note IH = \<open>\<And>m ms cs rs. \<lbrakk>msx'' = m # ms; valid_node m; valid_call_list cs m;
      \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i);
      valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk>
      \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and>
      (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and>
      valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and>
      upd_cs cs as = cs'\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>msx'' = ?m # ?ms; valid_node ?m; valid_call_list ?cs ?m; \<forall>i<length ?rs. ?rs ! i \<in> get_return_edges (?cs ! i); valid_return_list ?rs ?m; length ?rs = length ?cs; ?ms = targetnodes ?rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs ?cs as = cs'

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

goal (1 subgoal):
 1. (\<And>m'' ms''. msx'' = m'' # ms'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(cases msx'')(auto elim:silent_move.cases)
[PROOF STATE]
proof (state)
this:
msx'' = m'' # ms''

goal (1 subgoal):
 1. \<And>S f s a ms'a s' as s'' m ms cs rs. \<lbrakk>S,f \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'a,s'); S,f \<turnstile> (ms'a,s') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs as = cs'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs (a # as) = cs'
[PROOF STEP]
with \<open>S,f \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (msx'',s'')\<close> \<open>valid_call_list cs m\<close>
      \<open>\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)\<close> \<open>valid_return_list rs m\<close>
      \<open>length rs = length cs\<close> \<open>ms = targetnodes rs\<close>
[PROOF STATE]
proof (chain)
picking this:
S,f \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (msx'',s'')
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs
msx'' = m'' # ms''
[PROOF STEP]
obtain cs'' rs'' where hyps:"valid_node m''" "valid_call_list cs'' m''"
      "\<forall>i < length rs''. rs''!i \<in> get_return_edges (cs''!i)"
      "valid_return_list rs'' m''" "length rs'' = length cs''"
      "ms'' = targetnodes rs''" and "upd_cs cs [a] = cs''"
[PROOF STATE]
proof (prove)
using this:
S,f \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (msx'',s'')
valid_call_list cs m
\<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i)
valid_return_list rs m
length rs = length cs
ms = targetnodes rs
msx'' = m'' # ms''

goal (1 subgoal):
 1. (\<And>cs'' rs''. \<lbrakk>valid_node m''; valid_call_list cs'' m''; \<forall>i<length rs''. rs'' ! i \<in> get_return_edges (cs'' ! i); valid_return_list rs'' m''; length rs'' = length cs''; ms'' = targetnodes rs''; upd_cs cs [a] = cs''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto elim!:silent_move_preserves_stacks)
[PROOF STATE]
proof (state)
this:
valid_node m''
valid_call_list cs'' m''
\<forall>i<length rs''. rs'' ! i \<in> get_return_edges (cs'' ! i)
valid_return_list rs'' m''
length rs'' = length cs''
ms'' = targetnodes rs''
upd_cs cs [a] = cs''

goal (1 subgoal):
 1. \<And>S f s a ms'a s' as s'' m ms cs rs. \<lbrakk>S,f \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'a,s'); S,f \<turnstile> (ms'a,s') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs as = cs'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs (a # as) = cs'
[PROOF STEP]
from IH[OF _ hyps] \<open>msx'' = m'' # ms''\<close>
[PROOF STATE]
proof (chain)
picking this:
msx'' = m'' # ms'' \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs'' as = cs'
msx'' = m'' # ms''
[PROOF STEP]
obtain cs' rs' where results:"valid_node m'" "valid_call_list cs' m'"
      "\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)"
      "valid_return_list rs' m'" "length rs' = length cs'" "ms' = targetnodes rs'"
      and "upd_cs cs'' as = cs'"
[PROOF STATE]
proof (prove)
using this:
msx'' = m'' # ms'' \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs'' as = cs'
msx'' = m'' # ms''

goal (1 subgoal):
 1. (\<And>cs' rs'. \<lbrakk>valid_node m'; valid_call_list cs' m'; \<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i); valid_return_list rs' m'; length rs' = length cs'; ms' = targetnodes rs'; upd_cs cs'' as = cs'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
valid_node m'
valid_call_list cs' m'
\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)
valid_return_list rs' m'
length rs' = length cs'
ms' = targetnodes rs'
upd_cs cs'' as = cs'

goal (1 subgoal):
 1. \<And>S f s a ms'a s' as s'' m ms cs rs. \<lbrakk>S,f \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'a,s'); S,f \<turnstile> (ms'a,s') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs as = cs'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs (a # as) = cs'
[PROOF STEP]
from \<open>upd_cs cs [a] = cs''\<close> \<open>upd_cs cs'' as = cs'\<close>
[PROOF STATE]
proof (chain)
picking this:
upd_cs cs [a] = cs''
upd_cs cs'' as = cs'
[PROOF STEP]
have "upd_cs cs ([a] @ as) = cs'"
[PROOF STATE]
proof (prove)
using this:
upd_cs cs [a] = cs''
upd_cs cs'' as = cs'

goal (1 subgoal):
 1. upd_cs cs ([a] @ as) = cs'
[PROOF STEP]
by(rule upd_cs_Append)
[PROOF STATE]
proof (state)
this:
upd_cs cs ([a] @ as) = cs'

goal (1 subgoal):
 1. \<And>S f s a ms'a s' as s'' m ms cs rs. \<lbrakk>S,f \<turnstile> (m # ms,s) -a\<rightarrow>\<^sub>\<tau> (ms'a,s'); S,f \<turnstile> (ms'a,s') =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s''); \<And>m ms cs rs. \<lbrakk>ms'a = m # ms; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs as = cs'; valid_node m; valid_call_list cs m; \<forall>i<length rs. rs ! i \<in> get_return_edges (cs ! i); valid_return_list rs m; length rs = length cs; ms = targetnodes rs\<rbrakk> \<Longrightarrow> \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs (a # as) = cs'
[PROOF STEP]
with results
[PROOF STATE]
proof (chain)
picking this:
valid_node m'
valid_call_list cs' m'
\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)
valid_return_list rs' m'
length rs' = length cs'
ms' = targetnodes rs'
upd_cs cs ([a] @ as) = cs'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
valid_node m'
valid_call_list cs' m'
\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)
valid_return_list rs' m'
length rs' = length cs'
ms' = targetnodes rs'
upd_cs cs ([a] @ as) = cs'

goal (1 subgoal):
 1. \<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs (a # as) = cs'
[PROOF STEP]
apply(rule_tac x="cs'" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_node m'; valid_call_list cs' m'; \<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i); valid_return_list rs' m'; length rs' = length cs'; ms' = targetnodes rs'; upd_cs cs ([a] @ as) = cs'\<rbrakk> \<Longrightarrow> \<exists>rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs (a # as) = cs'
[PROOF STEP]
apply(rule_tac x="rs'" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_node m'; valid_call_list cs' m'; \<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i); valid_return_list rs' m'; length rs' = length cs'; ms' = targetnodes rs'; upd_cs cs ([a] @ as) = cs'\<rbrakk> \<Longrightarrow> valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs (a # as) = cs'
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
\<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs (a # as) = cs'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>cs' rs'. valid_node m' \<and> valid_call_list cs' m' \<and> (\<forall>i<length rs'. rs' ! i \<in> get_return_edges (cs' ! i)) \<and> valid_return_list rs' m' \<and> length rs' = length cs' \<and> ms' = targetnodes rs' \<and> upd_cs cs as = cs'

goal:
No subgoals!
[PROOF STEP]
qed