[View ccs_bisim_context.thm]

Click on a command or tactic to see a detailed view of its use.

Kind name,action,proc type.

Import "ccs_core". [View ccs_core]
Import "ccs_ctx". [View ccs_ctx]
Import "ccs_bisim". [View ccs_bisim]
Import "ccs_context". [View ccs_context]

Define bisim_context_t : proc -> proc -> proc -> proc -> prop by
  bisim_context_t P1 P3 Q1 Q3 :=
    exists P2 Q2, bisim_t P1 P2 Q1 Q2 /\ context_t P2 P3 Q2 Q3.

Theorem bisim_context_t_reflexive : forall P, bisim_context_t P P P P.

Theorem bisim_context_reflexive : forall P, bisim_up_to bisim_context_t P P.

Theorem bisim_context_t_contexts : forall C P1 P2 Q1 Q2,
  at C P2 P1 -> at C Q2 Q1 ->
  bisim_context_t P1 P2 Q1 Q2.

Theorem bisim_substitutive_ : forall C P1 Q1 P2 Q2,
  at C P1 Q1 -> at C P2 Q2 ->
  bisim_up_to refl_t P1 P2 ->
  bisim_up_to refl_t Q1 Q2.

Theorem ctx_mirror : forall C P1 P2 Q1, at C P1 P2 -> exists Q2, at C Q1 Q2.

Theorem bisim_context_substitutive : substitutive_rel (bisim_up_to bisim_context_t).

Theorem bisim_context_sound_fst : is_sound_fst bisim_context_t.

Theorem bisim_context_sound_snd : is_sound_snd bisim_context_t.

Theorem bisim_context_sound : is_sound bisim_context_t.