Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Thinking Intellekt

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/analysis_ax/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: csequence_insert_remove.pvs Sprache: PVS

Untersuchung PVS^©

continuous_functions_more [ T : TYPE FROM real ] : THEORY
%----------------------------------------------------------------------------
%
%  Additions made by Ricky W. Butler    NASA Langley
%
%----------------------------------------------------------------------------
BEGIN

   ASSUMING

     connected_domain : ASSUMPTION
FORALL (x, y : T), (z : real) :
     x <= z AND z <= y IMPLIES T_pred(z)

     not_one_element : ASSUMPTION
  FORALL (x : T) : EXISTS (y : T) : x /= y

   ENDASSUMING

  IMPORTING continuous_functions[T], convergence_sequences

  f: VAR [T -> real]
  a,b,c: VAR T
  cn: VAR sequence[T]
  n: VAR nat

  convergence_fun_of  : LEMMA convergence(cn,c) AND
                               continuous?(f,c) IMPLIES  % move to analysis
                                 convergence(LAMBDA n: f(cn(n)),f(c))


  IMPORTING unif_cont_fun   %% to maintain upward compatibility

END continuous_functions_more