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

Abella < Set subgoals off.

Abella < Import "pic_core".
Importing from "pic_core".
Warning: Definition can be used to defeat stratification
 (higher-order argument "Tech" 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

1 other subgoal.

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 L P1, one P L P1 ->
   (exists Q1, one Q L Q1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

5 other subgoals.

bisim_sound_fst < intros Pstep.
Subgoal 1:

Variables: P Q R S L 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 L P1
============================
 exists Q1, one Q L Q1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

5 other subgoals.

bisim_sound_fst < Left1 : case Left.
Subgoal 1:

Variables: P Q R S L 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 L P1
Left1 : forall L P1, one P L P1 ->
          (exists Q2, one R L Q2 /\
               (exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
Left2 : forall X P1, oneb P (dn X) P1 ->
          (exists Q2, oneb R (dn X) Q2 /\
               (exists P3 Q3, forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                    bisim_up_to refl_t (P3 N) (Q3 N)))
Left3 : forall X P1, oneb P (up X) P1 ->
          (exists Q2, oneb R (up X) Q2 /\
               (exists P3 Q3, nabla x, refl_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                    bisim_up_to refl_t (P3 x) (Q3 x)))
Left4 : forall L Q2, one R L Q2 ->
          (exists P1, one P L P1 /\
               (exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
Left5 : forall X Q2, oneb R (dn X) Q2 ->
          (exists P1, oneb P (dn X) P1 /\
               (exists P3 Q3, forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                    bisim_up_to refl_t (P3 N) (Q3 N)))
Left6 : forall X Q2, oneb R (up X) Q2 ->
          (exists P1, oneb P (up X) P1 /\
               (exists P3 Q3, nabla x, refl_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                    bisim_up_to refl_t (P3 x) (Q3 x)))
============================
 exists Q1, one Q L Q1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

5 other subgoals.

bisim_sound_fst < Rstep : apply Left1 to *Pstep.
Subgoal 1:

Variables: P Q R S L 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
Left1 : forall L P1, one P L P1 ->
          (exists Q2, one R L Q2 /\
               (exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
Left2 : forall X P1, oneb P (dn X) P1 ->
          (exists Q2, oneb R (dn X) Q2 /\
               (exists P3 Q3, forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                    bisim_up_to refl_t (P3 N) (Q3 N)))
Left3 : forall X P1, oneb P (up X) P1 ->
          (exists Q2, oneb R (up X) Q2 /\
               (exists P3 Q3, nabla x, refl_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                    bisim_up_to refl_t (P3 x) (Q3 x)))
Left4 : forall L Q2, one R L Q2 ->
          (exists P1, one P L P1 /\
               (exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
Left5 : forall X Q2, oneb R (dn X) Q2 ->
          (exists P1, oneb P (dn X) P1 /\
               (exists P3 Q3, forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                    bisim_up_to refl_t (P3 N) (Q3 N)))
Left6 : forall X Q2, oneb R (up X) Q2 ->
          (exists P1, oneb P (up X) P1 /\
               (exists P3 Q3, nabla x, refl_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                    bisim_up_to refl_t (P3 x) (Q3 x)))
Rstep : one R L Q2
Rstep1 : refl_t P1 P3 Q2 Q3
Rstep2 : bisim_up_to refl_t P3 Q3
============================
 exists Q1, one Q L Q1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

5 other subgoals.

bisim_sound_fst < clear Left1 Left2 Left3 Left4 Left5 Left6.
Subgoal 1:

Variables: P Q R S L 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
Rstep : one R L Q2
Rstep1 : refl_t P1 P3 Q2 Q3
Rstep2 : bisim_up_to refl_t P3 Q3
============================
 exists Q1, one Q L Q1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

5 other subgoals.

bisim_sound_fst < Middle1 : case Middle.
Subgoal 1:

Variables: P Q R S L 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
Rstep : one R L Q2
Rstep1 : refl_t P1 P3 Q2 Q3
Rstep2 : bisim_up_to refl_t P3 Q3
Middle1 : forall L P1, one R L P1 ->
            (exists Q2, one S L Q2 /\
                 (exists P3 Q3, bisim_t P1 P3 Q2 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle2 : forall X P1, oneb R (dn X) P1 ->
            (exists Q2, oneb S (dn X) Q2 /\
                 (exists P3 Q3, forall N, bisim_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle3 : forall X P1, oneb R (up X) P1 ->
            (exists Q2, oneb S (up X) Q2 /\
                 (exists P3 Q3, nabla x, bisim_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
Middle4 : forall L Q2, one S L Q2 ->
            (exists P1, one R L P1 /\
                 (exists P3 Q3, bisim_t P1 P3 Q2 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle5 : forall X Q2, oneb S (dn X) Q2 ->
            (exists P1, oneb R (dn X) P1 /\
                 (exists P3 Q3, forall N, bisim_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle6 : forall X Q2, oneb S (up X) Q2 ->
            (exists P1, oneb R (up X) P1 /\
                 (exists P3 Q3, nabla x, bisim_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
============================
 exists Q1, one Q L Q1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

5 other subgoals.

bisim_sound_fst < Sstep : apply Middle1 to *Rstep.
Subgoal 1:

Variables: P Q R S L 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
Rstep1 : refl_t P1 P3 Q2 Q3
Rstep2 : bisim_up_to refl_t P3 Q3
Middle1 : forall L P1, one R L P1 ->
            (exists Q2, one S L Q2 /\
                 (exists P3 Q3, bisim_t P1 P3 Q2 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle2 : forall X P1, oneb R (dn X) P1 ->
            (exists Q2, oneb S (dn X) Q2 /\
                 (exists P3 Q3, forall N, bisim_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle3 : forall X P1, oneb R (up X) P1 ->
            (exists Q2, oneb S (up X) Q2 /\
                 (exists P3 Q3, nabla x, bisim_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
Middle4 : forall L Q2, one S L Q2 ->
            (exists P1, one R L P1 /\
                 (exists P3 Q3, bisim_t P1 P3 Q2 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle5 : forall X Q2, oneb S (dn X) Q2 ->
            (exists P1, oneb R (dn X) P1 /\
                 (exists P3 Q3, forall N, bisim_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle6 : forall X Q2, oneb S (up X) Q2 ->
            (exists P1, oneb R (up X) P1 /\
                 (exists P3 Q3, nabla x, bisim_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
Sstep : one S L Q1
Sstep1 : bisim_t Q2 P2 Q1 Q4
Sstep2 : bisim_up_to bisim_t P2 Q4
============================
 exists Q1, one Q L Q1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

5 other subgoals.

bisim_sound_fst < clear Middle1 Middle2 Middle3 Middle4 Middle5 Middle6.
Subgoal 1:

Variables: P Q R S L 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
Rstep1 : refl_t P1 P3 Q2 Q3
Rstep2 : bisim_up_to refl_t P3 Q3
Sstep : one S L Q1
Sstep1 : bisim_t Q2 P2 Q1 Q4
Sstep2 : bisim_up_to bisim_t P2 Q4
============================
 exists Q1, one Q L Q1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

5 other subgoals.

bisim_sound_fst < Right1 : case Right.
Subgoal 1:

Variables: P Q R S L 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 +
Rstep1 : refl_t P1 P3 Q2 Q3
Rstep2 : bisim_up_to refl_t P3 Q3
Sstep : one S L Q1
Sstep1 : bisim_t Q2 P2 Q1 Q4
Sstep2 : bisim_up_to bisim_t P2 Q4
Right1 : forall L P1, one S L P1 ->
           (exists Q1, one Q L Q1 /\
                (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\
                     bisim_up_to refl_t P2 Q2))
Right2 : forall X P1, oneb S (dn X) P1 ->
           (exists Q1, oneb Q (dn X) Q1 /\
                (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                     bisim_up_to refl_t (P2 N) (Q2 N)))
Right3 : forall X P1, oneb S (up X) P1 ->
           (exists Q1, oneb Q (up X) Q1 /\
                (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                     bisim_up_to refl_t (P2 x) (Q2 x)))
Right4 : forall L Q1, one Q L Q1 ->
           (exists P1, one S L P1 /\
                (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\
                     bisim_up_to refl_t P2 Q2))
Right5 : forall X Q1, oneb Q (dn X) Q1 ->
           (exists P1, oneb S (dn X) P1 /\
                (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                     bisim_up_to refl_t (P2 N) (Q2 N)))
Right6 : forall X Q1, oneb Q (up X) Q1 ->
           (exists P1, oneb S (up X) P1 /\
                (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                     bisim_up_to refl_t (P2 x) (Q2 x)))
============================
 exists Q1, one Q L Q1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

5 other subgoals.

bisim_sound_fst < Qstep : apply Right1 to *Sstep.
Subgoal 1:

Variables: P Q R S L 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 +
Rstep1 : refl_t P1 P3 Q2 Q3
Rstep2 : bisim_up_to refl_t P3 Q3
Sstep1 : bisim_t Q2 P2 Q1 Q4
Sstep2 : bisim_up_to bisim_t P2 Q4
Right1 : forall L P1, one S L P1 ->
           (exists Q1, one Q L Q1 /\
                (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\
                     bisim_up_to refl_t P2 Q2))
Right2 : forall X P1, oneb S (dn X) P1 ->
           (exists Q1, oneb Q (dn X) Q1 /\
                (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                     bisim_up_to refl_t (P2 N) (Q2 N)))
Right3 : forall X P1, oneb S (up X) P1 ->
           (exists Q1, oneb Q (up X) Q1 /\
                (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                     bisim_up_to refl_t (P2 x) (Q2 x)))
Right4 : forall L Q1, one Q L Q1 ->
           (exists P1, one S L P1 /\
                (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\
                     bisim_up_to refl_t P2 Q2))
Right5 : forall X Q1, oneb Q (dn X) Q1 ->
           (exists P1, oneb S (dn X) P1 /\
                (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                     bisim_up_to refl_t (P2 N) (Q2 N)))
Right6 : forall X Q1, oneb Q (up X) Q1 ->
           (exists P1, oneb S (up X) P1 /\
                (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                     bisim_up_to refl_t (P2 x) (Q2 x)))
Qstep : one Q L Q5
Qstep1 : refl_t Q1 P4 Q5 Q6
Qstep2 : bisim_up_to refl_t P4 Q6
============================
 exists Q1, one Q L Q1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

5 other subgoals.

bisim_sound_fst < clear Right1 Right2 Right3 Right4 Right5 Right6.
Subgoal 1:

Variables: P Q R S L 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 +
Rstep1 : refl_t P1 P3 Q2 Q3
Rstep2 : bisim_up_to refl_t P3 Q3
Sstep1 : bisim_t Q2 P2 Q1 Q4
Sstep2 : bisim_up_to bisim_t P2 Q4
Qstep : one Q L Q5
Qstep1 : refl_t Q1 P4 Q5 Q6
Qstep2 : bisim_up_to refl_t P4 Q6
============================
 exists Q1, one Q L Q1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

5 other subgoals.

bisim_sound_fst < witness Q5.
Subgoal 1:

Variables: P Q R S L 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 +
Rstep1 : refl_t P1 P3 Q2 Q3
Rstep2 : bisim_up_to refl_t P3 Q3
Sstep1 : bisim_t Q2 P2 Q1 Q4
Sstep2 : bisim_up_to bisim_t P2 Q4
Qstep : one Q L Q5
Qstep1 : refl_t Q1 P4 Q5 Q6
Qstep2 : bisim_up_to refl_t P4 Q6
============================
 one Q L Q5 /\
   (exists P2 Q2, refl_t P1 P2 Q5 Q2 /\ bisim_up_to refl_t P2 Q2 +)

5 other subgoals.

bisim_sound_fst < split.
Subgoal 1.1:

Variables: P Q R S L 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 +
Rstep1 : refl_t P1 P3 Q2 Q3
Rstep2 : bisim_up_to refl_t P3 Q3
Sstep1 : bisim_t Q2 P2 Q1 Q4
Sstep2 : bisim_up_to bisim_t P2 Q4
Qstep : one Q L Q5
Qstep1 : refl_t Q1 P4 Q5 Q6
Qstep2 : bisim_up_to refl_t P4 Q6
============================
 one Q L Q5

6 other subgoals.

bisim_sound_fst < search.
Subgoal 1.2:

Variables: P Q R S L 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 +
Rstep1 : refl_t P1 P3 Q2 Q3
Rstep2 : bisim_up_to refl_t P3 Q3
Sstep1 : bisim_t Q2 P2 Q1 Q4
Sstep2 : bisim_up_to bisim_t P2 Q4
Qstep : one Q L Q5
Qstep1 : refl_t Q1 P4 Q5 Q6
Qstep2 : bisim_up_to refl_t P4 Q6
============================
 exists P2 Q2, refl_t P1 P2 Q5 Q2 /\ bisim_up_to refl_t P2 Q2 +

5 other subgoals.

bisim_sound_fst < clear Qstep.
Subgoal 1.2:

Variables: P Q R S L 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 +
Rstep1 : refl_t P1 P3 Q2 Q3
Rstep2 : bisim_up_to refl_t P3 Q3
Sstep1 : bisim_t Q2 P2 Q1 Q4
Sstep2 : bisim_up_to bisim_t P2 Q4
Qstep1 : refl_t Q1 P4 Q5 Q6
Qstep2 : bisim_up_to refl_t P4 Q6
============================
 exists P2 Q2, refl_t P1 P2 Q5 Q2 /\ bisim_up_to refl_t P2 Q2 +

5 other subgoals.

bisim_sound_fst < witness P1.
Subgoal 1.2:

Variables: P Q R S L 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 +
Rstep1 : refl_t P1 P3 Q2 Q3
Rstep2 : bisim_up_to refl_t P3 Q3
Sstep1 : bisim_t Q2 P2 Q1 Q4
Sstep2 : bisim_up_to bisim_t P2 Q4
Qstep1 : refl_t Q1 P4 Q5 Q6
Qstep2 : bisim_up_to refl_t P4 Q6
============================
 exists Q2, refl_t P1 P1 Q5 Q2 /\ bisim_up_to refl_t P1 Q2 +

5 other subgoals.

bisim_sound_fst < witness Q5.
Subgoal 1.2:

Variables: P Q R S L 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 +
Rstep1 : refl_t P1 P3 Q2 Q3
Rstep2 : bisim_up_to refl_t P3 Q3
Sstep1 : bisim_t Q2 P2 Q1 Q4
Sstep2 : bisim_up_to bisim_t P2 Q4
Qstep1 : refl_t Q1 P4 Q5 Q6
Qstep2 : bisim_up_to refl_t P4 Q6
============================
 refl_t P1 P1 Q5 Q5 /\ bisim_up_to refl_t P1 Q5 +

5 other subgoals.

bisim_sound_fst < split.
Subgoal 1.2.1:

Variables: P Q R S L 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 +
Rstep1 : refl_t P1 P3 Q2 Q3
Rstep2 : bisim_up_to refl_t P3 Q3
Sstep1 : bisim_t Q2 P2 Q1 Q4
Sstep2 : bisim_up_to bisim_t P2 Q4
Qstep1 : refl_t Q1 P4 Q5 Q6
Qstep2 : bisim_up_to refl_t P4 Q6
============================
 refl_t P1 P1 Q5 Q5

6 other subgoals.

bisim_sound_fst < search.
Subgoal 1.2.2:

Variables: P Q R S L 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 +
Rstep1 : refl_t P1 P3 Q2 Q3
Rstep2 : bisim_up_to refl_t P3 Q3
Sstep1 : bisim_t Q2 P2 Q1 Q4
Sstep2 : bisim_up_to bisim_t P2 Q4
Qstep1 : refl_t Q1 P4 Q5 Q6
Qstep2 : bisim_up_to refl_t P4 Q6
============================
 bisim_up_to refl_t P1 Q5 +

5 other subgoals.

bisim_sound_fst < case Rstep1.
Subgoal 1.2.2:

Variables: P Q R S L 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 +
Rstep2 : bisim_up_to refl_t P3 Q3
Sstep1 : bisim_t Q3 P2 Q1 Q4
Sstep2 : bisim_up_to bisim_t P2 Q4
Qstep1 : refl_t Q1 P4 Q5 Q6
Qstep2 : bisim_up_to refl_t P4 Q6
============================
 bisim_up_to refl_t P3 Q5 +

5 other subgoals.

bisim_sound_fst < case Qstep1.
Subgoal 1.2.2:

Variables: P Q R S L 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 +
Rstep2 : bisim_up_to refl_t P3 Q3
Sstep1 : bisim_t Q3 P2 P4 Q4
Sstep2 : bisim_up_to bisim_t P2 Q4
Qstep2 : bisim_up_to refl_t P4 Q6
============================
 bisim_up_to refl_t P3 Q6 +

5 other subgoals.

bisim_sound_fst < Sstep1 : case Sstep1.
Subgoal 1.2.2:

Variables: P Q R S L 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 +
Rstep2 : bisim_up_to refl_t P3 Q3
Sstep2 : bisim_up_to bisim_t P2 Q4
Qstep2 : bisim_up_to refl_t P4 Q6
Sstep1 : bisim_up_to refl_t Q3 P2
Sstep3 : bisim_up_to refl_t P4 Q4
============================
 bisim_up_to refl_t P3 Q6 +

5 other subgoals.

bisim_sound_fst < Link1 : apply bisim_transitive to *Rstep2 *Sstep1.
Subgoal 1.2.2:

Variables: P Q R S L 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 +
Sstep2 : bisim_up_to bisim_t P2 Q4
Qstep2 : bisim_up_to refl_t P4 Q6
Sstep3 : bisim_up_to refl_t P4 Q4
Link1 : bisim_up_to refl_t P3 P2
============================
 bisim_up_to refl_t P3 Q6 +

5 other subgoals.

bisim_sound_fst < Link1 : apply bisim_symmetric to *Sstep3.
Subgoal 1.2.2:

Variables: P Q R S L 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 +
Sstep2 : bisim_up_to bisim_t P2 Q4
Qstep2 : bisim_up_to refl_t P4 Q6
Link1 : bisim_up_to refl_t P3 P2
Link2 : bisim_up_to refl_t Q4 P4
============================
 bisim_up_to refl_t P3 Q6 +

5 other subgoals.

bisim_sound_fst < Link1 : apply bisim_transitive to *Link2 *Qstep2.
Subgoal 1.2.2:

Variables: P Q R S L 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 +
Sstep2 : bisim_up_to bisim_t P2 Q4
Link1 : bisim_up_to refl_t P3 P2
Link2 : bisim_up_to refl_t Q4 Q6
============================
 bisim_up_to refl_t P3 Q6 +

5 other subgoals.

bisim_sound_fst < backchain 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 X P1, oneb P (dn X) P1 ->
   (exists Q1, oneb Q (dn X) Q1 /\
        (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
             bisim_up_to refl_t (P2 N) (Q2 N) +))

4 other subgoals.

bisim_sound_fst < intros Pstep.
Subgoal 2:

Variables: P Q R S X 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 : oneb P (dn X) P1
============================
 exists Q1, oneb Q (dn X) Q1 /\
   (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
        bisim_up_to refl_t (P2 N) (Q2 N) +)

4 other subgoals.

bisim_sound_fst < Left1 : case Left.
Subgoal 2:

Variables: P Q R S X 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 : oneb P (dn X) P1
Left1 : forall L P1, one P L P1 ->
          (exists Q2, one R L Q2 /\
               (exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
Left2 : forall X P1, oneb P (dn X) P1 ->
          (exists Q2, oneb R (dn X) Q2 /\
               (exists P3 Q3, forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                    bisim_up_to refl_t (P3 N) (Q3 N)))
Left3 : forall X P1, oneb P (up X) P1 ->
          (exists Q2, oneb R (up X) Q2 /\
               (exists P3 Q3, nabla x, refl_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                    bisim_up_to refl_t (P3 x) (Q3 x)))
Left4 : forall L Q2, one R L Q2 ->
          (exists P1, one P L P1 /\
               (exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
Left5 : forall X Q2, oneb R (dn X) Q2 ->
          (exists P1, oneb P (dn X) P1 /\
               (exists P3 Q3, forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                    bisim_up_to refl_t (P3 N) (Q3 N)))
Left6 : forall X Q2, oneb R (up X) Q2 ->
          (exists P1, oneb P (up X) P1 /\
               (exists P3 Q3, nabla x, refl_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                    bisim_up_to refl_t (P3 x) (Q3 x)))
============================
 exists Q1, oneb Q (dn X) Q1 /\
   (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
        bisim_up_to refl_t (P2 N) (Q2 N) +)

4 other subgoals.

bisim_sound_fst < Rstep : apply Left2 to *Pstep.
Subgoal 2:

Variables: P Q R S X 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
Left1 : forall L P1, one P L P1 ->
          (exists Q2, one R L Q2 /\
               (exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
Left2 : forall X P1, oneb P (dn X) P1 ->
          (exists Q2, oneb R (dn X) Q2 /\
               (exists P3 Q3, forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                    bisim_up_to refl_t (P3 N) (Q3 N)))
Left3 : forall X P1, oneb P (up X) P1 ->
          (exists Q2, oneb R (up X) Q2 /\
               (exists P3 Q3, nabla x, refl_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                    bisim_up_to refl_t (P3 x) (Q3 x)))
Left4 : forall L Q2, one R L Q2 ->
          (exists P1, one P L P1 /\
               (exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
Left5 : forall X Q2, oneb R (dn X) Q2 ->
          (exists P1, oneb P (dn X) P1 /\
               (exists P3 Q3, forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                    bisim_up_to refl_t (P3 N) (Q3 N)))
Left6 : forall X Q2, oneb R (up X) Q2 ->
          (exists P1, oneb P (up X) P1 /\
               (exists P3 Q3, nabla x, refl_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                    bisim_up_to refl_t (P3 x) (Q3 x)))
Rstep : oneb R (dn X) Q2
Rstep1 : forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
============================
 exists Q1, oneb Q (dn X) Q1 /\
   (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
        bisim_up_to refl_t (P2 N) (Q2 N) +)

4 other subgoals.

bisim_sound_fst < clear Left1 Left2 Left3 Left4 Left5 Left6.
Subgoal 2:

Variables: P Q R S X 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
Rstep : oneb R (dn X) Q2
Rstep1 : forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
============================
 exists Q1, oneb Q (dn X) Q1 /\
   (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
        bisim_up_to refl_t (P2 N) (Q2 N) +)

4 other subgoals.

bisim_sound_fst < Middle1 : case Middle.
Subgoal 2:

Variables: P Q R S X 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
Rstep : oneb R (dn X) Q2
Rstep1 : forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Middle1 : forall L P1, one R L P1 ->
            (exists Q2, one S L Q2 /\
                 (exists P3 Q3, bisim_t P1 P3 Q2 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle2 : forall X P1, oneb R (dn X) P1 ->
            (exists Q2, oneb S (dn X) Q2 /\
                 (exists P3 Q3, forall N, bisim_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle3 : forall X P1, oneb R (up X) P1 ->
            (exists Q2, oneb S (up X) Q2 /\
                 (exists P3 Q3, nabla x, bisim_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
Middle4 : forall L Q2, one S L Q2 ->
            (exists P1, one R L P1 /\
                 (exists P3 Q3, bisim_t P1 P3 Q2 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle5 : forall X Q2, oneb S (dn X) Q2 ->
            (exists P1, oneb R (dn X) P1 /\
                 (exists P3 Q3, forall N, bisim_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle6 : forall X Q2, oneb S (up X) Q2 ->
            (exists P1, oneb R (up X) P1 /\
                 (exists P3 Q3, nabla x, bisim_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
============================
 exists Q1, oneb Q (dn X) Q1 /\
   (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
        bisim_up_to refl_t (P2 N) (Q2 N) +)

4 other subgoals.

bisim_sound_fst < Sstep : apply Middle2 to *Rstep.
Subgoal 2:

Variables: P Q R S X 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
Rstep1 : forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Middle1 : forall L P1, one R L P1 ->
            (exists Q2, one S L Q2 /\
                 (exists P3 Q3, bisim_t P1 P3 Q2 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle2 : forall X P1, oneb R (dn X) P1 ->
            (exists Q2, oneb S (dn X) Q2 /\
                 (exists P3 Q3, forall N, bisim_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle3 : forall X P1, oneb R (up X) P1 ->
            (exists Q2, oneb S (up X) Q2 /\
                 (exists P3 Q3, nabla x, bisim_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
Middle4 : forall L Q2, one S L Q2 ->
            (exists P1, one R L P1 /\
                 (exists P3 Q3, bisim_t P1 P3 Q2 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle5 : forall X Q2, oneb S (dn X) Q2 ->
            (exists P1, oneb R (dn X) P1 /\
                 (exists P3 Q3, forall N, bisim_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle6 : forall X Q2, oneb S (up X) Q2 ->
            (exists P1, oneb R (up X) P1 /\
                 (exists P3 Q3, nabla x, bisim_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
Sstep : oneb S (dn X) Q1
Sstep1 : forall N, bisim_t (Q2 N) (P2 N) (Q1 N) (Q4 N) /\
           bisim_up_to bisim_t (P2 N) (Q4 N)
============================
 exists Q1, oneb Q (dn X) Q1 /\
   (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
        bisim_up_to refl_t (P2 N) (Q2 N) +)

4 other subgoals.

bisim_sound_fst < clear Middle1 Middle2 Middle3 Middle4 Middle5 Middle6.
Subgoal 2:

Variables: P Q R S X 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
Rstep1 : forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Sstep : oneb S (dn X) Q1
Sstep1 : forall N, bisim_t (Q2 N) (P2 N) (Q1 N) (Q4 N) /\
           bisim_up_to bisim_t (P2 N) (Q4 N)
============================
 exists Q1, oneb Q (dn X) Q1 /\
   (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
        bisim_up_to refl_t (P2 N) (Q2 N) +)

4 other subgoals.

bisim_sound_fst < Right1 : case Right.
Subgoal 2:

Variables: P Q R S X 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 +
Rstep1 : forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Sstep : oneb S (dn X) Q1
Sstep1 : forall N, bisim_t (Q2 N) (P2 N) (Q1 N) (Q4 N) /\
           bisim_up_to bisim_t (P2 N) (Q4 N)
Right1 : forall L P1, one S L P1 ->
           (exists Q1, one Q L Q1 /\
                (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\
                     bisim_up_to refl_t P2 Q2))
Right2 : forall X P1, oneb S (dn X) P1 ->
           (exists Q1, oneb Q (dn X) Q1 /\
                (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                     bisim_up_to refl_t (P2 N) (Q2 N)))
Right3 : forall X P1, oneb S (up X) P1 ->
           (exists Q1, oneb Q (up X) Q1 /\
                (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                     bisim_up_to refl_t (P2 x) (Q2 x)))
Right4 : forall L Q1, one Q L Q1 ->
           (exists P1, one S L P1 /\
                (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\
                     bisim_up_to refl_t P2 Q2))
Right5 : forall X Q1, oneb Q (dn X) Q1 ->
           (exists P1, oneb S (dn X) P1 /\
                (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                     bisim_up_to refl_t (P2 N) (Q2 N)))
Right6 : forall X Q1, oneb Q (up X) Q1 ->
           (exists P1, oneb S (up X) P1 /\
                (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                     bisim_up_to refl_t (P2 x) (Q2 x)))
============================
 exists Q1, oneb Q (dn X) Q1 /\
   (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
        bisim_up_to refl_t (P2 N) (Q2 N) +)

4 other subgoals.

bisim_sound_fst < Qstep : apply Right2 to *Sstep.
Subgoal 2:

Variables: P Q R S X 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 +
Rstep1 : forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Sstep1 : forall N, bisim_t (Q2 N) (P2 N) (Q1 N) (Q4 N) /\
           bisim_up_to bisim_t (P2 N) (Q4 N)
Right1 : forall L P1, one S L P1 ->
           (exists Q1, one Q L Q1 /\
                (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\
                     bisim_up_to refl_t P2 Q2))
Right2 : forall X P1, oneb S (dn X) P1 ->
           (exists Q1, oneb Q (dn X) Q1 /\
                (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                     bisim_up_to refl_t (P2 N) (Q2 N)))
Right3 : forall X P1, oneb S (up X) P1 ->
           (exists Q1, oneb Q (up X) Q1 /\
                (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                     bisim_up_to refl_t (P2 x) (Q2 x)))
Right4 : forall L Q1, one Q L Q1 ->
           (exists P1, one S L P1 /\
                (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\
                     bisim_up_to refl_t P2 Q2))
Right5 : forall X Q1, oneb Q (dn X) Q1 ->
           (exists P1, oneb S (dn X) P1 /\
                (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                     bisim_up_to refl_t (P2 N) (Q2 N)))
Right6 : forall X Q1, oneb Q (up X) Q1 ->
           (exists P1, oneb S (up X) P1 /\
                (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                     bisim_up_to refl_t (P2 x) (Q2 x)))
Qstep : oneb Q (dn X) Q5
Qstep1 : forall N, refl_t (Q1 N) (P4 N) (Q5 N) (Q6 N) /\
           bisim_up_to refl_t (P4 N) (Q6 N)
============================
 exists Q1, oneb Q (dn X) Q1 /\
   (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
        bisim_up_to refl_t (P2 N) (Q2 N) +)

4 other subgoals.

bisim_sound_fst < clear Right1 Right2 Right3 Right4 Right5 Right6.
Subgoal 2:

Variables: P Q R S X 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 +
Rstep1 : forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Sstep1 : forall N, bisim_t (Q2 N) (P2 N) (Q1 N) (Q4 N) /\
           bisim_up_to bisim_t (P2 N) (Q4 N)
Qstep : oneb Q (dn X) Q5
Qstep1 : forall N, refl_t (Q1 N) (P4 N) (Q5 N) (Q6 N) /\
           bisim_up_to refl_t (P4 N) (Q6 N)
============================
 exists Q1, oneb Q (dn X) Q1 /\
   (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
        bisim_up_to refl_t (P2 N) (Q2 N) +)

4 other subgoals.

bisim_sound_fst < witness Q5.
Subgoal 2:

Variables: P Q R S X 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 +
Rstep1 : forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Sstep1 : forall N, bisim_t (Q2 N) (P2 N) (Q1 N) (Q4 N) /\
           bisim_up_to bisim_t (P2 N) (Q4 N)
Qstep : oneb Q (dn X) Q5
Qstep1 : forall N, refl_t (Q1 N) (P4 N) (Q5 N) (Q6 N) /\
           bisim_up_to refl_t (P4 N) (Q6 N)
============================
 oneb Q (dn X) Q5 /\
   (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q5 N) (Q2 N) /\
        bisim_up_to refl_t (P2 N) (Q2 N) +)

4 other subgoals.

bisim_sound_fst < split.
Subgoal 2.1:

Variables: P Q R S X 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 +
Rstep1 : forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Sstep1 : forall N, bisim_t (Q2 N) (P2 N) (Q1 N) (Q4 N) /\
           bisim_up_to bisim_t (P2 N) (Q4 N)
Qstep : oneb Q (dn X) Q5
Qstep1 : forall N, refl_t (Q1 N) (P4 N) (Q5 N) (Q6 N) /\
           bisim_up_to refl_t (P4 N) (Q6 N)
============================
 oneb Q (dn X) Q5

5 other subgoals.

bisim_sound_fst < search.
Subgoal 2.2:

Variables: P Q R S X 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 +
Rstep1 : forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Sstep1 : forall N, bisim_t (Q2 N) (P2 N) (Q1 N) (Q4 N) /\
           bisim_up_to bisim_t (P2 N) (Q4 N)
Qstep : oneb Q (dn X) Q5
Qstep1 : forall N, refl_t (Q1 N) (P4 N) (Q5 N) (Q6 N) /\
           bisim_up_to refl_t (P4 N) (Q6 N)
============================
 exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q5 N) (Q2 N) /\
   bisim_up_to refl_t (P2 N) (Q2 N) +

4 other subgoals.

bisim_sound_fst < clear Qstep.
Subgoal 2.2:

Variables: P Q R S X 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 +
Rstep1 : forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Sstep1 : forall N, bisim_t (Q2 N) (P2 N) (Q1 N) (Q4 N) /\
           bisim_up_to bisim_t (P2 N) (Q4 N)
Qstep1 : forall N, refl_t (Q1 N) (P4 N) (Q5 N) (Q6 N) /\
           bisim_up_to refl_t (P4 N) (Q6 N)
============================
 exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q5 N) (Q2 N) /\
   bisim_up_to refl_t (P2 N) (Q2 N) +

4 other subgoals.

bisim_sound_fst < witness P1.
Subgoal 2.2:

Variables: P Q R S X 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 +
Rstep1 : forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Sstep1 : forall N, bisim_t (Q2 N) (P2 N) (Q1 N) (Q4 N) /\
           bisim_up_to bisim_t (P2 N) (Q4 N)
Qstep1 : forall N, refl_t (Q1 N) (P4 N) (Q5 N) (Q6 N) /\
           bisim_up_to refl_t (P4 N) (Q6 N)
============================
 exists Q2, forall N, refl_t (P1 N) (P1 N) (Q5 N) (Q2 N) /\
   bisim_up_to refl_t (P1 N) (Q2 N) +

4 other subgoals.

bisim_sound_fst < witness Q5.
Subgoal 2.2:

Variables: P Q R S X 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 +
Rstep1 : forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Sstep1 : forall N, bisim_t (Q2 N) (P2 N) (Q1 N) (Q4 N) /\
           bisim_up_to bisim_t (P2 N) (Q4 N)
Qstep1 : forall N, refl_t (Q1 N) (P4 N) (Q5 N) (Q6 N) /\
           bisim_up_to refl_t (P4 N) (Q6 N)
============================
 forall N, refl_t (P1 N) (P1 N) (Q5 N) (Q5 N) /\
   bisim_up_to refl_t (P1 N) (Q5 N) +

4 other subgoals.

bisim_sound_fst < intros.
Subgoal 2.2:

Variables: P Q R S X P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6 N
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 +
Rstep1 : forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Sstep1 : forall N, bisim_t (Q2 N) (P2 N) (Q1 N) (Q4 N) /\
           bisim_up_to bisim_t (P2 N) (Q4 N)
Qstep1 : forall N, refl_t (Q1 N) (P4 N) (Q5 N) (Q6 N) /\
           bisim_up_to refl_t (P4 N) (Q6 N)
============================
 refl_t (P1 N) (P1 N) (Q5 N) (Q5 N) /\ bisim_up_to refl_t (P1 N) (Q5 N) +

4 other subgoals.

bisim_sound_fst < split.
Subgoal 2.2.1:

Variables: P Q R S X P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6 N
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 +
Rstep1 : forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Sstep1 : forall N, bisim_t (Q2 N) (P2 N) (Q1 N) (Q4 N) /\
           bisim_up_to bisim_t (P2 N) (Q4 N)
Qstep1 : forall N, refl_t (Q1 N) (P4 N) (Q5 N) (Q6 N) /\
           bisim_up_to refl_t (P4 N) (Q6 N)
============================
 refl_t (P1 N) (P1 N) (Q5 N) (Q5 N)

5 other subgoals.

bisim_sound_fst < search.
Subgoal 2.2.2:

Variables: P Q R S X P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6 N
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 +
Rstep1 : forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Sstep1 : forall N, bisim_t (Q2 N) (P2 N) (Q1 N) (Q4 N) /\
           bisim_up_to bisim_t (P2 N) (Q4 N)
Qstep1 : forall N, refl_t (Q1 N) (P4 N) (Q5 N) (Q6 N) /\
           bisim_up_to refl_t (P4 N) (Q6 N)
============================
 bisim_up_to refl_t (P1 N) (Q5 N) +

4 other subgoals.

bisim_sound_fst < Before : apply *Rstep1 with N = N.
Subgoal 2.2.2:

Variables: P Q R S X P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6 N
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 +
Sstep1 : forall N, bisim_t (Q2 N) (P2 N) (Q1 N) (Q4 N) /\
           bisim_up_to bisim_t (P2 N) (Q4 N)
Qstep1 : forall N, refl_t (Q1 N) (P4 N) (Q5 N) (Q6 N) /\
           bisim_up_to refl_t (P4 N) (Q6 N)
Before : refl_t (P1 N) (P3 N) (Q2 N) (Q3 N)
Before1 : bisim_up_to refl_t (P3 N) (Q3 N)
============================
 bisim_up_to refl_t (P1 N) (Q5 N) +

4 other subgoals.

bisim_sound_fst < Eq1 : case Before.
Subgoal 2.2.2:

Variables: P Q R S X P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6 N
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 +
Sstep1 : forall N, bisim_t (Q2 N) (P2 N) (Q1 N) (Q4 N) /\
           bisim_up_to bisim_t (P2 N) (Q4 N)
Qstep1 : forall N, refl_t (Q1 N) (P4 N) (Q5 N) (Q6 N) /\
           bisim_up_to refl_t (P4 N) (Q6 N)
Before1 : bisim_up_to refl_t (P3 N) (Q3 N)
Eq1 : Q2 N = Q3 N
Eq2 : P1 N = P3 N
============================
 bisim_up_to refl_t (P1 N) (Q5 N) +

4 other subgoals.

bisim_sound_fst < Tech : apply *Sstep1 with N = N.
Subgoal 2.2.2:

Variables: P Q R S X P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6 N
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 +
Qstep1 : forall N, refl_t (Q1 N) (P4 N) (Q5 N) (Q6 N) /\
           bisim_up_to refl_t (P4 N) (Q6 N)
Before1 : bisim_up_to refl_t (P3 N) (Q3 N)
Eq1 : Q2 N = Q3 N
Eq2 : P1 N = P3 N
Tech : bisim_t (Q2 N) (P2 N) (Q1 N) (Q4 N)
Tech1 : bisim_up_to bisim_t (P2 N) (Q4 N)
============================
 bisim_up_to refl_t (P1 N) (Q5 N) +

4 other subgoals.

bisim_sound_fst < Bis1 : case Tech.
Subgoal 2.2.2:

Variables: P Q R S X P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6 N
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 +
Qstep1 : forall N, refl_t (Q1 N) (P4 N) (Q5 N) (Q6 N) /\
           bisim_up_to refl_t (P4 N) (Q6 N)
Before1 : bisim_up_to refl_t (P3 N) (Q3 N)
Eq1 : Q2 N = Q3 N
Eq2 : P1 N = P3 N
Tech1 : bisim_up_to bisim_t (P2 N) (Q4 N)
Bis1 : bisim_up_to refl_t (Q2 N) (P2 N)
Bis2 : bisim_up_to refl_t (Q1 N) (Q4 N)
============================
 bisim_up_to refl_t (P1 N) (Q5 N) +

4 other subgoals.

bisim_sound_fst < After : apply *Qstep1 with N = N.
Subgoal 2.2.2:

Variables: P Q R S X P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6 N
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 +
Before1 : bisim_up_to refl_t (P3 N) (Q3 N)
Eq1 : Q2 N = Q3 N
Eq2 : P1 N = P3 N
Tech1 : bisim_up_to bisim_t (P2 N) (Q4 N)
Bis1 : bisim_up_to refl_t (Q2 N) (P2 N)
Bis2 : bisim_up_to refl_t (Q1 N) (Q4 N)
After : refl_t (Q1 N) (P4 N) (Q5 N) (Q6 N)
After1 : bisim_up_to refl_t (P4 N) (Q6 N)
============================
 bisim_up_to refl_t (P1 N) (Q5 N) +

4 other subgoals.

bisim_sound_fst < Eq1 : case After.
Subgoal 2.2.2:

Variables: P Q R S X P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6 N
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 +
Before1 : bisim_up_to refl_t (P3 N) (Q3 N)
Eq1 : Q2 N = Q3 N
Eq2 : P1 N = P3 N
Tech1 : bisim_up_to bisim_t (P2 N) (Q4 N)
Bis1 : bisim_up_to refl_t (Q2 N) (P2 N)
Bis2 : bisim_up_to refl_t (Q1 N) (Q4 N)
After1 : bisim_up_to refl_t (P4 N) (Q6 N)
Eq3 : Q5 N = Q6 N
Eq4 : Q1 N = P4 N
============================
 bisim_up_to refl_t (P1 N) (Q5 N) +

4 other subgoals.

bisim_sound_fst < Before : apply bisim_eq_1R to *Before1 *Eq2.
Subgoal 2.2.2:

Variables: P Q R S X P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6 N
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 +
Eq1 : Q2 N = Q3 N
Tech1 : bisim_up_to bisim_t (P2 N) (Q4 N)
Bis1 : bisim_up_to refl_t (Q2 N) (P2 N)
Bis2 : bisim_up_to refl_t (Q1 N) (Q4 N)
After1 : bisim_up_to refl_t (P4 N) (Q6 N)
Eq3 : Q5 N = Q6 N
Eq4 : Q1 N = P4 N
Before : bisim_up_to refl_t (P1 N) (Q3 N)
============================
 bisim_up_to refl_t (P1 N) (Q5 N) +

4 other subgoals.

bisim_sound_fst < Before : apply bisim_eq_2R to *Before *Eq1.
Subgoal 2.2.2:

Variables: P Q R S X P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6 N
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 +
Tech1 : bisim_up_to bisim_t (P2 N) (Q4 N)
Bis1 : bisim_up_to refl_t (Q2 N) (P2 N)
Bis2 : bisim_up_to refl_t (Q1 N) (Q4 N)
After1 : bisim_up_to refl_t (P4 N) (Q6 N)
Eq3 : Q5 N = Q6 N
Eq4 : Q1 N = P4 N
Before : bisim_up_to refl_t (P1 N) (Q2 N)
============================
 bisim_up_to refl_t (P1 N) (Q5 N) +

4 other subgoals.

bisim_sound_fst < Before : apply bisim_transitive to *Before *Bis1.
Subgoal 2.2.2:

Variables: P Q R S X P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6 N
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 +
Tech1 : bisim_up_to bisim_t (P2 N) (Q4 N)
Bis2 : bisim_up_to refl_t (Q1 N) (Q4 N)
After1 : bisim_up_to refl_t (P4 N) (Q6 N)
Eq3 : Q5 N = Q6 N
Eq4 : Q1 N = P4 N
Before : bisim_up_to refl_t (P1 N) (P2 N)
============================
 bisim_up_to refl_t (P1 N) (Q5 N) +

4 other subgoals.

bisim_sound_fst < After : apply bisim_eq_2R to *After1 *Eq3.
Subgoal 2.2.2:

Variables: P Q R S X P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6 N
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 +
Tech1 : bisim_up_to bisim_t (P2 N) (Q4 N)
Bis2 : bisim_up_to refl_t (Q1 N) (Q4 N)
Eq4 : Q1 N = P4 N
Before : bisim_up_to refl_t (P1 N) (P2 N)
After : bisim_up_to refl_t (P4 N) (Q5 N)
============================
 bisim_up_to refl_t (P1 N) (Q5 N) +

4 other subgoals.

bisim_sound_fst < Link : apply bisim_symmetric to *Bis2.
Subgoal 2.2.2:

Variables: P Q R S X P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6 N
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 +
Tech1 : bisim_up_to bisim_t (P2 N) (Q4 N)
Eq4 : Q1 N = P4 N
Before : bisim_up_to refl_t (P1 N) (P2 N)
After : bisim_up_to refl_t (P4 N) (Q5 N)
Link : bisim_up_to refl_t (Q4 N) (Q1 N)
============================
 bisim_up_to refl_t (P1 N) (Q5 N) +

4 other subgoals.

bisim_sound_fst < Link : apply bisim_eq_2L to *Link *Eq4.
Subgoal 2.2.2:

Variables: P Q R S X P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6 N
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 +
Tech1 : bisim_up_to bisim_t (P2 N) (Q4 N)
Before : bisim_up_to refl_t (P1 N) (P2 N)
After : bisim_up_to refl_t (P4 N) (Q5 N)
Link : bisim_up_to refl_t (Q4 N) (P4 N)
============================
 bisim_up_to refl_t (P1 N) (Q5 N) +

4 other subgoals.

bisim_sound_fst < After : apply bisim_transitive to *Link *After.
Subgoal 2.2.2:

Variables: P Q R S X P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6 N
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 +
Tech1 : bisim_up_to bisim_t (P2 N) (Q4 N)
Before : bisim_up_to refl_t (P1 N) (P2 N)
After : bisim_up_to refl_t (Q4 N) (Q5 N)
============================
 bisim_up_to refl_t (P1 N) (Q5 N) +

4 other subgoals.

bisim_sound_fst < backchain CH.
Subgoal 3:

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 X P1, oneb P (up X) P1 ->
   (exists Q1, oneb Q (up X) Q1 /\
        (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
             bisim_up_to refl_t (P2 x) (Q2 x) +))

3 other subgoals.

bisim_sound_fst < intros Pstep.
Subgoal 3:

Variables: P Q R S X 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 : oneb P (up X) P1
============================
 exists Q1, oneb Q (up X) Q1 /\
   (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
        bisim_up_to refl_t (P2 x) (Q2 x) +)

3 other subgoals.

bisim_sound_fst < Left1 : case Left.
Subgoal 3:

Variables: P Q R S X 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 : oneb P (up X) P1
Left1 : forall L P1, one P L P1 ->
          (exists Q2, one R L Q2 /\
               (exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
Left2 : forall X P1, oneb P (dn X) P1 ->
          (exists Q2, oneb R (dn X) Q2 /\
               (exists P3 Q3, forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                    bisim_up_to refl_t (P3 N) (Q3 N)))
Left3 : forall X P1, oneb P (up X) P1 ->
          (exists Q2, oneb R (up X) Q2 /\
               (exists P3 Q3, nabla x, refl_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                    bisim_up_to refl_t (P3 x) (Q3 x)))
Left4 : forall L Q2, one R L Q2 ->
          (exists P1, one P L P1 /\
               (exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
Left5 : forall X Q2, oneb R (dn X) Q2 ->
          (exists P1, oneb P (dn X) P1 /\
               (exists P3 Q3, forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                    bisim_up_to refl_t (P3 N) (Q3 N)))
Left6 : forall X Q2, oneb R (up X) Q2 ->
          (exists P1, oneb P (up X) P1 /\
               (exists P3 Q3, nabla x, refl_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                    bisim_up_to refl_t (P3 x) (Q3 x)))
============================
 exists Q1, oneb Q (up X) Q1 /\
   (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
        bisim_up_to refl_t (P2 x) (Q2 x) +)

3 other subgoals.

bisim_sound_fst < Rstep : apply Left3 to *Pstep.
Subgoal 3:

Variables: P Q R S X 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
Left1 : forall L P1, one P L P1 ->
          (exists Q2, one R L Q2 /\
               (exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
Left2 : forall X P1, oneb P (dn X) P1 ->
          (exists Q2, oneb R (dn X) Q2 /\
               (exists P3 Q3, forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                    bisim_up_to refl_t (P3 N) (Q3 N)))
Left3 : forall X P1, oneb P (up X) P1 ->
          (exists Q2, oneb R (up X) Q2 /\
               (exists P3 Q3, nabla x, refl_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                    bisim_up_to refl_t (P3 x) (Q3 x)))
Left4 : forall L Q2, one R L Q2 ->
          (exists P1, one P L P1 /\
               (exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
Left5 : forall X Q2, oneb R (dn X) Q2 ->
          (exists P1, oneb P (dn X) P1 /\
               (exists P3 Q3, forall N, refl_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                    bisim_up_to refl_t (P3 N) (Q3 N)))
Left6 : forall X Q2, oneb R (up X) Q2 ->
          (exists P1, oneb P (up X) P1 /\
               (exists P3 Q3, nabla x, refl_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                    bisim_up_to refl_t (P3 x) (Q3 x)))
Rstep : oneb R (up X) Q2
Rstep1 : refl_t (P1 n1) (P3 n1) (Q2 n1) (Q3 n1)
Rstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
============================
 exists Q1, oneb Q (up X) Q1 /\
   (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
        bisim_up_to refl_t (P2 x) (Q2 x) +)

3 other subgoals.

bisim_sound_fst < clear Left1 Left2 Left3 Left4 Left5 Left6.
Subgoal 3:

Variables: P Q R S X 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
Rstep : oneb R (up X) Q2
Rstep1 : refl_t (P1 n1) (P3 n1) (Q2 n1) (Q3 n1)
Rstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
============================
 exists Q1, oneb Q (up X) Q1 /\
   (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
        bisim_up_to refl_t (P2 x) (Q2 x) +)

3 other subgoals.

bisim_sound_fst < Middle1 : case Middle.
Subgoal 3:

Variables: P Q R S X 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
Rstep : oneb R (up X) Q2
Rstep1 : refl_t (P1 n1) (P3 n1) (Q2 n1) (Q3 n1)
Rstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Middle1 : forall L P1, one R L P1 ->
            (exists Q2, one S L Q2 /\
                 (exists P3 Q3, bisim_t P1 P3 Q2 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle2 : forall X P1, oneb R (dn X) P1 ->
            (exists Q2, oneb S (dn X) Q2 /\
                 (exists P3 Q3, forall N, bisim_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle3 : forall X P1, oneb R (up X) P1 ->
            (exists Q2, oneb S (up X) Q2 /\
                 (exists P3 Q3, nabla x, bisim_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
Middle4 : forall L Q2, one S L Q2 ->
            (exists P1, one R L P1 /\
                 (exists P3 Q3, bisim_t P1 P3 Q2 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle5 : forall X Q2, oneb S (dn X) Q2 ->
            (exists P1, oneb R (dn X) P1 /\
                 (exists P3 Q3, forall N, bisim_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle6 : forall X Q2, oneb S (up X) Q2 ->
            (exists P1, oneb R (up X) P1 /\
                 (exists P3 Q3, nabla x, bisim_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
============================
 exists Q1, oneb Q (up X) Q1 /\
   (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
        bisim_up_to refl_t (P2 x) (Q2 x) +)

3 other subgoals.

bisim_sound_fst < Sstep : apply Middle3 to *Rstep.
Subgoal 3:

Variables: P Q R S X 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
Rstep1 : refl_t (P1 n1) (P3 n1) (Q2 n1) (Q3 n1)
Rstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Middle1 : forall L P1, one R L P1 ->
            (exists Q2, one S L Q2 /\
                 (exists P3 Q3, bisim_t P1 P3 Q2 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle2 : forall X P1, oneb R (dn X) P1 ->
            (exists Q2, oneb S (dn X) Q2 /\
                 (exists P3 Q3, forall N, bisim_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle3 : forall X P1, oneb R (up X) P1 ->
            (exists Q2, oneb S (up X) Q2 /\
                 (exists P3 Q3, nabla x, bisim_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
Middle4 : forall L Q2, one S L Q2 ->
            (exists P1, one R L P1 /\
                 (exists P3 Q3, bisim_t P1 P3 Q2 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle5 : forall X Q2, oneb S (dn X) Q2 ->
            (exists P1, oneb R (dn X) P1 /\
                 (exists P3 Q3, forall N, bisim_t (P1 N) (P3 N) (Q2 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle6 : forall X Q2, oneb S (up X) Q2 ->
            (exists P1, oneb R (up X) P1 /\
                 (exists P3 Q3, nabla x, bisim_t (P1 x) (P3 x) (Q2 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
Sstep : oneb S (up X) Q1
Sstep1 : bisim_t (Q2 n1) (P2 n1) (Q1 n1) (Q4 n1)
Sstep2 : bisim_up_to bisim_t (P2 n1) (Q4 n1)
============================
 exists Q1, oneb Q (up X) Q1 /\
   (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
        bisim_up_to refl_t (P2 x) (Q2 x) +)

3 other subgoals.

bisim_sound_fst < clear Middle1 Middle2 Middle3 Middle4 Middle5 Middle6.
Subgoal 3:

Variables: P Q R S X 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
Rstep1 : refl_t (P1 n1) (P3 n1) (Q2 n1) (Q3 n1)
Rstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Sstep : oneb S (up X) Q1
Sstep1 : bisim_t (Q2 n1) (P2 n1) (Q1 n1) (Q4 n1)
Sstep2 : bisim_up_to bisim_t (P2 n1) (Q4 n1)
============================
 exists Q1, oneb Q (up X) Q1 /\
   (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
        bisim_up_to refl_t (P2 x) (Q2 x) +)

3 other subgoals.

bisim_sound_fst < Right1 : case Right.
Subgoal 3:

Variables: P Q R S X 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 +
Rstep1 : refl_t (P1 n1) (P3 n1) (Q2 n1) (Q3 n1)
Rstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Sstep : oneb S (up X) Q1
Sstep1 : bisim_t (Q2 n1) (P2 n1) (Q1 n1) (Q4 n1)
Sstep2 : bisim_up_to bisim_t (P2 n1) (Q4 n1)
Right1 : forall L P1, one S L P1 ->
           (exists Q1, one Q L Q1 /\
                (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\
                     bisim_up_to refl_t P2 Q2))
Right2 : forall X P1, oneb S (dn X) P1 ->
           (exists Q1, oneb Q (dn X) Q1 /\
                (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                     bisim_up_to refl_t (P2 N) (Q2 N)))
Right3 : forall X P1, oneb S (up X) P1 ->
           (exists Q1, oneb Q (up X) Q1 /\
                (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                     bisim_up_to refl_t (P2 x) (Q2 x)))
Right4 : forall L Q1, one Q L Q1 ->
           (exists P1, one S L P1 /\
                (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\
                     bisim_up_to refl_t P2 Q2))
Right5 : forall X Q1, oneb Q (dn X) Q1 ->
           (exists P1, oneb S (dn X) P1 /\
                (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                     bisim_up_to refl_t (P2 N) (Q2 N)))
Right6 : forall X Q1, oneb Q (up X) Q1 ->
           (exists P1, oneb S (up X) P1 /\
                (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                     bisim_up_to refl_t (P2 x) (Q2 x)))
============================
 exists Q1, oneb Q (up X) Q1 /\
   (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
        bisim_up_to refl_t (P2 x) (Q2 x) +)

3 other subgoals.

bisim_sound_fst < Qstep : apply Right3 to *Sstep.
Subgoal 3:

Variables: P Q R S X 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 +
Rstep1 : refl_t (P1 n1) (P3 n1) (Q2 n1) (Q3 n1)
Rstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Sstep1 : bisim_t (Q2 n1) (P2 n1) (Q1 n1) (Q4 n1)
Sstep2 : bisim_up_to bisim_t (P2 n1) (Q4 n1)
Right1 : forall L P1, one S L P1 ->
           (exists Q1, one Q L Q1 /\
                (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\
                     bisim_up_to refl_t P2 Q2))
Right2 : forall X P1, oneb S (dn X) P1 ->
           (exists Q1, oneb Q (dn X) Q1 /\
                (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                     bisim_up_to refl_t (P2 N) (Q2 N)))
Right3 : forall X P1, oneb S (up X) P1 ->
           (exists Q1, oneb Q (up X) Q1 /\
                (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                     bisim_up_to refl_t (P2 x) (Q2 x)))
Right4 : forall L Q1, one Q L Q1 ->
           (exists P1, one S L P1 /\
                (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\
                     bisim_up_to refl_t P2 Q2))
Right5 : forall X Q1, oneb Q (dn X) Q1 ->
           (exists P1, oneb S (dn X) P1 /\
                (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                     bisim_up_to refl_t (P2 N) (Q2 N)))
Right6 : forall X Q1, oneb Q (up X) Q1 ->
           (exists P1, oneb S (up X) P1 /\
                (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                     bisim_up_to refl_t (P2 x) (Q2 x)))
Qstep : oneb Q (up X) Q5
Qstep1 : refl_t (Q1 n1) (P4 n1) (Q5 n1) (Q6 n1)
Qstep2 : bisim_up_to refl_t (P4 n1) (Q6 n1)
============================
 exists Q1, oneb Q (up X) Q1 /\
   (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
        bisim_up_to refl_t (P2 x) (Q2 x) +)

3 other subgoals.

bisim_sound_fst < clear Right1 Right2 Right3 Right4 Right5 Right6.
Subgoal 3:

Variables: P Q R S X 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 +
Rstep1 : refl_t (P1 n1) (P3 n1) (Q2 n1) (Q3 n1)
Rstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Sstep1 : bisim_t (Q2 n1) (P2 n1) (Q1 n1) (Q4 n1)
Sstep2 : bisim_up_to bisim_t (P2 n1) (Q4 n1)
Qstep : oneb Q (up X) Q5
Qstep1 : refl_t (Q1 n1) (P4 n1) (Q5 n1) (Q6 n1)
Qstep2 : bisim_up_to refl_t (P4 n1) (Q6 n1)
============================
 exists Q1, oneb Q (up X) Q1 /\
   (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
        bisim_up_to refl_t (P2 x) (Q2 x) +)

3 other subgoals.

bisim_sound_fst < witness Q5.
Subgoal 3:

Variables: P Q R S X 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 +
Rstep1 : refl_t (P1 n1) (P3 n1) (Q2 n1) (Q3 n1)
Rstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Sstep1 : bisim_t (Q2 n1) (P2 n1) (Q1 n1) (Q4 n1)
Sstep2 : bisim_up_to bisim_t (P2 n1) (Q4 n1)
Qstep : oneb Q (up X) Q5
Qstep1 : refl_t (Q1 n1) (P4 n1) (Q5 n1) (Q6 n1)
Qstep2 : bisim_up_to refl_t (P4 n1) (Q6 n1)
============================
 oneb Q (up X) Q5 /\
   (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q5 x) (Q2 x) /\
        bisim_up_to refl_t (P2 x) (Q2 x) +)

3 other subgoals.

bisim_sound_fst < split.
Subgoal 3.1:

Variables: P Q R S X 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 +
Rstep1 : refl_t (P1 n1) (P3 n1) (Q2 n1) (Q3 n1)
Rstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Sstep1 : bisim_t (Q2 n1) (P2 n1) (Q1 n1) (Q4 n1)
Sstep2 : bisim_up_to bisim_t (P2 n1) (Q4 n1)
Qstep : oneb Q (up X) Q5
Qstep1 : refl_t (Q1 n1) (P4 n1) (Q5 n1) (Q6 n1)
Qstep2 : bisim_up_to refl_t (P4 n1) (Q6 n1)
============================
 oneb Q (up X) Q5

4 other subgoals.

bisim_sound_fst < search.
Subgoal 3.2:

Variables: P Q R S X 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 +
Rstep1 : refl_t (P1 n1) (P3 n1) (Q2 n1) (Q3 n1)
Rstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Sstep1 : bisim_t (Q2 n1) (P2 n1) (Q1 n1) (Q4 n1)
Sstep2 : bisim_up_to bisim_t (P2 n1) (Q4 n1)
Qstep : oneb Q (up X) Q5
Qstep1 : refl_t (Q1 n1) (P4 n1) (Q5 n1) (Q6 n1)
Qstep2 : bisim_up_to refl_t (P4 n1) (Q6 n1)
============================
 exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q5 x) (Q2 x) /\
   bisim_up_to refl_t (P2 x) (Q2 x) +

3 other subgoals.

bisim_sound_fst < clear Qstep.
Subgoal 3.2:

Variables: P Q R S X 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 +
Rstep1 : refl_t (P1 n1) (P3 n1) (Q2 n1) (Q3 n1)
Rstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Sstep1 : bisim_t (Q2 n1) (P2 n1) (Q1 n1) (Q4 n1)
Sstep2 : bisim_up_to bisim_t (P2 n1) (Q4 n1)
Qstep1 : refl_t (Q1 n1) (P4 n1) (Q5 n1) (Q6 n1)
Qstep2 : bisim_up_to refl_t (P4 n1) (Q6 n1)
============================
 exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q5 x) (Q2 x) /\
   bisim_up_to refl_t (P2 x) (Q2 x) +

3 other subgoals.

bisim_sound_fst < witness P1.
Subgoal 3.2:

Variables: P Q R S X 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 +
Rstep1 : refl_t (P1 n1) (P3 n1) (Q2 n1) (Q3 n1)
Rstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Sstep1 : bisim_t (Q2 n1) (P2 n1) (Q1 n1) (Q4 n1)
Sstep2 : bisim_up_to bisim_t (P2 n1) (Q4 n1)
Qstep1 : refl_t (Q1 n1) (P4 n1) (Q5 n1) (Q6 n1)
Qstep2 : bisim_up_to refl_t (P4 n1) (Q6 n1)
============================
 exists Q2, nabla x, refl_t (P1 x) (P1 x) (Q5 x) (Q2 x) /\
   bisim_up_to refl_t (P1 x) (Q2 x) +

3 other subgoals.

bisim_sound_fst < witness Q5.
Subgoal 3.2:

Variables: P Q R S X 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 +
Rstep1 : refl_t (P1 n1) (P3 n1) (Q2 n1) (Q3 n1)
Rstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Sstep1 : bisim_t (Q2 n1) (P2 n1) (Q1 n1) (Q4 n1)
Sstep2 : bisim_up_to bisim_t (P2 n1) (Q4 n1)
Qstep1 : refl_t (Q1 n1) (P4 n1) (Q5 n1) (Q6 n1)
Qstep2 : bisim_up_to refl_t (P4 n1) (Q6 n1)
============================
 nabla x, refl_t (P1 x) (P1 x) (Q5 x) (Q5 x) /\
   bisim_up_to refl_t (P1 x) (Q5 x) +

3 other subgoals.

bisim_sound_fst < intros.
Subgoal 3.2:

Variables: P Q R S X 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 +
Rstep1 : refl_t (P1 n1) (P3 n1) (Q2 n1) (Q3 n1)
Rstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Sstep1 : bisim_t (Q2 n1) (P2 n1) (Q1 n1) (Q4 n1)
Sstep2 : bisim_up_to bisim_t (P2 n1) (Q4 n1)
Qstep1 : refl_t (Q1 n1) (P4 n1) (Q5 n1) (Q6 n1)
Qstep2 : bisim_up_to refl_t (P4 n1) (Q6 n1)
============================
 refl_t (P1 n1) (P1 n1) (Q5 n1) (Q5 n1) /\
   bisim_up_to refl_t (P1 n1) (Q5 n1) +

3 other subgoals.

bisim_sound_fst < split.
Subgoal 3.2.1:

Variables: P Q R S X 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 +
Rstep1 : refl_t (P1 n1) (P3 n1) (Q2 n1) (Q3 n1)
Rstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Sstep1 : bisim_t (Q2 n1) (P2 n1) (Q1 n1) (Q4 n1)
Sstep2 : bisim_up_to bisim_t (P2 n1) (Q4 n1)
Qstep1 : refl_t (Q1 n1) (P4 n1) (Q5 n1) (Q6 n1)
Qstep2 : bisim_up_to refl_t (P4 n1) (Q6 n1)
============================
 refl_t (P1 n1) (P1 n1) (Q5 n1) (Q5 n1)

4 other subgoals.

bisim_sound_fst < search.
Subgoal 3.2.2:

Variables: P Q R S X 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 +
Rstep1 : refl_t (P1 n1) (P3 n1) (Q2 n1) (Q3 n1)
Rstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Sstep1 : bisim_t (Q2 n1) (P2 n1) (Q1 n1) (Q4 n1)
Sstep2 : bisim_up_to bisim_t (P2 n1) (Q4 n1)
Qstep1 : refl_t (Q1 n1) (P4 n1) (Q5 n1) (Q6 n1)
Qstep2 : bisim_up_to refl_t (P4 n1) (Q6 n1)
============================
 bisim_up_to refl_t (P1 n1) (Q5 n1) +

3 other subgoals.

bisim_sound_fst < case Rstep1.
Subgoal 3.2.2:

Variables: P Q R S X 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 +
Rstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Sstep1 : bisim_t (Q3 n1) (P2 n1) (Q1 n1) (Q4 n1)
Sstep2 : bisim_up_to bisim_t (P2 n1) (Q4 n1)
Qstep1 : refl_t (Q1 n1) (P4 n1) (Q5 n1) (Q6 n1)
Qstep2 : bisim_up_to refl_t (P4 n1) (Q6 n1)
============================
 bisim_up_to refl_t (P3 n1) (Q5 n1) +

3 other subgoals.

bisim_sound_fst < case Qstep1.
Subgoal 3.2.2:

Variables: P Q R S X 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 +
Rstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Sstep1 : bisim_t (Q3 n1) (P2 n1) (P4 n1) (Q4 n1)
Sstep2 : bisim_up_to bisim_t (P2 n1) (Q4 n1)
Qstep2 : bisim_up_to refl_t (P4 n1) (Q6 n1)
============================
 bisim_up_to refl_t (P3 n1) (Q6 n1) +

3 other subgoals.

bisim_sound_fst < Tech1 : case Sstep1.
Subgoal 3.2.2:

Variables: P Q R S X 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 +
Rstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Sstep2 : bisim_up_to bisim_t (P2 n1) (Q4 n1)
Qstep2 : bisim_up_to refl_t (P4 n1) (Q6 n1)
Tech1 : bisim_up_to refl_t (Q3 n1) (P2 n1)
Tech2 : bisim_up_to refl_t (P4 n1) (Q4 n1)
============================
 bisim_up_to refl_t (P3 n1) (Q6 n1) +

3 other subgoals.

bisim_sound_fst < Before : apply bisim_transitive to *Rstep2 *Tech1.
Subgoal 3.2.2:

Variables: P Q R S X 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 +
Sstep2 : bisim_up_to bisim_t (P2 n1) (Q4 n1)
Qstep2 : bisim_up_to refl_t (P4 n1) (Q6 n1)
Tech2 : bisim_up_to refl_t (P4 n1) (Q4 n1)
Before : bisim_up_to refl_t (P3 n1) (P2 n1)
============================
 bisim_up_to refl_t (P3 n1) (Q6 n1) +

3 other subgoals.

bisim_sound_fst < After : apply bisim_symmetric to *Tech2.
Subgoal 3.2.2:

Variables: P Q R S X 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 +
Sstep2 : bisim_up_to bisim_t (P2 n1) (Q4 n1)
Qstep2 : bisim_up_to refl_t (P4 n1) (Q6 n1)
Before : bisim_up_to refl_t (P3 n1) (P2 n1)
After : bisim_up_to refl_t (Q4 n1) (P4 n1)
============================
 bisim_up_to refl_t (P3 n1) (Q6 n1) +

3 other subgoals.

bisim_sound_fst < After : apply bisim_transitive to *After *Qstep2.
Subgoal 3.2.2:

Variables: P Q R S X 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 +
Sstep2 : bisim_up_to bisim_t (P2 n1) (Q4 n1)
Before : bisim_up_to refl_t (P3 n1) (P2 n1)
After : bisim_up_to refl_t (Q4 n1) (Q6 n1)
============================
 bisim_up_to refl_t (P3 n1) (Q6 n1) +

3 other subgoals.

bisim_sound_fst < backchain CH.
Subgoal 4:

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 L Q1, one Q L Q1 ->
   (exists P1, one P L P1 /\
        (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))

2 other subgoals.

bisim_sound_fst < intros Qstep.
Subgoal 4:

Variables: P Q R S L 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 L Q1
============================
 exists P1, one P L P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

2 other subgoals.

bisim_sound_fst < Right1 : case Right.
Subgoal 4:

Variables: P Q R S L 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 L Q1
Right1 : forall L P2, one S L P2 ->
           (exists Q1, one Q L Q1 /\
                (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\
                     bisim_up_to refl_t P3 Q3))
Right2 : forall X P2, oneb S (dn X) P2 ->
           (exists Q1, oneb Q (dn X) Q1 /\
                (exists P3 Q3, forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                     bisim_up_to refl_t (P3 N) (Q3 N)))
Right3 : forall X P2, oneb S (up X) P2 ->
           (exists Q1, oneb Q (up X) Q1 /\
                (exists P3 Q3, nabla x, refl_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                     bisim_up_to refl_t (P3 x) (Q3 x)))
Right4 : forall L Q1, one Q L Q1 ->
           (exists P2, one S L P2 /\
                (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\
                     bisim_up_to refl_t P3 Q3))
Right5 : forall X Q1, oneb Q (dn X) Q1 ->
           (exists P2, oneb S (dn X) P2 /\
                (exists P3 Q3, forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                     bisim_up_to refl_t (P3 N) (Q3 N)))
Right6 : forall X Q1, oneb Q (up X) Q1 ->
           (exists P2, oneb S (up X) P2 /\
                (exists P3 Q3, nabla x, refl_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                     bisim_up_to refl_t (P3 x) (Q3 x)))
============================
 exists P1, one P L P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

2 other subgoals.

bisim_sound_fst < Sstep : apply Right4 to *Qstep.
Subgoal 4:

Variables: P Q R S L 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
Right1 : forall L P2, one S L P2 ->
           (exists Q1, one Q L Q1 /\
                (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\
                     bisim_up_to refl_t P3 Q3))
Right2 : forall X P2, oneb S (dn X) P2 ->
           (exists Q1, oneb Q (dn X) Q1 /\
                (exists P3 Q3, forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                     bisim_up_to refl_t (P3 N) (Q3 N)))
Right3 : forall X P2, oneb S (up X) P2 ->
           (exists Q1, oneb Q (up X) Q1 /\
                (exists P3 Q3, nabla x, refl_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                     bisim_up_to refl_t (P3 x) (Q3 x)))
Right4 : forall L Q1, one Q L Q1 ->
           (exists P2, one S L P2 /\
                (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\
                     bisim_up_to refl_t P3 Q3))
Right5 : forall X Q1, oneb Q (dn X) Q1 ->
           (exists P2, oneb S (dn X) P2 /\
                (exists P3 Q3, forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                     bisim_up_to refl_t (P3 N) (Q3 N)))
Right6 : forall X Q1, oneb Q (up X) Q1 ->
           (exists P2, oneb S (up X) P2 /\
                (exists P3 Q3, nabla x, refl_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                     bisim_up_to refl_t (P3 x) (Q3 x)))
Sstep : one S L P2
Sstep1 : refl_t P2 P3 Q1 Q3
Sstep2 : bisim_up_to refl_t P3 Q3
============================
 exists P1, one P L P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

2 other subgoals.

bisim_sound_fst < clear Right1 Right2 Right3 Right4 Right5 Right6.
Subgoal 4:

Variables: P Q R S L 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
Sstep : one S L P2
Sstep1 : refl_t P2 P3 Q1 Q3
Sstep2 : bisim_up_to refl_t P3 Q3
============================
 exists P1, one P L P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

2 other subgoals.

bisim_sound_fst < Middle1 : case Middle.
Subgoal 4:

Variables: P Q R S L 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
Sstep : one S L P2
Sstep1 : refl_t P2 P3 Q1 Q3
Sstep2 : bisim_up_to refl_t P3 Q3
Middle1 : forall L P2, one R L P2 ->
            (exists Q1, one S L Q1 /\
                 (exists P3 Q3, bisim_t P2 P3 Q1 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle2 : forall X P2, oneb R (dn X) P2 ->
            (exists Q1, oneb S (dn X) Q1 /\
                 (exists P3 Q3, forall N, bisim_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle3 : forall X P2, oneb R (up X) P2 ->
            (exists Q1, oneb S (up X) Q1 /\
                 (exists P3 Q3, nabla x, bisim_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
Middle4 : forall L Q1, one S L Q1 ->
            (exists P2, one R L P2 /\
                 (exists P3 Q3, bisim_t P2 P3 Q1 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle5 : forall X Q1, oneb S (dn X) Q1 ->
            (exists P2, oneb R (dn X) P2 /\
                 (exists P3 Q3, forall N, bisim_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle6 : forall X Q1, oneb S (up X) Q1 ->
            (exists P2, oneb R (up X) P2 /\
                 (exists P3 Q3, nabla x, bisim_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
============================
 exists P1, one P L P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

2 other subgoals.

bisim_sound_fst < Rstep : apply Middle4 to *Sstep.
Subgoal 4:

Variables: P Q R S L 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
Sstep1 : refl_t P2 P3 Q1 Q3
Sstep2 : bisim_up_to refl_t P3 Q3
Middle1 : forall L P2, one R L P2 ->
            (exists Q1, one S L Q1 /\
                 (exists P3 Q3, bisim_t P2 P3 Q1 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle2 : forall X P2, oneb R (dn X) P2 ->
            (exists Q1, oneb S (dn X) Q1 /\
                 (exists P3 Q3, forall N, bisim_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle3 : forall X P2, oneb R (up X) P2 ->
            (exists Q1, oneb S (up X) Q1 /\
                 (exists P3 Q3, nabla x, bisim_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
Middle4 : forall L Q1, one S L Q1 ->
            (exists P2, one R L P2 /\
                 (exists P3 Q3, bisim_t P2 P3 Q1 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle5 : forall X Q1, oneb S (dn X) Q1 ->
            (exists P2, oneb R (dn X) P2 /\
                 (exists P3 Q3, forall N, bisim_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle6 : forall X Q1, oneb S (up X) Q1 ->
            (exists P2, oneb R (up X) P2 /\
                 (exists P3 Q3, nabla x, bisim_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
Rstep : one R L P1
Rstep1 : bisim_t P1 P4 P2 Q2
Rstep2 : bisim_up_to bisim_t P4 Q2
============================
 exists P1, one P L P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

2 other subgoals.

bisim_sound_fst < clear Middle1 Middle2 Middle3 Middle4 Middle5 Middle6.
Subgoal 4:

Variables: P Q R S L 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
Sstep1 : refl_t P2 P3 Q1 Q3
Sstep2 : bisim_up_to refl_t P3 Q3
Rstep : one R L P1
Rstep1 : bisim_t P1 P4 P2 Q2
Rstep2 : bisim_up_to bisim_t P4 Q2
============================
 exists P1, one P L P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

2 other subgoals.

bisim_sound_fst < Left1 : case Left.
Subgoal 4:

Variables: P Q R S L 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 +
Sstep1 : refl_t P2 P3 Q1 Q3
Sstep2 : bisim_up_to refl_t P3 Q3
Rstep : one R L P1
Rstep1 : bisim_t P1 P4 P2 Q2
Rstep2 : bisim_up_to bisim_t P4 Q2
Left1 : forall L P1, one P L P1 ->
          (exists Q1, one R L Q1 /\
               (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
Left2 : forall X P1, oneb P (dn X) P1 ->
          (exists Q1, oneb R (dn X) Q1 /\
               (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                    bisim_up_to refl_t (P2 N) (Q2 N)))
Left3 : forall X P1, oneb P (up X) P1 ->
          (exists Q1, oneb R (up X) Q1 /\
               (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                    bisim_up_to refl_t (P2 x) (Q2 x)))
Left4 : forall L Q1, one R L Q1 ->
          (exists P1, one P L P1 /\
               (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
Left5 : forall X Q1, oneb R (dn X) Q1 ->
          (exists P1, oneb P (dn X) P1 /\
               (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                    bisim_up_to refl_t (P2 N) (Q2 N)))
Left6 : forall X Q1, oneb R (up X) Q1 ->
          (exists P1, oneb P (up X) P1 /\
               (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                    bisim_up_to refl_t (P2 x) (Q2 x)))
============================
 exists P1, one P L P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

2 other subgoals.

bisim_sound_fst < Pstep : apply Left4 to *Rstep.
Subgoal 4:

Variables: P Q R S L 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 +
Sstep1 : refl_t P2 P3 Q1 Q3
Sstep2 : bisim_up_to refl_t P3 Q3
Rstep1 : bisim_t P1 P4 P2 Q2
Rstep2 : bisim_up_to bisim_t P4 Q2
Left1 : forall L P1, one P L P1 ->
          (exists Q1, one R L Q1 /\
               (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
Left2 : forall X P1, oneb P (dn X) P1 ->
          (exists Q1, oneb R (dn X) Q1 /\
               (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                    bisim_up_to refl_t (P2 N) (Q2 N)))
Left3 : forall X P1, oneb P (up X) P1 ->
          (exists Q1, oneb R (up X) Q1 /\
               (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                    bisim_up_to refl_t (P2 x) (Q2 x)))
Left4 : forall L Q1, one R L Q1 ->
          (exists P1, one P L P1 /\
               (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
Left5 : forall X Q1, oneb R (dn X) Q1 ->
          (exists P1, oneb P (dn X) P1 /\
               (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                    bisim_up_to refl_t (P2 N) (Q2 N)))
Left6 : forall X Q1, oneb R (up X) Q1 ->
          (exists P1, oneb P (up X) P1 /\
               (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                    bisim_up_to refl_t (P2 x) (Q2 x)))
Pstep : one P L P5
Pstep1 : refl_t P5 P6 P1 Q4
Pstep2 : bisim_up_to refl_t P6 Q4
============================
 exists P1, one P L P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

2 other subgoals.

bisim_sound_fst < clear Left1 Left2 Left3 Left4 Left5 Left6.
Subgoal 4:

Variables: P Q R S L 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 +
Sstep1 : refl_t P2 P3 Q1 Q3
Sstep2 : bisim_up_to refl_t P3 Q3
Rstep1 : bisim_t P1 P4 P2 Q2
Rstep2 : bisim_up_to bisim_t P4 Q2
Pstep : one P L P5
Pstep1 : refl_t P5 P6 P1 Q4
Pstep2 : bisim_up_to refl_t P6 Q4
============================
 exists P1, one P L P1 /\
   (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

2 other subgoals.

bisim_sound_fst < witness P5.
Subgoal 4:

Variables: P Q R S L 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 +
Sstep1 : refl_t P2 P3 Q1 Q3
Sstep2 : bisim_up_to refl_t P3 Q3
Rstep1 : bisim_t P1 P4 P2 Q2
Rstep2 : bisim_up_to bisim_t P4 Q2
Pstep : one P L P5
Pstep1 : refl_t P5 P6 P1 Q4
Pstep2 : bisim_up_to refl_t P6 Q4
============================
 one P L P5 /\
   (exists P2 Q2, refl_t P5 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)

2 other subgoals.

bisim_sound_fst < split.
Subgoal 4.1:

Variables: P Q R S L 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 +
Sstep1 : refl_t P2 P3 Q1 Q3
Sstep2 : bisim_up_to refl_t P3 Q3
Rstep1 : bisim_t P1 P4 P2 Q2
Rstep2 : bisim_up_to bisim_t P4 Q2
Pstep : one P L P5
Pstep1 : refl_t P5 P6 P1 Q4
Pstep2 : bisim_up_to refl_t P6 Q4
============================
 one P L P5

3 other subgoals.

bisim_sound_fst < search.
Subgoal 4.2:

Variables: P Q R S L 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 +
Sstep1 : refl_t P2 P3 Q1 Q3
Sstep2 : bisim_up_to refl_t P3 Q3
Rstep1 : bisim_t P1 P4 P2 Q2
Rstep2 : bisim_up_to bisim_t P4 Q2
Pstep : one P L P5
Pstep1 : refl_t P5 P6 P1 Q4
Pstep2 : bisim_up_to refl_t P6 Q4
============================
 exists P2 Q2, refl_t P5 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +

2 other subgoals.

bisim_sound_fst < clear Pstep.
Subgoal 4.2:

Variables: P Q R S L 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 +
Sstep1 : refl_t P2 P3 Q1 Q3
Sstep2 : bisim_up_to refl_t P3 Q3
Rstep1 : bisim_t P1 P4 P2 Q2
Rstep2 : bisim_up_to bisim_t P4 Q2
Pstep1 : refl_t P5 P6 P1 Q4
Pstep2 : bisim_up_to refl_t P6 Q4
============================
 exists P2 Q2, refl_t P5 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +

2 other subgoals.

bisim_sound_fst < witness P5.
Subgoal 4.2:

Variables: P Q R S L 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 +
Sstep1 : refl_t P2 P3 Q1 Q3
Sstep2 : bisim_up_to refl_t P3 Q3
Rstep1 : bisim_t P1 P4 P2 Q2
Rstep2 : bisim_up_to bisim_t P4 Q2
Pstep1 : refl_t P5 P6 P1 Q4
Pstep2 : bisim_up_to refl_t P6 Q4
============================
 exists Q2, refl_t P5 P5 Q1 Q2 /\ bisim_up_to refl_t P5 Q2 +

2 other subgoals.

bisim_sound_fst < witness Q1.
Subgoal 4.2:

Variables: P Q R S L 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 +
Sstep1 : refl_t P2 P3 Q1 Q3
Sstep2 : bisim_up_to refl_t P3 Q3
Rstep1 : bisim_t P1 P4 P2 Q2
Rstep2 : bisim_up_to bisim_t P4 Q2
Pstep1 : refl_t P5 P6 P1 Q4
Pstep2 : bisim_up_to refl_t P6 Q4
============================
 refl_t P5 P5 Q1 Q1 /\ bisim_up_to refl_t P5 Q1 +

2 other subgoals.

bisim_sound_fst < split.
Subgoal 4.2.1:

Variables: P Q R S L 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 +
Sstep1 : refl_t P2 P3 Q1 Q3
Sstep2 : bisim_up_to refl_t P3 Q3
Rstep1 : bisim_t P1 P4 P2 Q2
Rstep2 : bisim_up_to bisim_t P4 Q2
Pstep1 : refl_t P5 P6 P1 Q4
Pstep2 : bisim_up_to refl_t P6 Q4
============================
 refl_t P5 P5 Q1 Q1

3 other subgoals.

bisim_sound_fst < search.
Subgoal 4.2.2:

Variables: P Q R S L 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 +
Sstep1 : refl_t P2 P3 Q1 Q3
Sstep2 : bisim_up_to refl_t P3 Q3
Rstep1 : bisim_t P1 P4 P2 Q2
Rstep2 : bisim_up_to bisim_t P4 Q2
Pstep1 : refl_t P5 P6 P1 Q4
Pstep2 : bisim_up_to refl_t P6 Q4
============================
 bisim_up_to refl_t P5 Q1 +

2 other subgoals.

bisim_sound_fst < case Sstep1.
Subgoal 4.2.2:

Variables: P Q R S L 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 +
Sstep2 : bisim_up_to refl_t P3 Q3
Rstep1 : bisim_t P1 P4 P3 Q2
Rstep2 : bisim_up_to bisim_t P4 Q2
Pstep1 : refl_t P5 P6 P1 Q4
Pstep2 : bisim_up_to refl_t P6 Q4
============================
 bisim_up_to refl_t P5 Q3 +

2 other subgoals.

bisim_sound_fst < case Pstep1.
Subgoal 4.2.2:

Variables: P Q R S L 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 +
Sstep2 : bisim_up_to refl_t P3 Q3
Rstep1 : bisim_t Q4 P4 P3 Q2
Rstep2 : bisim_up_to bisim_t P4 Q2
Pstep2 : bisim_up_to refl_t P6 Q4
============================
 bisim_up_to refl_t P6 Q3 +

2 other subgoals.

bisim_sound_fst < Tech1 : case Rstep1.
Subgoal 4.2.2:

Variables: P Q R S L 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 +
Sstep2 : bisim_up_to refl_t P3 Q3
Rstep2 : bisim_up_to bisim_t P4 Q2
Pstep2 : bisim_up_to refl_t P6 Q4
Tech1 : bisim_up_to refl_t Q4 P4
Tech2 : bisim_up_to refl_t P3 Q2
============================
 bisim_up_to refl_t P6 Q3 +

2 other subgoals.

bisim_sound_fst < Before : apply bisim_transitive to *Pstep2 *Tech1.
Subgoal 4.2.2:

Variables: P Q R S L 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 +
Sstep2 : bisim_up_to refl_t P3 Q3
Rstep2 : bisim_up_to bisim_t P4 Q2
Tech2 : bisim_up_to refl_t P3 Q2
Before : bisim_up_to refl_t P6 P4
============================
 bisim_up_to refl_t P6 Q3 +

2 other subgoals.

bisim_sound_fst < Link : apply bisim_symmetric to *Tech2.
Subgoal 4.2.2:

Variables: P Q R S L 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 +
Sstep2 : bisim_up_to refl_t P3 Q3
Rstep2 : bisim_up_to bisim_t P4 Q2
Before : bisim_up_to refl_t P6 P4
Link : bisim_up_to refl_t Q2 P3
============================
 bisim_up_to refl_t P6 Q3 +

2 other subgoals.

bisim_sound_fst < After : apply bisim_transitive to *Link *Sstep2.
Subgoal 4.2.2:

Variables: P Q R S L 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 +
Rstep2 : bisim_up_to bisim_t P4 Q2
Before : bisim_up_to refl_t P6 P4
After : bisim_up_to refl_t Q2 Q3
============================
 bisim_up_to refl_t P6 Q3 +

2 other subgoals.

bisim_sound_fst < backchain CH.
Subgoal 5:

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 X Q1, oneb Q (dn X) Q1 ->
   (exists P1, oneb P (dn X) P1 /\
        (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
             bisim_up_to refl_t (P2 N) (Q2 N) +))

1 other subgoal.

bisim_sound_fst < intros Qstep.
Subgoal 5:

Variables: P Q R S X 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 : oneb Q (dn X) Q1
============================
 exists P1, oneb P (dn X) P1 /\
   (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
        bisim_up_to refl_t (P2 N) (Q2 N) +)

1 other subgoal.

bisim_sound_fst < Right1 : case Right.
Subgoal 5:

Variables: P Q R S X 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 : oneb Q (dn X) Q1
Right1 : forall L P2, one S L P2 ->
           (exists Q1, one Q L Q1 /\
                (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\
                     bisim_up_to refl_t P3 Q3))
Right2 : forall X P2, oneb S (dn X) P2 ->
           (exists Q1, oneb Q (dn X) Q1 /\
                (exists P3 Q3, forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                     bisim_up_to refl_t (P3 N) (Q3 N)))
Right3 : forall X P2, oneb S (up X) P2 ->
           (exists Q1, oneb Q (up X) Q1 /\
                (exists P3 Q3, nabla x, refl_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                     bisim_up_to refl_t (P3 x) (Q3 x)))
Right4 : forall L Q1, one Q L Q1 ->
           (exists P2, one S L P2 /\
                (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\
                     bisim_up_to refl_t P3 Q3))
Right5 : forall X Q1, oneb Q (dn X) Q1 ->
           (exists P2, oneb S (dn X) P2 /\
                (exists P3 Q3, forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                     bisim_up_to refl_t (P3 N) (Q3 N)))
Right6 : forall X Q1, oneb Q (up X) Q1 ->
           (exists P2, oneb S (up X) P2 /\
                (exists P3 Q3, nabla x, refl_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                     bisim_up_to refl_t (P3 x) (Q3 x)))
============================
 exists P1, oneb P (dn X) P1 /\
   (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
        bisim_up_to refl_t (P2 N) (Q2 N) +)

1 other subgoal.

bisim_sound_fst < Sstep : apply Right5 to *Qstep.
Subgoal 5:

Variables: P Q R S X 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
Right1 : forall L P2, one S L P2 ->
           (exists Q1, one Q L Q1 /\
                (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\
                     bisim_up_to refl_t P3 Q3))
Right2 : forall X P2, oneb S (dn X) P2 ->
           (exists Q1, oneb Q (dn X) Q1 /\
                (exists P3 Q3, forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                     bisim_up_to refl_t (P3 N) (Q3 N)))
Right3 : forall X P2, oneb S (up X) P2 ->
           (exists Q1, oneb Q (up X) Q1 /\
                (exists P3 Q3, nabla x, refl_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                     bisim_up_to refl_t (P3 x) (Q3 x)))
Right4 : forall L Q1, one Q L Q1 ->
           (exists P2, one S L P2 /\
                (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\
                     bisim_up_to refl_t P3 Q3))
Right5 : forall X Q1, oneb Q (dn X) Q1 ->
           (exists P2, oneb S (dn X) P2 /\
                (exists P3 Q3, forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                     bisim_up_to refl_t (P3 N) (Q3 N)))
Right6 : forall X Q1, oneb Q (up X) Q1 ->
           (exists P2, oneb S (up X) P2 /\
                (exists P3 Q3, nabla x, refl_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                     bisim_up_to refl_t (P3 x) (Q3 x)))
Sstep : oneb S (dn X) P2
Sstep1 : forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
============================
 exists P1, oneb P (dn X) P1 /\
   (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
        bisim_up_to refl_t (P2 N) (Q2 N) +)

1 other subgoal.

bisim_sound_fst < clear Right1 Right2 Right3 Right4 Right5 Right6.
Subgoal 5:

Variables: P Q R S X 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
Sstep : oneb S (dn X) P2
Sstep1 : forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
============================
 exists P1, oneb P (dn X) P1 /\
   (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
        bisim_up_to refl_t (P2 N) (Q2 N) +)

1 other subgoal.

bisim_sound_fst < Middle1 : case Middle.
Subgoal 5:

Variables: P Q R S X 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
Sstep : oneb S (dn X) P2
Sstep1 : forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Middle1 : forall L P2, one R L P2 ->
            (exists Q1, one S L Q1 /\
                 (exists P3 Q3, bisim_t P2 P3 Q1 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle2 : forall X P2, oneb R (dn X) P2 ->
            (exists Q1, oneb S (dn X) Q1 /\
                 (exists P3 Q3, forall N, bisim_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle3 : forall X P2, oneb R (up X) P2 ->
            (exists Q1, oneb S (up X) Q1 /\
                 (exists P3 Q3, nabla x, bisim_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
Middle4 : forall L Q1, one S L Q1 ->
            (exists P2, one R L P2 /\
                 (exists P3 Q3, bisim_t P2 P3 Q1 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle5 : forall X Q1, oneb S (dn X) Q1 ->
            (exists P2, oneb R (dn X) P2 /\
                 (exists P3 Q3, forall N, bisim_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle6 : forall X Q1, oneb S (up X) Q1 ->
            (exists P2, oneb R (up X) P2 /\
                 (exists P3 Q3, nabla x, bisim_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
============================
 exists P1, oneb P (dn X) P1 /\
   (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
        bisim_up_to refl_t (P2 N) (Q2 N) +)

1 other subgoal.

bisim_sound_fst < Rstep : apply Middle5 to *Sstep.
Subgoal 5:

Variables: P Q R S X 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
Sstep1 : forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Middle1 : forall L P2, one R L P2 ->
            (exists Q1, one S L Q1 /\
                 (exists P3 Q3, bisim_t P2 P3 Q1 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle2 : forall X P2, oneb R (dn X) P2 ->
            (exists Q1, oneb S (dn X) Q1 /\
                 (exists P3 Q3, forall N, bisim_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle3 : forall X P2, oneb R (up X) P2 ->
            (exists Q1, oneb S (up X) Q1 /\
                 (exists P3 Q3, nabla x, bisim_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
Middle4 : forall L Q1, one S L Q1 ->
            (exists P2, one R L P2 /\
                 (exists P3 Q3, bisim_t P2 P3 Q1 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle5 : forall X Q1, oneb S (dn X) Q1 ->
            (exists P2, oneb R (dn X) P2 /\
                 (exists P3 Q3, forall N, bisim_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle6 : forall X Q1, oneb S (up X) Q1 ->
            (exists P2, oneb R (up X) P2 /\
                 (exists P3 Q3, nabla x, bisim_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
Rstep : oneb R (dn X) P1
Rstep1 : forall N, bisim_t (P1 N) (P4 N) (P2 N) (Q2 N) /\
           bisim_up_to bisim_t (P4 N) (Q2 N)
============================
 exists P1, oneb P (dn X) P1 /\
   (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
        bisim_up_to refl_t (P2 N) (Q2 N) +)

1 other subgoal.

bisim_sound_fst < clear Middle1 Middle2 Middle3 Middle4 Middle5 Middle6.
Subgoal 5:

Variables: P Q R S X 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
Sstep1 : forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Rstep : oneb R (dn X) P1
Rstep1 : forall N, bisim_t (P1 N) (P4 N) (P2 N) (Q2 N) /\
           bisim_up_to bisim_t (P4 N) (Q2 N)
============================
 exists P1, oneb P (dn X) P1 /\
   (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
        bisim_up_to refl_t (P2 N) (Q2 N) +)

1 other subgoal.

bisim_sound_fst < Left1 : case Left.
Subgoal 5:

Variables: P Q R S X 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 +
Sstep1 : forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Rstep : oneb R (dn X) P1
Rstep1 : forall N, bisim_t (P1 N) (P4 N) (P2 N) (Q2 N) /\
           bisim_up_to bisim_t (P4 N) (Q2 N)
Left1 : forall L P1, one P L P1 ->
          (exists Q1, one R L Q1 /\
               (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
Left2 : forall X P1, oneb P (dn X) P1 ->
          (exists Q1, oneb R (dn X) Q1 /\
               (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                    bisim_up_to refl_t (P2 N) (Q2 N)))
Left3 : forall X P1, oneb P (up X) P1 ->
          (exists Q1, oneb R (up X) Q1 /\
               (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                    bisim_up_to refl_t (P2 x) (Q2 x)))
Left4 : forall L Q1, one R L Q1 ->
          (exists P1, one P L P1 /\
               (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
Left5 : forall X Q1, oneb R (dn X) Q1 ->
          (exists P1, oneb P (dn X) P1 /\
               (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                    bisim_up_to refl_t (P2 N) (Q2 N)))
Left6 : forall X Q1, oneb R (up X) Q1 ->
          (exists P1, oneb P (up X) P1 /\
               (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                    bisim_up_to refl_t (P2 x) (Q2 x)))
============================
 exists P1, oneb P (dn X) P1 /\
   (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
        bisim_up_to refl_t (P2 N) (Q2 N) +)

1 other subgoal.

bisim_sound_fst < Pstep : apply Left5 to *Rstep.
Subgoal 5:

Variables: P Q R S X 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 +
Sstep1 : forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Rstep1 : forall N, bisim_t (P1 N) (P4 N) (P2 N) (Q2 N) /\
           bisim_up_to bisim_t (P4 N) (Q2 N)
Left1 : forall L P1, one P L P1 ->
          (exists Q1, one R L Q1 /\
               (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
Left2 : forall X P1, oneb P (dn X) P1 ->
          (exists Q1, oneb R (dn X) Q1 /\
               (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                    bisim_up_to refl_t (P2 N) (Q2 N)))
Left3 : forall X P1, oneb P (up X) P1 ->
          (exists Q1, oneb R (up X) Q1 /\
               (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                    bisim_up_to refl_t (P2 x) (Q2 x)))
Left4 : forall L Q1, one R L Q1 ->
          (exists P1, one P L P1 /\
               (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
Left5 : forall X Q1, oneb R (dn X) Q1 ->
          (exists P1, oneb P (dn X) P1 /\
               (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                    bisim_up_to refl_t (P2 N) (Q2 N)))
Left6 : forall X Q1, oneb R (up X) Q1 ->
          (exists P1, oneb P (up X) P1 /\
               (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                    bisim_up_to refl_t (P2 x) (Q2 x)))
Pstep : oneb P (dn X) P5
Pstep1 : forall N, refl_t (P5 N) (P6 N) (P1 N) (Q4 N) /\
           bisim_up_to refl_t (P6 N) (Q4 N)
============================
 exists P1, oneb P (dn X) P1 /\
   (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
        bisim_up_to refl_t (P2 N) (Q2 N) +)

1 other subgoal.

bisim_sound_fst < clear Left1 Left2 Left3 Left4 Left5 Left6.
Subgoal 5:

Variables: P Q R S X 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 +
Sstep1 : forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Rstep1 : forall N, bisim_t (P1 N) (P4 N) (P2 N) (Q2 N) /\
           bisim_up_to bisim_t (P4 N) (Q2 N)
Pstep : oneb P (dn X) P5
Pstep1 : forall N, refl_t (P5 N) (P6 N) (P1 N) (Q4 N) /\
           bisim_up_to refl_t (P6 N) (Q4 N)
============================
 exists P1, oneb P (dn X) P1 /\
   (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
        bisim_up_to refl_t (P2 N) (Q2 N) +)

1 other subgoal.

bisim_sound_fst < witness P5.
Subgoal 5:

Variables: P Q R S X 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 +
Sstep1 : forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Rstep1 : forall N, bisim_t (P1 N) (P4 N) (P2 N) (Q2 N) /\
           bisim_up_to bisim_t (P4 N) (Q2 N)
Pstep : oneb P (dn X) P5
Pstep1 : forall N, refl_t (P5 N) (P6 N) (P1 N) (Q4 N) /\
           bisim_up_to refl_t (P6 N) (Q4 N)
============================
 oneb P (dn X) P5 /\
   (exists P2 Q2, forall N, refl_t (P5 N) (P2 N) (Q1 N) (Q2 N) /\
        bisim_up_to refl_t (P2 N) (Q2 N) +)

1 other subgoal.

bisim_sound_fst < split.
Subgoal 5.1:

Variables: P Q R S X 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 +
Sstep1 : forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Rstep1 : forall N, bisim_t (P1 N) (P4 N) (P2 N) (Q2 N) /\
           bisim_up_to bisim_t (P4 N) (Q2 N)
Pstep : oneb P (dn X) P5
Pstep1 : forall N, refl_t (P5 N) (P6 N) (P1 N) (Q4 N) /\
           bisim_up_to refl_t (P6 N) (Q4 N)
============================
 oneb P (dn X) P5

2 other subgoals.

bisim_sound_fst < search.
Subgoal 5.2:

Variables: P Q R S X 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 +
Sstep1 : forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Rstep1 : forall N, bisim_t (P1 N) (P4 N) (P2 N) (Q2 N) /\
           bisim_up_to bisim_t (P4 N) (Q2 N)
Pstep : oneb P (dn X) P5
Pstep1 : forall N, refl_t (P5 N) (P6 N) (P1 N) (Q4 N) /\
           bisim_up_to refl_t (P6 N) (Q4 N)
============================
 exists P2 Q2, forall N, refl_t (P5 N) (P2 N) (Q1 N) (Q2 N) /\
   bisim_up_to refl_t (P2 N) (Q2 N) +

1 other subgoal.

bisim_sound_fst < clear Pstep.
Subgoal 5.2:

Variables: P Q R S X 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 +
Sstep1 : forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Rstep1 : forall N, bisim_t (P1 N) (P4 N) (P2 N) (Q2 N) /\
           bisim_up_to bisim_t (P4 N) (Q2 N)
Pstep1 : forall N, refl_t (P5 N) (P6 N) (P1 N) (Q4 N) /\
           bisim_up_to refl_t (P6 N) (Q4 N)
============================
 exists P2 Q2, forall N, refl_t (P5 N) (P2 N) (Q1 N) (Q2 N) /\
   bisim_up_to refl_t (P2 N) (Q2 N) +

1 other subgoal.

bisim_sound_fst < witness P5.
Subgoal 5.2:

Variables: P Q R S X 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 +
Sstep1 : forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Rstep1 : forall N, bisim_t (P1 N) (P4 N) (P2 N) (Q2 N) /\
           bisim_up_to bisim_t (P4 N) (Q2 N)
Pstep1 : forall N, refl_t (P5 N) (P6 N) (P1 N) (Q4 N) /\
           bisim_up_to refl_t (P6 N) (Q4 N)
============================
 exists Q2, forall N, refl_t (P5 N) (P5 N) (Q1 N) (Q2 N) /\
   bisim_up_to refl_t (P5 N) (Q2 N) +

1 other subgoal.

bisim_sound_fst < witness Q1.
Subgoal 5.2:

Variables: P Q R S X 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 +
Sstep1 : forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Rstep1 : forall N, bisim_t (P1 N) (P4 N) (P2 N) (Q2 N) /\
           bisim_up_to bisim_t (P4 N) (Q2 N)
Pstep1 : forall N, refl_t (P5 N) (P6 N) (P1 N) (Q4 N) /\
           bisim_up_to refl_t (P6 N) (Q4 N)
============================
 forall N, refl_t (P5 N) (P5 N) (Q1 N) (Q1 N) /\
   bisim_up_to refl_t (P5 N) (Q1 N) +

1 other subgoal.

bisim_sound_fst < intros.
Subgoal 5.2:

Variables: P Q R S X Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4 N
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 +
Sstep1 : forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Rstep1 : forall N, bisim_t (P1 N) (P4 N) (P2 N) (Q2 N) /\
           bisim_up_to bisim_t (P4 N) (Q2 N)
Pstep1 : forall N, refl_t (P5 N) (P6 N) (P1 N) (Q4 N) /\
           bisim_up_to refl_t (P6 N) (Q4 N)
============================
 refl_t (P5 N) (P5 N) (Q1 N) (Q1 N) /\ bisim_up_to refl_t (P5 N) (Q1 N) +

1 other subgoal.

bisim_sound_fst < split.
Subgoal 5.2.1:

Variables: P Q R S X Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4 N
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 +
Sstep1 : forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Rstep1 : forall N, bisim_t (P1 N) (P4 N) (P2 N) (Q2 N) /\
           bisim_up_to bisim_t (P4 N) (Q2 N)
Pstep1 : forall N, refl_t (P5 N) (P6 N) (P1 N) (Q4 N) /\
           bisim_up_to refl_t (P6 N) (Q4 N)
============================
 refl_t (P5 N) (P5 N) (Q1 N) (Q1 N)

2 other subgoals.

bisim_sound_fst < search.
Subgoal 5.2.2:

Variables: P Q R S X Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4 N
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 +
Sstep1 : forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
           bisim_up_to refl_t (P3 N) (Q3 N)
Rstep1 : forall N, bisim_t (P1 N) (P4 N) (P2 N) (Q2 N) /\
           bisim_up_to bisim_t (P4 N) (Q2 N)
Pstep1 : forall N, refl_t (P5 N) (P6 N) (P1 N) (Q4 N) /\
           bisim_up_to refl_t (P6 N) (Q4 N)
============================
 bisim_up_to refl_t (P5 N) (Q1 N) +

1 other subgoal.

bisim_sound_fst < After : apply *Sstep1 with N = N.
Subgoal 5.2.2:

Variables: P Q R S X Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4 N
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 +
Rstep1 : forall N, bisim_t (P1 N) (P4 N) (P2 N) (Q2 N) /\
           bisim_up_to bisim_t (P4 N) (Q2 N)
Pstep1 : forall N, refl_t (P5 N) (P6 N) (P1 N) (Q4 N) /\
           bisim_up_to refl_t (P6 N) (Q4 N)
After : refl_t (P2 N) (P3 N) (Q1 N) (Q3 N)
After1 : bisim_up_to refl_t (P3 N) (Q3 N)
============================
 bisim_up_to refl_t (P5 N) (Q1 N) +

1 other subgoal.

bisim_sound_fst < Eq1 : case After.
Subgoal 5.2.2:

Variables: P Q R S X Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4 N
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 +
Rstep1 : forall N, bisim_t (P1 N) (P4 N) (P2 N) (Q2 N) /\
           bisim_up_to bisim_t (P4 N) (Q2 N)
Pstep1 : forall N, refl_t (P5 N) (P6 N) (P1 N) (Q4 N) /\
           bisim_up_to refl_t (P6 N) (Q4 N)
After1 : bisim_up_to refl_t (P3 N) (Q3 N)
Eq1 : Q1 N = Q3 N
Eq2 : P2 N = P3 N
============================
 bisim_up_to refl_t (P5 N) (Q1 N) +

1 other subgoal.

bisim_sound_fst < Link : apply *Rstep1 with N = N.
Subgoal 5.2.2:

Variables: P Q R S X Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4 N
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 +
Pstep1 : forall N, refl_t (P5 N) (P6 N) (P1 N) (Q4 N) /\
           bisim_up_to refl_t (P6 N) (Q4 N)
After1 : bisim_up_to refl_t (P3 N) (Q3 N)
Eq1 : Q1 N = Q3 N
Eq2 : P2 N = P3 N
Link : bisim_t (P1 N) (P4 N) (P2 N) (Q2 N)
Link1 : bisim_up_to bisim_t (P4 N) (Q2 N)
============================
 bisim_up_to refl_t (P5 N) (Q1 N) +

1 other subgoal.

bisim_sound_fst < Bis1 : case Link.
Subgoal 5.2.2:

Variables: P Q R S X Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4 N
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 +
Pstep1 : forall N, refl_t (P5 N) (P6 N) (P1 N) (Q4 N) /\
           bisim_up_to refl_t (P6 N) (Q4 N)
After1 : bisim_up_to refl_t (P3 N) (Q3 N)
Eq1 : Q1 N = Q3 N
Eq2 : P2 N = P3 N
Link1 : bisim_up_to bisim_t (P4 N) (Q2 N)
Bis1 : bisim_up_to refl_t (P1 N) (P4 N)
Bis2 : bisim_up_to refl_t (P2 N) (Q2 N)
============================
 bisim_up_to refl_t (P5 N) (Q1 N) +

1 other subgoal.

bisim_sound_fst < Before : apply *Pstep1 with N = N.
Subgoal 5.2.2:

Variables: P Q R S X Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4 N
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 +
After1 : bisim_up_to refl_t (P3 N) (Q3 N)
Eq1 : Q1 N = Q3 N
Eq2 : P2 N = P3 N
Link1 : bisim_up_to bisim_t (P4 N) (Q2 N)
Bis1 : bisim_up_to refl_t (P1 N) (P4 N)
Bis2 : bisim_up_to refl_t (P2 N) (Q2 N)
Before : refl_t (P5 N) (P6 N) (P1 N) (Q4 N)
Before1 : bisim_up_to refl_t (P6 N) (Q4 N)
============================
 bisim_up_to refl_t (P5 N) (Q1 N) +

1 other subgoal.

bisim_sound_fst < Eq1 : case Before.
Subgoal 5.2.2:

Variables: P Q R S X Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4 N
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 +
After1 : bisim_up_to refl_t (P3 N) (Q3 N)
Eq1 : Q1 N = Q3 N
Eq2 : P2 N = P3 N
Link1 : bisim_up_to bisim_t (P4 N) (Q2 N)
Bis1 : bisim_up_to refl_t (P1 N) (P4 N)
Bis2 : bisim_up_to refl_t (P2 N) (Q2 N)
Before1 : bisim_up_to refl_t (P6 N) (Q4 N)
Eq3 : P1 N = Q4 N
Eq4 : P5 N = P6 N
============================
 bisim_up_to refl_t (P5 N) (Q1 N) +

1 other subgoal.

bisim_sound_fst < Before : apply bisim_eq_1R to *Before1 *Eq4.
Subgoal 5.2.2:

Variables: P Q R S X Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4 N
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 +
After1 : bisim_up_to refl_t (P3 N) (Q3 N)
Eq1 : Q1 N = Q3 N
Eq2 : P2 N = P3 N
Link1 : bisim_up_to bisim_t (P4 N) (Q2 N)
Bis1 : bisim_up_to refl_t (P1 N) (P4 N)
Bis2 : bisim_up_to refl_t (P2 N) (Q2 N)
Eq3 : P1 N = Q4 N
Before : bisim_up_to refl_t (P5 N) (Q4 N)
============================
 bisim_up_to refl_t (P5 N) (Q1 N) +

1 other subgoal.

bisim_sound_fst < Before : apply bisim_eq_2R to *Before *Eq3.
Subgoal 5.2.2:

Variables: P Q R S X Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4 N
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 +
After1 : bisim_up_to refl_t (P3 N) (Q3 N)
Eq1 : Q1 N = Q3 N
Eq2 : P2 N = P3 N
Link1 : bisim_up_to bisim_t (P4 N) (Q2 N)
Bis1 : bisim_up_to refl_t (P1 N) (P4 N)
Bis2 : bisim_up_to refl_t (P2 N) (Q2 N)
Before : bisim_up_to refl_t (P5 N) (P1 N)
============================
 bisim_up_to refl_t (P5 N) (Q1 N) +

1 other subgoal.

bisim_sound_fst < Before : apply bisim_transitive to *Before *Bis1.
Subgoal 5.2.2:

Variables: P Q R S X Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4 N
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 +
After1 : bisim_up_to refl_t (P3 N) (Q3 N)
Eq1 : Q1 N = Q3 N
Eq2 : P2 N = P3 N
Link1 : bisim_up_to bisim_t (P4 N) (Q2 N)
Bis2 : bisim_up_to refl_t (P2 N) (Q2 N)
Before : bisim_up_to refl_t (P5 N) (P4 N)
============================
 bisim_up_to refl_t (P5 N) (Q1 N) +

1 other subgoal.

bisim_sound_fst < Bis2 : apply bisim_symmetric to *Bis2.
Subgoal 5.2.2:

Variables: P Q R S X Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4 N
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 +
After1 : bisim_up_to refl_t (P3 N) (Q3 N)
Eq1 : Q1 N = Q3 N
Eq2 : P2 N = P3 N
Link1 : bisim_up_to bisim_t (P4 N) (Q2 N)
Before : bisim_up_to refl_t (P5 N) (P4 N)
Bis2 : bisim_up_to refl_t (Q2 N) (P2 N)
============================
 bisim_up_to refl_t (P5 N) (Q1 N) +

1 other subgoal.

bisim_sound_fst < Bis2 : apply bisim_eq_2L to *Bis2 *Eq2.
Subgoal 5.2.2:

Variables: P Q R S X Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4 N
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 +
After1 : bisim_up_to refl_t (P3 N) (Q3 N)
Eq1 : Q1 N = Q3 N
Link1 : bisim_up_to bisim_t (P4 N) (Q2 N)
Before : bisim_up_to refl_t (P5 N) (P4 N)
Bis2 : bisim_up_to refl_t (Q2 N) (P3 N)
============================
 bisim_up_to refl_t (P5 N) (Q1 N) +

1 other subgoal.

bisim_sound_fst < After : apply bisim_eq_2R to *After1 *Eq1.
Subgoal 5.2.2:

Variables: P Q R S X Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4 N
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 +
Link1 : bisim_up_to bisim_t (P4 N) (Q2 N)
Before : bisim_up_to refl_t (P5 N) (P4 N)
Bis2 : bisim_up_to refl_t (Q2 N) (P3 N)
After : bisim_up_to refl_t (P3 N) (Q1 N)
============================
 bisim_up_to refl_t (P5 N) (Q1 N) +

1 other subgoal.

bisim_sound_fst < After : apply bisim_transitive to *Bis2 *After.
Subgoal 5.2.2:

Variables: P Q R S X Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4 N
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 +
Link1 : bisim_up_to bisim_t (P4 N) (Q2 N)
Before : bisim_up_to refl_t (P5 N) (P4 N)
After : bisim_up_to refl_t (Q2 N) (Q1 N)
============================
 bisim_up_to refl_t (P5 N) (Q1 N) +

1 other subgoal.

bisim_sound_fst < backchain CH.
Subgoal 6:

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 X Q1, oneb Q (up X) Q1 ->
   (exists P1, oneb P (up X) P1 /\
        (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
             bisim_up_to refl_t (P2 x) (Q2 x) +))

bisim_sound_fst < intros Qstep.
Subgoal 6:

Variables: P Q R S X 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 : oneb Q (up X) Q1
============================
 exists P1, oneb P (up X) P1 /\
   (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
        bisim_up_to refl_t (P2 x) (Q2 x) +)

bisim_sound_fst < Right1 : case Right.
Subgoal 6:

Variables: P Q R S X 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 : oneb Q (up X) Q1
Right1 : forall L P2, one S L P2 ->
           (exists Q1, one Q L Q1 /\
                (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\
                     bisim_up_to refl_t P3 Q3))
Right2 : forall X P2, oneb S (dn X) P2 ->
           (exists Q1, oneb Q (dn X) Q1 /\
                (exists P3 Q3, forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                     bisim_up_to refl_t (P3 N) (Q3 N)))
Right3 : forall X P2, oneb S (up X) P2 ->
           (exists Q1, oneb Q (up X) Q1 /\
                (exists P3 Q3, nabla x, refl_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                     bisim_up_to refl_t (P3 x) (Q3 x)))
Right4 : forall L Q1, one Q L Q1 ->
           (exists P2, one S L P2 /\
                (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\
                     bisim_up_to refl_t P3 Q3))
Right5 : forall X Q1, oneb Q (dn X) Q1 ->
           (exists P2, oneb S (dn X) P2 /\
                (exists P3 Q3, forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                     bisim_up_to refl_t (P3 N) (Q3 N)))
Right6 : forall X Q1, oneb Q (up X) Q1 ->
           (exists P2, oneb S (up X) P2 /\
                (exists P3 Q3, nabla x, refl_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                     bisim_up_to refl_t (P3 x) (Q3 x)))
============================
 exists P1, oneb P (up X) P1 /\
   (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
        bisim_up_to refl_t (P2 x) (Q2 x) +)

bisim_sound_fst < Sstep : apply Right6 to *Qstep.
Subgoal 6:

Variables: P Q R S X 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
Right1 : forall L P2, one S L P2 ->
           (exists Q1, one Q L Q1 /\
                (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\
                     bisim_up_to refl_t P3 Q3))
Right2 : forall X P2, oneb S (dn X) P2 ->
           (exists Q1, oneb Q (dn X) Q1 /\
                (exists P3 Q3, forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                     bisim_up_to refl_t (P3 N) (Q3 N)))
Right3 : forall X P2, oneb S (up X) P2 ->
           (exists Q1, oneb Q (up X) Q1 /\
                (exists P3 Q3, nabla x, refl_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                     bisim_up_to refl_t (P3 x) (Q3 x)))
Right4 : forall L Q1, one Q L Q1 ->
           (exists P2, one S L P2 /\
                (exists P3 Q3, refl_t P2 P3 Q1 Q3 /\
                     bisim_up_to refl_t P3 Q3))
Right5 : forall X Q1, oneb Q (dn X) Q1 ->
           (exists P2, oneb S (dn X) P2 /\
                (exists P3 Q3, forall N, refl_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                     bisim_up_to refl_t (P3 N) (Q3 N)))
Right6 : forall X Q1, oneb Q (up X) Q1 ->
           (exists P2, oneb S (up X) P2 /\
                (exists P3 Q3, nabla x, refl_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                     bisim_up_to refl_t (P3 x) (Q3 x)))
Sstep : oneb S (up X) P2
Sstep1 : refl_t (P2 n1) (P3 n1) (Q1 n1) (Q3 n1)
Sstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
============================
 exists P1, oneb P (up X) P1 /\
   (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
        bisim_up_to refl_t (P2 x) (Q2 x) +)

bisim_sound_fst < clear Right1 Right2 Right3 Right4 Right5 Right6.
Subgoal 6:

Variables: P Q R S X 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
Sstep : oneb S (up X) P2
Sstep1 : refl_t (P2 n1) (P3 n1) (Q1 n1) (Q3 n1)
Sstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
============================
 exists P1, oneb P (up X) P1 /\
   (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
        bisim_up_to refl_t (P2 x) (Q2 x) +)

bisim_sound_fst < Middle1 : case Middle.
Subgoal 6:

Variables: P Q R S X 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
Sstep : oneb S (up X) P2
Sstep1 : refl_t (P2 n1) (P3 n1) (Q1 n1) (Q3 n1)
Sstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Middle1 : forall L P2, one R L P2 ->
            (exists Q1, one S L Q1 /\
                 (exists P3 Q3, bisim_t P2 P3 Q1 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle2 : forall X P2, oneb R (dn X) P2 ->
            (exists Q1, oneb S (dn X) Q1 /\
                 (exists P3 Q3, forall N, bisim_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle3 : forall X P2, oneb R (up X) P2 ->
            (exists Q1, oneb S (up X) Q1 /\
                 (exists P3 Q3, nabla x, bisim_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
Middle4 : forall L Q1, one S L Q1 ->
            (exists P2, one R L P2 /\
                 (exists P3 Q3, bisim_t P2 P3 Q1 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle5 : forall X Q1, oneb S (dn X) Q1 ->
            (exists P2, oneb R (dn X) P2 /\
                 (exists P3 Q3, forall N, bisim_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle6 : forall X Q1, oneb S (up X) Q1 ->
            (exists P2, oneb R (up X) P2 /\
                 (exists P3 Q3, nabla x, bisim_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
============================
 exists P1, oneb P (up X) P1 /\
   (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
        bisim_up_to refl_t (P2 x) (Q2 x) +)

bisim_sound_fst < Rstep : apply Middle6 to *Sstep.
Subgoal 6:

Variables: P Q R S X 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
Sstep1 : refl_t (P2 n1) (P3 n1) (Q1 n1) (Q3 n1)
Sstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Middle1 : forall L P2, one R L P2 ->
            (exists Q1, one S L Q1 /\
                 (exists P3 Q3, bisim_t P2 P3 Q1 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle2 : forall X P2, oneb R (dn X) P2 ->
            (exists Q1, oneb S (dn X) Q1 /\
                 (exists P3 Q3, forall N, bisim_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle3 : forall X P2, oneb R (up X) P2 ->
            (exists Q1, oneb S (up X) Q1 /\
                 (exists P3 Q3, nabla x, bisim_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
Middle4 : forall L Q1, one S L Q1 ->
            (exists P2, one R L P2 /\
                 (exists P3 Q3, bisim_t P2 P3 Q1 Q3 /\
                      bisim_up_to bisim_t P3 Q3))
Middle5 : forall X Q1, oneb S (dn X) Q1 ->
            (exists P2, oneb R (dn X) P2 /\
                 (exists P3 Q3, forall N, bisim_t (P2 N) (P3 N) (Q1 N) (Q3 N) /\
                      bisim_up_to bisim_t (P3 N) (Q3 N)))
Middle6 : forall X Q1, oneb S (up X) Q1 ->
            (exists P2, oneb R (up X) P2 /\
                 (exists P3 Q3, nabla x, bisim_t (P2 x) (P3 x) (Q1 x) (Q3 x) /\
                      bisim_up_to bisim_t (P3 x) (Q3 x)))
Rstep : oneb R (up X) P1
Rstep1 : bisim_t (P1 n1) (P4 n1) (P2 n1) (Q2 n1)
Rstep2 : bisim_up_to bisim_t (P4 n1) (Q2 n1)
============================
 exists P1, oneb P (up X) P1 /\
   (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
        bisim_up_to refl_t (P2 x) (Q2 x) +)

bisim_sound_fst < clear Middle1 Middle2 Middle3 Middle4 Middle5 Middle6.
Subgoal 6:

Variables: P Q R S X 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
Sstep1 : refl_t (P2 n1) (P3 n1) (Q1 n1) (Q3 n1)
Sstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Rstep : oneb R (up X) P1
Rstep1 : bisim_t (P1 n1) (P4 n1) (P2 n1) (Q2 n1)
Rstep2 : bisim_up_to bisim_t (P4 n1) (Q2 n1)
============================
 exists P1, oneb P (up X) P1 /\
   (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
        bisim_up_to refl_t (P2 x) (Q2 x) +)

bisim_sound_fst < Left1 : case Left.
Subgoal 6:

Variables: P Q R S X 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 +
Sstep1 : refl_t (P2 n1) (P3 n1) (Q1 n1) (Q3 n1)
Sstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Rstep : oneb R (up X) P1
Rstep1 : bisim_t (P1 n1) (P4 n1) (P2 n1) (Q2 n1)
Rstep2 : bisim_up_to bisim_t (P4 n1) (Q2 n1)
Left1 : forall L P1, one P L P1 ->
          (exists Q1, one R L Q1 /\
               (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
Left2 : forall X P1, oneb P (dn X) P1 ->
          (exists Q1, oneb R (dn X) Q1 /\
               (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                    bisim_up_to refl_t (P2 N) (Q2 N)))
Left3 : forall X P1, oneb P (up X) P1 ->
          (exists Q1, oneb R (up X) Q1 /\
               (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                    bisim_up_to refl_t (P2 x) (Q2 x)))
Left4 : forall L Q1, one R L Q1 ->
          (exists P1, one P L P1 /\
               (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
Left5 : forall X Q1, oneb R (dn X) Q1 ->
          (exists P1, oneb P (dn X) P1 /\
               (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                    bisim_up_to refl_t (P2 N) (Q2 N)))
Left6 : forall X Q1, oneb R (up X) Q1 ->
          (exists P1, oneb P (up X) P1 /\
               (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                    bisim_up_to refl_t (P2 x) (Q2 x)))
============================
 exists P1, oneb P (up X) P1 /\
   (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
        bisim_up_to refl_t (P2 x) (Q2 x) +)

bisim_sound_fst < Pstep : apply Left6 to *Rstep.
Subgoal 6:

Variables: P Q R S X 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 +
Sstep1 : refl_t (P2 n1) (P3 n1) (Q1 n1) (Q3 n1)
Sstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Rstep1 : bisim_t (P1 n1) (P4 n1) (P2 n1) (Q2 n1)
Rstep2 : bisim_up_to bisim_t (P4 n1) (Q2 n1)
Left1 : forall L P1, one P L P1 ->
          (exists Q1, one R L Q1 /\
               (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
Left2 : forall X P1, oneb P (dn X) P1 ->
          (exists Q1, oneb R (dn X) Q1 /\
               (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                    bisim_up_to refl_t (P2 N) (Q2 N)))
Left3 : forall X P1, oneb P (up X) P1 ->
          (exists Q1, oneb R (up X) Q1 /\
               (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                    bisim_up_to refl_t (P2 x) (Q2 x)))
Left4 : forall L Q1, one R L Q1 ->
          (exists P1, one P L P1 /\
               (exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
Left5 : forall X Q1, oneb R (dn X) Q1 ->
          (exists P1, oneb P (dn X) P1 /\
               (exists P2 Q2, forall N, refl_t (P1 N) (P2 N) (Q1 N) (Q2 N) /\
                    bisim_up_to refl_t (P2 N) (Q2 N)))
Left6 : forall X Q1, oneb R (up X) Q1 ->
          (exists P1, oneb P (up X) P1 /\
               (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
                    bisim_up_to refl_t (P2 x) (Q2 x)))
Pstep : oneb P (up X) P5
Pstep1 : refl_t (P5 n1) (P6 n1) (P1 n1) (Q4 n1)
Pstep2 : bisim_up_to refl_t (P6 n1) (Q4 n1)
============================
 exists P1, oneb P (up X) P1 /\
   (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
        bisim_up_to refl_t (P2 x) (Q2 x) +)

bisim_sound_fst < clear Left1 Left2 Left3 Left4 Left5 Left6.
Subgoal 6:

Variables: P Q R S X 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 +
Sstep1 : refl_t (P2 n1) (P3 n1) (Q1 n1) (Q3 n1)
Sstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Rstep1 : bisim_t (P1 n1) (P4 n1) (P2 n1) (Q2 n1)
Rstep2 : bisim_up_to bisim_t (P4 n1) (Q2 n1)
Pstep : oneb P (up X) P5
Pstep1 : refl_t (P5 n1) (P6 n1) (P1 n1) (Q4 n1)
Pstep2 : bisim_up_to refl_t (P6 n1) (Q4 n1)
============================
 exists P1, oneb P (up X) P1 /\
   (exists P2 Q2, nabla x, refl_t (P1 x) (P2 x) (Q1 x) (Q2 x) /\
        bisim_up_to refl_t (P2 x) (Q2 x) +)

bisim_sound_fst < witness P5.
Subgoal 6:

Variables: P Q R S X 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 +
Sstep1 : refl_t (P2 n1) (P3 n1) (Q1 n1) (Q3 n1)
Sstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Rstep1 : bisim_t (P1 n1) (P4 n1) (P2 n1) (Q2 n1)
Rstep2 : bisim_up_to bisim_t (P4 n1) (Q2 n1)
Pstep : oneb P (up X) P5
Pstep1 : refl_t (P5 n1) (P6 n1) (P1 n1) (Q4 n1)
Pstep2 : bisim_up_to refl_t (P6 n1) (Q4 n1)
============================
 oneb P (up X) P5 /\
   (exists P2 Q2, nabla x, refl_t (P5 x) (P2 x) (Q1 x) (Q2 x) /\
        bisim_up_to refl_t (P2 x) (Q2 x) +)

bisim_sound_fst < split.
Subgoal 6.1:

Variables: P Q R S X 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 +
Sstep1 : refl_t (P2 n1) (P3 n1) (Q1 n1) (Q3 n1)
Sstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Rstep1 : bisim_t (P1 n1) (P4 n1) (P2 n1) (Q2 n1)
Rstep2 : bisim_up_to bisim_t (P4 n1) (Q2 n1)
Pstep : oneb P (up X) P5
Pstep1 : refl_t (P5 n1) (P6 n1) (P1 n1) (Q4 n1)
Pstep2 : bisim_up_to refl_t (P6 n1) (Q4 n1)
============================
 oneb P (up X) P5

1 other subgoal.

bisim_sound_fst < search.
Subgoal 6.2:

Variables: P Q R S X 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 +
Sstep1 : refl_t (P2 n1) (P3 n1) (Q1 n1) (Q3 n1)
Sstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Rstep1 : bisim_t (P1 n1) (P4 n1) (P2 n1) (Q2 n1)
Rstep2 : bisim_up_to bisim_t (P4 n1) (Q2 n1)
Pstep : oneb P (up X) P5
Pstep1 : refl_t (P5 n1) (P6 n1) (P1 n1) (Q4 n1)
Pstep2 : bisim_up_to refl_t (P6 n1) (Q4 n1)
============================
 exists P2 Q2, nabla x, refl_t (P5 x) (P2 x) (Q1 x) (Q2 x) /\
   bisim_up_to refl_t (P2 x) (Q2 x) +

bisim_sound_fst < clear Pstep.
Subgoal 6.2:

Variables: P Q R S X 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 +
Sstep1 : refl_t (P2 n1) (P3 n1) (Q1 n1) (Q3 n1)
Sstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Rstep1 : bisim_t (P1 n1) (P4 n1) (P2 n1) (Q2 n1)
Rstep2 : bisim_up_to bisim_t (P4 n1) (Q2 n1)
Pstep1 : refl_t (P5 n1) (P6 n1) (P1 n1) (Q4 n1)
Pstep2 : bisim_up_to refl_t (P6 n1) (Q4 n1)
============================
 exists P2 Q2, nabla x, refl_t (P5 x) (P2 x) (Q1 x) (Q2 x) /\
   bisim_up_to refl_t (P2 x) (Q2 x) +

bisim_sound_fst < witness P5.
Subgoal 6.2:

Variables: P Q R S X 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 +
Sstep1 : refl_t (P2 n1) (P3 n1) (Q1 n1) (Q3 n1)
Sstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Rstep1 : bisim_t (P1 n1) (P4 n1) (P2 n1) (Q2 n1)
Rstep2 : bisim_up_to bisim_t (P4 n1) (Q2 n1)
Pstep1 : refl_t (P5 n1) (P6 n1) (P1 n1) (Q4 n1)
Pstep2 : bisim_up_to refl_t (P6 n1) (Q4 n1)
============================
 exists Q2, nabla x, refl_t (P5 x) (P5 x) (Q1 x) (Q2 x) /\
   bisim_up_to refl_t (P5 x) (Q2 x) +

bisim_sound_fst < witness Q1.
Subgoal 6.2:

Variables: P Q R S X 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 +
Sstep1 : refl_t (P2 n1) (P3 n1) (Q1 n1) (Q3 n1)
Sstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Rstep1 : bisim_t (P1 n1) (P4 n1) (P2 n1) (Q2 n1)
Rstep2 : bisim_up_to bisim_t (P4 n1) (Q2 n1)
Pstep1 : refl_t (P5 n1) (P6 n1) (P1 n1) (Q4 n1)
Pstep2 : bisim_up_to refl_t (P6 n1) (Q4 n1)
============================
 nabla x, refl_t (P5 x) (P5 x) (Q1 x) (Q1 x) /\
   bisim_up_to refl_t (P5 x) (Q1 x) +

bisim_sound_fst < intros.
Subgoal 6.2:

Variables: P Q R S X 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 +
Sstep1 : refl_t (P2 n1) (P3 n1) (Q1 n1) (Q3 n1)
Sstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Rstep1 : bisim_t (P1 n1) (P4 n1) (P2 n1) (Q2 n1)
Rstep2 : bisim_up_to bisim_t (P4 n1) (Q2 n1)
Pstep1 : refl_t (P5 n1) (P6 n1) (P1 n1) (Q4 n1)
Pstep2 : bisim_up_to refl_t (P6 n1) (Q4 n1)
============================
 refl_t (P5 n1) (P5 n1) (Q1 n1) (Q1 n1) /\
   bisim_up_to refl_t (P5 n1) (Q1 n1) +

bisim_sound_fst < split.
Subgoal 6.2.1:

Variables: P Q R S X 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 +
Sstep1 : refl_t (P2 n1) (P3 n1) (Q1 n1) (Q3 n1)
Sstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Rstep1 : bisim_t (P1 n1) (P4 n1) (P2 n1) (Q2 n1)
Rstep2 : bisim_up_to bisim_t (P4 n1) (Q2 n1)
Pstep1 : refl_t (P5 n1) (P6 n1) (P1 n1) (Q4 n1)
Pstep2 : bisim_up_to refl_t (P6 n1) (Q4 n1)
============================
 refl_t (P5 n1) (P5 n1) (Q1 n1) (Q1 n1)

1 other subgoal.

bisim_sound_fst < search.
Subgoal 6.2.2:

Variables: P Q R S X 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 +
Sstep1 : refl_t (P2 n1) (P3 n1) (Q1 n1) (Q3 n1)
Sstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Rstep1 : bisim_t (P1 n1) (P4 n1) (P2 n1) (Q2 n1)
Rstep2 : bisim_up_to bisim_t (P4 n1) (Q2 n1)
Pstep1 : refl_t (P5 n1) (P6 n1) (P1 n1) (Q4 n1)
Pstep2 : bisim_up_to refl_t (P6 n1) (Q4 n1)
============================
 bisim_up_to refl_t (P5 n1) (Q1 n1) +

bisim_sound_fst < case Sstep1.
Subgoal 6.2.2:

Variables: P Q R S X 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 +
Sstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Rstep1 : bisim_t (P1 n1) (P4 n1) (P3 n1) (Q2 n1)
Rstep2 : bisim_up_to bisim_t (P4 n1) (Q2 n1)
Pstep1 : refl_t (P5 n1) (P6 n1) (P1 n1) (Q4 n1)
Pstep2 : bisim_up_to refl_t (P6 n1) (Q4 n1)
============================
 bisim_up_to refl_t (P5 n1) (Q3 n1) +

bisim_sound_fst < case Pstep1.
Subgoal 6.2.2:

Variables: P Q R S X 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 +
Sstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Rstep1 : bisim_t (Q4 n1) (P4 n1) (P3 n1) (Q2 n1)
Rstep2 : bisim_up_to bisim_t (P4 n1) (Q2 n1)
Pstep2 : bisim_up_to refl_t (P6 n1) (Q4 n1)
============================
 bisim_up_to refl_t (P6 n1) (Q3 n1) +

bisim_sound_fst < Tech1 : case Rstep1.
Subgoal 6.2.2:

Variables: P Q R S X 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 +
Sstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Rstep2 : bisim_up_to bisim_t (P4 n1) (Q2 n1)
Pstep2 : bisim_up_to refl_t (P6 n1) (Q4 n1)
Tech1 : bisim_up_to refl_t (Q4 n1) (P4 n1)
Tech2 : bisim_up_to refl_t (P3 n1) (Q2 n1)
============================
 bisim_up_to refl_t (P6 n1) (Q3 n1) +

bisim_sound_fst < Before : apply bisim_transitive to *Pstep2 *Tech1.
Subgoal 6.2.2:

Variables: P Q R S X 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 +
Sstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Rstep2 : bisim_up_to bisim_t (P4 n1) (Q2 n1)
Tech2 : bisim_up_to refl_t (P3 n1) (Q2 n1)
Before : bisim_up_to refl_t (P6 n1) (P4 n1)
============================
 bisim_up_to refl_t (P6 n1) (Q3 n1) +

bisim_sound_fst < Tech2 : apply bisim_symmetric to *Tech2.
Subgoal 6.2.2:

Variables: P Q R S X 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 +
Sstep2 : bisim_up_to refl_t (P3 n1) (Q3 n1)
Rstep2 : bisim_up_to bisim_t (P4 n1) (Q2 n1)
Before : bisim_up_to refl_t (P6 n1) (P4 n1)
Tech2 : bisim_up_to refl_t (Q2 n1) (P3 n1)
============================
 bisim_up_to refl_t (P6 n1) (Q3 n1) +

bisim_sound_fst < After : apply bisim_transitive to *Tech2 *Sstep2.
Subgoal 6.2.2:

Variables: P Q R S X 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 +
Rstep2 : bisim_up_to bisim_t (P4 n1) (Q2 n1)
Before : bisim_up_to refl_t (P6 n1) (P4 n1)
After : bisim_up_to refl_t (Q2 n1) (Q3 n1)
============================
 bisim_up_to refl_t (P6 n1) (Q3 n1) +

bisim_sound_fst < backchain 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

2 other subgoals.

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

1 other subgoal.

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 < Fst : apply bisim_sound_fst.

Fst : is_sound_fst bisim_t
============================
 is_sound bisim_t

bisim_sound < Fst : case Fst.

Fst : 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
============================
 is_sound bisim_t

bisim_sound < Snd : apply bisim_sound_snd.

Fst : 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
Snd : is_sound_snd bisim_t
============================
 is_sound bisim_t

bisim_sound < Snd : case Snd.

Fst : 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
Snd : 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)
============================
 is_sound bisim_t

bisim_sound < unfold.

Fst : 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
Snd : 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)
============================
 forall P Q, bisim_up_to bisim_t P Q -> bisim_up_to refl_t P Q

bisim_sound < intros PQ.

Variables: P Q
Fst : 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
Snd : 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)
PQ : bisim_up_to bisim_t P Q
============================
 bisim_up_to refl_t P Q

bisim_sound < apply *Snd to *PQ.

Variables: P Q R S
Fst : 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 : bisim_up_to refl_t P R
H2 : bisim_up_to bisim_t R S
H3 : bisim_up_to refl_t S Q
============================
 bisim_up_to refl_t P Q

bisim_sound < backchain Fst.
Proof completed.
Abella <