Theorem: match_concat_EpsilonNFA_toAbstract
Proof state before:
case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ ((fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := stop_state_list } ∈
              List.map
                    (fun arrow =>
                      { start_state := Sum.inr arrow.start_state,
                        stop_state_list := List.map Sum.inr arrow.stop_state_list })
                    (List.map
                      (fun arrow =>
                        { start_state := Sum.inl arrow.start_state,
                          stop_state_list := List.map Sum.inl arrow.stop_state_list })
                      M_0.epsilon_arrow_list) ++
                  List.map
                    (fun arrow =>
                      { start_state := Sum.inr arrow.start_state,
                        stop_state_list := List.map Sum.inr arrow.stop_state_list })
                    (List.map
                      (fun arrow =>
                        { start_state := Sum.inr arrow.start_state,
                          stop_state_list := List.map Sum.inr arrow.stop_state_list })
                      M_1.epsilon_arrow_list) ++
                List.map
                  (fun accepting_state =>
                    { start_state := accepting_state,
                      stop_state_list := List.map Sum.inr (List.map Sum.inr M_1.starting_state_list) })
                  (List.map Sum.inr (List.map Sum.inl 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 ∈ List.map Sum.inr (List.map Sum.inl 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 ∈ List.map Sum.inr (List.map Sum.inr M_1.accepting_state_list)) = fun p =>
        match p with
        | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
        | x => False
Tactic:
constructor
Proof state after:
case right.left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ (fun start_state stop_state =>
      ∃ stop_state_list,
        { start_state := start_state, stop_state_list := stop_state_list } ∈
            List.map
                  (fun arrow =>
                    { start_state := Sum.inr arrow.start_state,
                      stop_state_list := List.map Sum.inr arrow.stop_state_list })
                  (List.map
                    (fun arrow =>
                      { start_state := Sum.inl arrow.start_state,
                        stop_state_list := List.map Sum.inl arrow.stop_state_list })
                    M_0.epsilon_arrow_list) ++
                List.map
                  (fun arrow =>
                    { start_state := Sum.inr arrow.start_state,
                      stop_state_list := List.map Sum.inr arrow.stop_state_list })
                  (List.map
                    (fun arrow =>
                      { start_state := Sum.inr arrow.start_state,
                        stop_state_list := List.map Sum.inr arrow.stop_state_list })
                    M_1.epsilon_arrow_list) ++
              List.map
                (fun accepting_state =>
                  { start_state := accepting_state,
                    stop_state_list := List.map Sum.inr (List.map Sum.inr M_1.starting_state_list) })
                (List.map Sum.inr (List.map Sum.inl 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

case right.right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ ((fun state => state ∈ List.map Sum.inr (List.map Sum.inl 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 ∈ List.map Sum.inr (List.map Sum.inr M_1.accepting_state_list)) = fun p =>
      match p with
      | Sum.inr (Sum.inr p') => p' ∈ M_1.accepting_state_list
      | x => False