3.5. Engine Processing🔗

The S-Process rule (MailboxActors.OpStep.sProcess) is the composite rule for a single processing step: a busy engine evaluates its behaviour via EvalStep, executes the resulting effect via EffectEvalStep, and resolves its post-processing status.

MailboxActors.ProcessStep mirrors S-Process as a standalone proposition for use in property proofs.

The top-level reduction relation MailboxActors.SysStep is the existential: ∃ op, OpStep κ op κ'.