Consider nfa' := nfa.pushRegex next e. When there is a path in nfa' from nfa'.start to next,
it must have looped nfaExpr before n times, followed by the last step from nfa'.start to next.
A Loop term corresponds to such a loop. The last variant corresponds to the last step,
and the loop variant extracts the first iteration and the remaining loop.
- last [Star] {s : String} {pos : s.ValidPos} (step : nfa'.Step nfa.nodes.size nfa'.start pos next pos none) : Loop pos pos []
- loop [Star] {s : String} {pos pos' pos'' : s.ValidPos} {update₁ update₂ : List (ℕ × s.ValidPos)} (path : nfa'.Path nfaPlaceholder.nodes.size nfaExpr.start pos nfaPlaceholder.start pos' update₁) (loop : Loop pos' pos'' update₂) : Loop pos pos'' (update₁ ++ update₂)
Instances For
theorem
Regex.NFA.Compile.ProofData.Star.Loop.introAux
[Star]
{s : String}
{pos pos' : s.ValidPos}
{i j : ℕ}
{update : List (ℕ × s.ValidPos)}
(lt : i < nfa'.nodes.size)
(wf : nfa.WellFormed)
(next_lt : next < nfa.nodes.size)
(eqj : j = next)
(path : nfa'.Path nfa.nodes.size i pos j pos' update)
:
if i = nfa'.start then
nfa'.Step nfa.nodes.size nfa'.start pos next pos' none ∧ pos' = pos ∧ update = [] ∨ ∃ (posm : s.ValidPos) (update₁ : List (ℕ × s.ValidPos)) (update₂ : List (ℕ × s.ValidPos)),
nfa'.Path nfaPlaceholder.nodes.size nfaExpr.start pos nfaPlaceholder.start posm update₁ ∧ Loop posm pos' update₂ ∧ update = update₁ ++ update₂
else ∃ (posm : s.ValidPos) (update₁ : List (ℕ × s.ValidPos)) (update₂ : List (ℕ × s.ValidPos)),
nfa'.Path nfaPlaceholder.nodes.size i pos nfaPlaceholder.start posm update₁ ∧ Loop posm pos' update₂ ∧ update = update₁ ++ update₂