We will see more of this in a later example. Now this as all process algebras - the p-calculus has also a lable transition system - but as you see, the operation semantics when you view it is a transition system, is much more elaborate than in the previews styles, so, for instance, you have to introduce a number of rules like the open, reading rule, and the closing rule which tell you how to capture the behaviour of these local variables.