| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/structures/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle fun_preds_partial.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% partial order properties on functions % % Author: David Lester, Manchester University % % Version 1.0 14/06/09 Initial Version %------------------------------------------------------------------------------ fun_preds_partial[T1,T2:TYPE,le1:(partial_order?[T1]), le2:(partial_order?[T2])]: THEORY BEGIN f: VAR [T1->T2] x,y: VAR T1 a,b: VAR T2 lt1(x,y) : MACRO bool = le1(x,y) AND x /= y lt2(a,b) : MACRO bool = le2(a,b) AND a /= b increasing?(f) : bool = FORALL x, y : le1(x,y) IMPLIES le2(f(x),f(y)) decreasing?(f) : bool = FORALL x, y : le1(x,y) IMPLIES le2(f(y),f(x)) strict_increasing?(f) : bool = FORALL x, y : lt1(x,y) IMPLIES lt2(f(x),f(y)) strict_decreasing?(f) : bool = FORALL x, y : lt1(x,y) IMPLIES lt2(f(y),f(x)) constant?(f) : bool = FORALL x, y : f(x) = f(y) monotonic?(f) : bool = increasing?(f) OR decreasing?(f) strict_monotonic?(f) : bool = strict_increasing?(f) OR strict_decreasing?(f) strict_increasing_is_increasing: LEMMA strict_increasing?(f) IMPLIES increasing?(f) strict_decreasing_is_decreasing: LEMMA strict_decreasing?(f) IMPLIES decreasing?(f) END fun_preds_partial ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28