[View ccs_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]

%%% Up-to-context technique

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.

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.

Theorem context_reflexive : forall P, bisim_up_to context_t P P.

Theorem context_substitutive : substitutive_rel (bisim_up_to context_t).

Theorem context_sound : is_sound context_t.