Theorem: match_zero_EpsilonNFA_toAbstract (FOL/Parsing/RegExpToEpsilonNFA.lean)

State before:
α : Type
inst✝ : DecidableEq α
⊢ (match_zero_EpsilonNFA α).toAbstract = match_zero_AbstractEpsilonNFA α
Tactic:
simp only [match_zero_EpsilonNFA]
State after:
α : Type
inst✝ : DecidableEq α
⊢ { symbol_arrow_list := [], epsilon_arrow_list := [], starting_state_list := [0],
        accepting_state_list := [] }.toAbstract =
    match_zero_AbstractEpsilonNFA α

State before:
α : Type
inst✝ : DecidableEq α
⊢ { symbol_arrow_list := [], epsilon_arrow_list := [], starting_state_list := [0],
        accepting_state_list := [] }.toAbstract =
    match_zero_AbstractEpsilonNFA α
Tactic:
simp only [EpsilonNFA.toAbstract]
State after:
α : Type
inst✝ : DecidableEq α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈ [] ∧
            stop_state ∈ stop_state_list,
      epsilon := fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := stop_state_list } ∈ [] ∧ stop_state ∈ stop_state_list,
      start := fun state => state ∈ [0], accepting := fun state => state ∈ [] } =
    match_zero_AbstractEpsilonNFA α

State before:
α : Type
inst✝ : DecidableEq α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈ [] ∧
            stop_state ∈ stop_state_list,
      epsilon := fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := stop_state_list } ∈ [] ∧ stop_state ∈ stop_state_list,
      start := fun state => state ∈ [0], accepting := fun state => state ∈ [] } =
    match_zero_AbstractEpsilonNFA α
Tactic:
simp only [match_zero_AbstractEpsilonNFA]
State after:
α : Type
inst✝ : DecidableEq α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈ [] ∧
            stop_state ∈ stop_state_list,
      epsilon := fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := stop_state_list } ∈ [] ∧ stop_state ∈ stop_state_list,
      start := fun state => state ∈ [0], accepting := fun state => state ∈ [] } =
    { symbol := fun x x x => False, epsilon := fun x x => False, start := fun p => p = 0, accepting := fun x => False }

State before:
α : Type
inst✝ : DecidableEq α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈ [] ∧
            stop_state ∈ stop_state_list,
      epsilon := fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := stop_state_list } ∈ [] ∧ stop_state ∈ stop_state_list,
      start := fun state => state ∈ [0], accepting := fun state => state ∈ [] } =
    { symbol := fun x x x => False, epsilon := fun x x => False, start := fun p => p = 0, accepting := fun x => False }
Tactic:
simp
State after:
no goals