products/Sources/formale Sprachen/Isabelle/Tools/SML/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: inverse_image_Union.pvs   Sprache: Unknown

%------------------------------------------------------------------------------
% inverse_image_Union
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            14/06/09  Initial Version
%------------------------------------------------------------------------------
inverse_image_Union[S,T:TYPE]: THEORY

BEGIN

  f: VAR [S->T]
  y: VAR set[S]
  X: VAR setofsets[T]

  inverse_image_Union: LEMMA inverse_image(f,Union(X)) =
                             Union({y | EXISTS (x:(X)): y=inverse_image(f,x)})

END inverse_image_Union

[ Dauer der Verarbeitung: 0.0 Sekunden  (vorverarbeitet)  ]