| 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_inverse_extension.pvs Sprache: PVS |
|||||||||
|
%--------------------------------------------------------------%
% Author: Dragan Stosic % %--------------------------------------------------------------% relation_inverse_extension[T, U: TYPE+]: THEORY BEGIN IMPORTING relation_inverse_image[T, U], relation_inverse_image[U, T], relation_extension[T, U] f: VAR [T -> U] g: VAR [U -> T] m, n :VAR [T, U] re_U: VAR equivalence[U] re_T: VAR equivalence[T] l_T(re_U, f):pred[[T, T]] = image_inverse(re_U, f) le_U_induces_equivalence :JUDGEMENT l_T(re_U, f) HAS_TYPE equivalence[T] l_U(re_T, g):pred[[U, U]] = image_inverse(re_T, g) le_T_induces_equivalence: JUDGEMENT l_U(re_T, g) HAS_TYPE equivalence[U] % etended equivalence relation based on inverse images of equivalence % relations rel_inv_extension(re_T, re_U, f, g) : set[[[T, U], [T, U]]] = { (m, n) | l_T(re_U, f)(n`1,m`1) AND l_U(re_T, g)(n`2,m`2) } rel_inv_extension_is_equivalence: JUDGEMENT rel_inv_extension(re_T, re_U, f, g) HAS_TYPE equivalence[[T, U]] % connection between two relations: % rel_extension and rel_image_extension rel_extension_IFF_rel_ext : LEMMA LET GFm=(g(m`2),f(m`1)), GFn=(g(n`2),f(n`1)) IN rel_extension(re_T, re_U)(GFm, GFn) = rel_inv_extension(re_T, re_U, f, g)(n, m) % replaced: definition of the rel_inv_extension using the rel_extension rel_inv_extension2(re_T, re_U, f, g):set[[[T, U], [T, U]]] = { (n, m) | LET GFm=(g(m`2),f(m`1)), GFn=(g(n`2),f(n`1)) IN rel_extension(re_T, re_U)(GFm, GFn) } rel_inv_extension2_is_equivalence: JUDGEMENT rel_inv_extension2(re_T, re_U, f, g) HAS_TYPE equivalence[[T, U]] END relation_inverse_extension ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28