Mix Rule and Girardian Turnstile

One request and one question:

1. The request is for the "official" LaTeX macro for the Girardian turnstile.

2. The question is about the MIX rule

	/-  A      /- B
           /- A par B

that Girard mentions.  What are the consequences of having such
a rule (other than   A tensor B  -o  A par B)?  Has anyone used
the MIX rule to explain parallel composition of process calculi such
as CCS, particularly the way the parallel composition operator
(CCS |) is used to represent both connected and unconnected concurrency?

How would the MIX rule be rendered in LU?  Am I right in 
conjecturing the following?

	; Gamma' /- Delta' ; A		; Gamma' /- Delta' ; B
			; Gamma' /- Delta' ;  A par B

Thanks in advance for any insights.

- Sanjiva	(sanjiva@ecrc.de)

PS: I'm quite new to linear logic, and I'm interested more in
proof assignment than in proof search.