fact: Definition LTS_trace (t : trace Label) := match t with | trace_fin l => exists fl', LTS_init lts (fl' 0) /\ forall i (LLEN : i < length l) d, LTS_step lts (fl' i) (nth i l d) (fl' (S i)) | trace_inf fl => exists fl', LTS_init lts (fl' 0) /\ forall i, LTS_step lts (fl' i) (fl i) (fl' (S i)) end.
imports: HahnBase HahnList HahnSets HahnRelationsBasic HahnOmega HahnWf Arith micromega.Lia IndefiniteDescription