Deterministic prefix of the nondeterministic composition — proof internals

The branch-false projection of NTM.compositionNTM tmF N runs deterministically from the initial configuration through the first computation, the raw-output rewind, the copy onto the virtual-input tape, and the virtual-input rewind, stopping at the rewind phase's halt state — the last configuration before the branch-dependent seam into the placed retargeted phase. Every step source on the way satisfies NTM.BranchesAgreeAt, so the run is packaged as a TM.ReachesInVia annotated run, ready for NTM.trace_of_det_prefix.

The main result is NTM.compositionNTM_detPrefix_internal, which also records the boundary configuration's tape shape: the virtual-input tape holds f x parked at head 1, the second machine's scratch block and the output are parked blanks, and every tape is start-invariant with head at least 1.

def Complexity.NTM.DetPrefixBoundary {nf ng : ℕ} (tmF : TM nf) (N : NTM ng) (y : List Bool) (E : Cfg (TM.compositionTapeCount nf ng) (compositionNTM tmF N).Q) : Prop

The boundary configuration at the end of the deterministic prefix: state at the virtual-input rewind's halt, virtual input y parked at head 1, second scratch block and output parked blank, and every tape start-invariant with positive head.

Equations

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

theorem Complexity.NTM.compositionNTM_detPrefix_internal {nf ng : ℕ} (tmF : TM nf) (N : NTM ng) {f : List Bool → List Bool} {TF : ℕ → ℕ} (hF : tmF.ComputesInTime f TF) (x : List Bool) : ∃ (E : Cfg (TM.compositionTapeCount nf ng) (compositionNTM tmF N).Q), ∃ t ≤ 4 * TF x.length + 10, ((compositionNTM tmF N).det false).ReachesInVia (compositionNTM tmF N).BranchesAgreeAt t ((compositionNTM tmF N).initCfg x) E ∧ DetPrefixBoundary tmF N (f x) E

Deterministic prefix of the composite. From the initial configuration, the branch-false projection reaches a DetPrefixBoundary configuration for y = f x in at most 4 * TF |x| + 10 steps, with every step source satisfying BranchesAgreeAt.