diff --git a/src/Init/Data/Iterators/Basic.lean b/src/Init/Data/Iterators/Basic.lean
index e8f322bcb663..3b76667459d5 100644
--- a/src/Init/Data/Iterators/Basic.lean
+++ b/src/Init/Data/Iterators/Basic.lean
@@ -241,6 +241,16 @@ def IterStep.successor : IterStep α β → Option α
   | .skip it => some it
   | .done => none
 
+@[simp]
+theorem IterStep.successor_yield {it : α} {out : β} :
+  (IterStep.yield it out).successor = some it := rfl
+
+@[simp]
+theorem IterStep.successor_skip {it : α} : (IterStep.skip (β := β) it).successor = some it := rfl
+
+@[simp]
+theorem IterStep.successor_done : (IterStep.done (α := α) (β := β)).successor = none := rfl
+
 /--
 If present, applies `f` to the iterator of an `IterStep` and replaces the iterator
 with the result of the application of `f`.
@@ -543,6 +553,10 @@ def Iter.IsPlausibleSuccessorOf {α : Type w} {β : Type w} [Iterator α Id β]
     (it' it : Iter (α := α) β) : Prop :=
   it'.toIterM.IsPlausibleSuccessorOf it.toIterM
 
+theorem Iter.isPlausibleSuccessorOf_eq_invImage {α : Type w} {β : Type w} [Iterator α Id β] :
+    IsPlausibleSuccessorOf (α := α) (β := β) =
+      InvImage (IterM.IsPlausibleSuccessorOf (α := α) (β := β) (m := Id)) Iter.toIterM := rfl
+
 theorem Iter.isPlausibleSuccessorOf_iff_exists {α : Type w} {β : Type w} [Iterator α Id β]
     {it' it : Iter (α := α) β} :
     it'.IsPlausibleSuccessorOf it ↔ ∃ step, step.successor = some it' ∧ it.IsPlausibleStep step := by
@@ -555,6 +569,16 @@ theorem Iter.isPlausibleSuccessorOf_iff_exists {α : Type w} {β : Type w} [Iter
     exact ⟨step.mapIterator Iter.toIterM,
       by cases step <;> simp_all [IterStep.successor, Iter.IsPlausibleStep]⟩
 
+theorem Iter.IsPlausibleStep.isPlausibleSuccessor_of_yield {α : Type w} {β : Type w}
+    [Iterator α Id β] {it' it : Iter (α := α) β} {out : β}
+    (h : it.IsPlausibleStep (.yield it' out)) : it'.IsPlausibleSuccessorOf it := by
+  simpa [isPlausibleSuccessorOf_iff_exists] using ⟨.yield it' out, by simp [h]⟩
+
+theorem Iter.IsPlausibleStep.isPlausibleSuccessor_of_skip {α : Type w} {β : Type w}
+    [Iterator α Id β] {it' it : Iter (α := α) β} (h : it.IsPlausibleStep (.skip it')) :
+    it'.IsPlausibleSuccessorOf it := by
+  simpa [isPlausibleSuccessorOf_iff_exists] using ⟨.skip it', by simp [h]⟩
+
 /--
 Asserts that a certain iterator `it` could plausibly yield the value `out` after an arbitrary
 number of steps.
@@ -656,6 +680,10 @@ Given this typeclass, termination proofs for well-founded recursion over an iter
 class Finite (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] : Prop where
   wf : WellFounded (IterM.IsPlausibleSuccessorOf (α := α) (m := m))
 
+theorem Finite.wf_of_id {α : Type w} {β : Type w} [Iterator α Id β] [Finite α Id] :
+    WellFounded (Iter.IsPlausibleSuccessorOf (α := α)) := by
+  simpa [Iter.isPlausibleSuccessorOf_eq_invImage] using InvImage.wf _ Finite.wf
+
 /--
 This type is a wrapper around `IterM` so that it becomes a useful termination measure for
 recursion over finite iterators. See also `IterM.finitelyManySteps` and `Iter.finitelyManySteps`.
@@ -705,6 +733,12 @@ theorem IterM.TerminationMeasures.Finite.rel_of_skip
     Rel ⟨it'⟩ ⟨it⟩ := by
   exact .single ⟨_, rfl, h⟩
 
+theorem IterM.TerminationMeasures.Finite.rel_trans
+    {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β]
+    {it it' it'' : TerminationMeasures.Finite α m} :
+    it.Rel it' → it'.Rel it'' → it.Rel it'' :=
+  .trans
+
 macro_rules | `(tactic| decreasing_trivial) => `(tactic|
   first
   | exact IterM.TerminationMeasures.Finite.rel_of_yield ‹_›
diff --git a/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean b/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
index 5554d04cebd8..f161aab3c291 100644
--- a/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
+++ b/src/Init/Data/Iterators/Combinators/Monadic/FilterMap.lean
@@ -94,7 +94,7 @@ it.filterMapWithPostcondition     ---a'-----c'-------⊥
 **Termination properties:**
 
 * `Finite` instance: only if `it` is finite
-* `Productive` instance: only if `it` is finite`
+* `Productive` instance: only if `it` is finite
 
 For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though
 no `Finite` (or `Productive`) instance is provided. For example, if `f` never returns `none`, then
diff --git a/src/Init/Data/String/Pattern/Basic.lean b/src/Init/Data/String/Pattern/Basic.lean
index fbb9452ab9ca..7e28106181f5 100644
--- a/src/Init/Data/String/Pattern/Basic.lean
+++ b/src/Init/Data/String/Pattern/Basic.lean
@@ -35,7 +35,7 @@ inductive SearchStep (s : Slice) where
   -/
   | rejected (startPos endPos : s.Pos)
   /--
-  The subslice starting at {name}`startPos` and ending at {name}`endPos` did not match the pattern.
+  The subslice starting at {name}`startPos` and ending at {name}`endPos` matches the pattern.
   -/
   | matched (startPos endPos : s.Pos)
 deriving Inhabited
@@ -99,44 +99,6 @@ where
     simp [Pos.Raw.lt_iff] at h ⊢
     omega
 
-variable {ρ : Type} {σ : Slice → Type}
-variable [∀ s, Std.Iterators.Iterator (σ s) Id (SearchStep s)]
-variable [∀ s, Std.Iterators.Finite (σ s) Id]
-
-/--
-Tries to skip the {name}`searcher` until the next {name}`SearchStep.matched` and return it. If no
-match is found until the end returns {name}`none`.
--/
-@[inline]
-def nextMatch (searcher : Std.Iter (α := σ s) (SearchStep s)) :
-    Option (Std.Iter (α := σ s) (SearchStep s) × s.Pos × s.Pos) :=
-  go searcher
-where
-  go [∀ s, Std.Iterators.Finite (σ s) Id] (searcher : Std.Iter (α := σ s) (SearchStep s)) :
-      Option (Std.Iter (α := σ s) (SearchStep s) × s.Pos × s.Pos) :=
-    match searcher.step with
-    | .yield it (.matched startPos endPos) _ => some (it, startPos, endPos)
-    | .yield it (.rejected ..) _ | .skip it .. => go it
-    | .done .. => none
-  termination_by Std.Iterators.Iter.finitelyManySteps searcher
-
-/--
-Tries to skip the {name}`searcher` until the next {name}`SearchStep.rejected` and return it. If no
-reject is found until the end returns {name}`none`.
--/
-@[inline]
-def nextReject (searcher : Std.Iter (α := σ s) (SearchStep s)) :
-    Option (Std.Iter (α := σ s) (SearchStep s) × s.Pos × s.Pos) :=
-  go searcher
-where
-  go [∀ s, Std.Iterators.Finite (σ s) Id] (searcher : Std.Iter (α := σ s) (SearchStep s)) :
-      Option (Std.Iter (α := σ s) (SearchStep s) × s.Pos × s.Pos) :=
-    match searcher.step with
-    | .yield it (.rejected startPos endPos) _ => some (it, startPos, endPos)
-    | .yield it (.matched ..) _ | .skip it .. => go it
-    | .done .. => none
-  termination_by Std.Iterators.Iter.finitelyManySteps searcher
-
 end Internal
 
 namespace ForwardPattern
diff --git a/src/Init/Data/String/Slice.lean b/src/Init/Data/String/Slice.lean
index 5eb95930fd08..bf1d62fad806 100644
--- a/src/Init/Data/String/Slice.lean
+++ b/src/Init/Data/String/Slice.lean
@@ -112,8 +112,8 @@ Examples:
 def startsWith [ForwardPattern ρ] (s : Slice) (pat : ρ) : Bool :=
   ForwardPattern.startsWith s pat
 
-inductive SplitIterator (ρ : Type) [ToForwardSearcher ρ σ] where
-  | operating (s : Slice) (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
+inductive SplitIterator (ρ : Type) (s : Slice) [ToForwardSearcher ρ σ] where
+  | operating (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
   | atEnd
 deriving Inhabited
 
@@ -121,33 +121,72 @@ namespace SplitIterator
 
 variable [ToForwardSearcher ρ σ]
 
-instance [Pure m] : Std.Iterators.Iterator (SplitIterator ρ) m Slice where
-  IsPlausibleStep := fun _ _ => True
-  step := fun ⟨iter⟩ =>
-    match iter with
-    | .operating s currPos searcher =>
-      match Internal.nextMatch searcher with
-      | some (searcher, startPos, endPos) =>
+inductive PlausibleStep
+
+instance : Std.Iterators.Iterator (SplitIterator ρ s) Id Slice where
+  IsPlausibleStep
+    | ⟨.operating _ s⟩, .yield ⟨.operating _ s'⟩ _ => s'.IsPlausibleSuccessorOf s
+    | ⟨.operating _ s⟩, .yield ⟨.atEnd ..⟩ _ => True
+    | ⟨.operating _ s⟩, .skip ⟨.operating _ s'⟩ => s'.IsPlausibleSuccessorOf s
+    | ⟨.operating _ s⟩, .skip ⟨.atEnd ..⟩ => False
+    | ⟨.operating _ s⟩, .done => True
+    | ⟨.atEnd⟩, .yield .. => False
+    | ⟨.atEnd⟩, .skip _ => False
+    | ⟨.atEnd⟩, .done => True
+  step
+    | ⟨.operating currPos searcher⟩ =>
+      match h : searcher.step with
+      | ⟨.yield searcher' (.matched startPos endPos), hps⟩ =>
         let slice := s.replaceStartEnd! currPos startPos
-        let nextIt := ⟨.operating s endPos searcher⟩
-        pure (.deflate ⟨.yield nextIt slice, by simp⟩)
-      | none =>
+        let nextIt := ⟨.operating endPos searcher'⟩
+        pure (.deflate ⟨.yield nextIt slice, by simp [nextIt, hps.isPlausibleSuccessor_of_yield]⟩)
+      | ⟨.yield searcher' (.rejected ..), hps⟩ =>
+        pure (.deflate ⟨.skip ⟨.operating currPos searcher'⟩,
+          by simp [hps.isPlausibleSuccessor_of_yield]⟩)
+      | ⟨.skip searcher', hps⟩ =>
+        pure (.deflate ⟨.skip ⟨.operating currPos searcher'⟩,
+          by simp [hps.isPlausibleSuccessor_of_skip]⟩)
+      | ⟨.done, _⟩ =>
         let slice := s.replaceStart currPos
         pure (.deflate ⟨.yield ⟨.atEnd⟩ slice, by simp⟩)
-    | .atEnd => pure (.deflate ⟨.done, by simp⟩)
+    | ⟨.atEnd⟩ => pure (.deflate ⟨.done, by simp⟩)
 
--- TODO: Finiteness after we have a notion of lawful searcher
+private def toOption : SplitIterator ρ s → Option (Std.Iter (α := σ s) (SearchStep s))
+  | .operating _ s => some s
+  | .atEnd => none
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect (SplitIterator ρ) m n :=
+private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
+    Std.Iterators.FinitenessRelation (SplitIterator ρ s) Id where
+  rel := InvImage (Option.lt Std.Iterators.Iter.IsPlausibleSuccessorOf)
+    (SplitIterator.toOption ∘ Std.Iterators.IterM.internalState)
+  wf := InvImage.wf _ (Option.wellFounded_lt Std.Iterators.Finite.wf_of_id)
+  subrelation {it it'} h := by
+    simp_wf
+    obtain ⟨step, h, h'⟩ := h
+    match step with
+    | .yield it'' out | .skip it'' =>
+      obtain rfl : it' = it'' := by simpa using h.symm
+      simp only [Std.Iterators.IterM.IsPlausibleStep, Std.Iterators.Iterator.IsPlausibleStep] at h'
+      revert h'
+      match it, it' with
+      | ⟨.operating _ searcher⟩, ⟨.operating _ searcher'⟩ => simp [SplitIterator.toOption, Option.lt]
+      | ⟨.operating _ searcher⟩, ⟨.atEnd⟩ => simp [SplitIterator.toOption, Option.lt]
+      | ⟨.atEnd⟩, _ => simp
+
+@[no_expose]
+instance [Std.Iterators.Finite (σ s) Id] : Std.Iterators.Finite (SplitIterator ρ s) Id :=
+  .of_finitenessRelation finitenessRelation
+
+instance [Monad n] : Std.Iterators.IteratorCollect (SplitIterator ρ s) Id n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorCollectPartial (SplitIterator ρ) m n :=
+instance [Monad n] : Std.Iterators.IteratorCollectPartial (SplitIterator ρ s) Id n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop (SplitIterator ρ) m n :=
+instance [Monad n] : Std.Iterators.IteratorLoop (SplitIterator ρ s) Id n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (SplitIterator ρ) m n :=
+instance [Monad n] : Std.Iterators.IteratorLoopPartial (SplitIterator ρ s) Id n :=
   .defaultImplementation
 
 end SplitIterator
@@ -161,18 +200,18 @@ multiple subslices in a row match the pattern, the resulting list will contain e
 This function is generic over all currently supported patterns.
 
 Examples:
- * {lean}`("coffee tea water".toSlice.split Char.isWhitespace).allowNontermination.toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`
- * {lean}`("coffee tea water".toSlice.split ' ').allowNontermination.toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`
- * {lean}`("coffee tea water".toSlice.split " tea ").allowNontermination.toList == ["coffee".toSlice, "water".toSlice]`
- * {lean}`("ababababa".toSlice.split "aba").allowNontermination.toList == ["coffee".toSlice, "water".toSlice]`
- * {lean}`("baaab".toSlice.split "aa").allowNontermination.toList == ["b".toSlice, "ab".toSlice]`
+ * {lean}`("coffee tea water".toSlice.split Char.isWhitespace).toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`
+ * {lean}`("coffee tea water".toSlice.split ' ').toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]`
+ * {lean}`("coffee tea water".toSlice.split " tea ").toList == ["coffee".toSlice, "water".toSlice]`
+ * {lean}`("ababababa".toSlice.split "aba").toList == ["coffee".toSlice, "water".toSlice]`
+ * {lean}`("baaab".toSlice.split "aa").toList == ["b".toSlice, "ab".toSlice]`
 -/
 @[specialize pat]
-def split [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) : Std.Iter (α := SplitIterator ρ) Slice :=
-  { internalState := .operating s s.startPos (ToForwardSearcher.toSearcher s pat) }
+def split [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) : Std.Iter (α := SplitIterator ρ s) Slice :=
+  { internalState := .operating s.startPos (ToForwardSearcher.toSearcher s pat) }
 
-inductive SplitInclusiveIterator (ρ : Type) [ToForwardSearcher ρ σ] where
-  | operating (s : Slice) (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
+inductive SplitInclusiveIterator (ρ : Type) (s : Slice) [ToForwardSearcher ρ σ] where
+  | operating (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
   | atEnd
 deriving Inhabited
 
@@ -180,40 +219,79 @@ namespace SplitInclusiveIterator
 
 variable [ToForwardSearcher ρ σ]
 
-instance [Pure m] : Std.Iterators.Iterator (SplitInclusiveIterator ρ) m Slice where
-  IsPlausibleStep := fun _ _ => True
-  step := fun ⟨iter⟩ =>
-    match iter with
-    | .operating s currPos searcher =>
-      match Internal.nextMatch searcher with
-      | some (searcher, _, endPos) =>
+instance : Std.Iterators.Iterator (SplitInclusiveIterator ρ s) Id Slice where
+  IsPlausibleStep
+    | ⟨.operating _ s⟩, .yield ⟨.operating _ s'⟩ _ => s'.IsPlausibleSuccessorOf s
+    | ⟨.operating _ s⟩, .yield ⟨.atEnd ..⟩ _ => True
+    | ⟨.operating _ s⟩, .skip ⟨.operating _ s'⟩ => s'.IsPlausibleSuccessorOf s
+    | ⟨.operating _ s⟩, .skip ⟨.atEnd ..⟩ => False
+    | ⟨.operating _ s⟩, .done => True
+    | ⟨.atEnd⟩, .yield .. => False
+    | ⟨.atEnd⟩, .skip _ => False
+    | ⟨.atEnd⟩, .done => True
+  step
+    | ⟨.operating currPos searcher⟩ =>
+      match h : searcher.step with
+      | ⟨.yield searcher' (.matched _ endPos), hps⟩ =>
         let slice := s.replaceStartEnd! currPos endPos
-        let nextIt := ⟨.operating s endPos searcher⟩
-        pure (.deflate ⟨.yield nextIt slice, by simp⟩)
-      | none =>
+        let nextIt := ⟨.operating endPos searcher'⟩
+        pure (.deflate ⟨.yield nextIt slice,
+          by simp [nextIt, hps.isPlausibleSuccessor_of_yield]⟩)
+      | ⟨.yield searcher' (.rejected ..), hps⟩ =>
+        pure (.deflate ⟨.skip ⟨.operating currPos searcher'⟩,
+          by simp [hps.isPlausibleSuccessor_of_yield]⟩)
+      | ⟨.skip searcher', hps⟩ =>
+        pure (.deflate ⟨.skip ⟨.operating currPos searcher'⟩,
+          by simp [hps.isPlausibleSuccessor_of_skip]⟩)
+      | ⟨.done, _⟩ =>
         if currPos != s.endPos then
           let slice := s.replaceStart currPos
           pure (.deflate ⟨.yield ⟨.atEnd⟩ slice, by simp⟩)
         else
           pure (.deflate ⟨.done, by simp⟩)
-    | .atEnd => pure (.deflate ⟨.done, by simp⟩)
+    | ⟨.atEnd⟩ => pure (.deflate ⟨.done, by simp⟩)
 
--- TODO: Finiteness after we have a notion of lawful searcher
+private def toOption : SplitInclusiveIterator ρ s → Option (Std.Iter (α := σ s) (SearchStep s))
+  | .operating _ s => some s
+  | .atEnd => none
 
-instance [Monad m] [Monad n] :
-    Std.Iterators.IteratorCollect (SplitInclusiveIterator ρ) m n :=
+private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
+    Std.Iterators.FinitenessRelation (SplitInclusiveIterator ρ s) Id where
+  rel := InvImage (Option.lt Std.Iterators.Iter.IsPlausibleSuccessorOf)
+    (SplitInclusiveIterator.toOption ∘ Std.Iterators.IterM.internalState)
+  wf := InvImage.wf _ (Option.wellFounded_lt Std.Iterators.Finite.wf_of_id)
+  subrelation {it it'} h := by
+    simp_wf
+    obtain ⟨step, h, h'⟩ := h
+    match step with
+    | .yield it'' out | .skip it'' =>
+      obtain rfl : it' = it'' := by simpa using h.symm
+      simp only [Std.Iterators.IterM.IsPlausibleStep, Std.Iterators.Iterator.IsPlausibleStep] at h'
+      revert h'
+      match it, it' with
+      | ⟨.operating _ searcher⟩, ⟨.operating _ searcher'⟩ => simp [SplitInclusiveIterator.toOption, Option.lt]
+      | ⟨.operating _ searcher⟩, ⟨.atEnd⟩ => simp [SplitInclusiveIterator.toOption, Option.lt]
+      | ⟨.atEnd⟩, _ => simp
+
+@[no_expose]
+instance [Std.Iterators.Finite (σ s) Id] :
+    Std.Iterators.Finite (SplitInclusiveIterator ρ s) Id :=
+  .of_finitenessRelation finitenessRelation
+
+instance [Monad n] {s} :
+    Std.Iterators.IteratorCollect (SplitInclusiveIterator ρ s) Id n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] :
-    Std.Iterators.IteratorCollectPartial (SplitInclusiveIterator ρ) m n :=
+instance [Monad n] {s} :
+    Std.Iterators.IteratorCollectPartial (SplitInclusiveIterator ρ s) Id n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] :
-    Std.Iterators.IteratorLoop (SplitInclusiveIterator ρ) m n :=
+instance [Monad n] {s} :
+    Std.Iterators.IteratorLoop (SplitInclusiveIterator ρ s) Id n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] :
-    Std.Iterators.IteratorLoopPartial (SplitInclusiveIterator ρ) m n :=
+instance [Monad n] {s} :
+    Std.Iterators.IteratorLoopPartial (SplitInclusiveIterator ρ s) Id n :=
   .defaultImplementation
 
 end SplitInclusiveIterator
@@ -225,15 +303,15 @@ matched subslices are included at the end of each subslice.
 This function is generic over all currently supported patterns.
 
 Examples:
- * {lean}`("coffee tea water".toSlice.splitInclusive Char.isWhitespace).allowNontermination.toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]`
- * {lean}`("coffee tea water".toSlice.splitInclusive ' ').allowNontermination.toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]`
- * {lean}`("coffee tea water".toSlice.splitInclusive " tea ").allowNontermination.toList == ["coffee tea ".toSlice, "water".toSlice]`
- * {lean}`("baaab".toSlice.splitInclusive "aa").allowNontermination.toList == ["baa".toSlice, "ab".toSlice]`
+ * {lean}`("coffee tea water".toSlice.splitInclusive Char.isWhitespace).toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]`
+ * {lean}`("coffee tea water".toSlice.splitInclusive ' ').toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]`
+ * {lean}`("coffee tea water".toSlice.splitInclusive " tea ").toList == ["coffee tea ".toSlice, "water".toSlice]`
+ * {lean}`("baaab".toSlice.splitInclusive "aa").toList == ["baa".toSlice, "ab".toSlice]`
 -/
 @[specialize pat]
 def splitInclusive [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) :
-    Std.Iter (α := SplitInclusiveIterator ρ) Slice :=
-  { internalState := .operating s s.startPos (ToForwardSearcher.toSearcher s pat) }
+    Std.Iter (α := SplitInclusiveIterator ρ s) Slice :=
+  { internalState := .operating s.startPos (ToForwardSearcher.toSearcher s pat) }
 
 /--
 If {name}`pat` matches a prefix of {name}`s`, returns the remainder. Returns {name}`none` otherwise.
@@ -384,9 +462,7 @@ Examples:
 @[specialize pat]
 def find? [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) : Option s.Pos :=
   let searcher := ToForwardSearcher.toSearcher s pat
-  match Internal.nextMatch searcher with
-  | some (_, startPos, _) => some startPos
-  | none => none
+  searcher.findSome? (fun | .matched startPos _ => some startPos | .rejected .. => none)
 
 /--
 Checks whether a slice has a match of the pattern {name}`pat` anywhere.
@@ -401,7 +477,7 @@ Examples:
 @[specialize pat]
 def contains [ToForwardSearcher ρ σ] (s : Slice) (pat : ρ) : Bool :=
   let searcher := ToForwardSearcher.toSearcher s pat
-  Internal.nextMatch searcher |>.isSome
+  searcher.any (· matches .matched ..)
 
 /--
 Checks whether a slice only consists of matches of the pattern {name}`pat` anywhere.
@@ -415,6 +491,7 @@ Examples:
  * {lean}`"brown and orange".toSlice.all Char.isLower = false`
  * {lean}`"aaaaaa".toSlice.all 'a' = true`
  * {lean}`"aaaaaa".toSlice.all "aa" = true`
+ * {lean}`"aaaaaaa".toSlice.all "aa" = false`
 -/
 @[inline]
 def all [ForwardPattern ρ] (s : Slice) (pat : ρ) : Bool :=
@@ -445,8 +522,8 @@ Examples:
 def endsWith [BackwardPattern ρ] (s : Slice) (pat : ρ) : Bool :=
   BackwardPattern.endsWith s pat
 
-inductive RevSplitIterator (ρ : Type) [ToBackwardSearcher ρ σ] where
-  | operating (s : Slice) (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
+inductive RevSplitIterator (ρ : Type) (s : Slice) [ToBackwardSearcher ρ σ] where
+  | operating (currPos : s.Pos) (searcher : Std.Iter (α := σ s) (SearchStep s))
   | atEnd
 deriving Inhabited
 
@@ -454,37 +531,74 @@ namespace RevSplitIterator
 
 variable [ToBackwardSearcher ρ σ]
 
-instance [Pure m] : Std.Iterators.Iterator (RevSplitIterator ρ) m Slice where
-  IsPlausibleStep := fun _ _ => True
-  step := fun ⟨iter⟩ =>
-    match iter with
-    | .operating s currPos searcher =>
-      match Internal.nextMatch searcher with
-      | some (searcher, startPos, endPos) =>
+instance [Pure m] : Std.Iterators.Iterator (RevSplitIterator ρ s) m Slice where
+  IsPlausibleStep
+    | ⟨.operating _ s⟩, .yield ⟨.operating _ s'⟩ _ => s'.IsPlausibleSuccessorOf s
+    | ⟨.operating _ s⟩, .yield ⟨.atEnd ..⟩ _ => True
+    | ⟨.operating _ s⟩, .skip ⟨.operating _ s'⟩ => s'.IsPlausibleSuccessorOf s
+    | ⟨.operating _ s⟩, .skip ⟨.atEnd ..⟩ => False
+    | ⟨.operating _ s⟩, .done => True
+    | ⟨.atEnd⟩, .yield .. => False
+    | ⟨.atEnd⟩, .skip _ => False
+    | ⟨.atEnd⟩, .done => True
+  step
+    | ⟨.operating currPos searcher⟩ =>
+      match h : searcher.step with
+      | ⟨.yield searcher' (.matched startPos endPos), hps⟩ =>
         let slice := s.replaceStartEnd! endPos currPos
-        let nextIt := ⟨.operating s startPos searcher⟩
-        pure (.deflate ⟨.yield nextIt slice, by simp⟩)
-      | none =>
+        let nextIt := ⟨.operating startPos searcher'⟩
+        pure (.deflate ⟨.yield nextIt slice, by simp [nextIt, hps.isPlausibleSuccessor_of_yield]⟩)
+      | ⟨.yield searcher' (.rejected ..), hps⟩ =>
+        pure (.deflate ⟨.skip ⟨.operating currPos searcher'⟩,
+          by simp [hps.isPlausibleSuccessor_of_yield]⟩)
+      | ⟨.skip searcher', hps⟩ =>
+        pure (.deflate ⟨.skip ⟨.operating currPos searcher'⟩,
+          by simp [hps.isPlausibleSuccessor_of_skip]⟩)
+      | ⟨.done, _⟩ =>
         if currPos ≠ s.startPos then
           let slice := s.replaceEnd currPos
           pure (.deflate ⟨.yield ⟨.atEnd⟩ slice, by simp⟩)
         else
           pure (.deflate ⟨.done, by simp⟩)
-    | .atEnd => pure (.deflate ⟨.done, by simp⟩)
+    | ⟨.atEnd⟩ => pure (.deflate ⟨.done, by simp⟩)
+
+private def toOption : RevSplitIterator ρ s → Option (Std.Iter (α := σ s) (SearchStep s))
+  | .operating _ s => some s
+  | .atEnd => none
 
--- TODO: Finiteness after we have a notion of lawful searcher
+private def finitenessRelation [Std.Iterators.Finite (σ s) Id] :
+    Std.Iterators.FinitenessRelation (RevSplitIterator ρ s) Id where
+  rel := InvImage (Option.lt Std.Iterators.Iter.IsPlausibleSuccessorOf)
+    (RevSplitIterator.toOption ∘ Std.Iterators.IterM.internalState)
+  wf := InvImage.wf _ (Option.wellFounded_lt Std.Iterators.Finite.wf_of_id)
+  subrelation {it it'} h := by
+    simp_wf
+    obtain ⟨step, h, h'⟩ := h
+    match step with
+    | .yield it'' out | .skip it'' =>
+      obtain rfl : it' = it'' := by simpa using h.symm
+      simp only [Std.Iterators.IterM.IsPlausibleStep, Std.Iterators.Iterator.IsPlausibleStep] at h'
+      revert h'
+      match it, it' with
+      | ⟨.operating _ searcher⟩, ⟨.operating _ searcher'⟩ => simp [RevSplitIterator.toOption, Option.lt]
+      | ⟨.operating _ searcher⟩, ⟨.atEnd⟩ => simp [RevSplitIterator.toOption, Option.lt]
+      | ⟨.atEnd⟩, _ => simp
+
+@[no_expose]
+instance [Std.Iterators.Finite (σ s) Id] : Std.Iterators.Finite (RevSplitIterator ρ s) Id :=
+  .of_finitenessRelation finitenessRelation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect (RevSplitIterator ρ) m n :=
+instance [Monad m] [Monad n] : Std.Iterators.IteratorCollect (RevSplitIterator ρ s) m n :=
   .defaultImplementation
 
 instance [Monad m] [Monad n] :
-    Std.Iterators.IteratorCollectPartial (RevSplitIterator ρ) m n :=
+    Std.Iterators.IteratorCollectPartial (RevSplitIterator ρ s) m n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop (RevSplitIterator ρ) m n :=
+instance [Monad m] [Monad n] : Std.Iterators.IteratorLoop (RevSplitIterator ρ s) m n :=
   .defaultImplementation
 
-instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RevSplitIterator ρ) m n :=
+instance [Monad m] [Monad n] : Std.Iterators.IteratorLoopPartial (RevSplitIterator ρ s) m n :=
   .defaultImplementation
 
 end RevSplitIterator
@@ -500,13 +614,13 @@ This function is generic over all currently supported patterns except
 {name}`String`/{name}`String.Slice`.
 
 Examples:
- * {lean}`("coffee tea water".toSlice.revSplit Char.isWhitespace).allowNontermination.toList == ["water".toSlice, "tea".toSlice, "coffee".toSlice]`
- * {lean}`("coffee tea water".toSlice.revSplit ' ').allowNontermination.toList == ["water".toSlice, "tea".toSlice, "coffee".toSlice]`
+ * {lean}`("coffee tea water".toSlice.revSplit Char.isWhitespace).toList == ["water".toSlice, "tea".toSlice, "coffee".toSlice]`
+ * {lean}`("coffee tea water".toSlice.revSplit ' ').toList == ["water".toSlice, "tea".toSlice, "coffee".toSlice]`
 -/
 @[specialize pat]
 def revSplit [ToBackwardSearcher ρ σ] (s : Slice) (pat : ρ) :
-    Std.Iter (α := RevSplitIterator ρ) Slice :=
-  { internalState := .operating s s.endPos (ToBackwardSearcher.toSearcher s pat) }
+    Std.Iter (α := RevSplitIterator ρ s) Slice :=
+  { internalState := .operating s.endPos (ToBackwardSearcher.toSearcher s pat) }
 
 /--
 If {name}`pat` matches a suffix of {name}`s`, returns the remainder. Returns {name}`none` otherwise.
@@ -658,9 +772,7 @@ Examples:
 @[specialize pat]
 def revFind? [ToBackwardSearcher ρ σ] (s : Slice) (pat : ρ) : Option s.Pos :=
   let searcher := ToBackwardSearcher.toSearcher s pat
-  match Internal.nextMatch searcher with
-  | some (_, startPos, _) => some startPos
-  | none => none
+  searcher.findSome? (fun | .matched startPos _ => some startPos | .rejected .. => none)
 
 end BackwardPatternUsers
 
@@ -1048,9 +1160,9 @@ Creates an iterator over all lines in {name}`s` with the line ending characters
 stripped.
 
 Examples:
- * {lean}`"foo\r\nbar\n\nbaz\n".toSlice.lines.allowNontermination.toList  == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]`
- * {lean}`"foo\r\nbar\n\nbaz".toSlice.lines.allowNontermination.toList  == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]`
- * {lean}`"foo\r\nbar\n\nbaz\r".toSlice.lines.allowNontermination.toList  == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz\r".toSlice]`
+ * {lean}`"foo\r\nbar\n\nbaz\n".toSlice.lines.toList  == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]`
+ * {lean}`"foo\r\nbar\n\nbaz".toSlice.lines.toList  == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]`
+ * {lean}`"foo\r\nbar\n\nbaz\r".toSlice.lines.toList  == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz\r".toSlice]`
 -/
 def lines (s : Slice) :=
   s.splitInclusive '\n' |>.map lines.lineMap
