internlm/Lean-Github huggingface dataset:
Theorem: match_concat_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
q : ℕ ⊕ σ_0 ⊕ σ_1
p_0 : σ_0
⊢ (∃ stop_state_list,
      { start_state := Sum.inr (Sum.inl p_0), 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)) ∧
        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', 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
Tactic:
case _ p_0 =>
  cases q
  case _ q_0 =>
    simp
    intro xs a1
    cases a1
    case _ left =>
      cases left
      case _ x a2 =>
        cases a2
        case _ a2_left a2_right =>
          cases a2_right
          case _ a2_right_left a2_right_right =>
            simp only [← a2_right_right]
            simp
    case _ right =>
      cases right
      case _ x a2 =>
        cases a2
        case _ a2_left a2_right =>
          cases a2_right
          case _ a2_right_left a2_right_right =>
            simp only [← a2_right_right]
            simp
  case _ q_0 =>
    cases q_0
    case _ q_0 =>
      simp
      sorry
    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
q : ℕ ⊕ σ_0 ⊕ σ_1
p_0 : σ_1
⊢ (∃ stop_state_list,
      { start_state := Sum.inr (Sum.inr p_0), 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)) ∧
        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', 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
Tactic:
case _ p_0 =>
  cases q
  case _ q_0 =>
    simp
    intro xs x a1 a2 a3
    simp only [← a3]
    simp
  case _ q_0 =>
    cases q_0
    case _ q_0 =>
      simp
      intro xs x a1 a2 a3
      simp only [← a3]
      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
p_0 : σ_0
q_0 : ℕ
⊢ (∃ stop_state_list,
      { start_state := Sum.inr (Sum.inl p_0), 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)) ∧
        Sum.inl q_0 ∈ stop_state_list) =
    match (Sum.inr (Sum.inl p_0), Sum.inl q_0) 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
Tactic:
case _ q_0 =>
  simp
  intro xs a1
  cases a1
  case _ left =>
    cases left
    case _ x a2 =>
      cases a2
      case _ a2_left a2_right =>
        cases a2_right
        case _ a2_right_left a2_right_right =>
          simp only [← a2_right_right]
          simp
  case _ right =>
    cases right
    case _ x a2 =>
      cases a2
      case _ a2_left a2_right =>
        cases a2_right
        case _ a2_right_left a2_right_right =>
          simp only [← a2_right_right]
          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
p_0 : σ_0
q_0 : σ_0 ⊕ σ_1
⊢ (∃ stop_state_list,
      { start_state := Sum.inr (Sum.inl p_0), 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)) ∧
        Sum.inr q_0 ∈ stop_state_list) =
    match (Sum.inr (Sum.inl p_0), Sum.inr q_0) 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
Tactic:
case _ q_0 =>
  cases q_0
  case _ q_0 =>
    simp
    sorry
  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
p_0 : σ_0
q_0 : ℕ
⊢ (∃ stop_state_list,
      { start_state := Sum.inr (Sum.inl p_0), 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)) ∧
        Sum.inl q_0 ∈ stop_state_list) =
    match (Sum.inr (Sum.inl p_0), Sum.inl q_0) 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
Tactic:
simp
Proof state after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
⊢ ∀ (x : List (ℕ ⊕ σ_0 ⊕ σ_1)),
    ((∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map (Sum.inr ∘ Sum.inl) a.stop_state_list = x) ∨
        ∃ a ∈ M_0.accepting_state_list, a = p_0 ∧ List.map (Sum.inr ∘ Sum.inr) M_1.starting_state_list = x) →
      Sum.inl q_0 ∉ x
Theorem: match_concat_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
⊢ ∀ (x : List (ℕ ⊕ σ_0 ⊕ σ_1)),
    ((∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map (Sum.inr ∘ Sum.inl) a.stop_state_list = x) ∨
        ∃ a ∈ M_0.accepting_state_list, a = p_0 ∧ List.map (Sum.inr ∘ Sum.inr) M_1.starting_state_list = x) →
      Sum.inl q_0 ∉ x
Tactic:
intro xs a1
Proof state after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
a1 :
  (∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map (Sum.inr ∘ Sum.inl) a.stop_state_list = xs) ∨
    ∃ a ∈ M_0.accepting_state_list, a = p_0 ∧ List.map (Sum.inr ∘ Sum.inr) M_1.starting_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Theorem: match_concat_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
a1 :
  (∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map (Sum.inr ∘ Sum.inl) a.stop_state_list = xs) ∨
    ∃ a ∈ M_0.accepting_state_list, a = p_0 ∧ List.map (Sum.inr ∘ Sum.inr) M_1.starting_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Tactic:
cases a1
Proof state after:
case inl
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
h✝ : ∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map (Sum.inr ∘ Sum.inl) a.stop_state_list = xs
⊢ Sum.inl q_0 ∉ xs

