Finite executions of LTS

structure Cslib.LTS.Execution {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) (s1 : State) (μs : List Label) (s2 : State) (ss : List State) : Prop

Execution extends MTr by providing the intermediate states of a multistep transition.

• length : ss.length = μs.length + 1
• start : ss[0] = s1
• last : ss[ss.length - 1] = s2
• trans (k : ℕ) (hk : k < μs.length) : lts.Tr ss[k] μs[k] ss[k + 1]

theorem Cslib.LTS.Execution.length_ss_pos {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s₁ : State} {μs : List Label} {s₂ : State} {ss : List State} (h : lts.Execution s₁ μs s₂ ss) : 0 < ss.length

theorem Cslib.LTS.Execution.ss_ne_nil {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s₁ : State} {μs : List Label} {s₂ : State} {ss : List State} (h : lts.Execution s₁ μs s₂ ss) : ss ≠ []

Every execution has at least one intermediate state.

@[deprecated Cslib.LTS.Execution.ss_ne_nil (since := "2026-10-01")]

theorem Cslib.LTS.Execution.nonEmpty_states {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s₁ : State} {μs : List Label} {s₂ : State} {ss : List State} (h : lts.Execution s₁ μs s₂ ss) : ss ≠ []

Alias of Cslib.LTS.Execution.ss_ne_nil.

---

Every execution has at least one intermediate state.

theorem Cslib.LTS.Execution.length' {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s₁ : State} {μs : List Label} {s₂ : State} {ss : List State} (h : lts.Execution s₁ μs s₂ ss) : μs.length = ss.length - 1

theorem Cslib.LTS.Execution.last' {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s₁ : State} {μs : List Label} {s₂ : State} {ss : List State} (h : lts.Execution s₁ μs s₂ ss) : ss[μs.length] = s₂

theorem Cslib.LTS.Execution.getLast {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s₁ : State} {μs : List Label} {s₂ : State} {ss : List State} (h : lts.Execution s₁ μs s₂ ss) : ss.getLast ⋯ = s₂

theorem Cslib.LTS.Execution.refl {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) (s : State) : lts.Execution s [] s [s]

Every state has an execution of zero steps terminating in itself.

theorem Cslib.LTS.Execution.stepL {State : Type u_1} {Label : Type u_2} {s1 : State} {μ : Label} {s2 : State} {μs : List Label} {s3 : State} {ss : List State} {lts : LTS State Label} (htr : lts.Tr s1 μ s2) (hexec : lts.Execution s2 μs s3 ss) : lts.Execution s1 (μ :: μs) s3 (s1 :: ss)

Equivalent of MTr.stepL for executions.

theorem Cslib.LTS.Execution.cons_invert {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s1 : State} {μ : Label} {μs : List Label} {s2 : State} {ss : List State} (h : lts.Execution s1 (μ :: μs) s2 (s1 :: ss)) : lts.Execution ss[0] μs s2 ss

Deconstruction of executions with List.cons.

theorem Cslib.LTS.Execution.of_mTr {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s1 : State} {μs : List Label} {s2 : State} (h : lts.MTr s1 μs s2) : ∃ (ss : List State), lts.Execution s1 μs s2 ss

A multistep transition implies the existence of an execution.

theorem Cslib.LTS.Execution.to_mTr {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s1 : State} {μs : List Label} {s2 : State} {ss : List State} (hexec : lts.Execution s1 μs s2 ss) : lts.MTr s1 μs s2

Converts an execution into a multistep transition.

theorem Cslib.LTS.Execution.isChainFromTo {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s1 : State} {μs : List Label} {s2 : State} {ss : List State} (hexec : lts.Execution s1 μs s2 ss) : List.IsChainFromTo lts.UnlabelledTr ss s1 s2

The states visited by an execution form a chain from the initial to the final state in the underlying unlabelled relation.

theorem Cslib.LTS.Execution.isChain {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s1 : State} {μs : List Label} {s2 : State} {ss : List State} (hexec : lts.Execution s1 μs s2 ss) : List.IsChain lts.UnlabelledTr ss

The states visited by an execution form a chain in the underlying unlabelled relation.

theorem Cslib.LTS.mTr_iff_execution {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s1 : State} {μs : List Label} {s2 : State} : lts.MTr s1 μs s2 ↔ ∃ (ss : List State), lts.Execution s1 μs s2 ss

Correspondence of multistep transitions and executions.

theorem Cslib.LTS.Execution.comp {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s r t : State} {μs1 μs2 : List Label} {ss1 ss2 : List State} (h1 : lts.Execution s μs1 r ss1) (h2 : lts.Execution r μs2 t ss2) : lts.Execution s (μs1 ++ μs2) t (ss1 ++ ss2.tail)

The composition of two executions is an execution.

theorem Cslib.LTS.Execution.split {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s t : State} {μs : List Label} {ss : List State} (he : lts.Execution s μs t ss) (n : ℕ) (hn : n ≤ μs.length) : lts.Execution s (List.take n μs) ss[n] (List.take (n + 1) ss) ∧ lts.Execution ss[n] (List.drop n μs) t (List.drop n ss)

An execution can be split at any intermediate state into two executions.