internlm/Lean-Github huggingface dataset:
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : σ_1
⊢ (∃ stop_state_list,
      { start_state := Sum.inl p_0, stop_state_list := 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 })
              M_1.epsilon_arrow_list ∧
        Sum.inr q_0 ∈ stop_state_list) =
    match (Sum.inl p_0, Sum.inr q_0) with
    | (Sum.inl p', 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 p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | x => False
Tactic:
simp
Proof state after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : σ_1
⊢ ∀ (x : List (σ_0 ⊕ σ_1)),
    ∀ x_1 ∈ M_0.epsilon_arrow_list, x_1.start_state = p_0 → List.map Sum.inl x_1.stop_state_list = x → Sum.inr q_0 ∉ x
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : σ_1
⊢ ∀ (x : List (σ_0 ⊕ σ_1)),
    ∀ x_1 ∈ M_0.epsilon_arrow_list, x_1.start_state = p_0 → List.map Sum.inl x_1.stop_state_list = x → Sum.inr q_0 ∉ x
Tactic:
intro xs x _ _ a3
Proof state after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a✝¹ : x ∈ M_0.epsilon_arrow_list
a✝ : x.start_state = p_0
a3 : List.map Sum.inl x.stop_state_list = xs
⊢ Sum.inr q_0 ∉ 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 : σ_0
q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a✝¹ : x ∈ M_0.epsilon_arrow_list
a✝ : x.start_state = p_0
a3 : List.map Sum.inl x.stop_state_list = xs
⊢ Sum.inr q_0 ∉ xs
Tactic:
simp only [← a3]
Proof state after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a✝¹ : x ∈ M_0.epsilon_arrow_list
a✝ : x.start_state = p_0
a3 : List.map Sum.inl x.stop_state_list = xs
⊢ Sum.inr q_0 ∉ List.map Sum.inl x.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 : σ_0
q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a✝¹ : x ∈ M_0.epsilon_arrow_list
a✝ : x.start_state = p_0
a3 : List.map Sum.inl x.stop_state_list = xs
⊢ Sum.inr q_0 ∉ List.map Sum.inl x.stop_state_list
Tactic:
simp
Proof state after:
no goals
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inr p_0, stop_state_list := 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 })
              M_1.epsilon_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list) =
    match (Sum.inr p_0, Sum.inl q_0) with
    | (Sum.inl p', 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 p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | x => False
Tactic:
case _ q_0 =>
  simp
  intro xs x _ _ a3
  simp only [← a3]
  simp
Proof state after:
no goals
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inr p_0, stop_state_list := 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 })
              M_1.epsilon_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list) =
    match (Sum.inr p_0, Sum.inl q_0) with
    | (Sum.inl p', 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 p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | x => False
Tactic:
simp
Proof state after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : σ_0
⊢ ∀ (x : List (σ_0 ⊕ σ_1)),
    ∀ x_1 ∈ M_1.epsilon_arrow_list, x_1.start_state = p_0 → List.map Sum.inr x_1.stop_state_list = x → Sum.inl q_0 ∉ x
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : σ_0
⊢ ∀ (x : List (σ_0 ⊕ σ_1)),
    ∀ x_1 ∈ M_1.epsilon_arrow_list, x_1.start_state = p_0 → List.map Sum.inr x_1.stop_state_list = x → Sum.inl q_0 ∉ x
Tactic:
intro xs x _ _ a3
Proof state after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a✝¹ : x ∈ M_1.epsilon_arrow_list
a✝ : x.start_state = p_0
a3 : List.map Sum.inr x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ 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 : σ_1
q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a✝¹ : x ∈ M_1.epsilon_arrow_list
a✝ : x.start_state = p_0
a3 : List.map Sum.inr x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Tactic:
simp only [← a3]
Proof state after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_1
q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a✝¹ : x ∈ M_1.epsilon_arrow_list
a✝ : x.start_state = p_0
a3 : List.map Sum.inr x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ List.map Sum.inr x.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 : σ_1
q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a✝¹ : x ∈ M_1.epsilon_arrow_list
a✝ : x.start_state = p_0
a3 : List.map Sum.inr x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ List.map Sum.inr x.stop_state_list
Tactic:
simp
Proof state after:
no goals
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
⊢ (∃ stop_state_list,
      { start_state := Sum.inr p_0, stop_state_list := 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 })
              M_1.epsilon_arrow_list ∧
        Sum.inr q_0 ∈ stop_state_list) =
    match (Sum.inr p_0, Sum.inr q_0) with
    | (Sum.inl p', 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 p', Sum.inr q') =>
      ∃ stop_state_list,
        { start_state := p', stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q' ∈ stop_state_list
    | x => False
Tactic:
simp
Proof state after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
⊢ (∃ 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) ↔
    ∃ stop_state_list,
      { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ 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
⊢ (∃ 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) ↔
    ∃ stop_state_list,
      { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
constructor
Proof state after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
⊢ (∃ 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) →
    ∃ stop_state_list,
      { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list

case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
⊢ (∃ 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
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
⊢ (∃ 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) →
    ∃ stop_state_list,
      { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
intro a1
Proof state after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
a1 :
  ∃ 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
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
a1 :
  ∃ 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
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
cases a1
Proof state after:
case mp.intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
w✝ : List (σ_0 ⊕ σ_1)
h✝ : (∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = w✝) ∧ Sum.inr q_0 ∈ w✝
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ 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 (σ_0 ⊕ σ_1)
a2 : (∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = xs) ∧ Sum.inr q_0 ∈ xs
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ 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 (σ_0 ⊕ σ_1)
left✝ : ∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = xs
right✝ : Sum.inr q_0 ∈ xs
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ 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 (σ_0 ⊕ σ_1)
a2_left : ∃ a ∈ M_1.epsilon_arrow_list, a.start_state = p_0 ∧ List.map Sum.inr a.stop_state_list = xs
a2_right : Sum.inr q_0 ∈ xs
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
cases a2_left
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 (σ_0 ⊕ σ_1)
a2_right : Sum.inr q_0 ∈ xs
w✝ : EpsilonArrow σ_1
h✝ : w✝ ∈ M_1.epsilon_arrow_list ∧ w✝.start_state = p_0 ∧ List.map Sum.inr w✝.stop_state_list = xs
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ 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 (σ_0 ⊕ σ_1)
a2_right : Sum.inr q_0 ∈ xs
x : EpsilonArrow σ_1
a3 : x ∈ M_1.epsilon_arrow_list ∧ x.start_state = p_0 ∧ List.map Sum.inr x.stop_state_list = xs
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
cases a3
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 (σ_0 ⊕ σ_1)
a2_right : Sum.inr q_0 ∈ xs
x : EpsilonArrow σ_1
left✝ : x ∈ M_1.epsilon_arrow_list
right✝ : x.start_state = p_0 ∧ List.map Sum.inr x.stop_state_list = xs
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ 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 (σ_0 ⊕ σ_1)
a2_right : Sum.inr q_0 ∈ xs
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right : x.start_state = p_0 ∧ List.map Sum.inr x.stop_state_list = xs
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
cases a3_right
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 (σ_0 ⊕ σ_1)
a2_right : Sum.inr q_0 ∈ xs
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
left✝ : x.start_state = p_0
right✝ : List.map Sum.inr x.stop_state_list = xs
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ 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 (σ_0 ⊕ σ_1)
a2_right : Sum.inr q_0 ∈ xs
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a3_right_right : List.map Sum.inr x.stop_state_list = xs
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
simp only [← a3_right_right] at a2_right
Proof state after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a3_right_right : List.map Sum.inr x.stop_state_list = xs
a2_right : Sum.inr q_0 ∈ List.map Sum.inr x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ 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 (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a3_right_right : List.map Sum.inr x.stop_state_list = xs
a2_right : Sum.inr q_0 ∈ List.map Sum.inr x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
clear a3_right_right
Proof state after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : Sum.inr q_0 ∈ List.map Sum.inr x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ 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 (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : Sum.inr q_0 ∈ List.map Sum.inr x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
simp at a2_right
Proof state after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ 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 (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p_0, stop_state_list := stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ stop_state_list
Tactic:
apply Exists.intro x.stop_state_list
Proof state after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ { start_state := p_0, stop_state_list := x.stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ x.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 (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ { start_state := p_0, stop_state_list := x.stop_state_list } ∈ M_1.epsilon_arrow_list ∧ q_0 ∈ x.stop_state_list
Tactic:
simp only [← a3_right_left]
Proof state after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ { start_state := x.start_state, stop_state_list := x.stop_state_list } ∈ M_1.epsilon_arrow_list ∧
    q_0 ∈ x.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 (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ { start_state := x.start_state, stop_state_list := x.stop_state_list } ∈ M_1.epsilon_arrow_list ∧
    q_0 ∈ x.stop_state_list
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 (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ { start_state := x.start_state, stop_state_list := x.stop_state_list } ∈ M_1.epsilon_arrow_list

case right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 q_0 : σ_1
xs : List (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ q_0 ∈ x.stop_state_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 (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ { start_state := x.start_state, stop_state_list := x.stop_state_list } ∈ M_1.epsilon_arrow_list
Tactic:
exact a3_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 (σ_0 ⊕ σ_1)
x : EpsilonArrow σ_1
a3_left : x ∈ M_1.epsilon_arrow_list
a3_right_left : x.start_state = p_0
a2_right : q_0 ∈ x.stop_state_list
⊢ q_0 ∈ x.stop_state_list
Tactic:
exact a2_right
Proof state after:
no goals
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
⊢ (∃ 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:
intro a1
Proof state after:
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