internlm/Lean-Github huggingface dataset:
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case left
α : 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 } ∈
            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 })
                M_1.symbol_arrow_list ∧
          stop_state ∈ stop_state_list) =
    fun p c q =>
    match (p, q) with
    | (Sum.inl p', 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 p', 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:
funext p c q
Proof state after:
case left.h.h.h
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p : σ_0 ⊕ σ_1
c : α
q : σ_0 ⊕ σ_1
⊢ (∃ stop_state_list,
      { start_state := p, symbol := c, stop_state_list := 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 })
              M_1.symbol_arrow_list ∧
        q ∈ stop_state_list) =
    match (p, q) with
    | (Sum.inl p', 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 p', 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
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 : σ_0
q0 : σ_1
⊢ (∃ stop_state_list,
      { start_state := Sum.inl p_0, symbol := c, stop_state_list := 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 })
              M_1.symbol_arrow_list ∧
        Sum.inr q0 ∈ stop_state_list) =
    match (Sum.inl p_0, Sum.inr q0) with
    | (Sum.inl p', 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 p', 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 _ q0 =>
  simp
  intro xs x _ _ _ a4
  simp only [← a4]
  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
c : α
p_0 q_0 : σ_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.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 })
              M_1.symbol_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list) =
    match (Sum.inl p_0, Sum.inl q_0) with
    | (Sum.inl p', 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 p', 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 only [eq_iff_iff]
Proof state after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_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.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 })
              M_1.symbol_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list) ↔
    ∃ stop_state_list,
      { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_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
c : α
p_0 q_0 : σ_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.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 })
              M_1.symbol_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list) ↔
    ∃ stop_state_list,
      { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_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
c : α
p_0 q_0 : σ_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.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 })
              M_1.symbol_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list) →
    ∃ stop_state_list,
      { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
        q_0 ∈ stop_state_list

case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
        q_0 ∈ stop_state_list) →
    ∃ stop_state_list,
      { start_state := Sum.inl p_0, symbol := c, stop_state_list := 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 })
              M_1.symbol_arrow_list ∧
        Sum.inl 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
