% Specification of late pi-calculus and strong bisimulation
% 
% Please refer to the following paper for background:
%
% Alwen Tiu and Dale Miller. A proof search specification of 
% the pi-calculus. Proceedings of FGUC04. 
% Available from http://www.loria.fr/~tiu


% bound input
onep (in X M) (dn X) M := true.

% free output
one  (out X Y P) (up X Y) P := true.

% tau 
one  (taup P) tau P := true.

% match prefix
one  (match X X P) A Q := one P A Q.
onep (match X X P) A M := onep P A M.

% sum
one  (plus P Q) A R := one P A R.
one  (plus P Q) A R := one Q A R.
onep (plus P Q) A M := onep P A M.
onep (plus P Q) A M := onep Q A M.

% par
one  (par P Q) A (par P1 Q) := one P A P1.
one  (par P Q) A (par P Q1) := one Q A Q1.
onep (par P Q) A (x\par (M x) Q) := onep P A M.
onep (par P Q) A (x\par P (N x)) := onep Q A N.

% restriction
one  (nu x\P x) A (nu x\Q x) :=  nabla x\ one (P x) A (Q x).
onep  (nu x\P x) A (y\ nu x\Q x y) := nabla x\ onep (P x) A (y\ Q x y).

% open 
onep  (nu y\M y) (up X) N := nabla y\ one (M y) (up X y) (N y).

% close

one (par P Q) tau (nu y\ par (M y) (N y)) := 
   sigma X\ onep P (dn X) M & onep Q (up X) N.
one (par P Q) tau (nu y\ par (M y) (N y)) :=
   sigma X\ onep P (up X) M & onep Q (dn X) N.

% comm

one (par P Q) tau (par R T) :=
	sigma X\ sigma Y\ sigma M\ onep P (dn X) M & one Q (up X Y) T & (R = (M Y)).
	
one (par P Q) tau (par R T) :=
    sigma X\ sigma Y\ sigma M\ onep Q (dn X) M & one P (up X Y) R & (T = (M Y)).

% Rep-act

one (bang P) A (par P1 (bang P)) := one P A P1.
onep (bang P) X (y\ par (M y) (bang P)) := onep P X M.

% Rep-com

one (bang P) tau (par (par R T) (bang P)) :=
    sigma X\ sigma Y\ sigma M\ onep P (dn X) M & one P (up X Y) R & (T = (M Y)).

% Rep-close
one (bang P) tau (par (nu y\ par (M y) (N y)) (bang P)) := 
    sigma X\ onep P (up X) M & onep P (dn X) N.

     
sim P Q := 
	(pi A\ pi P1\ one P A P1 => sigma Q1\ one Q A Q1 & sim P1 Q1) &
	(pi X\ pi M\ onep P (dn X) M => sigma N\ onep Q (dn X) N & 
					pi w\ sim (M w) (N w)) &
	(pi X\ pi M\ onep P (up X) M => sigma N\ onep Q (up X) N &
					nabla w\ sim (M w) (N w)).

bisim P Q :=
	(pi A\ pi P1\ one P A P1 => sigma Q1\ one Q A Q1 & bisim P1 Q1) &
	(pi X\ pi M\ onep P (dn X) M => sigma N\ onep Q (dn X) N & 
					pi w\ bisim (M w) (N w)) &
	(pi X\ pi M\ onep P (up X) M => sigma N\ onep Q (up X) N &
					nabla w\ bisim (M w) (N w)) &
	(pi A\ pi Q1\ one Q A Q1 => sigma P1\ one P A P1 & bisim Q1 P1) &
	(pi X\ pi N\ onep Q (dn X) N => sigma M\ onep P (dn X) M & 
					pi w\ bisim (N w) (M w)) &
	(pi X\ pi N\ onep Q (up X) N => sigma M\ onep P (up X) M &
					nabla w\ bisim (N w) (M w)).


example 0 (nu x\ match x a (taup z)).
example 1 (par (in x y\z) (out x a z)).
example 2 (plus (in x y\out x a) (out x a (in x y\z))).
example 3 (in x u\ (plus (taup (taup z)) (taup z))) := true.
example 4 (in x u\ (plus (taup (taup z)) (plus (taup z) (taup (match u y (taup z)))))).
example 5 (nu a\ (par (in x y\z) (out x a z))).
example 6 (nu a\ (plus (in x y\out x a) (out x a (in x y\z)))).
example 7 (taup z).
example 8 (nu x\ (par (in x y\z) (out x a z))).
example 9 (nu x\ out a x z).
example 10 (par (in x y\ z) (nu y\ out x y z)).
example 11 (in x u\ nu y\ ((plus (taup (taup z)) (plus (taup z) (taup (match u y (taup z))))))).
example 12 (bang P) := example 1 P.