cantor.v

  1  D  e  f  i  n  i  t  i  o  n     e  n  u  m  e  r  a  t  i  o  n  :     T  y  p  e     :  =     n  a  t     -  >     (  n  a  t  -  >     n  a  t  )  . EOL()
  2  D  e  f  i  n  i  t  i  o  n     d  i  a  g  o  n  a  l     (  g  :     e  n  u  m  e  r  a  t  i  o  n  )     (  n  :     n  a  t  )  :     n  a  t     :  =     g     n     n  . EOL()
  3  D  e  f  i  n  i  t  i  o  n     d  i  f  f  e  r  e  n  t     (  f  :     n  a  t  -  >  n  a  t  )     (  g  :     n  a  t  -  >  n  a  t  )  :     P  r  o  p     :  =     e  x  i  s  t  s     n  :     n  a  t  ,     f  (  n  )  <  >  g  (  n  )  . EOL()
  4 EOL()
  5  T  h  e  o  r  e  m     c  a  n  t  o  r     :     f  o  r  a  l  l     g  :     e  n  u  m  e  r  a  t  i  o  n  ,     e  x  i  s  t  s     f  :     n  a  t  -  >  n  a  t  , EOL()
  6           f  o  r  a  l  l     i  :     n  a  t  ,     d  i  f  f  e  r  e  n  t     (  g     i  )     f  . EOL()
  7  i  n  t  r  o  .                    (  *     L  e  t     g     b  e     a  n     e  n  u  m  e  r  a  t  i  o  n     o  f     a  l  l     f  u  n  c  t  i  o  n  s  .     *  ) EOL()
  8  e  x  i  s  t  s     (  f  u  n     k  =  >  S  (  d  i  a  g  o  n  a  l     g     k  )  )  . EOL()
  9  i  n  t  r  o  .                    (  *     L  e  t     i     b  e     a     r  o  w  -  -  a  n     e  l  e  m  e  n  t     o  f     t  h  e     e  n  u  m  e  r  a  t  i  o  n  .     *  ) EOL()
 10  e  x  i  s  t  s     i  . EOL()
 11  a  u  t  o  . EOL()
 12  Q  e  d  . EOL()