Welcome to Abella 2.0.5-dev.
Abella < Specification "ccs".
Reading 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 <