products/sources/formale sprachen/VDM/VDMPP/AutomatedStockBrokerPP/lib/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei:   Sprache: PVS

Original von: PVS©
% various extras for the standard prelude

sets_lemmas_aux[T:TYPE]: THEORY

BEGIN

  x, y: VAR T
  a, b, c: VAR set[T]
  A, B : Var setofsets[T]

  IMPORTING sets_lemmas[T]

  union_complement:        LEMMA union(a,complement(a))        = fullset
  intersection_complement: LEMMA intersection(a,complement(a)) = emptyset
  disjoint_complement:     LEMMA disjoint?(a,complement(a))
  disjoint_commutative:    LEMMA disjoint?(a,b) = disjoint?(b,a)
  disjoint_empty:          LEMMA disjoint?(a,emptyset)
  powerset_fullset:        LEMMA member(a, powerset(a))
  union_diff_inter:        LEMMA union(difference(a,b),intersection(a,b)) = a
  disjoint_diff_inter:     LEMMA disjoint?(difference(a,b),intersection(a,b))
  disjoint_member:         LEMMA disjoint?(a,b) AND member(x,a) IMPLIES
                                                               NOT member(x,b)

END sets_lemmas_aux

¤ Dauer der Verarbeitung: 0.3 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff