Quelle top.pvs Sprache: PVS

top: THEORY
%------------------------------------------------------------------------
%
%    top_limits        -- Limit of a functions [T -> real] at a point
%    top_sequence      -- Limits and operations on sequences of reals
%    top_continuity    -- Continuous functions [T -> real]
%    top_derivative    -- Differential Calculus
%    top_integral      -- Integral Calculus
%
%  See top_limits, top_sequences, top_continuity, top_derivative
%  for summary of contents
%
%      by Bruno Dutertre     Royal Holloway & Bedford New College
%         Rick Butler        NASA Langley Research Center
%         Cesar Munoz        National Institute For Aerospace
%         David Lester       Manchester University
%         Anthony Narkawicz  NASA Langley Research Center
%
%      Version 1.0    last modified 7/12/96
%      Version 1.1    updated to PVS 2.3   8/1/2000 by Rick Butler
%      Version 1.2    updated to PVS 2.3   3/1/2001 by Bruno in
%                     a slightly different way.
%                     Bruno ELIMINATED "const_fun" and associated
%                     conversion.  Now uses prelude "K_conversion".
%                     RWB added back "const_fun" definition to
%                     help with upward compatibility (real_fun_ops).
%
%                     Bruno changed "below_bounded" to "bounded_below?"
%                           and changed structure of its definition.
%                     Bruno changed "above_bounded" to "bounded_above?"
%                           and changed structure of its definition.
%      Version 1.3    Added theorem in derivatives_more 5/22/01
%      Version 1.4    put back "const_fun" for PVS2.4
%      Version 1.5    Used MACRO feature to rename all predicates
%                     in real_fun_preds, adding ? to name    2/28/02
%      Version 1.6    Added quadratic theory in "special_functions"  3/14/02
%      Version 1.7    quadratic theory moved to reals
%      Version 1.8    removed open? assugmption in integral theories 4/2/03
%      Version 1.9    removed duplicates with reals library 4/14/03
%      Version 2.0    proved step_function_integrable? in integral_step
%      Version 2.1    ln_exp moved to lnexp library (12/8/03)
%      Version 2.2    David Lester added derivatives of inverse functions
%                     and derivative of sqrt
%      Version 2.3    NAME CHANGES -- See File NAME-CHANGES.txt
%      Version 2.4    ADDED integral_chg_var and integral_diff_doms
%      Version 2.5    NAME CHANGES: continuous2 --> cont_fun
%      Version 2.6    moved nth_derivatives, and taylors here from series
%      Version 2.7    add integration_by_parts and indefinite_integral 7/20/07
%      Version 2.8    metric spaces, compactness, uniform continuity
%
%  NOTE: top_integral relies on the Di Vito strategy package
%  NOTE: theories named  *_scaf are proof scaffolding, not intended for users
%------------------------------------------------------------------------
BEGIN

  IMPORTING top_limits,
            top_sequences,
            top_continuity,
            top_metric_spaces,
            top_derivative,
     top_riesz_representation,
            top_integral  %  requires Manip strategies

END top

quality100%

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

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.