Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 1 kB

Quelle epsilon_lemmas.pvs Sprache: PVS

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Lemmas used for limits of product and inverse
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

epsilon_lemmas : THEORY
BEGIN

  x1, x2, y1, y2 : VAR real
  e, e1, e2 : VAR posreal

  IMPORTING reals@real_facts, reals@abs_lems

  %--- Lemmas for product ---%

  prod_bound : LEMMA
abs(x1 - y1) < e1 AND abs(x2 - y2) < e2 IMPLIES
abs(x1 * x2 - y1 * y2) < e1 * e2 + abs(y1) * e2 + abs(y2) * e1

  prod_epsilon : LEMMA
EXISTS e1, e2 : e1 * e2 + abs(y1) * e2 + abs(y2) * e1 < e

  %--- Lemmas for inverse ---%

  inv_bound : LEMMA
abs(x1 - y1) < e1 and e1 < abs(y1) and x1 /= 0 and y1 /= 0
IMPLIES abs(1/x1 - 1/y1) < e1 / (abs(y1) * (abs(y1) - e1))

  inv_epsilon1 : LEMMA
y1 /= 0 IMPLIES
    EXISTS e1 : e1 < abs(y1) and e1 < e * (abs(y1) - e1)

  inv_epsilon : LEMMA
y1 /= 0  IMPLIES
    EXISTS e1 : e1 < abs(y1)
     and e1 / (abs(y1) * (abs(y1) - e1)) < e

% Proof "By varying epsilon"
%
% A technique to get the inequalities to run the "wrong way" for
% epsilon. Can be used to give yourself a small extra quantity to play with
% in analysis proofs.
%

  epsilon: VAR posreal
  x,y:     VAR real

  varying_epsilon: LEMMA x <= y <=> (FORALL epsilon: x <= y + epsilon)

END epsilon_lemmas

quality93%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.