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

quality100%

¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet) ¤

Versionsinformation zu Columbo

Bemerkung:

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Anfrage:

Dauer der Verarbeitung:

Sekunden

sprechenden Kalenders