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 →

Reachability

Conjectura.Defs.ComputerScience.Semantics.Reachable

/-
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
import Mathlib.Logic.Relation

/-! # Reachability

## 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

/-- A state is **reachable** from another when some finite sequence of labelled transitions
leads from the first to the second, whatever labels are used along the way. -/
def LTS.Reachable {State Label : Type*} (lts : LTS State Label) (s t : State) : Prop :=
  Relation.ReflTransGen (fun a b => ∃ μ : Label, lts.Tr a μ b) s t

end Conjectura.Semantics