test: THEORY

BEGIN

  IMPORTING trigx,
            hyperbolicx

  new_pi_bnds:    LEMMA % 60 dp
        3.141592653589793238462643383279502884197169399375105820974944 < pi AND
   pi < 3.141592653589793238462643383279502884197169399375105820974945

  new_ln2_bnds:   LEMMA % 60 dp
    LET l = ln(2) IN
        0.693147180559945309417232121458176568075500134360255254120680 < l  AND
    l < 0.693147180559945309417232121458176568075500134360255254120681

  new_e_bnds:     LEMMA % 60 dp
        2.718281828459045235360287471352662497757247093699959574966967 < e  AND
    e < 2.718281828459045235360287471352662497757247093699959574966968

  new_sqrt2_bnds: LEMMA % 60 dp
    LET s = sqrt(2) IN
        1.414213562373095048801688724209698078569671875376948073176679 < s  AND
    s < 1.414213562373095048801688724209698078569671875376948073176680

%%% THE COMMENTED LEMMAS CAN BE PROVED AS THE PREVIOUS LEMMAS, BUT THEY
%%% TAKE TOO MUCH TIME (CAM)

%  new_sin1_bnds: LEMMA % 60 dp
%    LET s = sin(1) IN
%        0.841470984807896506652502321630298999622563060798371065672751 < s  AND
%    s < 0.841470984807896506652502321630298999622563060798371065672752

%  new_cos1_bnds: LEMMA % 60 dp
%    LET c = cos(1) IN
%        0.540302305868139717400936607442976603732310420617922227670097 < c  AND
%    c < 0.540302305868139717400936607442976603732310420617922227670098

END test