inductive Regex.NFA.Compile.ProofData.Star.Loop [Star] {s : String} : s.Pos → s.Pos → List (ℕ × s.Pos) → Prop

Consider nfa' := nfa.pushRegex next (.star greedy e). When there is a path in nfa' from nfaExpr.start to next, it must have looped nfaExpr before n times, followed by the last step from nfa.size 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.Pos} (step : nfa'.Step nfa.size nfa.size pos next pos none) : Loop pos pos []
• loop [Star] {s : String} {pos pos' pos'' : s.Pos} {update₁ update₂ : List (ℕ × s.Pos)} (path : nfa'.Path nfaPlaceholder.size nfaExpr.start pos nfaPlaceholder.start pos' update₁) (loop : Loop pos' pos'' update₂) : Loop pos pos'' (update₁ ++ update₂)

theorem Regex.NFA.Compile.ProofData.Star.Loop.intro [Star] {s : String} {pos pos' : s.Pos} {update : List (ℕ × s.Pos)} (wf : nfa.WellFormed) (next_lt : next < nfa.size) (path : nfa'.Path nfa.size nfaExpr.start pos next pos' update) : Loop pos pos' update