Section Processes.

Variable Chnl : Set.
Variable A : Chnl → Set.

CoInductive Guarded : Set :=
  | TALK :
      ∀ c1 : Chnl,
      A c1 → Guarded → ∀ c2 : Chnl, (A c2 → Guarded) → Guarded
  | LISTEN : ∀ c : Chnl, (A c → Guarded) → Guarded.

Inductive Process : Set :=
  | INJ : Guarded → Process
  | PAR : Process → Process → Process.

Coercion INJ : Guarded >-> Process.


Section Semantics.

Variable c : Chnl.

Inductive Signal : Set :=
  | Noise : Signal
  | Clear : A c → Signal.

Inductive Action : Set :=
  | Transmit : Signal → Action
  | Receive : A c → Action.

Coercion Transmit : Signal >-> Action.

 Inductive SafeProcTrans : Process → Action → Process → Prop :=
   | sttalk1 :
       ∀ (v : A c) (c2 : Chnl) (f : A c2 → Guarded) (p : Guarded),
       SafeProcTrans (TALK c v p c2 f) (Clear v) p
   | sttalk2 :
       ∀ (c1 : Chnl) (v1 : A c1) (f : A c → Guarded)
         (p1 p2 : Guarded) (v : A c),
       f v = p2 → SafeProcTrans (TALK c1 v1 p1 c f) (Receive v) p2
   | sttalk3 :
       ∀ (c1 c2 : Chnl) (v1 : A c1) (f : A c2 → Guarded)
         (p : Guarded) (v2 : A c),
       c2 ≠ c →
       SafeProcTrans (TALK c1 v1 p c2 f) (Receive v2) (TALK c1 v1 p c2 f)
   | stlisten1 :
       ∀ (f : A c → Guarded) (v : A c) (p1 p2 : Guarded),
       f v = p2 → SafeProcTrans (LISTEN c f) (Receive v) p2
   | stlisten2 :
       ∀ (d : Chnl) (f : A d → Guarded) (v : A c),
       d ≠ c → SafeProcTrans (LISTEN d f) (Receive v) (LISTEN d f)
   | stpar1 :
       ∀ (p1 p2 p3 p4 : Process) (v : A c),
       SafeProcTrans p1 (Transmit (Clear v)) p2 →
       SafeProcTrans p3 (Receive v) p4 →
       SafeProcTrans (PAR p1 p3) (Clear v) (PAR p2 p4)
   | stpar2 :
       ∀ (p1 p2 p3 p4 : Process) (v : A c),
       SafeProcTrans p1 (Receive v) p2 →
       SafeProcTrans p3 (Clear v) p4 →
       SafeProcTrans (PAR p1 p3) (Clear v) (PAR p2 p4)
   | stpar3 :
       ∀ (p1 p2 p3 p4 : Process) (v : A c),
       SafeProcTrans p1 (Receive v) p2 →
       SafeProcTrans p3 (Receive v) p4 →
       SafeProcTrans (PAR p1 p3) (Receive v) (PAR p2 p4).


 Inductive UnrelProcTrans : Process → Action → Process → Prop :=
   | uttalk1 :
       ∀ (v : A c) (c2 : Chnl) (f : A c2 → Guarded) (p : Guarded),
       UnrelProcTrans (TALK c v p c2 f) (Clear v) p
   | uttalk2 :
       ∀ (c1 : Chnl) (v1 : A c1) (f : A c → Guarded)
         (p1 p2 : Guarded) (v : A c),
       f v = p2 → UnrelProcTrans (TALK c1 v1 p1 c f) (Receive v) p2
   | uttalk3 :
       ∀ (c1 : Chnl) (v1 : A c1) (c2 : Chnl) (f : A c2 → Guarded)
         (p : Guarded) (v2 : A c),
       c2 ≠ c →
       UnrelProcTrans (TALK c1 v1 p c2 f) (Receive v2) (TALK c1 v1 p c2 f)
   | uttalk4 :
       ∀ (v : A c) (c2 : Chnl) (f : A c2 → Guarded) (p : Guarded),
       UnrelProcTrans (TALK c v p c2 f) Noise p
   | utlisten1 :
       ∀ (f : A c → Guarded) (v : A c) (p : Guarded),
       f v = p → UnrelProcTrans (LISTEN c f) (Receive v) p
   | utlisten2 :
       ∀ (d : Chnl) (f : A d → Guarded) (v : A c),
       d ≠ c → UnrelProcTrans (LISTEN d f) (Receive v) (LISTEN d f)
   | utpar1 :
       ∀ (p1 p2 p3 p4 : Process) (v : A c),
       UnrelProcTrans p1 (Clear v) p2 →
       UnrelProcTrans p3 (Receive v) p4 →
       UnrelProcTrans (PAR p1 p3) (Clear v) (PAR p2 p4)
   | utpar2 :
       ∀ (p1 p2 p3 p4 : Process) (v : A c),
       UnrelProcTrans p1 (Receive v) p2 →
       UnrelProcTrans p3 (Clear v) p4 →
       UnrelProcTrans (PAR p1 p3) (Clear v) (PAR p2 p4)
   | utpar3 :
       ∀ (p1 p2 p3 p4 : Process) (v : A c),
       UnrelProcTrans p1 (Receive v) p2 →
       UnrelProcTrans p3 (Receive v) p4 →
       UnrelProcTrans (PAR p1 p3) (Receive v) (PAR p2 p4)
   | utpar4 :
       ∀ p1 p2 p3 p4 : Process,
       UnrelProcTrans p1 Noise p2 →
       UnrelProcTrans (PAR p1 p3) Noise (PAR p2 p4)
   | utpar5 :
       ∀ p1 p2 p3 p4 : Process,
       UnrelProcTrans p3 Noise p4 →
       UnrelProcTrans (PAR p1 p3) Noise (PAR p2 p4).

End Semantics.

End Processes.