diff --git a/Cslib/Computability/Machines/RTM/PB.lean b/Cslib/Computability/Machines/RTM/PB.lean
index 37e3f12fa0..d5cdfc7e67 100644
--- a/Cslib/Computability/Machines/RTM/PB.lean
+++ b/Cslib/Computability/Machines/RTM/PB.lean
@@ -114,6 +114,23 @@ This allows statements that `PB`s compute functions on lean datatypes. -/
 def ComputesEnc {α : Type} [DataEncode α] (env : List Value) (impl : PB) (x : α) :=
   Computes env impl (.data (DataEncode.encode x))
 
+def ComputesFunEnc {α β : Type} [DataEncode α] [DataEncode β]
+    (p : PB → PB) (φ : α → β) : Prop :=
+  ∀ (env : List Value) (a : PB) (x : α), a.ComputesEnc env x → (p a).ComputesEnc env (φ x)
+
+structure RTMFun (α : Type) [DataEncode α] where
+  φ : Data → α
+  impl : PB → PB
+  h_impl : ComputesFunEnc impl φ
+
+structure RTMFun' (α : Type) [DataEncode α] where
+  φ : (List Value) → α
+  impl : PB
+  h_impl : ∀ env, ∃ t s, ProgSem env (impl env.length) (.data (DataEncode.encode (φ env))) t s
+
+def RTMFun'.var (i : ℕ) : RTMFun' Value :=
+  ⟨fun env => env[i]?.getD Value.empty, PB.var i, sorry⟩
+
 /-- Var-lookup: `PB.var i` reads the `i`-th entry of the environment. -/
 @[simp]
 lemma var_computes {i : ℕ} (h : i < env.length) :
