Theorem: NFA.DFA_fromNFA_lang_subs_lang (FormalSystems/Chomsky/Regular/PowersetConstruction.lean)

State before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
⊢ DFA.AcceptedLanguage (DFA.fromNFA M) ⊆ AcceptedLanguage M
Tactic:
intro w ⟨_, hr⟩
State after:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
⊢ w ∈ AcceptedLanguage M

State before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
⊢ w ∈ AcceptedLanguage M
Tactic:
have ⟨q, hq, r, _⟩ := DFA.fromNFA_run_imp_run hr
State after:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ ↑(DFA.fromNFA M).q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ w ∈ AcceptedLanguage M

State before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ ↑(DFA.fromNFA M).q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ w ∈ AcceptedLanguage M
Tactic:
exists q
State after:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ ↑(DFA.fromNFA M).q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ q ∈ M.Q₀ ∧ ∃ run, Run.last run ∈ M.F

State before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ ↑(DFA.fromNFA M).q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ q ∈ M.Q₀ ∧ ∃ run, Run.last run ∈ M.F
Tactic:
dsimp [DFA.fromNFA] at hq
State after:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ M.Q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ q ∈ M.Q₀ ∧ ∃ run, Run.last run ∈ M.F

State before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ M.Q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ q ∈ M.Q₀ ∧ ∃ run, Run.last run ∈ M.F
Tactic:
constructor
State after:
case left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ M.Q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ q ∈ M.Q₀

case right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ M.Q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ ∃ run, Run.last run ∈ M.F

State before:
case left
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ M.Q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ q ∈ M.Q₀

case right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ M.Q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ ∃ run, Run.last run ∈ M.F
Tactic:
assumption
State after:
case right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ M.Q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ ∃ run, Run.last run ∈ M.F

State before:
case right
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ (DFA.fromNFA M).Z }
w✝ : DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
hr : Run.last w✝ ∈ (DFA.fromNFA M).F
q : { x // x ∈ M.Q }
hq : q ∈ M.Q₀
r : Run M q w
h✝ : Run.last r ∈ M.F
⊢ ∃ run, Run.last run ∈ M.F
Tactic:
exists r
State after:
no goals