1.7. Behaviours🔗

A MailboxActors.Behaviour is a list of guarded actions.

MailboxActors.NonOverlappingGuards is the key structural property: for any input, at most one guarded action's guard succeeds. This ensures determinism of behaviour evaluation (Proposition 3).

A MailboxActors.WellFormedBehaviour bundles the action list with a proof of non-overlapping guards, so downstream theorems never need NonOverlappingGuards as a separate hypothesis.