Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/PVS/reals/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 28.9.2014 mit Größe 2 kB

SSL exponent_props.pvs Interaktion und
PortierbarkeitPVS

exponent_props : THEORY
%-------------------------------------------------------------------------
%  More properties of expt
%
%      by Bruno Dutertre    Royal Holloway & Bedford New College
%
%     9/10/00  -- removed duplications with prelude  RWB
%                 changed names of
%
%                    expt_mult --> expt_of_mult
%                    expt_div  --> expt_of_div
%                    expt_inv  --> expt_of_inv
%
%                 to eliminate duplications with prelude
%
%  Note. This library is retained for upward compatibility only.  New
%        users should use the prelude theorems.
%-------------------------------------------------------------------------
BEGIN

  n, m: VAR nat
  p: VAR posnat
  x, y: VAR real
  z: VAR nzreal
  n0x, n0y: VAR nzreal

%  JUDGEMENT expt(z: nzreal, m: nat) HAS_TYPE nzreal

  abs_expt    : LEMMA abs(expt(x, n)) = expt(abs(x), n)

  expt_ne_0:    LEMMA expt(z, n) /= 0;

%% The following is named abs_of_expt_inv in prelude

  abs_expt_inv: LEMMA abs(1 / expt(z, n)) = 1 / expt(abs(z),n)

  i:  VAR int
  pn: VAR posnat

% The following all appear in the prelude under different names

  zero_hat : LEMMA 0^pn = 0

  mult_hat : LEMMA (n0x * n0y) ^i = n0x^i * n0y^i

  div_hat  : LEMMA (n0x / n0y)^i = n0x^i / n0y^i

  inv_hat  : LEMMA (1 / n0x)^i = 1 / n0x^i

  abs_hat  : LEMMA abs(n0x^i) = abs(n0x)^i

  AUTO_REWRITE+ expt_x0         % LEMMA x^0 = 1
  AUTO_REWRITE+ expt_x1         % LEMMA x^1 = x
  AUTO_REWRITE+ expt_1i         % LEMMA 1^i = 1
  AUTO_REWRITE+ zero_hat

%%  a, b: VAR posreal
%%  lt1x: VAR { a | a < 1}
%%  gt1x: VAR { a | 1 < a }
%%  expt_lt1_bound1 : LEMMA  expt(lt1x, n) <= 1   %%  In Prelude
%%  expt_lt1_bound2 : LEMMA  expt(lt1x, p) < 1    %%  In Prelude
%%  expt_gt1_bound1 : LEMMA  1 <= expt(gt1x, n)  %%  In Prelude
%%  expt_gt1_bound2 : LEMMA  1 < expt(gt1x, p)   %%  In Prelude
%%  nnx: VAR nonneg_real
%%  expt_lt1_le     : LEMMA nnx < 1 => nnx^pn <= nnx %%  In Prelude
%%  large_expt      : LEMMA 1 < a  IMPLIES (FORALL b: EXISTS n: b < expt(a, n))
%%  small_expt      : LEMMA a < 1  IMPLIES (FORALL b: EXISTS n: expt(a, n) < b)
END exponent_props

quality95%

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.14Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Eine klare Vorstellung vom Zielzustand

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.