| products/sources/formale Sprachen/PVS/Sturm/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: replacement.prf Sprache: PVSOriginal von: PVS© |
|
||||||
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Properties of real numbers % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% real_facts : THEORY BEGIN S: VAR (nonempty?[real]) bounded?_lem : LEMMA bounded?(S) IFF EXISTS (B: real): FORALL (x: (S)): abs(x) <= B %---------------------------------------- % More properties of archimedean field %---------------------------------------- archimedean2 : THEOREM FORALL (x : posreal) : EXISTS (a : posnat) : 1/a < x archimedean3 : THEOREM FORALL (x : nonneg_real) : (FORALL (a : posnat) : x <= 1/a) implies x = 0 %------------------------------------------------- % Every real is between two successive integers %------------------------------------------------- nat_interval : LEMMA FORALL (x : nonneg_real) : EXISTS (a : nat) : a <= x and x < a + 1 int_interval : LEMMA FORALL (x : real) : EXISTS (a : integer) : a <= x and x < a +1 %--------------------------------------- % Short cuts for lub and glb of sets %--------------------------------------- U: VAR (bounded_above?) V: VAR (bounded_below?) a,b,x, y: VAR real epsilon: VAR posreal lub_is_bound: LEMMA FORALL (x: (U)): x <= lub(U) lub_is_lub: LEMMA lub(U) <= y IFF FORALL (x: (U)): x <= y lub_closed_intv: LEMMA a < b IMPLIES lub({x | a <= x AND x <= b}) = b adherence_sup: LEMMA FORALL epsilon: EXISTS (x: (U)): lub(U) - epsilon < x glb_is_bound: LEMMA FORALL (x: (V)): glb(V) <= x glb_is_glb: LEMMA y <= glb(V) IFF FORALL (x: (V)): y <= x glb_closed_intv: LEMMA a < b IMPLIES glb({x | a <= x AND x <= b}) = a adherence_inf: LEMMA FORALL epsilon: EXISTS (x: (V)): x < glb(V) + epsilon END real_facts ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
