cantor.v

  1  V  a  r  i  a  b  l  e   G   :   S  e  t  . EOL()
  2  V  a  r  i  a  b  l  e   o  p  e  r  a  t  i  o  n   :   G   -  >   G   -  >   G  . EOL()
  3  V  a  r  i  a  b  l  e   e   :   G  . EOL()
  4  V  a  r  i  a  b  l  e   i  n  v   :   G   -  >   G  . EOL()
  5 EOL()
  6  I  n  f  i  x      ×      :  =   o  p  e  r  a  t  i  o  n   (  a  t   l  e  v  e  l   5  0  ,   l  e  f  t   a  s  s  o  c  i  a  t  i  v  i  t  y  )  . EOL()
  7 EOL()
  8  H  y  p  o  t  h  e  s  i  s   a  s  s  o  c  i  a  t  i  v  i  t  y   :   f  o  r  a  l  l   x   y   z   :   G  ,   (  x   ×   y  )   ×   z   =   x   ×   (  y   ×   z  )  . EOL()
  9  H  y  p  o  t  h  e  s  i  s   i  d  e  n  t  i  t  y   :   f  o  r  a  l  l   x   :   G  ,   (  x   ×   e  )   =   e   /  \   e   ×   x   =   x  . EOL()
 10  H  y  p  o  t  h  e  s  i  s   i  n  v  e  r  s  e   :   f  o  r  a  l  l   x   :   G  ,   (  x   ×   i  n  v   x  )   =   e   /  \   i  n  v   x   ×   x   =   x  . EOL()
 11 EOL()
 12  T  h  e  o  r  e  m   l  a  t  i  n  _  s  q  u  a  r  e  _  p  r  o  p  e  r  t  y   :   f  o  r  a  l  l   a   b   :   G  ,   e  x  i  s  t  s   x   :   G  ,   a   ×   x   =   b  . EOL()
 13    i  n  t  r  o  s   a   b  . EOL()
 14    e  x  i  s  t  s   (  i  n  v   a   ×   b  )  . EOL()
 15    r  e  w  r  i  t  e   <  -   a  s  s  o  c  i  a  t  i  v  i  t  y  . EOL()
 16    d  e  s  t  r  u  c  t   i  n  v  e  r  s  e   w  i  t  h   (  x  :  =  a  )   a  s   [  H   _  ]  . EOL()
 17    r  e  w  r  i  t  e   H  . EOL()
 18    d  e  s  t  r  u  c  t   i  d  e  n  t  i  t  y   w  i  t  h   (  x  :  =  b  )   a  s   [  _   H  '  ]  . EOL()
 19    t  r  i  v  i  a  l  . EOL()
 20  Q  e  d  . EOL()