The block-payload decoder — proof internals

Cobham.fstBlockTM is the same scan as Cobham.sndBlockTM, emitting each decoded payload bit as it goes and stopping at the separator. Malformed input halts with empty output.

Main results

• Cobham.fstBlock_mem_FP — the payload decoder is in FP

def Complexity.Cobham.fstBlockTM : TM 0

The payload decoder: scan doubled payload bits, emitting each decoded bit to the output, until the [false, true] separator or end of input. Computes fstBlock.

Equations

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

theorem Complexity.Cobham.fstBlock_mem_FP : fstBlock ∈ FP

fstBlock is polynomial-time, via the fstBlockTM scanner.