Clearing a binary work tape — proof internals #
This module packages the legacy rich clear/rewind proof behind a literal frame contract and proves that its component machines never move the output head left.
theorem
Complexity.TM.clearWorkTM_hoareTime_frame_internal
{n : ℕ}
(idx : Fin n)
(bits : List Bool)
(inp₀ : Tape)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(htarget : work₀ idx = (Tape.init (List.map Γ.ofBool bits)).move Dir3.right)
(hinp : Parked inp₀)
(hother : ∀ (i : Fin n), i ≠ idx → Parked (work₀ i))
(hout : Parked out₀)
:
(clearWorkTM idx).HoareTime
(fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀)
(fun (inp : Tape) (work : Fin n → Tape) (out : Tape) =>
inp = inp₀ ∧ work = Function.update work₀ idx ((Tape.init []).move Dir3.right) ∧ out = out₀)
(clearWorkTimeBound bits.length)
theorem
Complexity.TM.clearWorkTM_hoareTimeSpace_frame_internal
{n : ℕ}
(idx : Fin n)
(bits : List Bool)
(inputLength initialSpace : ℕ)
(inp₀ : Tape)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(htarget : work₀ idx = (Tape.init (List.map Γ.ofBool bits)).move Dir3.right)
(hinp : Parked inp₀)
(hother : ∀ (i : Fin n), i ≠ idx → Parked (work₀ i))
(hout : Parked out₀)
(hinitial :
{ state := (clearWorkTM idx).qstart, input := inp₀, work := work₀, output := out₀ }.WithinAuxSpace inputLength
initialSpace)
:
(clearWorkTM idx).HoareTimeSpace
(fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀)
(fun (inp : Tape) (work : Fin n → Tape) (out : Tape) =>
inp = inp₀ ∧ work = Function.update work₀ idx ((Tape.init []).move Dir3.right) ∧ out = out₀)
(clearWorkTimeBound bits.length) inputLength (initialSpace + clearWorkTimeBound bits.length)
theorem
Complexity.TM.blankWorkTM_isTransducer_internal
{n : ℕ}
(idx : Fin n)
:
(blankWorkTM idx).IsTransducer
theorem
Complexity.TM.rewindWorkTM_isTransducer_internal
{n : ℕ}
(idx : Fin n)
:
(rewindWorkTM idx).IsTransducer
theorem
Complexity.TM.clearWorkTM_isTransducer_internal
{n : ℕ}
(idx : Fin n)
:
(clearWorkTM idx).IsTransducer