Resetting a binary work tape — proof internals #
theorem
Complexity.TM.rewindBinaryWorkTM_hoareTime_frame_internal
{n : ℕ}
(idx : Fin n)
(bits : List Bool)
(headBound : ℕ)
(inp₀ : Tape)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(htarget : (work₀ idx).HasBinaryContent bits)
(htargetStart : (work₀ idx).cells 0 = Γ.start)
(htargetHead : 1 ≤ (work₀ idx).head ∧ (work₀ idx).head ≤ headBound)
(hinput : Parked inp₀)
(hother : ∀ (i : Fin n), i ≠ idx → Parked (work₀ i))
(houtput : Parked out₀)
:
(rewindWorkTM 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 idx = (Tape.init (List.map Γ.ofBool bits)).move Dir3.right ∧ (∀ (i : Fin n), i ≠ idx → work i = work₀ i) ∧ out = out₀)
(headBound + 2)
theorem
Complexity.TM.resetBinaryWorkTM_hoareTime_frame_internal
{n : ℕ}
(idx : Fin n)
(bits : List Bool)
(headBound : ℕ)
(inp₀ : Tape)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(htarget : (work₀ idx).HasBinaryContent bits)
(htargetStart : (work₀ idx).cells 0 = Γ.start)
(htargetHead : 1 ≤ (work₀ idx).head ∧ (work₀ idx).head ≤ headBound)
(hinput : Parked inp₀)
(hother : ∀ (i : Fin n), i ≠ idx → Parked (work₀ i))
(houtput : Parked out₀)
:
(resetBinaryWorkTM 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₀)
(resetBinaryWorkTime headBound bits.length)