| 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 relation_extension_properties.pvs Sprache: PVS |
|||||||||
|
%--------------------------------------------------------------%
% Author: Dragan Stosic % %--------------------------------------------------------------% relation_extension_props[T, U: TYPE+]: THEORY BEGIN IMPORTING relation_extension le_T: VAR equivalence[T] le_U: VAR equivalence[U] m, n: VAR [T, U] % NON-EMPTY LEMMAS extended_equiv_class_non_empty: LEMMA nonempty?[[T,U]](extended_equiv_class(rel_extension(le_T, le_U))(m)) nonempty_equivClass_impl_extended_equiv_class_non_empty: LEMMA nonempty?[T](EquivClass(le_T)(m`1)) IFF nonempty?[[T,U]](extended_equiv_class(rel_extension(le_T, le_U))(m)) nonempty_equivClass_iff_extended_equiv_classT_non_empty: LEMMA nonempty?[T](EquivClass(le_T)(m`1)) IFF nonempty?[T](extended_equiv_classT( rel_extension(le_T, le_U),proj_tuple_1, m, m)) nonempty_equivClass_iff_extended_equiv_classU_non_empty: LEMMA nonempty?[T](EquivClass(le_T)(m`1)) IFF nonempty?[U](extended_equiv_classU( rel_extension(le_T, le_U),proj_tuple_2, m, m)) % CLASS REPRESENTATIVE LEMMAS proj_tuple_1_equiv_class_representative: LEMMA m`1 = repEC_ext(le_T, le_U, m)`1 IMPLIES le_T( proj_tuple_1(repEC_ext(le_T, le_U, m)), repEC(le_T)(m`1)) proj_tuple_2_equiv_class_representative: LEMMA m`2 = repEC_ext(le_T, le_U, m)`2 IMPLIES le_U( proj_tuple_2(repEC_ext(le_T, le_U, m)), repEC(le_U)(m`2)); END relation_extension_props ¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28