RegularLanguage

Statistics

Metric	Count
Definitions	0
Theorems `add`, `compl`, `congr_fin_index`, `iInf`, `iSup`, `iff_dfa`, `iff_nfa`, `inf`, `kstar`, `mul`, `one`, `top`, `zero`	13
Total	13

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	—	—	—	—	`iff_dfa`
`compl` 📖	—	—	—	—	`iff_dfa`
`congr_fin_index` 📖	mathematical	—	`Cslib.RightCongruence.eqvCls`	—	`iff_dfa` `Cslib.Automata.DA.FinAcc.congr_language_eq`
`iInf` 📖	—	—	—	—	—
`iSup` 📖	—	—	—	—	`zero` `add`
`iff_dfa` 📖	mathematical	—	`Cslib.Automata.Acceptor.language` `Cslib.Automata.DA.FinAcc` `Cslib.Automata.DA.FinAcc.instAcceptor`	—	—
`iff_nfa` 📖	mathematical	—	`Cslib.Automata.Acceptor.language` `Cslib.Automata.NA.FinAcc` `Cslib.Automata.NA.FinAcc.instAcceptor`	—	`iff_dfa`
`inf` 📖	—	—	—	—	`iff_dfa`
`kstar` 📖	—	—	—	—	`iff_nfa` `Cslib.Automata.NA.FinAcc.loop_language_eq`
`mul` 📖	—	—	—	—	`iff_nfa` `Cslib.Automata.NA.FinAcc.finConcat_language_eq`
`one` 📖	—	—	—	—	`iff_dfa`
`top` 📖	—	—	—	—	`compl` `zero`
`zero` 📖	—	—	—	—	`iff_dfa`

---