%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%     Exercise Set 5: Real Number Proving
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

realproving : THEORY
BEGIN

  googol     : MACRO real = 10^100
  googolplex : MACRO real = 10^googol

  %
  % Exercise 1
  %

  googolplex_gt_googol2 : LEMMA
    googolplex > googol * googol

  %
  % Exercise 2
  %

  %% Prove that y*(1-x)*(1-x) <= 0 if y <= 0

  %
  % Exercise 3
  %

  IMPORTING reals@sqrt

  simplesqrt1 : LEMMA
    FORALL (nnx:nnreal) : 
      nnx <= 1 IMPLIES
        sqrt(1-nnx) <= 1

  %
  % Exercise 4
  %

  x,y : VAR real
  nx  : VAR negreal
  px  : VAR posreal

  p1 : LEMMA
   px+nx <= 0
   IMPLIES   
     1/px+1/nx >= px*nx

  p2 : LEMMA
    (px*px - 1)/(px+1) + 1 = px

  p3 : LEMMA
    x >= 20 AND
    y >= 10 IMPLIES
    x*y - 10*x - 20*y + 200 >= 0 

END realproving