Resetting several binary work tapes

This module exposes a framed compositional contract for resetting a fixed list of distinct canonical binary work tapes.

theorem Complexity.TM.resetBinaryWorkManyTime_le {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

A reset list has a uniform linear bound when every target head and represented bit string is bounded uniformly.

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

Every targeted work tape is the standard parked blank after the reset sequence.

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

Work tapes outside the target list are preserved literally.

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

Resetting a list of work tapes preserves parkedness of the whole work family.

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

The reset-sequence time depends on head bounds only at named targets.

theorem Complexity.TM.resetBinaryWorkManyTM_hoareTime_frame {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)

Sequentially reset a distinct list of canonical binary work tapes while preserving the complete external frame.

theorem Complexity.TM.resetBinaryWorkManyTM_isTransducer {n : ℕ} (targets : List (Fin n)) : (resetBinaryWorkManyTM targets).IsTransducer

Resetting several binary work tapes preserves one-way output safety.

theorem Complexity.TM.resetBinaryWorkManyTM_prefix_withinAuxSpace {n : ℕ} (targets : List (Fin n)) (bits : Fin n → List Bool) (headBound : Fin n → ℕ) (inputLength initialSpace time : ℕ) (start current : Cfg n (resetBinaryWorkManyTM targets).Q) (hinitial : start.WithinAuxSpace inputLength initialSpace) (hreach : (resetBinaryWorkManyTM targets).reachesIn time start current) (htime : time ≤ resetBinaryWorkManyTime bits headBound targets) : current.WithinAuxSpace inputLength (initialSpace + resetBinaryWorkManyTime bits headBound targets)

Coarse all-prefix auxiliary-space envelope for a reset sequence.