Welcome to Abella 2.0.3-dev
Abella < Kind name, action, proc type.
Abella < Import "ccs_bisim".
Importing from ccs_bisim
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 ->)
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 "Tech" occurs to the left of ->)
Abella < Import "ccs_ctx".
Importing from ccs_ctx
Warning: Definition can be used to defeat stratification
(higher-order argument "Rel" occurs to the left of ->)
Abella < Import "ccs_bisim_examples_helper".
Importing from ccs_bisim_examples_helper
Abella < Theorem ex_bang_plus :
bisim (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))).
============================
bisim (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null)))
ex_bang_plus < Sound : apply bisim_sound.
Sound : is_sound bisim_t
============================
bisim (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null)))
ex_bang_plus < Sound : case Sound.
Sound : forall P Q, bisim_up_to bisim_t P Q -> bisim_up_to refl_t P Q
============================
bisim (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null)))
ex_bang_plus < unfold.
Sound : forall P Q, bisim_up_to bisim_t P Q -> bisim_up_to refl_t P Q
============================
bisim_up_to refl_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null)))
ex_bang_plus < backchain Sound.
Sound : forall P Q, bisim_up_to bisim_t P Q -> bisim_up_to refl_t P Q
============================
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null)))
ex_bang_plus < clear Sound.
============================
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null)))
ex_bang_plus < coinduction.
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) #
ex_bang_plus < intros.
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) #
ex_bang_plus < unfold.
Subgoal 1:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
forall A P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 ->
(exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < intros.
Subgoal 1:
Variables: A P1
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
H1 : one (repl (plus (act (dn a) null) (act (dn b) null))) A P1
============================
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A Q1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < case H1.
Subgoal 1.1:
Variables: A Q
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
H2 : one (plus (act (dn a) null) (act (dn b) null)) A Q
============================
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) Q)
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < case H2.
Subgoal 1.1.1:
Variables: A Q
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
H3 : one (act (dn a) null) A Q
============================
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) Q)
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 1.1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) Q)
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < case H3.
Subgoal 1.1.1:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null)))
(dn a) Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
null)
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 1.1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) Q)
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < witness par (par (repl (act (dn a) null)) null) (repl (act (dn b) null)).
Subgoal 1.1.1:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
one (par (repl (act (dn a) null)) (repl (act (dn b) null))) (dn a)
(par (par (repl (act (dn a) null)) null) (repl (act (dn b) null))) /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
null)
P2
(par (par (repl (act (dn a) null)) null)
(repl (act (dn b) null)))
Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 1.1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) Q)
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < split.
Subgoal 1.1.1.1:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
one (par (repl (act (dn a) null)) (repl (act (dn b) null))) (dn a)
(par (par (repl (act (dn a) null)) null) (repl (act (dn b) null)))
Subgoal 1.1.1.2 is:
exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) null)
P2
(par (par (repl (act (dn a) null)) null)
(repl (act (dn b) null)))
Q2 /\
bisim_up_to bisim_t P2 Q2 +
Subgoal 1.1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) Q)
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < search.
Subgoal 1.1.1.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) null)
P2
(par (par (repl (act (dn a) null)) null)
(repl (act (dn b) null)))
Q2 /\
bisim_up_to bisim_t P2 Q2 +
Subgoal 1.1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) Q)
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < witness repl (plus (act (dn a) null) (act (dn b) null)).
Subgoal 1.1.1.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
exists Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) null)
(repl (plus (act (dn a) null) (act (dn b) null)))
(par (par (repl (act (dn a) null)) null)
(repl (act (dn b) null)))
Q2 /\
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null))) Q2 +
Subgoal 1.1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) Q)
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < witness par (repl (act (dn a) null)) (repl (act (dn b) null)).
Subgoal 1.1.1.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_t (par (repl (plus (act (dn a) null) (act (dn b) null))) null)
(repl (plus (act (dn a) null) (act (dn b) null)))
(par (par (repl (act (dn a) null)) null) (repl (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) /\
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 1.1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) Q)
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < split.
Subgoal 1.1.1.2.1:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_t (par (repl (plus (act (dn a) null) (act (dn b) null))) null)
(repl (plus (act (dn a) null) (act (dn b) null)))
(par (par (repl (act (dn a) null)) null) (repl (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null)))
Subgoal 1.1.1.2.2 is:
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 1.1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) Q)
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < unfold.
Subgoal 1.1.1.2.1.1:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_up_to refl_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) null)
(repl (plus (act (dn a) null) (act (dn b) null)))
Subgoal 1.1.1.2.1.2 is:
bisim_up_to refl_t
(par (par (repl (act (dn a) null)) null) (repl (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null)))
Subgoal 1.1.1.2.2 is:
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 1.1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) Q)
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < backchain bisim_par_null.
Subgoal 1.1.1.2.1.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_up_to refl_t
(par (par (repl (act (dn a) null)) null) (repl (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null)))
Subgoal 1.1.1.2.2 is:
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 1.1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) Q)
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < backchain bisim_par_subst_1.
Subgoal 1.1.1.2.1.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_up_to refl_t (par (repl (act (dn a) null)) null)
(repl (act (dn a) null))
Subgoal 1.1.1.2.2 is:
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 1.1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) Q)
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < backchain bisim_par_null.
Subgoal 1.1.1.2.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 1.1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) Q)
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < backchain CH.
Subgoal 1.1.2:
Variables: A Q
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
H3 : one (act (dn b) null) A Q
============================
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) Q)
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < case H3.
Subgoal 1.1.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null)))
(dn b) Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
null)
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < witness par (repl (act (dn a) null)) (par (repl (act (dn b) null)) null).
Subgoal 1.1.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
one (par (repl (act (dn a) null)) (repl (act (dn b) null))) (dn b)
(par (repl (act (dn a) null)) (par (repl (act (dn b) null)) null)) /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
null)
P2
(par (repl (act (dn a) null))
(par (repl (act (dn b) null)) null))
Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < split.
Subgoal 1.1.2.1:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
one (par (repl (act (dn a) null)) (repl (act (dn b) null))) (dn b)
(par (repl (act (dn a) null)) (par (repl (act (dn b) null)) null))
Subgoal 1.1.2.2 is:
exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) null)
P2
(par (repl (act (dn a) null))
(par (repl (act (dn b) null)) null))
Q2 /\
bisim_up_to bisim_t P2 Q2 +
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < search.
Subgoal 1.1.2.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) null)
P2
(par (repl (act (dn a) null))
(par (repl (act (dn b) null)) null))
Q2 /\
bisim_up_to bisim_t P2 Q2 +
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < witness repl (plus (act (dn a) null) (act (dn b) null)).
Subgoal 1.1.2.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
exists Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) null)
(repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null))
(par (repl (act (dn b) null)) null))
Q2 /\
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null))) Q2 +
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < witness par (repl (act (dn a) null)) (repl (act (dn b) null)).
Subgoal 1.1.2.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_t (par (repl (plus (act (dn a) null) (act (dn b) null))) null)
(repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (par (repl (act (dn b) null)) null))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) /\
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < split.
Subgoal 1.1.2.2.1:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_t (par (repl (plus (act (dn a) null) (act (dn b) null))) null)
(repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (par (repl (act (dn b) null)) null))
(par (repl (act (dn a) null)) (repl (act (dn b) null)))
Subgoal 1.1.2.2.2 is:
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < unfold.
Subgoal 1.1.2.2.1.1:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_up_to refl_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) null)
(repl (plus (act (dn a) null) (act (dn b) null)))
Subgoal 1.1.2.2.1.2 is:
bisim_up_to refl_t
(par (repl (act (dn a) null)) (par (repl (act (dn b) null)) null))
(par (repl (act (dn a) null)) (repl (act (dn b) null)))
Subgoal 1.1.2.2.2 is:
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < backchain bisim_par_null.
Subgoal 1.1.2.2.1.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_up_to refl_t
(par (repl (act (dn a) null)) (par (repl (act (dn b) null)) null))
(par (repl (act (dn a) null)) (repl (act (dn b) null)))
Subgoal 1.1.2.2.2 is:
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < backchain bisim_par_subst_2.
Subgoal 1.1.2.2.1.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_up_to refl_t (par (repl (act (dn b) null)) null)
(repl (act (dn b) null))
Subgoal 1.1.2.2.2 is:
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < backchain bisim_par_null.
Subgoal 1.1.2.2.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 1.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < backchain CH.
Subgoal 1.2:
Variables: X R Q
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
H2 : one (plus (act (dn a) null) (act (dn b) null)) (up X) Q
H3 : one (plus (act (dn a) null) (act (dn b) null)) (dn X) R
============================
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < case H2.
Subgoal 1.2.1:
Variables: X R Q
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
H3 : one (plus (act (dn a) null) (act (dn b) null)) (dn X) R
H4 : one (act (dn a) null) (up X) Q
============================
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 1.2.2 is:
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < case H4.
Subgoal 1.2.2:
Variables: X R Q
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
H3 : one (plus (act (dn a) null) (act (dn b) null)) (dn X) R
H4 : one (act (dn b) null) (up X) Q
============================
exists Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) tau
Q1 /\
(exists P2 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
(par Q R))
P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < case H4.
Subgoal 2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
forall A Q1, one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A
Q1 ->
(exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_plus < intros.
Subgoal 2:
Variables: A Q1
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
H1 : one (par (repl (act (dn a) null)) (repl (act (dn b) null))) A Q1
============================
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +)
ex_bang_plus < case H1.
Subgoal 2.1:
Variables: A P1
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
H2 : one (repl (act (dn a) null)) A P1
============================
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) A P2 /\
(exists P3 Q2, bisim_t P2 P3 (par P1 (repl (act (dn b) null))) Q2 /\
bisim_up_to bisim_t P3 Q2 +)
Subgoal 2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q1, bisim_t P1 P2 (par (repl (act (dn a) null)) Q2) Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < case H2.
Subgoal 2.1.1:
Variables: A Q
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
H3 : one (act (dn a) null) A Q
============================
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) A P2 /\
(exists P3 Q2, bisim_t P2 P3
(par (par (repl (act (dn a) null)) Q)
(repl (act (dn b) null)))
Q2 /\
bisim_up_to bisim_t P3 Q2 +)
Subgoal 2.1.2 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q2, bisim_t P2 P3
(par (par (repl (act (dn a) null)) (par Q R))
(repl (act (dn b) null)))
Q2 /\
bisim_up_to bisim_t P3 Q2 +)
Subgoal 2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q1, bisim_t P1 P2 (par (repl (act (dn a) null)) Q2) Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < case H3.
Subgoal 2.1.1:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) (dn a) P2 /\
(exists P3 Q2, bisim_t P2 P3
(par (par (repl (act (dn a) null)) null)
(repl (act (dn b) null)))
Q2 /\
bisim_up_to bisim_t P3 Q2 +)
Subgoal 2.1.2 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q2, bisim_t P2 P3
(par (par (repl (act (dn a) null)) (par Q R))
(repl (act (dn b) null)))
Q2 /\
bisim_up_to bisim_t P3 Q2 +)
Subgoal 2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q1, bisim_t P1 P2 (par (repl (act (dn a) null)) Q2) Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < witness par (repl (plus (act (dn a) null) (act (dn b) null))) null.
Subgoal 2.1.1:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
one (repl (plus (act (dn a) null) (act (dn b) null))) (dn a)
(par (repl (plus (act (dn a) null) (act (dn b) null))) null) /\
(exists P3 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
null)
P3
(par (par (repl (act (dn a) null)) null)
(repl (act (dn b) null)))
Q2 /\
bisim_up_to bisim_t P3 Q2 +)
Subgoal 2.1.2 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q2, bisim_t P2 P3
(par (par (repl (act (dn a) null)) (par Q R))
(repl (act (dn b) null)))
Q2 /\
bisim_up_to bisim_t P3 Q2 +)
Subgoal 2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q1, bisim_t P1 P2 (par (repl (act (dn a) null)) Q2) Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < split.
Subgoal 2.1.1.1:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
one (repl (plus (act (dn a) null) (act (dn b) null))) (dn a)
(par (repl (plus (act (dn a) null) (act (dn b) null))) null)
Subgoal 2.1.1.2 is:
exists P3 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) null)
P3
(par (par (repl (act (dn a) null)) null)
(repl (act (dn b) null)))
Q2 /\
bisim_up_to bisim_t P3 Q2 +
Subgoal 2.1.2 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q2, bisim_t P2 P3
(par (par (repl (act (dn a) null)) (par Q R))
(repl (act (dn b) null)))
Q2 /\
bisim_up_to bisim_t P3 Q2 +)
Subgoal 2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q1, bisim_t P1 P2 (par (repl (act (dn a) null)) Q2) Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < search.
Subgoal 2.1.1.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
exists P3 Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) null)
P3
(par (par (repl (act (dn a) null)) null)
(repl (act (dn b) null)))
Q2 /\
bisim_up_to bisim_t P3 Q2 +
Subgoal 2.1.2 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q2, bisim_t P2 P3
(par (par (repl (act (dn a) null)) (par Q R))
(repl (act (dn b) null)))
Q2 /\
bisim_up_to bisim_t P3 Q2 +)
Subgoal 2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q1, bisim_t P1 P2 (par (repl (act (dn a) null)) Q2) Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < witness repl (plus (act (dn a) null) (act (dn b) null)).
Subgoal 2.1.1.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
exists Q2, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) null)
(repl (plus (act (dn a) null) (act (dn b) null)))
(par (par (repl (act (dn a) null)) null)
(repl (act (dn b) null)))
Q2 /\
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null))) Q2 +
Subgoal 2.1.2 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q2, bisim_t P2 P3
(par (par (repl (act (dn a) null)) (par Q R))
(repl (act (dn b) null)))
Q2 /\
bisim_up_to bisim_t P3 Q2 +)
Subgoal 2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q1, bisim_t P1 P2 (par (repl (act (dn a) null)) Q2) Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < witness par (repl (act (dn a) null)) (repl (act (dn b) null)).
Subgoal 2.1.1.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_t (par (repl (plus (act (dn a) null) (act (dn b) null))) null)
(repl (plus (act (dn a) null) (act (dn b) null)))
(par (par (repl (act (dn a) null)) null) (repl (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) /\
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 2.1.2 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q2, bisim_t P2 P3
(par (par (repl (act (dn a) null)) (par Q R))
(repl (act (dn b) null)))
Q2 /\
bisim_up_to bisim_t P3 Q2 +)
Subgoal 2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q1, bisim_t P1 P2 (par (repl (act (dn a) null)) Q2) Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < split.
Subgoal 2.1.1.2.1:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_t (par (repl (plus (act (dn a) null) (act (dn b) null))) null)
(repl (plus (act (dn a) null) (act (dn b) null)))
(par (par (repl (act (dn a) null)) null) (repl (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null)))
Subgoal 2.1.1.2.2 is:
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 2.1.2 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q2, bisim_t P2 P3
(par (par (repl (act (dn a) null)) (par Q R))
(repl (act (dn b) null)))
Q2 /\
bisim_up_to bisim_t P3 Q2 +)
Subgoal 2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q1, bisim_t P1 P2 (par (repl (act (dn a) null)) Q2) Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < unfold.
Subgoal 2.1.1.2.1.1:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_up_to refl_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) null)
(repl (plus (act (dn a) null) (act (dn b) null)))
Subgoal 2.1.1.2.1.2 is:
bisim_up_to refl_t
(par (par (repl (act (dn a) null)) null) (repl (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null)))
Subgoal 2.1.1.2.2 is:
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 2.1.2 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q2, bisim_t P2 P3
(par (par (repl (act (dn a) null)) (par Q R))
(repl (act (dn b) null)))
Q2 /\
bisim_up_to bisim_t P3 Q2 +)
Subgoal 2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q1, bisim_t P1 P2 (par (repl (act (dn a) null)) Q2) Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < backchain bisim_par_null.
Subgoal 2.1.1.2.1.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_up_to refl_t
(par (par (repl (act (dn a) null)) null) (repl (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null)))
Subgoal 2.1.1.2.2 is:
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 2.1.2 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q2, bisim_t P2 P3
(par (par (repl (act (dn a) null)) (par Q R))
(repl (act (dn b) null)))
Q2 /\
bisim_up_to bisim_t P3 Q2 +)
Subgoal 2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q1, bisim_t P1 P2 (par (repl (act (dn a) null)) Q2) Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < backchain bisim_par_subst_1.
Subgoal 2.1.1.2.1.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_up_to refl_t (par (repl (act (dn a) null)) null)
(repl (act (dn a) null))
Subgoal 2.1.1.2.2 is:
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 2.1.2 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q2, bisim_t P2 P3
(par (par (repl (act (dn a) null)) (par Q R))
(repl (act (dn b) null)))
Q2 /\
bisim_up_to bisim_t P3 Q2 +)
Subgoal 2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q1, bisim_t P1 P2 (par (repl (act (dn a) null)) Q2) Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < backchain bisim_par_null.
Subgoal 2.1.1.2.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 2.1.2 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q2, bisim_t P2 P3
(par (par (repl (act (dn a) null)) (par Q R))
(repl (act (dn b) null)))
Q2 /\
bisim_up_to bisim_t P3 Q2 +)
Subgoal 2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q1, bisim_t P1 P2 (par (repl (act (dn a) null)) Q2) Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < backchain CH.
Subgoal 2.1.2:
Variables: X R Q
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
H3 : one (act (dn a) null) (up X) Q
H4 : one (act (dn a) null) (dn X) R
============================
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q2, bisim_t P2 P3
(par (par (repl (act (dn a) null)) (par Q R))
(repl (act (dn b) null)))
Q2 /\
bisim_up_to bisim_t P3 Q2 +)
Subgoal 2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q1, bisim_t P1 P2 (par (repl (act (dn a) null)) Q2) Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < case H3.
Subgoal 2.2:
Variables: A Q2
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
H2 : one (repl (act (dn b) null)) A Q2
============================
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q1, bisim_t P1 P2 (par (repl (act (dn a) null)) Q2) Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < case H2.
Subgoal 2.2.1:
Variables: A Q
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
H3 : one (act (dn b) null) A Q
============================
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) A P1 /\
(exists P2 Q1, bisim_t P1 P2
(par (repl (act (dn a) null))
(par (repl (act (dn b) null)) Q))
Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P1 /\
(exists P2 Q1, bisim_t P1 P2
(par (repl (act (dn a) null))
(par (repl (act (dn b) null)) (par Q R)))
Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < case H3.
Subgoal 2.2.1:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) (dn b) P1 /\
(exists P2 Q1, bisim_t P1 P2
(par (repl (act (dn a) null))
(par (repl (act (dn b) null)) null))
Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P1 /\
(exists P2 Q1, bisim_t P1 P2
(par (repl (act (dn a) null))
(par (repl (act (dn b) null)) (par Q R)))
Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < witness par (repl (plus (act (dn a) null) (act (dn b) null))) null.
Subgoal 2.2.1:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
one (repl (plus (act (dn a) null) (act (dn b) null))) (dn b)
(par (repl (plus (act (dn a) null) (act (dn b) null))) null) /\
(exists P2 Q1, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null)))
null)
P2
(par (repl (act (dn a) null))
(par (repl (act (dn b) null)) null))
Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P1 /\
(exists P2 Q1, bisim_t P1 P2
(par (repl (act (dn a) null))
(par (repl (act (dn b) null)) (par Q R)))
Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < split.
Subgoal 2.2.1.1:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
one (repl (plus (act (dn a) null) (act (dn b) null))) (dn b)
(par (repl (plus (act (dn a) null) (act (dn b) null))) null)
Subgoal 2.2.1.2 is:
exists P2 Q1, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) null)
P2
(par (repl (act (dn a) null))
(par (repl (act (dn b) null)) null))
Q1 /\
bisim_up_to bisim_t P2 Q1 +
Subgoal 2.2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P1 /\
(exists P2 Q1, bisim_t P1 P2
(par (repl (act (dn a) null))
(par (repl (act (dn b) null)) (par Q R)))
Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < search.
Subgoal 2.2.1.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
exists P2 Q1, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) null)
P2
(par (repl (act (dn a) null))
(par (repl (act (dn b) null)) null))
Q1 /\
bisim_up_to bisim_t P2 Q1 +
Subgoal 2.2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P1 /\
(exists P2 Q1, bisim_t P1 P2
(par (repl (act (dn a) null))
(par (repl (act (dn b) null)) (par Q R)))
Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < witness repl (plus (act (dn a) null) (act (dn b) null)).
Subgoal 2.2.1.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
exists Q1, bisim_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) null)
(repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null))
(par (repl (act (dn b) null)) null))
Q1 /\
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null))) Q1 +
Subgoal 2.2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P1 /\
(exists P2 Q1, bisim_t P1 P2
(par (repl (act (dn a) null))
(par (repl (act (dn b) null)) (par Q R)))
Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < witness par (repl (act (dn a) null)) (repl (act (dn b) null)).
Subgoal 2.2.1.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_t (par (repl (plus (act (dn a) null) (act (dn b) null))) null)
(repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (par (repl (act (dn b) null)) null))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) /\
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 2.2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P1 /\
(exists P2 Q1, bisim_t P1 P2
(par (repl (act (dn a) null))
(par (repl (act (dn b) null)) (par Q R)))
Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < split.
Subgoal 2.2.1.2.1:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_t (par (repl (plus (act (dn a) null) (act (dn b) null))) null)
(repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (par (repl (act (dn b) null)) null))
(par (repl (act (dn a) null)) (repl (act (dn b) null)))
Subgoal 2.2.1.2.2 is:
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 2.2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P1 /\
(exists P2 Q1, bisim_t P1 P2
(par (repl (act (dn a) null))
(par (repl (act (dn b) null)) (par Q R)))
Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < unfold.
Subgoal 2.2.1.2.1.1:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_up_to refl_t
(par (repl (plus (act (dn a) null) (act (dn b) null))) null)
(repl (plus (act (dn a) null) (act (dn b) null)))
Subgoal 2.2.1.2.1.2 is:
bisim_up_to refl_t
(par (repl (act (dn a) null)) (par (repl (act (dn b) null)) null))
(par (repl (act (dn a) null)) (repl (act (dn b) null)))
Subgoal 2.2.1.2.2 is:
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 2.2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P1 /\
(exists P2 Q1, bisim_t P1 P2
(par (repl (act (dn a) null))
(par (repl (act (dn b) null)) (par Q R)))
Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < backchain bisim_par_null.
Subgoal 2.2.1.2.1.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_up_to refl_t
(par (repl (act (dn a) null)) (par (repl (act (dn b) null)) null))
(par (repl (act (dn a) null)) (repl (act (dn b) null)))
Subgoal 2.2.1.2.2 is:
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 2.2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P1 /\
(exists P2 Q1, bisim_t P1 P2
(par (repl (act (dn a) null))
(par (repl (act (dn b) null)) (par Q R)))
Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < backchain bisim_par_subst_2.
Subgoal 2.2.1.2.1.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_up_to refl_t (par (repl (act (dn b) null)) null)
(repl (act (dn b) null))
Subgoal 2.2.1.2.2 is:
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 2.2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P1 /\
(exists P2 Q1, bisim_t P1 P2
(par (repl (act (dn a) null))
(par (repl (act (dn b) null)) (par Q R)))
Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < backchain bisim_par_null.
Subgoal 2.2.1.2.2:
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
============================
bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
Subgoal 2.2.2 is:
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P1 /\
(exists P2 Q1, bisim_t P1 P2
(par (repl (act (dn a) null))
(par (repl (act (dn b) null)) (par Q R)))
Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < backchain CH.
Subgoal 2.2.2:
Variables: X R Q
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
H3 : one (act (dn b) null) (up X) Q
H4 : one (act (dn b) null) (dn X) R
============================
exists P1, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P1 /\
(exists P2 Q1, bisim_t P1 P2
(par (repl (act (dn a) null))
(par (repl (act (dn b) null)) (par Q R)))
Q1 /\
bisim_up_to bisim_t P2 Q1 +)
Subgoal 2.3 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < case H3.
Subgoal 2.3:
Variables: X Q2 P1
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
H2 : one (repl (act (dn a) null)) (up X) P1
H3 : one (repl (act (dn b) null)) (dn X) Q2
============================
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < case H2.
Subgoal 2.3:
Variables: X Q2 Q
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
H3 : one (repl (act (dn b) null)) (dn X) Q2
H4 : one (act (dn a) null) (up X) Q
============================
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par (par (repl (act (dn a) null)) Q) Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
Subgoal 2.4 is:
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < case H4.
Subgoal 2.4:
Variables: X Q2 P1
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
H2 : one (repl (act (dn a) null)) (dn X) P1
H3 : one (repl (act (dn b) null)) (up X) Q2
============================
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 Q2) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < case H3.
Subgoal 2.4:
Variables: X P1 Q
CH : bisim_up_to bisim_t (repl (plus (act (dn a) null) (act (dn b) null)))
(par (repl (act (dn a) null)) (repl (act (dn b) null))) +
H2 : one (repl (act (dn a) null)) (dn X) P1
H4 : one (act (dn b) null) (up X) Q
============================
exists P2, one (repl (plus (act (dn a) null) (act (dn b) null))) tau P2 /\
(exists P3 Q1, bisim_t P2 P3 (par P1 (par (repl (act (dn b) null)) Q)) Q1 /\
bisim_up_to bisim_t P3 Q1 +)
ex_bang_plus < case H4.
Proof completed.
Abella < Import "ccs_bisim_context_examples".
Importing from ccs_bisim_context_examples
Abella < Theorem ex_bang_bang :
bisim (repl (repl (act (dn a) null))) (repl (act (dn a) null)).
============================
bisim (repl (repl (act (dn a) null))) (repl (act (dn a) null))
ex_bang_bang < Sound : apply bisim_sound.
Sound : is_sound bisim_t
============================
bisim (repl (repl (act (dn a) null))) (repl (act (dn a) null))
ex_bang_bang < Sound : case Sound.
Sound : forall P Q, bisim_up_to bisim_t P Q -> bisim_up_to refl_t P Q
============================
bisim (repl (repl (act (dn a) null))) (repl (act (dn a) null))
ex_bang_bang < unfold.
Sound : forall P Q, bisim_up_to bisim_t P Q -> bisim_up_to refl_t P Q
============================
bisim_up_to refl_t (repl (repl (act (dn a) null))) (repl (act (dn a) null))
ex_bang_bang < backchain Sound.
Sound : forall P Q, bisim_up_to bisim_t P Q -> bisim_up_to refl_t P Q
============================
bisim_up_to bisim_t (repl (repl (act (dn a) null))) (repl (act (dn a) null))
ex_bang_bang < clear Sound.
============================
bisim_up_to bisim_t (repl (repl (act (dn a) null))) (repl (act (dn a) null))
ex_bang_bang < coinduction.
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
bisim_up_to bisim_t (repl (repl (act (dn a) null))) (repl (act (dn a) null)) #
ex_bang_bang < intros.
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
bisim_up_to bisim_t (repl (repl (act (dn a) null))) (repl (act (dn a) null)) #
ex_bang_bang < unfold.
Subgoal 1:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
forall A P1, one (repl (repl (act (dn a) null))) A P1 ->
(exists Q1, one (repl (act (dn a) null)) A Q1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
Subgoal 2 is:
forall A Q1, one (repl (act (dn a) null)) A Q1 ->
(exists P1, one (repl (repl (act (dn a) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_bang < intros.
Subgoal 1:
Variables: A P1
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
H1 : one (repl (repl (act (dn a) null))) A P1
============================
exists Q1, one (repl (act (dn a) null)) A Q1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (repl (act (dn a) null)) A Q1 ->
(exists P1, one (repl (repl (act (dn a) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_bang < case H1.
Subgoal 1.1:
Variables: A Q
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
H2 : one (repl (act (dn a) null)) A Q
============================
exists Q1, one (repl (act (dn a) null)) A Q1 /\
(exists P2 Q2, bisim_t (par (repl (repl (act (dn a) null))) Q) P2 Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 1.2 is:
exists Q1, one (repl (act (dn a) null)) tau Q1 /\
(exists P2 Q2, bisim_t (par (repl (repl (act (dn a) null))) (par Q R)) P2
Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (repl (act (dn a) null)) A Q1 ->
(exists P1, one (repl (repl (act (dn a) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_bang < case H2.
Subgoal 1.1.1:
Variables: A Q1
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
H3 : one (act (dn a) null) A Q1
============================
exists Q2, one (repl (act (dn a) null)) A Q2 /\
(exists P2 Q3, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) Q1))
P2 Q2 Q3 /\
bisim_up_to bisim_t P2 Q3 +)
Subgoal 1.1.2 is:
exists Q2, one (repl (act (dn a) null)) tau Q2 /\
(exists P2 Q3, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) (par Q1 R)))
P2 Q2 Q3 /\
bisim_up_to bisim_t P2 Q3 +)
Subgoal 1.2 is:
exists Q1, one (repl (act (dn a) null)) tau Q1 /\
(exists P2 Q2, bisim_t (par (repl (repl (act (dn a) null))) (par Q R)) P2
Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (repl (act (dn a) null)) A Q1 ->
(exists P1, one (repl (repl (act (dn a) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_bang < case H3.
Subgoal 1.1.1:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
exists Q2, one (repl (act (dn a) null)) (dn a) Q2 /\
(exists P2 Q3, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) null))
P2 Q2 Q3 /\
bisim_up_to bisim_t P2 Q3 +)
Subgoal 1.1.2 is:
exists Q2, one (repl (act (dn a) null)) tau Q2 /\
(exists P2 Q3, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) (par Q1 R)))
P2 Q2 Q3 /\
bisim_up_to bisim_t P2 Q3 +)
Subgoal 1.2 is:
exists Q1, one (repl (act (dn a) null)) tau Q1 /\
(exists P2 Q2, bisim_t (par (repl (repl (act (dn a) null))) (par Q R)) P2
Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (repl (act (dn a) null)) A Q1 ->
(exists P1, one (repl (repl (act (dn a) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_bang < witness par (repl (act (dn a) null)) null.
Subgoal 1.1.1:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
one (repl (act (dn a) null)) (dn a) (par (repl (act (dn a) null)) null) /\
(exists P2 Q3, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) null))
P2 (par (repl (act (dn a) null)) null) Q3 /\
bisim_up_to bisim_t P2 Q3 +)
Subgoal 1.1.2 is:
exists Q2, one (repl (act (dn a) null)) tau Q2 /\
(exists P2 Q3, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) (par Q1 R)))
P2 Q2 Q3 /\
bisim_up_to bisim_t P2 Q3 +)
Subgoal 1.2 is:
exists Q1, one (repl (act (dn a) null)) tau Q1 /\
(exists P2 Q2, bisim_t (par (repl (repl (act (dn a) null))) (par Q R)) P2
Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (repl (act (dn a) null)) A Q1 ->
(exists P1, one (repl (repl (act (dn a) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_bang < split.
Subgoal 1.1.1.1:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
one (repl (act (dn a) null)) (dn a) (par (repl (act (dn a) null)) null)
Subgoal 1.1.1.2 is:
exists P2 Q3, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) null))
P2 (par (repl (act (dn a) null)) null) Q3 /\
bisim_up_to bisim_t P2 Q3 +
Subgoal 1.1.2 is:
exists Q2, one (repl (act (dn a) null)) tau Q2 /\
(exists P2 Q3, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) (par Q1 R)))
P2 Q2 Q3 /\
bisim_up_to bisim_t P2 Q3 +)
Subgoal 1.2 is:
exists Q1, one (repl (act (dn a) null)) tau Q1 /\
(exists P2 Q2, bisim_t (par (repl (repl (act (dn a) null))) (par Q R)) P2
Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (repl (act (dn a) null)) A Q1 ->
(exists P1, one (repl (repl (act (dn a) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_bang < search.
Subgoal 1.1.1.2:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
exists P2 Q3, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) null))
P2 (par (repl (act (dn a) null)) null) Q3 /\
bisim_up_to bisim_t P2 Q3 +
Subgoal 1.1.2 is:
exists Q2, one (repl (act (dn a) null)) tau Q2 /\
(exists P2 Q3, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) (par Q1 R)))
P2 Q2 Q3 /\
bisim_up_to bisim_t P2 Q3 +)
Subgoal 1.2 is:
exists Q1, one (repl (act (dn a) null)) tau Q1 /\
(exists P2 Q2, bisim_t (par (repl (repl (act (dn a) null))) (par Q R)) P2
Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (repl (act (dn a) null)) A Q1 ->
(exists P1, one (repl (repl (act (dn a) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_bang < witness repl (repl (act (dn a) null)).
Subgoal 1.1.1.2:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
exists Q3, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) null))
(repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) null) Q3 /\
bisim_up_to bisim_t (repl (repl (act (dn a) null))) Q3 +
Subgoal 1.1.2 is:
exists Q2, one (repl (act (dn a) null)) tau Q2 /\
(exists P2 Q3, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) (par Q1 R)))
P2 Q2 Q3 /\
bisim_up_to bisim_t P2 Q3 +)
Subgoal 1.2 is:
exists Q1, one (repl (act (dn a) null)) tau Q1 /\
(exists P2 Q2, bisim_t (par (repl (repl (act (dn a) null))) (par Q R)) P2
Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (repl (act (dn a) null)) A Q1 ->
(exists P1, one (repl (repl (act (dn a) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_bang < witness repl (act (dn a) null).
Subgoal 1.1.1.2:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
bisim_t
(par (repl (repl (act (dn a) null))) (par (repl (act (dn a) null)) null))
(repl (repl (act (dn a) null))) (par (repl (act (dn a) null)) null)
(repl (act (dn a) null)) /\
bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
Subgoal 1.1.2 is:
exists Q2, one (repl (act (dn a) null)) tau Q2 /\
(exists P2 Q3, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) (par Q1 R)))
P2 Q2 Q3 /\
bisim_up_to bisim_t P2 Q3 +)
Subgoal 1.2 is:
exists Q1, one (repl (act (dn a) null)) tau Q1 /\
(exists P2 Q2, bisim_t (par (repl (repl (act (dn a) null))) (par Q R)) P2
Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (repl (act (dn a) null)) A Q1 ->
(exists P1, one (repl (repl (act (dn a) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_bang < split.
Subgoal 1.1.1.2.1:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
bisim_t
(par (repl (repl (act (dn a) null))) (par (repl (act (dn a) null)) null))
(repl (repl (act (dn a) null))) (par (repl (act (dn a) null)) null)
(repl (act (dn a) null))
Subgoal 1.1.1.2.2 is:
bisim_up_to bisim_t (repl (repl (act (dn a) null))) (repl (act (dn a) null)) +
Subgoal 1.1.2 is:
exists Q2, one (repl (act (dn a) null)) tau Q2 /\
(exists P2 Q3, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) (par Q1 R)))
P2 Q2 Q3 /\
bisim_up_to bisim_t P2 Q3 +)
Subgoal 1.2 is:
exists Q1, one (repl (act (dn a) null)) tau Q1 /\
(exists P2 Q2, bisim_t (par (repl (repl (act (dn a) null))) (par Q R)) P2
Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (repl (act (dn a) null)) A Q1 ->
(exists P1, one (repl (repl (act (dn a) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_bang < unfold.
Subgoal 1.1.1.2.1.1:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
bisim_up_to refl_t
(par (repl (repl (act (dn a) null))) (par (repl (act (dn a) null)) null))
(repl (repl (act (dn a) null)))
Subgoal 1.1.1.2.1.2 is:
bisim_up_to refl_t (par (repl (act (dn a) null)) null)
(repl (act (dn a) null))
Subgoal 1.1.1.2.2 is:
bisim_up_to bisim_t (repl (repl (act (dn a) null))) (repl (act (dn a) null)) +
Subgoal 1.1.2 is:
exists Q2, one (repl (act (dn a) null)) tau Q2 /\
(exists P2 Q3, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) (par Q1 R)))
P2 Q2 Q3 /\
bisim_up_to bisim_t P2 Q3 +)
Subgoal 1.2 is:
exists Q1, one (repl (act (dn a) null)) tau Q1 /\
(exists P2 Q2, bisim_t (par (repl (repl (act (dn a) null))) (par Q R)) P2
Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (repl (act (dn a) null)) A Q1 ->
(exists P1, one (repl (repl (act (dn a) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_bang < apply bisim_par_null with P = repl (act (dn a) null).
Subgoal 1.1.1.2.1.1:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
H4 : bisim_up_to refl_t (par (repl (act (dn a) null)) null)
(repl (act (dn a) null))
============================
bisim_up_to refl_t
(par (repl (repl (act (dn a) null))) (par (repl (act (dn a) null)) null))
(repl (repl (act (dn a) null)))
Subgoal 1.1.1.2.1.2 is:
bisim_up_to refl_t (par (repl (act (dn a) null)) null)
(repl (act (dn a) null))
Subgoal 1.1.1.2.2 is:
bisim_up_to bisim_t (repl (repl (act (dn a) null))) (repl (act (dn a) null)) +
Subgoal 1.1.2 is:
exists Q2, one (repl (act (dn a) null)) tau Q2 /\
(exists P2 Q3, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) (par Q1 R)))
P2 Q2 Q3 /\
bisim_up_to bisim_t P2 Q3 +)
Subgoal 1.2 is:
exists Q1, one (repl (act (dn a) null)) tau Q1 /\
(exists P2 Q2, bisim_t (par (repl (repl (act (dn a) null))) (par Q R)) P2
Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (repl (act (dn a) null)) A Q1 ->
(exists P1, one (repl (repl (act (dn a) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_bang < apply bisim_par_subst_2 to H4 with R = repl (repl (act (dn a) null)).
Subgoal 1.1.1.2.1.1:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
H4 : bisim_up_to refl_t (par (repl (act (dn a) null)) null)
(repl (act (dn a) null))
H5 : bisim_up_to refl_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) null))
(par (repl (repl (act (dn a) null))) (repl (act (dn a) null)))
============================
bisim_up_to refl_t
(par (repl (repl (act (dn a) null))) (par (repl (act (dn a) null)) null))
(repl (repl (act (dn a) null)))
Subgoal 1.1.1.2.1.2 is:
bisim_up_to refl_t (par (repl (act (dn a) null)) null)
(repl (act (dn a) null))
Subgoal 1.1.1.2.2 is:
bisim_up_to bisim_t (repl (repl (act (dn a) null))) (repl (act (dn a) null)) +
Subgoal 1.1.2 is:
exists Q2, one (repl (act (dn a) null)) tau Q2 /\
(exists P2 Q3, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) (par Q1 R)))
P2 Q2 Q3 /\
bisim_up_to bisim_t P2 Q3 +)
Subgoal 1.2 is:
exists Q1, one (repl (act (dn a) null)) tau Q1 /\
(exists P2 Q2, bisim_t (par (repl (repl (act (dn a) null))) (par Q R)) P2
Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (repl (act (dn a) null)) A Q1 ->
(exists P1, one (repl (repl (act (dn a) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_bang < apply bisim_repl_absorb with P = repl (act (dn a) null).
Subgoal 1.1.1.2.1.1:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
H4 : bisim_up_to refl_t (par (repl (act (dn a) null)) null)
(repl (act (dn a) null))
H5 : bisim_up_to refl_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) null))
(par (repl (repl (act (dn a) null))) (repl (act (dn a) null)))
H6 : bisim_up_to refl_t
(par (repl (repl (act (dn a) null))) (repl (act (dn a) null)))
(repl (repl (act (dn a) null)))
============================
bisim_up_to refl_t
(par (repl (repl (act (dn a) null))) (par (repl (act (dn a) null)) null))
(repl (repl (act (dn a) null)))
Subgoal 1.1.1.2.1.2 is:
bisim_up_to refl_t (par (repl (act (dn a) null)) null)
(repl (act (dn a) null))
Subgoal 1.1.1.2.2 is:
bisim_up_to bisim_t (repl (repl (act (dn a) null))) (repl (act (dn a) null)) +
Subgoal 1.1.2 is:
exists Q2, one (repl (act (dn a) null)) tau Q2 /\
(exists P2 Q3, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) (par Q1 R)))
P2 Q2 Q3 /\
bisim_up_to bisim_t P2 Q3 +)
Subgoal 1.2 is:
exists Q1, one (repl (act (dn a) null)) tau Q1 /\
(exists P2 Q2, bisim_t (par (repl (repl (act (dn a) null))) (par Q R)) P2
Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (repl (act (dn a) null)) A Q1 ->
(exists P1, one (repl (repl (act (dn a) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_bang < backchain bisim_transitive_.
Subgoal 1.1.1.2.1.2:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
bisim_up_to refl_t (par (repl (act (dn a) null)) null)
(repl (act (dn a) null))
Subgoal 1.1.1.2.2 is:
bisim_up_to bisim_t (repl (repl (act (dn a) null))) (repl (act (dn a) null)) +
Subgoal 1.1.2 is:
exists Q2, one (repl (act (dn a) null)) tau Q2 /\
(exists P2 Q3, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) (par Q1 R)))
P2 Q2 Q3 /\
bisim_up_to bisim_t P2 Q3 +)
Subgoal 1.2 is:
exists Q1, one (repl (act (dn a) null)) tau Q1 /\
(exists P2 Q2, bisim_t (par (repl (repl (act (dn a) null))) (par Q R)) P2
Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (repl (act (dn a) null)) A Q1 ->
(exists P1, one (repl (repl (act (dn a) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_bang < backchain bisim_par_null.
Subgoal 1.1.1.2.2:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
bisim_up_to bisim_t (repl (repl (act (dn a) null))) (repl (act (dn a) null)) +
Subgoal 1.1.2 is:
exists Q2, one (repl (act (dn a) null)) tau Q2 /\
(exists P2 Q3, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) (par Q1 R)))
P2 Q2 Q3 /\
bisim_up_to bisim_t P2 Q3 +)
Subgoal 1.2 is:
exists Q1, one (repl (act (dn a) null)) tau Q1 /\
(exists P2 Q2, bisim_t (par (repl (repl (act (dn a) null))) (par Q R)) P2
Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (repl (act (dn a) null)) A Q1 ->
(exists P1, one (repl (repl (act (dn a) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_bang < backchain CH.
Subgoal 1.1.2:
Variables: X R Q1
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
H3 : one (act (dn a) null) (up X) Q1
H4 : one (act (dn a) null) (dn X) R
============================
exists Q2, one (repl (act (dn a) null)) tau Q2 /\
(exists P2 Q3, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) (par Q1 R)))
P2 Q2 Q3 /\
bisim_up_to bisim_t P2 Q3 +)
Subgoal 1.2 is:
exists Q1, one (repl (act (dn a) null)) tau Q1 /\
(exists P2 Q2, bisim_t (par (repl (repl (act (dn a) null))) (par Q R)) P2
Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (repl (act (dn a) null)) A Q1 ->
(exists P1, one (repl (repl (act (dn a) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_bang < case H3.
Subgoal 1.2:
Variables: X R Q
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
H2 : one (repl (act (dn a) null)) (up X) Q
H3 : one (repl (act (dn a) null)) (dn X) R
============================
exists Q1, one (repl (act (dn a) null)) tau Q1 /\
(exists P2 Q2, bisim_t (par (repl (repl (act (dn a) null))) (par Q R)) P2
Q1 Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one (repl (act (dn a) null)) A Q1 ->
(exists P1, one (repl (repl (act (dn a) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_bang < case H2.
Subgoal 1.2:
Variables: X R Q1
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
H3 : one (repl (act (dn a) null)) (dn X) R
H4 : one (act (dn a) null) (up X) Q1
============================
exists Q2, one (repl (act (dn a) null)) tau Q2 /\
(exists P2 Q3, bisim_t
(par (repl (repl (act (dn a) null)))
(par (par (repl (act (dn a) null)) Q1) R))
P2 Q2 Q3 /\
bisim_up_to bisim_t P2 Q3 +)
Subgoal 2 is:
forall A Q1, one (repl (act (dn a) null)) A Q1 ->
(exists P1, one (repl (repl (act (dn a) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_bang < case H4.
Subgoal 2:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
forall A Q1, one (repl (act (dn a) null)) A Q1 ->
(exists P1, one (repl (repl (act (dn a) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +))
ex_bang_bang < intros.
Subgoal 2:
Variables: A Q1
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
H1 : one (repl (act (dn a) null)) A Q1
============================
exists P1, one (repl (repl (act (dn a) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ bisim_up_to bisim_t P2 Q2 +)
ex_bang_bang < case H1.
Subgoal 2.1:
Variables: A Q
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
H2 : one (act (dn a) null) A Q
============================
exists P1, one (repl (repl (act (dn a) null))) A P1 /\
(exists P2 Q2, bisim_t P1 P2 (par (repl (act (dn a) null)) Q) Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2.2 is:
exists P1, one (repl (repl (act (dn a) null))) tau P1 /\
(exists P2 Q2, bisim_t P1 P2 (par (repl (act (dn a) null)) (par Q R)) Q2 /\
bisim_up_to bisim_t P2 Q2 +)
ex_bang_bang < case H2.
Subgoal 2.1:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
exists P1, one (repl (repl (act (dn a) null))) (dn a) P1 /\
(exists P2 Q2, bisim_t P1 P2 (par (repl (act (dn a) null)) null) Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2.2 is:
exists P1, one (repl (repl (act (dn a) null))) tau P1 /\
(exists P2 Q2, bisim_t P1 P2 (par (repl (act (dn a) null)) (par Q R)) Q2 /\
bisim_up_to bisim_t P2 Q2 +)
ex_bang_bang < witness par (repl (repl (act (dn a) null))) (par (repl (act (dn a) null)) null).
Subgoal 2.1:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
one (repl (repl (act (dn a) null))) (dn a)
(par (repl (repl (act (dn a) null))) (par (repl (act (dn a) null)) null)) /\
(exists P2 Q2, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) null))
P2 (par (repl (act (dn a) null)) null) Q2 /\
bisim_up_to bisim_t P2 Q2 +)
Subgoal 2.2 is:
exists P1, one (repl (repl (act (dn a) null))) tau P1 /\
(exists P2 Q2, bisim_t P1 P2 (par (repl (act (dn a) null)) (par Q R)) Q2 /\
bisim_up_to bisim_t P2 Q2 +)
ex_bang_bang < split.
Subgoal 2.1.1:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
one (repl (repl (act (dn a) null))) (dn a)
(par (repl (repl (act (dn a) null))) (par (repl (act (dn a) null)) null))
Subgoal 2.1.2 is:
exists P2 Q2, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) null))
P2 (par (repl (act (dn a) null)) null) Q2 /\
bisim_up_to bisim_t P2 Q2 +
Subgoal 2.2 is:
exists P1, one (repl (repl (act (dn a) null))) tau P1 /\
(exists P2 Q2, bisim_t P1 P2 (par (repl (act (dn a) null)) (par Q R)) Q2 /\
bisim_up_to bisim_t P2 Q2 +)
ex_bang_bang < search.
Subgoal 2.1.2:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
exists P2 Q2, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) null))
P2 (par (repl (act (dn a) null)) null) Q2 /\
bisim_up_to bisim_t P2 Q2 +
Subgoal 2.2 is:
exists P1, one (repl (repl (act (dn a) null))) tau P1 /\
(exists P2 Q2, bisim_t P1 P2 (par (repl (act (dn a) null)) (par Q R)) Q2 /\
bisim_up_to bisim_t P2 Q2 +)
ex_bang_bang < witness repl (repl (act (dn a) null)).
Subgoal 2.1.2:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
exists Q2, bisim_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) null))
(repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) null) Q2 /\
bisim_up_to bisim_t (repl (repl (act (dn a) null))) Q2 +
Subgoal 2.2 is:
exists P1, one (repl (repl (act (dn a) null))) tau P1 /\
(exists P2 Q2, bisim_t P1 P2 (par (repl (act (dn a) null)) (par Q R)) Q2 /\
bisim_up_to bisim_t P2 Q2 +)
ex_bang_bang < witness repl (act (dn a) null).
Subgoal 2.1.2:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
bisim_t
(par (repl (repl (act (dn a) null))) (par (repl (act (dn a) null)) null))
(repl (repl (act (dn a) null))) (par (repl (act (dn a) null)) null)
(repl (act (dn a) null)) /\
bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
Subgoal 2.2 is:
exists P1, one (repl (repl (act (dn a) null))) tau P1 /\
(exists P2 Q2, bisim_t P1 P2 (par (repl (act (dn a) null)) (par Q R)) Q2 /\
bisim_up_to bisim_t P2 Q2 +)
ex_bang_bang < split.
Subgoal 2.1.2.1:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
bisim_t
(par (repl (repl (act (dn a) null))) (par (repl (act (dn a) null)) null))
(repl (repl (act (dn a) null))) (par (repl (act (dn a) null)) null)
(repl (act (dn a) null))
Subgoal 2.1.2.2 is:
bisim_up_to bisim_t (repl (repl (act (dn a) null))) (repl (act (dn a) null)) +
Subgoal 2.2 is:
exists P1, one (repl (repl (act (dn a) null))) tau P1 /\
(exists P2 Q2, bisim_t P1 P2 (par (repl (act (dn a) null)) (par Q R)) Q2 /\
bisim_up_to bisim_t P2 Q2 +)
ex_bang_bang < unfold.
Subgoal 2.1.2.1.1:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
bisim_up_to refl_t
(par (repl (repl (act (dn a) null))) (par (repl (act (dn a) null)) null))
(repl (repl (act (dn a) null)))
Subgoal 2.1.2.1.2 is:
bisim_up_to refl_t (par (repl (act (dn a) null)) null)
(repl (act (dn a) null))
Subgoal 2.1.2.2 is:
bisim_up_to bisim_t (repl (repl (act (dn a) null))) (repl (act (dn a) null)) +
Subgoal 2.2 is:
exists P1, one (repl (repl (act (dn a) null))) tau P1 /\
(exists P2 Q2, bisim_t P1 P2 (par (repl (act (dn a) null)) (par Q R)) Q2 /\
bisim_up_to bisim_t P2 Q2 +)
ex_bang_bang < apply bisim_par_null with P = repl (act (dn a) null).
Subgoal 2.1.2.1.1:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
H3 : bisim_up_to refl_t (par (repl (act (dn a) null)) null)
(repl (act (dn a) null))
============================
bisim_up_to refl_t
(par (repl (repl (act (dn a) null))) (par (repl (act (dn a) null)) null))
(repl (repl (act (dn a) null)))
Subgoal 2.1.2.1.2 is:
bisim_up_to refl_t (par (repl (act (dn a) null)) null)
(repl (act (dn a) null))
Subgoal 2.1.2.2 is:
bisim_up_to bisim_t (repl (repl (act (dn a) null))) (repl (act (dn a) null)) +
Subgoal 2.2 is:
exists P1, one (repl (repl (act (dn a) null))) tau P1 /\
(exists P2 Q2, bisim_t P1 P2 (par (repl (act (dn a) null)) (par Q R)) Q2 /\
bisim_up_to bisim_t P2 Q2 +)
ex_bang_bang < apply bisim_par_subst_2 to H3 with R = repl (repl (act (dn a) null)).
Subgoal 2.1.2.1.1:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
H3 : bisim_up_to refl_t (par (repl (act (dn a) null)) null)
(repl (act (dn a) null))
H4 : bisim_up_to refl_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) null))
(par (repl (repl (act (dn a) null))) (repl (act (dn a) null)))
============================
bisim_up_to refl_t
(par (repl (repl (act (dn a) null))) (par (repl (act (dn a) null)) null))
(repl (repl (act (dn a) null)))
Subgoal 2.1.2.1.2 is:
bisim_up_to refl_t (par (repl (act (dn a) null)) null)
(repl (act (dn a) null))
Subgoal 2.1.2.2 is:
bisim_up_to bisim_t (repl (repl (act (dn a) null))) (repl (act (dn a) null)) +
Subgoal 2.2 is:
exists P1, one (repl (repl (act (dn a) null))) tau P1 /\
(exists P2 Q2, bisim_t P1 P2 (par (repl (act (dn a) null)) (par Q R)) Q2 /\
bisim_up_to bisim_t P2 Q2 +)
ex_bang_bang < apply bisim_repl_absorb with P = repl (act (dn a) null).
Subgoal 2.1.2.1.1:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
H3 : bisim_up_to refl_t (par (repl (act (dn a) null)) null)
(repl (act (dn a) null))
H4 : bisim_up_to refl_t
(par (repl (repl (act (dn a) null)))
(par (repl (act (dn a) null)) null))
(par (repl (repl (act (dn a) null))) (repl (act (dn a) null)))
H5 : bisim_up_to refl_t
(par (repl (repl (act (dn a) null))) (repl (act (dn a) null)))
(repl (repl (act (dn a) null)))
============================
bisim_up_to refl_t
(par (repl (repl (act (dn a) null))) (par (repl (act (dn a) null)) null))
(repl (repl (act (dn a) null)))
Subgoal 2.1.2.1.2 is:
bisim_up_to refl_t (par (repl (act (dn a) null)) null)
(repl (act (dn a) null))
Subgoal 2.1.2.2 is:
bisim_up_to bisim_t (repl (repl (act (dn a) null))) (repl (act (dn a) null)) +
Subgoal 2.2 is:
exists P1, one (repl (repl (act (dn a) null))) tau P1 /\
(exists P2 Q2, bisim_t P1 P2 (par (repl (act (dn a) null)) (par Q R)) Q2 /\
bisim_up_to bisim_t P2 Q2 +)
ex_bang_bang < backchain bisim_transitive_.
Subgoal 2.1.2.1.2:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
bisim_up_to refl_t (par (repl (act (dn a) null)) null)
(repl (act (dn a) null))
Subgoal 2.1.2.2 is:
bisim_up_to bisim_t (repl (repl (act (dn a) null))) (repl (act (dn a) null)) +
Subgoal 2.2 is:
exists P1, one (repl (repl (act (dn a) null))) tau P1 /\
(exists P2 Q2, bisim_t P1 P2 (par (repl (act (dn a) null)) (par Q R)) Q2 /\
bisim_up_to bisim_t P2 Q2 +)
ex_bang_bang < backchain bisim_par_null.
Subgoal 2.1.2.2:
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
============================
bisim_up_to bisim_t (repl (repl (act (dn a) null))) (repl (act (dn a) null)) +
Subgoal 2.2 is:
exists P1, one (repl (repl (act (dn a) null))) tau P1 /\
(exists P2 Q2, bisim_t P1 P2 (par (repl (act (dn a) null)) (par Q R)) Q2 /\
bisim_up_to bisim_t P2 Q2 +)
ex_bang_bang < backchain CH.
Subgoal 2.2:
Variables: X R Q
CH : bisim_up_to bisim_t (repl (repl (act (dn a) null)))
(repl (act (dn a) null)) +
H2 : one (act (dn a) null) (up X) Q
H3 : one (act (dn a) null) (dn X) R
============================
exists P1, one (repl (repl (act (dn a) null))) tau P1 /\
(exists P2 Q2, bisim_t P1 P2 (par (repl (act (dn a) null)) (par Q R)) Q2 /\
bisim_up_to bisim_t P2 Q2 +)
ex_bang_bang < case H2.
Proof completed.
Abella < Goodbye.
