internlm/Lean-Github huggingface dataset:
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
a1 :
  ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
⊢ ∃ stop_state_list,
    (∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
      Sum.inr q_0 ∈ stop_state_list
Tactic:
cases a1
Proof state after:
case mpr.intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
w✝ : List σ_1
h✝ : { start_state := p_0, stop_state_list := w✝ } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ w✝
⊢ ∃ stop_state_list,
    (∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
      Sum.inr q_0 ∈ stop_state_list
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2 : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ xs
⊢ ∃ stop_state_list,
    (∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
      Sum.inr q_0 ∈ stop_state_list
Tactic:
cases a2
Proof state after:
case intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
left✝ : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
right✝ : q_0 ∈ xs
⊢ ∃ stop_state_list,
    (∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
      Sum.inr q_0 ∈ stop_state_list
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ ∃ stop_state_list,
    (∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = stop_state_list) ∧
      Sum.inr q_0 ∈ stop_state_list
Tactic:
apply Exists.intro (xs.map Sum.inr)
Proof state after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ (∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = List.map Sum.inr xs) ∧
    Sum.inr q_0 ∈ List.map Sum.inr xs
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ (∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = List.map Sum.inr xs) ∧
    Sum.inr q_0 ∈ List.map Sum.inr xs
Tactic:
constructor
Proof state after:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ ∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = List.map Sum.inr xs

case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ Sum.inr q_0 ∈ List.map Sum.inr xs
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ ∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = List.map Sum.inr xs
Tactic:
apply Exists.intro { start_state := p_0, stop_state_list := xs }
Proof state after:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list ∧
    { start_state := p_0, stop_state_list := xs }.start_state = p_0 ∧
      List.map Sum.inr { start_state := p_0, stop_state_list := xs }.stop_state_list = List.map Sum.inr xs
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list ∧
    { start_state := p_0, stop_state_list := xs }.start_state = p_0 ∧
      List.map Sum.inr { start_state := p_0, stop_state_list := xs }.stop_state_list = List.map Sum.inr xs
Tactic:
simp
Proof state after:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
Tactic:
exact a2_left
Proof state after:
no goals
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ Sum.inr q_0 ∈ List.map Sum.inr xs
Tactic:
simp
Proof state after:
case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ q_0 ∈ xs
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List σ_1
a2_left : { start_state := p_0, stop_state_list := xs } ∈ M_1.epsilon_arrow_list
a2_right : q_0 ∈ xs
⊢ q_0 ∈ xs
Tactic:
exact a2_right
Proof state after:
no goals
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case right.right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ ((fun state => state ∈ List.map Sum.inl M_0.starting_state_list ++ List.map Sum.inr M_1.starting_state_list) =
      fun p =>
      match p with
      | Sum.inl p' => p' ∈ M_0.starting_state_list
      | Sum.inr p' => p' ∈ M_1.starting_state_list) ∧
    (fun state => state ∈ List.map Sum.inl M_0.accepting_state_list ++ List.map Sum.inr M_1.accepting_state_list) =
      fun p =>
      match p with
      | Sum.inl p' => p' ∈ M_0.accepting_state_list
      | Sum.inr p' => p' ∈ M_1.accepting_state_list
Tactic:
constructor
Proof state after:
case right.right.left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ (fun state => state ∈ List.map Sum.inl M_0.starting_state_list ++ List.map Sum.inr M_1.starting_state_list) = fun p =>
    match p with
    | Sum.inl p' => p' ∈ M_0.starting_state_list
    | Sum.inr p' => p' ∈ M_1.starting_state_list

case right.right.right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ (fun state => state ∈ List.map Sum.inl M_0.accepting_state_list ++ List.map Sum.inr M_1.accepting_state_list) =
    fun p =>
    match p with
    | Sum.inl p' => p' ∈ M_0.accepting_state_list
    | Sum.inr p' => p' ∈ M_1.accepting_state_list
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case right.right.left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ (fun state => state ∈ List.map Sum.inl M_0.starting_state_list ++ List.map Sum.inr M_1.starting_state_list) = fun p =>
    match p with
    | Sum.inl p' => p' ∈ M_0.starting_state_list
    | Sum.inr p' => p' ∈ M_1.starting_state_list
Tactic:
funext p
Proof state after:
case right.right.left.h
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p : σ_0 ⊕ σ_1
⊢ (p ∈ List.map Sum.inl M_0.starting_state_list ++ List.map Sum.inr M_1.starting_state_list) =
    match p with
    | Sum.inl p' => p' ∈ M_0.starting_state_list
    | Sum.inr p' => p' ∈ M_1.starting_state_list
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case right.right.left.h
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p : σ_0 ⊕ σ_1
⊢ (p ∈ List.map Sum.inl M_0.starting_state_list ++ List.map Sum.inr M_1.starting_state_list) =
    match p with
    | Sum.inl p' => p' ∈ M_0.starting_state_list
    | Sum.inr p' => p' ∈ M_1.starting_state_list
Tactic:
cases p
Proof state after:
case right.right.left.h.inl
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
val✝ : σ_0
⊢ (Sum.inl val✝ ∈ List.map Sum.inl M_0.starting_state_list ++ List.map Sum.inr M_1.starting_state_list) =
    match Sum.inl val✝ with
    | Sum.inl p' => p' ∈ M_0.starting_state_list
    | Sum.inr p' => p' ∈ M_1.starting_state_list

case right.right.left.h.inr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
val✝ : σ_1
⊢ (Sum.inr val✝ ∈ List.map Sum.inl M_0.starting_state_list ++ List.map Sum.inr M_1.starting_state_list) =
    match Sum.inr val✝ with
    | Sum.inl p' => p' ∈ M_0.starting_state_list
    | Sum.inr p' => p' ∈ M_1.starting_state_list
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case right.right.left.h.inl
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
val✝ : σ_0
⊢ (Sum.inl val✝ ∈ List.map Sum.inl M_0.starting_state_list ++ List.map Sum.inr M_1.starting_state_list) =
    match Sum.inl val✝ with
    | Sum.inl p' => p' ∈ M_0.starting_state_list
    | Sum.inr p' => p' ∈ M_1.starting_state_list
Tactic:
simp
Proof state after:
no goals
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case right.right.left.h.inr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
val✝ : σ_1
⊢ (Sum.inr val✝ ∈ List.map Sum.inl M_0.starting_state_list ++ List.map Sum.inr M_1.starting_state_list) =
    match Sum.inr val✝ with
    | Sum.inl p' => p' ∈ M_0.starting_state_list
    | Sum.inr p' => p' ∈ M_1.starting_state_list
Tactic:
simp
Proof state after:
no goals
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case right.right.right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ (fun state => state ∈ List.map Sum.inl M_0.accepting_state_list ++ List.map Sum.inr M_1.accepting_state_list) =
    fun p =>
    match p with
    | Sum.inl p' => p' ∈ M_0.accepting_state_list
    | Sum.inr p' => p' ∈ M_1.accepting_state_list
Tactic:
funext p
Proof state after:
case right.right.right.h
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p : σ_0 ⊕ σ_1
⊢ (p ∈ List.map Sum.inl M_0.accepting_state_list ++ List.map Sum.inr M_1.accepting_state_list) =
    match p with
    | Sum.inl p' => p' ∈ M_0.accepting_state_list
    | Sum.inr p' => p' ∈ M_1.accepting_state_list
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case right.right.right.h
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p : σ_0 ⊕ σ_1
⊢ (p ∈ List.map Sum.inl M_0.accepting_state_list ++ List.map Sum.inr M_1.accepting_state_list) =
    match p with
    | Sum.inl p' => p' ∈ M_0.accepting_state_list
    | Sum.inr p' => p' ∈ M_1.accepting_state_list
Tactic:
cases p
Proof state after:
case right.right.right.h.inl
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
val✝ : σ_0
⊢ (Sum.inl val✝ ∈ List.map Sum.inl M_0.accepting_state_list ++ List.map Sum.inr M_1.accepting_state_list) =
    match Sum.inl val✝ with
    | Sum.inl p' => p' ∈ M_0.accepting_state_list
    | Sum.inr p' => p' ∈ M_1.accepting_state_list

case right.right.right.h.inr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
val✝ : σ_1
⊢ (Sum.inr val✝ ∈ List.map Sum.inl M_0.accepting_state_list ++ List.map Sum.inr M_1.accepting_state_list) =
    match Sum.inr val✝ with
    | Sum.inl p' => p' ∈ M_0.accepting_state_list
    | Sum.inr p' => p' ∈ M_1.accepting_state_list
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case right.right.right.h.inl
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
val✝ : σ_0
⊢ (Sum.inl val✝ ∈ List.map Sum.inl M_0.accepting_state_list ++ List.map Sum.inr M_1.accepting_state_list) =
    match Sum.inl val✝ with
    | Sum.inl p' => p' ∈ M_0.accepting_state_list
    | Sum.inr p' => p' ∈ M_1.accepting_state_list
Tactic:
simp
Proof state after:
no goals
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case right.right.right.h.inr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
val✝ : σ_1
⊢ (Sum.inr val✝ ∈ List.map Sum.inl M_0.accepting_state_list ++ List.map Sum.inr M_1.accepting_state_list) =
    match Sum.inr val✝ with
    | Sum.inl p' => p' ∈ M_0.accepting_state_list
    | Sum.inr p' => p' ∈ M_1.accepting_state_list
Tactic:
simp
Proof state after:
no goals
Theorem: match_concat_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ (match_concat_EpsilonNFA α σ_0 σ_1 M_0 M_1).toAbstract =
    match_concat_AbstractEpsilonNFA α σ_0 σ_1 M_0.toAbstract M_1.toAbstract
Tactic:
simp only [match_concat_EpsilonNFA]
Proof state after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ {
        symbol_arrow_list :=
          (EpsilonNFA.wrapRight ℕ (EpsilonNFA.wrapLeft σ_1 M_0)).symbol_arrow_list ++
            (EpsilonNFA.wrapRight ℕ (EpsilonNFA.wrapRight σ_0 M_1)).symbol_arrow_list,
        epsilon_arrow_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,
        starting_state_list := (EpsilonNFA.wrapRight ℕ (EpsilonNFA.wrapLeft σ_1 M_0)).starting_state_list,
        accepting_state_list :=
          (EpsilonNFA.wrapRight ℕ (EpsilonNFA.wrapRight σ_0 M_1)).accepting_state_list }.toAbstract =
    match_concat_AbstractEpsilonNFA α σ_0 σ_1 M_0.toAbstract M_1.toAbstract
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 : ℕ
⊢ (∃ stop_state_list,
      { start_state := Sum.inl 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.inl 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:
case _ p_0 =>
  simp
Proof state after:
no goals
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 : σ_0 ⊕ σ_1
⊢ (∃ stop_state_list,
      { start_state := 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 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:
case _ p_0 =>
  cases p_0
  case _ p_0 =>
    cases q
    case _ q_0 =>
      simp
      intro xs x a1 a2 a3 a4
      simp only [← a4]
      simp
    case _ q_0 =>
      cases q_0
      case _ q_0 =>
        simp
        sorry
      case _ q_0 =>
        simp
        intro xs x a1 a2 a3 a4
        simp only [← a4]
        simp
  case _ p_0 =>
    cases q
    case _ q_0 =>
      simp
      intro xs x a1 a2 a3 a4
      simp only [← a4]
      simp
    case _ q_0 =>
      cases q_0
      case _ q_0 =>
        simp
        intro xs x a1 a2 a3 a4
        simp only [← a4]
        simp
      case _ q_0 =>
        simp
        sorry
Proof state after:
no goals
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 : ℕ
⊢ (∃ stop_state_list,
      { start_state := Sum.inl 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.inl 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:
simp
Proof state after:
no goals
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 : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inr (Sum.inl 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.inl 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:
case _ p_0 =>
  cases q
  case _ q_0 =>
    simp
    intro xs x a1 a2 a3 a4
    simp only [← a4]
    simp
  case _ q_0 =>
    cases q_0
    case _ q_0 =>
      simp
      sorry
    case _ q_0 =>
      simp
      intro xs x a1 a2 a3 a4
      simp only [← a4]
      simp
Proof state after:
no goals