∀ (n : UInt32),
  n.toNat < 16 →
    n.toNat < 10 →
      ¬((n.toNat + 48) % 4294967296 < 55296 ∨
            57343 < (n.toNat + 48) % 4294967296 ∧ (n.toNat + 48) % 4294967296 < 1114112) →
        False