products/sources/formale Sprachen/PVS/orders/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: ml_system.ML   Sprache: PVS

Untersuchung PVS©
%-------------------------------------------------------------------------
%
%  If there are injective (surjective) maps both ways between two sets,
%  then the sets are bijective.
%
%  For PVS version 3.2.  January 18, 2005
%  ---------------------------------------------------------------------
%      Author: Jerry James ([email protected]), University of Kansas
%
%  EXPORTS
%  -------
%  orders: set_antisymmetric[D, R]
%
%-------------------------------------------------------------------------
set_antisymmetric[D: TYPE, R: TYPE]: THEORY
 BEGIN

  in_closure(f: [D -> R], g: [R -> D], d: D): INDUCTIVE bool =
    member(d, complement(image(g, fullset[R]))) OR
    (EXISTS (e: D): g(f(e)) = d AND in_closure(f, g, e))

  % The Schroeder-Bernstein Theorem
  inj_inj_bij: THEOREM
    (EXISTS (f: [D -> R]): injective?(f)) AND
     (EXISTS (f: [R -> D]): injective?(f))
     => (EXISTS (f: [D -> R]): bijective?(f))

  surj_surj_bij: COROLLARY
    (EXISTS (f: [D -> R]): surjective?(f)) AND
     (EXISTS (f: [R -> D]): surjective?(f))
     => (EXISTS (f: [D -> R]): bijective?(f))

  inj_surj_bij: COROLLARY
    (EXISTS (f: [D -> R]): injective?(f)) AND
     (EXISTS (f: [D -> R]): surjective?(f))
     => (EXISTS (f: [D -> R]): bijective?(f))

 END set_antisymmetric

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.16Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff