|
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
¤ Dauer der Verarbeitung: 0.22 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
