What the block scanners compute — proof internals

The two total parsers of a self-delimiting block — pairFst decodes the leading block's payload, pairSnd returns the suffix after it (both defined in Complexitylib.Encoding.Pairing) — and the control states their scanners share. Complexity.pairSplitCoreTM handles only valid pair inputs, so the total decoders need machines of their own; those are Internal.SndBlock, Internal.FstBlock and Internal.Cat, one per machine.

theorem Complexity.Cobham.fstBlock_encodeVec_succ {n : ℕ} (v : Fin (n + 1) → List Bool) : pairFst (encodeVec v) = encodeVec (Fin.tail v)

Stripping the head component of an encoded vector yields the encoded tail. (Not a simp lemma: simp already reaches this via encodeVec_succ and pairFst_pair.)

theorem Complexity.Cobham.sndBlock_encodeVec_succ {n : ℕ} (v : Fin (n + 1) → List Bool) : pairSnd (encodeVec v) = v 0

The suffix of an encoded vector is its head component. (Not a simp lemma: simp already reaches this via encodeVec_succ and pairSnd_pair.)

inductive Complexity.Cobham.ScanPhase : Type

Control states of the block-decoding scanners.

• skip : ScanPhase
• scanA : ScanPhase
• scanBfalse : ScanPhase
• scanBtrue : ScanPhase
• emit : ScanPhase
• done : ScanPhase

@[instance_reducible]

instance Complexity.Cobham.instDecidableEqScanPhase : DecidableEq ScanPhase

Equations

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

@[instance_reducible]

instance Complexity.Cobham.instFintypeScanPhase : Fintype ScanPhase

Equations

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