inductive Regex.NFA.Step {s : String} (nfa : NFA) (lb : ℕ) : ℕ → s.Pos → ℕ → s.Pos → Option (ℕ × s.Pos) → Prop

• epsilon {s : String} {nfa : NFA} {lb i j : ℕ} {p : s.Pos} (ge : lb ≤ i) (lt : i < nfa.size) (eq : nfa[i] = Node.epsilon j) : nfa.Step lb i p j p none
• anchor {s : String} {nfa : NFA} {lb i j : ℕ} {p : s.Pos} {a : Data.Anchor} (ge : lb ≤ i) (lt : i < nfa.size) (eq : nfa[i] = Node.anchor a j) (h : Data.Anchor.test p a = true) : nfa.Step lb i p j p none
• splitLeft {s : String} {nfa : NFA} {lb i j₁ j₂ : ℕ} {p : s.Pos} (ge : lb ≤ i) (lt : i < nfa.size) (eq : nfa[i] = Node.split j₁ j₂) : nfa.Step lb i p j₁ p none
• splitRight {s : String} {nfa : NFA} {lb i j₁ j₂ : ℕ} {p : s.Pos} (ge : lb ≤ i) (lt : i < nfa.size) (eq : nfa[i] = Node.split j₁ j₂) : nfa.Step lb i p j₂ p none
• save {s : String} {nfa : NFA} {lb i j : ℕ} {p : s.Pos} {offset : ℕ} (ge : lb ≤ i) (lt : i < nfa.size) (eq : nfa[i] = Node.save offset j) : nfa.Step lb i p j p (some (offset, p))
• char {s : String} {nfa : NFA} {lb i j : ℕ} {p : s.Pos} {c : Char} (ge : lb ≤ i) (lt : i < nfa.size) (eq : nfa[i] = Node.char c j) (ne : p ≠ s.endPos) (eq' : p.get ne = c) : nfa.Step lb i p j (p.next ne) none
• sparse {s : String} {nfa : NFA} {lb i j : ℕ} {p : s.Pos} {cs : Data.Classes} (ge : lb ≤ i) (lt : i < nfa.size) (eq : nfa[i] = Node.sparse cs j) (ne : p ≠ s.endPos) (mem : p.get ne ∈ cs) : nfa.Step lb i p j (p.next ne) none

theorem Regex.NFA.Step.ge {s : String} {nfa : NFA} {lb : ℕ} {p p' : s.Pos} {i j : ℕ} {update : Option (ℕ × s.Pos)} (step : nfa.Step lb i p j p' update) : lb ≤ i

theorem Regex.NFA.Step.lt {s : String} {nfa : NFA} {lb : ℕ} {p p' : s.Pos} {i j : ℕ} {update : Option (ℕ × s.Pos)} (step : nfa.Step lb i p j p' update) : i < nfa.size

theorem Regex.NFA.Step.lt_right {s : String} {nfa : NFA} {lb : ℕ} {p p' : s.Pos} {i j : ℕ} {update : Option (ℕ × s.Pos)} (wf : nfa.WellFormed) (step : nfa.Step lb i p j p' update) : j < nfa.size

theorem Regex.NFA.Step.eq_or_next {s : String} {nfa : NFA} {lb : ℕ} {p p' : s.Pos} {i j : ℕ} {update : Option (ℕ × s.Pos)} (step : nfa.Step lb i p j p' update) : p' = p ∨ ∃ (ne : p ≠ s.endPos), p' = p.next ne

theorem Regex.NFA.Step.le {s : String} {nfa : NFA} {lb : ℕ} {p p' : s.Pos} {i j : ℕ} {update : Option (ℕ × s.Pos)} (step : nfa.Step lb i p j p' update) : p ≤ p'

theorem Regex.NFA.Step.cast {s : String} {nfa nfa' : NFA} {lb : ℕ} {p p' : s.Pos} {i j : ℕ} {update : Option (ℕ × s.Pos)} (step : nfa.Step lb i p j p' update) {lt : i < nfa'.size} (h : nfa[i] = nfa'[i]) : nfa'.Step lb i p j p' update

theorem Regex.NFA.Step.castFrom {s : String} {nfa nfa' : NFA} {lb : ℕ} {p p' : s.Pos} {i j : ℕ} {update : Option (ℕ × s.Pos)} (step : nfa'.Step lb i p j p' update) {lt : i < nfa.size} (h : nfa'[i] = nfa[i]) : nfa.Step lb i p j p' update

theorem Regex.NFA.Step.castIndex {s : String} {nfa : NFA} {lb : ℕ} {p p' : s.Pos} {j : ℕ} {update : Option (ℕ × s.Pos)} {i₁ i₂ : ℕ} (h₁ : i₁ < nfa.size) (h₂ : i₂ < nfa.size) (eq : nfa[i₁] = nfa[i₂]) (ge : lb ≤ i₂) (step : nfa.Step lb i₁ p j p' update) : nfa.Step lb i₂ p j p' update

theorem Regex.NFA.Step.liftBound' {s : String} {nfa : NFA} {lb lb' : ℕ} {p p' : s.Pos} {i j : ℕ} {update : Option (ℕ × s.Pos)} (ge : lb' ≤ i) (step : nfa.Step lb i p j p' update) : nfa.Step lb' i p j p' update

theorem Regex.NFA.Step.liftBound {s : String} {nfa : NFA} {lb lb' : ℕ} {p p' : s.Pos} {i j : ℕ} {update : Option (ℕ × s.Pos)} (le : lb' ≤ lb) (step : nfa.Step lb i p j p' update) : nfa.Step lb' i p j p' update

theorem Regex.NFA.Step.iff_done {s : String} {nfa : NFA} {lb : ℕ} {p p' : s.Pos} {i j : ℕ} {update : Option (ℕ × s.Pos)} {lt : i < nfa.size} (eq : nfa[i] = Node.done) : nfa.Step lb i p j p' update ↔ False

theorem Regex.NFA.Step.iff_fail {s : String} {nfa : NFA} {lb : ℕ} {p p' : s.Pos} {i j : ℕ} {update : Option (ℕ × s.Pos)} {lt : i < nfa.size} (eq : nfa[i] = Node.fail) : nfa.Step lb i p j p' update ↔ False

theorem Regex.NFA.Step.iff_epsilon {s : String} {nfa : NFA} {lb : ℕ} {p p' : s.Pos} {i j : ℕ} {update : Option (ℕ × s.Pos)} {next : ℕ} {lt : i < nfa.size} (eq : nfa[i] = Node.epsilon next) : nfa.Step lb i p j p' update ↔ lb ≤ i ∧ j = next ∧ p' = p ∧ update = none

theorem Regex.NFA.Step.iff_anchor {s : String} {nfa : NFA} {lb : ℕ} {p p' : s.Pos} {i j : ℕ} {update : Option (ℕ × s.Pos)} {anchor : Data.Anchor} {next : ℕ} {lt : i < nfa.size} (eq : nfa[i] = Node.anchor anchor next) : nfa.Step lb i p j p' update ↔ lb ≤ i ∧ j = next ∧ p' = p ∧ update = none ∧ Data.Anchor.test p anchor = true

theorem Regex.NFA.Step.iff_split {s : String} {nfa : NFA} {lb : ℕ} {p p' : s.Pos} {i j : ℕ} {update : Option (ℕ × s.Pos)} {next₁ next₂ : ℕ} {lt : i < nfa.size} (eq : nfa[i] = Node.split next₁ next₂) : nfa.Step lb i p j p' update ↔ lb ≤ i ∧ (j = next₁ ∨ j = next₂) ∧ p' = p ∧ update = none

theorem Regex.NFA.Step.iff_save {s : String} {nfa : NFA} {lb : ℕ} {p p' : s.Pos} {i j : ℕ} {update : Option (ℕ × s.Pos)} {offset next : ℕ} {lt : i < nfa.size} (eq : nfa[i] = Node.save offset next) : nfa.Step lb i p j p' update ↔ lb ≤ i ∧ j = next ∧ p' = p ∧ update = some (offset, p)

theorem Regex.NFA.Step.iff_char {s : String} {nfa : NFA} {lb : ℕ} {p p' : s.Pos} {i j : ℕ} {update : Option (ℕ × s.Pos)} {c : Char} {next : ℕ} {lt : i < nfa.size} (eq : nfa[i] = Node.char c next) : nfa.Step lb i p j p' update ↔ ∃ (ne : p ≠ s.endPos), lb ≤ i ∧ j = next ∧ p' = p.next ne ∧ update = none ∧ p.get ne = c

theorem Regex.NFA.Step.iff_sparse {s : String} {nfa : NFA} {lb : ℕ} {p p' : s.Pos} {i j : ℕ} {update : Option (ℕ × s.Pos)} {cs : Data.Classes} {next : ℕ} {lt : i < nfa.size} (eq : nfa[i] = Node.sparse cs next) : nfa.Step lb i p j p' update ↔ ∃ (ne : p ≠ s.endPos), lb ≤ i ∧ j = next ∧ p' = p.next ne ∧ update = none ∧ p.get ne ∈ cs

theorem Regex.NFA.Step.compile_liftBound {s : String} {p p' : s.Pos} {i j : ℕ} {update : Option (ℕ × s.Pos)} {e : Data.Expr} {nfa : NFA} (eq : compile e = nfa) (step : nfa.Step 0 i p j p' update) : nfa.Step 1 i p j p' update

inductive Regex.NFA.Path {s : String} (nfa : NFA) (lb : ℕ) : ℕ → s.Pos → ℕ → s.Pos → List (ℕ × s.Pos) → Prop

A collection of steps in an NFA forms a path. The path must contain at least one step (which implies that the first state is greater than or equal to the lower bound).

• last {s : String} {nfa : NFA} {lb i : ℕ} {p : s.Pos} {j : ℕ} {p' : s.Pos} {update : Option (ℕ × s.Pos)} (step : nfa.Step lb i p j p' update) : nfa.Path lb i p j p' (List.ofOption update)
• more {s : String} {nfa : NFA} {lb i : ℕ} {p : s.Pos} {j : ℕ} {p' : s.Pos} {k : ℕ} {p'' : s.Pos} {update : Option (ℕ × s.Pos)} {updates : List (ℕ × s.Pos)} (step : nfa.Step lb i p j p' update) (rest : nfa.Path lb j p' k p'' updates) : nfa.Path lb i p k p'' (update ::ₒ updates)

theorem Regex.NFA.Path.ge {s : String} {nfa : NFA} {lb : ℕ} {p p' : s.Pos} {i j : ℕ} {updates : List (ℕ × s.Pos)} (path : nfa.Path lb i p j p' updates) : lb ≤ i

theorem Regex.NFA.Path.lt {s : String} {nfa : NFA} {lb : ℕ} {p p' : s.Pos} {i j : ℕ} {updates : List (ℕ × s.Pos)} (path : nfa.Path lb i p j p' updates) : i < nfa.size

theorem Regex.NFA.Path.lt_right {s : String} {nfa : NFA} {lb : ℕ} {p p' : s.Pos} {i j : ℕ} {updates : List (ℕ × s.Pos)} (wf : nfa.WellFormed) (path : nfa.Path lb i p j p' updates) : j < nfa.size

theorem Regex.NFA.Path.le {s : String} {nfa : NFA} {lb : ℕ} {p p' : s.Pos} {i j : ℕ} {updates : List (ℕ × s.Pos)} (path : nfa.Path lb i p j p' updates) : p ≤ p'

theorem Regex.NFA.Path.cast {s : String} {nfa nfa' : NFA} {lb : ℕ} {p p' : s.Pos} {i j : ℕ} {updates : List (ℕ × s.Pos)} (eq : ∀ (i : ℕ), lb ≤ i → ∀ (x : i < nfa.size), ∃ (x_1 : i < nfa'.size), nfa[i] = nfa'[i]) (path : nfa.Path lb i p j p' updates) : nfa'.Path lb i p j p' updates

A simpler casting procedure where the equality can be proven easily, e.g., when casting to a larger NFA.

theorem Regex.NFA.Path.cast' {s : String} {nfa nfa' : NFA} {lb : ℕ} {p p' : s.Pos} {i j : ℕ} {updates : List (ℕ × s.Pos)} (lt : i < nfa.size) (size_le : nfa.size ≤ nfa'.size) (wf : nfa.WellFormed) (eq : ∀ (i : ℕ), lb ≤ i → ∀ (lt : i < nfa.size), nfa'[i] = nfa[i]) (path : nfa'.Path lb i p j p' updates) : nfa.Path lb i p j p' updates

A casting procedure that transports a path from a larger NFA to a smaller NFA.

theorem Regex.NFA.Path.castHead {s : String} {nfa : NFA} {lb : ℕ} {p p' : s.Pos} {j : ℕ} {updates : List (ℕ × s.Pos)} {i₁ i₂ : ℕ} (h₁ : i₁ < nfa.size) (h₂ : i₂ < nfa.size) (eq : nfa[i₁] = nfa[i₂]) (ge : lb ≤ i₂) (path : nfa.Path lb i₁ p j p' updates) : nfa.Path lb i₂ p j p' updates

theorem Regex.NFA.Path.liftBound {s : String} {nfa : NFA} {lb lb' : ℕ} {p p' : s.Pos} {i j : ℕ} {updates : List (ℕ × s.Pos)} (le : lb' ≤ lb) (path : nfa.Path lb i p j p' updates) : nfa.Path lb' i p j p' updates

theorem Regex.NFA.Path.liftBound' {s : String} {nfa : NFA} {lb lb' : ℕ} {p p' : s.Pos} {i j : ℕ} {updates : List (ℕ × s.Pos)} (ge : lb' ≤ i) (inv : ∀ {p p' : s.Pos} {i j : ℕ} {update : Option (ℕ × s.Pos)}, lb' ≤ i → lb ≤ j → nfa.Step lb i p j p' update → lb' ≤ j) (path : nfa.Path lb i p j p' updates) : nfa.Path lb' i p j p' updates

theorem Regex.NFA.Path.trans {s : String} {nfa : NFA} {lb : ℕ} {p p' p'' : s.Pos} {i j k : ℕ} {updates₁ updates₂ : List (ℕ × s.Pos)} (path₁ : nfa.Path lb i p j p' updates₁) (path₂ : nfa.Path lb j p' k p'' updates₂) : nfa.Path lb i p k p'' (updates₁ ++ updates₂)

theorem Regex.NFA.Path.compile_liftBound {s : String} {p p' : s.Pos} {i j : ℕ} {updates : List (ℕ × s.Pos)} {e : Data.Expr} {nfa : NFA} (eq : compile e = nfa) (path : nfa.Path 0 i p j p' updates) : nfa.Path 1 i p j p' updates

theorem Regex.NFA.Path.of_step_closure {s : String} {nfa : NFA} {lb : ℕ} (motive : ℕ → s.Pos → Prop) (closure : ∀ (i : ℕ) (p : s.Pos) (j : ℕ) (p' : s.Pos) (update : Option (ℕ × s.Pos)), motive i p → nfa.Step lb i p j p' update → motive j p') {i : ℕ} {p : s.Pos} {j : ℕ} {p' : s.Pos} {update : List (ℕ × s.Pos)} (base : motive i p) (path : nfa.Path lb i p j p' update) : motive j p'

If a property is closed under a single step, then it is closed under a path.