[STATEMENT]
lemma silent_moves_slp:
  "\<lbrakk>S,f \<turnstile> (m#ms,s) =as\<Rightarrow>\<^sub>\<tau> (m'#ms',s'); valid_node m;
  \<forall>mx \<in> set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>;
  \<forall>mx \<in> set ms'. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk>
  \<Longrightarrow> m -as\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> ms = ms'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S,f \<turnstile> (m # ms,s) =as\<Rightarrow>\<^sub>\<tau> (m' # ms',s'); valid_node m; \<forall>mx\<in>set ms. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; \<forall>mx\<in>set ms'. \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<rbrakk> \<Longrightarrow> m -as\<rightarrow>\<^bsub>sl\<^esub>* m' \<and> ms = ms'
[PROOF STEP]
by(fastforce dest!:silent_moves_slpa_path
                   [of _ _ _ "[]" _ _ _ _ _ _ "[]" "[]",simplified]
              simp:targetnodes_def valid_call_list_def valid_return_list_def
                   same_level_path_def slp_def)