noncomputable def TuringMachine.NTM.runWithChoices {Q Γ : Type} [DecidableEq Q] [DecidableEq Γ] (M : NTM Q Γ) (w : List Γ) (choices : ℕ → Q × Γ × Direction) : ℕ → Config Q Γ

Simulate the NTM M on input w along a fixed nondeterministic-choice sequence choices : ℕ → Q × Γ × Direction. At step n:

• if the current configuration is halting, stay put;
• if choices n is a valid transition from the current configuration, apply it;
• otherwise, stay put (the chosen transition is illegal here).