diff --git a/tests/lean/run/string_slice.lean b/tests/lean/run/string_slice.lean
index cbca34218b10..30edfb32991a 100644
--- a/tests/lean/run/string_slice.lean
+++ b/tests/lean/run/string_slice.lean
@@ -19,16 +19,16 @@ Tests for `String.Slice` functions
 #guard "red green blue".toSlice.startsWith 'r' = true
 #guard "red green blue".toSlice.startsWith Char.isLower = true
 
-#guard ("coffee tea water".toSlice.split Char.isWhitespace).allowNontermination.toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]
-#guard ("coffee tea water".toSlice.split ' ').allowNontermination.toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]
-#guard ("coffee tea water".toSlice.split " tea ").allowNontermination.toList == ["coffee".toSlice, "water".toSlice]
-#guard ("baaab".toSlice.split "aa").allowNontermination.toList == ["b".toSlice, "ab".toSlice]
+#guard ("coffee tea water".toSlice.split Char.isWhitespace).toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]
+#guard ("coffee tea water".toSlice.split ' ').toList == ["coffee".toSlice, "tea".toSlice, "water".toSlice]
+#guard ("coffee tea water".toSlice.split " tea ").toList == ["coffee".toSlice, "water".toSlice]
+#guard ("baaab".toSlice.split "aa").toList == ["b".toSlice, "ab".toSlice]
 
