Welcome to Abella 2.0.3-dev

Abella < Kind name, action, proc type.

Abella < Import "ccs_core".
Importing from ccs_core
Warning: Definition can be used to defeat stratification
  (higher-order argument "Tech" occurs to the left of ->)
Warning: Definition can be used to defeat stratification
  (higher-order argument "Rel" occurs to the left of ->)
Warning: Definition can be used to defeat stratification
  (higher-order argument "Rel" occurs to the left of ->)

Abella < Import "ccs_ctx".
Importing from ccs_ctx
Warning: Definition can be used to defeat stratification
  (higher-order argument "Rel" occurs to the left of ->)

Abella < Type a, b, c, d name.

Abella < Theorem bisim_par_null : 
forall P, bisim_up_to refl_t (par P null) P.

============================
 forall P, bisim_up_to refl_t (par P null) P

bisim_par_null < coinduction.

CH : forall P, bisim_up_to refl_t (par P null) P +
============================
 forall P, bisim_up_to refl_t (par P null) P #

bisim_par_null < intros.

Variables: P
CH : forall P, bisim_up_to refl_t (par P null) P +
============================
 bisim_up_to refl_t (par P null) P #

bisim_par_null < unfold.

Subgoal 1:

Variables: P
CH : forall P, bisim_up_to refl_t (par P null) P +
============================
 forall A P1, one (par P null) A P1 ->
   (exists Q1, one P A Q1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one (par P null) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_null < intros.

Subgoal 1:

Variables: P A P1
CH : forall P, bisim_up_to refl_t (par P null) P +
H1 : one (par P null) A P1
============================
 exists Q1, one P A Q1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one (par P null) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_null < case H1.

Subgoal 1.1:

Variables: P A P3
CH : forall P, bisim_up_to refl_t (par P null) P +
H2 : one P A P3
============================
 exists Q1, one P A Q1 /\
   (exists P2 Q2, refl_t (par P3 null) P2 Q1 Q2 /\
      bisim_up_to refl_t P2 Q2 +)

Subgoal 1.2 is:
 exists Q2, one P A Q2 /\
   (exists P2 Q3, refl_t (par P Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q2, one P tau Q2 /\
   (exists P2 Q3, refl_t (par P3 Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q2, one P tau Q2 /\
   (exists P2 Q3, refl_t (par P3 Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one (par P null) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_null < witness P3.

Subgoal 1.1:

Variables: P A P3
CH : forall P, bisim_up_to refl_t (par P null) P +
H2 : one P A P3
============================
 one P A P3 /\
   (exists P2 Q2, refl_t (par P3 null) P2 P3 Q2 /\
      bisim_up_to refl_t P2 Q2 +)

Subgoal 1.2 is:
 exists Q2, one P A Q2 /\
   (exists P2 Q3, refl_t (par P Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q2, one P tau Q2 /\
   (exists P2 Q3, refl_t (par P3 Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q2, one P tau Q2 /\
   (exists P2 Q3, refl_t (par P3 Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one (par P null) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_null < split.

Subgoal 1.1.1:

Variables: P A P3
CH : forall P, bisim_up_to refl_t (par P null) P +
H2 : one P A P3
============================
 one P A P3

Subgoal 1.1.2 is:
 exists P2 Q2, refl_t (par P3 null) P2 P3 Q2 /\ bisim_up_to refl_t P2 Q2 +

Subgoal 1.2 is:
 exists Q2, one P A Q2 /\
   (exists P2 Q3, refl_t (par P Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q2, one P tau Q2 /\
   (exists P2 Q3, refl_t (par P3 Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q2, one P tau Q2 /\
   (exists P2 Q3, refl_t (par P3 Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one (par P null) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_null < search.

Subgoal 1.1.2:

Variables: P A P3
CH : forall P, bisim_up_to refl_t (par P null) P +
H2 : one P A P3
============================
 exists P2 Q2, refl_t (par P3 null) P2 P3 Q2 /\ bisim_up_to refl_t P2 Q2 +

Subgoal 1.2 is:
 exists Q2, one P A Q2 /\
   (exists P2 Q3, refl_t (par P Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q2, one P tau Q2 /\
   (exists P2 Q3, refl_t (par P3 Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q2, one P tau Q2 /\
   (exists P2 Q3, refl_t (par P3 Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one (par P null) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_null < witness par P3 null.

Subgoal 1.1.2:

Variables: P A P3
CH : forall P, bisim_up_to refl_t (par P null) P +
H2 : one P A P3
============================
 exists Q2, refl_t (par P3 null) (par P3 null) P3 Q2 /\
   bisim_up_to refl_t (par P3 null) Q2 +

Subgoal 1.2 is:
 exists Q2, one P A Q2 /\
   (exists P2 Q3, refl_t (par P Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q2, one P tau Q2 /\
   (exists P2 Q3, refl_t (par P3 Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q2, one P tau Q2 /\
   (exists P2 Q3, refl_t (par P3 Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one (par P null) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_null < witness P3.

Subgoal 1.1.2:

Variables: P A P3
CH : forall P, bisim_up_to refl_t (par P null) P +
H2 : one P A P3
============================
 refl_t (par P3 null) (par P3 null) P3 P3 /\
   bisim_up_to refl_t (par P3 null) P3 +

Subgoal 1.2 is:
 exists Q2, one P A Q2 /\
   (exists P2 Q3, refl_t (par P Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q2, one P tau Q2 /\
   (exists P2 Q3, refl_t (par P3 Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q2, one P tau Q2 /\
   (exists P2 Q3, refl_t (par P3 Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one (par P null) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_null < split.

Subgoal 1.1.2.1:

Variables: P A P3
CH : forall P, bisim_up_to refl_t (par P null) P +
H2 : one P A P3
============================
 refl_t (par P3 null) (par P3 null) P3 P3

Subgoal 1.1.2.2 is:
 bisim_up_to refl_t (par P3 null) P3 +

Subgoal 1.2 is:
 exists Q2, one P A Q2 /\
   (exists P2 Q3, refl_t (par P Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q2, one P tau Q2 /\
   (exists P2 Q3, refl_t (par P3 Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q2, one P tau Q2 /\
   (exists P2 Q3, refl_t (par P3 Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one (par P null) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_null < search.

Subgoal 1.1.2.2:

Variables: P A P3
CH : forall P, bisim_up_to refl_t (par P null) P +
H2 : one P A P3
============================
 bisim_up_to refl_t (par P3 null) P3 +

Subgoal 1.2 is:
 exists Q2, one P A Q2 /\
   (exists P2 Q3, refl_t (par P Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q2, one P tau Q2 /\
   (exists P2 Q3, refl_t (par P3 Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q2, one P tau Q2 /\
   (exists P2 Q3, refl_t (par P3 Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one (par P null) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_null < backchain CH.

Subgoal 1.2:

Variables: P A Q1
CH : forall P, bisim_up_to refl_t (par P null) P +
H2 : one null A Q1
============================
 exists Q2, one P A Q2 /\
   (exists P2 Q3, refl_t (par P Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q2, one P tau Q2 /\
   (exists P2 Q3, refl_t (par P3 Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q2, one P tau Q2 /\
   (exists P2 Q3, refl_t (par P3 Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one (par P null) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_null < case H2.

Subgoal 1.3:

Variables: P X Q1 P3
CH : forall P, bisim_up_to refl_t (par P null) P +
H2 : one P (up X) P3
H3 : one null (dn X) Q1
============================
 exists Q2, one P tau Q2 /\
   (exists P2 Q3, refl_t (par P3 Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q2, one P tau Q2 /\
   (exists P2 Q3, refl_t (par P3 Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one (par P null) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_null < case H3.

Subgoal 1.4:

Variables: P X Q1 P3
CH : forall P, bisim_up_to refl_t (par P null) P +
H2 : one P (dn X) P3
H3 : one null (up X) Q1
============================
 exists Q2, one P tau Q2 /\
   (exists P2 Q3, refl_t (par P3 Q1) P2 Q2 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one P A Q1 ->
   (exists P1, one (par P null) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_null < case H3.

Subgoal 2:

Variables: P
CH : forall P, bisim_up_to refl_t (par P null) P +
============================
 forall A Q1, one P A Q1 ->
   (exists P1, one (par P null) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_null < intros.

Subgoal 2:

Variables: P A Q1
CH : forall P, bisim_up_to refl_t (par P null) P +
H1 : one P A Q1
============================
 exists P1, one (par P null) A P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_par_null < witness par Q1 null.

Subgoal 2:

Variables: P A Q1
CH : forall P, bisim_up_to refl_t (par P null) P +
H1 : one P A Q1
============================
 one (par P null) A (par Q1 null) /\
   (exists P2 Q2, refl_t (par Q1 null) P2 Q1 Q2 /\
      bisim_up_to refl_t P2 Q2 +)

bisim_par_null < split.

Subgoal 2.1:

Variables: P A Q1
CH : forall P, bisim_up_to refl_t (par P null) P +
H1 : one P A Q1
============================
 one (par P null) A (par Q1 null)

Subgoal 2.2 is:
 exists P2 Q2, refl_t (par Q1 null) P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +

bisim_par_null < search.

Subgoal 2.2:

Variables: P A Q1
CH : forall P, bisim_up_to refl_t (par P null) P +
H1 : one P A Q1
============================
 exists P2 Q2, refl_t (par Q1 null) P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +

bisim_par_null < witness par Q1 null.

Subgoal 2.2:

Variables: P A Q1
CH : forall P, bisim_up_to refl_t (par P null) P +
H1 : one P A Q1
============================
 exists Q2, refl_t (par Q1 null) (par Q1 null) Q1 Q2 /\
   bisim_up_to refl_t (par Q1 null) Q2 +

bisim_par_null < witness Q1.

Subgoal 2.2:

Variables: P A Q1
CH : forall P, bisim_up_to refl_t (par P null) P +
H1 : one P A Q1
============================
 refl_t (par Q1 null) (par Q1 null) Q1 Q1 /\
   bisim_up_to refl_t (par Q1 null) Q1 +

bisim_par_null < split.

Subgoal 2.2.1:

Variables: P A Q1
CH : forall P, bisim_up_to refl_t (par P null) P +
H1 : one P A Q1
============================
 refl_t (par Q1 null) (par Q1 null) Q1 Q1

Subgoal 2.2.2 is:
 bisim_up_to refl_t (par Q1 null) Q1 +

bisim_par_null < search.

Subgoal 2.2.2:

Variables: P A Q1
CH : forall P, bisim_up_to refl_t (par P null) P +
H1 : one P A Q1
============================
 bisim_up_to refl_t (par Q1 null) Q1 +

bisim_par_null < backchain CH.
Proof completed.

Abella < Theorem bisim_par_comm : 
forall P Q, bisim_up_to refl_t (par P Q) (par Q P).

============================
 forall P Q, bisim_up_to refl_t (par P Q) (par Q P)

bisim_par_comm < coinduction.

CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
============================
 forall P Q, bisim_up_to refl_t (par P Q) (par Q P) #

bisim_par_comm < intros.

Variables: P Q
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
============================
 bisim_up_to refl_t (par P Q) (par Q P) #

bisim_par_comm < unfold.

Subgoal 1:

Variables: P Q
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
============================
 forall A P1, one (par P Q) A P1 ->
   (exists Q1, one (par Q P) A Q1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < intros.

Subgoal 1:

Variables: P Q A P1
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H1 : one (par P Q) A P1
============================
 exists Q1, one (par Q P) A Q1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < case H1.

Subgoal 1.1:

Variables: P Q A P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P A P3
============================
 exists Q1, one (par Q P) A Q1 /\
   (exists P2 Q2, refl_t (par P3 Q) P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 1.2 is:
 exists Q1, one (par Q P) A Q1 /\
   (exists P2 Q3, refl_t (par P Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < witness par Q P3.

Subgoal 1.1:

Variables: P Q A P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P A P3
============================
 one (par Q P) A (par Q P3) /\
   (exists P2 Q2, refl_t (par P3 Q) P2 (par Q P3) Q2 /\
      bisim_up_to refl_t P2 Q2 +)

Subgoal 1.2 is:
 exists Q1, one (par Q P) A Q1 /\
   (exists P2 Q3, refl_t (par P Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < split.

Subgoal 1.1.1:

Variables: P Q A P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P A P3
============================
 one (par Q P) A (par Q P3)

Subgoal 1.1.2 is:
 exists P2 Q2, refl_t (par P3 Q) P2 (par Q P3) Q2 /\
   bisim_up_to refl_t P2 Q2 +

Subgoal 1.2 is:
 exists Q1, one (par Q P) A Q1 /\
   (exists P2 Q3, refl_t (par P Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < search.

Subgoal 1.1.2:

Variables: P Q A P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P A P3
============================
 exists P2 Q2, refl_t (par P3 Q) P2 (par Q P3) Q2 /\
   bisim_up_to refl_t P2 Q2 +

Subgoal 1.2 is:
 exists Q1, one (par Q P) A Q1 /\
   (exists P2 Q3, refl_t (par P Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < witness par P3 Q.

Subgoal 1.1.2:

Variables: P Q A P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P A P3
============================
 exists Q2, refl_t (par P3 Q) (par P3 Q) (par Q P3) Q2 /\
   bisim_up_to refl_t (par P3 Q) Q2 +

Subgoal 1.2 is:
 exists Q1, one (par Q P) A Q1 /\
   (exists P2 Q3, refl_t (par P Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < witness par Q P3.

Subgoal 1.1.2:

Variables: P Q A P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P A P3
============================
 refl_t (par P3 Q) (par P3 Q) (par Q P3) (par Q P3) /\
   bisim_up_to refl_t (par P3 Q) (par Q P3) +

Subgoal 1.2 is:
 exists Q1, one (par Q P) A Q1 /\
   (exists P2 Q3, refl_t (par P Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < split.

Subgoal 1.1.2.1:

Variables: P Q A P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P A P3
============================
 refl_t (par P3 Q) (par P3 Q) (par Q P3) (par Q P3)

Subgoal 1.1.2.2 is:
 bisim_up_to refl_t (par P3 Q) (par Q P3) +

Subgoal 1.2 is:
 exists Q1, one (par Q P) A Q1 /\
   (exists P2 Q3, refl_t (par P Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < search.

Subgoal 1.1.2.2:

Variables: P Q A P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P A P3
============================
 bisim_up_to refl_t (par P3 Q) (par Q P3) +

Subgoal 1.2 is:
 exists Q1, one (par Q P) A Q1 /\
   (exists P2 Q3, refl_t (par P Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < backchain CH.

Subgoal 1.2:

Variables: P Q A Q2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q A Q2
============================
 exists Q1, one (par Q P) A Q1 /\
   (exists P2 Q3, refl_t (par P Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < witness par Q2 P.

Subgoal 1.2:

Variables: P Q A Q2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q A Q2
============================
 one (par Q P) A (par Q2 P) /\
   (exists P2 Q3, refl_t (par P Q2) P2 (par Q2 P) Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < split.

Subgoal 1.2.1:

Variables: P Q A Q2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q A Q2
============================
 one (par Q P) A (par Q2 P)

Subgoal 1.2.2 is:
 exists P2 Q3, refl_t (par P Q2) P2 (par Q2 P) Q3 /\
   bisim_up_to refl_t P2 Q3 +

Subgoal 1.3 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < search.

Subgoal 1.2.2:

Variables: P Q A Q2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q A Q2
============================
 exists P2 Q3, refl_t (par P Q2) P2 (par Q2 P) Q3 /\
   bisim_up_to refl_t P2 Q3 +

Subgoal 1.3 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < witness par P Q2.

Subgoal 1.2.2:

Variables: P Q A Q2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q A Q2
============================
 exists Q3, refl_t (par P Q2) (par P Q2) (par Q2 P) Q3 /\
   bisim_up_to refl_t (par P Q2) Q3 +

Subgoal 1.3 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < witness par Q2 P.

Subgoal 1.2.2:

Variables: P Q A Q2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q A Q2
============================
 refl_t (par P Q2) (par P Q2) (par Q2 P) (par Q2 P) /\
   bisim_up_to refl_t (par P Q2) (par Q2 P) +

Subgoal 1.3 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < split.

Subgoal 1.2.2.1:

Variables: P Q A Q2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q A Q2
============================
 refl_t (par P Q2) (par P Q2) (par Q2 P) (par Q2 P)

Subgoal 1.2.2.2 is:
 bisim_up_to refl_t (par P Q2) (par Q2 P) +

Subgoal 1.3 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < search.

Subgoal 1.2.2.2:

Variables: P Q A Q2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q A Q2
============================
 bisim_up_to refl_t (par P Q2) (par Q2 P) +

Subgoal 1.3 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < backchain CH.

Subgoal 1.3:

Variables: P Q X Q2 P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P (up X) P3
H3 : one Q (dn X) Q2
============================
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < witness par Q2 P3.

Subgoal 1.3:

Variables: P Q X Q2 P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P (up X) P3
H3 : one Q (dn X) Q2
============================
 one (par Q P) tau (par Q2 P3) /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 (par Q2 P3) Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < split.

Subgoal 1.3.1:

Variables: P Q X Q2 P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P (up X) P3
H3 : one Q (dn X) Q2
============================
 one (par Q P) tau (par Q2 P3)

Subgoal 1.3.2 is:
 exists P2 Q3, refl_t (par P3 Q2) P2 (par Q2 P3) Q3 /\
   bisim_up_to refl_t P2 Q3 +

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < search.

Subgoal 1.3.2:

Variables: P Q X Q2 P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P (up X) P3
H3 : one Q (dn X) Q2
============================
 exists P2 Q3, refl_t (par P3 Q2) P2 (par Q2 P3) Q3 /\
   bisim_up_to refl_t P2 Q3 +

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < witness par P3 Q2.

Subgoal 1.3.2:

Variables: P Q X Q2 P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P (up X) P3
H3 : one Q (dn X) Q2
============================
 exists Q3, refl_t (par P3 Q2) (par P3 Q2) (par Q2 P3) Q3 /\
   bisim_up_to refl_t (par P3 Q2) Q3 +

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < witness par Q2 P3.

Subgoal 1.3.2:

Variables: P Q X Q2 P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P (up X) P3
H3 : one Q (dn X) Q2
============================
 refl_t (par P3 Q2) (par P3 Q2) (par Q2 P3) (par Q2 P3) /\
   bisim_up_to refl_t (par P3 Q2) (par Q2 P3) +

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < split.

Subgoal 1.3.2.1:

Variables: P Q X Q2 P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P (up X) P3
H3 : one Q (dn X) Q2
============================
 refl_t (par P3 Q2) (par P3 Q2) (par Q2 P3) (par Q2 P3)

Subgoal 1.3.2.2 is:
 bisim_up_to refl_t (par P3 Q2) (par Q2 P3) +

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < search.

Subgoal 1.3.2.2:

Variables: P Q X Q2 P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P (up X) P3
H3 : one Q (dn X) Q2
============================
 bisim_up_to refl_t (par P3 Q2) (par Q2 P3) +

Subgoal 1.4 is:
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < backchain CH.

Subgoal 1.4:

Variables: P Q X Q2 P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P (dn X) P3
H3 : one Q (up X) Q2
============================
 exists Q1, one (par Q P) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < witness par Q2 P3.

Subgoal 1.4:

Variables: P Q X Q2 P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P (dn X) P3
H3 : one Q (up X) Q2
============================
 one (par Q P) tau (par Q2 P3) /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 (par Q2 P3) Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < split.

Subgoal 1.4.1:

Variables: P Q X Q2 P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P (dn X) P3
H3 : one Q (up X) Q2
============================
 one (par Q P) tau (par Q2 P3)

Subgoal 1.4.2 is:
 exists P2 Q3, refl_t (par P3 Q2) P2 (par Q2 P3) Q3 /\
   bisim_up_to refl_t P2 Q3 +

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < search.

Subgoal 1.4.2:

Variables: P Q X Q2 P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P (dn X) P3
H3 : one Q (up X) Q2
============================
 exists P2 Q3, refl_t (par P3 Q2) P2 (par Q2 P3) Q3 /\
   bisim_up_to refl_t P2 Q3 +

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < witness par P3 Q2.

Subgoal 1.4.2:

Variables: P Q X Q2 P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P (dn X) P3
H3 : one Q (up X) Q2
============================
 exists Q3, refl_t (par P3 Q2) (par P3 Q2) (par Q2 P3) Q3 /\
   bisim_up_to refl_t (par P3 Q2) Q3 +

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < witness par Q2 P3.

Subgoal 1.4.2:

Variables: P Q X Q2 P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P (dn X) P3
H3 : one Q (up X) Q2
============================
 refl_t (par P3 Q2) (par P3 Q2) (par Q2 P3) (par Q2 P3) /\
   bisim_up_to refl_t (par P3 Q2) (par Q2 P3) +

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < split.

Subgoal 1.4.2.1:

Variables: P Q X Q2 P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P (dn X) P3
H3 : one Q (up X) Q2
============================
 refl_t (par P3 Q2) (par P3 Q2) (par Q2 P3) (par Q2 P3)

Subgoal 1.4.2.2 is:
 bisim_up_to refl_t (par P3 Q2) (par Q2 P3) +

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < search.

Subgoal 1.4.2.2:

Variables: P Q X Q2 P3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P (dn X) P3
H3 : one Q (up X) Q2
============================
 bisim_up_to refl_t (par P3 Q2) (par Q2 P3) +

Subgoal 2 is:
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < backchain CH.

Subgoal 2:

Variables: P Q
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
============================
 forall A Q1, one (par Q P) A Q1 ->
   (exists P1, one (par P Q) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_comm < intros.

Subgoal 2:

Variables: P Q A Q1
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H1 : one (par Q P) A Q1
============================
 exists P1, one (par P Q) A P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_par_comm < case H1.

Subgoal 2.1:

Variables: P Q A P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q A P2
============================
 exists P1, one (par P Q) A P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 P) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2 is:
 exists P1, one (par P Q) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par Q Q3) Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < witness par P P2.

Subgoal 2.1:

Variables: P Q A P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q A P2
============================
 one (par P Q) A (par P P2) /\
   (exists P3 Q2, refl_t (par P P2) P3 (par P2 P) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2 is:
 exists P1, one (par P Q) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par Q Q3) Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < split.

Subgoal 2.1.1:

Variables: P Q A P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q A P2
============================
 one (par P Q) A (par P P2)

Subgoal 2.1.2 is:
 exists P3 Q2, refl_t (par P P2) P3 (par P2 P) Q2 /\
   bisim_up_to refl_t P3 Q2 +

Subgoal 2.2 is:
 exists P1, one (par P Q) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par Q Q3) Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < search.

Subgoal 2.1.2:

Variables: P Q A P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q A P2
============================
 exists P3 Q2, refl_t (par P P2) P3 (par P2 P) Q2 /\
   bisim_up_to refl_t P3 Q2 +

Subgoal 2.2 is:
 exists P1, one (par P Q) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par Q Q3) Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < witness par P P2.

Subgoal 2.1.2:

Variables: P Q A P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q A P2
============================
 exists Q2, refl_t (par P P2) (par P P2) (par P2 P) Q2 /\
   bisim_up_to refl_t (par P P2) Q2 +

Subgoal 2.2 is:
 exists P1, one (par P Q) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par Q Q3) Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < witness par P2 P.

Subgoal 2.1.2:

Variables: P Q A P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q A P2
============================
 refl_t (par P P2) (par P P2) (par P2 P) (par P2 P) /\
   bisim_up_to refl_t (par P P2) (par P2 P) +

Subgoal 2.2 is:
 exists P1, one (par P Q) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par Q Q3) Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < split.

Subgoal 2.1.2.1:

Variables: P Q A P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q A P2
============================
 refl_t (par P P2) (par P P2) (par P2 P) (par P2 P)

Subgoal 2.1.2.2 is:
 bisim_up_to refl_t (par P P2) (par P2 P) +

Subgoal 2.2 is:
 exists P1, one (par P Q) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par Q Q3) Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < search.

Subgoal 2.1.2.2:

Variables: P Q A P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q A P2
============================
 bisim_up_to refl_t (par P P2) (par P2 P) +

Subgoal 2.2 is:
 exists P1, one (par P Q) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par Q Q3) Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < backchain CH.

Subgoal 2.2:

Variables: P Q A Q3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P A Q3
============================
 exists P1, one (par P Q) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par Q Q3) Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < witness par Q3 Q.

Subgoal 2.2:

Variables: P Q A Q3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P A Q3
============================
 one (par P Q) A (par Q3 Q) /\
   (exists P2 Q2, refl_t (par Q3 Q) P2 (par Q Q3) Q2 /\
      bisim_up_to refl_t P2 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < split.

Subgoal 2.2.1:

Variables: P Q A Q3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P A Q3
============================
 one (par P Q) A (par Q3 Q)

Subgoal 2.2.2 is:
 exists P2 Q2, refl_t (par Q3 Q) P2 (par Q Q3) Q2 /\
   bisim_up_to refl_t P2 Q2 +

Subgoal 2.3 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < search.

Subgoal 2.2.2:

Variables: P Q A Q3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P A Q3
============================
 exists P2 Q2, refl_t (par Q3 Q) P2 (par Q Q3) Q2 /\
   bisim_up_to refl_t P2 Q2 +

Subgoal 2.3 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < witness par Q3 Q.

Subgoal 2.2.2:

Variables: P Q A Q3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P A Q3
============================
 exists Q2, refl_t (par Q3 Q) (par Q3 Q) (par Q Q3) Q2 /\
   bisim_up_to refl_t (par Q3 Q) Q2 +

Subgoal 2.3 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < witness par Q Q3.

Subgoal 2.2.2:

Variables: P Q A Q3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P A Q3
============================
 refl_t (par Q3 Q) (par Q3 Q) (par Q Q3) (par Q Q3) /\
   bisim_up_to refl_t (par Q3 Q) (par Q Q3) +

Subgoal 2.3 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < split.

Subgoal 2.2.2.1:

Variables: P Q A Q3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P A Q3
============================
 refl_t (par Q3 Q) (par Q3 Q) (par Q Q3) (par Q Q3)

Subgoal 2.2.2.2 is:
 bisim_up_to refl_t (par Q3 Q) (par Q Q3) +

Subgoal 2.3 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < search.

Subgoal 2.2.2.2:

Variables: P Q A Q3
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one P A Q3
============================
 bisim_up_to refl_t (par Q3 Q) (par Q Q3) +

Subgoal 2.3 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < backchain CH.

Subgoal 2.3:

Variables: P Q X Q3 P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q (up X) P2
H3 : one P (dn X) Q3
============================
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < witness par Q3 P2.

Subgoal 2.3:

Variables: P Q X Q3 P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q (up X) P2
H3 : one P (dn X) Q3
============================
 one (par P Q) tau (par Q3 P2) /\
   (exists P3 Q2, refl_t (par Q3 P2) P3 (par P2 Q3) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < split.

Subgoal 2.3.1:

Variables: P Q X Q3 P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q (up X) P2
H3 : one P (dn X) Q3
============================
 one (par P Q) tau (par Q3 P2)

Subgoal 2.3.2 is:
 exists P3 Q2, refl_t (par Q3 P2) P3 (par P2 Q3) Q2 /\
   bisim_up_to refl_t P3 Q2 +

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < search.

Subgoal 2.3.2:

Variables: P Q X Q3 P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q (up X) P2
H3 : one P (dn X) Q3
============================
 exists P3 Q2, refl_t (par Q3 P2) P3 (par P2 Q3) Q2 /\
   bisim_up_to refl_t P3 Q2 +

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < witness par Q3 P2.

Subgoal 2.3.2:

Variables: P Q X Q3 P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q (up X) P2
H3 : one P (dn X) Q3
============================
 exists Q2, refl_t (par Q3 P2) (par Q3 P2) (par P2 Q3) Q2 /\
   bisim_up_to refl_t (par Q3 P2) Q2 +

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < witness par P2 Q3.

Subgoal 2.3.2:

Variables: P Q X Q3 P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q (up X) P2
H3 : one P (dn X) Q3
============================
 refl_t (par Q3 P2) (par Q3 P2) (par P2 Q3) (par P2 Q3) /\
   bisim_up_to refl_t (par Q3 P2) (par P2 Q3) +

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < split.

Subgoal 2.3.2.1:

Variables: P Q X Q3 P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q (up X) P2
H3 : one P (dn X) Q3
============================
 refl_t (par Q3 P2) (par Q3 P2) (par P2 Q3) (par P2 Q3)

Subgoal 2.3.2.2 is:
 bisim_up_to refl_t (par Q3 P2) (par P2 Q3) +

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < search.

Subgoal 2.3.2.2:

Variables: P Q X Q3 P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q (up X) P2
H3 : one P (dn X) Q3
============================
 bisim_up_to refl_t (par Q3 P2) (par P2 Q3) +

Subgoal 2.4 is:
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < backchain CH.

Subgoal 2.4:

Variables: P Q X Q3 P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q (dn X) P2
H3 : one P (up X) Q3
============================
 exists P1, one (par P Q) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < witness par Q3 P2.

Subgoal 2.4:

Variables: P Q X Q3 P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q (dn X) P2
H3 : one P (up X) Q3
============================
 one (par P Q) tau (par Q3 P2) /\
   (exists P3 Q2, refl_t (par Q3 P2) P3 (par P2 Q3) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

bisim_par_comm < split.

Subgoal 2.4.1:

Variables: P Q X Q3 P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q (dn X) P2
H3 : one P (up X) Q3
============================
 one (par P Q) tau (par Q3 P2)

Subgoal 2.4.2 is:
 exists P3 Q2, refl_t (par Q3 P2) P3 (par P2 Q3) Q2 /\
   bisim_up_to refl_t P3 Q2 +

bisim_par_comm < search.

Subgoal 2.4.2:

Variables: P Q X Q3 P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q (dn X) P2
H3 : one P (up X) Q3
============================
 exists P3 Q2, refl_t (par Q3 P2) P3 (par P2 Q3) Q2 /\
   bisim_up_to refl_t P3 Q2 +

bisim_par_comm < witness par Q3 P2.

Subgoal 2.4.2:

Variables: P Q X Q3 P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q (dn X) P2
H3 : one P (up X) Q3
============================
 exists Q2, refl_t (par Q3 P2) (par Q3 P2) (par P2 Q3) Q2 /\
   bisim_up_to refl_t (par Q3 P2) Q2 +

bisim_par_comm < witness par P2 Q3.

Subgoal 2.4.2:

Variables: P Q X Q3 P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q (dn X) P2
H3 : one P (up X) Q3
============================
 refl_t (par Q3 P2) (par Q3 P2) (par P2 Q3) (par P2 Q3) /\
   bisim_up_to refl_t (par Q3 P2) (par P2 Q3) +

bisim_par_comm < split.

Subgoal 2.4.2.1:

Variables: P Q X Q3 P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q (dn X) P2
H3 : one P (up X) Q3
============================
 refl_t (par Q3 P2) (par Q3 P2) (par P2 Q3) (par P2 Q3)

Subgoal 2.4.2.2 is:
 bisim_up_to refl_t (par Q3 P2) (par P2 Q3) +

bisim_par_comm < search.

Subgoal 2.4.2.2:

Variables: P Q X Q3 P2
CH : forall P Q, bisim_up_to refl_t (par P Q) (par Q P) +
H2 : one Q (dn X) P2
H3 : one P (up X) Q3
============================
 bisim_up_to refl_t (par Q3 P2) (par P2 Q3) +

bisim_par_comm < backchain CH.
Proof completed.

Abella < Theorem bisim_par_assoc : 
forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)).

============================
 forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R))

bisim_par_assoc < coinduction.

CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
============================
 forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) #

bisim_par_assoc < intros.

Variables: P Q R
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
============================
 bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) #

bisim_par_assoc < unfold.

Subgoal 1:

Variables: P Q R
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
============================
 forall A P1, one (par (par P Q) R) A P1 ->
   (exists Q1, one (par P (par Q R)) A Q1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < intros.

Subgoal 1:

Variables: P Q R A P1
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H1 : one (par (par P Q) R) A P1
============================
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < case H1.

Subgoal 1.1:

Variables: P Q R A P3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one (par P Q) A P3
============================
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q2, refl_t (par P3 R) P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < case H2.

Subgoal 1.1.1:

Variables: P Q R A P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P A P4
============================
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q2, refl_t (par (par P4 Q) R) P2 Q1 Q2 /\
      bisim_up_to refl_t P2 Q2 +)

Subgoal 1.1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par P4 (par Q R).

Subgoal 1.1.1:

Variables: P Q R A P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P A P4
============================
 one (par P (par Q R)) A (par P4 (par Q R)) /\
   (exists P2 Q2, refl_t (par (par P4 Q) R) P2 (par P4 (par Q R)) Q2 /\
      bisim_up_to refl_t P2 Q2 +)

Subgoal 1.1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < split.

Subgoal 1.1.1.1:

Variables: P Q R A P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P A P4
============================
 one (par P (par Q R)) A (par P4 (par Q R))

Subgoal 1.1.1.2 is:
 exists P2 Q2, refl_t (par (par P4 Q) R) P2 (par P4 (par Q R)) Q2 /\
   bisim_up_to refl_t P2 Q2 +

Subgoal 1.1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < search.

Subgoal 1.1.1.2:

Variables: P Q R A P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P A P4
============================
 exists P2 Q2, refl_t (par (par P4 Q) R) P2 (par P4 (par Q R)) Q2 /\
   bisim_up_to refl_t P2 Q2 +

Subgoal 1.1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par (par P4 Q) R.

Subgoal 1.1.1.2:

Variables: P Q R A P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P A P4
============================
 exists Q2, refl_t (par (par P4 Q) R) (par (par P4 Q) R) (par P4 (par Q R))
              Q2 /\
   bisim_up_to refl_t (par (par P4 Q) R) Q2 +

Subgoal 1.1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par P4 (par Q R).

Subgoal 1.1.1.2:

Variables: P Q R A P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P A P4
============================
 refl_t (par (par P4 Q) R) (par (par P4 Q) R) (par P4 (par Q R))
   (par P4 (par Q R)) /\
   bisim_up_to refl_t (par (par P4 Q) R) (par P4 (par Q R)) +

Subgoal 1.1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < split.

Subgoal 1.1.1.2.1:

Variables: P Q R A P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P A P4
============================
 refl_t (par (par P4 Q) R) (par (par P4 Q) R) (par P4 (par Q R))
   (par P4 (par Q R))

Subgoal 1.1.1.2.2 is:
 bisim_up_to refl_t (par (par P4 Q) R) (par P4 (par Q R)) +

Subgoal 1.1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < search.

Subgoal 1.1.1.2.2:

Variables: P Q R A P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P A P4
============================
 bisim_up_to refl_t (par (par P4 Q) R) (par P4 (par Q R)) +

Subgoal 1.1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < backchain CH.

Subgoal 1.1.2:

Variables: P Q R A Q2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q A Q2
============================
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par P (par Q2 R).

Subgoal 1.1.2:

Variables: P Q R A Q2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q A Q2
============================
 one (par P (par Q R)) A (par P (par Q2 R)) /\
   (exists P2 Q3, refl_t (par (par P Q2) R) P2 (par P (par Q2 R)) Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < split.

Subgoal 1.1.2.1:

Variables: P Q R A Q2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q A Q2
============================
 one (par P (par Q R)) A (par P (par Q2 R))

Subgoal 1.1.2.2 is:
 exists P2 Q3, refl_t (par (par P Q2) R) P2 (par P (par Q2 R)) Q3 /\
   bisim_up_to refl_t P2 Q3 +

Subgoal 1.1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < search.

Subgoal 1.1.2.2:

Variables: P Q R A Q2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q A Q2
============================
 exists P2 Q3, refl_t (par (par P Q2) R) P2 (par P (par Q2 R)) Q3 /\
   bisim_up_to refl_t P2 Q3 +

Subgoal 1.1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par (par P Q2) R.

Subgoal 1.1.2.2:

Variables: P Q R A Q2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q A Q2
============================
 exists Q3, refl_t (par (par P Q2) R) (par (par P Q2) R) (par P (par Q2 R))
              Q3 /\
   bisim_up_to refl_t (par (par P Q2) R) Q3 +

Subgoal 1.1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par P (par Q2 R).

Subgoal 1.1.2.2:

Variables: P Q R A Q2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q A Q2
============================
 refl_t (par (par P Q2) R) (par (par P Q2) R) (par P (par Q2 R))
   (par P (par Q2 R)) /\
   bisim_up_to refl_t (par (par P Q2) R) (par P (par Q2 R)) +

Subgoal 1.1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < split.

Subgoal 1.1.2.2.1:

Variables: P Q R A Q2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q A Q2
============================
 refl_t (par (par P Q2) R) (par (par P Q2) R) (par P (par Q2 R))
   (par P (par Q2 R))

Subgoal 1.1.2.2.2 is:
 bisim_up_to refl_t (par (par P Q2) R) (par P (par Q2 R)) +

Subgoal 1.1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < search.

Subgoal 1.1.2.2.2:

Variables: P Q R A Q2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q A Q2
============================
 bisim_up_to refl_t (par (par P Q2) R) (par P (par Q2 R)) +

Subgoal 1.1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < backchain CH.

Subgoal 1.1.3:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P (up X) P4
H4 : one Q (dn X) Q2
============================
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par P4 (par Q2 R).

Subgoal 1.1.3:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P (up X) P4
H4 : one Q (dn X) Q2
============================
 one (par P (par Q R)) tau (par P4 (par Q2 R)) /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 (par P4 (par Q2 R)) Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < split.

Subgoal 1.1.3.1:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P (up X) P4
H4 : one Q (dn X) Q2
============================
 one (par P (par Q R)) tau (par P4 (par Q2 R))

Subgoal 1.1.3.2 is:
 exists P2 Q3, refl_t (par (par P4 Q2) R) P2 (par P4 (par Q2 R)) Q3 /\
   bisim_up_to refl_t P2 Q3 +

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < search.

Subgoal 1.1.3.2:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P (up X) P4
H4 : one Q (dn X) Q2
============================
 exists P2 Q3, refl_t (par (par P4 Q2) R) P2 (par P4 (par Q2 R)) Q3 /\
   bisim_up_to refl_t P2 Q3 +

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par (par P4 Q2) R.

Subgoal 1.1.3.2:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P (up X) P4
H4 : one Q (dn X) Q2
============================
 exists Q3, refl_t (par (par P4 Q2) R) (par (par P4 Q2) R)
              (par P4 (par Q2 R)) Q3 /\
   bisim_up_to refl_t (par (par P4 Q2) R) Q3 +

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par P4 (par Q2 R).

Subgoal 1.1.3.2:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P (up X) P4
H4 : one Q (dn X) Q2
============================
 refl_t (par (par P4 Q2) R) (par (par P4 Q2) R) (par P4 (par Q2 R))
   (par P4 (par Q2 R)) /\
   bisim_up_to refl_t (par (par P4 Q2) R) (par P4 (par Q2 R)) +

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < split.

Subgoal 1.1.3.2.1:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P (up X) P4
H4 : one Q (dn X) Q2
============================
 refl_t (par (par P4 Q2) R) (par (par P4 Q2) R) (par P4 (par Q2 R))
   (par P4 (par Q2 R))

Subgoal 1.1.3.2.2 is:
 bisim_up_to refl_t (par (par P4 Q2) R) (par P4 (par Q2 R)) +

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < search.

Subgoal 1.1.3.2.2:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P (up X) P4
H4 : one Q (dn X) Q2
============================
 bisim_up_to refl_t (par (par P4 Q2) R) (par P4 (par Q2 R)) +

Subgoal 1.1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < backchain CH.

Subgoal 1.1.4:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P (dn X) P4
H4 : one Q (up X) Q2
============================
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par P4 (par Q2 R).

Subgoal 1.1.4:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P (dn X) P4
H4 : one Q (up X) Q2
============================
 one (par P (par Q R)) tau (par P4 (par Q2 R)) /\
   (exists P2 Q3, refl_t (par (par P4 Q2) R) P2 (par P4 (par Q2 R)) Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < split.

Subgoal 1.1.4.1:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P (dn X) P4
H4 : one Q (up X) Q2
============================
 one (par P (par Q R)) tau (par P4 (par Q2 R))

Subgoal 1.1.4.2 is:
 exists P2 Q3, refl_t (par (par P4 Q2) R) P2 (par P4 (par Q2 R)) Q3 /\
   bisim_up_to refl_t P2 Q3 +

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < search.

Subgoal 1.1.4.2:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P (dn X) P4
H4 : one Q (up X) Q2
============================
 exists P2 Q3, refl_t (par (par P4 Q2) R) P2 (par P4 (par Q2 R)) Q3 /\
   bisim_up_to refl_t P2 Q3 +

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par (par P4 Q2) R.

Subgoal 1.1.4.2:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P (dn X) P4
H4 : one Q (up X) Q2
============================
 exists Q3, refl_t (par (par P4 Q2) R) (par (par P4 Q2) R)
              (par P4 (par Q2 R)) Q3 /\
   bisim_up_to refl_t (par (par P4 Q2) R) Q3 +

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par P4 (par Q2 R).

Subgoal 1.1.4.2:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P (dn X) P4
H4 : one Q (up X) Q2
============================
 refl_t (par (par P4 Q2) R) (par (par P4 Q2) R) (par P4 (par Q2 R))
   (par P4 (par Q2 R)) /\
   bisim_up_to refl_t (par (par P4 Q2) R) (par P4 (par Q2 R)) +

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < split.

Subgoal 1.1.4.2.1:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P (dn X) P4
H4 : one Q (up X) Q2
============================
 refl_t (par (par P4 Q2) R) (par (par P4 Q2) R) (par P4 (par Q2 R))
   (par P4 (par Q2 R))

Subgoal 1.1.4.2.2 is:
 bisim_up_to refl_t (par (par P4 Q2) R) (par P4 (par Q2 R)) +

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < search.

Subgoal 1.1.4.2.2:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one P (dn X) P4
H4 : one Q (up X) Q2
============================
 bisim_up_to refl_t (par (par P4 Q2) R) (par P4 (par Q2 R)) +

Subgoal 1.2 is:
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < backchain CH.

Subgoal 1.2:

Variables: P Q R A Q2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one R A Q2
============================
 exists Q1, one (par P (par Q R)) A Q1 /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par P (par Q Q2).

Subgoal 1.2:

Variables: P Q R A Q2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one R A Q2
============================
 one (par P (par Q R)) A (par P (par Q Q2)) /\
   (exists P2 Q3, refl_t (par (par P Q) Q2) P2 (par P (par Q Q2)) Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < split.

Subgoal 1.2.1:

Variables: P Q R A Q2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one R A Q2
============================
 one (par P (par Q R)) A (par P (par Q Q2))

Subgoal 1.2.2 is:
 exists P2 Q3, refl_t (par (par P Q) Q2) P2 (par P (par Q Q2)) Q3 /\
   bisim_up_to refl_t P2 Q3 +

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < search.

Subgoal 1.2.2:

Variables: P Q R A Q2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one R A Q2
============================
 exists P2 Q3, refl_t (par (par P Q) Q2) P2 (par P (par Q Q2)) Q3 /\
   bisim_up_to refl_t P2 Q3 +

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par (par P Q) Q2.

Subgoal 1.2.2:

Variables: P Q R A Q2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one R A Q2
============================
 exists Q3, refl_t (par (par P Q) Q2) (par (par P Q) Q2) (par P (par Q Q2))
              Q3 /\
   bisim_up_to refl_t (par (par P Q) Q2) Q3 +

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par P (par Q Q2).

Subgoal 1.2.2:

Variables: P Q R A Q2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one R A Q2
============================
 refl_t (par (par P Q) Q2) (par (par P Q) Q2) (par P (par Q Q2))
   (par P (par Q Q2)) /\
   bisim_up_to refl_t (par (par P Q) Q2) (par P (par Q Q2)) +

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < split.

Subgoal 1.2.2.1:

Variables: P Q R A Q2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one R A Q2
============================
 refl_t (par (par P Q) Q2) (par (par P Q) Q2) (par P (par Q Q2))
   (par P (par Q Q2))

Subgoal 1.2.2.2 is:
 bisim_up_to refl_t (par (par P Q) Q2) (par P (par Q Q2)) +

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < search.

Subgoal 1.2.2.2:

Variables: P Q R A Q2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one R A Q2
============================
 bisim_up_to refl_t (par (par P Q) Q2) (par P (par Q Q2)) +

Subgoal 1.3 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < backchain CH.

Subgoal 1.3:

Variables: P Q R X Q2 P3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one (par P Q) (up X) P3
H3 : one R (dn X) Q2
============================
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < case H2.

Subgoal 1.3.1:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (dn X) Q2
H4 : one P (up X) P4
============================
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3.2 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q4, refl_t (par (par P Q3) Q2) P2 Q1 Q4 /\
      bisim_up_to refl_t P2 Q4 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par P4 (par Q Q2).

Subgoal 1.3.1:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (dn X) Q2
H4 : one P (up X) P4
============================
 one (par P (par Q R)) tau (par P4 (par Q Q2)) /\
   (exists P2 Q3, refl_t (par (par P4 Q) Q2) P2 (par P4 (par Q Q2)) Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.3.2 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q4, refl_t (par (par P Q3) Q2) P2 Q1 Q4 /\
      bisim_up_to refl_t P2 Q4 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < split.

Subgoal 1.3.1.1:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (dn X) Q2
H4 : one P (up X) P4
============================
 one (par P (par Q R)) tau (par P4 (par Q Q2))

Subgoal 1.3.1.2 is:
 exists P2 Q3, refl_t (par (par P4 Q) Q2) P2 (par P4 (par Q Q2)) Q3 /\
   bisim_up_to refl_t P2 Q3 +

Subgoal 1.3.2 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q4, refl_t (par (par P Q3) Q2) P2 Q1 Q4 /\
      bisim_up_to refl_t P2 Q4 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < search.

Subgoal 1.3.1.2:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (dn X) Q2
H4 : one P (up X) P4
============================
 exists P2 Q3, refl_t (par (par P4 Q) Q2) P2 (par P4 (par Q Q2)) Q3 /\
   bisim_up_to refl_t P2 Q3 +

Subgoal 1.3.2 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q4, refl_t (par (par P Q3) Q2) P2 Q1 Q4 /\
      bisim_up_to refl_t P2 Q4 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par (par P4 Q) Q2.

Subgoal 1.3.1.2:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (dn X) Q2
H4 : one P (up X) P4
============================
 exists Q3, refl_t (par (par P4 Q) Q2) (par (par P4 Q) Q2)
              (par P4 (par Q Q2)) Q3 /\
   bisim_up_to refl_t (par (par P4 Q) Q2) Q3 +

Subgoal 1.3.2 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q4, refl_t (par (par P Q3) Q2) P2 Q1 Q4 /\
      bisim_up_to refl_t P2 Q4 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par P4 (par Q Q2).

Subgoal 1.3.1.2:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (dn X) Q2
H4 : one P (up X) P4
============================
 refl_t (par (par P4 Q) Q2) (par (par P4 Q) Q2) (par P4 (par Q Q2))
   (par P4 (par Q Q2)) /\
   bisim_up_to refl_t (par (par P4 Q) Q2) (par P4 (par Q Q2)) +

Subgoal 1.3.2 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q4, refl_t (par (par P Q3) Q2) P2 Q1 Q4 /\
      bisim_up_to refl_t P2 Q4 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < split.

Subgoal 1.3.1.2.1:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (dn X) Q2
H4 : one P (up X) P4
============================
 refl_t (par (par P4 Q) Q2) (par (par P4 Q) Q2) (par P4 (par Q Q2))
   (par P4 (par Q Q2))

Subgoal 1.3.1.2.2 is:
 bisim_up_to refl_t (par (par P4 Q) Q2) (par P4 (par Q Q2)) +

Subgoal 1.3.2 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q4, refl_t (par (par P Q3) Q2) P2 Q1 Q4 /\
      bisim_up_to refl_t P2 Q4 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < search.

Subgoal 1.3.1.2.2:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (dn X) Q2
H4 : one P (up X) P4
============================
 bisim_up_to refl_t (par (par P4 Q) Q2) (par P4 (par Q Q2)) +

Subgoal 1.3.2 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q4, refl_t (par (par P Q3) Q2) P2 Q1 Q4 /\
      bisim_up_to refl_t P2 Q4 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < backchain CH.

Subgoal 1.3.2:

Variables: P Q R X Q2 Q3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (dn X) Q2
H4 : one Q (up X) Q3
============================
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q4, refl_t (par (par P Q3) Q2) P2 Q1 Q4 /\
      bisim_up_to refl_t P2 Q4 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par P (par Q3 Q2).

Subgoal 1.3.2:

Variables: P Q R X Q2 Q3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (dn X) Q2
H4 : one Q (up X) Q3
============================
 one (par P (par Q R)) tau (par P (par Q3 Q2)) /\
   (exists P2 Q4, refl_t (par (par P Q3) Q2) P2 (par P (par Q3 Q2)) Q4 /\
      bisim_up_to refl_t P2 Q4 +)

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < split.

Subgoal 1.3.2.1:

Variables: P Q R X Q2 Q3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (dn X) Q2
H4 : one Q (up X) Q3
============================
 one (par P (par Q R)) tau (par P (par Q3 Q2))

Subgoal 1.3.2.2 is:
 exists P2 Q4, refl_t (par (par P Q3) Q2) P2 (par P (par Q3 Q2)) Q4 /\
   bisim_up_to refl_t P2 Q4 +

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < search.

Subgoal 1.3.2.2:

Variables: P Q R X Q2 Q3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (dn X) Q2
H4 : one Q (up X) Q3
============================
 exists P2 Q4, refl_t (par (par P Q3) Q2) P2 (par P (par Q3 Q2)) Q4 /\
   bisim_up_to refl_t P2 Q4 +

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par (par P Q3) Q2.

Subgoal 1.3.2.2:

Variables: P Q R X Q2 Q3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (dn X) Q2
H4 : one Q (up X) Q3
============================
 exists Q4, refl_t (par (par P Q3) Q2) (par (par P Q3) Q2)
              (par P (par Q3 Q2)) Q4 /\
   bisim_up_to refl_t (par (par P Q3) Q2) Q4 +

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par P (par Q3 Q2).

Subgoal 1.3.2.2:

Variables: P Q R X Q2 Q3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (dn X) Q2
H4 : one Q (up X) Q3
============================
 refl_t (par (par P Q3) Q2) (par (par P Q3) Q2) (par P (par Q3 Q2))
   (par P (par Q3 Q2)) /\
   bisim_up_to refl_t (par (par P Q3) Q2) (par P (par Q3 Q2)) +

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < split.

Subgoal 1.3.2.2.1:

Variables: P Q R X Q2 Q3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (dn X) Q2
H4 : one Q (up X) Q3
============================
 refl_t (par (par P Q3) Q2) (par (par P Q3) Q2) (par P (par Q3 Q2))
   (par P (par Q3 Q2))

Subgoal 1.3.2.2.2 is:
 bisim_up_to refl_t (par (par P Q3) Q2) (par P (par Q3 Q2)) +

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < search.

Subgoal 1.3.2.2.2:

Variables: P Q R X Q2 Q3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (dn X) Q2
H4 : one Q (up X) Q3
============================
 bisim_up_to refl_t (par (par P Q3) Q2) (par P (par Q3 Q2)) +

Subgoal 1.4 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < backchain CH.

Subgoal 1.4:

Variables: P Q R X Q2 P3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one (par P Q) (dn X) P3
H3 : one R (up X) Q2
============================
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par P3 Q2) P2 Q1 Q3 /\ bisim_up_to refl_t P2 Q3 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < case H2.

Subgoal 1.4.1:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (up X) Q2
H4 : one P (dn X) P4
============================
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q3, refl_t (par (par P4 Q) Q2) P2 Q1 Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4.2 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q4, refl_t (par (par P Q3) Q2) P2 Q1 Q4 /\
      bisim_up_to refl_t P2 Q4 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par P4 (par Q Q2).

Subgoal 1.4.1:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (up X) Q2
H4 : one P (dn X) P4
============================
 one (par P (par Q R)) tau (par P4 (par Q Q2)) /\
   (exists P2 Q3, refl_t (par (par P4 Q) Q2) P2 (par P4 (par Q Q2)) Q3 /\
      bisim_up_to refl_t P2 Q3 +)

Subgoal 1.4.2 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q4, refl_t (par (par P Q3) Q2) P2 Q1 Q4 /\
      bisim_up_to refl_t P2 Q4 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < split.

Subgoal 1.4.1.1:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (up X) Q2
H4 : one P (dn X) P4
============================
 one (par P (par Q R)) tau (par P4 (par Q Q2))

Subgoal 1.4.1.2 is:
 exists P2 Q3, refl_t (par (par P4 Q) Q2) P2 (par P4 (par Q Q2)) Q3 /\
   bisim_up_to refl_t P2 Q3 +

Subgoal 1.4.2 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q4, refl_t (par (par P Q3) Q2) P2 Q1 Q4 /\
      bisim_up_to refl_t P2 Q4 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < search.

Subgoal 1.4.1.2:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (up X) Q2
H4 : one P (dn X) P4
============================
 exists P2 Q3, refl_t (par (par P4 Q) Q2) P2 (par P4 (par Q Q2)) Q3 /\
   bisim_up_to refl_t P2 Q3 +

Subgoal 1.4.2 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q4, refl_t (par (par P Q3) Q2) P2 Q1 Q4 /\
      bisim_up_to refl_t P2 Q4 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par (par P4 Q) Q2.

Subgoal 1.4.1.2:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (up X) Q2
H4 : one P (dn X) P4
============================
 exists Q3, refl_t (par (par P4 Q) Q2) (par (par P4 Q) Q2)
              (par P4 (par Q Q2)) Q3 /\
   bisim_up_to refl_t (par (par P4 Q) Q2) Q3 +

Subgoal 1.4.2 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q4, refl_t (par (par P Q3) Q2) P2 Q1 Q4 /\
      bisim_up_to refl_t P2 Q4 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par P4 (par Q Q2).

Subgoal 1.4.1.2:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (up X) Q2
H4 : one P (dn X) P4
============================
 refl_t (par (par P4 Q) Q2) (par (par P4 Q) Q2) (par P4 (par Q Q2))
   (par P4 (par Q Q2)) /\
   bisim_up_to refl_t (par (par P4 Q) Q2) (par P4 (par Q Q2)) +

Subgoal 1.4.2 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q4, refl_t (par (par P Q3) Q2) P2 Q1 Q4 /\
      bisim_up_to refl_t P2 Q4 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < split.

Subgoal 1.4.1.2.1:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (up X) Q2
H4 : one P (dn X) P4
============================
 refl_t (par (par P4 Q) Q2) (par (par P4 Q) Q2) (par P4 (par Q Q2))
   (par P4 (par Q Q2))

Subgoal 1.4.1.2.2 is:
 bisim_up_to refl_t (par (par P4 Q) Q2) (par P4 (par Q Q2)) +

Subgoal 1.4.2 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q4, refl_t (par (par P Q3) Q2) P2 Q1 Q4 /\
      bisim_up_to refl_t P2 Q4 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < search.

Subgoal 1.4.1.2.2:

Variables: P Q R X Q2 P4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (up X) Q2
H4 : one P (dn X) P4
============================
 bisim_up_to refl_t (par (par P4 Q) Q2) (par P4 (par Q Q2)) +

Subgoal 1.4.2 is:
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q4, refl_t (par (par P Q3) Q2) P2 Q1 Q4 /\
      bisim_up_to refl_t P2 Q4 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < backchain CH.

Subgoal 1.4.2:

Variables: P Q R X Q2 Q3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (up X) Q2
H4 : one Q (dn X) Q3
============================
 exists Q1, one (par P (par Q R)) tau Q1 /\
   (exists P2 Q4, refl_t (par (par P Q3) Q2) P2 Q1 Q4 /\
      bisim_up_to refl_t P2 Q4 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par P (par Q3 Q2).

Subgoal 1.4.2:

Variables: P Q R X Q2 Q3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (up X) Q2
H4 : one Q (dn X) Q3
============================
 one (par P (par Q R)) tau (par P (par Q3 Q2)) /\
   (exists P2 Q4, refl_t (par (par P Q3) Q2) P2 (par P (par Q3 Q2)) Q4 /\
      bisim_up_to refl_t P2 Q4 +)

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < split.

Subgoal 1.4.2.1:

Variables: P Q R X Q2 Q3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (up X) Q2
H4 : one Q (dn X) Q3
============================
 one (par P (par Q R)) tau (par P (par Q3 Q2))

Subgoal 1.4.2.2 is:
 exists P2 Q4, refl_t (par (par P Q3) Q2) P2 (par P (par Q3 Q2)) Q4 /\
   bisim_up_to refl_t P2 Q4 +

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < search.

Subgoal 1.4.2.2:

Variables: P Q R X Q2 Q3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (up X) Q2
H4 : one Q (dn X) Q3
============================
 exists P2 Q4, refl_t (par (par P Q3) Q2) P2 (par P (par Q3 Q2)) Q4 /\
   bisim_up_to refl_t P2 Q4 +

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par (par P Q3) Q2.

Subgoal 1.4.2.2:

Variables: P Q R X Q2 Q3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (up X) Q2
H4 : one Q (dn X) Q3
============================
 exists Q4, refl_t (par (par P Q3) Q2) (par (par P Q3) Q2)
              (par P (par Q3 Q2)) Q4 /\
   bisim_up_to refl_t (par (par P Q3) Q2) Q4 +

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < witness par P (par Q3 Q2).

Subgoal 1.4.2.2:

Variables: P Q R X Q2 Q3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (up X) Q2
H4 : one Q (dn X) Q3
============================
 refl_t (par (par P Q3) Q2) (par (par P Q3) Q2) (par P (par Q3 Q2))
   (par P (par Q3 Q2)) /\
   bisim_up_to refl_t (par (par P Q3) Q2) (par P (par Q3 Q2)) +

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < split.

Subgoal 1.4.2.2.1:

Variables: P Q R X Q2 Q3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (up X) Q2
H4 : one Q (dn X) Q3
============================
 refl_t (par (par P Q3) Q2) (par (par P Q3) Q2) (par P (par Q3 Q2))
   (par P (par Q3 Q2))

Subgoal 1.4.2.2.2 is:
 bisim_up_to refl_t (par (par P Q3) Q2) (par P (par Q3 Q2)) +

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < search.

Subgoal 1.4.2.2.2:

Variables: P Q R X Q2 Q3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R (up X) Q2
H4 : one Q (dn X) Q3
============================
 bisim_up_to refl_t (par (par P Q3) Q2) (par P (par Q3 Q2)) +

Subgoal 2 is:
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < backchain CH.

Subgoal 2:

Variables: P Q R
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
============================
 forall A Q1, one (par P (par Q R)) A Q1 ->
   (exists P1, one (par (par P Q) R) A P1 /\
      (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_par_assoc < intros.

Subgoal 2:

Variables: P Q R A Q1
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H1 : one (par P (par Q R)) A Q1
============================
 exists P1, one (par (par P Q) R) A P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_par_assoc < case H1.

Subgoal 2.1:

Variables: P Q R A P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P A P2
============================
 exists P1, one (par (par P Q) R) A P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 (par Q R)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2 is:
 exists P1, one (par (par P Q) R) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par P Q3) Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par (par P2 Q) R.

Subgoal 2.1:

Variables: P Q R A P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P A P2
============================
 one (par (par P Q) R) A (par (par P2 Q) R) /\
   (exists P3 Q2, refl_t (par (par P2 Q) R) P3 (par P2 (par Q R)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2 is:
 exists P1, one (par (par P Q) R) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par P Q3) Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < split.

Subgoal 2.1.1:

Variables: P Q R A P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P A P2
============================
 one (par (par P Q) R) A (par (par P2 Q) R)

Subgoal 2.1.2 is:
 exists P3 Q2, refl_t (par (par P2 Q) R) P3 (par P2 (par Q R)) Q2 /\
   bisim_up_to refl_t P3 Q2 +

Subgoal 2.2 is:
 exists P1, one (par (par P Q) R) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par P Q3) Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < search.

Subgoal 2.1.2:

Variables: P Q R A P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P A P2
============================
 exists P3 Q2, refl_t (par (par P2 Q) R) P3 (par P2 (par Q R)) Q2 /\
   bisim_up_to refl_t P3 Q2 +

Subgoal 2.2 is:
 exists P1, one (par (par P Q) R) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par P Q3) Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par (par P2 Q) R.

Subgoal 2.1.2:

Variables: P Q R A P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P A P2
============================
 exists Q2, refl_t (par (par P2 Q) R) (par (par P2 Q) R) (par P2 (par Q R))
              Q2 /\
   bisim_up_to refl_t (par (par P2 Q) R) Q2 +

Subgoal 2.2 is:
 exists P1, one (par (par P Q) R) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par P Q3) Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par P2 (par Q R).

Subgoal 2.1.2:

Variables: P Q R A P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P A P2
============================
 refl_t (par (par P2 Q) R) (par (par P2 Q) R) (par P2 (par Q R))
   (par P2 (par Q R)) /\
   bisim_up_to refl_t (par (par P2 Q) R) (par P2 (par Q R)) +

Subgoal 2.2 is:
 exists P1, one (par (par P Q) R) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par P Q3) Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < split.

Subgoal 2.1.2.1:

Variables: P Q R A P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P A P2
============================
 refl_t (par (par P2 Q) R) (par (par P2 Q) R) (par P2 (par Q R))
   (par P2 (par Q R))

Subgoal 2.1.2.2 is:
 bisim_up_to refl_t (par (par P2 Q) R) (par P2 (par Q R)) +

Subgoal 2.2 is:
 exists P1, one (par (par P Q) R) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par P Q3) Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < search.

Subgoal 2.1.2.2:

Variables: P Q R A P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P A P2
============================
 bisim_up_to refl_t (par (par P2 Q) R) (par P2 (par Q R)) +

Subgoal 2.2 is:
 exists P1, one (par (par P Q) R) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par P Q3) Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < backchain CH.

Subgoal 2.2:

Variables: P Q R A Q3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one (par Q R) A Q3
============================
 exists P1, one (par (par P Q) R) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par P Q3) Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < case H2.

Subgoal 2.2.1:

Variables: P Q R A P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q A P2
============================
 exists P1, one (par (par P Q) R) A P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 R)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2.2 is:
 exists P1, one (par (par P Q) R) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par P (par Q Q4)) Q2 /\
      bisim_up_to refl_t P2 Q2 +)

Subgoal 2.2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par (par P P2) R.

Subgoal 2.2.1:

Variables: P Q R A P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q A P2
============================
 one (par (par P Q) R) A (par (par P P2) R) /\
   (exists P3 Q2, refl_t (par (par P P2) R) P3 (par P (par P2 R)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2.2 is:
 exists P1, one (par (par P Q) R) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par P (par Q Q4)) Q2 /\
      bisim_up_to refl_t P2 Q2 +)

Subgoal 2.2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < split.

Subgoal 2.2.1.1:

Variables: P Q R A P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q A P2
============================
 one (par (par P Q) R) A (par (par P P2) R)

Subgoal 2.2.1.2 is:
 exists P3 Q2, refl_t (par (par P P2) R) P3 (par P (par P2 R)) Q2 /\
   bisim_up_to refl_t P3 Q2 +

Subgoal 2.2.2 is:
 exists P1, one (par (par P Q) R) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par P (par Q Q4)) Q2 /\
      bisim_up_to refl_t P2 Q2 +)

Subgoal 2.2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < search.

Subgoal 2.2.1.2:

Variables: P Q R A P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q A P2
============================
 exists P3 Q2, refl_t (par (par P P2) R) P3 (par P (par P2 R)) Q2 /\
   bisim_up_to refl_t P3 Q2 +

Subgoal 2.2.2 is:
 exists P1, one (par (par P Q) R) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par P (par Q Q4)) Q2 /\
      bisim_up_to refl_t P2 Q2 +)

Subgoal 2.2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par (par P P2) R.

Subgoal 2.2.1.2:

Variables: P Q R A P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q A P2
============================
 exists Q2, refl_t (par (par P P2) R) (par (par P P2) R) (par P (par P2 R))
              Q2 /\
   bisim_up_to refl_t (par (par P P2) R) Q2 +

Subgoal 2.2.2 is:
 exists P1, one (par (par P Q) R) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par P (par Q Q4)) Q2 /\
      bisim_up_to refl_t P2 Q2 +)

Subgoal 2.2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par P (par P2 R).

Subgoal 2.2.1.2:

Variables: P Q R A P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q A P2
============================
 refl_t (par (par P P2) R) (par (par P P2) R) (par P (par P2 R))
   (par P (par P2 R)) /\
   bisim_up_to refl_t (par (par P P2) R) (par P (par P2 R)) +

Subgoal 2.2.2 is:
 exists P1, one (par (par P Q) R) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par P (par Q Q4)) Q2 /\
      bisim_up_to refl_t P2 Q2 +)

Subgoal 2.2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < split.

Subgoal 2.2.1.2.1:

Variables: P Q R A P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q A P2
============================
 refl_t (par (par P P2) R) (par (par P P2) R) (par P (par P2 R))
   (par P (par P2 R))

Subgoal 2.2.1.2.2 is:
 bisim_up_to refl_t (par (par P P2) R) (par P (par P2 R)) +

Subgoal 2.2.2 is:
 exists P1, one (par (par P Q) R) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par P (par Q Q4)) Q2 /\
      bisim_up_to refl_t P2 Q2 +)

Subgoal 2.2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < search.

Subgoal 2.2.1.2.2:

Variables: P Q R A P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q A P2
============================
 bisim_up_to refl_t (par (par P P2) R) (par P (par P2 R)) +

Subgoal 2.2.2 is:
 exists P1, one (par (par P Q) R) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par P (par Q Q4)) Q2 /\
      bisim_up_to refl_t P2 Q2 +)

Subgoal 2.2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < backchain CH.

Subgoal 2.2.2:

Variables: P Q R A Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R A Q4
============================
 exists P1, one (par (par P Q) R) A P1 /\
   (exists P2 Q2, refl_t P1 P2 (par P (par Q Q4)) Q2 /\
      bisim_up_to refl_t P2 Q2 +)

Subgoal 2.2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par (par P Q) Q4.

Subgoal 2.2.2:

Variables: P Q R A Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R A Q4
============================
 one (par (par P Q) R) A (par (par P Q) Q4) /\
   (exists P2 Q2, refl_t (par (par P Q) Q4) P2 (par P (par Q Q4)) Q2 /\
      bisim_up_to refl_t P2 Q2 +)

Subgoal 2.2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < split.

Subgoal 2.2.2.1:

Variables: P Q R A Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R A Q4
============================
 one (par (par P Q) R) A (par (par P Q) Q4)

Subgoal 2.2.2.2 is:
 exists P2 Q2, refl_t (par (par P Q) Q4) P2 (par P (par Q Q4)) Q2 /\
   bisim_up_to refl_t P2 Q2 +

Subgoal 2.2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < search.

Subgoal 2.2.2.2:

Variables: P Q R A Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R A Q4
============================
 exists P2 Q2, refl_t (par (par P Q) Q4) P2 (par P (par Q Q4)) Q2 /\
   bisim_up_to refl_t P2 Q2 +

Subgoal 2.2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par (par P Q) Q4.

Subgoal 2.2.2.2:

Variables: P Q R A Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R A Q4
============================
 exists Q2, refl_t (par (par P Q) Q4) (par (par P Q) Q4) (par P (par Q Q4))
              Q2 /\
   bisim_up_to refl_t (par (par P Q) Q4) Q2 +

Subgoal 2.2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par P (par Q Q4).

Subgoal 2.2.2.2:

Variables: P Q R A Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R A Q4
============================
 refl_t (par (par P Q) Q4) (par (par P Q) Q4) (par P (par Q Q4))
   (par P (par Q Q4)) /\
   bisim_up_to refl_t (par (par P Q) Q4) (par P (par Q Q4)) +

Subgoal 2.2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < split.

Subgoal 2.2.2.2.1:

Variables: P Q R A Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R A Q4
============================
 refl_t (par (par P Q) Q4) (par (par P Q) Q4) (par P (par Q Q4))
   (par P (par Q Q4))

Subgoal 2.2.2.2.2 is:
 bisim_up_to refl_t (par (par P Q) Q4) (par P (par Q Q4)) +

Subgoal 2.2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < search.

Subgoal 2.2.2.2.2:

Variables: P Q R A Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one R A Q4
============================
 bisim_up_to refl_t (par (par P Q) Q4) (par P (par Q Q4)) +

Subgoal 2.2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < backchain CH.

Subgoal 2.2.3:

Variables: P Q R X Q4 P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q (up X) P2
H4 : one R (dn X) Q4
============================
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par (par P P2) Q4.

Subgoal 2.2.3:

Variables: P Q R X Q4 P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q (up X) P2
H4 : one R (dn X) Q4
============================
 one (par (par P Q) R) tau (par (par P P2) Q4) /\
   (exists P3 Q2, refl_t (par (par P P2) Q4) P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < split.

Subgoal 2.2.3.1:

Variables: P Q R X Q4 P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q (up X) P2
H4 : one R (dn X) Q4
============================
 one (par (par P Q) R) tau (par (par P P2) Q4)

Subgoal 2.2.3.2 is:
 exists P3 Q2, refl_t (par (par P P2) Q4) P3 (par P (par P2 Q4)) Q2 /\
   bisim_up_to refl_t P3 Q2 +

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < search.

Subgoal 2.2.3.2:

Variables: P Q R X Q4 P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q (up X) P2
H4 : one R (dn X) Q4
============================
 exists P3 Q2, refl_t (par (par P P2) Q4) P3 (par P (par P2 Q4)) Q2 /\
   bisim_up_to refl_t P3 Q2 +

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par (par P P2) Q4.

Subgoal 2.2.3.2:

Variables: P Q R X Q4 P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q (up X) P2
H4 : one R (dn X) Q4
============================
 exists Q2, refl_t (par (par P P2) Q4) (par (par P P2) Q4)
              (par P (par P2 Q4)) Q2 /\
   bisim_up_to refl_t (par (par P P2) Q4) Q2 +

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par P (par P2 Q4).

Subgoal 2.2.3.2:

Variables: P Q R X Q4 P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q (up X) P2
H4 : one R (dn X) Q4
============================
 refl_t (par (par P P2) Q4) (par (par P P2) Q4) (par P (par P2 Q4))
   (par P (par P2 Q4)) /\
   bisim_up_to refl_t (par (par P P2) Q4) (par P (par P2 Q4)) +

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < split.

Subgoal 2.2.3.2.1:

Variables: P Q R X Q4 P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q (up X) P2
H4 : one R (dn X) Q4
============================
 refl_t (par (par P P2) Q4) (par (par P P2) Q4) (par P (par P2 Q4))
   (par P (par P2 Q4))

Subgoal 2.2.3.2.2 is:
 bisim_up_to refl_t (par (par P P2) Q4) (par P (par P2 Q4)) +

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < search.

Subgoal 2.2.3.2.2:

Variables: P Q R X Q4 P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q (up X) P2
H4 : one R (dn X) Q4
============================
 bisim_up_to refl_t (par (par P P2) Q4) (par P (par P2 Q4)) +

Subgoal 2.2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < backchain CH.

Subgoal 2.2.4:

Variables: P Q R X Q4 P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q (dn X) P2
H4 : one R (up X) Q4
============================
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par (par P P2) Q4.

Subgoal 2.2.4:

Variables: P Q R X Q4 P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q (dn X) P2
H4 : one R (up X) Q4
============================
 one (par (par P Q) R) tau (par (par P P2) Q4) /\
   (exists P3 Q2, refl_t (par (par P P2) Q4) P3 (par P (par P2 Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < split.

Subgoal 2.2.4.1:

Variables: P Q R X Q4 P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q (dn X) P2
H4 : one R (up X) Q4
============================
 one (par (par P Q) R) tau (par (par P P2) Q4)

Subgoal 2.2.4.2 is:
 exists P3 Q2, refl_t (par (par P P2) Q4) P3 (par P (par P2 Q4)) Q2 /\
   bisim_up_to refl_t P3 Q2 +

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < search.

Subgoal 2.2.4.2:

Variables: P Q R X Q4 P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q (dn X) P2
H4 : one R (up X) Q4
============================
 exists P3 Q2, refl_t (par (par P P2) Q4) P3 (par P (par P2 Q4)) Q2 /\
   bisim_up_to refl_t P3 Q2 +

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par (par P P2) Q4.

Subgoal 2.2.4.2:

Variables: P Q R X Q4 P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q (dn X) P2
H4 : one R (up X) Q4
============================
 exists Q2, refl_t (par (par P P2) Q4) (par (par P P2) Q4)
              (par P (par P2 Q4)) Q2 /\
   bisim_up_to refl_t (par (par P P2) Q4) Q2 +

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par P (par P2 Q4).

Subgoal 2.2.4.2:

Variables: P Q R X Q4 P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q (dn X) P2
H4 : one R (up X) Q4
============================
 refl_t (par (par P P2) Q4) (par (par P P2) Q4) (par P (par P2 Q4))
   (par P (par P2 Q4)) /\
   bisim_up_to refl_t (par (par P P2) Q4) (par P (par P2 Q4)) +

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < split.

Subgoal 2.2.4.2.1:

Variables: P Q R X Q4 P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q (dn X) P2
H4 : one R (up X) Q4
============================
 refl_t (par (par P P2) Q4) (par (par P P2) Q4) (par P (par P2 Q4))
   (par P (par P2 Q4))

Subgoal 2.2.4.2.2 is:
 bisim_up_to refl_t (par (par P P2) Q4) (par P (par P2 Q4)) +

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < search.

Subgoal 2.2.4.2.2:

Variables: P Q R X Q4 P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H3 : one Q (dn X) P2
H4 : one R (up X) Q4
============================
 bisim_up_to refl_t (par (par P P2) Q4) (par P (par P2 Q4)) +

Subgoal 2.3 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < backchain CH.

Subgoal 2.3:

Variables: P Q R X Q3 P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (up X) P2
H3 : one (par Q R) (dn X) Q3
============================
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < case H3.

Subgoal 2.3.1:

Variables: P Q R X P2 P3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (up X) P2
H4 : one Q (dn X) P3
============================
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P4 Q2, refl_t P1 P4 (par P2 (par P3 R)) Q2 /\
      bisim_up_to refl_t P4 Q2 +)

Subgoal 2.3.2 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 (par Q Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par (par P2 P3) R.

Subgoal 2.3.1:

Variables: P Q R X P2 P3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (up X) P2
H4 : one Q (dn X) P3
============================
 one (par (par P Q) R) tau (par (par P2 P3) R) /\
   (exists P4 Q2, refl_t (par (par P2 P3) R) P4 (par P2 (par P3 R)) Q2 /\
      bisim_up_to refl_t P4 Q2 +)

Subgoal 2.3.2 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 (par Q Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < split.

Subgoal 2.3.1.1:

Variables: P Q R X P2 P3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (up X) P2
H4 : one Q (dn X) P3
============================
 one (par (par P Q) R) tau (par (par P2 P3) R)

Subgoal 2.3.1.2 is:
 exists P4 Q2, refl_t (par (par P2 P3) R) P4 (par P2 (par P3 R)) Q2 /\
   bisim_up_to refl_t P4 Q2 +

Subgoal 2.3.2 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 (par Q Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < search.

Subgoal 2.3.1.2:

Variables: P Q R X P2 P3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (up X) P2
H4 : one Q (dn X) P3
============================
 exists P4 Q2, refl_t (par (par P2 P3) R) P4 (par P2 (par P3 R)) Q2 /\
   bisim_up_to refl_t P4 Q2 +

Subgoal 2.3.2 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 (par Q Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par (par P2 P3) R.

Subgoal 2.3.1.2:

Variables: P Q R X P2 P3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (up X) P2
H4 : one Q (dn X) P3
============================
 exists Q2, refl_t (par (par P2 P3) R) (par (par P2 P3) R)
              (par P2 (par P3 R)) Q2 /\
   bisim_up_to refl_t (par (par P2 P3) R) Q2 +

Subgoal 2.3.2 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 (par Q Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par P2 (par P3 R).

Subgoal 2.3.1.2:

Variables: P Q R X P2 P3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (up X) P2
H4 : one Q (dn X) P3
============================
 refl_t (par (par P2 P3) R) (par (par P2 P3) R) (par P2 (par P3 R))
   (par P2 (par P3 R)) /\
   bisim_up_to refl_t (par (par P2 P3) R) (par P2 (par P3 R)) +

Subgoal 2.3.2 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 (par Q Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < split.

Subgoal 2.3.1.2.1:

Variables: P Q R X P2 P3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (up X) P2
H4 : one Q (dn X) P3
============================
 refl_t (par (par P2 P3) R) (par (par P2 P3) R) (par P2 (par P3 R))
   (par P2 (par P3 R))

Subgoal 2.3.1.2.2 is:
 bisim_up_to refl_t (par (par P2 P3) R) (par P2 (par P3 R)) +

Subgoal 2.3.2 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 (par Q Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < search.

Subgoal 2.3.1.2.2:

Variables: P Q R X P2 P3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (up X) P2
H4 : one Q (dn X) P3
============================
 bisim_up_to refl_t (par (par P2 P3) R) (par P2 (par P3 R)) +

Subgoal 2.3.2 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 (par Q Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < backchain CH.

Subgoal 2.3.2:

Variables: P Q R X P2 Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (up X) P2
H4 : one R (dn X) Q4
============================
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 (par Q Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par (par P2 Q) Q4.

Subgoal 2.3.2:

Variables: P Q R X P2 Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (up X) P2
H4 : one R (dn X) Q4
============================
 one (par (par P Q) R) tau (par (par P2 Q) Q4) /\
   (exists P3 Q2, refl_t (par (par P2 Q) Q4) P3 (par P2 (par Q Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < split.

Subgoal 2.3.2.1:

Variables: P Q R X P2 Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (up X) P2
H4 : one R (dn X) Q4
============================
 one (par (par P Q) R) tau (par (par P2 Q) Q4)

Subgoal 2.3.2.2 is:
 exists P3 Q2, refl_t (par (par P2 Q) Q4) P3 (par P2 (par Q Q4)) Q2 /\
   bisim_up_to refl_t P3 Q2 +

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < search.

Subgoal 2.3.2.2:

Variables: P Q R X P2 Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (up X) P2
H4 : one R (dn X) Q4
============================
 exists P3 Q2, refl_t (par (par P2 Q) Q4) P3 (par P2 (par Q Q4)) Q2 /\
   bisim_up_to refl_t P3 Q2 +

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par (par P2 Q) Q4.

Subgoal 2.3.2.2:

Variables: P Q R X P2 Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (up X) P2
H4 : one R (dn X) Q4
============================
 exists Q2, refl_t (par (par P2 Q) Q4) (par (par P2 Q) Q4)
              (par P2 (par Q Q4)) Q2 /\
   bisim_up_to refl_t (par (par P2 Q) Q4) Q2 +

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par P2 (par Q Q4).

Subgoal 2.3.2.2:

Variables: P Q R X P2 Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (up X) P2
H4 : one R (dn X) Q4
============================
 refl_t (par (par P2 Q) Q4) (par (par P2 Q) Q4) (par P2 (par Q Q4))
   (par P2 (par Q Q4)) /\
   bisim_up_to refl_t (par (par P2 Q) Q4) (par P2 (par Q Q4)) +

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < split.

Subgoal 2.3.2.2.1:

Variables: P Q R X P2 Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (up X) P2
H4 : one R (dn X) Q4
============================
 refl_t (par (par P2 Q) Q4) (par (par P2 Q) Q4) (par P2 (par Q Q4))
   (par P2 (par Q Q4))

Subgoal 2.3.2.2.2 is:
 bisim_up_to refl_t (par (par P2 Q) Q4) (par P2 (par Q Q4)) +

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < search.

Subgoal 2.3.2.2.2:

Variables: P Q R X P2 Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (up X) P2
H4 : one R (dn X) Q4
============================
 bisim_up_to refl_t (par (par P2 Q) Q4) (par P2 (par Q Q4)) +

Subgoal 2.4 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < backchain CH.

Subgoal 2.4:

Variables: P Q R X Q3 P2
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (dn X) P2
H3 : one (par Q R) (up X) Q3
============================
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 Q3) Q2 /\ bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < case H3.

Subgoal 2.4.1:

Variables: P Q R X P2 P3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (dn X) P2
H4 : one Q (up X) P3
============================
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P4 Q2, refl_t P1 P4 (par P2 (par P3 R)) Q2 /\
      bisim_up_to refl_t P4 Q2 +)

Subgoal 2.4.2 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 (par Q Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par (par P2 P3) R.

Subgoal 2.4.1:

Variables: P Q R X P2 P3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (dn X) P2
H4 : one Q (up X) P3
============================
 one (par (par P Q) R) tau (par (par P2 P3) R) /\
   (exists P4 Q2, refl_t (par (par P2 P3) R) P4 (par P2 (par P3 R)) Q2 /\
      bisim_up_to refl_t P4 Q2 +)

Subgoal 2.4.2 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 (par Q Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < split.

Subgoal 2.4.1.1:

Variables: P Q R X P2 P3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (dn X) P2
H4 : one Q (up X) P3
============================
 one (par (par P Q) R) tau (par (par P2 P3) R)

Subgoal 2.4.1.2 is:
 exists P4 Q2, refl_t (par (par P2 P3) R) P4 (par P2 (par P3 R)) Q2 /\
   bisim_up_to refl_t P4 Q2 +

Subgoal 2.4.2 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 (par Q Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < search.

Subgoal 2.4.1.2:

Variables: P Q R X P2 P3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (dn X) P2
H4 : one Q (up X) P3
============================
 exists P4 Q2, refl_t (par (par P2 P3) R) P4 (par P2 (par P3 R)) Q2 /\
   bisim_up_to refl_t P4 Q2 +

Subgoal 2.4.2 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 (par Q Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par (par P2 P3) R.

Subgoal 2.4.1.2:

Variables: P Q R X P2 P3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (dn X) P2
H4 : one Q (up X) P3
============================
 exists Q2, refl_t (par (par P2 P3) R) (par (par P2 P3) R)
              (par P2 (par P3 R)) Q2 /\
   bisim_up_to refl_t (par (par P2 P3) R) Q2 +

Subgoal 2.4.2 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 (par Q Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par P2 (par P3 R).

Subgoal 2.4.1.2:

Variables: P Q R X P2 P3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (dn X) P2
H4 : one Q (up X) P3
============================
 refl_t (par (par P2 P3) R) (par (par P2 P3) R) (par P2 (par P3 R))
   (par P2 (par P3 R)) /\
   bisim_up_to refl_t (par (par P2 P3) R) (par P2 (par P3 R)) +

Subgoal 2.4.2 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 (par Q Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < split.

Subgoal 2.4.1.2.1:

Variables: P Q R X P2 P3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (dn X) P2
H4 : one Q (up X) P3
============================
 refl_t (par (par P2 P3) R) (par (par P2 P3) R) (par P2 (par P3 R))
   (par P2 (par P3 R))

Subgoal 2.4.1.2.2 is:
 bisim_up_to refl_t (par (par P2 P3) R) (par P2 (par P3 R)) +

Subgoal 2.4.2 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 (par Q Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < search.

Subgoal 2.4.1.2.2:

Variables: P Q R X P2 P3
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (dn X) P2
H4 : one Q (up X) P3
============================
 bisim_up_to refl_t (par (par P2 P3) R) (par P2 (par P3 R)) +

Subgoal 2.4.2 is:
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 (par Q Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < backchain CH.

Subgoal 2.4.2:

Variables: P Q R X P2 Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (dn X) P2
H4 : one R (up X) Q4
============================
 exists P1, one (par (par P Q) R) tau P1 /\
   (exists P3 Q2, refl_t P1 P3 (par P2 (par Q Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < witness par (par P2 Q) Q4.

Subgoal 2.4.2:

Variables: P Q R X P2 Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (dn X) P2
H4 : one R (up X) Q4
============================
 one (par (par P Q) R) tau (par (par P2 Q) Q4) /\
   (exists P3 Q2, refl_t (par (par P2 Q) Q4) P3 (par P2 (par Q Q4)) Q2 /\
      bisim_up_to refl_t P3 Q2 +)

bisim_par_assoc < split.

Subgoal 2.4.2.1:

Variables: P Q R X P2 Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (dn X) P2
H4 : one R (up X) Q4
============================
 one (par (par P Q) R) tau (par (par P2 Q) Q4)

Subgoal 2.4.2.2 is:
 exists P3 Q2, refl_t (par (par P2 Q) Q4) P3 (par P2 (par Q Q4)) Q2 /\
   bisim_up_to refl_t P3 Q2 +

bisim_par_assoc < search.

Subgoal 2.4.2.2:

Variables: P Q R X P2 Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (dn X) P2
H4 : one R (up X) Q4
============================
 exists P3 Q2, refl_t (par (par P2 Q) Q4) P3 (par P2 (par Q Q4)) Q2 /\
   bisim_up_to refl_t P3 Q2 +

bisim_par_assoc < witness par (par P2 Q) Q4.

Subgoal 2.4.2.2:

Variables: P Q R X P2 Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (dn X) P2
H4 : one R (up X) Q4
============================
 exists Q2, refl_t (par (par P2 Q) Q4) (par (par P2 Q) Q4)
              (par P2 (par Q Q4)) Q2 /\
   bisim_up_to refl_t (par (par P2 Q) Q4) Q2 +

bisim_par_assoc < witness par P2 (par Q Q4).

Subgoal 2.4.2.2:

Variables: P Q R X P2 Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (dn X) P2
H4 : one R (up X) Q4
============================
 refl_t (par (par P2 Q) Q4) (par (par P2 Q) Q4) (par P2 (par Q Q4))
   (par P2 (par Q Q4)) /\
   bisim_up_to refl_t (par (par P2 Q) Q4) (par P2 (par Q Q4)) +

bisim_par_assoc < split.

Subgoal 2.4.2.2.1:

Variables: P Q R X P2 Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (dn X) P2
H4 : one R (up X) Q4
============================
 refl_t (par (par P2 Q) Q4) (par (par P2 Q) Q4) (par P2 (par Q Q4))
   (par P2 (par Q Q4))

Subgoal 2.4.2.2.2 is:
 bisim_up_to refl_t (par (par P2 Q) Q4) (par P2 (par Q Q4)) +

bisim_par_assoc < search.

Subgoal 2.4.2.2.2:

Variables: P Q R X P2 Q4
CH : forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par P (par Q R)) +
H2 : one P (dn X) P2
H4 : one R (up X) Q4
============================
 bisim_up_to refl_t (par (par P2 Q) Q4) (par P2 (par Q Q4)) +

bisim_par_assoc < backchain CH.
Proof completed.

Abella < Theorem bisim_par_assoc_left : 
forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par (par P R) Q).

============================
 forall P Q R, bisim_up_to refl_t (par (par P Q) R) (par (par P R) Q)

bisim_par_assoc_left < intros.

Variables: P Q R
============================
 bisim_up_to refl_t (par (par P Q) R) (par (par P R) Q)

bisim_par_assoc_left < apply bisim_reflexive_ with P = par (par P Q) R.

Variables: P Q R
H1 : bisim_up_to refl_t (par (par P Q) R) (par (par P Q) R)
============================
 bisim_up_to refl_t (par (par P Q) R) (par (par P R) Q)

bisim_par_assoc_left < apply bisim_par_assoc with P = P, Q = Q, R = R.

Variables: P Q R
H1 : bisim_up_to refl_t (par (par P Q) R) (par (par P Q) R)
H2 : bisim_up_to refl_t (par (par P Q) R) (par P (par Q R))
============================
 bisim_up_to refl_t (par (par P Q) R) (par (par P R) Q)

bisim_par_assoc_left < apply bisim_par_comm with P = P, Q = par Q R.

Variables: P Q R
H1 : bisim_up_to refl_t (par (par P Q) R) (par (par P Q) R)
H2 : bisim_up_to refl_t (par (par P Q) R) (par P (par Q R))
H3 : bisim_up_to refl_t (par P (par Q R)) (par (par Q R) P)
============================
 bisim_up_to refl_t (par (par P Q) R) (par (par P R) Q)

bisim_par_assoc_left < apply bisim_par_assoc with P = Q, Q = R, R = P.

Variables: P Q R
H1 : bisim_up_to refl_t (par (par P Q) R) (par (par P Q) R)
H2 : bisim_up_to refl_t (par (par P Q) R) (par P (par Q R))
H3 : bisim_up_to refl_t (par P (par Q R)) (par (par Q R) P)
H4 : bisim_up_to refl_t (par (par Q R) P) (par Q (par R P))
============================
 bisim_up_to refl_t (par (par P Q) R) (par (par P R) Q)

bisim_par_assoc_left < apply bisim_par_comm with P = Q, Q = par R P.

Variables: P Q R
H1 : bisim_up_to refl_t (par (par P Q) R) (par (par P Q) R)
H2 : bisim_up_to refl_t (par (par P Q) R) (par P (par Q R))
H3 : bisim_up_to refl_t (par P (par Q R)) (par (par Q R) P)
H4 : bisim_up_to refl_t (par (par Q R) P) (par Q (par R P))
H5 : bisim_up_to refl_t (par Q (par R P)) (par (par R P) Q)
============================
 bisim_up_to refl_t (par (par P Q) R) (par (par P R) Q)

bisim_par_assoc_left < assert bisim_up_to refl_t (par R P) (par P R).

Subgoal 1:

Variables: P Q R
H1 : bisim_up_to refl_t (par (par P Q) R) (par (par P Q) R)
H2 : bisim_up_to refl_t (par (par P Q) R) (par P (par Q R))
H3 : bisim_up_to refl_t (par P (par Q R)) (par (par Q R) P)
H4 : bisim_up_to refl_t (par (par Q R) P) (par Q (par R P))
H5 : bisim_up_to refl_t (par Q (par R P)) (par (par R P) Q)
============================
 bisim_up_to refl_t (par R P) (par P R)

Subgoal is:
 bisim_up_to refl_t (par (par P Q) R) (par (par P R) Q)

bisim_par_assoc_left < backchain bisim_par_comm.

Variables: P Q R
H1 : bisim_up_to refl_t (par (par P Q) R) (par (par P Q) R)
H2 : bisim_up_to refl_t (par (par P Q) R) (par P (par Q R))
H3 : bisim_up_to refl_t (par P (par Q R)) (par (par Q R) P)
H4 : bisim_up_to refl_t (par (par Q R) P) (par Q (par R P))
H5 : bisim_up_to refl_t (par Q (par R P)) (par (par R P) Q)
H6 : bisim_up_to refl_t (par R P) (par P R)
============================
 bisim_up_to refl_t (par (par P Q) R) (par (par P R) Q)

bisim_par_assoc_left < apply bisim_par_subst_1 to H6 with R = Q.

Variables: P Q R
H1 : bisim_up_to refl_t (par (par P Q) R) (par (par P Q) R)
H2 : bisim_up_to refl_t (par (par P Q) R) (par P (par Q R))
H3 : bisim_up_to refl_t (par P (par Q R)) (par (par Q R) P)
H4 : bisim_up_to refl_t (par (par Q R) P) (par Q (par R P))
H5 : bisim_up_to refl_t (par Q (par R P)) (par (par R P) Q)
H6 : bisim_up_to refl_t (par R P) (par P R)
H7 : bisim_up_to refl_t (par (par R P) Q) (par (par P R) Q)
============================
 bisim_up_to refl_t (par (par P Q) R) (par (par P R) Q)

bisim_par_assoc_left < Acc : apply bisim_transitive_ to H1 H2.

Variables: P Q R
H1 : bisim_up_to refl_t (par (par P Q) R) (par (par P Q) R)
H2 : bisim_up_to refl_t (par (par P Q) R) (par P (par Q R))
H3 : bisim_up_to refl_t (par P (par Q R)) (par (par Q R) P)
H4 : bisim_up_to refl_t (par (par Q R) P) (par Q (par R P))
H5 : bisim_up_to refl_t (par Q (par R P)) (par (par R P) Q)
H6 : bisim_up_to refl_t (par R P) (par P R)
H7 : bisim_up_to refl_t (par (par R P) Q) (par (par P R) Q)
Acc : bisim_up_to refl_t (par (par P Q) R) (par P (par Q R))
============================
 bisim_up_to refl_t (par (par P Q) R) (par (par P R) Q)

bisim_par_assoc_left < Acc : apply bisim_transitive_ to Acc H3.

Variables: P Q R
H1 : bisim_up_to refl_t (par (par P Q) R) (par (par P Q) R)
H2 : bisim_up_to refl_t (par (par P Q) R) (par P (par Q R))
H3 : bisim_up_to refl_t (par P (par Q R)) (par (par Q R) P)
H4 : bisim_up_to refl_t (par (par Q R) P) (par Q (par R P))
H5 : bisim_up_to refl_t (par Q (par R P)) (par (par R P) Q)
H6 : bisim_up_to refl_t (par R P) (par P R)
H7 : bisim_up_to refl_t (par (par R P) Q) (par (par P R) Q)
Acc : bisim_up_to refl_t (par (par P Q) R) (par P (par Q R))
Acc1 : bisim_up_to refl_t (par (par P Q) R) (par (par Q R) P)
============================
 bisim_up_to refl_t (par (par P Q) R) (par (par P R) Q)

bisim_par_assoc_left < Acc : apply bisim_transitive_ to Acc1 H4.

Variables: P Q R
H1 : bisim_up_to refl_t (par (par P Q) R) (par (par P Q) R)
H2 : bisim_up_to refl_t (par (par P Q) R) (par P (par Q R))
H3 : bisim_up_to refl_t (par P (par Q R)) (par (par Q R) P)
H4 : bisim_up_to refl_t (par (par Q R) P) (par Q (par R P))
H5 : bisim_up_to refl_t (par Q (par R P)) (par (par R P) Q)
H6 : bisim_up_to refl_t (par R P) (par P R)
H7 : bisim_up_to refl_t (par (par R P) Q) (par (par P R) Q)
Acc : bisim_up_to refl_t (par (par P Q) R) (par P (par Q R))
Acc1 : bisim_up_to refl_t (par (par P Q) R) (par (par Q R) P)
Acc2 : bisim_up_to refl_t (par (par P Q) R) (par Q (par R P))
============================
 bisim_up_to refl_t (par (par P Q) R) (par (par P R) Q)

bisim_par_assoc_left < Acc : apply bisim_transitive_ to Acc2 H5.

Variables: P Q R
H1 : bisim_up_to refl_t (par (par P Q) R) (par (par P Q) R)
H2 : bisim_up_to refl_t (par (par P Q) R) (par P (par Q R))
H3 : bisim_up_to refl_t (par P (par Q R)) (par (par Q R) P)
H4 : bisim_up_to refl_t (par (par Q R) P) (par Q (par R P))
H5 : bisim_up_to refl_t (par Q (par R P)) (par (par R P) Q)
H6 : bisim_up_to refl_t (par R P) (par P R)
H7 : bisim_up_to refl_t (par (par R P) Q) (par (par P R) Q)
Acc : bisim_up_to refl_t (par (par P Q) R) (par P (par Q R))
Acc1 : bisim_up_to refl_t (par (par P Q) R) (par (par Q R) P)
Acc2 : bisim_up_to refl_t (par (par P Q) R) (par Q (par R P))
Acc3 : bisim_up_to refl_t (par (par P Q) R) (par (par R P) Q)
============================
 bisim_up_to refl_t (par (par P Q) R) (par (par P R) Q)

bisim_par_assoc_left < Acc : apply bisim_transitive_ to Acc3 H7.

Variables: P Q R
H1 : bisim_up_to refl_t (par (par P Q) R) (par (par P Q) R)
H2 : bisim_up_to refl_t (par (par P Q) R) (par P (par Q R))
H3 : bisim_up_to refl_t (par P (par Q R)) (par (par Q R) P)
H4 : bisim_up_to refl_t (par (par Q R) P) (par Q (par R P))
H5 : bisim_up_to refl_t (par Q (par R P)) (par (par R P) Q)
H6 : bisim_up_to refl_t (par R P) (par P R)
H7 : bisim_up_to refl_t (par (par R P) Q) (par (par P R) Q)
Acc : bisim_up_to refl_t (par (par P Q) R) (par P (par Q R))
Acc1 : bisim_up_to refl_t (par (par P Q) R) (par (par Q R) P)
Acc2 : bisim_up_to refl_t (par (par P Q) R) (par Q (par R P))
Acc3 : bisim_up_to refl_t (par (par P Q) R) (par (par R P) Q)
Acc4 : bisim_up_to refl_t (par (par P Q) R) (par (par P R) Q)
============================
 bisim_up_to refl_t (par (par P Q) R) (par (par P R) Q)

bisim_par_assoc_left < search.
Proof completed.

Abella < Goodbye.