inductive
Regex.NFA.Compile.ProofData.Star.Loop
[Star]
:
String.Iterator → String.Iterator → List (ℕ × String.Pos) → Prop
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] {it : String.Iterator} (step : nfa'.Step nfa.nodes.size nfa'.start it next it none) : Loop it it []
- loop [Star] {it it' it'' : String.Iterator} {update₁ update₂ : List (ℕ × String.Pos)} (path : nfa'.Path nfaPlaceholder.nodes.size nfaExpr.start it nfaPlaceholder.start it' update₁) (loop : Loop it' it'' update₂) : Loop it it'' (update₁ ++ update₂)
Instances For
theorem
Regex.NFA.Compile.ProofData.Star.Loop.introAux
[Star]
{i : ℕ}
{it : String.Iterator}
{j : ℕ}
{it' : String.Iterator}
{update : List (ℕ × String.Pos)}
(lt : i < nfa'.nodes.size)
(wf : nfa.WellFormed)
(next_lt : next < nfa.nodes.size)
(eqj : j = next)
(path : nfa'.Path nfa.nodes.size i it j it' update)
:
if i = nfa'.start then
nfa'.Step nfa.nodes.size nfa'.start it next it' none ∧ it' = it ∧ update = [] ∨ ∃ (itm : String.Iterator) (update₁ : List (ℕ × String.Pos)) (update₂ : List (ℕ × String.Pos)),
nfa'.Path nfaPlaceholder.nodes.size nfaExpr.start it nfaPlaceholder.start itm update₁ ∧ Loop itm it' update₂ ∧ update = update₁ ++ update₂
else ∃ (itm : String.Iterator) (update₁ : List (ℕ × String.Pos)) (update₂ : List (ℕ × String.Pos)),
nfa'.Path nfaPlaceholder.nodes.size i it nfaPlaceholder.start itm update₁ ∧ Loop itm it' update₂ ∧ update = update₁ ++ update₂