c : α
p_0 q_0 : σ_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.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 })
              M_1.symbol_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list) →
    ∃ stop_state_list,
      { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
        q_0 ∈ stop_state_list
Tactic:
simp
Proof state after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
⊢ ∀ (x : List (σ_0 ⊕ σ_1)),
    ∀ x_1 ∈ M_0.symbol_arrow_list,
      x_1.start_state = p_0 →
        x_1.symbol = c →
          List.map Sum.inl x_1.stop_state_list = x →
            Sum.inl q_0 ∈ x →
              ∃ stop_state_list,
                { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_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
c : α
p_0 q_0 : σ_0
⊢ ∀ (x : List (σ_0 ⊕ σ_1)),
    ∀ x_1 ∈ M_0.symbol_arrow_list,
      x_1.start_state = p_0 →
        x_1.symbol = c →
          List.map Sum.inl x_1.stop_state_list = x →
            Sum.inl q_0 ∈ x →
              ∃ stop_state_list,
                { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
                  q_0 ∈ stop_state_list
Tactic:
intro xs x a1 a2 a3 a4 a5
Proof state after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a4 : List.map Sum.inl x.stop_state_list = xs
a5 : Sum.inl q_0 ∈ xs
⊢ ∃ stop_state_list,
    { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_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
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a4 : List.map Sum.inl x.stop_state_list = xs
a5 : Sum.inl q_0 ∈ xs
⊢ ∃ stop_state_list,
    { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
      q_0 ∈ stop_state_list
Tactic:
simp only [← a4] at a5
Proof state after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a4 : List.map Sum.inl x.stop_state_list = xs
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_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
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a4 : List.map Sum.inl x.stop_state_list = xs
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
      q_0 ∈ stop_state_list
Tactic:
clear a4
Proof state after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_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
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
      q_0 ∈ stop_state_list
Tactic:
simp only [← a2]
Proof state after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := x.start_state, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_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
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := x.start_state, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
      q_0 ∈ stop_state_list
Tactic:
simp only [← a3]
Proof state after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := x.start_state, symbol := x.symbol, stop_state_list := stop_state_list } ∈ M_0.symbol_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
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ ∃ stop_state_list,
    { start_state := x.start_state, symbol := x.symbol, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
      q_0 ∈ stop_state_list
Tactic:
apply Exists.intro x.stop_state_list
Proof state after:
case mp
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ { start_state := x.start_state, symbol := x.symbol, stop_state_list := x.stop_state_list } ∈ M_0.symbol_arrow_list ∧
    q_0 ∈ x.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
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ { start_state := x.start_state, symbol := x.symbol, stop_state_list := x.stop_state_list } ∈ M_0.symbol_arrow_list ∧
    q_0 ∈ x.stop_state_list
Tactic:
constructor
Proof state after:
case mp.left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ { start_state := x.start_state, symbol := x.symbol, stop_state_list := x.stop_state_list } ∈ M_0.symbol_arrow_list

case mp.right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ q_0 ∈ x.stop_state_list
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case mp.left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ { start_state := x.start_state, symbol := x.symbol, stop_state_list := x.stop_state_list } ∈ M_0.symbol_arrow_list
Tactic:
exact a1
Proof state after:
no goals
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case mp.right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : Sum.inl q_0 ∈ List.map Sum.inl x.stop_state_list
⊢ q_0 ∈ x.stop_state_list
Tactic:
simp at a5
Proof state after:
case mp.right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : q_0 ∈ x.stop_state_list
⊢ q_0 ∈ x.stop_state_list
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case mp.right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List (σ_0 ⊕ σ_1)
x : SymbolArrow α σ_0
a1 : x ∈ M_0.symbol_arrow_list
a2 : x.start_state = p_0
a3 : x.symbol = c
a5 : q_0 ∈ x.stop_state_list
⊢ q_0 ∈ x.stop_state_list
Tactic:
exact a5
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
c : α
p_0 q_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := p_0, symbol := c, stop_state_list := stop_state_list } ∈ M_0.symbol_arrow_list ∧
        q_0 ∈ stop_state_list) →
    ∃ stop_state_list,
      { start_state := Sum.inl p_0, symbol := c, stop_state_list := 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 })
              M_1.symbol_arrow_list ∧
        Sum.inl q_0 ∈ stop_state_list
Tactic:
simp
Proof state after:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
⊢ ∀ (x : List σ_0),
    { start_state := p_0, symbol := c, stop_state_list := x } ∈ M_0.symbol_arrow_list →
      q_0 ∈ x →
        ∃ stop_state_list,
          (∃ a ∈ M_0.symbol_arrow_list,
              a.start_state = p_0 ∧ a.symbol = c ∧ List.map Sum.inl a.stop_state_list = stop_state_list) ∧
            Sum.inl q_0 ∈ stop_state_list
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
⊢ ∀ (x : List σ_0),
    { start_state := p_0, symbol := c, stop_state_list := x } ∈ M_0.symbol_arrow_list →
      q_0 ∈ x →
        ∃ stop_state_list,
          (∃ a ∈ M_0.symbol_arrow_list,
              a.start_state = p_0 ∧ a.symbol = c ∧ List.map Sum.inl a.stop_state_list = stop_state_list) ∧
            Sum.inl q_0 ∈ stop_state_list
Tactic:
intro xs x a1
Proof state after:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List σ_0
x : { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list
a1 : q_0 ∈ xs
⊢ ∃ stop_state_list,
    (∃ a ∈ M_0.symbol_arrow_list,
        a.start_state = p_0 ∧ a.symbol = c ∧ List.map Sum.inl a.stop_state_list = stop_state_list) ∧
      Sum.inl q_0 ∈ stop_state_list
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List σ_0
x : { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list
a1 : q_0 ∈ xs
⊢ ∃ stop_state_list,
    (∃ a ∈ M_0.symbol_arrow_list,
        a.start_state = p_0 ∧ a.symbol = c ∧ List.map Sum.inl a.stop_state_list = stop_state_list) ∧
      Sum.inl q_0 ∈ stop_state_list
Tactic:
apply Exists.intro (xs.map Sum.inl)
Proof state after:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List σ_0
x : { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list
a1 : q_0 ∈ xs
⊢ (∃ a ∈ M_0.symbol_arrow_list,
      a.start_state = p_0 ∧ a.symbol = c ∧ List.map Sum.inl a.stop_state_list = List.map Sum.inl xs) ∧
    Sum.inl q_0 ∈ List.map Sum.inl xs
Theorem: match_union_EpsilonNFA_toAbstract
Proof state before:
case mpr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List σ_0
x : { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list
a1 : q_0 ∈ xs
⊢ (∃ a ∈ M_0.symbol_arrow_list,
      a.start_state = p_0 ∧ a.symbol = c ∧ List.map Sum.inl a.stop_state_list = List.map Sum.inl xs) ∧
    Sum.inl q_0 ∈ List.map Sum.inl xs
Tactic:
constructor
Proof state after:
case mpr.left
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List σ_0
x : { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list
a1 : q_0 ∈ xs
⊢ ∃ a ∈ M_0.symbol_arrow_list,
    a.start_state = p_0 ∧ a.symbol = c ∧ List.map Sum.inl a.stop_state_list = List.map Sum.inl xs

case mpr.right
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
c : α
p_0 q_0 : σ_0
xs : List σ_0
x : { start_state := p_0, symbol := c, stop_state_list := xs } ∈ M_0.symbol_arrow_list
a1 : q_0 ∈ xs
⊢ Sum.inl q_0 ∈ List.map Sum.inl xs