Nondeterministic trace API -- proof internals #
Proofs for the public finite-trace decomposition rules.
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)
theorem
Complexity.NTM.trace_map_prefix_internal
{n n' : ℕ}
(source : NTM n)
(target : NTM n')
(wrap : Cfg n source.Q → Cfg n' target.Q)
(step :
∀ (choice : Bool) (c : Cfg n source.Q),
c.state ≠ source.qhalt →
target.trace 1 (fun (x : Fin 1) => choice) (wrap c) = wrap (source.trace 1 (fun (x : Fin 1) => choice) c))
(T : ℕ)
(choices : Fin T → Bool)
(c : Cfg n source.Q)
(running : ∀ (t : ℕ) (ht : t < T), (source.trace t (fun (i : Fin t) => choices ⟨↑i, ⋯⟩) c).state ≠ source.qhalt)
: