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

State before:
α : Type
inst✝ : DecidableEq α
c : α
⊢ (match_char_EpsilonNFA c).toAbstract = match_char_AbstractEpsilonNFA c
Tactic:
simp only [match_char_EpsilonNFA]
State after:
α : Type
inst✝ : DecidableEq α
c : α
⊢ { symbol_arrow_list := [{ start_state := 0, symbol := c, stop_state_list := [1] }], epsilon_arrow_list := [],
        starting_state_list := [0], accepting_state_list := [1] }.toAbstract =
    match_char_AbstractEpsilonNFA c

State before:
α : Type
inst✝ : DecidableEq α
c : α
⊢ { symbol_arrow_list := [{ start_state := 0, symbol := c, stop_state_list := [1] }], epsilon_arrow_list := [],
        starting_state_list := [0], accepting_state_list := [1] }.toAbstract =
    match_char_AbstractEpsilonNFA c
Tactic:
simp only [EpsilonNFA.toAbstract]
State after:
α : Type
inst✝ : DecidableEq α
c : α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈
              [{ start_state := 0, symbol := c, stop_state_list := [1] }] ∧
            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 ∈ [1] } =
    match_char_AbstractEpsilonNFA c

State before:
α : Type
inst✝ : DecidableEq α
c : α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈
              [{ start_state := 0, symbol := c, stop_state_list := [1] }] ∧
            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 ∈ [1] } =
    match_char_AbstractEpsilonNFA c
Tactic:
simp only [match_char_AbstractEpsilonNFA]
State after:
α : Type
inst✝ : DecidableEq α
c : α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈
              [{ start_state := 0, symbol := c, stop_state_list := [1] }] ∧
            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 ∈ [1] } =
    { symbol := fun p a q => p = 0 ∧ a = c ∧ q = 1, epsilon := fun x x => False, start := fun p => p = 0,
      accepting := fun p => p = 1 }

State before:
α : Type
inst✝ : DecidableEq α
c : α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈
              [{ start_state := 0, symbol := c, stop_state_list := [1] }] ∧
            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 ∈ [1] } =
    { symbol := fun p a q => p = 0 ∧ a = c ∧ q = 1, epsilon := fun x x => False, start := fun p => p = 0,
      accepting := fun p => p = 1 }
Tactic:
simp
State after:
α : Type
inst✝ : DecidableEq α
c : α
⊢ (fun start_state symbol stop_state =>
      ∃ stop_state_list, (start_state = 0 ∧ symbol = c ∧ stop_state_list = [1]) ∧ stop_state ∈ stop_state_list) =
    fun p a q => p = 0 ∧ a = c ∧ q = 1

State before:
α : Type
inst✝ : DecidableEq α
c : α
⊢ (fun start_state symbol stop_state =>
      ∃ stop_state_list, (start_state = 0 ∧ symbol = c ∧ stop_state_list = [1]) ∧ stop_state ∈ stop_state_list) =
    fun p a q => p = 0 ∧ a = c ∧ q = 1
Tactic:
simp only [← and_assoc]
State after:
α : Type
inst✝ : DecidableEq α
c : α
⊢ (fun start_state symbol stop_state =>
      ∃ stop_state_list, ((start_state = 0 ∧ symbol = c) ∧ stop_state_list = [1]) ∧ stop_state ∈ stop_state_list) =
    fun p a q => (p = 0 ∧ a = c) ∧ q = 1

State before:
α : Type
inst✝ : DecidableEq α
c : α
⊢ (fun start_state symbol stop_state =>
      ∃ stop_state_list, ((start_state = 0 ∧ symbol = c) ∧ stop_state_list = [1]) ∧ stop_state ∈ stop_state_list) =
    fun p a q => (p = 0 ∧ a = c) ∧ q = 1
Tactic:
simp only [and_right_comm]
State after:
α : Type
inst✝ : DecidableEq α
c : α
⊢ (fun start_state symbol stop_state =>
      ∃ stop_state_list, ((start_state = 0 ∧ symbol = c) ∧ stop_state ∈ stop_state_list) ∧ stop_state_list = [1]) =
    fun p a q => (p = 0 ∧ a = c) ∧ q = 1

State before:
α : Type
inst✝ : DecidableEq α
c : α
⊢ (fun start_state symbol stop_state =>
      ∃ stop_state_list, ((start_state = 0 ∧ symbol = c) ∧ stop_state ∈ stop_state_list) ∧ stop_state_list = [1]) =
    fun p a q => (p = 0 ∧ a = c) ∧ q = 1
Tactic:
simp
State after:
no goals