Concatenating two blocks — proof internals

Cobham.catBlocks appends the payloads of two consecutive blocks, the string concatenation behind Cobham.appendFn_mem_FP, together with the Cobham.catTM scanner that computes it.

Main results

• Cobham.catBlocks_mem_FP — concatenation is in FP

Concatenation

catBlocks is fstBlock and sndBlock fused: decode the leading block's payload and keep the suffix, so on a genuine pair it is concatenation. Its machine is sndBlockTM with the scan also emitting each decoded bit — the one FP primitive that lets two computed strings be joined.

def Complexity.Cobham.catBlocks : List Bool → List Bool

Decode the leading self-delimiting block's payload and keep the suffix. On pair x y this is x ++ y (catBlocks_pair); on malformed input it returns the bits decoded so far.

Equations

• Complexity.Cobham.catBlocks (false :: false :: z) = false :: Complexity.Cobham.catBlocks z
• Complexity.Cobham.catBlocks (true :: true :: z) = true :: Complexity.Cobham.catBlocks z
• Complexity.Cobham.catBlocks (false :: true :: z) = z
• Complexity.Cobham.catBlocks x✝ = []

@[simp]

theorem Complexity.Cobham.catBlocks_pair (x y : List Bool) : catBlocks (pair x y) = x ++ y

def Complexity.Cobham.catTM : TM 0

The concatenator: like sndBlockTM, but the scan also emits each decoded payload bit, so the output ends up holding the payload followed by the suffix. Computes catBlocks.

Equations

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

theorem Complexity.Cobham.catBlocks_mem_FP : catBlocks ∈ FP

Concatenation is polynomial-time.