| products/sources/formale Sprachen/PVS/vectors/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: patch-101.lisp Sprache: PVSOriginal von: PVS© |
|
||||||
|
%------------------------------------------------------------------------------
% Cross Products % % Author: David Lester, Manchester University, NIA, Universite Perpignan % % % Version 1.0 17/08/07 Initial Version %------------------------------------------------------------------------------ cross_product[T1,T2:TYPE]: THEORY BEGIN A: VAR set[T1] B: VAR set[T2] NA: VAR (nonempty?[T1]) NB: VAR (nonempty?[T2]) X: VAR set[[T1,T2]] a: VAR T1 b: VAR T2 z: VAR [T1,T2] cross_product(A,B):set[[T1,T2]] = {z | A(z`1) AND B(z`2)} projection_1(X):set[T1] = {a | EXISTS z: X(z) AND z`1 = a} projection_2(X):set[T2] = {b | EXISTS z: X(z) AND z`2 = b} cross_product_empty1: LEMMA empty?(A) => empty?(cross_product(A,B)) cross_product_empty2: LEMMA empty?(B) => empty?(cross_product(A,B)) cross_product_emptyset1: LEMMA empty?(cross_product(emptyset[T1],B)) cross_product_emptyset2: LEMMA empty?(cross_product(A,emptyset[T2])) cross_product_fullset: LEMMA full?(cross_product(fullset[T1],fullset[T2])) projection_product1: LEMMA projection_1(cross_product(A,NB)) = A projection_product2: LEMMA projection_2(cross_product(NA,B)) = B projection_1_emptyset: LEMMA projection_1(emptyset[[T1,T2]]) = emptyset[T1] projection_2_emptyset: LEMMA projection_2(emptyset[[T1,T2]]) = emptyset[T2] projection_1_fullset: LEMMA (EXISTS b: TRUE) => projection_1(fullset[[T1,T2]]) = fullset[T1] projection_2_fullset: LEMMA (EXISTS a: TRUE) => projection_2(fullset[[T1,T2]]) = fullset[T2] cross_product_empty1_rew: LEMMA cross_product(emptyset[T1],B) = emptyset[[T1,T2]] cross_product_empty2_rew: LEMMA cross_product(A,emptyset[T2]) = emptyset[[T1,T2]] cross_product_full_rew: LEMMA cross_product(fullset[T1],fullset[T2]) = fullset[[T1,T2]] cross_product: TYPE+ = {X | EXISTS A,B: X = cross_product(A,B)} Y: VAR cross_product product_projection: LEMMA cross_product(projection_1(Y),projection_2(Y)) = Y x_section(X,a):set[T2] = {b | X(a,b)} % SKB 7.2.4 y_section(X,b):set[T1] = {a | X(a,b)} % SKB 7.2.6 x_section(X):[T1->set[T2]] = lambda a: x_section(X,a) y_section(X):[T2->set[T1]] = lambda b: y_section(X,b) END cross_product ¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
