internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Pred.One.Ind.substitution_is_valid
Proof state before:
case h3_var
F F' : Formula
P : PredName
zs : List VarName
H : Formula
h1 : IsSub P zs H F F'
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
J : Interpretation D :=
  { nonempty := ⋯, pred_const_ := I.pred_const_,
    pred_var_ := fun Q ds =>
      if Q = P ∧ ds.length = zs.length then Holds D I (Function.updateListITE V zs ds) E H else I.pred_var_ Q ds }
s1 :
  (∀ (Q : PredName) (ds : List D),
      Q = P ∧ ds.length = zs.length →
        (Holds D I (Function.updateListITE V zs ds) E H ↔
          if True ∧ ds.length = zs.length then Holds D I (Function.updateListITE V zs ds) E H else I.pred_var_ P ds)) →
    True →
      (∀ (Q : PredName) (ds : List D),
          ¬(Q = P ∧ ds.length = zs.length) →
            (I.pred_var_ Q ds ↔
              if Q = P ∧ ds.length = zs.length then Holds D I (Function.updateListITE V zs ds) E H
              else I.pred_var_ Q ds)) →
        (Holds D I V E F' ↔ Holds D J V E F)
Q : PredName
ds : List D
a1 : ¬(Q = P ∧ ds.length = zs.length)
⊢ I.pred_var_ Q ds ↔
    if Q = P ∧ ds.length = zs.length then Holds D I (Function.updateListITE V zs ds) E H else I.pred_var_ Q ds
Tactic:
simp only [if_neg a1]
Proof state after:
no goals
Theorem: match_char_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
c : α
⊢ (match_char_EpsilonNFA c).toAbstract = match_char_AbstractEpsilonNFA c
Tactic:
simp only [match_char_EpsilonNFA]
Proof state after:
α : Type
inst✝ : DecidableEq α
c : α
⊢ { symbol_arrow_list := [{ start_state := 0, symbol := c, stop_state_list := [1] }], epsilon_arrow_list := [],
        starting_state_list := [0], accepting_state_list := [1] }.toAbstract =
    match_char_AbstractEpsilonNFA c
Theorem: match_char_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
c : α
⊢ { symbol_arrow_list := [{ start_state := 0, symbol := c, stop_state_list := [1] }], epsilon_arrow_list := [],
        starting_state_list := [0], accepting_state_list := [1] }.toAbstract =
    match_char_AbstractEpsilonNFA c
Tactic:
simp only [EpsilonNFA.toAbstract]
Proof state after:
α : Type
inst✝ : DecidableEq α
c : α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈
              [{ start_state := 0, symbol := c, stop_state_list := [1] }] ∧
            stop_state ∈ stop_state_list,
      epsilon := fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := stop_state_list } ∈ [] ∧ stop_state ∈ stop_state_list,
      start := fun state => state ∈ [0], accepting := fun state => state ∈ [1] } =
    match_char_AbstractEpsilonNFA c
Theorem: match_char_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
c : α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈
              [{ start_state := 0, symbol := c, stop_state_list := [1] }] ∧
            stop_state ∈ stop_state_list,
      epsilon := fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := stop_state_list } ∈ [] ∧ stop_state ∈ stop_state_list,
      start := fun state => state ∈ [0], accepting := fun state => state ∈ [1] } =
    match_char_AbstractEpsilonNFA c
Tactic:
simp only [match_char_AbstractEpsilonNFA]
Proof state after:
α : Type
inst✝ : DecidableEq α
c : α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈
              [{ start_state := 0, symbol := c, stop_state_list := [1] }] ∧
            stop_state ∈ stop_state_list,
      epsilon := fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := stop_state_list } ∈ [] ∧ stop_state ∈ stop_state_list,
      start := fun state => state ∈ [0], accepting := fun state => state ∈ [1] } =
    { symbol := fun p a q => p = 0 ∧ a = c ∧ q = 1, epsilon := fun x x => False, start := fun p => p = 0,
      accepting := fun p => p = 1 }
Theorem: match_char_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
c : α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈
              [{ start_state := 0, symbol := c, stop_state_list := [1] }] ∧
            stop_state ∈ stop_state_list,
      epsilon := fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := stop_state_list } ∈ [] ∧ stop_state ∈ stop_state_list,
      start := fun state => state ∈ [0], accepting := fun state => state ∈ [1] } =
    { symbol := fun p a q => p = 0 ∧ a = c ∧ q = 1, epsilon := fun x x => False, start := fun p => p = 0,
      accepting := fun p => p = 1 }
