| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/interval_arith/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 828 B |
|
Quelle interval_sqrt.pvs Sprache: PVS |
|||||||||
|
%% interval_sqrt.pvs
interval_sqrt : THEORY BEGIN IMPORTING interval, reals@sqrt_approx X,Y : VAR Interval x,y : VAR real n : VAR nat % Sqrt Sqrt(n)(X) : (NonNeg?) = IF Ge(X,0) THEN [|sqrt_lb(lb(X),n),sqrt_ub(ub(X),n)|] ELSE EmptyInterval endif Sqrt_inclusion : LEMMA NonNeg?(X) AND x ## X IMPLIES sqrt(x) ## Sqrt(n)(X) Sqrt_fundamental : LEMMA NonNeg?(Y) AND Proper?(X) AND X << Y IMPLIES Sqrt(n)(X) << Sqrt(n)(Y) % Safe version of Sqrt IMPORTING safe_arith safe_Sqrt(n) : [Interval->Interval] = Safe1(NonNeg?,Sqrt(n)) % Proper version of Sqrt IMPORTING proper_arith XNn : VAR NonNegInterval Proper_Sqrt : JUDGEMENT Sqrt(n)(XNn) HAS_TYPE NonNegInterval proper_Sqrt(n)(XNn): ProperInterval = Sqrt(n)(XNn) END interval_sqrt ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28