simp at h
nfa : NFA
c : Char
pos : String.Pos
current : SparseSet nfa.nodes.size
i : ℕ
hle : i ≤ current.count
next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
h✝ : i = current.count
h : (none, next, saveSlots) = (matched', next', saveSlots')
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true
nfa : NFA
c : Char
pos : String.Pos
current : SparseSet nfa.nodes.size
i : ℕ
hle : i ≤ current.count
next : SparseSet nfa.nodes.size
saveSlots : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
matched' : Option (Array (Option String.Pos))
next' : SparseSet nfa.nodes.size
saveSlots' : Data.Vec (Array (Option String.Pos)) nfa.nodes.size
hnotDone : ∀ j ∈ next, nfa[j] ≠ Node.done
h✝ : i = current.count
h : none = matched' ∧ next = next' ∧ saveSlots = saveSlots'
⊢ (∃ j ∈ next', nfa[j] = Node.done) ↔ matched'.isSome = true