Welcome to Abella 2.0.5-dev.
Abella < Kind name, action type.

Abella < Type tau action.

Abella < Type up, dn name -> action.

Abella < Define is_action : action -> prop by 
is_action tau;
is_action (up N);
is_action (dn N).

Abella < Kind proc type.

Abella < Type null proc.

Abella < Type plus, par proc -> proc -> proc.

Abella < Type act action -> proc -> proc.

Abella < Type repl proc -> proc.

Abella < Define is_proc : proc -> prop by 
is_proc null;
is_proc (plus P Q) := is_proc P /\ is_proc Q;
is_proc (par P Q) := is_proc P /\ is_proc Q;
is_proc (act A P) := is_action A /\ is_proc P;
is_proc (repl P) := is_proc P.

Abella < Define one : proc -> action -> proc -> prop by 
one (act A P) A P;
one (plus P1 P2) A Q := one P1 A Q;
one (plus P1 P2) A Q := one P2 A Q;
one (par P Q) A (par P1 Q) := one P A P1;
one (par P Q) A (par P Q1) := one Q A Q1;
one (repl P) A (par (repl P) Q) := one P A Q;
one (par P Q) tau (par P1 Q1) := exists X, one P (up X) P1 /\ one Q (dn X) Q1;
one (par P Q) tau (par P1 Q1) := exists X, one P (dn X) P1 /\ one Q (up X) Q1;
one (repl P) tau (par (repl P) (par Q R)) := exists X, one P (up X) Q /\ one P (dn X) R.

Abella < CoDefine bisim_up_to : (proc -> proc -> proc -> proc -> prop) -> proc -> proc -> prop by 
bisim_up_to Tech P Q := (forall A P1, one P A P1 ->
     (exists Q1, one Q A Q1 /\
          (exists P2 Q2, Tech P1 P2 Q1 Q2 /\ bisim_up_to Tech P2 Q2))) /\
  (forall A Q1, one Q A Q1 ->
       (exists P1, one P A P1 /\
            (exists P2 Q2, Tech P1 P2 Q1 Q2 /\ bisim_up_to Tech P2 Q2))).

Abella < Define refl_t : proc -> proc -> proc -> proc -> prop by 
refl_t P P Q Q.

Abella < Define is_sound : (proc -> proc -> proc -> proc -> prop) -> prop by 
is_sound Tech := forall P Q, bisim_up_to Tech P Q -> bisim_up_to refl_t P Q.
Warning: Definition can be used to defeat stratification
 (higher-order argument "Tech" occurs to the left of ->)

Abella < CoDefine bisim : proc -> proc -> prop by 
bisim P Q := bisim_up_to refl_t P Q.

Abella < Define symmetric_rel : (proc -> proc -> prop) -> prop by 
symmetric_rel Rel := forall P Q, Rel P Q -> Rel Q P.
Warning: Definition can be used to defeat stratification
 (higher-order argument "Rel" occurs to the left of ->)

Abella < Theorem bisim_symmetric : 
symmetric_rel (bisim_up_to refl_t).


============================
 symmetric_rel (bisim_up_to refl_t)

bisim_symmetric < unfold.

============================
 forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P

bisim_symmetric < coinduction.

CH : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P +
============================
 forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P #

bisim_symmetric < intros.

Variables: P Q
CH : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P +
H1 : bisim_up_to refl_t P Q
============================
 bisim_up_to refl_t Q P #

bisim_symmetric < case H1.

Variables: P Q
CH : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P +
H2 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H3 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
============================
 bisim_up_to refl_t Q P #

bisim_symmetric < unfold.
Subgoal 1:

Variables: P Q
CH : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P +
H2 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H3 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
============================
 forall A P1, one Q 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 Q A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_symmetric < intros.
Subgoal 1:

Variables: P Q A P1
CH : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P +
H2 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H3 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : one Q 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 Q A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_symmetric < apply H3 to H4.
Subgoal 1:

Variables: P Q A P1 P2 P3 Q3
CH : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P +
H2 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H3 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : one Q A P1
H5 : one P A P2
H6 : refl_t P2 P3 P1 Q3
H7 : bisim_up_to refl_t P3 Q3
============================
 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 Q A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_symmetric < case H6.
