diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean b/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean
index 40c59283f..340304472 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Configuration.lean
@@ -60,6 +60,7 @@ the sub-linear space modifications from chapter 2.5 with the following changes:
     output tape
 * `Action`: what a machine does in one step
 * `Action.apply`: the effect of one action on a configuration
+* `HeadSymbols`, `Cfg.headSymbols`: the symbols under the heads, which a transition reads
 * `Cfg.Halted`, `Cfg.init`: halting, and the configuration a machine starts in
 
 ## References
@@ -198,6 +199,19 @@ lemma inputSymbolInner {cfg : Cfg k Symbol State input} (p : ℕ)
 def Cfg.workTapeSymbols (cfg : Cfg k Symbol State input) (i : Fin k) : Option Symbol :=
   cfg.workTapes i (cfg.workTapePos i)
 
+/-- The symbols under the heads of a machine with `k` work tapes, which its transitions read. -/
+@[ext]
+structure HeadSymbols (k : ℕ) (Symbol : Type*) where
+  /-- the symbol under the input head -/
+  inputSymbol : Option Symbol
+  /-- the symbols under the work-tape heads -/
+  workTapeSymbols : Fin k → Option Symbol
+
+/-- The symbols under the heads of a configuration. -/
+@[simps]
+def Cfg.headSymbols (cfg : Cfg k Symbol State input) : HeadSymbols k Symbol :=
+  ⟨cfg.inputSymbol, cfg.workTapeSymbols⟩
+
 /-- A configuration is halted when it has no state to continue from. -/
 abbrev Cfg.Halted (cfg : Cfg k Symbol State input) : Prop := cfg.state = none
 
