| 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 rr_rel.pvs Sprache: PVS |
|||||||||
|
%--------------------------------------------------------------%
% Author: Dragan Stosic % %--------------------------------------------------------------% rr_rel[T, U: TYPE+]: THEORY BEGIN IMPORTING relation_extension[T, U], relation_inverse_extension[T, U] le_T: VAR equivalence[T] le_U: VAR equivalence[U] n: VAR [T, U] f: VAR [T -> U] g: VAR [U -> T] % Definition 1: % Relation [T, U] % Domain T partitioned with the le_T equivalence relation % Codomain U partitioned with the le_U equivalence relation % Functions: f[ T -> U] and g [U -> T] RR(le_T, le_U, f, g):set[[T,U]] = { (n) | LET Fn = (n`1,f(n`1)), Gn = (g(n`2), n`2), GFn = (g(n`2), f(n`1)) IN rel_extension(le_T, le_U)(Fn, Gn) OR rel_extension(le_T, le_U)(GFn, Fn) OR rel_extension(le_T, le_U)(GFn, Gn) } % Definition 2: % Relation [T, U] % Domain T partitioned with the le_T equivalence relation % Codomain U partitioned with the le_U equivalence relation % Functions: f[ T -> U] and g [U -> T] RR2(le_T, le_U, f, g):set[[T,U]] = { (n) | LET Fn = (n`1,f(n`1)), Gn = (g(n`2), n`2), GFn = (g(n`2), f(n`1)) IN rel_inv_extension2(le_T, le_U, f, g)(Fn, Gn) OR rel_inv_extension2(le_T, le_U, f, g)(GFn, Fn) OR rel_inv_extension2(le_T, le_U, f, g)(GFn, Gn) } g_conistent_with_RR: LEMMA le_T( n`1, g(n`2) ) IMPLIES RR(le_T, le_U, f, g)(n) f_conistent_with_RR: LEMMA le_U( n`2, f(n`1) ) IMPLIES RR(le_T, le_U, f, g)(n) % Connection between RR and RR2 RR_functional_conditional_equal_RR2: LEMMA LET GFn=(g(n`2),f(n`1)) IN RR(le_T, le_U, f, g)(GFn) IFF RR2(le_T, le_U, f, g)(n) END rr_rel ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28