| products/Sources/formale Sprachen/PVS/exact_real_arith/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: atanx.prf Sprache: PVSOriginal von: PVS© |
|
||||||
|
%------------------------------------------------------------------------------
% sec/cosec/cot % % Author: David Lester, Manchester University % % Version 1.0 18/2/09 Initial Release Version %------------------------------------------------------------------------------ trigx: THEORY BEGIN IMPORTING sincosx x: VAR real c: VAR [nat->int] sin_nz: TYPE+ = {x | sin(x) /= 0} CONTAINING pi/2 cos_nz: TYPE+ = {x | cos(x) /= 0} CONTAINING 0 nsx: VAR sin_nz ncx: VAR cos_nz cauchy_sin_nz?(c):bool = EXISTS nsx: cauchy_prop(nsx,c) cauchy_cos_nz?(c):bool = EXISTS ncx: cauchy_prop(ncx,c) cauchy_sin_nz: TYPE+ = (cauchy_sin_nz?) CONTAINING cauchy_div2n(cauchy_pi,1) cauchy_cos_nz: TYPE+ = (cauchy_cos_nz?) CONTAINING cauchy_zero JUDGEMENT cauchy_sin_nz SUBTYPE_OF cauchy_real JUDGEMENT cauchy_cos_nz SUBTYPE_OF cauchy_real cnsx: VAR cauchy_sin_nz cncx: VAR cauchy_cos_nz cauchy_sec(cncx): cauchy_nzreal = cauchy_inv(cauchy_cos(cncx)) cauchy_cosec(cnsx):cauchy_nzreal = cauchy_inv(cauchy_sin(cnsx)) cauchy_tan(cncx):cauchy_real = cauchy_div(cauchy_sin(cncx),cauchy_cos(cncx)) cauchy_cot(cnsx):cauchy_real = cauchy_div(cauchy_cos(cnsx),cauchy_sin(cnsx)) % The following should be in the trig/trig_fnd library ... sec(ncx): nzreal = 1/cos(ncx) cosec(nsx):nzreal = 1/sin(nsx) cot(nsx): real = cos(nsx)/sin(nsx) sec_lemma: LEMMA cauchy_prop(ncx,cncx) => cauchy_prop(sec(ncx),cauchy_sec(cncx)) cosec_lemma: LEMMA cauchy_prop(nsx,cnsx) => cauchy_prop(cosec(nsx),cauchy_cosec(cnsx)) tan_lemma: LEMMA cauchy_prop(ncx,cncx) => cauchy_prop(tan(ncx),cauchy_tan(cncx)) cot_lemma: LEMMA cauchy_prop(nsx,cnsx) => cauchy_prop(cot(nsx),cauchy_cot(cnsx)) END trigx ¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
