Resetting several binary work tapes — proof internals #

theorem Complexity.TM.resetBinaryWorkManyTime_le_internal {n : ℕ} (targets : List (Fin n)) (bits : Fin n → List Bool) (headBound : Fin n → ℕ) (maxHead maxWidth : ℕ) (hhead : ∀ i ∈ targets, headBound i ≤ maxHead) (hwidth : ∀ i ∈ targets, (bits i).length ≤ maxWidth) :

resetBinaryWorkManyTime bits headBound targets ≤ targets.length * (maxHead + 2 * maxWidth + 9) + 1

theorem Complexity.TM.resetBinaryWorkManyResult_parked_internal {n : ℕ} (work₀ : Fin n → Tape) (targets : List (Fin n)) (hwork : ∀ (i : Fin n), Parked (work₀ i)) (i : Fin n) :

theorem Complexity.TM.resetBinaryWorkManyResult_eq_of_not_mem_internal {n : ℕ} (work₀ : Fin n → Tape) (targets : List (Fin n)) (idx : Fin n) (hidx : idx ∉ targets) :

resetBinaryWorkManyResult work₀ targets idx = work₀ idx

theorem Complexity.TM.resetBinaryWorkManyResult_eq_blank_of_mem_internal {n : ℕ} (work₀ : Fin n → Tape) (targets : List (Fin n)) (idx : Fin n) (hidx : idx ∈ targets) :

theorem Complexity.TM.resetBinaryWorkManyTime_congr_headBound_internal {n : ℕ} (targets : List (Fin n)) (bits : Fin n → List Bool) (left right : Fin n → ℕ) (heq : ∀ i ∈ targets, left i = right i) :

theorem Complexity.TM.resetBinaryWorkManyTM_hoareTime_frame_internal {n : ℕ} (targets : List (Fin n)) (bits : Fin n → List Bool) (headBound : Fin n → ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hnodup : targets.Nodup) (htarget : ∀ i ∈ targets, (work₀ i).HasBinaryContent (bits i)) (htargetStart : ∀ i ∈ targets, (work₀ i).cells 0 = Γ.start) (htargetHead : ∀ i ∈ targets, (work₀ i).head ≤ headBound i) (hinput : Parked inp₀) (hwork : ∀ (i : Fin n), Parked (work₀ i)) (houtput : Parked out₀) :

(resetBinaryWorkManyTM targets).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 = resetBinaryWorkManyResult work₀ targets ∧ out = out₀) (resetBinaryWorkManyTime bits headBound targets)

Documentation