case inr
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
h✝ : ∃ a ∈ M_0.accepting_state_list, a = p_0 ∧ List.map (Sum.inr ∘ Sum.inr) M_1.starting_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Theorem: match_concat_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
left : ∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map (Sum.inr ∘ Sum.inl) a.stop_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Tactic:
case _ left =>
  cases left
  case _ x a2 =>
    cases a2
    case _ a2_left a2_right =>
      cases a2_right
      case _ a2_right_left a2_right_right =>
        simp only [← a2_right_right]
        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
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
right : ∃ a ∈ M_0.accepting_state_list, a = p_0 ∧ List.map (Sum.inr ∘ Sum.inr) M_1.starting_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Tactic:
case _ right =>
  cases right
  case _ x a2 =>
    cases a2
    case _ a2_left a2_right =>
      cases a2_right
      case _ a2_right_left a2_right_right =>
        simp only [← a2_right_right]
        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
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
left : ∃ a ∈ M_0.epsilon_arrow_list, a.start_state = p_0 ∧ List.map (Sum.inr ∘ Sum.inl) a.stop_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Tactic:
cases left
Proof state after:
case intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
w✝ : EpsilonArrow σ_0
h✝ : w✝ ∈ M_0.epsilon_arrow_list ∧ w✝.start_state = p_0 ∧ List.map (Sum.inr ∘ Sum.inl) w✝.stop_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Theorem: match_concat_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a2 : x ∈ M_0.epsilon_arrow_list ∧ x.start_state = p_0 ∧ List.map (Sum.inr ∘ Sum.inl) x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Tactic:
case _ x a2 =>
  cases a2
  case _ a2_left a2_right =>
    cases a2_right
    case _ a2_right_left a2_right_right =>
      simp only [← a2_right_right]
      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
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a2 : x ∈ M_0.epsilon_arrow_list ∧ x.start_state = p_0 ∧ List.map (Sum.inr ∘ Sum.inl) x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Tactic:
cases a2
Proof state after:
case intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
left✝ : x ∈ M_0.epsilon_arrow_list
right✝ : x.start_state = p_0 ∧ List.map (Sum.inr ∘ Sum.inl) x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Theorem: match_concat_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a2_left : x ∈ M_0.epsilon_arrow_list
a2_right : x.start_state = p_0 ∧ List.map (Sum.inr ∘ Sum.inl) x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Tactic:
case _ a2_left a2_right =>
  cases a2_right
  case _ a2_right_left a2_right_right =>
    simp only [← a2_right_right]
    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
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a2_left : x ∈ M_0.epsilon_arrow_list
a2_right : x.start_state = p_0 ∧ List.map (Sum.inr ∘ Sum.inl) x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Tactic:
cases a2_right
Proof state after:
case intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a2_left : x ∈ M_0.epsilon_arrow_list
left✝ : x.start_state = p_0
right✝ : List.map (Sum.inr ∘ Sum.inl) x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Theorem: match_concat_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a2_left : x ∈ M_0.epsilon_arrow_list
a2_right_left : x.start_state = p_0
a2_right_right : List.map (Sum.inr ∘ Sum.inl) x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Tactic:
case _ a2_right_left a2_right_right =>
  simp only [← a2_right_right]
  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
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a2_left : x ∈ M_0.epsilon_arrow_list
a2_right_left : x.start_state = p_0
a2_right_right : List.map (Sum.inr ∘ Sum.inl) x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Tactic:
simp only [← a2_right_right]
Proof state after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a2_left : x ∈ M_0.epsilon_arrow_list
a2_right_left : x.start_state = p_0
a2_right_right : List.map (Sum.inr ∘ Sum.inl) x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ List.map (Sum.inr ∘ Sum.inl) x.stop_state_list
Theorem: match_concat_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : EpsilonArrow σ_0
a2_left : x ∈ M_0.epsilon_arrow_list
a2_right_left : x.start_state = p_0
a2_right_right : List.map (Sum.inr ∘ Sum.inl) x.stop_state_list = xs
⊢ Sum.inl q_0 ∉ List.map (Sum.inr ∘ Sum.inl) x.stop_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
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
right : ∃ a ∈ M_0.accepting_state_list, a = p_0 ∧ List.map (Sum.inr ∘ Sum.inr) M_1.starting_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Tactic:
cases right
Proof state after:
case intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
w✝ : σ_0
h✝ : w✝ ∈ M_0.accepting_state_list ∧ w✝ = p_0 ∧ List.map (Sum.inr ∘ Sum.inr) M_1.starting_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Theorem: match_concat_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : σ_0
a2 : x ∈ M_0.accepting_state_list ∧ x = p_0 ∧ List.map (Sum.inr ∘ Sum.inr) M_1.starting_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Tactic:
case _ x a2 =>
  cases a2
  case _ a2_left a2_right =>
    cases a2_right
    case _ a2_right_left a2_right_right =>
      simp only [← a2_right_right]
      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
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : σ_0
a2 : x ∈ M_0.accepting_state_list ∧ x = p_0 ∧ List.map (Sum.inr ∘ Sum.inr) M_1.starting_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Tactic:
cases a2
Proof state after:
case intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : σ_0
left✝ : x ∈ M_0.accepting_state_list
right✝ : x = p_0 ∧ List.map (Sum.inr ∘ Sum.inr) M_1.starting_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Theorem: match_concat_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : σ_0
a2_left : x ∈ M_0.accepting_state_list
a2_right : x = p_0 ∧ List.map (Sum.inr ∘ Sum.inr) M_1.starting_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Tactic:
case _ a2_left a2_right =>
  cases a2_right
  case _ a2_right_left a2_right_right =>
    simp only [← a2_right_right]
    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
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : σ_0
a2_left : x ∈ M_0.accepting_state_list
a2_right : x = p_0 ∧ List.map (Sum.inr ∘ Sum.inr) M_1.starting_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Tactic:
cases a2_right
Proof state after:
case intro
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : σ_0
a2_left : x ∈ M_0.accepting_state_list
left✝ : x = p_0
right✝ : List.map (Sum.inr ∘ Sum.inr) M_1.starting_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Theorem: match_concat_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
p_0 : σ_0
q_0 : ℕ
xs : List (ℕ ⊕ σ_0 ⊕ σ_1)
x : σ_0
a2_left : x ∈ M_0.accepting_state_list
a2_right_left : x = p_0
a2_right_right : List.map (Sum.inr ∘ Sum.inr) M_1.starting_state_list = xs
⊢ Sum.inl q_0 ∉ xs
Tactic:
case _ a2_right_left a2_right_right =>
  simp only [← a2_right_right]
  simp
Proof state after:
no goals