The block-suffix decoder — proof internals

Cobham.sndBlockTM scans the doubled payload two bits at a time until the [false, true] separator, then copies the rest of the input to the output. Malformed input halts with empty output, matching unpair? = none.

Main results

• Cobham.sndBlock_mem_FP — the suffix decoder is in FP

def Complexity.Cobham.sndBlockTM : TM 0

The suffix decoder: scan doubled payload bits until the [false, true] separator, then copy the remaining input (the suffix y of pair x y) to the output. On malformed input it halts with empty output. Computes sndBlock.

Equations

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

theorem Complexity.Cobham.sndBlock_mem_FP : sndBlock ∈ FP

sndBlock is polynomial-time, via the sndBlockTM scanner.