-#guard ("coffee tea water".toSlice.splitInclusive Char.isWhitespace).allowNontermination.toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]
-#guard ("coffee tea water".toSlice.splitInclusive ' ').allowNontermination.toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]
-#guard ("coffee tea water".toSlice.splitInclusive " tea ").allowNontermination.toList == ["coffee tea ".toSlice, "water".toSlice]
-#guard ("a".toSlice.splitInclusive (fun (_ : Char) => true)).allowNontermination.toList == ["a".toSlice]
-#guard ("baaab".toSlice.splitInclusive "aa").allowNontermination.toList == ["baa".toSlice, "ab".toSlice]
+#guard ("coffee tea water".toSlice.splitInclusive Char.isWhitespace).toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]
+#guard ("coffee tea water".toSlice.splitInclusive ' ').toList == ["coffee ".toSlice, "tea ".toSlice, "water".toSlice]
+#guard ("coffee tea water".toSlice.splitInclusive " tea ").toList == ["coffee tea ".toSlice, "water".toSlice]
+#guard ("a".toSlice.splitInclusive (fun (_ : Char) => true)).toList == ["a".toSlice]
+#guard ("baaab".toSlice.splitInclusive "aa").toList == ["baa".toSlice, "ab".toSlice]
 
 #guard "red green blue".toSlice.drop 4 == "green blue".toSlice
 #guard "red green blue".toSlice.drop 10 == "blue".toSlice
