| 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 complementary_orders.pvs Sprache: PVS |
|||||||||
|
% Ordered sets (T, <=) that have a "complement" function, i.e.,
% an involutorian, anti-monotone function from T to T. % complementary_orders[T: TYPE+]: THEORY BEGIN IMPORTING bounded_orders[T] rel: VAR pred[[T, T]] C: VAR [T -> T] t, t1, t2: VAR T S: VAR set[T] complement?(rel)(C): bool = C o C = id[T] & preserves(C, rel, converse(rel)) % complement_is_bijective: JUDGEMENT % (complement?(rel)) SUBTYPE_OF (bijective?[T, T]) complement_complement: LEMMA FORALL (C: (complement?(rel))): C(C(t)) = t image_complement: LEMMA FORALL (C: (complement?(rel))): image(C, image(C, S)) = S inverse_complement: LEMMA FORALL (C: (complement?(rel))): inverse[T, T](C) = C % inverse_complement_is_complement: JUDGEMENT % inverse[T, T](C: (complement?(rel))) HAS_TYPE (complement?(rel)) le_complement: LEMMA FORALL (C: (complement?(rel))): rel(C(t1), C(t2)) IFF rel(t2, t1) upper_bound_complement: LEMMA FORALL (C: (complement?(rel))): upper_bound?[T](t, S, rel) IFF lower_bound?[T](C(t), image(C, S), rel) bounded_above_complement: LEMMA FORALL (C: (complement?(rel))): bounded_above?[T](S, rel) IFF bounded_below?[T](image(C, S), rel) least_upper_bound_complement: LEMMA FORALL (C: (complement?(rel))): least_upper_bound?[T](t, S, rel) IFF greatest_lower_bound?[T](C(t), image(C, S), rel) least_bounded_above_complement: LEMMA FORALL (C: (complement?(rel))): least_bounded_above?[T](S, rel) IFF greatest_bounded_below?[T](image(C, S), rel) lub_complement: LEMMA FORALL (rel: (antisymmetric?[T]), C: (complement?(rel)), S: (least_bounded_above?(rel))): lub[T](rel)(S) = C(glb[T](rel)(image(C, S))) glb_complement: LEMMA FORALL (rel: (antisymmetric?[T]), C: (complement?(rel)), S: (greatest_bounded_below?(rel))): glb[T](rel)(S) = C(lub[T](rel)(image(C, S))) END complementary_orders ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28