Binary work-tape equality — definitions

TM.binaryEqTM compares two canonical binary strings and writes the Boolean result on a third work tape. Unlike the legacy output-oriented comparator, it preserves the public output tape and every unrelated work tape.

inductive Complexity.TM.BinaryEqPhase : Type

The binary comparator scans until the first mismatch or simultaneous termination, then halts immediately.

• scan : BinaryEqPhase
• done : BinaryEqPhase

@[implicit_reducible]

instance Complexity.TM.instDecidableEqBinaryEqPhase : DecidableEq BinaryEqPhase

Equations

• Complexity.TM.instDecidableEqBinaryEqPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.TM.instFintypeBinaryEqPhase : Fintype BinaryEqPhase

Equations

• Complexity.TM.instFintypeBinaryEqPhase = { elems := {Complexity.TM.BinaryEqPhase.scan, Complexity.TM.BinaryEqPhase.done}, complete := ⋯ }

structure Complexity.TM.BinaryEqDistinct {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) : Prop

Pairwise distinct work tapes used by binaryEqTM.

• lhs_rhs : lhsIdx ≠ rhsIdx
• lhs_result : lhsIdx ≠ resultIdx
• rhs_result : rhsIdx ≠ resultIdx

def Complexity.TM.binaryEqTM {n : ℕ} (lhsIdx rhsIdx resultIdx : Fin n) : TM n

Compare canonical binary strings on lhsIdx and rhsIdx, writing one to resultIdx exactly when they agree. The compared heads advance together over matching bits; all tape contents are preserved except the single result cell.

Equations

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

def Complexity.TM.binaryEqTime (lhs rhs : List Bool) : ℕ

Linear scan bound for binary equality.

Equations

• Complexity.TM.binaryEqTime lhs rhs = max lhs.length rhs.length + 1