Tactic:
simp
Proof state after:
α : Type
inst✝ : DecidableEq α
c : α
⊢ (fun start_state symbol stop_state =>
      ∃ stop_state_list, (start_state = 0 ∧ symbol = c ∧ stop_state_list = [1]) ∧ stop_state ∈ stop_state_list) =
    fun p a q => p = 0 ∧ a = c ∧ q = 1
Theorem: match_char_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
c : α
⊢ (fun start_state symbol stop_state =>
      ∃ stop_state_list, (start_state = 0 ∧ symbol = c ∧ stop_state_list = [1]) ∧ stop_state ∈ stop_state_list) =
    fun p a q => p = 0 ∧ a = c ∧ q = 1
Tactic:
simp only [← and_assoc]
Proof state after:
α : Type
inst✝ : DecidableEq α
c : α
⊢ (fun start_state symbol stop_state =>
      ∃ stop_state_list, ((start_state = 0 ∧ symbol = c) ∧ stop_state_list = [1]) ∧ stop_state ∈ stop_state_list) =
    fun p a q => (p = 0 ∧ a = c) ∧ q = 1
Theorem: match_char_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
c : α
⊢ (fun start_state symbol stop_state =>
      ∃ stop_state_list, ((start_state = 0 ∧ symbol = c) ∧ stop_state_list = [1]) ∧ stop_state ∈ stop_state_list) =
    fun p a q => (p = 0 ∧ a = c) ∧ q = 1
Tactic:
simp only [and_right_comm]
Proof state after:
α : Type
inst✝ : DecidableEq α
c : α
⊢ (fun start_state symbol stop_state =>
      ∃ stop_state_list, ((start_state = 0 ∧ symbol = c) ∧ stop_state ∈ stop_state_list) ∧ stop_state_list = [1]) =
    fun p a q => (p = 0 ∧ a = c) ∧ q = 1
Theorem: match_char_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
c : α
⊢ (fun start_state symbol stop_state =>
      ∃ stop_state_list, ((start_state = 0 ∧ symbol = c) ∧ stop_state ∈ stop_state_list) ∧ stop_state_list = [1]) =
    fun p a q => (p = 0 ∧ a = c) ∧ q = 1
Tactic:
simp
Proof state after:
no goals
Theorem: match_epsilon_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
⊢ (match_epsilon_EpsilonNFA α).toAbstract = match_epsilon_AbstractEpsilonNFA α
Tactic:
simp only [match_epsilon_EpsilonNFA]
Proof state after:
α : Type
inst✝ : DecidableEq α
⊢ { symbol_arrow_list := [], epsilon_arrow_list := [{ start_state := 0, stop_state_list := [1] }],
        starting_state_list := [0], accepting_state_list := [1] }.toAbstract =
    match_epsilon_AbstractEpsilonNFA α
Theorem: match_epsilon_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
⊢ { symbol_arrow_list := [], epsilon_arrow_list := [{ start_state := 0, stop_state_list := [1] }],
        starting_state_list := [0], accepting_state_list := [1] }.toAbstract =
    match_epsilon_AbstractEpsilonNFA α
Tactic:
simp only [EpsilonNFA.toAbstract]
Proof state after:
α : Type
inst✝ : DecidableEq α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈ [] ∧
            stop_state ∈ stop_state_list,
      epsilon := fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := stop_state_list } ∈
              [{ start_state := 0, stop_state_list := [1] }] ∧
            stop_state ∈ stop_state_list,
      start := fun state => state ∈ [0], accepting := fun state => state ∈ [1] } =
    match_epsilon_AbstractEpsilonNFA α
Theorem: match_epsilon_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈ [] ∧
            stop_state ∈ stop_state_list,
      epsilon := fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := stop_state_list } ∈
              [{ start_state := 0, stop_state_list := [1] }] ∧
            stop_state ∈ stop_state_list,
      start := fun state => state ∈ [0], accepting := fun state => state ∈ [1] } =
    match_epsilon_AbstractEpsilonNFA α
