Commit 2023-02-20 14:58 a4a916a2

View on Github →

feat: port Computability.EpsilonNFA (#2386)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Computability/EpsilonNFA.lean

added def NFA.toεNFA

added theorem NFA.toεNFA_correct

added theorem NFA.toεNFA_evalFrom_match

added theorem NFA.toεNFA_εClosure

added theorem εNFA.accept_one

added theorem εNFA.accept_zero

added def εNFA.accepts

added def εNFA.eval

added def εNFA.evalFrom

added theorem εNFA.evalFrom_append_singleton

added theorem εNFA.evalFrom_empty

added theorem εNFA.evalFrom_nil

added theorem εNFA.evalFrom_singleton

added theorem εNFA.eval_append_singleton

added theorem εNFA.eval_nil

added theorem εNFA.eval_singleton

added theorem εNFA.mem_stepSet_iff

added theorem εNFA.pumping_lemma

added theorem εNFA.start_one

added theorem εNFA.start_zero

added def εNFA.stepSet

added theorem εNFA.stepSet_empty

added theorem εNFA.step_one

added theorem εNFA.step_zero

added theorem εNFA.subset_εClosure

added def εNFA.toNFA

added theorem εNFA.toNFA_correct

added theorem εNFA.toNFA_evalFrom_match

added inductive εNFA.εClosure

added theorem εNFA.εClosure_empty

added theorem εNFA.εClosure_univ

added structure εNFA