Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-03 16:58 384ba88b

View on Github →

feat(computability/*FA): Deterministic and Nondeterministic Finite Automata (#5038) Definition and equivalence of NFA's and DFA's

Estimated changes

added def DFA.accepts
added def DFA.eval
added def DFA.eval_from
added structure DFA
added def DFA.to_NFA
added theorem DFA.to_NFA_correct
added def NFA.accepts
added def NFA.eval
added def NFA.eval_from
added theorem NFA.mem_step_set
added def NFA.step_set
added def NFA.to_DFA
added theorem NFA.to_DFA_correct
added structure NFA