Basic

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

Statistics

Metric	Count
Definitions HasTau, τ, Acyclic, CanReach, Deterministic, DivergenceFree, Divergent, DivergentTrace, FiniteLTS, FinitelyBranching, HasOutLabel, ImageFinite, IsExecution, MTr, toRelation, MayTerminate, STr, STrN, Stuck, Tr, toRelation, chooseFLTS, chooseωTr, deterministic_imageFinite, finiteState_finitelyBranching, finiteState_imageFinite, generatedBy, image, imageMultistep, inl, inr, outgoingLabels, saturate, setImage, setImageMultistep, totalize, union, unionSubtype, unionSum, τClosure, ωTr, toLTS, commandCreate_lts__, command_Lts_transition_notation__, instTransToRelationHAppendList, instTransToRelationToRelationCons, instTransToRelationToRelationConsNil, instTransToRelationToRelationHAppendListConsNil, lts_attr	49
Theorems acyclic, refl, deterministic, divergence_free, toAcyclic, flatten, refl, split, stepL, comp, nil_eq, single, single_invert, split, stepR, comp, single, trans_τ, append, comp, trans_τ, mTr_ωTr, total, ωTr_exists, total, deterministic_image_char, deterministic_not_lto, deterministic_tr_image_singleton, divergentTrace_drop, isExecution_cons_invert, isExecution_mTr, isExecution_nonEmpty_states, mTr_isExecution, mTr_isExecution_iff, mTr_setImage, mem_foldl_setImage, mem_saturate_image_τ, mem_setImage, mem_setImageMultistep, sTr_sTrN, saturate_sTr_tr, saturate_tr_sTr, setImageMultistep_foldl_setImage, setImageMultistep_setImage_head, setImage_empty, mtr_left_iff, not_right_left, tr_left_iff, tr_setImage, append, cons, flatten, ωTr_mTr, instFiniteElemImageOfDeterministic, instTotalSumUnitTotalize	55
Total	104

Cslib

Definitions

Name	Category	Theorems
HasTau 📖	CompData	—
commandCreate_lts__ 📖	CompOp	—
command_Lts_transition_notation__ 📖	CompOp	—
instTransToRelationHAppendList 📖	CompOp	—
instTransToRelationToRelationCons 📖	CompOp	—
instTransToRelationToRelationConsNil 📖	CompOp	—
instTransToRelationToRelationHAppendListConsNil 📖	CompOp	—
lts_attr 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFiniteElemImageOfDeterministic 📖	mathematical	—	LTS.image	—	LTS.deterministic_image_char
instTotalSumUnitTotalize 📖	mathematical	—	LTS.Total LTS.totalize	—	—

Cslib.HasTau

Definitions

