| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/exact_real_arith/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle unique.pvs Sprache: PVS |
|||||||||
|
unique: THEORY
BEGIN IMPORTING prelude_aux IMPORTING cauchy IMPORTING neg IMPORTING add p,s: VAR nat x,y: VAR real cx: VAR cauchy_real nzcx: VAR cauchy_nzreal nncx: VAR cauchy_nnreal npcx: VAR cauchy_npreal ncx: VAR cauchy_negreal pcx: VAR cauchy_posreal px: VAR posreal nzx: VAR nzreal f: VAR [nzreal->nzreal] cf: VAR [cauchy_nzreal->cauchy_nzreal] unique_cauchy: LEMMA cauchy_prop(x,cx) AND cauchy_prop(y,cx) => x = y cauchy_dich1: LEMMA cauchy_posreal?(nzcx) IFF NOT cauchy_negreal?(nzcx) cauchy_dich2: LEMMA cauchy_negreal?(nzcx) IFF NOT cauchy_posreal?(nzcx) cauchy_dich3: LEMMA cauchy_nnreal?(nncx) IFF NOT cauchy_negreal?(nncx) cauchy_dich4: LEMMA cauchy_npreal?(npcx) IFF NOT cauchy_posreal?(npcx) cauchy_dich5: LEMMA cauchy_negreal?(nzcx) OR cauchy_posreal?(nzcx) cauchy_trich: LEMMA cauchy_negreal?(cx) OR cx = cauchy_zero OR cauchy_posreal?(cx) cauchy_pos_characteristic: LEMMA 0 <= pcx(p) cauchy_neg_characteristic: LEMMA ncx(p) <= 0 cauchy_pos_monotonic: LEMMA 3 <= pcx(s) => 3 <= pcx(s+p) cauchy_monotonic: LEMMA 3 <= abs(nzcx(s)) => 3 <= abs(nzcx(s+p)) odd_real_fn?(f:[nzreal->nzreal]):bool = FORALL (x:nzreal): (f(-x) = -f(x)) odd_cauchy_fn?(cf:[cauchy_nzreal->cauchy_nzreal]):bool = FORALL (cx:cauchy_nzreal):(cf(cauchy_neg(cx)) = cauchy_neg(cf(cx))) cauchy_odd_extend: LEMMA odd_real_fn?(f) AND odd_cauchy_fn?(cf) AND (FORALL (px:posreal, pcx:cauchy_posreal): cauchy_prop(px,pcx) => cauchy_prop(f(px),cf(pcx))) => (cauchy_prop(nzx,nzcx) => cauchy_prop(f(nzx),cf(nzcx))) END unique ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28