ifTM simulation — proof internals

This file contains the simulation lemmas for ifTM tmTest tmThen tmElse.

Key definitions

• ifTestWrap — embed a tmTest config into the ifTM config space
• ifThenWrap — embed a tmThen config into the ifTM config space
• ifElseWrap — embed a tmElse config into the ifTM config space

def Complexity.TM.ifTestWrap {n : ℕ} (tmTest tmThen tmElse : TM n) (c : Cfg n tmTest.Q) : Cfg n (IfQ tmTest.Q tmThen.Q tmElse.Q)

Embed a tmTest config into the ifTM config space (test phase).

Equations

• tmTest.ifTestWrap tmThen tmElse c = { state := Sum.inl c.state, input := c.input, work := c.work, output := c.output }

def Complexity.TM.ifThenWrap {n : ℕ} (tmTest tmThen tmElse : TM n) (c : Cfg n tmThen.Q) : Cfg n (IfQ tmTest.Q tmThen.Q tmElse.Q)

Embed a tmThen config into the ifTM config space (then branch).

Equations

• tmTest.ifThenWrap tmThen tmElse c = { state := Sum.inr (Sum.inr (Sum.inl c.state)), input := c.input, work := c.work, output := c.output }

def Complexity.TM.ifElseWrap {n : ℕ} (tmTest tmThen tmElse : TM n) (c : Cfg n tmElse.Q) : Cfg n (IfQ tmTest.Q tmThen.Q tmElse.Q)

Embed a tmElse config into the ifTM config space (else branch).

Equations

• tmTest.ifElseWrap tmThen tmElse c = { state := Sum.inr (Sum.inr (Sum.inr c.state)), input := c.input, work := c.work, output := c.output }

