[STATEMENT]
lemma sumAssoc:
  fixes P :: pi
  and   Q :: pi
  and   R :: pi
  
  shows "(P \<oplus> Q) \<oplus> R \<simeq> P \<oplus> (Q \<oplus> R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<oplus> Q) \<oplus> R \<simeq> P \<oplus> Q \<oplus> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (P \<oplus> Q) \<oplus> R \<simeq> P \<oplus> Q \<oplus> R
[PROOF STEP]
have "(P \<oplus> Q) \<oplus> R \<sim> P \<oplus> (Q \<oplus> R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<oplus> Q) \<oplus> R \<sim> P \<oplus> Q \<oplus> R
[PROOF STEP]
by(rule Strong_Late_Bisim_SC.sumAssoc)
[PROOF STATE]
proof (state)
this:
(P \<oplus> Q) \<oplus> R \<sim> P \<oplus> Q \<oplus> R

goal (1 subgoal):
 1. (P \<oplus> Q) \<oplus> R \<simeq> P \<oplus> Q \<oplus> R
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(P \<oplus> Q) \<oplus> R \<sim> P \<oplus> Q \<oplus> R

goal (1 subgoal):
 1. (P \<oplus> Q) \<oplus> R \<simeq> P \<oplus> Q \<oplus> R
[PROOF STEP]
by(rule strongBisimWeakEq)
[PROOF STATE]
proof (state)
this:
(P \<oplus> Q) \<oplus> R \<simeq> P \<oplus> Q \<oplus> R

goal:
No subgoals!
[PROOF STEP]
qed