State-independent safety contracts

TM.HoareSafety requires a tape predicate at every reachable configuration. Unlike a fixed space predicate, it can charge only selected work tapes while still bounding the output. Ordinary time contracts supply termination separately.

def Complexity.TM.HoareSafety {n : ℕ} (M : TM n) (pre safe : TapePred n) : Prop

Every configuration reachable from a permitted entry satisfies safe.

Equations

• One or more equations did not get rendered due to their size.