| 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 2 kB |
|
Quellcode-Bibliothek card_comp_set_transitive.pvs Sprache: PVS |
|||||||||
|
%-------------------------------------------------------------------------
% % Transitivity properties of the set cardinality comparison functions. % % For PVS version 3.2. November 4, 2004 % --------------------------------------------------------------------- % Author: Jerry James (jamesj@acm.org), University of Kansas % % EXPORTS % ------- % sets_aux: card_comp_set[T1,T2], card_comp_set[T1,T3], % card_comp_set[T2,T3], card_comp_set_transitive[T1,T2,T3] % %------------------------------------------------------------------------- card_comp_set_transitive[T1: TYPE, T2: TYPE, T3: TYPE]: THEORY EXPORTING ALL WITH card_comp_set[T1, T2], card_comp_set[T2, T3], card_comp_set[T1, T3] BEGIN IMPORTING card_comp_set[T1, T2], card_comp_set[T2, T3], card_comp_set[T1, T3] % The following import is for the proofs only IMPORTING orders@set_dichotomous S1: VAR set[T1] S2: VAR set[T2] S3: VAR set[T3] % card_lt card_lt_transitive: LEMMA FORALL S1, S2, S3: card_lt(S1, S2) AND card_lt(S2, S3) => card_lt(S1, S3) card_lt_le_transitive: LEMMA FORALL S1, S2, S3: card_lt(S1, S2) AND card_le(S2, S3) => card_lt(S1, S3) card_lt_eq_transitive: LEMMA FORALL S1, S2, S3: card_lt(S1, S2) AND card_eq(S2, S3) => card_lt(S1, S3) card_le_lt_transitive: LEMMA FORALL S1, S2, S3: card_le(S1, S2) AND card_lt(S2, S3) => card_lt(S1, S3) card_eq_lt_transitive: LEMMA FORALL S1, S2, S3: card_eq(S1, S2) AND card_lt(S2, S3) => card_lt(S1, S3) % card_le card_le_transitive: LEMMA FORALL S1, S2, S3: card_le(S1, S2) AND card_le(S2, S3) => card_le(S1, S3) card_le_eq_transitive: LEMMA FORALL S1, S2, S3: card_le(S1, S2) AND card_eq(S2, S3) => card_le(S1, S3) card_eq_le_transitive: LEMMA FORALL S1, S2, S3: card_eq(S1, S2) AND card_le(S2, S3) => card_le(S1, S3) % card_eq card_eq_transitive: LEMMA FORALL S1, S2, S3: card_eq(S1, S2) AND card_eq(S2, S3) => card_eq(S1, S3) % card_ge card_eq_ge_transitive: LEMMA FORALL S1, S2, S3: card_eq(S1, S2) AND card_ge(S2, S3) => card_ge(S1, S3) card_ge_eq_transitive: LEMMA FORALL S1, S2, S3: card_ge(S1, S2) AND card_eq(S2, S3) => card_ge(S1, S3) card_ge_transitive: LEMMA FORALL S1, S2, S3: card_ge(S1, S2) AND card_ge(S2, S3) => card_ge(S1, S3) % card_gt card_eq_gt_transitive: LEMMA FORALL S1, S2, S3: card_eq(S1, S2) AND card_gt(S2, S3) => card_gt(S1, S3) card_ge_gt_transitive: LEMMA FORALL S1, S2, S3: card_ge(S1, S2) AND card_gt(S2, S3) => card_gt(S1, S3) card_gt_eq_transitive: LEMMA FORALL S1, S2, S3: card_gt(S1, S2) AND card_eq(S2, S3) => card_gt(S1, S3) card_gt_ge_transitive: LEMMA FORALL S1, S2, S3: card_gt(S1, S2) AND card_ge(S2, S3) => card_gt(S1, S3) card_gt_transitive: LEMMA FORALL S1, S2, S3: card_gt(S1, S2) AND card_gt(S2, S3) => card_gt(S1, S3) END card_comp_set_transitive ¤ 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.0.0Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28