Basic theorems for parallel processes in timed $ mu $ CRL

Timed $mucrl$ is a process algebra-based formalism for the specification and verification of parallel, communicating systems with explicit time cite{Gr97. In this paper various basic results are derived, such as theorems for {it basic forms/, the expansion of terms with operators for parallelism, elimination of parallelism, and commutativity and associativity of the merge and communication merge (the operators $|$ and $|$). The interpretation of the operators, in particular the left merge, is far from trivial, and more in general, it has to be stated that working with a time-based formalism such as timed $mucrl$ can be fairly complicated. Therefore we pay a lot of attention to all kinds of proof details that could enhance the understanding -- and thus facilitate the use -- of the formalism. Many basic lemmas are included, and examples are used to illustrate the intuition behind the various results.