Decoded sparse-address equality — definitions

The entry decoder leaves an address target at its append position. This stage rewinds it and compares it against a canonical query address, writing the Boolean result on a third work tape.

def Complexity.RAM.RegisterStore.Machine.decodedAddressEqTM {n : ℕ} (addressIdx queryIdx resultIdx : Fin n) : TM n

Rewind a decoded address and compare it with a canonical query address.

Equations

• Complexity.RAM.RegisterStore.Machine.decodedAddressEqTM addressIdx queryIdx resultIdx = (Complexity.TM.rewindWorkTM addressIdx).seqTM (Complexity.TM.binaryEqTM addressIdx queryIdx resultIdx)

def Complexity.RAM.RegisterStore.Machine.decodedAddressEqTime (addressBits queryBits : List Bool) : ℕ

Linear time bound for decoded-address equality, including its composition seam.

Equations

• Complexity.RAM.RegisterStore.Machine.decodedAddressEqTime addressBits queryBits = addressBits.length + 3 + 1 + Complexity.TM.binaryEqTime addressBits queryBits