|
%------------------------------------------------------------------------------
% Definition and properties of sqrt
%
% Author: David Lester, Manchester University
%
% Version 1.0 18/2/09 Initial Release Version
%------------------------------------------------------------------------------
prelude_sqrt: THEORY
BEGIN
IMPORTING prelude_aux
nnx,nny,nnz: VAR nnreal
px,py,pz: VAR posreal
y,w: VAR real
square_le1: LEMMA nnx*nnx <= (nnx+nny)*(nnx+nny)
square_le2: LEMMA nnx*nnx <= 1 <=> nnx <= 1
square_le3: LEMMA nnx*nnx < nny*nny <=> nnx < nny
square_eq1: LEMMA nnx*nnx = nny*nny <=> nnx = nny
square_le4: LEMMA nnx*nnx <= nny*nny <=> nnx <= nny
square_le5: LEMMA 1 < px*px <=> 1 < px
square_le6: LEMMA nnx*nnx <= py AND 1 < py => nnx < py
square_archimedean1: LEMMA EXISTS (n:posnat): 1/(n*n) < px
square_archimedean2: LEMMA EXISTS (n:posnat): 2/n + 1/(n*n) < px
square_exist_lt1: LEMMA py <= 1 AND py*py < px =>
EXISTS pz: py < pz AND pz*pz < px
square_exist_lt2: LEMMA EXISTS pz: pz*pz < px
square_exist_lt3: LEMMA nny*nny < px => EXISTS pz: nny < pz AND pz*pz < px
square_exist_gt3: LEMMA nnx < py*py =>
EXISTS nnz: nnz < py AND nnx < nnz*nnz
sqrt_set(nnx:nnreal):setof[nnreal] = {y | y*y <= nnx}
sqrt_set_UB(nnx:nnreal):nnreal = IF nnx <= 1 THEN 1 ELSE nnx ENDIF
sqrt_set_nonempty: LEMMA nonempty?(sqrt_set(nnx))
sqrt_set_has_UB: LEMMA upper_bound?(sqrt_set_UB(nnx),sqrt_set(nnx))
sqrt_set_LUB: LEMMA nny*nny = nnx <=> least_upper_bound?(nny,sqrt_set(nnx))
square(nnx:nnreal):nnreal = nnx*nnx
square_injective: LEMMA injective?(square)
square_surjective: LEMMA surjective?(square)
square_bijective: LEMMA bijective?(square)
sqrt:[nnreal->nnreal] = inverse(square)
square_is: LEMMA square(nnx) = nnx*nnx
sqrt_square1: LEMMA square(sqrt(nnx))=nnx
sqrt_square2: LEMMA sqrt(square(nnx))=nnx
square_times: LEMMA square(nnx*nny) = square(nnx)*square(nny)
sqrt_times: LEMMA sqrt(nnx)*sqrt(nny) = sqrt(nnx*nny)
sqrt_zero: LEMMA sqrt(0) = 0
sqrt_one: LEMMA sqrt(1) = 1
both_sides_sqrt1: LEMMA sqrt(nnx) = nny <=> nnx = nny*nny
both_sides_sqrt2: LEMMA sqrt(nnx) = sqrt(nny) <=> nnx = nny
both_sides_sqrt_lt1: LEMMA sqrt(nnx) < nny <=> nnx < nny*nny
both_sides_sqrt_lt2: LEMMA sqrt(nnx) < sqrt(nny) <=> nnx < nny
both_sides_sqrt_lt3: LEMMA nnx < sqrt(nny) <=> nnx*nnx < nny
both_sides_sqrt_le1: LEMMA sqrt(nnx) <= nny <=> nnx <= nny*nny
both_sides_sqrt_le2: LEMMA sqrt(nnx) <= sqrt(nny) <=> nnx <= nny
both_sides_sqrt_le3: LEMMA nnx <= sqrt(nny) <=> nnx*nnx <= nny
END prelude_sqrt
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.19Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
