Resetting several binary work tapes — definitions

resetBinaryWorkManyTM targets sequentially rewinds and clears every work tape named by targets. The executable machine depends only on the tape-index list; represented contents and resource bounds occur only in its contracts.

def Complexity.TM.resetBinaryBlank : Tape

The standard parked blank work tape produced by binary reset.

Equations

• Complexity.TM.resetBinaryBlank = (Complexity.Tape.init []).move Complexity.Dir3.right

def Complexity.TM.resetBinaryWorkManyTM {n : ℕ} : List (Fin n) → TM n

Sequentially reset every work tape in targets, with skipTM as the empty-list identity.

Equations

• Complexity.TM.resetBinaryWorkManyTM [] = Complexity.TM.skipTM
• Complexity.TM.resetBinaryWorkManyTM (idx :: rest) = (Complexity.TM.resetBinaryWorkTM idx).seqTM (Complexity.TM.resetBinaryWorkManyTM rest)

def Complexity.TM.resetBinaryWorkManyResult {n : ℕ} : (Fin n → Tape) → List (Fin n) → Fin n → Tape

Exact work family obtained by applying the advertised resets in order.

Equations

• Complexity.TM.resetBinaryWorkManyResult x✝ [] = x✝
• Complexity.TM.resetBinaryWorkManyResult x✝ (idx :: rest) = Complexity.TM.resetBinaryWorkManyResult (Function.update x✝ idx Complexity.TM.resetBinaryBlank) rest

def Complexity.TM.resetBinaryWorkManyTime {n : ℕ} (bits : Fin n → List Bool) (headBound : Fin n → ℕ) : List (Fin n) → ℕ

Compositional time bound: every reset is followed by one sequencing seam, and the empty-list skipTM costs one final step.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.TM.resetBinaryWorkManyTime bits headBound [] = 1