Basic

📁 Source: Cslib/Foundations/Semantics/FLTS/Basic.lean

Statistics

Metric	Count
Definitions FLTS, mtr, tr	3
Theorems mtr_concat_eq, mtr_nil_eq	2
Total	5

Cslib

Definitions

Name	Category	Theorems
FLTS 📖	CompData	—

Cslib.FLTS

Definitions

Name	Category	Theorems
mtr 📖	CompOp	9 math math: Cslib.Automata.DA.prod_mtr_eq, toLTS_mtr, mtr_concat_eq, Cslib.LTS.toFLTS_mtr_setImageMultistep, Cslib.Automata.DA.congr_mtr_eq, Cslib.LTS.toFLTS_mem_mtr, Cslib.Automata.DA.mtr_extract_eq_run, mtr_nil_eq, prod_mtr_eq
tr 📖	CompOp	5 math math: Cslib.LTS.chooseFLTS.total, Cslib.Automata.DA.run_succ, mtr_concat_eq, toLTS_tr, Cslib.LTS.toFLTS_mem_tr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mtr_concat_eq 📖	mathematical	—	mtr tr	—	—
mtr_nil_eq 📖	mathematical	—	mtr	—	—

---

← Back to Index