Loop

📁 Source: Cslib/Computability/Automata/NA/Loop.lean

Statistics

Metric	Count
Definitions finLoop, loop	2
Theorems loop_language_eq, instTotalSumUnitFinLoopOfNonemptyElemStart, loop_language_eq, loop_fin_run_exists, loop_fin_run_mtr, loop_run_exists, loop_run_from_left, loop_run_left_left, loop_run_left_right, loop_run_left_right_left, loop_run_one_iter	11
Total	13

Cslib.Automata.NA

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
loop_fin_run_exists 📖	mathematical	Cslib.Automata.Acceptor.language FinAcc FinAcc.instAcceptor	Cslib.LTS.Tr toLTS FinAcc.loop	—	Cslib.LTS.mTr_isExecution
loop_fin_run_mtr 📖	mathematical	Cslib.Automata.Acceptor.language FinAcc FinAcc.instAcceptor	Cslib.LTS.MTr toLTS FinAcc.loop	—	loop_fin_run_exists
loop_run_exists 📖	mathematical	Cslib.Automata.Acceptor.language FinAcc FinAcc.instAcceptor Cslib.ωSequence Cslib.instFunLikeωSequenceNat	Run FinAcc.loop Cslib.ωSequence.flatten Cslib.ωSequence.cumLen	—	Cslib.LTS.ωTr.flatten
loop_run_from_left 📖	mathematical	Run FinAcc.loop Cslib.ωSequence Cslib.instFunLikeωSequenceNat	Cslib.ωSequence.drop	—	—
loop_run_left_left 📖	mathematical	Run FinAcc.loop Cslib.ωSequence Cslib.instFunLikeωSequenceNat	Cslib.Automata.Acceptor.language FinAcc FinAcc.instAcceptor	—	Run.start Run.trans
loop_run_left_right 📖	mathematical	Run FinAcc.loop Cslib.ωSequence Cslib.instFunLikeωSequenceNat	Cslib.LTS.MTr toLTS FinAcc.toNA Cslib.ωSequence.take start	—	—
loop_run_left_right_left 📖	mathematical	Run FinAcc.loop Cslib.ωSequence Cslib.instFunLikeωSequenceNat	Cslib.Automata.Acceptor.language FinAcc FinAcc.instAcceptor Cslib.ωSequence.take	—	loop_run_left_right
loop_run_one_iter 📖	mathematical	Run FinAcc.loop Cslib.ωSequence Cslib.instFunLikeωSequenceNat	Cslib.Automata.Acceptor.language FinAcc FinAcc.instAcceptor Cslib.ωSequence.take Cslib.ωSequence.drop	—	—

Cslib.Automata.NA.Buchi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
loop_language_eq 📖	mathematical	—	Cslib.Automata.ωAcceptor.language Cslib.Automata.NA.Buchi instωAcceptor Cslib.Automata.NA.FinAcc.loop Cslib.ωLanguage.OmegaPow.omegaPow Cslib.ωLanguage Cslib.ωLanguage.instOmegaPowLanguageOfInhabited Cslib.Automata.Acceptor.language Cslib.Automata.NA.FinAcc Cslib.Automata.NA.FinAcc.instAcceptor	—	Cslib.ωLanguage.omegaPow_coind Cslib.Automata.NA.loop_run_one_iter Cslib.ωSequence.drop_frequently_iff_frequently Cslib.ωSequence.append_take_drop Cslib.ωLanguage.mem_omegaPow Cslib.Automata.NA.loop_run_exists Cslib.ωSequence.frequently_iff_strictMono

Cslib.Automata.NA.FinAcc

Definitions

Name	Category	Theorems
finLoop 📖	CompOp	2 math math: loop_language_eq, instTotalSumUnitFinLoopOfNonemptyElemStart
loop 📖	CompOp	4 math math: Cslib.Automata.NA.loop_fin_run_mtr, Cslib.Automata.NA.loop_fin_run_exists, Cslib.Automata.NA.loop_run_exists, Cslib.Automata.NA.Buchi.loop_language_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instTotalSumUnitFinLoopOfNonemptyElemStart 📖	mathematical	—	Cslib.LTS.Total Cslib.Automata.NA.toLTS finLoop	—	—
loop_language_eq 📖	mathematical	Cslib.Automata.Acceptor.language Cslib.Automata.NA.FinAcc instAcceptor	finLoop	—	Language.kstar_iff_mul_add Cslib.LTS.Total.mTr_ωTr instTotalSumUnitFinLoopOfNonemptyElemStart Cslib.Automata.NA.loop_run_one_iter Cslib.LTS.ωTr_mTr Cslib.Automata.NA.loop_fin_run_mtr totalize_language_eq Cslib.LTS.MTr.comp

---

← Back to Index