@@ -212,12 +226,6 @@ output, so prepending to it preserves steps: cf. `Turing.MultiTapeNTM.prependOut
     {State' : Type*} (q : Option State') : Cfg k Symbol State' input :=
   ⟨q, cfg.inputPos, cfg.workTapes, cfg.workTapePos, cfg.output⟩
 
-/-- Forget the control state of a configuration, keeping the input head, the work tapes, the
-work-tape heads and the output. A property of this part of a configuration makes sense for every
-machine, whatever its state type. -/
-@[simps] def Cfg.forgetState (cfg : Cfg k Symbol State input) : Cfg k Symbol Unit input :=
-  ⟨some (), cfg.inputPos, cfg.workTapes, cfg.workTapePos, cfg.output⟩
-
 /-- Remap the (optional) state of a configuration through `φ`, leaving the input head, the work
 tapes, the work-tape heads and the output alone. Control-flow combinators such as `seq` embed a
 sub-machine's configurations into the combined machine by exactly such a state remap. -/
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean
index 33afcdebb..00d35bc14 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Deterministic.lean
@@ -31,6 +31,8 @@ We define a number of structures and concepts related to multi-tape Turing machi
     symbols to exactly one action
 * `MultiTapeTM`: the TM itself
 * `tr`, `ofTr`: the derived transition function and construction from a function
+* `adapt`: the machine run through an adapter
+* `wire`: two machines on the same tapes wired into one
 * `step`, `runFrom`: the successor configuration and iteration of this function
 * `MultiTapeNTM.RunPath.ofDeterministic`, `MultiTapeNTM.ComputationPath.ofDeterministic`:
     paths of a given length from an arbitrary or initial configuration
@@ -110,6 +112,53 @@ lemma tr_ofTr (q₀ : State)
     (ofTr q₀ tr).tr q input work = tr q input work :=
   tr_iff.mp rfl
 
+/-- The transitions of `tm` performed through `adapter`: it reads what `tm` reads through `adapter`
+and performs the adaptation of the action of `tm`. -/
+noncomputable def adaptedTr {k' : ℕ} {State' : Type*} (tm : MultiTapeTM k Symbol State)
+    (adapter : MultiTapeNTM.Adapter k k' Symbol State State') (q : State) (inp : Option Symbol)
+    (work : Fin k' → Option Symbol) : Action k' Symbol State' :=
+  adapter.action ⟨inp, work⟩ (tm.tr q (adapter.read ⟨inp, work⟩).inputSymbol
+    (adapter.read ⟨inp, work⟩).workTapeSymbols)
+
+/-- `tm` run through `adapter`, a `MultiTapeNTM.Adapter`: the adapter computes what `tm` reads
+from the symbols under the heads of the new machine, and gives the action of the new machine
+performing each action of `tm`. In state `q`, `tm.adapt adapter` performs the adaptation of the
+action of `tm` in `q` on what the adapter reads. -/
+noncomputable def adapt {k' : ℕ} (tm : MultiTapeTM k Symbol State)
+    (adapter : MultiTapeNTM.Adapter k k' Symbol State State) : MultiTapeTM k' Symbol State :=
+  ofTr tm.q₀ (tm.adaptedTr adapter)
+
+/-- `tm.adapt adapter` follows `tm`. -/
+lemma adapt.follows {k' : ℕ} {adapter : MultiTapeNTM.Adapter k k' Symbol State State} :
+    (tm.adapt adapter).Follows tm id adapter :=
+  fun _ _ _ h => tr_iff.mp h ▸ rfl
+
+/-- `tm₀` and `tm₁` wired into one machine on their shared tapes, which starts in `q₀`: in a state
+`inl q` it performs the transition of `tm₀` in `q`, and in `inr q` that of `tm₁`. The wires `next₀`
+and `next₁` say where the steps of each machine lead: within the same machine, to the other
+machine, or to halting. -/
+noncomputable def wire {State₀ State₁ : Type*} (tm₀ : MultiTapeTM k Symbol State₀)
+    (tm₁ : MultiTapeTM k Symbol State₁) (next₀ : Option State₀ → Option (State₀ ⊕ State₁))
+    (next₁ : Option State₁ → Option (State₀ ⊕ State₁)) (q₀ : State₀ ⊕ State₁) :
+    MultiTapeTM k Symbol (State₀ ⊕ State₁) :=
+  ofTr q₀ fun q => q.elim (tm₀.adaptedTr (.mapState next₀)) (tm₁.adaptedTr (.mapState next₁))
+
+namespace wire
+
+variable {State₀ State₁ : Type*} {tm₀ : MultiTapeTM k Symbol State₀}
+  {tm₁ : MultiTapeTM k Symbol State₁} {next₀ : Option State₀ → Option (State₀ ⊕ State₁)}
+  {next₁ : Option State₁ → Option (State₀ ⊕ State₁)} {q₀ : State₀ ⊕ State₁}
+
+/-- In its states `inl q`, the wiring follows `tm₀`, its steps leading along `next₀`. -/
+lemma follows_left : (wire tm₀ tm₁ next₀ next₁ q₀).Follows tm₀ .inl (.mapState next₀) :=
+  fun _ _ _ h => tr_iff.mp h ▸ rfl
+
+/-- In its states `inr q`, the wiring follows `tm₁`, its steps leading along `next₁`. -/
+lemma follows_right : (wire tm₀ tm₁ next₀ next₁ q₀).Follows tm₁ .inr (.mapState next₁) :=
+  fun _ _ _ h => tr_iff.mp h ▸ rfl
+
+end wire
+
 /-!
 ## Stepping a Turing Machine
 
@@ -169,27 +218,6 @@ lemma step_of_halt {cfg : Cfg k Symbol State input} (h : cfg.state = none) :
     tm.step cfg = cfg :=
   step_iff.mp ((MultiTapeNTM.step_of_halt h).mpr rfl)
 
-/-- A configuration map semiconjugating the step functions is a homomorphism of the step relations,
-so it maps run paths with `RelSeries.map`. -/
-def stepHom {k' : ℕ} {State' : Type*} {input' : List Symbol}
-    {tm' : MultiTapeTM k' Symbol State'}
-    (f : Cfg k Symbol State input → Cfg k' Symbol State' input')
-    (h : Function.Semiconj f tm.step tm'.step) :
-    (tm.stepRel input).Hom (tm'.stepRel input') where
-  toFun := f
-  map_rel' hc := step_iff.mpr ((h _).symm.trans (congrArg f (step_iff.mp hc)))
-
-/-- A configuration map commuting with the step functions on running configurations is a
-homomorphism from the running steps of `tm` to the steps of `tm'`. -/
-@[simps! apply]
-def runningStepHom {k' : ℕ} {State' : Type*} {input' : List Symbol}
-    {tm' : MultiTapeTM k' Symbol State'}
-    (f : Cfg k Symbol State input → Cfg k' Symbol State' input')
-    (h : ∀ c, ¬c.Halted → tm'.step (f c) = f (tm.step c)) :
-    (tm.runningStepRel input).Hom (tm'.stepRel input') where
-  toFun := f
-  map_rel' {c _} hc := step_iff.mpr ((h c hc.1).trans (congrArg f (step_iff.mp hc.2)))
-
 end MultiTapeTM
 
 namespace MultiTapeNTM
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean
index 447e62baa..c344b1aea 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Nondeterministic.lean
@@ -39,6 +39,10 @@ requires every path of at least `t` steps to end in a halted configuration.
 * `Step`: the one-step relation on configurations
 * `RunPath`: finite relation series of steps
 * `ComputationPath`: a run path starting at the initial configuration
+* `Adapter`, `Follows`: a machine follows another when it performs each of its transitions,
+  reading and acting through an adapter
+* `Follows.runningStepHom`, `Follows.stepHom`: a configuration map that agrees with the adapter is a
+  homomorphism of step relations, so it maps run paths
 * `RunsInTime`: every computation path of at least the given length ends in a halted
   configuration
 
@@ -173,20 +177,6 @@ lemma exists_running (p : ntm.RunPath input) (h : p.last.Halted) :
 
 end RunPath
 
-/-- A machine never reads its output tape, so prepending a word to the output preserves steps. -/
-@[simps]
-def prependOutputHom (ntm : MultiTapeNTM k Symbol State) (pre : List Symbol) :
-    (ntm.stepRel input).Hom (ntm.stepRel input) where
-  toFun c := c.prependOutput pre
-  map_rel' {c c'} h := by
-    change ntm.Step c c' at h
-    change ntm.Step (c.prependOutput pre) (c'.prependOutput pre)
-    unfold Step at h ⊢
-    rcases hq : c.state with _ | q <;> simp only [hq, Cfg.prependOutput_state] at h ⊢
-    · rw [h]
-    · obtain ⟨a, ha, rfl⟩ := h
-      exact ⟨a, ha, Cfg.ext rfl rfl rfl rfl (by simp [Action.apply])⟩
-
 /-- A run path starting at the initial configuration for `input`. -/
 structure ComputationPath (ntm : MultiTapeNTM k Symbol State) (input : List Symbol)
     extends toRunPath : ntm.RunPath input where
@@ -210,6 +200,82 @@ lemma RunsInTime.mono {input : List Symbol} {t t' : ℕ}
     (h : ntm.RunsInTime input t) (ht : t ≤ t') : ntm.RunsInTime input t' :=
   fun p hp ↦ h p (ht.trans hp)
 
+/-! ### Following a machine -/
+
+/-- How a machine with `k'` work tapes and states `State'` performs the transitions of a machine
+with `k` work tapes and states `State`. A transition turns the symbols under the heads into an
+action, so the outer machine translates both ends: `read` computes the symbols the inner machine
+reads from those under the outer heads, and `action` turns the inner action into an outer one,
+which may also depend on the outer symbols. -/
+structure Adapter (k k' : ℕ) (Symbol State State' : Type*) where
+  /-- the symbols the inner machine reads -/
+  read : HeadSymbols k' Symbol → HeadSymbols k Symbol
+  /-- the outer action performing an inner action -/
+  action : HeadSymbols k' Symbol → Action k Symbol State → Action k' Symbol State'
+
+/-- The adapter that relabels the states through `φ` and reads and acts on the same tapes. -/
+def Adapter.mapState {State' : Type*} (φ : Option State → Option State') :
+    Adapter k k Symbol State State' :=
+  ⟨id, fun _ a => { a with state := φ a.state }⟩
+
+/-- `ntm'` follows `ntm` through `adapter`, in state `state q` while `ntm` is in state `q`: whatever
+`ntm` may do in `q` on what `adapter` reads, `ntm'` may do the adapted action in `state q`. -/
+def Follows {k' : ℕ} {State' : Type*} (ntm' : MultiTapeNTM k' Symbol State')
+    (ntm : MultiTapeNTM k Symbol State) (state : State → State')
+    (adapter : Adapter k k' Symbol State State') : Prop :=
+  ∀ q heads action,
+    ntm.Tr q (adapter.read heads).inputSymbol (adapter.read heads).workTapeSymbols action →
+      ntm'.Tr (state q) heads.inputSymbol heads.workTapeSymbols (adapter.action heads action)
+
+namespace Follows
+
+variable {k' : ℕ} {State' : Type*} {input' : List Symbol} {ntm' : MultiTapeNTM k' Symbol State'}
+  {state : State → State'} {adapter : Adapter k k' Symbol State State'}
+
+/-- **A follower mirrors the running steps.** If `ntm'` follows `ntm`, and `f` sends a configuration
+in state `q` to one in state `state q`, from which `adapter` reads what the configuration reads and
+on which each adapted action acts as the action acts on the configuration, then `f` maps each
+running step of `ntm` to a step of `ntm'`. -/
+def runningStepHom (h : ntm'.Follows ntm state adapter)
+    (f : Cfg k Symbol State input → Cfg k' Symbol State' input')
+    (hstate : ∀ c q, c.state = some q → (f c).state = some (state q))
+    (hread : ∀ c, adapter.read (f c).headSymbols = c.headSymbols)
+    (haction : ∀ c action,
+      (adapter.action (f c).headSymbols action).apply (f c) = f (action.apply c)) :
+    (ntm.runningStepRel input).Hom (ntm'.stepRel input') where
+  toFun := f
+  map_rel' {c _} := fun ⟨hrunning, hstep⟩ => by
+    obtain ⟨q, hq⟩ := Option.ne_none_iff_exists'.mp hrunning
+    simp only [Set.mem_ofPred_eq, Step, hq, hstate c q hq] at hstep ⊢
+    obtain ⟨action, hTr, rfl⟩ := hstep
+    exact ⟨_, h q _ action (by rwa [hread]), (haction c action).symm⟩
+
+/-- **A follower mirrors the steps.** As `runningStepHom`, for an `f` that relabels every state
+through `state`, so that it also keeps halted configurations halted. -/
+def stepHom (h : ntm'.Follows ntm state adapter)
+    (f : Cfg k Symbol State input → Cfg k' Symbol State' input')
+    (hstate : ∀ c, c.state.map state = (f c).state)
+    (hread : ∀ c, adapter.read (f c).headSymbols = c.headSymbols)
+    (haction : ∀ c action,
+      (adapter.action (f c).headSymbols action).apply (f c) = f (action.apply c)) :
+    (ntm.stepRel input).Hom (ntm'.stepRel input') where
+  toFun := f
+  map_rel' {c _} hc :=
+    if hc' : c.Halted then ((step_of_halt hc').mp hc).symm ▸
+      (step_of_halt ((hstate c).symm.trans (congrArg (Option.map state) hc'))).mpr rfl
+    else (h.runningStepHom f (fun c _ hq => (hstate c).symm.trans (congrArg (Option.map state) hq))
+      hread haction).map_rel ⟨hc', hc⟩
+
+end Follows
+
+/-- A machine never reads its output tape, so prepending a word to the output preserves steps. -/
+@[simps! apply]
+def prependOutputHom (ntm : MultiTapeNTM k Symbol State) (pre : List Symbol) :
+    (ntm.stepRel input).Hom (ntm.stepRel input) :=
+  Follows.stepHom (state := id) (adapter := .mapState id) (fun _ _ _ h => h) (·.prependOutput pre)
+    (fun _ => Option.map_id_apply) (fun _ => rfl) fun _ _ =>
+      Cfg.ext rfl rfl rfl rfl (by simp [Action.apply, Adapter.mapState])
+
 end MultiTapeNTM
 
 end Turing
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ClearWork.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ClearWork.lean
index db56718d5..cefff3ef5 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ClearWork.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ClearWork.lean
@@ -64,22 +64,20 @@ public theorem transformsTapes_clearWork (w : List Symbol) :
       Cfg 1 Symbol RewindWorkState input) (w.length + 2)
   have h₀ : p₀.last = _ := runFrom_forwardWork (input := input) 1 w out (zero_add _)
   have h₁ : p₁.last = _ := runFrom_rewindWork_erase (input := input) 1 (tapeOfList w) out rfl
-  obtain ⟨p, hh, hl, ht, hmem⟩ := exists_runPath_seq (p₀ := p₀) (p₁ := p₁) (by rw [h₀])
-    (by rw [h₀]; rfl) (by rw [h₁])
+  obtain ⟨p, hh, hl, ht, hvisited⟩ := exists_runPath_seq (p₀ := p₀) (p₁ := p₁) (by rw [h₀])
+    (by rw [h₀]; rfl)
   refine ⟨fun _ => [], [], ⟨rfl, rfl⟩, p, hh,
     by rw [hl, h₁]; simp [rightCfg, Cfg.mapState, wordsCfg],
     (show p.length ≤ w.length + 1 + (w.length + 2) from ht).trans (by lia), ?_⟩
-  -- every head position of the two passes is in `[-1, w.length]`
+  -- both passes keep the head within `[-1, w.length]`
   rw [MultiTapeNTM.RunPath.space, Fin.sum_univ_one]
-  refine (p.spaceUsedByTape_le_card (S := .Icc (-1) (w.length : ℤ)) fun c hc => ?_).trans
-    (by simp; lia)
-  rcases hmem c hc with ⟨_, ⟨m, rfl⟩, he⟩ | ⟨_, ⟨m, rfl⟩, he⟩ <;>
-    rw [show c.workTapePos 0 = _ from congrArg (·.workTapePos 0) he]
-  · exact Finset.mem_Icc.2 (Set.Icc_subset_Icc_left (by lia)
-      (workTapePos_runFrom_forwardWork (input := input) 1 w out (Nat.zero_le w.length) m))
-  · exact Finset.mem_Icc.2
-      (workTapePos_runFrom_rewindWork (some none) (input := input) 1 (tapeOfList w) out rfl
-        le_rfl m)
+  refine (Finset.card_le_card (t := .Icc (-1 : ℤ) w.length)
+    ((hvisited 0).trans (Finset.union_subset ?_ ?_))).trans (by simp; lia) <;>
+    refine Finset.image_subset_iff.mpr fun m _ => Finset.mem_Icc.2 ?_
+  · exact Set.Icc_subset_Icc_left (by lia)
+      (workTapePos_runFrom_forwardWork (input := input) 1 w out (Nat.zero_le w.length) m)
+  · exact workTapePos_runFrom_rewindWork (some none) (input := input) 1 (tapeOfList w) out rfl
+      le_rfl m
 
 /-! ### Clearing one of several work tapes -/
 
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ExtendTapes.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ExtendTapes.lean
index 9faac83bc..13b324aea 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ExtendTapes.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/ExtendTapes.lean
@@ -19,8 +19,8 @@ tape `j`. The remaining tapes are left unchanged.
 The configuration map `embed e cfg extraTapes extraPos` places `cfg` on the selected tapes and
 initialises the remaining tapes from `extraTapes` and `extraPos`.
 
-The main lemmas show that one step and an entire run path of the larger machine mirror the
-corresponding step and run path of `tm`.
+The configuration map is a homomorphism of step relations (`embedHom`), so each run path of `tm`
+maps to a run path of the larger machine.
 
 ## Main definitions
 
@@ -34,7 +34,6 @@ corresponding step and run path of `tm`.
 
 ## Main results
 
-* `Turing.MultiTapeTM.step_embed`: the one-step mirroring lemma.
 * `Turing.MultiTapeTM.space_map_embedHom_le`: the space bound for a mapped path.
 * `Turing.MultiTapeTM.oneTapeCfg`: the one-tape view of a configuration.
 * `Turing.MultiTapeTM.runFrom_tapeEmb`: the run of a one-tape machine placed on work tape `i`.
@@ -64,14 +63,12 @@ public lemma partialInv_isPartialInv (e : Fin k ↪ Fin k') :
 moves. -/
 @[expose] public noncomputable def extendTapes (tm : MultiTapeTM k Symbol State)
     (e : Fin k ↪ Fin k') : MultiTapeTM k' Symbol State :=
-  ofTr tm.q₀ fun q inp work =>
-    let a := tm.tr q inp fun j => work (e j)
-    { inputTape := a.inputTape
-      workTapes := fun l => match partialInv e l with
-        | some j => a.workTapes j
-        | none => (none, 0)
-      output := a.output
-      state := a.state }
+  tm.adapt
+    { read := fun heads => ⟨heads.inputSymbol, heads.workTapeSymbols ∘ e⟩
+      action := fun _ a =>
+        { a with workTapes := fun l => match partialInv e l with
+            | some j => a.workTapes j
+            | none => (none, 0) } }
 
 @[simp]
 public lemma extendTapes_q₀ (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') :
@@ -106,11 +103,6 @@ public lemma partialInv_eq_some (e : Fin k ↪ Fin k') {l : Fin k'} {j : Fin k}
     (h : partialInv e l = some j) : e j = l :=
   (partialInv_isPartialInv e j l).mp h
 
-@[simp]
-public lemma embed_inputSymbol (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input)
-    (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) :
-    (embed e cfg extraTapes extraPos).inputSymbol = cfg.inputSymbol := rfl
-
 @[simp]
 public lemma embed_workTapes_embed (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input)
     (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) (j : Fin k) :
@@ -129,30 +121,18 @@ public lemma embed_workTapeSymbols_embed (e : Fin k ↪ Fin k') (cfg : Cfg k Sym
     (embed e cfg extraTapes extraPos).workTapeSymbols (e j) = cfg.workTapeSymbols j := by
   simp [Cfg.workTapeSymbols]
 
-/-- Reindexing is a step-semiconjugation: the reindexed machine acts on the embedded tapes exactly
-as `tm` does, and never touches the extra tapes. -/
-public lemma step_embed (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k')
-    (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) :
-    Function.Semiconj (embed (input := input) e · extraTapes extraPos) tm.step
-      (tm.extendTapes e).step := by
-  intro cfg
-  symm
-  cases hq : cfg.state with
-  | none => simp [embed, hq]
-  | some q =>
-    rw [step_of_state (cfg := embed e cfg extraTapes extraPos) hq, step_of_state hq]
-    simp only [extendTapes, tr_ofTr, embed_inputSymbol, embed_workTapeSymbols_embed]
-    refine Cfg.ext rfl rfl ?_ ?_ rfl <;> funext l <;> simp only [Action.apply, embed] <;>
-      cases partialInv e l <;> simp
-
 /-- `embed` as a homomorphism of step relations: each step `c → c'` of `tm` becomes the step
 `embed c → embed c'` of the reindexed machine, so a run path of `tm` maps to a run path of the
-reindexed machine, with the extra tapes held fixed. `stepHom` builds it from `step_embed`, which
-says that `embed` commutes with the step functions. -/
+reindexed machine, with the extra tapes held fixed. `Follows.stepHom` builds it, since `embed`
+agrees with the adapter defining `extendTapes`. -/
 @[expose, simps! apply] public noncomputable def embedHom (tm : MultiTapeTM k Symbol State)
     (e : Fin k ↪ Fin k') (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) :
     (tm.stepRel input).Hom ((tm.extendTapes e).stepRel input) :=
-  stepHom (embed e · extraTapes extraPos) (step_embed tm e extraTapes extraPos)
+  adapt.follows.stepHom (embed e · extraTapes extraPos) (fun _ => Option.map_id_apply)
+    (fun c => HeadSymbols.ext rfl (funext (embed_workTapeSymbols_embed e c extraTapes extraPos)))
+    fun c a => by
+      refine Cfg.ext rfl rfl ?_ ?_ rfl <;> funext l <;> simp only [Action.apply, embed] <;>
+        cases partialInv e l <;> simp
 
 section Space
 
@@ -243,12 +223,10 @@ public theorem TransformsTapes.tapeEmb {tm : MultiTapeTM 1 Symbol State}
         (fun _ => 0) = wordsCfg input q (Function.update ws i (v 0)) o := by
     rw [embed_tapeEmb]
     refine Cfg.ext rfl rfl ?_ ?_ rfl <;> funext l <;> by_cases hl : l = i <;> simp [hl, wordsCfg]
-  refine ⟨Function.update ws i (v 0), emitted, ⟨v, hQ, rfl⟩,
-    p.map (embedHom tm (MultiTapeTM.tapeEmb i) (fun l => tapeOfList (ws l)) (fun _ => 0)),
-    ?_, ?_, htime, (space_map_embedHom_le ..).trans (Nat.add_le_add_right hspace _)⟩
-  · simp only [RelSeries.head_map, hhead, embedHom_apply, hplace, Function.update_eq_self]
-    rfl
-  · simp only [RelSeries.last_map, hlast, embedHom_apply, hplace]
+  exact ⟨Function.update ws i (v 0), emitted, ⟨v, hQ, rfl⟩,
+    p.map (embedHom tm (MultiTapeTM.tapeEmb i) (fun l => tapeOfList (ws l)) fun _ => 0),
+    by simp [hhead, hplace], by simp [hlast, hplace], htime,
+    (space_map_embedHom_le ..).trans (Nat.add_le_add_right hspace _)⟩
 
 end OneTape
 
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromTape.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromTape.lean
index 9c9497046..1dac546ff 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromTape.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/InputFromTape.lean
@@ -26,8 +26,8 @@ reading the flag. Reading blank on both the virtual input tape and the flag tape
 boundary.
 
 The configuration map `inCfg` places the simulated input on the virtual input tape, places the
-marker on the flag tape, and leaves the real input tape unused. The main lemmas show that one step
-and an entire run path of the redirected machine mirror the corresponding step and run path of `tm`.
+marker on the flag tape, and leaves the real input tape unused. It is a homomorphism of step
+relations (`inCfgHom`), so each run path of `tm` maps to a run path of the redirected machine.
 -/
 
 namespace Turing.MultiTapeTM
@@ -50,12 +50,15 @@ are. -/
 moved. -/
 @[expose] public noncomputable def inputFromTape (tm : MultiTapeTM k Symbol State) :
     MultiTapeTM (k + 2) Symbol State :=
-  ofTr tm.q₀ fun q _ work =>
-    let a := tm.tr q (work (Fin.natAdd k 0)) fun j => work (j.castAdd 2)
-    let m := clampMove (work (Fin.natAdd k 0)) (work (Fin.natAdd k 1)) a.inputTape
-    { a with
-      inputTape := 0
-      workTapes := Fin.append a.workTapes fun _ => (none, m) }
+  tm.adapt
+    { read := fun heads =>
+        ⟨heads.workTapeSymbols (Fin.natAdd k 0), heads.workTapeSymbols ∘ Fin.castAdd 2⟩
+      action := fun heads a =>
+        let m := clampMove (heads.workTapeSymbols (Fin.natAdd k 0))
+          (heads.workTapeSymbols (Fin.natAdd k 1)) a.inputTape
+        { a with
+          inputTape := 0
+          workTapes := Fin.append a.workTapes fun _ => (none, m) } }
 
 /-- A configuration of `tm` on `input`, as the redirecting machine sees it, over an arbitrary
 ambient input: `input` sits on the virtual input tape with the head at cell `inputPos - 1`, the flag
@@ -153,28 +156,19 @@ public lemma val_moveInputPos_sub_one_eq_clampMove (mark : Symbol) (c : Cfg k Sy
     rw [inputSymbolInner (c.inputPos.val - 1) (by omega) (by omega)]
     rcases m with _ | _ | _ <;> simp only [clampMove, SignType.cast] <;> omega
 
-/-- **The redirection is a step-semiconjugation.** One step of the machine reading its input from
-the virtual tape mirrors one step of the original, under the embedding `inCfg`. -/
-public lemma step_inCfg (tm : MultiTapeTM k Symbol State) (mark : Symbol)
-    (outerInput : List Symbol) :
-    Function.Semiconj (inCfg (input := input) mark · outerInput) tm.step tm.inputFromTape.step := by
-  intro c
-  symm
-  cases hq : c.state with
-  | none => simp [inCfg, hq]
-  | some q =>
-    rw [step_of_state (cfg := inCfg mark c outerInput) hq, step_of_state hq]
-    simp only [inputFromTape, tr_ofTr, inCfg_workTapeSymbols_vip, inCfg_workTapeSymbols_flag,
-      inCfg_workTapeSymbols_castAdd]
-    refine Cfg.ext rfl (by simp [inCfg]) ?_ ?_ rfl <;> funext l <;>
-      induction l using Fin.addCases <;> simp [inCfg, val_moveInputPos_sub_one_eq_clampMove mark]
-
 /-- The redirection preserves steps, so it maps run paths of `tm` to run paths of the redirected
 machine. -/
 @[expose, simps! apply] public noncomputable def inCfgHom (tm : MultiTapeTM k Symbol State)
     (mark : Symbol) (outerInput : List Symbol) :
-    (tm.stepRel input).Hom (tm.inputFromTape.stepRel outerInput) :=
-  stepHom (inCfg mark · outerInput) (step_inCfg tm mark outerInput)
+    (tm.stepRel input).Hom (tm.inputFromTape.stepRel outerInput) := by
+  refine adapt.follows.stepHom (inCfg mark · outerInput) (fun _ => Option.map_id_apply)
+    (fun c => HeadSymbols.ext (inCfg_workTapeSymbols_vip c)
+      (funext (inCfg_workTapeSymbols_castAdd c))) fun c a => ?_
+  simp only [Cfg.headSymbols_workTapeSymbols, inCfg_workTapeSymbols_vip, inCfg_workTapeSymbols_flag]
+  refine Cfg.ext rfl (by simp [inCfg]) (funext fun l => ?_) (funext fun l => ?_) rfl <;>
+    induction l using Fin.addCases with
+    | left j => simp [inCfg, Action.apply]
+    | right j => simp [inCfg, Action.apply, val_moveInputPos_sub_one_eq_clampMove mark]
 
 /-- **Space of the input-redirected path.** The `k` inner tapes visit exactly what the original
 path visits; the two extra tapes (virtual input, flag) each move only with the simulated input
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/OutputToTape.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/OutputToTape.lean
index 6fbf45675..ba3e9070b 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/OutputToTape.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/OutputToTape.lean
@@ -18,8 +18,8 @@ frontier.
 
 Since the output is append-only, the frontier position is a *function of the configuration* —
 the length of the output so far — so the redirected machine mirrors the original through the
-configuration map `outCfg`. The main lemmas show that one step and an entire run path of the
-redirected machine mirror the corresponding step and run path of `tm`.
+configuration map `outCfg`, a homomorphism of step relations (`outCfgHom`), so each run path of `tm`
+maps to a run path of the redirected machine.
 -/
 
 namespace Turing.MultiTapeTM
@@ -30,16 +30,16 @@ variable {k : ℕ} {Symbol State : Type*} {input : List Symbol}
 at the write frontier. -/
 @[expose] public noncomputable def outputToTape (tm : MultiTapeTM k Symbol State) :
     MultiTapeTM (k + 1) Symbol State :=
-  ofTr tm.q₀ fun q inp work =>
-    let a := tm.tr q inp fun j => work j.castSucc
-    { inputTape := a.inputTape
-      workTapes := Fin.lastCases
-        (match a.output with
-          | none => (none, 0)
-          | some s => (some (some s), 1))
-        (fun j => a.workTapes j)
-      output := none
-      state := a.state }
+  tm.adapt
+    { read := fun heads => ⟨heads.inputSymbol, heads.workTapeSymbols ∘ Fin.castSucc⟩
+      action := fun _ a =>
+        { a with
+          workTapes := Fin.lastCases
+            (match a.output with
+              | none => (none, 0)
+              | some s => (some (some s), 1))
+            a.workTapes
+          output := none } }
 
 /-- A configuration of `tm`, as the redirected machine sees it: the output so far sits on the
 last work tape with the head at its end, and the real output is empty. -/
@@ -50,10 +50,6 @@ last work tape with the head at its end, and the real output is empty. -/
     Fin.lastCases (c.output.length : ℤ) (fun j => c.workTapePos j),
     []⟩
 
-@[simp]
-public lemma outCfg_inputSymbol (c : Cfg k Symbol State input) :
-    (outCfg c).inputSymbol = c.inputSymbol := rfl
-
 @[simp]
 public lemma outCfg_workTapes_last (c : Cfg k Symbol State input) :
     (outCfg c).workTapes (Fin.last k) = tapeOfList c.output := by
@@ -79,27 +75,17 @@ public lemma outCfg_workTapeSymbols_castSucc (c : Cfg k Symbol State input) (j :
     (outCfg c).workTapeSymbols j.castSucc = c.workTapeSymbols j := by
   simp [Cfg.workTapeSymbols]
 
-/-- The redirection is a step-semiconjugation. -/
-public lemma step_outCfg (tm : MultiTapeTM k Symbol State) :
-    Function.Semiconj (outCfg (input := input)) tm.step tm.outputToTape.step := by
-  intro c
-  symm
-  cases hq : c.state with
-  | none => simp [outCfg, hq]
-  | some q =>
-    rw [step_of_state (cfg := outCfg c) hq, step_of_state hq]
-    simp only [outputToTape, tr_ofTr, outCfg_inputSymbol, outCfg_workTapeSymbols_castSucc]
-    refine Cfg.ext rfl rfl ?_ ?_ rfl <;> funext l <;> induction l using Fin.lastCases with
-    | cast j => simp
-    | last =>
-      cases h : (tm.tr q c.inputSymbol c.workTapeSymbols).output <;>
-        simp [h, tapeOfList_append_single, SignType.cast]
-
 /-- The redirection preserves steps, so it maps run paths of `tm` to run paths of the redirected
 machine. -/
 @[expose, simps! apply] public noncomputable def outCfgHom (tm : MultiTapeTM k Symbol State) :
     (tm.stepRel input).Hom (tm.outputToTape.stepRel input) :=
-  stepHom outCfg (step_outCfg tm)
+  adapt.follows.stepHom outCfg (fun _ => Option.map_id_apply)
+    (fun c => HeadSymbols.ext rfl (funext (outCfg_workTapeSymbols_castSucc c))) fun c a => by
+      refine Cfg.ext rfl rfl (funext fun l => ?_) (funext fun l => ?_) rfl <;>
+        induction l using Fin.lastCases with
+        | last =>
+          cases h : a.output <;> simp [h, Action.apply, tapeOfList_append_single, SignType.cast]
+        | cast j => simp [Action.apply]
 
 /-- The initial configuration of the redirected machine is the original's through `outCfg`. -/
 public lemma initCfg_outputToTape (tm : MultiTapeTM k Symbol State) (input : List Symbol) :
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/RepeatUntilBlank.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/RepeatUntilBlank.lean
index a6408af81..d2b4d42d4 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/RepeatUntilBlank.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/RepeatUntilBlank.lean
@@ -6,8 +6,7 @@ Authors: Christian Reitwiessner
 
 module
 
-public import Mathlib.Data.Fintype.Option
-public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.TransformsTapes
+public import Cslib.Computability.Machines.Turing.MultiTape.Plumbing.Sequential
 
 /-!
 # Repeating a machine until a tape goes blank
@@ -28,76 +27,41 @@ namespace Turing.MultiTapeTM
 
 variable {k : ℕ} {Symbol State : Type*} {input : List Symbol}
 
-/-- The states of `repeatUntilBlank i tm`: those of `tm`, and a state `check` for reading tape `i`
-between rounds. -/
-public inductive RepeatUntilBlankState (State : Type*) where
-  /-- The repeated machine is running, in its state `q`. -/
-  | run (q : State)
-  /-- Tape `i` is being read, between two rounds. -/
-  | check
+/-- The test of tape `i`: it halts if the cell under the head of tape `i` is blank and otherwise
+stays in its only state, moving no head. -/
+noncomputable def RepeatUntilBlank.blankTest (i : Fin k) : MultiTapeTM k Symbol Unit :=
+  ofTr () fun _ _ work =>
+    { inputTape := 0, workTapes := fun _ => (none, 0), output := none,
+      state := (work i).map fun _ => () }
 
-public instance [Finite State] : Finite (RepeatUntilBlankState State) :=
-  Finite.of_injective (fun q => match q with | .run q => some q | .check => none)
-    fun q q' h => by cases q <;> cases q' <;> simp_all
-
-/-- `tm`, with its halting transitions sent to the state `check`. From `check`, the machine halts
-if the cell under the head of tape `i` is blank and otherwise restarts `tm`, moving no head. -/
+/-- `tm` wired with the test of tape `i`: halting of `tm` goes to the test, which halts the loop if
+the cell under the head of tape `i` is blank and otherwise restarts `tm`. -/
 public noncomputable def repeatUntilBlank (i : Fin k) (tm : MultiTapeTM k Symbol State) :
-    MultiTapeTM k Symbol (RepeatUntilBlankState State) :=
-  ofTr (.run tm.q₀) fun q inp work =>
-    match q with
-    | .run q =>
-      let a := tm.tr q inp work
-      { a with state := some (a.state.elim .check .run) }
-    | .check =>
-      { inputTape := 0, workTapes := fun _ => (none, 0), output := none,
-        state := (work i).map fun _ => .run tm.q₀ }
+    MultiTapeTM k Symbol (State ⊕ Unit) :=
+  wire tm (RepeatUntilBlank.blankTest i) (Sequential.leftState ()) (Option.map fun _ => .inl tm.q₀)
+    (.inl tm.q₀)
 
 namespace RepeatUntilBlank
 
 variable {i : Fin k} {tm : MultiTapeTM k Symbol State}
 
-/-- A configuration of `tm` as a configuration of `repeatUntilBlank i tm`: a live state `q` becomes
-`run q` and the halted state becomes `check`. -/
-def runCfg (cfg : Cfg k Symbol State input) :
-    Cfg k Symbol (RepeatUntilBlankState State) input :=
-  cfg.mapState (fun st => some (st.elim .check .run))
-
-@[simp]
-lemma workTapePos_runCfg (cfg : Cfg k Symbol State input) :
-    (runCfg cfg).workTapePos = cfg.workTapePos := rfl
-
-@[simp]
-lemma runCfg_wordsCfg_some (q : State) (ws : Fin k → List Symbol) (out : List Symbol) :
-    runCfg (input := input) (wordsCfg input (some q) ws out) =
-      wordsCfg input (some (.run q)) ws out := rfl
-
-@[simp]
-lemma runCfg_wordsCfg_none (ws : Fin k → List Symbol) (out : List Symbol) :
-    runCfg (State := State) (input := input) (wordsCfg input none ws out) =
-      wordsCfg input (some .check) ws out := rfl
-
-lemma q₀_repeatUntilBlank : (repeatUntilBlank i tm).q₀ = .run tm.q₀ := rfl
-
-/-- On `tm`'s live configurations, the looping machine mirrors `tm` step for step. -/
-lemma step_runCfg (cfg : Cfg k Symbol State input) (h : ¬ cfg.Halted) :
-    (repeatUntilBlank i tm).step (runCfg cfg) = runCfg (tm.step cfg) := by
-  obtain ⟨q, hq⟩ := Option.ne_none_iff_exists'.mp h
-  have hstate : (runCfg cfg).state = some (RepeatUntilBlankState.run q) := by
-    simp [runCfg, Cfg.mapState, hq]
-  rw [step_of_state hstate, step_of_state hq]
-  simp only [repeatUntilBlank, tr_ofTr]
-  rfl
-
-/-- From `check` on a `wordsCfg` configuration, the machine halts if the word on tape `i` is empty
+/-- A configuration of `tm` as one of `repeatUntilBlank i tm`, a live state `q` becoming `inl q` and
+the halted state the test `inr ()`: the loop mirrors the running steps of `tm`. -/
+@[simps! apply]
+noncomputable def runHom (i : Fin k) :
+    (tm.runningStepRel input).Hom ((repeatUntilBlank i tm).stepRel input) :=
+  wire.follows_left.runningStepHom (Sequential.leftCfg ())
+    (fun _ _ => congrArg (Sequential.leftState ())) (fun _ => rfl) fun _ _ => rfl
+
+/-- From the test on a `wordsCfg` configuration, the machine halts if the word on tape `i` is empty
 and otherwise restarts `tm`, leaving the words unchanged. -/
 lemma step_check (ws : Fin k → List Symbol) (out : List Symbol) :
-    (repeatUntilBlank i tm).step (wordsCfg input (some .check) ws out) =
-      wordsCfg input (if ws i = [] then none else some (.run tm.q₀)) ws out := by
+    (repeatUntilBlank i tm).step (wordsCfg input (some (.inr ())) ws out) =
+      wordsCfg input (if ws i = [] then none else some (.inl tm.q₀)) ws out := by
   rw [step_of_state rfl]
   refine Cfg.ext ?_ ?_ ?_ ?_ ?_ <;> cases h : ws i <;>
-    simp [repeatUntilBlank, Cfg.workTapeSymbols, tapeOfList_zero, wordsCfg, Action.apply,
-      SignType.cast, h]
+    simp [repeatUntilBlank, wire, adaptedTr, blankTest, MultiTapeNTM.Adapter.mapState,
+      Cfg.workTapeSymbols, tapeOfList_zero, wordsCfg, Action.apply, SignType.cast, h]
 
 /-- One round of the loop. If `tm` transforms words satisfying `P` within `t` steps and `s` cells,
 then from `tm`'s initial state on such words `w` the loop has a run path of at most `t + 1` steps
@@ -109,16 +73,16 @@ lemma exists_round {P : (input : List Symbol) → (Fin k → List Symbol) → Pr
     (h : TransformsTapes tm P Q t s) {w : Fin k → List Symbol} (out : List Symbol)
     (hP : P input w) :
     ∃ w' e, Q input w w' e ∧ ∃ p : (repeatUntilBlank i tm).RunPath input,
-      p.head = wordsCfg input (some (.run tm.q₀)) w out ∧
-      p.last = wordsCfg input (if w' i = [] then none else some (.run tm.q₀)) w' (out ++ e) ∧
+      p.head = wordsCfg input (some (.inl tm.q₀)) w out ∧
+      p.last = wordsCfg input (if w' i = [] then none else some (.inl tm.q₀)) w' (out ++ e) ∧
       p.length ≤ t + 1 ∧ p.InWindow s := by
   obtain ⟨w', e, hQ, p, hhead, hlast, htime, hspace⟩ := h input w out hP
   obtain ⟨q, hqhead, hqlast, hqlen, hqmem⟩ := p.exists_running (by rw [hlast]; rfl)
-  let f := runningStepHom (tm' := repeatUntilBlank i tm) (input := input) runCfg step_runCfg
-  have hcheck : (repeatUntilBlank i tm).Step (q.map f).last
-      (wordsCfg input (if w' i = [] then none else some (.run tm.q₀)) w' (out ++ e)) := by
-    simp [f, hqlast, hlast, step_check]
-  refine ⟨w', e, hQ, (q.map f).snoc _ hcheck, by simp [f, hqhead, hhead], by simp,
+  have hcheck : (repeatUntilBlank i tm).Step (q.map (runHom i)).last
+      (wordsCfg input (if w' i = [] then none else some (.inl tm.q₀)) w' (out ++ e)) := by
+    simp [hqlast, hlast, Sequential.leftCfg, Sequential.leftState, step_check]
+  refine ⟨w', e, hQ, (q.map (runHom i)).snoc _ hcheck,
+    by simp [hqhead, hhead, Sequential.leftCfg, Sequential.leftState], by simp,
     by simp [MultiTapeNTM.RunPath.time] at htime ⊢; lia, ?_⟩
   -- the heads of `tm` stay within `[-s, s]`, and reading tape `i` moves none of them
   have hwin := MultiTapeNTM.RunPath.inWindow_of_space_le (p := p) (by simp [hhead]) hspace
@@ -149,22 +113,20 @@ public theorem transformsTapes_repeatUntilBlank (i : Fin k) {tm : MultiTapeTM k
       (fun input _ ws' emitted => R input ws' emitted)
       ((rounds + 1) * (t + 1)) (2 * k * s + k) := by
   intro input ws out hP0
-  rw [q₀_repeatUntilBlank]
-  set start := wordsCfg (State := RepeatUntilBlankState State) input (some (.run tm.q₀)) ws out
+  rw [show (repeatUntilBlank i tm).q₀ = .inl tm.q₀ from rfl]
+  set start := wordsCfg (State := State ⊕ Unit) input (some (.inl tm.q₀)) ws out
     with hstart
   -- after `n ≤ rounds` rounds, the loop has a run path of at most `n * (t + 1)` steps within
   -- `[-s, s]` back to `tm`'s initial state, with `P n` holding
   have hrec : ∀ n ≤ rounds, ∃ (p : (repeatUntilBlank i tm).RunPath input)
       (wsn : Fin k → List Symbol) (acc : List Symbol), p.head = start ∧
-      p.last = wordsCfg input (some (.run tm.q₀)) wsn (out ++ acc) ∧ p.length ≤ n * (t + 1) ∧
+      p.last = wordsCfg input (some (.inl tm.q₀)) wsn (out ++ acc) ∧ p.length ≤ n * (t + 1) ∧
       p.InWindow s ∧ P n input wsn acc := by
     intro n hn
     induction n with
     | zero =>
-      refine ⟨.singleton _ start, ws, [], rfl, by simp [hstart], by simp, ?_, hP0⟩
-      rintro _ ⟨_, rfl⟩ l
-      change start.workTapePos l ∈ _
-      simp [hstart, mem_window]
+      exact ⟨.singleton _ start, ws, [], rfl, by simp [hstart], by simp,
+        fun _ ⟨_, h⟩ _ => h ▸ by simp [RelSeries.singleton, hstart, mem_window], hP0⟩
     | succ n ih =>
       obtain ⟨p, wsn, acc, hhead, hlast, hlen, hwin, hPn⟩ := ih (by lia)
       obtain ⟨wsn', e, hQ, q, hqhead, hqlast, hqlen, hqwin⟩ :=
diff --git a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean
index 80ce75b66..815e5e6d6 100644
--- a/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean
+++ b/Cslib/Computability/Machines/Turing/MultiTape/Plumbing/Sequential.lean
@@ -24,8 +24,8 @@ second.
 ## Main results
 
 * `Turing.MultiTapeTM.seq`: the composed machine.
-* `Turing.MultiTapeTM.exists_runPath_seq`: run paths compose, and the configurations of the
-  composed path are those of the two paths up to their states.
+* `Turing.MultiTapeTM.exists_runPath_seq`: run paths compose, and the composed path visits only
+  cells that the two paths visit.
 * `Turing.MultiTapeTM.transformsTapes_seq`: transformations compose, bounds adding.
 -/
 
@@ -35,30 +35,28 @@ namespace Turing.MultiTapeTM
 
 variable {k : ℕ} {Symbol State₀ State₁ : Type*} {input : List Symbol}
 
+/-- The state of the sequential composition while `tm₀` runs: halting hands over to the second
+machine in its state `q₁`. -/
+def Sequential.leftState (q₁ : State₁) (state : Option State₀) : Option (State₀ ⊕ State₁) :=
+  some (state.elim (.inr q₁) .inl)
+
 /-- The sequential composition of `tm₀` and `tm₁`: it behaves like `tm₀` until `tm₀` would halt,
 at which point it switches to the initial state of `tm₁` and behaves like `tm₁`. The switch is
 folded into the halting transition of `tm₀`, so it costs no step. -/
 noncomputable def seq (tm₀ : MultiTapeTM k Symbol State₀) (tm₁ : MultiTapeTM k Symbol State₁) :
     MultiTapeTM k Symbol (State₀ ⊕ State₁) :=
-  ofTr (.inl tm₀.q₀) fun q inp work =>
-    match q with
-    | .inl q₀ =>
-      let a := tm₀.tr q₀ inp work
-      { a with state := some (a.state.elim (.inr tm₁.q₀) .inl) }
-    | .inr q₁ =>
-      let a := tm₁.tr q₁ inp work
-      { a with state := a.state.map .inr }
+  wire tm₀ tm₁ (Sequential.leftState tm₁.q₀) (Option.map .inr) (.inl tm₀.q₀)
 
 variable {tm₀ : MultiTapeTM k Symbol State₀} {tm₁ : MultiTapeTM k Symbol State₁}
 
 namespace Sequential
 
 /-- A configuration of the first phase: a configuration of `tm₀`, with a halted state mapped to
-the initial state of the second phase. Under this map, the whole first phase of `seq` mirrors the
+the state `q₁` of the second phase. Under this map, the whole first phase of `seq` mirrors the
 run of `tm₀`, *including* its halting step. -/
-def leftCfg (tm₁ : MultiTapeTM k Symbol State₁) (cfg : Cfg k Symbol State₀ input) :
+def leftCfg (q₁ : State₁) (cfg : Cfg k Symbol State₀ input) :
     Cfg k Symbol (State₀ ⊕ State₁) input :=
-  cfg.mapState (fun st => some (st.elim (.inr tm₁.q₀) .inl))
+  cfg.mapState (leftState q₁)
 
 /-- A configuration of the second phase. Under this map, the second phase of `seq` mirrors the
 run of `tm₁`. -/
@@ -66,66 +64,44 @@ def rightCfg (cfg : Cfg k Symbol State₁ input) :
     Cfg k Symbol (State₀ ⊕ State₁) input :=
   cfg.mapState (Option.map .inr)
 
-lemma step_leftCfg (cfg : Cfg k Symbol State₀ input) (h : cfg.state ≠ none) :
-    (tm₀.seq tm₁).step (leftCfg tm₁ cfg) = leftCfg tm₁ (tm₀.step cfg) := by
-  obtain ⟨q, hq⟩ := Option.ne_none_iff_exists'.mp h
-  have h1 : (leftCfg tm₁ cfg).state = some (Sum.inl q : State₀ ⊕ State₁) := by
-    simp [leftCfg, Cfg.mapState, hq]
-  rw [step_of_state h1, step_of_state hq]
-  simp only [seq, tr_ofTr]
-  rfl
-
-lemma step_rightCfg (cfg : Cfg k Symbol State₁ input) :
-    (tm₀.seq tm₁).step (rightCfg cfg) = rightCfg (tm₁.step cfg) := by
-  cases hq : cfg.state with
-  | none =>
-    have h1 : (rightCfg (State₀ := State₀) cfg).state = none := by simp [rightCfg, Cfg.mapState, hq]
-    rw [step_of_halt h1, step_of_halt hq]
-  | some q =>
-    have h1 : (rightCfg (State₀ := State₀) cfg).state = some (Sum.inr q : State₀ ⊕ State₁) := by
-      simp [rightCfg, hq]
-    rw [step_of_state h1, step_of_state hq]
-    simp only [seq, tr_ofTr]
-    rfl
-
-@[simp]
-lemma forgetState_leftCfg (cfg : Cfg k Symbol State₀ input) :
-    (leftCfg tm₁ cfg).forgetState = cfg.forgetState := rfl
-
-@[simp]
-lemma forgetState_rightCfg (cfg : Cfg k Symbol State₁ input) :
-    (rightCfg (State₀ := State₀) cfg).forgetState = cfg.forgetState := rfl
+/-- The first phase of `seq tm₀ tm₁` mirrors the running steps of `tm₀`. -/
+@[simps! apply]
+noncomputable def leftCfgHom : (tm₀.runningStepRel input).Hom ((tm₀.seq tm₁).stepRel input) :=
+  wire.follows_left.runningStepHom (leftCfg tm₁.q₀)
+    (fun _ _ => congrArg (leftState tm₁.q₀)) (fun _ => rfl) fun _ _ => rfl
+
+/-- The second phase of `seq tm₀ tm₁` mirrors the steps of `tm₁`. -/
+@[simps! apply]
+noncomputable def rightCfgHom : (tm₁.stepRel input).Hom ((tm₀.seq tm₁).stepRel input) :=
+  wire.follows_right.stepHom rightCfg (fun _ => rfl) (fun _ => rfl) fun _ _ => rfl
 
 /-- A halted configuration of the first phase is the start of the second phase. -/
-lemma leftCfg_of_halt {cfg : Cfg k Symbol State₀ input} (h : cfg.state = none) :
-    leftCfg tm₁ cfg = rightCfg (cfg.withState (some tm₁.q₀)) := by
-  simp [leftCfg, rightCfg, Cfg.withState, Cfg.mapState, h]
+lemma leftCfg_of_halt {q₁ : State₁} {cfg : Cfg k Symbol State₀ input} (h : cfg.state = none) :
+    leftCfg q₁ cfg = rightCfg (cfg.withState (some q₁)) := by
+  simp [leftCfg, leftState, rightCfg, Cfg.withState, Cfg.mapState, h]
 
 end Sequential
 
 open Sequential in
-/-- **Sequential composition of runs.** A run path of `tm₀` to a halted configuration, followed by a
-run path of `tm₁` to a halted configuration started where `tm₀` halted, gives a run path of `seq`
-of at most as many steps, whose configurations are those of the two paths up to their states. -/
+/-- **Sequential composition of runs.** A run path of `tm₀` to a halted configuration and a run path
+of `tm₁` started where `tm₀` halted combine into a run path of `seq`: the first path up to its first
+halted configuration, followed by the second. It takes at most as many steps as the two paths
+together, and visits only cells that they visit. -/
 theorem exists_runPath_seq {p₀ : tm₀.RunPath input} (h₀ : p₀.last.Halted)
-    {p₁ : tm₁.RunPath input} (h₁ : p₁.head = p₀.last.withState (some tm₁.q₀))
-    (hp₁ : p₁.last.Halted) :
-    ∃ p : (tm₀.seq tm₁).RunPath input, p.head = leftCfg tm₁ p₀.head ∧
+    {p₁ : tm₁.RunPath input} (h₁ : p₁.head = p₀.last.withState (some tm₁.q₀)) :
+    ∃ p : (tm₀.seq tm₁).RunPath input, p.head = leftCfg tm₁.q₀ p₀.head ∧
       p.last = rightCfg p₁.last ∧ p.length ≤ p₀.length + p₁.length ∧
-      ∀ c ∈ p, (∃ c₀ ∈ p₀, c.forgetState = c₀.forgetState) ∨
-        ∃ c₁ ∈ p₁, c.forgetState = c₁.forgetState := by
-  -- `seq` takes the running steps of `tm₀`, then those of `tm₁`
+      ∀ i, p.visitedByTapeHead i ⊆ p₀.visitedByTapeHead i ∪ p₁.visitedByTapeHead i := by
+  -- `seq` takes the running steps of `tm₀`, then the steps of `tm₁`
   obtain ⟨q₀, hh₀, hl₀, hlen₀, hmem₀⟩ := p₀.exists_running h₀
-  obtain ⟨q₁, hh₁, hl₁, hlen₁, hmem₁⟩ := p₁.exists_running hp₁
-  let f₀ := runningStepHom (tm' := tm₀.seq tm₁) (input := input) (leftCfg tm₁) step_leftCfg
-  let f₁ := runningStepHom (tm' := tm₀.seq tm₁) (input := input) rightCfg
-    fun c _ => step_rightCfg c
-  refine ⟨(q₀.map f₀).smash (q₁.map f₁) (by simp [f₀, f₁, hl₀, hh₁, h₁, leftCfg_of_halt h₀]),
-    by simp [f₀, hh₀], by simp [f₁, hl₁], by simp; lia, fun c hc => ?_⟩
+  refine ⟨(q₀.map leftCfgHom).smash (p₁.map rightCfgHom)
+    (by simp [hl₀, h₁, leftCfg_of_halt h₀]), by simp [hh₀], by simp, by simp; lia,
+    fun i z hz => ?_⟩
+  obtain ⟨c, hc, rfl⟩ := (MultiTapeNTM.RunPath.mem_visitedByTapeHead _).mp hz
   rcases RelSeries.mem_or_mem_of_mem_smash hc with hc | hc <;>
     obtain ⟨c', hc', rfl⟩ := RelSeries.exists_of_mem_map hc
-  · exact .inl ⟨c', hmem₀ c' hc', rfl⟩
-  · exact .inr ⟨c', hmem₁ c' hc', rfl⟩
+  · exact Finset.mem_union_left _ (p₀.mem_visitedByTapeHead.mpr ⟨c', hmem₀ c' hc', rfl⟩)
+  · exact Finset.mem_union_right _ (p₁.mem_visitedByTapeHead.mpr ⟨c', hc', rfl⟩)
 
 open Sequential in
 /-- **Sequential composition of transformations.** If the postcondition of the first
@@ -147,18 +123,12 @@ theorem transformsTapes_seq
   obtain ⟨ws', e₀, hQ₀, p₀, hh₀, hl₀, ht₀, hs₀⟩ := h₀ input ws out hP₀
   obtain ⟨ws'', e₁, hQ₁, p₁, hh₁, hl₁, ht₁, hs₁⟩ :=
     h₁ input ws' (out ++ e₀) (hmid input ws ws' e₀ hP₀ hQ₀)
-  obtain ⟨p, hh, hl, ht, hmem⟩ := exists_runPath_seq (p₀ := p₀) (p₁ := p₁) (by rw [hl₀]; rfl)
-    (by simp [hh₁, hl₀]) (by rw [hl₁]; rfl)
-  refine ⟨ws'', e₀ ++ e₁, ⟨ws', e₀, e₁, hQ₀, hQ₁, rfl⟩, p, by simp [hh, hh₀, leftCfg]; rfl,
-    by simp [hl, hl₁, rightCfg], ht.trans (Nat.add_le_add ht₀ ht₁), ?_⟩
-  -- every head position of the composed run is one of the first path or one of the second
-  refine (p.space_le_sum_card
-    (S := fun i => p₀.visitedByTapeHead i ∪ p₁.visitedByTapeHead i) fun c hc i => ?_).trans
-    (((Finset.sum_le_sum fun i _ => Finset.card_union_le _ _).trans_eq
-      Finset.sum_add_distrib).trans (Nat.add_le_add hs₀ hs₁))
-  rcases hmem c hc with ⟨_, ⟨n, rfl⟩, he⟩ | ⟨_, ⟨n, rfl⟩, he⟩ <;>
-    rw [show c.workTapePos i = _ from congrArg (·.workTapePos i) he]
-  · exact Finset.mem_union_left _ (Finset.mem_image_of_mem _ (Finset.mem_univ n))
-  · exact Finset.mem_union_right _ (Finset.mem_image_of_mem _ (Finset.mem_univ n))
+  obtain ⟨p, hh, hl, ht, hvisited⟩ := exists_runPath_seq (p₀ := p₀) (p₁ := p₁)
+    (by rw [hl₀]; rfl) (by simp [hh₁, hl₀])
+  -- the composed run visits only cells that one of the two runs visits
+  exact ⟨ws'', e₀ ++ e₁, ⟨ws', e₀, e₁, hQ₀, hQ₁, rfl⟩, p, by simp [hh, hh₀, leftCfg]; rfl,
+    by simp [hl, hl₁, rightCfg], ht.trans (Nat.add_le_add ht₀ ht₁),
+    ((Finset.sum_le_sum fun i _ => (Finset.card_le_card (hvisited i)).trans
+      (Finset.card_union_le _ _)).trans_eq Finset.sum_add_distrib).trans (Nat.add_le_add hs₀ hs₁)⟩
 
 end Turing.MultiTapeTM