Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: abs_rews.pvs Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.