Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `Acyclic`, `CanReach`, `Deterministic`, `FiniteLTS`, `FinitelyBranching`, `HasOutLabel`, `ImageFinite`, `MTr`, `Tr`, `generatedBy`, `image`, `imageMultistep`, `outgoingLabels`, `setImage`, `setImageMultistep`	15
Theorems `acyclic`, `refl`, `deterministic`, `toAcyclic`, `finite_state`, `image_finite`, `of_finite`, `comp`, `nil_eq`, `single`, `single_invert`, `stepR`, `deterministic_imageFinite`, `deterministic_image_char`, `deterministic_not_lto`, `deterministic_tr_image_singleton`, `finiteState_imageFinite`, `instFiniteElemImageOfDeterministic`, `mTr_setImage`, `mem_foldl_setImage`, `mem_setImage`, `mem_setImageMultistep`, `setImageMultistep_foldl_setImage`, `setImageMultistep_setImage_head`, `setImage_empty`, `tr_setImage`	26
Total	41

Cslib.LTS

Definitions

Name	Category	Theorems
`Acyclic` 📖	CompData	1 math math: `FiniteLTS.toAcyclic`
`CanReach` 📖	MathDef	1 math math: `CanReach.refl`
`Deterministic` 📖	CompData	1 math math: `Cslib.FLTS.toLTS_deterministic`
`FiniteLTS` 📖	CompData	—
`FinitelyBranching` 📖	CompData	1 math math: `FinitelyBranching.of_finite`
`HasOutLabel` 📖	MathDef	—
`ImageFinite` 📖	MathDef	4 math math: `finiteState_imageFinite`, `deterministic_imageFinite`, `Cslib.FLTS.toLTS_imageFinite`, `FinitelyBranching.image_finite`
`MTr` 📖	CompData	21 math math: `noε_saturate_mTr`, `Cslib.Automata.NA.loop_run_left_right`, `Cslib.Automata.NA.loop_fin_run_mtr`, `Execution.to_mTr`, `MTr.comp`, `mTr_iff_execution`, `Cslib.Automata.NA.concat_run_left`, `totalize.nonsink_mtr_iff`, `OmegaExecution.extract_mTr`, `mem_pairLang`, `Cslib.FLTS.toLTS_mtr`, `MTr.single`, `MTr.stepR`, `mem_setImageMultistep`, `Cslib.Automata.NA.totalize_run_mtr`, `toFLTS_mem_mtr`, `IsBisimulation.bisim_trace`, `totalize.no_sink_to_nonsink`, `MTr.split`, `mem_foldl_setImage`, `mem_pairViaLang`
`Tr` 📖	MathDef	14 math math: `Total.chooseFLTS`, `MTr.single_invert`, `IsBisimulation.follow_fst`, `deterministic_not_lto`, `Cslib.FLTS.toLTS_tr`, `toFLTS_mem_tr`, `saturate_tr_sTr`, `totalize.nonsink_tr_iff`, `Total.total`, `IsBisimulation.follow_snd`, `mem_setImage`, `Cslib.Automata.NA.loop_fin_run_exists`, `saturate_tr_saturate_sTr`, `deterministic_tr_image_singleton`
`generatedBy` 📖	CompOp	—
`image` 📖	CompOp	4 math math: `mem_saturate_image_τ`, `deterministic_image_char`, `instFiniteElemImageOfDeterministic`, `deterministic_tr_image_singleton`
`imageMultistep` 📖	CompOp	—
`outgoingLabels` 📖	CompOp	1 math math: `FinitelyBranching.finite_state`
`setImage` 📖	CompOp	6 math math: `setImageMultistep_foldl_setImage`, `setImage_empty`, `tr_setImage`, `setImageMultistep_setImage_head`, `mem_setImage`, `mem_foldl_setImage`
`setImageMultistep` 📖	CompOp	5 math math: `setImageMultistep_foldl_setImage`, `mTr_setImage`, `setImageMultistep_setImage_head`, `mem_setImageMultistep`, `toFLTS_mtr_setImageMultistep`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`deterministic_imageFinite` 📖	mathematical	—	`ImageFinite`	—	`instFiniteElemImageOfDeterministic`
`deterministic_image_char` 📖	mathematical	—	`image`	—	—
`deterministic_not_lto` 📖	mathematical	`Tr`	`Tr`	—	—
`deterministic_tr_image_singleton` 📖	mathematical	—	`image` `Tr`	—	—
`finiteState_imageFinite` 📖	mathematical	—	`ImageFinite`	—	—
`instFiniteElemImageOfDeterministic` 📖	mathematical	—	`image`	—	`deterministic_image_char`
`mTr_setImage` 📖	mathematical	`MTr`	`setImageMultistep`	—	—
`mem_foldl_setImage` 📖	mathematical	—	`setImage` `MTr`	—	`setImageMultistep_foldl_setImage` `mem_setImageMultistep`
`mem_setImage` 📖	mathematical	—	`setImage` `Tr`	—	—
`mem_setImageMultistep` 📖	mathematical	—	`setImageMultistep` `MTr`	—	—
`setImageMultistep_foldl_setImage` 📖	mathematical	—	`setImageMultistep` `setImage`	—	—
`setImageMultistep_setImage_head` 📖	mathematical	—	`setImageMultistep` `setImage`	—	—
`setImage_empty` 📖	mathematical	—	`setImage`	—	—
`tr_setImage` 📖	mathematical	`Tr`	`setImage`	—	—

Cslib.LTS.Acyclic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`acyclic` 📖	—	—	—	—	—

Cslib.LTS.CanReach

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`refl` 📖	mathematical	—	`Cslib.LTS.CanReach`	—	—

Cslib.LTS.Deterministic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`deterministic` 📖	—	`Cslib.LTS.Tr`	—	—	—

Cslib.LTS.FiniteLTS

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toAcyclic` 📖	mathematical	—	`Cslib.LTS.Acyclic`	—	—

Cslib.LTS.FinitelyBranching

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_state` 📖	mathematical	—	`Cslib.LTS.outgoingLabels`	—	—
`image_finite` 📖	mathematical	—	`Cslib.LTS.ImageFinite`	—	—
`of_finite` 📖	mathematical	—	`Cslib.LTS.FinitelyBranching`	—	`Cslib.LTS.finiteState_imageFinite`

Cslib.LTS.MTr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`Cslib.LTS.MTr`	`Cslib.LTS.MTr`	—	—
`nil_eq` 📖	—	`Cslib.LTS.MTr`	—	—	—
`single` 📖	mathematical	`Cslib.LTS.Tr`	`Cslib.LTS.MTr`	—	—
`single_invert` 📖	mathematical	`Cslib.LTS.MTr`	`Cslib.LTS.Tr`	—	—
`stepR` 📖	mathematical	`Cslib.LTS.MTr` `Cslib.LTS.Tr`	`Cslib.LTS.MTr`	—	`single`

---

← Back to Index