Tactic:
simp only [match_epsilon_AbstractEpsilonNFA]
Proof state after:
α : Type
inst✝ : DecidableEq α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈ [] ∧
            stop_state ∈ stop_state_list,
      epsilon := fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := stop_state_list } ∈
              [{ start_state := 0, stop_state_list := [1] }] ∧
            stop_state ∈ stop_state_list,
      start := fun state => state ∈ [0], accepting := fun state => state ∈ [1] } =
    { symbol := fun x x x => False, epsilon := fun p q => p = 0 ∧ q = 1, start := fun p => p = 0,
      accepting := fun p => p = 1 }
Theorem: match_epsilon_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈ [] ∧
            stop_state ∈ stop_state_list,
      epsilon := fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := stop_state_list } ∈
              [{ start_state := 0, stop_state_list := [1] }] ∧
            stop_state ∈ stop_state_list,
      start := fun state => state ∈ [0], accepting := fun state => state ∈ [1] } =
    { symbol := fun x x x => False, epsilon := fun p q => p = 0 ∧ q = 1, start := fun p => p = 0,
      accepting := fun p => p = 1 }
Tactic:
simp
Proof state after:
α : Type
inst✝ : DecidableEq α
⊢ (fun start_state stop_state =>
      ∃ stop_state_list, (start_state = 0 ∧ stop_state_list = [1]) ∧ stop_state ∈ stop_state_list) =
    fun p q => p = 0 ∧ q = 1
Theorem: match_epsilon_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
⊢ (fun start_state stop_state =>
      ∃ stop_state_list, (start_state = 0 ∧ stop_state_list = [1]) ∧ stop_state ∈ stop_state_list) =
    fun p q => p = 0 ∧ q = 1
Tactic:
funext p q
Proof state after:
case h.h
α : Type
inst✝ : DecidableEq α
p q : ℕ
⊢ (∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list) = (p = 0 ∧ q = 1)
Theorem: match_epsilon_EpsilonNFA_toAbstract
Proof state before:
case h.h
α : Type
inst✝ : DecidableEq α
p q : ℕ
⊢ (∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list) = (p = 0 ∧ q = 1)
Tactic:
simp
Proof state after:
case h.h
α : Type
inst✝ : DecidableEq α
p q : ℕ
⊢ (∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list) ↔ p = 0 ∧ q = 1
Theorem: match_epsilon_EpsilonNFA_toAbstract
Proof state before:
case h.h
α : Type
inst✝ : DecidableEq α
p q : ℕ
⊢ (∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list) ↔ p = 0 ∧ q = 1
Tactic:
constructor
Proof state after:
case h.h.mp
α : Type
inst✝ : DecidableEq α
p q : ℕ
⊢ (∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list) → p = 0 ∧ q = 1

