Theorem: NAtoDAisEquiv (FOL/Parsing/Compute.lean)

State before:
α σ : Type
N : NA α σ
⊢ N.toDA.accepts = N.accepts
Tactic:
ext cs
State after:
case h.a
α σ : Type
N : NA α σ
cs : List α
⊢ N.toDA.accepts cs ↔ N.accepts cs

State before:
case h.a
α σ : Type
N : NA α σ
cs : List α
⊢ N.toDA.accepts cs ↔ N.accepts cs
Tactic:
simp only [DA.memAccepts]
State after:
case h.a
α σ : Type
N : NA α σ
cs : List α
⊢ N.toDA.evalFrom N.toDA.startingState cs ∈ N.toDA.acceptingStates ↔ N.accepts cs

State before:
case h.a
α σ : Type
N : NA α σ
cs : List α
⊢ N.toDA.evalFrom N.toDA.startingState cs ∈ N.toDA.acceptingStates ↔ N.accepts cs
Tactic:
simp only [NA.memAccepts]
State after:
case h.a
α σ : Type
N : NA α σ
cs : List α
⊢ N.toDA.evalFrom N.toDA.startingState cs ∈ N.toDA.acceptingStates ↔
    ∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates

State before:
case h.a
α σ : Type
N : NA α σ
cs : List α
⊢ N.toDA.evalFrom N.toDA.startingState cs ∈ N.toDA.acceptingStates ↔
    ∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates
Tactic:
simp only [NA.toDA]
State after:
case h.a
α σ : Type
N : NA α σ
cs : List α
⊢ { step := N.stepSet, startingState := N.startingStates,
            acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
        N.startingStates cs ∈
      {S | ∃ s ∈ S, s ∈ N.acceptingStates} ↔
    ∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates

State before:
case h.a
α σ : Type
N : NA α σ
cs : List α
⊢ { step := N.stepSet, startingState := N.startingStates,
            acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
        N.startingStates cs ∈
      {S | ∃ s ∈ S, s ∈ N.acceptingStates} ↔
    ∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates
Tactic:
simp
State after:
case h.a
α σ : Type
N : NA α σ
cs : List α
⊢ (∃
      s ∈
        { step := N.stepSet, startingState := N.startingStates,
              acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
          N.startingStates cs,
      s ∈ N.acceptingStates) ↔
    ∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates

State before:
case h.a
α σ : Type
N : NA α σ
cs : List α
⊢ (∃
      s ∈
        { step := N.stepSet, startingState := N.startingStates,
              acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
          N.startingStates cs,
      s ∈ N.acceptingStates) ↔
    ∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates
Tactic:
constructor
State after:
case h.a.mp
α σ : Type
N : NA α σ
cs : List α
⊢ (∃
      s ∈
        { step := N.stepSet, startingState := N.startingStates,
              acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
          N.startingStates cs,
      s ∈ N.acceptingStates) →
    ∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates

case h.a.mpr
α σ : Type
N : NA α σ
cs : List α
⊢ (∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates) →
    ∃
      s ∈
        { step := N.stepSet, startingState := N.startingStates,
              acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
          N.startingStates cs,
      s ∈ N.acceptingStates

State before:
case h.a.mp
α σ : Type
N : NA α σ
cs : List α
⊢ (∃
      s ∈
        { step := N.stepSet, startingState := N.startingStates,
              acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
          N.startingStates cs,
      s ∈ N.acceptingStates) →
    ∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates

case h.a.mpr
α σ : Type
N : NA α σ
cs : List α
⊢ (∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates) →
    ∃
      s ∈
        { step := N.stepSet, startingState := N.startingStates,
              acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
          N.startingStates cs,
      s ∈ N.acceptingStates
Tactic:
all_goals
  simp
  intro s a1 a2
  apply Exists.intro s
  tauto
State after:
no goals

State before:
case h.a.mpr
α σ : Type
N : NA α σ
cs : List α
⊢ (∃ s ∈ N.evalFrom N.startingStates cs, s ∈ N.acceptingStates) →
    ∃
      s ∈
        { step := N.stepSet, startingState := N.startingStates,
              acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
          N.startingStates cs,
      s ∈ N.acceptingStates
Tactic:
simp
State after:
case h.a.mpr
α σ : Type
N : NA α σ
cs : List α
⊢ ∀ x ∈ N.evalFrom N.startingStates cs,
    x ∈ N.acceptingStates →
      ∃
        s ∈
          { step := N.stepSet, startingState := N.startingStates,
                acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
            N.startingStates cs,
        s ∈ N.acceptingStates

State before:
case h.a.mpr
α σ : Type
N : NA α σ
cs : List α
⊢ ∀ x ∈ N.evalFrom N.startingStates cs,
    x ∈ N.acceptingStates →
      ∃
        s ∈
          { step := N.stepSet, startingState := N.startingStates,
                acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
            N.startingStates cs,
        s ∈ N.acceptingStates
Tactic:
intro s a1 a2
State after:
case h.a.mpr
α σ : Type
N : NA α σ
cs : List α
s : σ
a1 : s ∈ N.evalFrom N.startingStates cs
a2 : s ∈ N.acceptingStates
⊢ ∃
    s ∈
      { step := N.stepSet, startingState := N.startingStates,
            acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
        N.startingStates cs,
    s ∈ N.acceptingStates

State before:
case h.a.mpr
α σ : Type
N : NA α σ
cs : List α
s : σ
a1 : s ∈ N.evalFrom N.startingStates cs
a2 : s ∈ N.acceptingStates
⊢ ∃
    s ∈
      { step := N.stepSet, startingState := N.startingStates,
            acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
        N.startingStates cs,
    s ∈ N.acceptingStates
Tactic:
apply Exists.intro s
State after:
case h.a.mpr
α σ : Type
N : NA α σ
cs : List α
s : σ
a1 : s ∈ N.evalFrom N.startingStates cs
a2 : s ∈ N.acceptingStates
⊢ s ∈
      { step := N.stepSet, startingState := N.startingStates,
            acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
        N.startingStates cs ∧
    s ∈ N.acceptingStates

State before:
case h.a.mpr
α σ : Type
N : NA α σ
cs : List α
s : σ
a1 : s ∈ N.evalFrom N.startingStates cs
a2 : s ∈ N.acceptingStates
⊢ s ∈
      { step := N.stepSet, startingState := N.startingStates,
            acceptingStates := {S | ∃ s ∈ S, s ∈ N.acceptingStates} }.evalFrom
        N.startingStates cs ∧
    s ∈ N.acceptingStates
Tactic:
tauto
State after:
no goals