Resetting a binary work tape — definitions

resetBinaryWorkTM first rewinds an arbitrary cursor over canonical binary contents and then clears the resulting completed string to the standard blank work tape.

def Complexity.TM.resetBinaryWorkTM {n : ℕ} (idx : Fin n) : TM n

Rewind and clear one canonical binary work tape.

Equations

• Complexity.TM.resetBinaryWorkTM idx = (Complexity.TM.rewindWorkTM idx).seqTM (Complexity.TM.clearWorkTM idx)

def Complexity.TM.resetBinaryWorkTime (headBound bitLength : ℕ) : ℕ

Time bound in terms of the initial head bound and represented bit length.

Equations

• Complexity.TM.resetBinaryWorkTime headBound bitLength = headBound + 2 + 1 + Complexity.TM.clearWorkTimeBound bitLength