| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/VDM/ (Wiener Entwicklungsmethode ©) Datei vom 15.2.2013 mit Größe 83 kB |
|
Quelle finite_orders.pvs Sprache: PVS |
|||||||||
|
% orders on a finite type have special properties:
% e.g., every lattice is complete; every strict-order is well-founded. % % Author: Alfons Geser, National Institute of Aerospace % Date: Dec 2004/Jan 2005 finite_orders[T: TYPE+]: THEORY BEGIN ASSUMING finite_type: ASSUMPTION is_finite_type[T] ENDASSUMING IMPORTING bounded_orders[T], finite_types[T] R: VAR pred[[T, T]] S: VAR (nonempty?[T]) % used in proofs % lattice properties finite_lower_semilattice_is_complete: LEMMA greatest_bounded_below?(R)(emptyset) & lower_semilattice?(R) => complete_lower_semilattice?(R) finite_upper_semilattice_is_complete: LEMMA least_bounded_above?(R)(emptyset) & upper_semilattice?(R) => complete_upper_semilattice?(R) finite_lattice_is_complete: JUDGEMENT (lattice?) SUBTYPE_OF (complete_lattice?) % well-foundedness properties finite_strict_order_is_well_founded: JUDGEMENT (strict_order?) SUBTYPE_OF (well_founded?[T]) finite_strict_total_order_is_well_ordered: JUDGEMENT (strict_total_order?) SUBTYPE_OF (well_ordered?[T]) END finite_orders ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28