Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: divergence.pvs Sprache: PVS

Original von: PVS^©

%
% Divergence
%

divergence[D:posreal] : THEORY
BEGIN

  IMPORTING horizontal,
       predicate_coordination_2D

  s       : VAR Vect2
  v,vo,vi,
  nv,nw   : VAR Vect2
  nvo,nvi : VAR Vect2
  eps   : VAR Sign

  divergence_crit?: Criterion_2D = (LAMBDA (s,v,eps): (LAMBDA (nv): s*nv > 0))

  divergence_pred?: Vector_Predicate_2D = (LAMBDA (s,v): (LAMBDA (nv): NOT divergent?(s,nv)))

  divergence_crit_oriented: LEMMA symmetric_oriented_2D?(divergence_crit?)

  divergence_crit_sum_indep: LEMMA sum_independent_2D?(divergence_crit?, divergence_pred?)

  divergence_pred_sum_closed: LEMMA sum_closed_2D?(divergence_pred?)

  divergence_crit_coordinated: LEMMA coordinated_oriented_2D?(divergence_crit?,divergence_pred?)

  divergence_crit_coordinated2: LEMMA
        NOT divergent?(s, zero, vo - vi, zero) AND
        divergence_crit?(s, vo - vi, eps)(nvo - vi) AND
        divergence_crit?(-s, vi - vo, eps)(nvi - vo)
        IMPLIES
divergent?(s, zero, nvo - nvi, zero)

END divergence

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.