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/ints/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 775 B

Quelle abs_rews.pvs Sprache: PVS

abs_rews : THEORY
%------------------------------------------------------------------------
%
% Author: Rick Butler                  NASA Langley Research Center
%
% This introduces some lemmas and rewrites especially useful for integer
% arguments.  See also reals@abs_lems
%
% To prevent name duplication with reals@abs_lems these rewrites are given
% non-standard names.
%------------------------------------------------------------------------
BEGIN

  n: VAR nat
  x: VAR real

  abs_nat_rew      : LEMMA abs(n) = n

  abs_0_rew        : LEMMA abs(0) = 0

  abs_neg_rew      : LEMMA abs(-x) = abs(x)

  sgn_nat_rew      : LEMMA sgn(n) = 1

  AUTO_REWRITE+  abs_0_rew
  AUTO_REWRITE+  abs_nat_rew
  AUTO_REWRITE+  abs_neg_rew
  AUTO_REWRITE+  sgn_nat_rew

END abs_rews

quality100%

¤ Dauer der Verarbeitung: 0.12 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.