Theorem: Regex.NFA.pathToNext_of_compile_of_pathInAux (RegexCorrectness/NFA/Transition/Path/Equivalence.lean)

State before:
r : Data.Expr
nfa : NFA
i next : ℕ
cs : List Char
eq : compile r = nfa
assm₁ : 0 < i
assm₂ : next = 0
path : nfa.pathIn 0 i next cs
⊢ nfa.pathToNext 0 1 i cs
Tactic:
induction path with
| base _ =>
  subst assm₂
  contradiction
| @step i j k cs cs' step rest ih =>
  cases rest with
  | base _ =>
    subst assm₂
    exact ⟨i, [], cs, by simp, .base assm₁, step.castStart' assm₁⟩
  | step step' rest =>
    have : 0 < j := by
      cases Nat.eq_or_lt_of_le (Nat.zero_le j) with
      | inl eqj =>
        have : 0 < nfa.nodes.size :=
          calc
            0 < 1 := by decide
            _ < _ := (NFA.done.pushRegex ⟨0, by decide⟩ r).property
            _ = _ := by simp [←eq, compile]
        have hn : nfa[0] = .done := by
          simp [←eq]
          unfold compile
          rw [pushRegex_get_lt rfl 0 (by decide)]
          rfl
        simp [eqj] at hn
        cases step'.step <;> simp [hn, NFA.Node.charStep, NFA.Node.εStep] at *
      | inr gt => exact gt
    have ih := ih this assm₂
    apply ih.cons (step.castStart' assm₁)
State after:
no goals

State before:
case base
r : Data.Expr
nfa : NFA
i next : ℕ
cs : List Char
eq : compile r = nfa
i✝ : ℕ
h✝ : 0 ≤ i✝
assm₁ : 0 < i✝
assm₂ : i✝ = 0
⊢ nfa.pathToNext 0 1 i✝ []
Tactic:
subst assm₂
State after:
case base
r : Data.Expr
nfa : NFA
i next : ℕ
cs : List Char
eq : compile r = nfa
h✝ : 0 ≤ 0
assm₁ : 0 < 0
⊢ nfa.pathToNext 0 1 0 []

State before:
case base
r : Data.Expr
nfa : NFA
i next : ℕ
cs : List Char
eq : compile r = nfa
h✝ : 0 ≤ 0
assm₁ : 0 < 0
⊢ nfa.pathToNext 0 1 0 []
Tactic:
contradiction
State after:
no goals

State before:
case step
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs cs' : List Char
step : nfa.stepIn 0 i j cs
rest : nfa.pathIn 0 j k cs'
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j cs'
assm₁ : 0 < i
assm₂ : k = 0
⊢ nfa.pathToNext 0 1 i (cs ++ cs')
Tactic:
cases rest with
| base _ =>
  subst assm₂
  exact ⟨i, [], cs, by simp, .base assm₁, step.castStart' assm₁⟩
| step step' rest =>
  have : 0 < j := by
    cases Nat.eq_or_lt_of_le (Nat.zero_le j) with
    | inl eqj =>
      have : 0 < nfa.nodes.size :=
        calc
          0 < 1 := by decide
          _ < _ := (NFA.done.pushRegex ⟨0, by decide⟩ r).property
          _ = _ := by simp [←eq, compile]
      have hn : nfa[0] = .done := by
        simp [←eq]
        unfold compile
        rw [pushRegex_get_lt rfl 0 (by decide)]
        rfl
      simp [eqj] at hn
      cases step'.step <;> simp [hn, NFA.Node.charStep, NFA.Node.εStep] at *
    | inr gt => exact gt
  have ih := ih this assm₂
  apply ih.cons (step.castStart' assm₁)
State after:
no goals

State before:
case step.base
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
h✝ : 0 ≤ j
assm₂ : j = 0
ih : 0 < j → j = 0 → nfa.pathToNext 0 1 j []
⊢ nfa.pathToNext 0 1 i (cs ++ [])
Tactic:
subst assm₂
State after:
case step.base
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i : ℕ
cs : List Char
assm₁ : 0 < i
step : nfa.stepIn 0 i 0 cs
h✝ : 0 ≤ 0
ih : 0 < 0 → 0 = 0 → nfa.pathToNext 0 1 0 []
⊢ nfa.pathToNext 0 1 i (cs ++ [])

State before:
case step.base
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i : ℕ
cs : List Char
assm₁ : 0 < i
step : nfa.stepIn 0 i 0 cs
h✝ : 0 ≤ 0
ih : 0 < 0 → 0 = 0 → nfa.pathToNext 0 1 0 []
⊢ nfa.pathToNext 0 1 i (cs ++ [])
Tactic:
exact ⟨i, [], cs, by simp, .base assm₁, step.castStart' assm₁⟩
State after:
no goals

State before:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i : ℕ
cs : List Char
assm₁ : 0 < i
step : nfa.stepIn 0 i 0 cs
h✝ : 0 ≤ 0
ih : 0 < 0 → 0 = 0 → nfa.pathToNext 0 1 0 []
⊢ cs ++ [] = [] ++ cs
Tactic:
simp
State after:
no goals

State before:
case step.step
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
⊢ nfa.pathToNext 0 1 i (cs ++ (cs₁✝ ++ cs₂✝))
Tactic:
have : 0 < j := by
  cases Nat.eq_or_lt_of_le (Nat.zero_le j) with
  | inl eqj =>
    have : 0 < nfa.nodes.size :=
      calc
        0 < 1 := by decide
        _ < _ := (NFA.done.pushRegex ⟨0, by decide⟩ r).property
        _ = _ := by simp [←eq, compile]
    have hn : nfa[0] = .done := by
      simp [←eq]
      unfold compile
      rw [pushRegex_get_lt rfl 0 (by decide)]
      rfl
    simp [eqj] at hn
    cases step'.step <;> simp [hn, NFA.Node.charStep, NFA.Node.εStep] at *
  | inr gt => exact gt
State after:
case step.step
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
this : 0 < j
⊢ nfa.pathToNext 0 1 i (cs ++ (cs₁✝ ++ cs₂✝))

State before:
case step.step
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
this : 0 < j
⊢ nfa.pathToNext 0 1 i (cs ++ (cs₁✝ ++ cs₂✝))
Tactic:
have ih := ih this assm₂
State after:
case step.step
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih✝ : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
this : 0 < j
ih : nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
⊢ nfa.pathToNext 0 1 i (cs ++ (cs₁✝ ++ cs₂✝))

State before:
case step.step
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih✝ : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
this : 0 < j
ih : nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
⊢ nfa.pathToNext 0 1 i (cs ++ (cs₁✝ ++ cs₂✝))
Tactic:
apply ih.cons (step.castStart' assm₁)
State after:
no goals

State before:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
⊢ 0 < j
Tactic:
cases Nat.eq_or_lt_of_le (Nat.zero_le j) with
| inl eqj =>
  have : 0 < nfa.nodes.size :=
    calc
      0 < 1 := by decide
      _ < _ := (NFA.done.pushRegex ⟨0, by decide⟩ r).property
      _ = _ := by simp [←eq, compile]
  have hn : nfa[0] = .done := by
    simp [←eq]
    unfold compile
    rw [pushRegex_get_lt rfl 0 (by decide)]
    rfl
  simp [eqj] at hn
  cases step'.step <;> simp [hn, NFA.Node.charStep, NFA.Node.εStep] at *
| inr gt => exact gt
State after:
no goals

State before:
case inl
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
⊢ 0 < j
Tactic:
have : 0 < nfa.nodes.size :=
  calc
    0 < 1 := by decide
    _ < _ := (NFA.done.pushRegex ⟨0, by decide⟩ r).property
    _ = _ := by simp [←eq, compile]
State after:
case inl
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
⊢ 0 < j

State before:
case inl
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
⊢ 0 < j
Tactic:
have hn : nfa[0] = .done := by
  simp [←eq]
  unfold compile
  rw [pushRegex_get_lt rfl 0 (by decide)]
  rfl
State after:
case inl
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
hn : nfa[0] = Node.done
⊢ 0 < j

State before:
case inl
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
hn : nfa[0] = Node.done
⊢ 0 < j
Tactic:
simp [eqj] at hn
State after:
case inl
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
hn : nfa[j] = Node.done
⊢ 0 < j

State before:
case inl
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
hn : nfa[j] = Node.done
⊢ 0 < j
Tactic:
cases step'.step <;> simp [hn, NFA.Node.charStep, NFA.Node.εStep] at *
State after:
no goals

State before:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
⊢ 0 < 1
Tactic:
decide
State after:
no goals

State before:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
⊢ 0 < done.nodes.size
Tactic:
decide
State after:
no goals

State before:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
⊢ (↑(done.pushRegex ⟨0, ⋯⟩ r)).nodes.size = nfa.nodes.size
Tactic:
simp [←eq, compile]
State after:
no goals

State before:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
⊢ nfa[0] = Node.done
Tactic:
simp [←eq]
State after:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
⊢ (compile r)[0] = Node.done

State before:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
⊢ (compile r)[0] = Node.done
Tactic:
unfold compile
State after:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
⊢ (↑(done.pushRegex ⟨0, compile.proof_1⟩ r))[0] = Node.done

State before:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
⊢ (↑(done.pushRegex ⟨0, compile.proof_1⟩ r))[0] = Node.done
Tactic:
rw [pushRegex_get_lt rfl 0 (by decide)]
State after:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
⊢ done[0] = Node.done

State before:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
⊢ done[0] = Node.done
Tactic:
rfl
State after:
no goals

State before:
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
eqj : 0 = j
this : 0 < nfa.nodes.size
⊢ 0 < done.nodes.size
Tactic:
decide
State after:
no goals

State before:
case inr
r : Data.Expr
nfa : NFA
i✝ next : ℕ
cs✝ : List Char
eq : compile r = nfa
i j k : ℕ
cs : List Char
step : nfa.stepIn 0 i j cs
assm₁ : 0 < i
assm₂ : k = 0
j✝ : ℕ
cs₁✝ cs₂✝ : List Char
step' : nfa.stepIn 0 j j✝ cs₁✝
rest : nfa.pathIn 0 j✝ k cs₂✝
ih : 0 < j → k = 0 → nfa.pathToNext 0 1 j (cs₁✝ ++ cs₂✝)
gt : 0 < j
⊢ 0 < j
Tactic:
exact gt
State after:
no goals