Concat

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

Statistics

Metric	Count
Definitions finConcat, concat	2
Theorems concat_language_eq, finConcat_language_eq, instTotalSumUnitFinConcat, concat_run_exists, concat_run_left, concat_run_left_right, concat_run_proj, concat_run_right, concat_start_right	9
Total	11

Cslib.Automata.NA

Definitions

Name	Category	Theorems
concat 📖	CompOp	2 math math: concat_run_exists, Buchi.concat_language_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
concat_run_exists 📖	mathematical	Cslib.Automata.Acceptor.language FinAcc FinAcc.instAcceptor Run	concat Cslib.ωSequence.appendωSequence Cslib.ωSequence.drop Cslib.ωSequence.map	—	Cslib.LTS.mTr_isExecution
concat_run_left 📖	mathematical	Run concat Cslib.ωSequence Cslib.instFunLikeωSequenceNat	Cslib.LTS.MTr toLTS FinAcc.toNA Cslib.ωSequence.take start	—	—
concat_run_left_right 📖	mathematical	Run concat Cslib.ωSequence Cslib.instFunLikeωSequenceNat	Cslib.Automata.Acceptor.language FinAcc FinAcc.instAcceptor Cslib.ωSequence.take	—	concat_run_left
concat_run_proj 📖	mathematical	Run concat Cslib.ωSequence Cslib.instFunLikeωSequenceNat	Cslib.Automata.Acceptor.language FinAcc FinAcc.instAcceptor Cslib.ωSequence.take Cslib.ωSequence.drop Cslib.ωSequence.map	—	concat_run_right
concat_run_right 📖	mathematical	Run concat Cslib.ωSequence Cslib.instFunLikeωSequenceNat	Cslib.ωSequence.drop Cslib.ωSequence.map	—	—
concat_start_right 📖	mathematical	Run concat Cslib.ωSequence Cslib.instFunLikeωSequenceNat	Cslib.Automata.Acceptor.language FinAcc FinAcc.instAcceptor	—	—

Cslib.Automata.NA.Buchi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
concat_language_eq 📖	mathematical	—	Cslib.Automata.ωAcceptor.language Cslib.Automata.NA.Buchi instωAcceptor Cslib.Automata.NA.concat Cslib.ωLanguage Cslib.ωLanguage.instHMulLanguage Cslib.Automata.Acceptor.language Cslib.Automata.NA.FinAcc Cslib.Automata.NA.FinAcc.instAcceptor	—	Cslib.ωLanguage.ext Cslib.Automata.NA.concat_run_proj Cslib.ωSequence.append_take_drop Cslib.Automata.NA.concat_run_exists Cslib.ωSequence.drop_frequently_iff_frequently

Cslib.Automata.NA.FinAcc

Definitions

Name	Category	Theorems
finConcat 📖	CompOp	2 math math: instTotalSumUnitFinConcat, finConcat_language_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finConcat_language_eq 📖	mathematical	—	Cslib.Automata.Acceptor.language Cslib.Automata.NA.FinAcc instAcceptor finConcat accept	—	Cslib.LTS.Total.mTr_ωTr instTotalSumUnitFinConcat Cslib.Automata.NA.concat_run_proj Cslib.Automata.NA.totalize_mtr_run Cslib.Automata.NA.concat_run_exists totalize_language_eq
instTotalSumUnitFinConcat 📖	mathematical	—	Cslib.LTS.Total Cslib.Automata.NA.toLTS finConcat	—	—

---

← Back to Index