| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/vect_analysis/ (Wiener Entwicklungsmethode ©) Datei vom 28.9.2014 mit Größe 3 kB |
|
Quelle total_lattices.pvs Sprache: PVS |
|||||||||
|
% lattices formed by a total order.
% % Author: Alfons Geser (geser@nianet.org), National Institute of Aerospace % Date: Dec 2004 % % 8 Feb 2005, Jerry James added singleton_has_X, union_preserves_has_X, % add_preserves_has_X, X_singleton, X_union, and X_add, where % X ranges over {greatest, least}. total_lattices[T: TYPE, <=: (total_order?[T])]: THEORY BEGIN IMPORTING minmax_orders[T], lattices[T, <=] G, G1, G2: VAR (has_greatest?(<=)) L, L1, L2: VAR (has_least?(<=)) t: VAR T singleton_has_greatest: JUDGEMENT singleton(t) HAS_TYPE (has_greatest?(<=)) union_preserves_has_greatest: JUDGEMENT union(G1, G2) HAS_TYPE (has_greatest?(<=)) add_preserves_has_greatest: JUDGEMENT add(t, G) HAS_TYPE (has_greatest?(<=)) greatest_singleton: LEMMA FORALL t: greatest(<=)(singleton(t)) = t greatest_union: LEMMA FORALL G1, G2: greatest(<=)(union(G1, G2)) = IF greatest(<=)(G1) <= greatest(<=)(G2) THEN greatest(<=)(G2) ELSE greatest(<=)(G1) ENDIF greatest_add: LEMMA FORALL G, t: greatest(<=)(add(t, G)) = IF greatest(<=)(G) <= t THEN t ELSE greatest(<=)(G) ENDIF singleton_has_least: JUDGEMENT singleton(t) HAS_TYPE (has_least?(<=)) union_preserves_has_least: JUDGEMENT union(L1, L2) HAS_TYPE (has_least?(<=)) add_preserves_has_least: JUDGEMENT add(t, L) HAS_TYPE (has_least?(<=)) least_singleton: LEMMA FORALL t: least(<=)(singleton(t)) = t least_union: LEMMA FORALL L1, L2: least(<=)(union(L1, L2)) = IF least(<=)(L1) <= least(<=)(L2) THEN least(<=)(L1) ELSE least(<=)(L2) ENDIF least_add: LEMMA FORALL L, t: least(<=)(add(t, L)) = IF least(<=)(L) <= t THEN least(<=)(L) ELSE t ENDIF END total_lattices ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28