[STATEMENT]
lemma resActRight:
  fixes x :: name
  and   \<alpha> :: act
  and   P :: ccs

  assumes "x \<sharp> \<alpha>"
  and     "Id \<subseteq> Rel"

  shows "\<alpha>.(\<lparr>\<nu>x\<rparr>P) \<leadsto>[Rel] \<lparr>\<nu>x\<rparr>(\<alpha>.(P))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha>.(\<lparr>\<nu>x\<rparr>P) \<leadsto>[Rel] \<lparr>\<nu>x\<rparr>\<alpha>.P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<sharp> \<alpha>
Id \<subseteq> Rel

goal (1 subgoal):
 1. \<alpha>.(\<lparr>\<nu>x\<rparr>P) \<leadsto>[Rel] \<lparr>\<nu>x\<rparr>\<alpha>.P
[PROOF STEP]
by(fastforce simp add: simulation_def elim: resCases actCases intro: Action)