Require Export ABP.ABP.BISIMULATION.Protocol.











Notation UTrans := (UnrelProcTrans Channel Act) (only parsing).

Notation STrans := (SafeProcTrans Channel Act del) (only parsing).


Definition Trans (c : Channel) :=
  match c return (Process → Action c → Process → Prop) with
  | lnk1 ⇒ UnrelProcTrans Channel Act lnk1
  | lnk2 ⇒ UnrelProcTrans Channel Act lnk2
  | del ⇒ SafeProcTrans Channel Act del
  end.


Lemma compare : ∀ c1 c2 : Channel, {c1 = c2} + {c1 ≠ c2}.
simple destruct c1.
simple destruct c2.
left; try trivial.
right; red in |- *; intros H; discriminate H.
right; red in |- *; intros H; discriminate H.
simple destruct c2.
right; red in |- *; intros H; discriminate H.
left; trivial.
right; red in |- *; intros H; discriminate H.
simple destruct c2.
right; red in |- *; intros H; discriminate H.
right; red in |- *; intros H; discriminate H.
left; trivial.
Defined.


Definition Silent (c : Channel) (w : Signal _ Act c) :=
  match c with
  | lnk1 ⇒ True
  | lnk2 ⇒ True
  | del ⇒ False
  end.