Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: coqpp_main.ml Sprache: Unknown

Original von: PVS^©

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.30 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

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.