case h.h.mpr
α : Type
inst✝ : DecidableEq α
p q : ℕ
⊢ p = 0 ∧ q = 1 → ∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
Theorem: match_epsilon_EpsilonNFA_toAbstract
Proof state before:
case h.h.mp
α : Type
inst✝ : DecidableEq α
p q : ℕ
⊢ (∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list) → p = 0 ∧ q = 1
Tactic:
intro a1
Proof state after:
case h.h.mp
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : ∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
⊢ p = 0 ∧ q = 1
Theorem: match_epsilon_EpsilonNFA_toAbstract
Proof state before:
case h.h.mp
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : ∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
⊢ p = 0 ∧ q = 1
Tactic:
apply Exists.elim a1
Proof state after:
case h.h.mp
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : ∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
⊢ ∀ (a : List ℕ), (p = 0 ∧ a = [1]) ∧ q ∈ a → p = 0 ∧ q = 1
Theorem: match_epsilon_EpsilonNFA_toAbstract
Proof state before:
case h.h.mp
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : ∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
⊢ ∀ (a : List ℕ), (p = 0 ∧ a = [1]) ∧ q ∈ a → p = 0 ∧ q = 1
Tactic:
intro stop_state_list a2
Proof state after:
case h.h.mp
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : ∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
stop_state_list : List ℕ
a2 : (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
⊢ p = 0 ∧ q = 1
Theorem: match_epsilon_EpsilonNFA_toAbstract
Proof state before:
case h.h.mp
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : ∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
stop_state_list : List ℕ
a2 : (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
⊢ p = 0 ∧ q = 1
Tactic:
clear a1
Proof state after:
case h.h.mp
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2 : (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
⊢ p = 0 ∧ q = 1
Theorem: match_epsilon_EpsilonNFA_toAbstract
Proof state before:
case h.h.mp
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2 : (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
⊢ p = 0 ∧ q = 1
Tactic:
cases a2
Proof state after:
case h.h.mp.intro
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
left✝ : p = 0 ∧ stop_state_list = [1]
right✝ : q ∈ stop_state_list
⊢ p = 0 ∧ q = 1
Theorem: match_epsilon_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2_left : p = 0 ∧ stop_state_list = [1]
a2_right : q ∈ stop_state_list
⊢ p = 0 ∧ q = 1
Tactic:
case _ a2_left a2_right =>
  cases a2_left
  case _ a2_left_left a2_left_right =>
    simp only [a2_left_right] at a2_right
    simp at a2_right
    tauto
Proof state after:
no goals
Theorem: match_epsilon_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2_left : p = 0 ∧ stop_state_list = [1]
a2_right : q ∈ stop_state_list
⊢ p = 0 ∧ q = 1
Tactic:
cases a2_left
Proof state after:
case intro
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2_right : q ∈ stop_state_list
left✝ : p = 0
right✝ : stop_state_list = [1]
⊢ p = 0 ∧ q = 1
Theorem: match_epsilon_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2_right : q ∈ stop_state_list
a2_left_left : p = 0
a2_left_right : stop_state_list = [1]
⊢ p = 0 ∧ q = 1
Tactic:
case _ a2_left_left a2_left_right =>
  simp only [a2_left_right] at a2_right
  simp at a2_right
  tauto
Proof state after:
no goals
Theorem: match_epsilon_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2_right : q ∈ stop_state_list
a2_left_left : p = 0
a2_left_right : stop_state_list = [1]
⊢ p = 0 ∧ q = 1
Tactic:
simp only [a2_left_right] at a2_right
Proof state after:
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2_left_left : p = 0
a2_left_right : stop_state_list = [1]
a2_right : q ∈ [1]
⊢ p = 0 ∧ q = 1
Theorem: match_epsilon_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2_left_left : p = 0
a2_left_right : stop_state_list = [1]
a2_right : q ∈ [1]
⊢ p = 0 ∧ q = 1
Tactic:
simp at a2_right
Proof state after:
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2_left_left : p = 0
a2_left_right : stop_state_list = [1]
a2_right : q = 1
⊢ p = 0 ∧ q = 1
Theorem: match_epsilon_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
p q : ℕ
stop_state_list : List ℕ
a2_left_left : p = 0
a2_left_right : stop_state_list = [1]
a2_right : q = 1
⊢ p = 0 ∧ q = 1
Tactic:
tauto
Proof state after:
no goals
Theorem: match_epsilon_EpsilonNFA_toAbstract
Proof state before:
case h.h.mpr
α : Type
inst✝ : DecidableEq α
p q : ℕ
⊢ p = 0 ∧ q = 1 → ∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
Tactic:
intro a1
Proof state after:
case h.h.mpr
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : p = 0 ∧ q = 1
⊢ ∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
Theorem: match_epsilon_EpsilonNFA_toAbstract
Proof state before:
case h.h.mpr
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : p = 0 ∧ q = 1
⊢ ∃ stop_state_list, (p = 0 ∧ stop_state_list = [1]) ∧ q ∈ stop_state_list
Tactic:
apply Exists.intro [1]
Proof state after:
case h.h.mpr
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : p = 0 ∧ q = 1
⊢ (p = 0 ∧ [1] = [1]) ∧ q ∈ [1]
Theorem: match_epsilon_EpsilonNFA_toAbstract
Proof state before:
case h.h.mpr
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : p = 0 ∧ q = 1
⊢ (p = 0 ∧ [1] = [1]) ∧ q ∈ [1]
Tactic:
simp
Proof state after:
case h.h.mpr
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : p = 0 ∧ q = 1
⊢ p = 0 ∧ q = 1
Theorem: match_epsilon_EpsilonNFA_toAbstract
Proof state before:
case h.h.mpr
α : Type
inst✝ : DecidableEq α
p q : ℕ
a1 : p = 0 ∧ q = 1
⊢ p = 0 ∧ q = 1
Tactic:
exact a1
Proof state after:
no goals
Theorem: match_zero_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
⊢ (match_zero_EpsilonNFA α).toAbstract = match_zero_AbstractEpsilonNFA α
Tactic:
simp only [match_zero_EpsilonNFA]
Proof state after:
α : Type
inst✝ : DecidableEq α
⊢ { symbol_arrow_list := [], epsilon_arrow_list := [], starting_state_list := [0],
        accepting_state_list := [] }.toAbstract =
    match_zero_AbstractEpsilonNFA α
Theorem: match_zero_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
⊢ { symbol_arrow_list := [], epsilon_arrow_list := [], starting_state_list := [0],
        accepting_state_list := [] }.toAbstract =
    match_zero_AbstractEpsilonNFA α
Tactic:
simp only [EpsilonNFA.toAbstract]
Proof state after:
α : Type
inst✝ : DecidableEq α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈ [] ∧
            stop_state ∈ stop_state_list,
      epsilon := fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := stop_state_list } ∈ [] ∧ stop_state ∈ stop_state_list,
      start := fun state => state ∈ [0], accepting := fun state => state ∈ [] } =
    match_zero_AbstractEpsilonNFA α
Theorem: match_zero_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈ [] ∧
            stop_state ∈ stop_state_list,
      epsilon := fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := stop_state_list } ∈ [] ∧ stop_state ∈ stop_state_list,
      start := fun state => state ∈ [0], accepting := fun state => state ∈ [] } =
    match_zero_AbstractEpsilonNFA α
