Quelle real_order_ep.pvs Sprache: PVS

real_order_ep: THEORY

BEGIN

  x,y:VAR real
  epsil:VAR posreal

  real_ord_ep(epsil)(x,y): bool =
    floor(abs(x)/epsil) < floor(abs(y)/epsil)

  real_ord_ep_well_founded: JUDGEMENT
    real_ord_ep(epsil) has_type (well_founded?[real])

  real_ord_ep_decreases_halves: LEMMA
    abs(x)>=epsil IMPLIES
    real_ord_ep(epsil)(x/2,x)

END real_order_ep

quality100%

¤ Dauer der Verarbeitung: 0.8 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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.