theory Reduction
imports
Main
begin
section
‹Reduction Function›
text ‹This definition was taken from the developements at
\url{https://github.com/wimmers/poly-reductions}
``Karp21/Reductions.thy''.
TODO: When this repo comes into the AFP, link to original definition.›
definition is_reduction ::
"('a → 'b) → 'a set → 'b set → bool" where
"is_reduction f A B ≡ ∀a. a ∈ A ⟷ f a ∈ B "
end
¤ Dauer der Verarbeitung: 0.1 Sekunden
¤
*© Formatika GbR, Deutschland