Tactic:
simp only [match_zero_AbstractEpsilonNFA]
Proof state after:
α : Type
inst✝ : DecidableEq α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈ [] ∧
            stop_state ∈ stop_state_list,
      epsilon := fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := stop_state_list } ∈ [] ∧ stop_state ∈ stop_state_list,
      start := fun state => state ∈ [0], accepting := fun state => state ∈ [] } =
    { symbol := fun x x x => False, epsilon := fun x x => False, start := fun p => p = 0, accepting := fun x => False }
Theorem: match_zero_EpsilonNFA_toAbstract
Proof state before:
α : Type
inst✝ : DecidableEq α
⊢ {
      symbol := fun start_state symbol stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, symbol := symbol, stop_state_list := stop_state_list } ∈ [] ∧
            stop_state ∈ stop_state_list,
      epsilon := fun start_state stop_state =>
        ∃ stop_state_list,
          { start_state := start_state, stop_state_list := stop_state_list } ∈ [] ∧ stop_state ∈ stop_state_list,
      start := fun state => state ∈ [0], accepting := fun state => state ∈ [] } =
    { symbol := fun x x x => False, epsilon := fun x x => False, start := fun p => p = 0, accepting := fun x => False }
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
⊢ (match_union_EpsilonNFA α σ_0 σ_1 M_0 M_1).toAbstract =
    match_union_AbstractEpsilonNFA α σ_0 σ_1 M_0.toAbstract M_1.toAbstract
Tactic:
simp only [match_union_EpsilonNFA]
Proof state after:
α : Type
inst✝ : DecidableEq α
σ_0 σ_1 : Type
M_0 : EpsilonNFA α σ_0
M_1 : EpsilonNFA α σ_1
⊢ {
        symbol_arrow_list :=
          (EpsilonNFA.wrapLeft σ_1 M_0).symbol_arrow_list ++ (EpsilonNFA.wrapRight σ_0 M_1).symbol_arrow_list,
        epsilon_arrow_list :=
          (EpsilonNFA.wrapLeft σ_1 M_0).epsilon_arrow_list ++ (EpsilonNFA.wrapRight σ_0 M_1).epsilon_arrow_list,
        starting_state_list :=
          (EpsilonNFA.wrapLeft σ_1 M_0).starting_state_list ++ (EpsilonNFA.wrapRight σ_0 M_1).starting_state_list,
        accepting_state_list :=
          (EpsilonNFA.wrapLeft σ_1 M_0).accepting_state_list ++
            (EpsilonNFA.wrapRight σ_0 M_1).accepting_state_list }.toAbstract =
    match_union_AbstractEpsilonNFA α σ_0 σ_1 M_0.toAbstract M_1.toAbstract