def Regex.Backtracker.StackEntry.Refines {nfa : NFA} {startIdx maxIdx bufferSize : ℕ} (entryH : StackEntry HistoryStrategy nfa startIdx maxIdx) (entryB : StackEntry (BufferStrategy bufferSize) nfa startIdx maxIdx) : Prop

Equations

• entryH.Refines entryB = (Regex.Strategy.refineUpdate entryH.update entryB.update ∧ entryH.state = entryB.state ∧ entryH.it = entryB.it)

theorem Regex.Backtracker.StackEntry.Refines.simpL {nfa : NFA} {startIdx maxIdx bufferSize : ℕ} {update : HistoryStrategy.Update} {state : Fin nfa.nodes.size} {it : Data.BoundedIterator startIdx maxIdx} {entryB : StackEntry (BufferStrategy bufferSize) nfa startIdx maxIdx} (ref : { update := update, state := state, it := it }.Refines entryB) : entryB = { update := entryB.update, state := state, it := it }

theorem Regex.Backtracker.StackEntry.Refines.mk {nfa : NFA} {startIdx maxIdx bufferSize : ℕ} {update : HistoryStrategy.Update} {state state' : Fin nfa.nodes.size} {it it' : Data.BoundedIterator startIdx maxIdx} {entryB : StackEntry (BufferStrategy bufferSize) nfa startIdx maxIdx} (ref : { update := update, state := state, it := it }.Refines entryB) : { update := update, state := state', it := it' }.Refines { update := entryB.update, state := state', it := it' }

theorem Regex.Backtracker.StackEntry.Refines.empty {nfa : NFA} {startIdx maxIdx bufferSize : ℕ} {state : Fin nfa.nodes.size} {it : Data.BoundedIterator startIdx maxIdx} : { update := HistoryStrategy.empty, state := state, it := it }.Refines { update := (BufferStrategy bufferSize).empty, state := state, it := it }

inductive Regex.Backtracker.RefineStack {nfa : NFA} {startIdx maxIdx bufferSize : ℕ} : List (StackEntry HistoryStrategy nfa startIdx maxIdx) → List (StackEntry (BufferStrategy bufferSize) nfa startIdx maxIdx) → Prop

• nil {nfa : NFA} {startIdx maxIdx bufferSize : ℕ} : RefineStack [] []
• cons {nfa : NFA} {startIdx maxIdx bufferSize : ℕ} (entryH : StackEntry HistoryStrategy nfa startIdx maxIdx) (entryB : StackEntry (BufferStrategy bufferSize) nfa startIdx maxIdx) (stackH : List (StackEntry HistoryStrategy nfa startIdx maxIdx)) (stackB : List (StackEntry (BufferStrategy bufferSize) nfa startIdx maxIdx)) : entryH.Refines entryB → RefineStack stackH stackB → RefineStack (entryH :: stackH) (entryB :: stackB)

def Regex.Backtracker.Refines {nfa : NFA} {startIdx maxIdx bufferSize : ℕ} (resultH : Option (List (ℕ × String.Pos)) × Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)) (resultB : Option (Buffer bufferSize) × Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)) : Prop

Equations

• Regex.Backtracker.Refines resultH resultB = (Regex.Strategy.refineUpdateOpt resultH.1 resultB.1 ∧ resultH.2 = resultB.2)

theorem Regex.Backtracker.captureNextAux.pushNext.refines {nfa : NFA} {wf : nfa.WellFormed} {startIdx maxIdx bufferSize : ℕ} {stackH : List (StackEntry HistoryStrategy nfa startIdx maxIdx)} {stackB : List (StackEntry (BufferStrategy bufferSize) nfa startIdx maxIdx)} {updateH : HistoryStrategy.Update} {updateB : (BufferStrategy bufferSize).Update} {state : Fin nfa.nodes.size} {it : Data.BoundedIterator startIdx maxIdx} (refEntry : { update := updateH, state := state, it := it }.Refines { update := updateB, state := state, it := it }) (refStack : RefineStack stackH stackB) : RefineStack (pushNext HistoryStrategy nfa wf startIdx maxIdx stackH updateH state it) (pushNext (BufferStrategy bufferSize) nfa wf startIdx maxIdx stackB updateB state it)

theorem Regex.Backtracker.captureNextAux.refines (nfa : NFA) (wf : nfa.WellFormed) (startIdx maxIdx bufferSize : ℕ) (visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)) {stackH : List (StackEntry HistoryStrategy nfa startIdx maxIdx)} {stackB : List (StackEntry (BufferStrategy bufferSize) nfa startIdx maxIdx)} (refStack : RefineStack stackH stackB) : Refines (captureNextAux HistoryStrategy nfa wf startIdx maxIdx visited stackH) (captureNextAux (BufferStrategy bufferSize) nfa wf startIdx maxIdx visited stackB)

theorem Regex.Backtracker.captureNext.go.refines {maxIdx : ℕ} (nfa : NFA) (wf : nfa.WellFormed) (startIdx bufferSize : ℕ) (bit : Data.BoundedIterator startIdx maxIdx) (visited : Data.BitMatrix nfa.nodes.size (maxIdx + 1 - startIdx)) : Strategy.refineUpdateOpt (go HistoryStrategy nfa wf startIdx maxIdx bit visited) (go (BufferStrategy bufferSize) nfa wf startIdx maxIdx bit visited)

theorem Regex.Backtracker.captureNext.refines (nfa : NFA) (wf : nfa.WellFormed) (bufferSize : ℕ) (it : String.Iterator) : Strategy.refineUpdateOpt (captureNext HistoryStrategy nfa wf it) (captureNext (BufferStrategy bufferSize) nfa wf it)