| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle bounded_order_props.pvs Sprache: PVS |
|||||||||
|
%------------------------------------------------------------------------------
% % These are properties of bounded partial orders. Because we're importing the % the partial order, it needn't clutter up the theories. % % We're defining the least_upper_bound and greatest_lower_bound operators % (lub(S) and glb(S) respectively) for all suitable sets S. Notice that they % needn't be nonempty. % %------------------------------------------------------------------------------ bounded_order_props[T:TYPE,<=:(partial_order?[T])]: THEORY BEGIN IMPORTING sets[T], bounded_orders[T] x,y: VAR T S,A,B: VAR set[T] above?(A,B): bool = FORALL (x:(B)): EXISTS (y:(A)): x <= y below?(A,B): bool = FORALL (x:(B)): EXISTS (y:(A)): y <= x lub_set?(S):bool = least_bounded_above?(<=)(S) singleton_is_lub_set: JUDGEMENT (singleton?) SUBTYPE_OF (lub_set?) SA,XA,YA: VAR (lub_set?) lub(SA): {x | bounded_orders[T].least_upper_bound?(x,SA,<=)} lub_rew: LEMMA lub(SA) = lub(<=)(SA) lub_singleton: LEMMA lub(singleton(x)) = x lub_lem: LEMMA lub(SA) = x IFF bounded_orders[T].least_upper_bound?(x,SA,<=) above_lub: LEMMA above?(XA,YA) IMPLIES lub(YA) <= lub(XA) glb_set?(S):bool = bounded_orders[T].greatest_bounded_below?(<=)(S) singleton_is_glb_set: JUDGEMENT (singleton?) SUBTYPE_OF (glb_set?) SB,XB,YB: VAR (glb_set?) glb(SB): {x | bounded_orders[T].greatest_lower_bound?(x,SB,<=)} glb_rew: LEMMA glb(SB) = glb(<=)(SB) glb_singleton: LEMMA glb(singleton(x)) = x glb_lem: LEMMA glb(SB) = x IFF bounded_orders[T].greatest_lower_bound?(x,SB,<=) below_glb: LEMMA below?(XB,YB) IMPLIES glb(XB) <= glb(YB) END bounded_order_props ¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28