diff --git a/Batteries/Data/Stream.lean b/Batteries/Data/Stream.lean
index fb9df787be..a1d99e57f2 100644
--- a/Batteries/Data/Stream.lean
+++ b/Batteries/Data/Stream.lean
@@ -1,93 +1,2 @@
-/-
-Copyright (c) 2024 François G. Dorais. All rights reserved.
-Released under Apache 2. license as described in the file LICENSE.
-Authors: François G. Dorais
--/
-
-namespace Stream
-
-/-- Drop up to `n` values from the stream `s`. -/
-def drop [Stream σ α] (s : σ) : Nat → σ
-  | 0 => s
-  | n+1 =>
-    match next? s with
-    | none => s
-    | some (_, s) => drop s n
-
-/-- Read up to `n` values from the stream `s` as a list from first to last. -/
-def take [Stream σ α] (s : σ) : Nat → List α × σ
-  | 0 => ([], s)
-  | n+1 =>
-    match next? s with
-    | none => ([], s)
-    | some (a, s) =>
-      match take s n with
-      | (as, s) => (a :: as, s)
-
-@[simp] theorem fst_take_zero [Stream σ α] (s : σ) :
-    (take s 0).fst = [] := rfl
-
-theorem fst_take_succ [Stream σ α] (s : σ) :
-    (take s (n+1)).fst = match next? s with
-      | none => []
-      | some (a, s) => a :: (take s n).fst := by
-  simp only [take]; split <;> rfl
-
-@[simp] theorem snd_take_eq_drop [Stream σ α] (s : σ) (n : Nat) :
-    (take s n).snd = drop s n := by
-  induction n generalizing s with
-  | zero => rfl
-  | succ n ih =>
-    simp only [take, drop]
-    split <;> simp [ih]
-
-/-- Tail recursive version of `Stream.take`. -/
-def takeTR [Stream σ α] (s : σ) (n : Nat) : List α × σ :=
-  loop s [] n
-where
-  /-- Inner loop for `Stream.takeTR`. -/
-  loop (s : σ) (acc : List α)
-    | 0 => (acc.reverse, s)
-    | n+1 => match next? s with
-      | none => (acc.reverse, s)
-      | some (a, s) => loop s (a :: acc) n
-
-theorem fst_takeTR_loop [Stream σ α] (s : σ) (acc : List α) (n : Nat) :
-    (takeTR.loop s acc n).fst = acc.reverseAux (take s n).fst := by
-  induction n generalizing acc s with
-  | zero => rfl
-  | succ n ih => simp only [take, takeTR.loop]; split; rfl; simp [ih]
-
-theorem fst_takeTR [Stream σ α] (s : σ) (n : Nat) : (takeTR s n).fst = (take s n).fst :=
-  fst_takeTR_loop ..
-
-theorem snd_takeTR_loop [Stream σ α] (s : σ) (acc : List α) (n : Nat) :
-    (takeTR.loop s acc n).snd = drop s n := by
-  induction n generalizing acc s with
-  | zero => rfl
-  | succ n ih => simp only [takeTR.loop, drop]; split; rfl; simp [ih]
-
-theorem snd_takeTR [Stream σ α] (s : σ) (n : Nat) :
-    (takeTR s n).snd = drop s n := snd_takeTR_loop ..
-
-@[csimp] theorem take_eq_takeTR : @take = @takeTR := by
-  funext; ext : 1; rw [fst_takeTR]; rw [snd_takeTR, snd_take_eq_drop]
-
-end Stream
-
-@[simp] theorem List.stream_drop_eq_drop (l : List α) : Stream.drop l n = l.drop n := by
-  induction n generalizing l with
-  | zero => rfl
-  | succ n ih =>
-    match l with
-    | [] => rfl
-    | _::_ => simp [Stream.drop, List.drop_succ_cons, ih]
-
-@[simp] theorem List.stream_take_eq_take_drop (l : List α) :
-    Stream.take l n = (l.take n, l.drop n) := by
-  induction n generalizing l with
-  | zero => rfl
-  | succ n ih =>
-    match l with
-    | [] => rfl
-    | _::_ => simp [Stream.take, ih]
+import Batteries.Data.Stream.Basic
+import Batteries.Data.Stream.Finite
diff --git a/Batteries/Data/Stream/Basic.lean b/Batteries/Data/Stream/Basic.lean
new file mode 100644
index 0000000000..b2f0475924
--- /dev/null
+++ b/Batteries/Data/Stream/Basic.lean
@@ -0,0 +1,146 @@
+/-
+Copyright (c) 2024 François G. Dorais. All rights reserved.
+Released under Apache 2. license as described in the file LICENSE.
+Authors: François G. Dorais
+-/
+
+namespace Stream
+
+/-- Drop up to `n` values from the stream `s`. -/
+def drop [Stream σ α] (s : σ) : Nat → σ
+  | 0 => s
+  | n+1 =>
+    match next? s with
+    | none => s
+    | some (_, s) => drop s n
+
+/-- Read up to `n` values from the stream `s` as a list from first to last. -/
+def take [Stream σ α] (s : σ) : Nat → List α × σ
+  | 0 => ([], s)
+  | n+1 =>
+    match next? s with
+    | none => ([], s)
+    | some (a, s) =>
+      match take s n with
+      | (as, s) => (a :: as, s)
+
+@[simp] theorem fst_take_zero [Stream σ α] (s : σ) :
+    (take s 0).fst = [] := rfl
+
+theorem fst_take_succ [Stream σ α] (s : σ) :
+    (take s (n+1)).fst = match next? s with
+      | none => []
+      | some (a, s) => a :: (take s n).fst := by
+  simp only [take]; split <;> rfl
+
+@[simp] theorem snd_take_eq_drop [Stream σ α] (s : σ) (n : Nat) :
+    (take s n).snd = drop s n := by
+  induction n generalizing s with
+  | zero => rfl
+  | succ n ih =>
+    simp only [take, drop]
+    split <;> simp [ih]
+
+/-- Tail recursive version of `Stream.take`. -/
+def takeTR [Stream σ α] (s : σ) (n : Nat) : List α × σ :=
+  loop s [] n
+where
+  /-- Inner loop for `Stream.takeTR`. -/
+  loop (s : σ) (acc : List α)
+    | 0 => (acc.reverse, s)
+    | n+1 => match next? s with
+      | none => (acc.reverse, s)
+      | some (a, s) => loop s (a :: acc) n
+
+theorem fst_takeTR_loop [Stream σ α] (s : σ) (acc : List α) (n : Nat) :
+    (takeTR.loop s acc n).fst = acc.reverseAux (take s n).fst := by
+  induction n generalizing acc s with
+  | zero => rfl
+  | succ n ih => simp only [take, takeTR.loop]; split; rfl; simp [ih]
+
+theorem fst_takeTR [Stream σ α] (s : σ) (n : Nat) : (takeTR s n).fst = (take s n).fst :=
+  fst_takeTR_loop ..
+
+theorem snd_takeTR_loop [Stream σ α] (s : σ) (acc : List α) (n : Nat) :
+    (takeTR.loop s acc n).snd = drop s n := by
+  induction n generalizing acc s with
+  | zero => rfl
+  | succ n ih => simp only [takeTR.loop, drop]; split; rfl; simp [ih]
+
+theorem snd_takeTR [Stream σ α] (s : σ) (n : Nat) :
+    (takeTR s n).snd = drop s n := snd_takeTR_loop ..
+
+@[csimp] theorem take_eq_takeTR : @take = @takeTR := by
+  funext; ext : 1; rw [fst_takeTR]; rw [snd_takeTR, snd_take_eq_drop]
+
+end Stream
+
+@[simp] theorem List.stream_drop_eq_drop (l : List α) : Stream.drop l n = l.drop n := by
+  induction n generalizing l with
+  | zero => rfl
+  | succ n ih =>
+    match l with
+    | [] => rfl
+    | _::_ => simp [Stream.drop, List.drop_succ_cons, ih]
+
+@[simp] theorem List.stream_take_eq_take_drop (l : List α) :
+    Stream.take l n = (l.take n, l.drop n) := by
+  induction n generalizing l with
+  | zero => rfl
+  | succ n ih =>
+    match l with
+    | [] => rfl
+    | _::_ => simp [Stream.take, ih]
+
+/--
+The underlying state of a stream iterator.
+-/
+structure StreamIterator (σ α) [Stream σ α] where
+  /-- Underlying stream of a stream iterator. -/
+  stream : σ
+
+/--
+Returns a pure iterator for the given stream.
+
+**Termination properties:**
+
+* `Finite` instance: maybe available
+* `Productive` instance: always
+-/
+@[always_inline, inline]
+def Stream.iter [Stream σ α] (stream : σ) : Std.Iterators.Iter (α := StreamIterator σ α) α :=
+  Std.Iterators.toIterM { stream } Id α |>.toIter
+
+@[always_inline, inline]
+instance (σ α) [Stream σ α] : Std.Iterators.Iterator (StreamIterator σ α) Id α where
+  IsPlausibleStep it
+    | .yield it' _ =>
+      ∃ x, Stream.next? it.internalState.stream = some (x, it'.internalState.stream)
+    | .skip _ => False
+    | .done => Stream.next? it.internalState.stream = none
+  step it :=
+    match Stream.next? it.internalState.stream with
+    | some (out, stream) => .yield ⟨⟨stream⟩⟩ out ⟨out, rfl⟩
+    | none => .done rfl
+
+private def StreamIterator.instProductivenessRelation [Stream σ α] :
+    Std.Iterators.ProductivenessRelation (StreamIterator σ α) Id where
+  rel := emptyWf.rel
+  wf := emptyWf.wf
+  subrelation h := by cases h
+
+instance StreamIterator.instProductive [Stream σ α] :
+    Std.Iterators.Productive (StreamIterator σ α) Id :=
+  Std.Iterators.Productive.of_productivenessRelation StreamIterator.instProductivenessRelation
+
+instance StreamIterator.instIteratorLoop [Stream σ α] [Monad n] :
+    Std.Iterators.IteratorLoop (StreamIterator σ α) Id n := .defaultImplementation
+
+instance StreamIterator.instIteratorLoopPartial [Stream σ α] [Monad n] :
+    Std.Iterators.IteratorLoopPartial (StreamIterator σ α) Id n := .defaultImplementation
+
+instance StreamIterator.instIteratorCollect [Stream σ α] [Monad n] :
+    Std.Iterators.IteratorCollect (StreamIterator σ α) Id n := .defaultImplementation
+
+instance StreamIterator.instIteratorCollectPartial [Stream σ α] [Monad n] :
+    Std.Iterators.IteratorCollectPartial (StreamIterator σ α) Id n := .defaultImplementation
diff --git a/Batteries/Data/Stream/Finite.lean b/Batteries/Data/Stream/Finite.lean
new file mode 100644
index 0000000000..6e661a8e56
--- /dev/null
+++ b/Batteries/Data/Stream/Finite.lean
@@ -0,0 +1,431 @@
+/-
+Copyright (c) 2025 François G. Dorais. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: François G. Dorais
+-/
+import Batteries.Data.Stream.Basic
+import Batteries.Data.ByteSubarray
+import Batteries.Tactic.Basic
+import Batteries.WF
+
+/-! # Finite and Well-Founded Streams
+
+This file defines two main classes:
+
+- `Stream.Finite` provides a proof that a specific stream is finite.
+- `Stream.WellFounded` extends the `Stream` class and provides an instance of `Stream.Finite` for
+  every stream of the given type.
+
+The importance of these classes is that iterating along a finite stream is guaranteed to terminate.
+Therefore, it is possible to prove facts about such iterations.
+
+The `Stream.WellFounded` class is easiest to use: match on `Stream.next?` and provide a termination
+hint. The general pattern is this:
+```
+def foo [Stream.WellFounded σ α] (s : σ) : β :=
+  match _hint : Stream.next? s with
+  | none => _
+  | some (x, t) => _
+termination_by s
+```
+(The underscore in `_hint` is only to avoid the unused variable linter from complaining.)
+
+The `Stream.Finite` class is more general but is slightly trickier to use.
+```
+def foo [Stream σ α] (s : σ) [Stream.Finite s] : β :=
+  match hint : Stream.next? s with
+  | none => _
+  | some (x, t) =>
+    have : Stream.Finite t := .ofSome hint
+    _
+termination_by Stream.Finite.wrap s
+```
+Several examples of this pattern can be found below. We hope to avoid the need for the extra `have`
+at some point in the future.
+
+## Constructing `Stream.WellFounded` Classes
+
+TODO
+
+## Constructing `Stream.Finite` Classes
+
+TODO
+
+-/
+
+namespace Stream
+
+/-- Class to define the next relation of a stream type. -/
+class WithNextRelation (σ : Type _) (α : outParam <| Type _) extends Stream σ α where
+  /-- Next relation for a stream type `σ`. -/
+  rel : σ → σ → Prop -- this is named `rel` to match `WellFoundedRelatiom`
+  /-- Next relation extends the default. -/
+  rel_of_next?_eq_some : next? s = some (x, t) → rel t s
+
+/-- Default next relation for a stream type. -/
+instance (priority := low) defaultNextRelation (σ) [Stream σ α] : WithNextRelation σ α where
+  rel t s := ∃ x, next? s = some (x, t)
+  rel_of_next?_eq_some h := ⟨_, h⟩
+
+/-- Next relation for a stream. -/
+abbrev Next [WithNextRelation σ α] : σ → σ → Prop := WithNextRelation.rel
+
+/-- Next relation, restricted to a subset of streams. -/
+abbrev RestrictedNext [WithNextRelation σ α] (p : σ → Prop) (s t : σ) : Prop :=
+  p t ∧ Next s t
+
+theorem next_of_next?_eq_some [WithNextRelation σ α] {s t : σ} :
+    next? s = some (x, t) → Next t s := WithNextRelation.rel_of_next?_eq_some
+
+/-- Class for well-founded stream type. -/
+protected class WellFounded.{u,v} (σ : Type u) (α : outParam <| Type v) extends
+  WithNextRelation σ α, WellFoundedRelation σ
+
+/-- Define a well-founded stream type instance from a well-founded relation. -/
+def WellFounded.ofRelation.{u,v} [Stream.{u,v} σ α] [inst : WellFoundedRelation σ]
+    (h : {s t : σ} → {x : α} → next? s = (x, t) → WellFoundedRelation.rel t s) :
+    Stream.WellFounded σ α := { inst with rel_of_next?_eq_some := h }
+
+/-- Define a well-founded stream type instance from a measure. -/
+def WellFounded.ofMeasure.{u,v} [Stream.{u,v} σ α] (f : σ → Nat)
+    (h : {s t : σ} → {x : α} → next? s = (x, t) → f t < f s) :
+    Stream.WellFounded σ α := { measure f with rel_of_next?_eq_some := h }
+
+macro_rules
+| `(tactic| decreasing_trivial) => `(tactic| apply Stream.next_of_next?_eq_some; assumption)
+
+instance (α) : Stream.WellFounded (List α) α :=
+  .ofMeasure List.length <| by
+    intro _ _ _ h
+    simp only [next?] at h
+    split at h
+    · contradiction
+    · cases h; simp
+
+instance : Stream.WellFounded Substring Char :=
+  .ofMeasure Substring.bsize <| by
+    intro _ _ _ h
+    simp only [next?] at h
+    split at h
+    · next hlt =>
+      cases h
+      simp only [Substring.bsize, String.next, String.pos_add_char, Nat.sub_eq]
+      apply Nat.sub_lt_sub_left hlt
+      apply Nat.lt_add_of_pos_right
+      exact Char.utf8Size_pos _
+    · contradiction
+
+instance (α) : Stream.WellFounded (Subarray α) α :=
+  .ofMeasure Subarray.size <| by
+    intro _ _ _ h
+    simp only [next?] at h
+    split at h
+    · cases h
+      simp only [Subarray.size, Subarray.stop, Subarray.start]
+      apply Nat.sub_one_lt
+      apply Nat.sub_ne_zero_of_lt
+      assumption
+    · contradiction
+
+instance : Stream.WellFounded Batteries.ByteSubarray UInt8 :=
+  .ofMeasure Batteries.ByteSubarray.size <| by
+    intro _ _ _ h
+    simp only [next?, bind, Option.bind] at h
+    split at h
+    · contradiction
+    · next heq =>
+      rw [getElem?_def] at heq
+      split at heq
+      · next hpos =>
+        cases h
+        simp only [Batteries.ByteSubarray.size, Batteries.ByteSubarray.popFront] at hpos ⊢
+        split
+        · next heq =>
+          simp [heq] at hpos
+        · simp
+          apply Nat.sub_one_lt
+          exact Nat.ne_zero_of_lt hpos
+      · contradiction
+      done
+
+instance : Stream.WellFounded Std.Range Nat :=
+  .ofMeasure (fun r => r.stop - r.start) <| by
+    intro _ _ _ h
+    simp only [next?] at h
+    split at h
+    · next hlt =>
+      cases h
+      apply Nat.sub_lt_sub_left hlt
+      apply Nat.lt_add_of_pos_right
+      exact Std.Range.step_pos _
+    · contradiction
+
+section iterator_interfaces
+open Std.Iterators
+
+private theorem IsPlausibleSuccessorOf_eq (σ α) [Stream σ α] :
+    IterM.IsPlausibleSuccessorOf (m := Id) (α := StreamIterator σ α) =
+      InvImage (fun s s' : σ => ∃ x, next? s' = some (x, s)) (·.internalState.stream) := by
+  funext i₁ i₂
+  simp only [IterM.IsPlausibleSuccessorOf, IterM.IsPlausibleStep, InvImage, eq_iff_iff]
+  constructor
+  · intro
+    | ⟨.yield i x, heq, h⟩ =>
+      cases heq
+      exact h
+  · intro ⟨x, h⟩
+    exact ⟨.yield i₁ x, rfl, ⟨x, h⟩⟩
+
+instance (σ α) [wf : Stream.WellFounded σ α] : Finite (α := StreamIterator σ α) Id where
+  wf := by
+    rw [IsPlausibleSuccessorOf_eq]
+    refine InvImage.wf _ ?_
+    refine Subrelation.wf ?_ wf.wf
+    intro _ _ ⟨_, h⟩
+    exact next_of_next?_eq_some h
+
+private theorem finite_rel_of_isPlausible0thOutputStep [Iterator α m β] [Productive α m]
+    {s t : IterM (α := α) m β}
+    (h : ∃ v, IterM.IsPlausibleNthOutputStep 0 s (IterStep.yield t v)) :
+    IterM.TerminationMeasures.Finite.Rel ⟨t⟩ ⟨s⟩ := by
+  match h with
+  | ⟨_, .zero_yield h⟩ =>
+    exact IterM.TerminationMeasures.Finite.rel_of_yield h
+  | ⟨v, .skip hs h⟩ =>
+    apply Relation.TransGen.trans
+    exact finite_rel_of_isPlausible0thOutputStep ⟨v, h⟩
+    exact IterM.TerminationMeasures.Finite.rel_of_skip hs
+termination_by s.finitelyManySkips
+
+instance [Iterator α Id β] [Std.Iterators.Finite α Id] [IteratorAccess α Id] :
+    Stream.WellFounded (Iter (α := α) β) β where
+  rel t s := ∃ v, IterM.IsPlausibleNthOutputStep 0 s.toIterM (IterStep.yield t.toIterM v)
+  wf := by
+    apply Subrelation.wf finite_rel_of_isPlausible0thOutputStep
+    apply InvImage.wf
+    apply WellFoundedRelation.wf
+  rel_of_next?_eq_some := by
+    intros _ v _ hnext
+    simp only [next?] at hnext
+    split at hnext
+    · cases hnext
+      exists v
+    · next h _ =>
+      absurd h
+      exact IterM.not_isPlausibleNthOutputStep_yield
+    · cases hnext
+
+end iterator_interfaces
+
+/-- Class for a finite stream of type `σ`. -/
+protected class Finite [WithNextRelation σ α] (s : σ) : Prop where
+  /-- A finite stream is accessible with respect to the `Next` relation. -/
+  acc : Acc Next s
+
+instance [Stream.WellFounded σ α] (s : σ) : Stream.Finite s where
+  acc := match WellFounded.wf (σ := σ) with | ⟨h⟩ => h s
+
+namespace Finite
+
+/-- Predecessor of a finite stream is finite. -/
+theorem ofNext [WithNextRelation σ α] {s t : σ} [Stream.Finite s] (h : Next t s) :
+    Stream.Finite t where
+  acc := match acc (s := s) with | ⟨_, a⟩ => a _ h
+
+/-- Predecessor of a finite stream is finite. -/
+theorem ofSome [WithNextRelation σ α] {s t : σ} [Stream.Finite s]
+    (h : next? s = some (x, t)) : Stream.Finite t := .ofNext <| next_of_next?_eq_some h
+
+/-- Define a finite stream instance for a restricted subset of streams. -/
+theorem ofRestrictedNext.{u,v} [WithNextRelation.{u,v} σ α] {p : σ → Prop}
+    (H : ∀ {s t}, Next s t → p t → p s) (h : p s) (acc : Acc (RestrictedNext p) s) :
+    Stream.Finite s where
+  acc :=
+    Subrelation.accessible (fun h₁ h₂ => ⟨H h₁ h₂, h₂, h₁⟩) (Acc.restriction p acc h)
+
+/-- Wrap a finite stream into a well-founded type for use in termination proofs. -/
+def wrap [WithNextRelation σ α] (s : σ) [Stream.Finite s] : { s : σ // Acc Next s } :=
+  ⟨s, Finite.acc⟩
+
+end Finite
+
+/-- Folds a monadic function over a finite stream from left to right. -/
+@[inline, specialize]
+def foldlM [Monad m] [WithNextRelation σ α] (s : σ) [Stream.Finite s] (f : β → α → m β)
+    (init : β) : m β :=
+  match h : next? s with
+  | none => pure init
+  | some (x, t) =>
+    have : Stream.Finite t := .ofSome h
+    f init x >>= foldlM t f
+termination_by Finite.wrap s
+
+theorem foldlM_none [Monad m] [WithNextRelation σ α] {s : σ} [Stream.Finite s]
+    {f : β → α → m β} (h : next? s = none) : foldlM s f init = pure init := by
+  simp only [foldlM]
+  split <;> simp_all
+
+theorem foldlM_some [Monad m] [WithNextRelation σ α] {s t : σ} [Stream.Finite s] [Stream.Finite t]
+    {f : β → α → m β} (h : next? s = some (x, t)) : foldlM s f init = f init x >>= foldlM t f := by
+  simp only [foldlM]
+  split
+  · simp_all
+  · next heq =>
+    simp only [h, Option.some.injEq, Prod.mk.injEq] at heq
+    cases heq.1; cases heq.2; rfl
+
+/-- Folds a monadic function over a finite stream from right to left. -/
+@[specialize]
+def foldrM [Monad m] [WithNextRelation σ α] (s : σ) [Stream.Finite s] (f : α → β → m β)
+    (init : β) : m β :=
+  match h : next? s with
+  | none => pure init
+  | some (x, t) =>
+    have : Stream.Finite t := .ofSome h
+    foldrM t f init >>= f x
+termination_by Finite.wrap s
+
+theorem foldrM_none [Monad m] [WithNextRelation σ α] {s : σ} [Stream.Finite s]
+    {f : α → β → m β} (h : next? s = none) : foldrM s f init = pure init := by
+  rw [foldrM]; split <;> simp_all
+
+theorem foldrM_some [Monad m] [WithNextRelation σ α] {s t : σ} [Stream.Finite s] [Stream.Finite t]
+    {f : α → β → m β} (h : next? s = some (x, t)) : foldrM s f init = foldrM t f init >>= f x := by
+  rw [foldrM]; split <;> simp_all
+
+/-- Folds a function over a finite stream from left to right. -/
+@[specialize]
+def foldl [WithNextRelation σ α] (s : σ) [Stream.Finite s] (f : β → α → β) (init : β) : β :=
+  match h : next? s with
+  | none => init
+  | some (x, t) =>
+    have : Stream.Finite t := .ofSome h
+    foldl t f (f init x)
+termination_by Finite.wrap s
+
+theorem foldl_none [WithNextRelation σ α] {s : σ} [Stream.Finite s] {f : β → α → β}
+    (h : next? s = none) : foldl s f init = init := by
+  rw [foldl]; split <;> simp_all
+
+theorem foldl_some [WithNextRelation σ α] {s t : σ} [Stream.Finite s] [Stream.Finite t]
+    {f : β → α → β} (h : next? s = some (x, t)) : foldl s f init = foldl t f (f init x) := by
+  rw [foldl]; split <;> simp_all
+
+/-- Folds a function over a finite stream from right to left. -/
+@[specialize]
+def foldr [WithNextRelation σ α] (s : σ) [Stream.Finite s] (f : α → β → β) (init : β) : β :=
+  match h : next? s with
+  | none => init
+  | some (x, t) =>
+    have : Stream.Finite t := .ofSome h
+    f x <| foldr t f init
+termination_by Finite.wrap s
+
+theorem foldr_none [WithNextRelation σ α] {s : σ} [Stream.Finite s]
+    {f : α → β → β} (h : next? s = none) : foldr s f init = init := by
+  rw [foldr]
+  split <;> simp_all
+
+theorem foldr_some [WithNextRelation σ α] {s t : σ} [Stream.Finite s] [Stream.Finite t]
+    {f : α → β → β} (h : next? s = some (x, t)) : foldr s f init = f x (foldr t f init) := by
+  rw [foldr]
+  split <;> simp_all
+
+/-- Extract the length of a finite stream. -/
+@[inline]
+def length [WithNextRelation σ α] (s : σ) [Stream.Finite s] : Nat :=
+  foldl s (fun l _ => l + 1) 0
+
+theorem length_none [WithNextRelation σ α] {s : σ} [Stream.Finite s]
+    (h : next? s = none) : length s = 0 := foldl_none h
+
+private theorem length_aux [WithNextRelation σ α] {s : σ} [Stream.Finite s] :
+    foldl s (fun l _ => l + 1) n = foldl s (fun l _ => l + 1) 0 + n := by
+  match h : next? s with
+  | none => simp [foldl_none h]
+  | some (x, t) =>
+    have : Stream.Finite t := .ofSome h
+    conv => lhs; rw [foldl_some h, length_aux]
+    conv => rhs; rw [foldl_some h, length_aux]
+    simp +arith
+termination_by Finite.wrap s
+
+theorem length_some [WithNextRelation σ α] {s t : σ} [Stream.Finite s] [Stream.Finite t]
+    (h : next? s = some (x, t)) : length s = length t + 1 := by
+  simp [length, foldl_some h, length_aux (n := 1)]
+
+/-- Extract the sequence of values of a finite stream as a `List` in reverse order. -/
+@[inline]
+def toListRev [WithNextRelation σ α] (s : σ) [Stream.Finite s] : List α :=
+  foldl s (fun r x => x :: r) []
+
+theorem toListRev_none [WithNextRelation σ α] {s : σ} [Stream.Finite s]
+    (h : next? s = none) : toListRev s = [] := by
+  simp [toListRev, foldl_none h]
+
+private theorem toListRev_aux [WithNextRelation σ α] {s : σ} [Stream.Finite s] :
+    foldl s (fun r x => x :: r) l = foldl s (fun r x => x :: r) [] ++ l := by
+  match h : next? s with
+  | none => simp [foldl_none h]
+  | some (x, t) =>
+    have : Stream.Finite t := .ofSome h
+    conv => lhs; rw [foldl_some h, toListRev_aux]
+    conv => rhs; rw [foldl_some h, toListRev_aux]
+    simp
+termination_by Finite.wrap s
+
+theorem toListRev_some [WithNextRelation σ α] {s t : σ} [Stream.Finite s] [Stream.Finite t]
+    (h : next? s = some (x, t)) : toListRev s = toListRev t ++ [x] := by
+  simp [toListRev, foldl_some h, toListRev_aux (l := [x])]
+
+/-- Extract the sequence of values of a finite stream as a `List`. -/
+@[inline]
+def toList [WithNextRelation σ α] (s : σ) [Stream.Finite s] : List α :=
+  toListRev s |>.reverse
+
+theorem toList_none [WithNextRelation σ α] {s : σ} [Stream.Finite s]
+    (h : next? s = none) : toList s = [] := by
+  simp [toList, toListRev_none h]
+
+theorem toList_some [WithNextRelation σ α] {s t : σ} [Stream.Finite s] [Stream.Finite t]
+    (h : next? s = some (x, t)) : toList s = x :: toList t := by
+  simp [toList, toListRev_some h]
+
+/-- Extract the sequence of values of a finite stream as an `Array`. -/
+@[inline]
+def toArray [WithNextRelation σ α] (s : σ) [Stream.Finite s] : Array α :=
+  foldl s Array.push #[]
+
+theorem toArray_none [WithNextRelation σ α] {s : σ} [Stream.Finite s]
+    (h : next? s = none) : toArray s = #[] := by
+  simp [toArray, foldl_none h]
+
+private theorem toArray_aux [WithNextRelation σ α] {s : σ} [Stream.Finite s] :
+    foldl s Array.push l = l ++ foldl s Array.push #[] := by
+  match h : next? s with
+  | none => simp [foldl_none h]
+  | some (x, t) =>
+    have : Stream.Finite t := .ofSome h
+    conv => lhs; rw [foldl_some h, toArray_aux]
+    conv => rhs; rw [foldl_some h, toArray_aux]
+    simp
+termination_by Finite.wrap s
+
+theorem toArray_some [WithNextRelation σ α] {s t : σ} [Stream.Finite s] [Stream.Finite t]
+    (h : next? s = some (x, t)) : toArray s = #[x] ++ toArray t := by
+  simp [toArray, foldl_some h, toArray_aux (l := #[x])]
+
+theorem toArray_toList_eq_toArray [WithNextRelation σ α] {s : σ} [Stream.Finite s] :
+    (toList s).toArray = toArray s := by
+  match h : next? s with
+  | none => simp [toList_none h, toArray_none h]
+  | some (x, t) =>
+    have : Stream.Finite t := .ofSome h
+    simp only [toList_some h, toArray_some h]
+    rw [List.toArray_cons, toArray_toList_eq_toArray]
+termination_by Finite.wrap s
+
+@[simp] theorem toList_eq_self (l : List α) : toList l = l := by
+  induction l with
+  | nil => rw [toList_none rfl]
+  | cons x l ih => rw [toList_some rfl, ih]
diff --git a/Batteries/WF.lean b/Batteries/WF.lean
index a510a8d9de..45f24f1493 100644
--- a/Batteries/WF.lean
+++ b/Batteries/WF.lean
@@ -86,6 +86,13 @@ private theorem recC_intro {motive : (a : α) → Acc r a → Sort v}
   funext α r motive intro a t
   rw [Acc.ndrecOn, rec_eq_recC, Acc.ndrecOnC]
 
+/-- Introduces a predicate `p` into an accessibility relation, provided that it holds of the
+initial point. -/
+theorem restriction (p : α → Prop) {r : α → α → Prop} {a : α}
+    (acc : Acc r a) (h : p a) : Acc (fun x y => p y → p x ∧ r x y) a := by
+  induction acc with
+  | intro x _ ih => exact ⟨_, fun y hr => ih y (hr h).2 (hr h).1⟩
+
 end Acc
 
 namespace WellFounded
diff --git a/BatteriesTest/stream_finite.lean b/BatteriesTest/stream_finite.lean
new file mode 100644
index 0000000000..941a4c81eb
--- /dev/null
+++ b/BatteriesTest/stream_finite.lean
@@ -0,0 +1,50 @@
+import Batteries.Data.Stream.Finite
+
+/- Example of a stream type which is not well-founded but has many derivable finite instances. -/
+structure Test where
+  decr : Bool
+  val : Nat
+  deriving Repr
+
+instance : Stream Test Nat where
+  next? s :=
+    if ¬ s.decr then
+      some (s.val, {s with val := s.val+1})
+    else if s.val ≠ 0 then
+      some (s.val-1, {s with val := s.val-1})
+    else
+      none
+
+instance : Stream.WithNextRelation Test Nat where
+  rel s t := t.decr → s.decr ∧ s.val < t.val
+  rel_of_next?_eq_some := by
+    intro _ _ _ h
+    simp [Stream.next?] at h
+    split at h
+    · cases h
+      simp [*]
+    · split at h
+      · contradiction
+      · next h0 =>
+        intro h'
+        cases h
+        constructor
+        · exact h'
+        · exact Nat.sub_one_lt h0
+
+instance : Stream.Finite (Test.mk true n) :=
+  have wf : WellFounded (Stream.RestrictedNext (Test.decr ·)) :=
+    Subrelation.wf (fun h => (h.2 h.1).2) (measure Test.val).wf
+  Stream.Finite.ofRestrictedNext (p := (Test.decr ·))
+    (fun h h' => (h h').1) rfl (wf.apply _)
+
+#guard Stream.toList (Test.mk true 3) == [2, 1, 0]
+
+/--
+error: failed to synthesize
+  Stream.Finite { decr := false, val := 3 }
+
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+-/
+#guard_msgs in
+#eval Stream.toList (Test.mk false 3)