Theorem: match_concat_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
q : ℕ ⊕ σ_0 ⊕ σ_1
p_0 : σ_1
⊢ (∃ stop_state_list,
      { start_state := Sum.inr (Sum.inr p_0), symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              (List.map
                (fun arrow =>
                  { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                    stop_state_list := List.map Sum.inl arrow.stop_state_list })
                M_0.symbol_arrow_list) ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              (List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                M_1.symbol_arrow_list) ∧
        q ∈ stop_state_list) =
    match (Sum.inr (Sum.inr p_0), 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
Tactic:
cases q
Proof state after:
case inl
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 : σ_1
val✝ : ℕ
⊢ (∃ stop_state_list,
      { start_state := Sum.inr (Sum.inr p_0), symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              (List.map
                (fun arrow =>
                  { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                    stop_state_list := List.map Sum.inl arrow.stop_state_list })
                M_0.symbol_arrow_list) ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              (List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                M_1.symbol_arrow_list) ∧
        Sum.inl val✝ ∈ stop_state_list) =
    match (Sum.inr (Sum.inr p_0), Sum.inl val✝) 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

case inr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 : σ_1
val✝ : σ_0 ⊕ σ_1
⊢ (∃ stop_state_list,
      { start_state := Sum.inr (Sum.inr p_0), symbol := c, stop_state_list := stop_state_list } ∈
          List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              (List.map
                (fun arrow =>
                  { start_state := Sum.inl arrow.start_state, symbol := arrow.symbol,
                    stop_state_list := List.map Sum.inl arrow.stop_state_list })
                M_0.symbol_arrow_list) ++
            List.map
              (fun arrow =>
                { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                  stop_state_list := List.map Sum.inr arrow.stop_state_list })
              (List.map
                (fun arrow =>
                  { start_state := Sum.inr arrow.start_state, symbol := arrow.symbol,
                    stop_state_list := List.map Sum.inr arrow.stop_state_list })
                M_1.symbol_arrow_list) ∧
        Sum.inr val✝ ∈ stop_state_list) =
    match (Sum.inr (Sum.inr p_0), Sum.inr val✝) 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