[STATEMENT]
lemma init_fin_silent_movesD:
  assumes "\<tau>trsys.silent_moves (init_fin t) init_fin_\<tau>move ((s, x), m) ((s', x'), m')"
  shows "silent_moves t (x, m) (x', m') \<and> s = s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. silent_moves t (x, m) (x', m') \<and> s = s'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<tau>trsys.silent_move (init_fin t) init_fin_\<tau>move)\<^sup>*\<^sup>* ((s, x), m) ((s', x'), m')

goal (1 subgoal):
 1. silent_moves t (x, m) (x', m') \<and> s = s'
[PROOF STEP]
by(induct "((s, x), m)" "((s', x'), m')" arbitrary: s' x' m')
  (auto 7 2 simp only: dest!: init_fin_silent_moveD intro: rtranclp.rtrancl_into_rtrancl)