@@ -320,6 +337,96 @@ lemma app_fn_computes {body : PB → PB} {arg : PB} {dx out : Value}
     rw [hmap]; exact hb
   exact ⟨_, _, ProgSem.app ProgSem.fn ha (AppSem.mk hb')⟩
 
+/-- Lift `PB.elim` into `RTMFun`. The scrutinee `v` produces a list-shaped `Data`; on the empty
+list the `em` branch runs, and on a `head :: tail` the cons branch `cs` is run with `head` and
+`tail` supplied as `RTMFun`s over the same input (computed by projecting from `v`). Both the
+program and the correctness proof are derived. -/
+def RTMFun.elim (v em : RTMFun Data) (cs : RTMFun Data → RTMFun Data → RTMFun Data) :
+    RTMFun Data :=
+  let hd : RTMFun Data :=
+    ⟨fun d => (v.φ d).asList.headD .empty,
+     fun a => PB.elim (v.impl a) PB.empty (fun h _ => h),
+     by
+       intro env a d h
+       have hv := v.h_impl env a d h
+       simp only [ComputesEnc, DataEncode.encode] at hv ⊢
+       cases hvd : v.φ d with
+       | l xs =>
+         cases xs with
+         | nil =>
+           rw [hvd] at hv
+           exact elim_nil_computes hv empty_computes
+         | cons hd0 tl0 =>
+           rw [hvd] at hv
+           exact elim_cons_computes hv
+             (computesFun₂_branch (fun ext => var_computes_fresh ext [.data (Data.l tl0)]))⟩
+  let tl : RTMFun Data :=
+    ⟨fun d => Data.l (v.φ d).asList.tail,
+     fun a => PB.elim (v.impl a) PB.empty (fun _ t => t),
+     by
+       intro env a d h
+       have hv := v.h_impl env a d h
+       simp only [ComputesEnc, DataEncode.encode] at hv ⊢
+       cases hvd : v.φ d with
+       | l xs =>
+         cases xs with
+         | nil =>
+           rw [hvd] at hv
+           exact elim_nil_computes hv empty_computes
+         | cons hd0 tl0 =>
+           rw [hvd] at hv
+           exact elim_cons_computes hv
+             (computesFun₂_branch2 (body := fun _ t => t)
+               (fun ext => var_computes_fresh' ext (binds := [.data hd0, .data (Data.l tl0)])
+                 (j := 1) (by simp)))⟩
+  ⟨fun d => match v.φ d with
+    | Data.l [] => em.φ d
+    | Data.l (_ :: _) => (cs hd tl).φ d,
+   fun a => PB.elim (v.impl a) (em.impl a) (fun _ _ => (cs hd tl).impl a),
+   by
+     intro env a d h
+     have hv := v.h_impl env a d h
+     simp only [ComputesEnc, DataEncode.encode] at hv ⊢
+     cases hvd : v.φ d with
+     | l xs =>
+       cases xs with
+       | nil =>
+         rw [hvd] at hv
+         exact elim_nil_computes hv (em.h_impl env a d h)
+       | cons hd0 tl0 =>
+         rw [hvd] at hv
+         exact elim_cons_computes hv
+           (computesFun₂_const ((cs hd tl).h_impl env a d h))⟩
+
+def RTMFun'.cons (hd tl : RTMFun' Data) :
+    RTMFun' Data :=
+  ⟨fun env => Data.l (hd.φ env :: (tl.φ env).asList),
+  PB.cons hd.impl tl.impl, sorry ⟩
+
+
+def RTMFun'.elim (v em : RTMFun' Data) (cs : RTMFun' Data → RTMFun' Data → RTMFun' Data) :
+    RTMFun' Data :=
+  ⟨fun env => match v.φ env with
+    | Data.l [] => em.φ env
+    | Data.l (hd :: tl) =>
+      (cs (.var (env.length)) (.var (env.length + 1))).φ (env ++ [Value.data hd, Value.data (Data.l tl)]),
+   fun a => PB.elim (v.impl a) (em.impl a) (fun h t => (cs ⟨fun _ => h, sorry⟩ ⟨fun _ => t, sorry⟩).impl a),
+   by
+     intro env a d h
+     have hv := v.h_impl env a d h
+     simp only [ComputesEnc, DataEncode.encode] at hv ⊢
+     cases hvd : v.φ env with
+     | l xs =>
+       cases xs with
+       | nil =>
+         rw [hvd] at hv
+         exact elim_nil_computes hv (em.h_impl env a d h)
+       | cons hd0 tl0 =>
+         rw [hvd] at hv
+         exact elim_cons_computes hv
+           (computesFun₂_const ((cs ⟨fun _ => hd0, sorry⟩ ⟨fun _ => Data.l tl0, sorry⟩).h_impl env a d h))⟩
+
+
 /-- Resource-erased iteration of a `while_` loop body. `WhileComputes env body acc r` says that,
 under any outer extension `ext`, repeatedly applying the loop-body closure (the closure produced by
 `while_ _ body` at the current depth) starting from accumulator `acc` eventually yields `r`.
diff --git a/Cslib/Computability/Machines/RTM/Prog.lean b/Cslib/Computability/Machines/RTM/Prog.lean
index 53db589151..18ed690583 100644
--- a/Cslib/Computability/Machines/RTM/Prog.lean
+++ b/Cslib/Computability/Machines/RTM/Prog.lean
@@ -86,6 +86,12 @@ lemma Value.size_pos {v : Value} : 0 < v.size := by
   | data d => simp only [Value.size]; exact Data.size_le
   | closure _ env => simp only [Value.size]; omega
 
+instance : DataEncode Value where
+  encode
+    | .data d => sorry
+    | .closure body env => sorry
+  h_inj := sorry
+
 mutual
 /-- Semantics of `Prog` including time and space resource bounds.
 `ProgSem σ p x t s` means that on environment `σ`, the program `p` evaluates to the value
diff --git a/Cslib/Computability/Machines/RTM/TMSimulator.lean b/Cslib/Computability/Machines/RTM/TMSimulator.lean
index 89bf7d04ef..2dcc6e0e57 100644
--- a/Cslib/Computability/Machines/RTM/TMSimulator.lean
+++ b/Cslib/Computability/Machines/RTM/TMSimulator.lean
@@ -100,6 +100,42 @@ lemma stackTapeCons_computes
     apply PB.optionElim_computesEnc_some h_x
       (PB.computesFun₂_const (PB.cons_computes h_x h_st))
 
+/-! ### Proof-of-concept: `stackTapeCons` rebuilt from the composable `RTMFun` combinators
+
+The block below demonstrates the `RTMFun` combinator library (`Tools.lean`). `stackTapeConsF` is the
+applicative-style combinator: it takes the head and tail transformers (over an arbitrary ambient
+input `I`) and produces the consed list, mirroring the direct `PB.optionElim`/`PB.elim`/`PB.cons`
+version. The program and its correctness proof are *derived*; only a small bridge from the derived
+list-valued `φ` to `StackTape.cons` is proven by hand (`stackTapeConsF_φ`). -/
+
+/-- A `StackTape` is encoded exactly as its `toList`, so the identity program retyped at
+`List (Option Symbol)` computes `StackTape.toList`. -/
+def toListF : PB.RTMFun (α := StackTape Symbol) (β := List (Option Symbol)) :=
+  ⟨StackTape.toList, id, fun _ _ _ h => h⟩
+
+open scoped PB in
+/-- `stackTapeCons` in applicative style: a combinator over an ambient input `I` taking the head
+transformer `x` and tail transformer `st`. The body mirrors the direct `PB.optionElim`/`PB.elim`/
+`PB.cons` version almost verbatim; both the program and the correctness proof are derived. -/
+def stackTapeConsF {I : Type} [DataEncode I]
+    (x : PB.RTMFun (α := I) (β := Option Symbol))
+    (st : PB.RTMFun (α := I) (β := StackTape Symbol)) :
+    PB.RTMFun (α := I) (β := List (Option Symbol)) :=
+  let stl := st >>> toListF
+  PB.RTMFun.optionElimC x
+    (PB.RTMFun.elimC stl PB.RTMFun.emptyF (PB.RTMFun.consF x stl))
+    (PB.RTMFun.consF x stl)
+
+/-- Bridge: the derived `φ` of `stackTapeConsF` computes `StackTape.cons` pointwise. -/
+lemma stackTapeConsF_φ {I : Type} [DataEncode I]
+    (x : PB.RTMFun (α := I) (β := Option Symbol))
+    (st : PB.RTMFun (α := I) (β := StackTape Symbol)) (i : I) :
+    (stackTapeConsF x st).φ i = (StackTape.cons (x.φ i) (st.φ i)).toList := by
+  simp only [stackTapeConsF, PB.RTMFun.optionElimC, PB.RTMFun.elimC, PB.RTMFun.consF,
+    PB.RTMFun.comp, toListF, Function.comp]
+  obtain ⟨l, hl⟩ := st.φ i
+  cases x.φ i <;> cases l <;> rfl --simp [StackTape.cons]
+
 --- The head component of the bitape
 def bitapeHead (t : PB) : PB := t.fst
 --- The left component of the bitape
diff --git a/Cslib/Computability/Machines/RTM/Tools.lean b/Cslib/Computability/Machines/RTM/Tools.lean
index b3df4ffc48..7c4f236817 100644
--- a/Cslib/Computability/Machines/RTM/Tools.lean
+++ b/Cslib/Computability/Machines/RTM/Tools.lean
@@ -82,6 +82,10 @@ lemma fst_ComputesEnc {x : PB} {a : α × β} (hx : x.ComputesEnc env a) :
   obtain ⟨a, b⟩ := a
   apply PB.head_computes hx
 
+def fst' (p : RTMFun (α × β)) : RTMFun α :=
+  ⟨fun d => (p.φ d).fst, fun a => head (p.impl a), fun env a d h_x =>
+    PB.head_computes (p.h_impl env a d h_x)⟩
+
 /-- Second projection (`head` of `tail`). -/
 def snd (x : PB) : PB := head (PB.tail x)
 
@@ -90,6 +94,10 @@ lemma snd_ComputesEnc {x : PB} {a : α × β} (hx : x.ComputesEnc env a) :
   obtain ⟨a, b⟩ := a
   apply PB.head_computes (PB.tail_computes hx)
 
+def snd' (p : RTMFun (α × β)) : RTMFun β :=
+  ⟨fun d => (p.φ d).snd, fun x => (p.impl x).tail.head,
+    fun env a d h_x => PB.head_computes (PB.tail_computes (p.h_impl env a d h_x))⟩
+
 /-- `Option.some` as a singleton list. -/
 def some (x : PB) : PB := cons x empty
 
@@ -101,6 +109,26 @@ lemma some_ComputesEnc {x : PB} {a : α} (hx : x.ComputesEnc env a) :
 def optionElim (x noneCase : PB) (someCase : PB → PB) : PB :=
   elim x noneCase (fun v _ => someCase v)
 
+def optionElim' (x : RTMFun (Option α)) (noneCase : RTMFun β) (someCase : RTMFun α → RTMFun β) :
+    RTMFun β :=
+  ⟨fun d => match x.φ d with
+      | .none => noneCase.φ d
+      | .some v => (someCase (⟨fun _ => v, fun _ => PB.empty, fun _ _ _ _ => empty_computes⟩)).φ d,
+   fun a => optionElim (x.impl a) (noneCase.impl a) (fun v => someCase.impl a v),
+   by
+     intro env a d h_x
+     dsimp only
+     have hcond := x.h_impl env a d h_x
+     cases hc : x.φ d with
+     | none =>
+       rw [hc] at hcond
+       exact optionElim_computesEnc_none hcond (noneCase.h_impl env a d h_x)
+     | some v =>
+       rw [hc] at hcond
+       exact optionElim_computesEnc_some hcond
+         (computesFun₂_branch2 (someCase.h_impl env a d h_x))⟩
+
+
 lemma optionElim_computesEnc_none
     {x noneCase : PB} {someCase : PB → PB}
     (hx : x.ComputesEnc env (none : Option α))
@@ -148,6 +176,132 @@ lemma constantEnc_computesEnc {α : Type} [DataEncode α] {a : α} :
     (constantEnc a).ComputesEnc env a := by
   simp [ComputesEnc, constantEnc]
 
+/-! ### Composable `RTMFun` combinators
+
+`RTMFun` bundles a mathematical function `φ`, a program builder `impl`, and a proof that `impl`
+computes `φ`. The combinators below are closed under this bundle: each derives the resulting `φ`,
+the resulting `impl`, and the correctness proof in one go. Branching combinators (`optionElimC`,
+`elimC`, `ifEqC`) pay their `cases` proof obligation *once*, here, so user code never repeats it.
+
+The function `φ` is automatically *derived* (verifiable by `rfl`), so a program built from these
+combinators needs no separate `_computes` lemma. The combinators operate on the structural encoding
+types (products, lists, `Option`); connecting to abstractions carrying invariants (e.g. `StackTape`)
+still requires a small bridge lemma relating the derived `φ` to the abstraction. -/
+
+/-- Identity transformer: computes `id`. -/
+def RTMFun.idF : RTMFun (α := α) (β := α) :=
+  ⟨id, id, fun _ _ _ h => h⟩
+
+/-- Composition: `g.comp f` computes `g.φ ∘ f.φ` via `fun a => g.impl (f.impl a)`. -/
+def RTMFun.comp {γ : Type} [DataEncode γ]
+    (g : RTMFun (α := β) (β := γ)) (f : RTMFun (α := α) (β := β)) :
+    RTMFun (α := α) (β := γ) :=
+  ⟨g.φ ∘ f.φ, fun a => g.impl (f.impl a),
+    fun env a x h => g.h_impl env (f.impl a) (f.φ x) (f.h_impl env a x h)⟩
+
+@[inherit_doc RTMFun.comp]
+scoped infixr:90 " >>> " => fun f g => RTMFun.comp g f
+
+/-- First projection of a pair-valued transformer: `f.fst` computes `Prod.fst ∘ f.φ`. Lets you write
+`x.fst` to project a sub-result, keeping the "arrow" style close to direct `PB` code. -/
+def RTMFun.fst {I A B : Type} [DataEncode I] [DataEncode A] [DataEncode B]
+    (f : RTMFun (α := I) (β := A × B)) : RTMFun (α := I) (β := A) :=
+  RTMFun.comp fst' f
+
+/-- Second projection of a pair-valued transformer: `f.snd` computes `Prod.snd ∘ f.φ`. -/
+def RTMFun.snd {I A B : Type} [DataEncode I] [DataEncode A] [DataEncode B]
+    (f : RTMFun (α := I) (β := A × B)) : RTMFun (α := I) (β := B) :=
+  RTMFun.comp snd' f
+
+/-- Fanout: run `f` and `g` on the same input and pair the results. -/
+def RTMFun.fanout {γ : Type} [DataEncode γ]
+    (f : RTMFun (α := α) (β := β)) (g : RTMFun (α := α) (β := γ)) :
+    RTMFun (α := α) (β := β × γ) :=
+  ⟨fun a => (f.φ a, g.φ a), fun a => toPair (f.impl a) (g.impl a),
+    fun env a x h => toPair_computesEnc (f.h_impl env a x h) (g.h_impl env a x h)⟩
+
+/-- Constant transformer: ignores the input, computes a fixed value `c`. -/
+def RTMFun.const (c : β) : RTMFun (α := α) (β := β) :=
+  ⟨fun _ => c, fun _ => constantEnc c, fun _ _ _ _ => constantEnc_computesEnc⟩
+
+/-- Lifted empty list. -/
+def RTMFun.emptyF : RTMFun (α := α) (β := (List β)) :=
+  ⟨fun _ => [], fun _ => empty, fun _ _ _ _ => empty_computesEnc β⟩
+
+/-- Lifted `cons`: prepend the head transformer's result to the tail transformer's list. -/
+def RTMFun.consF (h : RTMFun (α := α) (β := β)) (t : RTMFun (α := α) (β := (List β))) :
+    RTMFun (α := α) (β := (List β)) :=
+  ⟨fun a => h.φ a :: t.φ a, fun a => cons (h.impl a) (t.impl a),
+    fun env a x hx => cons_computesEnc (h.h_impl env a x hx) (t.h_impl env a x hx)⟩
+
+/-- Lifted `Option.some`. -/
+def RTMFun.someF (h : RTMFun (α := α) (β := β)) : RTMFun (α := α) (β := (Option β)) :=
+  ⟨fun a => Option.some (h.φ a), fun a => PB.some (h.impl a),
+    fun env a x hx => some_ComputesEnc (h.h_impl env a x hx)⟩
+
+/-- Lifted `optionElim` with constant branches: branches on whether the condition is `none` or
+`some`, ignoring the wrapped value. The `cases` proof is paid once. -/
+def RTMFun.optionElimC {I : Type} [DataEncode I]
+    (cond : RTMFun (α := I) (β := Option α))
+    (noneCase someCase : RTMFun (α := I) (β := β)) : RTMFun (α := I) (β := β) :=
+  ⟨fun i => (cond.φ i).elim (noneCase.φ i) (fun _ => someCase.φ i),
+   fun a => optionElim (cond.impl a) (noneCase.impl a) (fun _ => someCase.impl a),
+   by
+     intro env a x h
+     dsimp only
+     have hcond := cond.h_impl env a x h
+     cases hc : cond.φ x with
+     | none =>
+       rw [hc] at hcond
+       exact optionElim_computesEnc_none hcond (noneCase.h_impl env a x h)
+     | some v =>
+       rw [hc] at hcond
+       exact optionElim_computesEnc_some hcond
+         (computesFun₂_const (someCase.h_impl env a x h))⟩
+
+/-- Lifted list `elim` with constant branches: branches on whether the condition is `[]` or
+`hd :: tl`, ignoring `hd`/`tl`. The `cases` proof is paid once. -/
+def RTMFun.elimC {I : Type} [DataEncode I]
+    (cond : RTMFun (α := I) (β := List α))
+    (nilCase consCase : RTMFun (α := I) (β := β)) : RTMFun (α := I) (β := β) :=
+  ⟨fun i => (cond.φ i).casesOn (nilCase.φ i) (fun _ _ => consCase.φ i),
+   fun a => elim (cond.impl a) (nilCase.impl a) (fun _ _ => consCase.impl a),
+   by
+     intro env a x h
+     dsimp only
+     have hcond := cond.h_impl env a x h
+     cases hc : cond.φ x with
+     | nil =>
+       rw [hc] at hcond
+       exact elim_nil_computes hcond (nilCase.h_impl env a x h)
+     | cons hd tl =>
+       rw [hc] at hcond
+       refine elim_cons_computes (head := DataEncode.encode hd)
+         (tail := (tl.map DataEncode.encode)) ?_
+         (computesFun₂_const (consCase.h_impl env a x h))
+       simpa [ComputesEnc, DataEncode.encode] using hcond⟩
+
+/-- Lifted `ifEq` against a constant `c`: takes `thenCase` when the condition equals `c` (decided by
+`DecidableEq`), else `elseCase`. The case split is paid once. -/
+def RTMFun.ifEqC {I : Type} [DataEncode I] [DecidableEq α]
+    (cond : RTMFun (α := I) (β := α)) (c : α)
+    (thenCase elseCase : RTMFun (α := I) (β := β)) : RTMFun (α := I) (β := β) :=
+  ⟨fun i => if cond.φ i = c then thenCase.φ i else elseCase.φ i,
+   fun a => PB.ifEq (cond.impl a) (constantEnc c) (thenCase.impl a) (elseCase.impl a),
+   by
+     intro env a x h
+     dsimp only
+     have hcond := cond.h_impl env a x h
+     by_cases hx : cond.φ x = c
+     · rw [if_pos hx]
+       rw [hx] at hcond
+       exact ifeq_eq_computes hcond constantEnc_computesEnc (thenCase.h_impl env a x h)
+     · rw [if_neg hx]
+       refine ifeq_ne_computes hcond constantEnc_computesEnc ?_ (elseCase.h_impl env a x h)
+       intro heq
+       exact hx (DataEncode.h_inj heq)⟩
+
+
 /-- `foldl f init list`: left fold of `f` (taking `acc` then `el`) over `list`. -/
 def foldl (f : PB → PB → PB) (init list : PB) : PB :=
   snd (PB.while_ (toPair list init)