Clearing a binary work tape — definitions

This module names the concrete time bound used by the public framed contract for TM.clearWorkTM.

def Complexity.TM.clearWorkTimeBound (length : ℕ) : ℕ

Concrete running-time bound for clearing and rewinding a Boolean work tape whose represented string has length bits.

Equations

• Complexity.TM.clearWorkTimeBound length = 2 * length + 5