Congr

📁 Source: Cslib/Computability/Automata/DA/Congr.lean

Statistics

Metric	Count
Definitions toDA	1
Theorems congr_language_eq, congr_mtr_eq	2
Total	3

Cslib.Automata.DA

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_mtr_eq 📖	mathematical	—	Cslib.FLTS.mtr Cslib.RightCongruence.eq toFLTS Cslib.RightCongruence.toDA start	—	—

Cslib.Automata.DA.FinAcc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
congr_language_eq 📖	mathematical	—	Cslib.Automata.Acceptor.language Cslib.Automata.DA.FinAcc Cslib.RightCongruence.eq instAcceptor Cslib.RightCongruence.toDA Cslib.RightCongruence.eqvCls	—	—

Cslib.RightCongruence

Definitions

Name	Category	Theorems
toDA 📖	CompOp	2 math math: Cslib.Automata.DA.FinAcc.congr_language_eq, Cslib.Automata.DA.congr_mtr_eq

---

← Back to Index