theorem Complexity.TM.ifTM_test_step {n : ℕ} (tmTest tmThen tmElse : TM n) {c c' : Cfg n tmTest.Q} (hstep : tmTest.step c = some c') : (tmTest.ifTM tmThen tmElse).step (tmTest.ifTestWrap tmThen tmElse c) = some (tmTest.ifTestWrap tmThen tmElse c')

One step of tmTest corresponds to one step of ifTM during the test phase.

theorem Complexity.TM.ifTM_reachesIn_ifTestWrap {n : ℕ} (tmTest tmThen tmElse : TM n) {t : ℕ} {c_start c_end : Cfg n tmTest.Q} (hreach : tmTest.reachesIn t c_start c_end) : (tmTest.ifTM tmThen tmElse).reachesIn t (tmTest.ifTestWrap tmThen tmElse c_start) (tmTest.ifTestWrap tmThen tmElse c_end)

Multi-step test phase simulation.

theorem Complexity.TM.ifTM_then_step {n : ℕ} (tmTest tmThen tmElse : TM n) {c c' : Cfg n tmThen.Q} (hstep : tmThen.step c = some c') : (tmTest.ifTM tmThen tmElse).step (tmTest.ifThenWrap tmThen tmElse c) = some (tmTest.ifThenWrap tmThen tmElse c')

One step of tmThen corresponds to one step of ifTM during the then branch.

theorem Complexity.TM.ifTM_reachesIn_ifThenWrap {n : ℕ} (tmTest tmThen tmElse : TM n) {t : ℕ} {c_start c_end : Cfg n tmThen.Q} (hreach : tmThen.reachesIn t c_start c_end) : (tmTest.ifTM tmThen tmElse).reachesIn t (tmTest.ifThenWrap tmThen tmElse c_start) (tmTest.ifThenWrap tmThen tmElse c_end)

Multi-step then-branch simulation.

theorem Complexity.TM.ifTM_else_step {n : ℕ} (tmTest tmThen tmElse : TM n) {c c' : Cfg n tmElse.Q} (hstep : tmElse.step c = some c') : (tmTest.ifTM tmThen tmElse).step (tmTest.ifElseWrap tmThen tmElse c) = some (tmTest.ifElseWrap tmThen tmElse c')

One step of tmElse corresponds to one step of ifTM during the else branch.

theorem Complexity.TM.ifTM_reachesIn_ifElseWrap {n : ℕ} (tmTest tmThen tmElse : TM n) {t : ℕ} {c_start c_end : Cfg n tmElse.Q} (hreach : tmElse.reachesIn t c_start c_end) : (tmTest.ifTM tmThen tmElse).reachesIn t (tmTest.ifElseWrap tmThen tmElse c_start) (tmTest.ifElseWrap tmThen tmElse c_end)

Multi-step else-branch simulation.

theorem Complexity.TM.ifTM_then_halt_step {n : ℕ} (tmTest tmThen tmElse : TM n) {c : Cfg n tmThen.Q} (hhalt : c.state = tmThen.qhalt) : (tmTest.ifTM tmThen tmElse).step (tmTest.ifThenWrap tmThen tmElse c) = some { state := Sum.inr (Sum.inl IfPhase.done), input := transitionInput c.input, work := fun (i : Fin n) => transitionTape (c.work i), output := transitionTape c.output }

When tmThen halts, one step transitions to done.

theorem Complexity.TM.ifTM_else_halt_step {n : ℕ} (tmTest tmThen tmElse : TM n) {c : Cfg n tmElse.Q} (hhalt : c.state = tmElse.qhalt) : (tmTest.ifTM tmThen tmElse).step (tmTest.ifElseWrap tmThen tmElse c) = some { state := Sum.inr (Sum.inl IfPhase.done), input := transitionInput c.input, work := fun (i : Fin n) => transitionTape (c.work i), output := transitionTape c.output }

When tmElse halts, one step transitions to done.

theorem Complexity.TM.ifTM_test_to_rewind {n : ℕ} (tmTest tmThen tmElse : TM n) {c : Cfg n tmTest.Q} (hhalt : c.state = tmTest.qhalt) : (tmTest.ifTM tmThen tmElse).step (tmTest.ifTestWrap tmThen tmElse c) = some { state := Sum.inr (Sum.inl IfPhase.rewindOut), input := transitionInput c.input, work := fun (i : Fin n) => transitionTape (c.work i), output := transitionTape c.output }

When tmTest halts, one step enters the rewindOut phase.

theorem Complexity.TM.ifTM_qhalt_eq_done {n : ℕ} (tmTest tmThen tmElse : TM n) : (tmTest.ifTM tmThen tmElse).qhalt = Sum.inr (Sum.inl IfPhase.done)

theorem Complexity.TM.ifTM_halted_of_state_eq_done {n : ℕ} (tmTest tmThen tmElse : TM n) (c : Cfg n (IfQ tmTest.Q tmThen.Q tmElse.Q)) (h : c.state = Sum.inr (Sum.inl IfPhase.done)) : (tmTest.ifTM tmThen tmElse).halted c

The done state is halted in ifTM.

theorem Complexity.TM.ifTM_rewindOut_reachesIn_check {n : ℕ} (tmTest tmThen tmElse : TM n) (p : ℕ) (c : Cfg n (IfQ tmTest.Q tmThen.Q tmElse.Q)) : c.state = Sum.inr (Sum.inl IfPhase.rewindOut) → c.output.cells 0 = Γ.start → (∀ j ≥ 1, c.output.cells j ≠ Γ.start) → c.output.head = p → c.input.head ≥ 1 → (∀ j ≥ 1, c.input.cells j ≠ Γ.start) → (∀ (i : Fin n), (c.work i).head ≥ 1) → (∀ (i : Fin n), ∀ j ≥ 1, (c.work i).cells j ≠ Γ.start) → ∃ (c_check : Cfg n (tmTest.ifTM tmThen tmElse).Q), (tmTest.ifTM tmThen tmElse).reachesIn (p + 1) c c_check ∧ c_check.state = Sum.inr (Sum.inl IfPhase.check) ∧ c_check.output.head = 1 ∧ c_check.output.cells = c.output.cells ∧ c_check.input = c.input ∧ c_check.work = c.work

Extended rewind loop: also tracks that input and work tapes are preserved when they satisfy the stability condition (head ≥ 1, cells ≥ 1 ≠ start).

theorem Complexity.TM.ifTM_check_step_then_full {n : ℕ} (tmTest tmThen tmElse : TM n) (c : Cfg n (IfQ tmTest.Q tmThen.Q tmElse.Q)) (hstate : c.state = Sum.inr (Sum.inl IfPhase.check)) (hhead : c.output.head = 1) (hcell1 : c.output.cells 1 = Γ.one) (h_ih : c.input.head ≥ 1) (h_ins : ∀ j ≥ 1, c.input.cells j ≠ Γ.start) (h_wh : ∀ (i : Fin n), (c.work i).head ≥ 1) (h_wns : ∀ (i : Fin n), ∀ j ≥ 1, (c.work i).cells j ≠ Γ.start) : ∃ (c' : Cfg n (tmTest.ifTM tmThen tmElse).Q), (tmTest.ifTM tmThen tmElse).step c = some c' ∧ c'.state = Sum.inr (Sum.inr (Sum.inl tmThen.qstart)) ∧ c'.output.cells = c.output.cells ∧ c'.output.head = 1 ∧ c'.input = c.input ∧ c'.work = c.work

Check step to then-branch, tracking all tapes.

theorem Complexity.TM.ifTM_check_step_else_full {n : ℕ} (tmTest tmThen tmElse : TM n) (c : Cfg n (IfQ tmTest.Q tmThen.Q tmElse.Q)) (hstate : c.state = Sum.inr (Sum.inl IfPhase.check)) (hhead : c.output.head = 1) (hcell1 : c.output.cells 1 ≠ Γ.one) (hnostart_out : ∀ j ≥ 1, c.output.cells j ≠ Γ.start) (h_ih : c.input.head ≥ 1) (h_ins : ∀ j ≥ 1, c.input.cells j ≠ Γ.start) (h_wh : ∀ (i : Fin n), (c.work i).head ≥ 1) (h_wns : ∀ (i : Fin n), ∀ j ≥ 1, (c.work i).cells j ≠ Γ.start) : ∃ (c' : Cfg n (tmTest.ifTM tmThen tmElse).Q), (tmTest.ifTM tmThen tmElse).step c = some c' ∧ c'.state = Sum.inr (Sum.inr (Sum.inr tmElse.qstart)) ∧ c'.output.cells = c.output.cells ∧ c'.output.head = 1 ∧ c'.input = c.input ∧ c'.work = c.work

Check step to else-branch, tracking all tapes.