| products/Sources/formale Sprachen/PVS/analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: deriv_domain.pvs Sprache: PVSOriginal von: PVS© |
|
||||||
|
deriv_domain: THEORY
BEGIN a,b: VAR real IMPORTING deriv_domain_def deriv_domain_real : LEMMA deriv_domain?[real] deriv_domain_nzreal : LEMMA deriv_domain?[nzreal] deriv_domain_posreal: LEMMA deriv_domain?[posreal] deriv_domain_nnreal : LEMMA deriv_domain?[nnreal] deriv_domain_negreal: LEMMA deriv_domain?[negreal] IMPORTING reals@intervals_real deriv_domain_open : LEMMA deriv_domain?[open_interval(a,b)] deriv_domain_closed : LEMMA a /= b IMPLIES deriv_domain?[closed_interval(a,b)] deriv_domain_oc : LEMMA deriv_domain?[{x: real | a < x AND x <= b}] deriv_domain_co : LEMMA deriv_domain?[{x: real | a <= x AND x < b}] deriv_domain_posreal_le: LEMMA deriv_domain?[{x: posreal | x <= a}] deriv_domain_posreal_lt: LEMMA deriv_domain?[{x: posreal | x < a}] deriv_domain_nnreal_lt : LEMMA deriv_domain?[{x: nnreal | x < a}] % ------- Not One Element Lemmas not_one_element_real : LEMMA not_one_element?[real] not_one_element_nzreal : LEMMA not_one_element?[nzreal] not_one_element_posreal: LEMMA not_one_element?[posreal] not_one_element_nnreal : LEMMA not_one_element?[nnreal] not_one_element_negreal: LEMMA not_one_element?[negreal] % ------- Connected Lemmas connected_real : LEMMA connected?[real] connected_posreal: LEMMA connected?[posreal] connected_nnreal : LEMMA connected?[nnreal] connected_negreal: LEMMA not_one_element?[negreal] END deriv_domain ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