Name	Category	Theorems
τ 📖	CompOp	1 math math: Cslib.LTS.mem_saturate_image_τ

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
DivergenceFree 📖	CompData	—
Divergent 📖	MathDef	1 math math: DivergenceFree.divergence_free
DivergentTrace 📖	MathDef	—
FiniteLTS 📖	CompData	—
FinitelyBranching 📖	CompData	—
HasOutLabel 📖	MathDef	—
ImageFinite 📖	CompData	—
IsExecution 📖	MathDef	3 math math: mTr_isExecution, mTr_isExecution_iff, IsExecution.refl
MTr 📖	CompData	17 math math: noε_saturate_mTr, Cslib.Automata.NA.loop_run_left_right, Cslib.Automata.NA.loop_fin_run_mtr, Cslib.Automata.NA.concat_run_left, mem_pairLang, ωTr_mTr, Cslib.FLTS.toLTS_mtr, MTr.single, mTr_isExecution_iff, totalize.not_right_left, mem_setImageMultistep, Cslib.Automata.NA.totalize_run_mtr, toFLTS_mem_mtr, isExecution_mTr, mem_foldl_setImage, mem_pairViaLang, totalize.mtr_left_iff
MayTerminate 📖	MathDef	—
STr 📖	CompData	6 math math: Cslib.SWBisimulation.follow_internal_snd_n, STr.single, Cslib.SWBisimulation.follow_internal_fst_n, sTr_sTrN, saturate_sTr_tr, saturate_tr_sTr
STrN 📖	CompData	1 math math: sTr_sTrN
Stuck 📖	MathDef	—
Tr 📖	MathDef	11 math math: chooseFLTS.total, MTr.single_invert, totalize.tr_left_iff, Cslib.FLTS.toLTS_tr, toFLTS_mem_tr, saturate_sTr_tr, saturate_tr_sTr, Total.total, mem_setImage, Cslib.Automata.NA.loop_fin_run_exists, deterministic_tr_image_singleton
chooseFLTS 📖	CompOp	1 math math: chooseFLTS.total
chooseωTr 📖	CompOp	—
deterministic_imageFinite 📖	CompOp	—
finiteState_finitelyBranching 📖	CompOp	—
finiteState_imageFinite 📖	CompOp	—
generatedBy 📖	CompOp	—
image 📖	CompOp	4 math math: mem_saturate_image_τ, deterministic_image_char, Cslib.instFiniteElemImageOfDeterministic, deterministic_tr_image_singleton
imageMultistep 📖	CompOp	—
inl 📖	CompOp	—
inr 📖	CompOp	—
outgoingLabels 📖	CompOp	—
saturate 📖	CompOp	4 math math: noε_saturate_mTr, mem_saturate_image_τ, saturate_sTr_tr, saturate_tr_sTr
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
totalize 📖	CompOp	4 math math: totalize.tr_left_iff, totalize.not_right_left, Cslib.instTotalSumUnitTotalize, totalize.mtr_left_iff
union 📖	CompOp	—
unionSubtype 📖	CompOp	—
unionSum 📖	CompOp	—
τClosure 📖	CompOp	—
ωTr 📖	MathDef	5 math math: Cslib.Automata.NA.Run.trans, IsExecution.flatten, ωTr.flatten, Total.mTr_ωTr, Total.ωTr_exists

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deterministic_image_char 📖	mathematical	—	image	—	—
deterministic_not_lto 📖	—	Tr	—	—	—
deterministic_tr_image_singleton 📖	mathematical	—	image Tr	—	—
divergentTrace_drop 📖	mathematical	DivergentTrace	Cslib.ωSequence.drop	—	—
isExecution_cons_invert 📖	—	IsExecution	—	—	—
isExecution_mTr 📖	mathematical	IsExecution	MTr	—	isExecution_cons_invert
isExecution_nonEmpty_states 📖	—	IsExecution	—	—	—
mTr_isExecution 📖	mathematical	MTr	IsExecution	—	—
mTr_isExecution_iff 📖	mathematical	—	MTr IsExecution	—	—
mTr_setImage 📖	mathematical	MTr	setImageMultistep	—	—
mem_foldl_setImage 📖	mathematical	—	setImage MTr	—	setImageMultistep_foldl_setImage mem_setImageMultistep
mem_saturate_image_τ 📖	mathematical	—	image saturate Cslib.HasTau.τ	—	—
mem_setImage 📖	mathematical	—	setImage Tr	—	—
mem_setImageMultistep 📖	mathematical	—	setImageMultistep MTr	—	—
sTr_sTrN 📖	mathematical	—	STr STrN	—	—
saturate_sTr_tr 📖	mathematical	Cslib.HasTau.τ	Tr saturate STr	—	saturate_tr_sTr STr.single
saturate_tr_sTr 📖	mathematical	—	Tr saturate STr	—	—
setImageMultistep_foldl_setImage 📖	mathematical	—	setImageMultistep setImage	—	—
setImageMultistep_setImage_head 📖	mathematical	—	setImageMultistep setImage	—	—
setImage_empty 📖	mathematical	—	setImage	—	—
tr_setImage 📖	mathematical	Tr	setImage	—	—
ωTr_mTr 📖	mathematical	ωTr	MTr Cslib.ωSequence Cslib.instFunLikeωSequenceNat Cslib.ωSequence.extract	—	—

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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
divergence_free 📖	mathematical	—	Cslib.LTS.Divergent	—	—

Cslib.LTS.FiniteLTS

Theorems

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

