| Quellcodebibliothek Statistik Leitseite 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 ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28