Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: sigma_countable.prf   Sprache: Lisp

deriv_domain_def[T : TYPE FROM real]: THEORY
BEGIN

   deriv_domain?: bool = FORALL (e: posreal, x:T):
                                  EXISTS (y: {u: nzreal | T_pred(u + x)}): abs(y) < e

   not_one_element?: bool = (FORALL (x: T): EXISTS (y: T): x /= y)

   connected?: bool =   FORALL (x, y : T), (z : real): x <= z AND z <= y IMPLIES T_pred[T](z)


   connected_deriv_domain: LEMMA connected? AND not_one_element?
                            IMPLIES deriv_domain?

   del_neigh_all?: bool = FORALL (a: T): EXISTS (del: posreal): FORALL (xx:real):
                            abs(xx-a) < del IMPLIES T_pred[T](xx)


%  The following lemma shows that our derivative domain is more general than just
%  having a delta neighborhood around every point.

   del_neigh_all_lem : LEMMA del_neigh_all? IMPLIES deriv_domain?


END deriv_domain_def

[ Seitenstruktur0.0Drucken  etwas mehr zur Ethik  ]

                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik