Compatibility for the former internal verifier entry point #
This legacy import preserves the original verifier-membership names and the
exact guessVerify_decidesInTime theorem about SAT.satGuessVerifyNTM.
New membership clients should import Complexitylib.Classes.NP.Verifier, whose
implementation does not depend on SAT. Clients needing the old concrete machine
should import the public Complexitylib.SAT.GuessVerify compatibility surface.
theorem
Complexity.guessVerify_decidesInTime
{k : ℕ}
(M : TM k)
{L L₀ : Language}
{f : ℕ → ℕ}
(hM : M.DecidesInTime L₀ f)
(hchar : ∀ (x : List Bool), x ∈ L ↔ ∃ (y : List Bool), y.length ≤ x.length + 1 ∧ pair x y ∈ L₀)
:
The guess-and-verify machine decides any language whose members are exactly
the inputs with a short certificate accepted by M.