Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-13 22:35 07600ee4

View on Github →

feat(computability/epsilon_nfa): epsilon-NFA definition (#6108)

Estimated changes

Created src/computability/epsilon_NFA.lean

added def NFA.to_ε_NFA

added theorem NFA.to_ε_NFA_correct

added theorem NFA.to_ε_NFA_eval_from_match

added theorem NFA.to_ε_NFA_ε_closure

added def ε_NFA.accepts

added def ε_NFA.eval

added def ε_NFA.eval_from

added theorem ε_NFA.pumping_lemma

added def ε_NFA.step_set

added def ε_NFA.to_NFA

added theorem ε_NFA.to_NFA_correct

added theorem ε_NFA.to_NFA_eval_from_match

added inductive ε_NFA.ε_closure

added structure ε_NFA