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

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: xz.scala   Sprache: PVS

Untersuchung PVS©
reals_complete_more[T: TYPE FROM real]: THEORY
BEGIN

  IMPORTING  bound_defs[real,T]

  real_complete2: LEMMA   % this could replace real_complete in prelude
    (FORALL (S: (nonempty?[T])):
      (EXISTS (y: real): upper_bound(<=)(y, S)) IMPLIES
        (EXISTS (x: real): least_upper_bound(<=)(x, S)))

  real_lower_complete2: LEMMA % this could replace real_complete in prelude
    (FORALL (S: (nonempty?[T])):
      (EXISTS (y : real): lower_bound(<=)(y, S)) IMPLIES 
        (EXISTS (x: real): greatest_lower_bound(<=)(x, S)))


END reals_complete_more



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



Kontakt
Drucken
Kontakt
Hier finden Sie eine Liste der Produkte des Unternehmens

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff