|
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.26 Sekunden
(vorverarbeitet)
¤
|
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.
|
