Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/exact_real_arith/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 28.9.2014 mit Größe 1 kB image not shown  

Quellcode-Bibliothek test.pvs   Sprache: 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

98%


¤ 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.0.0Bemerkung:  (vorverarbeitet)  ¤

*Bot Zugriff




Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.