@[reducible, inline]

abbrev PolyTimeReducible {Γ : Type} (A B : Set (List Γ)) : Prop

Sipser, Lecture 14. Polynomial-time mapping reducibility A ≤_P B: A reduces to B via a polynomial-time computable function f with w ∈ A ↔ f w ∈ B. (Alias for TuringMachine.PolyReducible.)

theorem inP_of_polyTimeReducible {Γ : Type} {A B : Set (List Γ)} (hAB : PolyTimeReducible A B) (hB : TuringMachine.InP B) : TuringMachine.InP A

Sipser, Lecture 14. If A ≤_P B and B ∈ P, then A ∈ P.