The UTM halt test machine

haltTestTM : TM 6 compares the state tape (work tape 3) against the description's second field (the qhalt field of the desc tape, work tape 4) and writes the verdict to output cell 1: Γ.one on match, Γ.zero on mismatch. Both tape heads are rewound to cell 1 before halting.

Phases (from qstart = .skip):

• A (skip) — move the desc head right past the first field and its separator (□), landing on the first cell of the qhalt field;
• B (compare) — lockstep compare of state head vs desc head: both □ simultaneously ⇒ match; any difference ⇒ mismatch;
• C (verdict) — one step: write Γ.one/Γ.zero at output cell 1 (output head stays at 1);
• D (rewind) — rewind the state head to cell 1, then the desc head to cell 1, then halt.

The machine writes readBackWrite on every work tape at every step, so no work-tape cell is ever changed; tapes 3 and 4 are restored exactly (same head, same cells), and all other tapes are untouched.

Main results

• TM.haltTestTM_hoareTime — full HoareTime specification with ghost initial tapes, verdict Γ.one iff stSyms = (takeField (takeField dSyms).2).1, in time 2·|dSyms| + 2·|stSyms| + 12.

takeField connection: the desc tape holds dSyms (Tape.HoldsExact); cells beyond the content read Γ.blank, indistinguishable from an in-content Γw.blank — and takeField semantics agrees, by design. The stSyms blank-freeness hypothesis is required: a □ inside stSyms would truncate the machine's comparison at that point while stSyms as a list extends beyond it (and takeField fields are always blank-free). The UTM state tape holds bit symbols only, so this is no restriction in use.

theorem Complexity.takeField_fst_ne_blank (l : List Γw) (s : Γw) : s ∈ (takeField l).1 → s ≠ Γw.blank

The first field produced by takeField is blank-free.

theorem Complexity.takeField_structure (l : List Γw) : l = (takeField l).1 ++ Γw.blank :: (takeField l).2 ∨ (takeField l).1 = l ∧ (takeField l).2 = []

takeField decomposition: either the input splits as field ++ □ :: rest, or it contains no separator and the field is the whole input.

inductive Complexity.TM.HaltTestPhase : Type

Control states of haltTestTM.

• skip : HaltTestPhase
• compare : HaltTestPhase
• writeOne : HaltTestPhase
• writeZero : HaltTestPhase
• rewindSt : HaltTestPhase
• rewindD : HaltTestPhase
• done : HaltTestPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqHaltTestPhase : DecidableEq HaltTestPhase

Equations

• Complexity.TM.instDecidableEqHaltTestPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.TM.instFintypeHaltTestPhase : Fintype HaltTestPhase

Equations

• One or more equations did not get rendered due to their size.

def Complexity.TM.haltTestTM : TM 6

The UTM halt test: skip the first desc field, compare the state tape (work tape 3) with the second desc field (work tape 4), write the verdict to output cell 1, rewind both heads to cell 1, halt.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.TM.haltTestTM_hoareTime (stSyms dSyms : List Γw) (hstnb : ∀ s ∈ stSyms, s ≠ Γw.blank) (inp₀ : Tape) (work₀ : Fin 6 → Tape) (out₀ : Tape) (hst : (work₀ 3).HoldsExact stSyms) (hsth : (work₀ 3).head = 1) (hd : (work₀ 4).HoldsExact dSyms) (hdh : (work₀ 4).head = 1) (_hout0 : out₀.cells 0 = Γ.start) (houtns : ∀ (j : ℕ), 1 ≤ j → out₀.cells j ≠ Γ.start) (houth : out₀.head = 1) (hinp : inp₀.read ≠ Γ.start) (hothers : ∀ (i : Fin 6), i ≠ 3 → i ≠ 4 → (work₀ i).read ≠ Γ.start) : haltTestTM.HoareTime (fun (inp : Tape) (work : Fin 6 → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin 6 → Tape) (out : Tape) => inp = inp₀ ∧ (∀ (i : Fin 6), i ≠ 3 → i ≠ 4 → work i = work₀ i) ∧ work 3 = work₀ 3 ∧ work 4 = work₀ 4 ∧ out.cells = Function.update out₀.cells 1 (if stSyms = (takeField (takeField dSyms).2).1 then Γ.one else Γ.zero) ∧ out.head = 1) (2 * dSyms.length + 2 * stSyms.length + 12)

Halt test specification (ghost-initial-tape style). Starting from qstart where the state tape (work tape 3) holds the blank-free string stSyms and the desc tape (work tape 4) holds dSyms (both heads at cell 1), with the output head resting at cell 1, haltTestTM halts within 2·|dSyms| + 2·|stSyms| + 12 steps having

• written the verdict at output cell 1: Γ.one iff stSyms equals the second field of dSyms (the qhalt field, (takeField (takeField dSyms).2).1), Γ.zero otherwise;
• restored work tapes 3 and 4 exactly (same cells, head back at 1);
• left the input tape, the other four work tapes, all other output cells, and the output head unchanged.