We shall only consider finite processes (processes without recursive definitions)
- a limited handling of recursion is possible
- deciding bisimilarity for general processes is undecidable

Inference system = axioms + inference rules
- soundness;