4.3. Effect Determinism (Proposition 3)🔗

@MailboxActors.effectDeterminism : ∀ [inst : MailboxActors.EngineSpec] (i : MailboxActors.EngineSpec.EngIdx)
  (p : MailboxActors.Engine i) (v : MailboxActors.EngineSpec.MsgType i) (E₁ E₂ : MailboxActors.Effect i),
  MailboxActors.EvalStep i p v E₁ → MailboxActors.EvalStep i p v E₂ → E₁ = E₂#check @MailboxActors.effectDeterminism

Under non-overlapping guards, the effect produced by behaviour evaluation is unique. The NonOverlappingGuards proof is embedded in WellFormedBehaviour, so no explicit hypothesis is needed.

The proof case-splits on both EvalStep derivations. When two different guards appear to match (guardStrategy/guardStrategy), the non-overlapping invariant forces one to produce noop, yielding a contradiction.