Body machine: step reduction

The single lemma every phase proof of the body correctness uses: bodyTM.step on a non-halted configuration, when the transition arm is a mkAct (they all are, by bodyδ_shape), produces the configuration whose work tapes act per acts, whose real input idles, and whose real output write-backs — in closed form.

theorem Complexity.TM.UTMBody.step_mkAct {c : Cfg 6 bodyTM.Q} (hne : c.state ≠ BodyQ.bodyDone) {q' : BodyQ} {acts : TapeActs} (h : bodyδ c.state c.input.read (fun (i : Fin 6) => (c.work i).read) c.output.read = mkAct q' c.input.read (fun (i : Fin 6) => (c.work i).read) c.output.read acts) : bodyTM.step c = some { state := q', input := c.input.move (idleDir c.input.read), work := fun (i : Fin 6) => match acts i with | some (w, d) => (c.work i).writeAndMove w.toΓ (if (c.work i).read = Γ.start then Dir3.right else d) | none => (c.work i).writeAndMove (readBackWrite (c.work i).read).toΓ (idleDir (c.work i).read), output := c.output.writeAndMove (readBackWrite c.output.read).toΓ (idleDir c.output.read) }

Closed form of one bodyTM step whose transition arm is mkAct q' acts (every arm is — bodyδ_shape). The real input tape idle-moves, the real output tape write-backs and idle-moves, and work tape i performs acts i (with the ▷ ⇒ right sanitization) or idles.

theorem Complexity.TM.UTMBody.idle_tape_id {t : Tape} (h : t.read ≠ Γ.start) : t.writeAndMove (readBackWrite t.read).toΓ (idleDir t.read) = t

An idle work tape is exactly preserved by a mkAct step when it reads a non-▷ symbol (its action is precisely transitionTape).

theorem Complexity.TM.UTMBody.idle_input_id {t : Tape} (h : t.read ≠ Γ.start) : t.move (idleDir t.read) = t

The idled real input tape is exactly preserved when reading non-▷.

theorem Complexity.TM.UTMBody.step_act1 {c : Cfg 6 bodyTM.Q} (hne : c.state ≠ BodyQ.bodyDone) {q' : BodyQ} {t : Fin 6} {w : Γw} {d : Dir3} (h : bodyδ c.state c.input.read (fun (i : Fin 6) => (c.work i).read) c.output.read = act1 q' c.input.read (fun (i : Fin 6) => (c.work i).read) c.output.read t w d) : bodyTM.step c = some { state := q', input := c.input.move (idleDir c.input.read), work := fun (i : Fin 6) => if i = t then (c.work i).writeAndMove w.toΓ (if (c.work i).read = Γ.start then Dir3.right else d) else (c.work i).writeAndMove (readBackWrite (c.work i).read).toΓ (idleDir (c.work i).read), output := c.output.writeAndMove (readBackWrite c.output.read).toΓ (idleDir c.output.read) }

Closed form of a step whose arm is act1 (one active tape).

theorem Complexity.TM.UTMBody.step_act2 {c : Cfg 6 bodyTM.Q} (hne : c.state ≠ BodyQ.bodyDone) {q' : BodyQ} {t₁ t₂ : Fin 6} {w₁ w₂ : Γw} {d₁ d₂ : Dir3} (h : bodyδ c.state c.input.read (fun (i : Fin 6) => (c.work i).read) c.output.read = act2 q' c.input.read (fun (i : Fin 6) => (c.work i).read) c.output.read t₁ w₁ d₁ t₂ w₂ d₂) : bodyTM.step c = some { state := q', input := c.input.move (idleDir c.input.read), work := fun (i : Fin 6) => if i = t₁ then (c.work i).writeAndMove w₁.toΓ (if (c.work i).read = Γ.start then Dir3.right else d₁) else if i = t₂ then (c.work i).writeAndMove w₂.toΓ (if (c.work i).read = Γ.start then Dir3.right else d₂) else (c.work i).writeAndMove (readBackWrite (c.work i).read).toΓ (idleDir (c.work i).read), output := c.output.writeAndMove (readBackWrite c.output.read).toΓ (idleDir c.output.read) }

Closed form of a step whose arm is act2 (two active tapes).

theorem Complexity.TM.UTMBody.step_act3 {c : Cfg 6 bodyTM.Q} (hne : c.state ≠ BodyQ.bodyDone) {q' : BodyQ} {t₁ t₂ t₃ : Fin 6} {w₁ w₂ w₃ : Γw} {d₁ d₂ d₃ : Dir3} (h : bodyδ c.state c.input.read (fun (i : Fin 6) => (c.work i).read) c.output.read = act3 q' c.input.read (fun (i : Fin 6) => (c.work i).read) c.output.read t₁ w₁ d₁ t₂ w₂ d₂ t₃ w₃ d₃) : bodyTM.step c = some { state := q', input := c.input.move (idleDir c.input.read), work := fun (i : Fin 6) => if i = t₁ then (c.work i).writeAndMove w₁.toΓ (if (c.work i).read = Γ.start then Dir3.right else d₁) else if i = t₂ then (c.work i).writeAndMove w₂.toΓ (if (c.work i).read = Γ.start then Dir3.right else d₂) else if i = t₃ then (c.work i).writeAndMove w₃.toΓ (if (c.work i).read = Γ.start then Dir3.right else d₃) else (c.work i).writeAndMove (readBackWrite (c.work i).read).toΓ (idleDir (c.work i).read), output := c.output.writeAndMove (readBackWrite c.output.read).toΓ (idleDir c.output.read) }

Closed form of a step whose arm is act3 (three active tapes).

theorem Complexity.TM.UTMBody.rewStep_loop {cur next : BodyQ} {t : Fin 6} (hcur : cur ≠ BodyQ.bodyDone) (hδ : ∀ (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ), bodyδ cur iH wH oH = rewStep cur next iH wH oH t) (W : ℕ → Γ) (hW0 : W 0 = Γ.start) (hWns : ∀ (j : ℕ), 1 ≤ j → W j ≠ Γ.start) (p : ℕ) (c : Cfg 6 bodyTM.Q) : c.state = cur → (c.work t).cells = W → (c.work t).head = p → c.input.read ≠ Γ.start → c.output.read ≠ Γ.start → (∀ (i : Fin 6), i ≠ t → (c.work i).read ≠ Γ.start) → ∃ (c' : Cfg 6 bodyTM.Q), bodyTM.reachesIn (p + 1) c c' ∧ c'.state = next ∧ c'.work t = { head := 1, cells := W } ∧ c'.input = c.input ∧ c'.output = c.output ∧ ∀ (i : Fin 6), i ≠ t → c'.work i = c.work i

Generic rewind loop for any pair of states whose transition is rewStep cur next · t: from state cur with work-tape-t head at p (cells W, well-formed), reach state next with head 1 in p + 1 steps; tape t's cells and every other tape are exactly preserved.

theorem Complexity.TM.UTMBody.blankRewStep_loop {cur next : BodyQ} {t : Fin 6} (hcur : cur ≠ BodyQ.bodyDone) (hδ : ∀ (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ), bodyδ cur iH wH oH = blankRewStep cur next iH wH oH t) (p : ℕ) (W : ℕ → Γ) : W 0 = Γ.start → (∀ (j : ℕ), 1 ≤ j → W j ≠ Γ.start) → ∀ (c : Cfg 6 bodyTM.Q), c.state = cur → (c.work t).cells = W → (c.work t).head = p → c.input.read ≠ Γ.start → c.output.read ≠ Γ.start → (∀ (i : Fin 6), i ≠ t → (c.work i).read ≠ Γ.start) → ∃ (c' : Cfg 6 bodyTM.Q), bodyTM.reachesIn (p + 1) c c' ∧ c'.state = next ∧ c'.work t = { head := 1, cells := fun (j : ℕ) => if 1 ≤ j ∧ j ≤ p then Γ.blank else W j } ∧ c'.input = c.input ∧ c'.output = c.output ∧ ∀ (i : Fin 6), i ≠ t → c'.work i = c.work i

Generic blank-rewind loop for any pair of states whose transition is blankRewStep cur next · t: from state cur with work-tape-t head at p, reach state next with head 1 in p + 1 steps, with cells 1..p blanked; every other tape exactly preserved.

theorem Complexity.TM.UTMBody.scanRight_loop {cur next : BodyQ} {t : Fin 6} (hcur : cur ≠ BodyQ.bodyDone) (hδ : ∀ (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ), bodyδ cur iH wH oH = act1 (if wH t = Γ.blank then next else cur) iH wH oH t (readBackWrite (wH t)) Dir3.right) (W : ℕ → Γ) (hWns : ∀ (j : ℕ), 1 ≤ j → W j ≠ Γ.start) (k h : ℕ) : 1 ≤ h → (∀ j < k, W (h + j) ≠ Γ.blank) → W (h + k) = Γ.blank → ∀ (c : Cfg 6 bodyTM.Q), c.state = cur → (c.work t).cells = W → (c.work t).head = h → c.input.read ≠ Γ.start → c.output.read ≠ Γ.start → (∀ (i : Fin 6), i ≠ t → (c.work i).read ≠ Γ.start) → ∃ (c' : Cfg 6 bodyTM.Q), bodyTM.reachesIn (k + 1) c c' ∧ c'.state = next ∧ c'.work t = { head := h + k + 1, cells := W } ∧ c'.input = c.input ∧ c'.output = c.output ∧ ∀ (i : Fin 6), i ≠ t → c'.work i = c.work i

Generic scan-right loop for any pair of states whose transition is act1 (if □ then next else cur) · t readBack right — the machine walks right to the first □ and steps past it. k is the distance to that □. Cells are preserved exactly; every other tape untouched.

theorem Complexity.TM.UTMBody.arm_haltRewS (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) : bodyδ BodyQ.haltRewS iH wH oH = rewStep BodyQ.haltRewS BodyQ.haltRewD iH wH oH stT

theorem Complexity.TM.UTMBody.arm_haltRewD (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) : bodyδ BodyQ.haltRewD iH wH oH = rewStep BodyQ.haltRewD BodyQ.bodyDone iH wH oH dsT

theorem Complexity.TM.UTMBody.arm_preRewS (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) : bodyδ BodyQ.preRewS iH wH oH = rewStep BodyQ.preRewS BodyQ.preRewD iH wH oH stT

theorem Complexity.TM.UTMBody.arm_preRewD (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) : bodyδ BodyQ.preRewD iH wH oH = rewStep BodyQ.preRewD BodyQ.peek1 iH wH oH dsT

theorem Complexity.TM.UTMBody.arm_rewindSt (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (f : VFlags) : bodyδ (BodyQ.rewindSt f) iH wH oH = rewStep (BodyQ.rewindSt f) (BodyQ.cmpQ f) iH wH oH stT

theorem Complexity.TM.UTMBody.arm_appRewScr (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (f : VFlags) : bodyδ (BodyQ.appRewScr f) iH wH oH = rewStep (BodyQ.appRewScr f) (BodyQ.appQ' f) iH wH oH scT

theorem Complexity.TM.UTMBody.arm_dfStRew (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) : bodyδ BodyQ.dfStRew iH wH oH = rewStep BodyQ.dfStRew BodyQ.dfBlank iH wH oH stT

theorem Complexity.TM.UTMBody.arm_dfStRew2 (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) : bodyδ BodyQ.dfStRew2 iH wH oH = rewStep BodyQ.dfStRew2 BodyQ.dfDescRew iH wH oH stT

theorem Complexity.TM.UTMBody.arm_dfDescRew (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) : bodyδ BodyQ.dfDescRew iH wH oH = rewStep BodyQ.dfDescRew BodyQ.dfSkip iH wH oH dsT

theorem Complexity.TM.UTMBody.arm_dfStRew3 (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) : bodyδ BodyQ.dfStRew3 iH wH oH = rewStep BodyQ.dfStRew3 BodyQ.dfDescRew2 iH wH oH stT

theorem Complexity.TM.UTMBody.arm_dfDescRew2 (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) : bodyδ BodyQ.dfDescRew2 iH wH oH = rewStep BodyQ.dfDescRew2 BodyQ.bodyDone iH wH oH dsT

theorem Complexity.TM.UTMBody.arm_clSt (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) : bodyδ BodyQ.clSt iH wH oH = rewStep BodyQ.clSt BodyQ.clDesc iH wH oH stT

theorem Complexity.TM.UTMBody.arm_clDesc (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) : bodyδ BodyQ.clDesc iH wH oH = rewStep BodyQ.clDesc BodyQ.bodyDone iH wH oH dsT

theorem Complexity.TM.UTMBody.arm_mmScr (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (f : VFlags) : bodyδ (BodyQ.mmScr f) iH wH oH = blankRewStep (BodyQ.mmScr f) (BodyQ.rewindSt f) iH wH oH scT

theorem Complexity.TM.UTMBody.arm_dfScr (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) : bodyδ BodyQ.dfScr iH wH oH = blankRewStep BodyQ.dfScr BodyQ.dfStRew iH wH oH scT

theorem Complexity.TM.UTMBody.arm_clScr (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) : bodyδ BodyQ.clScr iH wH oH = blankRewStep BodyQ.clScr BodyQ.clSt iH wH oH scT

theorem Complexity.TM.UTMBody.arm_hc0 (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) : bodyδ BodyQ.hc0 iH wH oH = act1 (if wH dsT = Γ.blank then BodyQ.hc1 else BodyQ.hc0) iH wH oH dsT (readBackWrite (wH dsT)) Dir3.right

theorem Complexity.TM.UTMBody.arm_seek1 (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (f : VFlags) : bodyδ (BodyQ.seek1 f) iH wH oH = act1 (if wH dsT = Γ.blank then BodyQ.seek2 f else BodyQ.seek1 f) iH wH oH dsT (readBackWrite (wH dsT)) Dir3.right

theorem Complexity.TM.UTMBody.arm_seek2 (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (f : VFlags) : bodyδ (BodyQ.seek2 f) iH wH oH = act1 (if wH dsT = Γ.blank then BodyQ.cmpQ f else BodyQ.seek2 f) iH wH oH dsT (readBackWrite (wH dsT)) Dir3.right

theorem Complexity.TM.UTMBody.arm_skipSeg (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (f : VFlags) : bodyδ (BodyQ.skipSeg f) iH wH oH = act1 (if wH dsT = Γ.blank then BodyQ.segCheck f else BodyQ.skipSeg f) iH wH oH dsT (readBackWrite (wH dsT)) Dir3.right

theorem Complexity.TM.UTMBody.arm_dfSkip (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) : bodyδ BodyQ.dfSkip iH wH oH = act1 (if wH dsT = Γ.blank then BodyQ.dfCopy else BodyQ.dfSkip) iH wH oH dsT (readBackWrite (wH dsT)) Dir3.right

theorem Complexity.TM.UTMBody.arm_hc1 (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) : bodyδ BodyQ.hc1 iH wH oH = if wH stT = Γ.blank ∧ wH dsT = Γ.blank then idle BodyQ.haltRewS iH wH oH else if wH stT ≠ Γ.blank ∧ wH dsT ≠ Γ.blank ∧ wH stT = wH dsT then act2 BodyQ.hc1 iH wH oH stT (readBackWrite (wH stT)) Dir3.right dsT (readBackWrite (wH dsT)) Dir3.right else idle BodyQ.preRewS iH wH oH

theorem Complexity.TM.UTMBody.arm_peek1 (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) : bodyδ BodyQ.peek1 iH wH oH = act3 BodyQ.peek2 iH wH oH vIn (readBackWrite (wH vIn)) Dir3.left vWk (readBackWrite (wH vWk)) Dir3.left vOut (readBackWrite (wH vOut)) Dir3.left

theorem Complexity.TM.UTMBody.arm_peek2 (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) : bodyδ BodyQ.peek2 iH wH oH = act3 (BodyQ.seek1 (decide (wH vIn = Γ.start), decide (wH vWk = Γ.start), decide (wH vOut = Γ.start))) iH wH oH vIn (readBackWrite (wH vIn)) Dir3.right vWk (readBackWrite (wH vWk)) Dir3.right vOut (readBackWrite (wH vOut)) Dir3.right

theorem Complexity.TM.UTMBody.arm_cmpQ (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (f : VFlags) : bodyδ (BodyQ.cmpQ f) iH wH oH = if wH stT = Γ.blank then idle (BodyQ.cmpS f 0) iH wH oH else if wH dsT ≠ Γ.blank ∧ wH stT = wH dsT then act2 (BodyQ.cmpQ f) iH wH oH stT (readBackWrite (wH stT)) Dir3.right dsT (readBackWrite (wH dsT)) Dir3.right else idle (BodyQ.skipSeg f) iH wH oH

theorem Complexity.TM.UTMBody.arm_cmpS (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (f : VFlags) (idx : Fin 6) : bodyδ (BodyQ.cmpS f idx) iH wH oH = if wH dsT = keyCell f (wH vIn) (wH vWk) (wH vOut) idx ∧ wH dsT ≠ Γ.blank then if h : ↑idx < 5 then act1 (BodyQ.cmpS f ⟨↑idx + 1, ⋯⟩) iH wH oH dsT (readBackWrite (wH dsT)) Dir3.right else act2 (BodyQ.copyQ' f) iH wH oH dsT (readBackWrite (wH dsT)) Dir3.right stT (readBackWrite (wH stT)) Dir3.left else idle (BodyQ.skipSeg f) iH wH oH

theorem Complexity.TM.UTMBody.arm_copyQ' (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (f : VFlags) : bodyδ (BodyQ.copyQ' f) iH wH oH = if wH stT = Γ.start then act1 (BodyQ.copyAct f 0) iH wH oH stT (readBackWrite (wH stT)) Dir3.right else if wH dsT = Γ.blank then idle (BodyQ.skipSeg f) iH wH oH else act3 (BodyQ.copyQ' f) iH wH oH scT (readBackWrite (wH dsT)) Dir3.right dsT (readBackWrite (wH dsT)) Dir3.right stT (readBackWrite (wH stT)) Dir3.left

theorem Complexity.TM.UTMBody.arm_copyAct (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (f : VFlags) (j : Fin 10) : bodyδ (BodyQ.copyAct f j) iH wH oH = if wH dsT = Γ.blank then idle (BodyQ.skipSeg f) iH wH oH else act2 (if h : ↑j < 9 then BodyQ.copyAct f ⟨↑j + 1, ⋯⟩ else BodyQ.appRewScr f) iH wH oH scT (readBackWrite (wH dsT)) Dir3.right dsT (readBackWrite (wH dsT)) Dir3.right

theorem Complexity.TM.UTMBody.arm_segCheck (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (f : VFlags) : bodyδ (BodyQ.segCheck f) iH wH oH = if wH dsT = Γ.blank then act3 BodyQ.dfScr iH wH oH vIn (readBackWrite (wH vIn)) (if f.1 = true then Dir3.right else Dir3.stay) vWk (readBackWrite (wH vWk)) (if f.2.1 = true then Dir3.right else Dir3.stay) vOut (readBackWrite (wH vOut)) (if f.2.2 = true then Dir3.right else Dir3.stay) else idle (BodyQ.mmScr f) iH wH oH

theorem Complexity.TM.UTMBody.arm_appQ' (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (f : VFlags) : bodyδ (BodyQ.appQ' f) iH wH oH = if wH stT = Γ.blank then idle (BodyQ.appAct f 0 none) iH wH oH else act2 (BodyQ.appQ' f) iH wH oH stT (readBackWrite (wH scT)) Dir3.right scT (readBackWrite (wH scT)) Dir3.right

theorem Complexity.TM.UTMBody.arm_appAct_none (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (f : VFlags) (g : Fin 5) : bodyδ (BodyQ.appAct f g none) iH wH oH = act1 (BodyQ.appAct f g (some (cellBit (wH scT)))) iH wH oH scT (readBackWrite (wH scT)) Dir3.right

theorem Complexity.TM.UTMBody.arm_appAct0 (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (f : VFlags) (b₀ : Bool) : bodyδ (BodyQ.appAct f 0 (some b₀)) iH wH oH = act2 (BodyQ.appAct f 1 none) iH wH oH scT (readBackWrite (wH scT)) Dir3.right vWk (if f.2.1 = true then Γw.blank else grpΓw b₀ (cellBit (wH scT))) Dir3.stay

theorem Complexity.TM.UTMBody.arm_appAct1 (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (f : VFlags) (b₀ : Bool) : bodyδ (BodyQ.appAct f 1 (some b₀)) iH wH oH = act2 (BodyQ.appAct f 2 none) iH wH oH scT (readBackWrite (wH scT)) Dir3.right vOut (if f.2.2 = true then Γw.blank else grpΓw b₀ (cellBit (wH scT))) Dir3.stay

theorem Complexity.TM.UTMBody.arm_appAct2 (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (f : VFlags) (b₀ : Bool) : bodyδ (BodyQ.appAct f 2 (some b₀)) iH wH oH = act2 (BodyQ.appAct f 3 none) iH wH oH scT (readBackWrite (wH scT)) Dir3.right vIn (readBackWrite (wH vIn)) (if f.1 = true then Dir3.right else grpDir b₀ (cellBit (wH scT)))

theorem Complexity.TM.UTMBody.arm_appAct3 (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (f : VFlags) (b₀ : Bool) : bodyδ (BodyQ.appAct f 3 (some b₀)) iH wH oH = act2 (BodyQ.appAct f 4 none) iH wH oH scT (readBackWrite (wH scT)) Dir3.right vWk (readBackWrite (wH vWk)) (if f.2.1 = true then Dir3.right else grpDir b₀ (cellBit (wH scT)))

theorem Complexity.TM.UTMBody.arm_appAct4 (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) (f : VFlags) (b₀ : Bool) : bodyδ (BodyQ.appAct f 4 (some b₀)) iH wH oH = act2 BodyQ.clScr iH wH oH scT (readBackWrite (wH scT)) Dir3.right vOut (readBackWrite (wH vOut)) (if f.2.2 = true then Dir3.right else grpDir b₀ (cellBit (wH scT)))

theorem Complexity.TM.UTMBody.arm_dfBlank (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) : bodyδ BodyQ.dfBlank iH wH oH = if wH stT = Γ.blank then idle BodyQ.dfStRew2 iH wH oH else act1 BodyQ.dfBlank iH wH oH stT Γw.blank Dir3.right

theorem Complexity.TM.UTMBody.arm_dfCopy (iH : Γ) (wH : Fin 6 → Γ) (oH : Γ) : bodyδ BodyQ.dfCopy iH wH oH = if wH dsT = Γ.blank then idle BodyQ.dfStRew3 iH wH oH else act2 BodyQ.dfCopy iH wH oH stT (readBackWrite (wH dsT)) Dir3.right dsT (readBackWrite (wH dsT)) Dir3.right

theorem Complexity.TM.UTMBody.dfBlank_loop (k : ℕ) (W : ℕ → Γ) : (∀ (j : ℕ), 1 ≤ j → W j ≠ Γ.start) → ∀ (h : ℕ), 1 ≤ h → (∀ j < k, W (h + j) ≠ Γ.blank) → W (h + k) = Γ.blank → ∀ (c : Cfg 6 bodyTM.Q), c.state = BodyQ.dfBlank → (c.work stT).cells = W → (c.work stT).head = h → c.input.read ≠ Γ.start → c.output.read ≠ Γ.start → (∀ (i : Fin 6), i ≠ stT → (c.work i).read ≠ Γ.start) → ∃ (c' : Cfg 6 bodyTM.Q), bodyTM.reachesIn (k + 1) c c' ∧ c'.state = BodyQ.dfStRew2 ∧ c'.work stT = { head := h + k, cells := fun (j : ℕ) => if h ≤ j ∧ j < h + k then Γ.blank else W j } ∧ c'.input = c.input ∧ c'.output = c.output ∧ ∀ (i : Fin 6), i ≠ stT → c'.work i = c.work i

The default path's state-tape blanking: from dfBlank with the state head at h ≥ 1 and the first □ at distance k, blank cells h..h+k-1 and stop on the □ (head at h + k, one idle transition step) in k + 1 steps. All other tapes exactly preserved.

theorem Complexity.TM.UTMBody.dfCopy_loop (W : ℕ → Γ) (hWns : ∀ (j : ℕ), 1 ≤ j → W j ≠ Γ.start) (k : ℕ) (V : ℕ → Γ) : (∀ (j : ℕ), 1 ≤ j → V j ≠ Γ.start) → ∀ (a b : ℕ), 1 ≤ a → 1 ≤ b → (∀ j < k, W (b + j) ≠ Γ.blank) → W (b + k) = Γ.blank → ∀ (c : Cfg 6 bodyTM.Q), c.state = BodyQ.dfCopy → (c.work stT).cells = V → (c.work stT).head = a → (c.work dsT).cells = W → (c.work dsT).head = b → c.input.read ≠ Γ.start → c.output.read ≠ Γ.start → (∀ (i : Fin 6), i ≠ stT → i ≠ dsT → (c.work i).read ≠ Γ.start) → ∃ (c' : Cfg 6 bodyTM.Q), bodyTM.reachesIn (k + 1) c c' ∧ c'.state = BodyQ.dfStRew3 ∧ c'.work stT = { head := a + k, cells := fun (j : ℕ) => if a ≤ j ∧ j < a + k then W (b + (j - a)) else V j } ∧ c'.work dsT = { head := b + k, cells := W } ∧ c'.input = c.input ∧ c'.output = c.output ∧ ∀ (i : Fin 6), i ≠ stT → i ≠ dsT → c'.work i = c.work i

The default path's qhalt-field copy: from dfCopy with the state head at a ≥ 1 and the desc head at b ≥ 1, where the desc field ends at distance k (first □), copy the field onto state cells a..a+k-1 and stop (one idle transition on the □) in k + 1 steps. Desc cells and all other tapes exactly preserved.