``` ```

# Labelled Transition Systems (LTS)

``` Require Export Diagrams. Ltac cgen H := generalize H; clear H. Section Reductions.   Section R.     Variables A X: Type.     Definition reduction := A -> relation X.     Definition incl_r: relation reduction := fun R1 R2 => forall a, incl (R1 a) (R2 a).     Definition eeq_r: relation reduction := fun R1 R2 => forall a, eeq (R1 a) (R2 a).   End R.   Variable A: Type.   Section Diagram.     Variables X Y: Type.     Definition diagram_r(RX: reduction A X) R (RY: reduction A Y) S := forall a, diagram (RX a) R (RY a) S.   End Diagram.   Section Weak. ```
A `label' is either the silent action, or a visible one
```     Inductive Lbl: Type := T | L(a: A).     Definition reduction_t := reduction Lbl.     Variable X: Type.     Variable Red: reduction_t X. ```
Weak transition relation
```     Definition Weak: reduction_t X := fun l =>       match l with         | T => star (Red T)         | L a => comp (star (Red T)) (comp (Red (L a)) (star (Red T)))       end. ```
Transition relation for expansion
```     Definition EWeak: reduction_t X := fun l =>       match l with         | T => union2 (eq (A:=X)) (Red T)         | L a => Red (L a)       end. ```
Transition relation for relaxed expansion
```     Definition REWeak: reduction_t X := fun l =>       match l with         | T => union2 (eq (A:=X)) (Red T)         | L a => comp (Red (L a)) (star (Red T))       end.     Lemma weak_refl: forall x, Weak T x x.     Hint Immediate weak_refl.     Lemma tau_weak: forall y l x z, Red T x y -> Weak l y z -> Weak l x z.     Lemma weak_tau: forall y l x z, Red l x y -> Weak T y z -> Weak l x z.     Lemma red_weak: forall l x y, Red l x y -> Weak l x y.     Lemma taus_weak: forall y l x z, Weak T x y -> Weak l y z -> Weak l x z.     Lemma weak_taus: forall y l x z, Weak l x y -> Weak T y z -> Weak l x z. ```
A useful induction principle: just look at the first action
```     Theorem Weak_ind:        forall P: Lbl -> X -> X -> Prop,        (forall x, P T x x) ->        (forall y l x z ,         Red T x y -> Weak l y z -> P l y z -> P l x z) ->        (forall y a x z,         Red (L a) x y -> Weak T y z -> P T y z -> P (L a) x z) ->        forall l x x', Weak l x x' -> P l x x'.   End Weak. End Reductions. Hint Immediate weak_refl. Hint Resolve red_weak. ```