The file 'cantor.v' as Latin-1 characters

  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(␊)