Quellcode-Bibliothek 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%

¤ 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.