@@ -77,6 +77,7 @@ Tests for `String.Slice` functions
 #guard "brown and orange".toSlice.all Char.isLower = false
 #guard "aaaaaa".toSlice.all 'a' = true
 #guard "aaaaaa".toSlice.all "aa" = true
+#guard "aaaaaaa".toSlice.all "aa" = false
 
 #guard "red green blue".toSlice.endsWith "blue" = true
 #guard "red green blue".toSlice.endsWith "green" = false
@@ -84,8 +85,8 @@ Tests for `String.Slice` functions
 #guard "red green blue".toSlice.endsWith 'e' = true
 #guard "red green blue".toSlice.endsWith Char.isLower = true
 
-#guard ("coffee tea water".toSlice.revSplit Char.isWhitespace).allowNontermination.toList == ["water".toSlice, "tea".toSlice, "coffee".toSlice]
-#guard ("coffee tea water".toSlice.revSplit ' ').allowNontermination.toList == ["water".toSlice, "tea".toSlice, "coffee".toSlice]
+#guard ("coffee tea water".toSlice.revSplit Char.isWhitespace).toList == ["water".toSlice, "tea".toSlice, "coffee".toSlice]
+#guard ("coffee tea water".toSlice.revSplit ' ').toList == ["water".toSlice, "tea".toSlice, "coffee".toSlice]
 
 #guard "red green blue".toSlice.dropEnd 5 == "red green".toSlice
 #guard "red green blue".toSlice.dropEnd 11 == "red".toSlice
@@ -158,9 +159,9 @@ Tests for `String.Slice` functions
 #guard "abc".toSlice.revBytes.toList = [99, 98, 97]
 #guard "ab∀c".toSlice.revBytes.toList = [99, 128, 136, 226, 98, 97]
 
-#guard "foo\r\nbar\n\nbaz\n".toSlice.lines.allowNontermination.toList  == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]
-#guard "foo\r\nbar\n\nbaz".toSlice.lines.allowNontermination.toList  == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]
-#guard "foo\r\nbar\n\nbaz\r".toSlice.lines.allowNontermination.toList  == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz\r".toSlice]
+#guard "foo\r\nbar\n\nbaz\n".toSlice.lines.toList  == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]
+#guard "foo\r\nbar\n\nbaz".toSlice.lines.toList  == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz".toSlice]
+#guard "foo\r\nbar\n\nbaz\r".toSlice.lines.toList  == ["foo".toSlice, "bar".toSlice, "".toSlice, "baz\r".toSlice]
 
 #guard "coffee tea water".toSlice.foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 2
 #guard "coffee tea and water".toSlice.foldl (fun n c => if c.isWhitespace then n + 1 else n) 0 = 3