One loopTM iteration that continues

TM.loopTM_iteration_halt traces a single pass through loopTM that ends in the halting branch. The complementary pass — the one where the test says keep going — had no counterpart, which left the indexed loop rule TM.loopTM_hoareTime_indexed without a way to discharge its per-iteration obligation: that obligation asks for a run from the loop's start state back to the loop's start state, and only the check phase's continue branch produces one.

The pass is body, then test, then the rewind of the output tape, then the check. Everything outside the two simulations moves each tape by idleDir and writes back what it read, so on tapes that carry their left marker and are parked past it the whole phase machinery is the identity — which is what makes an invariant on the work tapes survive into the next iteration.

Main results

• TM.loopTM_check_continue_frame — the continue branch of the check phase leaves every tape identical
• TM.loopTM_iteration_continue — a full iteration returning to qstart, tapes and all
• TM.loopTM_check_halt_frame, TM.loopTM_iteration_halt_frame — the halting pass, likewise reporting the tapes it ends on
• TM.loopTM_continue_of_hoare, TM.loopTM_halt_of_hoare — both passes packaged as the two obligations of TM.loopTM_hoareTime_indexed, from a contract for the body and one for the test

theorem Complexity.TM.loopTM_check_continue_frame {n : ℕ} (tmBody tmTest : TM n) (c : Cfg n (LoopQ tmBody.Q tmTest.Q)) (hstate : c.state = Sum.inr (Sum.inl LoopPhase.check)) (hhead : c.output.head = 1) (hcell1 : c.output.cells 1 ≠ Γ.one) (hout : Parked c.output) (hinp : Parked c.input) (hwork : ∀ (i : Fin n), Parked (c.work i)) : ∃ (c' : Cfg n (tmBody.loopTM tmTest).Q), (tmBody.loopTM tmTest).step c = some c' ∧ c'.state = (tmBody.loopTM tmTest).qstart ∧ c'.input = c.input ∧ c'.work = c.work ∧ c'.output = c.output

The continue branch of the check phase, framed. Everything the branch does is write back what it read and move by idleDir, so a tape parked past its left marker is untouched.

theorem Complexity.TM.loopTM_iteration_continue {n : ℕ} (tmBody tmTest : TM n) {t_body : ℕ} {c_body_start c_body_end : Cfg n tmBody.Q} (hreach_body : tmBody.reachesIn t_body c_body_start c_body_end) (hhalt_body : c_body_end.state = tmBody.qhalt) (hinp_body : Parked c_body_end.input) (hwork_body : ∀ (i : Fin n), Parked (c_body_end.work i)) (hout_body : Parked c_body_end.output) {t_test : ℕ} {c_test_end : Cfg n tmTest.Q} (hreach_test : tmTest.reachesIn t_test { state := tmTest.qstart, input := c_body_end.input, work := c_body_end.work, output := c_body_end.output } c_test_end) (hhalt_test : c_test_end.state = tmTest.qhalt) (hinp_test : Parked c_test_end.input) (hwork_test : ∀ (i : Fin n), Parked (c_test_end.work i)) (hout_test : Parked c_test_end.output) (hout0 : c_test_end.output.cells 0 = Γ.start) {p : ℕ} (hp : c_test_end.output.head = p) (hcell1 : c_test_end.output.cells 1 ≠ Γ.one) : ∃ (c_final : Cfg n (tmBody.loopTM tmTest).Q), (tmBody.loopTM tmTest).reachesIn (t_body + 1 + t_test + 1 + (p + 1) + 1) (tmBody.loopBodyWrap tmTest c_body_start) c_final ∧ c_final.state = (tmBody.loopTM tmTest).qstart ∧ c_final.input = c_test_end.input ∧ c_final.work = c_test_end.work ∧ c_final.output.head = 1 ∧ c_final.output.cells = c_test_end.output.cells

One full loopTM iteration that continues. The body runs to its halt state, the test runs to its halt state, the output tape is rewound to cell one, and the verdict cell fails to hold 1 — so the machine returns to its own start state with the test's tapes intact.

The step count matches TM.loopTM_iteration_halt: the two simulations, the two phase transitions between them, the rewind of p + 1 steps, and the check.

theorem Complexity.TM.loopTM_check_halt_frame {n : ℕ} (tmBody tmTest : TM n) (c : Cfg n (LoopQ tmBody.Q tmTest.Q)) (hstate : c.state = Sum.inr (Sum.inl LoopPhase.check)) (hhead : c.output.head = 1) (hcell1 : c.output.cells 1 = Γ.one) (hout : Parked c.output) (hinp : Parked c.input) (hwork : ∀ (i : Fin n), Parked (c.work i)) : ∃ (c' : Cfg n (tmBody.loopTM tmTest).Q), (tmBody.loopTM tmTest).step c = some c' ∧ (tmBody.loopTM tmTest).halted c' ∧ c'.input = c.input ∧ c'.work = c.work ∧ c'.output = c.output

The halting branch of the check phase, framed. As with the continue branch, the step writes back what it read and idles, so parked tapes are untouched.

theorem Complexity.TM.loopTM_iteration_halt_frame {n : ℕ} (tmBody tmTest : TM n) {t_body : ℕ} {c_body_start c_body_end : Cfg n tmBody.Q} (hreach_body : tmBody.reachesIn t_body c_body_start c_body_end) (hhalt_body : c_body_end.state = tmBody.qhalt) (hinp_body : Parked c_body_end.input) (hwork_body : ∀ (i : Fin n), Parked (c_body_end.work i)) (hout_body : Parked c_body_end.output) {t_test : ℕ} {c_test_end : Cfg n tmTest.Q} (hreach_test : tmTest.reachesIn t_test { state := tmTest.qstart, input := c_body_end.input, work := c_body_end.work, output := c_body_end.output } c_test_end) (hhalt_test : c_test_end.state = tmTest.qhalt) (hinp_test : Parked c_test_end.input) (hwork_test : ∀ (i : Fin n), Parked (c_test_end.work i)) (hout_test : Parked c_test_end.output) (hout0 : c_test_end.output.cells 0 = Γ.start) {p : ℕ} (hp : c_test_end.output.head = p) (hcell1 : c_test_end.output.cells 1 = Γ.one) : ∃ (c_final : Cfg n (tmBody.loopTM tmTest).Q), (tmBody.loopTM tmTest).reachesIn (t_body + 1 + t_test + 1 + (p + 1) + 1) (tmBody.loopBodyWrap tmTest c_body_start) c_final ∧ (tmBody.loopTM tmTest).halted c_final ∧ c_final.input = c_test_end.input ∧ c_final.work = c_test_end.work ∧ c_final.output.head = 1 ∧ c_final.output.cells = c_test_end.output.cells

One full loopTM iteration that halts, framed. The same pass as TM.loopTM_iteration_halt, but reporting the input and work tapes of the halted configuration — which a loop's postcondition generally talks about, and which the unframed version discards.

def Complexity.TM.LoopParked {n : ℕ} (inp : Tape) (work : Fin n → Tape) (out : Tape) : Prop

The side conditions a loop's intermediate and final tape states must meet for the phase machinery to be transparent: every tape carries its left marker nowhere but cell zero, and every head is parked past it.

Equations

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

theorem Complexity.TM.loopTM_continue_of_hoare {n : ℕ} (tmBody tmTest : TM n) {E mid E' : TapePred n} {bBody bTest : ℕ} (hbody : tmBody.HoareTime E mid bBody) (htest : tmTest.HoareTime mid E' bTest) (hmid : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), mid inp work out → LoopParked inp work out) (hpost : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), E' inp work out → LoopParked inp work out ∧ out.cells 1 ≠ Γ.one) (inp : Tape) (work : Fin n → Tape) (out : Tape) : E inp work out → ∃ (inp' : Tape) (work' : Fin n → Tape) (out' : Tape) (t : ℕ), 1 ≤ t ∧ t ≤ bBody + bTest + 5 ∧ (tmBody.loopTM tmTest).reachesIn t { state := (tmBody.loopTM tmTest).qstart, input := inp, work := work, output := out } { state := (tmBody.loopTM tmTest).qstart, input := inp', work := work', output := out' } ∧ E' inp' work' out'

The per-iteration obligation of TM.loopTM_hoareTime_indexed, from two Hoare triples. Give a contract for the body and one for the test; if the test's postcondition leaves the tapes parked with a verdict cell that is not 1, the loop returns to its own start state with that postcondition intact.

theorem Complexity.TM.loopTM_halt_of_hoare {n : ℕ} (tmBody tmTest : TM n) {E mid E' : TapePred n} {bBody bTest : ℕ} (hbody : tmBody.HoareTime E mid bBody) (htest : tmTest.HoareTime mid E' bTest) (hmid : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), mid inp work out → LoopParked inp work out) (hpost : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), E' inp work out → LoopParked inp work out ∧ out.cells 1 = Γ.one) (inp : Tape) (work : Fin n → Tape) (out : Tape) : E inp work out → ∃ (c' : Cfg n (tmBody.loopTM tmTest).Q), ∃ t ≤ bBody + bTest + 5, (tmBody.loopTM tmTest).reachesIn t { state := (tmBody.loopTM tmTest).qstart, input := inp, work := work, output := out } c' ∧ (tmBody.loopTM tmTest).halted c' ∧ E' c'.input c'.work c'.output

The terminating obligation of TM.loopTM_hoareTime_indexed, from two Hoare triples. The companion of TM.loopTM_continue_of_hoare for the pass whose verdict cell does hold 1.