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

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

State before:
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ w ∈ DFA.AcceptedLanguage (DFA.fromNFA M)
Tactic:
constructor
State after:
case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last ?w ∈ (DFA.fromNFA M).F

case w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w

State before:
case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last ?w ∈ (DFA.fromNFA M).F

case w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w
Tactic:
swap
State after:
case w
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ DFA.Run (DFA.fromNFA M) (DFA.fromNFA M).q₀ w

case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last ?w ∈ (DFA.fromNFA M).F

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

case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last ?w ∈ (DFA.fromNFA M).F
Tactic:
apply DFA.fromNFA.RunFromRestricted
State after:
case w.r
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ DFA.Run (DFA.fromNFA M) ?w.q w

case w.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ ↑?w.q ⊆ ↑(DFA.fromNFA M).q₀

case w.q
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ { x // x ∈ (DFA.toNFA (DFA.fromNFA M)).Q }

case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.RunFromRestricted ?w.r ?w.h) ∈ (DFA.fromNFA M).F

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

case w.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ ↑?w.q ⊆ ↑(DFA.fromNFA M).q₀

case w.q
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ { x // x ∈ (DFA.toNFA (DFA.fromNFA M)).Q }

case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.RunFromRestricted ?w.r ?w.h) ∈ (DFA.fromNFA M).F
Tactic:
apply DFA.fromNFA.NFARunToRun
State after:
case w.r.r
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run M ?w.r.q w

case w.r.q
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ { x // x ∈ M.Q }

case w.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ ↑{ val := {?w.r.q}, property := ⋯ } ⊆ ↑(DFA.fromNFA M).q₀

case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.RunFromRestricted (DFA.fromNFA.NFARunToRun ?w.r.r) ?w.h) ∈ (DFA.fromNFA M).F

State before:
case w.r.r
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run M ?w.r.q w

case w.r.q
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ { x // x ∈ M.Q }

case w.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ ↑{ val := {?w.r.q}, property := ⋯ } ⊆ ↑(DFA.fromNFA M).q₀

case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.RunFromRestricted (DFA.fromNFA.NFARunToRun ?w.r.r) ?w.h) ∈ (DFA.fromNFA M).F
Tactic:
assumption
State after:
case w.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ ↑{ val := {w✝}, property := ⋯ } ⊆ ↑(DFA.fromNFA M).q₀

case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.RunFromRestricted (DFA.fromNFA.NFARunToRun run) ?w.h) ∈ (DFA.fromNFA M).F

State before:
case w.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ ↑{ val := {w✝}, property := ⋯ } ⊆ ↑(DFA.fromNFA M).q₀

case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.RunFromRestricted (DFA.fromNFA.NFARunToRun run) ?w.h) ∈ (DFA.fromNFA M).F
Tactic:
simp [DFA.fromNFA]
State after:
case w.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ w✝ ∈ M.Q₀

case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.RunFromRestricted (DFA.fromNFA.NFARunToRun run) ⋯) ∈ (DFA.fromNFA M).F

State before:
case w.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ w✝ ∈ M.Q₀

case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.RunFromRestricted (DFA.fromNFA.NFARunToRun run) ⋯) ∈ (DFA.fromNFA M).F
Tactic:
assumption
State after:
case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.RunFromRestricted (DFA.fromNFA.NFARunToRun run) ⋯) ∈ (DFA.fromNFA M).F

State before:
case h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.RunFromRestricted (DFA.fromNFA.NFARunToRun run) ⋯) ∈ (DFA.fromNFA M).F
Tactic:
apply DFA.fromNFA.RunFromRestricted_final
State after:
case h.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.NFARunToRun run) ∈ (DFA.fromNFA M).F

State before:
case h.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last (DFA.fromNFA.NFARunToRun run) ∈ (DFA.fromNFA M).F
Tactic:
apply DFA.fromNFA.NFARunToRun_final_imp_final
State after:
case h.h.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last run ∈ M.F

State before:
case h.h.h
α qs : Type
inst✝³ : DecidableEq α
inst✝² : DecidableEq qs
inst✝¹ : DecidableEq α
inst✝ : DecidableEq qs
M : NFA α qs
w : Word { x // x ∈ M.Z }
w✝ : { x // x ∈ M.Q }
h_start : w✝ ∈ M.Q₀
run : Run M w✝ w
h_run : Run.last run ∈ M.F
⊢ Run.last run ∈ M.F
Tactic:
assumption
State after:
no goals