Labelled Transition System (LTS)

A Labelled Transition System (LTS) models the observable behaviour of the possible states of a system. They are particularly popular in the fields of concurrency theory, logic, and programming languages.

Main definitions

• LTS is a structure for labelled transition systems, consisting of a labelled transition relation Tr between states. We follow the style and conventions in [San].

• LTS.MTr extends the transition relation of any LTS to a multi-step transition relation, formalising the inference system and admissible rules for such relations in [Mon23].

• Definitions for all the common classes of LTSs: image-finite, finitely branching, finite-state, finite, and deterministic.

Main statements

• A series of results on LTS.MTr that allow for obtaining and composing multi-step transitions in different ways.

• LTS.deterministic_imageFinite: every deterministic LTS is also image-finite.

• LTS.finiteState_imageFinite: every finite-state LTS is also image-finite.

• LTS.finiteState_finitelyBranching: every finite-state LTS is also finitely-branching, if the type of labels is finite.

References

• F. Montesi, Introduction to Choreographies
• D. Sangiorgi, Introduction to Bisimulation and Coinduction

structure Cslib.LTS (State : Type u) (Label : Type v) : Type (max u v)

A Labelled Transition System (LTS) for a type of states (State) and a type of transition labels (Label) consists of a labelled transition relation (Tr).

• Tr : State → Label → State → Prop

  The transition relation.

Multi-step transitions

inductive Cslib.LTS.MTr {State : Type u} {Label : Type v} (lts : LTS State Label) : State → List Label → State → Prop

Definition of a multi-step transition.

(Implementation note: compared to [Mon23], we choose stepL instead of stepR as fundamental rule. This makes working with lists of labels more convenient, because we follow the same construction. It is also similar to what is done in the SimpleGraph library in mathlib.)

• refl {State : Type u} {Label : Type v} {lts : LTS State Label} {s : State} : lts.MTr s [] s
• stepL {State : Type u} {Label : Type v} {lts : LTS State Label} {s1 : State} {μ : Label} {s2 : State} {μs : List Label} {s3 : State} : lts.Tr s1 μ s2 → lts.MTr s2 μs s3 → lts.MTr s1 (μ :: μs) s3

theorem Cslib.LTS.MTr.single {State : Type u} {Label : Type v} (lts : LTS State Label) {s1 : State} {μ : Label} {s2 : State} : lts.Tr s1 μ s2 → lts.MTr s1 [μ] s2

Any transition is also a multi-step transition.

theorem Cslib.LTS.MTr.stepR {State : Type u} {Label : Type v} (lts : LTS State Label) {s1 : State} {μs : List Label} {s2 : State} {μ : Label} {s3 : State} : lts.MTr s1 μs s2 → lts.Tr s2 μ s3 → lts.MTr s1 (μs ++ [μ]) s3

Any multi-step transition can be extended by adding a transition.

theorem Cslib.LTS.MTr.comp {State : Type u} {Label : Type v} (lts : LTS State Label) {s1 : State} {μs1 : List Label} {s2 : State} {μs2 : List Label} {s3 : State} : lts.MTr s1 μs1 s2 → lts.MTr s2 μs2 s3 → lts.MTr s1 (μs1 ++ μs2) s3

Multi-step transitions can be composed.

theorem Cslib.LTS.MTr.single_invert {State : Type u} {Label : Type v} (lts : LTS State Label) (s1 : State) (μ : Label) (s2 : State) : lts.MTr s1 [μ] s2 → lts.Tr s1 μ s2

Any 1-sized multi-step transition implies a transition with the same states and label.

theorem Cslib.LTS.MTr.nil_eq {State : Type u} {Label : Type v} (lts : LTS State Label) {s1 s2 : State} (h : lts.MTr s1 [] s2) : s1 = s2

In any zero-steps multi-step transition, the origin and the derivative are the same.

def Cslib.LTS.CanReach {State : Type u} {Label : Type v} (lts : LTS State Label) (s1 s2 : State) : Prop

A state s1 can reach a state s2 if there exists a multi-step transition from s1 to s2.

Equations

• lts.CanReach s1 s2 = ∃ (μs : List Label), lts.MTr s1 μs s2

theorem Cslib.LTS.CanReach.refl {State : Type u} {Label : Type v} (lts : LTS State Label) (s : State) : lts.CanReach s s

Any state can reach itself.

