Dropping the third component of a triple — proof internals

Cobham.reorder turns pair A (pair B C) into pair A B: copy the leading block verbatim, then decode the next block's payload. It is the one machine the comp constructor needs, via Cobham.pairFn_mem_FP.

Main results

• Cobham.reorder_mem_FP — the triple reorder is in FP

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

Drop the third component of a right-nested triple. Copy doubled payload bits verbatim until the [false, true] separator, then decode the next block's payload (fstBlock). On a valid triple this satisfies reorder (pair A (pair B C)) = pair A B (reorder_pair_pair). The incremental recursion (writing before knowing validity) is what the reorderTM scanner computes; it is total and needs no sub-machines.

Equations

• Complexity.Cobham.reorder (false :: false :: z) = false :: false :: Complexity.Cobham.reorder z
• Complexity.Cobham.reorder (true :: true :: z) = true :: true :: Complexity.Cobham.reorder z
• Complexity.Cobham.reorder (false :: true :: z) = false :: true :: Complexity.Cobham.fstBlock z
• Complexity.Cobham.reorder (c :: tail) = [c]
• Complexity.Cobham.reorder [] = []

theorem Complexity.Cobham.reorder_pair_pair (A B C : List Bool) : reorder (pair A (pair B C)) = pair A B

inductive Complexity.Cobham.ReorderPhase : Type

Control states of reorderTM: skip the marker; phase 1 (rcopyA/rcopyBf/ rcopyBt) copies doubled pairs verbatim until the separator; phase 2 (rdecA/rdecBf/rdecBt) decodes the next block's payload; then halt.

• rskip : ReorderPhase
• rcopyA : ReorderPhase
• rcopyBf : ReorderPhase
• rcopyBt : ReorderPhase
• rdecA : ReorderPhase
• rdecBf : ReorderPhase
• rdecBt : ReorderPhase
• rdone : ReorderPhase

@[implicit_reducible]

instance Complexity.Cobham.instDecidableEqReorderPhase : DecidableEq ReorderPhase

Equations

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

@[implicit_reducible]

instance Complexity.Cobham.instFintypeReorderPhase : Fintype ReorderPhase

Equations

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

def Complexity.Cobham.reorderTM : TM 0

The reorder transducer computing reorder: copy the leading block verbatim (phase 1) up to and including the [false,true] separator, then decode and emit the payload of the following block (phase 2).

Equations

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

theorem Complexity.Cobham.reorder_mem_FP : reorder ∈ FP

reorder is polynomial-time, via the reorderTM scanner.