| products/sources/formale Sprachen/PVS/fault_tolerance/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: root.bib Sprache: PVSOriginal von: PVS© |
|
||||||
|
%
% % Purpose: rewrite rules for inequalities involving floor and ceiling % % floor_ceiling_ineq: THEORY BEGIN a, b: VAR real i: VAR integer ge_floor_l: LEMMA floor(a) >= i IFF a >= i ge_floor_r: LEMMA i >= floor(a) IFF i+1 > a gt_floor_l: LEMMA floor(a) > i IFF a >= i+1 gt_floor_r: LEMMA i > floor(a) IFF i > a le_floor_l: LEMMA floor(a) <= i IFF a < i+1 le_floor_r: LEMMA i <= floor(a) IFF i <= a lt_floor_l: LEMMA floor(a) < i IFF a < i lt_floor_r: LEMMA i < floor(a) IFF i+1 <= a floor_monotone: LEMMA a <= b IMPLIES floor(a) <= floor(b) ge_ceiling_l: LEMMA ceiling(a) >= i IFF a > i-1 ge_ceiling_r: LEMMA i >= ceiling(a) IFF i >= a gt_ceiling_l: LEMMA ceiling(a) > i IFF a > i gt_ceiling_r: LEMMA i > ceiling(a) IFF i-1 >= a le_ceiling_l: LEMMA ceiling(a) <= i IFF a <= i le_ceiling_r: LEMMA i <= ceiling(a) IFF i-1 < a lt_ceiling_l: LEMMA ceiling(a) < i IFF a <= i-1 lt_ceiling_r: LEMMA i < ceiling(a) IFF i < a ceiling_monotone: LEMMA a <= b IMPLIES ceiling(a) <= ceiling(b) END floor_ceiling_ineq ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
