Welcome to Abella 2.0.5-dev.
```Abella < Specification "ccs".

```
```Abella < Theorem mu_id_step_absurd :
forall A Q, {step (mu x\x) A Q} -> false.

```
```
============================
forall A Q, {step (mu x\x) A Q} -> false

mu_id_step_absurd < induction on 1.
```
```
IH : forall A Q, {step (mu x\x) A Q}* -> false
============================
forall A Q, {step (mu x\x) A Q}@ -> false

mu_id_step_absurd < intros.
```
```
Variables: A Q
IH : forall A Q, {step (mu x\x) A Q}* -> false
H1 : {step (mu x\x) A Q}@
============================
false

mu_id_step_absurd < case H1.
```
```
Variables: A Q
IH : forall A Q, {step (mu x\x) A Q}* -> false
H2 : {step (mu x\x) A Q}*
============================
false

mu_id_step_absurd < apply IH to H2.
Proof completed.
```
```Abella < CoDefine sim : proc -> proc -> prop by
sim P Q := forall A P1, {step P A P1} -> (exists Q1, {step Q A Q1} /\ sim P1 Q1).

```
```Abella < Theorem sim_mu_par_ext :
forall Q Q1, {step Q a (par Q Q1)} -> sim (mu (x\out a x)) Q.

```
```
============================
forall Q Q1, {step Q a (par Q Q1)} -> sim (mu (x\out a x)) Q

sim_mu_par_ext < coinduction.
```
```
CH : forall Q Q1, {step Q a (par Q Q1)} -> sim (mu (x\out a x)) Q +
============================
forall Q Q1, {step Q a (par Q Q1)} -> sim (mu (x\out a x)) Q #

sim_mu_par_ext < intros.
```
```
Variables: Q Q1
CH : forall Q Q1, {step Q a (par Q Q1)} -> sim (mu (x\out a x)) Q +
H1 : {step Q a (par Q Q1)}
============================
sim (mu (x\out a x)) Q #

sim_mu_par_ext < unfold.
```
```
Variables: Q Q1
CH : forall Q Q1, {step Q a (par Q Q1)} -> sim (mu (x\out a x)) Q +
H1 : {step Q a (par Q Q1)}
============================
forall A P1, {step (mu (x\out a x)) A P1} ->
(exists Q1, {step Q A Q1} /\ sim P1 Q1 +)

sim_mu_par_ext < intros.
```
```
Variables: Q Q1 A P1
CH : forall Q Q1, {step Q a (par Q Q1)} -> sim (mu (x\out a x)) Q +
H1 : {step Q a (par Q Q1)}
H2 : {step (mu (x\out a x)) A P1}
============================
exists Q1, {step Q A Q1} /\ sim P1 Q1 +

sim_mu_par_ext < case H2.
```
```
Variables: Q Q1 A P1
CH : forall Q Q1, {step Q a (par Q Q1)} -> sim (mu (x\out a x)) Q +
H1 : {step Q a (par Q Q1)}
H3 : {step (out a (mu (x\out a x))) A P1}
============================
exists Q1, {step Q A Q1} /\ sim P1 Q1 +

sim_mu_par_ext < case H3.
```
```
Variables: Q Q1
CH : forall Q Q1, {step Q a (par Q Q1)} -> sim (mu (x\out a x)) Q +
H1 : {step Q a (par Q Q1)}
============================
exists Q1, {step Q a Q1} /\ sim (mu (x\out a x)) Q1 +

sim_mu_par_ext < assert {step (par Q Q1) a (par (par Q Q1) Q1)}.
```
```
Variables: Q Q1
CH : forall Q Q1, {step Q a (par Q Q1)} -> sim (mu (x\out a x)) Q +
H1 : {step Q a (par Q Q1)}
H4 : {step (par Q Q1) a (par (par Q Q1) Q1)}
============================
exists Q1, {step Q a Q1} /\ sim (mu (x\out a x)) Q1 +

sim_mu_par_ext < apply CH to H4.
```
```
Variables: Q Q1
CH : forall Q Q1, {step Q a (par Q Q1)} -> sim (mu (x\out a x)) Q +
H1 : {step Q a (par Q Q1)}
H4 : {step (par Q Q1) a (par (par Q Q1) Q1)}
H5 : sim (mu (x\out a x)) (par Q Q1) +
============================
exists Q1, {step Q a Q1} /\ sim (mu (x\out a x)) Q1 +

sim_mu_par_ext < search.
Proof completed.
```
```Abella < Theorem sim_mu_par :
sim (mu (x\out a x)) (mu (x\par (out a x) (out a x))).

```
```
============================
sim (mu (x\out a x)) (mu (x\par (out a x) (out a x)))

sim_mu_par < apply sim_mu_par_ext to _ with Q = mu (x\par (out a x) (out a x)).
```
```
H1 : sim (mu (x\out a x)) (mu (x\par (out a x) (out a x)))
============================
sim (mu (x\out a x)) (mu (x\par (out a x) (out a x)))

sim_mu_par < search.
Proof completed.
```
```Abella < Theorem sim_refl :
forall P, sim P P.

```
```
============================
forall P, sim P P

sim_refl < coinduction.
```
```
CH : forall P, sim P P +
============================
forall P, sim P P #

sim_refl < intros.
```
```
Variables: P
CH : forall P, sim P P +
============================
sim P P #

sim_refl < unfold.
```
```
Variables: P
CH : forall P, sim P P +
============================
forall A P1, {step P A P1} -> (exists Q1, {step P A Q1} /\ sim P1 Q1 +)

sim_refl < intros.
```
```
Variables: P A P1
CH : forall P, sim P P +
H1 : {step P A P1}
============================
exists Q1, {step P A Q1} /\ sim P1 Q1 +

sim_refl < apply CH with P = P1.
```
```
Variables: P A P1
CH : forall P, sim P P +
H1 : {step P A P1}
H2 : sim P1 P1 +
============================
exists Q1, {step P A Q1} /\ sim P1 Q1 +

sim_refl < search.
Proof completed.
```
```Abella < Theorem sim_trans :
forall P Q R, sim P Q -> sim Q R -> sim P R.

```
```
============================
forall P Q R, sim P Q -> sim Q R -> sim P R

sim_trans < coinduction.
```
```
CH : forall P Q R, sim P Q -> sim Q R -> sim P R +
============================
forall P Q R, sim P Q -> sim Q R -> sim P R #

sim_trans < intros.
```
```
Variables: P Q R
CH : forall P Q R, sim P Q -> sim Q R -> sim P R +
H1 : sim P Q
H2 : sim Q R
============================
sim P R #

sim_trans < unfold.
```
```
Variables: P Q R
CH : forall P Q R, sim P Q -> sim Q R -> sim P R +
H1 : sim P Q
H2 : sim Q R
============================
forall A P1, {step P A P1} -> (exists Q1, {step R A Q1} /\ sim P1 Q1 +)

sim_trans < intros.
```
```
Variables: P Q R A P1
CH : forall P Q R, sim P Q -> sim Q R -> sim P R +
H1 : sim P Q
H2 : sim Q R
H3 : {step P A P1}
============================
exists Q1, {step R A Q1} /\ sim P1 Q1 +

sim_trans < case H1.
```
```
Variables: P Q R A P1
CH : forall P Q R, sim P Q -> sim Q R -> sim P R +
H2 : sim Q R
H3 : {step P A P1}
H4 : forall A P1, {step P A P1} -> (exists Q2, {step Q A Q2} /\ sim P1 Q2)
============================
exists Q1, {step R A Q1} /\ sim P1 Q1 +

sim_trans < apply H4 to H3.
```
```
Variables: P Q R A P1 Q2
CH : forall P Q R, sim P Q -> sim Q R -> sim P R +
H2 : sim Q R
H3 : {step P A P1}
H4 : forall A P1, {step P A P1} -> (exists Q2, {step Q A Q2} /\ sim P1 Q2)
H5 : {step Q A Q2}
H6 : sim P1 Q2
============================
exists Q1, {step R A Q1} /\ sim P1 Q1 +

sim_trans < case H2.
```
```
Variables: P Q R A P1 Q2
CH : forall P Q R, sim P Q -> sim Q R -> sim P R +
H3 : {step P A P1}
H4 : forall A P1, {step P A P1} -> (exists Q2, {step Q A Q2} /\ sim P1 Q2)
H5 : {step Q A Q2}
H6 : sim P1 Q2
H7 : forall A P1, {step Q A P1} -> (exists Q2, {step R A Q2} /\ sim P1 Q2)
============================
exists Q1, {step R A Q1} /\ sim P1 Q1 +

sim_trans < apply H7 to H5.
```
```
Variables: P Q R A P1 Q2 Q1
CH : forall P Q R, sim P Q -> sim Q R -> sim P R +
H3 : {step P A P1}
H4 : forall A P1, {step P A P1} -> (exists Q2, {step Q A Q2} /\ sim P1 Q2)
H5 : {step Q A Q2}
H6 : sim P1 Q2
H7 : forall A P1, {step Q A P1} -> (exists Q2, {step R A Q2} /\ sim P1 Q2)
H8 : {step R A Q1}
H9 : sim Q2 Q1
============================
exists Q1, {step R A Q1} /\ sim P1 Q1 +

sim_trans < apply CH to H6 H9.
```
```
Variables: P Q R A P1 Q2 Q1
CH : forall P Q R, sim P Q -> sim Q R -> sim P R +
H3 : {step P A P1}
H4 : forall A P1, {step P A P1} -> (exists Q2, {step Q A Q2} /\ sim P1 Q2)
H5 : {step Q A Q2}
H6 : sim P1 Q2
H7 : forall A P1, {step Q A P1} -> (exists Q2, {step R A Q2} /\ sim P1 Q2)
H8 : {step R A Q1}
H9 : sim Q2 Q1
H10 : sim P1 Q1 +
============================
exists Q1, {step R A Q1} /\ sim P1 Q1 +

sim_trans < search.
Proof completed.
```
```Abella < CoDefine bisim : proc -> proc -> prop by
bisim P Q := (forall A P1, {step P A P1} -> (exists Q1, {step Q A Q1} /\ bisim P1 Q1)) /\
(forall A Q1, {step Q A Q1} -> (exists P1, {step P A P1} /\ bisim P1 Q1)).

```
```Abella < Theorem bisim_refl :
forall P, bisim P P.

```
```
============================
forall P, bisim P P

bisim_refl < coinduction.
```
```
CH : forall P, bisim P P +
============================
forall P, bisim P P #

bisim_refl < intros.
```
```
Variables: P
CH : forall P, bisim P P +
============================
bisim P P #

bisim_refl < unfold.
```
```Subgoal 1:

Variables: P
CH : forall P, bisim P P +
============================
forall A P1, {step P A P1} -> (exists Q1, {step P A Q1} /\ bisim P1 Q1 +)

Subgoal 2 is:
forall A Q1, {step P A Q1} -> (exists P1, {step P A P1} /\ bisim P1 Q1 +)

bisim_refl < intros.
```
```Subgoal 1:

Variables: P A P1
CH : forall P, bisim P P +
H1 : {step P A P1}
============================
exists Q1, {step P A Q1} /\ bisim P1 Q1 +

Subgoal 2 is:
forall A Q1, {step P A Q1} -> (exists P1, {step P A P1} /\ bisim P1 Q1 +)

bisim_refl < apply CH with P = P1.
```
```Subgoal 1:

Variables: P A P1
CH : forall P, bisim P P +
H1 : {step P A P1}
H2 : bisim P1 P1 +
============================
exists Q1, {step P A Q1} /\ bisim P1 Q1 +

Subgoal 2 is:
forall A Q1, {step P A Q1} -> (exists P1, {step P A P1} /\ bisim P1 Q1 +)

bisim_refl < search.
```
```Subgoal 2:

Variables: P
CH : forall P, bisim P P +
============================
forall A Q1, {step P A Q1} -> (exists P1, {step P A P1} /\ bisim P1 Q1 +)

bisim_refl < intros.
```
```Subgoal 2:

Variables: P A Q1
CH : forall P, bisim P P +
H1 : {step P A Q1}
============================
exists P1, {step P A P1} /\ bisim P1 Q1 +

bisim_refl < apply CH with P = Q1.
```
```Subgoal 2:

Variables: P A Q1
CH : forall P, bisim P P +
H1 : {step P A Q1}
H2 : bisim Q1 Q1 +
============================
exists P1, {step P A P1} /\ bisim P1 Q1 +

bisim_refl < search.
Proof completed.
```
```Abella < Theorem bisim_sym :
forall P Q, bisim P Q -> bisim Q P.

```
```
============================
forall P Q, bisim P Q -> bisim Q P

bisim_sym < coinduction.
```
```
CH : forall P Q, bisim P Q -> bisim Q P +
============================
forall P Q, bisim P Q -> bisim Q P #

bisim_sym < intros.
```
```
Variables: P Q
CH : forall P Q, bisim P Q -> bisim Q P +
H1 : bisim P Q
============================
bisim Q P #

bisim_sym < case H1.
```
```
Variables: P Q
CH : forall P Q, bisim P Q -> bisim Q P +
H2 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\ bisim P2 Q2)
H3 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\ bisim P2 Q2)
============================
bisim Q P #

bisim_sym < unfold.
```
```Subgoal 1:

Variables: P Q
CH : forall P Q, bisim P Q -> bisim Q P +
H2 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\ bisim P2 Q2)
H3 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\ bisim P2 Q2)
============================
forall A P1, {step Q A P1} -> (exists Q1, {step P A Q1} /\ bisim P1 Q1 +)

Subgoal 2 is:
forall A Q1, {step P A Q1} -> (exists P1, {step Q A P1} /\ bisim P1 Q1 +)

bisim_sym < intros.
```
```Subgoal 1:

Variables: P Q A P1
CH : forall P Q, bisim P Q -> bisim Q P +
H2 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\ bisim P2 Q2)
H3 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\ bisim P2 Q2)
H4 : {step Q A P1}
============================
exists Q1, {step P A Q1} /\ bisim P1 Q1 +

Subgoal 2 is:
forall A Q1, {step P A Q1} -> (exists P1, {step Q A P1} /\ bisim P1 Q1 +)

bisim_sym < apply H3 to H4.
```
```Subgoal 1:

Variables: P Q A P1 P2
CH : forall P Q, bisim P Q -> bisim Q P +
H2 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\ bisim P2 Q2)
H3 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\ bisim P2 Q2)
H4 : {step Q A P1}
H5 : {step P A P2}
H6 : bisim P2 P1
============================
exists Q1, {step P A Q1} /\ bisim P1 Q1 +

Subgoal 2 is:
forall A Q1, {step P A Q1} -> (exists P1, {step Q A P1} /\ bisim P1 Q1 +)

bisim_sym < apply CH to H6.
```
```Subgoal 1:

Variables: P Q A P1 P2
CH : forall P Q, bisim P Q -> bisim Q P +
H2 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\ bisim P2 Q2)
H3 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\ bisim P2 Q2)
H4 : {step Q A P1}
H5 : {step P A P2}
H6 : bisim P2 P1
H7 : bisim P1 P2 +
============================
exists Q1, {step P A Q1} /\ bisim P1 Q1 +

Subgoal 2 is:
forall A Q1, {step P A Q1} -> (exists P1, {step Q A P1} /\ bisim P1 Q1 +)

bisim_sym < search.
```
```Subgoal 2:

Variables: P Q
CH : forall P Q, bisim P Q -> bisim Q P +
H2 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\ bisim P2 Q2)
H3 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\ bisim P2 Q2)
============================
forall A Q1, {step P A Q1} -> (exists P1, {step Q A P1} /\ bisim P1 Q1 +)

bisim_sym < intros.
```
```Subgoal 2:

Variables: P Q A Q1
CH : forall P Q, bisim P Q -> bisim Q P +
H2 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\ bisim P2 Q2)
H3 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\ bisim P2 Q2)
H4 : {step P A Q1}
============================
exists P1, {step Q A P1} /\ bisim P1 Q1 +

bisim_sym < apply H2 to H4.
```
```Subgoal 2:

Variables: P Q A Q1 Q2
CH : forall P Q, bisim P Q -> bisim Q P +
H2 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\ bisim P2 Q2)
H3 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\ bisim P2 Q2)
H4 : {step P A Q1}
H5 : {step Q A Q2}
H6 : bisim Q1 Q2
============================
exists P1, {step Q A P1} /\ bisim P1 Q1 +

bisim_sym < apply CH to H6.
```
```Subgoal 2:

Variables: P Q A Q1 Q2
CH : forall P Q, bisim P Q -> bisim Q P +
H2 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\ bisim P2 Q2)
H3 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\ bisim P2 Q2)
H4 : {step P A Q1}
H5 : {step Q A Q2}
H6 : bisim Q1 Q2
H7 : bisim Q2 Q1 +
============================
exists P1, {step Q A P1} /\ bisim P1 Q1 +

bisim_sym < search.
Proof completed.
```
```Abella < Theorem bisim_trans :
forall P Q R, bisim P Q -> bisim Q R -> bisim P R.

```
```
============================
forall P Q R, bisim P Q -> bisim Q R -> bisim P R

bisim_trans < coinduction.
```
```
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
============================
forall P Q R, bisim P Q -> bisim Q R -> bisim P R #

bisim_trans < intros.
```
```
Variables: P Q R
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H1 : bisim P Q
H2 : bisim Q R
============================
bisim P R #

bisim_trans < case H1.
```
```
Variables: P Q R
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H2 : bisim Q R
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\ bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\ bisim P2 Q2)
============================
bisim P R #

bisim_trans < case H2.
```
```
Variables: P Q R
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\ bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\ bisim P2 Q2)
H5 : forall A P2, {step Q A P2} -> (exists Q2, {step R A Q2} /\ bisim P2 Q2)
H6 : forall A Q2, {step R A Q2} -> (exists P2, {step Q A P2} /\ bisim P2 Q2)
============================
bisim P R #

bisim_trans < unfold.
```
```Subgoal 1:

Variables: P Q R
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\ bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\ bisim P2 Q2)
H5 : forall A P2, {step Q A P2} -> (exists Q2, {step R A Q2} /\ bisim P2 Q2)
H6 : forall A Q2, {step R A Q2} -> (exists P2, {step Q A P2} /\ bisim P2 Q2)
============================
forall A P1, {step P A P1} -> (exists Q1, {step R A Q1} /\ bisim P1 Q1 +)

Subgoal 2 is:
forall A Q1, {step R A Q1} -> (exists P1, {step P A P1} /\ bisim P1 Q1 +)

bisim_trans < intros.
```
```Subgoal 1:

Variables: P Q R A P1
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\ bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\ bisim P2 Q2)
H5 : forall A P2, {step Q A P2} -> (exists Q2, {step R A Q2} /\ bisim P2 Q2)
H6 : forall A Q2, {step R A Q2} -> (exists P2, {step Q A P2} /\ bisim P2 Q2)
H7 : {step P A P1}
============================
exists Q1, {step R A Q1} /\ bisim P1 Q1 +

Subgoal 2 is:
forall A Q1, {step R A Q1} -> (exists P1, {step P A P1} /\ bisim P1 Q1 +)

bisim_trans < apply H3 to H7.
```
```Subgoal 1:

Variables: P Q R A P1 Q2
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\ bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\ bisim P2 Q2)
H5 : forall A P2, {step Q A P2} -> (exists Q2, {step R A Q2} /\ bisim P2 Q2)
H6 : forall A Q2, {step R A Q2} -> (exists P2, {step Q A P2} /\ bisim P2 Q2)
H7 : {step P A P1}
H8 : {step Q A Q2}
H9 : bisim P1 Q2
============================
exists Q1, {step R A Q1} /\ bisim P1 Q1 +

Subgoal 2 is:
forall A Q1, {step R A Q1} -> (exists P1, {step P A P1} /\ bisim P1 Q1 +)

bisim_trans < apply H5 to H8.
```
```Subgoal 1:

Variables: P Q R A P1 Q2 Q1
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\ bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\ bisim P2 Q2)
H5 : forall A P2, {step Q A P2} -> (exists Q2, {step R A Q2} /\ bisim P2 Q2)
H6 : forall A Q2, {step R A Q2} -> (exists P2, {step Q A P2} /\ bisim P2 Q2)
H7 : {step P A P1}
H8 : {step Q A Q2}
H9 : bisim P1 Q2
H10 : {step R A Q1}
H11 : bisim Q2 Q1
============================
exists Q1, {step R A Q1} /\ bisim P1 Q1 +

Subgoal 2 is:
forall A Q1, {step R A Q1} -> (exists P1, {step P A P1} /\ bisim P1 Q1 +)

bisim_trans < apply CH to H9 H11.
```
```Subgoal 1:

Variables: P Q R A P1 Q2 Q1
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\ bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\ bisim P2 Q2)
H5 : forall A P2, {step Q A P2} -> (exists Q2, {step R A Q2} /\ bisim P2 Q2)
H6 : forall A Q2, {step R A Q2} -> (exists P2, {step Q A P2} /\ bisim P2 Q2)
H7 : {step P A P1}
H8 : {step Q A Q2}
H9 : bisim P1 Q2
H10 : {step R A Q1}
H11 : bisim Q2 Q1
H12 : bisim P1 Q1 +
============================
exists Q1, {step R A Q1} /\ bisim P1 Q1 +

Subgoal 2 is:
forall A Q1, {step R A Q1} -> (exists P1, {step P A P1} /\ bisim P1 Q1 +)

bisim_trans < search.
```
```Subgoal 2:

Variables: P Q R
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\ bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\ bisim P2 Q2)
H5 : forall A P2, {step Q A P2} -> (exists Q2, {step R A Q2} /\ bisim P2 Q2)
H6 : forall A Q2, {step R A Q2} -> (exists P2, {step Q A P2} /\ bisim P2 Q2)
============================
forall A Q1, {step R A Q1} -> (exists P1, {step P A P1} /\ bisim P1 Q1 +)

bisim_trans < intros.
```
```Subgoal 2:

Variables: P Q R A Q1
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\ bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\ bisim P2 Q2)
H5 : forall A P2, {step Q A P2} -> (exists Q2, {step R A Q2} /\ bisim P2 Q2)
H6 : forall A Q2, {step R A Q2} -> (exists P2, {step Q A P2} /\ bisim P2 Q2)
H7 : {step R A Q1}
============================
exists P1, {step P A P1} /\ bisim P1 Q1 +

bisim_trans < apply H6 to H7.
```
```Subgoal 2:

Variables: P Q R A Q1 P2
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\ bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\ bisim P2 Q2)
H5 : forall A P2, {step Q A P2} -> (exists Q2, {step R A Q2} /\ bisim P2 Q2)
H6 : forall A Q2, {step R A Q2} -> (exists P2, {step Q A P2} /\ bisim P2 Q2)
H7 : {step R A Q1}
H8 : {step Q A P2}
H9 : bisim P2 Q1
============================
exists P1, {step P A P1} /\ bisim P1 Q1 +

bisim_trans < apply H4 to H8.
```
```Subgoal 2:

Variables: P Q R A Q1 P2 P1
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\ bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\ bisim P2 Q2)
H5 : forall A P2, {step Q A P2} -> (exists Q2, {step R A Q2} /\ bisim P2 Q2)
H6 : forall A Q2, {step R A Q2} -> (exists P2, {step Q A P2} /\ bisim P2 Q2)
H7 : {step R A Q1}
H8 : {step Q A P2}
H9 : bisim P2 Q1
H10 : {step P A P1}
H11 : bisim P1 P2
============================
exists P1, {step P A P1} /\ bisim P1 Q1 +

bisim_trans < apply CH to H11 H9.
```
```Subgoal 2:

Variables: P Q R A Q1 P2 P1
CH : forall P Q R, bisim P Q -> bisim Q R -> bisim P R +
H3 : forall A P2, {step P A P2} -> (exists Q2, {step Q A Q2} /\ bisim P2 Q2)
H4 : forall A Q2, {step Q A Q2} -> (exists P2, {step P A P2} /\ bisim P2 Q2)
H5 : forall A P2, {step Q A P2} -> (exists Q2, {step R A Q2} /\ bisim P2 Q2)
H6 : forall A Q2, {step R A Q2} -> (exists P2, {step Q A P2} /\ bisim P2 Q2)
H7 : {step R A Q1}
H8 : {step Q A P2}
H9 : bisim P2 Q1
H10 : {step P A P1}
H11 : bisim P1 P2
H12 : bisim P1 Q1 +
============================
exists P1, {step P A P1} /\ bisim P1 Q1 +

bisim_trans < search.
Proof completed.
```
```Abella <
```