Finite executions of LTS

def 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.

Equations

• lts.Execution s1 μs s2 ss = ∃ (x : ss.length = μs.length + 1), ss[0] = s1 ∧ ss[ss.length - 1] = s2 ∧ ∀ (k : ℕ) {x_1 : k < μs.length}, lts.Tr ss[k] μs[k] ss[k + 1]

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

Every execution has at least one intermediate state.

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

theorem Cslib.LTS.MTr.split {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s0 : State} {μs1 μs2 : List Label} {s2 : State} (h : lts.MTr s0 (μs1 ++ μs2) s2) : ∃ (s1 : State), lts.MTr s0 μs1 s1 ∧ lts.MTr s1 μs2 s2

A multistep transition over a concatenation can be split into two multistep transitions.