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

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

Abella < Define bisim_t : proc -> proc -> proc -> proc -> prop by 
bisim_t P1 P2 Q1 Q2 := bisim_up_to refl_t P1 P2 /\ bisim_up_to refl_t Q1 Q2.

Abella < Define is_sound_fst : (proc -> proc -> proc -> proc -> prop) -> prop by 
is_sound_fst Tech := forall P Q, (exists R S, bisim_up_to refl_t P R /\ bisim_up_to Tech R S /\
                 bisim_up_to refl_t S 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 < Define is_sound_snd : (proc -> proc -> proc -> proc -> prop) -> prop by 
is_sound_snd Tech := forall P Q, bisim_up_to Tech P Q ->
  (exists R S, bisim_up_to refl_t P R /\ bisim_up_to Tech R S /\
       bisim_up_to refl_t S Q).
Warning: Definition can be used to defeat stratification
 (higher-order argument "Tech" occurs to the left of ->)

Abella < Theorem bisim_t_reflexive : 
forall P, bisim_t P P P P.


============================
 forall P, bisim_t P P P P

bisim_t_reflexive < intros.

Variables: P
============================
 bisim_t P P P P

bisim_t_reflexive < unfold.
Subgoal 1:

Variables: P
============================
 bisim_up_to refl_t P P

Subgoal 2 is:
 bisim_up_to refl_t P P

bisim_t_reflexive < backchain bisim_reflexive_.
Subgoal 2:

Variables: P
============================
 bisim_up_to refl_t P P

bisim_t_reflexive < backchain bisim_reflexive_.
Proof completed.
Abella < Theorem bisim_sound_fst : 
is_sound_fst bisim_t.


============================
 is_sound_fst bisim_t

bisim_sound_fst < unfold.

============================
 forall P Q, (exists R S, bisim_up_to refl_t P R /\
                  bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
   bisim_up_to refl_t P Q

bisim_sound_fst < coinduction.

CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
============================
 forall P Q, (exists R S, bisim_up_to refl_t P R /\
                  bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
   bisim_up_to refl_t P Q #

bisim_sound_fst < intros.

Variables: P Q
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H1 : exists R S, bisim_up_to refl_t P R /\ bisim_up_to bisim_t R S /\
       bisim_up_to refl_t S Q
============================
 bisim_up_to refl_t P Q #

bisim_sound_fst < case H1.

Variables: P Q R S
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
H2 : bisim_up_to refl_t P R
H3 : bisim_up_to bisim_t R S
H4 : bisim_up_to refl_t S Q
============================
 bisim_up_to refl_t P Q #

bisim_sound_fst < rename H2 to Left.

Variables: P Q R S
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
H3 : bisim_up_to bisim_t R S
H4 : bisim_up_to refl_t S Q
============================
 bisim_up_to refl_t P Q #

bisim_sound_fst < rename H3 to Middle.

Variables: P Q R S
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Middle : bisim_up_to bisim_t R S
H4 : bisim_up_to refl_t S Q
============================
 bisim_up_to refl_t P Q #

bisim_sound_fst < rename H4 to Right.

Variables: P Q R S
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Middle : bisim_up_to bisim_t R S
Right : bisim_up_to refl_t S Q
============================
 bisim_up_to refl_t P Q #

bisim_sound_fst < unfold.
Subgoal 1:

Variables: P Q R S
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Middle : bisim_up_to bisim_t R S
Right : bisim_up_to refl_t S Q
============================
 forall A P1, one P A P1 ->
   (exists Q1, one Q 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 Q 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_sound_fst < intros Pstep.
Subgoal 1:

Variables: P Q R S A P1
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Middle : bisim_up_to bisim_t R S
Right : bisim_up_to refl_t S Q
Pstep : one P A P1
============================
 exists Q1, one Q 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 Q 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_sound_fst < Left : case Left.
Subgoal 1:

Variables: P Q R S A P1
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Middle : bisim_up_to bisim_t R S
Right : bisim_up_to refl_t S Q
Pstep : one P A P1
Left : forall A P1, one P A P1 ->
         (exists Q2, one R A Q2 /\
              (exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
Left1 : forall A Q2, one R A Q2 ->
          (exists P1, one P A P1 /\
               (exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
============================
 exists Q1, one Q 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 Q 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_sound_fst < clear Left1.
Subgoal 1:

Variables: P Q R S A P1
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Middle : bisim_up_to bisim_t R S
Right : bisim_up_to refl_t S Q
Pstep : one P A P1
Left : forall A P1, one P A P1 ->
         (exists Q2, one R A Q2 /\
              (exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
============================
 exists Q1, one Q 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 Q 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_sound_fst < Left : apply Left to Pstep.
Subgoal 1:

Variables: P Q R S A P1 Q2 P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Middle : bisim_up_to bisim_t R S
Right : bisim_up_to refl_t S Q
Pstep : one P A P1
Left : forall A P1, one P A P1 ->
         (exists Q2, one R A Q2 /\
              (exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
Left1 : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
============================
 exists Q1, one Q 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 Q 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_sound_fst < clear Left.
Subgoal 1:

Variables: P Q R S A P1 Q2 P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Middle : bisim_up_to bisim_t R S
Right : bisim_up_to refl_t S Q
Pstep : one P A P1
Left1 : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
============================
 exists Q1, one Q 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 Q 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_sound_fst < rename Left1 to PPstep.
Subgoal 1:

Variables: P Q R S A P1 Q2 P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Middle : bisim_up_to bisim_t R S
Right : bisim_up_to refl_t S Q
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
============================
 exists Q1, one Q 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 Q 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_sound_fst < Middle : case Middle.
Subgoal 1:

Variables: P Q R S A P1 Q2 P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Right : bisim_up_to refl_t S Q
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
Middle : forall A P1, one R A P1 ->
           (exists Q2, one S A Q2 /\
                (exists P3 Q3, bisim_t P1 P3 Q2 Q3 /\
                     bisim_up_to bisim_t P3 Q3))
Middle1 : forall A Q2, one S A Q2 ->
            (exists P1, one R A P1 /\
                 (exists P3 Q3, bisim_t P1 P3 Q2 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
============================
 exists Q1, one Q 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 Q 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_sound_fst < clear Middle1.
Subgoal 1:

Variables: P Q R S A P1 Q2 P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Right : bisim_up_to refl_t S Q
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
Middle : forall A P1, one R A P1 ->
           (exists Q2, one S A Q2 /\
                (exists P3 Q3, bisim_t P1 P3 Q2 Q3 /\
                     bisim_up_to bisim_t P3 Q3))
============================
 exists Q1, one Q 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 Q 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_sound_fst < Middle : apply Middle to PPstep.
Subgoal 1:

Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Right : bisim_up_to refl_t S Q
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
Middle : forall A P1, one R A P1 ->
           (exists Q2, one S A Q2 /\
                (exists P3 Q3, bisim_t P1 P3 Q2 Q3 /\
                     bisim_up_to bisim_t P3 Q3))
Middle1 : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
============================
 exists Q1, one Q 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 Q 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_sound_fst < clear Middle.
Subgoal 1:

Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Right : bisim_up_to refl_t S Q
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
Middle1 : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
============================
 exists Q1, one Q 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 Q 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_sound_fst < rename Middle1 to QQstep.
Subgoal 1:

Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Right : bisim_up_to refl_t S Q
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
============================
 exists Q1, one Q 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 Q 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_sound_fst < Right : case Right.
Subgoal 1:

Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Right : forall A P1, one S A P1 ->
          (exists Q1, one Q A Q1 /\
               (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
Right1 : forall A Q1, one Q A Q1 ->
           (exists P1, one S A P1 /\
                (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\
                     bisim_up_to refl_t P2 Q2))
============================
 exists Q1, one Q 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 Q 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_sound_fst < clear Right1.
Subgoal 1:

Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Right : forall A P1, one S A P1 ->
          (exists Q1, one Q A Q1 /\
               (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
============================
 exists Q1, one Q 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 Q 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_sound_fst < Right : apply Right to QQstep.
Subgoal 1:

Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Right : forall A P1, one S A P1 ->
          (exists Q1, one Q A Q1 /\
               (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
Right1 : one Q A Q5
Right2 : refl_t Q1 P4 Q5 Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
 exists Q1, one Q 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 Q 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_sound_fst < clear Right.
Subgoal 1:

Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Right1 : one Q A Q5
Right2 : refl_t Q1 P4 Q5 Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
 exists Q1, one Q 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 Q 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_sound_fst < rename Right1 to Qstep.
Subgoal 1:

Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q5
Right2 : refl_t Q1 P4 Q5 Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
 exists Q1, one Q 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 Q 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_sound_fst < witness Q5.
Subgoal 1:

Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q5
Right2 : refl_t Q1 P4 Q5 Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
 one Q A Q5 /\
   (exists P2 Q2, refl_t P1 P2 Q5 Q2 /\ bisim_up_to refl_t P2 Q2 +)

Subgoal 2 is:
 forall A Q1, one Q 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_sound_fst < split.
Subgoal 1.1:

Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q5
Right2 : refl_t Q1 P4 Q5 Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
 one Q A Q5

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

Subgoal 2 is:
 forall A Q1, one Q 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_sound_fst < search.
Subgoal 1.2:

Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q5
Right2 : refl_t Q1 P4 Q5 Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
 exists P2 Q2, refl_t P1 P2 Q5 Q2 /\ bisim_up_to refl_t P2 Q2 +

Subgoal 2 is:
 forall A Q1, one Q 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_sound_fst < witness P1.
Subgoal 1.2:

Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q5
Right2 : refl_t Q1 P4 Q5 Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
 exists Q2, refl_t P1 P1 Q5 Q2 /\ bisim_up_to refl_t P1 Q2 +

Subgoal 2 is:
 forall A Q1, one Q 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_sound_fst < witness Q5.
Subgoal 1.2:

Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q5
Right2 : refl_t Q1 P4 Q5 Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
 refl_t P1 P1 Q5 Q5 /\ bisim_up_to refl_t P1 Q5 +

Subgoal 2 is:
 forall A Q1, one Q 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_sound_fst < split.
Subgoal 1.2.1:

Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q5
Right2 : refl_t Q1 P4 Q5 Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
 refl_t P1 P1 Q5 Q5

Subgoal 1.2.2 is:
 bisim_up_to refl_t P1 Q5 +

Subgoal 2 is:
 forall A Q1, one Q 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_sound_fst < search.
Subgoal 1.2.2:

Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q5
Right2 : refl_t Q1 P4 Q5 Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
 bisim_up_to refl_t P1 Q5 +

Subgoal 2 is:
 forall A Q1, one Q 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_sound_fst < case Left2.
Subgoal 1.2.2:

Variables: P Q R S A P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Pstep : one P A P3
PPstep : one R A Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q3 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q5
Right2 : refl_t Q1 P4 Q5 Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
 bisim_up_to refl_t P3 Q5 +

Subgoal 2 is:
 forall A Q1, one Q 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_sound_fst < case Right2.
Subgoal 1.2.2:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Pstep : one P A P3
PPstep : one R A Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A P4
Middle2 : bisim_t Q3 P2 P4 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
 bisim_up_to refl_t P3 Q6 +

Subgoal 2 is:
 forall A Q1, one Q 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_sound_fst < Bisim : case Middle2.
Subgoal 1.2.2:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Pstep : one P A P3
PPstep : one R A Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A P4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q6
Right3 : bisim_up_to refl_t P4 Q6
Bisim : bisim_up_to refl_t Q3 P2
Bisim1 : bisim_up_to refl_t P4 Q4
============================
 bisim_up_to refl_t P3 Q6 +

Subgoal 2 is:
 forall A Q1, one Q 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_sound_fst < Link : apply bisim_transitive_ to Left3 Bisim.
Subgoal 1.2.2:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Pstep : one P A P3
PPstep : one R A Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A P4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q6
Right3 : bisim_up_to refl_t P4 Q6
Bisim : bisim_up_to refl_t Q3 P2
Bisim1 : bisim_up_to refl_t P4 Q4
Link : bisim_up_to refl_t P3 P2
============================
 bisim_up_to refl_t P3 Q6 +

Subgoal 2 is:
 forall A Q1, one Q 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_sound_fst < Link : apply bisim_symmetric_ to Bisim1.
Subgoal 1.2.2:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Pstep : one P A P3
PPstep : one R A Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A P4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q6
Right3 : bisim_up_to refl_t P4 Q6
Bisim : bisim_up_to refl_t Q3 P2
Bisim1 : bisim_up_to refl_t P4 Q4
Link : bisim_up_to refl_t P3 P2
Link1 : bisim_up_to refl_t Q4 P4
============================
 bisim_up_to refl_t P3 Q6 +

Subgoal 2 is:
 forall A Q1, one Q 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_sound_fst < Link : apply bisim_transitive_ to Link1 Right3.
Subgoal 1.2.2:

Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Pstep : one P A P3
PPstep : one R A Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A P4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q6
Right3 : bisim_up_to refl_t P4 Q6
Bisim : bisim_up_to refl_t Q3 P2
Bisim1 : bisim_up_to refl_t P4 Q4
Link : bisim_up_to refl_t P3 P2
Link1 : bisim_up_to refl_t Q4 P4
Link2 : bisim_up_to refl_t Q4 Q6
============================
 bisim_up_to refl_t P3 Q6 +

Subgoal 2 is:
 forall A Q1, one Q 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_sound_fst < backchain 1 CH.
Subgoal 2:

Variables: P Q R S
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Middle : bisim_up_to bisim_t R S
Right : bisim_up_to refl_t S Q
============================
 forall A Q1, one Q 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_sound_fst < intros Qstep.
Subgoal 2:

Variables: P Q R S A Q1
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Middle : bisim_up_to bisim_t R S
Right : bisim_up_to refl_t S Q
Qstep : one Q 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_sound_fst < Right : case Right.
Subgoal 2:

Variables: P Q R S A Q1
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Middle : bisim_up_to bisim_t R S
Qstep : one Q A Q1
Right : forall A P2, one S A P2 ->
          (exists Q1, one Q A Q1 /\
               (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\ bisim_up_to refl_t P3 Q3))
Right1 : forall A Q1, one Q A Q1 ->
           (exists P2, one S A P2 /\
                (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\
                     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_sound_fst < Right : apply Right1 to Qstep.
Subgoal 2:

Variables: P Q R S A Q1 P2 P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Middle : bisim_up_to bisim_t R S
Qstep : one Q A Q1
Right : forall A P2, one S A P2 ->
          (exists Q1, one Q A Q1 /\
               (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\ bisim_up_to refl_t P3 Q3))
Right1 : forall A Q1, one Q A Q1 ->
           (exists P2, one S A P2 /\
                (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\
                     bisim_up_to refl_t P3 Q3))
Right2 : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : 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_sound_fst < clear Right Right1.
Subgoal 2:

Variables: P Q R S A Q1 P2 P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Middle : bisim_up_to bisim_t R S
Qstep : one Q A Q1
Right2 : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : 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_sound_fst < rename Right2 to Pstep.
Subgoal 2:

Variables: P Q R S A Q1 P2 P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Middle : bisim_up_to bisim_t R S
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : 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_sound_fst < Middle : case Middle.
Subgoal 2:

Variables: P Q R S A Q1 P2 P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
Middle : forall A P2, one R A P2 ->
           (exists Q1, one S A Q1 /\
                (exists P3 Q3, bisim_t P2 P3 Q1 Q3 /\
                     bisim_up_to bisim_t P3 Q3))
Middle1 : forall A Q1, one S A Q1 ->
            (exists P2, one R A P2 /\
                 (exists P3 Q3, bisim_t P2 P3 Q1 Q3 /\
                      bisim_up_to bisim_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_sound_fst < Middle : apply Middle1 to Pstep.
Subgoal 2:

Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
Middle : forall A P2, one R A P2 ->
           (exists Q1, one S A Q1 /\
                (exists P3 Q3, bisim_t P2 P3 Q1 Q3 /\
                     bisim_up_to bisim_t P3 Q3))
Middle1 : forall A Q1, one S A Q1 ->
            (exists P2, one R A P2 /\
                 (exists P3 Q3, bisim_t P2 P3 Q1 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle2 : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_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_sound_fst < clear Middle Middle1.
Subgoal 2:

Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
Middle2 : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_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_sound_fst < rename Middle2 to PPstep.
Subgoal 2:

Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_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_sound_fst < Left : case Left.
Subgoal 2:

Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
Left : 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))
Left1 : 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))
============================
 exists P1, one P A P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_sound_fst < Left : apply Left1 to PPstep.
Subgoal 2:

Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
Left : 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))
Left1 : 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))
Left2 : one P A P5
Left3 : refl_t P5 P6 P1 Q4
Left4 : bisim_up_to refl_t P6 Q4
============================
 exists P1, one P A P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_sound_fst < clear Left Left1.
Subgoal 2:

Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
Left2 : one P A P5
Left3 : refl_t P5 P6 P1 Q4
Left4 : bisim_up_to refl_t P6 Q4
============================
 exists P1, one P A P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_sound_fst < rename Left2 to QQstep.
Subgoal 2:

Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P5
Left3 : refl_t P5 P6 P1 Q4
Left4 : bisim_up_to refl_t P6 Q4
============================
 exists P1, one P A P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_sound_fst < witness P5.
Subgoal 2:

Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P5
Left3 : refl_t P5 P6 P1 Q4
Left4 : bisim_up_to refl_t P6 Q4
============================
 one P A P5 /\
   (exists P2 Q2, refl_t P5 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

bisim_sound_fst < split.
Subgoal 2.1:

Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P5
Left3 : refl_t P5 P6 P1 Q4
Left4 : bisim_up_to refl_t P6 Q4
============================
 one P A P5

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

bisim_sound_fst < search.
Subgoal 2.2:

Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P5
Left3 : refl_t P5 P6 P1 Q4
Left4 : bisim_up_to refl_t P6 Q4
============================
 exists P2 Q2, refl_t P5 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +

bisim_sound_fst < witness P5.
Subgoal 2.2:

Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P5
Left3 : refl_t P5 P6 P1 Q4
Left4 : bisim_up_to refl_t P6 Q4
============================
 exists Q2, refl_t P5 P5 Q1 Q2 /\ bisim_up_to refl_t P5 Q2 +

bisim_sound_fst < witness Q1.
Subgoal 2.2:

Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P5
Left3 : refl_t P5 P6 P1 Q4
Left4 : bisim_up_to refl_t P6 Q4
============================
 refl_t P5 P5 Q1 Q1 /\ bisim_up_to refl_t P5 Q1 +

bisim_sound_fst < split.
Subgoal 2.2.1:

Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P5
Left3 : refl_t P5 P6 P1 Q4
Left4 : bisim_up_to refl_t P6 Q4
============================
 refl_t P5 P5 Q1 Q1

Subgoal 2.2.2 is:
 bisim_up_to refl_t P5 Q1 +

bisim_sound_fst < search.
Subgoal 2.2.2:

Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P5
Left3 : refl_t P5 P6 P1 Q4
Left4 : bisim_up_to refl_t P6 Q4
============================
 bisim_up_to refl_t P5 Q1 +

bisim_sound_fst < case Left3.
Subgoal 2.2.2:

Variables: P Q R S A Q1 P2 P3 Q3 P4 Q2 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A Q4
Middle3 : bisim_t Q4 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P6
Left4 : bisim_up_to refl_t P6 Q4
============================
 bisim_up_to refl_t P6 Q1 +

bisim_sound_fst < case Right3.
Subgoal 2.2.2:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Qstep : one Q A Q3
Pstep : one S A P3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A Q4
Middle3 : bisim_t Q4 P4 P3 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P6
Left4 : bisim_up_to refl_t P6 Q4
============================
 bisim_up_to refl_t P6 Q3 +

bisim_sound_fst < Link : case Middle3.
Subgoal 2.2.2:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Qstep : one Q A Q3
Pstep : one S A P3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A Q4
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P6
Left4 : bisim_up_to refl_t P6 Q4
Link : bisim_up_to refl_t Q4 P4
Link1 : bisim_up_to refl_t P3 Q2
============================
 bisim_up_to refl_t P6 Q3 +

bisim_sound_fst < Link : apply bisim_transitive_ to Left4 Link.
Subgoal 2.2.2:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Qstep : one Q A Q3
Pstep : one S A P3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A Q4
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P6
Left4 : bisim_up_to refl_t P6 Q4
Link : bisim_up_to refl_t Q4 P4
Link1 : bisim_up_to refl_t P3 Q2
Link2 : bisim_up_to refl_t P6 P4
============================
 bisim_up_to refl_t P6 Q3 +

bisim_sound_fst < Link : apply bisim_symmetric_ to Link1.
Subgoal 2.2.2:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Qstep : one Q A Q3
Pstep : one S A P3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A Q4
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P6
Left4 : bisim_up_to refl_t P6 Q4
Link : bisim_up_to refl_t Q4 P4
Link1 : bisim_up_to refl_t P3 Q2
Link2 : bisim_up_to refl_t P6 P4
Link3 : bisim_up_to refl_t Q2 P3
============================
 bisim_up_to refl_t P6 Q3 +

bisim_sound_fst < Link : apply bisim_transitive_ to Link3 Right4.
Subgoal 2.2.2:

Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q +
Qstep : one Q A Q3
Pstep : one S A P3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A Q4
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P6
Left4 : bisim_up_to refl_t P6 Q4
Link : bisim_up_to refl_t Q4 P4
Link1 : bisim_up_to refl_t P3 Q2
Link2 : bisim_up_to refl_t P6 P4
Link3 : bisim_up_to refl_t Q2 P3
Link4 : bisim_up_to refl_t Q2 Q3
============================
 bisim_up_to refl_t P6 Q3 +

bisim_sound_fst < backchain 1 CH.
Proof completed.
Abella < Theorem bisim_sound_snd : 
is_sound_snd bisim_t.


============================
 is_sound_snd bisim_t

bisim_sound_snd < unfold.

============================
 forall P Q, bisim_up_to bisim_t P Q ->
   (exists R S, bisim_up_to refl_t P R /\ bisim_up_to bisim_t R S /\
        bisim_up_to refl_t S Q)

bisim_sound_snd < intros.

Variables: P Q
H1 : bisim_up_to bisim_t P Q
============================
 exists R S, bisim_up_to refl_t P R /\ bisim_up_to bisim_t R S /\
   bisim_up_to refl_t S Q

bisim_sound_snd < witness P.

Variables: P Q
H1 : bisim_up_to bisim_t P Q
============================
 exists S, bisim_up_to refl_t P P /\ bisim_up_to bisim_t P S /\
   bisim_up_to refl_t S Q

bisim_sound_snd < witness Q.

Variables: P Q
H1 : bisim_up_to bisim_t P Q
============================
 bisim_up_to refl_t P P /\ bisim_up_to bisim_t P Q /\ bisim_up_to refl_t Q Q

bisim_sound_snd < split.
Subgoal 1:

Variables: P Q
H1 : bisim_up_to bisim_t P Q
============================
 bisim_up_to refl_t P P

Subgoal 2 is:
 bisim_up_to bisim_t P Q

Subgoal 3 is:
 bisim_up_to refl_t Q Q

bisim_sound_snd < backchain bisim_reflexive_.
Subgoal 2:

Variables: P Q
H1 : bisim_up_to bisim_t P Q
============================
 bisim_up_to bisim_t P Q

Subgoal 3 is:
 bisim_up_to refl_t Q Q

bisim_sound_snd < search.
Subgoal 3:

Variables: P Q
H1 : bisim_up_to bisim_t P Q
============================
 bisim_up_to refl_t Q Q

bisim_sound_snd < backchain bisim_reflexive_.
Proof completed.
Abella < Theorem bisim_sound : 
is_sound bisim_t.


============================
 is_sound bisim_t

bisim_sound < unfold.

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

bisim_sound < intros.

Variables: P Q
H1 : bisim_up_to bisim_t P Q
============================
 bisim_up_to refl_t P Q

bisim_sound < apply bisim_sound_snd.

Variables: P Q
H1 : bisim_up_to bisim_t P Q
H2 : is_sound_snd bisim_t
============================
 bisim_up_to refl_t P Q

bisim_sound < case H2.

Variables: P Q
H1 : bisim_up_to bisim_t P Q
H3 : forall P Q, bisim_up_to bisim_t P Q ->
       (exists R S, bisim_up_to refl_t P R /\ bisim_up_to bisim_t R S /\
            bisim_up_to refl_t S Q)
============================
 bisim_up_to refl_t P Q

bisim_sound < apply H3 to H1.

Variables: P Q R S
H1 : bisim_up_to bisim_t P Q
H3 : forall P Q, bisim_up_to bisim_t P Q ->
       (exists R S, bisim_up_to refl_t P R /\ bisim_up_to bisim_t R S /\
            bisim_up_to refl_t S Q)
H4 : bisim_up_to refl_t P R
H5 : bisim_up_to bisim_t R S
H6 : bisim_up_to refl_t S Q
============================
 bisim_up_to refl_t P Q

bisim_sound < apply bisim_sound_fst.

Variables: P Q R S
H1 : bisim_up_to bisim_t P Q
H3 : forall P Q, bisim_up_to bisim_t P Q ->
       (exists R S, bisim_up_to refl_t P R /\ bisim_up_to bisim_t R S /\
            bisim_up_to refl_t S Q)
H4 : bisim_up_to refl_t P R
H5 : bisim_up_to bisim_t R S
H6 : bisim_up_to refl_t S Q
H7 : is_sound_fst bisim_t
============================
 bisim_up_to refl_t P Q

bisim_sound < case H7.

Variables: P Q R S
H1 : bisim_up_to bisim_t P Q
H3 : forall P Q, bisim_up_to bisim_t P Q ->
       (exists R S, bisim_up_to refl_t P R /\ bisim_up_to bisim_t R S /\
            bisim_up_to refl_t S Q)
H4 : bisim_up_to refl_t P R
H5 : bisim_up_to bisim_t R S
H6 : bisim_up_to refl_t S Q
H8 : forall P Q, (exists R S, bisim_up_to refl_t P R /\
                      bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
       bisim_up_to refl_t P Q
============================
 bisim_up_to refl_t P Q

bisim_sound < backchain H8.
Proof completed.
Abella <