| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/fault_tolerance/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 kB |
|
Quelle relations_extra.pvs Sprache: PVS |
|||||||||
|
%
% % Purpose: rewrite rules for the properties that % binary relations may have % % Author: Alfons Geser (geser@nianet.org), NIA % % relations_extra[T: TYPE]: THEORY BEGIN IMPORTING relations[T], orders[T] x, y, z: VAR T R: VAR pred[[T, T]] p: VAR pred[T] asymmetric?(R): bool = FORALL x, y: NOT R(x, y) OR NOT R(y, x) strict_order_is_asymmetric: JUDGEMENT (strict_order?) SUBTYPE_OF (asymmetric?) asymmetric_is_antisymmetric: JUDGEMENT (asymmetric?) SUBTYPE_OF (antisymmetric?) asymmetric_is_irreflexive: JUDGEMENT (asymmetric?) SUBTYPE_OF (irreflexive?) reflexive: LEMMA FORALL (R: (reflexive?)): FORALL x: R(x, x) irreflexive: LEMMA FORALL (R: (irreflexive?)): FORALL x: NOT R(x, x) symmetric: LEMMA FORALL (R: (symmetric?)): FORALL x, y: R(x, y) => R(y, x) antisymmetric: LEMMA FORALL (R: (antisymmetric?)): FORALL x, y: R(x, y) & R(y, x) => x = y asymmetric: LEMMA FORALL (R: (asymmetric?)): FORALL x, y: NOT R(x, y) OR NOT R(y, x) % connected? is the same as trichotomous? % connected: LEMMA FORALL (R: (connected?)): x = y OR R(x, y) OR R(y, x) transitive: LEMMA FORALL (R: (transitive?)): FORALL x, y, z: R(x, y) & R(y, z) => R(x, z) dichotomous: LEMMA FORALL (R: (dichotomous?)): FORALL x, y: R(x, y) OR R(y, x) trichotomous: LEMMA FORALL (R: (trichotomous?)): FORALL x, y: R(x, y) OR R(y, x) OR x = y dichotomous_is_trichotomous: JUDGEMENT (dichotomous?) SUBTYPE_OF (trichotomous?) well_founded: LEMMA FORALL (R: (well_founded?)): FORALL p: (EXISTS y: p(y)) IMPLIES EXISTS (y: (p)): FORALL (x: (p)): NOT R(x, y) reflexive_closure(R): (reflexive?) = union(R, =) irreflexive_kernel(R): (irreflexive?) = difference(R, =) symmetric_closure(R): (symmetric?) = union(R, converse(R)) symmetric_kernel(R): (symmetric?) = intersection(R, converse(R)) reflexive_closure_preserves_transitive: JUDGEMENT reflexive_closure(R: (transitive?)) HAS_TYPE (preorder?) strict_order_to_partial_order: JUDGEMENT reflexive_closure(R: (strict_order?)) HAS_TYPE (partial_order?) reflexive_closure_dichotomous: JUDGEMENT reflexive_closure(R: (trichotomous?)) HAS_TYPE (dichotomous?) strict_total_order_to_total_order: JUDGEMENT reflexive_closure(R: (strict_total_order?)) HAS_TYPE (total_order?) partial_order_to_strict_order: JUDGEMENT irreflexive_kernel(R: (partial_order?)) HAS_TYPE (strict_order?) irreflexive_kernel_trichotomous: JUDGEMENT irreflexive_kernel(R: (dichotomous?)) HAS_TYPE (trichotomous?) total_order_to_strict_total_order: JUDGEMENT irreflexive_kernel(R: (total_order?)) HAS_TYPE (strict_total_order?) symmetric_kernel_of_preorder: JUDGEMENT symmetric_kernel(R: (preorder?)) HAS_TYPE (equivalence?) END relations_extra ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28