Subgoal 1:

Variables: P Q A P3 Q3
CH : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P +
H2 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H3 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : one Q A Q3
H5 : one P A P3
H7 : bisim_up_to refl_t P3 Q3
============================
 exists Q1, one P A Q1 /\
   (exists P2 Q2, refl_t Q3 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

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

bisim_symmetric < exists P3.
Subgoal 1:

Variables: P Q A P3 Q3
CH : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P +
H2 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H3 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : one Q A Q3
H5 : one P A P3
H7 : bisim_up_to refl_t P3 Q3
============================
 one P A P3 /\
   (exists P2 Q2, refl_t Q3 P2 P3 Q2 /\ bisim_up_to refl_t P2 Q2 +)

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

bisim_symmetric < split.
Subgoal 1.1:

Variables: P Q A P3 Q3
CH : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P +
H2 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H3 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : one Q A Q3
H5 : one P A P3
H7 : bisim_up_to refl_t P3 Q3
============================
 one P A P3

Subgoal 1.2 is:
 exists P2 Q2, refl_t Q3 P2 P3 Q2 /\ bisim_up_to refl_t P2 Q2 +

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

bisim_symmetric < search.
Subgoal 1.2:

Variables: P Q A P3 Q3
CH : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P +
H2 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H3 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : one Q A Q3
H5 : one P A P3
H7 : bisim_up_to refl_t P3 Q3
============================
 exists P2 Q2, refl_t Q3 P2 P3 Q2 /\ bisim_up_to refl_t P2 Q2 +

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

bisim_symmetric < witness Q3.
Subgoal 1.2:

Variables: P Q A P3 Q3
CH : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P +
H2 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H3 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : one Q A Q3
H5 : one P A P3
H7 : bisim_up_to refl_t P3 Q3
============================
 exists Q2, refl_t Q3 Q3 P3 Q2 /\ bisim_up_to refl_t Q3 Q2 +

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

bisim_symmetric < witness P3.
Subgoal 1.2:

Variables: P Q A P3 Q3
CH : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P +
H2 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H3 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : one Q A Q3
H5 : one P A P3
H7 : bisim_up_to refl_t P3 Q3
============================
 refl_t Q3 Q3 P3 P3 /\ bisim_up_to refl_t Q3 P3 +

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

bisim_symmetric < split.
Subgoal 1.2.1:

Variables: P Q A P3 Q3
CH : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P +
H2 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H3 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : one Q A Q3
H5 : one P A P3
H7 : bisim_up_to refl_t P3 Q3
============================
 refl_t Q3 Q3 P3 P3

Subgoal 1.2.2 is:
 bisim_up_to refl_t Q3 P3 +

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

bisim_symmetric < search.
Subgoal 1.2.2:

Variables: P Q A P3 Q3
CH : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P +
H2 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H3 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : one Q A Q3
H5 : one P A P3
H7 : bisim_up_to refl_t P3 Q3
============================
 bisim_up_to refl_t Q3 P3 +

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

bisim_symmetric < backchain CH.
Subgoal 2:

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

bisim_symmetric < intros.
Subgoal 2:

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

bisim_symmetric < apply H2 to H4.
Subgoal 2:

Variables: P Q A Q1 Q2 P3 Q3
CH : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P +
H2 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H3 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : one P A Q1
H5 : one Q A Q2
H6 : refl_t Q1 P3 Q2 Q3
H7 : bisim_up_to refl_t P3 Q3
============================
 exists P1, one Q A P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_symmetric < case H6.
Subgoal 2:

Variables: P Q A P3 Q3
CH : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P +
H2 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H3 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : one P A P3
H5 : one Q A Q3
H7 : bisim_up_to refl_t P3 Q3
============================
 exists P1, one Q A P1 /\
   (exists P2 Q2, refl_t P1 P2 P3 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_symmetric < exists Q3.
Subgoal 2:

Variables: P Q A P3 Q3
CH : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P +
H2 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H3 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : one P A P3
H5 : one Q A Q3
H7 : bisim_up_to refl_t P3 Q3
============================
 one Q A Q3 /\
   (exists P2 Q2, refl_t Q3 P2 P3 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_symmetric < split.
Subgoal 2.1:

Variables: P Q A P3 Q3
CH : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P +
H2 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H3 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : one P A P3
H5 : one Q A Q3
H7 : bisim_up_to refl_t P3 Q3
============================
 one Q A Q3

Subgoal 2.2 is:
 exists P2 Q2, refl_t Q3 P2 P3 Q2 /\ bisim_up_to refl_t P2 Q2 +

bisim_symmetric < search.
Subgoal 2.2:

Variables: P Q A P3 Q3
CH : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P +
H2 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H3 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : one P A P3
H5 : one Q A Q3
H7 : bisim_up_to refl_t P3 Q3
============================
 exists P2 Q2, refl_t Q3 P2 P3 Q2 /\ bisim_up_to refl_t P2 Q2 +

bisim_symmetric < witness Q3.
Subgoal 2.2:

Variables: P Q A P3 Q3
CH : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P +
H2 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H3 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : one P A P3
H5 : one Q A Q3
H7 : bisim_up_to refl_t P3 Q3
============================
 exists Q2, refl_t Q3 Q3 P3 Q2 /\ bisim_up_to refl_t Q3 Q2 +

bisim_symmetric < witness P3.
Subgoal 2.2:

Variables: P Q A P3 Q3
CH : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P +
H2 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H3 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : one P A P3
H5 : one Q A Q3
H7 : bisim_up_to refl_t P3 Q3
============================
 refl_t Q3 Q3 P3 P3 /\ bisim_up_to refl_t Q3 P3 +

bisim_symmetric < split.
Subgoal 2.2.1:

Variables: P Q A P3 Q3
CH : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P +
H2 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H3 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : one P A P3
H5 : one Q A Q3
H7 : bisim_up_to refl_t P3 Q3
============================
 refl_t Q3 Q3 P3 P3

Subgoal 2.2.2 is:
 bisim_up_to refl_t Q3 P3 +

bisim_symmetric < search.
Subgoal 2.2.2:

Variables: P Q A P3 Q3
CH : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P +
H2 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H3 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : one P A P3
H5 : one Q A Q3
H7 : bisim_up_to refl_t P3 Q3
============================
 bisim_up_to refl_t Q3 P3 +

bisim_symmetric < backchain CH.
Proof completed.
Abella < Theorem bisim_symmetric_ : 
forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P.


============================
 forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P

bisim_symmetric_ < apply bisim_symmetric.

H1 : symmetric_rel (bisim_up_to refl_t)
============================
 forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P

bisim_symmetric_ < case H1.

H2 : forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P
============================
 forall P Q, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q P

bisim_symmetric_ < search.
Proof completed.
Abella < Define transitive_rel : (proc -> proc -> prop) -> prop by 
transitive_rel Rel := forall P Q R, Rel P Q -> Rel Q R -> Rel P R.
Warning: Definition can be used to defeat stratification
 (higher-order argument "Rel" occurs to the left of ->)

Abella < Theorem bisim_transitive : 
transitive_rel (bisim_up_to refl_t).


============================
 transitive_rel (bisim_up_to refl_t)

bisim_transitive < unfold.

============================
 forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
   bisim_up_to refl_t P R

bisim_transitive < coinduction.

CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
============================
 forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
   bisim_up_to refl_t P R #

bisim_transitive < intros.

Variables: P Q R
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H1 : bisim_up_to refl_t P Q
H2 : bisim_up_to refl_t Q R
============================
 bisim_up_to refl_t P R #

bisim_transitive < case H1.

Variables: P Q R
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H2 : bisim_up_to refl_t Q R
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
============================
 bisim_up_to refl_t P R #

bisim_transitive < case H2.

Variables: P Q R
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
============================
 bisim_up_to refl_t P R #

bisim_transitive < unfold.
Subgoal 1:

Variables: P Q R
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
============================
 forall A P1, one P A P1 ->
   (exists Q1, one 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 R A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_transitive < intros.
Subgoal 1:

Variables: P Q R A P1
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one P A P1
============================
 exists Q1, one 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 R A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_transitive < apply H3 to H7.
Subgoal 1:

Variables: P Q R A P1 Q2 P3 Q3
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one P A P1
H8 : one Q A Q2
H9 : refl_t P1 P3 Q2 Q3
H10 : bisim_up_to refl_t P3 Q3
============================
 exists Q1, one 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 R A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_transitive < apply H5 to H8.
Subgoal 1:

Variables: P Q R A P1 Q2 P3 Q3 Q1 P2 Q4
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one P A P1
H8 : one Q A Q2
H9 : refl_t P1 P3 Q2 Q3
H10 : bisim_up_to refl_t P3 Q3
H11 : one R A Q1
H12 : refl_t Q2 P2 Q1 Q4
H13 : bisim_up_to refl_t P2 Q4
============================
 exists Q1, one 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 R A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_transitive < case H9.
Subgoal 1:

Variables: P Q R A P3 Q3 Q1 P2 Q4
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one P A P3
H8 : one Q A Q3
H10 : bisim_up_to refl_t P3 Q3
H11 : one R A Q1
H12 : refl_t Q3 P2 Q1 Q4
H13 : bisim_up_to refl_t P2 Q4
============================
 exists Q1, one R A Q1 /\
   (exists P2 Q2, refl_t P3 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

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

bisim_transitive < case H12.
Subgoal 1:

Variables: P Q R A P3 P2 Q4
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one P A P3
H8 : one Q A P2
H10 : bisim_up_to refl_t P3 P2
H11 : one R A Q4
H13 : bisim_up_to refl_t P2 Q4
============================
 exists Q1, one R A Q1 /\
   (exists P2 Q2, refl_t P3 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

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

bisim_transitive < exists Q4.
Subgoal 1:

Variables: P Q R A P3 P2 Q4
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one P A P3
H8 : one Q A P2
H10 : bisim_up_to refl_t P3 P2
H11 : one R A Q4
H13 : bisim_up_to refl_t P2 Q4
============================
 one R A Q4 /\
   (exists P2 Q2, refl_t P3 P2 Q4 Q2 /\ bisim_up_to refl_t P2 Q2 +)

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

bisim_transitive < split.
Subgoal 1.1:

Variables: P Q R A P3 P2 Q4
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one P A P3
H8 : one Q A P2
H10 : bisim_up_to refl_t P3 P2
H11 : one R A Q4
H13 : bisim_up_to refl_t P2 Q4
============================
 one R A Q4

Subgoal 1.2 is:
 exists P2 Q2, refl_t P3 P2 Q4 Q2 /\ bisim_up_to refl_t P2 Q2 +

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

bisim_transitive < search.
Subgoal 1.2:

Variables: P Q R A P3 P2 Q4
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one P A P3
H8 : one Q A P2
H10 : bisim_up_to refl_t P3 P2
H11 : one R A Q4
H13 : bisim_up_to refl_t P2 Q4
============================
 exists P2 Q2, refl_t P3 P2 Q4 Q2 /\ bisim_up_to refl_t P2 Q2 +

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

bisim_transitive < witness P3.
Subgoal 1.2:

Variables: P Q R A P3 P2 Q4
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one P A P3
H8 : one Q A P2
H10 : bisim_up_to refl_t P3 P2
H11 : one R A Q4
H13 : bisim_up_to refl_t P2 Q4
============================
 exists Q2, refl_t P3 P3 Q4 Q2 /\ bisim_up_to refl_t P3 Q2 +

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

bisim_transitive < witness Q4.
Subgoal 1.2:

Variables: P Q R A P3 P2 Q4
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one P A P3
H8 : one Q A P2
H10 : bisim_up_to refl_t P3 P2
H11 : one R A Q4
H13 : bisim_up_to refl_t P2 Q4
============================
 refl_t P3 P3 Q4 Q4 /\ bisim_up_to refl_t P3 Q4 +

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

bisim_transitive < split.
Subgoal 1.2.1:

Variables: P Q R A P3 P2 Q4
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one P A P3
H8 : one Q A P2
H10 : bisim_up_to refl_t P3 P2
H11 : one R A Q4
H13 : bisim_up_to refl_t P2 Q4
============================
 refl_t P3 P3 Q4 Q4

Subgoal 1.2.2 is:
 bisim_up_to refl_t P3 Q4 +

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

bisim_transitive < search.
Subgoal 1.2.2:

Variables: P Q R A P3 P2 Q4
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one P A P3
H8 : one Q A P2
H10 : bisim_up_to refl_t P3 P2
H11 : one R A Q4
H13 : bisim_up_to refl_t P2 Q4
============================
 bisim_up_to refl_t P3 Q4 +

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

bisim_transitive < backchain CH.
Subgoal 2:

Variables: P Q R
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
============================
 forall A Q1, one R A Q1 ->
   (exists P1, one P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_transitive < intros.
Subgoal 2:

Variables: P Q R A Q1
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one R A Q1
============================
 exists P1, one P A P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_transitive < apply H6 to H7.
Subgoal 2:

Variables: P Q R A Q1 P2 P3 Q3
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one R A Q1
H8 : one Q A P2
H9 : refl_t P2 P3 Q1 Q3
H10 : bisim_up_to refl_t P3 Q3
============================
 exists P1, one P A P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_transitive < apply H4 to H8.
Subgoal 2:

Variables: P Q R A Q1 P2 P3 Q3 P1 P4 Q2
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one R A Q1
H8 : one Q A P2
H9 : refl_t P2 P3 Q1 Q3
H10 : bisim_up_to refl_t P3 Q3
H11 : one P A P1
H12 : refl_t P1 P4 P2 Q2
H13 : bisim_up_to refl_t P4 Q2
============================
 exists P1, one P A P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_transitive < case H9.
Subgoal 2:

Variables: P Q R A P3 Q3 P1 P4 Q2
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one R A Q3
H8 : one Q A P3
H10 : bisim_up_to refl_t P3 Q3
H11 : one P A P1
H12 : refl_t P1 P4 P3 Q2
H13 : bisim_up_to refl_t P4 Q2
============================
 exists P1, one P A P1 /\
   (exists P2 Q2, refl_t P1 P2 Q3 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_transitive < case H12.
Subgoal 2:

Variables: P Q R A Q3 P4 Q2
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one R A Q3
H8 : one Q A Q2
H10 : bisim_up_to refl_t Q2 Q3
H11 : one P A P4
H13 : bisim_up_to refl_t P4 Q2
============================
 exists P1, one P A P1 /\
   (exists P2 Q2, refl_t P1 P2 Q3 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_transitive < exists P4.
Subgoal 2:

Variables: P Q R A Q3 P4 Q2
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one R A Q3
H8 : one Q A Q2
H10 : bisim_up_to refl_t Q2 Q3
H11 : one P A P4
H13 : bisim_up_to refl_t P4 Q2
============================
 one P A P4 /\
   (exists P2 Q2, refl_t P4 P2 Q3 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_transitive < split.
Subgoal 2.1:

Variables: P Q R A Q3 P4 Q2
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one R A Q3
H8 : one Q A Q2
H10 : bisim_up_to refl_t Q2 Q3
H11 : one P A P4
H13 : bisim_up_to refl_t P4 Q2
============================
 one P A P4

Subgoal 2.2 is:
 exists P2 Q2, refl_t P4 P2 Q3 Q2 /\ bisim_up_to refl_t P2 Q2 +

bisim_transitive < search.
Subgoal 2.2:

Variables: P Q R A Q3 P4 Q2
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one R A Q3
H8 : one Q A Q2
H10 : bisim_up_to refl_t Q2 Q3
H11 : one P A P4
H13 : bisim_up_to refl_t P4 Q2
============================
 exists P2 Q2, refl_t P4 P2 Q3 Q2 /\ bisim_up_to refl_t P2 Q2 +

bisim_transitive < witness P4.
Subgoal 2.2:

Variables: P Q R A Q3 P4 Q2
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one R A Q3
H8 : one Q A Q2
H10 : bisim_up_to refl_t Q2 Q3
H11 : one P A P4
H13 : bisim_up_to refl_t P4 Q2
============================
 exists Q2, refl_t P4 P4 Q3 Q2 /\ bisim_up_to refl_t P4 Q2 +

bisim_transitive < witness Q3.
Subgoal 2.2:

Variables: P Q R A Q3 P4 Q2
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one R A Q3
H8 : one Q A Q2
H10 : bisim_up_to refl_t Q2 Q3
H11 : one P A P4
H13 : bisim_up_to refl_t P4 Q2
============================
 refl_t P4 P4 Q3 Q3 /\ bisim_up_to refl_t P4 Q3 +

bisim_transitive < split.
Subgoal 2.2.1:

Variables: P Q R A Q3 P4 Q2
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one R A Q3
H8 : one Q A Q2
H10 : bisim_up_to refl_t Q2 Q3
H11 : one P A P4
H13 : bisim_up_to refl_t P4 Q2
============================
 refl_t P4 P4 Q3 Q3

Subgoal 2.2.2 is:
 bisim_up_to refl_t P4 Q3 +

bisim_transitive < search.
Subgoal 2.2.2:

Variables: P Q R A Q3 P4 Q2
CH : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R +
H3 : forall A P2, one P A P2 ->
       (exists Q2, one Q A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H4 : forall A Q2, one Q A Q2 ->
       (exists P2, one P A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H5 : forall A P2, one Q A P2 ->
       (exists Q2, one R A Q2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H6 : forall A Q2, one R A Q2 ->
       (exists P2, one Q A P2 /\
            (exists P3 Q3, refl_t P2 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
H7 : one R A Q3
H8 : one Q A Q2
H10 : bisim_up_to refl_t Q2 Q3
H11 : one P A P4
H13 : bisim_up_to refl_t P4 Q2
============================
 bisim_up_to refl_t P4 Q3 +

bisim_transitive < backchain CH.
Proof completed.
Abella < Theorem bisim_transitive_ : 
forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
  bisim_up_to refl_t P R.


============================
 forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
   bisim_up_to refl_t P R

bisim_transitive_ < apply bisim_transitive.

H1 : transitive_rel (bisim_up_to refl_t)
============================
 forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
   bisim_up_to refl_t P R

bisim_transitive_ < case H1.

H2 : forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
       bisim_up_to refl_t P R
============================
 forall P Q R, bisim_up_to refl_t P Q -> bisim_up_to refl_t Q R ->
   bisim_up_to refl_t P R

bisim_transitive_ < search.
Proof completed.
Abella < Define reflexive_rel : (proc -> proc -> prop) -> prop by 
reflexive_rel Rel := forall P, Rel P P.

Abella < Theorem bisim_reflexive : 
reflexive_rel (bisim_up_to refl_t).


============================
 reflexive_rel (bisim_up_to refl_t)

bisim_reflexive < unfold.

============================
 forall P, bisim_up_to refl_t P P

bisim_reflexive < coinduction.

CH : forall P, bisim_up_to refl_t P P +
============================
 forall P, bisim_up_to refl_t P P #

bisim_reflexive < intros.

Variables: P
CH : forall P, bisim_up_to refl_t P P +
============================
 bisim_up_to refl_t P P #

bisim_reflexive < unfold.
Subgoal 1:

Variables: P
CH : forall P, bisim_up_to refl_t P P +
============================
 forall A P1, one P 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 P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_reflexive < intros.
Subgoal 1:

Variables: P A P1
CH : forall P, bisim_up_to refl_t P P +
H1 : one P 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 P A P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

bisim_reflexive < witness P1.
Subgoal 1:

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

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

bisim_reflexive < split.
Subgoal 1.1:

Variables: P A P1
CH : forall P, bisim_up_to refl_t P P +
H1 : one P A P1
============================
 one P A P1

Subgoal 1.2 is:
 exists P2 Q2, refl_t P1 P2 P1 Q2 /\ bisim_up_to refl_t P2 Q2 +

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

bisim_reflexive < search.
Subgoal 1.2:

Variables: P A P1
CH : forall P, bisim_up_to refl_t P P +
H1 : one P A P1
============================
 exists P2 Q2, refl_t P1 P2 P1 Q2 /\ bisim_up_to refl_t P2 Q2 +

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

bisim_reflexive < witness P1.
Subgoal 1.2:

Variables: P A P1
CH : forall P, bisim_up_to refl_t P P +
H1 : one P A P1
============================
 exists Q2, refl_t P1 P1 P1 Q2 /\ bisim_up_to refl_t P1 Q2 +

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

bisim_reflexive < witness P1.
Subgoal 1.2:

Variables: P A P1
CH : forall P, bisim_up_to refl_t P P +
H1 : one P A P1
============================
 refl_t P1 P1 P1 P1 /\ bisim_up_to refl_t P1 P1 +

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

bisim_reflexive < split.
Subgoal 1.2.1:

Variables: P A P1
CH : forall P, bisim_up_to refl_t P P +
H1 : one P A P1
============================
 refl_t P1 P1 P1 P1

Subgoal 1.2.2 is:
 bisim_up_to refl_t P1 P1 +

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

bisim_reflexive < search.
Subgoal 1.2.2:

Variables: P A P1
CH : forall P, bisim_up_to refl_t P P +
H1 : one P A P1
============================
 bisim_up_to refl_t P1 P1 +

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

bisim_reflexive < backchain CH.
Subgoal 2:

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

bisim_reflexive < intros.
Subgoal 2:

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

bisim_reflexive < witness Q1.
Subgoal 2:

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

bisim_reflexive < split.
Subgoal 2.1:

Variables: P A Q1
CH : forall P, bisim_up_to refl_t P P +
H1 : one P A Q1
============================
 one P A Q1

Subgoal 2.2 is:
 exists P2 Q2, refl_t Q1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +

bisim_reflexive < search.
Subgoal 2.2:

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

bisim_reflexive < witness Q1.
Subgoal 2.2:

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

bisim_reflexive < witness Q1.
Subgoal 2.2:

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

bisim_reflexive < split.
Subgoal 2.2.1:

Variables: P A Q1
CH : forall P, bisim_up_to refl_t P P +
H1 : one P A Q1
============================
 refl_t Q1 Q1 Q1 Q1

Subgoal 2.2.2 is:
 bisim_up_to refl_t Q1 Q1 +

bisim_reflexive < search.
Subgoal 2.2.2:

Variables: P A Q1
CH : forall P, bisim_up_to refl_t P P +
H1 : one P A Q1
============================
 bisim_up_to refl_t Q1 Q1 +

bisim_reflexive < backchain CH.
Proof completed.
Abella < Theorem bisim_reflexive_ : 
forall P, bisim_up_to refl_t P P.


============================
 forall P, bisim_up_to refl_t P P

bisim_reflexive_ < apply bisim_reflexive.

H1 : reflexive_rel (bisim_up_to refl_t)
============================
 forall P, bisim_up_to refl_t P P

bisim_reflexive_ < case H1.

H2 : forall P, bisim_up_to refl_t P P
============================
 forall P, bisim_up_to refl_t P P

bisim_reflexive_ < search.
Proof completed.
Abella < Define equiv_rel : (proc -> proc -> prop) -> prop by 
equiv_rel R := reflexive_rel R /\ symmetric_rel R /\ transitive_rel R.

Abella < Theorem bisim_equiv : 
equiv_rel (bisim_up_to refl_t).


============================
 equiv_rel (bisim_up_to refl_t)

bisim_equiv < unfold.
Subgoal 1:

============================
 reflexive_rel (bisim_up_to refl_t)

Subgoal 2 is:
 symmetric_rel (bisim_up_to refl_t)

Subgoal 3 is:
 transitive_rel (bisim_up_to refl_t)

bisim_equiv < backchain bisim_reflexive.
Subgoal 2:

============================
 symmetric_rel (bisim_up_to refl_t)

Subgoal 3 is:
 transitive_rel (bisim_up_to refl_t)

bisim_equiv < backchain bisim_symmetric.
Subgoal 3:

============================
 transitive_rel (bisim_up_to refl_t)

bisim_equiv < backchain bisim_transitive.
Proof completed.
Abella <