Conjectura
Sign inRegister
Beta.Proofs cannot be submitted yet. The corpus is open to read, and we are looking for researchers to maintain a subject area.Maintaining a field →

Deterministic system

Conjectura.Defs.ComputerScience.Semantics.Deterministic

/-
Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Fabrizio Montesi
-/
import Conjectura.Defs.ComputerScience.Semantics.LabelledTransitionSystem

/-! # Deterministic system

## Source

Adapted for Conjectura from [cslib](https://github.com/leanprover/cslib), split into one concept per module. Released by its authors under Apache 2.0.
-/

namespace Conjectura.Semantics

/-- An LTS is **deterministic** when each state has at most one successor per label, so the
label alone determines what happens next. -/
def LTS.Deterministic {State Label : Type*} (lts : LTS State Label) : Prop :=
  ∀ s μ s₁ s₂, lts.Tr s μ s₁ → lts.Tr s μ s₂ → s₁ = s₂

end Conjectura.Semantics