For a fixed natural number and a standard encoding of natural numbers, validate the input and compare its encoded value with . This decides . A well-ordering argument can prove that an upward-closed set of natural numbers has this form without calculating its least element. A decider may contain that fixed least element in its finite description; its existence does not give a uniform method to discover the least element from another program.
New to topics? Read the docs here!