| 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 1 kB |
|
Quelle select_minmax.pvs Sprache: PVS |
|||||||||
|
%
% % Purpose : properties of the min/max of the results % from a set of parallel nodes % % select_minmax[N: posnat, T: TYPE+, <=: (total_order?[T])]: THEORY BEGIN IMPORTING finite_sets@finite_sets_minmax[T, <=], node[N, T], relations_extra[T] node_set: VAR non_empty_finite_set[below(N)] v: VAR vec n: VAR below(N) t: VAR T v_min(v, node_set): T = min(image(v, node_set)) v_max(v, node_set): T = max(image(v, node_set)) v_min_witness: LEMMA EXISTS n: node_set(n) AND v_min(v, node_set) = v(n) v_max_witness: LEMMA EXISTS n: node_set(n) AND v_max(v, node_set) = v(n) v_min_is_min: LEMMA node_set(n) IMPLIES v_min(v, node_set) <= v(n) v_max_is_max: LEMMA node_set(n) IMPLIES v(n) <= v_max(v, node_set) min_le_max: LEMMA v_min(v, node_set) <= v_max(v, node_set) min_le_max_alt: LEMMA v_max(v, node_set) = v_min(v, node_set) IFF (v_max(v, node_set) <= v_min(v, node_set)) v_minmax_choose: LEMMA uniform?(v, t)(node_set) IFF (v_max(v, node_set) = v_min(v, node_set) AND v_min(v, node_set) = t) v_minmax_choose_alt: LEMMA uniform?(v, t)(node_set) IFF (v_max(v, node_set) <= t AND t <= v_min(v, node_set)) END select_minmax ¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28