Welcome to Abella 2.0.3-dev
Abella < Kind name, action, proc type.
Abella < Import "ccs_core".
Importing from ccs_core
Warning: Definition can be used to defeat stratification
(higher-order argument "Tech" occurs to the left of ->)
Warning: Definition can be used to defeat stratification
(higher-order argument "Rel" occurs to the left of ->)
Warning: Definition can be used to defeat stratification
(higher-order argument "Rel" occurs to the left of ->)
Abella < Define bisim_t : proc -> proc -> proc -> proc -> prop by
bisim_t P1 P2 Q1 Q2 := bisim_up_to refl_t P1 P2 /\ bisim_up_to refl_t Q1 Q2.
Abella < Define is_sound_fst : (proc -> proc -> proc -> proc -> prop) -> prop by
is_sound_fst Tech := forall P Q, (exists R S, bisim_up_to refl_t P R /\ bisim_up_to Tech R S /\
bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q.
Warning: Definition can be used to defeat stratification
(higher-order argument "Tech" occurs to the left of ->)
Abella < Define is_sound_snd : (proc -> proc -> proc -> proc -> prop) -> prop by
is_sound_snd Tech := forall P Q, bisim_up_to Tech P Q ->
(exists R S, bisim_up_to refl_t P R /\ bisim_up_to Tech R S /\
bisim_up_to refl_t S Q).
Warning: Definition can be used to defeat stratification
(higher-order argument "Tech" occurs to the left of ->)
Abella < Theorem bisim_t_reflexive :
forall P, bisim_t P P P P.
============================
forall P, bisim_t P P P P
bisim_t_reflexive < intros.
Variables: P
============================
bisim_t P P P P
bisim_t_reflexive < unfold.
Subgoal 1:
Variables: P
============================
bisim_up_to refl_t P P
Subgoal 2 is:
bisim_up_to refl_t P P
bisim_t_reflexive < backchain bisim_reflexive_.
Subgoal 2:
Variables: P
============================
bisim_up_to refl_t P P
bisim_t_reflexive < backchain bisim_reflexive_.
Proof completed.
Abella < Theorem bisim_sound_fst :
is_sound_fst bisim_t.
============================
is_sound_fst bisim_t
bisim_sound_fst < unfold.
============================
forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q
bisim_sound_fst < coinduction.
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
============================
forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q #
bisim_sound_fst < intros.
Variables: P Q
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
H1 : exists R S, bisim_up_to refl_t P R /\ bisim_up_to bisim_t R S /\
bisim_up_to refl_t S Q
============================
bisim_up_to refl_t P Q #
bisim_sound_fst < case H1.
Variables: P Q R S
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
H2 : bisim_up_to refl_t P R
H3 : bisim_up_to bisim_t R S
H4 : bisim_up_to refl_t S Q
============================
bisim_up_to refl_t P Q #
bisim_sound_fst < rename H2 to Left.
Variables: P Q R S
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
H3 : bisim_up_to bisim_t R S
H4 : bisim_up_to refl_t S Q
============================
bisim_up_to refl_t P Q #
bisim_sound_fst < rename H3 to Middle.
Variables: P Q R S
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Middle : bisim_up_to bisim_t R S
H4 : bisim_up_to refl_t S Q
============================
bisim_up_to refl_t P Q #
bisim_sound_fst < rename H4 to Right.
Variables: P Q R S
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Middle : bisim_up_to bisim_t R S
Right : bisim_up_to refl_t S Q
============================
bisim_up_to refl_t P Q #
bisim_sound_fst < unfold.
Subgoal 1:
Variables: P Q R S
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Middle : bisim_up_to bisim_t R S
Right : bisim_up_to refl_t S Q
============================
forall A P1, one P A P1 ->
(exists Q1, one Q A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < intros Pstep.
Subgoal 1:
Variables: P Q R S A P1
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Middle : bisim_up_to bisim_t R S
Right : bisim_up_to refl_t S Q
Pstep : one P A P1
============================
exists Q1, one Q A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < Left : case Left.
Subgoal 1:
Variables: P Q R S A P1
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Middle : bisim_up_to bisim_t R S
Right : bisim_up_to refl_t S Q
Pstep : one P A P1
Left : forall A P1, one P A P1 ->
(exists Q2, one R A Q2 /\
(exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
Left1 : forall A Q2, one R A Q2 ->
(exists P1, one P A P1 /\
(exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
============================
exists Q1, one Q A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < clear Left1.
Subgoal 1:
Variables: P Q R S A P1
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Middle : bisim_up_to bisim_t R S
Right : bisim_up_to refl_t S Q
Pstep : one P A P1
Left : forall A P1, one P A P1 ->
(exists Q2, one R A Q2 /\
(exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
============================
exists Q1, one Q A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < Left : apply Left to Pstep.
Subgoal 1:
Variables: P Q R S A P1 Q2 P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Middle : bisim_up_to bisim_t R S
Right : bisim_up_to refl_t S Q
Pstep : one P A P1
Left : forall A P1, one P A P1 ->
(exists Q2, one R A Q2 /\
(exists P3 Q3, refl_t P1 P3 Q2 Q3 /\ bisim_up_to refl_t P3 Q3))
Left1 : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
============================
exists Q1, one Q A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < clear Left.
Subgoal 1:
Variables: P Q R S A P1 Q2 P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Middle : bisim_up_to bisim_t R S
Right : bisim_up_to refl_t S Q
Pstep : one P A P1
Left1 : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
============================
exists Q1, one Q A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < rename Left1 to PPstep.
Subgoal 1:
Variables: P Q R S A P1 Q2 P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Middle : bisim_up_to bisim_t R S
Right : bisim_up_to refl_t S Q
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
============================
exists Q1, one Q A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < Middle : case Middle.
Subgoal 1:
Variables: P Q R S A P1 Q2 P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Right : bisim_up_to refl_t S Q
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
Middle : forall A P1, one R A P1 ->
(exists Q2, one S A Q2 /\
(exists P3 Q3, bisim_t P1 P3 Q2 Q3 /\
bisim_up_to bisim_t P3 Q3))
Middle1 : forall A Q2, one S A Q2 ->
(exists P1, one R A P1 /\
(exists P3 Q3, bisim_t P1 P3 Q2 Q3 /\
bisim_up_to bisim_t P3 Q3))
============================
exists Q1, one Q A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < clear Middle1.
Subgoal 1:
Variables: P Q R S A P1 Q2 P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Right : bisim_up_to refl_t S Q
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
Middle : forall A P1, one R A P1 ->
(exists Q2, one S A Q2 /\
(exists P3 Q3, bisim_t P1 P3 Q2 Q3 /\
bisim_up_to bisim_t P3 Q3))
============================
exists Q1, one Q A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < Middle : apply Middle to PPstep.
Subgoal 1:
Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Right : bisim_up_to refl_t S Q
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
Middle : forall A P1, one R A P1 ->
(exists Q2, one S A Q2 /\
(exists P3 Q3, bisim_t P1 P3 Q2 Q3 /\
bisim_up_to bisim_t P3 Q3))
Middle1 : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
============================
exists Q1, one Q A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < clear Middle.
Subgoal 1:
Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Right : bisim_up_to refl_t S Q
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
Middle1 : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
============================
exists Q1, one Q A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < rename Middle1 to QQstep.
Subgoal 1:
Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Right : bisim_up_to refl_t S Q
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
============================
exists Q1, one Q A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < Right : case Right.
Subgoal 1:
Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Right : forall A P1, one S A P1 ->
(exists Q1, one Q A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
Right1 : forall A Q1, one Q A Q1 ->
(exists P1, one S A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
============================
exists Q1, one Q A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < clear Right1.
Subgoal 1:
Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Right : forall A P1, one S A P1 ->
(exists Q1, one Q A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
============================
exists Q1, one Q A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < Right : apply Right to QQstep.
Subgoal 1:
Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Right : forall A P1, one S A P1 ->
(exists Q1, one Q A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
Right1 : one Q A Q5
Right2 : refl_t Q1 P4 Q5 Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
exists Q1, one Q A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < clear Right.
Subgoal 1:
Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Right1 : one Q A Q5
Right2 : refl_t Q1 P4 Q5 Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
exists Q1, one Q A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < rename Right1 to Qstep.
Subgoal 1:
Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q5
Right2 : refl_t Q1 P4 Q5 Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
exists Q1, one Q A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < witness Q5.
Subgoal 1:
Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q5
Right2 : refl_t Q1 P4 Q5 Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
one Q A Q5 /\
(exists P2 Q2, refl_t P1 P2 Q5 Q2 /\ bisim_up_to refl_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < split.
Subgoal 1.1:
Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q5
Right2 : refl_t Q1 P4 Q5 Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
one Q A Q5
Subgoal 1.2 is:
exists P2 Q2, refl_t P1 P2 Q5 Q2 /\ bisim_up_to refl_t P2 Q2 +
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < search.
Subgoal 1.2:
Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q5
Right2 : refl_t Q1 P4 Q5 Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
exists P2 Q2, refl_t P1 P2 Q5 Q2 /\ bisim_up_to refl_t P2 Q2 +
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < witness P1.
Subgoal 1.2:
Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q5
Right2 : refl_t Q1 P4 Q5 Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
exists Q2, refl_t P1 P1 Q5 Q2 /\ bisim_up_to refl_t P1 Q2 +
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < witness Q5.
Subgoal 1.2:
Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q5
Right2 : refl_t Q1 P4 Q5 Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
refl_t P1 P1 Q5 Q5 /\ bisim_up_to refl_t P1 Q5 +
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < split.
Subgoal 1.2.1:
Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q5
Right2 : refl_t Q1 P4 Q5 Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
refl_t P1 P1 Q5 Q5
Subgoal 1.2.2 is:
bisim_up_to refl_t P1 Q5 +
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < search.
Subgoal 1.2.2:
Variables: P Q R S A P1 Q2 P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Pstep : one P A P1
PPstep : one R A Q2
Left2 : refl_t P1 P3 Q2 Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q2 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q5
Right2 : refl_t Q1 P4 Q5 Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
bisim_up_to refl_t P1 Q5 +
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < case Left2.
Subgoal 1.2.2:
Variables: P Q R S A P3 Q3 Q1 P2 Q4 Q5 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Pstep : one P A P3
PPstep : one R A Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A Q1
Middle2 : bisim_t Q3 P2 Q1 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q5
Right2 : refl_t Q1 P4 Q5 Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
bisim_up_to refl_t P3 Q5 +
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < case Right2.
Subgoal 1.2.2:
Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Pstep : one P A P3
PPstep : one R A Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A P4
Middle2 : bisim_t Q3 P2 P4 Q4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q6
Right3 : bisim_up_to refl_t P4 Q6
============================
bisim_up_to refl_t P3 Q6 +
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < Bisim : case Middle2.
Subgoal 1.2.2:
Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Pstep : one P A P3
PPstep : one R A Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A P4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q6
Right3 : bisim_up_to refl_t P4 Q6
Bisim : bisim_up_to refl_t Q3 P2
Bisim1 : bisim_up_to refl_t P4 Q4
============================
bisim_up_to refl_t P3 Q6 +
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < Link : apply bisim_transitive_ to Left3 Bisim.
Subgoal 1.2.2:
Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Pstep : one P A P3
PPstep : one R A Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A P4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q6
Right3 : bisim_up_to refl_t P4 Q6
Bisim : bisim_up_to refl_t Q3 P2
Bisim1 : bisim_up_to refl_t P4 Q4
Link : bisim_up_to refl_t P3 P2
============================
bisim_up_to refl_t P3 Q6 +
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < Link : apply bisim_symmetric_ to Bisim1.
Subgoal 1.2.2:
Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Pstep : one P A P3
PPstep : one R A Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A P4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q6
Right3 : bisim_up_to refl_t P4 Q6
Bisim : bisim_up_to refl_t Q3 P2
Bisim1 : bisim_up_to refl_t P4 Q4
Link : bisim_up_to refl_t P3 P2
Link1 : bisim_up_to refl_t Q4 P4
============================
bisim_up_to refl_t P3 Q6 +
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < Link : apply bisim_transitive_ to Link1 Right3.
Subgoal 1.2.2:
Variables: P Q R S A P3 Q3 P2 Q4 P4 Q6
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Pstep : one P A P3
PPstep : one R A Q3
Left3 : bisim_up_to refl_t P3 Q3
QQstep : one S A P4
Middle3 : bisim_up_to bisim_t P2 Q4
Qstep : one Q A Q6
Right3 : bisim_up_to refl_t P4 Q6
Bisim : bisim_up_to refl_t Q3 P2
Bisim1 : bisim_up_to refl_t P4 Q4
Link : bisim_up_to refl_t P3 P2
Link1 : bisim_up_to refl_t Q4 P4
Link2 : bisim_up_to refl_t Q4 Q6
============================
bisim_up_to refl_t P3 Q6 +
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < backchain CH.
Subgoal 2:
Variables: P Q R S
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Middle : bisim_up_to bisim_t R S
Right : bisim_up_to refl_t S Q
============================
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
bisim_sound_fst < intros Qstep.
Subgoal 2:
Variables: P Q R S A Q1
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Middle : bisim_up_to bisim_t R S
Right : bisim_up_to refl_t S Q
Qstep : one Q A Q1
============================
exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
bisim_sound_fst < Right : case Right.
Subgoal 2:
Variables: P Q R S A Q1
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Middle : bisim_up_to bisim_t R S
Qstep : one Q A Q1
Right : forall A P2, one S A P2 ->
(exists Q1, one Q A Q1 /\
(exists P3 Q3, refl_t P2 P3 Q1 Q3 /\ bisim_up_to refl_t P3 Q3))
Right1 : forall A Q1, one Q A Q1 ->
(exists P2, one S A P2 /\
(exists P3 Q3, refl_t P2 P3 Q1 Q3 /\ bisim_up_to refl_t P3 Q3))
============================
exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
bisim_sound_fst < Right : apply Right1 to Qstep.
Subgoal 2:
Variables: P Q R S A Q1 P2 P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Middle : bisim_up_to bisim_t R S
Qstep : one Q A Q1
Right : forall A P2, one S A P2 ->
(exists Q1, one Q A Q1 /\
(exists P3 Q3, refl_t P2 P3 Q1 Q3 /\ bisim_up_to refl_t P3 Q3))
Right1 : forall A Q1, one Q A Q1 ->
(exists P2, one S A P2 /\
(exists P3 Q3, refl_t P2 P3 Q1 Q3 /\ bisim_up_to refl_t P3 Q3))
Right2 : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
============================
exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
bisim_sound_fst < clear Right Right1.
Subgoal 2:
Variables: P Q R S A Q1 P2 P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Middle : bisim_up_to bisim_t R S
Qstep : one Q A Q1
Right2 : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
============================
exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
bisim_sound_fst < rename Right2 to Pstep.
Subgoal 2:
Variables: P Q R S A Q1 P2 P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Middle : bisim_up_to bisim_t R S
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
============================
exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
bisim_sound_fst < Middle : case Middle.
Subgoal 2:
Variables: P Q R S A Q1 P2 P3 Q3
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
Middle : forall A P2, one R A P2 ->
(exists Q1, one S A Q1 /\
(exists P3 Q3, bisim_t P2 P3 Q1 Q3 /\
bisim_up_to bisim_t P3 Q3))
Middle1 : forall A Q1, one S A Q1 ->
(exists P2, one R A P2 /\
(exists P3 Q3, bisim_t P2 P3 Q1 Q3 /\
bisim_up_to bisim_t P3 Q3))
============================
exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
bisim_sound_fst < Middle : apply Middle1 to Pstep.
Subgoal 2:
Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
Middle : forall A P2, one R A P2 ->
(exists Q1, one S A Q1 /\
(exists P3 Q3, bisim_t P2 P3 Q1 Q3 /\
bisim_up_to bisim_t P3 Q3))
Middle1 : forall A Q1, one S A Q1 ->
(exists P2, one R A P2 /\
(exists P3 Q3, bisim_t P2 P3 Q1 Q3 /\
bisim_up_to bisim_t P3 Q3))
Middle2 : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
============================
exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
bisim_sound_fst < clear Middle Middle1.
Subgoal 2:
Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
Middle2 : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
============================
exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
bisim_sound_fst < rename Middle2 to PPstep.
Subgoal 2:
Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Left : bisim_up_to refl_t P R
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
============================
exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
bisim_sound_fst < Left : case Left.
Subgoal 2:
Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
Left : forall A P1, one P A P1 ->
(exists Q1, one R A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
Left1 : forall A Q1, one R A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
============================
exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
bisim_sound_fst < Left : apply Left1 to PPstep.
Subgoal 2:
Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
Left : forall A P1, one P A P1 ->
(exists Q1, one R A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
Left1 : forall A Q1, one R A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2))
Left2 : one P A P5
Left3 : refl_t P5 P6 P1 Q4
Left4 : bisim_up_to refl_t P6 Q4
============================
exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
bisim_sound_fst < clear Left Left1.
Subgoal 2:
Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
Left2 : one P A P5
Left3 : refl_t P5 P6 P1 Q4
Left4 : bisim_up_to refl_t P6 Q4
============================
exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
bisim_sound_fst < rename Left2 to QQstep.
Subgoal 2:
Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P5
Left3 : refl_t P5 P6 P1 Q4
Left4 : bisim_up_to refl_t P6 Q4
============================
exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
bisim_sound_fst < witness P5.
Subgoal 2:
Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P5
Left3 : refl_t P5 P6 P1 Q4
Left4 : bisim_up_to refl_t P6 Q4
============================
one P A P5 /\
(exists P2 Q2, refl_t P5 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
bisim_sound_fst < split.
Subgoal 2.1:
Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P5
Left3 : refl_t P5 P6 P1 Q4
Left4 : bisim_up_to refl_t P6 Q4
============================
one P A P5
Subgoal 2.2 is:
exists P2 Q2, refl_t P5 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +
bisim_sound_fst < search.
Subgoal 2.2:
Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P5
Left3 : refl_t P5 P6 P1 Q4
Left4 : bisim_up_to refl_t P6 Q4
============================
exists P2 Q2, refl_t P5 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +
bisim_sound_fst < witness P5.
Subgoal 2.2:
Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P5
Left3 : refl_t P5 P6 P1 Q4
Left4 : bisim_up_to refl_t P6 Q4
============================
exists Q2, refl_t P5 P5 Q1 Q2 /\ bisim_up_to refl_t P5 Q2 +
bisim_sound_fst < witness Q1.
Subgoal 2.2:
Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P5
Left3 : refl_t P5 P6 P1 Q4
Left4 : bisim_up_to refl_t P6 Q4
============================
refl_t P5 P5 Q1 Q1 /\ bisim_up_to refl_t P5 Q1 +
bisim_sound_fst < split.
Subgoal 2.2.1:
Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P5
Left3 : refl_t P5 P6 P1 Q4
Left4 : bisim_up_to refl_t P6 Q4
============================
refl_t P5 P5 Q1 Q1
Subgoal 2.2.2 is:
bisim_up_to refl_t P5 Q1 +
bisim_sound_fst < search.
Subgoal 2.2.2:
Variables: P Q R S A Q1 P2 P3 Q3 P1 P4 Q2 P5 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A P1
Middle3 : bisim_t P1 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P5
Left3 : refl_t P5 P6 P1 Q4
Left4 : bisim_up_to refl_t P6 Q4
============================
bisim_up_to refl_t P5 Q1 +
bisim_sound_fst < case Left3.
Subgoal 2.2.2:
Variables: P Q R S A Q1 P2 P3 Q3 P4 Q2 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Qstep : one Q A Q1
Pstep : one S A P2
Right3 : refl_t P2 P3 Q1 Q3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A Q4
Middle3 : bisim_t Q4 P4 P2 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P6
Left4 : bisim_up_to refl_t P6 Q4
============================
bisim_up_to refl_t P6 Q1 +
bisim_sound_fst < case Right3.
Subgoal 2.2.2:
Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Qstep : one Q A Q3
Pstep : one S A P3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A Q4
Middle3 : bisim_t Q4 P4 P3 Q2
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P6
Left4 : bisim_up_to refl_t P6 Q4
============================
bisim_up_to refl_t P6 Q3 +
bisim_sound_fst < Link : case Middle3.
Subgoal 2.2.2:
Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Qstep : one Q A Q3
Pstep : one S A P3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A Q4
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P6
Left4 : bisim_up_to refl_t P6 Q4
Link : bisim_up_to refl_t Q4 P4
Link1 : bisim_up_to refl_t P3 Q2
============================
bisim_up_to refl_t P6 Q3 +
bisim_sound_fst < Link : apply bisim_transitive_ to Left4 Link.
Subgoal 2.2.2:
Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Qstep : one Q A Q3
Pstep : one S A P3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A Q4
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P6
Left4 : bisim_up_to refl_t P6 Q4
Link : bisim_up_to refl_t Q4 P4
Link1 : bisim_up_to refl_t P3 Q2
Link2 : bisim_up_to refl_t P6 P4
============================
bisim_up_to refl_t P6 Q3 +
bisim_sound_fst < Link : apply bisim_symmetric_ to Link1.
Subgoal 2.2.2:
Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Qstep : one Q A Q3
Pstep : one S A P3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A Q4
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P6
Left4 : bisim_up_to refl_t P6 Q4
Link : bisim_up_to refl_t Q4 P4
Link1 : bisim_up_to refl_t P3 Q2
Link2 : bisim_up_to refl_t P6 P4
Link3 : bisim_up_to refl_t Q2 P3
============================
bisim_up_to refl_t P6 Q3 +
bisim_sound_fst < Link : apply bisim_transitive_ to Link3 Right4.
Subgoal 2.2.2:
Variables: P Q R S A P3 Q3 P4 Q2 P6 Q4
CH : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q +
Qstep : one Q A Q3
Pstep : one S A P3
Right4 : bisim_up_to refl_t P3 Q3
PPstep : one R A Q4
Middle4 : bisim_up_to bisim_t P4 Q2
QQstep : one P A P6
Left4 : bisim_up_to refl_t P6 Q4
Link : bisim_up_to refl_t Q4 P4
Link1 : bisim_up_to refl_t P3 Q2
Link2 : bisim_up_to refl_t P6 P4
Link3 : bisim_up_to refl_t Q2 P3
Link4 : bisim_up_to refl_t Q2 Q3
============================
bisim_up_to refl_t P6 Q3 +
bisim_sound_fst < backchain CH.
Proof completed.
Abella < Theorem bisim_sound_snd :
is_sound_snd bisim_t.
============================
is_sound_snd bisim_t
bisim_sound_snd < unfold.
============================
forall P Q, bisim_up_to bisim_t P Q ->
(exists R S, bisim_up_to refl_t P R /\ bisim_up_to bisim_t R S /\
bisim_up_to refl_t S Q)
bisim_sound_snd < intros.
Variables: P Q
H1 : bisim_up_to bisim_t P Q
============================
exists R S, bisim_up_to refl_t P R /\ bisim_up_to bisim_t R S /\
bisim_up_to refl_t S Q
bisim_sound_snd < witness P.
Variables: P Q
H1 : bisim_up_to bisim_t P Q
============================
exists S, bisim_up_to refl_t P P /\ bisim_up_to bisim_t P S /\
bisim_up_to refl_t S Q
bisim_sound_snd < witness Q.
Variables: P Q
H1 : bisim_up_to bisim_t P Q
============================
bisim_up_to refl_t P P /\ bisim_up_to bisim_t P Q /\ bisim_up_to refl_t Q Q
bisim_sound_snd < split.
Subgoal 1:
Variables: P Q
H1 : bisim_up_to bisim_t P Q
============================
bisim_up_to refl_t P P
Subgoal 2 is:
bisim_up_to bisim_t P Q
Subgoal 3 is:
bisim_up_to refl_t Q Q
bisim_sound_snd < backchain bisim_reflexive_.
Subgoal 2:
Variables: P Q
H1 : bisim_up_to bisim_t P Q
============================
bisim_up_to bisim_t P Q
Subgoal 3 is:
bisim_up_to refl_t Q Q
bisim_sound_snd < search.
Subgoal 3:
Variables: P Q
H1 : bisim_up_to bisim_t P Q
============================
bisim_up_to refl_t Q Q
bisim_sound_snd < backchain bisim_reflexive_.
Proof completed.
Abella < Theorem bisim_sound :
is_sound bisim_t.
============================
is_sound bisim_t
bisim_sound < unfold.
============================
forall P Q, bisim_up_to bisim_t P Q -> bisim_up_to refl_t P Q
bisim_sound < intros.
Variables: P Q
H1 : bisim_up_to bisim_t P Q
============================
bisim_up_to refl_t P Q
bisim_sound < apply bisim_sound_snd.
Variables: P Q
H1 : bisim_up_to bisim_t P Q
H2 : is_sound_snd bisim_t
============================
bisim_up_to refl_t P Q
bisim_sound < case H2.
Variables: P Q
H1 : bisim_up_to bisim_t P Q
H3 : forall P Q, bisim_up_to bisim_t P Q ->
(exists R S, bisim_up_to refl_t P R /\ bisim_up_to bisim_t R S /\
bisim_up_to refl_t S Q)
============================
bisim_up_to refl_t P Q
bisim_sound < apply H3 to H1.
Variables: P Q R S
H1 : bisim_up_to bisim_t P Q
H3 : forall P Q, bisim_up_to bisim_t P Q ->
(exists R S, bisim_up_to refl_t P R /\ bisim_up_to bisim_t R S /\
bisim_up_to refl_t S Q)
H4 : bisim_up_to refl_t P R
H5 : bisim_up_to bisim_t R S
H6 : bisim_up_to refl_t S Q
============================
bisim_up_to refl_t P Q
bisim_sound < apply bisim_sound_fst.
Variables: P Q R S
H1 : bisim_up_to bisim_t P Q
H3 : forall P Q, bisim_up_to bisim_t P Q ->
(exists R S, bisim_up_to refl_t P R /\ bisim_up_to bisim_t R S /\
bisim_up_to refl_t S Q)
H4 : bisim_up_to refl_t P R
H5 : bisim_up_to bisim_t R S
H6 : bisim_up_to refl_t S Q
H7 : is_sound_fst bisim_t
============================
bisim_up_to refl_t P Q
bisim_sound < case H7.
Variables: P Q R S
H1 : bisim_up_to bisim_t P Q
H3 : forall P Q, bisim_up_to bisim_t P Q ->
(exists R S, bisim_up_to refl_t P R /\ bisim_up_to bisim_t R S /\
bisim_up_to refl_t S Q)
H4 : bisim_up_to refl_t P R
H5 : bisim_up_to bisim_t R S
H6 : bisim_up_to refl_t S Q
H8 : forall P Q, (exists R S, bisim_up_to refl_t P R /\
bisim_up_to bisim_t R S /\ bisim_up_to refl_t S Q) ->
bisim_up_to refl_t P Q
============================
bisim_up_to refl_t P Q
bisim_sound < backchain H8.
Proof completed.
Abella < Goodbye.
