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

• epsilon {nfa : NFA} {lb i j : ℕ} {it : String.Iterator} (ge : lb ≤ i) (lt : i < nfa.nodes.size) (eq : nfa[i] = Node.epsilon j) (v : it.Valid) : nfa.Step lb i it j it none
• anchor {nfa : NFA} {lb i j : ℕ} {it : String.Iterator} {a : Data.Anchor} (ge : lb ≤ i) (lt : i < nfa.nodes.size) (eq : nfa[i] = Node.anchor a j) (v : it.Valid) (h : Data.Anchor.test it a = true) : nfa.Step lb i it j it none
• splitLeft {nfa : NFA} {lb i j₁ j₂ : ℕ} {it : String.Iterator} (ge : lb ≤ i) (lt : i < nfa.nodes.size) (eq : nfa[i] = Node.split j₁ j₂) (v : it.Valid) : nfa.Step lb i it j₁ it none
• splitRight {nfa : NFA} {lb i j₁ j₂ : ℕ} {it : String.Iterator} (ge : lb ≤ i) (lt : i < nfa.nodes.size) (eq : nfa[i] = Node.split j₁ j₂) (v : it.Valid) : nfa.Step lb i it j₂ it none
• save {nfa : NFA} {lb i j : ℕ} {it : String.Iterator} {offset : ℕ} (ge : lb ≤ i) (lt : i < nfa.nodes.size) (eq : nfa[i] = Node.save offset j) (v : it.Valid) : nfa.Step lb i it j it (some (offset, it.pos))
• char {nfa : NFA} {lb i j : ℕ} {it : String.Iterator} {l : List Char} {c : Char} {r : List Char} (ge : lb ≤ i) (lt : i < nfa.nodes.size) (eq : nfa[i] = Node.char c j) (vf : String.Iterator.ValidFor l (c :: r) it) : nfa.Step lb i it j it.next none
• sparse {nfa : NFA} {lb i j : ℕ} {it : String.Iterator} {l : List Char} {c : Char} {r : List Char} {cs : Data.Classes} (ge : lb ≤ i) (lt : i < nfa.nodes.size) (eq : nfa[i] = Node.sparse cs j) (vf : String.Iterator.ValidFor l (c :: r) it) (mem : c ∈ cs) : nfa.Step lb i it j it.next none

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

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

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

theorem Regex.NFA.Step.it_eq_or_next {nfa : NFA} {lb i : ℕ} {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : Option (ℕ × String.Pos)} (step : nfa.Step lb i it j it' update) : it' = it ∨ it.hasNext = true ∧ it' = it.next

theorem Regex.NFA.Step.le_pos {nfa : NFA} {lb i : ℕ} {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : Option (ℕ × String.Pos)} (step : nfa.Step lb i it j it' update) : it.pos ≤ it'.pos

theorem Regex.NFA.Step.validL {nfa : NFA} {lb i : ℕ} {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : Option (ℕ × String.Pos)} (step : nfa.Step lb i it j it' update) : it.Valid

theorem Regex.NFA.Step.validR {nfa : NFA} {lb i : ℕ} {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : Option (ℕ × String.Pos)} (step : nfa.Step lb i it j it' update) : it'.Valid

theorem Regex.NFA.Step.toString_eq {nfa : NFA} {lb i : ℕ} {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : Option (ℕ × String.Pos)} (step : nfa.Step lb i it j it' update) : it'.toString = it.toString

theorem Regex.NFA.Step.le_endPos {nfa : NFA} {lb i : ℕ} {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : Option (ℕ × String.Pos)} (step : nfa.Step lb i it j it' update) : it'.pos ≤ it.toString.endPos

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

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

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

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

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

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

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

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

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

theorem Regex.NFA.Step.iff_char {nfa : NFA} {lb i : ℕ} {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : Option (ℕ × String.Pos)} {c : Char} {next : ℕ} {lt : i < nfa.nodes.size} (eq : nfa[i] = Node.char c next) : nfa.Step lb i it j it' update ↔ ∃ (l : List Char) (r : List Char), lb ≤ i ∧ j = next ∧ it' = it.next ∧ update = none ∧ String.Iterator.ValidFor l (c :: r) it

theorem Regex.NFA.Step.iff_sparse {nfa : NFA} {lb i : ℕ} {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {update : Option (ℕ × String.Pos)} {cs : Data.Classes} {next : ℕ} {lt : i < nfa.nodes.size} (eq : nfa[i] = Node.sparse cs next) : nfa.Step lb i it j it' update ↔ ∃ (l : List Char) (c : Char) (r : List Char), lb ≤ i ∧ j = next ∧ it' = it.next ∧ update = none ∧ String.Iterator.ValidFor l (c :: r) it ∧ c ∈ cs

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

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

A collection of steps in an NFA forms a path.

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

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

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

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

theorem Regex.NFA.Path.toString {nfa : NFA} {lb i : ℕ} {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {updates : List (ℕ × String.Pos)} (path : nfa.Path lb i it j it' updates) : it'.toString = it.toString

theorem Regex.NFA.Path.le_pos {nfa : NFA} {lb i : ℕ} {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {updates : List (ℕ × String.Pos)} (path : nfa.Path lb i it j it' updates) : it.pos ≤ it'.pos

theorem Regex.NFA.Path.validL {nfa : NFA} {lb i : ℕ} {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {updates : List (ℕ × String.Pos)} (path : nfa.Path lb i it j it' updates) : it.Valid

theorem Regex.NFA.Path.validR {nfa : NFA} {lb i : ℕ} {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {updates : List (ℕ × String.Pos)} (path : nfa.Path lb i it j it' updates) : it'.Valid

theorem Regex.NFA.Path.cast {nfa nfa' : NFA} {lb i : ℕ} {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {updates : List (ℕ × String.Pos)} (eq : ∀ (i : ℕ), lb ≤ i → ∀ (x : i < nfa.nodes.size), ∃ (x_1 : i < nfa'.nodes.size), nfa[i] = nfa'[i]) (path : nfa.Path lb i it j it' updates) : nfa'.Path lb i it j it' 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' {nfa nfa' : NFA} {lb i : ℕ} {it : String.Iterator} {j : ℕ} {it' : String.Iterator} {updates : List (ℕ × String.Pos)} (lt : i < nfa.nodes.size) (size_le : nfa.nodes.size ≤ nfa'.nodes.size) (wf : nfa.WellFormed) (eq : ∀ (i : ℕ), lb ≤ i → ∀ (lt : i < nfa.nodes.size), nfa'[i] = nfa[i]) (path : nfa'.Path lb i it j it' updates) : nfa.Path lb i it j it' updates

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

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

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

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

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

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

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