Cslib.LTS.IsExecution

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
flatten 📖	mathematical	Cslib.LTS.IsExecution Cslib.ωSequence Cslib.instFunLikeωSequenceNat	Cslib.LTS.ωTr Cslib.ωSequence.flatten Cslib.ωSequence.extract Cslib.ωSequence.cumLen	—	Cslib.ωSequence.cumLen_strictMono Cslib.ωSequence.cumLen_zero Nat.segment_lower_bound Nat.segment_range_val Nat.segment_idem Cslib.ωSequence.extract_flatten
refl 📖	mathematical	—	Cslib.LTS.IsExecution	—	—
split 📖	—	Cslib.LTS.IsExecution	—	—	—
stepL 📖	—	Cslib.LTS.Tr Cslib.LTS.IsExecution	—	—	—

Cslib.LTS.MTr

Definitions

Name	Category	Theorems
toRelation 📖	MathDef	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	—	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	—	—
split 📖	—	Cslib.LTS.MTr	—	—	Cslib.LTS.mTr_isExecution Cslib.LTS.IsExecution.split
stepR 📖	—	Cslib.LTS.MTr Cslib.LTS.Tr	—	—	single

Cslib.LTS.STr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp 📖	—	Cslib.LTS.STr Cslib.HasTau.τ	—	—	Cslib.LTS.sTr_sTrN Cslib.LTS.STrN.comp
single 📖	mathematical	Cslib.LTS.Tr	Cslib.LTS.STr	—	—
trans_τ 📖	—	Cslib.LTS.STr Cslib.HasTau.τ	—	—	Cslib.LTS.sTr_sTrN Cslib.LTS.STrN.trans_τ

Cslib.LTS.STrN

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
append 📖	—	Cslib.LTS.STrN Cslib.HasTau.τ	—	—	trans_τ
comp 📖	—	Cslib.LTS.STrN Cslib.HasTau.τ	—	—	trans_τ append
trans_τ 📖	—	Cslib.LTS.STrN Cslib.HasTau.τ	—	—	—

Cslib.LTS.Total

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mTr_ωTr 📖	mathematical	Cslib.LTS.MTr	Cslib.LTS.ωTr Cslib.ωSequence.appendωSequence Cslib.ωSequence Cslib.instFunLikeωSequenceNat	—	ωTr_exists
total 📖	mathematical	—	Cslib.LTS.Tr	—	—
ωTr_exists 📖	mathematical	—	Cslib.LTS.ωTr Cslib.ωSequence Cslib.instFunLikeωSequenceNat	—	—

Cslib.LTS.Tr

Definitions

Name	Category	Theorems
toRelation 📖	MathDef	—

Cslib.LTS.chooseFLTS

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
total 📖	mathematical	—	Cslib.LTS.Tr Cslib.FLTS.tr Cslib.LTS.chooseFLTS	—	Cslib.LTS.Total.total

Cslib.LTS.totalize

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mtr_left_iff 📖	mathematical	—	Cslib.LTS.MTr Cslib.LTS.totalize	—	—
not_right_left 📖	mathematical	—	Cslib.LTS.MTr Cslib.LTS.totalize	—	—
tr_left_iff 📖	mathematical	—	Cslib.LTS.Tr Cslib.LTS.totalize	—	—

Cslib.LTS.ωTr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
append 📖	mathematical	Cslib.LTS.MTr Cslib.LTS.ωTr Cslib.ωSequence Cslib.instFunLikeωSequenceNat	Cslib.ωSequence.appendωSequence Cslib.ωSequence.drop	—	Cslib.LTS.mTr_isExecution
cons 📖	mathematical	Cslib.LTS.Tr Cslib.LTS.ωTr Cslib.ωSequence Cslib.instFunLikeωSequenceNat	Cslib.ωSequence.cons	—	—
flatten 📖	mathematical	Cslib.LTS.MTr Cslib.ωSequence Cslib.instFunLikeωSequenceNat	Cslib.LTS.ωTr Cslib.ωSequence.flatten Cslib.ωSequence.cumLen	—	Cslib.LTS.IsExecution.flatten Cslib.LTS.mTr_isExecution

Cslib.Relation

Definitions

Name	Category	Theorems
toLTS 📖	CompOp	—

---

← Back to Index