For a binary word , define where is the binary expansion of . Shortlex Order We say that encodes a natural number as a binary word, while decodes it. Partial Numerical Function