Theorem: match_concat_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈
              (EpsilonNFA.wrapRight ℕ (EpsilonNFA.wrapLeft σ_1 M_0)).symbol_arrow_list ++
                (EpsilonNFA.wrapRight ℕ (EpsilonNFA.wrapRight σ_0 M_1)).symbol_arrow_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 } ∈
              (EpsilonNFA.wrapRight ℕ (EpsilonNFA.wrapLeft σ_1 M_0)).epsilon_arrow_list ++
                  (EpsilonNFA.wrapRight ℕ (EpsilonNFA.wrapRight σ_0 M_1)).epsilon_arrow_list ++
                List.map
                  (fun accepting_state =>
                    { start_state := accepting_state,
                      stop_state_list := (EpsilonNFA.wrapRight ℕ (EpsilonNFA.wrapRight σ_0 M_1)).starting_state_list })
                  (EpsilonNFA.wrapRight ℕ (EpsilonNFA.wrapLeft σ_1 M_0)).accepting_state_list ∧
            stop_state ∈ stop_state_list,
      start := fun state => state ∈ (EpsilonNFA.wrapRight ℕ (EpsilonNFA.wrapLeft σ_1 M_0)).starting_state_list,
      accepting := fun state => state ∈ (EpsilonNFA.wrapRight ℕ (EpsilonNFA.wrapRight σ_0 M_1)).accepting_state_list } =
    {
      symbol := fun p c q =>
        match (p, q) with
        | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inl q')) =>
          ∃ stop_state_list,
            { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
              q' ∈ stop_state_list
        | (Sum.inr (Sum.inr p'), Sum.inr (Sum.inr q')) =>
          ∃ stop_state_list,
            { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
              q' ∈ stop_state_list
        | x => False,
      epsilon := fun p q =>
        match (p, q) with
        | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inl q')) =>
          ∃ stop_state_list,
            { start_state := p', stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q' ∈ stop_state_list
        | (Sum.inr (Sum.inr p'), Sum.inr (Sum.inr q')) =>
          ∃ stop_state_list,
            { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
        | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inr q')) => p' ∈ M_0.accepting_state_list ∧ q' ∈ M_1.starting_state_list
        | x => False,
      start := fun p =>
        match p with
        | Sum.inr (Sum.inl p') => p' ∈ M_0.starting_state_list
        | x => False,
      accepting := fun p =>
        match p with
        | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
        | x => False }
Tactic:
simp only [AbstractEpsilonNFA.mk.injEq]
Proof state after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ ((fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈
              (EpsilonNFA.wrapRight ℕ (EpsilonNFA.wrapLeft σ_1 M_0)).symbol_arrow_list ++
                (EpsilonNFA.wrapRight ℕ (EpsilonNFA.wrapRight σ_0 M_1)).symbol_arrow_list ∧
            stop_state ∈ stop_state_list) =
      fun p c q =>
      match (p, q) with
      | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inl q')) =>
        ∃ stop_state_list,
          { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
            q' ∈ stop_state_list
      | (Sum.inr (Sum.inr p'), Sum.inr (Sum.inr q')) =>
        ∃ stop_state_list,
          { start_state := p', symbol := c, stop_state_list := stop_state_list } ∈ M_1.symbol_arrow_list ∧
            q' ∈ stop_state_list
      | x => False) ∧
    ((fun start_state stop_state =>
          ∃ stop_state_list,
            { start_state := start_state, stop_state_list := stop_state_list } ∈
                (EpsilonNFA.wrapRight ℕ (EpsilonNFA.wrapLeft σ_1 M_0)).epsilon_arrow_list ++
                    (EpsilonNFA.wrapRight ℕ (EpsilonNFA.wrapRight σ_0 M_1)).epsilon_arrow_list ++
                  List.map
                    (fun accepting_state =>
                      { start_state := accepting_state,
                        stop_state_list :=
                          (EpsilonNFA.wrapRight ℕ (EpsilonNFA.wrapRight σ_0 M_1)).starting_state_list })
                    (EpsilonNFA.wrapRight ℕ (EpsilonNFA.wrapLeft σ_1 M_0)).accepting_state_list ∧
              stop_state ∈ stop_state_list) =
        fun p q =>
        match (p, q) with
        | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inl q')) =>
          ∃ stop_state_list,
            { start_state := p', stop_state_list := stop_state_list } ∈ M_0.epsilon_arrow_list ∧ q' ∈ stop_state_list
        | (Sum.inr (Sum.inr p'), Sum.inr (Sum.inr q')) =>
          ∃ stop_state_list,
            { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
        | (Sum.inr (Sum.inl p'), Sum.inr (Sum.inr q')) => p' ∈ M_0.accepting_state_list ∧ q' ∈ M_1.starting_state_list
        | x => False) ∧
      ((fun state => state ∈ (EpsilonNFA.wrapRight ℕ (EpsilonNFA.wrapLeft σ_1 M_0)).starting_state_list) = fun p =>
          match p with
          | Sum.inr (Sum.inl p') => p' ∈ M_0.starting_state_list
          | x => False) ∧
        (fun state => state ∈ (EpsilonNFA.wrapRight ℕ (EpsilonNFA.wrapRight σ_0 M_1)).accepting_state_list) = fun p =>
          match p with
          | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
          | x => False