Sequencing emitter stages

bigSeqTM folds a list of machines with seqTM, and bigSeqTM_hoareTime chains their EmitPred specs: stage k carries the ghost state (W k, Y k) to (W (k+1), Y (k+1)). All the finite-tuple folds of the reduction emitter (literal chains, clause chains, the per-state/symbol/choice unrollings of the transition family) are instances of this single rule.

def Complexity.TM.bigSeqTM {n : ℕ} : List (TM n) → TM n

Sequence a list of machines (right fold, skipTM base).

Equations

• Complexity.TM.bigSeqTM [] = Complexity.TM.skipTM
• Complexity.TM.bigSeqTM (m :: ms) = m.seqTM (Complexity.TM.bigSeqTM ms)

theorem Complexity.TM.bigSeqTM_hoareTime {n : ℕ} (ms : List (TM n)) (inp₀ : Tape) (W : ℕ → Fin n → Tape) (Y : ℕ → List Bool) (b : ℕ) (hinp₀ : Parked inp₀) (hWP : ∀ (k : ℕ) (j : Fin n), Parked (W k j)) (hms : ∀ (k : ℕ) (hk : k < ms.length), ms[k].HoareTime (EmitPred inp₀ (W k) (Y k)) (EmitPred inp₀ (W (k + 1)) (Y (k + 1))) b) : (bigSeqTM ms).HoareTime (EmitPred inp₀ (W 0) (Y 0)) (EmitPred inp₀ (W ms.length) (Y ms.length)) (ms.length * (b + 1) + 1)

Indexed chain rule. Machine ms[k] carries the EmitPred state from stage k to stage k + 1; the fold carries stage 0 to stage ms.length, in |ms| · (b + 1) + 1 steps.