content: -- File "seemingly-impossible.hs",
  -- automatically extracted from literate Haskell
  -- file http://www.cs.bham.ac.uk/~mhe/papers/seemingly-impossible.html
  --
  -- Martin Escardo, September 2007
  -- School of Computer Science, University of Birmingham, UK
  --
  -- These algorithms have been published and hence are in the
  -- public domain.
  --
  -- If you use them, I'd like to know! mailto:m.escardo@cs.bham.ac.uk
  
  data Bit = Zero | One
           deriving (Eq)
  type Natural = Integer
  type Cantor = Natural -> Bit
  (#) :: Bit -> Cantor -> Cantor 
  x # a = \i -> if i == 0 then x else a(i-1)
  forsome, forevery :: (Cantor -> Bool) -> Bool
  find :: (Cantor -> Bool) -> Cantor
  find = find_i
  forsome p = p(find(\a -> p a))
  forevery p = not(forsome(\a -> not(p a)))
  find_i :: (Cantor -> Bool) -> Cantor
  find_i p = if forsome(\a -> p(Zero # a))
             then Zero # find_i(\a -> p(Zero # a))
             else One  # find_i(\a -> p(One  # a))
  search :: (Cantor -> Bool) -> Maybe Cantor
  search p = if forsome(\a -> p a) then Just(find(\a -> p a)) else Nothing
  equal :: Eq y => (Cantor -> y) -> (Cantor -> y) -> Bool
  equal f g = forevery(\a -> f a == g a)
  coerce :: Bit -> Natural
  coerce Zero = 0
  coerce One = 1
  f, g, h :: Cantor -> Integer
  f a = coerce(a(7 * coerce(a 4) +  4 * (coerce(a 7)) + 4))
  g a = coerce(a(coerce(a 4) + 11 * (coerce(a 7))))
  h a = if a 7 == Zero
        then if a 4 == Zero then coerce(a  4) else coerce(a 11)
        else if a 4 == One  then coerce(a 15) else coerce(a  8)
  modulus :: (Cantor -> Integer) -> Natural
  modulus f = least(\n -> forevery(\a -> forevery(\b -> eq n a b --> (f a == f b))))
  least :: (Natural -> Bool) -> Natural
  least p = if p 0 then 0 else 1 + least(\n -> p(n+1))
  (-->) :: Bool -> Bool -> Bool
  p --> q = not p || q
  eq :: Natural -> Cantor -> Cantor -> Bool
  eq 0 a b = True
  eq (n+1) a b = a n == b n  &&  eq n a b
  proj :: Natural -> (Cantor -> Integer)
  proj i = \a -> coerce(a i)
  find_ii p = if p(Zero # find_ii(\a -> p(Zero # a)))
              then Zero # find_ii(\a -> p(Zero # a))
              else One  # find_ii(\a -> p(One  # a))
  find_iii :: (Cantor -> Bool) -> Cantor
  find_iii p = h # find_iii(\a -> p(h # a))
         where h = if p(Zero # find_iii(\a -> p(Zero # a))) then Zero else One
  find_iv :: (Cantor -> Bool) -> Cantor
  find_iv p = let leftbranch = Zero # find_iv(\a -> p(Zero # a))
              in if p(leftbranch)
                 then leftbranch
                 else One # find_iv(\a -> p(One # a))
  find_v :: (Cantor -> Bool) -> Cantor
  find_v p = \n ->  if q n (find_v(q n)) then Zero else One
   where q n a = p(\i -> if i < n then find_v p i else if i == n then Zero else a(i-n-1))
  find_vi :: (Cantor -> Bool) -> Cantor
  find_vi p = b 
   where b = \n -> if q n (find_vi(q n)) then Zero else One
         q n a = p(\i -> if i < n then b i else if i == n then Zero else a(i-n-1))
  find_vii :: (Cantor -> Bool) -> Cantor
  find_vii p = b 
   where b = id'(\n -> if q n (find_vii(q n)) then Zero else One)
         q n a = p(\i -> if i < n then b i else if i == n then Zero else a(i-n-1))
  data T x = B x (T x) (T x)
  code :: (Natural -> x) -> T x
  code f = B (f 0) (code(\n -> f(2*n+1))) 
                   (code(\n -> f(2*n+2)))
  decode :: T x -> (Natural -> x)
  decode (B x l r) n |  n == 0    = x
                     |  odd n     = decode l ((n-1) `div` 2)
                     |  otherwise = decode r ((n-2) `div` 2)
  id' :: (Natural -> x) -> (Natural -> x)
  id' = decode.code
  f',g',h' :: Cantor -> Integer
  f' a = a'(10*a'(3^80)+100*a'(4^80)+1000*a'(5^80)) where a' i = coerce(a i)
  g' a = a'(10*a'(3^80)+100*a'(4^80)+1000*a'(6^80)) where a' i = coerce(a i)
  h' a = a' k 
      where i = if a'(5^80) == 0 then 0    else 1000
            j = if a'(3^80) == 1 then 10+i else i
            k = if a'(4^80) == 0 then j    else 100+j 
            a' i = coerce(a i)
  pointwiseand :: [Natural] -> (Cantor -> Bool)
  pointwiseand [] = \b -> True
  pointwiseand (n:a) = \b -> (b n == One) && pointwiseand a b
  sameelements :: [Natural] -> [Natural] -> Bool
  sameelements a b = equal (pointwiseand a) (pointwiseand b)
  