| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/sets_aux/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle card_finite.pvs Sprache: PVS |
|||||||||
|
%-------------------------------------------------------------------------
% % The relationship between the cardinality comparison functions when % applied to finite sets, and the finite_sets card(S) function. % % For PVS version 3.2. November 4, 2004 % --------------------------------------------------------------------- % Author: Jerry James (jamesj@acm.org), University of Kansas % % EXPORTS % ------- % prelude: finite_sets[T1], finite_sets[T2] % sets_aux: card_comp_set[T1,T2], card_comp_set[T2,T1], % card_comp_set_props[T1,T2], card_finite[T1,T2] % %------------------------------------------------------------------------- card_finite[T1: TYPE, T2: TYPE]: THEORY BEGIN IMPORTING card_comp_set_props[T1, T2], finite_sets[T1], finite_sets[T2] n, m: VAR nat F1: VAR finite_set[T1] F2: VAR finite_set[T2] card_less_than: THEOREM FORALL F1, F2: card(F1) < card(F2) IFF card_lt(F1, F2) card_less_than_equal: THEOREM FORALL F1, F2: card(F1) <= card(F2) IFF card_le(F1, F2) card_equal: THEOREM FORALL F1, F2: card(F1) = card(F2) IFF card_eq(F1, F2) card_greater_than_equal: THEOREM FORALL F1, F2: card(F1) >= card(F2) IFF card_ge(F1, F2) card_greater_than: THEOREM FORALL F1, F2: card(F1) > card(F2) IFF card_gt(F1, F2) END card_finite ¤ Dauer der Verarbeitung: 0.10 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28