products/sources/formale Sprachen/PVS/TRS/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: acosx.pvs   Sprache: Unknown

%------------------------------------------------------------------------------
% Arcosine
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            18/2/09   Initial Release Version
%------------------------------------------------------------------------------

acosx: THEORY

BEGIN

  IMPORTING asinx, trig_fnd@acos

  x:  VAR real_abs_le1
  cx: VAR cauchy_real_abs_le1

  cauchy_acos(cx):cauchy_real
    = cauchy_sub(cauchy_div2n(cauchy_pi, 1), cauchy_asin(cx))

  acos_lemma: LEMMA cauchy_prop(x,cx) IMPLIES
                                          cauchy_prop(acos(x),cauchy_acos(cx))

END acosx

[ Verzeichnis aufwärts0.2unsichere Verbindung  Übersetzung europäischer Sprachen durch Browser  ]