All operations that we plan to define for a telephone net will share certain properties. We capture these once and for all in the schema Event, which states that an operation will not disconnect any connections provided they are still requested after the operation.
The operation Call adds a request to the set of requests of a telephone net.
Given the maximality constraint on TN it is possible to infer from this operation that if neither phone is already connected, the request will be connected. (Exercise for the reader.)
The next operation, Hangup, terminates a connnection (if any) involving the phone ph?.
Finally, we define an operation Busy, which tells whether a phone is involved in a connection.
It is possible to show that cons does not change as a result of this operation. (Exercise for the reader.)