Executable Specification

[View processes_terms.sig] [View processes_terms.mod]
sig processes_terms.

kind pt type.

%lsc terms
type abs (pt -> pt) -> pt.
type app pt -> pt -> pt.
type subex (pt -> pt) -> pt -> pt.

%pi-calculus terms
type null       pt.
type nu 	(pt -> pt) -> pt.
type par	pt -> pt -> pt.
type out	pt -> pt -> pt.
type out2	pt -> pt -> pt -> pt.
type in		pt -> (pt -> pt) -> pt.
type in2 	pt -> (pt -> pt -> pt) -> pt.
module processes_terms.

Reasoning

[View trans.thm]

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

Specification "processes_terms".

Define trans : pt -> (pt -> pt) -> prop by
   nabla x, trans x (out x)
;  trans (app U V) a\nu b\nu x\par (P b) (par (out2 b x a) (in x Q))
      := trans U P /\ trans V Q
;  trans (abs U) a\in2 a P := nabla x, trans (U x) (P x)
;  trans (subex U V) a\nu x\par (P x a) (in x Q)
      := (nabla y, trans (U y) (P y)) /\ trans V Q.

Theorem trans_fonc : forall U P Q,
  trans U P -> trans U Q -> P = Q.