[STATEMENT]
lemma weakBisimScopeExtChainSym:
  fixes xvec :: "name list"
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"

  assumes "xvec \<sharp>* \<Psi>"
  and     "xvec \<sharp>* Q"

  shows "\<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>(P \<parallel> Q) \<approx> (\<lparr>\<nu>*xvec\<rparr>P) \<parallel> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<parallel> Q \<approx> (\<lparr>\<nu>*xvec\<rparr>P) \<parallel> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xvec \<sharp>* \<Psi>
xvec \<sharp>* Q

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<parallel> Q \<approx> (\<lparr>\<nu>*xvec\<rparr>P) \<parallel> Q
[PROOF STEP]
by(induct xvec) (auto intro: weakBisimScopeExtSym weakBisimReflexive weakBisimTransitive weakBisimResPres)