Welcome to Abella 2.0.3-dev
Abella < Kind name, action, proc type.
Abella < Import "ccs_core".
Importing from ccs_core
Warning: Definition can be used to defeat stratification
(higher-order argument "Tech" occurs to the left of ->)
Warning: Definition can be used to defeat stratification
(higher-order argument "Rel" occurs to the left of ->)
Warning: Definition can be used to defeat stratification
(higher-order argument "Rel" occurs to the left of ->)
Abella < 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 < Define context_t : proc -> proc -> proc -> proc -> prop by
context_t P1 P2 Q1 Q2 := exists C, at C P2 P1 /\ at C Q2 Q1.
Abella < Theorem concat_ctx2 :
forall C1 C2 P1 P2 P3 Q1 Q2 Q3, at C1 P1 P2 -> at C2 P2 P3 -> at C1 Q1 Q2 ->
at C2 Q2 Q3 -> (exists C3, at C3 P1 P3 /\ at C3 Q1 Q3).
============================
forall C1 C2 P1 P2 P3 Q1 Q2 Q3, at C1 P1 P2 -> at C2 P2 P3 -> at C1 Q1 Q2 ->
at C2 Q2 Q3 -> (exists C3, at C3 P1 P3 /\ at C3 Q1 Q3)
concat_ctx2 < induction on 2.
IH : forall C1 C2 P1 P2 P3 Q1 Q2 Q3, at C1 P1 P2 -> at C2 P2 P3 * ->
at C1 Q1 Q2 -> at C2 Q2 Q3 -> (exists C3, at C3 P1 P3 /\ at C3 Q1 Q3)
============================
forall C1 C2 P1 P2 P3 Q1 Q2 Q3, at C1 P1 P2 -> at C2 P2 P3 @ ->
at C1 Q1 Q2 -> at C2 Q2 Q3 -> (exists C3, at C3 P1 P3 /\ at C3 Q1 Q3)
concat_ctx2 < intros.
Variables: C1 C2 P1 P2 P3 Q1 Q2 Q3
IH : forall C1 C2 P1 P2 P3 Q1 Q2 Q3, at C1 P1 P2 -> at C2 P2 P3 * ->
at C1 Q1 Q2 -> at C2 Q2 Q3 -> (exists C3, at C3 P1 P3 /\ at C3 Q1 Q3)
H1 : at C1 P1 P2
H2 : at C2 P2 P3 @
H3 : at C1 Q1 Q2
H4 : at C2 Q2 Q3
============================
exists C3, at C3 P1 P3 /\ at C3 Q1 Q3
concat_ctx2 < case H2.
Subgoal 1:
Variables: C1 P1 P3 Q1 Q2 Q3
IH : forall C1 C2 P1 P2 P3 Q1 Q2 Q3, at C1 P1 P2 -> at C2 P2 P3 * ->
at C1 Q1 Q2 -> at C2 Q2 Q3 -> (exists C3, at C3 P1 P3 /\ at C3 Q1 Q3)
H1 : at C1 P1 P3
H3 : at C1 Q1 Q2
H4 : at hole Q2 Q3
============================
exists C3, at C3 P1 P3 /\ at C3 Q1 Q3
Subgoal 2 is:
exists C3, at C3 P1 (plus Q R) /\ at C3 Q1 Q3
Subgoal 3 is:
exists C3, at C3 P1 (plus R Q) /\ at C3 Q1 Q3
Subgoal 4 is:
exists C3, at C3 P1 (par Q R) /\ at C3 Q1 Q3
Subgoal 5 is:
exists C3, at C3 P1 (par R Q) /\ at C3 Q1 Q3
Subgoal 6 is:
exists C3, at C3 P1 (act A Q) /\ at C3 Q1 Q3
concat_ctx2 < case H4.
Subgoal 1:
Variables: C1 P1 P3 Q1 Q3
IH : forall C1 C2 P1 P2 P3 Q1 Q2 Q3, at C1 P1 P2 -> at C2 P2 P3 * ->
at C1 Q1 Q2 -> at C2 Q2 Q3 -> (exists C3, at C3 P1 P3 /\ at C3 Q1 Q3)
H1 : at C1 P1 P3
H3 : at C1 Q1 Q3
============================
exists C3, at C3 P1 P3 /\ at C3 Q1 Q3
Subgoal 2 is:
exists C3, at C3 P1 (plus Q R) /\ at C3 Q1 Q3
Subgoal 3 is:
exists C3, at C3 P1 (plus R Q) /\ at C3 Q1 Q3
Subgoal 4 is:
exists C3, at C3 P1 (par Q R) /\ at C3 Q1 Q3
Subgoal 5 is:
exists C3, at C3 P1 (par R Q) /\ at C3 Q1 Q3
Subgoal 6 is:
exists C3, at C3 P1 (act A Q) /\ at C3 Q1 Q3
concat_ctx2 < search.
Subgoal 2:
Variables: C1 P1 P2 Q1 Q2 Q3 R Q C
IH : forall C1 C2 P1 P2 P3 Q1 Q2 Q3, at C1 P1 P2 -> at C2 P2 P3 * ->
at C1 Q1 Q2 -> at C2 Q2 Q3 -> (exists C3, at C3 P1 P3 /\ at C3 Q1 Q3)
H1 : at C1 P1 P2
H3 : at C1 Q1 Q2
H4 : at (plus_l C R) Q2 Q3
H5 : at C P2 Q *
============================
exists C3, at C3 P1 (plus Q R) /\ at C3 Q1 Q3
Subgoal 3 is:
exists C3, at C3 P1 (plus R Q) /\ at C3 Q1 Q3
Subgoal 4 is:
exists C3, at C3 P1 (par Q R) /\ at C3 Q1 Q3
Subgoal 5 is:
exists C3, at C3 P1 (par R Q) /\ at C3 Q1 Q3
Subgoal 6 is:
exists C3, at C3 P1 (act A Q) /\ at C3 Q1 Q3
concat_ctx2 < case H4.
Subgoal 2:
Variables: C1 P1 P2 Q1 Q2 R Q C Q4
IH : forall C1 C2 P1 P2 P3 Q1 Q2 Q3, at C1 P1 P2 -> at C2 P2 P3 * ->
at C1 Q1 Q2 -> at C2 Q2 Q3 -> (exists C3, at C3 P1 P3 /\ at C3 Q1 Q3)
H1 : at C1 P1 P2
H3 : at C1 Q1 Q2
H5 : at C P2 Q *
H6 : at C Q2 Q4
============================
exists C3, at C3 P1 (plus Q R) /\ at C3 Q1 (plus Q4 R)
Subgoal 3 is:
exists C3, at C3 P1 (plus R Q) /\ at C3 Q1 Q3
Subgoal 4 is:
exists C3, at C3 P1 (par Q R) /\ at C3 Q1 Q3
Subgoal 5 is:
exists C3, at C3 P1 (par R Q) /\ at C3 Q1 Q3
Subgoal 6 is:
exists C3, at C3 P1 (act A Q) /\ at C3 Q1 Q3
concat_ctx2 < apply IH to H1 H5 H3 H6.
Subgoal 2:
Variables: C1 P1 P2 Q1 Q2 R Q C Q4 C3
IH : forall C1 C2 P1 P2 P3 Q1 Q2 Q3, at C1 P1 P2 -> at C2 P2 P3 * ->
at C1 Q1 Q2 -> at C2 Q2 Q3 -> (exists C3, at C3 P1 P3 /\ at C3 Q1 Q3)
H1 : at C1 P1 P2
H3 : at C1 Q1 Q2
H5 : at C P2 Q *
H6 : at C Q2 Q4
H7 : at C3 P1 Q
H8 : at C3 Q1 Q4
============================
exists C3, at C3 P1 (plus Q R) /\ at C3 Q1 (plus Q4 R)
Subgoal 3 is:
exists C3, at C3 P1 (plus R Q) /\ at C3 Q1 Q3
Subgoal 4 is:
exists C3, at C3 P1 (par Q R) /\ at C3 Q1 Q3
Subgoal 5 is:
exists C3, at C3 P1 (par R Q) /\ at C3 Q1 Q3
Subgoal 6 is:
exists C3, at C3 P1 (act A Q) /\ at C3 Q1 Q3
concat_ctx2 < search.
Subgoal 3:
Variables: C1 P1 P2 Q1 Q2 Q3 Q R C
IH : forall C1 C2 P1 P2 P3 Q1 Q2 Q3, at C1 P1 P2 -> at C2 P2 P3 * ->
at C1 Q1 Q2 -> at C2 Q2 Q3 -> (exists C3, at C3 P1 P3 /\ at C3 Q1 Q3)
H1 : at C1 P1 P2
H3 : at C1 Q1 Q2
H4 : at (plus_r R C) Q2 Q3
H5 : at C P2 Q *
============================
exists C3, at C3 P1 (plus R Q) /\ at C3 Q1 Q3
Subgoal 4 is:
exists C3, at C3 P1 (par Q R) /\ at C3 Q1 Q3
Subgoal 5 is:
exists C3, at C3 P1 (par R Q) /\ at C3 Q1 Q3
Subgoal 6 is:
exists C3, at C3 P1 (act A Q) /\ at C3 Q1 Q3
concat_ctx2 < case H4.
Subgoal 3:
Variables: C1 P1 P2 Q1 Q2 Q R C Q4
IH : forall C1 C2 P1 P2 P3 Q1 Q2 Q3, at C1 P1 P2 -> at C2 P2 P3 * ->
at C1 Q1 Q2 -> at C2 Q2 Q3 -> (exists C3, at C3 P1 P3 /\ at C3 Q1 Q3)
H1 : at C1 P1 P2
H3 : at C1 Q1 Q2
H5 : at C P2 Q *
H6 : at C Q2 Q4
============================
exists C3, at C3 P1 (plus R Q) /\ at C3 Q1 (plus R Q4)
Subgoal 4 is:
exists C3, at C3 P1 (par Q R) /\ at C3 Q1 Q3
Subgoal 5 is:
exists C3, at C3 P1 (par R Q) /\ at C3 Q1 Q3
Subgoal 6 is:
exists C3, at C3 P1 (act A Q) /\ at C3 Q1 Q3
concat_ctx2 < apply IH to H1 H5 H3 H6.
Subgoal 3:
Variables: C1 P1 P2 Q1 Q2 Q R C Q4 C3
IH : forall C1 C2 P1 P2 P3 Q1 Q2 Q3, at C1 P1 P2 -> at C2 P2 P3 * ->
at C1 Q1 Q2 -> at C2 Q2 Q3 -> (exists C3, at C3 P1 P3 /\ at C3 Q1 Q3)
H1 : at C1 P1 P2
H3 : at C1 Q1 Q2
H5 : at C P2 Q *
H6 : at C Q2 Q4
H7 : at C3 P1 Q
H8 : at C3 Q1 Q4
============================
exists C3, at C3 P1 (plus R Q) /\ at C3 Q1 (plus R Q4)
Subgoal 4 is:
exists C3, at C3 P1 (par Q R) /\ at C3 Q1 Q3
Subgoal 5 is:
exists C3, at C3 P1 (par R Q) /\ at C3 Q1 Q3
Subgoal 6 is:
exists C3, at C3 P1 (act A Q) /\ at C3 Q1 Q3
concat_ctx2 < search.
Subgoal 4:
Variables: C1 P1 P2 Q1 Q2 Q3 R Q C
IH : forall C1 C2 P1 P2 P3 Q1 Q2 Q3, at C1 P1 P2 -> at C2 P2 P3 * ->
at C1 Q1 Q2 -> at C2 Q2 Q3 -> (exists C3, at C3 P1 P3 /\ at C3 Q1 Q3)
H1 : at C1 P1 P2
H3 : at C1 Q1 Q2
H4 : at (par_l C R) Q2 Q3
H5 : at C P2 Q *
============================
exists C3, at C3 P1 (par Q R) /\ at C3 Q1 Q3
Subgoal 5 is:
exists C3, at C3 P1 (par R Q) /\ at C3 Q1 Q3
Subgoal 6 is:
exists C3, at C3 P1 (act A Q) /\ at C3 Q1 Q3
concat_ctx2 < case H4.
Subgoal 4:
Variables: C1 P1 P2 Q1 Q2 R Q C Q4
IH : forall C1 C2 P1 P2 P3 Q1 Q2 Q3, at C1 P1 P2 -> at C2 P2 P3 * ->
at C1 Q1 Q2 -> at C2 Q2 Q3 -> (exists C3, at C3 P1 P3 /\ at C3 Q1 Q3)
H1 : at C1 P1 P2
H3 : at C1 Q1 Q2
H5 : at C P2 Q *
H6 : at C Q2 Q4
============================
exists C3, at C3 P1 (par Q R) /\ at C3 Q1 (par Q4 R)
Subgoal 5 is:
exists C3, at C3 P1 (par R Q) /\ at C3 Q1 Q3
Subgoal 6 is:
exists C3, at C3 P1 (act A Q) /\ at C3 Q1 Q3
concat_ctx2 < apply IH to H1 H5 H3 H6.
Subgoal 4:
Variables: C1 P1 P2 Q1 Q2 R Q C Q4 C3
IH : forall C1 C2 P1 P2 P3 Q1 Q2 Q3, at C1 P1 P2 -> at C2 P2 P3 * ->
at C1 Q1 Q2 -> at C2 Q2 Q3 -> (exists C3, at C3 P1 P3 /\ at C3 Q1 Q3)
H1 : at C1 P1 P2
H3 : at C1 Q1 Q2
H5 : at C P2 Q *
H6 : at C Q2 Q4
H7 : at C3 P1 Q
H8 : at C3 Q1 Q4
============================
exists C3, at C3 P1 (par Q R) /\ at C3 Q1 (par Q4 R)
Subgoal 5 is:
exists C3, at C3 P1 (par R Q) /\ at C3 Q1 Q3
Subgoal 6 is:
exists C3, at C3 P1 (act A Q) /\ at C3 Q1 Q3
concat_ctx2 < search.
Subgoal 5:
Variables: C1 P1 P2 Q1 Q2 Q3 Q R C
IH : forall C1 C2 P1 P2 P3 Q1 Q2 Q3, at C1 P1 P2 -> at C2 P2 P3 * ->
at C1 Q1 Q2 -> at C2 Q2 Q3 -> (exists C3, at C3 P1 P3 /\ at C3 Q1 Q3)
H1 : at C1 P1 P2
H3 : at C1 Q1 Q2
H4 : at (par_r R C) Q2 Q3
H5 : at C P2 Q *
============================
exists C3, at C3 P1 (par R Q) /\ at C3 Q1 Q3
Subgoal 6 is:
exists C3, at C3 P1 (act A Q) /\ at C3 Q1 Q3
concat_ctx2 < case H4.
Subgoal 5:
Variables: C1 P1 P2 Q1 Q2 Q R C Q4
IH : forall C1 C2 P1 P2 P3 Q1 Q2 Q3, at C1 P1 P2 -> at C2 P2 P3 * ->
at C1 Q1 Q2 -> at C2 Q2 Q3 -> (exists C3, at C3 P1 P3 /\ at C3 Q1 Q3)
H1 : at C1 P1 P2
H3 : at C1 Q1 Q2
H5 : at C P2 Q *
H6 : at C Q2 Q4
============================
exists C3, at C3 P1 (par R Q) /\ at C3 Q1 (par R Q4)
Subgoal 6 is:
exists C3, at C3 P1 (act A Q) /\ at C3 Q1 Q3
concat_ctx2 < apply IH to H1 H5 H3 H6.
Subgoal 5:
Variables: C1 P1 P2 Q1 Q2 Q R C Q4 C3
IH : forall C1 C2 P1 P2 P3 Q1 Q2 Q3, at C1 P1 P2 -> at C2 P2 P3 * ->
at C1 Q1 Q2 -> at C2 Q2 Q3 -> (exists C3, at C3 P1 P3 /\ at C3 Q1 Q3)
H1 : at C1 P1 P2
H3 : at C1 Q1 Q2
H5 : at C P2 Q *
H6 : at C Q2 Q4
H7 : at C3 P1 Q
H8 : at C3 Q1 Q4
============================
exists C3, at C3 P1 (par R Q) /\ at C3 Q1 (par R Q4)
Subgoal 6 is:
exists C3, at C3 P1 (act A Q) /\ at C3 Q1 Q3
concat_ctx2 < search.
Subgoal 6:
Variables: C1 P1 P2 Q1 Q2 Q3 Q A C
IH : forall C1 C2 P1 P2 P3 Q1 Q2 Q3, at C1 P1 P2 -> at C2 P2 P3 * ->
at C1 Q1 Q2 -> at C2 Q2 Q3 -> (exists C3, at C3 P1 P3 /\ at C3 Q1 Q3)
H1 : at C1 P1 P2
H3 : at C1 Q1 Q2
H4 : at (act_d A C) Q2 Q3
H5 : at C P2 Q *
============================
exists C3, at C3 P1 (act A Q) /\ at C3 Q1 Q3
concat_ctx2 < case H4.
Subgoal 6:
Variables: C1 P1 P2 Q1 Q2 Q A C Q4
IH : forall C1 C2 P1 P2 P3 Q1 Q2 Q3, at C1 P1 P2 -> at C2 P2 P3 * ->
at C1 Q1 Q2 -> at C2 Q2 Q3 -> (exists C3, at C3 P1 P3 /\ at C3 Q1 Q3)
H1 : at C1 P1 P2
H3 : at C1 Q1 Q2
H5 : at C P2 Q *
H6 : at C Q2 Q4
============================
exists C3, at C3 P1 (act A Q) /\ at C3 Q1 (act A Q4)
concat_ctx2 < apply IH to H1 H5 H3 H6.
Subgoal 6:
Variables: C1 P1 P2 Q1 Q2 Q A C Q4 C3
IH : forall C1 C2 P1 P2 P3 Q1 Q2 Q3, at C1 P1 P2 -> at C2 P2 P3 * ->
at C1 Q1 Q2 -> at C2 Q2 Q3 -> (exists C3, at C3 P1 P3 /\ at C3 Q1 Q3)
H1 : at C1 P1 P2
H3 : at C1 Q1 Q2
H5 : at C P2 Q *
H6 : at C Q2 Q4
H7 : at C3 P1 Q
H8 : at C3 Q1 Q4
============================
exists C3, at C3 P1 (act A Q) /\ at C3 Q1 (act A Q4)
concat_ctx2 < search.
Proof completed.
Abella < Theorem context_reflexive :
forall P, bisim_up_to context_t P P.
============================
forall P, bisim_up_to context_t P P
context_reflexive < coinduction.
CH : forall P, bisim_up_to context_t P P +
============================
forall P, bisim_up_to context_t P P #
context_reflexive < intros.
Variables: P
CH : forall P, bisim_up_to context_t P P +
============================
bisim_up_to context_t P P #
context_reflexive < unfold.
Subgoal 1:
Variables: P
CH : forall P, bisim_up_to context_t P P +
============================
forall A P1, one P A P1 ->
(exists Q1, one P A Q1 /\
(exists P2 Q2, context_t P1 P2 Q1 Q2 /\ bisim_up_to context_t P2 Q2 +))
Subgoal 2 is:
forall A Q1, one P A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, context_t P1 P2 Q1 Q2 /\ bisim_up_to context_t P2 Q2 +))
context_reflexive < intros.
Subgoal 1:
Variables: P A P1
CH : forall P, bisim_up_to context_t P P +
H1 : one P A P1
============================
exists Q1, one P A Q1 /\
(exists P2 Q2, context_t P1 P2 Q1 Q2 /\ bisim_up_to context_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one P A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, context_t P1 P2 Q1 Q2 /\ bisim_up_to context_t P2 Q2 +))
context_reflexive < witness P1.
Subgoal 1:
Variables: P A P1
CH : forall P, bisim_up_to context_t P P +
H1 : one P A P1
============================
one P A P1 /\
(exists P2 Q2, context_t P1 P2 P1 Q2 /\ bisim_up_to context_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one P A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, context_t P1 P2 Q1 Q2 /\ bisim_up_to context_t P2 Q2 +))
context_reflexive < split.
Subgoal 1.1:
Variables: P A P1
CH : forall P, bisim_up_to context_t P P +
H1 : one P A P1
============================
one P A P1
Subgoal 1.2 is:
exists P2 Q2, context_t P1 P2 P1 Q2 /\ bisim_up_to context_t P2 Q2 +
Subgoal 2 is:
forall A Q1, one P A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, context_t P1 P2 Q1 Q2 /\ bisim_up_to context_t P2 Q2 +))
context_reflexive < search.
Subgoal 1.2:
Variables: P A P1
CH : forall P, bisim_up_to context_t P P +
H1 : one P A P1
============================
exists P2 Q2, context_t P1 P2 P1 Q2 /\ bisim_up_to context_t P2 Q2 +
Subgoal 2 is:
forall A Q1, one P A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, context_t P1 P2 Q1 Q2 /\ bisim_up_to context_t P2 Q2 +))
context_reflexive < witness P1.
Subgoal 1.2:
Variables: P A P1
CH : forall P, bisim_up_to context_t P P +
H1 : one P A P1
============================
exists Q2, context_t P1 P1 P1 Q2 /\ bisim_up_to context_t P1 Q2 +
Subgoal 2 is:
forall A Q1, one P A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, context_t P1 P2 Q1 Q2 /\ bisim_up_to context_t P2 Q2 +))
context_reflexive < witness P1.
Subgoal 1.2:
Variables: P A P1
CH : forall P, bisim_up_to context_t P P +
H1 : one P A P1
============================
context_t P1 P1 P1 P1 /\ bisim_up_to context_t P1 P1 +
Subgoal 2 is:
forall A Q1, one P A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, context_t P1 P2 Q1 Q2 /\ bisim_up_to context_t P2 Q2 +))
context_reflexive < split.
Subgoal 1.2.1:
Variables: P A P1
CH : forall P, bisim_up_to context_t P P +
H1 : one P A P1
============================
context_t P1 P1 P1 P1
Subgoal 1.2.2 is:
bisim_up_to context_t P1 P1 +
Subgoal 2 is:
forall A Q1, one P A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, context_t P1 P2 Q1 Q2 /\ bisim_up_to context_t P2 Q2 +))
context_reflexive < search.
Subgoal 1.2.2:
Variables: P A P1
CH : forall P, bisim_up_to context_t P P +
H1 : one P A P1
============================
bisim_up_to context_t P1 P1 +
Subgoal 2 is:
forall A Q1, one P A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, context_t P1 P2 Q1 Q2 /\ bisim_up_to context_t P2 Q2 +))
context_reflexive < backchain CH.
Subgoal 2:
Variables: P
CH : forall P, bisim_up_to context_t P P +
============================
forall A Q1, one P A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, context_t P1 P2 Q1 Q2 /\ bisim_up_to context_t P2 Q2 +))
context_reflexive < intros.
Subgoal 2:
Variables: P A Q1
CH : forall P, bisim_up_to context_t P P +
H1 : one P A Q1
============================
exists P1, one P A P1 /\
(exists P2 Q2, context_t P1 P2 Q1 Q2 /\ bisim_up_to context_t P2 Q2 +)
context_reflexive < witness Q1.
Subgoal 2:
Variables: P A Q1
CH : forall P, bisim_up_to context_t P P +
H1 : one P A Q1
============================
one P A Q1 /\
(exists P2 Q2, context_t Q1 P2 Q1 Q2 /\ bisim_up_to context_t P2 Q2 +)
context_reflexive < split.
Subgoal 2.1:
Variables: P A Q1
CH : forall P, bisim_up_to context_t P P +
H1 : one P A Q1
============================
one P A Q1
Subgoal 2.2 is:
exists P2 Q2, context_t Q1 P2 Q1 Q2 /\ bisim_up_to context_t P2 Q2 +
context_reflexive < search.
Subgoal 2.2:
Variables: P A Q1
CH : forall P, bisim_up_to context_t P P +
H1 : one P A Q1
============================
exists P2 Q2, context_t Q1 P2 Q1 Q2 /\ bisim_up_to context_t P2 Q2 +
context_reflexive < witness Q1.
Subgoal 2.2:
Variables: P A Q1
CH : forall P, bisim_up_to context_t P P +
H1 : one P A Q1
============================
exists Q2, context_t Q1 Q1 Q1 Q2 /\ bisim_up_to context_t Q1 Q2 +
context_reflexive < witness Q1.
Subgoal 2.2:
Variables: P A Q1
CH : forall P, bisim_up_to context_t P P +
H1 : one P A Q1
============================
context_t Q1 Q1 Q1 Q1 /\ bisim_up_to context_t Q1 Q1 +
context_reflexive < split.
Subgoal 2.2.1:
Variables: P A Q1
CH : forall P, bisim_up_to context_t P P +
H1 : one P A Q1
============================
context_t Q1 Q1 Q1 Q1
Subgoal 2.2.2 is:
bisim_up_to context_t Q1 Q1 +
context_reflexive < search.
Subgoal 2.2.2:
Variables: P A Q1
CH : forall P, bisim_up_to context_t P P +
H1 : one P A Q1
============================
bisim_up_to context_t Q1 Q1 +
context_reflexive < backchain CH.
Proof completed.
Abella < Theorem context_substitutive :
substitutive_rel (bisim_up_to context_t).
============================
substitutive_rel (bisim_up_to context_t)
context_substitutive < unfold.
============================
forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
context_substitutive < coinduction.
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
============================
forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 #
context_substitutive < intros.
Variables: P1 P2 C Q1 Q2
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
============================
bisim_up_to context_t Q1 Q2 #
context_substitutive < unfold.
Subgoal 1:
Variables: P1 P2 C Q1 Q2
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
============================
forall A P1, one Q1 A P1 ->
(exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < intros.
Subgoal 1:
Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q1 A P3
============================
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < apply ctx_faithful to H1 H4.
Subgoal 1:
Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q1 A P3
H5 : (exists CC, at CC P1 P3 /\
(forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR))) \/
(exists CC PBP B, one P1 B PBP /\ at CC PBP P3 /\
(forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 ->
(exists RR, one Q0 A RR /\ at CC QBQ RR)))) \/
(forall Q Q0, at C Q Q0 -> one Q0 A P3)
============================
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < case H5.
Subgoal 1.1:
Variables: P1 P2 C Q1 Q2 A P3 CC
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q1 A P3
H6 : at CC P1 P3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
============================
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 1.2 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 1.3 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < apply H7 to H2.
Subgoal 1.1:
Variables: P1 P2 C Q1 Q2 A P3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q1 A P3
H6 : at CC P1 P3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q2 A RR
H9 : at CC P2 RR
============================
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 1.2 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 1.3 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < witness RR.
Subgoal 1.1:
Variables: P1 P2 C Q1 Q2 A P3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q1 A P3
H6 : at CC P1 P3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q2 A RR
H9 : at CC P2 RR
============================
one Q2 A RR /\
(exists P2 Q4, context_t P3 P2 RR Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 1.2 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 1.3 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < split.
Subgoal 1.1.1:
Variables: P1 P2 C Q1 Q2 A P3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q1 A P3
H6 : at CC P1 P3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q2 A RR
H9 : at CC P2 RR
============================
one Q2 A RR
Subgoal 1.1.2 is:
exists P2 Q4, context_t P3 P2 RR Q4 /\ bisim_up_to context_t P2 Q4 +
Subgoal 1.2 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 1.3 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < search.
Subgoal 1.1.2:
Variables: P1 P2 C Q1 Q2 A P3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q1 A P3
H6 : at CC P1 P3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q2 A RR
H9 : at CC P2 RR
============================
exists P2 Q4, context_t P3 P2 RR Q4 /\ bisim_up_to context_t P2 Q4 +
Subgoal 1.2 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 1.3 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < witness P1.
Subgoal 1.1.2:
Variables: P1 P2 C Q1 Q2 A P3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q1 A P3
H6 : at CC P1 P3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q2 A RR
H9 : at CC P2 RR
============================
exists Q4, context_t P3 P1 RR Q4 /\ bisim_up_to context_t P1 Q4 +
Subgoal 1.2 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 1.3 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < witness P2.
Subgoal 1.1.2:
Variables: P1 P2 C Q1 Q2 A P3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q1 A P3
H6 : at CC P1 P3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q2 A RR
H9 : at CC P2 RR
============================
context_t P3 P1 RR P2 /\ bisim_up_to context_t P1 P2 +
Subgoal 1.2 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 1.3 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < split.
Subgoal 1.1.2.1:
Variables: P1 P2 C Q1 Q2 A P3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q1 A P3
H6 : at CC P1 P3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q2 A RR
H9 : at CC P2 RR
============================
context_t P3 P1 RR P2
Subgoal 1.1.2.2 is:
bisim_up_to context_t P1 P2 +
Subgoal 1.2 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 1.3 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < search.
Subgoal 1.1.2.2:
Variables: P1 P2 C Q1 Q2 A P3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q1 A P3
H6 : at CC P1 P3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q2 A RR
H9 : at CC P2 RR
============================
bisim_up_to context_t P1 P2 +
Subgoal 1.2 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 1.3 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < backchain CH.
Subgoal 1.2:
Variables: P1 P2 C Q1 Q2 A P3 CC PBP B
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
============================
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 1.3 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < case H3.
Subgoal 1.2:
Variables: P1 P2 C Q1 Q2 A P3 CC PBP B
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
============================
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 1.3 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < apply H9 to H6.
Subgoal 1.2:
Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P2 B Q3
H12 : context_t PBP P4 Q3 Q4
H13 : bisim_up_to context_t P4 Q4
============================
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 1.3 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < apply H8 to H11.
Subgoal 1.2:
Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P2 B Q3
H12 : context_t PBP P4 Q3 Q4
H13 : bisim_up_to context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
============================
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 1.3 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < apply H14 to H2.
Subgoal 1.2:
Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P2 B Q3
H12 : context_t PBP P4 Q3 Q4
H13 : bisim_up_to context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
============================
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 1.3 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < witness RR.
Subgoal 1.2:
Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P2 B Q3
H12 : context_t PBP P4 Q3 Q4
H13 : bisim_up_to context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
============================
one Q2 A RR /\
(exists P2 Q4, context_t P3 P2 RR Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 1.3 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < split.
Subgoal 1.2.1:
Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P2 B Q3
H12 : context_t PBP P4 Q3 Q4
H13 : bisim_up_to context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
============================
one Q2 A RR
Subgoal 1.2.2 is:
exists P2 Q4, context_t P3 P2 RR Q4 /\ bisim_up_to context_t P2 Q4 +
Subgoal 1.3 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < search.
Subgoal 1.2.2:
Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P2 B Q3
H12 : context_t PBP P4 Q3 Q4
H13 : bisim_up_to context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
============================
exists P2 Q4, context_t P3 P2 RR Q4 /\ bisim_up_to context_t P2 Q4 +
Subgoal 1.3 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < case H12.
Subgoal 1.2.2:
Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR C1
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P2 B Q3
H13 : bisim_up_to context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
H17 : at C1 P4 PBP
H18 : at C1 Q4 Q3
============================
exists P2 Q4, context_t P3 P2 RR Q4 /\ bisim_up_to context_t P2 Q4 +
Subgoal 1.3 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < apply concat_ctx2 to H17 H7 H18 H16.
Subgoal 1.2.2:
Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR C1 C3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P2 B Q3
H13 : bisim_up_to context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
H17 : at C1 P4 PBP
H18 : at C1 Q4 Q3
H19 : at C3 P4 P3
H20 : at C3 Q4 RR
============================
exists P2 Q4, context_t P3 P2 RR Q4 /\ bisim_up_to context_t P2 Q4 +
Subgoal 1.3 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < witness P4.
Subgoal 1.2.2:
Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR C1 C3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P2 B Q3
H13 : bisim_up_to context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
H17 : at C1 P4 PBP
H18 : at C1 Q4 Q3
H19 : at C3 P4 P3
H20 : at C3 Q4 RR
============================
exists Q4, context_t P3 P4 RR Q4 /\ bisim_up_to context_t P4 Q4 +
Subgoal 1.3 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < witness Q4.
Subgoal 1.2.2:
Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR C1 C3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P2 B Q3
H13 : bisim_up_to context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
H17 : at C1 P4 PBP
H18 : at C1 Q4 Q3
H19 : at C3 P4 P3
H20 : at C3 Q4 RR
============================
context_t P3 P4 RR Q4 /\ bisim_up_to context_t P4 Q4 +
Subgoal 1.3 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < split.
Subgoal 1.2.2.1:
Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR C1 C3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P2 B Q3
H13 : bisim_up_to context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
H17 : at C1 P4 PBP
H18 : at C1 Q4 Q3
H19 : at C3 P4 P3
H20 : at C3 Q4 RR
============================
context_t P3 P4 RR Q4
Subgoal 1.2.2.2 is:
bisim_up_to context_t P4 Q4 +
Subgoal 1.3 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < search.
Subgoal 1.2.2.2:
Variables: P1 P2 C Q1 Q2 A P3 CC PBP B Q3 P4 Q4 RR C1 C3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q1 A P3
H6 : one P1 B PBP
H7 : at CC PBP P3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P2 B Q3
H13 : bisim_up_to context_t P4 Q4
H14 : forall Q0, at C P2 Q0 -> (exists RR, one Q0 A RR /\ at CC Q3 RR)
H15 : one Q2 A RR
H16 : at CC Q3 RR
H17 : at C1 P4 PBP
H18 : at C1 Q4 Q3
H19 : at C3 P4 P3
H20 : at C3 Q4 RR
============================
bisim_up_to context_t P4 Q4 +
Subgoal 1.3 is:
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < backchain CH.
Subgoal 1.3:
Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q1 A P3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A P3
============================
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < apply H6 to H2.
Subgoal 1.3:
Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q1 A P3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A P3
H7 : one Q2 A P3
============================
exists Q3, one Q2 A Q3 /\
(exists P2 Q4, context_t P3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < witness P3.
Subgoal 1.3:
Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q1 A P3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A P3
H7 : one Q2 A P3
============================
one Q2 A P3 /\
(exists P2 Q4, context_t P3 P2 P3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < split.
Subgoal 1.3.1:
Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q1 A P3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A P3
H7 : one Q2 A P3
============================
one Q2 A P3
Subgoal 1.3.2 is:
exists P2 Q4, context_t P3 P2 P3 Q4 /\ bisim_up_to context_t P2 Q4 +
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < search.
Subgoal 1.3.2:
Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q1 A P3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A P3
H7 : one Q2 A P3
============================
exists P2 Q4, context_t P3 P2 P3 Q4 /\ bisim_up_to context_t P2 Q4 +
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < witness P3.
Subgoal 1.3.2:
Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q1 A P3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A P3
H7 : one Q2 A P3
============================
exists Q4, context_t P3 P3 P3 Q4 /\ bisim_up_to context_t P3 Q4 +
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < witness P3.
Subgoal 1.3.2:
Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q1 A P3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A P3
H7 : one Q2 A P3
============================
context_t P3 P3 P3 P3 /\ bisim_up_to context_t P3 P3 +
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < split.
Subgoal 1.3.2.1:
Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q1 A P3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A P3
H7 : one Q2 A P3
============================
context_t P3 P3 P3 P3
Subgoal 1.3.2.2 is:
bisim_up_to context_t P3 P3 +
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < search.
Subgoal 1.3.2.2:
Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q1 A P3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A P3
H7 : one Q2 A P3
============================
bisim_up_to context_t P3 P3 +
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < backchain CH.
Subgoal 1.3.2.2:
Variables: P1 P2 C Q1 Q2 A P3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q1 A P3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A P3
H7 : one Q2 A P3
============================
bisim_up_to context_t P3 P3
Subgoal 2 is:
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < backchain context_reflexive.
Subgoal 2:
Variables: P1 P2 C Q1 Q2
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
============================
forall A Q3, one Q2 A Q3 ->
(exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +))
context_substitutive < intros.
Subgoal 2:
Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q2 A Q3
============================
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < apply ctx_faithful to H2 H4.
Subgoal 2:
Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q2 A Q3
H5 : (exists CC, at CC P2 Q3 /\
(forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR))) \/
(exists CC PBP B, one P2 B PBP /\ at CC PBP Q3 /\
(forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 ->
(exists RR, one Q0 A RR /\ at CC QBQ RR)))) \/
(forall Q Q0, at C Q Q0 -> one Q0 A Q3)
============================
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < case H5.
Subgoal 2.1:
Variables: P1 P2 C Q1 Q2 A Q3 CC
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q2 A Q3
H6 : at CC P2 Q3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
============================
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2.2 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2.3 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < apply H7 to H1.
Subgoal 2.1:
Variables: P1 P2 C Q1 Q2 A Q3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q2 A Q3
H6 : at CC P2 Q3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q1 A RR
H9 : at CC P1 RR
============================
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2.2 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2.3 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < witness RR.
Subgoal 2.1:
Variables: P1 P2 C Q1 Q2 A Q3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q2 A Q3
H6 : at CC P2 Q3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q1 A RR
H9 : at CC P1 RR
============================
one Q1 A RR /\
(exists P2 Q4, context_t RR P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2.2 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2.3 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < split.
Subgoal 2.1.1:
Variables: P1 P2 C Q1 Q2 A Q3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q2 A Q3
H6 : at CC P2 Q3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q1 A RR
H9 : at CC P1 RR
============================
one Q1 A RR
Subgoal 2.1.2 is:
exists P2 Q4, context_t RR P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +
Subgoal 2.2 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2.3 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < search.
Subgoal 2.1.2:
Variables: P1 P2 C Q1 Q2 A Q3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q2 A Q3
H6 : at CC P2 Q3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q1 A RR
H9 : at CC P1 RR
============================
exists P2 Q4, context_t RR P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +
Subgoal 2.2 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2.3 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < witness P1.
Subgoal 2.1.2:
Variables: P1 P2 C Q1 Q2 A Q3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q2 A Q3
H6 : at CC P2 Q3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q1 A RR
H9 : at CC P1 RR
============================
exists Q4, context_t RR P1 Q3 Q4 /\ bisim_up_to context_t P1 Q4 +
Subgoal 2.2 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2.3 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < witness P2.
Subgoal 2.1.2:
Variables: P1 P2 C Q1 Q2 A Q3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q2 A Q3
H6 : at CC P2 Q3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q1 A RR
H9 : at CC P1 RR
============================
context_t RR P1 Q3 P2 /\ bisim_up_to context_t P1 P2 +
Subgoal 2.2 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2.3 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < split.
Subgoal 2.1.2.1:
Variables: P1 P2 C Q1 Q2 A Q3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q2 A Q3
H6 : at CC P2 Q3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q1 A RR
H9 : at CC P1 RR
============================
context_t RR P1 Q3 P2
Subgoal 2.1.2.2 is:
bisim_up_to context_t P1 P2 +
Subgoal 2.2 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2.3 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < search.
Subgoal 2.1.2.2:
Variables: P1 P2 C Q1 Q2 A Q3 CC RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q2 A Q3
H6 : at CC P2 Q3
H7 : forall Q Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC Q RR)
H8 : one Q1 A RR
H9 : at CC P1 RR
============================
bisim_up_to context_t P1 P2 +
Subgoal 2.2 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2.3 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < backchain CH.
Subgoal 2.2:
Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
============================
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2.3 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < case H3.
Subgoal 2.2:
Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
============================
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2.3 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < apply H10 to H6.
Subgoal 2.2:
Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P1 B P3
H12 : context_t P3 P4 PBP Q4
H13 : bisim_up_to context_t P4 Q4
============================
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2.3 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < apply H8 to H11.
Subgoal 2.2:
Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P1 B P3
H12 : context_t P3 P4 PBP Q4
H13 : bisim_up_to context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
============================
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2.3 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < apply H14 to H1.
Subgoal 2.2:
Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P1 B P3
H12 : context_t P3 P4 PBP Q4
H13 : bisim_up_to context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
============================
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2.3 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < witness RR.
Subgoal 2.2:
Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P1 B P3
H12 : context_t P3 P4 PBP Q4
H13 : bisim_up_to context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
============================
one Q1 A RR /\
(exists P2 Q4, context_t RR P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
Subgoal 2.3 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < split.
Subgoal 2.2.1:
Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P1 B P3
H12 : context_t P3 P4 PBP Q4
H13 : bisim_up_to context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
============================
one Q1 A RR
Subgoal 2.2.2 is:
exists P2 Q4, context_t RR P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +
Subgoal 2.3 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < search.
Subgoal 2.2.2:
Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P1 B P3
H12 : context_t P3 P4 PBP Q4
H13 : bisim_up_to context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
============================
exists P2 Q4, context_t RR P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +
Subgoal 2.3 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < case H12.
Subgoal 2.2.2:
Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR C1
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P1 B P3
H13 : bisim_up_to context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
H17 : at C1 P4 P3
H18 : at C1 Q4 PBP
============================
exists P2 Q4, context_t RR P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +
Subgoal 2.3 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < apply concat_ctx2 to H17 H16 H18 H7.
Subgoal 2.2.2:
Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR C1 C3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P1 B P3
H13 : bisim_up_to context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
H17 : at C1 P4 P3
H18 : at C1 Q4 PBP
H19 : at C3 P4 RR
H20 : at C3 Q4 Q3
============================
exists P2 Q4, context_t RR P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +
Subgoal 2.3 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < witness P4.
Subgoal 2.2.2:
Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR C1 C3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P1 B P3
H13 : bisim_up_to context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
H17 : at C1 P4 P3
H18 : at C1 Q4 PBP
H19 : at C3 P4 RR
H20 : at C3 Q4 Q3
============================
exists Q4, context_t RR P4 Q3 Q4 /\ bisim_up_to context_t P4 Q4 +
Subgoal 2.3 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < witness Q4.
Subgoal 2.2.2:
Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR C1 C3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P1 B P3
H13 : bisim_up_to context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
H17 : at C1 P4 P3
H18 : at C1 Q4 PBP
H19 : at C3 P4 RR
H20 : at C3 Q4 Q3
============================
context_t RR P4 Q3 Q4 /\ bisim_up_to context_t P4 Q4 +
Subgoal 2.3 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < split.
Subgoal 2.2.2.1:
Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR C1 C3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P1 B P3
H13 : bisim_up_to context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
H17 : at C1 P4 P3
H18 : at C1 Q4 PBP
H19 : at C3 P4 RR
H20 : at C3 Q4 Q3
============================
context_t RR P4 Q3 Q4
Subgoal 2.2.2.2 is:
bisim_up_to context_t P4 Q4 +
Subgoal 2.3 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < search.
Subgoal 2.2.2.2:
Variables: P1 P2 C Q1 Q2 A Q3 CC PBP B P3 P4 Q4 RR C1 C3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H4 : one Q2 A Q3
H6 : one P2 B PBP
H7 : at CC PBP Q3
H8 : forall Q QBQ, one Q B QBQ ->
(forall Q0, at C Q Q0 -> (exists RR, one Q0 A RR /\ at CC QBQ RR))
H9 : forall A P3, one P1 A P3 ->
(exists Q1, one P2 A Q1 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H10 : forall A Q1, one P2 A Q1 ->
(exists P3, one P1 A P3 /\
(exists P4 Q2, context_t P3 P4 Q1 Q2 /\
bisim_up_to context_t P4 Q2))
H11 : one P1 B P3
H13 : bisim_up_to context_t P4 Q4
H14 : forall Q0, at C P1 Q0 -> (exists RR, one Q0 A RR /\ at CC P3 RR)
H15 : one Q1 A RR
H16 : at CC P3 RR
H17 : at C1 P4 P3
H18 : at C1 Q4 PBP
H19 : at C3 P4 RR
H20 : at C3 Q4 Q3
============================
bisim_up_to context_t P4 Q4 +
Subgoal 2.3 is:
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < backchain CH.
Subgoal 2.3:
Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q2 A Q3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A Q3
============================
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < apply H6 to H1.
Subgoal 2.3:
Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q2 A Q3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A Q3
H7 : one Q1 A Q3
============================
exists P1, one Q1 A P1 /\
(exists P2 Q4, context_t P1 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < witness Q3.
Subgoal 2.3:
Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q2 A Q3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A Q3
H7 : one Q1 A Q3
============================
one Q1 A Q3 /\
(exists P2 Q4, context_t Q3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +)
context_substitutive < split.
Subgoal 2.3.1:
Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q2 A Q3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A Q3
H7 : one Q1 A Q3
============================
one Q1 A Q3
Subgoal 2.3.2 is:
exists P2 Q4, context_t Q3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +
context_substitutive < search.
Subgoal 2.3.2:
Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q2 A Q3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A Q3
H7 : one Q1 A Q3
============================
exists P2 Q4, context_t Q3 P2 Q3 Q4 /\ bisim_up_to context_t P2 Q4 +
context_substitutive < witness Q3.
Subgoal 2.3.2:
Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q2 A Q3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A Q3
H7 : one Q1 A Q3
============================
exists Q4, context_t Q3 Q3 Q3 Q4 /\ bisim_up_to context_t Q3 Q4 +
context_substitutive < witness Q3.
Subgoal 2.3.2:
Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q2 A Q3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A Q3
H7 : one Q1 A Q3
============================
context_t Q3 Q3 Q3 Q3 /\ bisim_up_to context_t Q3 Q3 +
context_substitutive < split.
Subgoal 2.3.2.1:
Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q2 A Q3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A Q3
H7 : one Q1 A Q3
============================
context_t Q3 Q3 Q3 Q3
Subgoal 2.3.2.2 is:
bisim_up_to context_t Q3 Q3 +
context_substitutive < search.
Subgoal 2.3.2.2:
Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q2 A Q3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A Q3
H7 : one Q1 A Q3
============================
bisim_up_to context_t Q3 Q3 +
context_substitutive < backchain CH.
Subgoal 2.3.2.2:
Variables: P1 P2 C Q1 Q2 A Q3
CH : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2 +
H1 : at C P1 Q1
H2 : at C P2 Q2
H3 : bisim_up_to context_t P1 P2
H4 : one Q2 A Q3
H6 : forall Q Q0, at C Q Q0 -> one Q0 A Q3
H7 : one Q1 A Q3
============================
bisim_up_to context_t Q3 Q3
context_substitutive < backchain context_reflexive.
Proof completed.
Abella < Theorem context_sound :
is_sound context_t.
============================
is_sound context_t
context_sound < apply context_substitutive.
H1 : substitutive_rel (bisim_up_to context_t)
============================
is_sound context_t
context_sound < case H1.
H2 : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
============================
is_sound context_t
context_sound < rename H2 to cs_lemma.
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
============================
is_sound context_t
context_sound < unfold.
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
============================
forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q
context_sound < coinduction.
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
============================
forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q #
context_sound < intros.
Variables: P Q
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H3 : bisim_up_to context_t P Q
============================
bisim_up_to refl_t P Q #
context_sound < case H3.
Variables: P Q
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
============================
bisim_up_to refl_t P Q #
context_sound < unfold.
Subgoal 1:
Variables: P Q
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
============================
forall A P1, one P A P1 ->
(exists Q1, one Q A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
context_sound < intros.
Subgoal 1:
Variables: P Q A P1
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H6 : one P A P1
============================
exists Q1, one Q A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
context_sound < apply H4 to H6.
Subgoal 1:
Variables: P Q A P1 Q2 P3 Q3
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H6 : one P A P1
H7 : one Q A Q2
H8 : context_t P1 P3 Q2 Q3
H9 : bisim_up_to context_t P3 Q3
============================
exists Q1, one Q A Q1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
context_sound < witness Q2.
Subgoal 1:
Variables: P Q A P1 Q2 P3 Q3
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H6 : one P A P1
H7 : one Q A Q2
H8 : context_t P1 P3 Q2 Q3
H9 : bisim_up_to context_t P3 Q3
============================
one Q A Q2 /\
(exists P2 Q1, refl_t P1 P2 Q2 Q1 /\ bisim_up_to refl_t P2 Q1 +)
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
context_sound < split.
Subgoal 1.1:
Variables: P Q A P1 Q2 P3 Q3
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H6 : one P A P1
H7 : one Q A Q2
H8 : context_t P1 P3 Q2 Q3
H9 : bisim_up_to context_t P3 Q3
============================
one Q A Q2
Subgoal 1.2 is:
exists P2 Q1, refl_t P1 P2 Q2 Q1 /\ bisim_up_to refl_t P2 Q1 +
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
context_sound < search.
Subgoal 1.2:
Variables: P Q A P1 Q2 P3 Q3
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H6 : one P A P1
H7 : one Q A Q2
H8 : context_t P1 P3 Q2 Q3
H9 : bisim_up_to context_t P3 Q3
============================
exists P2 Q1, refl_t P1 P2 Q2 Q1 /\ bisim_up_to refl_t P2 Q1 +
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
context_sound < witness P1.
Subgoal 1.2:
Variables: P Q A P1 Q2 P3 Q3
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H6 : one P A P1
H7 : one Q A Q2
H8 : context_t P1 P3 Q2 Q3
H9 : bisim_up_to context_t P3 Q3
============================
exists Q1, refl_t P1 P1 Q2 Q1 /\ bisim_up_to refl_t P1 Q1 +
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
context_sound < witness Q2.
Subgoal 1.2:
Variables: P Q A P1 Q2 P3 Q3
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H6 : one P A P1
H7 : one Q A Q2
H8 : context_t P1 P3 Q2 Q3
H9 : bisim_up_to context_t P3 Q3
============================
refl_t P1 P1 Q2 Q2 /\ bisim_up_to refl_t P1 Q2 +
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
context_sound < split.
Subgoal 1.2.1:
Variables: P Q A P1 Q2 P3 Q3
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H6 : one P A P1
H7 : one Q A Q2
H8 : context_t P1 P3 Q2 Q3
H9 : bisim_up_to context_t P3 Q3
============================
refl_t P1 P1 Q2 Q2
Subgoal 1.2.2 is:
bisim_up_to refl_t P1 Q2 +
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
context_sound < search.
Subgoal 1.2.2:
Variables: P Q A P1 Q2 P3 Q3
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H6 : one P A P1
H7 : one Q A Q2
H8 : context_t P1 P3 Q2 Q3
H9 : bisim_up_to context_t P3 Q3
============================
bisim_up_to refl_t P1 Q2 +
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
context_sound < case H8.
Subgoal 1.2.2:
Variables: P Q A P1 Q2 P3 Q3 C
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H6 : one P A P1
H7 : one Q A Q2
H9 : bisim_up_to context_t P3 Q3
H10 : at C P3 P1
H11 : at C Q3 Q2
============================
bisim_up_to refl_t P1 Q2 +
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
context_sound < apply cs_lemma to H10 H11 H9.
Subgoal 1.2.2:
Variables: P Q A P1 Q2 P3 Q3 C
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H6 : one P A P1
H7 : one Q A Q2
H9 : bisim_up_to context_t P3 Q3
H10 : at C P3 P1
H11 : at C Q3 Q2
H12 : bisim_up_to context_t P1 Q2
============================
bisim_up_to refl_t P1 Q2 +
Subgoal 2 is:
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
context_sound < backchain CH.
Subgoal 2:
Variables: P Q
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
============================
forall A Q1, one Q A Q1 ->
(exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +))
context_sound < intros.
Subgoal 2:
Variables: P Q A Q1
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H6 : one Q A Q1
============================
exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
context_sound < apply H5 to H6.
Subgoal 2:
Variables: P Q A Q1 P2 P3 Q3
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H6 : one Q A Q1
H7 : one P A P2
H8 : context_t P2 P3 Q1 Q3
H9 : bisim_up_to context_t P3 Q3
============================
exists P1, one P A P1 /\
(exists P2 Q2, refl_t P1 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +)
context_sound < witness P2.
Subgoal 2:
Variables: P Q A Q1 P2 P3 Q3
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H6 : one Q A Q1
H7 : one P A P2
H8 : context_t P2 P3 Q1 Q3
H9 : bisim_up_to context_t P3 Q3
============================
one P A P2 /\
(exists P1 Q2, refl_t P2 P1 Q1 Q2 /\ bisim_up_to refl_t P1 Q2 +)
context_sound < split.
Subgoal 2.1:
Variables: P Q A Q1 P2 P3 Q3
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H6 : one Q A Q1
H7 : one P A P2
H8 : context_t P2 P3 Q1 Q3
H9 : bisim_up_to context_t P3 Q3
============================
one P A P2
Subgoal 2.2 is:
exists P1 Q2, refl_t P2 P1 Q1 Q2 /\ bisim_up_to refl_t P1 Q2 +
context_sound < search.
Subgoal 2.2:
Variables: P Q A Q1 P2 P3 Q3
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H6 : one Q A Q1
H7 : one P A P2
H8 : context_t P2 P3 Q1 Q3
H9 : bisim_up_to context_t P3 Q3
============================
exists P1 Q2, refl_t P2 P1 Q1 Q2 /\ bisim_up_to refl_t P1 Q2 +
context_sound < witness P2.
Subgoal 2.2:
Variables: P Q A Q1 P2 P3 Q3
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H6 : one Q A Q1
H7 : one P A P2
H8 : context_t P2 P3 Q1 Q3
H9 : bisim_up_to context_t P3 Q3
============================
exists Q2, refl_t P2 P2 Q1 Q2 /\ bisim_up_to refl_t P2 Q2 +
context_sound < witness Q1.
Subgoal 2.2:
Variables: P Q A Q1 P2 P3 Q3
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H6 : one Q A Q1
H7 : one P A P2
H8 : context_t P2 P3 Q1 Q3
H9 : bisim_up_to context_t P3 Q3
============================
refl_t P2 P2 Q1 Q1 /\ bisim_up_to refl_t P2 Q1 +
context_sound < split.
Subgoal 2.2.1:
Variables: P Q A Q1 P2 P3 Q3
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H6 : one Q A Q1
H7 : one P A P2
H8 : context_t P2 P3 Q1 Q3
H9 : bisim_up_to context_t P3 Q3
============================
refl_t P2 P2 Q1 Q1
Subgoal 2.2.2 is:
bisim_up_to refl_t P2 Q1 +
context_sound < search.
Subgoal 2.2.2:
Variables: P Q A Q1 P2 P3 Q3
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H6 : one Q A Q1
H7 : one P A P2
H8 : context_t P2 P3 Q1 Q3
H9 : bisim_up_to context_t P3 Q3
============================
bisim_up_to refl_t P2 Q1 +
context_sound < case H8.
Subgoal 2.2.2:
Variables: P Q A Q1 P2 P3 Q3 C
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H6 : one Q A Q1
H7 : one P A P2
H9 : bisim_up_to context_t P3 Q3
H10 : at C P3 P2
H11 : at C Q3 Q1
============================
bisim_up_to refl_t P2 Q1 +
context_sound < apply cs_lemma to H10 H11 H9.
Subgoal 2.2.2:
Variables: P Q A Q1 P2 P3 Q3 C
cs_lemma : forall P1 P2 C Q1 Q2, at C P1 Q1 -> at C P2 Q2 ->
bisim_up_to context_t P1 P2 -> bisim_up_to context_t Q1 Q2
CH : forall P Q, bisim_up_to context_t P Q -> bisim_up_to refl_t P Q +
H4 : forall A P2, one P A P2 ->
(exists Q2, one Q A Q2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H5 : forall A Q2, one Q A Q2 ->
(exists P2, one P A P2 /\
(exists P3 Q3, context_t P2 P3 Q2 Q3 /\
bisim_up_to context_t P3 Q3))
H6 : one Q A Q1
H7 : one P A P2
H9 : bisim_up_to context_t P3 Q3
H10 : at C P3 P2
H11 : at C Q3 Q1
H12 : bisim_up_to context_t P2 Q1
============================
bisim_up_to refl_t P2 Q1 +
context_sound < backchain CH.
Proof completed.
Abella < Goodbye.