def Cslib.LTS.generatedBy {State : Type u} {Label : Type v} (lts : LTS State Label) (s : State) : LTS { s' : State // lts.CanReach s s' } Label

The LTS generated by a state s is the LTS given by all the states reachable from s.

Equations

• One or more equations did not get rendered due to their size.

Definitions about termination

def Cslib.LTS.MayTerminate {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) {Terminated : State → Prop} (s : State) : Prop

A state 'may terminate' if it can reach a terminated state. The definition of Terminated is a parameter.

Equations

• lts.MayTerminate s = ∃ (s' : State), Terminated s' ∧ lts.CanReach s s'

def Cslib.LTS.Stuck {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) {Terminated : State → Prop} (s : State) : Prop

A state 'is stuck' if it is not terminated and cannot go forward. The definition of Terminated is a parameter.

Equations

• lts.Stuck s = (¬Terminated s ∧ ¬∃ (μ : Label) (s' : State), lts.Tr s μ s')

Definitions for the unions of LTSs

Note: there is a nontrivial balance between ergonomics and generality here. These definitions might change in the future.

def Cslib.LTS.union {State : Type u} {Label : Type v} (lts1 lts2 : LTS State Label) : LTS State Label

The union of two LTSs defined on the same types.

Equations

• lts1.union lts2 = { Tr := lts1.Tr ⊔ lts2.Tr }

def Cslib.LTS.unionSubtype {State : Type u} {Label : Type v} {S1 : State → Prop} {L1 : Label → Prop} {S2 : State → Prop} {L2 : Label → Prop} [DecidablePred S1] [DecidablePred L1] [DecidablePred S2] [DecidablePred L2] (lts1 : LTS (Subtype S1) (Subtype L1)) (lts2 : LTS (Subtype S2) (Subtype L2)) : LTS State Label

The union of two LTSs that have common supertypes for states and labels.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.LTS.inl {State : Type u} {Label : Type v} {State' : Type u_1} (lts : LTS State Label) : LTS { x : State ⊕ State' // x.isLeft = true } { _label : Label // True }

Lifting of an LTS State Label to LTS (State ⊕ State') Label.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.LTS.inr {State : Type u} {Label : Type v} {State' : Type u_1} (lts : LTS State Label) : LTS { x : State' ⊕ State // x.isRight = true } { _label : Label // True }

Lifting of an LTS State Label to LTS (State' ⊕ State) Label.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.LTS.unionSum {Label : Type v} {State1 : Type u_1} {State2 : Type u_2} (lts1 : LTS State1 Label) (lts2 : LTS State2 Label) : LTS (State1 ⊕ State2) Label

Union of two LTSs with the same Label type. The result combines the original respective state types State1 and State2 into (State1 ⊕ State2).

Equations

• lts1.unionSum lts2 = lts1.inl.unionSubtype lts2.inr

Classes of LTSs

class Cslib.LTS.Deterministic {State : Type u} {Label : Type v} (lts : LTS State Label) : Prop

An lts is deterministic if a state cannot reach different states with the same transition label.

• deterministic (s1 : State) (μ : Label) (s2 s3 : State) : lts.Tr s1 μ s2 → lts.Tr s1 μ s3 → s2 = s3

def Cslib.LTS.image {State : Type u} {Label : Type v} (lts : LTS State Label) (s : State) (μ : Label) : Set State

The μ-image of a state s is the set of all μ-derivatives of s.

Equations

• lts.image s μ = {s' : State | lts.Tr s μ s'}

def Cslib.LTS.imageMultistep {State : Type u} {Label : Type v} (lts : LTS State Label) (s : State) (μs : List Label) : Set State

The μs-image of a state s, where μs is a list of labels, is the set of all μs-derivatives of s.

Equations

• lts.imageMultistep s μs = {s' : State | lts.MTr s μs s'}

def Cslib.LTS.setImage {State : Type u} {Label : Type v} (lts : LTS State Label) (S : Set State) (μ : Label) : Set State

The μ-image of a set of states S is the union of all μ-images of the states in S.

Equations

• lts.setImage S μ = ⋃ s ∈ S, lts.image s μ

def Cslib.LTS.setImageMultistep {State : Type u} {Label : Type v} (lts : LTS State Label) (S : Set State) (μs : List Label) : Set State

The μs-image of a set of states S, where μs is a list of labels, is the union of all μs-images of the states in S.

Equations

• lts.setImageMultistep S μs = ⋃ s ∈ S, lts.imageMultistep s μs

theorem Cslib.LTS.mem_setImage {State : Type u} {Label : Type v} {S : Set State} {μ : Label} {s' : State} {lts : LTS State Label} : s' ∈ lts.setImage S μ ↔ ∃ s ∈ S, lts.Tr s μ s'

Characterisation of setImage wrt Tr.

theorem Cslib.LTS.tr_setImage {State : Type u} {Label : Type v} {S : Set State} {s : State} {μ : Label} {s' : State} {lts : LTS State Label} (hs : s ∈ S) (htr : lts.Tr s μ s') : s' ∈ lts.setImage S μ

theorem Cslib.LTS.mem_setImageMultistep {State : Type u} {Label : Type v} {S : Set State} {μs : List Label} {s' : State} {lts : LTS State Label} : s' ∈ lts.setImageMultistep S μs ↔ ∃ s ∈ S, lts.MTr s μs s'

Characterisation of setImageMultistep with MTr.

theorem Cslib.LTS.mTr_setImage {State : Type u} {Label : Type v} {S : Set State} {s : State} {μs : List Label} {s' : State} {lts : LTS State Label} (hs : s ∈ S) (htr : lts.MTr s μs s') : s' ∈ lts.setImageMultistep S μs

theorem Cslib.LTS.setImage_empty {State : Type u} {Label : Type v} {μ : Label} (lts : LTS State Label) : lts.setImage ∅ μ = ∅

The image of the empty set is always the empty set.

theorem Cslib.LTS.setImageMultistep_setImage_head {State : Type u} {Label : Type v} {S : Set State} {μ : Label} {μs : List Label} (lts : LTS State Label) : lts.setImageMultistep S (μ :: μs) = lts.setImageMultistep (lts.setImage S μ) μs

theorem Cslib.LTS.setImageMultistep_foldl_setImage {State : Type u} {Label : Type v} (lts : LTS State Label) : lts.setImageMultistep = List.foldl lts.setImage

Characterisation of LTS.setImageMultistep as List.foldl on LTS.setImage.

theorem Cslib.LTS.mem_foldl_setImage {State : Type u} {Label : Type v} {S : Set State} {μs : List Label} {s' : State} (lts : LTS State Label) : s' ∈ List.foldl lts.setImage S μs ↔ ∃ s ∈ S, lts.MTr s μs s'

Characterisation of membership in List.foldl lts.setImage with MTr.

class Cslib.LTS.ImageFinite {State : Type u} {Label : Type v} (lts : LTS State Label) [image_finite : ∀ (s : State) (μ : Label), Finite ↑(lts.image s μ)] : Type

An lts is image-finite if all images of its states are finite.

theorem Cslib.LTS.deterministic_not_lto {State : Type u} {Label : Type v} (lts : LTS State Label) [h : lts.Deterministic] (s : State) (μ : Label) (s' s'' : State) : s' ≠ s'' → lts.Tr s μ s' → ¬lts.Tr s μ s''

In a deterministic LTS, if a state has a μ-derivative, then it can have no other μ-derivative.

theorem Cslib.LTS.deterministic_tr_image_singleton {State : Type u} {Label : Type v} (lts : LTS State Label) {s : State} {μ : Label} {s' : State} [lts.Deterministic] : lts.image s μ = {s'} ↔ lts.Tr s μ s'

theorem Cslib.LTS.deterministic_image_char {State : Type u} {Label : Type v} (lts : LTS State Label) [lts.Deterministic] (s : State) (μ : Label) : (∃ (s' : State), lts.image s μ = {s'}) ∨ lts.image s μ = ∅

In a deterministic LTS, any image is either a singleton or the empty set.

instance Cslib.instFiniteElemImageOfDeterministic {State : Type u} {Label : Type v} (lts : LTS State Label) [lts.Deterministic] (s : State) (μ : Label) : Finite ↑(lts.image s μ)

In a deterministic LTS, the image of any state-label combination is finite.

instance Cslib.LTS.deterministic_imageFinite {State : Type u} {Label : Type v} (lts : LTS State Label) [lts.Deterministic] : lts.ImageFinite

Every deterministic LTS is also image-finite.

Equations

• lts.deterministic_imageFinite = { }

instance Cslib.LTS.finiteState_imageFinite {State : Type u} {Label : Type v} (lts : LTS State Label) [Finite State] : lts.ImageFinite

Every finite-state LTS is also image-finite.

Equations

• lts.finiteState_imageFinite = { }

def Cslib.LTS.HasOutLabel {State : Type u} {Label : Type v} (lts : LTS State Label) (s : State) (μ : Label) : Prop

A state has an outgoing label μ if it has a μ-derivative.

Equations

• lts.HasOutLabel s μ = ∃ (s' : State), lts.Tr s μ s'

def Cslib.LTS.outgoingLabels {State : Type u} {Label : Type v} (lts : LTS State Label) (s : State) : Set Label

The set of outgoing labels of a state.

Equations

• lts.outgoingLabels s = {μ : Label | lts.HasOutLabel s μ}

class Cslib.LTS.FinitelyBranching {State : Type u} {Label : Type v} (lts : LTS State Label) [image_finite : ∀ (s : State) (μ : Label), Finite ↑(lts.image s μ)] [finite_state : ∀ (s : State), Finite ↑(lts.outgoingLabels s)] : Type

An LTS is finitely branching if it is image-finite and all states have finite sets of outgoing labels.

instance Cslib.LTS.finiteState_finitelyBranching {State : Type u} {Label : Type v} (lts : LTS State Label) [Finite State] [Finite Label] : lts.FinitelyBranching

Every LTS with finite types for states and labels is also finitely branching.

Equations

• lts.finiteState_finitelyBranching = { }

class Cslib.LTS.Acyclic {State : Type u} {Label : Type v} (lts : LTS State Label) : Prop

An LTS is acyclic if there are no infinite multi-step transitions.

• acyclic : ∃ (n : ℕ), ∀ (s1 : State) (μs : List Label) (s2 : State), lts.MTr s1 μs s2 → μs.length < n

class Cslib.LTS.FiniteLTS {State : Type u} {Label : Type v} [Finite State] (lts : LTS State Label) extends lts.Acyclic : Prop

An LTS is finite if it is finite-state and acyclic.

We call this FiniteLTS instead of just Finite to avoid confusion with the standard Finite class.

• acyclic : ∃ (n : ℕ), ∀ (s1 : State) (μs : List Label) (s2 : State), lts.MTr s1 μs s2 → μs.length < n

class Cslib.LTS.LeftTotal {State : Type u} {Label : Type v} (lts : LTS State Label) : Prop

An LTS is left-total if every state has a μ-derivative for every label μ.

• left_total (s : State) (μ : Label) : ∃ (s' : State), lts.Tr s μ s'

Weak transitions (single- and multi-step)

class Cslib.HasTau (Label : Type v) : Type v

A type of transition labels that includes a special 'internal' transition τ.

• τ : Label

  The internal transition label, also known as τ.

inductive Cslib.LTS.STr {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) : State → Label → State → Prop

Saturated transition relation.

• refl {Label : Type u_1} {State : Type u_2} [HasTau Label] {lts : LTS State Label} {s : State} : lts.STr s HasTau.τ s
• tr {Label : Type u_1} {State : Type u_2} [HasTau Label] {lts : LTS State Label} {s1 s2 : State} {μ : Label} {s3 s4 : State} : lts.STr s1 HasTau.τ s2 → lts.Tr s2 μ s3 → lts.STr s3 HasTau.τ s4 → lts.STr s1 μ s4

def Cslib.LTS.saturate {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) : LTS State Label

The LTS obtained by saturating the transition relation in lts.

Equations

• lts.saturate = { Tr := lts.STr }

theorem Cslib.LTS.saturate_tr_sTr {Label : Type u_1} {State : Type u_2} [HasTau Label] {lts : LTS State Label} : lts.saturate.Tr = lts.STr

theorem Cslib.LTS.STr.single {Label : Type u_1} {State : Type u_2} {s : State} {μ : Label} {s' : State} [HasTau Label] (lts : LTS State Label) : lts.Tr s μ s' → lts.STr s μ s'

Any transition is also a saturated transition.

inductive Cslib.LTS.STrN {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) : ℕ → State → Label → State → Prop

As LTS.str, but counts the number of τ-transitions. This is convenient as induction metric.

• refl {Label : Type u_1} {State : Type u_2} [HasTau Label] {lts : LTS State Label} {s : State} : lts.STrN 0 s HasTau.τ s
• tr {Label : Type u_1} {State : Type u_2} [HasTau Label] {lts : LTS State Label} {n : ℕ} {s1 s2 : State} {μ : Label} {s3 : State} {m : ℕ} {s4 : State} : lts.STrN n s1 HasTau.τ s2 → lts.Tr s2 μ s3 → lts.STrN m s3 HasTau.τ s4 → lts.STrN (n + m + 1) s1 μ s4

theorem Cslib.LTS.sTr_sTrN {Label : Type u_1} {State : Type u_2} {s1 : State} {μ : Label} {s2 : State} [HasTau Label] (lts : LTS State Label) : lts.STr s1 μ s2 ↔ ∃ (n : ℕ), lts.STrN n s1 μ s2

LTS.str and LTS.strN are equivalent.

@[irreducible]

theorem Cslib.LTS.STrN.trans_τ {Label : Type u_1} {State : Type u_2} {n : ℕ} {s1 s2 : State} {m : ℕ} {s3 : State} [HasTau Label] (lts : LTS State Label) (h1 : lts.STrN n s1 HasTau.τ s2) (h2 : lts.STrN m s2 HasTau.τ s3) : lts.STrN (n + m) s1 HasTau.τ s3

Saturated transitions labelled by τ can be composed (weighted version).

theorem Cslib.LTS.STr.trans_τ {Label : Type u_1} {State : Type u_2} {s1 s2 s3 : State} [HasTau Label] (lts : LTS State Label) (h1 : lts.STr s1 HasTau.τ s2) (h2 : lts.STr s2 HasTau.τ s3) : lts.STr s1 HasTau.τ s3

Saturated transitions labelled by τ can be composed.

theorem Cslib.LTS.STrN.append {Label : Type u_1} {State : Type u_2} {n1 : ℕ} {s1 : State} {μ : Label} {s2 : State} {n2 : ℕ} {s3 : State} [HasTau Label] (lts : LTS State Label) (h1 : lts.STrN n1 s1 μ s2) (h2 : lts.STrN n2 s2 HasTau.τ s3) : lts.STrN (n1 + n2) s1 μ s3

Saturated transitions can be appended with τ-transitions (weighted version).

theorem Cslib.LTS.STrN.comp {Label : Type u_1} {State : Type u_2} {n1 : ℕ} {s1 s2 : State} {n2 : ℕ} {μ : Label} {s3 : State} {n3 : ℕ} {s4 : State} [HasTau Label] (lts : LTS State Label) (h1 : lts.STrN n1 s1 HasTau.τ s2) (h2 : lts.STrN n2 s2 μ s3) (h3 : lts.STrN n3 s3 HasTau.τ s4) : lts.STrN (n1 + n2 + n3) s1 μ s4

Saturated transitions can be composed (weighted version).

theorem Cslib.LTS.STr.comp {Label : Type u_1} {State : Type u_2} {s1 s2 : State} {μ : Label} {s3 s4 : State} [HasTau Label] (lts : LTS State Label) (h1 : lts.STr s1 HasTau.τ s2) (h2 : lts.STr s2 μ s3) (h3 : lts.STr s3 HasTau.τ s4) : lts.STr s1 μ s4

Saturated transitions can be composed.

theorem Cslib.LTS.saturate_sTr_tr {Label : Type u_1} {State : Type u_2} {μ : Label} {s : State} [hHasTau : HasTau Label] (lts : LTS State Label) (hμ : μ = HasTau.τ) : lts.saturate.Tr s μ = lts.saturate.STr s μ

In a saturated LTS, the transition and saturated transition relations are the same.

theorem Cslib.LTS.mem_saturate_image_τ {Label : Type u_1} {State : Type u_2} {s : State} [HasTau Label] (lts : LTS State Label) : s ∈ lts.saturate.image s HasTau.τ

In a saturated LTS, every state is in its τ-image.

def Cslib.LTS.τClosure {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) (S : Set State) : Set State

The τ-closure of a set of states S is the set of states reachable by any state in S by performing only τ-transitions.

Equations

• lts.τClosure S = lts.saturate.setImage S Cslib.HasTau.τ

Divergence

def Cslib.LTS.DivergentExecution {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) (stream : Stream' State) : Prop

A divergent execution is a stream of states where each state is the anti-τ-derivative of the next.

Equations

• lts.DivergentExecution stream = ∀ (n : ℕ), lts.Tr (stream n) Cslib.HasTau.τ (stream n.succ)

def Cslib.LTS.Divergent {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) (s : State) : Prop

A state is divergent if there is a divergent execution from it.

Equations

• lts.Divergent s = ∃ (stream : Stream' State), stream 0 = s ∧ lts.DivergentExecution stream

theorem Cslib.LTS.divergent_drop {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) (stream : Stream' State) (h : lts.DivergentExecution stream) (n : ℕ) : lts.DivergentExecution (Stream'.drop n stream)

If a stream is a divergent execution, then any 'suffix' is also a divergent execution.

class Cslib.LTS.DivergenceFree {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) : Prop

An LTS is divergence-free if it has no divergent state.

• divergence_free : ¬∃ (s : State), lts.Divergent s

def Cslib.LTS.Tr.toRelation {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) (μ : Label) : State → State → Prop

Returns the relation that relates all states s1 and s2 via a fixed transition label μ.

Equations

• Cslib.LTS.Tr.toRelation lts μ s1 s2 = lts.Tr s1 μ s2

def Cslib.LTS.MTr.toRelation {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) (μs : List Label) : State → State → Prop

Returns the relation that relates all states s1 and s2 via a fixed list of transition labels μs.

Equations

• Cslib.LTS.MTr.toRelation lts μs s1 s2 = lts.MTr s1 μs s2

def Cslib.Relation.toLTS {Label : Type u_1} {State : Type u_2} [DecidableEq Label] (r : State → State → Prop) (μ : Label) : LTS State Label

Any homogeneous relation can be seen as an LTS where all transitions have the same label.

Equations

• Cslib.Relation.toLTS r μ = { Tr := fun (s1 : State) (μ' : Label) (s2 : State) => if μ' = μ then r s1 s2 else False }

Support for the calc tactic

instance Cslib.instTransToRelationToRelationConsNil {State : Type u_1} {Label : Type u_2} {μ1 μ2 : Label} (lts : LTS State Label) : Trans (LTS.Tr.toRelation lts μ1) (LTS.Tr.toRelation lts μ2) (LTS.MTr.toRelation lts [μ1, μ2])

Transitions can be chained.

Equations

• Cslib.instTransToRelationToRelationConsNil lts = { trans := ⋯ }

instance Cslib.instTransToRelationToRelationCons {State : Type u_1} {Label : Type u_2} {μ : Label} {μs : List Label} (lts : LTS State Label) : Trans (LTS.Tr.toRelation lts μ) (LTS.MTr.toRelation lts μs) (LTS.MTr.toRelation lts (μ :: μs))

Transitions can be chained with multi-step transitions.

Equations

• Cslib.instTransToRelationToRelationCons lts = { trans := ⋯ }

instance Cslib.instTransToRelationToRelationHAppendListConsNil {State : Type u_1} {Label : Type u_2} {μs : List Label} {μ : Label} (lts : LTS State Label) : Trans (LTS.MTr.toRelation lts μs) (LTS.Tr.toRelation lts μ) (LTS.MTr.toRelation lts (μs ++ [μ]))

Multi-step transitions can be chained with transitions.

Equations

• Cslib.instTransToRelationToRelationHAppendListConsNil lts = { trans := ⋯ }

instance Cslib.instTransToRelationHAppendList {State : Type u_1} {Label : Type u_2} {μs1 μs2 : List Label} (lts : LTS State Label) : Trans (LTS.MTr.toRelation lts μs1) (LTS.MTr.toRelation lts μs2) (LTS.MTr.toRelation lts (μs1 ++ μs2))

Multi-step transitions can be chained.

Equations

• Cslib.instTransToRelationHAppendList lts = { trans := ⋯ }

def Cslib.commandCreate_lts__ : Lean.ParserDescr

A command to create an LTS from a labelled transition α → β → α → Prop, robust to use of variable

Equations

• One or more equations did not get rendered due to their size.

def Cslib.command_Lts_transition_notation__ : Lean.ParserDescr

This command adds transition notations for an LTS. This should not usually be called directly, but from the lts attribute.

As an example lts_transition_notation foo "β" will add the notations "[⬝]⭢β" and "[⬝]↠β"

Note that the string used will afterwards be registered as a notation. This means that if you have also used this as a constructor name, you will need quotes to access corresponding cases, e.g. «β» in the above example.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.lts_attr : Lean.ParserDescr

This attribute calls the lts_transition_notation command for the annotated declaration.

Equations

• One or more equations did not get rendered due to their size.