Theorem: Regex.VM.eachStepChar_spec.mem_next_iff.go
Proof state before:
case h_1
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
inv₁ :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next ↔ ∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
inv₂ : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
inv₁' :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next'' ↔
      ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
inv₂' : ∀ (i j : Fin nfa.nodes.size), i ∈ next'' → ↑j ∈ nfa.εStep ↑i → j ∈ next''
x✝ : Option (Array (Option String.Pos))
heq✝ : (matched'', next'', saveSlots'').1 = none
h :
  eachStepChar.go nfa c pos current (i + 1) ⋯ (matched'', next'', saveSlots'').2.1
      (matched'', next'', saveSlots'').2.2 =
    (matched', next', saveSlots')
⊢ ∃ istop,
    ∀ (j : Fin nfa.nodes.size),
      j ∈ next' ↔
        ∃ i', ∃ (x : i' < current.count), i' < istop ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''

case h_2
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
inv₁ :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next ↔ ∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
inv₂ : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
inv₁' :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next'' ↔
      ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
inv₂' : ∀ (i j : Fin nfa.nodes.size), i ∈ next'' → ↑j ∈ nfa.εStep ↑i → j ∈ next''
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq✝ : (matched'', next'', saveSlots'').1 = some val✝
h : (matched'', next'', saveSlots'') = (matched', next', saveSlots')
⊢ ∃ istop,
    ∀ (j : Fin nfa.nodes.size),
      j ∈ next' ↔
        ∃ i', ∃ (x : i' < current.count), i' < istop ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
Tactic:
next =>
  exact go h inv₁' inv₂'
Proof state after:
case h_2
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
inv₁ :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next ↔ ∃ i', ∃ (x : i' < current.count), i' < i ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
inv₂ : ∀ (i j : Fin nfa.nodes.size), i ∈ next → ↑j ∈ nfa.εStep ↑i → j ∈ next
hi : ¬i = current.count
hlt : i < current.count
result :
  Option (Array (Option String.Pos)) × SparseSet nfa.nodes.size × 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
hres : stepChar nfa c pos next saveSlots current[i] = (matched'', next'', saveSlots'')
inv₁' :
  ∀ (j : Fin nfa.nodes.size),
    j ∈ next'' ↔
      ∃ i', ∃ (x : i' < current.count), i' < i + 1 ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''
inv₂' : ∀ (i j : Fin nfa.nodes.size), i ∈ next'' → ↑j ∈ nfa.εStep ↑i → j ∈ next''
x✝ : Option (Array (Option String.Pos))
val✝ : Array (Option String.Pos)
heq✝ : (matched'', next'', saveSlots'').1 = some val✝
h : (matched'', next'', saveSlots'') = (matched', next', saveSlots')
⊢ ∃ istop,
    ∀ (j : Fin nfa.nodes.size),
      j ∈ next' ↔
        ∃ i', ∃ (x : i' < current.count), i' < istop ∧ ∃ i'' ∈ nfa.charStep (↑current[i']) c, ↑j ∈ nfa.εClosure i''