| products/Sources/formale Sprachen/PVS/sets_aux/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: card_comp_transitive.pvs Sprache: PVSOriginal von: PVS© |
|
||||||
|
%-------------------------------------------------------------------------
% % Transitivity properties of the cardinality comparison functions. % % For PVS version 3.2. November 4, 2004 % --------------------------------------------------------------------- % Author: Jerry James ([email protected]), University of Kansas % % % EXPORTS % ------- % prelude: functions[T1,T2], functions[T1,T3], functions[T2,T1], % functions[T2,T3], functions[T3,T1], functions[T3,T2] % sets_aux: card_comp[T1,T2], card_comp[T1,T3], card_comp[T2,T3], % card_comp_transitive[T1,T2,T3] % %------------------------------------------------------------------------- card_comp_transitive[T1: TYPE, T2: TYPE, T3: TYPE]: THEORY EXPORTING ALL WITH functions[T1, T2], functions[T1, T3], functions[T2, T1], functions[T2, T3], functions[T3, T1], functions[T3, T2], card_comp[T1, T2], card_comp[T2, T3], card_comp[T1, T3] BEGIN IMPORTING card_comp[T1, T2], card_comp[T2, T3], card_comp[T1, T3] % The following imports are for the proofs only IMPORTING function_inverse_def[T1, T2], function_inverse_def[T2, T3] IMPORTING orders@set_dichotomous[T1, T2] % card_lt card_lt_transitive: LEMMA card_lt[T1, T2] AND card_lt[T2, T3] => card_lt[T1, T3] card_lt_le_transitive: LEMMA card_lt[T1, T2] AND card_le[T2, T3] => card_lt[T1, T3] card_lt_eq_transitive: LEMMA card_lt[T1, T2] AND card_eq[T2, T3] => card_lt[T1, T3] card_le_lt_transitive: LEMMA card_le[T1, T2] AND card_lt[T2, T3] => card_lt[T1, T3] card_eq_lt_transitive: LEMMA card_eq[T1, T2] AND card_lt[T2, T3] => card_lt[T1, T3] % card_le card_le_transitive: LEMMA card_le[T1, T2] AND card_le[T2, T3] => card_le[T1, T3] card_le_eq_transitive: LEMMA card_le[T1, T2] AND card_eq[T2, T3] => card_le[T1, T3] card_eq_le_transitive: LEMMA card_eq[T1, T2] AND card_le[T2, T3] => card_le[T1, T3] % card_eq card_eq_transitive: LEMMA card_eq[T1, T2] AND card_eq[T2, T3] => card_eq[T1, T3] % card_ge card_eq_ge_transitive: LEMMA card_eq[T1, T2] AND card_ge[T2, T3] => card_ge[T1, T3] card_ge_eq_transitive: LEMMA card_ge[T1, T2] AND card_eq[T2, T3] => card_ge[T1, T3] card_ge_transitive: LEMMA card_ge[T1, T2] AND card_ge[T2, T3] => card_ge[T1, T3] % card_gt card_eq_gt_transitive: LEMMA card_eq[T1, T2] AND card_gt[T2, T3] => card_gt[T1, T3] card_ge_gt_transitive: LEMMA card_ge[T1, T2] AND card_gt[T2, T3] => card_gt[T1, T3] card_gt_eq_transitive: LEMMA card_gt[T1, T2] AND card_eq[T2, T3] => card_gt[T1, T3] card_gt_ge_transitive: LEMMA card_gt[T1, T2] AND card_ge[T2, T3] => card_gt[T1, T3] card_gt_transitive: LEMMA card_gt[T1, T2] AND card_gt[T2, T3] => card_gt[T1, T3] END card_comp_transitive ¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
