Sequential composition before a nondeterministic machine

NTM.compositionTM tmF N runs the deterministic function computation tmF, pipes its output to a fresh virtual-input tape, and then runs the nondeterministic machine N on that virtual input.

The construction shares TM.compositionTM's state skeleton: none of the deterministic composition's states, start/halt markers, or tape layout depend on the second machine's transition function, so branch b of the composite can be defined as the deterministic composition with branch b of N. The det projections then coincide with the deterministic compositions definitionally (compositionNTM_det), which lets every deterministic simulation lemma about TM.compositionTM be reused for the composite's traces through NTM.trace_of_det_prefix.

def Complexity.NTM.compositionNTM {nf ng : ℕ} (tmF : TM nf) (N : NTM ng) : NTM (TM.compositionTapeCount nf ng)

Sequential composition of a deterministic function computation with a nondeterministic machine. Branch b of the composite is the deterministic composition TM.compositionTM tmF (N.det b); the state skeleton is branch-independent.

Equations

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

theorem Complexity.NTM.compositionNTM_det {nf ng : ℕ} (tmF : TM nf) (N : NTM ng) (b : Bool) : (compositionNTM tmF N).det b = tmF.compositionTM (N.det b)

The det projections of the composite are exactly the deterministic compositions with the corresponding branch of N.

theorem Complexity.NTM.compositionNTM_initCfg {nf ng : ℕ} (tmF : TM nf) (N : NTM ng) (x : List Bool) : (compositionNTM tmF N).initCfg x = (tmF.compositionTM (N.det false)).initCfg x

The composite and its branch compositions share initial configurations.

Branch agreement on the deterministic phases

The composite's two branches consult N's transition functions only inside the placed retargeted phase (the innermost Sum.inr block of the state space). At every other state the transition is the same term for both branches, so agreement holds definitionally once the state shape is fixed.

theorem Complexity.NTM.compositionNTM_branchesAgreeAt_first {nf ng : ℕ} (tmF : TM nf) (N : NTM ng) {c : Cfg (TM.compositionTapeCount nf ng) (compositionNTM tmF N).Q} (q : (tmF.compositionFirstTM ng).Q) (hq : c.state = Sum.inl q) : (compositionNTM tmF N).BranchesAgreeAt c

Branch agreement at first-computation states.

theorem Complexity.NTM.compositionNTM_branchesAgreeAt_rewindRaw {nf ng : ℕ} (tmF : TM nf) (N : NTM ng) {c : Cfg (TM.compositionTapeCount nf ng) (compositionNTM tmF N).Q} (q : (TM.rewindWorkTM (TM.compositionRawOutputIdx nf ng)).Q) (hq : c.state = Sum.inr (Sum.inl q)) : (compositionNTM tmF N).BranchesAgreeAt c

Branch agreement at raw-output-rewind states.

theorem Complexity.NTM.compositionNTM_branchesAgreeAt_copy {nf ng : ℕ} (tmF : TM nf) (N : NTM ng) {c : Cfg (TM.compositionTapeCount nf ng) (compositionNTM tmF N).Q} (q : (TM.copyWorkToWorkTM (TM.compositionRawOutputIdx nf ng) (TM.compositionVirtualInputIdx nf ng)).Q) (hq : c.state = Sum.inr (Sum.inr (Sum.inl q))) : (compositionNTM tmF N).BranchesAgreeAt c

Branch agreement at copy states.

theorem Complexity.NTM.compositionNTM_branchesAgreeAt_rewindVirtual {nf ng : ℕ} (tmF : TM nf) (N : NTM ng) {c : Cfg (TM.compositionTapeCount nf ng) (compositionNTM tmF N).Q} (q : (TM.rewindWorkTM (TM.compositionVirtualInputIdx nf ng)).Q) (hne : q ≠ (TM.rewindWorkTM (TM.compositionVirtualInputIdx nf ng)).qhalt) (hq : c.state = Sum.inr (Sum.inr (Sum.inr (Sum.inl q)))) : (compositionNTM tmF N).BranchesAgreeAt c

Branch agreement at live virtual-input-rewind states. The rewind phase's halt state is excluded: the seam out of it enters the placed retargeted phase at N's post-first-transition state, which is the composite's first branch-dependent transition.