Count-preserving shared-tape sequencing

The existing sequential compiler preserves List occurrences, including duplicate endpoints. With nonblocking transition tables, the two native all-branches halting clocks add. This is sequencing on the same tapes; preparing encoded inputs, copying and clearing remain charged obligations of the buffered composition compiler.

Main results

• Turing.MultiTapeCTM.Nonblocking.seq: the compiler introduces no stuck local views.
• Turing.MultiTapeCTM.runList_seq: exact List bind for the existing sequential compiler.
• Turing.MultiTapeCTM.HaltsWithin.seq: native all-branches clocks add.

References

The shared compiler and its source credit are in MultiTape.Machine.Sequential.

theorem Turing.MultiTapeCTM.Nonblocking.seq {k : ℕ} {Symbol State₀ State₁ : Type} {first : MultiTapeCTM k Symbol State₀} {second : MultiTapeCTM k Symbol State₁} (hfirst : first.Nonblocking) (hsecond : second.Nonblocking) : Nonblocking (MultiTapeMachine.seq first second)

Sequencing maps each transition occurrence once and introduces no empty live choice lists.

theorem Turing.MultiTapeCTM.runList_seq {k : ℕ} {Symbol State₀ State₁ : Type} {input : List Symbol} (first : MultiTapeCTM k Symbol State₀) (second : MultiTapeCTM k Symbol State₁) (cfg : MultiTapeMachine.Config k Symbol State₀ Empty input) (firstTime secondTime : ℕ) (hfirst : first.HaltsWithin firstTime cfg.tapes) (hsecond : ∀ result ∈ first.runList firstTime cfg.tapes, second.HaltsWithin secondTime (result.withState (some second.initial))) : runList (MultiTapeMachine.seq first second) (firstTime + secondTime) (MultiTapeMachine.Sequential.left second cfg).tapes = List.flatMap (fun (result : Cfg k Symbol State₀ input) => List.map (fun (final : Cfg k Symbol State₁ input) => Cfg.mapState (Option.map Sum.inr) final) (second.runList secondTime (result.withState (some second.initial)))) (first.runList firstTime cfg.tapes)

Exact native List execution of shared-tape sequencing. Each first-phase occurrence runs its own continuation, even when several first-phase occurrences have the same final configuration.

theorem Turing.MultiTapeCTM.HaltsWithin.seq {k : ℕ} {Symbol State₀ State₁ : Type} {input : List Symbol} {first : MultiTapeCTM k Symbol State₀} {second : MultiTapeCTM k Symbol State₁} (hnonfirst : first.Nonblocking) (hnonsecond : second.Nonblocking) (cfg : MultiTapeMachine.Config k Symbol State₀ Empty input) (firstTime secondTime : ℕ) (hfirst : first.HaltsWithin firstTime cfg.tapes) (hsecond : ∀ result ∈ first.runList firstTime cfg.tapes, second.HaltsWithin secondTime (result.withState (some second.initial))) : HaltsWithin (MultiTapeMachine.seq first second) (firstTime + secondTime) (MultiTapeMachine.Sequential.left second cfg).tapes

Under the explicit no-stuck table hypotheses, every sequential branch halts within the sum. The conclusion is the native occurrence-labelled bound, not just a support condition.