Nondeterministic trace API -- proof internals

Proofs for the public finite-trace decomposition rules.

theorem Complexity.NTM.trace_snoc_internal {n : ℕ} (tm : NTM n) (T : ℕ) (choices : Fin (T + 1) → Bool) (c : Cfg n tm.Q) : tm.trace (T + 1) choices c = tm.trace 1 (fun (x : Fin 1) => choices (Fin.last T)) (tm.trace T (fun (i : Fin T) => choices i.castSucc) c)

theorem Complexity.NTM.trace_invariant_internal {n : ℕ} (tm : NTM n) (T : ℕ) (choices : Fin T → Bool) (c : Cfg n tm.Q) (invariant : ℕ → Cfg n tm.Q → Prop) (initial : invariant 0 c) (step : ∀ (time : ℕ) (htime : time < T) (current : Cfg n tm.Q), invariant time current → invariant (time + 1) (tm.trace 1 (fun (x : Fin 1) => choices ⟨time, htime⟩) current)) : invariant T (tm.trace T choices c)